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

ExprEngine: Add condition branches for the while loops (#2970)

This commit is contained in:
Georgy Komarov 2020-12-22 22:21:57 +03:00 committed by GitHub
parent a9e7974963
commit 259f562e73
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 204 additions and 143 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

137
lib/exprengine.cpp
View File

@ -141,6 +141,7 @@
#include <limits>
#include <memory>
#include <iostream>
#include <tuple>
#ifdef USE_Z3
#include <z3++.h>
#include <z3_version.h>
@ -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<Data *>(dataBase);
const Data *data = dynamic_cast<const Data *>(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<Data *>(dataBase);
const Data *data = dynamic_cast<const Data *>(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<Data *>(dataBase);
const Data *data = dynamic_cast<const Data *>(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<Data *>(dataBase);
const Data *data = dynamic_cast<const Data *>(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<Data *>(dataBase);
const Data *data = dynamic_cast<const Data *>(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<Data *>(dataBase);
const Data *data = dynamic_cast<const Data *>(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<bool, bool> checkConditionBranches(const ExprEngine::ValuePtr &condValue, const Data &data) {
bool canBeFalse = true;
bool canBeTrue = true;
if (auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(condValue)) {
canBeFalse = b->isEqual(&data, 0);
canBeTrue = b->isTrue(&data);
} else if (auto i = std::dynamic_pointer_cast<ExprEngine::IntRange>(condValue)) {
canBeFalse = i->isEqual(&data, 0);
canBeTrue = ExprEngine::BinOpResult("!=", i, std::make_shared<ExprEngine::IntRange>("0", 0, 0)).isTrue(&data);
} else if (std::dynamic_pointer_cast<ExprEngine::StringLiteralValue>(condValue)) {
canBeFalse = false;
canBeTrue = true;
} else if (auto f = std::dynamic_pointer_cast<ExprEngine::FloatRange>(condValue)) {
canBeFalse = f->isEqual(&data, 0);
canBeTrue = ExprEngine::BinOpResult("!=", f, std::make_shared<ExprEngine::FloatRange>("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<ExprEngine::BinOpResult>(condValue)) {
canBeFalse = b->isEqual(&data, 0);
canBeTrue = b->isTrue(&data);
} else if (auto i = std::dynamic_pointer_cast<ExprEngine::IntRange>(condValue)) {
canBeFalse = i->isEqual(&data, 0);
canBeTrue = ExprEngine::BinOpResult("!=", i, std::make_shared<ExprEngine::IntRange>("0", 0, 0)).isTrue(&data);
} else if (std::dynamic_pointer_cast<ExprEngine::StringLiteralValue>(condValue)) {
canBeFalse = false;
canBeTrue = true;
} else if (auto f = std::dynamic_pointer_cast<ExprEngine::FloatRange>(condValue)) {
canBeFalse = f->isEqual(&data, 0);
canBeTrue = ExprEngine::BinOpResult("!=", f, std::make_shared<ExprEngine::FloatRange>("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,10 +2679,26 @@ 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
if (canBeTrue) {
std::set<int> changedVariables;
for (const Token *tok2 = tok; tok2 != bodyEnd; tok2 = tok2->next()) {
if (Token::Match(tok2, "%assign%")) {
@ -2689,7 +2712,7 @@ static std::string execute(const Token *start, const Token *end, Data &data)
while (Token::Match(structToken, ".|["))
structToken = structToken->astOperand1();
if (Token::Match(structToken, "%var%")) {
data.assignValue(structToken, structToken->varId(), std::make_shared<ExprEngine::BailoutValue>());
bodyData.assignValue(structToken, structToken->varId(), std::make_shared<ExprEngine::BailoutValue>());
changedVariables.insert(structToken->varId());
continue;
}
@ -2705,16 +2728,16 @@ static std::string execute(const Token *start, const Token *end, Data &data)
ExprEngine::ValuePtr memberValue;
for (const Variable &member : structScope->varlist) {
if (memberName == member.name() && member.valueType()) {
memberValue = createVariableValue(member, data);
memberValue = createVariableValue(member, bodyData);
break;
}
}
if (!memberValue)
throw ExprEngineException(tok2, "Unhandled assignment in loop");
ExprEngine::ValuePtr structVal1 = data.getValue(structToken->varId(), structToken->valueType(), structToken);
ExprEngine::ValuePtr structVal1 = bodyData.getValue(structToken->varId(), structToken->valueType(), structToken);
if (!structVal1)
structVal1 = createVariableValue(*structToken->variable(), data);
structVal1 = createVariableValue(*structToken->variable(), bodyData);
auto structVal = std::dynamic_pointer_cast<ExprEngine::StructValue>(structVal1);
if (!structVal) {
// Handle pointer to a struct
@ -2730,12 +2753,12 @@ static std::string execute(const Token *start, const Token *end, Data &data)
throw ExprEngineException(tok2, "Unhandled assignment in loop");
}
data.assignStructMember(tok2, &*structVal, memberName, memberValue);
bodyData.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);
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<ExprEngine::ArrayValue>(val);
@ -2750,16 +2773,16 @@ static std::string execute(const Token *start, const Token *end, Data &data)
if (changedVariables.find(varid) != changedVariables.end())
continue;
changedVariables.insert(varid);
auto oldValue = data.getValue(varid, nullptr, nullptr);
auto oldValue = bodyData.getValue(varid, nullptr, nullptr);
if (oldValue && oldValue->isUninit())
call(data.callbacks, lhs, oldValue, &data);
call(bodyData.callbacks, lhs, oldValue, &bodyData);
if (oldValue && oldValue->type == ExprEngine::ValueType::ArrayValue) {
// Try to assign "any" value
auto arrayValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(oldValue);
arrayValue->assign(std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 0, ~0ULL), std::make_shared<ExprEngine::BailoutValue>());
arrayValue->assign(std::make_shared<ExprEngine::IntRange>(bodyData.getNewSymbolName(), 0, ~0ULL), std::make_shared<ExprEngine::BailoutValue>());
continue;
}
data.assignValue(tok2, varid, getValueRangeFromValueType(lhs->valueType(), data));
bodyData.assignValue(tok2, varid, getValueRangeFromValueType(lhs->valueType(), bodyData));
continue;
} else if (Token::Match(tok2, "++|--") && tok2->astOperand1() && tok2->astOperand1()->variable()) {
// give variable "any" value
@ -2768,13 +2791,37 @@ static std::string execute(const Token *start, const Token *end, Data &data)
if (changedVariables.find(varid) != changedVariables.end())
continue;
changedVariables.insert(varid);
auto oldValue = data.getValue(varid, nullptr, nullptr);
auto oldValue = bodyData.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));
call(bodyData.callbacks, tok2, oldValue, &bodyData);
bodyData.assignValue(tok2, varid, getValueRangeFromValueType(vartok->valueType(), bodyData));
}
}
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 {"))

30
lib/exprengine.h
View File

@ -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 {

30
test/testexprengine.cpp
View File

@ -668,10 +668,14 @@ private:
" x = x + 34;\n"
" x == 340;\n"
"}";
ASSERT_EQUALS("(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n"
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",
expr(code, "=="));
"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"
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",
expr(code, "=="));
"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() {