Merge pull request #1000 from diffblue/structure_pattern_key

SystemVerilog: assignment patterns with structure keys

Author: tautschnig

CHANGELOG

@@ -1,6 +1,7 @@
 # EBMC 5.6
 
 * SystemVerilog: typedefs from package scopes
+* SystemVerilog: assignment patterns with keys for structs
 
 # EBMC 5.5
 

regression/verilog/structs/assignment_pattern1.desc

@@ -0,0 +1,6 @@
+CORE
+assignment_pattern1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--

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

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$
+--

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

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$
+--

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

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;

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();