From 9dad39a1a1f82c6eb8a2b4eba8b1149db403f807 Mon Sep 17 00:00:00 2001 From: Georgy Komarov Date: Mon, 14 Dec 2020 20:13:06 +0300 Subject: [PATCH 1/3] ExprEngine: Remove redundant bailout value from pointer assignment The following source code: ``` void foo(int *a) { while (1) *a = 42; *a == 42; } ``` Before this commit generates a redundant "bailout" value on the assigment: 15:12: 0:memory:{a=($2,[$1],[:]=?,[0]=bailout,[0]=42)} After this commit: 15:12: 0:memory:{a=($2,[$1],[:]=?,[0]=42)} The added tests are redundant and can't detect this error, but they increase the number of similar cases to handle possible regressions in the future. --- lib/exprengine.cpp | 24 ++++++++++++++++++------ test/testexprengine.cpp | 16 ++++++++++++++++ 2 files changed, 34 insertions(+), 6 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index f688407a46b..45cf7e23745 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -138,6 +138,7 @@ #include "symboldatabase.h" #include "tokenize.h" +#include #include #include #include @@ -2646,19 +2647,30 @@ static std::string execute(const Token *start, const Token *end, Data &data) data.assignStructMember(tok2, &*structVal, memberName, memberValue); continue; } + + // Assign a pointer value if (lhs->isUnaryOp("*") && lhs->astOperand1()->varId()) { const Token *varToken = tok2->astOperand1()->astOperand1(); ExprEngine::ValuePtr val = data.getValue(varToken->varId(), varToken->valueType(), varToken); - if (val && val->type == ExprEngine::ValueType::ArrayValue) { - // Try to assign "any" value - auto arrayValue = std::dynamic_pointer_cast(val); - arrayValue->assign(std::make_shared("0", 0, 0), std::make_shared()); + if (!val || val->type != ExprEngine::ValueType::ArrayValue) + throw ExprEngineException(tok2, "Unhandled assignment in loop"); + auto arrayValue = std::dynamic_pointer_cast(val); + assert(arrayValue); + int varid = varToken->varId(); + if (changedVariables.find(varid) != changedVariables.end()) continue; - } + changedVariables.insert(varid); + auto oldValue = data.getValue(varid, nullptr, nullptr); + if (oldValue && oldValue->isUninit()) + call(data.callbacks, varToken, oldValue, &data); + data.assignValue(tok2, varid, val); + continue; } + if (!lhs->variable()) throw ExprEngineException(tok2, "Unhandled assignment in loop"); - // give variable "any" value + + // Give variable "any" value int varid = lhs->varId(); if (changedVariables.find(varid) != changedVariables.end()) continue; diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 774df1d0cf6..2d17b6b2169 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -50,6 +50,7 @@ class TestExprEngine : public TestFixture { TEST_CASE(expr9); TEST_CASE(exprAssign1); TEST_CASE(exprAssign2); // Truncation + TEST_CASE(exprAssign3); TEST_CASE(exprNot); TEST_CASE(getValueConst1); @@ -78,6 +79,7 @@ class TestExprEngine : public TestFixture { TEST_CASE(while3); TEST_CASE(while4); TEST_CASE(while5); + TEST_CASE(while6); TEST_CASE(array1); TEST_CASE(array2); @@ -358,6 +360,10 @@ class TestExprEngine : public TestFixture { ASSERT_EQUALS("2", getRange("void f(unsigned char x) { x = 258; int a = x }", "a=x")); } + void exprAssign3() { + ASSERT_EQUALS("1", getRange("void f(unsigned char *a) { *a = 1 }", "*a=1")); + } + void exprNot() { ASSERT_EQUALS("($1)==(0)", getRange("void f(unsigned char a) { return !a; }", "!a")); } @@ -607,6 +613,16 @@ class TestExprEngine : public TestFixture { ASSERT(getRange(code, "x", 4).find("?") != std::string::npos); } + void while6() { + const char code[] = "void f(int *arr) {\n" + " while (cond)\n" + " *arr = 4;\n" + " arr[0] == 4;" + "}"; + ASSERT_EQUALS("(= 4 4)\n" + "z3::sat\n", expr(code, "==")); + } + void array1() { ASSERT_EQUALS("(= 5 0)\nz3::unsat\n", From 040837b7117afcd4e3111da3fe9f7bbb7578cd6e Mon Sep 17 00:00:00 2001 From: Georgy Komarov Date: Tue, 15 Dec 2020 06:54:10 +0300 Subject: [PATCH 2/3] testexprengine: Fix code --- test/testexprengine.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 2d17b6b2169..5e335401810 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -357,11 +357,11 @@ class TestExprEngine : public TestFixture { } void exprAssign2() { - ASSERT_EQUALS("2", getRange("void f(unsigned char x) { x = 258; int a = x }", "a=x")); + ASSERT_EQUALS("2", getRange("void f(unsigned char x) { x = 258; int a = x; }", "a=x")); } void exprAssign3() { - ASSERT_EQUALS("1", getRange("void f(unsigned char *a) { *a = 1 }", "*a=1")); + ASSERT_EQUALS("1", getRange("void f(unsigned char *a) { *a = 1; }", "*a=1")); } void exprNot() { From c39a860ce4a6024c13d0fadfdfc233929b1c6c03 Mon Sep 17 00:00:00 2001 From: Georgy Komarov Date: Tue, 15 Dec 2020 07:43:01 +0300 Subject: [PATCH 3/3] ExprEngine: Handle pointers to a known variable --- lib/exprengine.cpp | 19 +++++++++++++++---- test/testexprengine.cpp | 12 ++++++++++++ 2 files changed, 27 insertions(+), 4 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 45cf7e23745..3f225ffa7ba 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -2651,11 +2651,12 @@ static std::string execute(const Token *start, const Token *end, Data &data) // Assign a pointer value if (lhs->isUnaryOp("*") && lhs->astOperand1()->varId()) { const Token *varToken = tok2->astOperand1()->astOperand1(); + // Get value of the pointer ExprEngine::ValuePtr val = data.getValue(varToken->varId(), varToken->valueType(), varToken); - if (!val || val->type != ExprEngine::ValueType::ArrayValue) + if (!val || (val->type != ExprEngine::ValueType::ArrayValue && + val->type != ExprEngine::ValueType::AddressOfValue)) throw ExprEngineException(tok2, "Unhandled assignment in loop"); - auto arrayValue = std::dynamic_pointer_cast(val); - assert(arrayValue); + // Handle the value that we are pointing to int varid = varToken->varId(); if (changedVariables.find(varid) != changedVariables.end()) continue; @@ -2663,7 +2664,17 @@ static std::string execute(const Token *start, const Token *end, Data &data) auto oldValue = data.getValue(varid, nullptr, nullptr); if (oldValue && oldValue->isUninit()) call(data.callbacks, varToken, oldValue, &data); - data.assignValue(tok2, varid, val); + if (val->type == ExprEngine::ValueType::ArrayValue) { + // Unknown pointer, array or struct + auto arrayValue = std::dynamic_pointer_cast(val); + assert(arrayValue); + data.assignValue(tok2, varid, val); + } else if (val->type == ExprEngine::ValueType::AddressOfValue) { + // Address of a known variable + auto addressOf = std::dynamic_pointer_cast(val); + assert(addressOf); + data.assignValue(tok2, varid, val); + } continue; } diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 5e335401810..cd3ae9b57cb 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -80,6 +80,7 @@ class TestExprEngine : public TestFixture { TEST_CASE(while4); TEST_CASE(while5); TEST_CASE(while6); + TEST_CASE(while7); TEST_CASE(array1); TEST_CASE(array2); @@ -623,6 +624,17 @@ class TestExprEngine : public TestFixture { "z3::sat\n", expr(code, "==")); } + void while7() { + const char code[] = "void foo() {\n" + " int a = 2;\n" + " int *p = &a;\n" + " while (1) *p = 0;\n" + " return a == 2;\n" + "}"; + ASSERT_EQUALS("(= 0 2)\n" + "z3::unsat\n", expr(code, "==")); + } + void array1() { ASSERT_EQUALS("(= 5 0)\nz3::unsat\n",