From 1a426db0c171490fa6a2d4243a62e15371b5bdfd Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 23 Oct 2025 13:12:53 -0700
Subject: [PATCH] SMV: enums are global

SMV's enum name space is global, i.e., crosses modules.

This moves the resolution of identifier to variables or enums from the
parser to the typechecking phase.
---
 src/hw_cbmc_irep_ids.h       |  1 +
 src/smvlang/parser.y         | 31 ++++---------------------------
 src/smvlang/smv_parse_tree.h |  4 +++-
 3 files changed, 8 insertions(+), 28 deletions(-)

diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 912591f66..87ca0a2a7 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -26,6 +26,7 @@ IREP_ID_ONE(smv_extend)
 IREP_ID_ONE(smv_max)
 IREP_ID_ONE(smv_min)
 IREP_ID_ONE(smv_next)
+IREP_ID_ONE(smv_identifier)
 IREP_ID_ONE(smv_iff)
 IREP_ID_TWO(C_smv_iff, "#smv_iff")
 IREP_ID_ONE(smv_resize)
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index d2e37796c..ee82d5456 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -675,7 +675,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());
 
              exprt expr(ID_symbol);
              expr.set(ID_identifier, stack_expr($1).id());
@@ -950,33 +950,10 @@ identifier : IDENTIFIER_Token
 
 variable_identifier: complex_identifier
            {
+             // Could be a variable, or an enum
              auto id = merge_complex_identifier(stack_expr($1));
-
-             bool is_enum=(PARSER.module->enum_set.find(id)!=
-                           PARSER.module->enum_set.end());
-             bool is_var=(PARSER.module->vars.find(id)!=
-                          PARSER.module->vars.end());
-
-             if(is_var && is_enum)
-             {
-               yyerror("identifier `"+id2string(id)+"' is ambiguous");
-               YYERROR;
-             }
-             else if(is_enum)
-             {
-               init($$, ID_constant);
-               stack_expr($$).type()=typet(ID_smv_enumeration);
-               stack_expr($$).set(ID_value, id);
-             }
-             else // not an enum, probably a variable
-             {
-               init($$, ID_symbol);
-               stack_expr($$).set(ID_identifier, id);
-               auto var_it = PARSER.module->vars.find(id);
-               if(var_it!= PARSER.module->vars.end())
-                 stack_expr($$).type()=var_it->second.type;
-               //PARSER.module->vars[stack_expr($1).id()];
-             }
+             init($$, ID_smv_identifier);
+             stack_expr($$).set(ID_identifier, id);
            }
            | STRING_Token
            {
diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h
index 610e61ee8..89564900d 100644
--- a/src/smvlang/smv_parse_tree.h
+++ b/src/smvlang/smv_parse_tree.h
@@ -274,10 +274,12 @@ class smv_parse_treet
     }
 
     mc_varst vars;
-    enum_sett enum_set;
 
     std::list<irep_idt> ports;
   };
+
+  // enums are global
+  enum_sett enum_set;
    
   typedef std::unordered_map<irep_idt, modulet, irep_id_hash> modulest;