From f4e2663e949e5ae23e97ba646ea98c0c1edc3ef2 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 20 Feb 2025 18:20:34 +0000
Subject: [PATCH] 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.
---
 regression/smv/expressions/smv_if2.desc    |  4 +-
 regression/smv/expressions/smv_if2.smv     |  2 +
 regression/smv/range-type/range_type5.desc |  4 +-
 src/smvlang/smv_parse_tree.h               | 10 +++-
 src/smvlang/smv_typecheck.cpp              | 66 +++++++++++++---------
 5 files changed, 53 insertions(+), 33 deletions(-)

diff --git a/regression/smv/expressions/smv_if2.desc b/regression/smv/expressions/smv_if2.desc
index dceb2b55f..4f7cbafab 100644
--- a/regression/smv/expressions/smv_if2.desc
+++ b/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.
diff --git a/regression/smv/expressions/smv_if2.smv b/regression/smv/expressions/smv_if2.smv
index 92a61c882..ac808a23d 100644
--- a/regression/smv/expressions/smv_if2.smv
+++ b/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)
diff --git a/regression/smv/range-type/range_type5.desc b/regression/smv/range-type/range_type5.desc
index c49089296..7bf5b33dc 100644
--- a/regression/smv/range-type/range_type5.desc
+++ b/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
diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h
index 2377d0477..e80d255df 100644
--- a/src/smvlang/smv_parse_tree.h
+++ b/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() ||
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 371ef9a80..e194515ea 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/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;
+  }
 }
 
 /*******************************************************************\