SMV: make ASSIGN typed

Given ASSIGN lhs := rhs, require rhs to have a type no larger than the type of lhs.

This enables better error messages.

Author: kroening

regression/smv/expressions/smv_if2.desc

@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 smv_if2.smv
 
+^\[.*\] X \(b = 2 \| b = 4\): PROVED up to bound 5$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This yields a type error.

regression/smv/expressions/smv_if2.smv

@@ -6,3 +6,5 @@ VAR b : 1..4;
 
 ASSIGN init(b) := 1;
 ASSIGN next(b) := (input ? 1 : 3) + 1;
+
+LTLSPEC X (b = 2 | b = 4)

regression/smv/range-type/range_type5.desc

@@ -1,8 +1,8 @@
 CORE broken-smt-backend
 range_type5.smv
 --bound 3
-^EXIT=0$
+^file .* line 14: Expected expression of type `5..10', but got expression `x', which is of type `0..6'$
+^EXIT=2$
 ^SIGNAL=0$
-^\[spec1\] AG \(!x = 6\): PROVED up to bound 3$
 --
 ^warning: ignoring

src/smvlang/smv_parse_tree.h

@@ -113,7 +113,15 @@ class smv_parse_treet
       }
 
       // for ASSIGN_CURRENT, ASSIGN_INIT, ASSIGN_NEXT, DEFINE
-      const equal_exprt &equal_expr()
+      const equal_exprt &equal_expr() const
+      {
+        PRECONDITION(
+          is_assign_current() || is_assign_init() || is_assign_next() ||
+          is_define());
+        return to_equal_expr(expr);
+      }
+
+      equal_exprt &equal_expr()
       {
         PRECONDITION(
           is_assign_current() || is_assign_init() || is_assign_next() ||

src/smvlang/smv_typecheck.cpp

@@ -1257,47 +1257,57 @@ Function: smv_typecheckt::typecheck
 void smv_typecheckt::typecheck(
   smv_parse_treet::modulet::itemt &item)
 {
-  modet mode;
-
   switch(item.item_type)
   {
-  case smv_parse_treet::modulet::itemt::ASSIGN_CURRENT:
-    mode = OTHER;
-    break;
-
-  case smv_parse_treet::modulet::itemt::ASSIGN_INIT:
-    mode = INIT;
-    break;
-
-  case smv_parse_treet::modulet::itemt::ASSIGN_NEXT:
-    mode = TRANS;
-    break;
-
   case smv_parse_treet::modulet::itemt::INIT:
-    mode=INIT;
-    break;
+    typecheck(item.expr, INIT);
+    convert_expr_to(item.expr, bool_typet{});
+    return;
 
   case smv_parse_treet::modulet::itemt::TRANS:
-    mode=TRANS;
-    break;
+    typecheck(item.expr, TRANS);
+    convert_expr_to(item.expr, bool_typet{});
+    return;
 
   case smv_parse_treet::modulet::itemt::CTLSPEC:
-    mode = CTL;
-    break;
+    typecheck(item.expr, CTL);
+    convert_expr_to(item.expr, bool_typet{});
+    return;
 
   case smv_parse_treet::modulet::itemt::LTLSPEC:
-    mode = LTL;
-    break;
+    typecheck(item.expr, LTL);
+    convert_expr_to(item.expr, bool_typet{});
+    return;
 
-  case smv_parse_treet::modulet::itemt::DEFINE:
   case smv_parse_treet::modulet::itemt::INVAR:
   case smv_parse_treet::modulet::itemt::FAIRNESS:
-  default:
-    mode=OTHER;
-  }
+    typecheck(item.expr, OTHER);
+    convert_expr_to(item.expr, bool_typet{});
+    return;
+
+  case smv_parse_treet::modulet::itemt::ASSIGN_CURRENT:
+    typecheck(item.equal_expr().lhs(), OTHER);
+    typecheck(item.equal_expr().rhs(), item.equal_expr().lhs().type(), OTHER);
+    item.equal_expr().type() = bool_typet{};
+    return;
+
+  case smv_parse_treet::modulet::itemt::ASSIGN_INIT:
+    typecheck(item.equal_expr().lhs(), INIT);
+    typecheck(item.equal_expr().rhs(), item.equal_expr().lhs().type(), INIT);
+    item.equal_expr().type() = bool_typet{};
+    return;
 
-  typecheck(item.expr, mode);
-  convert_expr_to(item.expr, bool_typet{});
+  case smv_parse_treet::modulet::itemt::ASSIGN_NEXT:
+    typecheck(item.equal_expr().lhs(), TRANS);
+    typecheck(item.equal_expr().rhs(), item.equal_expr().lhs().type(), TRANS);
+    item.equal_expr().type() = bool_typet{};
+    return;
+
+  case smv_parse_treet::modulet::itemt::DEFINE:
+    typecheck(item.expr, OTHER);
+    item.equal_expr().type() = bool_typet{};
+    return;
+  }
 }
 
 /*******************************************************************\