From 22c689d516bc69b49797005de0cd64c23fcaad2f Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 29 Sep 2017 16:53:26 +0200 Subject: Check for conditions being constant. --- libsolidity/formal/SMTChecker.cpp | 113 +++++++++++++++++++++++++++-------- libsolidity/formal/SMTChecker.h | 13 ++++ libsolidity/formal/SolverInterface.h | 1 + libsolidity/formal/Z3Interface.cpp | 2 +- 4 files changed, 102 insertions(+), 27 deletions(-) (limited to 'libsolidity') 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 #include +#include 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 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 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(&_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> +SMTChecker::checkSatisifableAndGenerateModel(vector const& _expressionsToEvaluate) +{ + smt::CheckResult result; + vector 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> + checkSatisifableAndGenerateModel(std::vector const& _expressionsToEvaluate); + + smt::CheckResult checkSatisifable(); void initializeLocalVariables(FunctionDefinition const& _function); void resetVariables(std::vector _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> Z3Interface::check(vector 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) -- cgit v1.2.3