diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 48bf50ea7..39b05e4f6 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -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(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(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); } diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 6063862a6..a6af2ec94 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -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(&value); if (!b) return; - ret = b->getExpr(dataBase); + if (!ret.empty()) + ret += "\n"; + ret += b->getExpr(dataBase); }; std::vector 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; }", "=="));