From 24d6e6d94f715cf74cc5b7b5e065034d3af2e267 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 19 Feb 2025 13:49:08 +0000
Subject: [PATCH] SystemVerilog: assignment patterns with structure keys

This adds 1800-2017 assignment patters with keys for struct types.
---
 CHANGELOG                                     |  1 +
 .../verilog/structs/assignment_pattern1.desc  |  6 ++
 .../verilog/structs/assignment_pattern1.sv    |  9 +++
 .../verilog/structs/assignment_pattern2.desc  |  7 +++
 .../verilog/structs/assignment_pattern2.sv    |  6 ++
 .../verilog/structs/assignment_pattern3.desc  |  7 +++
 .../verilog/structs/assignment_pattern3.sv    |  6 ++
 src/verilog/parser.y                          | 26 +++++++-
 src/verilog/verilog_typecheck_expr.cpp        | 63 ++++++++++++++++---
 9 files changed, 120 insertions(+), 11 deletions(-)
 create mode 100644 regression/verilog/structs/assignment_pattern1.desc
 create mode 100644 regression/verilog/structs/assignment_pattern1.sv
 create mode 100644 regression/verilog/structs/assignment_pattern2.desc
 create mode 100644 regression/verilog/structs/assignment_pattern2.sv
 create mode 100644 regression/verilog/structs/assignment_pattern3.desc
 create mode 100644 regression/verilog/structs/assignment_pattern3.sv

diff --git a/CHANGELOG b/CHANGELOG
index e2f85d661..4148240e2 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,6 +1,7 @@
 # EBMC 5.6
 
 * SystemVerilog: typedefs from package scopes
+* SystemVerilog: assignment patterns with keys for structs
 
 # EBMC 5.5
 
diff --git a/regression/verilog/structs/assignment_pattern1.desc b/regression/verilog/structs/assignment_pattern1.desc
new file mode 100644
index 000000000..def0d09ed
--- /dev/null
+++ b/regression/verilog/structs/assignment_pattern1.desc
@@ -0,0 +1,6 @@
+CORE
+assignment_pattern1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/verilog/structs/assignment_pattern1.sv b/regression/verilog/structs/assignment_pattern1.sv
new file mode 100644
index 000000000..6c6cbf061
--- /dev/null
+++ b/regression/verilog/structs/assignment_pattern1.sv
@@ -0,0 +1,9 @@
+module main;
+
+  typedef struct {int a, b;} S;
+  var S x = '{b:1, a:0};
+
+  assert final (x.a == 0);
+  assert final (x.b == 1);
+
+endmodule
diff --git a/regression/verilog/structs/assignment_pattern2.desc b/regression/verilog/structs/assignment_pattern2.desc
new file mode 100644
index 000000000..7580d01be
--- /dev/null
+++ b/regression/verilog/structs/assignment_pattern2.desc
@@ -0,0 +1,7 @@
+CORE
+assignment_pattern2.sv
+
+^file .* line 4: struct does not have a member `something_else'$
+^EXIT=2$
+^SIGNAL=0$
+--
diff --git a/regression/verilog/structs/assignment_pattern2.sv b/regression/verilog/structs/assignment_pattern2.sv
new file mode 100644
index 000000000..5dbbe32fc
--- /dev/null
+++ b/regression/verilog/structs/assignment_pattern2.sv
@@ -0,0 +1,6 @@
+module main;
+
+  typedef struct {int a, b;} S;
+  var S x = '{b:1, something_else:0};
+
+endmodule
diff --git a/regression/verilog/structs/assignment_pattern3.desc b/regression/verilog/structs/assignment_pattern3.desc
new file mode 100644
index 000000000..c949f462b
--- /dev/null
+++ b/regression/verilog/structs/assignment_pattern3.desc
@@ -0,0 +1,7 @@
+CORE
+assignment_pattern3.sv
+
+^file .* line 4: assignment pattern does not assign member `a'$
+^EXIT=2$
+^SIGNAL=0$
+--
diff --git a/regression/verilog/structs/assignment_pattern3.sv b/regression/verilog/structs/assignment_pattern3.sv
new file mode 100644
index 000000000..afe2b45c5
--- /dev/null
+++ b/regression/verilog/structs/assignment_pattern3.sv
@@ -0,0 +1,6 @@
+module main;
+
+  typedef struct {int a, b;} S;
+  var S x = '{b:1}; // forgot a
+
+endmodule
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index ee0a7ba31..ba1d9c12f 100644
--- a/src/verilog/parser.y
+++ b/src/verilog/parser.y
@@ -3649,8 +3649,30 @@ open_value_range: value_range;
 // A.6.7.1 Patterns
 
 assignment_pattern:
-	'\'' '{' expression_brace '}'
+	  '\'' '{' expression_brace '}'
 		{ init($$, ID_verilog_assignment_pattern); swapop($$, $3); }
+	| '\'' '{' structure_pattern_key_brace '}'
+		{ init($$, ID_verilog_assignment_pattern); swapop($$, $3); }
+	;
+
+structure_pattern_key_and_expression:
+	  structure_pattern_key TOK_COLON expression
+		{ $$ = $1; mto($$, $3); }
+	;
+
+structure_pattern_key_brace:
+	  structure_pattern_key_and_expression
+		{ init($$); mto($$, $1); }
+	| structure_pattern_key_brace ',' structure_pattern_key_and_expression
+		{ $$ = $1; mto($$, $3); }
+	;
+
+structure_pattern_key:
+	  member_identifier
+		{
+		  init($$, ID_member_initializer);
+		  stack_expr($$).set(ID_member_name, stack_expr($1).get(ID_base_name));
+		}
 	;
 
 assignment_pattern_expression:
@@ -4456,6 +4478,8 @@ ps_covergroup_identifier:
 	
 memory_identifier: identifier;
 
+member_identifier: identifier;
+
 method_identifier: identifier;
 
 signal_identifier: identifier;
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index 920648c6d..5d19d8572 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -2019,21 +2019,59 @@ void verilog_typecheck_exprt::implicit_typecast(
       auto &struct_type = to_struct_type(dest_type);
       auto &components = struct_type.components();
 
-      if(expr.operands().size() != components.size())
+      if(
+        !expr.operands().empty() &&
+        expr.operands().front().id() == ID_member_initializer)
       {
-        throw errort().with_location(expr.source_location())
-          << "number of expressions does not match number of struct members";
-      }
+        exprt::operandst initializers{components.size(), nil_exprt{}};
+
+        for(auto &op : expr.operands())
+        {
+          PRECONDITION(op.id() == ID_member_initializer);
+          auto member_name = op.get(ID_member_name);
+          if(!struct_type.has_component(member_name))
+          {
+            throw errort().with_location(op.source_location())
+              << "struct does not have a member `" << member_name << "'";
+          }
+          auto nr = struct_type.component_number(member_name);
+          auto value = to_unary_expr(op).op();
+          // rec. call
+          implicit_typecast(value, components[nr].type());
+          initializers[nr] = std::move(value);
+        }
 
-      for(std::size_t i = 0; i < components.size(); i++)
+        // Is every member covered?
+        for(std::size_t i = 0; i < components.size(); i++)
+          if(initializers[i].is_nil())
+          {
+            throw errort().with_location(expr.source_location())
+              << "assignment pattern does not assign member `"
+              << components[i].get_name() << "'";
+          }
+
+        expr = struct_exprt{std::move(initializers), struct_type}
+                 .with_source_location(expr.source_location());
+      }
+      else
       {
-        // rec. call
-        implicit_typecast(expr.operands()[i], components[i].type());
+        if(expr.operands().size() != components.size())
+        {
+          throw errort().with_location(expr.source_location())
+            << "number of expressions does not match number of struct members";
+        }
+
+        for(std::size_t i = 0; i < components.size(); i++)
+        {
+          // rec. call
+          implicit_typecast(expr.operands()[i], components[i].type());
+        }
+
+        // turn into struct expression
+        expr.id(ID_struct);
+        expr.type() = dest_type;
       }
 
-      // turn into struct expression
-      expr.id(ID_struct);
-      expr.type() = dest_type;
       return;
     }
     else if(dest_type.id() == ID_array)
@@ -2620,6 +2658,11 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     // The type of these expressions is determined by their context.
     expr.type() = typet(ID_verilog_new);
   }
+  else if(expr.id() == ID_member_initializer)
+  {
+    // assignment patterns, 1800 2017 10.9
+    convert_expr(expr.op());
+  }
   else
   {
     throw errort() << "no conversion for unary expression " << expr.id();