SystemVerilog: associative arrays

Author: kroening

src/hw_cbmc_irep_ids.h

@@ -78,6 +78,7 @@ IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)
 IREP_ID_ONE(verilog_array_range)
 IREP_ID_ONE(verilog_assignment_pattern)
+IREP_ID_ONE(verilog_associative_array)
 IREP_ID_ONE(verilog_declarations)
 IREP_ID_ONE(verilog_lifetime)
 IREP_ID_ONE(verilog_logical_equality)

src/verilog/parser.y

@@ -1979,6 +1979,24 @@ packed_dimension:
 	| unsized_dimension
 	;
 
+associative_dimension:
+	  '[' data_type ']'
+		{ init($$, ID_verilog_associative_array);
+		  // for the element type
+		  stack_type($$).add_subtype().make_nil();
+		}
+	| '[' '*' ']'
+		{ init($$, ID_verilog_associative_array);
+		  // for the element type
+		  stack_type($$).add_subtype().make_nil();
+		}
+	| "[*" ']'
+		{ init($$, ID_verilog_associative_array);
+		  // for the element type
+		  stack_type($$).add_subtype().make_nil();
+		}
+	;
+
 unpacked_dimension:
 	  '[' const_expression TOK_COLON const_expression ']'
 		{ init($$, ID_verilog_unpacked_array);
@@ -1997,6 +2015,7 @@ unpacked_dimension:
 variable_dimension:
 	  unsized_dimension
 	| unpacked_dimension
+	| associative_dimension
 	;
 
 variable_dimension_brace:

src/verilog/verilog_elaborate_type.cpp

@@ -177,6 +177,13 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
     // one bit, unsigned
     return unsignedbv_typet{1}.with_source_location(source_location);
   }
+  else if(src.id() == ID_verilog_associative_array)
+  {
+    // The subtype is the element type.
+    auto tmp = to_type_with_subtype(src);
+    tmp.subtype() = elaborate_type(tmp.subtype());
+    return std::move(tmp);
+  }
   else if(src.id() == ID_verilog_byte)
   {
     return signedbv_typet{8}.with_source_location(source_location);

src/verilog/verilog_expr.cpp

@@ -33,10 +33,16 @@ typet verilog_declaratort::merged_type(const typet &declaration_type) const
   typet result = type();
   typet *p = &result;
 
-  while(p->id() == ID_verilog_unpacked_array)
+  while(p->id() == ID_verilog_unpacked_array ||
+        p->id() == ID_verilog_associative_array)
+  {
     p = &to_type_with_subtype(*p).subtype();
+  }
+
+  DATA_INVARIANT(
+    p->is_nil(),
+    "merged_type only works on unpacked arrays and associative arrays");
 
-  DATA_INVARIANT(p->is_nil(), "merged_type only works on unpacked arrays");
   *p = declaration_type;
 
   return result;