diff --git a/lib/astutils.cpp b/lib/astutils.cpp index f43713107..712847e46 100644 --- a/lib/astutils.cpp +++ b/lib/astutils.cpp @@ -436,6 +436,34 @@ const Token* getCondTokFromEnd(const Token* endBlock) return getCondTokFromEndImpl(endBlock); } +bool extractForLoopValues(const Token *forToken, + nonneg int * const varid, + MathLib::bigint * const initValue, + MathLib::bigint * const stepValue, + MathLib::bigint * const lastValue) +{ + if (!Token::simpleMatch(forToken, "for (") || !Token::simpleMatch(forToken->next()->astOperand2(), ";")) + return false; + const Token *initExpr = forToken->next()->astOperand2()->astOperand1(); + const Token *condExpr = forToken->next()->astOperand2()->astOperand2()->astOperand1(); + const Token *incExpr = forToken->next()->astOperand2()->astOperand2()->astOperand2(); + if (!initExpr || !initExpr->isBinaryOp() || initExpr->str() != "=" || !Token::Match(initExpr->astOperand1(), "%var%") || !initExpr->astOperand2()->hasKnownIntValue()) + return false; + *varid = initExpr->astOperand1()->varId(); + *initValue = initExpr->astOperand2()->getKnownIntValue(); + if (!Token::Match(condExpr, "<|<=") || !condExpr->isBinaryOp() || condExpr->astOperand1()->varId() != *varid || !condExpr->astOperand2()->hasKnownIntValue()) + return false; + if (!incExpr || !incExpr->isUnaryOp("++") || incExpr->astOperand1()->varId() != *varid) + return false; + *stepValue = 1; + if (condExpr->str() == "<") + *lastValue = condExpr->astOperand2()->getKnownIntValue() - 1; + else + *lastValue = condExpr->astOperand2()->getKnownIntValue(); + return true; +} + + static const Token * getVariableInitExpression(const Variable * var) { if (!var || !var->declEndToken()) diff --git a/lib/astutils.h b/lib/astutils.h index eb83e2bc9..3cd883f4d 100644 --- a/lib/astutils.h +++ b/lib/astutils.h @@ -108,6 +108,15 @@ const Token* getCondTok(const Token* tok); Token* getCondTokFromEnd(Token* endBlock); const Token* getCondTokFromEnd(const Token* endBlock); +/** + * Extract for loop values: loopvar varid, init value, step value, last value (inclusive) + */ +bool extractForLoopValues(const Token *forToken, + nonneg int * const varid, + long long * const initValue, + long long * const stepValue, + long long * const lastValue); + bool precedes(const Token * tok1, const Token * tok2); bool exprDependsOnThis(const Token* expr, nonneg int depth = 0); diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 74682f5bd..dc31b8ad8 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -371,8 +371,12 @@ namespace { int recursion; std::time_t startTime; - bool isC() const OVERRIDE { return tokenizer->isC(); } - bool isCPP() const OVERRIDE { return tokenizer->isCPP(); } + bool isC() const OVERRIDE { + return tokenizer->isC(); + } + bool isCPP() const OVERRIDE { + return tokenizer->isCPP(); + } ExprEngine::ValuePtr executeContract(const Function *function, ExprEngine::ValuePtr(*executeExpression)(const Token*, Data&)) { const auto it = settings->functionContracts.find(function->fullName()); @@ -2344,6 +2348,17 @@ static std::string execute(const Token *start, const Token *end, Data &data) return ret.str(); } + if (Token::simpleMatch(tok, "for (")) { + nonneg int varid; + MathLib::bigint initValue, stepValue, lastValue; + if (extractForLoopValues(tok, &varid, &initValue, &stepValue, &lastValue)) { + auto loopValues = std::make_shared(data.getNewSymbolName(), initValue, lastValue); + data.assignValue(tok, varid, loopValues); + tok = tok->linkAt(1); + continue; + } + } + if (Token::Match(tok, "for|while (") && Token::simpleMatch(tok->linkAt(1), ") {")) { const Token *bodyStart = tok->linkAt(1)->next(); const Token *bodyEnd = bodyStart->link(); diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index c273d2103..b34f38e0a 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -66,6 +66,8 @@ private: TEST_CASE(switch1); TEST_CASE(switch2); + TEST_CASE(for1); + TEST_CASE(while1); TEST_CASE(while2); TEST_CASE(while3); @@ -328,13 +330,13 @@ private: ASSERT_EQUALS("1:26: $3=0:ffffffff\n" "1:26: $2=-128:127\n" - "1:27: { s=($4,[$3],[:]=$2)}\n", + "1:27: 0:{ s=($4,[$3],[:]=$2)}\n", trackExecution("void foo() { std::string s; }", &settings)); ASSERT_EQUALS("1:52: $3=0:ffffffff\n" "1:52: $2=-128:127\n" - "1:66: { s=($4,[$3],[:]=$2)}\n", + "1:66: 0:{ s=($4,[$3],[:]=$2)}\n", trackExecution("std::string getName(int); void foo() { std::string s = getName(1); }", &settings)); } @@ -481,6 +483,20 @@ private: expr(code, "==")); } + + void for1() { + const char code[] = "void f() {\n" + " int x[10];\n" + " for (int i = 0; i < 10; i++) x[i] = 0;\n" + " x[4] == 67;\n" + "}"; + ASSERT_EQUALS("(and (>= $3 (- 2147483648)) (<= $3 2147483647))\n" + "(= $3 67)\n" + "z3::sat\n", + expr(code, "==")); + } + + void while1() { const char code[] = "void f(int y) {\n" " int x = 0;\n" @@ -566,7 +582,7 @@ private: "void f() { int x = buf[0]; }"; ASSERT_EQUALS("2:16: $2:0=-2147483648:2147483647\n" "2:20: $2=-2147483648:2147483647\n" - "2:26: { buf=($1,[10],[:]=$2) x=$2:0}\n", + "2:26: 0:{ buf=($1,[10],[:]=$2) x=$2:0}\n", trackExecution(code)); } @@ -577,9 +593,9 @@ private: " return buf[0][1][2];\n" "}"; ASSERT_EQUALS("1:14: $1=-2147483648:2147483647\n" - "1:14: { x=$1}\n" - "2:19: { x=$1 buf=($2,[3][4][5],[:]=?)}\n" - "3:20: { x=$1 buf=($2,[3][4][5],[:]=?,[((20)*($1))+(7)]=10)}\n", + "1:14: 0:{ x=$1}\n" + "2:19: 0:{ x=$1 buf=($2,[3][4][5],[:]=?)}\n" + "3:20: 0:{ x=$1 buf=($2,[3][4][5],[:]=?,[((20)*($1))+(7)]=10)}\n", trackExecution(code)); }