From 6ea1875a84636dcc4a1edadb5c532bb9ed17fe4a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Mon, 30 Dec 2019 12:53:59 +0100 Subject: [PATCH] Verification; Ensure assertions for variable type limits are added --- lib/exprengine.cpp | 36 ++++++++++++++++++-------------- test/testexprengine.cpp | 46 +++++++++++++++++++++++++++++------------ 2 files changed, 54 insertions(+), 28 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 72653049f..4a9c3a36e 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -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(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(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(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(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(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(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(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(dataBase)->constraints) solver.add(exprData.getConstraintExpr(constraint)); + exprData.addAssertions(solver); solver.add(e); std::ostringstream os; os << solver; diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 0b7e1b944..9c92781f6 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -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, "=="));