SMV: add a lowering pass

We currently expect that our solver backends support all expressions
generated by the SMV-front-end as-is.

To avoid introducing additional, redundant expressions, this adds a lowering
pass to the SMV type checker.

The lowering pass lowers SMV extend, resize, signed, and unsigned
expressions to typecast expressions.

Author: kroening

regression/smv/word/extend1.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 extend1.smv
 
+^\[p0\] extend\(0ud1_1, 7\) = 0ud8_1: PROVED$
+^\[p1\] extend\(-0sd1_1, 7\) = -0sd8_1: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/word/extend1.smv

@@ -1,4 +1,4 @@
 MODULE main
 
-SPEC extend(uwconst(1, 1), 7) = uwconst(1, 8)
-SPEC extend(swconst(-1, 1), 7) = swconst(-1, 8)
+SPEC NAME p0 := extend(uwconst(1, 1), 7) = uwconst(1, 8)
+SPEC NAME p1 := extend(swconst(-1, 1), 7) = swconst(-1, 8)

regression/smv/word/resize1.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 resize1.smv
 
+^\[p0\] resize\(0ud1_1, 8\) = 0ud8_1: PROVED$
+^\[p1\] resize\(-0sd1_1, 1\) = -0sd1_1: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/word/resize1.smv

@@ -1,4 +1,4 @@
 MODULE main
 
-SPEC resize(uwconst(1, 1), 8) = uwconst(1, 8)
-SPEC resize(swconst(123, 1), 1) = swconst(-1, 1)
+SPEC NAME p0 := resize(uwconst(1, 1), 8) = uwconst(1, 8)
+SPEC NAME p1 := resize(swconst(123, 1), 1) = swconst(-1, 1)

regression/smv/word/signed1.desc

@@ -1,6 +1,7 @@
-KNOWNBUG
+CORE
 signed1.smv
 
+^\[p0\] signed\(0ud1_1\) = -0sd1_1: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/word/signed1.smv

@@ -1,3 +1,3 @@
 MODULE main
 
-SPEC signed(uwconst(1, 1)) = swconst(-1, 1)
+SPEC NAME p0 := signed(uwconst(1, 1)) = swconst(-1, 1)

regression/smv/word/unsigned1.desc

@@ -1,6 +1,7 @@
-KNOWNBUG
+CORE
 unsigned1.smv
 
+^\[p0\] unsigned\(-0sd1_1\) = 0ud1_1: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/word/unsigned1.smv

@@ -1,3 +1,3 @@
 MODULE main
 
-SPEC unsigned(swconst(-1, 1)) = uwconst(1, 1)
+SPEC NAME p0 := unsigned(swconst(-1, 1)) = uwconst(1, 1)

src/smvlang/expr2smv.cpp

@@ -124,6 +124,43 @@ expr2smvt::resultt expr2smvt::convert_binary(
 
 /*******************************************************************\
 
+Function: expr2smvt::convert_function_application
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2smvt::resultt expr2smvt::convert_function_application(
+  const std::string &symbol,
+  const exprt &src)
+{
+  bool first = true;
+
+  std::string dest = symbol + '(';
+
+  for(auto &op : src.operands())
+  {
+    if(first)
+      first = false;
+    else
+    {
+      dest += ',';
+      dest += ' ';
+    }
+
+    auto op_rec = convert_rec(op);
+    dest += op_rec.s;
+  }
+
+  return {precedencet::MAX, dest + ')'};
+}
+
+/*******************************************************************\
+
 Function: expr2smvt::convert_rtctl
 
   Inputs:
@@ -584,6 +621,18 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
     return convert_binary(to_binary_expr(src), ">>", precedencet::SHIFT);
   }
 
+  else if(src.id() == ID_smv_extend)
+    return convert_function_application("extend", src);
+
+  else if(src.id() == ID_smv_resize)
+    return convert_function_application("resize", src);
+
+  else if(src.id() == ID_smv_signed_cast)
+    return convert_function_application("signed", src);
+
+  else if(src.id() == ID_smv_unsigned_cast)
+    return convert_function_application("unsigned", src);
+
   else if(src.id() == ID_typecast)
   {
     return convert_rec(to_typecast_expr(src).op());

src/smvlang/expr2smv_class.h

@@ -116,6 +116,9 @@ class expr2smvt
 
   resultt convert_cond(const exprt &);
 
+  resultt
+  convert_function_application(const std::string &symbol, const exprt &);
+
   resultt convert_norep(const exprt &);
 };
 

src/smvlang/smv_typecheck.cpp

@@ -137,6 +137,13 @@ class smv_typecheckt:public typecheckt
     else
       return id;
   }
+
+  void lower_node(exprt &) const;
+
+  void lower(exprt &expr) const
+  {
+    expr.visit_post([this](exprt &expr) { lower_node(expr); });
+  }
 };
 
 /*******************************************************************\
@@ -1227,6 +1234,40 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
 
 /*******************************************************************\
 
+Function: smv_typecheckt::lower_node
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::lower_node(exprt &expr) const
+{
+  if(expr.id() == ID_smv_extend)
+  {
+    auto &binary = to_binary_expr(expr);
+    expr = typecast_exprt{binary.lhs(), expr.type()};
+  }
+  else if(expr.id() == ID_smv_resize)
+  {
+    auto &binary = to_binary_expr(expr);
+    expr = typecast_exprt{binary.lhs(), expr.type()};
+  }
+  else if(expr.id() == ID_smv_signed_cast)
+  {
+    expr = typecast_exprt{to_unary_expr(expr).op(), expr.type()};
+  }
+  else if(expr.id() == ID_smv_unsigned_cast)
+  {
+    expr = typecast_exprt{to_unary_expr(expr).op(), expr.type()};
+  }
+}
+
+/*******************************************************************\
+
 Function: smv_typecheckt::convert_expr_to
 
   Inputs:
@@ -1814,6 +1855,9 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
         transt{ID_trans, conjunction(trans_invar), conjunction(trans_init),
                conjunction(trans_trans), module_symbol.type};
 
+    // lowering
+    lower(module_symbol.value);
+
     module_symbol.pretty_name = strip_smv_prefix(module_symbol.name);
 
     symbol_table.add(module_symbol);
@@ -1851,6 +1895,9 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
         else
           spec_symbol.pretty_name = strip_smv_prefix(spec_symbol.name);
 
+        // lowering
+        lower(spec_symbol.value);
+
         symbol_table.add(spec_symbol);
       }
     }