From 00f08c5ce3bffe287a19856deb3b057b0b6db8ce Mon Sep 17 00:00:00 2001 From: Volodymyr Peschanenko Date: Wed, 31 Aug 2022 17:26:12 +0300 Subject: [PATCH 1/4] Fixing bug for issue692-bmv2 --- midend/parserUnroll.cpp | 72 ++++++++++++++++++++++++++++++----------- 1 file changed, 54 insertions(+), 18 deletions(-) diff --git a/midend/parserUnroll.cpp b/midend/parserUnroll.cpp index f19679cf116..43fd41ba2e5 100644 --- a/midend/parserUnroll.cpp +++ b/midend/parserUnroll.cpp @@ -75,8 +75,9 @@ struct VisitedKey { if (name > e.name) return false; std::unordered_map, StackVariableHash > mp; - for (auto& i1 : indexes) + for (auto& i1 : indexes) { mp.emplace(i1.first, std::make_pair(i1.second, -1)); + } for (auto& i2 : e.indexes) { auto ref = mp.find(i2.first); if (ref == mp.end()) @@ -153,7 +154,7 @@ class ParserStateRewriter : public Transform { ExpressionEvaluator* afterExec, StatesVisitedMap& visitedStates) : parserStructure(parserStructure), state(state), valueMap(valueMap), refMap(refMap), typeMap(typeMap), afterExec(afterExec), - visitedStates(visitedStates) { + visitedStates(visitedStates), wasOutOfBound(false) { CHECK_NULL(parserStructure); CHECK_NULL(state); CHECK_NULL(refMap); CHECK_NULL(typeMap); CHECK_NULL(parserStructure); CHECK_NULL(state); @@ -175,7 +176,11 @@ class ParserStateRewriter : public Transform { auto* res = value->to()->constant->clone(); newExpression->right = res; BUG_CHECK(res->fitsInt64(), "To big integer for a header stack index %1%", res); - state->statesIndexes[expression->left] = (size_t)res->asInt64(); + const auto* arrayType = basetype->to(); + if (res->asUnsigned() >= arrayType->getSize()) { + wasOutOfBound = true; + return expression; + } return newExpression; } @@ -192,13 +197,17 @@ class ParserStateRewriter : public Transform { unsigned offset = 0; if (state->statesIndexes.count(expression->expr)) { idx = state->statesIndexes.at(expression->expr); - if (idx + 1 < array->size && expression->member.name != IR::Type_Stack::last) { + if (expression->member.name != IR::Type_Stack::last) { offset = 1; } } if (expression->member.name == IR::Type_Stack::lastIndex) { return new IR::Constant(IR::Type_Bits::get(32), idx); } else { + if (idx + offset >= array->size) { + wasOutOfBound = true; + return expression; + } state->statesIndexes[expression->expr] = idx + offset; return new IR::ArrayIndex(expression->expr->clone(), new IR::Constant(IR::Type_Bits::get(32), idx + offset)); @@ -218,6 +227,7 @@ class ParserStateRewriter : public Transform { return new IR::PathExpression(expression->type, new IR::Path(newName, false)); } inline size_t getIndex() { return currentIndex; } + bool isOutOfBound() {return wasOutOfBound;} protected: const IR::Type* getTypeArray(const IR::Node* element) { @@ -277,6 +287,7 @@ class ParserStateRewriter : public Transform { ExpressionEvaluator* afterExec; StatesVisitedMap& visitedStates; size_t currentIndex; + bool wasOutOfBound; }; class ParserSymbolicInterpreter { @@ -447,6 +458,9 @@ class ParserSymbolicInterpreter { ParserStateRewriter rewriter(structure, state, valueMap, refMap, typeMap, &ev, visitedStates); const IR::Node* node = sord->apply(rewriter); + if (rewriter.isOutOfBound()) { + return nullptr; + } newSord = node->to(); LOG2("After " << sord << " state is\n" << valueMap); return newSord; @@ -472,6 +486,9 @@ class ParserSymbolicInterpreter { ParserStateRewriter rewriter(structure, state, valueMap, refMap, typeMap, nullptr, visitedStates); const IR::Expression* node = select->apply(rewriter); + if (rewriter.isOutOfBound()) { + return EvaluationSelectResult(nullptr, nullptr); + } CHECK_NULL(node); newSelect = node->to(); CHECK_NULL(newSelect); @@ -489,6 +506,9 @@ class ParserSymbolicInterpreter { ParserStateRewriter rewriter(structure, state, valueMap, refMap, typeMap, &ev, visitedStates); const IR::Node* node = se->select->apply(rewriter); + if (rewriter.isOutOfBound()) { + return EvaluationSelectResult(nullptr, nullptr); + } const IR::ListExpression* newListSelect = node->to(); auto etalonStateIndexes = state->statesIndexes; for (auto c : se->selectCases) { @@ -501,6 +521,9 @@ class ParserSymbolicInterpreter { ParserStateRewriter rewriter(structure, state, valueMap, refMap, typeMap, nullptr, visitedStates); const IR::Node* node = c->apply(rewriter); + if (rewriter.isOutOfBound()) { + return EvaluationSelectResult(nullptr, nullptr); + } CHECK_NULL(node); auto newC = node->to(); CHECK_NULL(newC); @@ -601,10 +624,6 @@ class ParserSymbolicInterpreter { // If no header validity has changed we can't really unroll if (!headerValidityChange(crt->before, state->before)) { - if (unroll) - ::warning(ErrorType::ERR_INVALID, - "Parser cycle cannot be unrolled:\n%1%", - stateChain(state)); return true; } break; @@ -616,7 +635,6 @@ class ParserSymbolicInterpreter { /// Gets new name for a state IR::ID getNewName(ParserStateInfo* state) { if (state->currentIndex == 0) { - structure->callsIndexes.emplace(state->state->name.name, 0); return state->state->name; } return IR::ID(state->state->name + std::to_string(state->currentIndex)); @@ -649,7 +667,9 @@ class ParserSymbolicInterpreter { state->after = valueMap; auto result = evaluateSelect(state, valueMap); if (unroll) { - BUG_CHECK(result.second, "Can't generate new selection %1%", state); + if (result.second == nullptr) { + return EvaluationStateResult(nullptr, true); + } if (state->name == newName) { state->newState = new IR::ParserState(state->state->srcInfo, newName, state->state->annotations, components, @@ -674,6 +694,22 @@ class ParserSymbolicInterpreter { parser = structure->parser; hasOutOfboundState = false; } + + /// generate call OutOfBound + void addOutFoBound(ParserStateInfo* stateInfo, std::unordered_set& newStates, + bool checkBefore = true) { + hasOutOfboundState = true; + IR::ID newName = getNewName(stateInfo); + if (checkBefore && newStates.count(newName)) { + return; + } + newStates.insert(newName); + stateInfo->newState = new IR::ParserState(newName, + IR::IndexedVector(), + new IR::PathExpression(new IR::Type_State(), + new IR::Path(outOfBoundsStateName, false))); + } + /// running symbolic execution ParserInfo* run() { synthesizedParser = new ParserInfo(); @@ -682,6 +718,8 @@ class ParserSymbolicInterpreter { // error during initializer evaluation return synthesizedParser; auto startInfo = newStateInfo(nullptr, structure->start->name.name, initMap, 0); + structure->callsIndexes.emplace(structure->start->name.name, 0); + startInfo->scenarioStates.insert(structure->start->name.name); std::vector toRun; // worklist toRun.push_back(startInfo); std::set visited; @@ -703,21 +741,19 @@ class ParserSymbolicInterpreter { stateInfo->scenarioStates.insert(stateInfo->name); // add to loops detection bool infLoop = checkLoops(stateInfo); if (infLoop) { - wasError = true; // don't evaluate successors anymore + // generate call OutOfBound + addOutFoBound(stateInfo, newStates); continue; } - bool notAdded = newStates.count(getNewName(stateInfo)) == 0; + 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 && - stateInfo->state->name !=stateInfo->predecessor->newState->name) { + newName.name !=stateInfo->predecessor->newState->name) { // generate call OutOfBound - hasOutOfboundState = true; - stateInfo->newState = new IR::ParserState(getNewName(stateInfo), - IR::IndexedVector(), - new IR::PathExpression(new IR::Type_State(), - new IR::Path(outOfBoundsStateName, false))); + addOutFoBound(stateInfo, newStates, false); } else { // save current state if (notAdded) { From 8b1ce9a0d886c7d5f08ffb7ab71d6ee94d706489 Mon Sep 17 00:00:00 2001 From: Volodymyr Peschanenko Date: Wed, 31 Aug 2022 20:03:43 +0300 Subject: [PATCH 2/4] Changes according review --- midend/parserUnroll.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/midend/parserUnroll.cpp b/midend/parserUnroll.cpp index 43fd41ba2e5..408b2dd735f 100644 --- a/midend/parserUnroll.cpp +++ b/midend/parserUnroll.cpp @@ -695,8 +695,8 @@ class ParserSymbolicInterpreter { hasOutOfboundState = false; } - /// generate call OutOfBound - void addOutFoBound(ParserStateInfo* stateInfo, std::unordered_set& newStates, + /// Creates a new state that immediately transitions to the "outOfBoundsState" state. + void addOutOfBound(ParserStateInfo* stateInfo, std::unordered_set& newStates, bool checkBefore = true) { hasOutOfboundState = true; IR::ID newName = getNewName(stateInfo); @@ -743,7 +743,7 @@ class ParserSymbolicInterpreter { if (infLoop) { // don't evaluate successors anymore // generate call OutOfBound - addOutFoBound(stateInfo, newStates); + addOutOfBound(stateInfo, newStates); continue; } IR::ID newName = getNewName(stateInfo); @@ -753,7 +753,7 @@ class ParserSymbolicInterpreter { if (nextStates.second && stateInfo->predecessor && newName.name !=stateInfo->predecessor->newState->name) { // generate call OutOfBound - addOutFoBound(stateInfo, newStates, false); + addOutOfBound(stateInfo, newStates, false); } else { // save current state if (notAdded) { From 2ef69a205db216fe5d25bd734ccd436bb8e54a88 Mon Sep 17 00:00:00 2001 From: Volodymyr Peschanenko Date: Thu, 1 Sep 2022 17:23:07 +0300 Subject: [PATCH 3/4] These changes allow to pass TVL_parsing, pna-direction-parser-err examples --- midend/parserUnroll.cpp | 26 ++++++++++++++++++-------- midend/parserUnroll.h | 6 +++++- 2 files changed, 23 insertions(+), 9 deletions(-) diff --git a/midend/parserUnroll.cpp b/midend/parserUnroll.cpp index 408b2dd735f..e48bf7f1c4d 100644 --- a/midend/parserUnroll.cpp +++ b/midend/parserUnroll.cpp @@ -175,7 +175,12 @@ class ParserStateRewriter : public Transform { return expression; auto* res = value->to()->constant->clone(); newExpression->right = res; - BUG_CHECK(res->fitsInt64(), "To big integer for a header stack index %1%", res); + if (!res->fitsInt64()) { + // we need to leave expression as is. + ::warning(ErrorType::ERR_EXPRESSION, "Index can't be concretized : %1%", + expression); + return expression; + } const auto* arrayType = basetype->to(); if (res->asUnsigned() >= arrayType->getSize()) { wasOutOfBound = true; @@ -481,7 +486,6 @@ class ParserSymbolicInterpreter { auto path = select->to()->path; auto next = refMap->getDeclaration(path); BUG_CHECK(next->is(), "%1%: expected a state", path); - // update call indexes ParserStateRewriter rewriter(structure, state, valueMap, refMap, typeMap, nullptr, visitedStates); @@ -502,7 +506,13 @@ class ParserSymbolicInterpreter { auto se = select->to(); IR::Vector newSelectCases; ExpressionEvaluator ev(refMap, typeMap, valueMap); - ev.evaluate(se->select, true); + try { + ev.evaluate(se->select, true); + } + catch (...) { + // Ignore throws from evaluator. + // If an index of a header stack is not substituted then we should leave a state as is. + } ParserStateRewriter rewriter(structure, state, valueMap, refMap, typeMap, &ev, visitedStates); const IR::Node* node = se->select->apply(rewriter); @@ -695,14 +705,14 @@ class ParserSymbolicInterpreter { hasOutOfboundState = false; } - /// Creates a new state that immediately transitions to the "outOfBoundsState" state. - void addOutOfBound(ParserStateInfo* stateInfo, std::unordered_set& newStates, + /// generate call OutOfBound + void addOutFoBound(ParserStateInfo* stateInfo, std::unordered_set& newStates, bool checkBefore = true) { - hasOutOfboundState = true; IR::ID newName = getNewName(stateInfo); if (checkBefore && newStates.count(newName)) { return; } + hasOutOfboundState = true; newStates.insert(newName); stateInfo->newState = new IR::ParserState(newName, IR::IndexedVector(), @@ -743,7 +753,7 @@ class ParserSymbolicInterpreter { if (infLoop) { // don't evaluate successors anymore // generate call OutOfBound - addOutOfBound(stateInfo, newStates); + addOutFoBound(stateInfo, newStates); continue; } IR::ID newName = getNewName(stateInfo); @@ -753,7 +763,7 @@ class ParserSymbolicInterpreter { if (nextStates.second && stateInfo->predecessor && newName.name !=stateInfo->predecessor->newState->name) { // generate call OutOfBound - addOutOfBound(stateInfo, newStates, false); + addOutFoBound(stateInfo, newStates, false); } else { // save current state if (notAdded) { diff --git a/midend/parserUnroll.h b/midend/parserUnroll.h index 95437a93d08..6893d7bb21a 100644 --- a/midend/parserUnroll.h +++ b/midend/parserUnroll.h @@ -262,8 +262,12 @@ class RewriteAllParsers : public Transform { } for (auto& i : rewriter->current.result->states) { for (auto& j : *i.second) - if (j->newState) + if (j->newState) { + if (rewriter->hasOutOfboundState && j->newState->name.name == "stateOutOfBound") { + continue; + } newParser->states.push_back(j->newState); + } } // adding accept/reject newParser->states.push_back(new IR::ParserState(IR::ParserState::accept, nullptr)); From 81cacba6411d52e95738f73d9856ed66514e07f6 Mon Sep 17 00:00:00 2001 From: Volodymyr Peschanenko Date: Thu, 1 Sep 2022 18:54:38 +0300 Subject: [PATCH 4/4] update --- midend/parserUnroll.cpp | 5 +++-- midend/parserUnroll.h | 3 ++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/midend/parserUnroll.cpp b/midend/parserUnroll.cpp index e48bf7f1c4d..7942640e638 100644 --- a/midend/parserUnroll.cpp +++ b/midend/parserUnroll.cpp @@ -177,7 +177,7 @@ class ParserStateRewriter : public Transform { newExpression->right = res; if (!res->fitsInt64()) { // we need to leave expression as is. - ::warning(ErrorType::ERR_EXPRESSION, "Index can't be concretized : %1%", + ::warning(ErrorType::ERR_EXPRESSION, "Index can't be concretized : %1%", expression); return expression; } @@ -511,7 +511,8 @@ class ParserSymbolicInterpreter { } catch (...) { // Ignore throws from evaluator. - // If an index of a header stack is not substituted then we should leave a state as is. + // If an index of a header stack is not substituted then + // we should leave a state as is. } ParserStateRewriter rewriter(structure, state, valueMap, refMap, typeMap, &ev, visitedStates); diff --git a/midend/parserUnroll.h b/midend/parserUnroll.h index 6893d7bb21a..d15d40579a0 100644 --- a/midend/parserUnroll.h +++ b/midend/parserUnroll.h @@ -263,7 +263,8 @@ class RewriteAllParsers : public Transform { for (auto& i : rewriter->current.result->states) { for (auto& j : *i.second) if (j->newState) { - if (rewriter->hasOutOfboundState && j->newState->name.name == "stateOutOfBound") { + if (rewriter->hasOutOfboundState && + j->newState->name.name == "stateOutOfBound") { continue; } newParser->states.push_back(j->newState);