Fixing bug in ParserUnroll for infinite loops without header stacks (#…

…3538)

* fixing bug for issue3537

* fixing other bug with infinite loop

Co-authored-by: Volodymyr Peschanenko <[email protected]>

midend/parserUnroll.cpp

@@ -596,6 +596,20 @@ class ParserSymbolicInterpreter {
         return false;
     }
 
+    /// True if both structures are equal.
+    bool equStackVariableMap(const StackVariableMap& l, const StackVariableMap& r) const {
+        if (l.empty()) {
+            return r.empty();
+        }
+        for (const auto& i : l) {
+            const auto j = r.find(i.first);
+            if (j == r.end() || i.second != j->second) {
+                return false;
+            }
+        }
+        return true;
+    }
+
     /// Return true if we have detected a loop we cannot unroll
     bool checkLoops(ParserStateInfo* state) const {
         const ParserStateInfo* crt = state;
@@ -630,11 +644,17 @@ class ParserSymbolicInterpreter {
                         ::warning(ErrorType::ERR_INVALID,
                                   "Parser cycle without extracting any bytes:\n%1%",
                                   stateChain(state));
+                    if (equStackVariableMap(crt->statesIndexes, state->statesIndexes)) {
+                        wasError = true;
+                    }
                     return true;
                 }
 
                 // If no header validity has changed we can't really unroll
                 if (!headerValidityChange(crt->before, state->before)) {
+                    if (equStackVariableMap(crt->statesIndexes, state->statesIndexes)) {
+                        wasError = true;
+                    }
                     return true;
                 }
                 break;
@@ -752,6 +772,10 @@ class ParserSymbolicInterpreter {
             stateInfo->scenarioStates.insert(stateInfo->name);  // add to loops detection
             bool infLoop = checkLoops(stateInfo);
             if (infLoop) {
+                // Stop unrolling if it was an error.
+                if (wasError) {
+                    break;
+                }
                 // don't evaluate successors anymore
                 // generate call OutOfBound
                 addOutFoBound(stateInfo, newStates);

testdata/p4_16_samples/parser-unroll-issue3537-1.p4

@@ -0,0 +1,71 @@
+#include <core.p4>
+#include <v1model.p4>
+
+struct H { }
+
+struct M { }
+
+parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) {
+    state start {
+        transition s0;
+    }
+
+    state s0 {
+        transition s1;
+    }
+
+    state s1 {
+        packet.advance(16);
+        transition select(packet.lookahead<bit<16>>()) {
+            0 : s1;
+            default : s2;
+        }
+    }
+
+    state s2 {
+        transition s3;
+    }
+
+    state s3 {
+        packet.advance(16);
+        transition select(packet.lookahead<bit<16>>()) {
+            0 : s1;
+            1 : s2;
+            default : s4;
+        }
+    }
+
+    state s4 {
+        transition accept;
+    }
+}
+
+control Aux(inout M meta) {
+    apply {
+    }
+}
+
+control IngressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
+    apply {
+    }
+}
+
+control EgressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
+    apply { }
+}
+
+control DeparserI(packet_out pk, in H hdr) {
+    apply { }
+}
+
+control VerifyChecksumI(inout H hdr, inout M meta) {
+    apply { }
+}
+
+control ComputeChecksumI(inout H hdr, inout M meta) {
+    apply { }
+}
+
+
+V1Switch(ParserI(), VerifyChecksumI(), IngressI(), EgressI(),
+         ComputeChecksumI(), DeparserI()) main;

testdata/p4_16_samples/parser-unroll-issue3537.p4

@@ -0,0 +1,99 @@
+#include <core.p4>
+#include <v1model.p4>
+
+header h1_t {}
+header h2_t {
+    bit<16> f1;
+}
+header h3_t {
+    bit<3> pad;
+    bit<13> f2;
+    bit<8> f3;
+}
+header h4_t {
+    bit<8> f4;
+}
+header h5_t {}
+header h6_t {
+    bit<16> f5;
+}
+
+struct H {
+    h1_t h1;
+    h2_t h2;
+    h3_t h3;
+    h4_t h4;
+    h5_t h5;
+    h6_t h6;
+};
+struct M { };
+
+parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) {
+    state start {
+        packet.extract<h1_t>(hdr.h1);
+        packet.extract<h2_t>(hdr.h2);
+        transition select(hdr.h2.f1) {
+            16w0x800: parse_ipv4;
+            16w0x86dd: parse_ipv6;
+            default: accept;
+        }
+    }
+    state parse_ipv4 {
+        packet.extract<h3_t>(hdr.h3);
+        transition select(hdr.h3.f2, hdr.h3.f3) {
+            (13w0, 8w6): parse_tcp;
+            (13w0, 8w17): parse_udp;
+            default: accept;
+        }
+    }
+    state parse_ipv6 {
+        packet.extract<h4_t>(hdr.h4);
+        transition select(hdr.h4.f4) {
+            8w6: parse_tcp;
+            8w17: parse_udp;
+            default: accept;
+        }
+    }
+    state parse_tcp {
+        packet.extract<h5_t>(hdr.h5);
+        transition accept;
+    }
+    state parse_udp {
+        packet.extract<h6_t>(hdr.h6);
+        transition select(hdr.h6.f5) {
+            16w0xcafe: parse_ipv4;
+            16w0xffff: reject;
+            default: accept;
+        }
+    }
+}
+
+control Aux(inout M meta) {
+    apply {
+    }
+}
+
+control IngressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
+    apply {
+    }
+}
+
+control EgressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
+    apply { }
+}
+
+control DeparserI(packet_out pk, in H hdr) {
+    apply { }
+}
+
+control VerifyChecksumI(inout H hdr, inout M meta) {
+    apply { }
+}
+
+control ComputeChecksumI(inout H hdr, inout M meta) {
+    apply { }
+}
+
+
+V1Switch(ParserI(), VerifyChecksumI(), IngressI(), EgressI(),
+         ComputeChecksumI(), DeparserI()) main;

testdata/p4_16_samples_outputs/parser-unroll-issue3537-1-first.p4

@@ -0,0 +1,72 @@
+#include <core.p4>
+#define V1MODEL_VERSION 20180101
+#include <v1model.p4>
+
+struct H {
+}
+
+struct M {
+}
+
+parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) {
+    state start {
+        transition s0;
+    }
+    state s0 {
+        transition s1;
+    }
+    state s1 {
+        packet.advance(32w16);
+        transition select(packet.lookahead<bit<16>>()) {
+            16w0: s1;
+            default: s2;
+        }
+    }
+    state s2 {
+        transition s3;
+    }
+    state s3 {
+        packet.advance(32w16);
+        transition select(packet.lookahead<bit<16>>()) {
+            16w0: s1;
+            16w1: s2;
+            default: s4;
+        }
+    }
+    state s4 {
+        transition accept;
+    }
+}
+
+control Aux(inout M meta) {
+    apply {
+    }
+}
+
+control IngressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
+    apply {
+    }
+}
+
+control EgressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
+    apply {
+    }
+}
+
+control DeparserI(packet_out pk, in H hdr) {
+    apply {
+    }
+}
+
+control VerifyChecksumI(inout H hdr, inout M meta) {
+    apply {
+    }
+}
+
+control ComputeChecksumI(inout H hdr, inout M meta) {
+    apply {
+    }
+}
+
+V1Switch<H, M>(ParserI(), VerifyChecksumI(), IngressI(), EgressI(), ComputeChecksumI(), DeparserI()) main;
+

testdata/p4_16_samples_outputs/parser-unroll-issue3537-1-frontend.p4

@@ -0,0 +1,69 @@
+#include <core.p4>
+#define V1MODEL_VERSION 20180101
+#include <v1model.p4>
+
+struct H {
+}
+
+struct M {
+}
+
+parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) {
+    @name("ParserI.tmp") bit<16> tmp;
+    @name("ParserI.tmp_0") bit<16> tmp_0;
+    @name("ParserI.tmp_1") bit<16> tmp_1;
+    @name("ParserI.tmp_2") bit<16> tmp_2;
+    state start {
+        transition s1;
+    }
+    state s1 {
+        packet.advance(32w16);
+        tmp_0 = packet.lookahead<bit<16>>();
+        tmp = tmp_0;
+        transition select(tmp) {
+            16w0: s1;
+            default: s2;
+        }
+    }
+    state s2 {
+        packet.advance(32w16);
+        tmp_2 = packet.lookahead<bit<16>>();
+        tmp_1 = tmp_2;
+        transition select(tmp_1) {
+            16w0: s1;
+            16w1: s2;
+            default: s4;
+        }
+    }
+    state s4 {
+        transition accept;
+    }
+}
+
+control IngressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
+    apply {
+    }
+}
+
+control EgressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
+    apply {
+    }
+}
+
+control DeparserI(packet_out pk, in H hdr) {
+    apply {
+    }
+}
+
+control VerifyChecksumI(inout H hdr, inout M meta) {
+    apply {
+    }
+}
+
+control ComputeChecksumI(inout H hdr, inout M meta) {
+    apply {
+    }
+}
+
+V1Switch<H, M>(ParserI(), VerifyChecksumI(), IngressI(), EgressI(), ComputeChecksumI(), DeparserI()) main;
+