Verilog: distinguish packed and unpacked arrays

regression/verilog/arrays/packed_real1.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+packed_real1.sv
+--module main --bound 0
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+A packed array of reals must be rejected.

regression/verilog/arrays/packed_real1.sv

@@ -0,0 +1,9 @@
+module main;
+
+  // Packed arrays can be made of single bit data types
+  // or other packed types.
+  typedef real my_real;
+  my_real [7:0] my_array;
+
+endmodule
+

regression/verilog/arrays/packed_typedef1.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+packed_typedef1.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The packed array type must not be dropped.

regression/verilog/arrays/packed_typedef1.sv

@@ -0,0 +1,8 @@
+module main;
+
+  typedef bit my_bit;
+  my_bit [7:0] my_vector;
+
+  always assert p0: ($bits(my_vector) == 8);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -110,9 +110,11 @@ IREP_ID_ONE(wire)
 IREP_ID_ONE(uwire)
 IREP_ID_ONE(wand)
 IREP_ID_ONE(automatic)
-IREP_ID_ONE(verilog_enum)
 IREP_ID_TWO(C_verilog_type, #verilog_type)
+IREP_ID_ONE(verilog_enum)
+IREP_ID_ONE(verilog_packed_array)
 IREP_ID_ONE(verilog_type_reference)
+IREP_ID_ONE(verilog_unpacked_array)
 IREP_ID_ONE(enum_names)
 IREP_ID_ONE(var)
 IREP_ID_ONE(trireg)

src/verilog/parser.y

@@ -826,23 +826,29 @@ module_port_input_declaration:
 	  TOK_INPUT net_port_type port_identifier unpacked_dimension_brace
 		{ init($$, ID_decl);
                   stack_expr($$).set(ID_class, ID_input);
-                  add_as_subtype(stack_type($4), stack_type($2));
-                  addswap($$, ID_type, $4);
+                  // The net_port_type goes onto the declaration,
+                  // and the unpacked_array_type goes onto the declarator.
+                  addswap($$, ID_type, $2);
+                  addswap($3, ID_type, $4);
                   mto($$, $3); }
 	;
 
 module_port_output_declaration:
 	  TOK_OUTPUT net_port_type port_identifier unpacked_dimension_brace
 		{ init($$, ID_decl);
                   stack_expr($$).set(ID_class, ID_output);
-                  add_as_subtype(stack_type($4), stack_type($2));
-                  addswap($$, ID_type, $4);
+                  // The data_type goes onto the declaration,
+                  // and the unpacked_array_type goes onto the declarator.
+                  addswap($$, ID_type, $2);
+                  addswap($3, ID_type, $4);
                   mto($$, $3); }
 	| TOK_OUTPUT data_type port_identifier unpacked_dimension_brace
 		{ init($$, ID_decl);
                   stack_expr($$).set(ID_class, ID_output_register);
-                  add_as_subtype(stack_type($4), stack_type($2));
-                  addswap($$, ID_type, $4);
+                  // The data_type goes onto the declaration,
+                  // and the unpacked_array_type goes onto the declarator.
+                  addswap($$, ID_type, $2);
+                  addswap($3, ID_type, $4);
                   mto($$, $3); }
 	;
 
@@ -1173,12 +1179,7 @@ genvar_declaration:
 	;
 
 net_declaration:
-          net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_names ';'
-		{ init($$, ID_decl);
-                  addswap($$, ID_class, $1);
-                  addswap($$, ID_type, $4);
-                  swapop($$, $6); }
-        | net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_decl_assignments ';'
+          net_type drive_strength_opt vectored_scalared_opt data_type_or_implicit delay3_opt list_of_net_decl_assignments ';'
 		{ init($$, ID_decl);
                   addswap($$, ID_class, $1);
                   addswap($$, ID_type, $4);
@@ -1208,21 +1209,6 @@ vectored_scalared_opt:
 	| TOK_SCALARED     { init($$, "scalared"); }
 	;
 
-list_of_net_names:
-	  net_name
-		{ init($$); mto($$, $1); }
-	| list_of_net_names ',' net_name
-		{ $$=$1;    mto($$, $3); }
-	;
-
-net_name: net_identifier packed_dimension_brace
-          {
-            $$=$1;
-            stack_expr($$).id(ID_declarator);
-            addswap($$, ID_type, $2);
-          }
-	;
-
 list_of_net_decl_assignments:
 	  net_decl_assignment
 		{ init($$); mto($$, $1); }
@@ -1285,7 +1271,9 @@ data_type:
 	| TOK_VIRTUAL interface_opt interface_identifier
 	        { init($$, "virtual_interface"); }
 	| /*scope_opt*/ type_identifier packed_dimension_brace
-		{ $$ = $1; stack_expr($$).id(ID_typedef_type); }
+		{ stack_expr($1).id(ID_typedef_type);
+                  add_as_subtype(stack_type($2), stack_type($1));
+                  $$ = $2; }
 //	| class_type
 	| TOK_EVENT
 	        { init($$, ID_event); }
@@ -1700,8 +1688,16 @@ range:	part_select;
 // System Verilog standard 1800-2017
 // A.2.4 Declaration assignments
 
-net_decl_assignment: net_identifier '=' expression
-		{ $$ = $1; stack_expr($$).id(ID_declarator); addswap($$, ID_value, $3); }
+net_decl_assignment:
+	  net_identifier unpacked_dimension_brace
+		{ $$ = $1;
+		  stack_expr($$).id(ID_declarator);
+		  addswap($$, ID_type, $2); }
+	| net_identifier unpacked_dimension_brace '=' expression
+		{ $$ = $1;
+		  stack_expr($$).id(ID_declarator);
+		  addswap($$, ID_type, $2);
+		  addswap($$, ID_value, $4); }
 	;
 
 variable_decl_assignment:
@@ -1734,7 +1730,7 @@ packed_dimension_opt:
 
 packed_dimension:
 	  '[' const_expression TOK_COLON const_expression ']'
-		{ init($$, ID_array);
+		{ init($$, ID_verilog_packed_array);
 		  stack_type($$).add_subtype().make_nil();
 		  exprt &range=static_cast<exprt &>(stack_type($$).add(ID_range));
 		  range.add_to_operands(stack_expr($2));
@@ -1744,13 +1740,14 @@ packed_dimension:
 
 unpacked_dimension:
 	  '[' const_expression TOK_COLON const_expression ']'
-		{ init($$, ID_array);
+		{ init($$, ID_verilog_unpacked_array);
 		  stack_type($$).add_subtype().make_nil();
 		  exprt &range=static_cast<exprt &>(stack_type($$).add(ID_range));
 		  range.add_to_operands(stack_expr($2));
 		  range.add_to_operands(stack_expr($4)); }
 	| '[' expression ']'
-		{ init($$, ID_array);
+		{ // starts at index 0
+		  init($$, ID_verilog_unpacked_array);
 		  stack_type($$).add_subtype().make_nil();
 		  stack_type($$).set(ID_size, std::move(stack_expr($2)));
 		}

src/verilog/verilog_elaborate.cpp

@@ -24,7 +24,9 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl)
 
   const irep_idt &base_name = declarator.base_name();
   const irep_idt &port_class = decl.get_class();
+
   auto type = convert_type(decl.type());
+
   irep_idt identifier = hierarchical_identifier(base_name);
 
   if(port_class.empty())
@@ -34,7 +36,18 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl)
   else
   {
     // add the symbol
-    symbolt new_symbol(identifier, type, mode);
+    typet final_type;
+    if(declarator.type().is_nil())
+      final_type = type;
+    else if(declarator.type().id() == ID_verilog_unpacked_array)
+      final_type = unpacked_array_type(declarator.type(), type);
+    else
+    {
+      throw errort().with_location(declarator.source_location())
+        << "unexpected type on declarator";
+    }
+
+    symbolt new_symbol(identifier, final_type, mode);
 
     if(port_class == ID_input)
     {
@@ -222,8 +235,8 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
         if(declarator.type().is_nil())
           symbol.type = type;
-        else if(declarator.type().id() == ID_array)
-          symbol.type = array_type(declarator.type(), type);
+        else if(declarator.type().id() == ID_verilog_unpacked_array)
+          symbol.type = unpacked_array_type(declarator.type(), type);
         else
         {
           throw errort().with_location(declarator.source_location())
@@ -315,7 +328,15 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
             << "empty symbol name";
         }
 
-        symbol.type = type;
+        if(declarator.type().is_nil())
+          symbol.type = type;
+        else if(declarator.type().id() == ID_verilog_unpacked_array)
+          symbol.type = unpacked_array_type(declarator.type(), type);
+        else
+        {
+          throw errort().with_location(declarator.source_location())
+            << "unexpected type on declarator";
+        }
 
         symbol.name = hierarchical_identifier(symbol.base_name);
 
@@ -401,8 +422,8 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
       if(declarator.type().is_nil())
         symbol.type = type;
-      else if(declarator.type().id() == ID_array)
-        symbol.type = array_type(declarator.type(), type);
+      else if(declarator.type().id() == ID_verilog_unpacked_array)
+        symbol.type = unpacked_array_type(declarator.type(), type);
       else
       {
         throw errort().with_location(symbol.location)
@@ -468,8 +489,8 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
       if(declarator.type().is_nil())
         symbol.type = type;
-      else if(declarator.type().id() == ID_array)
-        symbol.type = array_type(declarator.type(), type);
+      else if(declarator.type().id() == ID_verilog_unpacked_array)
+        symbol.type = unpacked_array_type(declarator.type(), type);
       else
       {
         throw errort().with_location(symbol.location)

src/verilog/verilog_typecheck.cpp

@@ -28,80 +28,6 @@ Author: Daniel Kroening, [email protected]
 
 /*******************************************************************\
 
-Function: verilog_typecheckt::array_type
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-array_typet verilog_typecheckt::array_type(
-  const irept &src,
-  const typet &element_type)
-{
-  // int whatnot[x:y];
-  // 'src' is yet to be converted, but 'element_type' is already converted.
-  PRECONDITION(src.id() == ID_array);
-
-  // Unpacked arrays may have a range [x:y],
-  // or a size [s], equivalent to [0:s-1]
-  const exprt &range_expr = static_cast<const exprt &>(src.find(ID_range));
-  const exprt &size_expr = static_cast<const exprt &>(src.find(ID_size));
-
-  mp_integer size, offset;
-  bool little_endian;
-
-  if(range_expr.is_not_nil())
-  {
-    // these may be negative
-    mp_integer msb, lsb;
-    convert_range(range_expr, msb, lsb);
-    little_endian = (lsb <= msb);
-    size = (little_endian ? msb - lsb : lsb - msb) + 1;
-    offset = little_endian ? lsb : msb;
-  }
-  else if(size_expr.is_not_nil())
-  {
-    little_endian = true;
-    size = convert_integer_constant_expression(size_expr);
-    offset = 0;
-    if(size < 0)
-    {
-      throw errort().with_location(size_expr.find_source_location())
-        << "array size must be nonnegative";
-    }
-  }
-  else
-  {
-    throw errort() << "array must have range or size";
-  }
-
-  const typet src_subtype =
-    static_cast<const typet &>(src).has_subtype()
-      ? static_cast<const type_with_subtypet &>(src).subtype()
-      : typet(ID_nil);
-
-  typet array_subtype;
-
-  // may need to go recursive
-  if(src_subtype.is_nil())
-    array_subtype=element_type;
-  else
-    array_subtype=array_type(src_subtype, element_type);
-
-  const exprt final_size_expr = from_integer(size, integer_typet());
-  array_typet result(array_subtype, final_size_expr);
-  result.set(ID_offset, from_integer(offset, integer_typet()));
-  result.set(ID_C_little_endian, little_endian);
-
-  return result;
-}
-
-/*******************************************************************\
-
 Function: verilog_typecheckt::typecheck_port_connection
 
   Inputs:

src/verilog/verilog_typecheck.h

@@ -125,10 +125,6 @@ class verilog_typecheckt:
   void interface_generate_block(const class verilog_generate_blockt &);
   void interface_statement(const class verilog_statementt &);
 
-  array_typet array_type(
-    const irept &src,
-    const typet &element_type);
-
   // type checking
 
   typedef enum { A_CONTINUOUS, A_BLOCKING, A_NON_BLOCKING } vassignt;

src/verilog/verilog_typecheck_expr.h

@@ -64,6 +64,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 
   typet convert_type(const typet &);
   typet convert_enum(const class verilog_enum_typet &);
+  array_typet unpacked_array_type(const typet &src, const typet &element_type);
 
   void convert_range(
     const exprt &range,