Allow SymbolicArray to represent arrays of non-header/header union types

midend/interpreter.cpp

@@ -456,12 +456,14 @@ SymbolicArray::SymbolicArray(const IR::Type_Array *type, bool uninitialized,
         if (type->elementType->to<IR::Type_Header>()) {
             auto elem = factory->create(elemType, uninitialized);
             BUG_CHECK(elem->is<SymbolicHeader>(), "%1%: expected a header", elem);
-            values.push_back(elem->to<SymbolicHeader>());
-        }
-        if (auto newElemType = type->elementType->to<IR::Type_HeaderUnion>()) {
+            values.push_back(elem);
+        } else if (auto newElemType = type->elementType->to<IR::Type_HeaderUnion>()) {
             auto elem = factory->create(newElemType, uninitialized);
             BUG_CHECK(elem->is<SymbolicHeaderUnion>(), "%1%: expected a header union", elem);
-            values.push_back(elem->to<SymbolicHeaderUnion>());
+            values.push_back(elem);
+        } else {
+            auto elem = factory->create(type->elementType, uninitialized);
+            values.push_back(elem);
         }
     }
 }
@@ -543,8 +545,7 @@ void SymbolicArray::setAllUnknown() {
 
 SymbolicValue *SymbolicArray::clone() const {
     auto result = new SymbolicArray(type->to<IR::Type_Array>());
-    for (unsigned i = 0; i < values.size(); i++)
-        result->values.push_back(get(nullptr, i)->clone()->to<SymbolicStruct>());
+    for (unsigned i = 0; i < values.size(); i++) result->values.push_back(get(nullptr, i)->clone());
     return result;
 }
 

midend/interpreter.h

@@ -483,7 +483,7 @@ class SymbolicHeaderUnion : public SymbolicStruct {
 };
 
 class SymbolicArray final : public SymbolicValue {
-    std::vector<SymbolicStruct *> values;
+    std::vector<SymbolicValue *> values;
     friend class AnyElement;
     explicit SymbolicArray(const IR::Type_Array *type)
         : SymbolicValue(type),

testdata/p4_16_samples/non_header_array_access_in_parser.p4

@@ -0,0 +1,36 @@
+#include <core.p4>
+
+@command_line("--loopsUnroll")
+
+struct S {
+    bit<8> f1;
+    bit<8> f2;
+}
+
+header h_t {
+    S[2] array;
+}
+
+struct metadata_t {
+    S[2] array;
+    h_t h;
+}
+
+parser p(packet_in packet, out metadata_t metadata) {
+    state start { transition s0; }
+    state s0 {
+        transition select(packet.lookahead<bit<8>>()) {
+            1 : s1;
+            default : accept;
+        }
+    }
+    state s1 {
+        packet.extract(metadata.h);
+        metadata.array[1].f1 = metadata.h.array[0].f1;
+        transition accept;
+    }
+}
+
+parser simple(packet_in packet, out metadata_t metadata);
+package top(simple e);
+top(p()) main;

testdata/p4_16_samples_outputs/non_header_array_access_in_parser-first.p4

@@ -0,0 +1,36 @@
+#include <core.p4>
+
+@command_line("--loopsUnroll") struct S {
+    bit<8> f1;
+    bit<8> f2;
+}
+
+header h_t {
+    S[2] array;
+}
+
+struct metadata_t {
+    S[2] array;
+    h_t  h;
+}
+
+parser p(packet_in packet, out metadata_t metadata) {
+    state start {
+        transition s0;
+    }
+    state s0 {
+        transition select(packet.lookahead<bit<8>>()) {
+            8w1: s1;
+            default: accept;
+        }
+    }
+    state s1 {
+        packet.extract<h_t>(metadata.h);
+        metadata.array[1].f1 = metadata.h.array[0].f1;
+        transition accept;
+    }
+}
+
+parser simple(packet_in packet, out metadata_t metadata);
+package top(simple e);
+top(p()) main;

testdata/p4_16_samples_outputs/non_header_array_access_in_parser-frontend.p4

@@ -0,0 +1,37 @@
+#include <core.p4>
+
+@command_line("--loopsUnroll") struct S {
+    bit<8> f1;
+    bit<8> f2;
+}
+
+header h_t {
+    S[2] array;
+}
+
+struct metadata_t {
+    S[2] array;
+    h_t  h;
+}
+
+parser p(packet_in packet, out metadata_t metadata) {
+    @name("p.tmp") bit<8> tmp;
+    @name("p.tmp_0") bit<8> tmp_0;
+    state start {
+        tmp_0 = packet.lookahead<bit<8>>();
+        tmp = tmp_0;
+        transition select(tmp) {
+            8w1: s1;
+            default: accept;
+        }
+    }
+    state s1 {
+        packet.extract<h_t>(metadata.h);
+        metadata.array[1].f1 = metadata.h.array[0].f1;
+        transition accept;
+    }
+}
+
+parser simple(packet_in packet, out metadata_t metadata);
+package top(simple e);
+top(p()) main;

testdata/p4_16_samples_outputs/non_header_array_access_in_parser-midend.p4

@@ -0,0 +1,35 @@
+#include <core.p4>
+
+@command_line("--loopsUnroll") struct S {
+    bit<8> f1;
+    bit<8> f2;
+}
+
+header h_t {
+    S[2] array;
+}
+
+struct metadata_t {
+    S[2] array;
+    h_t  h;
+}
+
+parser p(packet_in packet, out metadata_t metadata) {
+    @name("p.tmp_0") bit<8> tmp_0;
+    state s1 {
+        packet.extract<h_t>(metadata.h);
+        metadata.array[1].f1 = metadata.h.array[0].f1;
+        transition accept;
+    }
+    state start {
+        tmp_0 = packet.lookahead<bit<8>>();
+        transition select(tmp_0) {
+            8w1: s1;
+            default: accept;
+        }
+    }
+}
+
+parser simple(packet_in packet, out metadata_t metadata);
+package top(simple e);
+top(p()) main;

testdata/p4_16_samples_outputs/non_header_array_access_in_parser.p4

@@ -0,0 +1,36 @@
+#include <core.p4>
+
+@command_line("--loopsUnroll") struct S {
+    bit<8> f1;
+    bit<8> f2;
+}
+
+header h_t {
+    S[2] array;
+}
+
+struct metadata_t {
+    S[2] array;
+    h_t  h;
+}
+
+parser p(packet_in packet, out metadata_t metadata) {
+    state start {
+        transition s0;
+    }
+    state s0 {
+        transition select(packet.lookahead<bit<8>>()) {
+            1: s1;
+            default: accept;
+        }
+    }
+    state s1 {
+        packet.extract(metadata.h);
+        metadata.array[1].f1 = metadata.h.array[0].f1;
+        transition accept;
+    }
+}
+
+parser simple(packet_in packet, out metadata_t metadata);
+package top(simple e);
+top(p()) main;