SMV: add enums to the parse tree

This adds enums as items to the parse tree data structure.

Author: kroening

regression/smv/enums/name_collision1.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+name_collision1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This crashes.

regression/smv/enums/name_collision1.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR some_var: { red, green, yellow, off };
+
+-- identifier already used
+VAR red : boolean;

regression/smv/enums/name_collision2.desc

@@ -0,0 +1,9 @@
+CORE
+name_collision2.smv
+
+^file .* line 8: enum red already declared, at file .* line 3$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/smv/enums/name_collision2.smv

@@ -0,0 +1,8 @@
+MODULE main
+
+VAR red : boolean;
+
+-- The identifier "red" is already used.
+-- NuSMV doesn't error this, but yields an error when attempting
+-- to use the identifier.
+VAR some_var: { red, green, yellow, off };

regression/smv/enums/name_collision3.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+name_collision3.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This crashes.

regression/smv/enums/name_collision3.smv

@@ -0,0 +1,9 @@
+MODULE submodule
+
+MODULE main
+
+VAR some_var: { red, green, yellow, off };
+
+-- identifier already used
+VAR red : submodule;
+

src/smvlang/parser.y

@@ -676,6 +676,11 @@ enum_element: IDENTIFIER_Token
            {
              $$=$1;
              PARSER.module->enum_set.insert(stack_expr($1).id_string());
+
+             exprt expr(ID_symbol);
+             expr.set(ID_identifier, stack_expr($1).id());
+             PARSER.set_source_location(expr);
+             PARSER.module->add_enum(std::move(expr));
            }
            ;
 

src/smvlang/smv_parse_tree.cpp

@@ -74,6 +74,8 @@ std::string to_string(smv_parse_treet::modulet::itemt::item_typet i)
   case smv_parse_treet::modulet::itemt::FAIRNESS: return "FAIRNESS";
   case smv_parse_treet::modulet::itemt::DEFINE:
     return "DEFINE";
+  case smv_parse_treet::modulet::itemt::ENUM:
+    return "ENUM";
   case smv_parse_treet::modulet::itemt::VAR:
     return "VAR";
 

src/smvlang/smv_parse_tree.h

@@ -48,6 +48,7 @@ class smv_parse_treet
         ASSIGN_NEXT,
         CTLSPEC,
         DEFINE,
+        ENUM,
         FAIRNESS,
         INIT,
         INVAR,
@@ -127,6 +128,11 @@ class smv_parse_treet
         return item_type==INIT;
       }
 
+      bool is_enum() const
+      {
+        return item_type == ENUM;
+      }
+
       bool is_var() const
       {
         return item_type == VAR;
@@ -261,6 +267,12 @@ class smv_parse_treet
       items.emplace_back(itemt::VAR, std::move(expr), std::move(location));
     }
 
+    void add_enum(exprt expr)
+    {
+      auto location = expr.source_location();
+      items.emplace_back(itemt::ENUM, std::move(expr), std::move(location));
+    }
+
     mc_varst vars;
     enum_sett enum_set;
 

src/smvlang/smv_typecheck.cpp

@@ -1870,6 +1870,7 @@ void smv_typecheckt::typecheck(
     item.equal_expr().type() = bool_typet{};
     return;
 
+  case smv_parse_treet::modulet::itemt::ENUM:
   case smv_parse_treet::modulet::itemt::VAR:
     return;
   }
@@ -1977,6 +1978,19 @@ void smv_typecheckt::create_var_symbols(
 
       symbol_table.insert(std::move(symbol));
     }
+    else if(item.is_enum())
+    {
+      irep_idt base_name = to_symbol_expr(item.expr).get_identifier();
+      irep_idt identifier = module + "::var::" + id2string(base_name);
+
+      auto symbol_ptr = symbol_table.lookup(identifier);
+      if(symbol_ptr != nullptr)
+      {
+        throw errort{}.with_location(item.expr.source_location())
+          << "enum " << base_name << " already declared, at "
+          << symbol_ptr->location;
+      }
+    }
   }
 }