diff options
Diffstat (limited to 'libsolidity')
| -rw-r--r-- | libsolidity/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | libsolidity/ast/AST.cpp | 1 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 36 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 45 | ||||
| -rw-r--r-- | libsolidity/formal/SMTCheckerImpl.cpp | 456 | ||||
| -rw-r--r-- | libsolidity/formal/SMTCheckerImpl.h | 99 | ||||
| -rw-r--r-- | libsolidity/interface/CompilerStack.cpp | 8 |
7 files changed, 646 insertions, 1 deletions
diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 11fd6fe2..a88d16b8 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -3,4 +3,4 @@ file(GLOB_RECURSE sources "*.cpp" "../libjulia/*.cpp") file(GLOB_RECURSE headers "*.h" "../libjulia/*.h") add_library(solidity ${sources} ${headers}) -target_link_libraries(solidity PUBLIC evmasm devcore) +target_link_libraries(solidity PUBLIC evmasm devcore z3) 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/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp new file mode 100644 index 00000000..0e559fae --- /dev/null +++ b/libsolidity/formal/SMTChecker.cpp @@ -0,0 +1,36 @@ +/* + 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> + +#include <libsolidity/formal/SMTCheckerImpl.h> + +#include <libsolidity/interface/ErrorReporter.h> + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SMTChecker::SMTChecker(ErrorReporter& _errorReporter): + m_impl(make_shared<SMTCheckerImpl>(_errorReporter)) +{ +} + +void SMTChecker::analyze(SourceUnit const& _source) +{ + m_impl->analyze(_source); +} diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h new file mode 100644 index 00000000..7e7ee3d9 --- /dev/null +++ b/libsolidity/formal/SMTChecker.h @@ -0,0 +1,45 @@ +/* + 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 <map> +#include <string> +#include <memory> + +namespace dev +{ +namespace solidity +{ + +class ErrorReporter; +class SourceUnit; +class SMTCheckerImpl; + +class SMTChecker +{ +public: + SMTChecker(ErrorReporter& _errorReporter); + + void analyze(SourceUnit const& _sources); + +private: + std::shared_ptr<SMTCheckerImpl> m_impl; +}; + +} +} diff --git a/libsolidity/formal/SMTCheckerImpl.cpp b/libsolidity/formal/SMTCheckerImpl.cpp new file mode 100644 index 00000000..0a9ad66e --- /dev/null +++ b/libsolidity/formal/SMTCheckerImpl.cpp @@ -0,0 +1,456 @@ +/* + 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_solver(m_context), + 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_solver.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_solver.push(); + return true; +} + +void SMTCheckerImpl::endVisit(FunctionDefinition const&) +{ + // TOOD we could check for "reachability", i.e. satisfiability here. + m_solver.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_solver.add(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_solver.add(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_solver.add(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_solver.add(expr(*args[0])); + } + else if (funType.kind() == FunctionType::Kind::Require) + { + solAssert(args.size() == 1, ""); + solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); + m_solver.add(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_solver.add(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_solver.add(expr(_literal) == m_context.int_val(type.literalValue(&_literal).str().c_str())); + } + 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, ""); + z3::expr left(expr(_op.leftExpression())); + z3::expr right(expr(_op.rightExpression())); + Token::Value op = _op.getOperator(); + z3::expr 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_solver.add(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) + { + z3::expr left(expr(_op.leftExpression())); + z3::expr right(expr(_op.rightExpression())); + Token::Value op = _op.getOperator(); + z3::expr 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_solver.add(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_solver.add(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression())); + else + m_solver.add(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( + z3::expr _condition, + SourceLocation const& _location, + string const& _description, + string const& _additionalValueName, + z3::expr* _additionalValue +) +{ + m_solver.push(); + m_solver.add(_condition); + switch (m_solver.check()) + { + case z3::check_result::sat: + { + std::ostringstream message; + message << _description << " happens here"; + if (m_currentFunction) + { + message << " for:\n"; + z3::model m = m_solver.get_model(); + if (_additionalValue) + message << " " << _additionalValueName << " = " << m.eval(*_additionalValue) << "\n"; + for (auto const& param: m_currentFunction->parameters()) + if (knownVariable(*param)) + message << " " << param->name() << " = " << m.eval(currentValue(*param)) << "\n"; + for (auto const& var: m_currentFunction->localVariables()) + if (knownVariable(*var)) + message << " " << var->name() << " = " << m.eval(currentValue(*var)) << "\n"; +// message << m << endl; +// message << m_solver << endl; + } + else + message << "."; + m_errorReporter.warning(_location, message.str()); + break; + } + case z3::check_result::unsat: + break; + case z3::check_result::unknown: + m_errorReporter.warning(_location, _description + " might happen here."); + break; + } + m_solver.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_context.function(uniqueSymbol(_varDecl).c_str(), m_context.int_sort(), m_context.int_sort())); + if (_setToZero) + m_solver.add(currentValue(_varDecl) == 0); + else + { + m_solver.add(currentValue(_varDecl) >= minValue(*intType)); + m_solver.add(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); +} + +z3::expr SMTCheckerImpl::currentValue(Declaration const& _decl) +{ + solAssert(m_currentSequenceCounter.count(&_decl), ""); + return var(_decl)(m_currentSequenceCounter.at(&_decl)); +} + +z3::expr SMTCheckerImpl::newValue(const Declaration& _decl) +{ + solAssert(m_currentSequenceCounter.count(&_decl), ""); + m_currentSequenceCounter[&_decl]++; + return currentValue(_decl); +} + +z3::expr SMTCheckerImpl::minValue(IntegerType const& _t) +{ + return m_context.int_val(_t.minValue().str().c_str()); +} + +z3::expr SMTCheckerImpl::maxValue(IntegerType const& _t) +{ + return m_context.int_val(_t.maxValue().str().c_str()); +} + +z3::expr 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_context.int_const(uniqueSymbol(_e).c_str())); + break; + } + case Type::Category::Integer: + m_z3Expressions.emplace(&_e, m_context.int_const(uniqueSymbol(_e).c_str())); + break; + case Type::Category::Bool: + m_z3Expressions.emplace(&_e, m_context.bool_const(uniqueSymbol(_e).c_str())); + break; + default: + solAssert(false, "Type not implemented."); + } + } + return m_z3Expressions.at(&_e); +} + +z3::func_decl 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 new file mode 100644 index 00000000..a82ec92a --- /dev/null +++ b/libsolidity/formal/SMTCheckerImpl.h @@ -0,0 +1,99 @@ +/* + 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 <z3++.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( + z3::expr _condition, + SourceLocation const& _location, + std::string const& _description, + std::string const& _additionalValueName = "", + z3::expr* _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); + z3::expr currentValue(Declaration const& _decl); + z3::expr newValue(Declaration const& _decl); + + z3::expr minValue(IntegerType const& _t); + z3::expr maxValue(IntegerType const& _t); + + /// Returns the z3 expression corresponding to the AST node. Creates a new expression + /// if it does not exist yet. + z3::expr expr(Expression const& _e); + /// Returns the z3 function declaration corresponding to the given variable. + /// The function takes one argument which is the "sequence number". + z3::func_decl var(Declaration const& _decl); + + z3::context m_context; + z3::solver m_solver; + std::map<Declaration const*, int> m_currentSequenceCounter; + std::map<Expression const*, z3::expr> m_z3Expressions; + std::map<Declaration const*, z3::func_decl> m_z3Variables; + ErrorReporter& m_errorReporter; + + FunctionDefinition const* m_currentFunction = nullptr; +}; + +} +} diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 412d2fd3..4283cd99 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); + for (Source const* source: m_sourceOrder) + smtChecker.analyze(*source->ast); + } + + if (noErrors) + { m_stackState = AnalysisSuccessful; return true; } |