SMV: enums are global

SMV's enum name space is global, i.e., crosses modules.  There is now only
one global set of enums.

Author: kroening

regression/smv/modules/module_with_enum1.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE broken-smt-backend
 module_with_enum1.smv
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The enum literal is not found.

regression/smv/modules/module_with_enum2.desc

@@ -0,0 +1,9 @@
+CORE
+module_with_enum2.smv
+
+^file .* line 11: enum a already declared, at file .* line 7$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/smv/modules/module_with_enum2.smv

@@ -0,0 +1,13 @@
+MODULE main
+
+VAR sub : my-module;
+
+-- There is an enum in another module with the same identifier,
+-- which is an error!
+VAR a : boolean;
+
+MODULE my-module
+
+VAR some_enum : { a, b };
+
+ASSIGN some_enum := a;

src/smvlang/parser.y

@@ -664,7 +664,7 @@ enum_list  : enum_element
 enum_element: IDENTIFIER_Token
            {
              $$=$1;
-             PARSER.module->enum_set.insert(stack_expr($1).id_string());
+             PARSER.parse_tree.enum_set.insert(stack_expr($1).id_string());
              PARSER.module->add_enum(
                smv_identifier_exprt{stack_expr($1).id(), PARSER.source_location()});
            }
@@ -907,6 +907,7 @@ identifier : IDENTIFIER_Token
 
 variable_identifier: complex_identifier
            {
+             // Could be a variable, or an enum
              auto id = merge_complex_identifier(stack_expr($1));
              init($$, ID_smv_identifier);
              stack_expr($$).set(ID_identifier, id);

src/smvlang/smv_parse_tree.cpp

@@ -30,6 +30,7 @@ void smv_parse_treet::swap(smv_parse_treet &smv_parse_tree)
 {
   smv_parse_tree.module_list.swap(module_list);
   smv_parse_tree.module_map.swap(module_map);
+  smv_parse_tree.enum_set.swap(enum_set);
 }
 
 /*******************************************************************\

src/smvlang/smv_parse_tree.h

@@ -291,8 +291,6 @@ class smv_parse_treet
       elements.emplace_back(
         elementt::ENUM, std::move(expr), std::move(location));
     }
-
-    enum_sett enum_set;
   };
 
   using module_listt = std::list<modulet>;
@@ -302,7 +300,10 @@ class smv_parse_treet
     std::unordered_map<irep_idt, module_listt::iterator, irep_id_hash>;
   module_mapt module_map;
 
-  void swap(smv_parse_treet &smv_parse_tree);
+  // enums are global
+  enum_sett enum_set;
+
+  void swap(smv_parse_treet &);
   void clear();
 
   void show(std::ostream &) const;

src/smvlang/smv_typecheck.cpp

@@ -277,18 +277,25 @@ void smv_typecheckt::instantiate(
     auto copy = src_element;
 
     // replace the parameter identifiers,
-    // and add the prefix to non-parameter identifiers
+    // and add the prefix to non-parameter, non-enum identifiers
     copy.expr.visit_post(
-      [&parameter_map, &prefix](exprt &expr)
+      [&parameter_map, &prefix, this](exprt &expr)
       {
         if(expr.id() == ID_smv_identifier)
         {
           auto identifier = to_smv_identifier_expr(expr).identifier();
           auto parameter_it = parameter_map.find(identifier);
           if(parameter_it != parameter_map.end())
           {
+            // It's a parameter
             expr = parameter_it->second;
           }
+          else if(
+            smv_parse_tree.enum_set.find(identifier) !=
+            smv_parse_tree.enum_set.end())
+          {
+            // It's an enum, leave as is
+          }
           else
           {
             // add the prefix
@@ -1774,7 +1781,8 @@ void smv_typecheckt::convert(exprt &expr)
       identifier.find("::") == std::string::npos, "conversion is done once");
 
     // enum or variable?
-    if(modulep->enum_set.find(identifier) == modulep->enum_set.end())
+    if(
+      smv_parse_tree.enum_set.find(identifier) == smv_parse_tree.enum_set.end())
     {
       std::string id = module + "::var::" + identifier;