Verilog: use direction field instead of input/output for module_typet

This replaces the boolean input and output fields of the port class by a
single field direction, to enable ref ports.

Author: kroening

src/ebmc/output_verilog.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <verilog/verilog_language.h>
 #include <verilog/verilog_synthesis.h>
 #include <verilog/verilog_typecheck.h>
+#include <verilog/verilog_types.h>
 
 #include "output_verilog.h"
 
@@ -585,17 +586,17 @@ void output_verilog_baset::module_header(const symbolt &symbol)
 {
   out << "module " << symbol.base_name;
 
-  const irept &ports=symbol.type.find(ID_ports);
+  const auto &ports=to_module_type(symbol.type).ports();
 
   //
   // print port in module statement
   //
-  if(!ports.get_sub().empty())
+  if(!ports.empty())
   {
     out << '(';
 
     bool first = true;
-    for(auto &port : ports.get_sub())
+    for(auto &port : ports)
     {
       if(first)
         first = false;
@@ -615,10 +616,10 @@ void output_verilog_baset::module_header(const symbolt &symbol)
   //
   // port declarations
   //
-  for(auto &port : ports.get_sub())
+  for(auto &port : ports)
   {
-    bool is_input = port.get_bool(ID_input);
-    bool is_output = port.get_bool(ID_output);
+    bool is_input = port.input();
+    bool is_output = port.output();
 
     out << "  ";
 
@@ -629,7 +630,7 @@ void output_verilog_baset::module_header(const symbolt &symbol)
     else
       out << "output";
 
-    const typet &type = static_cast<const typet &>(port.find(ID_type));
+    const typet &type = port.type();
 
     if(type.id()==ID_named_block)
       continue;

src/ebmc/transition_system.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <langapi/mode.h>
 #include <trans-word-level/show_module_hierarchy.h>
 #include <trans-word-level/show_modules.h>
+#include <verilog/verilog_types.h>
 
 #include "ebmc_error.h"
 #include "ebmc_version.h"
@@ -424,17 +425,15 @@ std::vector<symbol_exprt> transition_systemt::inputs() const
   DATA_INVARIANT(
     module_symbol.type.id() == ID_module, "main_symbol must be module");
 
-  const auto &ports_irep = module_symbol.type.find(ID_ports);
-
   // filter out the inputs
-  auto &ports = static_cast<const exprt &>(ports_irep).operands();
+  auto &ports = to_module_type(module_symbol.type).ports();
   for(auto &port : ports)
   {
     DATA_INVARIANT(port.id() == ID_symbol, "port must be a symbol");
-    if(port.get_bool(ID_input) && !port.get_bool(ID_output))
+    if(port.input() && !port.output())
     {
       symbol_exprt input_symbol(
-        to_symbol_expr(port).get_identifier(), port.type());
+        port.identifier(), port.type());
       input_symbol.add_source_location() = port.source_location();
       inputs.push_back(std::move(input_symbol));
     }

src/hw_cbmc_irep_ids.h

@@ -107,6 +107,7 @@ IREP_ID_ONE(module_instance)
 IREP_ID_TWO(C_const, #const)
 IREP_ID_TWO(C_offset, #offset)
 IREP_ID_TWO(C_increasing, #increasing)
+IREP_ID_ONE(direction)
 IREP_ID_ONE(ports)
 IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)

src/verilog/verilog_interfaces.cpp

@@ -98,11 +98,7 @@ void verilog_typecheckt::check_module_ports(
         << "port `" << base_name << "' not declared as input or output";
     }
 
-    ports.emplace_back(
-      identifier,
-      port_symbol->type,
-      port_symbol->is_input,
-      port_symbol->is_output);
+    ports.emplace_back(identifier, port_symbol->type, decl.get_class());
 
     ports.back().set("#name", base_name);
     ports.back().set(ID_C_source_location, declarator.source_location());

src/verilog/verilog_types.h

@@ -145,13 +145,12 @@ class module_typet:public typet
   class portt : public irept
   {
   public:
-    portt(irep_idt _identifier, typet _type, bool _input, bool _output)
+    portt(irep_idt _identifier, typet _type, irep_idt _direction)
       : irept(ID_symbol)
     {
-      type() = std::move(_type);
       identifier(_identifier);
-      input(_input);
-      output(_output);
+      type() = std::move(_type);
+      direction(_direction);
     }
 
     typet &type()
@@ -174,24 +173,29 @@ class module_typet:public typet
       set(ID_identifier, _identifier);
     }
 
-    bool output() const
+    irep_idt direction() const
+    {
+      return get(ID_direction);
+    }
+
+    void direction(irep_idt _direction)
     {
-      return get_bool(ID_output);
+      set(ID_direction, _direction);
     }
 
-    void output(bool _output)
+    bool output() const
     {
-      set(ID_output, _output);
+      return direction() == ID_output || direction() == ID_inout;
     }
 
     bool input() const
     {
-      return get_bool(ID_input);
+      return direction() == ID_input || direction() == ID_inout;
     }
 
-    void input(bool _input)
+    const source_locationt &source_location() const
     {
-      set(ID_input, _input);
+      return (const source_locationt &)find(ID_C_source_location);
     }
   };