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

ExprEngine: Fix ExprEngin::IntRange::isIntValueInRange

This commit is contained in:
Daniel Marjamäki 2019-10-05 16:33:40 +02:00
parent 954e98cc03
commit e686699294
3 changed files with 71 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

43
lib/exprengine.cpp
View File

@ -486,10 +486,10 @@ std::string ExprEngine::IntegerTruncation::getSymbolicExpression() const
#ifdef USE_Z3
struct ExprData {
typedef std::map<ExprEngine::ValuePtr, z3::expr> ValueExpr;
typedef std::map<std::string, z3::expr> ValueExpr;
typedef std::vector<z3::expr> AssertionList;
z3::context c;
z3::context context;
ValueExpr valueExpr;
AssertionList assertionList;
@ -539,12 +539,12 @@ static z3::expr getExpr(ExprEngine::ValuePtr v, ExprData &exprData)
{
if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) {
if (intRange->name[0] != '$')
return exprData.c.int_val(int64_t(intRange->minValue));
auto it = exprData.valueExpr.find(v);
return exprData.context.int_val(int64_t(intRange->minValue));
auto it = exprData.valueExpr.find(v->name);
if (it != exprData.valueExpr.end())
return it->second;
auto e = exprData.c.int_const(("v" + std::to_string(exprData.valueExpr.size())).c_str());
exprData.valueExpr.emplace(v, e);
auto e = exprData.context.int_const(v->name.c_str());
exprData.valueExpr.emplace(v->name, e);
if (intRange->maxValue <= INT_MAX)
exprData.assertionList.push_back(e <= int(intRange->maxValue));
if (intRange->minValue >= INT_MIN)
@ -566,16 +566,41 @@ static z3::expr getExpr(ExprEngine::ValuePtr v, ExprData &exprData)
}
if (v->type == ExprEngine::ValueType::UninitValue)
return exprData.c.int_val(0);
return exprData.context.int_val(0);
throw std::runtime_error("Internal error: Unhandled value type");
}
#endif
bool ExprEngine::IntRange::isIntValueInRange(DataBase *dataBase, int value) const
{
if (value < minValue || value > maxValue)
return false;
const Data *data = dynamic_cast<Data *>(dataBase);
if (data->constraints.empty())
return true;
#ifdef USE_Z3
// Check the value against the constraints
ExprData exprData;
z3::solver solver(exprData.context);
z3::expr e = exprData.context.int_const(name.c_str());
exprData.valueExpr.emplace(name, e);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(::getExpr(constraint, exprData));
solver.add(e == value);
return solver.check() == z3::sat;
#else
// The value may or may not be in range
return false;
#endif
}
bool ExprEngine::BinOpResult::isIntValueInRange(ExprEngine::DataBase *dataBase, int value) const
{
#ifdef USE_Z3
ExprData exprData;
z3::solver solver(exprData.c);
z3::solver solver(exprData.context);
z3::expr e = ::getExpr(this, exprData);
exprData.addAssertions(solver);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
@ -593,7 +618,7 @@ std::string ExprEngine::BinOpResult::getExpr(ExprEngine::DataBase *dataBase) con
{
#ifdef USE_Z3
ExprData exprData;
z3::solver solver(exprData.c);
z3::solver solver(exprData.context);
z3::expr e = ::getExpr(this, exprData);
exprData.addAssertions(solver);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)

5
lib/exprengine.h
View File

@ -113,10 +113,7 @@ namespace ExprEngine {
return str(minValue);
return str(minValue) + ":" + str(maxValue);
}
bool isIntValueInRange(DataBase *dataBase, int value) const override {
(void)dataBase;
return value >= minValue && value <= maxValue;
}
bool isIntValueInRange(DataBase *dataBase, int value) const override;
int128_t minValue;
int128_t maxValue;

72
test/testexprengine.cpp
View File

@ -160,23 +160,23 @@ private:
}
void if1() {
ASSERT_EQUALS("(declare-fun v0 () Int)\n"
"(declare-fun v1 () Int)\n"
"(assert (<= v0 2147483647))\n"
"(assert (>= v0 (- 2147483648)))\n"
"(assert (<= v1 2147483647))\n"
"(assert (>= v1 (- 2147483648)))\n"
"(assert (< v0 v1))\n"
"(assert (= v0 v1))\n",
ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(declare-fun $2 () Int)\n"
"(assert (<= $1 2147483647))\n"
"(assert (>= $1 (- 2147483648)))\n"
"(assert (<= $2 2147483647))\n"
"(assert (>= $2 (- 2147483648)))\n"
"(assert (< $1 $2))\n"
"(assert (= $1 $2))\n",
expr("void f(int x, int y) { if (x < y) return x == y; }", "=="));
}
void ifelse1() {
ASSERT_EQUALS("(declare-fun v0 () Int)\n"
"(assert (<= v0 32767))\n"
"(assert (>= v0 (- 32768)))\n"
"(assert (<= v0 5))\n"
"(assert (= (+ v0 2) 40))\n",
ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (<= $1 32767))\n"
"(assert (>= $1 (- 32768)))\n"
"(assert (<= $1 5))\n"
"(assert (= (+ $1 2) 40))\n",
expr("void f(short x) { if (x > 5) ; else if (x+2==40); }", "=="));
}
@ -187,20 +187,20 @@ private:
}
void array2() {
ASSERT_EQUALS("(declare-fun v0 () Int)\n"
"(assert (<= v0 255))\n"
"(assert (>= v0 0))\n"
"(assert (= v0 365))\n",
ASSERT_EQUALS("(declare-fun |$3:4| () Int)\n"
"(assert (<= |$3:4| 255))\n"
"(assert (>= |$3:4| 0))\n"
"(assert (= |$3:4| 365))\n",
expr("void dostuff(unsigned char *); int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4] == 365; }", "=="));
}
void array3() {
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("(declare-fun v0 () Int)\n"
"(assert (<= v0 255))\n"
"(assert (>= v0 0))\n"
"(assert (= (ite (= v0 4) 43 0) 12))\n",
ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (<= $1 255))\n"
"(assert (>= $1 0))\n"
"(assert (= (ite (= $1 4) 43 0) 12))\n",
expr(code, "=="));
}
@ -256,10 +256,10 @@ private:
void int1() {
ASSERT_EQUALS("(declare-fun v0 () Int)\n"
"(assert (<= v0 2147483647))\n"
"(assert (>= v0 (- 2147483648)))\n"
"(assert (= (+ 2 v0) 3))\n",
ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (<= $1 2147483647))\n"
"(assert (>= $1 (- 2147483648)))\n"
"(assert (= (+ 2 $1) 3))\n",
expr("void f(int x) { return 2+x==3; }", "=="));
}
@ -267,10 +267,10 @@ private:
void pointer1() {
const char code[] = "void f(unsigned char *p) { return *p == 7; }";
ASSERT_EQUALS("->$1,null,->?", getRange(code, "p"));
ASSERT_EQUALS("(declare-fun v0 () Int)\n"
"(assert (<= v0 255))\n"
"(assert (>= v0 0))\n"
"(assert (= v0 7))\n",
ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (<= $1 255))\n"
"(assert (>= $1 0))\n"
"(assert (= $1 7))\n",
expr(code, "=="));
}
@ -301,13 +301,13 @@ private:
void structMember() {
ASSERT_EQUALS("(declare-fun v0 () Int)\n"
"(declare-fun v1 () Int)\n"
"(assert (<= v0 255))\n"
"(assert (>= v0 0))\n"
"(assert (<= v1 255))\n"
"(assert (>= v1 0))\n"
"(assert (= (+ v0 v1) 0))\n",
ASSERT_EQUALS("(declare-fun $2 () Int)\n"
"(declare-fun $3 () Int)\n"
"(assert (<= $2 255))\n"
"(assert (>= $2 0))\n"
"(assert (<= $3 255))\n"
"(assert (>= $3 0))\n"
"(assert (= (+ $2 $3) 0))\n",
expr("struct S {\n"
" unsigned char a;\n"
" unsigned char b;\n"