ExprEngine; Fixed testing

This commit is contained in:
Daniel Marjamäki 2020-06-28 13:41:27 +02:00
parent f85cdd3f77
commit c42c751d61
4 changed files with 76 additions and 8 deletions

View File

@ -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())

View File

@ -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);

View File

@ -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<ExprEngine::IntRange>(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();

View File

@ -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));
}