Merge pull request #1271 from diffblue/ref1

Verilog: `ref` port direction

Author: tautschnig

CHANGELOG

@@ -7,6 +7,7 @@
 * Verilog: $isunknown
 * SystemVerilog: fix for #-# and #=# for empty matches
 * SystemVerilog: fix for |-> and |=> for empty matches
+* SystemVerilog: ref module port direction
 * LTL/SVA to Buechi with --buechi
 * SMV: abs, bool, count, max, min, toint, word1
 * BMC: new encoding for F, avoiding spurious traces

regression/verilog/modules/ref1.desc

@@ -0,0 +1,7 @@
+CORE
+ref1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/modules/ref1.sv

@@ -0,0 +1,9 @@
+module M(ref [31:0] some_ref);
+  initial some_ref = 123;
+endmodule
+
+module main;
+  bit [31:0] some_var;
+  M m(some_var);
+  assert final (some_var == 123);
+endmodule

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,14 @@ 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());
+      symbol_exprt input_symbol(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_elaborate.cpp

@@ -56,6 +56,14 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl)
       new_symbol.is_input = true;
       new_symbol.is_output = true;
     }
+    else if(port_class == ID_verilog_ref)
+    {
+      new_symbol.is_input = false;
+      new_symbol.is_output = false;
+      new_symbol.is_state_var = true;
+    }
+    else
+      DATA_INVARIANT(false, "unexpected port class");
 
     new_symbol.module = module_identifier;
     new_symbol.value.make_nil();

src/verilog/verilog_interfaces.cpp

@@ -92,17 +92,24 @@ void verilog_typecheckt::check_module_ports(
         << "port `" << base_name << "' not declared";
     }
 
-    if(!port_symbol->is_input && !port_symbol->is_output)
+    irep_idt direction = decl.get_class();
+
+    if(direction.empty())
     {
-      throw errort().with_location(declarator.source_location())
-        << "port `" << base_name << "' not declared as input or output";
+      if(!port_symbol->is_input && !port_symbol->is_output)
+      {
+        throw errort().with_location(declarator.source_location())
+          << "port `" << base_name << "' not declared as input or output";
+      }
+      else if(port_symbol->is_input && !port_symbol->is_output)
+        direction = ID_input;
+      else if(!port_symbol->is_input && port_symbol->is_output)
+        direction = ID_output;
+      else
+        direction = ID_inout;
     }
 
-    ports.emplace_back(
-      identifier,
-      port_symbol->type,
-      port_symbol->is_input,
-      port_symbol->is_output);
+    ports.emplace_back(identifier, port_symbol->type, direction);
 
     ports.back().set("#name", base_name);
     ports.back().set(ID_C_source_location, declarator.source_location());

src/verilog/verilog_typecheck.cpp

@@ -43,10 +43,13 @@ void verilog_typecheckt::typecheck_port_connection(
 {
   const symbolt &symbol = ns.lookup(port.identifier());
 
-  if(!symbol.is_input && !symbol.is_output)
+  if(port.direction() != ID_verilog_ref)
   {
-    throw errort().with_location(op.source_location())
-      << "port `" << symbol.name << "' is neither input nor output";
+    if(!symbol.is_input && !symbol.is_output)
+    {
+      throw errort().with_location(op.source_location())
+        << "port `" << symbol.name << "' is neither input nor output";
+    }
   }
 
   if(op.is_nil())

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,34 @@ class module_typet:public typet
       set(ID_identifier, _identifier);
     }
 
-    bool output() const
+    irep_idt direction() const
     {
-      return get_bool(ID_output);
+      return get(ID_direction);
     }
 
-    void output(bool _output)
+    void direction(irep_idt _direction)
     {
-      set(ID_output, _output);
+      set(ID_direction, _direction);
+    }
+
+    bool output() const
+    {
+      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)
+    bool ref() const
+    {
+      return direction() == ID_verilog_ref;
+    }
+
+    const source_locationt &source_location() const
     {
-      set(ID_input, _input);
+      return (const source_locationt &)find(ID_C_source_location);
     }
   };