Unroll finite loops in the programs with infinite ones

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<std::vector<ParserStateInfo*>*, bool>;
+    using EvaluationStateResult =
+        std::tuple<std::vector<ParserStateInfo*>*, bool, IR::IndexedVector<IR::StatOrDecl>>;
 
     /// 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<IR::StatOrDecl>;
+
     /// generate call OutOfBound
-    void addOutFoBound(ParserStateInfo* stateInfo, std::unordered_set<cstring>& newStates,
-                       bool checkBefore = true) {
+    void addOutOfBound(ParserStateInfo* stateInfo, std::unordered_set<cstring>& 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<IR::StatOrDecl>(),
-                                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;

midend/parserUnroll.h

@@ -67,6 +67,8 @@ class StackVariableHash {
 };
 
 typedef std::unordered_map<StackVariable, size_t, StackVariableHash> StackVariableMap;
+typedef std::unordered_map<StackVariable, const IR::Expression*, StackVariableHash>
+    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<cstring> scenarioStates;
-    std::unordered_set<cstring> scenarioHS;  // scenario header stack's operations
+    std::unordered_set<cstring> 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;
         }
     }
 };

testdata/p4_16_samples/parser-unroll-test9.p4

@@ -0,0 +1,96 @@
+#include <core.p4>
+#define V1MODEL_VERSION 20180101
+#include <v1model.p4>
+
+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;