Merge branch 'main' into verilog_string

tautschnig · web-flow · commit 30190ba2966d · 2025-01-13T11:02:37.000+01:00
diff --git a/CHANGELOG b/CHANGELOG
@@ -9,6 +9,7 @@
 * SystemVerilog: $bitstoreal/$bitstoshortreal, $realtobits/$shortrealtobits
 * SystemVerilog: $itor, $rtoi
 * SystemVerilog: chandle, event, string
+* SystemVerilog: package scope operator
 
 # EBMC 5.4
 
diff --git a/regression/verilog/packages/package2.desc b/regression/verilog/packages/package2.desc
@@ -0,0 +1,7 @@
+CORE
+package2.sv
+
+^^\[.*\] always main\.Q == 123: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/verilog/packages/package2.sv b/regression/verilog/packages/package2.sv
@@ -0,0 +1,15 @@
+package moo;
+
+  parameter P = 123;
+
+endpackage
+
+module main;
+
+  import moo::*;
+
+  parameter Q = moo::P;
+
+  assert final (Q == 123);
+
+endmodule
diff --git a/regression/verilog/packages/package_enum1.desc b/regression/verilog/packages/package_enum1.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+package_enum1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Support for enums in packages is missing.
diff --git a/regression/verilog/packages/package_enum1.sv b/regression/verilog/packages/package_enum1.sv
@@ -0,0 +1,13 @@
+package moo;
+
+  typedef enum { RED, GREEN } my_type;
+
+endpackage
+
+module main;
+
+  import moo::*;
+
+  assert final (moo::GREEN == 1);
+
+endmodule
diff --git a/regression/verilog/packages/package_typedef1.desc b/regression/verilog/packages/package_typedef1.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+package_typedef1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Support for typedefs in packages is missing.
diff --git a/regression/verilog/packages/package_typedef1.sv b/regression/verilog/packages/package_typedef1.sv
@@ -0,0 +1,15 @@
+package moo;
+
+  typedef byte my_type;
+
+endpackage
+
+module main;
+
+  import moo::*;
+
+  moo::my_type some_var;
+
+  assert final ($typename(some_var) == "byte");
+
+endmodule
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -251,6 +251,7 @@ IREP_ID_ONE(verilog_class)
 IREP_ID_ONE(verilog_module)
 IREP_ID_ONE(verilog_package)
 IREP_ID_ONE(verilog_package_import)
+IREP_ID_ONE(verilog_package_scope)
 IREP_ID_ONE(verilog_program)
 IREP_ID_ONE(verilog_udp)
 IREP_ID_ONE(module_source)
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -1355,9 +1355,13 @@ package_import_item_brace:
 
 package_import_item:
 	  package_identifier "::" identifier
-		{ init($$, ID_verilog_import_item); mto($$, $1); mto($$, $3); }
+		{ init($$, ID_verilog_import_item);
+		  stack_expr($$).set(ID_verilog_package, stack_expr($1).id());
+		  stack_expr($$).set(ID_identifier, stack_expr($3).id()); }
 	| package_identifier "::" "*"
-		{ init($$, ID_verilog_import_item); mto($$, $1); }
+		{ init($$, ID_verilog_import_item);
+		  stack_expr($$).set(ID_verilog_package, stack_expr($1).id());
+		  stack_expr($$).set(ID_identifier, "*"); }
 	;
 
 genvar_declaration:
@@ -4032,6 +4036,10 @@ part_select_range:
 
 primary:  primary_literal
 	| hierarchical_identifier_select
+	| package_scope hierarchical_identifier_select
+		{ init($$, ID_verilog_package_scope);
+		  mto($$, $1);
+		  mto($$, $2); }
 	| concatenation 
         | multiple_concatenation
         | function_subroutine_call
@@ -4209,6 +4217,9 @@ net_identifier: identifier;
 
 package_identifier: TOK_NON_TYPE_IDENTIFIER;
 
+package_scope: package_identifier "::"
+	;
+
 param_identifier: TOK_NON_TYPE_IDENTIFIER;
 
 port_identifier: identifier;
diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp
@@ -100,6 +100,14 @@ static void dependencies_rec(
   {
     dependencies_rec(to_verilog_generate_for(module_item).body(), dest);
   }
+  else if(module_item.id() == ID_verilog_package_import)
+  {
+    for(auto &import_item : module_item.get_sub())
+    {
+      dest.push_back(
+        verilog_package_identifier(import_item.get(ID_verilog_package)));
+    }
+  }
 }
 
 std::vector<irep_idt> verilog_item_containert::dependencies() const
diff --git a/src/verilog/verilog_language.cpp b/src/verilog/verilog_language.cpp
@@ -132,7 +132,7 @@ void verilog_languaget::dependencies(
   std::set<std::string> &dependency_set)
 {
   verilog_parse_treet::item_mapt::const_iterator it =
-    parse_tree.item_map.find(id2string(verilog_module_name(module)));
+    parse_tree.item_map.find(id2string(verilog_item_key(module)));
 
   if(it != parse_tree.item_map.end())
   {
diff --git a/src/verilog/verilog_parse_tree.cpp b/src/verilog/verilog_parse_tree.cpp
@@ -62,8 +62,15 @@ void verilog_parse_treet::modules_provided(
   for(auto &item : items)
   {
     if(item.id() == ID_verilog_module)
+    {
       module_set.insert(id2string(
         verilog_module_symbol(to_verilog_module_source(item).base_name())));
+    }
+    else if(item.id() == ID_verilog_package)
+    {
+      module_set.insert(id2string(verilog_package_identifier(
+        to_verilog_module_source(item).base_name())));
+    }
   }
 }
 
diff --git a/src/verilog/verilog_parse_tree.h b/src/verilog/verilog_parse_tree.h
@@ -75,7 +75,7 @@ class verilog_parse_treet
 
   // An index into the items list.
   // The key is
-  //   package::name for pagages
+  //   package::name for packages
   //   name          for modules, etc.
   // as packages have a separate name space (1800-2017 3.13).
   typedef std::
diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp
@@ -1947,55 +1947,27 @@ Function: verilog_typecheck
 bool verilog_typecheck(
   const verilog_parse_treet &parse_tree,
   symbol_table_baset &symbol_table,
-  const std::string &module,
+  const irep_idt &module_identifier,
   bool warn_implicit_nets,
   message_handlert &message_handler)
 {
   verilog_parse_treet::item_mapt::const_iterator it =
-    parse_tree.item_map.find(id2string(verilog_module_name(module)));
+    parse_tree.item_map.find(id2string(verilog_item_key(module_identifier)));
 
   if(it == parse_tree.item_map.end())
   {
     messaget message(message_handler);
-    message.error() << "module `" << module 
-                    << "' not found" << messaget::eom;
+    message.error() << "module `" << module_identifier << "' not found"
+                    << messaget::eom;
     return true;
   }
 
-  auto &module_source = to_verilog_module_source(*it->second);
-
-  return verilog_typecheck(
-    symbol_table,
-    module_source,
-    parse_tree.standard,
-    warn_implicit_nets,
-    message_handler);
-}
-
-/*******************************************************************\
-
-Function: verilog_typecheck
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-bool verilog_typecheck(
-  symbol_table_baset &symbol_table,
-  const verilog_module_sourcet &verilog_module_source,
-  verilog_standardt standard,
-  bool warn_implicit_nets,
-  message_handlert &message_handler)
-{
-  // create symbol
+  auto &verilog_module_source = to_verilog_module_source(*it->second);
 
+  // create the symbol
   irep_idt base_name = verilog_module_source.base_name();
 
-  symbolt symbol{verilog_module_symbol(base_name), module_typet{}, ID_Verilog};
+  symbolt symbol{module_identifier, module_typet{}, ID_Verilog};
 
   symbol.base_name = base_name;
   symbol.pretty_name = base_name;
@@ -2017,7 +1989,11 @@ bool verilog_typecheck(
   }
 
   verilog_typecheckt verilog_typecheck(
-    standard, warn_implicit_nets, *new_symbol, symbol_table, message_handler);
+    parse_tree.standard,
+    warn_implicit_nets,
+    *new_symbol,
+    symbol_table,
+    message_handler);
 
   return verilog_typecheck.typecheck_main();
 }
diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h
@@ -22,21 +22,13 @@ Author: Daniel Kroening, kroening@kroening.com
 bool verilog_typecheck(
   const verilog_parse_treet &parse_tree,
   symbol_table_baset &,
-  const std::string &module,
+  const irep_idt &module_identifier,
   bool warn_implicit_nets,
   message_handlert &message_handler);
 
 bool verilog_typecheck(
   symbol_table_baset &,
-  const verilog_module_sourcet &verilog_module_source,
-  verilog_standardt,
-  bool warn_implicit_nets,
-  message_handlert &message_handler);
-
-bool verilog_typecheck(
-  symbol_table_baset &,
-  const std::string &module_identifier,
-  verilog_standardt,
+  const irep_idt &module_identifier,
   const exprt::operandst &parameters,
   message_handlert &message_handler);
 
diff --git a/src/verilog/verilog_typecheck_base.cpp b/src/verilog/verilog_typecheck_base.cpp
@@ -36,6 +36,25 @@ irep_idt verilog_module_symbol(const irep_idt &base_name)
 
 /*******************************************************************\
 
+Function: verilog_package_identifier
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+irep_idt verilog_package_identifier(const irep_idt &base_name)
+{
+  // Packages and modules have separate name spaces,
+  // hence the prefix.
+  return "Verilog::package::" + id2string(base_name);
+}
+
+/*******************************************************************\
+
 Function: strip_verilog_prefix
 
   Inputs:
@@ -58,7 +77,7 @@ irep_idt strip_verilog_prefix(const irep_idt &identifier)
 
 /*******************************************************************\
 
-Function: verilog_module_name
+Function: verilog_item_key
 
   Inputs:
 
@@ -68,7 +87,7 @@ Function: verilog_module_name
 
 \*******************************************************************/
 
-irep_idt verilog_module_name(const irep_idt &identifier)
+irep_idt verilog_item_key(const irep_idt &identifier)
 {
   return strip_verilog_prefix(identifier);
 }
diff --git a/src/verilog/verilog_typecheck_base.h b/src/verilog/verilog_typecheck_base.h
@@ -17,7 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "verilog_standard.h"
 
 irep_idt verilog_module_symbol(const irep_idt &base_name);
-irep_idt verilog_module_name(const irep_idt &identifier);
+irep_idt verilog_package_identifier(const irep_idt &base_name);
+irep_idt verilog_item_key(const irep_idt &identifier);
 irep_idt strip_verilog_prefix(const irep_idt &identifier);
 
 class array_typet;
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
@@ -2809,6 +2809,34 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 {
   if(expr.id() == ID_verilog_bit_select)
     return convert_bit_select_expr(to_binary_expr(expr));
+  else if(expr.id() == ID_verilog_package_scope)
+  {
+    auto location = expr.source_location();
+
+    if(expr.rhs().id() != ID_symbol)
+      throw errort().with_location(location)
+        << expr.id() << " expects symbol on the rhs";
+
+    auto package_base = expr.lhs().id();
+    auto rhs_base = expr.rhs().get(ID_base_name);
+
+    // stitch together
+    irep_idt full_identifier =
+      id2string(verilog_package_identifier(expr.lhs().id())) + '.' +
+      id2string(rhs_base);
+
+    const symbolt *symbol;
+    if(ns.lookup(full_identifier, symbol))
+    {
+      throw errort().with_location(location)
+        << "identifier " << rhs_base << " not found in package "
+        << package_base;
+    }
+
+    // found!
+    return symbol_exprt{full_identifier, symbol->type}.with_source_location(
+      location);
+  }
   else if(expr.id()==ID_replication)
     return convert_replication_expr(to_replication_expr(expr));
   else if(expr.id() == ID_and || expr.id() == ID_or)

Original file line number	Diff line number	Diff line change
`@@ -100,6 +100,14 @@ static void dependencies_rec(`
`100`	`100`	`{`
`101`	`101`	`dependencies_rec(to_verilog_generate_for(module_item).body(), dest);`
`102`	`102`	`}`
	`103`	`+ else if(module_item.id() == ID_verilog_package_import)`
	`104`	`+ {`
	`105`	`+ for(auto &import_item : module_item.get_sub())`
	`106`	`+ {`
	`107`	`+ dest.push_back(`
	`108`	`+ verilog_package_identifier(import_item.get(ID_verilog_package)));`
	`109`	`+ }`
	`110`	`+ }`
`103`	`111`	`}`
`104`	`112`
`105`	`113`	`std::vector<irep_idt> verilog_item_containert::dependencies() const`