walkero
/
cppcheck
1
0
Fork 0
Code Issues Pull Requests Projects Releases 1 Wiki Activity

Verification; Merged handling of pointers and arrays

This commit is contained in:
Daniel Marjamäki 2019-12-29 16:26:11 +01:00
parent 1cef732e1b
commit 2710a94b4b
3 changed files with 59 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

69
lib/exprengine.cpp
View File

@ -360,8 +360,9 @@ static int128_t truncateInt(int128_t value, int bits, char sign)
return value;
}
ExprEngine::ArrayValue::ArrayValue(const std::string &name, ExprEngine::ValuePtr size, ExprEngine::ValuePtr value)
ExprEngine::ArrayValue::ArrayValue(const std::string &name, ExprEngine::ValuePtr size, ExprEngine::ValuePtr value, bool pointer, bool nullPointer, bool uninitPointer)
: Value(name, ExprEngine::ValueType::ArrayValue)
, pointer(pointer), nullPointer(nullPointer), uninitPointer(uninitPointer)
, size(size)
{
assign(ExprEngine::ValuePtr(), value);
@ -369,6 +370,7 @@ ExprEngine::ArrayValue::ArrayValue(const std::string &name, ExprEngine::ValuePtr
ExprEngine::ArrayValue::ArrayValue(DataBase *data, const Variable *var)
: Value(data->getNewSymbolName(), ExprEngine::ValueType::ArrayValue)
, pointer(var->isPointer()), nullPointer(var->isPointer()), uninitPointer(var->isPointer())
{
if (var) {
int sz = 1;
@ -393,6 +395,16 @@ ExprEngine::ArrayValue::ArrayValue(DataBase *data, const Variable *var)
assign(ExprEngine::ValuePtr(), val);
}
std::string ExprEngine::ArrayValue::getRange() const
{
std::string r = getSymbolicExpression();
if (nullPointer)
r += std::string(r.empty() ? "" : ",") + "null";
if (uninitPointer)
r += std::string(r.empty() ? "" : ",") + "->?";
return r;
}
void ExprEngine::ArrayValue::assign(ExprEngine::ValuePtr index, ExprEngine::ValuePtr value)
{
if (!index)
@ -541,18 +553,6 @@ std::string ExprEngine::StructValue::getSymbolicExpression() const
return ostr.str();
}
std::string ExprEngine::PointerValue::getRange() const
{
std::string r;
if (data)
r = "->" + data->getSymbolicExpression();
if (null)
r += std::string(r.empty() ? "" : ",") + "null";
if (uninitData)
r += std::string(r.empty() ? "" : ",") + "->?";
return r;
}
std::string ExprEngine::IntegerTruncation::getSymbolicExpression() const
{
return sign + std::to_string(bits) + "(" + inputValue->getSymbolicExpression() + ")";
@ -983,7 +983,7 @@ static ExprEngine::ValuePtr executeAssign(const Token *tok, Data &data)
if (!rhsValue && tok->astOperand2()->valueType() && tok->astOperand2()->valueType()->container && tok->astOperand2()->valueType()->container->stdStringLike) {
auto size = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 0, ~0ULL);
auto value = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), -128, 127);
rhsValue = std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), size, value);
rhsValue = std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), size, value, false, false, false);
call(data.callbacks, tok->astOperand2(), rhsValue, &data);
}
@ -1114,13 +1114,14 @@ static ExprEngine::ValuePtr executeCast(const Token *tok, Data &data)
if (tok->valueType()->pointer == 0)
return range;
bool uninit = false, null = false;
if (val && val->type == ExprEngine::ValueType::PointerValue) {
null = std::static_pointer_cast<ExprEngine::PointerValue>(val)->null;
uninit = std::static_pointer_cast<ExprEngine::PointerValue>(val)->uninitData;
bool uninitPointer = false, nullPointer = false;
if (val && val->type == ExprEngine::ValueType::ArrayValue) {
nullPointer = std::static_pointer_cast<ExprEngine::ArrayValue>(val)->nullPointer;
uninitPointer = std::static_pointer_cast<ExprEngine::ArrayValue>(val)->uninitPointer;
}
return std::make_shared<ExprEngine::PointerValue>(data.getNewSymbolName(), range, null, uninit);
auto bufferSize = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 1, ~0UL);
return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), bufferSize, range, true, nullPointer, uninitPointer);
}
if (val)
@ -1140,10 +1141,10 @@ static ExprEngine::ValuePtr executeDot(const Token *tok, Data &data)
std::shared_ptr<ExprEngine::StructValue> structValue = std::dynamic_pointer_cast<ExprEngine::StructValue>(data.getValue(tok->astOperand1()->varId(), nullptr, nullptr));
if (!structValue) {
if (tok->originalName() == "->") {
std::shared_ptr<ExprEngine::PointerValue> pointerValue = std::dynamic_pointer_cast<ExprEngine::PointerValue>(data.getValue(tok->astOperand1()->varId(), nullptr, nullptr));
if (pointerValue) {
std::shared_ptr<ExprEngine::ArrayValue> pointerValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(data.getValue(tok->astOperand1()->varId(), nullptr, nullptr));
if (pointerValue && pointerValue->pointer && pointerValue->data.size() == 1) {
call(data.callbacks, tok->astOperand1(), pointerValue, &data);
structValue = std::dynamic_pointer_cast<ExprEngine::StructValue>(pointerValue->data);
structValue = std::dynamic_pointer_cast<ExprEngine::StructValue>(pointerValue->data[0].value);
} else {
call(data.callbacks, tok->astOperand1(), data.getValue(tok->astOperand1()->varId(), nullptr, nullptr), &data);
}
@ -1190,7 +1191,7 @@ static ExprEngine::ValuePtr executeDeref(const Token *tok, Data &data)
if (!pval) {
auto v = getValueRangeFromValueType(data.getNewSymbolName(), tok->valueType(), *data.settings);
if (tok->astOperand1()->varId()) {
pval = std::make_shared<ExprEngine::PointerValue>(data.getNewSymbolName(), v, false, false);
pval = std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), ExprEngine::ValuePtr(), v, true, false, false);
data.assignValue(tok->astOperand1(), tok->astOperand1()->varId(), pval);
}
call(data.callbacks, tok, v, &data);
@ -1202,11 +1203,15 @@ static ExprEngine::ValuePtr executeDeref(const Token *tok, Data &data)
call(data.callbacks, tok, val, &data);
return val;
}
auto pointer = std::dynamic_pointer_cast<ExprEngine::PointerValue>(pval);
auto pointer = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(pval);
if (pointer) {
auto val = pointer->data;
call(data.callbacks, tok, val, &data);
return val;
auto indexValue = std::make_shared<ExprEngine::IntRange>("0", 0, 0);
auto conditionalValues = pointer->read(indexValue);
for (auto value: conditionalValues)
call(data.callbacks, tok, value.second, &data);
if (conditionalValues.size() == 1 && !conditionalValues[0].first)
return conditionalValues[0].second;
return std::make_shared<ExprEngine::ConditionalValue>(data.getNewSymbolName(), conditionalValues);
}
return ExprEngine::ValuePtr();
}
@ -1522,7 +1527,8 @@ static ExprEngine::ValuePtr createVariableValue(const Variable &var, Data &data)
ValueType vt(*valueType);
vt.pointer = 0;
auto range = getValueRangeFromValueType(data.getNewSymbolName(), &vt, *data.settings);
return std::make_shared<ExprEngine::PointerValue>(data.getNewSymbolName(), range, true, true);
auto size = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 1, ~0UL);
return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), size, range, true, true, true);
}
if (var.isArray())
return std::make_shared<ExprEngine::ArrayValue>(&data, &var);
@ -1535,7 +1541,8 @@ static ExprEngine::ValuePtr createVariableValue(const Variable &var, Data &data)
return createStructVal(valueType->typeScope, var.isLocal() && !var.isStatic(), data);
if (valueType->smartPointerType) {
auto structValue = createStructVal(valueType->smartPointerType->classScope, var.isLocal() && !var.isStatic(), data);
return std::make_shared<ExprEngine::PointerValue>(data.getNewSymbolName(), structValue, true, false);
auto size = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 1, ~0UL);
return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), size, structValue, true, true, false);
}
if (valueType->container) {
ExprEngine::ValuePtr value;
@ -1546,8 +1553,8 @@ static ExprEngine::ValuePtr createVariableValue(const Variable &var, Data &data)
value = getValueRangeFromValueType(data.getNewSymbolName(), &vt, *data.settings);
} else
return ExprEngine::ValuePtr();
auto size = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 0, ~0ULL);
return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), size, value);
auto bufferSize = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 0, ~0U);
return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), bufferSize, value, false, false, false);
}
return ExprEngine::ValuePtr();
}

23
lib/exprengine.h
View File

@ -57,7 +57,6 @@ namespace ExprEngine {
UninitValue,
IntRange,
FloatRange,
PointerValue,
ConditionalValue,
ArrayValue,
StringLiteralValue,
@ -157,20 +156,6 @@ namespace ExprEngine {
long double maxValue;
};
class PointerValue: public Value {
public:
PointerValue(const std::string &name, ValuePtr data, bool null, bool uninitData)
: Value(name, ValueType::PointerValue)
, data(data)
, null(null)
, uninitData(uninitData) {
}
std::string getRange() const OVERRIDE;
ValuePtr data;
bool null;
bool uninitData;
};
class ConditionalValue : public Value {
public:
typedef std::vector<std::pair<ValuePtr,ValuePtr>> Vector;
@ -182,19 +167,25 @@ namespace ExprEngine {
Vector values;
};
// Array or pointer
class ArrayValue: public Value {
public:
const int MAXSIZE = 0x100000;
ArrayValue(const std::string &name, ValuePtr size, ValuePtr value);
ArrayValue(const std::string &name, ValuePtr size, ValuePtr value, bool pointer, bool nullPointer, bool uninitPointer);
ArrayValue(DataBase *data, const Variable *var);
std::string getRange() const;
std::string getSymbolicExpression() const OVERRIDE;
void assign(ValuePtr index, ValuePtr value);
void clear();
ConditionalValue::Vector read(ValuePtr index) const;
bool pointer;
bool nullPointer;
bool uninitPointer;
struct IndexAndValue {
ValuePtr index;
ValuePtr value;

18
test/testexprengine.cpp
View File

@ -74,6 +74,7 @@ private:
TEST_CASE(int1);
TEST_CASE(pointer1);
TEST_CASE(pointer2);
TEST_CASE(pointerAlias1);
TEST_CASE(pointerAlias2);
TEST_CASE(pointerAlias3);
@ -414,10 +415,19 @@ private:
void pointer1() {
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 (and (>= $1 0) (<= $1 255)))\n"
"(assert (= $1 7))\n"
ASSERT_EQUALS("size=$2,[:]=$1,null,->?", getRange(code, "p"));
ASSERT_EQUALS("(declare-fun |$1:0| () Int)\n"
"(assert (and (>= |$1:0| 0) (<= |$1:0| 255)))\n"
"(assert (= |$1:0| 7))\n"
"z3::sat",
expr(code, "=="));
}
void pointer2() {
const char code[] = "void f(unsigned char *p) { return p[2] == 7; }";
ASSERT_EQUALS("(declare-fun |$1:2| () Int)\n"
"(assert (and (>= |$1:2| 0) (<= |$1:2| 255)))\n"
"(assert (= |$1:2| 7))\n"
"z3::sat",
expr(code, "=="));
}