walkero
/
cppcheck
1
0
Fork 0
Code Issues Pull Requests Projects Releases 1 Wiki Activity

ExprEngine: Fix FP for 'int' overflows

This commit is contained in:
Daniel Marjamäki 2019-10-09 11:24:57 +02:00
parent b7e48a9b27
commit 273a1a7402
2 changed files with 66 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
lib/exprengine.cpp
View File

@ -564,9 +564,11 @@ struct ExprData {
return it->second; return it->second;
auto e = context.int_const(v->name.c_str()); auto e = context.int_const(v->name.c_str());
valueExpr.emplace(v->name, e); valueExpr.emplace(v->name, e);
if (intRange->maxValue <= INT_MAX) if (intRange->minValue >= INT_MIN && intRange->maxValue <= INT_MAX)
assertionList.push_back(e >= int(intRange->minValue) && e <= int(intRange->maxValue));
else if (intRange->maxValue <= INT_MAX)
assertionList.push_back(e <= int(intRange->maxValue)); assertionList.push_back(e <= int(intRange->maxValue));
if (intRange->minValue >= INT_MIN) else if (intRange->minValue >= INT_MIN)
assertionList.push_back(e >= int(intRange->minValue)); assertionList.push_back(e >= int(intRange->minValue));
return e; return e;
} }
@ -708,6 +710,17 @@ std::string ExprEngine::BinOpResult::getExpr(ExprEngine::DataBase *dataBase) con
solver.add(e); solver.add(e);
std::ostringstream os; std::ostringstream os;
os << solver; os << solver;
switch (solver.check()) {
case z3::sat:
os << "z3::sat";
break;
case z3::unsat:
os << "z3::unsat";
break;
case z3::unknown:
os << "z3::unknown";
break;
}
return os.str(); return os.str();
#else #else
(void)dataBase; (void)dataBase;
@ -1369,7 +1382,7 @@ void ExprEngine::runChecks(ErrorLogger *errorLogger, const Tokenizer *tokenizer,
std::string errorMessage; std::string errorMessage;
if (tok->valueType()->sign == ::ValueType::Sign::SIGNED) { if (tok->valueType()->sign == ::ValueType::Sign::SIGNED) {
MathLib::bigint v = 1LL << (bits - 1); MathLib::bigint v = 1LL << (bits - 1);
if (b->isGreaterThan(dataBase, v)) if (b->isGreaterThan(dataBase, v-1))
errorMessage = "greater than " + std::to_string(v); errorMessage = "greater than " + std::to_string(v);
if (b->isLessThan(dataBase, -v)) { if (b->isLessThan(dataBase, -v)) {
if (!errorMessage.empty()) if (!errorMessage.empty())

86
test/testexprengine.cpp
View File

@ -38,6 +38,7 @@ private:
TEST_CASE(expr3); TEST_CASE(expr3);
TEST_CASE(expr4); TEST_CASE(expr4);
TEST_CASE(expr5); TEST_CASE(expr5);
TEST_CASE(expr6);
TEST_CASE(exprAssign1); TEST_CASE(exprAssign1);
TEST_CASE(exprAssign2); // Truncation TEST_CASE(exprAssign2); // Truncation
@ -158,6 +159,21 @@ private:
ASSERT_EQUALS("($1)+($2)", getRange("void f(short a, short b, short c, short d) { if (a+b<c+d) {} }", "a+b")); ASSERT_EQUALS("($1)+($2)", getRange("void f(short a, short b, short c, short d) { if (a+b<c+d) {} }", "a+b"));
} }
void expr6() {
const char code[] = "void f(unsigned char x) {\n"
" unsigned char result = 8 - x;\n"
" result > 1000;"
"}";
ASSERT_EQUALS("(8)-($1)", getRange(code, "8-x"));
ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (and (>= $1 0) (<= $1 255)))\n"
"(assert (> (- 8 $1) 1000))\n"
"z3::unsat",
expr(code, ">"));
}
void exprAssign1() { void exprAssign1() {
ASSERT_EQUALS("($1)+(1)", getRange("void f(unsigned char a) { a += 1; }", "a+=1")); ASSERT_EQUALS("($1)+(1)", getRange("void f(unsigned char a) { a += 1; }", "a+=1"));
} }
@ -169,21 +185,20 @@ private:
void if1() { void if1() {
ASSERT_EQUALS("(declare-fun $1 () Int)\n" ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(declare-fun $2 () Int)\n" "(declare-fun $2 () Int)\n"
"(assert (<= $1 2147483647))\n" "(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (>= $1 (- 2147483648)))\n" "(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n"
"(assert (<= $2 2147483647))\n"
"(assert (>= $2 (- 2147483648)))\n"
"(assert (< $1 $2))\n" "(assert (< $1 $2))\n"
"(assert (= $1 $2))\n", "(assert (= $1 $2))\n"
"z3::unsat",
expr("void f(int x, int y) { if (x < y) return x == y; }", "==")); expr("void f(int x, int y) { if (x < y) return x == y; }", "=="));
} }
void ifelse1() { void ifelse1() {
ASSERT_EQUALS("(declare-fun $1 () Int)\n" ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (<= $1 32767))\n" "(assert (and (>= $1 (- 32768)) (<= $1 32767)))\n"
"(assert (>= $1 (- 32768)))\n"
"(assert (<= $1 5))\n" "(assert (<= $1 5))\n"
"(assert (= (+ $1 2) 40))\n", "(assert (= (+ $1 2) 40))\n"
"z3::unsat",
expr("void f(short x) { if (x > 5) ; else if (x+2==40); }", "==")); expr("void f(short x) { if (x > 5) ; else if (x+2==40); }", "=="));
} }
@ -197,10 +212,10 @@ private:
" x<=4;\n" " x<=4;\n"
"}"; "}";
ASSERT_EQUALS("(declare-fun $1 () Int)\n" ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (<= $1 2147483647))\n" "(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (>= $1 (- 2147483648)))\n"
"(assert (= $1 1))\n" "(assert (= $1 1))\n"
"(assert (= $1 3))\n", "(assert (= $1 3))\n"
"z3::unsat",
expr(code, "==")); expr(code, "=="));
} }
@ -209,12 +224,12 @@ private:
" int x = 0;\n" " int x = 0;\n"
" while (x < y)\n" " while (x < y)\n"
" x = x + 34;\n" " x = x + 34;\n"
" x == 1;\n" " x == 340;\n"
"}"; "}";
ASSERT_EQUALS("(declare-fun $2 () Int)\n" ASSERT_EQUALS("(declare-fun $2 () Int)\n"
"(assert (<= $2 2147483647))\n" "(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n"
"(assert (>= $2 (- 2147483648)))\n" "(assert (= (+ $2 34) 340))\n"
"(assert (= (+ $2 34) 1))\n", "z3::sat",
expr(code, "==")); expr(code, "=="));
} }
@ -226,23 +241,23 @@ private:
" x == 1;\n" " x == 1;\n"
"}"; "}";
ASSERT_EQUALS("(declare-fun $2 () Int)\n" ASSERT_EQUALS("(declare-fun $2 () Int)\n"
"(assert (<= $2 2147483647))\n" "(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n"
"(assert (>= $2 (- 2147483648)))\n" "(assert (= $2 1))\n"
"(assert (= $2 1))\n", "z3::sat",
expr(code, "==")); expr(code, "=="));
} }
void array1() { void array1() {
ASSERT_EQUALS("(assert (= 5 0))\n", ASSERT_EQUALS("(assert (= 5 0))\nz3::unsat",
expr("int f() { int arr[10]; arr[4] = 5; return arr[4]==0; }", "==")); expr("int f() { int arr[10]; arr[4] = 5; return arr[4]==0; }", "=="));
} }
void array2() { void array2() {
ASSERT_EQUALS("(declare-fun |$3:4| () Int)\n" ASSERT_EQUALS("(declare-fun |$3:4| () Int)\n"
"(assert (<= |$3:4| 255))\n" "(assert (and (>= |$3:4| 0) (<= |$3:4| 255)))\n"
"(assert (>= |$3:4| 0))\n" "(assert (= |$3:4| 365))\n"
"(assert (= |$3:4| 365))\n", "z3::unsat",
expr("void dostuff(unsigned char *); int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4] == 365; }", "==")); expr("void dostuff(unsigned char *); int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4] == 365; }", "=="));
} }
@ -250,9 +265,9 @@ private:
const char code[] = "void f(unsigned char x) { int arr[10]; arr[4] = 43; return arr[x] == 12; }"; const char code[] = "void f(unsigned char x) { int arr[10]; arr[4] = 43; return arr[x] == 12; }";
ASSERT_EQUALS("?,43", getRange(code, "arr[x]")); ASSERT_EQUALS("?,43", getRange(code, "arr[x]"));
ASSERT_EQUALS("(declare-fun $1 () Int)\n" ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (<= $1 255))\n" "(assert (and (>= $1 0) (<= $1 255)))\n"
"(assert (>= $1 0))\n" "(assert (= (ite (= $1 4) 43 0) 12))\n"
"(assert (= (ite (= $1 4) 43 0) 12))\n", "z3::unsat",
expr(code, "==")); expr(code, "=="));
} }
@ -309,9 +324,9 @@ private:
void int1() { void int1() {
ASSERT_EQUALS("(declare-fun $1 () Int)\n" ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (<= $1 2147483647))\n" "(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (>= $1 (- 2147483648)))\n" "(assert (= (+ 2 $1) 3))\n"
"(assert (= (+ 2 $1) 3))\n", "z3::sat",
expr("void f(int x) { return 2+x==3; }", "==")); expr("void f(int x) { return 2+x==3; }", "=="));
} }
@ -320,9 +335,9 @@ private:
const char code[] = "void f(unsigned char *p) { return *p == 7; }"; const char code[] = "void f(unsigned char *p) { return *p == 7; }";
ASSERT_EQUALS("->$1,null,->?", getRange(code, "p")); ASSERT_EQUALS("->$1,null,->?", getRange(code, "p"));
ASSERT_EQUALS("(declare-fun $1 () Int)\n" ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (<= $1 255))\n" "(assert (and (>= $1 0) (<= $1 255)))\n"
"(assert (>= $1 0))\n" "(assert (= $1 7))\n"
"(assert (= $1 7))\n", "z3::sat",
expr(code, "==")); expr(code, "=="));
} }
@ -355,11 +370,10 @@ private:
void structMember() { void structMember() {
ASSERT_EQUALS("(declare-fun $2 () Int)\n" ASSERT_EQUALS("(declare-fun $2 () Int)\n"
"(declare-fun $3 () Int)\n" "(declare-fun $3 () Int)\n"
"(assert (<= $2 255))\n" "(assert (and (>= $2 0) (<= $2 255)))\n"
"(assert (>= $2 0))\n" "(assert (and (>= $3 0) (<= $3 255)))\n"
"(assert (<= $3 255))\n" "(assert (= (+ $2 $3) 0))\n"
"(assert (>= $3 0))\n" "z3::sat",
"(assert (= (+ $2 $3) 0))\n",
expr("struct S {\n" expr("struct S {\n"
" unsigned char a;\n" " unsigned char a;\n"
" unsigned char b;\n" " unsigned char b;\n"