$past now supports array and struct types

regression/verilog/structs/array_in_struct1.sv

@@ -5,13 +5,13 @@ module main;
     int array1[4];
 
     // packed
-    bit [31:0] [3:0] array2;
+    bit [3:0] [31:0] array2;
   } s;
 
   initial s = '{ '{ 1, 2, 3, 4 }, '{ 1, 2, 3, 4 } };
 
   // Expected to pass.
-  p0: assert property ($bits(s) == 4);
+  p0: assert final ($bits(s) == 4 * 32 + 4 * 32);
   p11: assert property (s.array1[0] == 1);
   p12: assert property (s.array1[1] == 2);
   p13: assert property (s.array1[2] == 3);

regression/verilog/system-functions/past5.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 past5.sv
 
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-$past doesn't support the array.

regression/verilog/system-functions/past5.sv

@@ -2,6 +2,6 @@ module main;
 
   logic [31:0] mem[123];
 
-  assert property (##1 mem == $past(mem));
+  assert property (mem == $past(mem));
 
 endmodule

regression/verilog/system-functions/past6.desc

@@ -0,0 +1,8 @@
+CORE
+past6.sv
+
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/system-functions/past6.sv

@@ -0,0 +1,17 @@
+module main;
+
+  typedef struct {
+    bit some_bit;
+  } inner_struct;
+
+  typedef struct {
+    bit [31:0] array [123];
+    bit other_bit;
+    inner_struct inner;
+  } my_struct;
+
+  my_struct s;
+
+  assert property (s == $past(s));
+
+endmodule

src/verilog/verilog_elaborate_type.cpp

@@ -402,30 +402,19 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
         declaration.id() == ID_decl, "struct type must have declarations");
 
       // Convert the type
-      auto type = elaborate_type(declaration_expr.type());
+      auto &type = declaration_expr.type();
 
       // Convert the declarators
       for(auto &declarator_expr : declaration_expr.operands())
       {
         auto &declarator =
           static_cast<const verilog_declaratort &>(declarator_expr);
 
-        struct_union_typet::componentt component;
-
-        // compose the type
-        if(declarator.type().is_nil())
-          component.type() = type;
-        else if(declarator.type().id() == ID_array)
-        {
-          throw errort().with_location(declarator.source_location())
-            << "array in struct";
-        }
-        else
-        {
-          throw errort().with_location(declarator.source_location())
-            << "unexpected type on declarator";
-        }
+        // merge the types, and elaborate
+        auto merged_type = elaborate_type(declarator.merged_type(type));
 
+        struct_union_typet::componentt component;
+        component.type() = std::move(merged_type);
         component.add_source_location() = declarator.source_location();
         component.set_base_name(declarator.base_name());
         component.set_name(declarator.base_name());

src/verilog/verilog_expr.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mathematical_types.h>
 #include <util/prefix.h>
 
+#include "verilog_initializer.h"
 #include "verilog_typecheck_base.h"
 #include "verilog_types.h"
 
@@ -535,9 +536,7 @@ exprt verilog_inside_exprt::lower() const
 
 exprt verilog_past_exprt::default_value() const
 {
-  auto zero = from_integer(0, type());
-  if(zero.is_nil())
-    throw "failed to create $past default value";
-  else
-    return std::move(zero);
+  auto value_opt = verilog_default_initializer(type());
+  CHECK_RETURN(value_opt.has_value());
+  return *value_opt;
 }