Verilog: introduce verilog_identifier_exprt

The RHS of the '.' operator is always a simple identifier, which is never
decorated or qualified, and hence, the use of symbol_exprt is inappropriate.
This introduces verilog_identifier_exprt as the RHS of '.', which represents
a base name only.

Author: kroening

src/hw_cbmc_irep_ids.h

@@ -127,6 +127,7 @@ IREP_ID_ONE(verilog_associative_array)
 IREP_ID_ONE(verilog_declarations)
 IREP_ID_ONE(verilog_default_clocking)
 IREP_ID_ONE(verilog_default_disable)
+IREP_ID_ONE(verilog_identifier)
 IREP_ID_ONE(verilog_interconnect)
 IREP_ID_ONE(verilog_lifetime)
 IREP_ID_ONE(verilog_logical_equality)

src/verilog/parser.y

@@ -4770,6 +4770,7 @@ hierarchical_identifier:
         | hierarchical_identifier '.' identifier
 		{ init($$, ID_hierarchical_identifier);
 		  stack_expr($$).reserve_operands(2);
+		  stack_expr($3).id(ID_verilog_identifier);
 		  mto($$, $1);
 		  mto($$, $3);
 		}

src/verilog/verilog_expr.h

@@ -11,6 +11,36 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_expr.h>
 
+/// A simple Verilog identifier, unqualified
+class verilog_identifier_exprt : public nullary_exprt
+{
+public:
+  const irep_idt &base_name() const
+  {
+    return get(ID_base_name);
+  }
+
+  void identifier(irep_idt _base_name)
+  {
+    set(ID_base_name, _base_name);
+  }
+};
+
+inline const verilog_identifier_exprt &
+to_verilog_identifier_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_identifier);
+  verilog_identifier_exprt::check(expr);
+  return static_cast<const verilog_identifier_exprt &>(expr);
+}
+
+inline verilog_identifier_exprt &to_verilog_identifier_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_identifier);
+  verilog_identifier_exprt::check(expr);
+  return static_cast<verilog_identifier_exprt &>(expr);
+}
+
 /// The syntax for these A.B, where A is a module identifier and B
 /// is an identifier within that module. B is given als symbol_exprt.
 class hierarchical_identifier_exprt : public binary_exprt
@@ -21,12 +51,12 @@ class hierarchical_identifier_exprt : public binary_exprt
     return op0();
   }
 
-  const symbol_exprt &item() const
+  const verilog_identifier_exprt &item() const
   {
-    return static_cast<const symbol_exprt &>(binary_exprt::op1());
+    return static_cast<const verilog_identifier_exprt &>(binary_exprt::op1());
   }
 
-  const symbol_exprt &rhs() const
+  const verilog_identifier_exprt &rhs() const
   {
     return item();
   }
@@ -2049,6 +2079,7 @@ class verilog_assert_assume_cover_module_itemt : public verilog_module_itemt
     return op1();
   }
 
+  // The full identifier created by the type checker
   const irep_idt &identifier() const
   {
     return get(ID_identifier);
@@ -2058,6 +2089,11 @@ class verilog_assert_assume_cover_module_itemt : public verilog_module_itemt
   {
     set(ID_identifier, identifier);
   }
+
+  const irep_idt &base_name() const
+  {
+    return get(ID_base_name);
+  }
 };
 
 inline const verilog_assert_assume_cover_module_itemt &
@@ -2119,6 +2155,16 @@ class verilog_assert_assume_cover_statementt : public verilog_statementt
   {
     set(ID_identifier, _identifier);
   }
+
+  const irep_idt &base_name() const
+  {
+    return get(ID_base_name);
+  }
+
+  void base_name(irep_idt _base_name)
+  {
+    set(ID_base_name, _base_name);
+  }
 };
 
 inline const verilog_assert_assume_cover_statementt &

src/verilog/verilog_synthesis.cpp

@@ -510,12 +510,12 @@ void verilog_synthesist::expand_hierarchical_identifier(
   const irep_idt &lhs_identifier = expr.lhs().get(ID_identifier);
 
   // rhs
-  const irep_idt &rhs_identifier = expr.rhs().get_identifier();
+  const irep_idt &rhs_base_name = expr.rhs().base_name();
 
   // just patch together
 
   irep_idt full_identifier =
-    id2string(lhs_identifier) + '.' + id2string(rhs_identifier);
+    id2string(lhs_identifier) + '.' + id2string(rhs_base_name);
 
   // Note: the instance copy may not yet be in symbol table,
   // as the inst module item may be later.

src/verilog/verilog_typecheck.cpp

@@ -962,7 +962,7 @@ void verilog_typecheckt::convert_parameter_override(
 
     auto module_instance =
       to_symbol_expr(hierarchical_identifier.module()).get_identifier();
-    auto parameter_name = hierarchical_identifier.item().get_identifier();
+    auto parameter_name = hierarchical_identifier.item().base_name();
 
     // The rhs must be a constant at this point.
     auto rhs_value =

src/verilog/verilog_typecheck_expr.cpp

@@ -1421,19 +1421,21 @@ exprt verilog_typecheck_exprt::convert_hierarchical_identifier(
 {
   convert_expr(expr.lhs());
 
-  DATA_INVARIANT(expr.rhs().id() == ID_symbol, "expected symbol on rhs of `.'");
+  DATA_INVARIANT(
+    expr.rhs().id() == ID_verilog_identifier,
+    "expected verilog_identifier as rhs of `.'");
 
-  const irep_idt &rhs_identifier = expr.rhs().get_identifier();
+  const irep_idt &rhs_base_name = expr.rhs().base_name();
 
   if(expr.lhs().type().id() == ID_struct || expr.lhs().type().id() == ID_union)
   {
     // look up the component
     auto &compound_type = to_struct_union_type(expr.lhs().type());
-    auto &component = compound_type.get_component(rhs_identifier);
+    auto &component = compound_type.get_component(rhs_base_name);
     if(component.is_nil())
       throw errort().with_location(expr.source_location())
         << compound_type.id() << " does not have a member named "
-        << rhs_identifier;
+        << rhs_base_name;
 
     // create the member expression
     return member_exprt{expr.lhs(), component.get_name(), component.type()}
@@ -1467,7 +1469,7 @@ exprt verilog_typecheck_exprt::convert_hierarchical_identifier(
 
     // the identifier in the module
     const irep_idt full_identifier =
-      id2string(module) + "." + id2string(rhs_identifier);
+      id2string(module) + "." + id2string(rhs_base_name);
 
     const symbolt *symbol;
     if(!ns.lookup(full_identifier, symbol))
@@ -1485,7 +1487,7 @@ exprt verilog_typecheck_exprt::convert_hierarchical_identifier(
     else
     {
       throw errort().with_location(expr.source_location())
-        << "identifier `" << rhs_identifier << "' not found in module `"
+        << "identifier `" << rhs_base_name << "' not found in module `"
         << module_instance_symbol->pretty_name << "'";
     }
 
@@ -1497,7 +1499,7 @@ exprt verilog_typecheck_exprt::convert_hierarchical_identifier(
   else if(expr.lhs().type().id() == ID_named_block)
   {
     const irep_idt full_identifier =
-      id2string(lhs_identifier) + "." + id2string(rhs_identifier);
+      id2string(lhs_identifier) + "." + id2string(rhs_base_name);
 
     const symbolt *symbol;
     if(!ns.lookup(full_identifier, symbol))
@@ -1519,7 +1521,7 @@ exprt verilog_typecheck_exprt::convert_hierarchical_identifier(
     else
     {
       throw errort().with_location(expr.source_location())
-        << "identifier `" << rhs_identifier << "' not found in named block";
+        << "identifier `" << rhs_base_name << "' not found in named block";
     }
   }
   else