From 6997a06f74f4743f32e72452582b5528801c1443 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 2 Jan 2025 19:46:47 +0000
Subject: [PATCH] SystemVerilog: associative arrays

---
 src/hw_cbmc_irep_ids.h                 |  1 +
 src/verilog/parser.y                   | 19 +++++++++++++++++++
 src/verilog/verilog_elaborate_type.cpp |  7 +++++++
 src/verilog/verilog_expr.cpp           | 10 ++++++++--
 4 files changed, 35 insertions(+), 2 deletions(-)

diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 71f1c930..ef2cf523 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/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)
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index fbd33040..731e0eae 100644
--- a/src/verilog/parser.y
+++ b/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:
diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp
index a543c6b6..5234e642 100644
--- a/src/verilog/verilog_elaborate_type.cpp
+++ b/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);
diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp
index 9d3aebbf..633edfe8 100644
--- a/src/verilog/verilog_expr.cpp
+++ b/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;