Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixing bug in parserUnroll #3503

Merged
merged 4 commits into from
Sep 9, 2022
Merged

Fixing bug in parserUnroll #3503

Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
00f08c5
Fixing bug for issue692-bmv2
VolodymyrPeschanenko Aug 31, 2022
8b1ce9a
Changes according review
VolodymyrPeschanenko Aug 31, 2022
2ef69a2
These changes allow to pass TVL_parsing, pna-direction-parser-err exa…
VolodymyrPeschanenko Sep 1, 2022
81cacba
update
VolodymyrPeschanenko Sep 1, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
Fixing bug for issue692-bmv2
  • Loading branch information
@VolodymyrPeschanenko
VolodymyrPeschanenko committed Aug 31, 2022
commit 00f08c5ce3bffe287a19856deb3b057b0b6db8ce
72 changes: 54 additions & 18 deletions midend/parserUnroll.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,8 +75,9 @@ struct VisitedKey {
if (name > e.name)
return false;
std::unordered_map<StackVariable, std::pair<size_t, size_t>, 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())
Expand Down Expand Up @@ -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);
Expand All @@ -175,7 +176,11 @@ class ParserStateRewriter : public Transform {
auto* res = value->to<SymbolicInteger>()->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<IR::Type_Stack>();
if (res->asUnsigned() >= arrayType->getSize()) {
wasOutOfBound = true;
return expression;
}
return newExpression;
}

Expand All @@ -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));
Expand All @@ -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) {
Expand Down Expand Up @@ -277,6 +287,7 @@ class ParserStateRewriter : public Transform {
ExpressionEvaluator* afterExec;
StatesVisitedMap& visitedStates;
size_t currentIndex;
bool wasOutOfBound;
};

class ParserSymbolicInterpreter {
Expand Down Expand Up @@ -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<IR::StatOrDecl>();
LOG2("After " << sord << " state is\n" << valueMap);
return newSord;
Expand All @@ -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<IR::Expression>();
CHECK_NULL(newSelect);
Expand All @@ -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<IR::ListExpression>();
auto etalonStateIndexes = state->statesIndexes;
for (auto c : se->selectCases) {
Expand All @@ -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<IR::SelectCase>();
CHECK_NULL(newC);
Expand Down Expand Up @@ -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;
Expand All @@ -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));
Expand Down Expand Up @@ -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,
Expand All @@ -674,6 +694,22 @@ class ParserSymbolicInterpreter {
parser = structure->parser;
hasOutOfboundState = false;
}

/// generate call OutOfBound
VolodymyrPeschanenkoLitSoft marked this conversation as resolved.
Show resolved Hide resolved
void addOutFoBound(ParserStateInfo* stateInfo, std::unordered_set<cstring>& newStates,
VolodymyrPeschanenkoLitSoft marked this conversation as resolved.
Show resolved Hide resolved
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<IR::StatOrDecl>(),
new IR::PathExpression(new IR::Type_State(),
new IR::Path(outOfBoundsStateName, false)));
}

/// running symbolic execution
ParserInfo* run() {
synthesizedParser = new ParserInfo();
Expand All @@ -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<ParserStateInfo*> toRun; // worklist
toRun.push_back(startInfo);
std::set<VisitedKey> visited;
Expand All @@ -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<IR::StatOrDecl>(),
new IR::PathExpression(new IR::Type_State(),
new IR::Path(outOfBoundsStateName, false)));
addOutFoBound(stateInfo, newStates, false);
} else {
// save current state
if (notAdded) {
Expand Down