Merge pull request #1275 from diffblue/module-type-ports

Verilog: strengthen typing when using module type

Author: kroening

src/verilog/verilog_interfaces.cpp

@@ -50,8 +50,9 @@ Function: verilog_typecheckt::check_module_ports
 void verilog_typecheckt::check_module_ports(
   const verilog_module_sourcet::port_listt &module_ports)
 {
-  auto &ports = module_symbol.type.add(ID_ports).get_sub();
-  ports.resize(module_ports.size());
+  auto &ports = to_module_type(module_symbol.type).ports();
+  ports.clear();
+  ports.reserve(module_ports.size());
   std::map<irep_idt, unsigned> port_names;
 
   unsigned nr=0;
@@ -97,19 +98,22 @@ void verilog_typecheckt::check_module_ports(
         << "port `" << base_name << "' not declared as input or output";
     }
 
-    ports[nr].set("#name", base_name);
-    ports[nr].id(ID_symbol);
-    ports[nr].set(ID_identifier, identifier);
-    ports[nr].set(ID_C_source_location, declarator.source_location());
-    ports[nr].set(ID_type, port_symbol->type);
-    ports[nr].set(ID_input, port_symbol->is_input);
-    ports[nr].set(ID_output, port_symbol->is_output);
+    ports.emplace_back(
+      identifier,
+      port_symbol->type,
+      port_symbol->is_input,
+      port_symbol->is_output);
+
+    ports.back().set("#name", base_name);
+    ports.back().set(ID_C_source_location, declarator.source_location());
 
     port_names[base_name] = nr;
 
     nr++;
   }
 
+  DATA_INVARIANT(ports.size() == module_ports.size(), "number of ports");
+
   // check that all declared ports are also in the port list
 
   for(auto it=symbol_table.symbol_module_map.lower_bound(module_identifier);

src/verilog/verilog_synthesis.cpp

@@ -1349,14 +1349,13 @@ Function: verilog_synthesist::instantiate_port
 \*******************************************************************/
 
 void verilog_synthesist::instantiate_port(
-  bool is_output,
-  const symbol_exprt &port,
+  const module_typet::portt &port,
   const exprt &value,
   const replace_mapt &replace_map,
   const source_locationt &source_location,
   transt &trans)
 {
-  irep_idt port_identifier = port.get_identifier();
+  irep_idt port_identifier = port.identifier();
 
   replace_mapt::const_iterator it = replace_map.find(port_identifier);
 
@@ -1372,7 +1371,7 @@ void verilog_synthesist::instantiate_port(
   // Note that the types need not match.
   exprt lhs, rhs;
 
-  if(is_output)
+  if(port.output())
   {
     lhs = value;
     rhs = typecast_exprt::conditional_cast(it->second, value.type());
@@ -1417,31 +1416,29 @@ void verilog_synthesist::instantiate_ports(
   if(inst.connections().empty())
     return;
 
+  auto &module_type = to_module_type(symbol.type);
+
   // named port connection?
 
   if(inst.named_port_connections())
   {
-    const irept::subt &ports = symbol.type.find(ID_ports).get_sub();
-
-    std::set<irep_idt> output_identifiers;
-    for(auto &port : ports)
-      if(port.get_bool(ID_output))
-        output_identifiers.insert(
-          to_symbol_expr((const exprt &)(port)).get_identifier());
+    const auto &ports = module_type.ports();
+    auto port_map = module_type.port_map();
 
     // no requirement that all ports are connected
     for(const auto &connection : inst.connections())
     {
       auto &named_connection = to_verilog_named_port_connection(connection);
-      const auto &port = to_symbol_expr(named_connection.port());
+      auto port_it =
+        port_map.find(to_symbol_expr(named_connection.port()).get_identifier());
+      CHECK_RETURN(port_it != port_map.end());
+      auto &port = port_it->second;
       const exprt &value = named_connection.value();
 
       if(value.is_not_nil())
       {
-        bool is_output = output_identifiers.find(port.get_identifier()) !=
-                         output_identifiers.end();
         instantiate_port(
-          is_output, port, value, replace_map, inst.source_location(), trans);
+          port, value, replace_map, inst.source_location(), trans);
       }
     }
 
@@ -1456,17 +1453,15 @@ void verilog_synthesist::instantiate_ports(
 
     // unconnected inputs may be given a default value
     for(auto &port : ports)
-      if(port.get_bool(ID_input))
+      if(port.input())
       {
-        auto &port_symbol_expr = to_symbol_expr((const exprt &)(port));
-        auto identifier = port_symbol_expr.get_identifier();
+        auto identifier = port.identifier();
         if(connected_ports.find(identifier) == connected_ports.end())
         {
-          auto &port_symbol = ns.lookup(port_symbol_expr);
+          auto &port_symbol = ns.lookup(identifier);
           if(port_symbol.value.is_not_nil())
             instantiate_port(
-              false,
-              port_symbol_expr,
+              port,
               port_symbol.value,
               replace_map,
               inst.source_location(),
@@ -1476,7 +1471,7 @@ void verilog_synthesist::instantiate_ports(
   }
   else // just a list without names
   {
-    const irept::subt &ports = symbol.type.find(ID_ports).get_sub();
+    const auto &ports = module_type.ports();
 
     if(inst.connections().size() != ports.size())
     {
@@ -1485,24 +1480,15 @@ void verilog_synthesist::instantiate_ports(
         << inst.connections().size();
     }
 
-    irept::subt::const_iterator p_it=
-      ports.begin();
+    auto p_it = ports.begin();
 
     for(const auto &connection : inst.connections())
     {
       DATA_INVARIANT(connection.is_not_nil(), "all ports must be connected");
 
-      auto &port = to_symbol_expr((const exprt &)(*p_it));
-
-      bool is_output = port.get_bool(ID_output);
-
       instantiate_port(
-        is_output,
-        port,
-        connection,
-        replace_map,
-        inst.source_location(),
-        trans);
+        *p_it, connection, replace_map, inst.source_location(), trans);
+
       p_it++;
     }
   }

src/verilog/verilog_synthesis_class.h

@@ -326,8 +326,7 @@ class verilog_synthesist:
   void replace_symbols(const irep_idt &target, exprt &dest);
 
   void instantiate_port(
-    bool is_output,
-    const symbol_exprt &port,
+    const module_typet::portt &,
     const exprt &value,
     const replace_mapt &,
     const source_locationt &,

src/verilog/verilog_typecheck.cpp

@@ -39,10 +39,9 @@ Function: verilog_typecheckt::typecheck_port_connection
 
 void verilog_typecheckt::typecheck_port_connection(
   exprt &op,
-  const exprt &port)
+  const module_typet::portt &port)
 {
-  const symbolt &symbol=
-    ns.lookup(port.get(ID_identifier));
+  const symbolt &symbol = ns.lookup(port.identifier());
 
   if(!symbol.is_input && !symbol.is_output)
   {
@@ -101,7 +100,7 @@ void verilog_typecheckt::typecheck_port_connections(
   else
     range = convert_range(range_expr);
 
-  const irept::subt &ports=symbol.type.find(ID_ports).get_sub();
+  const auto &ports = to_module_type(symbol.type).ports();
 
   // no connection is one connection that is nil
   if(inst.connections().size() == 1 && inst.connections().front().is_nil())
@@ -148,10 +147,9 @@ void verilog_typecheckt::typecheck_port_connections(
       {
         if(port.get(ID_identifier) == identifier)
         {
-          auto &p_expr = static_cast<const exprt &>(port);
           found=true;
-          typecheck_port_connection(value, p_expr);
-          named_port_connection.port().type() = p_expr.type();
+          typecheck_port_connection(value, port);
+          named_port_connection.port().type() = port.type();
           break;
         }
       }
@@ -174,12 +172,11 @@ void verilog_typecheckt::typecheck_port_connections(
         << " but got " << inst.connections().size();
     }
 
-    irept::subt::const_iterator p_it=
-      ports.begin();
+    auto p_it = ports.begin();
 
     for(auto &connection : inst.connections())
     {
-      typecheck_port_connection(connection, (exprt &)*p_it);
+      typecheck_port_connection(connection, *p_it);
       p_it++;
     }
   }

src/verilog/verilog_typecheck.h

@@ -202,9 +202,7 @@ class verilog_typecheckt:
 
   void typecheck_builtin_port_connections(verilog_inst_baset::instancet &);
 
-  void typecheck_port_connection(
-    exprt &op,
-    const exprt &port);
+  void typecheck_port_connection(exprt &op, const module_typet::portt &);
 
   bool replace_symbols(const replace_mapt &what, exprt &dest);
   void replace_symbols(const std::string &target, exprt &dest);

src/verilog/verilog_types.h

@@ -141,8 +141,109 @@ class module_typet:public typet
   inline module_typet():typet(ID_module)
   {
   }
+
+  class portt : public irept
+  {
+  public:
+    portt(irep_idt _identifier, typet _type, bool _input, bool _output)
+      : irept(ID_symbol)
+    {
+      type() = std::move(_type);
+      identifier(_identifier);
+      input(_input);
+      output(_output);
+    }
+
+    typet &type()
+    {
+      return static_cast<typet &>(add(ID_type));
+    }
+
+    const typet &type() const
+    {
+      return static_cast<const typet &>(find(ID_type));
+    }
+
+    irep_idt identifier() const
+    {
+      return get(ID_identifier);
+    }
+
+    void identifier(irep_idt _identifier)
+    {
+      set(ID_identifier, _identifier);
+    }
+
+    bool output() const
+    {
+      return get_bool(ID_output);
+    }
+
+    void output(bool _output)
+    {
+      set(ID_output, _output);
+    }
+
+    bool input() const
+    {
+      return get_bool(ID_input);
+    }
+
+    void input(bool _input)
+    {
+      set(ID_input, _input);
+    }
+  };
+
+  using portst = std::vector<portt>;
+
+  portst &ports()
+  {
+    return (portst &)(add(ID_ports).get_sub());
+  }
+
+  const portst &ports() const
+  {
+    return (const portst &)(find(ID_ports).get_sub());
+  }
+
+  using port_mapt = std::unordered_map<irep_idt, portt, irep_id_hash>;
+
+  port_mapt port_map() const
+  {
+    port_mapt result;
+    auto &ports = this->ports();
+    for(auto &port : ports)
+      result.emplace(port.identifier(), port);
+    return result;
+  }
 };
 
+/*! \brief Cast a generic typet to a \ref module_typet
+ *
+ * This is an unchecked conversion. \a type must be known to be \ref
+ * module_typet.
+ *
+ * \param type Source type
+ * \return Object of type \ref module_typet
+ *
+ * \ingroup gr_std_types
+*/
+inline const module_typet &to_module_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_module);
+  return static_cast<const module_typet &>(type);
+}
+
+/*! \copydoc to_module_type(const typet &)
+ * \ingroup gr_std_types
+*/
+inline module_typet &to_module_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_module);
+  return static_cast<module_typet &>(type);
+}
+
 class verilog_genvar_typet : public typet
 {
 public: