SMV: variable definitions are now parse tree items

Instead of using a separate data structure, variable definitions are now
items in the parse tree like all other syntactic elements.

Author: kroening

src/smvlang/parser.y

@@ -594,7 +594,7 @@ vardecl    : variable_identifier ':' type_specifier ';'
              switch(var.var_class)
              {
              case smv_parse_treet::mc_vart::UNKNOWN:
-               var.type=(typet &)stack_expr($3);
+               var.type=stack_type($3);
                var.var_class=smv_parse_treet::mc_vart::DECLARED;
                break;
 
@@ -616,6 +616,8 @@ vardecl    : variable_identifier ':' type_specifier ';'
              default:
                DATA_INVARIANT(false, "unexpected variable class");
              }
+
+             PARSER.module->add_var(stack_expr($1), stack_type($3));
            }
            ;
 

src/smvlang/smv_parse_tree.cpp

@@ -72,8 +72,10 @@ std::string to_string(smv_parse_treet::modulet::itemt::item_typet i)
   case smv_parse_treet::modulet::itemt::LTLSPEC:
     return "LTLSPEC";
   case smv_parse_treet::modulet::itemt::FAIRNESS: return "FAIRNESS";
-  case smv_parse_treet::modulet::itemt::DEFINE:    return "DEFINE";  
-  
+  case smv_parse_treet::modulet::itemt::DEFINE:    return "DEFINE";
+  case smv_parse_treet::modulet::itemt::VAR:
+    return "VAR";
+
   default:;
   }
 

src/smvlang/smv_parse_tree.h

@@ -46,12 +46,13 @@ class smv_parse_treet
         ASSIGN_INIT,
         ASSIGN_NEXT,
         CTLSPEC,
-        LTLSPEC,
-        INIT,
-        TRANS,
         DEFINE,
+        FAIRNESS,
+        INIT,
         INVAR,
-        FAIRNESS
+        LTLSPEC,
+        TRANS,
+        VAR
       };
 
       itemt(item_typet __item_type, exprt __expr, source_locationt __location)
@@ -125,6 +126,11 @@ class smv_parse_treet
         return item_type==INIT;
       }
 
+      bool is_var() const
+      {
+        return item_type == VAR;
+      }
+
       // for ASSIGN_CURRENT, ASSIGN_INIT, ASSIGN_NEXT, DEFINE
       const equal_exprt &equal_expr() const
       {
@@ -246,7 +252,14 @@ class smv_parse_treet
     {
       items.emplace_back(itemt::TRANS, std::move(expr), std::move(location));
     }
-    
+
+    void add_var(exprt expr, typet type)
+    {
+      expr.type() = std::move(type);
+      auto location = expr.source_location();
+      items.emplace_back(itemt::VAR, std::move(expr), std::move(location));
+    }
+
     mc_varst vars;
     enum_sett enum_set;
 

src/smvlang/smv_typecheck.cpp

@@ -1893,6 +1893,9 @@ void smv_typecheckt::typecheck(
     typecheck(item.expr, OTHER);
     item.equal_expr().type() = bool_typet{};
     return;
+
+  case smv_parse_treet::modulet::itemt::VAR:
+    return;
   }
 }
 
@@ -2104,6 +2107,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
 
   define_map.clear();
 
+  // variables first, need to be visible before declaration
   convert(smv_module.vars);
 
   // transition relation
@@ -2122,9 +2126,10 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
 
     convert_ports(smv_module, module_symbol.type);
 
-    for (auto &item : smv_module.items) {
-      convert(item);
-    }
+    // non-variable items
+    for(auto &item : smv_module.items)
+      if(!item.is_var())
+        convert(item);
 
     flatten_hierarchy(smv_module);