SystemVerilog: discover package dependencies in expressions and types

Dependencies on a package via the package scope operator :: are now
discovered when used in types or expressions.

Author: kroening

lib/cbmc

@@ -6,8 +6,6 @@ endpackage
 
 module main;
 
-  import moo::*;
-
   parameter Q = moo::P;
 
   assert final (Q == 123);

regression/verilog/packages/package2.sv

@@ -6,8 +6,6 @@ endpackage
 
 module main;
 
-  import moo::*;
-
   moo::my_type some_var;
 
   assert final ($typename(some_var) == "bit signed[7:0]");

regression/verilog/packages/package_typedef1.sv

@@ -160,7 +160,7 @@ Function: verilog_typecheck_exprt::elaborate_package_scope_typedef
 \*******************************************************************/
 
 typet verilog_typecheck_exprt::elaborate_package_scope_typedef(
-  const type_with_subtypest &src)
+  const verilog_package_scope_typet &src)
 {
   auto location = src.source_location();
 
@@ -445,7 +445,7 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
   else if(src.id() == ID_verilog_package_scope)
   {
     // package::typedef
-    return elaborate_package_scope_typedef(to_type_with_subtypes(src));
+    return elaborate_package_scope_typedef(to_verilog_package_scope_type(src));
   }
   else
   {

src/verilog/verilog_elaborate_type.cpp

@@ -81,6 +81,34 @@ void verilog_module_sourcet::show(std::ostream &out) const
   out << '\n';
 }
 
+static void
+dependencies_rec(const verilog_module_itemt &, std::vector<irep_idt> &);
+
+static void dependencies_rec(const exprt &expr, std::vector<irep_idt> &dest)
+{
+  if(expr.id() == ID_verilog_package_scope)
+  {
+    auto &package_scope_expr = to_verilog_package_scope_expr(expr);
+    dest.push_back(
+      verilog_package_identifier(package_scope_expr.package_base_name()));
+  }
+  else
+  {
+    for(auto &op : expr.operands())
+      dependencies_rec(op, dest);
+  }
+}
+
+static void dependencies_rec(const typet &type, std::vector<irep_idt> &dest)
+{
+  if(type.id() == ID_verilog_package_scope)
+  {
+    auto &package_scope_type = to_verilog_package_scope_type(type);
+    dest.push_back(
+      verilog_package_identifier(package_scope_type.package_base_name()));
+  }
+}
+
 static void dependencies_rec(
   const verilog_module_itemt &module_item,
   std::vector<irep_idt> &dest)
@@ -114,6 +142,86 @@ static void dependencies_rec(
         verilog_package_identifier(import_item.get(ID_verilog_package)));
     }
   }
+  else if(module_item.id() == ID_parameter_decl)
+  {
+    auto &parameter_decl = to_verilog_parameter_decl(module_item);
+    for(auto &decl : parameter_decl.declarations())
+    {
+      dependencies_rec(decl.type(), dest);
+      dependencies_rec(decl.value(), dest);
+    }
+  }
+  else if(module_item.id() == ID_local_parameter_decl)
+  {
+    auto &localparam_decl = to_verilog_local_parameter_decl(module_item);
+    for(auto &decl : localparam_decl.declarations())
+    {
+      dependencies_rec(decl.type(), dest);
+      dependencies_rec(decl.value(), dest);
+    }
+  }
+  else if(module_item.id() == ID_decl)
+  {
+    auto &decl = to_verilog_decl(module_item);
+    dependencies_rec(decl.type(), dest);
+    for(auto &declarator : decl.declarators())
+    {
+      dependencies_rec(declarator.type(), dest);
+      dependencies_rec(declarator.value(), dest);
+    }
+  }
+  else if(
+    module_item.id() == ID_verilog_always ||
+    module_item.id() == ID_verilog_always_comb ||
+    module_item.id() == ID_verilog_always_ff ||
+    module_item.id() == ID_verilog_always_latch)
+  {
+    dependencies_rec(to_verilog_always_base(module_item).statement(), dest);
+  }
+  else if(module_item.id() == ID_initial)
+  {
+    dependencies_rec(to_verilog_initial(module_item).statement(), dest);
+  }
+  else if(module_item.id() == ID_inst)
+  {
+  }
+  else if(module_item.id() == ID_inst_builtin)
+  {
+  }
+  else if(module_item.id() == ID_continuous_assign)
+  {
+  }
+  else if(
+    module_item.id() == ID_verilog_assert_property ||
+    module_item.id() == ID_verilog_assume_property ||
+    module_item.id() == ID_verilog_restrict_property ||
+    module_item.id() == ID_verilog_cover_property)
+  {
+  }
+  else if(module_item.id() == ID_verilog_assertion_item)
+  {
+  }
+  else if(module_item.id() == ID_parameter_override)
+  {
+  }
+  else if(module_item.id() == ID_verilog_final)
+  {
+  }
+  else if(module_item.id() == ID_verilog_let)
+  {
+    // to_verilog_let(module_item));
+  }
+  else if(module_item.id() == ID_verilog_smv_assume)
+  {
+  }
+  else if(module_item.id() == ID_verilog_property_declaration)
+  {
+    // to_verilog_property_declaration(module_item)
+  }
+  else if(module_item.id() == ID_verilog_sequence_declaration)
+  {
+    // to_verilog_sequence_declaration(module_item)
+  }
 }
 
 std::vector<irep_idt> verilog_item_containert::dependencies() const

src/verilog/verilog_expr.cpp

@@ -3011,4 +3011,39 @@ inline verilog_value_range_exprt &to_verilog_value_range_expr(exprt &expr)
   return static_cast<verilog_value_range_exprt &>(expr);
 }
 
+/// package::identifier
+class verilog_package_scope_exprt : public binary_exprt
+{
+public:
+  irep_idt package_base_name() const
+  {
+    return op0().id();
+  }
+
+  const exprt &identifier() const
+  {
+    return op1();
+  }
+};
+
+/// Cast a generic typet to a \ref verilog_package_scope_exprt. This is an unchecked
+/// conversion. \a type must be known to be \ref verilog_package_scope_exprt.
+/// \param type: Source type
+/// \return Object of type \ref verilog_package_scope_exprt
+inline const verilog_package_scope_exprt &
+to_verilog_package_scope_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_package_scope);
+  verilog_package_scope_exprt::check(expr);
+  return static_cast<const verilog_package_scope_exprt &>(expr);
+}
+
+/// \copydoc to_verilog_exprdef_expr(const exprt &)
+inline verilog_package_scope_exprt &to_verilog_package_scope_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_package_scope);
+  verilog_package_scope_exprt::check(expr);
+  return static_cast<verilog_package_scope_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_expr.h

@@ -2829,13 +2829,14 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
   else if(expr.id() == ID_verilog_package_scope)
   {
     auto location = expr.source_location();
+    auto &package_scope = to_verilog_package_scope_expr(expr);
 
-    if(expr.rhs().id() != ID_symbol)
+    if(package_scope.identifier().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);
+    auto package_base = package_scope.package_base_name();
+    auto rhs_base = package_scope.identifier().get(ID_base_name);
 
     // stitch together
     irep_idt full_identifier =

src/verilog/verilog_typecheck_expr.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 
 class function_call_exprt;
 class power_exprt;
+class verilog_package_scope_typet;
 
 class verilog_typecheck_exprt:public verilog_typecheck_baset
 {
@@ -66,7 +67,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 elaborate_package_scope_typedef(const verilog_package_scope_typet &);
   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 &);

src/verilog/verilog_typecheck_expr.h

@@ -19,3 +19,15 @@ constant_exprt verilog_event_typet::null_expr() const
 {
   return encoding().all_zeros_expr();
 }
+
+void verilog_package_scope_typet::check(
+  const typet &type,
+  const validation_modet vm)
+{
+  PRECONDITION(type.id() == ID_verilog_package_scope);
+  type_with_subtypest::check(type);
+  DATA_CHECK(
+    vm,
+    to_type_with_subtypes(type).subtypes().size() == 2,
+    "verilog_package_scope type must have two subtypes");
+}

src/verilog/verilog_types.cpp

@@ -656,4 +656,42 @@ inline verilog_typedef_typet &to_verilog_typedef_type(typet &type)
   return static_cast<verilog_typedef_typet &>(type);
 }
 
+/// package::type
+class verilog_package_scope_typet : public type_with_subtypest
+{
+public:
+  irep_idt package_base_name() const
+  {
+    return subtypes()[0].id();
+  }
+
+  const typet &typedef_type() const
+  {
+    return subtypes()[1];
+  }
+
+  static void
+  check(const typet &, const validation_modet = validation_modet::INVARIANT);
+};
+
+/// Cast a generic typet to a \ref verilog_package_scope_typet. This is an unchecked
+/// conversion. \a type must be known to be \ref verilog_package_scope_typet.
+/// \param type: Source type
+/// \return Object of type \ref verilog_package_scope_typet
+inline const verilog_package_scope_typet &
+to_verilog_package_scope_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_verilog_package_scope);
+  verilog_package_scope_typet::check(type);
+  return static_cast<const verilog_package_scope_typet &>(type);
+}
+
+/// \copydoc to_verilog_typedef_type(const typet &)
+inline verilog_package_scope_typet &to_verilog_package_scope_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_verilog_package_scope);
+  verilog_package_scope_typet::check(type);
+  return static_cast<verilog_package_scope_typet &>(type);
+}
+
 #endif