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

Verification; Ensure assertions for variable type limits are added

This commit is contained in:
Daniel Marjamäki 2019-12-30 12:53:59 +01:00
parent 39a6eefef5
commit 6ea1875a84
2 changed files with 54 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
lib/exprengine.cpp
View File

@ -573,6 +573,18 @@ struct ExprData {
solver.add(assertExpr);
}
z3::expr addInt(const std::string &name, int128_t minValue, int128_t maxValue) {
z3::expr e = context.int_const(name.c_str());
valueExpr.emplace(name, e);
if (minValue >= INT_MIN && maxValue <= INT_MAX)
assertionList.push_back(e >= int(minValue) && e <= int(maxValue));
else if (maxValue <= INT_MAX)
assertionList.push_back(e <= int(maxValue));
else if (minValue >= INT_MIN)
assertionList.push_back(e >= int(minValue));
return e;
}
z3::expr getExpr(const ExprEngine::BinOpResult *b) {
auto op1 = getExpr(b->op1);
auto op2 = getExpr(b->op2);
@ -619,15 +631,7 @@ struct ExprData {
auto it = valueExpr.find(v->name);
if (it != valueExpr.end())
return it->second;
auto e = context.int_const(v->name.c_str());
valueExpr.emplace(v->name, e);
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));
else if (intRange->minValue >= INT_MIN)
assertionList.push_back(e >= int(intRange->minValue));
return e;
return addInt(v->name, intRange->minValue, intRange->maxValue);
}
if (auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(v)) {
@ -692,10 +696,10 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const
ExprData exprData;
z3::solver solver(exprData.context);
try {
z3::expr e = exprData.context.int_const(name.c_str());
exprData.valueExpr.emplace(name, e);
z3::expr e = exprData.addInt(name, minValue, maxValue);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
solver.add(e == value);
return solver.check() == z3::sat;
} catch (const z3::exception &exception) {
@ -725,6 +729,7 @@ bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const
exprData.valueExpr.emplace(name, e);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
solver.add(e > value);
return solver.check() == z3::sat;
} catch (const z3::exception &exception) {
@ -754,6 +759,7 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const
exprData.valueExpr.emplace(name, e);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
solver.add(e < value);
return solver.check() == z3::sat;
} catch (const z3::exception &exception) {
@ -772,9 +778,9 @@ bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value)
ExprData exprData;
z3::solver solver(exprData.context);
z3::expr e = exprData.getExpr(this);
exprData.addAssertions(solver);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
solver.add(e == value);
return solver.check() == z3::sat;
#else
@ -791,9 +797,9 @@ bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int
ExprData exprData;
z3::solver solver(exprData.context);
z3::expr e = exprData.getExpr(this);
exprData.addAssertions(solver);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
solver.add(e > value);
return solver.check() == z3::sat;
} catch (const z3::exception &exception) {
@ -814,9 +820,9 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val
ExprData exprData;
z3::solver solver(exprData.context);
z3::expr e = exprData.getExpr(this);
exprData.addAssertions(solver);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
solver.add(e < value);
return solver.check() == z3::sat;
} catch (const z3::exception &exception) {
@ -837,9 +843,9 @@ std::string ExprEngine::BinOpResult::getExpr(ExprEngine::DataBase *dataBase) con
ExprData exprData;
z3::solver solver(exprData.context);
z3::expr e = exprData.getExpr(this);
exprData.addAssertions(solver);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
solver.add(e);
std::ostringstream os;
os << solver;

46
test/testexprengine.cpp
View File

@ -48,6 +48,7 @@ private:
TEST_CASE(if1);
TEST_CASE(if2);
TEST_CASE(if3);
TEST_CASE(if4);
TEST_CASE(ifelse1);
TEST_CASE(switch1);
@ -153,8 +154,8 @@ private:
"}";
const char expected[] = "(declare-fun $1 () Int)\n"
"(assert (and (>= $1 (- 32768)) (<= $1 32767)))\n"
"(assert (>= $1 100))\n" // <- annotation
"(assert (and (>= $1 (- 32768)) (<= $1 32767)))\n"
"(assert (< $1 10))\n"
"z3::unsat";
@ -202,18 +203,22 @@ private:
" c > 1000;"
"}";
ASSERT_EQUALS("(declare-fun $3 () Int)\n"
"(declare-fun $2 () Int)\n"
ASSERT_EQUALS("(declare-fun $2 () Int)\n"
"(declare-fun $1 () Int)\n"
"(assert (and (>= $3 (- 2147483648)) (<= $3 2147483647)))\n"
"(declare-fun $3 () Int)\n"
"(assert (or (distinct $1 0) (distinct $2 0)))\n"
"(assert (and (>= $3 (- 2147483648)) (<= $3 2147483647)))\n"
"(assert (and (>= $1 0) (<= $1 1)))\n"
"(assert (and (>= $2 0) (<= $2 1)))\n"
"(assert (> $3 1000))\n"
"z3::sat\n"
"(declare-fun $3 () Int)\n"
"(declare-fun $2 () Int)\n"
"(declare-fun $1 () Int)\n"
"(assert (and (>= $3 (- 2147483648)) (<= $3 2147483647)))\n"
"(declare-fun $3 () Int)\n"
"(assert (= (ite (or (distinct $1 0) (distinct $2 0)) 1 0) 0))\n"
"(assert (and (>= $3 (- 2147483648)) (<= $3 2147483647)))\n"
"(assert (and (>= $1 0) (<= $1 1)))\n"
"(assert (and (>= $2 0) (<= $2 1)))\n"
"(assert (> $3 1000))\n"
"z3::sat",
expr(code, ">"));
@ -228,11 +233,11 @@ private:
}
void if1() {
ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(declare-fun $2 () Int)\n"
ASSERT_EQUALS("(declare-fun $2 () Int)\n"
"(declare-fun $1 () Int)\n"
"(assert (< $1 $2))\n"
"(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n"
"(assert (< $1 $2))\n"
"(assert (= $1 $2))\n"
"z3::unsat",
expr("void f(int x, int y) { if (x < y) return x == y; }", "=="));
@ -244,8 +249,8 @@ private:
"}";
// In expression "x + x < 20", "x" is greater than 0
const char expected[] = "(declare-fun $1 () Int)\n"
"(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (> $1 0))\n"
"(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (= $1 20))\n"
"z3::sat";
ASSERT_EQUALS(expected, expr(code, "=="));
@ -257,17 +262,32 @@ private:
"}";
// In expression "x + x < 20", "x" is greater than 0
const char expected[] = "(declare-fun $1 () Int)\n"
"(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (<= $1 0))\n"
"(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (= $1 20))\n"
"z3::unsat"; // "x == 20" is unsat
ASSERT_EQUALS(expected, expr(code, "=="));
}
void if4() {
const char code[] = "void foo(unsigned int x, unsigned int y) {\n"
" unsigned int z = y;"
" if (x < z) { return z == 0; }\n"
"}";
const char expected[] = "(declare-fun $2 () Int)\n"
"(declare-fun $1 () Int)\n"
"(assert (< $1 $2))\n"
"(assert (>= $2 0))\n"
"(assert (>= $1 0))\n"
"(assert (= $2 0))\n"
"z3::unsat";
ASSERT_EQUALS(expected, expr(code, "=="));
}
void ifelse1() {
ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (and (>= $1 (- 32768)) (<= $1 32767)))\n"
"(assert (<= $1 5))\n"
"(assert (and (>= $1 (- 32768)) (<= $1 32767)))\n"
"(assert (= (+ $1 2) 40))\n"
"z3::unsat",
expr("void f(short x) { if (x > 5) ; else if (x+2==40); }", "=="));
@ -283,8 +303,8 @@ private:
" x<=4;\n"
"}";
ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (= $1 1))\n"
"(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (= $1 3))\n"
"z3::unsat",
expr(code, "=="));