Merge pull request #957 from diffblue/package-scope-typedef

SystemVerilog: use typedefs from package scopes
diffblue · Feb 3, 2025 · e042948 · e042948
2 parents d3b36a4 + 6c1c0d4
commit e042948
Show file tree

Hide file tree

Showing 6 changed files with 89 additions and 5 deletions.
diff --git a/CHANGELOG b/CHANGELOG
@@ -12,6 +12,7 @@
 * SystemVerilog: package scope operator
 * SystemVerilog: checkers
 * SystemVerilog: clocking block declarations
+* SystemVerilog: typedefs from package scopes
 
 # EBMC 5.4
 

diff --git a/regression/verilog/packages/package_typedef1.sv b/regression/verilog/packages/package_typedef1.sv
@@ -10,6 +10,6 @@ module main;
 
   moo::my_type some_var;
 
-  assert final ($typename(some_var) == "byte");
+  assert final ($typename(some_var) == "bit signed[7:0]");
 
 endmodule
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -1546,10 +1546,13 @@ data_type:
 	        { init($$, ID_verilog_chandle); }
 	| TOK_VIRTUAL interface_opt interface_identifier
 	        { init($$, "virtual_interface"); }
-	| /*scope_opt*/ type_identifier packed_dimension_brace
-		{ stack_expr($1).id(ID_typedef_type);
-                  add_as_subtype(stack_type($2), stack_type($1));
+	| type_identifier packed_dimension_brace
+		{ add_as_subtype(stack_type($2), stack_type($1));
                   $$ = $2; }
+	| package_scope type_identifier packed_dimension_brace
+		{ mto($1, $2);
+		  add_as_subtype(stack_type($3), stack_type($2));
+		  $$ = $3; }
 //	| class_type
 	| TOK_EVENT
 	        { init($$, ID_verilog_event); }

diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp
@@ -149,6 +149,42 @@ typet verilog_typecheck_exprt::convert_packed_array_type(
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::elaborate_package_scope_typedef
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet verilog_typecheck_exprt::elaborate_package_scope_typedef(
+  const type_with_subtypest &src)
+{
+  auto location = src.source_location();
+
+  if(src.subtypes()[1].id() != ID_typedef_type)
+    throw errort().with_location(location)
+      << "verilog_package_scope expects typedef_type on the rhs";
+
+  auto package_base_name = src.subtypes()[0].id();
+  auto typedef_base_name = src.subtypes()[1].get(ID_base_name);
+
+  // stitch together
+  irep_idt full_identifier =
+    id2string(verilog_package_identifier(package_base_name)) + '.' +
+    id2string(typedef_base_name);
+
+  // recursive call
+  verilog_typedef_typet full_typedef_type(full_identifier);
+  full_typedef_type.set(ID_identifier, full_identifier);
+
+  return elaborate_type(full_typedef_type);
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::elaborate_type
 
   Inputs:
@@ -283,7 +319,7 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
     // Look it up!
     const symbolt *symbol_ptr;
 
-    auto identifier = src.get(ID_identifier);
+    auto identifier = to_verilog_typedef_type(src).identifier();
 
     if(ns.lookup(identifier, symbol_ptr))
       throw errort().with_location(source_location)
@@ -402,6 +438,11 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
   {
     return src;
   }
+  else if(src.id() == ID_verilog_package_scope)
+  {
+    // package::typedef
+    return elaborate_package_scope_typedef(to_type_with_subtypes(src));
+  }
   else
   {
     throw errort().with_location(source_location)

diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h
@@ -66,6 +66,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   void propagate_type(exprt &expr, const typet &type);
 
   typet elaborate_type(const typet &);
+  typet elaborate_package_scope_typedef(const type_with_subtypest &);
   typet convert_enum(const class verilog_enum_typet &);
   array_typet convert_unpacked_array_type(const type_with_subtypet &);
   typet convert_packed_array_type(const type_with_subtypet &);

diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h
@@ -618,4 +618,42 @@ inline verilog_event_typet &to_verilog_event_type(typet &type)
   return static_cast<verilog_event_typet &>(type);
 }
 
+/// A typedef
+class verilog_typedef_typet : public typet
+{
+public:
+  explicit verilog_typedef_typet(const irep_idt &_identifier)
+    : typet(ID_typedef_type)
+  {
+    identifier(_identifier);
+  }
+
+  void identifier(const irep_idt &identifier)
+  {
+    set(ID_identifier, identifier);
+  }
+
+  const irep_idt &identifier() const
+  {
+    return get(ID_identifier);
+  }
+};
+
+/// Cast a generic typet to a \ref verilog_typedef_typet. This is an unchecked
+/// conversion. \a type must be known to be \ref verilog_typedef_typet.
+/// \param type: Source type
+/// \return Object of type \ref verilog_typedef_typet
+inline const verilog_typedef_typet &to_verilog_typedef_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_typedef_type);
+  return static_cast<const verilog_typedef_typet &>(type);
+}
+
+/// \copydoc to_verilog_typedef_type(const typet &)
+inline verilog_typedef_typet &to_verilog_typedef_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_typedef_type);
+  return static_cast<verilog_typedef_typet &>(type);
+}
+
 #endif