Bug hunting; review and improve handling of multi dimensional arrays
This commit is contained in:
parent
d984d84450
commit
4947a3b7ab
|
@ -204,7 +204,6 @@ namespace {
|
||||||
return;
|
return;
|
||||||
mSymbols.insert(symbolicExpression);
|
mSymbols.insert(symbolicExpression);
|
||||||
mMap[tok].push_back(symbolicExpression + "=" + value->getRange());
|
mMap[tok].push_back(symbolicExpression + "=" + value->getRange());
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
void state(const Token *tok, const std::string &s) {
|
void state(const Token *tok, const std::string &s) {
|
||||||
|
@ -342,7 +341,8 @@ namespace {
|
||||||
mTrackExecution->symbolRange(tok, value);
|
mTrackExecution->symbolRange(tok, value);
|
||||||
if (value) {
|
if (value) {
|
||||||
if (auto arr = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(value)) {
|
if (auto arr = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(value)) {
|
||||||
mTrackExecution->symbolRange(tok, arr->size);
|
for (const auto &dim: arr->size)
|
||||||
|
mTrackExecution->symbolRange(tok, dim);
|
||||||
for (const auto &indexAndValue: arr->data)
|
for (const auto &indexAndValue: arr->data)
|
||||||
mTrackExecution->symbolRange(tok, indexAndValue.value);
|
mTrackExecution->symbolRange(tok, indexAndValue.value);
|
||||||
} else if (auto s = std::dynamic_pointer_cast<ExprEngine::StructValue>(value)) {
|
} else if (auto s = std::dynamic_pointer_cast<ExprEngine::StructValue>(value)) {
|
||||||
|
@ -564,7 +564,7 @@ static int128_t truncateInt(int128_t value, int bits, char sign)
|
||||||
ExprEngine::ArrayValue::ArrayValue(const std::string &name, ExprEngine::ValuePtr size, ExprEngine::ValuePtr value, bool pointer, bool nullPointer, bool uninitPointer)
|
ExprEngine::ArrayValue::ArrayValue(const std::string &name, ExprEngine::ValuePtr size, ExprEngine::ValuePtr value, bool pointer, bool nullPointer, bool uninitPointer)
|
||||||
: Value(name, ExprEngine::ValueType::ArrayValue)
|
: Value(name, ExprEngine::ValueType::ArrayValue)
|
||||||
, pointer(pointer), nullPointer(nullPointer), uninitPointer(uninitPointer)
|
, pointer(pointer), nullPointer(nullPointer), uninitPointer(uninitPointer)
|
||||||
, size(size)
|
, size{size}
|
||||||
{
|
{
|
||||||
assign(ExprEngine::ValuePtr(), value);
|
assign(ExprEngine::ValuePtr(), value);
|
||||||
}
|
}
|
||||||
|
@ -574,17 +574,16 @@ ExprEngine::ArrayValue::ArrayValue(DataBase *data, const Variable *var)
|
||||||
, pointer(var->isPointer()), nullPointer(var->isPointer()), uninitPointer(var->isPointer())
|
, pointer(var->isPointer()), nullPointer(var->isPointer()), uninitPointer(var->isPointer())
|
||||||
{
|
{
|
||||||
if (var) {
|
if (var) {
|
||||||
int sz = 1;
|
|
||||||
for (const auto &dim : var->dimensions()) {
|
for (const auto &dim : var->dimensions()) {
|
||||||
if (!dim.known) {
|
if (dim.known)
|
||||||
sz = -1;
|
size.push_back(std::make_shared<ExprEngine::IntRange>(std::to_string(dim.num), dim.num, dim.num));
|
||||||
break;
|
else
|
||||||
}
|
size.push_back(std::make_shared<ExprEngine::IntRange>(data->getNewSymbolName(), 1, ExprEngine::ArrayValue::MAXSIZE));
|
||||||
sz *= dim.num;
|
|
||||||
}
|
}
|
||||||
if (sz >= 1)
|
} else {
|
||||||
size = std::make_shared<ExprEngine::IntRange>(std::to_string(sz), sz, sz);
|
size.push_back(std::make_shared<ExprEngine::IntRange>(data->getNewSymbolName(), 1, ExprEngine::ArrayValue::MAXSIZE));
|
||||||
}
|
}
|
||||||
|
|
||||||
ValuePtr val;
|
ValuePtr val;
|
||||||
if (var && !var->isGlobal() && !var->isStatic())
|
if (var && !var->isGlobal() && !var->isStatic())
|
||||||
val = std::make_shared<ExprEngine::UninitValue>();
|
val = std::make_shared<ExprEngine::UninitValue>();
|
||||||
|
@ -727,7 +726,12 @@ std::string ExprEngine::ConditionalValue::getSymbolicExpression() const
|
||||||
std::string ExprEngine::ArrayValue::getSymbolicExpression() const
|
std::string ExprEngine::ArrayValue::getSymbolicExpression() const
|
||||||
{
|
{
|
||||||
std::ostringstream ostr;
|
std::ostringstream ostr;
|
||||||
ostr << "size=" << (size ? size->name : std::string("(null)"));
|
if (size.empty())
|
||||||
|
ostr << "(null)";
|
||||||
|
else {
|
||||||
|
for (const auto &dim: size)
|
||||||
|
ostr << "[" << (dim ? dim->name : std::string("(null)")) << "]";
|
||||||
|
}
|
||||||
for (const auto &indexAndValue : data) {
|
for (const auto &indexAndValue : data) {
|
||||||
ostr << ",["
|
ostr << ",["
|
||||||
<< (!indexAndValue.index ? std::string(":") : indexAndValue.index->name)
|
<< (!indexAndValue.index ? std::string(":") : indexAndValue.index->name)
|
||||||
|
@ -1252,6 +1256,47 @@ static void call(const std::vector<ExprEngine::Callback> &callbacks, const Token
|
||||||
static ExprEngine::ValuePtr executeExpression(const Token *tok, Data &data);
|
static ExprEngine::ValuePtr executeExpression(const Token *tok, Data &data);
|
||||||
static ExprEngine::ValuePtr executeExpression1(const Token *tok, Data &data);
|
static ExprEngine::ValuePtr executeExpression1(const Token *tok, Data &data);
|
||||||
|
|
||||||
|
static ExprEngine::ValuePtr calculateArrayIndex(const Token *tok, Data &data, const ExprEngine::ArrayValue &arrayValue)
|
||||||
|
{
|
||||||
|
int nr = 1;
|
||||||
|
const Token *tok2 = tok;
|
||||||
|
while (Token::simpleMatch(tok2->astOperand1(), "[")) {
|
||||||
|
tok2 = tok2->astOperand1();
|
||||||
|
nr++;
|
||||||
|
}
|
||||||
|
|
||||||
|
ExprEngine::ValuePtr totalIndex;
|
||||||
|
ExprEngine::ValuePtr dim;
|
||||||
|
while (Token::simpleMatch(tok, "[")) {
|
||||||
|
auto rawIndex = executeExpression(tok->astOperand2(), data);
|
||||||
|
|
||||||
|
ExprEngine::ValuePtr index;
|
||||||
|
if (dim)
|
||||||
|
index = simplifyValue(std::make_shared<ExprEngine::BinOpResult>("*", dim, rawIndex));
|
||||||
|
else
|
||||||
|
index = rawIndex;
|
||||||
|
|
||||||
|
if (!totalIndex)
|
||||||
|
totalIndex = index;
|
||||||
|
else
|
||||||
|
totalIndex = simplifyValue(std::make_shared<ExprEngine::BinOpResult>("+", index, totalIndex));
|
||||||
|
|
||||||
|
if (arrayValue.size.size() >= nr) {
|
||||||
|
if (arrayValue.size[nr-1]) {
|
||||||
|
if (!dim)
|
||||||
|
dim = arrayValue.size[nr-1];
|
||||||
|
else
|
||||||
|
dim = simplifyValue(std::make_shared<ExprEngine::BinOpResult>("*", dim, arrayValue.size[nr-1]));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
nr--;
|
||||||
|
tok = tok->astOperand1();
|
||||||
|
}
|
||||||
|
|
||||||
|
return totalIndex;
|
||||||
|
}
|
||||||
|
|
||||||
static ExprEngine::ValuePtr executeReturn(const Token *tok, Data &data)
|
static ExprEngine::ValuePtr executeReturn(const Token *tok, Data &data)
|
||||||
{
|
{
|
||||||
ExprEngine::ValuePtr retval = executeExpression(tok->astOperand1(), data);
|
ExprEngine::ValuePtr retval = executeExpression(tok->astOperand1(), data);
|
||||||
|
@ -1334,15 +1379,18 @@ static ExprEngine::ValuePtr executeAssign(const Token *tok, Data &data)
|
||||||
if (lhsToken->varId() > 0) {
|
if (lhsToken->varId() > 0) {
|
||||||
data.assignValue(lhsToken, lhsToken->varId(), assignValue);
|
data.assignValue(lhsToken, lhsToken->varId(), assignValue);
|
||||||
} else if (lhsToken->str() == "[") {
|
} else if (lhsToken->str() == "[") {
|
||||||
auto arrayValue = data.getArrayValue(lhsToken->astOperand1());
|
const Token *tok2 = lhsToken;
|
||||||
|
while (Token::simpleMatch(tok2->astOperand1(), "["))
|
||||||
|
tok2 = tok2->astOperand1();
|
||||||
|
auto arrayValue = data.getArrayValue(tok2->astOperand1());
|
||||||
if (arrayValue) {
|
if (arrayValue) {
|
||||||
// Is it array initialization?
|
// Is it array initialization?
|
||||||
const Token *arrayInit = lhsToken->astOperand1();
|
const Token *arrayInit = tok2->astOperand1();
|
||||||
if (arrayInit && arrayInit->variable() && arrayInit->variable()->nameToken() == arrayInit) {
|
if (arrayInit && arrayInit->variable() && arrayInit->variable()->nameToken() == arrayInit) {
|
||||||
if (assignValue->type == ExprEngine::ValueType::StringLiteralValue)
|
if (assignValue->type == ExprEngine::ValueType::StringLiteralValue)
|
||||||
arrayValue->assign(ExprEngine::ValuePtr(), assignValue);
|
arrayValue->assign(ExprEngine::ValuePtr(), assignValue);
|
||||||
} else {
|
} else {
|
||||||
auto indexValue = executeExpression(lhsToken->astOperand2(), data);
|
auto indexValue = calculateArrayIndex(lhsToken, data, *arrayValue);
|
||||||
arrayValue->assign(indexValue, assignValue);
|
arrayValue->assign(indexValue, assignValue);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -1511,9 +1559,12 @@ static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data)
|
||||||
|
|
||||||
static ExprEngine::ValuePtr executeArrayIndex(const Token *tok, Data &data)
|
static ExprEngine::ValuePtr executeArrayIndex(const Token *tok, Data &data)
|
||||||
{
|
{
|
||||||
auto arrayValue = data.getArrayValue(tok->astOperand1());
|
const Token *tok2 = tok;
|
||||||
|
while (Token::simpleMatch(tok2->astOperand1(), "["))
|
||||||
|
tok2 = tok2->astOperand1();
|
||||||
|
auto arrayValue = data.getArrayValue(tok2->astOperand1());
|
||||||
if (arrayValue) {
|
if (arrayValue) {
|
||||||
auto indexValue = executeExpression(tok->astOperand2(), data);
|
auto indexValue = calculateArrayIndex(tok, data, *arrayValue);
|
||||||
auto conditionalValues = arrayValue->read(indexValue);
|
auto conditionalValues = arrayValue->read(indexValue);
|
||||||
for (auto value: conditionalValues)
|
for (auto value: conditionalValues)
|
||||||
call(data.callbacks, tok, value.second, &data);
|
call(data.callbacks, tok, value.second, &data);
|
||||||
|
|
|
@ -204,7 +204,7 @@ namespace ExprEngine {
|
||||||
ValuePtr value;
|
ValuePtr value;
|
||||||
};
|
};
|
||||||
std::vector<IndexAndValue> data;
|
std::vector<IndexAndValue> data;
|
||||||
ValuePtr size;
|
std::vector<ValuePtr> size;
|
||||||
};
|
};
|
||||||
|
|
||||||
class StringLiteralValue: public Value {
|
class StringLiteralValue: public Value {
|
||||||
|
|
|
@ -70,6 +70,7 @@ private:
|
||||||
TEST_CASE(array2);
|
TEST_CASE(array2);
|
||||||
TEST_CASE(array3);
|
TEST_CASE(array3);
|
||||||
TEST_CASE(array4);
|
TEST_CASE(array4);
|
||||||
|
TEST_CASE(array5);
|
||||||
TEST_CASE(arrayInit1);
|
TEST_CASE(arrayInit1);
|
||||||
TEST_CASE(arrayInit2);
|
TEST_CASE(arrayInit2);
|
||||||
TEST_CASE(arrayUninit);
|
TEST_CASE(arrayUninit);
|
||||||
|
@ -509,7 +510,20 @@ private:
|
||||||
"void f() { int x = buf[0]; }";
|
"void f() { int x = buf[0]; }";
|
||||||
ASSERT_EQUALS("2:16: $2:0=-2147483648:2147483647\n"
|
ASSERT_EQUALS("2:16: $2:0=-2147483648:2147483647\n"
|
||||||
"2:20: $2=-2147483648:2147483647\n"
|
"2:20: $2=-2147483648:2147483647\n"
|
||||||
"2:26: { buf=($1,size=10,[:]=$2) x=$2:0}\n",
|
"2:26: { buf=($1,[10],[:]=$2) x=$2:0}\n",
|
||||||
|
trackExecution(code));
|
||||||
|
}
|
||||||
|
|
||||||
|
void array5() {
|
||||||
|
const char code[] = "int f(int x) {\n"
|
||||||
|
" int buf[3][4][5];\n"
|
||||||
|
" buf[x][1][2] = 10;\n"
|
||||||
|
" return buf[0][1][2];\n"
|
||||||
|
"}";
|
||||||
|
ASSERT_EQUALS("1:14: $1=-2147483648:2147483647\n"
|
||||||
|
"1:14: { x=$1}\n"
|
||||||
|
"2:19: { x=$1 buf=($2,[3][4][5],[:]=?)}\n"
|
||||||
|
"3:20: { x=$1 buf=($2,[3][4][5],[:]=?,[((20)*($1))+(7)]=10)}\n",
|
||||||
trackExecution(code));
|
trackExecution(code));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -531,7 +545,7 @@ private:
|
||||||
" for (int i = 0; i < 3; i++) arr[i][0] = arr[1][2];\n"
|
" for (int i = 0; i < 3; i++) arr[i][0] = arr[1][2];\n"
|
||||||
" return arr[0][0];"
|
" return arr[0][0];"
|
||||||
"}";
|
"}";
|
||||||
ASSERT_EQUALS("?", getRange(code, "arr[1]"));
|
ASSERT_EQUALS("?", getRange(code, "arr[1][2]"));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@ -601,7 +615,7 @@ private:
|
||||||
|
|
||||||
void pointer1() {
|
void pointer1() {
|
||||||
const char code[] = "void f(unsigned char *p) { return *p == 7; }";
|
const char code[] = "void f(unsigned char *p) { return *p == 7; }";
|
||||||
ASSERT_EQUALS("size=$1,[:]=?,null", getRange(code, "p"));
|
ASSERT_EQUALS("[$1],[:]=?,null", getRange(code, "p"));
|
||||||
ASSERT_EQUALS("(and (>= $3 0) (<= $3 255))\n"
|
ASSERT_EQUALS("(and (>= $3 0) (<= $3 255))\n"
|
||||||
"(= $3 7)\n"
|
"(= $3 7)\n"
|
||||||
"z3::sat\n",
|
"z3::sat\n",
|
||||||
|
|
Loading…
Reference in New Issue