SMV: introduce smv_identifier_exprt

This introduces a class for the identifiers used in the SMV parse tree.

The type checker subsequently turns them into symbols, when this is
appropriate.

Author: kroening

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)

src/smvlang/parser.y

@@ -142,8 +142,8 @@ Function: merge_complex_identifier
 
 irep_idt merge_complex_identifier(const exprt &expr)
 {
-  if(expr.id() == ID_symbol)
-    return to_symbol_expr(expr).get_identifier();
+  if(expr.id() == ID_smv_identifier)
+    return expr.get(ID_identifier);
   else if(expr.id() == ID_member)
   {
     auto &member_expr = to_member_expr(expr);
@@ -677,7 +677,7 @@ enum_element: IDENTIFIER_Token
              $$=$1;
              PARSER.module->enum_set.insert(stack_expr($1).id_string());
 
-             exprt expr(ID_symbol);
+             exprt expr(ID_smv_identifier);
              expr.set(ID_identifier, stack_expr($1).id());
              PARSER.set_source_location(expr);
              PARSER.module->add_enum(std::move(expr));
@@ -970,7 +970,7 @@ variable_identifier: complex_identifier
              }
              else // not an enum, probably a variable
              {
-               init($$, ID_symbol);
+               init($$, ID_smv_identifier);
                stack_expr($$).set(ID_identifier, id);
                auto var_it = PARSER.module->vars.find(id);
                if(var_it!= PARSER.module->vars.end())
@@ -983,7 +983,7 @@ variable_identifier: complex_identifier
              // Not in the NuSMV grammar.
              const irep_idt &id=stack_expr($1).id();
 
-             init($$, ID_symbol);
+             init($$, ID_smv_identifier);
              stack_expr($$).set(ID_identifier, id);
              PARSER.module->vars[id];
            }
@@ -994,7 +994,7 @@ complex_identifier:
            {
              $$ = $1;
              irep_idt identifier = stack_expr($$).id();
-             stack_expr($$).id(ID_symbol);
+             stack_expr($$).id(ID_smv_identifier);
              stack_expr($$).set(ID_identifier, identifier);
            }
            | complex_identifier DOT_Token QIDENTIFIER_Token

src/smvlang/smv_expr.h

@@ -326,4 +326,40 @@ inline smv_word1_exprt &to_smv_word1_expr(exprt &expr)
   return static_cast<smv_word1_exprt &>(expr);
 }
 
+// parse tree only -- used for identifiers, which may turn into
+// symbols or enums
+class smv_identifier_exprt : public nullary_exprt
+{
+public:
+  explicit smv_identifier_exprt(irep_idt _identifier)
+    : nullary_exprt{ID_smv_identifier, typet{}}
+  {
+    identifier(_identifier);
+  }
+
+  irep_idt identifier() const
+  {
+    return get(ID_identifier);
+  }
+
+  void identifier(irep_idt _identifier)
+  {
+    set(ID_identifier, _identifier);
+  }
+};
+
+inline const smv_identifier_exprt &to_smv_identifier_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_identifier);
+  smv_identifier_exprt::check(expr);
+  return static_cast<const smv_identifier_exprt &>(expr);
+}
+
+inline smv_identifier_exprt &to_smv_identifier_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_identifier);
+  smv_identifier_exprt::check(expr);
+  return static_cast<smv_identifier_exprt &>(expr);
+}
+
 #endif // CPROVER_SMV_EXPR_H

src/smvlang/smv_typecheck.cpp

@@ -203,7 +203,7 @@ void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
       for(auto &op : inst.operands())
         convert(op);
 
-      auto instance_base_name = to_symbol_expr(item.expr).get_identifier();
+      auto instance_base_name = to_smv_identifier_expr(item.expr).identifier();
 
       instantiate(
         smv_module,
@@ -1701,7 +1701,7 @@ void smv_typecheckt::convert(exprt &expr)
   for(auto &op : expr.operands())
     convert(op);
 
-  if(expr.id()==ID_symbol)
+  if(expr.id() == ID_smv_identifier)
   {
     const std::string &identifier=expr.get_string(ID_identifier);
 
@@ -1711,6 +1711,7 @@ void smv_typecheckt::convert(exprt &expr)
     std::string id = module + "::var::" + identifier;
 
     expr.set(ID_identifier, id);
+    expr.id(ID_symbol);
   }
   else if(expr.id()=="smv_nondet_choice" ||
           expr.id()=="smv_union")
@@ -1914,7 +1915,7 @@ void smv_typecheckt::create_var_symbols(
   {
     if(item.is_var())
     {
-      irep_idt base_name = to_symbol_expr(item.expr).get_identifier();
+      irep_idt base_name = to_smv_identifier_expr(item.expr).identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
 
       auto symbol_ptr = symbol_table.lookup(identifier);
@@ -1953,8 +1954,9 @@ void smv_typecheckt::create_var_symbols(
     }
     else if(item.is_define())
     {
-      const auto &symbol_expr = to_symbol_expr(to_equal_expr(item.expr).lhs());
-      irep_idt base_name = symbol_expr.get_identifier();
+      const auto &identifier_expr =
+        to_smv_identifier_expr(to_equal_expr(item.expr).lhs());
+      irep_idt base_name = identifier_expr.identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
       typet type;
       type.make_nil();
@@ -1973,13 +1975,13 @@ void smv_typecheckt::create_var_symbols(
       symbol.value = nil_exprt{};
       symbol.is_input = true;
       symbol.is_state_var = false;
-      symbol.location = symbol_expr.source_location();
+      symbol.location = identifier_expr.source_location();
 
       symbol_table.insert(std::move(symbol));
     }
     else if(item.is_enum())
     {
-      irep_idt base_name = to_symbol_expr(item.expr).get_identifier();
+      irep_idt base_name = to_smv_identifier_expr(item.expr).identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
 
       auto symbol_ptr = symbol_table.lookup(identifier);