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

Revert "2" 

This reverts commit db386b2a7f.

That commit was half-done and not intended to be merged.
This commit is contained in:
Daniel Marjamäki 2020-12-06 22:29:46 +01:00
parent 8d9f0b3528
commit 7e9cbda2d5
1 changed files with 26 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

59
lib/exprengine.cpp
View File

@ -1029,16 +1029,10 @@ std::string ExprEngine::IntegerTruncation::getSymbolicExpression() const
#ifdef USE_Z3 #ifdef USE_Z3
class ExprData { struct ExprData {
public:
typedef std::map<std::string, z3::expr> ValueExpr; typedef std::map<std::string, z3::expr> ValueExpr;
typedef std::vector<z3::expr> AssertionList; typedef std::vector<z3::expr> AssertionList;
class BailoutValueException {
public:
BailoutValueException() {}
};
z3::context context; z3::context context;
ValueExpr valueExpr; ValueExpr valueExpr;
AssertionList assertionList; AssertionList assertionList;
@ -1048,15 +1042,6 @@ public:
solver.add(assertExpr); solver.add(assertExpr);
} }
void addConstraints(z3::solver &solver, const Data* data) {
for (auto constraint : data->constraints) {
try {
solver.add(getConstraintExpr(constraint));
} catch (const BailoutValueException &) {
}
}
}
z3::expr addInt(const std::string &name, int128_t minValue, int128_t maxValue) { z3::expr addInt(const std::string &name, int128_t minValue, int128_t maxValue) {
z3::expr e = context.int_const(name.c_str()); z3::expr e = context.int_const(name.c_str());
valueExpr.emplace(name, e); valueExpr.emplace(name, e);
@ -1123,8 +1108,6 @@ public:
z3::expr getExpr(ExprEngine::ValuePtr v) { z3::expr getExpr(ExprEngine::ValuePtr v) {
if (!v) if (!v)
throw ExprEngineException(nullptr, "Can not solve expressions, operand value is null"); throw ExprEngineException(nullptr, "Can not solve expressions, operand value is null");
if (v->type == ExprEngine::ValueType::BailoutValue)
throw BailoutValueException();
if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) { if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) {
if (intRange->name[0] != '$') if (intRange->name[0] != '$')
#if Z3_VERSION_INT >= GET_VERSION_INT(4,7,1) #if Z3_VERSION_INT >= GET_VERSION_INT(4,7,1)
@ -1179,6 +1162,7 @@ public:
} }
private: private:
z3::expr bool_expr(z3::expr e) { z3::expr bool_expr(z3::expr e) {
if (e.is_bool()) if (e.is_bool())
return e; return e;
@ -1207,7 +1191,8 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
try { try {
z3::expr e = exprData.addInt(name, minValue, maxValue); z3::expr e = exprData.addInt(name, minValue, maxValue);
exprData.addConstraints(solver, data); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
solver.add(e == value); solver.add(e == value);
return solver.check() == z3::sat; return solver.check() == z3::sat;
@ -1235,7 +1220,8 @@ bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
try { try {
z3::expr e = exprData.addInt(name, minValue, maxValue); z3::expr e = exprData.addInt(name, minValue, maxValue);
exprData.addConstraints(solver, data); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
solver.add(e > value); solver.add(e > value);
return solver.check() == z3::sat; return solver.check() == z3::sat;
@ -1263,7 +1249,8 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
try { try {
z3::expr e = exprData.addInt(name, minValue, maxValue); z3::expr e = exprData.addInt(name, minValue, maxValue);
exprData.addConstraints(solver, data); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
solver.add(e < value); solver.add(e < value);
return solver.check() == z3::sat; return solver.check() == z3::sat;
@ -1292,7 +1279,8 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
try { try {
z3::expr e = exprData.addFloat(name); z3::expr e = exprData.addFloat(name);
exprData.addConstraints(solver, data); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
solver.add(e >= value && e <= value); solver.add(e >= value && e <= value);
return solver.check() != z3::unsat; return solver.check() != z3::unsat;
@ -1322,7 +1310,8 @@ bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
try { try {
z3::expr e = exprData.addFloat(name); z3::expr e = exprData.addFloat(name);
exprData.addConstraints(solver, data); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
solver.add(e > value); solver.add(e > value);
return solver.check() == z3::sat; return solver.check() == z3::sat;
@ -1352,7 +1341,8 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
try { try {
z3::expr e = exprData.addFloat(name); z3::expr e = exprData.addFloat(name);
exprData.addConstraints(solver, data); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
solver.add(e < value); solver.add(e < value);
return solver.check() == z3::sat; return solver.check() == z3::sat;
@ -1373,7 +1363,8 @@ bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value)
ExprData exprData; ExprData exprData;
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
z3::expr e = exprData.getExpr(this); z3::expr e = exprData.getExpr(this);
exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase)); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
solver.add(e == value); solver.add(e == value);
return solver.check() == z3::sat; return solver.check() == z3::sat;
@ -1391,7 +1382,8 @@ bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int
ExprData exprData; ExprData exprData;
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
z3::expr e = exprData.getExpr(this); z3::expr e = exprData.getExpr(this);
exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase)); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
solver.add(e > value); solver.add(e > value);
return solver.check() == z3::sat; return solver.check() == z3::sat;
@ -1413,7 +1405,8 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val
ExprData exprData; ExprData exprData;
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
z3::expr e = exprData.getExpr(this); z3::expr e = exprData.getExpr(this);
exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase)); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
solver.add(e < value); solver.add(e < value);
return solver.check() == z3::sat; return solver.check() == z3::sat;
@ -1435,7 +1428,8 @@ bool ExprEngine::BinOpResult::isTrue(ExprEngine::DataBase *dataBase) const
ExprData exprData; ExprData exprData;
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
z3::expr e = exprData.getExpr(this); z3::expr e = exprData.getExpr(this);
exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase)); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
return solver.check() == z3::sat; return solver.check() == z3::sat;
} catch (const z3::exception &exception) { } catch (const z3::exception &exception) {
@ -1455,7 +1449,8 @@ std::string ExprEngine::BinOpResult::getExpr(ExprEngine::DataBase *dataBase) con
ExprData exprData; ExprData exprData;
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
z3::expr e = exprData.getExpr(this); z3::expr e = exprData.getExpr(this);
exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase)); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver); exprData.addAssertions(solver);
solver.add(e); solver.add(e);
std::ostringstream os; std::ostringstream os;
@ -1772,11 +1767,7 @@ static void checkContract(Data &data, const Token *tok, const Function *function
z3::solver solver(exprData.context); z3::solver solver(exprData.context);
try { try {
// Invert contract, we want to know if the contract might not be met // Invert contract, we want to know if the contract might not be met
try {
solver.add(z3::ite(exprData.getConstraintExpr(data.executeContract(function, executeExpression1)), exprData.context.bool_val(false), exprData.context.bool_val(true))); solver.add(z3::ite(exprData.getConstraintExpr(data.executeContract(function, executeExpression1)), exprData.context.bool_val(false), exprData.context.bool_val(true)));
} catch (const ExprData::BailoutValueException &) {
throw ExprEngineException(tok, "Internal error: Bailout value used");
}
bool bailoutValue = false; bool bailoutValue = false;
for (nonneg int i = 0; i < argValues.size(); ++i) { for (nonneg int i = 0; i < argValues.size(); ++i) {
@ -1823,7 +1814,7 @@ static void checkContract(Data &data, const Token *tok, const Function *function
} }
} catch (const z3::exception &exception) { } catch (const z3::exception &exception) {
std::cerr << "z3: " << exception << std::endl; std::cerr << "z3: " << exception << std::endl;
} catch (const ExprEngineException &) { } catch (const ExprEngineException &e) {
const char id[] = "internalErrorInExprEngine"; const char id[] = "internalErrorInExprEngine";
const auto contractIt = data.settings->functionContracts.find(function->fullName()); const auto contractIt = data.settings->functionContracts.find(function->fullName());
const std::string functionName = contractIt->first; const std::string functionName = contractIt->first;