Verilog: function/task ports

This adds support for port declarations as part of the function/task header.

regression/verilog/functioncall/function_ports1.desc

@@ -0,0 +1,8 @@
+CORE
+function_ports1.v
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.property\.test16\] always .*: PROVED up to bound 0$
+--
+^warning: ignoring

regression/verilog/functioncall/function_ports1.v

@@ -0,0 +1,16 @@
+module main;
+
+  function [31:0] clog2(input [63:0] value);
+  reg [63:0] tmp;
+  begin
+    tmp = value - 1;
+    for (clog2 = 0; tmp>0; clog2 = clog2 + 32'h1)
+      tmp = tmp >> 1;
+  end
+  endfunction // clog2
+
+  wire [31:0] clog2_of_16 = clog2(16);
+
+  always assert test16: clog2_of_16 == 4;
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -123,6 +123,7 @@ IREP_ID_ONE(verilog_longint)
 IREP_ID_ONE(verilog_byte)
 IREP_ID_ONE(verilog_bit)
 IREP_ID_ONE(verilog_logic)
+IREP_ID_ONE(verilog_ref)
 IREP_ID_ONE(verilog_reg)
 IREP_ID_ONE(verilog_integer)
 IREP_ID_ONE(verilog_time)

src/verilog/parser.y

@@ -842,6 +842,17 @@ module_port_output_declaration:
                   mto($$, $3); }
 	;
 
+port_direction:
+	  TOK_INPUT
+		{ init($$, ID_input); }
+	| TOK_OUTPUT
+		{ init($$, ID_output); }
+	| TOK_INOUT
+		{ init($$, ID_inout); }
+	| TOK_REF
+		{ init($$, ID_verilog_ref); }
+	;
+
 // System Verilog standard 1800-2017
 // A.1.4 Module items
 
@@ -1731,20 +1742,38 @@ struct_union:
 // System Verilog standard 1800-2017
 // A.2.6 Function declarations
 
-function_declaration:
-	  TOK_FUNCTION
-	  automatic_opt signing_opt range_or_type_opt
+function_declaration: TOK_FUNCTION automatic_opt function_body_declaration
+		{ $$ = $3; }
+	;
+
+function_body_declaration:
+	  signing_opt range_or_type_opt
 	  function_identifier
-		{ push_scope(stack_expr($5).get(ID_identifier), "."); }
-	  list_of_ports_opt ';'
+		{ push_scope(stack_expr($3).get(ID_identifier), "."); }
+	  ';'
           tf_item_declaration_brace statement
           TOK_ENDFUNCTION
 		{ init($$, ID_decl);
-                  stack_expr($$).set(ID_class, ID_function); 
-                  addswap($$, ID_type, $4);
-                  add_as_subtype(stack_type($4), stack_type($3));
-                  addswap($$, ID_symbol, $5);
-		  addswap($$, ID_ports, $7);
+                  stack_expr($$).set(ID_class, ID_function);
+                  addswap($$, ID_type, $2);
+                  add_as_subtype(stack_type($2), stack_type($1));
+                  addswap($$, ID_symbol, $3);
+		  addswap($$, "declarations", $6);
+		  addswap($$, ID_body, $7);
+		  pop_scope();
+		}
+	| signing_opt range_or_type_opt
+	  function_identifier
+		{ push_scope(stack_expr($3).get(ID_identifier), "."); }
+	  '(' tf_port_list_opt ')' ';'
+          tf_item_declaration_brace statement
+          TOK_ENDFUNCTION
+		{ init($$, ID_decl);
+                  stack_expr($$).set(ID_class, ID_function);
+                  addswap($$, ID_type, $2);
+                  add_as_subtype(stack_type($2), stack_type($1));
+                  addswap($$, ID_symbol, $3);
+		  addswap($$, ID_ports, $6);
 		  addswap($$, "declarations", $9);
 		  addswap($$, ID_body, $10);
 		  pop_scope();
@@ -1793,15 +1822,27 @@ function_prototype: TOK_FUNCTION data_type_or_void function_identifier
 task_declaration:
 	  TOK_TASK task_identifier
 		{ push_scope(stack_expr($2).get(ID_identifier), "."); }
-	  list_of_ports_opt ';'
+	  ';'
 	  tf_item_declaration_brace
 	  statement_or_null TOK_ENDTASK
 		{ init($$, ID_decl);
-                  stack_expr($$).set(ID_class, ID_task); 
+                  stack_expr($$).set(ID_class, ID_task);
 		  addswap($$, ID_symbol, $2);
-		  addswap($$, ID_ports, $4);
-		  addswap($$, "declarations", $6);
-		  addswap($$, ID_body, $7);
+		  addswap($$, "declarations", $5);
+		  addswap($$, ID_body, $6);
+		  pop_scope();
+                }
+	| TOK_TASK task_identifier
+		{ push_scope(stack_expr($2).get(ID_identifier), "."); }
+	  '(' tf_port_list_opt ')' ';'
+	  tf_item_declaration_brace
+	  statement_or_null TOK_ENDTASK
+		{ init($$, ID_decl);
+                  stack_expr($$).set(ID_class, ID_task);
+		  addswap($$, ID_symbol, $2);
+		  addswap($$, ID_ports, $5);
+		  addswap($$, "declarations", $8);
+		  addswap($$, ID_body, $9);
 		  pop_scope();
                 }
 	;
@@ -1809,6 +1850,39 @@ task_declaration:
 task_prototype: TOK_TASK task_identifier
 	;
 
+tf_port_list_opt:
+	/* Optional */
+		{ init($$); }
+	| tf_port_list
+	;
+
+tf_port_list:
+	  tf_port_item
+		{ init($$); mts($$, $1); }
+	| tf_port_list ',' tf_port_item
+		{ $$ = $1; mts($$, $3); }
+	;
+
+tf_port_item:
+	  attribute_instance_brace
+	  tf_port_direction_opt
+	  data_type_or_implicit
+	  port_identifier
+	  variable_dimension_brace
+		{ init($$, ID_decl);
+		  addswap($$, ID_class, $2);
+		  addswap($$, ID_type, $3);
+		  stack_expr($4).id(ID_declarator);
+		  mto($$, $4); }
+	;
+
+tf_port_direction_opt:
+	  /* Optional */
+	| port_direction
+	| TOK_CONST TOK_REF
+		{ $$ = $2; }
+	;
+
 // System Verilog standard 1800-2017
 // A.2.8 Block item declarations
 

src/verilog/verilog_elaborate.cpp

@@ -532,6 +532,15 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
     function_or_task_name = symbol.name;
 
+    // do the ANSI-style ports, if applicable
+    for(auto &port_decl : decl.ports())
+    {
+      // These must have one declarator exactly.
+      DATA_INVARIANT(
+        port_decl.declarators().size() == 1, "must have one port declarator");
+      collect_symbols(port_decl); // rec. call
+    }
+
     // add a symbol for the return value of functions, if applicable
 
     if(decl_class == ID_function)

src/verilog/verilog_expr.h

@@ -689,8 +689,9 @@ public:
 
   // Function and task declarations have:
   // a) an identifier,
-  // b) further declarations,
-  // c) a body.
+  // b) an optional list of ANSI-style ports,
+  // c) further declarations,
+  // d) a body.
   irep_idt get_identifier() const
   {
     return find(ID_symbol).get(ID_identifier);
@@ -701,6 +702,18 @@ public:
     add(ID_symbol).set(ID_identifier, identifier);
   }
 
+  using portst = std::vector<verilog_declt>;
+
+  portst &ports()
+  {
+    return (portst &)(add(ID_ports).get_sub());
+  }
+
+  const portst &ports() const
+  {
+    return (const portst &)(find(ID_ports).get_sub());
+  }
+
   using declarationst = std::vector<verilog_declt>;
 
   declarationst &declarations()