diff options
| -rw-r--r-- | cmake/UseSolidity.cmake | 2 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 447 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 65 | ||||
| -rw-r--r-- | libsolidity/formal/SMTCheckerImpl.cpp | 469 | ||||
| -rw-r--r-- | libsolidity/formal/SMTCheckerImpl.h | 97 | ||||
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.cpp | 168 | ||||
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.h | 29 | ||||
| -rw-r--r-- | libsolidity/formal/SMTSolverCommunicator.cpp | 75 | ||||
| -rw-r--r-- | libsolidity/formal/SMTSolverCommunicator.h | 50 | ||||
| -rw-r--r-- | libsolidity/interface/CompilerStack.cpp | 2 |
10 files changed, 687 insertions, 717 deletions
diff --git a/cmake/UseSolidity.cmake b/cmake/UseSolidity.cmake index 9e2dea3e..5080f71b 100644 --- a/cmake/UseSolidity.cmake +++ b/cmake/UseSolidity.cmake @@ -25,7 +25,7 @@ function(eth_apply TARGET REQUIRED SUBMODULE) if (${SUBMODULE} STREQUAL "solidity" OR ${SUBMODULE} STREQUAL "") eth_use(${TARGET} ${REQUIRED} Dev::soldevcore Solidity::solevmasm) - target_link_libraries(${TARGET} ${Solidity_SOLIDITY_LIBRARIES} z3) + target_link_libraries(${TARGET} ${Solidity_SOLIDITY_LIBRARIES}) endif() target_compile_definitions(${TARGET} PUBLIC ETH_SOLIDITY) diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 0e559fae..b9e0e8f3 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -17,7 +17,6 @@ #include <libsolidity/formal/SMTChecker.h> -#include <libsolidity/formal/SMTCheckerImpl.h> #include <libsolidity/interface/ErrorReporter.h> @@ -25,12 +24,452 @@ using namespace std; using namespace dev; using namespace dev::solidity; -SMTChecker::SMTChecker(ErrorReporter& _errorReporter): - m_impl(make_shared<SMTCheckerImpl>(_errorReporter)) +SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadFile::Callback const& _readFileCallback): + m_interface(_readFileCallback), + m_errorReporter(_errorReporter) { } void SMTChecker::analyze(SourceUnit const& _source) { - m_impl->analyze(_source); + bool pragmaFound = false; + for (auto const& node: _source.nodes()) + if (auto const* pragma = dynamic_cast<PragmaDirective const*>(node.get())) + if (pragma->literals()[0] == "checkAssertionsZ3") + pragmaFound = true; + if (pragmaFound) + { + m_interface.reset(); + m_currentSequenceCounter.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. + m_interface.pop(); + m_currentFunction = nullptr; +} + +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]) && _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 " + intType.minValue().str() + ")", + "value", + &value + ); + checkCondition( + value > maxValue(intType), + _op.location(), + "Overflow (resulting value larger than " + intType.maxValue().str() + ")", + "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; + if (m_currentFunction) + { + if (_additionalValue) + expressionsToEvaluate.emplace_back(*_additionalValue); + for (auto const& param: m_currentFunction->parameters()) + if (knownVariable(*param)) + expressionsToEvaluate.emplace_back(currentValue(*param)); + for (auto const& var: m_currentFunction->localVariables()) + if (knownVariable(*var)) + expressionsToEvaluate.emplace_back(currentValue(*var)); + } + smt::CheckResult result; + vector<string> values; + tie(result, values) = m_interface.check(expressionsToEvaluate); + switch (result) + { + case smt::CheckResult::SAT: + { + std::ostringstream message; + message << _description << " happens here"; + size_t i = 0; + if (m_currentFunction) + { + message << " for:\n"; + if (_additionalValue) + message << " " << _additionalValueName << " = " << values.at(i++) << "\n"; + for (auto const& param: m_currentFunction->parameters()) + if (knownVariable(*param)) + message << " " << param->name() << " = " << values.at(i++) << "\n"; + for (auto const& var: m_currentFunction->localVariables()) + if (knownVariable(*var)) + message << " " << var->name() << " = " << values.at(i++) << "\n"; + } + else + message << "."; + m_errorReporter.warning(_location, message.str()); + break; + } + case smt::CheckResult::UNSAT: + 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 (auto intType = dynamic_cast<IntegerType const*>(_varDecl.type().get())) + { + solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, ""); + solAssert(m_z3Variables.count(&_varDecl) == 0, ""); + m_currentSequenceCounter[&_varDecl] = 0; + m_z3Variables.emplace(&_varDecl, m_interface.newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); + if (_setToZero) + m_interface.addAssertion(currentValue(_varDecl) == 0); + else + { + m_interface.addAssertion(currentValue(_varDecl) >= minValue(*intType)); + m_interface.addAssertion(currentValue(_varDecl) <= maxValue(*intType)); + } + } + 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 var(_decl)(m_currentSequenceCounter.at(&_decl)); +} + +smt::Expression SMTChecker::newValue(const Declaration& _decl) +{ + solAssert(m_currentSequenceCounter.count(&_decl), ""); + m_currentSequenceCounter[&_decl]++; + return currentValue(_decl); +} + +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_z3Expressions.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_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e))); + break; + } + case Type::Category::Integer: + m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e))); + break; + case Type::Category::Bool: + m_z3Expressions.emplace(&_e, m_interface.newBool(uniqueSymbol(_e))); + break; + default: + solAssert(false, "Type not implemented."); + } + } + return m_z3Expressions.at(&_e); +} + +smt::Expression SMTChecker::var(Declaration const& _decl) +{ + solAssert(m_z3Variables.count(&_decl), ""); + return m_z3Variables.at(&_decl); } diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 7e7ee3d9..8c6a2327 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -17,9 +17,12 @@ #pragma once +#include <libsolidity/ast/ASTVisitor.h> +#include <libsolidity/formal/SMTLib2Interface.h> +#include <libsolidity/interface/ReadFile.h> + #include <map> #include <string> -#include <memory> namespace dev { @@ -27,18 +30,68 @@ namespace solidity { class ErrorReporter; -class SourceUnit; -class SMTCheckerImpl; -class SMTChecker +class SMTChecker: private ASTConstVisitor { public: - SMTChecker(ErrorReporter& _errorReporter); + SMTChecker(ErrorReporter& _errorReporter, ReadFile::Callback const& _readCallback); void analyze(SourceUnit const& _sources); private: - std::shared_ptr<SMTCheckerImpl> m_impl; + // 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 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); + + std::string uniqueSymbol(Declaration const& _decl); + std::string uniqueSymbol(Expression const& _expr); + bool knownVariable(Declaration const& _decl); + smt::Expression currentValue(Declaration const& _decl); + smt::Expression newValue(Declaration const& _decl); + + smt::Expression minValue(IntegerType const& _t); + 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); + + smt::SMTLib2Interface m_interface; + std::map<Declaration const*, int> m_currentSequenceCounter; + std::map<Expression const*, smt::Expression> m_z3Expressions; + std::map<Declaration const*, smt::Expression> m_z3Variables; + ErrorReporter& m_errorReporter; + + FunctionDefinition const* m_currentFunction = nullptr; }; } diff --git a/libsolidity/formal/SMTCheckerImpl.cpp b/libsolidity/formal/SMTCheckerImpl.cpp deleted file mode 100644 index b86a0279..00000000 --- a/libsolidity/formal/SMTCheckerImpl.cpp +++ /dev/null @@ -1,469 +0,0 @@ -/* - 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/SMTCheckerImpl.h> - - -#include <libsolidity/interface/ErrorReporter.h> - -using namespace std; -using namespace dev; -using namespace dev::solidity; - -SMTCheckerImpl::SMTCheckerImpl(ErrorReporter& _errorReporter): - m_errorReporter(_errorReporter) -{ -} - -void SMTCheckerImpl::analyze(SourceUnit const& _source) -{ - bool pragmaFound = false; - for (auto const& node: _source.nodes()) - if (auto const* pragma = dynamic_cast<PragmaDirective const*>(node.get())) - if (pragma->literals()[0] == "checkAssertionsZ3") - pragmaFound = true; - if (pragmaFound) - { - m_interface.reset(); - m_currentSequenceCounter.clear(); - _source.accept(*this); - } -} - -void SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::endVisit(FunctionDefinition const&) -{ - // TOOD we could check for "reachability", i.e. satisfiability here. - m_interface.pop(); - m_currentFunction = nullptr; -} - -void SMTCheckerImpl::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]) && _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 SMTCheckerImpl::endVisit(ExpressionStatement const&) -{ -} - -void SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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 " + intType.minValue().str() + ")", - "value", - &value - ); - checkCondition( - value > maxValue(intType), - _op.location(), - "Overflow (resulting value larger than " + intType.maxValue().str() + ")", - "value", - &value - ); - - m_interface.addAssertion(expr(_op) == value); - break; - } - default: - m_errorReporter.warning( - _op.location(), - "Assertion checker does not yet implement this operator." - ); - } -} - -void SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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; - if (m_currentFunction) - { - if (_additionalValue) - expressionsToEvaluate.emplace_back(*_additionalValue); - for (auto const& param: m_currentFunction->parameters()) - if (knownVariable(*param)) - expressionsToEvaluate.emplace_back(currentValue(*param)); - for (auto const& var: m_currentFunction->localVariables()) - if (knownVariable(*var)) - expressionsToEvaluate.emplace_back(currentValue(*var)); - } - smt::CheckResult result; - vector<string> values; - tie(result, values) = m_interface.check(expressionsToEvaluate); - switch (result) - { - case smt::CheckResult::SAT: - { - std::ostringstream message; - message << _description << " happens here"; - size_t i = 0; - if (m_currentFunction) - { - message << " for:\n"; - if (_additionalValue) - message << " " << _additionalValueName << " = " << values.at(i++) << "\n"; - for (auto const& param: m_currentFunction->parameters()) - if (knownVariable(*param)) - message << " " << param->name() << " = " << values.at(i++) << "\n"; - for (auto const& var: m_currentFunction->localVariables()) - if (knownVariable(*var)) - message << " " << var->name() << " = " << values.at(i++) << "\n"; - } - else - message << "."; - m_errorReporter.warning(_location, message.str()); - break; - } - case smt::CheckResult::UNSAT: - break; - case smt::CheckResult::UNKNOWN: - m_errorReporter.warning(_location, _description + " might happen here."); - break; - } - m_interface.pop(); -} - -void SMTCheckerImpl::createVariable(VariableDeclaration const& _varDecl, bool _setToZero) -{ - if (auto intType = dynamic_cast<IntegerType const*>(_varDecl.type().get())) - { - solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, ""); - solAssert(m_z3Variables.count(&_varDecl) == 0, ""); - m_currentSequenceCounter[&_varDecl] = 0; - m_z3Variables.emplace(&_varDecl, m_interface.newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); - if (_setToZero) - m_interface.addAssertion(currentValue(_varDecl) == 0); - else - { - m_interface.addAssertion(currentValue(_varDecl) >= minValue(*intType)); - m_interface.addAssertion(currentValue(_varDecl) <= maxValue(*intType)); - } - } - else - m_errorReporter.warning( - _varDecl.location(), - "Assertion checker does not yet support the type of this variable." - ); -} - -string SMTCheckerImpl::uniqueSymbol(Declaration const& _decl) -{ - return _decl.name() + "_" + to_string(_decl.id()); -} - -string SMTCheckerImpl::uniqueSymbol(Expression const& _expr) -{ - return "expr_" + to_string(_expr.id()); -} - -bool SMTCheckerImpl::knownVariable(Declaration const& _decl) -{ - return m_currentSequenceCounter.count(&_decl); -} - -smt::Expression SMTCheckerImpl::currentValue(Declaration const& _decl) -{ - solAssert(m_currentSequenceCounter.count(&_decl), ""); - return var(_decl)(m_currentSequenceCounter.at(&_decl)); -} - -smt::Expression SMTCheckerImpl::newValue(const Declaration& _decl) -{ - solAssert(m_currentSequenceCounter.count(&_decl), ""); - m_currentSequenceCounter[&_decl]++; - return currentValue(_decl); -} - -smt::Expression SMTCheckerImpl::minValue(IntegerType const& _t) -{ - return smt::Expression(_t.minValue()); -} - -smt::Expression SMTCheckerImpl::maxValue(IntegerType const& _t) -{ - return smt::Expression(_t.maxValue()); -} - -smt::Expression SMTCheckerImpl::expr(Expression const& _e) -{ - if (!m_z3Expressions.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_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e))); - break; - } - case Type::Category::Integer: - m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e))); - break; - case Type::Category::Bool: - m_z3Expressions.emplace(&_e, m_interface.newBool(uniqueSymbol(_e))); - break; - default: - solAssert(false, "Type not implemented."); - } - } - return m_z3Expressions.at(&_e); -} - -smt::Expression SMTCheckerImpl::var(Declaration const& _decl) -{ - solAssert(m_z3Variables.count(&_decl), ""); - return m_z3Variables.at(&_decl); -} diff --git a/libsolidity/formal/SMTCheckerImpl.h b/libsolidity/formal/SMTCheckerImpl.h deleted file mode 100644 index e5179440..00000000 --- a/libsolidity/formal/SMTCheckerImpl.h +++ /dev/null @@ -1,97 +0,0 @@ -/* - 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/SMTLib2Interface.h> - -#include <map> -#include <string> - -namespace dev -{ -namespace solidity -{ - -class ErrorReporter; - -class SMTCheckerImpl: private ASTConstVisitor -{ -public: - SMTCheckerImpl(ErrorReporter& _errorReporter); - - 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 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); - - std::string uniqueSymbol(Declaration const& _decl); - std::string uniqueSymbol(Expression const& _expr); - bool knownVariable(Declaration const& _decl); - smt::Expression currentValue(Declaration const& _decl); - smt::Expression newValue(Declaration const& _decl); - - smt::Expression minValue(IntegerType const& _t); - smt::Expression maxValue(IntegerType const& _t); - - /// Returns the z3 expression corresponding to the AST node. Creates a new expression - /// if it does not exist yet. - smt::Expression expr(Expression const& _e); - /// Returns the z3 function declaration corresponding to the given variable. - /// The function takes one argument which is the "sequence number". - smt::Expression var(Declaration const& _decl); - - smt::SMTLib2Interface m_interface; - std::map<Declaration const*, int> m_currentSequenceCounter; - std::map<Expression const*, smt::Expression> m_z3Expressions; - std::map<Declaration const*, smt::Expression> m_z3Variables; - ErrorReporter& m_errorReporter; - - FunctionDefinition const* m_currentFunction = nullptr; -}; - -} -} diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index 8d40c354..63ab1679 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -21,6 +21,7 @@ #include <boost/algorithm/string/predicate.hpp> #include <boost/algorithm/string/join.hpp> +#include <boost/filesystem/operations.hpp> #include <cstdio> #include <fstream> @@ -30,99 +31,31 @@ #include <string> #include <array> -#include <sys/types.h> -#include <unistd.h> -#include <stdio.h> -#include <stdlib.h> - using namespace std; using namespace dev; using namespace dev::solidity::smt; - -//namespace -//{ - -//void createSubprocess(FILE*& _readPipe, FILE*& _writePipe) -//{ -// int pipe_in[2]; /* This is the pipe with wich we write to the child process. */ -// int pipe_out[2]; /* This is the pipe with wich we read from the child process. */ - -// solAssert(!pipe(pipe_in) && !pipe(pipe_out), ""); - -// /* Attempt to fork and check for errors */ -// pid_t pid = fork(); -// solAssert(pid != -1, ""); - -// if (pid) -// { -// /* The parent has the non-zero PID. */ -// _readPipe = fdopen(pipe_out[0], "r"); -// _writePipe = fdopen(pipe_in[1], "w"); -// close(pipe_out[1]); -// close(pipe_in[0]); -// } -// else -// { -// /* The child has the zero pid returned by fork*/ -// cout << "child" << endl; -// solAssert(dup2(pipe_out[1], 1) != -1, ""); -// solAssert(dup2(pipe_in[0], 0) != -1, ""); -// solAssert(close(pipe_out[0]) == 0, ""); -// solAssert(close(pipe_out[1]) == 0, ""); -// solAssert(close(pipe_in[0]) == 0, ""); -// solAssert(close(pipe_in[1]) == 0, ""); -// execl("/usr/bin/z3", "z3", "-smt2", "-in", NULL); -// exit(1); /* Only reached if execl() failed */ -// } -//} - -//} - -SMTLib2Interface::SMTLib2Interface() +SMTLib2Interface::SMTLib2Interface(ReadFile::Callback const& _readFileCallback): + m_communicator(_readFileCallback) { - // TODO using pipes did not really work, so trying it the hard way for now. -// createSubprocess(m_solverWrite, m_solverRead); -// solAssert(m_solverWrite, "Unable to start Z3"); -// solAssert(m_solverRead, "Unable to start Z3"); -// write("(set-option :produce-models true)\n(set-logic QF_LIA)\n"); reset(); } -SMTLib2Interface::~SMTLib2Interface() -{ -// if (m_solverWrite) -// { -// write("(exit)\n"); -// fflush(m_solverWrite); -// fclose(m_solverWrite); -// m_solverWrite = nullptr; -// } -// if (m_solverRead) -// { -// fclose(m_solverRead); -// m_solverRead = nullptr; -// } -} - void SMTLib2Interface::reset() { -// write("(reset)\n"); -// write("(set-option :produce-models true)\n"); m_accumulatedOutput.clear(); m_accumulatedOutput.emplace_back(); - write("(set-option :produce-models true)\n(set-logic QF_UFLIA)\n"); + write("(set-option :produce-models true)"); + write("(set-logic QF_UFLIA)"); } void SMTLib2Interface::push() { m_accumulatedOutput.emplace_back(); - //write("(push)\n"); } void SMTLib2Interface::pop() { - //write("(pop)\n"); solAssert(!m_accumulatedOutput.empty(), ""); m_accumulatedOutput.pop_back(); } @@ -136,50 +69,34 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom (_domain == Sort::Int ? "Int" : "Bool") + ") " + (_codomain == Sort::Int ? "Int" : "Bool") + - ")\n" + ")" ); - return Expression(_name, {}); + return Expression(std::move(_name), {}); } Expression SMTLib2Interface::newInteger(string _name) { - write("(declare-const |" + _name + "| Int)\n"); - return Expression(_name, {}); + write("(declare-const |" + _name + "| Int)"); + return Expression(std::move(_name), {}); } Expression SMTLib2Interface::newBool(string _name) { - write("(declare-const |" + _name + "| Bool)\n"); - return Expression(_name, {}); + write("(declare-const |" + _name + "| Bool)"); + return Expression(std::move(_name), {}); } -void SMTLib2Interface::addAssertion(Expression _expr) +void SMTLib2Interface::addAssertion(Expression const& _expr) { - write("(assert " + _expr.toSExpr() + ")\n"); + write("(assert " + _expr.toSExpr() + ")"); } pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate) { - string checks; - if (_expressionsToEvaluate.empty()) - checks = "(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... - checks += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n"; - checks += "(assert (= |EVALEXPR_" + to_string(i) + "| " + e.toSExpr() + "))\n"; - } - checks += "(check-sat)\n"; - checks += "(get-value ("; - for (size_t i = 0; i < _expressionsToEvaluate.size(); i++) - checks += "|EVALEXPR_" + to_string(i) + "| "; - checks += "))\n"; - } - string response = communicate(boost::algorithm::join(m_accumulatedOutput, "\n") + checks); + string response = m_communicator.communicate( + boost::algorithm::join(m_accumulatedOutput, "\n") + + checkSatAndGetValuesCommand(_expressionsToEvaluate) + ); CheckResult result; // TODO proper parsing if (boost::starts_with(response, "sat\n")) @@ -189,44 +106,43 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con else if (boost::starts_with(response, "unknown\n")) result = CheckResult::UNKNOWN; else - solAssert(false, "Invalid response to check-sat: " + response); + result = CheckResult::ERROR; vector<string> values; - if (result != CheckResult::UNSAT) + if (result != CheckResult::UNSAT && result != CheckResult::ERROR) values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend()); return make_pair(result, values); } -//string SMTLib2Interface::eval(Expression _expr) -//{ -// write("(get-value (" + _expr.toSExpr() + ")\n"); -// std::string reply = communicate(); -// cout << "<-- Z3: " << reply << endl; -// // TODO parse -// return reply; -//} - void SMTLib2Interface::write(string _data) { -// cout << " --> Z3: " << _data << endl; -// solAssert(m_solverWrite, ""); -// solAssert(fputs(_data.c_str(), m_solverWrite) >= 0 || true, "EOF while communicating with Z3."); -// solAssert(fflush(m_solverWrite) == 0 || true, ""); solAssert(!m_accumulatedOutput.empty(), ""); - m_accumulatedOutput.back() += move(_data); + m_accumulatedOutput.back() += move(_data) + "\n"; } -string SMTLib2Interface::communicate(std::string const& _input) +string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate) { - ofstream("/tmp/z3exchange.smt2") << _input << "(exit)" << endl; - FILE* solverOutput = popen("z3 -smt2 /tmp/z3exchange.smt2", "r"); - string result; - array<char, 128> buffer; - while (!feof(solverOutput)) - if (fgets(buffer.data(), 127, solverOutput) != nullptr) - result += buffer.data(); - fclose(solverOutput); - return result; + 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) + "| " + e.toSExpr() + "))\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) diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index b7bab043..d8c11df9 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -17,10 +17,15 @@ #pragma once +#include <libsolidity/formal/SMTSolverCommunicator.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> @@ -35,7 +40,7 @@ namespace smt enum class CheckResult { - SAT, UNSAT, UNKNOWN + SAT, UNSAT, UNKNOWN, ERROR }; enum class Sort @@ -43,6 +48,7 @@ enum class Sort Int, Bool }; +/// C++ representation of an SMTLIB2 expression. class Expression { friend class SMTLib2Interface; @@ -62,23 +68,23 @@ public: friend Expression operator!(Expression _a) { - return Expression("not", _a); + return Expression("not", std::move(_a)); } friend Expression operator&&(Expression _a, Expression _b) { - return Expression("and", _a, _b); + return Expression("and", std::move(_a), std::move(_b)); } friend Expression operator||(Expression _a, Expression _b) { - return Expression("or", _a, _b); + return Expression("or", std::move(_a), std::move(_b)); } friend Expression operator==(Expression _a, Expression _b) { - return Expression("=", _a, _b); + return Expression("=", std::move(_a), std::move(_b)); } friend Expression operator!=(Expression _a, Expression _b) { - return !(_a == _b); + return !(std::move(_a) == std::move(_b)); } friend Expression operator<(Expression _a, Expression _b) { @@ -140,8 +146,7 @@ private: class SMTLib2Interface: public boost::noncopyable { public: - SMTLib2Interface(); - ~SMTLib2Interface(); + SMTLib2Interface(ReadFile::Callback const& _readFileCallback); void reset(); @@ -152,19 +157,17 @@ public: Expression newInteger(std::string _name); Expression newBool(std::string _name); - void addAssertion(Expression _expr); + void addAssertion(Expression const& _expr); std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate); -// std::string eval(Expression _expr); private: void write(std::string _data); - std::string communicate(std::string const& _input); + std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate); std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end); + SMTSolverCommunicator m_communicator; std::vector<std::string> m_accumulatedOutput; -// FILE* m_solverWrite = nullptr; -// FILE* m_solverRead = nullptr; }; diff --git a/libsolidity/formal/SMTSolverCommunicator.cpp b/libsolidity/formal/SMTSolverCommunicator.cpp new file mode 100644 index 00000000..a97e5fcc --- /dev/null +++ b/libsolidity/formal/SMTSolverCommunicator.cpp @@ -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/>. +*/ + +#include <libsolidity/formal/SMTSolverCommunicator.h> + +#include <libdevcore/Common.h> + +#include <boost/filesystem/operations.hpp> + +#include <fstream> + +#include <stdio.h> + +using namespace std; +using namespace dev; +using namespace dev::solidity::smt; + +#ifdef EMSCRIPTEN + +string SMTSolverCommunicator::communicate(string const& _input) +{ + auto result = m_readFileCallback("SMTLIB2Solver>> " + _input); + if (result.success) + return result.contentsOrErrorMessage; + else + return ""; +} + +#else + +#ifndef _WIN32 +inline FILE* _popen(char const* command, char const* type) +{ + return popen(command, type); +} +inline int _pclose(FILE* file) +{ + return pclose(file); +} +#endif + +string SMTSolverCommunicator::communicate(string const& _input) +{ + namespace fs = boost::filesystem; + auto tempPath = fs::unique_path(fs::temp_directory_path() / "%%%%-%%%%-%%%%.smt2"); + ScopeGuard s1([&]() { fs::remove(tempPath); }); + ofstream(tempPath.string()) << _input << "(exit)" << endl; + + // TODO Escaping might not be 100% perfect. + FILE* solverOutput = _popen(("z3 -smt2 \"" + tempPath.string() + "\"").c_str(), "r"); + ScopeGuard s2([&]() { _pclose(solverOutput); }); + + string result; + array<char, 128> buffer; + while (!feof(solverOutput)) + if (fgets(buffer.data(), 127, solverOutput) != nullptr) + result += buffer.data(); + return result; +} + +#endif diff --git a/libsolidity/formal/SMTSolverCommunicator.h b/libsolidity/formal/SMTSolverCommunicator.h new file mode 100644 index 00000000..25aeba61 --- /dev/null +++ b/libsolidity/formal/SMTSolverCommunicator.h @@ -0,0 +1,50 @@ +/* + 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/ReadFile.h> + +#include <string> + +namespace dev +{ +namespace solidity +{ +namespace smt +{ + +/// Platform-specific way to access the SMT solver. +class SMTSolverCommunicator +{ +public: + /// Creates the communicator, the read file callback is used only + /// on the emscripten platform. + SMTSolverCommunicator(ReadFile::Callback const& _readFileCallback): + m_readFileCallback(_readFileCallback) + {} + + std::string communicate(std::string const& _input); + +private: + ReadFile::Callback m_readFileCallback; +}; + + +} +} +} diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 4283cd99..50e20b3d 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -239,7 +239,7 @@ bool CompilerStack::analyze() if (noErrors) { - SMTChecker smtChecker(m_errorReporter); + SMTChecker smtChecker(m_errorReporter, m_readFile); for (Source const* source: m_sourceOrder) smtChecker.analyze(*source->ast); } |