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 expressions to typecast expressions.

Author: kroening

regression/smv/word/extend1.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 extend1.smv
 
+^\[p0\] 0ud1_1 = 0ud8_1: PROVED$
+^\[p1\] -0sd1_1 = -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)

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,11 @@ 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_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,12 @@ 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 +1233,27 @@ 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()};
+  }
+}
+
+/*******************************************************************\
+
 Function: smv_typecheckt::convert_expr_to
 
   Inputs:
@@ -1497,53 +1524,62 @@ void smv_typecheckt::typecheck(
   case smv_parse_treet::modulet::itemt::INIT:
     typecheck(item.expr, INIT);
     convert_expr_to(item.expr, bool_typet{});
+    lower(item.expr);
     return;
 
   case smv_parse_treet::modulet::itemt::TRANS:
     typecheck(item.expr, TRANS);
     convert_expr_to(item.expr, bool_typet{});
+    lower(item.expr);
     return;
 
   case smv_parse_treet::modulet::itemt::CTLSPEC:
     typecheck(item.expr, CTL);
     convert_expr_to(item.expr, bool_typet{});
+    lower(item.expr);
     return;
 
   case smv_parse_treet::modulet::itemt::LTLSPEC:
     typecheck(item.expr, LTL);
     convert_expr_to(item.expr, bool_typet{});
+    lower(item.expr);
     return;
 
   case smv_parse_treet::modulet::itemt::INVAR:
   case smv_parse_treet::modulet::itemt::FAIRNESS:
     typecheck(item.expr, OTHER);
     convert_expr_to(item.expr, bool_typet{});
+    lower(item.expr);
     return;
 
   case smv_parse_treet::modulet::itemt::ASSIGN_CURRENT:
     typecheck(item.equal_expr().lhs(), OTHER);
     typecheck(item.equal_expr().rhs(), OTHER);
     convert_expr_to(item.equal_expr().rhs(), item.equal_expr().lhs().type());
     item.equal_expr().type() = bool_typet{};
+    lower(item.expr);
     return;
 
   case smv_parse_treet::modulet::itemt::ASSIGN_INIT:
     typecheck(item.equal_expr().lhs(), INIT);
     typecheck(item.equal_expr().rhs(), INIT);
     convert_expr_to(item.equal_expr().rhs(), item.equal_expr().lhs().type());
     item.equal_expr().type() = bool_typet{};
+    lower(item.expr);
     return;
 
   case smv_parse_treet::modulet::itemt::ASSIGN_NEXT:
     typecheck(item.equal_expr().lhs(), TRANS);
     typecheck(item.equal_expr().rhs(), TRANS);
     convert_expr_to(item.equal_expr().rhs(), item.equal_expr().lhs().type());
     item.equal_expr().type() = bool_typet{};
+    lower(item.expr);
     return;
 
   case smv_parse_treet::modulet::itemt::DEFINE:
     typecheck(item.expr, OTHER);
     item.equal_expr().type() = bool_typet{};
+    lower(item.expr);
     return;
   }
 }