SMV: clean up parse tree

This replaces the mechanism used for parsing an SMV expression.

Assignments are now stored explicitly in the parse tree.

Author: kroening

src/hw_cbmc_irep_ids.h

@@ -17,8 +17,11 @@ IREP_ID_ONE(F)
 IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
-IREP_ID_ONE(smv_next)
 IREP_ID_ONE(smv_iff)
+IREP_ID_ONE(smv_assign_current)
+IREP_ID_ONE(smv_assign_init)
+IREP_ID_ONE(smv_assign_next)
+IREP_ID_ONE(smv_next)
 IREP_ID_TWO(C_smv_iff, "#smv_iff")
 IREP_ID_ONE(smv_setin)
 IREP_ID_ONE(smv_setnotin)

src/smvlang/parser.y

@@ -468,8 +468,8 @@ assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
 assignment_var: variable_name
            ;
 
-assignment_head: init_Token { init($$, ID_init); }
-               | NEXT_Token { init($$, ID_smv_next); }
+assignment_head: init_Token { init($$, ID_smv_assign_init); }
+               | NEXT_Token { init($$, ID_smv_assign_next); }
                ;
 
 defines:     define

src/smvlang/smv_parse_tree.h

@@ -106,7 +106,7 @@ class smv_parse_treet
       }
 
       // for ASSIGN_CURRENT, ASSIGN_INIT, ASSIGN_NEXT, DEFINE
-      const equal_exprt &equal_expr()
+      equal_exprt &equal_expr()
       {
         PRECONDITION(
           is_assign_current() || is_assign_init() || is_assign_next() ||
@@ -223,7 +223,7 @@ class smv_parse_treet
   typedef std::unordered_map<irep_idt, modulet, irep_id_hash> modulest;
 
   modulest modules;
-  
+
   void swap(smv_parse_treet &smv_parse_tree);
   void clear();
 };

src/smvlang/smv_typecheck.cpp

@@ -1167,46 +1167,60 @@ 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;
+  {
+    auto &equal_expr = item.equal_expr();
+    auto &symbol_expr = to_symbol_expr(equal_expr.lhs());
+    auto &nil_type = static_cast<const typet &>(get_nil_irep());
+    typecheck(symbol_expr, nil_type, OTHER);
+    typecheck(equal_expr.rhs(), symbol_expr.type(), OTHER);
+  }
     break;
 
   case smv_parse_treet::modulet::itemt::ASSIGN_INIT:
-    mode = INIT;
+  {
+    auto &equal_expr = item.equal_expr();
+    auto &symbol_expr = to_symbol_expr(to_unary_expr(equal_expr.lhs()).op());
+    auto &nil_type = static_cast<const typet &>(get_nil_irep());
+    typecheck(symbol_expr, nil_type, OTHER);
+    typecheck(equal_expr.rhs(), symbol_expr.type(), INIT);
+  }
     break;
 
   case smv_parse_treet::modulet::itemt::ASSIGN_NEXT:
-    mode = TRANS;
+  {
+    auto &equal_expr = item.equal_expr();
+    auto &symbol_expr = to_symbol_expr(to_unary_expr(equal_expr.lhs()).op());
+    auto &nil_type = static_cast<const typet &>(get_nil_irep());
+    typecheck(symbol_expr, nil_type, OTHER);
+    typecheck(equal_expr.rhs(), symbol_expr.type(), TRANS);
+  }
     break;
 
   case smv_parse_treet::modulet::itemt::INIT:
-    mode=INIT;
+    typecheck(item.expr, bool_typet(), INIT);
     break;
 
   case smv_parse_treet::modulet::itemt::TRANS:
-    mode=TRANS;
+    typecheck(item.expr, bool_typet(), TRANS);
     break;
 
   case smv_parse_treet::modulet::itemt::CTLSPEC:
-    mode = CTL;
+    typecheck(item.expr, bool_typet(), CTL);
     break;
 
   case smv_parse_treet::modulet::itemt::LTLSPEC:
-    mode = LTL;
+    typecheck(item.expr, bool_typet(), LTL);
     break;
 
   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, bool_typet(), OTHER);
   }
-
-  typecheck(item.expr, bool_typet(), mode);
 }
 
 /*******************************************************************\