From e686699294f7ec66f229cd77ce6de6282adb45be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Sat, 5 Oct 2019 16:33:40 +0200 Subject: [PATCH] ExprEngine: Fix ExprEngin::IntRange::isIntValueInRange --- lib/exprengine.cpp | 43 ++++++++++++++++++------ lib/exprengine.h | 5 +-- test/testexprengine.cpp | 72 ++++++++++++++++++++--------------------- 3 files changed, 71 insertions(+), 49 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index fbb280fef..015aedbec 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -486,10 +486,10 @@ std::string ExprEngine::IntegerTruncation::getSymbolicExpression() const #ifdef USE_Z3 struct ExprData { - typedef std::map ValueExpr; + typedef std::map ValueExpr; typedef std::vector 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(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(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(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(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(dataBase)->constraints) diff --git a/lib/exprengine.h b/lib/exprengine.h index d238cd631..1f4d9458e 100644 --- a/lib/exprengine.h +++ b/lib/exprengine.h @@ -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; diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index a773d6eb3..6063862a6 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -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"