Merge pull request #1660 from diffblue/verilog-package-separator

SystemVerilog: use `::` as separator for identifiers in packages

Author: tautschnig

regression/verilog/packages/package_function1.desc

@@ -3,6 +3,6 @@ package_function1.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.assert\.1\] always package::moo\.foo\(\) == 123: PROVED
+^\[main\.assert\.1\] always package::moo::foo\(\) == 123: PROVED
 --
 --

regression/verilog/packages/package_typedef2.desc

@@ -0,0 +1,7 @@
+CORE
+package_typedef2.sv
+
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/verilog/packages/package_typedef2.sv

@@ -0,0 +1,12 @@
+package some_package;
+
+typedef int some_type;
+
+typedef struct packed {
+  some_type some_field;
+} other_type;
+
+endpackage
+
+module top;
+endmodule

src/verilog/verilog_elaborate_type.cpp

@@ -177,8 +177,8 @@ typet verilog_typecheck_exprt::elaborate_package_scope_typedef(
 
   // stitch together
   irep_idt full_identifier =
-    id2string(verilog_package_identifier(package_base_name)) + '.' +
-    id2string(typedef_base_name);
+    id2string(verilog_package_identifier(package_base_name)) +
+    "::" + id2string(typedef_base_name);
 
   // look it up
   const symbolt *symbol_ptr;

src/verilog/verilog_typecheck.cpp

@@ -285,8 +285,7 @@ Function: verilog_typecheckt::convert_function_or_task
 void verilog_typecheckt::convert_function_or_task(
   verilog_function_or_task_declt &decl)
 {
-  const std::string identifier =
-    id2string(module_identifier) + "." + id2string(decl.base_name());
+  const auto identifier = hierarchical_identifier(decl.base_name());
 
   auto result=symbol_table.get_writeable(identifier);
 
@@ -423,26 +422,11 @@ void verilog_typecheckt::convert_decl(verilog_declt &decl)
   {
     DATA_INVARIANT(declarator.id() == ID_declarator, "must have declarator");
 
-    // in a named block?
-    irep_idt named_block;
-    if(!named_blocks.empty())
-      named_block = named_blocks.back();
+    irep_idt full_identifier = hierarchical_identifier(declarator.base_name());
+    symbolt &symbol = symbol_table_lookup(full_identifier);
 
     // fix the type and identifier
-    irep_idt full_identifier;
-
-    if(!function_or_task_name.empty())
-      full_identifier = id2string(function_or_task_name) + "." +
-                        id2string(named_block) +
-                        id2string(declarator.base_name());
-    else
-      full_identifier = id2string(module_identifier) + "." +
-                        id2string(named_block) +
-                        id2string(declarator.base_name());
-
-    symbolt &symbol = symbol_table_lookup(full_identifier);
     declarator.type() = symbol.type;
-
     declarator.identifier(full_identifier);
 
     if(declarator.has_value())

src/verilog/verilog_typecheck_expr.cpp

@@ -57,8 +57,18 @@ verilog_typecheck_exprt::hierarchical_identifier(irep_idt base_name) const
     return id2string(function_or_task_name) + "." + named_block +
            id2string(base_name);
   else if(!module_identifier.empty())
-    return id2string(module_identifier) + "." + named_block +
-           id2string(base_name);
+  {
+    if(has_prefix(id2string(module_identifier), "Verilog::package::"))
+    {
+      return id2string(module_identifier) + "::" + named_block +
+             id2string(base_name);
+    }
+    else
+    {
+      return id2string(module_identifier) + "." + named_block +
+             id2string(base_name);
+    }
+  }
   else
   {
     // not in a function/task, not in a module/checker/package etc.
@@ -662,7 +672,7 @@ exprt verilog_typecheck_exprt::convert_expr_function_call(
       to_verilog_identifier_expr(package_scope.identifier()).base_name();
 
     full_identifier = id2string(verilog_package_identifier(package_base)) +
-                      '.' + id2string(base_name);
+                      "::" + id2string(base_name);
   }
   else if(f_op.id() == ID_verilog_identifier)
   {
@@ -1316,22 +1326,32 @@ const symbolt *verilog_typecheck_exprt::resolve(const irep_idt base_name)
       return symbol; // found!
   }
 
+  // determine the pacakge/module prefix, using the right separator
+  std::string prefix;
+
+  if(has_prefix(id2string(module_identifier), "Verilog::package::"))
+  {
+    prefix = id2string(module_identifier) + "::";
+  }
+  else
+  {
+    prefix = id2string(module_identifier) + '.';
+  }
+
   // try named blocks, beginning with inner one
   for(named_blockst::const_reverse_iterator
       it=named_blocks.rbegin();
       it!=named_blocks.rend();
       it++)
   {
-    auto full_identifier = id2string(module_identifier) + "." + id2string(*it) +
-                           id2string(base_name);
+    irep_idt full_identifier = prefix + id2string(*it) + id2string(base_name);
 
     const symbolt *symbol;
     if(!ns.lookup(full_identifier, symbol))
       return symbol; // found!
   }
 
-  auto full_identifier =
-    id2string(module_identifier) + "." + id2string(base_name);
+  irep_idt full_identifier = prefix + id2string(base_name);
 
   const symbolt *symbol;
   if(!ns.lookup(full_identifier, symbol))
@@ -3006,8 +3026,8 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     // stitch together
     irep_idt full_identifier =
-      id2string(verilog_package_identifier(package_base)) + '.' +
-      id2string(rhs_base);
+      id2string(verilog_package_identifier(package_base)) +
+      "::" + id2string(rhs_base);
 
     const symbolt *symbol;
     if(ns.lookup(full_identifier, symbol))