From 7e9cbda2d5398aee567f2c4d492a39bcf71a07c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Sun, 6 Dec 2020 22:29:46 +0100 Subject: [PATCH] Revert "2" This reverts commit db386b2a7fba2eecb313bae3f65784bea0ecac9b. That commit was half-done and not intended to be merged. --- lib/exprengine.cpp | 61 ++++++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 35 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 93ef209f9..b5f18fbee 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -1029,16 +1029,10 @@ std::string ExprEngine::IntegerTruncation::getSymbolicExpression() const #ifdef USE_Z3 -class ExprData { -public: +struct ExprData { typedef std::map ValueExpr; typedef std::vector AssertionList; - class BailoutValueException { - public: - BailoutValueException() {} - }; - z3::context context; ValueExpr valueExpr; AssertionList assertionList; @@ -1048,15 +1042,6 @@ public: 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 e = context.int_const(name.c_str()); valueExpr.emplace(name, e); @@ -1123,8 +1108,6 @@ public: z3::expr getExpr(ExprEngine::ValuePtr v) { if (!v) 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(v)) { if (intRange->name[0] != '$') #if Z3_VERSION_INT >= GET_VERSION_INT(4,7,1) @@ -1179,6 +1162,7 @@ public: } private: + z3::expr bool_expr(z3::expr e) { if (e.is_bool()) return e; @@ -1207,7 +1191,8 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addInt(name, minValue, maxValue); - exprData.addConstraints(solver, data); + for (auto constraint : dynamic_cast(dataBase)->constraints) + solver.add(exprData.getConstraintExpr(constraint)); exprData.addAssertions(solver); solver.add(e == value); return solver.check() == z3::sat; @@ -1235,7 +1220,8 @@ bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addInt(name, minValue, maxValue); - exprData.addConstraints(solver, data); + for (auto constraint : dynamic_cast(dataBase)->constraints) + solver.add(exprData.getConstraintExpr(constraint)); exprData.addAssertions(solver); solver.add(e > value); return solver.check() == z3::sat; @@ -1263,7 +1249,8 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addInt(name, minValue, maxValue); - exprData.addConstraints(solver, data); + for (auto constraint : dynamic_cast(dataBase)->constraints) + solver.add(exprData.getConstraintExpr(constraint)); exprData.addAssertions(solver); solver.add(e < value); return solver.check() == z3::sat; @@ -1292,7 +1279,8 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addFloat(name); - exprData.addConstraints(solver, data); + for (auto constraint : dynamic_cast(dataBase)->constraints) + solver.add(exprData.getConstraintExpr(constraint)); exprData.addAssertions(solver); solver.add(e >= value && e <= value); return solver.check() != z3::unsat; @@ -1322,7 +1310,8 @@ bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addFloat(name); - exprData.addConstraints(solver, data); + for (auto constraint : dynamic_cast(dataBase)->constraints) + solver.add(exprData.getConstraintExpr(constraint)); exprData.addAssertions(solver); solver.add(e > value); return solver.check() == z3::sat; @@ -1352,7 +1341,8 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addFloat(name); - exprData.addConstraints(solver, data); + for (auto constraint : dynamic_cast(dataBase)->constraints) + solver.add(exprData.getConstraintExpr(constraint)); exprData.addAssertions(solver); solver.add(e < value); return solver.check() == z3::sat; @@ -1373,7 +1363,8 @@ bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value) ExprData exprData; z3::solver solver(exprData.context); z3::expr e = exprData.getExpr(this); - exprData.addConstraints(solver, dynamic_cast(dataBase)); + for (auto constraint : dynamic_cast(dataBase)->constraints) + solver.add(exprData.getConstraintExpr(constraint)); exprData.addAssertions(solver); solver.add(e == value); return solver.check() == z3::sat; @@ -1391,7 +1382,8 @@ bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int ExprData exprData; z3::solver solver(exprData.context); z3::expr e = exprData.getExpr(this); - exprData.addConstraints(solver, dynamic_cast(dataBase)); + for (auto constraint : dynamic_cast(dataBase)->constraints) + solver.add(exprData.getConstraintExpr(constraint)); exprData.addAssertions(solver); solver.add(e > value); return solver.check() == z3::sat; @@ -1413,7 +1405,8 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val ExprData exprData; z3::solver solver(exprData.context); z3::expr e = exprData.getExpr(this); - exprData.addConstraints(solver, dynamic_cast(dataBase)); + for (auto constraint : dynamic_cast(dataBase)->constraints) + solver.add(exprData.getConstraintExpr(constraint)); exprData.addAssertions(solver); solver.add(e < value); return solver.check() == z3::sat; @@ -1435,7 +1428,8 @@ bool ExprEngine::BinOpResult::isTrue(ExprEngine::DataBase *dataBase) const ExprData exprData; z3::solver solver(exprData.context); z3::expr e = exprData.getExpr(this); - exprData.addConstraints(solver, dynamic_cast(dataBase)); + for (auto constraint : dynamic_cast(dataBase)->constraints) + solver.add(exprData.getConstraintExpr(constraint)); exprData.addAssertions(solver); return solver.check() == z3::sat; } catch (const z3::exception &exception) { @@ -1455,7 +1449,8 @@ std::string ExprEngine::BinOpResult::getExpr(ExprEngine::DataBase *dataBase) con ExprData exprData; z3::solver solver(exprData.context); z3::expr e = exprData.getExpr(this); - exprData.addConstraints(solver, dynamic_cast(dataBase)); + for (auto constraint : dynamic_cast(dataBase)->constraints) + solver.add(exprData.getConstraintExpr(constraint)); exprData.addAssertions(solver); solver.add(e); std::ostringstream os; @@ -1772,11 +1767,7 @@ static void checkContract(Data &data, const Token *tok, const Function *function z3::solver solver(exprData.context); try { // 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))); - } catch (const ExprData::BailoutValueException &) { - throw ExprEngineException(tok, "Internal error: Bailout value used"); - } + solver.add(z3::ite(exprData.getConstraintExpr(data.executeContract(function, executeExpression1)), exprData.context.bool_val(false), exprData.context.bool_val(true))); bool bailoutValue = false; 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) { std::cerr << "z3: " << exception << std::endl; - } catch (const ExprEngineException &) { + } catch (const ExprEngineException &e) { const char id[] = "internalErrorInExprEngine"; const auto contractIt = data.settings->functionContracts.find(function->fullName()); const std::string functionName = contractIt->first;