diff options
| -rw-r--r-- | Changelog.md | 1 | ||||
| -rw-r--r-- | cmake/FindZ3.cmake | 9 | ||||
| -rw-r--r-- | libdevcore/CommonData.h | 11 | ||||
| -rw-r--r-- | libsolidity/CMakeLists.txt | 14 | ||||
| -rw-r--r-- | libsolidity/ast/AST.cpp | 1 | ||||
| -rw-r--r-- | libsolidity/ast/ExperimentalFeatures.h | 3 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 588 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 114 | ||||
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.cpp | 187 | ||||
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.h | 75 | ||||
| -rw-r--r-- | libsolidity/formal/SolverInterface.h | 178 | ||||
| -rw-r--r-- | libsolidity/formal/Z3Interface.cpp | 189 | ||||
| -rw-r--r-- | libsolidity/formal/Z3Interface.h | 65 | ||||
| -rw-r--r-- | libsolidity/interface/CompilerStack.cpp | 14 | ||||
| -rw-r--r-- | libsolidity/interface/CompilerStack.h | 5 | ||||
| -rw-r--r-- | libsolidity/interface/ReadFile.h | 8 | ||||
| -rw-r--r-- | libsolidity/interface/StandardCompiler.cpp | 8 | ||||
| -rw-r--r-- | libsolidity/interface/StandardCompiler.h | 4 | ||||
| -rwxr-xr-x | scripts/install_deps.sh | 55 | ||||
| -rw-r--r-- | solc/CommandLineInterface.cpp | 14 | ||||
| -rw-r--r-- | solc/jsonCompiler.cpp | 12 |
21 files changed, 1503 insertions, 52 deletions
diff --git a/Changelog.md b/Changelog.md index efcea03f..ed004d8c 100644 --- a/Changelog.md +++ b/Changelog.md @@ -2,6 +2,7 @@ Features: * ABI JSON: Include new field ``statemutability`` with values ``view``, ``nonpayable`` and ``payable``. + * Analyzer: Experimental partial support for Z3 SMT checker. * Parser: Display previous visibility specifier in error if multiple are found. * Parser: Introduce ``view`` keyword on functions (``constant`` remains an alias for ``view``). * Syntax Checker: Support ``pragma experimental <feature>;`` to turn on experimental features. diff --git a/cmake/FindZ3.cmake b/cmake/FindZ3.cmake new file mode 100644 index 00000000..8f3f9ee1 --- /dev/null +++ b/cmake/FindZ3.cmake @@ -0,0 +1,9 @@ +find_path(Z3_INCLUDE_DIR z3++.h) +find_library(Z3_LIBRARY NAMES z3 ) +include(${CMAKE_CURRENT_LIST_DIR}/FindPackageHandleStandardArgs.cmake) +FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3 DEFAULT_MSG Z3_LIBRARY Z3_INCLUDE_DIR) + +if(Z3_FOUND) + set(Z3_LIBRARIES ${Z3_LIBRARY}) +endif() + diff --git a/libdevcore/CommonData.h b/libdevcore/CommonData.h index 0321011e..5df8986a 100644 --- a/libdevcore/CommonData.h +++ b/libdevcore/CommonData.h @@ -145,6 +145,17 @@ inline std::string toHex(u256 val, HexPrefix prefix = HexPrefix::DontAdd) return (prefix == HexPrefix::Add) ? "0x" + str : str; } +/// Returns decimal representation for small numbers and hex for large numbers. +inline std::string formatNumber(bigint const& _value) +{ + if (_value < 0) + return "-" + formatNumber(-_value); + if (_value > 0x1000000) + return toHex(toCompactBigEndian(_value), 2, HexPrefix::Add); + else + return _value.str(); +} + inline std::string toCompactHexWithPrefix(u256 val) { std::ostringstream ret; diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 11fd6fe2..f7c1a390 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -2,5 +2,19 @@ file(GLOB_RECURSE sources "*.cpp" "../libjulia/*.cpp") file(GLOB_RECURSE headers "*.h" "../libjulia/*.h") +find_package(Z3 QUIET) +if (${Z3_FOUND}) + include_directories(${Z3_INCLUDE_DIR}) + add_definitions(-DHAVE_Z3) + message("Z3 SMT solver FOUND.") +else() + message("Z3 SMT solver NOT found.") + list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/Z3Interface.cpp") +endif() + add_library(solidity ${sources} ${headers}) target_link_libraries(solidity PUBLIC evmasm devcore) + +if (${Z3_FOUND}) + target_link_libraries(solidity PUBLIC ${Z3_LIBRARY}) +endif()
\ No newline at end of file diff --git a/libsolidity/ast/AST.cpp b/libsolidity/ast/AST.cpp index 605daf55..7f4dea0e 100644 --- a/libsolidity/ast/AST.cpp +++ b/libsolidity/ast/AST.cpp @@ -22,6 +22,7 @@ #include <libsolidity/ast/AST.h> #include <libsolidity/ast/ASTVisitor.h> +#include <libsolidity/interface/Exceptions.h> #include <libsolidity/ast/AST_accept.h> #include <libdevcore/SHA3.h> diff --git a/libsolidity/ast/ExperimentalFeatures.h b/libsolidity/ast/ExperimentalFeatures.h index 0c03ea4a..2c089671 100644 --- a/libsolidity/ast/ExperimentalFeatures.h +++ b/libsolidity/ast/ExperimentalFeatures.h @@ -29,6 +29,7 @@ namespace solidity enum class ExperimentalFeature { + SMTChecker, ABIEncoderV2, // new ABI encoder that makes use of JULIA Test, TestOnlyAnalysis @@ -36,11 +37,13 @@ enum class ExperimentalFeature static const std::map<ExperimentalFeature, bool> ExperimentalFeatureOnlyAnalysis = { + { ExperimentalFeature::SMTChecker, true }, { ExperimentalFeature::TestOnlyAnalysis, true }, }; static const std::map<std::string, ExperimentalFeature> ExperimentalFeatureNames = { + { "SMTChecker", ExperimentalFeature::SMTChecker }, { "ABIEncoderV2", ExperimentalFeature::ABIEncoderV2 }, { "__test", ExperimentalFeature::Test }, { "__testOnlyAnalysis", ExperimentalFeature::TestOnlyAnalysis }, diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp new file mode 100644 index 00000000..fd78e578 --- /dev/null +++ b/libsolidity/formal/SMTChecker.cpp @@ -0,0 +1,588 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#include <libsolidity/formal/SMTChecker.h> + +#ifdef HAVE_Z3 +#include <libsolidity/formal/Z3Interface.h> +#else +#include <libsolidity/formal/SMTLib2Interface.h> +#endif + +#include <libsolidity/interface/ErrorReporter.h> + +#include <boost/range/adaptor/map.hpp> + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback): +#ifdef HAVE_Z3 + m_interface(make_shared<smt::Z3Interface>()), +#else + m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)), +#endif + m_errorReporter(_errorReporter) +{ + (void)_readFileCallback; +} + +void SMTChecker::analyze(SourceUnit const& _source) +{ + if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) + { + m_interface->reset(); + m_currentSequenceCounter.clear(); + m_nextFreeSequenceCounter.clear(); + _source.accept(*this); + } +} + +void SMTChecker::endVisit(VariableDeclaration const& _varDecl) +{ + if (_varDecl.value()) + { + m_errorReporter.warning( + _varDecl.location(), + "Assertion checker does not yet support this." + ); + } + else if (_varDecl.isLocalOrReturn()) + createVariable(_varDecl, true); + else if (_varDecl.isCallableParameter()) + createVariable(_varDecl, false); +} + +bool SMTChecker::visit(FunctionDefinition const& _function) +{ + if (!_function.modifiers().empty() || _function.isConstructor()) + m_errorReporter.warning( + _function.location(), + "Assertion checker does not yet support constructors and functions with modifiers." + ); + // TODO actually we probably also have to reset all local variables and similar things. + m_currentFunction = &_function; + m_interface->push(); + return true; +} + +void SMTChecker::endVisit(FunctionDefinition const&) +{ + // TOOD we could check for "reachability", i.e. satisfiability here. + // We only handle local variables, so we clear everything. + // If we add storage variables, those should be cleared differently. + m_currentSequenceCounter.clear(); + m_nextFreeSequenceCounter.clear(); + m_interface->pop(); + m_currentFunction = nullptr; +} + +bool SMTChecker::visit(IfStatement const& _node) +{ + _node.condition().accept(*this); + + // TODO Check if condition is always true + + auto countersAtStart = m_currentSequenceCounter; + m_interface->push(); + m_interface->addAssertion(expr(_node.condition())); + _node.trueStatement().accept(*this); + auto countersAtEndOfTrue = m_currentSequenceCounter; + m_interface->pop(); + + decltype(m_currentSequenceCounter) countersAtEndOfFalse; + if (_node.falseStatement()) + { + m_currentSequenceCounter = countersAtStart; + m_interface->push(); + m_interface->addAssertion(!expr(_node.condition())); + _node.falseStatement()->accept(*this); + countersAtEndOfFalse = m_currentSequenceCounter; + m_interface->pop(); + } + else + countersAtEndOfFalse = countersAtStart; + + // Reset all values that have been touched. + + // TODO this should use a previously generated side-effect structure + + solAssert(countersAtEndOfFalse.size() == countersAtEndOfTrue.size(), ""); + for (auto const& declCounter: countersAtEndOfTrue) + { + solAssert(countersAtEndOfFalse.count(declCounter.first), ""); + auto decl = declCounter.first; + int trueCounter = countersAtEndOfTrue.at(decl); + int falseCounter = countersAtEndOfFalse.at(decl); + if (trueCounter == falseCounter) + continue; // Was not modified + newValue(*decl); + setValue(*decl, 0); + } + return false; +} + +bool SMTChecker::visit(WhileStatement const& _node) +{ + _node.condition().accept(*this); + + //m_interface->push(); + //m_interface->addAssertion(expr(_node.condition())); + // TDOO clear knowledge (increment sequence numbers and add bounds assertions ) apart from assertions + + // TODO combine similar to if + return true; +} + +void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl) +{ + if (_varDecl.declarations().size() != 1) + m_errorReporter.warning( + _varDecl.location(), + "Assertion checker does not yet support such variable declarations." + ); + else if (knownVariable(*_varDecl.declarations()[0])) + { + if (_varDecl.initialValue()) + // TODO more checks? + // TODO add restrictions about type (might be assignment from smaller type) + m_interface->addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue())); + } + else + m_errorReporter.warning( + _varDecl.location(), + "Assertion checker does not yet implement such variable declarations." + ); +} + +void SMTChecker::endVisit(ExpressionStatement const&) +{ +} + +void SMTChecker::endVisit(Assignment const& _assignment) +{ + if (_assignment.assignmentOperator() != Token::Value::Assign) + m_errorReporter.warning( + _assignment.location(), + "Assertion checker does not yet implement compound assignment." + ); + else if (_assignment.annotation().type->category() != Type::Category::Integer) + m_errorReporter.warning( + _assignment.location(), + "Assertion checker does not yet implement type " + _assignment.annotation().type->toString() + ); + else if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide())) + { + Declaration const* decl = identifier->annotation().referencedDeclaration; + if (knownVariable(*decl)) + // TODO more checks? + // TODO add restrictions about type (might be assignment from smaller type) + m_interface->addAssertion(newValue(*decl) == expr(_assignment.rightHandSide())); + else + m_errorReporter.warning( + _assignment.location(), + "Assertion checker does not yet implement such assignments." + ); + } + else + m_errorReporter.warning( + _assignment.location(), + "Assertion checker does not yet implement such assignments." + ); +} + +void SMTChecker::endVisit(TupleExpression const& _tuple) +{ + if (_tuple.isInlineArray() || _tuple.components().size() != 1) + m_errorReporter.warning( + _tuple.location(), + "Assertion checker does not yet implement tules and inline arrays." + ); + else + m_interface->addAssertion(expr(_tuple) == expr(*_tuple.components()[0])); +} + +void SMTChecker::endVisit(BinaryOperation const& _op) +{ + if (Token::isArithmeticOp(_op.getOperator())) + arithmeticOperation(_op); + else if (Token::isCompareOp(_op.getOperator())) + compareOperation(_op); + else if (Token::isBooleanOp(_op.getOperator())) + booleanOperation(_op); + else + m_errorReporter.warning( + _op.location(), + "Assertion checker does not yet implement this operator." + ); +} + +void SMTChecker::endVisit(FunctionCall const& _funCall) +{ + FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type); + + std::vector<ASTPointer<Expression const>> const args = _funCall.arguments(); + if (funType.kind() == FunctionType::Kind::Assert) + { + solAssert(args.size() == 1, ""); + solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); + checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation"); + m_interface->addAssertion(expr(*args[0])); + } + else if (funType.kind() == FunctionType::Kind::Require) + { + solAssert(args.size() == 1, ""); + solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); + m_interface->addAssertion(expr(*args[0])); + checkCondition(!(expr(*args[0])), _funCall.location(), "Unreachable code"); + // TODO is there something meaningful we can check here? + // We can check whether the condition is always fulfilled or never fulfilled. + } +} + +void SMTChecker::endVisit(Identifier const& _identifier) +{ + Declaration const* decl = _identifier.annotation().referencedDeclaration; + solAssert(decl, ""); + if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get())) + { + m_interface->addAssertion(expr(_identifier) == currentValue(*decl)); + return; + } + else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get())) + { + if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require) + return; + // TODO for others, clear our knowledge about storage and memory + } + m_errorReporter.warning( + _identifier.location(), + "Assertion checker does not yet support the type of this expression (" + + _identifier.annotation().type->toString() + + ")." + ); +} + +void SMTChecker::endVisit(Literal const& _literal) +{ + Type const& type = *_literal.annotation().type; + if (type.category() == Type::Category::Integer || type.category() == Type::Category::RationalNumber) + { + if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type)) + solAssert(!rational->isFractional(), ""); + + m_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal))); + } + else + m_errorReporter.warning( + _literal.location(), + "Assertion checker does not yet support the type of this expression (" + + _literal.annotation().type->toString() + + ")." + ); +} + +void SMTChecker::arithmeticOperation(BinaryOperation const& _op) +{ + switch (_op.getOperator()) + { + case Token::Add: + case Token::Sub: + case Token::Mul: + { + solAssert(_op.annotation().commonType, ""); + solAssert(_op.annotation().commonType->category() == Type::Category::Integer, ""); + smt::Expression left(expr(_op.leftExpression())); + smt::Expression right(expr(_op.rightExpression())); + Token::Value op = _op.getOperator(); + smt::Expression value( + op == Token::Add ? left + right : + op == Token::Sub ? left - right : + /*op == Token::Mul*/ left * right + ); + + // Overflow check + auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType); + checkCondition( + value < minValue(intType), + _op.location(), + "Underflow (resulting value less than " + formatNumber(intType.minValue()) + ")", + "value", + &value + ); + checkCondition( + value > maxValue(intType), + _op.location(), + "Overflow (resulting value larger than " + formatNumber(intType.maxValue()) + ")", + "value", + &value + ); + + m_interface->addAssertion(expr(_op) == value); + break; + } + default: + m_errorReporter.warning( + _op.location(), + "Assertion checker does not yet implement this operator." + ); + } +} + +void SMTChecker::compareOperation(BinaryOperation const& _op) +{ + solAssert(_op.annotation().commonType, ""); + if (_op.annotation().commonType->category() == Type::Category::Integer) + { + smt::Expression left(expr(_op.leftExpression())); + smt::Expression right(expr(_op.rightExpression())); + Token::Value op = _op.getOperator(); + smt::Expression value = ( + op == Token::Equal ? (left == right) : + op == Token::NotEqual ? (left != right) : + op == Token::LessThan ? (left < right) : + op == Token::LessThanOrEqual ? (left <= right) : + op == Token::GreaterThan ? (left > right) : + /*op == Token::GreaterThanOrEqual*/ (left >= right) + ); + // TODO: check that other values for op are not possible. + m_interface->addAssertion(expr(_op) == value); + } + else + m_errorReporter.warning( + _op.location(), + "Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for comparisons" + ); +} + +void SMTChecker::booleanOperation(BinaryOperation const& _op) +{ + solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, ""); + solAssert(_op.annotation().commonType, ""); + if (_op.annotation().commonType->category() == Type::Category::Bool) + { + if (_op.getOperator() == Token::And) + m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression())); + else + m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression())); + } + else + m_errorReporter.warning( + _op.location(), + "Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations" + ); +} + +void SMTChecker::checkCondition( + smt::Expression _condition, + SourceLocation const& _location, + string const& _description, + string const& _additionalValueName, + smt::Expression* _additionalValue +) +{ + m_interface->push(); + m_interface->addAssertion(_condition); + + vector<smt::Expression> expressionsToEvaluate; + vector<string> expressionNames; + if (m_currentFunction) + { + if (_additionalValue) + { + expressionsToEvaluate.emplace_back(*_additionalValue); + expressionNames.push_back(_additionalValueName); + } + for (auto const& param: m_currentFunction->parameters()) + if (knownVariable(*param)) + { + expressionsToEvaluate.emplace_back(currentValue(*param)); + expressionNames.push_back(param->name()); + } + for (auto const& var: m_currentFunction->localVariables()) + if (knownVariable(*var)) + { + expressionsToEvaluate.emplace_back(currentValue(*var)); + expressionNames.push_back(var->name()); + } + } + 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; + } + + switch (result) + { + case smt::CheckResult::SATISFIABLE: + { + std::ostringstream message; + message << _description << " happens here"; + if (m_currentFunction) + { + 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"; + } + } + else + message << "."; + m_errorReporter.warning(_location, message.str()); + break; + } + case smt::CheckResult::UNSATISFIABLE: + break; + case smt::CheckResult::UNKNOWN: + m_errorReporter.warning(_location, _description + " might happen here."); + break; + case smt::CheckResult::ERROR: + m_errorReporter.warning(_location, "Error trying to invoke SMT solver."); + break; + default: + solAssert(false, ""); + } + m_interface->pop(); +} + +void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero) +{ + if (dynamic_cast<IntegerType const*>(_varDecl.type().get())) + { + solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, ""); + solAssert(m_nextFreeSequenceCounter.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)); + setValue(_varDecl, _setToZero); + } + else + m_errorReporter.warning( + _varDecl.location(), + "Assertion checker does not yet support the type of this variable." + ); +} + +string SMTChecker::uniqueSymbol(Declaration const& _decl) +{ + return _decl.name() + "_" + to_string(_decl.id()); +} + +string SMTChecker::uniqueSymbol(Expression const& _expr) +{ + return "expr_" + to_string(_expr.id()); +} + +bool SMTChecker::knownVariable(Declaration const& _decl) +{ + return m_currentSequenceCounter.count(&_decl); +} + +smt::Expression SMTChecker::currentValue(Declaration const& _decl) +{ + solAssert(m_currentSequenceCounter.count(&_decl), ""); + return valueAtSequence(_decl, m_currentSequenceCounter.at(&_decl)); +} + +smt::Expression SMTChecker::valueAtSequence(const Declaration& _decl, int _sequence) +{ + return var(_decl)(_sequence); +} + +smt::Expression SMTChecker::newValue(Declaration const& _decl) +{ + solAssert(m_currentSequenceCounter.count(&_decl), ""); + solAssert(m_nextFreeSequenceCounter.count(&_decl), ""); + m_currentSequenceCounter[&_decl] = m_nextFreeSequenceCounter[&_decl]++; + return currentValue(_decl); +} + +void SMTChecker::setValue(Declaration const& _decl, bool _setToZero) +{ + auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type()); + + if (_setToZero) + m_interface->addAssertion(currentValue(_decl) == 0); + else + { + m_interface->addAssertion(currentValue(_decl) >= minValue(intType)); + m_interface->addAssertion(currentValue(_decl) <= maxValue(intType)); + } +} + +smt::Expression SMTChecker::minValue(IntegerType const& _t) +{ + return smt::Expression(_t.minValue()); +} + +smt::Expression SMTChecker::maxValue(IntegerType const& _t) +{ + return smt::Expression(_t.maxValue()); +} + +smt::Expression SMTChecker::expr(Expression const& _e) +{ + if (!m_Expressions.count(&_e)) + { + solAssert(_e.annotation().type, ""); + switch (_e.annotation().type->category()) + { + case Type::Category::RationalNumber: + { + if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get())) + solAssert(!rational->isFractional(), ""); + m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + break; + } + case Type::Category::Integer: + m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + break; + case Type::Category::Bool: + m_Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); + break; + default: + solAssert(false, "Type not implemented."); + } + } + return m_Expressions.at(&_e); +} + +smt::Expression SMTChecker::var(Declaration const& _decl) +{ + solAssert(m_Variables.count(&_decl), ""); + return m_Variables.at(&_decl); +} diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h new file mode 100644 index 00000000..d23fd201 --- /dev/null +++ b/libsolidity/formal/SMTChecker.h @@ -0,0 +1,114 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#pragma once + +#include <libsolidity/ast/ASTVisitor.h> +#include <libsolidity/formal/SolverInterface.h> +#include <libsolidity/interface/ReadFile.h> + +#include <map> +#include <string> + +namespace dev +{ +namespace solidity +{ + +class ErrorReporter; + +class SMTChecker: private ASTConstVisitor +{ +public: + SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback); + + void analyze(SourceUnit const& _sources); + +private: + // TODO: Check that we do not have concurrent reads and writes to a variable, + // because the order of expression evaluation is undefined + // TODO: or just force a certain order, but people might have a different idea about that. + + virtual void endVisit(VariableDeclaration const& _node) override; + virtual bool visit(FunctionDefinition const& _node) override; + virtual void endVisit(FunctionDefinition const& _node) override; + virtual bool visit(IfStatement const& _node) override; + virtual bool visit(WhileStatement const& _node) override; + virtual void endVisit(VariableDeclarationStatement const& _node) override; + virtual void endVisit(ExpressionStatement const& _node) override; + virtual void endVisit(Assignment const& _node) override; + virtual void endVisit(TupleExpression const& _node) override; + virtual void endVisit(BinaryOperation const& _node) override; + virtual void endVisit(FunctionCall const& _node) override; + virtual void endVisit(Identifier const& _node) override; + virtual void endVisit(Literal const& _node) override; + + void arithmeticOperation(BinaryOperation const& _op); + void compareOperation(BinaryOperation const& _op); + void booleanOperation(BinaryOperation const& _op); + + void checkCondition( + smt::Expression _condition, + SourceLocation const& _location, + std::string const& _description, + std::string const& _additionalValueName = "", + smt::Expression* _additionalValue = nullptr + ); + + void createVariable(VariableDeclaration const& _varDecl, bool _setToZero); + + static std::string uniqueSymbol(Declaration const& _decl); + static std::string uniqueSymbol(Expression const& _expr); + + /// @returns true if _delc is a variable that is known at the current point, i.e. + /// has a valid sequence number + bool knownVariable(Declaration const& _decl); + /// @returns an expression denoting the value of the variable declared in @a _decl + /// at the current point. + smt::Expression currentValue(Declaration const& _decl); + /// @returns an expression denoting the value of the variable declared in @a _decl + /// at the given sequence point. Does not ensure that this sequence point exists. + smt::Expression valueAtSequence(Declaration const& _decl, int _sequence); + /// Allocates a new sequence number for the declaration, updates the current + /// sequence number to this value and returns the expression. + smt::Expression newValue(Declaration const& _decl); + + /// Sets the value of the declaration either to zero or to its intrinsic range. + void setValue(Declaration const& _decl, bool _setToZero); + + static smt::Expression minValue(IntegerType const& _t); + static smt::Expression maxValue(IntegerType const& _t); + + /// Returns the expression corresponding to the AST node. Creates a new expression + /// if it does not exist yet. + smt::Expression expr(Expression const& _e); + /// Returns the function declaration corresponding to the given variable. + /// The function takes one argument which is the "sequence number". + smt::Expression var(Declaration const& _decl); + + 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; + ErrorReporter& m_errorReporter; + + FunctionDefinition const* m_currentFunction = nullptr; +}; + +} +} diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp new file mode 100644 index 00000000..cbd766fb --- /dev/null +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -0,0 +1,187 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#include <libsolidity/formal/SMTLib2Interface.h> + +#include <libsolidity/interface/Exceptions.h> +#include <libsolidity/interface/ReadFile.h> + +#include <boost/algorithm/string/predicate.hpp> +#include <boost/algorithm/string/join.hpp> +#include <boost/filesystem/operations.hpp> + +#include <cstdio> +#include <fstream> +#include <iostream> +#include <memory> +#include <stdexcept> +#include <string> +#include <array> + +using namespace std; +using namespace dev; +using namespace dev::solidity; +using namespace dev::solidity::smt; + +SMTLib2Interface::SMTLib2Interface(ReadCallback::Callback const& _queryCallback): + m_queryCallback(_queryCallback) +{ + reset(); +} + +void SMTLib2Interface::reset() +{ + m_accumulatedOutput.clear(); + m_accumulatedOutput.emplace_back(); + write("(set-option :produce-models true)"); + write("(set-logic QF_UFLIA)"); +} + +void SMTLib2Interface::push() +{ + m_accumulatedOutput.emplace_back(); +} + +void SMTLib2Interface::pop() +{ + solAssert(!m_accumulatedOutput.empty(), ""); + m_accumulatedOutput.pop_back(); +} + +Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain) +{ + write( + "(declare-fun |" + + _name + + "| (" + + (_domain == Sort::Int ? "Int" : "Bool") + + ") " + + (_codomain == Sort::Int ? "Int" : "Bool") + + ")" + ); + return SolverInterface::newFunction(move(_name), _domain, _codomain); +} + +Expression SMTLib2Interface::newInteger(string _name) +{ + write("(declare-const |" + _name + "| Int)"); + return SolverInterface::newInteger(move(_name)); +} + +Expression SMTLib2Interface::newBool(string _name) +{ + write("(declare-const |" + _name + "| Bool)"); + return SolverInterface::newBool(std::move(_name)); +} + +void SMTLib2Interface::addAssertion(Expression const& _expr) +{ + write("(assert " + toSExpr(_expr) + ")"); +} + +pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate) +{ + string response = querySolver( + boost::algorithm::join(m_accumulatedOutput, "\n") + + checkSatAndGetValuesCommand(_expressionsToEvaluate) + ); + + CheckResult result; + // TODO proper parsing + if (boost::starts_with(response, "sat\n")) + result = CheckResult::SATISFIABLE; + else if (boost::starts_with(response, "unsat\n")) + result = CheckResult::UNSATISFIABLE; + else if (boost::starts_with(response, "unknown\n")) + result = CheckResult::UNKNOWN; + else + result = CheckResult::ERROR; + + vector<string> values; + if (result != CheckResult::UNSATISFIABLE && result != CheckResult::ERROR) + values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend()); + return make_pair(result, values); +} + +string SMTLib2Interface::toSExpr(Expression const& _expr) +{ + if (_expr.arguments.empty()) + return _expr.name; + std::string sexpr = "(" + _expr.name; + for (auto const& arg: _expr.arguments) + sexpr += " " + toSExpr(arg); + sexpr += ")"; + return sexpr; +} + +void SMTLib2Interface::write(string _data) +{ + solAssert(!m_accumulatedOutput.empty(), ""); + m_accumulatedOutput.back() += move(_data) + "\n"; +} + +string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate) +{ + string command; + if (_expressionsToEvaluate.empty()) + command = "(check-sat)\n"; + else + { + // TODO make sure these are unique + for (size_t i = 0; i < _expressionsToEvaluate.size(); i++) + { + auto const& e = _expressionsToEvaluate.at(i); + // TODO they don't have to be ints... + command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n"; + command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n"; + } + command += "(check-sat)\n"; + command += "(get-value ("; + for (size_t i = 0; i < _expressionsToEvaluate.size(); i++) + command += "|EVALEXPR_" + to_string(i) + "| "; + command += "))\n"; + } + + return command; +} + +vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, string::const_iterator _end) +{ + vector<string> values; + while (_start < _end) + { + auto valStart = find(_start, _end, ' '); + if (valStart < _end) + ++valStart; + auto valEnd = find(valStart, _end, ')'); + values.emplace_back(valStart, valEnd); + _start = find(valEnd, _end, '('); + } + + return values; +} + +string SMTLib2Interface::querySolver(string const& _input) +{ + if (!m_queryCallback) + BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment("No SMT solver available.")); + + ReadCallback::Result queryResult = m_queryCallback(_input); + if (!queryResult.success) + BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment(queryResult.responseOrErrorMessage)); + return queryResult.responseOrErrorMessage; +} diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h new file mode 100644 index 00000000..b8dac366 --- /dev/null +++ b/libsolidity/formal/SMTLib2Interface.h @@ -0,0 +1,75 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#pragma once + +#include <libsolidity/formal/SolverInterface.h> + +#include <libsolidity/interface/Exceptions.h> +#include <libsolidity/interface/ReadFile.h> + +#include <libdevcore/Common.h> + +#include <boost/noncopyable.hpp> + +#include <map> +#include <string> +#include <vector> +#include <cstdio> + +namespace dev +{ +namespace solidity +{ +namespace smt +{ + +class SMTLib2Interface: public SolverInterface, public boost::noncopyable +{ +public: + SMTLib2Interface(ReadCallback::Callback const& _queryCallback); + + void reset() override; + + void push() override; + void pop() override; + + Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override; + Expression newInteger(std::string _name) override; + Expression newBool(std::string _name) override; + + void addAssertion(Expression const& _expr) override; + std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; + +private: + std::string toSExpr(Expression const& _expr); + + void write(std::string _data); + + std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate); + std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end); + + /// Communicates with the solver via the callback. Throws SMTSolverError on error. + std::string querySolver(std::string const& _input); + + ReadCallback::Callback m_queryCallback; + std::vector<std::string> m_accumulatedOutput; +}; + +} +} +} diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h new file mode 100644 index 00000000..32d92a2a --- /dev/null +++ b/libsolidity/formal/SolverInterface.h @@ -0,0 +1,178 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#pragma once + +#include <libsolidity/interface/Exceptions.h> +#include <libsolidity/interface/ReadFile.h> + +#include <libdevcore/Common.h> +#include <libdevcore/Exceptions.h> + +#include <boost/noncopyable.hpp> + +#include <map> +#include <string> +#include <vector> +#include <cstdio> + +namespace dev +{ +namespace solidity +{ +namespace smt +{ + +enum class CheckResult +{ + SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR +}; + +enum class Sort +{ + Int, Bool +}; + +/// C++ representation of an SMTLIB2 expression. +class Expression +{ + friend class SolverInterface; +public: + Expression(size_t _number): name(std::to_string(_number)) {} + Expression(u256 const& _number): name(_number.str()) {} + Expression(bigint const& _number): name(_number.str()) {} + + Expression(Expression const& _other) = default; + Expression(Expression&& _other) = default; + Expression& operator=(Expression const& _other) = default; + Expression& operator=(Expression&& _other) = default; + + static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue) + { + return Expression("ite", std::vector<Expression>{ + std::move(_condition), std::move(_trueValue), std::move(_falseValue) + }); + } + + friend Expression operator!(Expression _a) + { + return Expression("not", std::move(_a)); + } + friend Expression operator&&(Expression _a, Expression _b) + { + return Expression("and", std::move(_a), std::move(_b)); + } + friend Expression operator||(Expression _a, Expression _b) + { + return Expression("or", std::move(_a), std::move(_b)); + } + friend Expression operator==(Expression _a, Expression _b) + { + return Expression("=", std::move(_a), std::move(_b)); + } + friend Expression operator!=(Expression _a, Expression _b) + { + return !(std::move(_a) == std::move(_b)); + } + friend Expression operator<(Expression _a, Expression _b) + { + return Expression("<", std::move(_a), std::move(_b)); + } + friend Expression operator<=(Expression _a, Expression _b) + { + return Expression("<=", std::move(_a), std::move(_b)); + } + friend Expression operator>(Expression _a, Expression _b) + { + return Expression(">", std::move(_a), std::move(_b)); + } + friend Expression operator>=(Expression _a, Expression _b) + { + return Expression(">=", std::move(_a), std::move(_b)); + } + friend Expression operator+(Expression _a, Expression _b) + { + return Expression("+", std::move(_a), std::move(_b)); + } + friend Expression operator-(Expression _a, Expression _b) + { + return Expression("-", std::move(_a), std::move(_b)); + } + friend Expression operator*(Expression _a, Expression _b) + { + return Expression("*", std::move(_a), std::move(_b)); + } + Expression operator()(Expression _a) const + { + solAssert(arguments.empty(), "Attempted function application to non-function."); + return Expression(name, _a); + } + + std::string const name; + std::vector<Expression> const arguments; + +private: + /// Manual constructor, should only be used by SolverInterface and this class itself. + Expression(std::string _name, std::vector<Expression> _arguments): + name(std::move(_name)), arguments(std::move(_arguments)) {} + + explicit Expression(std::string _name): + Expression(std::move(_name), std::vector<Expression>{}) {} + Expression(std::string _name, Expression _arg): + Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}) {} + Expression(std::string _name, Expression _arg1, Expression _arg2): + Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}) {} +}; + +DEV_SIMPLE_EXCEPTION(SolverError); + +class SolverInterface +{ +public: + virtual void reset() = 0; + + virtual void push() = 0; + virtual void pop() = 0; + + virtual Expression newFunction(std::string _name, Sort /*_domain*/, Sort /*_codomain*/) + { + // Subclasses should do something here + return Expression(std::move(_name), {}); + } + virtual Expression newInteger(std::string _name) + { + // Subclasses should do something here + return Expression(std::move(_name), {}); + } + virtual Expression newBool(std::string _name) + { + // Subclasses should do something here + return Expression(std::move(_name), {}); + } + + virtual void addAssertion(Expression const& _expr) = 0; + + /// Checks for satisfiability, evaluates the expressions if a model + /// is available. Throws SMTSolverError on error. + virtual std::pair<CheckResult, std::vector<std::string>> + check(std::vector<Expression> const& _expressionsToEvaluate) = 0; +}; + + +} +} +} diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp new file mode 100644 index 00000000..522928f0 --- /dev/null +++ b/libsolidity/formal/Z3Interface.cpp @@ -0,0 +1,189 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#include <libsolidity/formal/Z3Interface.h> + +#include <libsolidity/interface/Exceptions.h> + +#include <libdevcore/CommonIO.h> + +using namespace std; +using namespace dev; +using namespace dev::solidity::smt; + +Z3Interface::Z3Interface(): + m_solver(m_context) +{ +} + +void Z3Interface::reset() +{ + m_constants.clear(); + m_functions.clear(); + m_solver.reset(); +} + +void Z3Interface::push() +{ + m_solver.push(); +} + +void Z3Interface::pop() +{ + m_solver.pop(); +} + +Expression Z3Interface::newFunction(string _name, Sort _domain, Sort _codomain) +{ + m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))}); + return SolverInterface::newFunction(move(_name), _domain, _codomain); +} + +Expression Z3Interface::newInteger(string _name) +{ + m_constants.insert({_name, m_context.int_const(_name.c_str())}); + return SolverInterface::newInteger(move(_name)); +} + +Expression Z3Interface::newBool(string _name) +{ + m_constants.insert({_name, m_context.bool_const(_name.c_str())}); + return SolverInterface::newBool(std::move(_name)); +} + +void Z3Interface::addAssertion(Expression const& _expr) +{ + m_solver.add(toZ3Expr(_expr)); +} + +pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate) +{ +// cout << "---------------------------------" << endl; +// cout << m_solver << endl; + CheckResult result; + switch (m_solver.check()) + { + case z3::check_result::sat: + result = CheckResult::SATISFIABLE; + cout << "sat" << endl; + break; + case z3::check_result::unsat: + result = CheckResult::UNSATISFIABLE; + cout << "unsat" << endl; + break; + case z3::check_result::unknown: + result = CheckResult::UNKNOWN; + cout << "unknown" << endl; + break; + default: + solAssert(false, ""); + } +// cout << "---------------------------------" << endl; + + + vector<string> values; + if (result != CheckResult::UNSATISFIABLE) + { + z3::model m = m_solver.get_model(); + for (Expression const& e: _expressionsToEvaluate) + values.push_back(toString(m.eval(toZ3Expr(e)))); + } + return make_pair(result, values); +} + +z3::expr Z3Interface::toZ3Expr(Expression const& _expr) +{ + if (_expr.arguments.empty() && m_constants.count(_expr.name)) + return m_constants.at(_expr.name); + z3::expr_vector arguments(m_context); + for (auto const& arg: _expr.arguments) + arguments.push_back(toZ3Expr(arg)); + + static map<string, unsigned> arity{ + {"ite", 3}, + {"not", 1}, + {"and", 2}, + {"or", 2}, + {"=", 2}, + {"<", 2}, + {"<=", 2}, + {">", 2}, + {">=", 2}, + {"+", 2}, + {"-", 2}, + {"*", 2}, + {">=", 2} + }; + string const& n = _expr.name; + if (m_functions.count(n)) + return m_functions.at(n)(arguments); + else if (m_constants.count(n)) + { + solAssert(arguments.empty(), ""); + return m_constants.at(n); + } + else if (arguments.empty()) + { + // We assume it is an integer... + return m_context.int_val(n.c_str()); + } + + assert(arity.count(n) && arity.at(n) == arguments.size()); + if (n == "ite") + return z3::ite(arguments[0], arguments[1], arguments[2]); + else if (n == "not") + return !arguments[0]; + else if (n == "and") + return arguments[0] && arguments[1]; + else if (n == "or") + return arguments[0] || arguments[1]; + else if (n == "=") + return arguments[0] == arguments[1]; + else if (n == "<") + return arguments[0] < arguments[1]; + else if (n == "<=") + return arguments[0] <= arguments[1]; + else if (n == ">") + return arguments[0] > arguments[1]; + else if (n == ">=") + return arguments[0] >= arguments[1]; + else if (n == "+") + return arguments[0] + arguments[1]; + else if (n == "-") + return arguments[0] - arguments[1]; + else if (n == "*") + return arguments[0] * arguments[1]; + // Cannot reach here. + solAssert(false, ""); + return arguments[0]; +} + +z3::sort Z3Interface::z3Sort(Sort _sort) +{ + switch (_sort) + { + case Sort::Bool: + return m_context.bool_sort(); + case Sort::Int: + return m_context.int_sort(); + default: + break; + } + solAssert(false, ""); + // Cannot be reached. + return m_context.int_sort(); +} diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h new file mode 100644 index 00000000..44d4bb2f --- /dev/null +++ b/libsolidity/formal/Z3Interface.h @@ -0,0 +1,65 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#pragma once + +#include <libsolidity/formal/SolverInterface.h> + +#include <boost/noncopyable.hpp> + +#include <z3++.h> + +namespace dev +{ +namespace solidity +{ +namespace smt +{ + +class Z3Interface: public SolverInterface, public boost::noncopyable +{ +public: + Z3Interface(); + + void reset() override; + + void push() override; + void pop() override; + + Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override; + Expression newInteger(std::string _name) override; + Expression newBool(std::string _name) override; + + void addAssertion(Expression const& _expr) override; + std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; + +private: + z3::expr toZ3Expr(Expression const& _expr); + z3::sort z3Sort(smt::Sort _sort); + + std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate); + std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end); + + z3::context m_context; + z3::solver m_solver; + std::map<std::string, z3::expr> m_constants; + std::map<std::string, z3::func_decl> m_functions; +}; + +} +} +} diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 412d2fd3..363f45dd 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -37,6 +37,7 @@ #include <libsolidity/analysis/PostTypeChecker.h> #include <libsolidity/analysis/SyntaxChecker.h> #include <libsolidity/codegen/Compiler.h> +#include <libsolidity/formal/SMTChecker.h> #include <libsolidity/interface/ABI.h> #include <libsolidity/interface/Natspec.h> #include <libsolidity/interface/GasEstimator.h> @@ -238,6 +239,13 @@ bool CompilerStack::analyze() if (noErrors) { + SMTChecker smtChecker(m_errorReporter, m_smtQuery); + for (Source const* source: m_sourceOrder) + smtChecker.analyze(*source->ast); + } + + if (noErrors) + { m_stackState = AnalysisSuccessful; return true; } @@ -527,17 +535,17 @@ StringMap CompilerStack::loadMissingSources(SourceUnit const& _ast, std::string if (m_sources.count(importPath) || newSources.count(importPath)) continue; - ReadFile::Result result{false, string("File not supplied initially.")}; + ReadCallback::Result result{false, string("File not supplied initially.")}; if (m_readFile) result = m_readFile(importPath); if (result.success) - newSources[importPath] = result.contentsOrErrorMessage; + newSources[importPath] = result.responseOrErrorMessage; else { m_errorReporter.parserError( import->location(), - string("Source \"" + importPath + "\" not found: " + result.contentsOrErrorMessage) + string("Source \"" + importPath + "\" not found: " + result.responseOrErrorMessage) ); continue; } diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index bb0f4126..361b8a45 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -82,7 +82,7 @@ public: /// Creates a new compiler stack. /// @param _readFile callback to used to read files for import statements. Must return /// and must not emit exceptions. - explicit CompilerStack(ReadFile::Callback const& _readFile = ReadFile::Callback()): + explicit CompilerStack(ReadCallback::Callback const& _readFile = ReadCallback::Callback()): m_readFile(_readFile), m_errorList(), m_errorReporter(m_errorList) {} @@ -287,7 +287,8 @@ private: std::string target; }; - ReadFile::Callback m_readFile; + ReadCallback::Callback m_readFile; + ReadCallback::Callback m_smtQuery; bool m_optimize = false; unsigned m_optimizeRuns = 200; std::map<std::string, h160> m_libraries; diff --git a/libsolidity/interface/ReadFile.h b/libsolidity/interface/ReadFile.h index 2e8a6bd8..7068629d 100644 --- a/libsolidity/interface/ReadFile.h +++ b/libsolidity/interface/ReadFile.h @@ -27,17 +27,17 @@ namespace dev namespace solidity { -class ReadFile: boost::noncopyable +class ReadCallback: boost::noncopyable { public: - /// File reading result. + /// File reading or generic query result. struct Result { bool success; - std::string contentsOrErrorMessage; + std::string responseOrErrorMessage; }; - /// File reading callback. + /// File reading or generic query callback. using Callback = std::function<Result(std::string const&)>; }; diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 7a6f9989..be823743 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -203,10 +203,10 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input) for (auto const& url: sources[sourceName]["urls"]) { - ReadFile::Result result = m_readFile(url.asString()); + ReadCallback::Result result = m_readFile(url.asString()); if (result.success) { - if (!hash.empty() && !hashMatchesContent(hash, result.contentsOrErrorMessage)) + if (!hash.empty() && !hashMatchesContent(hash, result.responseOrErrorMessage)) errors.append(formatError( false, "IOError", @@ -215,13 +215,13 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input) )); else { - m_compilerStack.addSource(sourceName, result.contentsOrErrorMessage); + m_compilerStack.addSource(sourceName, result.responseOrErrorMessage); found = true; break; } } else - failures.push_back("Cannot import url (\"" + url.asString() + "\"): " + result.contentsOrErrorMessage); + failures.push_back("Cannot import url (\"" + url.asString() + "\"): " + result.responseOrErrorMessage); } for (auto const& failure: failures) diff --git a/libsolidity/interface/StandardCompiler.h b/libsolidity/interface/StandardCompiler.h index d9787a40..11a0b4c2 100644 --- a/libsolidity/interface/StandardCompiler.h +++ b/libsolidity/interface/StandardCompiler.h @@ -40,7 +40,7 @@ public: /// Creates a new StandardCompiler. /// @param _readFile callback to used to read files for import statements. Must return /// and must not emit exceptions. - explicit StandardCompiler(ReadFile::Callback const& _readFile = ReadFile::Callback()) + explicit StandardCompiler(ReadCallback::Callback const& _readFile = ReadCallback::Callback()) : m_compilerStack(_readFile), m_readFile(_readFile) { } @@ -56,7 +56,7 @@ private: Json::Value compileInternal(Json::Value const& _input); CompilerStack m_compilerStack; - ReadFile::Callback m_readFile; + ReadCallback::Callback m_readFile; }; } diff --git a/scripts/install_deps.sh b/scripts/install_deps.sh index 24cf49d5..3a1abe10 100755 --- a/scripts/install_deps.sh +++ b/scripts/install_deps.sh @@ -115,7 +115,7 @@ case $(uname -s) in echo "Installing solidity dependencies on FreeBSD." echo "ERROR - 'install_deps.sh' doesn't have FreeBSD support yet." echo "Please let us know if you see this error message, and we can work out what is missing." - echo "Drop us a message at https://gitter.im/ethereum/solidity." + echo "Drop us a message at https://gitter.im/ethereum/solidity-dev." exit 1 ;; @@ -167,6 +167,7 @@ case $(uname -s) in Debian) #Debian + install_z3="" case $(lsb_release -cs) in wheezy) #wheezy @@ -174,7 +175,7 @@ case $(uname -s) in echo "ERROR - 'install_deps.sh' doesn't have Debian Wheezy support yet." echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions." echo "If you would like to get 'install_deps.sh' working for Debian Wheezy, that would be fantastic." - echo "Drop us a message at https://gitter.im/ethereum/solidity." + echo "Drop us a message at https://gitter.im/ethereum/solidity-dev." echo "See also https://github.com/ethereum/webthree-umbrella/issues/495 where we are working through Alpine support." exit 1 ;; @@ -185,20 +186,19 @@ case $(uname -s) in stretch) #stretch echo "Installing solidity dependencies on Debian Stretch (9.x)." - echo "ERROR - 'install_deps.sh' doesn't have Debian Stretch support yet." - echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions." - echo "If you would like to get 'install_deps.sh' working for Debian Stretch, that would be fantastic." - echo "Drop us a message at https://gitter.im/ethereum/solidity." - exit 1 + install_z3="libz3-dev" + ;; + buster) + #buster + echo "Installing solidity dependencies on Debian Buster (10.x)." + install_z3="libz3-dev" ;; *) #other Debian echo "Installing solidity dependencies on unknown Debian version." - echo "ERROR - Debian Jessie is the only Debian version which solidity has been tested on." - echo "If you are using a different release and would like to get 'install_deps.sh'" - echo "working for that release that would be fantastic." - echo "Drop us a message at https://gitter.im/ethereum/solidity." - exit 1 + echo "ERROR - This might not work, but we are trying anyway." + echo "Drop us a message at https://gitter.im/ethereum/solidity-dev" + install_z3="libz3-dev" ;; esac @@ -211,7 +211,9 @@ case $(uname -s) in gcc \ git \ libboost-all-dev \ - unzip + unzip \ + "$install_z3" + ;; @@ -267,6 +269,7 @@ case $(uname -s) in Ubuntu) #Ubuntu + install_z3="" case $(lsb_release -cs) in trusty) #trusty @@ -287,22 +290,25 @@ case $(uname -s) in xenial) #xenial echo "Installing solidity dependencies on Ubuntu Xenial Xerus (16.04)." + install_z3="libz3-dev" ;; yakkety) #yakkety echo "Installing solidity dependencies on Ubuntu Yakkety Yak (16.10)." - echo "" - echo "NOTE - You are in unknown territory with this preview OS." - echo "We will need to update the Ethereum PPAs, work through build and runtime breaks, etc." - echo "See https://github.com/ethereum/webthree-umbrella/issues/624." - echo "If you would like to partner with us to work through these, that" - echo "would be fantastic. Please just comment on that issue. Thanks!" + install_z3="libz3-dev" + ;; + zesty) + #zesty + echo "Installing solidity dependencies on Ubuntu Zesty (17.04)." + install_z3="libz3-dev" ;; *) #other Ubuntu echo "ERROR - Unknown or unsupported Ubuntu version (" $(lsb_release -cs) ")" - echo "We only support Trusty, Utopic, Vivid, Wily and Xenial, with work-in-progress on Yakkety." - exit 1 + echo "ERROR - This might not work, but we are trying anyway." + echo "Please drop us a message at https://gitter.im/ethereum/solidity-dev." + echo "We only support Trusty, Utopic, Vivid, Wily, Xenial and Yakkety." + install_z3="libz3-dev" ;; esac @@ -311,7 +317,8 @@ case $(uname -s) in build-essential \ cmake \ git \ - libboost-all-dev + libboost-all-dev \ + "$install_z3" if [ "$CI" = true ]; then # Install 'eth', for use in the Solidity Tests-over-IPC. # We will not use this 'eth', but its dependencies @@ -375,7 +382,7 @@ case $(uname -s) in echo "ERROR - Unsupported or unidentified Linux distro." echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions." echo "If you would like to get your distro working, that would be fantastic." - echo "Drop us a message at https://gitter.im/ethereum/solidity." + echo "Drop us a message at https://gitter.im/ethereum/solidity-dev." exit 1 ;; esac @@ -392,6 +399,6 @@ case $(uname -s) in echo "ERROR - Unsupported or unidentified operating system." echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions." echo "If you would like to get your operating system working, that would be fantastic." - echo "Drop us a message at https://gitter.im/ethereum/solidity." + echo "Drop us a message at https://gitter.im/ethereum/solidity-dev." ;; esac diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp index bfc53aef..315f951e 100644 --- a/solc/CommandLineInterface.cpp +++ b/solc/CommandLineInterface.cpp @@ -663,7 +663,7 @@ Allowed options)", bool CommandLineInterface::processInput() { - ReadFile::Callback fileReader = [this](string const& _path) + ReadCallback::Callback fileReader = [this](string const& _path) { try { @@ -683,25 +683,25 @@ bool CommandLineInterface::processInput() } } if (!isAllowed) - return ReadFile::Result{false, "File outside of allowed directories."}; + return ReadCallback::Result{false, "File outside of allowed directories."}; else if (!boost::filesystem::exists(path)) - return ReadFile::Result{false, "File not found."}; + return ReadCallback::Result{false, "File not found."}; else if (!boost::filesystem::is_regular_file(canonicalPath)) - return ReadFile::Result{false, "Not a valid file."}; + return ReadCallback::Result{false, "Not a valid file."}; else { auto contents = dev::contentsString(canonicalPath.string()); m_sourceCodes[path.string()] = contents; - return ReadFile::Result{true, contents}; + return ReadCallback::Result{true, contents}; } } catch (Exception const& _exception) { - return ReadFile::Result{false, "Exception in read callback: " + boost::diagnostic_information(_exception)}; + return ReadCallback::Result{false, "Exception in read callback: " + boost::diagnostic_information(_exception)}; } catch (...) { - return ReadFile::Result{false, "Unknown exception in read callback."}; + return ReadCallback::Result{false, "Unknown exception in read callback."}; } }; diff --git a/solc/jsonCompiler.cpp b/solc/jsonCompiler.cpp index ab928ac0..684d49e4 100644 --- a/solc/jsonCompiler.cpp +++ b/solc/jsonCompiler.cpp @@ -41,9 +41,9 @@ typedef void (*CStyleReadFileCallback)(char const* _path, char** o_contents, cha namespace { -ReadFile::Callback wrapReadCallback(CStyleReadFileCallback _readCallback = nullptr) +ReadCallback::Callback wrapReadCallback(CStyleReadFileCallback _readCallback = nullptr) { - ReadFile::Callback readCallback; + ReadCallback::Callback readCallback; if (_readCallback) { readCallback = [=](string const& _path) @@ -51,23 +51,23 @@ ReadFile::Callback wrapReadCallback(CStyleReadFileCallback _readCallback = nullp char* contents_c = nullptr; char* error_c = nullptr; _readCallback(_path.c_str(), &contents_c, &error_c); - ReadFile::Result result; + ReadCallback::Result result; result.success = true; if (!contents_c && !error_c) { result.success = false; - result.contentsOrErrorMessage = "File not found."; + result.responseOrErrorMessage = "File not found."; } if (contents_c) { result.success = true; - result.contentsOrErrorMessage = string(contents_c); + result.responseOrErrorMessage = string(contents_c); free(contents_c); } if (error_c) { result.success = false; - result.contentsOrErrorMessage = string(error_c); + result.responseOrErrorMessage = string(error_c); free(error_c); } return result; |