Merge branch 'main' of https://github.com/ShashankVM/hw-cbmc into vcd_for_all_cover

Author: ShashankVM

regression/verilog/arrays/unpacked_array_concatenation1.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+unpacked_array_concatenation1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This yields a type checking error.

regression/verilog/arrays/unpacked_array_concatenation1.sv

@@ -0,0 +1,11 @@
+module main;
+
+  // 1800-2017 10.10 Unpacked array concatenation
+  byte my_bytes [1:4] = { 1, 2, 3, 4 };
+
+  assert final(my_bytes[1] == 1);
+  assert final(my_bytes[2] == 2);
+  assert final(my_bytes[3] == 3);
+  assert final(my_bytes[4] == 4);
+
+endmodule

regression/verilog/structs/structs4.sv

@@ -12,7 +12,7 @@ module main;
     s.field3 = 'b1110011;
   end
 
-  // structs can be converted without cast to bit-vectors
+  // packed structs can be converted without cast to bit-vectors
   wire [8:0] w = s;
 
   // Expected to pass.

regression/verilog/structs/unpacked_struct1.desc

@@ -0,0 +1,7 @@
+CORE
+unpacked_struct1.sv
+
+^file .* line 9: failed to convert `struct' to `\[8:0\]'$
+^EXIT=2$
+^SIGNAL=0$
+--

regression/verilog/structs/unpacked_struct1.sv

@@ -0,0 +1,11 @@
+module main;
+
+  // an unpacked struct
+  struct {
+    bit field;
+  } s;
+
+  // unpacked structs cannot be converted to bit-vectors
+  wire [8:0] w = s;
+
+endmodule

src/verilog/expr2verilog.cpp

@@ -2149,7 +2149,10 @@ std::string expr2verilogt::convert(const typet &type)
   }
   else if(type.id() == ID_struct)
   {
-    return "struct";
+    if(type.get_bool(ID_packed))
+      return "struct packed";
+    else
+      return "struct";
   }
   else if(type.id() == ID_union)
   {

src/verilog/parser.y

@@ -1552,6 +1552,8 @@ data_type:
 	| struct_union packed_opt signing_opt 
 	  '{' struct_union_member_brace '}' packed_dimension_brace
 	        { $$=$1;
+	          if(stack_expr($2).id() == ID_packed)
+	            stack_type($1).set(ID_packed, true);
 	          addswap($$, ID_declaration_list, $5); }
 	| TOK_ENUM enum_base_type_opt '{' enum_name_declaration_list '}'
 	        { // Like in C, these do _not_ create a scope.

src/verilog/verilog_elaborate_type.cpp

@@ -425,8 +425,14 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
       }
     }
 
-    return struct_union_typet{src.id(), std::move(components)}
-      .with_source_location(src.source_location());
+    auto result =
+      struct_union_typet{src.id(), std::move(components)}.with_source_location(
+        src.source_location());
+
+    if(src.get_bool(ID_packed))
+      result.set(ID_packed, true);
+
+    return result;
   }
   else if(src.id() == ID_verilog_string)
   {

src/verilog/verilog_typecheck.cpp

@@ -41,6 +41,104 @@ void verilog_typecheckt::assignment_conversion(
   exprt &rhs,
   const typet &lhs_type)
 {
+  // 1800-2017 10.9
+  if(rhs.type().id() == ID_verilog_assignment_pattern)
+  {
+    DATA_INVARIANT(
+      rhs.id() == ID_verilog_assignment_pattern,
+      "verilog_assignment_pattern expression expected");
+    if(lhs_type.id() == ID_struct)
+    {
+      auto &struct_type = to_struct_type(lhs_type);
+      auto &components = struct_type.components();
+
+      if(
+        !rhs.operands().empty() &&
+        rhs.operands().front().id() == ID_member_initializer)
+      {
+        exprt::operandst initializers{components.size(), nil_exprt{}};
+
+        for(auto &op : rhs.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
+          assignment_conversion(value, components[nr].type());
+          initializers[nr] = std::move(value);
+        }
+
+        // Is every member covered?
+        for(std::size_t i = 0; i < components.size(); i++)
+          if(initializers[i].is_nil())
+          {
+            throw errort().with_location(rhs.source_location())
+              << "assignment pattern does not assign member `"
+              << components[i].get_name() << "'";
+          }
+
+        rhs = struct_exprt{std::move(initializers), struct_type}
+                .with_source_location(rhs.source_location());
+      }
+      else
+      {
+        if(rhs.operands().size() != components.size())
+        {
+          throw errort().with_location(rhs.source_location())
+            << "number of expressions does not match number of struct members";
+        }
+
+        for(std::size_t i = 0; i < components.size(); i++)
+        {
+          // rec. call
+          assignment_conversion(rhs.operands()[i], components[i].type());
+        }
+
+        // turn into struct expression
+        rhs.id(ID_struct);
+        rhs.type() = lhs_type;
+      }
+
+      return;
+    }
+    else if(lhs_type.id() == ID_array)
+    {
+      auto &array_type = to_array_type(lhs_type);
+      auto &element_type = array_type.element_type();
+      auto array_size =
+        numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
+
+      if(array_size != rhs.operands().size())
+      {
+        throw errort().with_location(rhs.source_location())
+          << "number of expressions does not match number of array elements";
+      }
+
+      for(std::size_t i = 0; i < array_size; i++)
+      {
+        // rec. call
+        assignment_conversion(rhs.operands()[i], element_type);
+      }
+
+      // turn into array expression
+      rhs.id(ID_array);
+      rhs.type() = lhs_type;
+      return;
+    }
+    else
+    {
+      throw errort().with_location(rhs.source_location())
+        << "cannot convert assignment pattern to '" << to_string(lhs_type)
+        << '\'';
+    }
+  }
+
   // Implements 1800-2017 10.7
   // If the RHS is smaller than the LHS:
   // * if the RHS is unsigned, it is zero-padded

src/verilog/verilog_typecheck_expr.cpp

@@ -2191,102 +2191,6 @@ void verilog_typecheck_exprt::implicit_typecast(
       return;
     }
   }
-  else if(src_type.id() == ID_verilog_assignment_pattern)
-  {
-    DATA_INVARIANT(
-      expr.id() == ID_verilog_assignment_pattern,
-      "verilog_assignment_pattern expression expected");
-    if(dest_type.id() == ID_struct)
-    {
-      auto &struct_type = to_struct_type(dest_type);
-      auto &components = struct_type.components();
-
-      if(
-        !expr.operands().empty() &&
-        expr.operands().front().id() == ID_member_initializer)
-      {
-        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);
-        }
-
-        // 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
-      {
-        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;
-      }
-
-      return;
-    }
-    else if(dest_type.id() == ID_array)
-    {
-      auto &array_type = to_array_type(dest_type);
-      auto &element_type = array_type.element_type();
-      auto array_size =
-        numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
-
-      if(array_size != expr.operands().size())
-      {
-        throw errort().with_location(expr.source_location())
-          << "number of expressions does not match number of array elements";
-      }
-
-      for(std::size_t i = 0; i < array_size; i++)
-      {
-        // rec. call
-        implicit_typecast(expr.operands()[i], element_type);
-      }
-
-      // turn into array expression
-      expr.id(ID_array);
-      expr.type() = dest_type;
-      return;
-    }
-    else
-    {
-      throw errort().with_location(expr.source_location())
-        << "cannot convert assignment pattern to '" << to_string(dest_type)
-        << '\'';
-    }
-  }
   else if(src_type.id() == ID_verilog_real)
   {
     if(
@@ -2481,7 +2385,7 @@ void verilog_typecheck_exprt::struct_decay(exprt &expr) const
   // Verilog packed struct types decay to a vector type [$bits(t)-1:0]
   // when used in relational or arithmetic expressions.
   auto &type = expr.type();
-  if(type.id() == ID_struct)
+  if(type.id() == ID_struct && type.get_bool(ID_packed))
   {
     auto new_type =
       unsignedbv_typet{numeric_cast_v<std::size_t>(get_width(type))};