From 273a1a7402c2eae360f12e990750cc5809cf4ba8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Wed, 9 Oct 2019 11:24:57 +0200 Subject: [PATCH] ExprEngine: Fix FP for 'int' overflows --- lib/exprengine.cpp | 19 +++++++-- test/testexprengine.cpp | 86 ++++++++++++++++++++++++----------------- 2 files changed, 66 insertions(+), 39 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 472baa4b3..a0d8a8bef 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -564,9 +564,11 @@ struct ExprData { return it->second; auto e = context.int_const(v->name.c_str()); valueExpr.emplace(v->name, e); - if (intRange->maxValue <= INT_MAX) + 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)); - if (intRange->minValue >= INT_MIN) + else if (intRange->minValue >= INT_MIN) assertionList.push_back(e >= int(intRange->minValue)); return e; } @@ -708,6 +710,17 @@ std::string ExprEngine::BinOpResult::getExpr(ExprEngine::DataBase *dataBase) con 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(); #else (void)dataBase; @@ -1369,7 +1382,7 @@ void ExprEngine::runChecks(ErrorLogger *errorLogger, const Tokenizer *tokenizer, std::string errorMessage; if (tok->valueType()->sign == ::ValueType::Sign::SIGNED) { MathLib::bigint v = 1LL << (bits - 1); - if (b->isGreaterThan(dataBase, v)) + if (b->isGreaterThan(dataBase, v-1)) errorMessage = "greater than " + std::to_string(v); if (b->isLessThan(dataBase, -v)) { if (!errorMessage.empty()) diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 9506176b3..f0a74e725 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -38,6 +38,7 @@ private: TEST_CASE(expr3); TEST_CASE(expr4); TEST_CASE(expr5); + TEST_CASE(expr6); TEST_CASE(exprAssign1); TEST_CASE(exprAssign2); // Truncation @@ -158,6 +159,21 @@ private: ASSERT_EQUALS("($1)+($2)", getRange("void f(short a, short b, short c, short d) { if (a+b 1000;" + "}"; + + ASSERT_EQUALS("(8)-($1)", getRange(code, "8-x")); + + ASSERT_EQUALS("(declare-fun $1 () Int)\n" + "(assert (and (>= $1 0) (<= $1 255)))\n" + "(assert (> (- 8 $1) 1000))\n" + "z3::unsat", + expr(code, ">")); + } + void exprAssign1() { ASSERT_EQUALS("($1)+(1)", getRange("void f(unsigned char a) { a += 1; }", "a+=1")); } @@ -169,21 +185,20 @@ private: void if1() { 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 (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n" + "(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n" "(assert (< $1 $2))\n" - "(assert (= $1 $2))\n", + "(assert (= $1 $2))\n" + "z3::unsat", expr("void f(int x, int y) { if (x < y) return x == y; }", "==")); } void ifelse1() { ASSERT_EQUALS("(declare-fun $1 () Int)\n" - "(assert (<= $1 32767))\n" - "(assert (>= $1 (- 32768)))\n" + "(assert (and (>= $1 (- 32768)) (<= $1 32767)))\n" "(assert (<= $1 5))\n" - "(assert (= (+ $1 2) 40))\n", + "(assert (= (+ $1 2) 40))\n" + "z3::unsat", expr("void f(short x) { if (x > 5) ; else if (x+2==40); }", "==")); } @@ -197,10 +212,10 @@ private: " x<=4;\n" "}"; ASSERT_EQUALS("(declare-fun $1 () Int)\n" - "(assert (<= $1 2147483647))\n" - "(assert (>= $1 (- 2147483648)))\n" + "(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n" "(assert (= $1 1))\n" - "(assert (= $1 3))\n", + "(assert (= $1 3))\n" + "z3::unsat", expr(code, "==")); } @@ -209,12 +224,12 @@ private: " int x = 0;\n" " while (x < y)\n" " x = x + 34;\n" - " x == 1;\n" + " x == 340;\n" "}"; ASSERT_EQUALS("(declare-fun $2 () Int)\n" - "(assert (<= $2 2147483647))\n" - "(assert (>= $2 (- 2147483648)))\n" - "(assert (= (+ $2 34) 1))\n", + "(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n" + "(assert (= (+ $2 34) 340))\n" + "z3::sat", expr(code, "==")); } @@ -226,23 +241,23 @@ private: " x == 1;\n" "}"; ASSERT_EQUALS("(declare-fun $2 () Int)\n" - "(assert (<= $2 2147483647))\n" - "(assert (>= $2 (- 2147483648)))\n" - "(assert (= $2 1))\n", + "(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n" + "(assert (= $2 1))\n" + "z3::sat", expr(code, "==")); } void array1() { - ASSERT_EQUALS("(assert (= 5 0))\n", + ASSERT_EQUALS("(assert (= 5 0))\nz3::unsat", expr("int f() { int arr[10]; arr[4] = 5; return arr[4]==0; }", "==")); } void array2() { ASSERT_EQUALS("(declare-fun |$3:4| () Int)\n" - "(assert (<= |$3:4| 255))\n" - "(assert (>= |$3:4| 0))\n" - "(assert (= |$3:4| 365))\n", + "(assert (and (>= |$3:4| 0) (<= |$3:4| 255)))\n" + "(assert (= |$3:4| 365))\n" + "z3::unsat", expr("void dostuff(unsigned char *); int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4] == 365; }", "==")); } @@ -250,9 +265,9 @@ private: 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 $1 () Int)\n" - "(assert (<= $1 255))\n" - "(assert (>= $1 0))\n" - "(assert (= (ite (= $1 4) 43 0) 12))\n", + "(assert (and (>= $1 0) (<= $1 255)))\n" + "(assert (= (ite (= $1 4) 43 0) 12))\n" + "z3::unsat", expr(code, "==")); } @@ -309,9 +324,9 @@ private: void int1() { ASSERT_EQUALS("(declare-fun $1 () Int)\n" - "(assert (<= $1 2147483647))\n" - "(assert (>= $1 (- 2147483648)))\n" - "(assert (= (+ 2 $1) 3))\n", + "(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n" + "(assert (= (+ 2 $1) 3))\n" + "z3::sat", expr("void f(int x) { return 2+x==3; }", "==")); } @@ -320,9 +335,9 @@ private: const char code[] = "void f(unsigned char *p) { return *p == 7; }"; ASSERT_EQUALS("->$1,null,->?", getRange(code, "p")); ASSERT_EQUALS("(declare-fun $1 () Int)\n" - "(assert (<= $1 255))\n" - "(assert (>= $1 0))\n" - "(assert (= $1 7))\n", + "(assert (and (>= $1 0) (<= $1 255)))\n" + "(assert (= $1 7))\n" + "z3::sat", expr(code, "==")); } @@ -355,11 +370,10 @@ private: void structMember() { 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", + "(assert (and (>= $2 0) (<= $2 255)))\n" + "(assert (and (>= $3 0) (<= $3 255)))\n" + "(assert (= (+ $2 $3) 0))\n" + "z3::sat", expr("struct S {\n" " unsigned char a;\n" " unsigned char b;\n"