ExprEngine: Initial handling of switch

This commit is contained in:
Daniel Marjamäki 2019-10-06 19:58:51 +02:00
parent 05aae9569b
commit d82b1b29ce
2 changed files with 67 additions and 6 deletions

View File

@ -225,6 +225,13 @@ namespace {
else
constraints.push_back(notValue(condValue));
}
void addConstraint(ExprEngine::ValuePtr lhsValue, ExprEngine::ValuePtr rhsValue, bool equals) {
if (!lhsValue || !rhsValue)
return;
constraints.push_back(std::make_shared<ExprEngine::BinOpResult>(equals?"==":"!=", lhsValue, rhsValue));
}
private:
TrackExecution * const mTrackExecution;
const int mDataIndex;
@ -1051,10 +1058,18 @@ static void execute(const Token *start, const Token *end, Data &data)
continue;
}
if (tok->str() == "break")
return;
if (tok->str() == "break") {
const Scope *scope = tok->scope();
while (scope->type == Scope::eIf || scope->type == Scope::eElse)
scope = scope->nestedIn;
tok = scope->bodyEnd;
}
if (Token::Match(tok, "for|while|switch ("))
if (Token::simpleMatch(tok, "try"))
// TODO this is a bailout
throw std::runtime_error("Unhandled:" + tok->str());
if (Token::Match(tok, "for|while ("))
// TODO this is a bailout
throw std::runtime_error("Unhandled:" + tok->str());
@ -1081,11 +1096,14 @@ static void execute(const Token *start, const Token *end, Data &data)
tok = tok->linkAt(1);
} else if (Token::Match(tok, "%var% ;"))
data.assignValue(tok, tok->varId(), createVariableValue(*tok->variable(), data));
} else if (!tok->astParent() && (tok->astOperand1() || tok->astOperand2()))
} else if (!tok->astParent() && (tok->astOperand1() || tok->astOperand2())) {
executeExpression(tok, data);
if (Token::Match(tok, "throw|return"))
return;
}
else if (Token::simpleMatch(tok, "if (")) {
const Token *cond = tok->next()->astOperand2();
const Token *cond = tok->next()->astOperand2(); // TODO: C++17 condition
const ExprEngine::ValuePtr condValue = executeExpression(cond, data);
Data ifData(data);
Data elseData(data);
@ -1104,6 +1122,28 @@ static void execute(const Token *start, const Token *end, Data &data)
return;
}
else if (Token::simpleMatch(tok, "switch (")) {
auto condValue = executeExpression(tok->next()->astOperand2(), data); // TODO: C++17 condition
const Token *bodyStart = tok->linkAt(1)->next();
const Token *bodyEnd = bodyStart->link();
const Token *defaultStart = nullptr;
Data defaultData(data);
for (const Token *tok2 = bodyStart->next(); tok2 != bodyEnd; tok2 = tok2->next()) {
if (tok2->str() == "{")
tok2 = tok2->link();
else if (Token::Match(tok2, "case %num% :")) {
auto caseValue = std::make_shared<ExprEngine::IntRange>(tok2->strAt(1), MathLib::toLongNumber(tok2->strAt(1)), MathLib::toLongNumber(tok2->strAt(1)));
Data caseData(data);
caseData.addConstraint(condValue, caseValue, true);
defaultData.addConstraint(condValue, caseValue, false);
execute(tok2->tokAt(2), end, caseData);
} else if (Token::simpleMatch(tok2, "default :"))
defaultStart = tok2;
}
execute(defaultStart ? defaultStart : bodyEnd, end, defaultData);
return;
}
if (Token::simpleMatch(tok, "} else {"))
tok = tok->linkAt(2);
}

View File

@ -44,6 +44,8 @@ private:
TEST_CASE(if1);
TEST_CASE(ifelse1);
TEST_CASE(switch1);
TEST_CASE(array1);
TEST_CASE(array2);
TEST_CASE(array3);
@ -85,7 +87,9 @@ private:
auto b = dynamic_cast<const ExprEngine::BinOpResult *>(&value);
if (!b)
return;
ret = b->getExpr(dataBase);
if (!ret.empty())
ret += "\n";
ret += b->getExpr(dataBase);
};
std::vector<ExprEngine::Callback> callbacks;
callbacks.push_back(f);
@ -181,6 +185,23 @@ private:
}
void switch1() {
const char code[] = "void f(int x) {\n"
" switch (x) {\n"
" case 1: x==3; break;\n"
" case 2: x>0; break;\n"
" };\n"
" x<=4;\n"
"}";
ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (<= $1 2147483647))\n"
"(assert (>= $1 (- 2147483648)))\n"
"(assert (= $1 1))\n"
"(assert (= $1 3))\n",
expr(code, "=="));
}
void array1() {
ASSERT_EQUALS("(assert (= 5 0))\n",
expr("int f() { int arr[10]; arr[4] = 5; return arr[4]==0; }", "=="));