From 259f562e731beb1fdb6cb9813cb9720423520a13 Mon Sep 17 00:00:00 2001 From: Georgy Komarov Date: Tue, 22 Dec 2020 22:21:57 +0300 Subject: [PATCH] ExprEngine: Add condition branches for the while loops (#2970) --- lib/exprengine.cpp | 283 +++++++++++++++++++++++----------------- lib/exprengine.h | 30 ++--- test/testexprengine.cpp | 34 +++-- 3 files changed, 204 insertions(+), 143 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index a32def59c..5a0d47810 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -141,6 +141,7 @@ #include #include #include +#include #ifdef USE_Z3 #include #include @@ -1309,12 +1310,12 @@ public: }; #endif -bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const +bool ExprEngine::IntRange::isEqual(const DataBase *dataBase, int value) const { if (value < minValue || value > maxValue) return false; - const Data *data = dynamic_cast(dataBase); + const Data *data = dynamic_cast(dataBase); if (data->constraints.empty()) return true; #ifdef USE_Z3 @@ -1341,12 +1342,12 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const #endif } -bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const +bool ExprEngine::IntRange::isGreaterThan(const DataBase *dataBase, int value) const { if (maxValue <= value) return false; - const Data *data = dynamic_cast(dataBase); + const Data *data = dynamic_cast(dataBase); if (data->constraints.empty()) return true; #ifdef USE_Z3 @@ -1373,12 +1374,12 @@ bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const #endif } -bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const +bool ExprEngine::IntRange::isLessThan(const DataBase *dataBase, int value) const { if (minValue >= value) return false; - const Data *data = dynamic_cast(dataBase); + const Data *data = dynamic_cast(dataBase); if (data->constraints.empty()) return true; #ifdef USE_Z3 @@ -1405,13 +1406,13 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const #endif } -bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const +bool ExprEngine::FloatRange::isEqual(const DataBase *dataBase, int value) const { if (MathLib::isFloat(name)) { float f = MathLib::toDoubleNumber(name); return value >= f - 0.00001 && value <= f + 0.00001; } - const Data *data = dynamic_cast(dataBase); + const Data *data = dynamic_cast(dataBase); if (data->constraints.empty()) return true; #ifdef USE_Z3 @@ -1444,12 +1445,12 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const #endif } -bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const +bool ExprEngine::FloatRange::isGreaterThan(const DataBase *dataBase, int value) const { if (value < minValue || value > maxValue) return false; - const Data *data = dynamic_cast(dataBase); + const Data *data = dynamic_cast(dataBase); if (data->constraints.empty()) return true; if (MathLib::isFloat(name)) @@ -1478,12 +1479,12 @@ bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const #endif } -bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const +bool ExprEngine::FloatRange::isLessThan(const DataBase *dataBase, int value) const { if (value < minValue || value > maxValue) return false; - const Data *data = dynamic_cast(dataBase); + const Data *data = dynamic_cast(dataBase); if (data->constraints.empty()) return true; if (MathLib::isFloat(name)) @@ -1513,7 +1514,7 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const } -bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value) const +bool ExprEngine::BinOpResult::isEqual(const ExprEngine::DataBase *dataBase, int value) const { #ifdef USE_Z3 try { @@ -1539,7 +1540,7 @@ bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value) #endif } -bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int value) const +bool ExprEngine::BinOpResult::isGreaterThan(const ExprEngine::DataBase *dataBase, int value) const { #ifdef USE_Z3 try { @@ -1565,7 +1566,7 @@ bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int #endif } -bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int value) const +bool ExprEngine::BinOpResult::isLessThan(const ExprEngine::DataBase *dataBase, int value) const { #ifdef USE_Z3 try { @@ -1591,7 +1592,7 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val #endif } -bool ExprEngine::BinOpResult::isTrue(ExprEngine::DataBase *dataBase) const +bool ExprEngine::BinOpResult::isTrue(const ExprEngine::DataBase *dataBase) const { #ifdef USE_Z3 try { @@ -2460,6 +2461,25 @@ static ExprEngine::ValuePtr executeExpression(const Token *tok, Data &data) static ExprEngine::ValuePtr createVariableValue(const Variable &var, Data &data); +static std::tuple checkConditionBranches(const ExprEngine::ValuePtr &condValue, const Data &data) { + bool canBeFalse = true; + bool canBeTrue = true; + if (auto b = std::dynamic_pointer_cast(condValue)) { + canBeFalse = b->isEqual(&data, 0); + canBeTrue = b->isTrue(&data); + } else if (auto i = std::dynamic_pointer_cast(condValue)) { + canBeFalse = i->isEqual(&data, 0); + canBeTrue = ExprEngine::BinOpResult("!=", i, std::make_shared("0", 0, 0)).isTrue(&data); + } else if (std::dynamic_pointer_cast(condValue)) { + canBeFalse = false; + canBeTrue = true; + } else if (auto f = std::dynamic_pointer_cast(condValue)) { + canBeFalse = f->isEqual(&data, 0); + canBeTrue = ExprEngine::BinOpResult("!=", f, std::make_shared("0.0", 0.0, 0.0)).isTrue(&data); + } + return std::make_tuple(canBeFalse, canBeTrue); +} + static std::string execute(const Token *start, const Token *end, Data &data) { if (data.recursion > 20) @@ -2550,21 +2570,8 @@ static std::string execute(const Token *start, const Token *end, Data &data) const Token *cond = tok->next()->astOperand2(); // TODO: C++17 condition const ExprEngine::ValuePtr condValue = executeExpression(cond, data); - bool canBeFalse = true; - bool canBeTrue = true; - if (auto b = std::dynamic_pointer_cast(condValue)) { - canBeFalse = b->isEqual(&data, 0); - canBeTrue = b->isTrue(&data); - } else if (auto i = std::dynamic_pointer_cast(condValue)) { - canBeFalse = i->isEqual(&data, 0); - canBeTrue = ExprEngine::BinOpResult("!=", i, std::make_shared("0", 0, 0)).isTrue(&data); - } else if (std::dynamic_pointer_cast(condValue)) { - canBeFalse = false; - canBeTrue = true; - } else if (auto f = std::dynamic_pointer_cast(condValue)) { - canBeFalse = f->isEqual(&data, 0); - canBeTrue = ExprEngine::BinOpResult("!=", f, std::make_shared("0.0", 0.0, 0.0)).isTrue(&data); - } + bool canBeFalse, canBeTrue; + std::tie(canBeFalse, canBeTrue) = checkConditionBranches(condValue, data); Data &thenData(data); Data elseData(data); @@ -2672,109 +2679,149 @@ static std::string execute(const Token *start, const Token *end, Data &data) } if (Token::Match(tok, "for|while (") && Token::simpleMatch(tok->linkAt(1), ") {")) { + const Token *cond = tok->next()->astOperand2(); + const ExprEngine::ValuePtr condValue = executeExpression(cond, data); + + bool canBeFalse = false, canBeTrue = true; + if (tok->str() == "while") + std::tie(canBeFalse, canBeTrue) = checkConditionBranches(condValue, data); + + Data &bodyData(data); + Data noexecData(data); + if (canBeFalse && canBeTrue) { // Avoid that constraints are overspecified + bodyData.addConstraint(condValue, true); + } + + Data::ifSplit(tok, bodyData, noexecData); + const Token *bodyStart = tok->linkAt(1)->next(); const Token *bodyEnd = bodyStart->link(); // TODO this is very rough code - std::set changedVariables; - for (const Token *tok2 = tok; tok2 != bodyEnd; tok2 = tok2->next()) { - if (Token::Match(tok2, "%assign%")) { - const Token *lhs = tok2->astOperand1(); - while (Token::simpleMatch(lhs, "[")) - lhs = lhs->astOperand1(); - if (!lhs) - throw ExprEngineException(tok2, "Unhandled assignment in loop"); - if (Token::Match(lhs, ". %name% =|[") && Token::simpleMatch(lhs->astOperand1(), ".")) { - const Token *structToken = lhs; - while (Token::Match(structToken, ".|[")) - structToken = structToken->astOperand1(); - if (Token::Match(structToken, "%var%")) { - data.assignValue(structToken, structToken->varId(), std::make_shared()); - changedVariables.insert(structToken->varId()); - continue; - } - } - if (Token::Match(lhs, ". %name% =|[") && lhs->astOperand1() && lhs->astOperand1()->valueType()) { - const Token *structToken = lhs->astOperand1(); - if (!structToken->valueType() || !structToken->varId()) + if (canBeTrue) { + std::set changedVariables; + for (const Token *tok2 = tok; tok2 != bodyEnd; tok2 = tok2->next()) { + if (Token::Match(tok2, "%assign%")) { + const Token *lhs = tok2->astOperand1(); + while (Token::simpleMatch(lhs, "[")) + lhs = lhs->astOperand1(); + if (!lhs) throw ExprEngineException(tok2, "Unhandled assignment in loop"); - const Scope *structScope = structToken->valueType()->typeScope; - if (!structScope) - throw ExprEngineException(tok2, "Unhandled assignment in loop"); - const std::string &memberName = tok2->previous()->str(); - ExprEngine::ValuePtr memberValue; - for (const Variable &member : structScope->varlist) { - if (memberName == member.name() && member.valueType()) { - memberValue = createVariableValue(member, data); - break; + if (Token::Match(lhs, ". %name% =|[") && Token::simpleMatch(lhs->astOperand1(), ".")) { + const Token *structToken = lhs; + while (Token::Match(structToken, ".|[")) + structToken = structToken->astOperand1(); + if (Token::Match(structToken, "%var%")) { + bodyData.assignValue(structToken, structToken->varId(), std::make_shared()); + changedVariables.insert(structToken->varId()); + continue; } } - if (!memberValue) - throw ExprEngineException(tok2, "Unhandled assignment in loop"); - - ExprEngine::ValuePtr structVal1 = data.getValue(structToken->varId(), structToken->valueType(), structToken); - if (!structVal1) - structVal1 = createVariableValue(*structToken->variable(), data); - auto structVal = std::dynamic_pointer_cast(structVal1); - if (!structVal) { - // Handle pointer to a struct - if (auto structPtr = std::dynamic_pointer_cast(structVal1)) { - if (structPtr->pointer && !structPtr->data.empty()) { - auto indexValue = std::make_shared("0", 0, 0); - for (auto val: structPtr->read(indexValue)) { - structVal = std::dynamic_pointer_cast(val.second); - } + if (Token::Match(lhs, ". %name% =|[") && lhs->astOperand1() && lhs->astOperand1()->valueType()) { + const Token *structToken = lhs->astOperand1(); + if (!structToken->valueType() || !structToken->varId()) + throw ExprEngineException(tok2, "Unhandled assignment in loop"); + const Scope *structScope = structToken->valueType()->typeScope; + if (!structScope) + throw ExprEngineException(tok2, "Unhandled assignment in loop"); + const std::string &memberName = tok2->previous()->str(); + ExprEngine::ValuePtr memberValue; + for (const Variable &member : structScope->varlist) { + if (memberName == member.name() && member.valueType()) { + memberValue = createVariableValue(member, bodyData); + break; } } - if (!structVal) + if (!memberValue) throw ExprEngineException(tok2, "Unhandled assignment in loop"); - } - data.assignStructMember(tok2, &*structVal, memberName, memberValue); - continue; - } - if (lhs->isUnaryOp("*") && lhs->astOperand1()->varId()) { - const Token *varToken = tok2->astOperand1()->astOperand1(); - 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(val); - arrayValue->assign(std::make_shared("0", 0, 0), std::make_shared()); + ExprEngine::ValuePtr structVal1 = bodyData.getValue(structToken->varId(), structToken->valueType(), structToken); + if (!structVal1) + structVal1 = createVariableValue(*structToken->variable(), bodyData); + auto structVal = std::dynamic_pointer_cast(structVal1); + if (!structVal) { + // Handle pointer to a struct + if (auto structPtr = std::dynamic_pointer_cast(structVal1)) { + if (structPtr->pointer && !structPtr->data.empty()) { + auto indexValue = std::make_shared("0", 0, 0); + for (auto val: structPtr->read(indexValue)) { + structVal = std::dynamic_pointer_cast(val.second); + } + } + } + if (!structVal) + throw ExprEngineException(tok2, "Unhandled assignment in loop"); + } + + bodyData.assignStructMember(tok2, &*structVal, memberName, memberValue); continue; } + if (lhs->isUnaryOp("*") && lhs->astOperand1()->varId()) { + const Token *varToken = tok2->astOperand1()->astOperand1(); + ExprEngine::ValuePtr val = bodyData.getValue(varToken->varId(), varToken->valueType(), varToken); + if (val && val->type == ExprEngine::ValueType::ArrayValue) { + // Try to assign "any" value + auto arrayValue = std::dynamic_pointer_cast(val); + arrayValue->assign(std::make_shared("0", 0, 0), std::make_shared()); + continue; + } + } + if (!lhs->variable()) + throw ExprEngineException(tok2, "Unhandled assignment in loop"); + // give variable "any" value + int varid = lhs->varId(); + if (changedVariables.find(varid) != changedVariables.end()) + continue; + changedVariables.insert(varid); + auto oldValue = bodyData.getValue(varid, nullptr, nullptr); + if (oldValue && oldValue->isUninit()) + call(bodyData.callbacks, lhs, oldValue, &bodyData); + if (oldValue && oldValue->type == ExprEngine::ValueType::ArrayValue) { + // Try to assign "any" value + auto arrayValue = std::dynamic_pointer_cast(oldValue); + arrayValue->assign(std::make_shared(bodyData.getNewSymbolName(), 0, ~0ULL), std::make_shared()); + continue; + } + bodyData.assignValue(tok2, varid, getValueRangeFromValueType(lhs->valueType(), bodyData)); + continue; + } else if (Token::Match(tok2, "++|--") && tok2->astOperand1() && tok2->astOperand1()->variable()) { + // give variable "any" value + const Token *vartok = tok2->astOperand1(); + int varid = vartok->varId(); + if (changedVariables.find(varid) != changedVariables.end()) + continue; + changedVariables.insert(varid); + auto oldValue = bodyData.getValue(varid, nullptr, nullptr); + if (oldValue && oldValue->type == ExprEngine::ValueType::UninitValue) + call(bodyData.callbacks, tok2, oldValue, &bodyData); + bodyData.assignValue(tok2, varid, getValueRangeFromValueType(vartok->valueType(), bodyData)); } - if (!lhs->variable()) - throw ExprEngineException(tok2, "Unhandled assignment in loop"); - // give variable "any" value - int varid = lhs->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, lhs, oldValue, &data); - if (oldValue && oldValue->type == ExprEngine::ValueType::ArrayValue) { - // Try to assign "any" value - auto arrayValue = std::dynamic_pointer_cast(oldValue); - arrayValue->assign(std::make_shared(data.getNewSymbolName(), 0, ~0ULL), std::make_shared()); - continue; - } - data.assignValue(tok2, varid, getValueRangeFromValueType(lhs->valueType(), data)); - continue; - } else if (Token::Match(tok2, "++|--") && tok2->astOperand1() && tok2->astOperand1()->variable()) { - // give variable "any" value - const Token *vartok = tok2->astOperand1(); - int varid = vartok->varId(); - if (changedVariables.find(varid) != changedVariables.end()) - continue; - changedVariables.insert(varid); - auto oldValue = data.getValue(varid, nullptr, nullptr); - if (oldValue && oldValue->type == ExprEngine::ValueType::UninitValue) - call(data.callbacks, tok2, oldValue, &data); - data.assignValue(tok2, varid, getValueRangeFromValueType(vartok->valueType(), data)); } } - tok = tok->linkAt(1); + + const Token *exceptionToken = nullptr; + std::string exceptionMessage; + auto exec = [&](const Token *tok1, const Token *tok2, Data& data) { + try { + execute(tok1, tok2, data); + } catch (ExprEngineException &e) { + if (!exceptionToken || (e.tok && precedes(e.tok, exceptionToken))) { + exceptionToken = e.tok; + exceptionMessage = e.what; + } + } + }; + + if (canBeTrue) + exec(bodyStart->next(), end, bodyData); + if (canBeFalse) + exec(bodyEnd, end, noexecData); + + if (exceptionToken) + throw ExprEngineException(exceptionToken, exceptionMessage); + + return (canBeTrue ? bodyData.str() : std::string()) + + (canBeFalse ? noexecData.str() : std::string()); } if (Token::simpleMatch(tok, "} else {")) diff --git a/lib/exprengine.h b/lib/exprengine.h index 9151cc2af..305f0392d 100644 --- a/lib/exprengine.h +++ b/lib/exprengine.h @@ -103,17 +103,17 @@ namespace ExprEngine { virtual std::string getSymbolicExpression() const { return name; } - virtual bool isEqual(DataBase *dataBase, int value) const { + virtual bool isEqual(const DataBase *dataBase, int value) const { (void)dataBase; (void)value; return false; } - virtual bool isGreaterThan(DataBase *dataBase, int value) const { + virtual bool isGreaterThan(const DataBase *dataBase, int value) const { (void)dataBase; (void)value; return false; } - virtual bool isLessThan(DataBase *dataBase, int value) const { + virtual bool isLessThan(const DataBase *dataBase, int value) const { (void)dataBase; (void)value; return false; @@ -129,7 +129,7 @@ namespace ExprEngine { class UninitValue: public Value { public: UninitValue() : Value("?", ValueType::UninitValue) {} - bool isEqual(DataBase *dataBase, int value) const OVERRIDE { + bool isEqual(const DataBase *dataBase, int value) const OVERRIDE { (void)dataBase; (void)value; return true; @@ -152,9 +152,9 @@ namespace ExprEngine { return str(minValue); return str(minValue) + ":" + str(maxValue); } - bool isEqual(DataBase *dataBase, int value) const OVERRIDE; - bool isGreaterThan(DataBase *dataBase, int value) const OVERRIDE; - bool isLessThan(DataBase *dataBase, int value) const OVERRIDE; + bool isEqual(const DataBase *dataBase, int value) const OVERRIDE; + bool isGreaterThan(const DataBase *dataBase, int value) const OVERRIDE; + bool isLessThan(const DataBase *dataBase, int value) const OVERRIDE; int128_t minValue; int128_t maxValue; @@ -173,9 +173,9 @@ namespace ExprEngine { return std::to_string(minValue) + ":" + std::to_string(maxValue); } - bool isEqual(DataBase *dataBase, int value) const OVERRIDE; - bool isGreaterThan(DataBase *dataBase, int value) const OVERRIDE; - bool isLessThan(DataBase *dataBase, int value) const OVERRIDE; + bool isEqual(const DataBase *dataBase, int value) const OVERRIDE; + bool isGreaterThan(const DataBase *dataBase, int value) const OVERRIDE; + bool isLessThan(const DataBase *dataBase, int value) const OVERRIDE; long double minValue; long double maxValue; @@ -283,10 +283,10 @@ namespace ExprEngine { , op2(op2) { } - bool isEqual(DataBase *dataBase, int value) const OVERRIDE; - bool isGreaterThan(DataBase *dataBase, int value) const OVERRIDE; - virtual bool isLessThan(DataBase *dataBase, int value) const OVERRIDE; - bool isTrue(DataBase *dataBase) const; + bool isEqual(const DataBase *dataBase, int value) const OVERRIDE; + bool isGreaterThan(const DataBase *dataBase, int value) const OVERRIDE; + virtual bool isLessThan(const DataBase *dataBase, int value) const OVERRIDE; + bool isTrue(const DataBase *dataBase) const; std::string getExpr(DataBase *dataBase) const; @@ -330,7 +330,7 @@ namespace ExprEngine { class BailoutValue : public Value { public: BailoutValue() : Value("bailout", ValueType::BailoutValue) {} - bool isEqual(DataBase * /*dataBase*/, int /*value*/) const OVERRIDE { + bool isEqual(const DataBase * /*dataBase*/, int /*value*/) const OVERRIDE { return true; } bool isUninit() const OVERRIDE { diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index f204fce03..daabd2bf9 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -668,10 +668,14 @@ private: " x = x + 34;\n" " x == 340;\n" "}"; - ASSERT_EQUALS("(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n" - "(= (+ $2 34) 340)\n" - "z3::sat\n", - expr(code, "==")); + const char expected[] = "(< 0 $1)\n" + "(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n" + "(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n" + "(= (+ $2 34) 340)\n" + "z3::sat\n" + "(= 0 340)\n" + "z3::unsat\n"; + ASSERT_EQUALS(expected, expr(code, "==")); } void while2() { @@ -681,10 +685,14 @@ private: " x++;\n" " x == 1;\n" "}"; - ASSERT_EQUALS("(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n" - "(= (+ $2 1) 1)\n" - "z3::sat\n", - expr(code, "==")); + const char expected[] = "(< 0 $1)\n" + "(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n" + "(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n" + "(= (+ $2 1) 1)\n" + "z3::sat\n" + "(= 0 1)\n" + "z3::unsat\n"; + ASSERT_EQUALS(expected, expr(code, "==")); } void while3() { @@ -706,8 +714,14 @@ private: " *len = 0;\n" " *len == 0;\n" "}"; - ASSERT_EQUALS("(= 0 0)\n" - "z3::sat\n", expr(code, "==")); + const char expected[] = "(distinct |$2:0| 0)\n" + "(and (>= |$2:0| (- 128)) (<= |$2:0| 127))\n" + "(= 0 0)\n" + "z3::sat\n" + "(and (>= $8 (- 2147483648)) (<= $8 2147483647))\n" + "(= $8 0)\n" + "z3::sat\n"; + ASSERT_EQUALS(expected, expr(code, "==")); } void while5() {