From 2710a94b4b92a72f12c1c733ca14207c0b52a005 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Sun, 29 Dec 2019 16:26:11 +0100 Subject: [PATCH] Verification; Merged handling of pointers and arrays --- lib/exprengine.cpp | 69 +++++++++++++++++++++++------------------ lib/exprengine.h | 23 +++++--------- test/testexprengine.cpp | 18 ++++++++--- 3 files changed, 59 insertions(+), 51 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 8b998209d..fefe4a239 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -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(data.getNewSymbolName(), 0, ~0ULL); auto value = std::make_shared(data.getNewSymbolName(), -128, 127); - rhsValue = std::make_shared(data.getNewSymbolName(), size, value); + rhsValue = std::make_shared(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(val)->null; - uninit = std::static_pointer_cast(val)->uninitData; + bool uninitPointer = false, nullPointer = false; + if (val && val->type == ExprEngine::ValueType::ArrayValue) { + nullPointer = std::static_pointer_cast(val)->nullPointer; + uninitPointer = std::static_pointer_cast(val)->uninitPointer; } - return std::make_shared(data.getNewSymbolName(), range, null, uninit); + auto bufferSize = std::make_shared(data.getNewSymbolName(), 1, ~0UL); + return std::make_shared(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 structValue = std::dynamic_pointer_cast(data.getValue(tok->astOperand1()->varId(), nullptr, nullptr)); if (!structValue) { if (tok->originalName() == "->") { - std::shared_ptr pointerValue = std::dynamic_pointer_cast(data.getValue(tok->astOperand1()->varId(), nullptr, nullptr)); - if (pointerValue) { + std::shared_ptr pointerValue = std::dynamic_pointer_cast(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(pointerValue->data); + structValue = std::dynamic_pointer_cast(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(data.getNewSymbolName(), v, false, false); + pval = std::make_shared(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(pval); + auto pointer = std::dynamic_pointer_cast(pval); if (pointer) { - auto val = pointer->data; - call(data.callbacks, tok, val, &data); - return val; + auto indexValue = std::make_shared("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(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(data.getNewSymbolName(), range, true, true); + auto size = std::make_shared(data.getNewSymbolName(), 1, ~0UL); + return std::make_shared(data.getNewSymbolName(), size, range, true, true, true); } if (var.isArray()) return std::make_shared(&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(data.getNewSymbolName(), structValue, true, false); + auto size = std::make_shared(data.getNewSymbolName(), 1, ~0UL); + return std::make_shared(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(data.getNewSymbolName(), 0, ~0ULL); - return std::make_shared(data.getNewSymbolName(), size, value); + auto bufferSize = std::make_shared(data.getNewSymbolName(), 0, ~0U); + return std::make_shared(data.getNewSymbolName(), bufferSize, value, false, false, false); } return ExprEngine::ValuePtr(); } diff --git a/lib/exprengine.h b/lib/exprengine.h index 909959f76..07ae97e34 100644 --- a/lib/exprengine.h +++ b/lib/exprengine.h @@ -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> 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; diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index c6bb8147d..f2a4d8031 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -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, "==")); }