ExprEngine: ConditionalValues, output symbolic expressions
This commit is contained in:
parent
c2a6053d7f
commit
c5302d20a3
|
@ -66,12 +66,6 @@ namespace {
|
|||
return;
|
||||
if (!value)
|
||||
map[tok].push_back(tok->expressionString() + "=TODO_NO_VALUE");
|
||||
/*
|
||||
else if (value->name[0] == '$')
|
||||
map[tok].push_back(tok->expressionString() + "=(" + value->name + "," + value->getRange() + ")");
|
||||
else
|
||||
map[tok].push_back(tok->expressionString() + "=" + value->name);
|
||||
*/
|
||||
}
|
||||
|
||||
void state(const Token *tok, const std::string &s) {
|
||||
|
@ -224,7 +218,7 @@ namespace {
|
|||
if (!value)
|
||||
s << "(null)";
|
||||
else if (value->name[0] == '$')
|
||||
s << "(" << value->name << "," << value->getRange() << ")";
|
||||
s << "(" << value->name << "," << value->getSymbolicExpression() << ")";
|
||||
else
|
||||
s << value->name;
|
||||
}
|
||||
|
@ -268,14 +262,14 @@ static ExprEngine::ValuePtr simplifyValue(ExprEngine::ValuePtr origValue)
|
|||
|
||||
|
||||
ExprEngine::ArrayValue::ArrayValue(const std::string &name, ExprEngine::ValuePtr size, ExprEngine::ValuePtr value)
|
||||
: Value(name)
|
||||
: Value(name, ExprEngine::ValueType::ArrayValue)
|
||||
, size(size)
|
||||
{
|
||||
assign(ExprEngine::ValuePtr(), value);
|
||||
}
|
||||
|
||||
ExprEngine::ArrayValue::ArrayValue(const std::string &name, const Variable *var)
|
||||
: Value(name)
|
||||
: Value(name, ExprEngine::ValueType::ArrayValue)
|
||||
{
|
||||
if (var) {
|
||||
int sz = 1;
|
||||
|
@ -315,8 +309,7 @@ static bool isEqual(ExprEngine::ValuePtr v1, ExprEngine::ValuePtr v2)
|
|||
{
|
||||
if (!v1 || !v2)
|
||||
return !v1 && !v2;
|
||||
// TODO: Maybe we need better logic here:
|
||||
return v1->getRange() == v2->getRange();
|
||||
return v1->name == v2->name;
|
||||
}
|
||||
|
||||
static bool isNonOverlapping(ExprEngine::ValuePtr v1, ExprEngine::ValuePtr v2)
|
||||
|
@ -330,18 +323,19 @@ static bool isNonOverlapping(ExprEngine::ValuePtr v1, ExprEngine::ValuePtr v2)
|
|||
return false;
|
||||
}
|
||||
|
||||
std::vector<ExprEngine::ValuePtr> ExprEngine::ArrayValue::read(ExprEngine::ValuePtr index)
|
||||
ExprEngine::ConditionalValue::Vector ExprEngine::ArrayValue::read(ExprEngine::ValuePtr index) const
|
||||
{
|
||||
std::vector<ExprEngine::ValuePtr> ret;
|
||||
ExprEngine::ConditionalValue::Vector ret;
|
||||
for (const auto indexAndValue : data) {
|
||||
if (isEqual(index, indexAndValue.index))
|
||||
ret.clear();
|
||||
if (isNonOverlapping(index, indexAndValue.index))
|
||||
continue;
|
||||
if (!indexAndValue.index && indexAndValue.value->type() == ExprEngine::ValueType::StringLiteralValue) {
|
||||
// Array contains string literal data...
|
||||
if (!indexAndValue.index && indexAndValue.value->type == ExprEngine::ValueType::StringLiteralValue) {
|
||||
auto stringLiteral = std::dynamic_pointer_cast<ExprEngine::StringLiteralValue>(indexAndValue.value);
|
||||
if (!stringLiteral) {
|
||||
ret.push_back(std::make_shared<ExprEngine::IntRange>("", -128, 128));
|
||||
ret.push_back(std::pair<ValuePtr,ValuePtr>(indexAndValue.index, std::make_shared<ExprEngine::IntRange>("", -128, 128)));
|
||||
continue;
|
||||
}
|
||||
if (auto i = std::dynamic_pointer_cast<ExprEngine::IntRange>(index)) {
|
||||
|
@ -349,7 +343,7 @@ std::vector<ExprEngine::ValuePtr> ExprEngine::ArrayValue::read(ExprEngine::Value
|
|||
int c = 0;
|
||||
if (i->minValue < stringLiteral->size())
|
||||
c = stringLiteral->string[i->minValue];
|
||||
ret.push_back(std::make_shared<ExprEngine::IntRange>(std::to_string(c), c, c));
|
||||
ret.push_back(std::pair<ValuePtr,ValuePtr>(indexAndValue.index, std::make_shared<ExprEngine::IntRange>(std::to_string(c), c, c)));
|
||||
continue;
|
||||
}
|
||||
}
|
||||
|
@ -360,15 +354,48 @@ std::vector<ExprEngine::ValuePtr> ExprEngine::ArrayValue::read(ExprEngine::Value
|
|||
else if (c > cmax)
|
||||
cmax = c;
|
||||
}
|
||||
ret.push_back(std::make_shared<ExprEngine::IntRange>("", cmin, cmax));
|
||||
ret.push_back(std::pair<ValuePtr,ValuePtr>(indexAndValue.index, std::make_shared<ExprEngine::IntRange>("", cmin, cmax)));
|
||||
continue;
|
||||
}
|
||||
ret.push_back(indexAndValue.value);
|
||||
ret.push_back(std::pair<ValuePtr,ValuePtr>(indexAndValue.index, indexAndValue.value));
|
||||
}
|
||||
|
||||
if (ret.size() == 1)
|
||||
ret[0].first = ExprEngine::ValuePtr();
|
||||
else if (ret.size() == 2 && !ret[0].first) {
|
||||
ret[0].first = std::make_shared<ExprEngine::BinOpResult>("!=", index, ret[1].first);
|
||||
ret[1].first = std::make_shared<ExprEngine::BinOpResult>("==", index, ret[1].first);
|
||||
} else {
|
||||
// FIXME!!
|
||||
ret.clear();
|
||||
}
|
||||
|
||||
return ret;
|
||||
}
|
||||
|
||||
std::string ExprEngine::ArrayValue::getRange() const
|
||||
std::string ExprEngine::ConditionalValue::getSymbolicExpression() const
|
||||
{
|
||||
std::ostringstream ostr;
|
||||
ostr << "{";
|
||||
bool first = true;
|
||||
for (auto condvalue : values) {
|
||||
ValuePtr cond = condvalue.first;
|
||||
ValuePtr value = condvalue.second;
|
||||
|
||||
if (!first)
|
||||
ostr << ",";
|
||||
first = false;
|
||||
ostr << "{"
|
||||
<< (cond ? cond->getSymbolicExpression() : std::string("(null)"))
|
||||
<< ","
|
||||
<< value->getSymbolicExpression()
|
||||
<< "}";
|
||||
}
|
||||
ostr << "}";
|
||||
return ostr.str();
|
||||
}
|
||||
|
||||
std::string ExprEngine::ArrayValue::getSymbolicExpression() const
|
||||
{
|
||||
std::ostringstream ostr;
|
||||
ostr << "size=" << (size ? size->name : std::string("(null)"));
|
||||
|
@ -385,7 +412,7 @@ std::string ExprEngine::PointerValue::getRange() const
|
|||
{
|
||||
std::string r;
|
||||
if (data)
|
||||
r = "->" + data->getRange();
|
||||
r = "->" + data->getSymbolicExpression();
|
||||
if (null)
|
||||
r += std::string(r.empty() ? "" : ",") + "null";
|
||||
if (uninitData)
|
||||
|
@ -446,9 +473,9 @@ void ExprEngine::BinOpResult::getRange(ExprEngine::BinOpResult::IntOrFloatValue
|
|||
}
|
||||
}
|
||||
|
||||
std::string ExprEngine::IntegerTruncation::getRange() const
|
||||
std::string ExprEngine::IntegerTruncation::getSymbolicExpression() const
|
||||
{
|
||||
return sign + std::to_string(bits) + "(" + inputValue->getRange() + ")";
|
||||
return sign + std::to_string(bits) + "(" + inputValue->getSymbolicExpression() + ")";
|
||||
}
|
||||
|
||||
bool ExprEngine::BinOpResult::isIntValueInRange(int value) const
|
||||
|
@ -500,6 +527,12 @@ ExprEngine::BinOpResult::IntOrFloatValue ExprEngine::BinOpResult::evaluate(int t
|
|||
BINARY_INT_OP(^)
|
||||
BINARY_INT_OP(<<)
|
||||
BINARY_INT_OP(>>)
|
||||
BINARY_INT_OP(==)
|
||||
BINARY_INT_OP(!=)
|
||||
BINARY_OP(>=)
|
||||
BINARY_OP(>)
|
||||
BINARY_OP(<=)
|
||||
BINARY_OP(<)
|
||||
|
||||
if (binop == "%" && rhs.intValue != 0) {
|
||||
struct ExprEngine::BinOpResult::IntOrFloatValue result;
|
||||
|
@ -531,7 +564,7 @@ ExprEngine::BinOpResult::IntOrFloatValue ExprEngine::BinOpResult::evaluateOperan
|
|||
result.setFloatValue(valueType ? floatRange->minValue : floatRange->maxValue);
|
||||
return result;
|
||||
}
|
||||
throw std::runtime_error("Internal error: Unhandled value:" + std::to_string((int)value->type()));
|
||||
throw std::runtime_error("Internal error: Unhandled value:" + std::to_string((int)value->type));
|
||||
}
|
||||
|
||||
// Todo: This is taken from ValueFlow and modified.. we should reuse it
|
||||
|
@ -670,7 +703,7 @@ static ExprEngine::ValuePtr executeAssign(const Token *tok, Data &data)
|
|||
// Is it array initialization?
|
||||
const Token *arrayInit = lhsToken->astOperand1();
|
||||
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);
|
||||
} else {
|
||||
auto indexValue = executeExpression(lhsToken->astOperand2(), data);
|
||||
|
@ -679,16 +712,16 @@ static ExprEngine::ValuePtr executeAssign(const Token *tok, Data &data)
|
|||
}
|
||||
} else if (lhsToken->isUnaryOp("*")) {
|
||||
auto pval = executeExpression(lhsToken->astOperand1(), data);
|
||||
if (pval && pval->type() == ExprEngine::ValueType::AddressOfValue) {
|
||||
if (pval && pval->type == ExprEngine::ValueType::AddressOfValue) {
|
||||
auto val = std::dynamic_pointer_cast<ExprEngine::AddressOfValue>(pval);
|
||||
if (val)
|
||||
data.memory[val->varId] = assignValue;
|
||||
} else if (pval && pval->type() == ExprEngine::ValueType::BinOpResult) {
|
||||
} else if (pval && pval->type == ExprEngine::ValueType::BinOpResult) {
|
||||
auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(pval);
|
||||
if (b && b->binop == "+") {
|
||||
std::shared_ptr<ExprEngine::ArrayValue> arr;
|
||||
ExprEngine::ValuePtr offset;
|
||||
if (b->op1->type() == ExprEngine::ValueType::ArrayValue) {
|
||||
if (b->op1->type == ExprEngine::ValueType::ArrayValue) {
|
||||
arr = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(b->op1);
|
||||
offset = b->op2;
|
||||
} else {
|
||||
|
@ -743,10 +776,10 @@ static ExprEngine::ValuePtr executeArrayIndex(const Token *tok, Data &data)
|
|||
auto arrayValue = data.getArrayValue(tok->astOperand1());
|
||||
if (arrayValue) {
|
||||
auto indexValue = executeExpression(tok->astOperand2(), data);
|
||||
auto values = arrayValue->read(indexValue);
|
||||
for (auto value: values)
|
||||
call(data.callbacks, tok, value);
|
||||
return values[0]; // FIXME we need to split the programstate here
|
||||
auto conditionalValues = arrayValue->read(indexValue);
|
||||
for (auto value: conditionalValues)
|
||||
call(data.callbacks, tok, value.second);
|
||||
return std::make_shared<ExprEngine::ConditionalValue>(data.getNewSymbolName(), conditionalValues);
|
||||
}
|
||||
return ExprEngine::ValuePtr();
|
||||
}
|
||||
|
|
|
@ -58,6 +58,7 @@ namespace ExprEngine {
|
|||
IntRange,
|
||||
FloatRange,
|
||||
PointerValue,
|
||||
ConditionalValue,
|
||||
ArrayValue,
|
||||
StringLiteralValue,
|
||||
StructValue,
|
||||
|
@ -71,40 +72,34 @@ namespace ExprEngine {
|
|||
|
||||
class Value {
|
||||
public:
|
||||
Value(const std::string &name) : name(name) {}
|
||||
Value(const std::string &name, const ValueType type) : name(name), type(type) {}
|
||||
virtual ~Value() {}
|
||||
virtual ValueType type() const = 0;
|
||||
virtual std::string getRange() const = 0;
|
||||
virtual std::string getRange() const {
|
||||
return name;
|
||||
}
|
||||
virtual std::string getSymbolicExpression() const {
|
||||
return name;
|
||||
}
|
||||
virtual bool isIntValueInRange(int value) const {
|
||||
(void)value;
|
||||
return false;
|
||||
}
|
||||
const std::string name;
|
||||
ValueType type;
|
||||
};
|
||||
|
||||
class UninitValue: public Value {
|
||||
public:
|
||||
UninitValue() : Value("?") {}
|
||||
ValueType type() const override {
|
||||
return ValueType::UninitValue;
|
||||
}
|
||||
std::string getRange() const override {
|
||||
return "?";
|
||||
}
|
||||
UninitValue() : Value("?", ValueType::UninitValue) {}
|
||||
};
|
||||
|
||||
class IntRange : public Value {
|
||||
public:
|
||||
IntRange(const std::string &name, int128_t minValue, int128_t maxValue)
|
||||
: Value(name)
|
||||
: Value(name, ValueType::IntRange)
|
||||
, minValue(minValue)
|
||||
, maxValue(maxValue) {
|
||||
}
|
||||
~IntRange() OVERRIDE {}
|
||||
|
||||
ValueType type() const override {
|
||||
return ValueType::IntRange;
|
||||
}
|
||||
std::string getRange() const override {
|
||||
if (minValue == maxValue)
|
||||
return str(minValue);
|
||||
|
@ -121,15 +116,11 @@ namespace ExprEngine {
|
|||
class FloatRange : public Value {
|
||||
public:
|
||||
FloatRange(const std::string &name, long double minValue, long double maxValue)
|
||||
: Value(name)
|
||||
: Value(name, ValueType::FloatRange)
|
||||
, minValue(minValue)
|
||||
, maxValue(maxValue) {
|
||||
}
|
||||
~FloatRange() OVERRIDE {}
|
||||
|
||||
ValueType type() const override {
|
||||
return ValueType::FloatRange;
|
||||
}
|
||||
std::string getRange() const override {
|
||||
return std::to_string(minValue) + ":" + std::to_string(maxValue);
|
||||
}
|
||||
|
@ -141,20 +132,28 @@ namespace ExprEngine {
|
|||
class PointerValue: public Value {
|
||||
public:
|
||||
PointerValue(const std::string &name, ValuePtr data, bool null, bool uninitData)
|
||||
: Value(name)
|
||||
: Value(name, ValueType::PointerValue)
|
||||
, data(data)
|
||||
, null(null)
|
||||
, uninitData(uninitData) {
|
||||
}
|
||||
ValueType type() const override {
|
||||
return ValueType::PointerValue;
|
||||
}
|
||||
std::string getRange() const override;
|
||||
ValuePtr data;
|
||||
bool null;
|
||||
bool uninitData;
|
||||
};
|
||||
|
||||
class ConditionalValue : public Value {
|
||||
public:
|
||||
typedef std::vector<std::pair<ValuePtr,ValuePtr>> Vector;
|
||||
|
||||
ConditionalValue(const std::string &name, const Vector &values) : Value(name, ValueType::ConditionalValue), values(values) {}
|
||||
|
||||
std::string getSymbolicExpression() const override;
|
||||
|
||||
Vector values;
|
||||
};
|
||||
|
||||
class ArrayValue: public Value {
|
||||
public:
|
||||
const int MAXSIZE = 0x100000;
|
||||
|
@ -162,14 +161,11 @@ namespace ExprEngine {
|
|||
ArrayValue(const std::string &name, ValuePtr size, ValuePtr value);
|
||||
ArrayValue(const std::string &name, const Variable *var);
|
||||
|
||||
ValueType type() const override {
|
||||
return ValueType::ArrayValue;
|
||||
}
|
||||
std::string getRange() const override;
|
||||
std::string getSymbolicExpression() const override;
|
||||
|
||||
void assign(ValuePtr index, ValuePtr value);
|
||||
void clear();
|
||||
std::vector<ExprEngine::ValuePtr> read(ValuePtr index);
|
||||
ConditionalValue::Vector read(ValuePtr index) const;
|
||||
|
||||
struct IndexAndValue {
|
||||
ValuePtr index;
|
||||
|
@ -181,14 +177,8 @@ namespace ExprEngine {
|
|||
|
||||
class StringLiteralValue: public Value {
|
||||
public:
|
||||
StringLiteralValue(const std::string &name, const std::string &s)
|
||||
: Value(name)
|
||||
, string(s) {
|
||||
}
|
||||
StringLiteralValue(const std::string &name, const std::string &s) : Value(name, ValueType::StringLiteralValue), string(s) {}
|
||||
|
||||
ValueType type() const override {
|
||||
return ValueType::StringLiteralValue;
|
||||
}
|
||||
std::string getRange() const override {
|
||||
return "\"" + string + "\"";
|
||||
}
|
||||
|
@ -201,13 +191,8 @@ namespace ExprEngine {
|
|||
|
||||
class StructValue: public Value {
|
||||
public:
|
||||
explicit StructValue(const std::string &name) : Value(name) {}
|
||||
ValueType type() const override {
|
||||
return ValueType::StructValue;
|
||||
}
|
||||
std::string getRange() const override {
|
||||
return name;
|
||||
}
|
||||
explicit StructValue(const std::string &name) : Value(name, ValueType::StructValue) {}
|
||||
|
||||
ValuePtr getValueOfMember(const std::string &name) const {
|
||||
auto it = member.find(name);
|
||||
return (it == member.end()) ? ValuePtr() : it->second;
|
||||
|
@ -218,15 +203,12 @@ namespace ExprEngine {
|
|||
class AddressOfValue: public Value {
|
||||
public:
|
||||
AddressOfValue(const std::string &name, int varId)
|
||||
: Value(name)
|
||||
: Value(name, ValueType::AddressOfValue)
|
||||
, varId(varId)
|
||||
{}
|
||||
|
||||
ValueType type() const override {
|
||||
return ValueType::AddressOfValue;
|
||||
}
|
||||
std::string getRange() const override {
|
||||
return "(&@" + std::to_string(varId);
|
||||
return "&@" + std::to_string(varId);
|
||||
}
|
||||
|
||||
int varId;
|
||||
|
@ -235,7 +217,7 @@ namespace ExprEngine {
|
|||
class BinOpResult : public Value {
|
||||
public:
|
||||
BinOpResult(const std::string &binop, ValuePtr op1, ValuePtr op2)
|
||||
: Value("(" + op1->name + ")" + binop + "(" + op2->name + ")")
|
||||
: Value("(" + op1->name + ")" + binop + "(" + op2->name + ")", ValueType::BinOpResult)
|
||||
, binop(binop)
|
||||
, op1(op1)
|
||||
, op2(op2) {
|
||||
|
@ -252,9 +234,6 @@ namespace ExprEngine {
|
|||
mLeafs.insert(op2);
|
||||
}
|
||||
|
||||
ValueType type() const override {
|
||||
return ValueType::BinOpResult;
|
||||
}
|
||||
std::string getRange() const override;
|
||||
|
||||
struct IntOrFloatValue {
|
||||
|
@ -292,16 +271,13 @@ namespace ExprEngine {
|
|||
class IntegerTruncation : public Value {
|
||||
public:
|
||||
IntegerTruncation(const std::string &name, ValuePtr inputValue, int bits, char sign)
|
||||
: Value(name)
|
||||
: Value(name, ValueType::IntegerTruncation)
|
||||
, inputValue(inputValue)
|
||||
, bits(bits)
|
||||
, sign(sign) {
|
||||
}
|
||||
|
||||
ValueType type() const override {
|
||||
return ValueType::IntegerTruncation;
|
||||
}
|
||||
std::string getRange() const override;
|
||||
std::string getSymbolicExpression() const override;
|
||||
|
||||
ExprEngine::ValuePtr inputValue;
|
||||
int bits;
|
||||
|
|
|
@ -63,6 +63,7 @@ private:
|
|||
|
||||
TEST_CASE(localArray1);
|
||||
TEST_CASE(localArray2);
|
||||
TEST_CASE(localArray3);
|
||||
TEST_CASE(localArrayInit1);
|
||||
TEST_CASE(localArrayInit2);
|
||||
TEST_CASE(localArrayUninit);
|
||||
|
@ -96,7 +97,7 @@ private:
|
|||
}
|
||||
|
||||
void argPointer() {
|
||||
ASSERT_EQUALS("->0:255,null,->?", getRange("void f(unsigned char *p) { a = *p; }", "p"));
|
||||
ASSERT_EQUALS("->$1,null,->?", getRange("void f(unsigned char *p) { a = *p; }", "p"));
|
||||
}
|
||||
|
||||
void argSmartPointer() {
|
||||
|
@ -113,7 +114,7 @@ private:
|
|||
}
|
||||
|
||||
void dynamicAllocation1() {
|
||||
ASSERT_EQUALS("size=1,[:]=0", getRange("char *f() { char *p = calloc(1,1); return p; }", "p"));
|
||||
ASSERT_EQUALS("$2", getRange("char *f() { char *p = calloc(1,1); return p; }", "p"));
|
||||
}
|
||||
|
||||
void expr1() {
|
||||
|
@ -203,6 +204,10 @@ private:
|
|||
ASSERT_EQUALS("0:255", getRange("int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4]; }", "arr[4]"));
|
||||
}
|
||||
|
||||
void localArray3() {
|
||||
ASSERT_EQUALS("?,43", getRange("int f(unsigned char x) { int arr[10]; arr[4] = 43; int vx = arr[x]; }", "arr[x]"));
|
||||
}
|
||||
|
||||
void localArrayInit1() {
|
||||
ASSERT_EQUALS("0", getRange("inf f() { char arr[10] = \"\"; return arr[4]; }", "arr[4]"));
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue