Verilog: distinguish packed and unpacked arrays

This adds two new IDs to distinguish packed and unpacked arrays in the
Verilog parse tree.

Author: kroening

src/hw_cbmc_irep_ids.h

@@ -106,9 +106,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

@@ -1202,7 +1202,7 @@ list_of_net_names:
 		{ $$=$1;    mto($$, $3); }
 	;
 
-net_name: net_identifier packed_dimension_brace
+net_name: net_identifier unpacked_dimension_brace
           {
             $$=$1;
             stack_expr($$).id(ID_declarator);
@@ -1707,7 +1707,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));
@@ -1717,13 +1717,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

@@ -222,7 +222,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
         if(declarator.type().is_nil())
           symbol.type = type;
-        else if(declarator.type().id() == ID_array)
+        else if(declarator.type().id() == ID_verilog_unpacked_array)
           symbol.type = array_type(declarator.type(), type);
         else
         {
@@ -401,7 +401,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
       if(declarator.type().is_nil())
         symbol.type = type;
-      else if(declarator.type().id() == ID_array)
+      else if(declarator.type().id() == ID_verilog_unpacked_array)
         symbol.type = array_type(declarator.type(), type);
       else
       {
@@ -468,7 +468,7 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl)
 
       if(declarator.type().is_nil())
         symbol.type = type;
-      else if(declarator.type().id() == ID_array)
+      else if(declarator.type().id() == ID_verilog_unpacked_array)
         symbol.type = array_type(declarator.type(), type);
       else
       {

src/verilog/verilog_typecheck.cpp

@@ -44,7 +44,7 @@ array_typet verilog_typecheckt::array_type(
 {
   // int whatnot[x:y];
   // 'src' is yet to be converted, but 'element_type' is already converted.
-  PRECONDITION(src.id() == ID_array);
+  PRECONDITION(src.id() == ID_verilog_unpacked_array);
 
   // Unpacked arrays may have a range [x:y],
   // or a size [s], equivalent to [0:s-1]

src/verilog/verilog_typecheck_type.cpp

@@ -115,7 +115,7 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
     result.set(ID_C_identifier, enum_type.identifier());
     return result.with_source_location(source_location);
   }
-  else if(src.id() == ID_array)
+  else if(src.id() == ID_verilog_packed_array)
   {
     const exprt &range=static_cast<const exprt &>(src.find(ID_range));
 
@@ -151,7 +151,8 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
     }
     else
     {
-      // we have a genuine array, and do a recursive call
+      // We have a multi-dimensional packed array,
+      // and do a recursive call.
       const exprt size=from_integer(width, integer_typet());
       typet s=convert_type(subtype);
 
@@ -162,6 +163,11 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
       return std::move(result).with_source_location(source_location);
     }
   }
+  else if(src.id() == ID_verilog_unpacked_array)
+  {
+    // not expected here -- these stick to the declarators
+    PRECONDITION(false);
+  }
   else if(src.id() == ID_verilog_type_reference)
   {
     auto &type_reference = to_verilog_type_reference(src);