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

ExprEngine: Adapt to z3 handling of bool/int expressions

This commit is contained in:
Daniel Marjamäki 2019-10-09 20:17:26 +02:00
parent 4d305d5c54
commit 63bd182e83
2 changed files with 68 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

67
lib/exprengine.cpp
View File

@ -533,7 +533,7 @@ struct ExprData {
if (b->binop == "%")
return op1 % op2;
if (b->binop == "==")
return op1 == op2;
return int_expr(op1) == int_expr(op2);
if (b->binop == "!=")
return op1 != op2;
if (b->binop == ">=")
@ -545,9 +545,9 @@ struct ExprData {
if (b->binop == "<")
return op1 < op2;
if (b->binop == "&&")
return op1 && op2;
return bool_expr(op1) && bool_expr(op2);
if (b->binop == "||")
return op1 || op2;
return bool_expr(op1) || bool_expr(op2);
if (b->binop == "<<")
return z3::shl(op1, op2);
if (b->binop == ">>")
@ -602,6 +602,21 @@ struct ExprData {
return (getExpr(v) != 0);
return getExpr(v);
}
private:
z3::expr bool_expr(z3::expr e) {
if (e.is_bool())
return e;
return e != 0;
}
z3::expr int_expr(z3::expr e) {
if (e.is_bool())
return z3::ite(e, context.int_val(1), context.int_val(0));
return e;
}
};
#endif
@ -701,27 +716,33 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val
std::string ExprEngine::BinOpResult::getExpr(ExprEngine::DataBase *dataBase) const
{
#ifdef USE_Z3
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));
solver.add(e);
std::ostringstream os;
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;
try {
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));
solver.add(e);
std::ostringstream os;
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();
} catch (const z3::exception &exception) {
std::ostringstream os;
os << "z3:" << exception;
return os.str();
}
return os.str();
#else
(void)dataBase;
return "";

24
test/testexprengine.cpp
View File

@ -39,6 +39,7 @@ private:
TEST_CASE(expr4);
TEST_CASE(expr5);
TEST_CASE(expr6);
TEST_CASE(expr7);
TEST_CASE(exprAssign1);
TEST_CASE(exprAssign2); // Truncation
@ -174,6 +175,29 @@ private:
expr(code, ">"));
}
void expr7() {
const char code[] = "void f(bool a, bool b, int c) {\n"
" if (a||b) {}\n"
" c > 1000;"
"}";
ASSERT_EQUALS("(declare-fun $3 () Int)\n"
"(declare-fun $2 () Int)\n"
"(declare-fun $1 () Int)\n"
"(assert (and (>= $3 (- 2147483648)) (<= $3 2147483647)))\n"
"(assert (or (distinct $1 0) (distinct $2 0)))\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"
"(assert (= (ite (or (distinct $1 0) (distinct $2 0)) 1 0) 0))\n"
"(assert (> $3 1000))\n"
"z3::sat",
expr(code, ">"));
}
void exprAssign1() {
ASSERT_EQUALS("($1)+(1)", getRange("void f(unsigned char a) { a += 1; }", "a+=1"));
}