diff --git a/midend/parserUnroll.cpp b/midend/parserUnroll.cpp index 59c5365319b..1b0621e84b3 100644 --- a/midend/parserUnroll.cpp +++ b/midend/parserUnroll.cpp @@ -181,6 +181,7 @@ class ParserStateRewriter : public Transform { wasOutOfBound = true; return expression; } + state->substitutedIndexes[newExpression->left] = res; return newExpression; } @@ -248,6 +249,44 @@ class ParserStateRewriter : public Transform { return true; } + /// Checks values of the headers stacks which were evaluated. + bool checkIndexes(const StackVariableIndexMap& prev, const StackVariableIndexMap& cur) { + if (prev.size() != cur.size()) { + return false; + } + for (auto& i : prev) { + auto j = cur.find(i.first); + if (j == cur.end()) { + return false; + } + if (!i.second->equiv(*j->second)) { + return false; + } + } + return true; + } + + /// Returns true for current id if indexes of the headers stack + /// are the same before previous call of the same parser state. + bool calledWithNoChanges(IR::ID id, const ParserStateInfo* state) { + CHECK_NULL(state); + const auto* prevState = state; + while (prevState->state->name.name != id.name) { + prevState = prevState->predecessor; + if (prevState == nullptr) { + return false; + } + } + if (prevState->predecessor != nullptr) { + prevState = prevState->predecessor; + } else if (prevState == state && state->predecessor == nullptr) { + // The map should be empty if no next operators in a start. + return state->statesIndexes.empty(); + } + return prevState->statesIndexes == state->statesIndexes && + checkIndexes(prevState->substitutedIndexes, state->substitutedIndexes); + } + /// Generated new state name IR::ID genNewName(IR::ID id) { if (isTerminalState(id)) return id; @@ -256,12 +295,26 @@ class ParserStateRewriter : public Transform { if (parserStructure->callsIndexes.count(id.name) && (state->scenarioStates.count(id.name) || parserStructure->reachableHSUsage(id, state))) { - if (was_called(name, id)) return id; - index = parserStructure->callsIndexes[id.name]; - parserStructure->callsIndexes[id.name] = index + 1; - if (index + 1 > 0) { - index++; - id = IR::ID(id.name + std::to_string(index)); + // or self called with no extraction... + // in this case we need to use the same name as it was in previous call + if (was_called(name, id)) { + return id; + } + if (calledWithNoChanges(id, state)) { + index = 0; + if (parserStructure->callsIndexes.count(id.name)) { + index = parserStructure->callsIndexes[id.name]; + } + if (index > 0) { + id = IR::ID(id.name + std::to_string(index)); + } + } else { + index = parserStructure->callsIndexes[id.name]; + parserStructure->callsIndexes[id.name] = index + 1; + if (index + 1 > 0) { + index++; + id = IR::ID(id.name + std::to_string(index)); + } } } else if (!parserStructure->callsIndexes.count(id.name)) { index = 0; @@ -645,7 +698,8 @@ class ParserSymbolicInterpreter { return IR::ID(state->state->name + std::to_string(state->currentIndex)); } - using EvaluationStateResult = std::pair*, bool>; + using EvaluationStateResult = + std::tuple*, bool, IR::IndexedVector>; /// Generates new state with the help of symbolic execution. /// If corresponded state was generated previously then it returns @a nullptr and false. @@ -658,19 +712,25 @@ class ParserSymbolicInterpreter { IR::ID newName; if (unroll) { newName = getNewName(state); - if (newStates.count(newName)) return EvaluationStateResult(nullptr, false); + if (newStates.count(newName)) { + return EvaluationStateResult(nullptr, false, components); + } newStates.insert(newName); } for (auto s : state->state->components) { auto* newComponent = executeStatement(state, s, valueMap); - if (!newComponent) return EvaluationStateResult(nullptr, true); - if (unroll) components.push_back(newComponent); + if (!newComponent) { + return EvaluationStateResult(nullptr, true, components); + } + if (unroll) { + components.push_back(newComponent); + } } state->after = valueMap; auto result = evaluateSelect(state, valueMap); if (unroll) { if (result.second == nullptr) { - return EvaluationStateResult(nullptr, true); + return EvaluationStateResult(nullptr, true, components); } if (state->name == newName) { state->newState = @@ -681,7 +741,7 @@ class ParserSymbolicInterpreter { new IR::ParserState(state->state->srcInfo, newName, components, result.second); } } - return EvaluationStateResult(result.first, true); + return EvaluationStateResult(result.first, true, components); } public: @@ -703,19 +763,20 @@ class ParserSymbolicInterpreter { hasOutOfboundState = false; } + using StatOrDeclVector = IR::IndexedVector; + /// generate call OutOfBound - void addOutFoBound(ParserStateInfo* stateInfo, std::unordered_set& newStates, - bool checkBefore = true) { + void addOutOfBound(ParserStateInfo* stateInfo, std::unordered_set& newStates, + bool checkBefore = true, StatOrDeclVector components = StatOrDeclVector()) { IR::ID newName = getNewName(stateInfo); if (checkBefore && newStates.count(newName)) { return; } hasOutOfboundState = true; newStates.insert(newName); - stateInfo->newState = - new IR::ParserState(newName, IR::IndexedVector(), - new IR::PathExpression(new IR::Type_State(), - new IR::Path(outOfBoundsStateName, false))); + auto* pathExpr = + new IR::PathExpression(new IR::Type_State(), new IR::Path(outOfBoundsStateName, false)); + stateInfo->newState = new IR::ParserState(newName, components, pathExpr); } /// running symbolic execution @@ -751,21 +812,26 @@ class ParserSymbolicInterpreter { if (infLoop) { // Stop unrolling if it was an error. if (wasError) { - break; + IR::ID newName = getNewName(stateInfo); + if (newStates.count(newName) != 0) { + evaluateState(stateInfo, newStates); + } + wasError = false; + continue; } // don't evaluate successors anymore // generate call OutOfBound - addOutFoBound(stateInfo, newStates); + addOutOfBound(stateInfo, newStates); continue; } IR::ID newName = getNewName(stateInfo); bool notAdded = newStates.count(newName) == 0; auto nextStates = evaluateState(stateInfo, newStates); - if (nextStates.first == nullptr) { - if (nextStates.second && stateInfo->predecessor && + if (get<0>(nextStates) == nullptr) { + if (get<1>(nextStates) && stateInfo->predecessor && newName.name != stateInfo->predecessor->newState->name) { // generate call OutOfBound - addOutFoBound(stateInfo, newStates, false); + addOutOfBound(stateInfo, newStates, false, get<2>(nextStates)); } else { // save current state if (notAdded) { @@ -775,7 +841,7 @@ class ParserSymbolicInterpreter { LOG1("No next states"); continue; } - toRun.insert(toRun.end(), nextStates.first->begin(), nextStates.first->end()); + toRun.insert(toRun.end(), get<0>(nextStates)->begin(), get<0>(nextStates)->end()); } return synthesizedParser; diff --git a/midend/parserUnroll.h b/midend/parserUnroll.h index c7030356dfd..3997328e213 100644 --- a/midend/parserUnroll.h +++ b/midend/parserUnroll.h @@ -67,6 +67,8 @@ class StackVariableHash { }; typedef std::unordered_map StackVariableMap; +typedef std::unordered_map + StackVariableIndexMap; /// Information produced for a parser state by the symbolic evaluator struct ParserStateInfo { @@ -82,7 +84,8 @@ struct ParserStateInfo { StackVariableMap statesIndexes; // global map in state indexes // set of parsers' states names with are in current path. std::unordered_set scenarioStates; - std::unordered_set scenarioHS; // scenario header stack's operations + std::unordered_set scenarioHS; // scenario header stack's operations + StackVariableIndexMap substitutedIndexes; // values of the evaluated indexes ParserStateInfo(cstring name, const IR::P4Parser* parser, const IR::ParserState* state, const ParserStateInfo* predecessor, ValueMap* before, size_t index) : name(name), @@ -99,6 +102,7 @@ struct ParserStateInfo { if (predecessor) { statesIndexes = predecessor->statesIndexes; scenarioHS = predecessor->scenarioHS; + substitutedIndexes = predecessor->substitutedIndexes; } } }; diff --git a/testdata/p4_16_samples/parser-unroll-test9.p4 b/testdata/p4_16_samples/parser-unroll-test9.p4 new file mode 100644 index 00000000000..01af72c25b8 --- /dev/null +++ b/testdata/p4_16_samples/parser-unroll-test9.p4 @@ -0,0 +1,96 @@ +#include +#define V1MODEL_VERSION 20180101 +#include + +header h_stack { + bit<8> i1; + bit<8> i2; +} + +header h_index { + bit<8> index; + bit<8> counter; +} + +struct headers { + h_stack[2] h; + h_index i; +} + +struct Meta { +} + +parser p(packet_in pkt, out headers hdr, inout Meta m, inout standard_metadata_t sm) { + state start { + pkt.extract(hdr.i); + hdr.i.counter = 0; + transition start_loops; + } + state start_loops { + hdr.i.counter = hdr.i.counter + 1; + transition select(hdr.i.index) { + 0: mixed_finite_loop; + 1: mixed_infinite_loop; + 2: infinite_loop; + 3: finite_loop; + default: reject; + } + } + state finite_loop { + hdr.i.counter = hdr.i.counter + 1; + pkt.extract(hdr.h.next); + transition select (hdr.h.last.i1) { + 2 : accept; + default: finite_loop; + } + } + state mixed_finite_loop { + pkt.extract(hdr.h.next); + transition select (hdr.h.last.i2) { + 1 : start_loops; + 2 : accept; + } + } + state mixed_infinite_loop { + transition select (hdr.i.counter) { + 3 : accept; + default : start_loops; + } + } + state infinite_loop { + hdr.i.counter = hdr.i.counter + 1; + transition select (hdr.i.counter) { + 3 : accept; + default : infinite_loop; + } + } +} + +control ingress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control vrfy(inout headers h, inout Meta m) { + apply { + } +} + +control update(inout headers h, inout Meta m) { + apply { + } +} + +control egress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control deparser(packet_out pkt, in headers h) { + apply { + pkt.emit(h.h); + pkt.emit(h.i); + } +} + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; diff --git a/testdata/p4_16_samples_outputs/parser-unroll-test9-first.p4 b/testdata/p4_16_samples_outputs/parser-unroll-test9-first.p4 new file mode 100644 index 00000000000..7f11eaecace --- /dev/null +++ b/testdata/p4_16_samples_outputs/parser-unroll-test9-first.p4 @@ -0,0 +1,96 @@ +#include +#define V1MODEL_VERSION 20180101 +#include + +header h_stack { + bit<8> i1; + bit<8> i2; +} + +header h_index { + bit<8> index; + bit<8> counter; +} + +struct headers { + h_stack[2] h; + h_index i; +} + +struct Meta { +} + +parser p(packet_in pkt, out headers hdr, inout Meta m, inout standard_metadata_t sm) { + state start { + pkt.extract(hdr.i); + hdr.i.counter = 8w0; + transition start_loops; + } + state start_loops { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.index) { + 8w0: mixed_finite_loop; + 8w1: mixed_infinite_loop; + 8w2: infinite_loop; + 8w3: finite_loop; + default: reject; + } + } + state finite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i1) { + 8w2: accept; + default: finite_loop; + } + } + state mixed_finite_loop { + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i2) { + 8w1: start_loops; + 8w2: accept; + } + } + state mixed_infinite_loop { + transition select(hdr.i.counter) { + 8w3: accept; + default: start_loops; + } + } + state infinite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.counter) { + 8w3: accept; + default: infinite_loop; + } + } +} + +control ingress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control vrfy(inout headers h, inout Meta m) { + apply { + } +} + +control update(inout headers h, inout Meta m) { + apply { + } +} + +control egress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control deparser(packet_out pkt, in headers h) { + apply { + pkt.emit(h.h); + pkt.emit(h.i); + } +} + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; diff --git a/testdata/p4_16_samples_outputs/parser-unroll-test9-frontend.p4 b/testdata/p4_16_samples_outputs/parser-unroll-test9-frontend.p4 new file mode 100644 index 00000000000..7f11eaecace --- /dev/null +++ b/testdata/p4_16_samples_outputs/parser-unroll-test9-frontend.p4 @@ -0,0 +1,96 @@ +#include +#define V1MODEL_VERSION 20180101 +#include + +header h_stack { + bit<8> i1; + bit<8> i2; +} + +header h_index { + bit<8> index; + bit<8> counter; +} + +struct headers { + h_stack[2] h; + h_index i; +} + +struct Meta { +} + +parser p(packet_in pkt, out headers hdr, inout Meta m, inout standard_metadata_t sm) { + state start { + pkt.extract(hdr.i); + hdr.i.counter = 8w0; + transition start_loops; + } + state start_loops { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.index) { + 8w0: mixed_finite_loop; + 8w1: mixed_infinite_loop; + 8w2: infinite_loop; + 8w3: finite_loop; + default: reject; + } + } + state finite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i1) { + 8w2: accept; + default: finite_loop; + } + } + state mixed_finite_loop { + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i2) { + 8w1: start_loops; + 8w2: accept; + } + } + state mixed_infinite_loop { + transition select(hdr.i.counter) { + 8w3: accept; + default: start_loops; + } + } + state infinite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.counter) { + 8w3: accept; + default: infinite_loop; + } + } +} + +control ingress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control vrfy(inout headers h, inout Meta m) { + apply { + } +} + +control update(inout headers h, inout Meta m) { + apply { + } +} + +control egress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control deparser(packet_out pkt, in headers h) { + apply { + pkt.emit(h.h); + pkt.emit(h.i); + } +} + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; diff --git a/testdata/p4_16_samples_outputs/parser-unroll-test9-midend.p4 b/testdata/p4_16_samples_outputs/parser-unroll-test9-midend.p4 new file mode 100644 index 00000000000..a22d8ed8537 --- /dev/null +++ b/testdata/p4_16_samples_outputs/parser-unroll-test9-midend.p4 @@ -0,0 +1,102 @@ +#include +#define V1MODEL_VERSION 20180101 +#include + +header h_stack { + bit<8> i1; + bit<8> i2; +} + +header h_index { + bit<8> index; + bit<8> counter; +} + +struct headers { + h_stack[2] h; + h_index i; +} + +struct Meta { +} + +parser p(packet_in pkt, out headers hdr, inout Meta m, inout standard_metadata_t sm) { + state start { + pkt.extract(hdr.i); + hdr.i.counter = 8w0; + transition start_loops; + } + state start_loops { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.index) { + 8w0: mixed_finite_loop; + 8w1: mixed_infinite_loop; + 8w2: infinite_loop; + 8w3: finite_loop; + default: reject; + } + } + state finite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i1) { + 8w2: accept; + default: finite_loop; + } + } + state mixed_finite_loop { + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i2) { + 8w1: start_loops; + 8w2: accept; + default: noMatch; + } + } + state mixed_infinite_loop { + transition select(hdr.i.counter) { + 8w3: accept; + default: start_loops; + } + } + state infinite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.counter) { + 8w3: accept; + default: infinite_loop; + } + } + state noMatch { + verify(false, error.NoMatch); + transition reject; + } +} + +control ingress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control vrfy(inout headers h, inout Meta m) { + apply { + } +} + +control update(inout headers h, inout Meta m) { + apply { + } +} + +control egress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control deparser(packet_out pkt, in headers h) { + apply { + pkt.emit(h.h[0]); + pkt.emit(h.h[1]); + pkt.emit(h.i); + } +} + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; diff --git a/testdata/p4_16_samples_outputs/parser-unroll-test9.p4 b/testdata/p4_16_samples_outputs/parser-unroll-test9.p4 new file mode 100644 index 00000000000..bd853e8cdce --- /dev/null +++ b/testdata/p4_16_samples_outputs/parser-unroll-test9.p4 @@ -0,0 +1,96 @@ +#include +#define V1MODEL_VERSION 20180101 +#include + +header h_stack { + bit<8> i1; + bit<8> i2; +} + +header h_index { + bit<8> index; + bit<8> counter; +} + +struct headers { + h_stack[2] h; + h_index i; +} + +struct Meta { +} + +parser p(packet_in pkt, out headers hdr, inout Meta m, inout standard_metadata_t sm) { + state start { + pkt.extract(hdr.i); + hdr.i.counter = 0; + transition start_loops; + } + state start_loops { + hdr.i.counter = hdr.i.counter + 1; + transition select(hdr.i.index) { + 0: mixed_finite_loop; + 1: mixed_infinite_loop; + 2: infinite_loop; + 3: finite_loop; + default: reject; + } + } + state finite_loop { + hdr.i.counter = hdr.i.counter + 1; + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i1) { + 2: accept; + default: finite_loop; + } + } + state mixed_finite_loop { + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i2) { + 1: start_loops; + 2: accept; + } + } + state mixed_infinite_loop { + transition select(hdr.i.counter) { + 3: accept; + default: start_loops; + } + } + state infinite_loop { + hdr.i.counter = hdr.i.counter + 1; + transition select(hdr.i.counter) { + 3: accept; + default: infinite_loop; + } + } +} + +control ingress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control vrfy(inout headers h, inout Meta m) { + apply { + } +} + +control update(inout headers h, inout Meta m) { + apply { + } +} + +control egress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control deparser(packet_out pkt, in headers h) { + apply { + pkt.emit(h.h); + pkt.emit(h.i); + } +} + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; diff --git a/testdata/p4_16_samples_outputs/parser-unroll-test9.p4-stderr b/testdata/p4_16_samples_outputs/parser-unroll-test9.p4-stderr new file mode 100644 index 00000000000..e69de29bb2d diff --git a/testdata/p4_16_samples_outputs/parser-unroll-test9.p4.entries.txt b/testdata/p4_16_samples_outputs/parser-unroll-test9.p4.entries.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/testdata/p4_16_samples_outputs/parser-unroll-test9.p4.p4info.txt b/testdata/p4_16_samples_outputs/parser-unroll-test9.p4.p4info.txt new file mode 100644 index 00000000000..9ec92493e4c --- /dev/null +++ b/testdata/p4_16_samples_outputs/parser-unroll-test9.p4.p4info.txt @@ -0,0 +1,3 @@ +pkg_info { + arch: "v1model" +} diff --git a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-1-midend.p4 b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-1-midend.p4 index 32eccc1d985..5ab4bf841b7 100644 --- a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-1-midend.p4 +++ b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-1-midend.p4 @@ -11,9 +11,6 @@ struct M { parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) { @name("ParserI.tmp_0") bit<16> tmp_0; @name("ParserI.tmp_2") bit<16> tmp_2; - state start { - transition s1; - } state s1 { packet.advance(32w16); tmp_0 = packet.lookahead>(); @@ -34,6 +31,9 @@ parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadat state s4 { transition accept; } + state start { + transition s1; + } } control IngressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) { diff --git a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-1.p4-stderr b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-1.p4-stderr index cbc7f8caaf8..ac6d7790049 100644 --- a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-1.p4-stderr +++ b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-1.p4-stderr @@ -1,2 +1,6 @@ [--Wwarn=invalid] warning: Parser cycle can't be unrolled, because ParserUnroll can't detect the number of loop iterations: Parser ParserI state chain: start, s1, s2, s2 +[--Wwarn=invalid] warning: Parser cycle can't be unrolled, because ParserUnroll can't detect the number of loop iterations: +Parser ParserI state chain: start, s1, s2, s1 +[--Wwarn=invalid] warning: Parser cycle can't be unrolled, because ParserUnroll can't detect the number of loop iterations: +Parser ParserI state chain: start, s1, s1 diff --git a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-midend.p4 b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-midend.p4 index 6ba6cdab74c..86396411c25 100644 --- a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-midend.p4 +++ b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537-midend.p4 @@ -39,15 +39,6 @@ struct M { } parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) { - state start { - packet.extract(hdr.h1); - packet.extract(hdr.h2); - transition select(hdr.h2.f1) { - 16w0x800: parse_ipv4; - 16w0x86dd: parse_ipv6; - default: accept; - } - } state parse_ipv4 { packet.extract(hdr.h3); transition select(hdr.h3.f2, hdr.h3.f3) { @@ -76,6 +67,15 @@ parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadat default: accept; } } + state start { + packet.extract(hdr.h1); + packet.extract(hdr.h2); + transition select(hdr.h2.f1) { + 16w0x800: parse_ipv4; + 16w0x86dd: parse_ipv6; + default: accept; + } + } } control IngressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) { diff --git a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537.p4-stderr b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537.p4-stderr index d313aa617cd..e69de29bb2d 100644 --- a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537.p4-stderr +++ b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-issue3537.p4-stderr @@ -1,8 +0,0 @@ -parser-unroll-issue3537.p4(62): [--Wwarn=ignore-prop] warning: Result of packet.extract is not defined: Exception: OverwritingHeader - packet.extract(hdr.h6); - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -parser-unroll-issue3537.p4(42): [--Wwarn=ignore-prop] warning: Result of packet.extract is not defined: Exception: OverwritingHeader - packet.extract(hdr.h3); - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -[--Wwarn=invalid] warning: Parser cycle can't be unrolled, because ParserUnroll can't detect the number of loop iterations: -Parser ParserI state chain: start, parse_ipv6, parse_udp, parse_ipv4, parse_udp, parse_ipv4, parse_udp diff --git a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9-first.p4 b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9-first.p4 new file mode 100644 index 00000000000..7f11eaecace --- /dev/null +++ b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9-first.p4 @@ -0,0 +1,96 @@ +#include +#define V1MODEL_VERSION 20180101 +#include + +header h_stack { + bit<8> i1; + bit<8> i2; +} + +header h_index { + bit<8> index; + bit<8> counter; +} + +struct headers { + h_stack[2] h; + h_index i; +} + +struct Meta { +} + +parser p(packet_in pkt, out headers hdr, inout Meta m, inout standard_metadata_t sm) { + state start { + pkt.extract(hdr.i); + hdr.i.counter = 8w0; + transition start_loops; + } + state start_loops { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.index) { + 8w0: mixed_finite_loop; + 8w1: mixed_infinite_loop; + 8w2: infinite_loop; + 8w3: finite_loop; + default: reject; + } + } + state finite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i1) { + 8w2: accept; + default: finite_loop; + } + } + state mixed_finite_loop { + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i2) { + 8w1: start_loops; + 8w2: accept; + } + } + state mixed_infinite_loop { + transition select(hdr.i.counter) { + 8w3: accept; + default: start_loops; + } + } + state infinite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.counter) { + 8w3: accept; + default: infinite_loop; + } + } +} + +control ingress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control vrfy(inout headers h, inout Meta m) { + apply { + } +} + +control update(inout headers h, inout Meta m) { + apply { + } +} + +control egress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control deparser(packet_out pkt, in headers h) { + apply { + pkt.emit(h.h); + pkt.emit(h.i); + } +} + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; diff --git a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9-frontend.p4 b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9-frontend.p4 new file mode 100644 index 00000000000..7f11eaecace --- /dev/null +++ b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9-frontend.p4 @@ -0,0 +1,96 @@ +#include +#define V1MODEL_VERSION 20180101 +#include + +header h_stack { + bit<8> i1; + bit<8> i2; +} + +header h_index { + bit<8> index; + bit<8> counter; +} + +struct headers { + h_stack[2] h; + h_index i; +} + +struct Meta { +} + +parser p(packet_in pkt, out headers hdr, inout Meta m, inout standard_metadata_t sm) { + state start { + pkt.extract(hdr.i); + hdr.i.counter = 8w0; + transition start_loops; + } + state start_loops { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.index) { + 8w0: mixed_finite_loop; + 8w1: mixed_infinite_loop; + 8w2: infinite_loop; + 8w3: finite_loop; + default: reject; + } + } + state finite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i1) { + 8w2: accept; + default: finite_loop; + } + } + state mixed_finite_loop { + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i2) { + 8w1: start_loops; + 8w2: accept; + } + } + state mixed_infinite_loop { + transition select(hdr.i.counter) { + 8w3: accept; + default: start_loops; + } + } + state infinite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.counter) { + 8w3: accept; + default: infinite_loop; + } + } +} + +control ingress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control vrfy(inout headers h, inout Meta m) { + apply { + } +} + +control update(inout headers h, inout Meta m) { + apply { + } +} + +control egress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control deparser(packet_out pkt, in headers h) { + apply { + pkt.emit(h.h); + pkt.emit(h.i); + } +} + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; diff --git a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9-midend.p4 b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9-midend.p4 new file mode 100644 index 00000000000..4dc4054dfc8 --- /dev/null +++ b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9-midend.p4 @@ -0,0 +1,161 @@ +#include +#define V1MODEL_VERSION 20180101 +#include + +header h_stack { + bit<8> i1; + bit<8> i2; +} + +header h_index { + bit<8> index; + bit<8> counter; +} + +struct headers { + h_stack[2] h; + h_index i; +} + +struct Meta { +} + +parser p(packet_in pkt, out headers hdr, inout Meta m, inout standard_metadata_t sm) { + state stateOutOfBound { + verify(false, error.StackOutOfBounds); + transition reject; + } + state finite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + pkt.extract(hdr.h[32w0]); + transition select(hdr.h[32w0].i1) { + 8w2: accept; + default: finite_loop1; + } + } + state finite_loop1 { + hdr.i.counter = hdr.i.counter + 8w1; + pkt.extract(hdr.h[32w1]); + transition select(hdr.h[32w1].i1) { + 8w2: accept; + default: finite_loop2; + } + } + state finite_loop2 { + hdr.i.counter = hdr.i.counter + 8w1; + transition stateOutOfBound; + } + state infinite_loop { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.counter) { + 8w3: accept; + default: infinite_loop; + } + } + state mixed_finite_loop { + pkt.extract(hdr.h[32w0]); + transition select(hdr.h[32w0].i2) { + 8w1: start_loops1; + 8w2: accept; + default: noMatch; + } + } + state mixed_finite_loop1 { + pkt.extract(hdr.h[32w1]); + transition select(hdr.h[32w1].i2) { + 8w1: start_loops2; + 8w2: accept; + default: noMatch; + } + } + state mixed_finite_loop2 { + transition stateOutOfBound; + } + state mixed_infinite_loop { + transition select(hdr.i.counter) { + 8w3: accept; + default: start_loops; + } + } + state mixed_infinite_loop1 { + transition select(hdr.i.counter) { + 8w3: accept; + default: start_loops1; + } + } + state mixed_infinite_loop2 { + transition select(hdr.i.counter) { + 8w3: accept; + default: start_loops2; + } + } + state noMatch { + verify(false, error.NoMatch); + transition reject; + } + state start { + pkt.extract(hdr.i); + hdr.i.counter = 8w0; + transition start_loops; + } + state start_loops { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.index) { + 8w0: mixed_finite_loop; + 8w1: mixed_infinite_loop; + 8w2: infinite_loop; + 8w3: finite_loop; + default: reject; + } + } + state start_loops1 { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.index) { + 8w0: mixed_finite_loop1; + 8w1: mixed_infinite_loop1; + 8w2: infinite_loop; + 8w3: finite_loop1; + default: reject; + } + } + state start_loops2 { + hdr.i.counter = hdr.i.counter + 8w1; + transition select(hdr.i.index) { + 8w0: mixed_finite_loop2; + 8w1: mixed_infinite_loop2; + 8w2: infinite_loop; + 8w3: finite_loop2; + default: reject; + } + } +} + +control ingress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control vrfy(inout headers h, inout Meta m) { + apply { + } +} + +control update(inout headers h, inout Meta m) { + apply { + } +} + +control egress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control deparser(packet_out pkt, in headers h) { + apply { + pkt.emit(h.h[0]); + pkt.emit(h.h[1]); + pkt.emit(h.i); + } +} + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; diff --git a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9.p4 b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9.p4 new file mode 100644 index 00000000000..bd853e8cdce --- /dev/null +++ b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9.p4 @@ -0,0 +1,96 @@ +#include +#define V1MODEL_VERSION 20180101 +#include + +header h_stack { + bit<8> i1; + bit<8> i2; +} + +header h_index { + bit<8> index; + bit<8> counter; +} + +struct headers { + h_stack[2] h; + h_index i; +} + +struct Meta { +} + +parser p(packet_in pkt, out headers hdr, inout Meta m, inout standard_metadata_t sm) { + state start { + pkt.extract(hdr.i); + hdr.i.counter = 0; + transition start_loops; + } + state start_loops { + hdr.i.counter = hdr.i.counter + 1; + transition select(hdr.i.index) { + 0: mixed_finite_loop; + 1: mixed_infinite_loop; + 2: infinite_loop; + 3: finite_loop; + default: reject; + } + } + state finite_loop { + hdr.i.counter = hdr.i.counter + 1; + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i1) { + 2: accept; + default: finite_loop; + } + } + state mixed_finite_loop { + pkt.extract(hdr.h.next); + transition select(hdr.h.last.i2) { + 1: start_loops; + 2: accept; + } + } + state mixed_infinite_loop { + transition select(hdr.i.counter) { + 3: accept; + default: start_loops; + } + } + state infinite_loop { + hdr.i.counter = hdr.i.counter + 1; + transition select(hdr.i.counter) { + 3: accept; + default: infinite_loop; + } + } +} + +control ingress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control vrfy(inout headers h, inout Meta m) { + apply { + } +} + +control update(inout headers h, inout Meta m) { + apply { + } +} + +control egress(inout headers h, inout Meta m, inout standard_metadata_t sm) { + apply { + } +} + +control deparser(packet_out pkt, in headers h) { + apply { + pkt.emit(h.h); + pkt.emit(h.i); + } +} + +V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main; diff --git a/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9.p4-stderr b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9.p4-stderr new file mode 100644 index 00000000000..6a8d84ee2a5 --- /dev/null +++ b/testdata/p4_16_samples_outputs/parser-unroll/parser-unroll-test9.p4-stderr @@ -0,0 +1,8 @@ +[--Wwarn=invalid] warning: Parser cycle can't be unrolled, because ParserUnroll can't detect the number of loop iterations: +Parser p state chain: start, start_loops, infinite_loop, infinite_loop +[--Wwarn=invalid] warning: Parser cycle can't be unrolled, because ParserUnroll can't detect the number of loop iterations: +Parser p state chain: start, start_loops, mixed_infinite_loop, start_loops +[--Wwarn=invalid] warning: Parser cycle can't be unrolled, because ParserUnroll can't detect the number of loop iterations: +Parser p state chain: start, start_loops, mixed_finite_loop, start_loops, mixed_infinite_loop, start_loops +[--Wwarn=invalid] warning: Parser cycle can't be unrolled, because ParserUnroll can't detect the number of loop iterations: +Parser p state chain: start, start_loops, mixed_finite_loop, start_loops, mixed_finite_loop, start_loops, mixed_infinite_loop, start_loops