Skip to content

ExprEngine: Handle pointer assignments in loops without bailout #2949

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
jubnzv wants to merge 3 commits into from
Closed

ExprEngine: Handle pointer assignments in loops without bailout #2949

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9dad39a
ExprEngine: Remove redundant bailout value from pointer assignment
jubnzv Dec 14, 2020
040837b
testexprengine: Fix code
jubnzv Dec 15, 2020
c39a860
ExprEngine: Handle pointers to a known variable
jubnzv Dec 15, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 28 additions & 5 deletions lib/exprengine.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,7 @@
#include "symboldatabase.h"
#include "tokenize.h"

#include <cassert>
#include <limits>
#include <memory>
#include <iostream>
Expand Down Expand Up @@ -2646,19 +2647,41 @@ 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();
// Get value of the pointer
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<ExprEngine::ArrayValue>(val);
arrayValue->assign(std::make_shared<ExprEngine::IntRange>("0", 0, 0), std::make_shared<ExprEngine::BailoutValue>());
if (!val || (val->type != ExprEngine::ValueType::ArrayValue &&
val->type != ExprEngine::ValueType::AddressOfValue))
Comment thread
jubnzv marked this conversation as resolved.
throw ExprEngineException(tok2, "Unhandled assignment in loop");
Comment thread
jubnzv marked this conversation as resolved.
// Handle the value that we are pointing to
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);

@danmar danmar Dec 15, 2020

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We are not trying to execute the loop yet. We should call callbacks later when the loop is executed. We also do not know if the variable will still have the oldValue when this code is reached (it will if this is unconditionally executed).

@jubnzv jubnzv Dec 16, 2020

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Then why do we call them in variable assignments here?

if (val->type == ExprEngine::ValueType::ArrayValue) {
// Unknown pointer, array or struct
auto arrayValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(val);
assert(arrayValue);
data.assignValue(tok2, varid, val);

@danmar danmar Dec 15, 2020

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

as far as I see this assignment is redundant.. it assigns the same value as we already have.

} else if (val->type == ExprEngine::ValueType::AddressOfValue) {
// Address of a known variable
auto addressOf = std::dynamic_pointer_cast<ExprEngine::AddressOfValue>(val);
assert(addressOf);
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;
Expand Down
30 changes: 29 additions & 1 deletion test/testexprengine.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -78,6 +79,8 @@ class TestExprEngine : public TestFixture {
TEST_CASE(while3);
TEST_CASE(while4);
TEST_CASE(while5);
TEST_CASE(while6);
TEST_CASE(while7);

TEST_CASE(array1);
TEST_CASE(array2);
Expand Down Expand Up @@ -355,7 +358,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"));
}

void exprNot() {
Expand Down Expand Up @@ -607,6 +614,27 @@ 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 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",
Expand Down