diff options
Diffstat (limited to 'libsolidity/formal')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 53 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 | ||||
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.cpp | 21 | ||||
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.h | 127 | ||||
| -rw-r--r-- | libsolidity/formal/SolverInterface.h | 168 |
5 files changed, 225 insertions, 148 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 76232c2e..a8ad60ed 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -17,6 +17,7 @@ #include <libsolidity/formal/SMTChecker.h> +#include <libsolidity/formal/SMTLib2Interface.h> #include <libsolidity/interface/ErrorReporter.h> @@ -25,7 +26,7 @@ using namespace dev; using namespace dev::solidity; SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadFile::Callback const& _readFileCallback): - m_interface(_readFileCallback), + m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)), m_errorReporter(_errorReporter) { } @@ -39,7 +40,7 @@ void SMTChecker::analyze(SourceUnit const& _source) pragmaFound = true; if (pragmaFound) { - m_interface.reset(); + m_interface->reset(); m_currentSequenceCounter.clear(); _source.accept(*this); } @@ -69,7 +70,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function) ); // TODO actually we probably also have to reset all local variables and similar things. m_currentFunction = &_function; - m_interface.push(); + m_interface->push(); return true; } @@ -79,7 +80,7 @@ void SMTChecker::endVisit(FunctionDefinition const&) // We only handle local variables, so we clear everything. // If we add storage variables, those should be cleared differently. m_currentSequenceCounter.clear(); - m_interface.pop(); + m_interface->pop(); m_currentFunction = nullptr; } @@ -93,7 +94,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl) 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())); + m_interface->addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue())); else m_errorReporter.warning( _varDecl.location(), @@ -123,7 +124,7 @@ void SMTChecker::endVisit(Assignment const& _assignment) 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())); + m_interface->addAssertion(newValue(*decl) == expr(_assignment.rightHandSide())); else m_errorReporter.warning( _assignment.location(), @@ -145,7 +146,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) "Assertion checker does not yet implement tules and inline arrays." ); else - m_interface.addAssertion(expr(_tuple) == expr(*_tuple.components()[0])); + m_interface->addAssertion(expr(_tuple) == expr(*_tuple.components()[0])); } void SMTChecker::endVisit(BinaryOperation const& _op) @@ -173,13 +174,13 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) 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])); + 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])); + 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. @@ -192,7 +193,7 @@ void SMTChecker::endVisit(Identifier const& _identifier) solAssert(decl, ""); if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get())) { - m_interface.addAssertion(expr(_identifier) == currentValue(*decl)); + m_interface->addAssertion(expr(_identifier) == currentValue(*decl)); return; } else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get())) @@ -217,7 +218,7 @@ void SMTChecker::endVisit(Literal const& _literal) if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type)) solAssert(!rational->isFractional(), ""); - m_interface.addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal))); + m_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal))); } else m_errorReporter.warning( @@ -264,7 +265,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) &value ); - m_interface.addAssertion(expr(_op) == value); + m_interface->addAssertion(expr(_op) == value); break; } default: @@ -292,7 +293,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op) /*op == Token::GreaterThanOrEqual*/ (left >= right) ); // TODO: check that other values for op are not possible. - m_interface.addAssertion(expr(_op) == value); + m_interface->addAssertion(expr(_op) == value); } else m_errorReporter.warning( @@ -308,9 +309,9 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op) if (_op.annotation().commonType->category() == Type::Category::Bool) { if (_op.getOperator() == Token::And) - m_interface.addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression())); + m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression())); else - m_interface.addAssertion(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression())); + m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression())); } else m_errorReporter.warning( @@ -327,8 +328,8 @@ void SMTChecker::checkCondition( smt::Expression* _additionalValue ) { - m_interface.push(); - m_interface.addAssertion(_condition); + m_interface->push(); + m_interface->addAssertion(_condition); vector<smt::Expression> expressionsToEvaluate; if (m_currentFunction) @@ -344,7 +345,7 @@ void SMTChecker::checkCondition( } smt::CheckResult result; vector<string> values; - tie(result, values) = m_interface.check(expressionsToEvaluate); + tie(result, values) = m_interface->check(expressionsToEvaluate); switch (result) { case smt::CheckResult::SAT: @@ -380,7 +381,7 @@ void SMTChecker::checkCondition( default: solAssert(false, ""); } - m_interface.pop(); + m_interface->pop(); } void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero) @@ -390,13 +391,13 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo 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)); + m_z3Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); if (_setToZero) - m_interface.addAssertion(currentValue(_varDecl) == 0); + m_interface->addAssertion(currentValue(_varDecl) == 0); else { - m_interface.addAssertion(currentValue(_varDecl) >= minValue(*intType)); - m_interface.addAssertion(currentValue(_varDecl) <= maxValue(*intType)); + m_interface->addAssertion(currentValue(_varDecl) >= minValue(*intType)); + m_interface->addAssertion(currentValue(_varDecl) <= maxValue(*intType)); } } else @@ -455,14 +456,14 @@ smt::Expression SMTChecker::expr(Expression const& _e) { if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get())) solAssert(!rational->isFractional(), ""); - m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e))); + m_z3Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); break; } case Type::Category::Integer: - m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e))); + m_z3Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); break; case Type::Category::Bool: - m_z3Expressions.emplace(&_e, m_interface.newBool(uniqueSymbol(_e))); + m_z3Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); break; default: solAssert(false, "Type not implemented."); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 8c6a2327..afe5897d 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -18,7 +18,7 @@ #pragma once #include <libsolidity/ast/ASTVisitor.h> -#include <libsolidity/formal/SMTLib2Interface.h> +#include <libsolidity/formal/SolverInterface.h> #include <libsolidity/interface/ReadFile.h> #include <map> @@ -85,7 +85,7 @@ private: /// The function takes one argument which is the "sequence number". smt::Expression var(Declaration const& _decl); - smt::SMTLib2Interface m_interface; + std::shared_ptr<smt::SolverInterface> 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; diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index 63ab1679..8cc4da66 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -71,24 +71,24 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom (_codomain == Sort::Int ? "Int" : "Bool") + ")" ); - return Expression(std::move(_name), {}); + return SolverInterface::newFunction(move(_name), _domain, _codomain); } Expression SMTLib2Interface::newInteger(string _name) { write("(declare-const |" + _name + "| Int)"); - return Expression(std::move(_name), {}); + return SolverInterface::newInteger(move(_name)); } Expression SMTLib2Interface::newBool(string _name) { write("(declare-const |" + _name + "| Bool)"); - return Expression(std::move(_name), {}); + return SolverInterface::newBool(std::move(_name)); } void SMTLib2Interface::addAssertion(Expression const& _expr) { - write("(assert " + _expr.toSExpr() + ")"); + write("(assert " + toSExpr(_expr) + ")"); } pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate) @@ -114,6 +114,17 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con 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(), ""); @@ -133,7 +144,7 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _ 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 += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n"; } command += "(check-sat)\n"; command += "(get-value ("; diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index d8c11df9..5755ae3f 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -18,6 +18,7 @@ #pragma once #include <libsolidity/formal/SMTSolverCommunicator.h> +#include <libsolidity/formal/SolverInterface.h> #include <libsolidity/interface/Exceptions.h> #include <libsolidity/interface/ReadFile.h> @@ -38,129 +39,26 @@ namespace solidity namespace smt { -enum class CheckResult -{ - SAT, UNSAT, UNKNOWN, ERROR -}; - -enum class Sort -{ - Int, Bool -}; - -/// C++ representation of an SMTLIB2 expression. -class Expression -{ - friend class SMTLib2Interface; - /// Manual constructor, should only be used by SMTLib2Interface and the class itself. - Expression(std::string _name, std::vector<Expression> _arguments): - m_name(std::move(_name)), m_arguments(std::move(_arguments)) {} - -public: - Expression(size_t _number): m_name(std::to_string(_number)) {} - Expression(u256 const& _number): m_name(_number.str()) {} - Expression(bigint const& _number): m_name(_number.str()) {} - - Expression(Expression const& _other) = default; - Expression(Expression&& _other) = default; - Expression& operator=(Expression const& _other) = default; - Expression& operator=(Expression&& _other) = default; - - 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(m_arguments.empty(), "Attempted function application to non-function."); - return Expression(m_name, _a); - } - - std::string toSExpr() const - { - if (m_arguments.empty()) - return m_name; - std::string sexpr = "(" + m_name; - for (auto const& arg: m_arguments) - sexpr += " " + arg.toSExpr(); - sexpr += ")"; - return sexpr; - } - -private: - 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)}) {} - - std::string const m_name; - std::vector<Expression> const m_arguments; -}; - -class SMTLib2Interface: public boost::noncopyable +class SMTLib2Interface: public SolverInterface, public boost::noncopyable { public: SMTLib2Interface(ReadFile::Callback const& _readFileCallback); - void reset(); + void reset() override; - void push(); - void pop(); + void push() override; + void pop() override; - Expression newFunction(std::string _name, Sort _domain, Sort _codomain); - Expression newInteger(std::string _name); - Expression newBool(std::string _name); + 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); - std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate); + 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); @@ -170,7 +68,6 @@ private: std::vector<std::string> m_accumulatedOutput; }; - } } } diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h new file mode 100644 index 00000000..e9fa5cc7 --- /dev/null +++ b/libsolidity/formal/SolverInterface.h @@ -0,0 +1,168 @@ +/* + 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/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> +#include <cstdio> + +namespace dev +{ +namespace solidity +{ +namespace smt +{ + +enum class CheckResult +{ + SAT, UNSAT, 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; + + 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)}) {} +}; + +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; + + virtual std::pair<CheckResult, std::vector<std::string>> + check(std::vector<Expression> const& _expressionsToEvaluate) = 0; +}; + + +} +} +} |