diff options
Diffstat (limited to 'libsolidity')
-rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 113 | ||||
-rw-r--r-- | libsolidity/formal/SMTChecker.h | 13 | ||||
-rw-r--r-- | libsolidity/formal/SolverInterface.h | 1 | ||||
-rw-r--r-- | libsolidity/formal/Z3Interface.cpp | 2 |
4 files changed, 102 insertions, 27 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 1cf5dc95..3ad9db92 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -28,6 +28,7 @@ #include <libsolidity/interface/ErrorReporter.h> #include <boost/range/adaptor/map.hpp> +#include <boost/algorithm/string/replace.hpp> using namespace std; using namespace dev; @@ -87,7 +88,7 @@ bool SMTChecker::visit(IfStatement const& _node) { _node.condition().accept(*this); - // TODO Check if condition is always true + checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE."); visitBranch(_node.trueStatement(), expr(_node.condition())); vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement()); @@ -104,8 +105,6 @@ bool SMTChecker::visit(IfStatement const& _node) bool SMTChecker::visit(WhileStatement const& _node) { - // TODO Check if condition is always true - auto touchedVariables = m_variableUsage->touchedVariables(_node); resetVariables(touchedVariables); if (_node.isDoWhile()) @@ -113,10 +112,13 @@ bool SMTChecker::visit(WhileStatement const& _node) visitBranch(_node.body()); // TODO the assertions generated in the body should still be active in the condition _node.condition().accept(*this); + checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE."); } else { _node.condition().accept(*this); + checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE."); + visitBranch(_node.body(), expr(_node.condition())); } resetVariables(touchedVariables); @@ -264,6 +266,8 @@ void SMTChecker::endVisit(Literal const& _literal) m_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal))); } + else if (type.category() == Type::Category::Bool) + m_interface->addAssertion(expr(_literal) == smt::Expression(_literal.token() == Token::TrueLiteral ? true : false)); else m_errorReporter.warning( _literal.location(), @@ -426,18 +430,7 @@ void SMTChecker::checkCondition( } smt::CheckResult result; vector<string> values; - try - { - tie(result, values) = m_interface->check(expressionsToEvaluate); - } - catch (smt::SolverError const& _e) - { - string description("Error querying SMT solver"); - if (_e.comment()) - description += ": " + *_e.comment(); - m_errorReporter.warning(_location, description); - return; - } + tie(result, values) = checkSatisifableAndGenerateModel(expressionsToEvaluate); string conditionalComment; if (m_conditionalExecutionHappened) @@ -455,17 +448,7 @@ void SMTChecker::checkCondition( message << " for:\n"; solAssert(values.size() == expressionNames.size(), ""); for (size_t i = 0; i < values.size(); ++i) - { - string formattedValue = values.at(i); - try - { - // Parse and re-format nicely - formattedValue = formatNumber(bigint(formattedValue)); - } - catch (...) { } - - message << " " << expressionNames.at(i) << " = " << formattedValue << "\n"; - } + message << " " << expressionNames.at(i) << " = " << values.at(i) << "\n"; } else message << "."; @@ -486,6 +469,84 @@ void SMTChecker::checkCondition( m_interface->pop(); } +void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string const& _description) +{ + // Do not check for const-ness if this is a constant. + if (dynamic_cast<Literal const*>(&_condition)) + return; + + m_interface->push(); + m_interface->addAssertion(expr(_condition)); + auto positiveResult = checkSatisifable(); + m_interface->pop(); + + m_interface->push(); + m_interface->addAssertion(!expr(_condition)); + auto negatedResult = checkSatisifable(); + m_interface->pop(); + + if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR) + m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver."); + else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE) + { + // everything fine. + } + else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE) + m_errorReporter.warning(_condition.location(), "Condition unreachable."); + else + { + string value; + if (positiveResult == smt::CheckResult::SATISFIABLE) + { + solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, ""); + value = "true"; + } + else + { + solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, ""); + solAssert(negatedResult == smt::CheckResult::SATISFIABLE, ""); + value = "false"; + } + m_errorReporter.warning(_condition.location(), boost::algorithm::replace_all_copy(_description, "$VALUE", value)); + } +} + +pair<smt::CheckResult, vector<string>> +SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate) +{ + smt::CheckResult result; + vector<string> values; + try + { + tie(result, values) = m_interface->check(_expressionsToEvaluate); + } + catch (smt::SolverError const& _e) + { + string description("Error querying SMT solver"); + if (_e.comment()) + description += ": " + *_e.comment(); + m_errorReporter.warning(description); + result = smt::CheckResult::ERROR; + } + + for (string& value: values) + { + try + { + // Parse and re-format nicely + value = formatNumber(bigint(value)); + } + catch (...) { } + } + + return make_pair(result, values); +} + +smt::CheckResult SMTChecker::checkSatisifable() +{ + return checkSatisifableAndGenerateModel({}).first; +} + void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) { for (auto const& variable: _function.localVariables()) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index b2726a42..85a37f2c 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -72,6 +72,7 @@ private: void visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr); void visitBranch(Statement const& _statement, smt::Expression _condition); + /// Check that a condition can be satisfied. void checkCondition( smt::Expression _condition, SourceLocation const& _location, @@ -79,6 +80,18 @@ private: std::string const& _additionalValueName = "", smt::Expression* _additionalValue = nullptr ); + /// Checks that a boolean condition is not constant. Do not warn if the expression + /// is a literal constant. + /// @param _description the warning string, $VALUE will be replaced by the constant value. + void checkBooleanNotConstant( + Expression const& _condition, + std::string const& _description + ); + + std::pair<smt::CheckResult, std::vector<std::string>> + checkSatisifableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate); + + smt::CheckResult checkSatisifable(); void initializeLocalVariables(FunctionDefinition const& _function); void resetVariables(std::vector<Declaration const*> _variables); diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 70dc1585..a69d19d5 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -52,6 +52,7 @@ class Expression { friend class SolverInterface; public: + explicit Expression(bool _v): name(_v ? "true" : "false") {} Expression(size_t _number): name(std::to_string(_number)) {} Expression(u256 const& _number): name(_number.str()) {} Expression(bigint const& _number): name(_number.str()) {} diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 6111b2c8..0c083abc 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -91,7 +91,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _ solAssert(false, ""); } - if (result != CheckResult::UNSATISFIABLE) + if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty()) { z3::model m = m_solver.get_model(); for (Expression const& e: _expressionsToEvaluate) |