diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index a376bba9f..81e86e621 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -77,6 +77,8 @@ set(sources codegen/ir/IRLValue.h formal/BMC.cpp formal/BMC.h + formal/CHC.cpp + formal/CHC.h formal/CHCSolverInterface.h formal/EncodingContext.cpp formal/EncodingContext.h diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 21a001d04..16160a186 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -43,12 +43,13 @@ BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map const& _scanner) +void BMC::analyze(SourceUnit const& _source, shared_ptr const& _scanner, set _safeAssertions) { solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), ""); m_scanner = _scanner; + m_safeAssertions += move(_safeAssertions); m_context.setSolver(m_interface); m_context.clear(); m_variableUsage.setFunctionInlining(true); @@ -673,13 +674,14 @@ void BMC::checkBalance(VerificationTarget& _target) void BMC::checkAssert(VerificationTarget& _target) { solAssert(_target.type == VerificationTarget::Type::Assert, ""); - checkCondition( - _target.constraints && !_target.value, - _target.callStack, - _target.modelExpressions, - _target.expression->location(), - "Assertion violation" - ); + if (!m_safeAssertions.count(_target.expression)) + checkCondition( + _target.constraints && !_target.value, + _target.callStack, + _target.modelExpressions, + _target.expression->location(), + "Assertion violation" + ); } void BMC::addVerificationTarget( diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 28ea2117e..dff0f5f71 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -36,6 +36,7 @@ #include #include +#include #include #include @@ -55,7 +56,7 @@ class BMC: public SMTEncoder public: BMC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses); - void analyze(SourceUnit const& _sources, std::shared_ptr const& _scanner); + void analyze(SourceUnit const& _sources, std::shared_ptr const& _scanner, std::set _safeAssertions); /// This is used if the SMT solver is not directly linked into this binary. /// @returns a list of inputs to the SMT solver that were not part of the argument to @@ -175,6 +176,9 @@ private: std::vector m_verificationTargets; + /// Assertions that are known to be safe. + std::set m_safeAssertions; + std::shared_ptr m_interface; }; diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp new file mode 100644 index 000000000..9301a5b2b --- /dev/null +++ b/libsolidity/formal/CHC.cpp @@ -0,0 +1,178 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#include + +#ifdef HAVE_Z3 +#include +#endif + +#include + +#include + +using namespace std; +using namespace dev; +using namespace langutil; +using namespace dev::solidity; + +CHC::CHC(smt::EncodingContext& _context, ErrorReporter& _errorReporter): + SMTEncoder(_context), +#ifdef HAVE_Z3 + m_interface(make_shared()), +#endif + m_outerErrorReporter(_errorReporter) +{ +} + +void CHC::analyze(SourceUnit const& _source, shared_ptr const& _scanner) +{ + solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), ""); + + m_scanner = _scanner; + +#ifdef HAVE_Z3 + auto z3Interface = dynamic_pointer_cast(m_interface); + solAssert(z3Interface, ""); + m_context.setSolver(z3Interface->z3Interface()); + m_context.clear(); + m_variableUsage.setFunctionInlining(false); + + _source.accept(*this); +#endif +} + +bool CHC::visit(ContractDefinition const& _contract) +{ + if (!shouldVisit(_contract)) + return false; + + reset(); + + if (!SMTEncoder::visit(_contract)) + return false; + + return true; +} + +void CHC::endVisit(ContractDefinition const& _contract) +{ + if (!shouldVisit(_contract)) + return; + + SMTEncoder::endVisit(_contract); +} + +bool CHC::visit(FunctionDefinition const& _function) +{ + if (!shouldVisit(_function)) + return false; + + solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented"); + m_currentFunction = &_function; + + SMTEncoder::visit(*m_currentFunction); + + return false; +} + +void CHC::endVisit(FunctionDefinition const& _function) +{ + if (!shouldVisit(_function)) + return; + + solAssert(m_currentFunction == &_function, "Inlining internal function calls not yet implemented"); + m_currentFunction = nullptr; + + SMTEncoder::endVisit(_function); +} + +bool CHC::visit(IfStatement const& _if) +{ + solAssert(m_currentFunction, ""); + + SMTEncoder::visit(_if); + + return false; +} + +void CHC::endVisit(FunctionCall const& _funCall) +{ + solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, ""); + + if (_funCall.annotation().kind == FunctionCallKind::FunctionCall) + { + FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); + if (funType.kind() == FunctionType::Kind::Assert) + visitAssert(_funCall); + } + + SMTEncoder::endVisit(_funCall); +} + +void CHC::visitAssert(FunctionCall const&) +{ +} + +void CHC::reset() +{ + m_verificationTargets.clear(); + m_safeAssertions.clear(); +} + +bool CHC::shouldVisit(ContractDefinition const& _contract) const +{ + if ( + _contract.isLibrary() || + _contract.isInterface() + ) + return false; + return true; +} + +bool CHC::shouldVisit(FunctionDefinition const& _function) const +{ + if ( + _function.isPublic() && + _function.isImplemented() + ) + return true; + return false; +} + +bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location) +{ + smt::CheckResult result; + vector values; + tie(result, values) = m_interface->query(_query); + switch (result) + { + case smt::CheckResult::SATISFIABLE: + break; + case smt::CheckResult::UNSATISFIABLE: + return true; + case smt::CheckResult::UNKNOWN: + break; + case smt::CheckResult::CONFLICTING: + m_outerErrorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound."); + break; + case smt::CheckResult::ERROR: + m_outerErrorReporter.warning(_location, "Error trying to invoke SMT solver."); + break; + } + return false; +} diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h new file mode 100644 index 000000000..ffbc8cd19 --- /dev/null +++ b/libsolidity/formal/CHC.h @@ -0,0 +1,100 @@ +/* + 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 . +*/ + +/** + * Model checker based on Constrained Horn Clauses. + * + * A Solidity contract's CFG is encoded into a system of Horn clauses where + * each block has a predicate and edges are rules. + * + * The entry block is the constructor which has no in-edges. + * The constructor has one out-edge to an artificial block named _Interface_ + * which has in/out-edges from/to all public functions. + * + * Loop invariants for Interface -> Interface' are state invariants. + */ + +#pragma once + +#include + +#include + +#include + +namespace dev +{ +namespace solidity +{ + +class CHC: public SMTEncoder +{ +public: + CHC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter); + + void analyze(SourceUnit const& _sources, std::shared_ptr const& _scanner); + + std::set const& safeAssertions() const { return m_safeAssertions; } + +private: + /// Visitor functions. + //@{ + bool visit(ContractDefinition const& _node) override; + void endVisit(ContractDefinition const& _node) override; + bool visit(FunctionDefinition const& _node) override; + void endVisit(FunctionDefinition const& _node) override; + bool visit(IfStatement const& _node) override; + void endVisit(FunctionCall const& _node) override; + + void visitAssert(FunctionCall const& _funCall); + //@} + + /// Helpers. + //@{ + void reset(); + bool shouldVisit(ContractDefinition const& _contract) const; + bool shouldVisit(FunctionDefinition const& _function) const; + //@} + + /// Solver related. + //@{ + /// @returns true if query is unsatisfiable (safe). + bool query(smt::Expression const& _query, langutil::SourceLocation const& _location); + //@} + + /// Verification targets. + //@{ + std::vector m_verificationTargets; + + /// Assertions proven safe. + std::set m_safeAssertions; + //@} + + /// Control-flow. + //@{ + FunctionDefinition const* m_currentFunction = nullptr; + //@} + + /// CHC solver. + std::shared_ptr m_interface; + + /// ErrorReporter that comes from CompilerStack. + langutil::ErrorReporter& m_outerErrorReporter; +}; + +} +} diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index 51eb29024..e4b0ba35d 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -24,6 +24,7 @@ using namespace dev::solidity; ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map const& _smtlib2Responses): m_bmc(m_context, _errorReporter, _smtlib2Responses), + m_chc(m_context, _errorReporter), m_context() { } @@ -33,7 +34,8 @@ void ModelChecker::analyze(SourceUnit const& _source, shared_ptr const& if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) return; - m_bmc.analyze(_source, _scanner); + m_chc.analyze(_source, _scanner); + m_bmc.analyze(_source, _scanner, m_chc.safeAssertions()); } vector ModelChecker::unhandledQueries() diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index 96e8be910..f9ad23e5f 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -23,6 +23,7 @@ #pragma once #include +#include #include #include @@ -56,6 +57,9 @@ private: /// Bounded Model Checker engine. BMC m_bmc; + /// Constrained Horn Clauses engine. + CHC m_chc; + /// Stores the context of the encoding. smt::EncodingContext m_context; }; diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json index 780a15a2d..06a8f0be4 100644 --- a/test/libsolidity/smtCheckerTestsJSON/multi.json +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -3,9 +3,9 @@ { "smtlib2responses": { - "0x6e5cf865938b82f1627009d26ecb4c59e9b8c05cc1024ccf548b9b94c1c73e56": "unsat\n", - "0x890d45bd5b96d51c4d11683bcf3b7547cea993b3e15961c216a0a782d5d3ccb2": "sat\n((|EVALEXPR_0| 0))\n", - "0xa649be28767cedec4a7b7f5591e3fb237447405a823dbd861869eb35d91bebce": "sat\n((|EVALEXPR_0| 1))\n" + "0x0e5da3eca3d435940329103801b225604b2117438acea19504f980c5c1aaa571": "sat\n((|EVALEXPR_0| 0))\n", + "0xb83649564ec7bcc0c986c9c9c9d3fc28d90ad276ed2a6605fd48d10d30bef5e6": "sat\n((|EVALEXPR_0| 1))\n", + "0xeb8a2252226643551271abef0bc6c5c68b3a12fa509ad78a687c2cf76ddb4148": "unsat\n" } } } diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json index 4f0cafbac..9a362fd55 100644 --- a/test/libsolidity/smtCheckerTestsJSON/simple.json +++ b/test/libsolidity/smtCheckerTestsJSON/simple.json @@ -3,7 +3,7 @@ { "smtlib2responses": { - "0xcae00c08b91a968103a89431c473645366101a2b037d72aa10fbe3099ccd6931": "sat\n((|EVALEXPR_0| 0))\n" + "0x9804531ddd39e0d6df2dcb24d8dfd9e7b8c7ed3ece5d33f1680063d3e02f18f0": "sat\n((|EVALEXPR_0| 0))\n" } } }