diff options
| -rw-r--r-- | libsolidity/ast/ASTForward.h | 1 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 18 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 | ||||
| -rw-r--r-- | libsolidity/formal/Z3Interface.cpp | 48 |
4 files changed, 40 insertions, 31 deletions
diff --git a/libsolidity/ast/ASTForward.h b/libsolidity/ast/ASTForward.h index 15735368..46675e51 100644 --- a/libsolidity/ast/ASTForward.h +++ b/libsolidity/ast/ASTForward.h @@ -57,6 +57,7 @@ class UserDefinedTypeName; class FunctionTypeName; class Mapping; class ArrayTypeName; +class InlineAssembly; class Statement; class Block; class PlaceholderStatement; diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 7c8c089e..2d2f05ec 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -494,10 +494,10 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo { solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, ""); solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, ""); - solAssert(m_Variables.count(&_varDecl) == 0, ""); + solAssert(m_variables.count(&_varDecl) == 0, ""); m_currentSequenceCounter[&_varDecl] = 0; m_nextFreeSequenceCounter[&_varDecl] = 1; - m_Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); + m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); setValue(_varDecl, _setToZero); } else @@ -566,7 +566,7 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t) smt::Expression SMTChecker::expr(Expression const& _e) { - if (!m_Expressions.count(&_e)) + if (!m_expressions.count(&_e)) { solAssert(_e.annotation().type, ""); switch (_e.annotation().type->category()) @@ -575,24 +575,24 @@ smt::Expression SMTChecker::expr(Expression const& _e) { if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get())) solAssert(!rational->isFractional(), ""); - m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); break; } case Type::Category::Integer: - m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); break; case Type::Category::Bool: - m_Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); + m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); break; default: solAssert(false, "Type not implemented."); } } - return m_Expressions.at(&_e); + return m_expressions.at(&_e); } smt::Expression SMTChecker::var(Declaration const& _decl) { - solAssert(m_Variables.count(&_decl), ""); - return m_Variables.at(&_decl); + solAssert(m_variables.count(&_decl), ""); + return m_variables.at(&_decl); } diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index d23fd201..faaac639 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -103,8 +103,8 @@ private: std::shared_ptr<smt::SolverInterface> m_interface; std::map<Declaration const*, int> m_currentSequenceCounter; std::map<Declaration const*, int> m_nextFreeSequenceCounter; - std::map<Expression const*, smt::Expression> m_Expressions; - std::map<Declaration const*, smt::Expression> m_Variables; + std::map<Expression const*, smt::Expression> m_expressions; + std::map<Declaration const*, smt::Expression> m_variables; ErrorReporter& m_errorReporter; FunctionDefinition const* m_currentFunction = nullptr; diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 0ceed3a7..ab28baa3 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -73,28 +73,37 @@ void Z3Interface::addAssertion(Expression const& _expr) pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate) { CheckResult result; - switch (m_solver.check()) + vector<string> values; + try { - case z3::check_result::sat: - result = CheckResult::SATISFIABLE; - break; - case z3::check_result::unsat: - result = CheckResult::UNSATISFIABLE; - break; - case z3::check_result::unknown: - result = CheckResult::UNKNOWN; - break; - default: - solAssert(false, ""); + switch (m_solver.check()) + { + case z3::check_result::sat: + result = CheckResult::SATISFIABLE; + break; + case z3::check_result::unsat: + result = CheckResult::UNSATISFIABLE; + break; + case z3::check_result::unknown: + result = CheckResult::UNKNOWN; + break; + default: + solAssert(false, ""); + } + + if (result != CheckResult::UNSATISFIABLE) + { + z3::model m = m_solver.get_model(); + for (Expression const& e: _expressionsToEvaluate) + values.push_back(toString(m.eval(toZ3Expr(e)))); + } } - - vector<string> values; - if (result != CheckResult::UNSATISFIABLE) + catch (z3::exception const& _e) { - z3::model m = m_solver.get_model(); - for (Expression const& e: _expressionsToEvaluate) - values.push_back(toString(m.eval(toZ3Expr(e)))); + result = CheckResult::ERROR; + values.clear(); } + return make_pair(result, values); } @@ -118,8 +127,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) {">=", 2}, {"+", 2}, {"-", 2}, - {"*", 2}, - {">=", 2} + {"*", 2} }; string const& n = _expr.name; if (m_functions.count(n)) |