Verilog: stengthen typing when using verilog_instt

This adds typing for the sub-ireps of verilog_instt.

Author: kroening

src/verilog/verilog_expr.h

@@ -392,6 +392,38 @@ class verilog_instt:public verilog_module_itemt
   {
     return static_cast<const exprt &>(find(ID_parameter_assignments)).operands();
   }
+
+  class instancet : public exprt
+  {
+  public:
+    const irep_idt &name() const
+    {
+      return get(ID_instance);
+    }
+
+    const exprt::operandst &connections() const
+    {
+      return operands();
+    }
+
+  protected:
+    using exprt::operands;
+  };
+
+  using instancest = std::vector<instancet>;
+
+  const instancest &instances() const
+  {
+    return (const instancest &)(operands());
+  }
+
+  instancest &instances()
+  {
+    return (instancest &)(operands());
+  }
+
+protected:
+  using exprt::operands;
 };
 
 inline const verilog_instt &to_verilog_inst(const exprt &expr)

src/verilog/verilog_synthesis.cpp

@@ -1058,8 +1058,8 @@ void verilog_synthesist::synth_module_instance(
   verilog_synthesis(
     symbol_table, identifier, get_message_handler(), options);
 
-  forall_operands(it, statement)
-    expand_module_instance(symbol, *it, trans);
+  for(auto &instance : statement.instances())
+    expand_module_instance(symbol, instance, trans);
 }
 
 /*******************************************************************\
@@ -1249,20 +1249,21 @@ Function: verilog_synthesist::expand_module_instance
 \*******************************************************************/
 
 void verilog_synthesist::expand_module_instance(
-  const symbolt &symbol,
-  const exprt &op,
+  const symbolt &module_symbol,
+  const verilog_instt::instancet &instance,
   transt &trans)
 {
   construct=constructt::OTHER;
 
-  const irep_idt &instance=op.get(ID_instance);
+  const irep_idt &instance_name = instance.name();
 
   replace_mapt replace_map;
 
   std::list<irep_idt> new_symbols;
 
-  for(auto it=symbol_table.symbol_module_map.lower_bound(symbol.module);
-      it!=symbol_table.symbol_module_map.upper_bound(symbol.module);
+  for(auto it =
+        symbol_table.symbol_module_map.lower_bound(module_symbol.module);
+      it != symbol_table.symbol_module_map.upper_bound(module_symbol.module);
       it++)
   {
     const symbolt &symbol=ns.lookup(it->second);
@@ -1285,7 +1286,7 @@ void verilog_synthesist::expand_module_instance(
 
       full_identifier=id2string(mode)+"::";
       full_identifier+=id2string(verilog_module_name(module));
-      full_identifier+="."+id2string(instance);
+      full_identifier += "." + id2string(instance_name);
       full_identifier+=identifier_without_module;
 
       new_symbol.pretty_name=strip_verilog_prefix(full_identifier);
@@ -1320,11 +1321,11 @@ void verilog_synthesist::expand_module_instance(
   // do the trans
 
   {
-    exprt tmp=symbol.value;
+    exprt tmp = module_symbol.value;
 
     if(tmp.id()!=ID_trans || tmp.operands().size()!=3)
     {
-      error().source_location=op.source_location();
+      error().source_location = instance.source_location();
       error() << "Expected transition system, but got `"
               << tmp.id() << '\'' << eom;
       throw 0;
@@ -1336,7 +1337,7 @@ void verilog_synthesist::expand_module_instance(
       trans.operands()[i].add_to_operands(std::move(tmp.operands()[i]));
   }
 
-  instantiate_ports(instance, op, symbol, replace_map, trans);
+  instantiate_ports(instance_name, instance, module_symbol, replace_map, trans);
 }
 
 /*******************************************************************\

src/verilog/verilog_synthesis_class.h

@@ -9,19 +9,20 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_VERILOG_SYNTHESIS_CLASS_H
 #define CPROVER_VERILOG_SYNTHESIS_CLASS_H
 
-#include <cassert>
-#include <map>
-#include <set>
-#include <unordered_set>
-
 #include <util/mathematical_expr.h>
 #include <util/mp_arith.h>
 #include <util/options.h>
 #include <util/std_expr.h>
 #include <util/string_hash.h>
 
-#include "verilog_typecheck_base.h"
+#include "verilog_expr.h"
 #include "verilog_symbol_table.h"
+#include "verilog_typecheck_base.h"
+
+#include <cassert>
+#include <map>
+#include <set>
+#include <unordered_set>
 
 /*******************************************************************\
 
@@ -201,36 +202,36 @@ class verilog_synthesist:
 
   // module items
   virtual void convert_module_items(symbolt &);
-  void synth_module_item(const class verilog_module_itemt &, transt &);
-  void synth_always(const class verilog_alwayst &);
-  void synth_initial(const class verilog_initialt &);
-  void synth_assert_module_item(const class verilog_module_itemt &);
-  void synth_assume_module_item(const class verilog_module_itemt &);
-  void synth_continuous_assign(const class verilog_continuous_assignt &);
+  void synth_module_item(const verilog_module_itemt &, transt &);
+  void synth_always(const verilog_alwayst &);
+  void synth_initial(const verilog_initialt &);
+  void synth_assert_module_item(const verilog_module_itemt &);
+  void synth_assume_module_item(const verilog_module_itemt &);
+  void synth_continuous_assign(const verilog_continuous_assignt &);
   void synth_force_rec(exprt &lhs, exprt &rhs, transt &);
-  void synth_module_instance(const class verilog_instt &, transt &);
-  void synth_module_instance_builtin(const class verilog_inst_builtint &, transt &);
+  void synth_module_instance(const verilog_instt &, transt &);
+  void synth_module_instance_builtin(const verilog_inst_builtint &, transt &);
 
   // statements
-  void synth_statement(const class verilog_statementt &);
-  void synth_decl(const class verilog_declt &);
-  void synth_block(const class verilog_blockt &);
-  void synth_case(const class verilog_statementt &);
-  void synth_if(const class verilog_ift &);
-  void synth_event_guard(const class verilog_event_guardt &);
-  void synth_delay(const class verilog_delayt &);
-  void synth_for(const class verilog_fort &);
-  void synth_force(const class verilog_forcet &);
+  void synth_statement(const verilog_statementt &);
+  void synth_decl(const verilog_declt &);
+  void synth_block(const verilog_blockt &);
+  void synth_case(const verilog_statementt &);
+  void synth_if(const verilog_ift &);
+  void synth_event_guard(const verilog_event_guardt &);
+  void synth_delay(const verilog_delayt &);
+  void synth_for(const verilog_fort &);
+  void synth_force(const verilog_forcet &);
   void synth_force_rec(const exprt &lhs, const exprt &rhs);
-  void synth_forever(const class verilog_forevert &);
-  void synth_while(const class verilog_whilet &);
-  void synth_repeat(const class verilog_repeatt &);
-  void synth_function_call_or_task_enable(const class verilog_function_callt &);
+  void synth_forever(const verilog_forevert &);
+  void synth_while(const verilog_whilet &);
+  void synth_repeat(const verilog_repeatt &);
+  void synth_function_call_or_task_enable(const verilog_function_callt &);
   [[nodiscard]] exprt synth_expr(exprt expr, symbol_statet symbol_state);
   void synth_assign(const exprt &, bool blocking);
-  void synth_assert(const class verilog_assertt &);
-  void synth_assume(const class verilog_assumet &);
-  void synth_prepostincdec(const class verilog_statementt &);
+  void synth_assert(const verilog_assertt &);
+  void synth_assume(const verilog_assumet &);
+  void synth_prepostincdec(const verilog_statementt &);
   void synth_assignments(transt &);
 
   exprt make_supply_value(const irep_idt &decl_class, const typet &);
@@ -259,8 +260,8 @@ class verilog_synthesist:
     const exprt &case_operand);
 
   void expand_module_instance(
-    const symbolt &symbol,
-    const exprt &op,
+    const symbolt &module_symbol,
+    const verilog_instt::instancet &,
     transt &trans);
 
   void expand_hierarchical_identifier(

src/verilog/verilog_typecheck.cpp

@@ -571,9 +571,9 @@ void verilog_typecheckt::convert_inst(verilog_instt &inst)
   }
 
   // get the instance symbols
-  Forall_operands(it, inst)
+  for(auto &instance : inst.instances())
   {
-    const auto instance_name = it->get(ID_instance);
+    const auto instance_name = instance.name();
 
     const irep_idt instance_identifier =
       id2string(module_symbol.name) + "." + id2string(instance_name);
@@ -598,7 +598,7 @@ void verilog_typecheckt::convert_inst(verilog_instt &inst)
       symbol_table_lookup(new_module_identifier);
 
     // check the port connections
-    typecheck_port_connections(*it, parameterized_module_symbol);
+    typecheck_port_connections(instance, parameterized_module_symbol);
   }
 }