From 3bee348525de032cdc510dc62b7366c90cf13d89 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 11 Feb 2020 22:52:35 -0300 Subject: [PATCH] Change CHC encoding to functions forest instead of explicit CFG --- libsolidity/formal/CHC.cpp | 385 +++++++++++++----- libsolidity/formal/CHC.h | 77 +++- libsolidity/formal/EncodingContext.h | 1 + libsolidity/formal/ModelChecker.cpp | 4 +- libsolidity/formal/ModelChecker.h | 6 +- libsolidity/formal/Z3Interface.h | 6 +- .../functions/library_constant.sol | 26 ++ .../functions/library_constant_2.sol | 9 + .../invariants/loop_nested.sol | 5 + .../invariants/loop_nested_for.sol | 5 + ...r_loop_array_assignment_storage_memory.sol | 6 +- ..._loop_array_assignment_storage_storage.sol | 8 +- .../operators/delete_array_index_2d.sol | 4 +- 13 files changed, 426 insertions(+), 116 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/functions/library_constant.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/library_constant_2.sol diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 25201474b..af50b2722 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -27,6 +27,8 @@ #include +#include + using namespace std; using namespace solidity; using namespace solidity::langutil; @@ -75,16 +77,39 @@ void CHC::analyze(SourceUnit const& _source) m_context.setAssertionAccumulation(false); m_variableUsage.setFunctionInlining(false); + resetSourceAnalysis(); + auto boolSort = make_shared(smt::Kind::Bool); auto genesisSort = make_shared( vector(), boolSort ); m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis"); - auto genesis = (*m_genesisPredicate)({}); - addRule(genesis, genesis.name); + addRule(genesis(), "genesis"); - _source.accept(*this); + set sources; + sources.insert(&_source); + for (auto const& source: _source.referencedSourceUnits(true)) + sources.insert(source); + for (auto const* source: sources) + defineInterfacesAndSummaries(*source); + for (auto const* source: sources) + source->accept(*this); + + for (auto const& [scope, target]: m_verificationTargets) + { + auto assertions = transactionAssertions(scope); + for (auto const* assertion: assertions) + { + createErrorBlock(); + connectBlocks(target.value, error(), target.constraints && (target.errorId == assertion->id())); + auto [result, model] = query(error(), assertion->location()); + // This should be fine but it's a bug in the old compiler + (void)model; + if (result == smt::CheckResult::UNSATISFIABLE) + m_safeAssertions.insert(assertion); + } + } } vector CHC::unhandledQueries() const @@ -97,26 +122,15 @@ vector CHC::unhandledQueries() const bool CHC::visit(ContractDefinition const& _contract) { - if (!shouldVisit(_contract)) - return false; - - reset(); + resetContractAnalysis(); initContract(_contract); - m_stateVariables = _contract.stateVariablesIncludingInherited(); - - for (auto const& var: m_stateVariables) - // SMT solvers do not support function types as arguments. - if (var->type()->category() == Type::Category::Function) - m_stateSorts.push_back(make_shared(smt::Kind::Int)); - else - m_stateSorts.push_back(smt::smtSort(*var->type())); + m_stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract); + m_stateSorts = stateSorts(_contract); clearIndices(&_contract); - string suffix = _contract.name() + "_" + to_string(_contract.id()); - m_interfacePredicate = createSymbolicBlock(interfaceSort(), "interface_" + suffix); // TODO create static instances for Bool/Int sorts in SolverInterface. auto boolSort = make_shared(smt::Kind::Bool); @@ -125,10 +139,12 @@ bool CHC::visit(ContractDefinition const& _contract) boolSort ); + string suffix = _contract.name() + "_" + to_string(_contract.id()); m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error_" + suffix); - m_constructorPredicate = createSymbolicBlock(constructorSort(), "implicit_constructor_" + to_string(_contract.id())); + m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix); + m_implicitConstructorPredicate = createSymbolicBlock(interfaceSort(), "implicit_constructor_" + suffix); auto stateExprs = currentStateVariables(); - setCurrentBlock(*m_interfacePredicate, &stateExprs); + setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs); SMTEncoder::visit(_contract); return false; @@ -136,33 +152,33 @@ bool CHC::visit(ContractDefinition const& _contract) void CHC::endVisit(ContractDefinition const& _contract) { - if (!shouldVisit(_contract)) - return; - for (auto const& var: m_stateVariables) { solAssert(m_context.knownVariable(*var), ""); + auto const& symbVar = m_context.variable(*var); + symbVar->resetIndex(); m_context.setZeroValue(*var); + symbVar->increaseIndex(); } - auto genesisPred = (*m_genesisPredicate)({}); - auto implicitConstructor = (*m_constructorPredicate)(currentStateVariables()); - connectBlocks(genesisPred, implicitConstructor); + auto implicitConstructor = (*m_implicitConstructorPredicate)(initialStateVariables()); + connectBlocks(genesis(), implicitConstructor); m_currentBlock = implicitConstructor; + m_context.addAssertion(m_error.currentValue() == 0); if (auto constructor = _contract.constructor()) constructor->accept(*this); else inlineConstructorHierarchy(_contract); - connectBlocks(m_currentBlock, interface()); + auto summary = predicate(*m_constructorSummaryPredicate, vector{m_error.currentValue()} + currentStateVariables()); + connectBlocks(m_currentBlock, summary); - for (unsigned i = 0; i < m_verificationTargets.size(); ++i) - { - auto const& target = m_verificationTargets.at(i); - auto errorAppl = error(i + 1); - if (query(errorAppl, target->location())) - m_safeAssertions.insert(target); - } + clearIndices(m_currentContract, nullptr); + auto stateExprs = vector{m_error.currentValue()} + currentStateVariables(); + setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs); + + addVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue()); + connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0); SMTEncoder::endVisit(_contract); } @@ -182,7 +198,7 @@ bool CHC::visit(FunctionDefinition const& _function) return false; } - solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented"); + solAssert(!m_currentFunction, "Function inlining should not happen in CHC."); m_currentFunction = &_function; initFunction(_function); @@ -193,7 +209,17 @@ bool CHC::visit(FunctionDefinition const& _function) auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables()); auto bodyPred = predicate(*bodyBlock); - connectBlocks(m_currentBlock, functionPred); + if (_function.isConstructor()) + connectBlocks(m_currentBlock, functionPred); + else + connectBlocks(genesis(), functionPred); + + m_context.addAssertion(m_error.currentValue() == 0); + for (auto const* var: m_stateVariables) + m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var)); + for (auto const& var: _function.parameters()) + m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var)); + connectBlocks(functionPred, bodyPred); setCurrentBlock(*bodyBlock); @@ -225,18 +251,30 @@ void CHC::endVisit(FunctionDefinition const& _function) // This is done in endVisit(ContractDefinition). if (_function.isConstructor()) { - auto constructorExit = createSymbolicBlock(interfaceSort(), "constructor_exit_" + to_string(_function.id())); - connectBlocks(m_currentBlock, predicate(*constructorExit, currentStateVariables())); + string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id()); + auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix); + connectBlocks(m_currentBlock, predicate(*constructorExit, vector{m_error.currentValue()} + currentStateVariables())); + clearIndices(m_currentContract, m_currentFunction); - auto stateExprs = currentStateVariables(); + auto stateExprs = vector{m_error.currentValue()} + currentStateVariables(); setCurrentBlock(*constructorExit, &stateExprs); } else { - connectBlocks(m_currentBlock, interface()); - clearIndices(m_currentContract, m_currentFunction); - auto stateExprs = currentStateVariables(); - setCurrentBlock(*m_interfacePredicate, &stateExprs); + auto assertionError = m_error.currentValue(); + auto sum = summary(_function); + connectBlocks(m_currentBlock, sum); + + auto iface = interface(); + + auto stateExprs = initialStateVariables(); + setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs); + + if (_function.isPublic()) + { + addVerificationTarget(&_function, m_currentBlock, sum, assertionError); + connectBlocks(m_currentBlock, iface, sum && (assertionError == 0)); + } } m_currentFunction = nullptr; } @@ -468,12 +506,23 @@ void CHC::visitAssert(FunctionCall const& _funCall) solAssert(args.size() == 1, ""); solAssert(args.front()->annotation().type->category() == Type::Category::Bool, ""); - createErrorBlock(); + solAssert(m_currentContract, ""); + solAssert(m_currentFunction, ""); + if (m_currentFunction->isConstructor()) + m_functionAssertions[m_currentContract].insert(&_funCall); + else + m_functionAssertions[m_currentFunction].insert(&_funCall); - smt::Expression assertNeg = !(m_context.expression(*args.front())->currentValue()); - connectBlocks(m_currentBlock, error(), currentPathConditions() && assertNeg); + auto previousError = m_error.currentValue(); + m_error.increaseIndex(); - m_verificationTargets.push_back(&_funCall); + connectBlocks( + m_currentBlock, + m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction), + currentPathConditions() && !m_context.expression(*args.front())->currentValue() && (m_error.currentValue() == _funCall.id()) + ); + + m_context.addAssertion(m_error.currentValue() == previousError); } void CHC::unknownFunctionCall(FunctionCall const&) @@ -488,15 +537,23 @@ void CHC::unknownFunctionCall(FunctionCall const&) m_unknownFunctionCallSeen = true; } -void CHC::reset() +void CHC::resetSourceAnalysis() +{ + m_verificationTargets.clear(); + m_safeAssertions.clear(); + m_functionAssertions.clear(); + m_callGraph.clear(); + m_summaries.clear(); +} + +void CHC::resetContractAnalysis() { m_stateSorts.clear(); m_stateVariables.clear(); - m_verificationTargets.clear(); - m_safeAssertions.clear(); m_unknownFunctionCallSeen = false; m_breakDest = nullptr; m_continueDest = nullptr; + m_error.resetIndex(); } void CHC::eraseKnowledge() @@ -521,17 +578,6 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c } } - -bool CHC::shouldVisit(ContractDefinition const& _contract) const -{ - if ( - _contract.isLibrary() || - _contract.isInterface() - ) - return false; - return true; -} - bool CHC::shouldVisit(FunctionDefinition const& _function) const { if ( @@ -547,7 +593,8 @@ void CHC::setCurrentBlock( vector const* _arguments ) { - m_context.popSolver(); + if (m_context.solverStackHeigh() > 0) + m_context.popSolver(); solAssert(m_currentContract, ""); clearIndices(m_currentContract, m_currentFunction); m_context.pushSolver(); @@ -557,10 +604,42 @@ void CHC::setCurrentBlock( m_currentBlock = predicate(_block); } +set CHC::transactionAssertions(ASTNode const* _txRoot) +{ + set assertions; + solidity::util::BreadthFirstSearch{{_txRoot}}.run([&](auto const* function, auto&& _addChild) { + assertions.insert(m_functionAssertions[function].begin(), m_functionAssertions[function].end()); + for (auto const* called: m_callGraph[function]) + _addChild(called); + }); + return assertions; +} + +vector CHC::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract) +{ + vector stateVars; + for (auto const& contract: _contract.annotation().linearizedBaseContracts) + for (auto var: contract->stateVariables()) + stateVars.push_back(var); + return stateVars; +} + +vector CHC::stateSorts(ContractDefinition const& _contract) +{ + vector stateSorts; + for (auto const& var: stateVariablesIncludingInheritedAndPrivate(_contract)) + stateSorts.push_back(smt::smtSortAbstractFunction(*var->type())); + return stateSorts; +} + smt::SortPointer CHC::constructorSort() { - // TODO this will change once we support function calls. - return interfaceSort(); + auto boolSort = make_shared(smt::Kind::Bool); + auto intSort = make_shared(smt::Kind::Int); + return make_shared( + vector{intSort} + m_stateSorts, + boolSort + ); } smt::SortPointer CHC::interfaceSort() @@ -572,20 +651,38 @@ smt::SortPointer CHC::interfaceSort() ); } +smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract) +{ + auto boolSort = make_shared(smt::Kind::Bool); + return make_shared( + stateSorts(_contract), + boolSort + ); +} + +/// A function in the symbolic CFG requires: +/// - Index of failed assertion. 0 means no assertion failed. +/// - 2 sets of state variables: +/// - State variables at the beginning of the current function, immutable +/// - Current state variables +/// At the beginning of the function these must equal set 1 +/// - 2 sets of input variables: +/// - Input variables at the beginning of the current function, immutable +/// - Current input variables +/// At the beginning of the function these must equal set 1 +/// - 1 set of output variables smt::SortPointer CHC::sort(FunctionDefinition const& _function) { auto boolSort = make_shared(smt::Kind::Bool); - vector varSorts; - for (auto const& var: _function.parameters() + _function.returnParameters()) - { - // SMT solvers do not support function types as arguments. - if (var->type()->category() == Type::Category::Function) - varSorts.push_back(make_shared(smt::Kind::Int)); - else - varSorts.push_back(smt::smtSort(*var->type())); - } + auto intSort = make_shared(smt::Kind::Int); + vector inputSorts; + for (auto const& var: _function.parameters()) + inputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); + vector outputSorts; + for (auto const& var: _function.returnParameters()) + outputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); return make_shared( - m_stateSorts + varSorts, + vector{intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts, boolSort ); } @@ -601,19 +698,31 @@ smt::SortPointer CHC::sort(ASTNode const* _node) auto boolSort = make_shared(smt::Kind::Bool); vector varSorts; for (auto const& var: m_currentFunction->localVariables()) - { - // SMT solvers do not support function types as arguments. - if (var->type()->category() == Type::Category::Function) - varSorts.push_back(make_shared(smt::Kind::Int)); - else - varSorts.push_back(smt::smtSort(*var->type())); - } + varSorts.push_back(smt::smtSortAbstractFunction(*var->type())); return make_shared( fSort->domain + varSorts, boolSort ); } +smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract) +{ + auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract); + auto sorts = stateSorts(_contract); + + auto boolSort = make_shared(smt::Kind::Bool); + auto intSort = make_shared(smt::Kind::Int); + vector inputSorts, outputSorts; + for (auto const& var: _function.parameters()) + inputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); + for (auto const& var: _function.returnParameters()) + outputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); + return make_shared( + vector{intSort} + sorts + inputSorts + sorts + outputSorts, + boolSort + ); +} + unique_ptr CHC::createSymbolicBlock(smt::SortPointer _sort, string const& _name) { auto block = make_unique( @@ -625,12 +734,33 @@ unique_ptr CHC::createSymbolicBlock(smt::SortPoin return block; } +void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) +{ + for (auto const& node: _source.nodes()) + if (auto const* contract = dynamic_cast(node.get())) + for (auto const* base: contract->annotation().linearizedBaseContracts) + { + string suffix = base->name() + "_" + to_string(base->id()); + m_interfaces[base] = createSymbolicBlock(interfaceSort(*base), "interface_" + suffix); + for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base)) + if (!m_context.knownVariable(*var)) + createVariable(*var); + for (auto const* function: base->definedFunctions()) + m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract)); + } +} + smt::Expression CHC::interface() { vector paramExprs; for (auto const& var: m_stateVariables) paramExprs.push_back(m_context.variable(*var)->currentValue()); - return (*m_interfacePredicate)(paramExprs); + return (*m_interfaces.at(m_currentContract))(paramExprs); +} + +smt::Expression CHC::interface(ContractDefinition const& _contract) +{ + return (*m_interfaces.at(&_contract))(stateVariablesAtIndex(0, _contract)); } smt::Expression CHC::error() @@ -643,6 +773,27 @@ smt::Expression CHC::error(unsigned _idx) return m_errorPredicate->functionValueAtIndex(_idx)({}); } +smt::Expression CHC::summary(ContractDefinition const&) +{ + return (*m_constructorSummaryPredicate)( + vector{m_error.currentValue()} + + currentStateVariables() + ); +} + +smt::Expression CHC::summary(FunctionDefinition const& _function) +{ + vector args{m_error.currentValue()}; + auto contract = _function.annotation().contract; + args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables(); + for (auto const& var: _function.parameters()) + args.push_back(m_context.variable(*var)->valueAtIndex(0)); + args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables(); + for (auto const& var: _function.returnParameters()) + args.push_back(m_context.variable(*var)->currentValue()); + return (*m_summaries.at(m_currentContract).at(&_function))(args); +} + unique_ptr CHC::createBlock(ASTNode const* _node, string const& _prefix) { return createSymbolicBlock(sort(_node), @@ -653,6 +804,15 @@ unique_ptr CHC::createBlock(ASTNode const* _node, predicateName(_node)); } +unique_ptr CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract) +{ + return createSymbolicBlock(summarySort(_function, _contract), + "summary_" + + uniquePrefix() + + "_" + + predicateName(&_function, &_contract)); +} + void CHC::createErrorBlock() { solAssert(m_errorPredicate, ""); @@ -669,6 +829,28 @@ void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to addRule(edge, _from.name + "_to_" + _to.name); } +vector CHC::initialStateVariables() +{ + return stateVariablesAtIndex(0); +} + +vector CHC::stateVariablesAtIndex(int _index) +{ + solAssert(m_currentContract, ""); + vector exprs; + for (auto const& var: m_stateVariables) + exprs.push_back(m_context.variable(*var)->valueAtIndex(_index)); + return exprs; +} + +vector CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract) +{ + vector exprs; + for (auto const& var: stateVariablesIncludingInheritedAndPrivate(_contract)) + exprs.push_back(m_context.variable(*var)->valueAtIndex(_index)); + return exprs; +} + vector CHC::currentStateVariables() { solAssert(m_currentContract, ""); @@ -680,11 +862,22 @@ vector CHC::currentStateVariables() vector CHC::currentFunctionVariables() { - vector paramExprs; - if (m_currentFunction) - for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters()) - paramExprs.push_back(m_context.variable(*var)->currentValue()); - return currentStateVariables() + paramExprs; + vector initInputExprs; + vector mutableInputExprs; + for (auto const& var: m_currentFunction->parameters()) + { + initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0)); + mutableInputExprs.push_back(m_context.variable(*var)->currentValue()); + } + vector returnExprs; + for (auto const& var: m_currentFunction->returnParameters()) + returnExprs.push_back(m_context.variable(*var)->currentValue()); + return vector{m_error.currentValue()} + + initialStateVariables() + + initInputExprs + + currentStateVariables() + + mutableInputExprs + + returnExprs; } vector CHC::currentBlockVariables() @@ -696,7 +889,7 @@ vector CHC::currentBlockVariables() return currentFunctionVariables() + paramExprs; } -string CHC::predicateName(ASTNode const* _node) +string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contract) { string prefix; if (auto funDef = dynamic_cast(_node)) @@ -705,7 +898,12 @@ string CHC::predicateName(ASTNode const* _node) if (!funDef->name().empty()) prefix += "_" + funDef->name() + "_"; } - return prefix + to_string(_node->id()); + else if (m_currentFunction && !m_currentFunction->name().empty()) + prefix += m_currentFunction->name(); + + auto contract = _contract ? _contract : m_currentContract; + solAssert(contract, ""); + return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id()); } smt::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block) @@ -726,7 +924,7 @@ void CHC::addRule(smt::Expression const& _rule, string const& _ruleName) m_interface->addRule(_rule, _ruleName); } -bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location) +pair> CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location) { smt::CheckResult result; vector values; @@ -736,7 +934,7 @@ bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _ case smt::CheckResult::SATISFIABLE: break; case smt::CheckResult::UNSATISFIABLE: - return true; + break; case smt::CheckResult::UNKNOWN: break; case smt::CheckResult::CONFLICTING: @@ -746,7 +944,12 @@ bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _ m_outerErrorReporter.warning(_location, "Error trying to invoke SMT solver."); break; } - return false; + return {result, values}; +} + +void CHC::addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId) +{ + m_verificationTargets.emplace(_scope, CHCVerificationTarget{{VerificationTarget::Type::Assert, _from, _constraints}, _errorId}); } string CHC::uniquePrefix() diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 6f912fbd8..889c21b6a 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -79,22 +79,38 @@ private: void unknownFunctionCall(FunctionCall const& _funCall); //@} + struct IdCompare + { + bool operator()(ASTNode const* lhs, ASTNode const* rhs) const + { + return lhs->id() < rhs->id(); + } + }; + /// Helpers. //@{ - void reset(); + void resetSourceAnalysis(); + void resetContractAnalysis(); void eraseKnowledge(); void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override; - bool shouldVisit(ContractDefinition const& _contract) const; bool shouldVisit(FunctionDefinition const& _function) const; void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector const* _arguments = nullptr); + std::set transactionAssertions(ASTNode const* _txRoot); + static std::vector stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract); //@} /// Sort helpers. //@{ + static std::vector stateSorts(ContractDefinition const& _contract); smt::SortPointer constructorSort(); smt::SortPointer interfaceSort(); + static smt::SortPointer interfaceSort(ContractDefinition const& _const); smt::SortPointer sort(FunctionDefinition const& _function); smt::SortPointer sort(ASTNode const* _block); + /// @returns the sort of a predicate that represents the summary of _function in the scope of _contract. + /// The _contract is also needed because the same function might be in many contracts due to inheritance, + /// where the sort changes because the set of state variables might change. + static smt::SortPointer summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract); //@} /// Predicate helpers. @@ -102,14 +118,24 @@ private: /// @returns a new block of given _sort and _name. std::unique_ptr createSymbolicBlock(smt::SortPointer _sort, std::string const& _name); + /// Creates summary predicates for all functions of all contracts + /// in a given _source. + void defineInterfacesAndSummaries(SourceUnit const& _source); + + /// Genesis predicate. + smt::Expression genesis() { return (*m_genesisPredicate)({}); } /// Interface predicate over current variables. smt::Expression interface(); + smt::Expression interface(ContractDefinition const& _contract); /// Error predicate over current variables. smt::Expression error(); smt::Expression error(unsigned _idx); /// Creates a block for the given _node. std::unique_ptr createBlock(ASTNode const* _node, std::string const& _prefix = ""); + /// Creates a call block for the given function _function from contract _contract. + /// The contract is needed here because of inheritance. + std::unique_ptr createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract); /// Creates a new error block to be used by an assertion. /// Also registers the predicate. @@ -117,6 +143,11 @@ private: void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true)); + /// @returns the symbolic values of the state variables at the beginning + /// of the current transaction. + std::vector initialStateVariables(); + std::vector stateVariablesAtIndex(int _index); + std::vector stateVariablesAtIndex(int _index, ContractDefinition const& _contract); /// @returns the current symbolic values of the current state variables. std::vector currentStateVariables(); @@ -128,19 +159,26 @@ private: std::vector currentBlockVariables(); /// @returns the predicate name for a given node. - std::string predicateName(ASTNode const* _node); + std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr); /// @returns a predicate application over the current scoped variables. smt::Expression predicate(smt::SymbolicFunctionVariable const& _block); /// @returns a predicate application over @param _arguments. smt::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector const& _arguments); + /// @returns a predicate that defines a constructor summary. + smt::Expression summary(ContractDefinition const& _contract); + /// @returns a predicate that defines a function summary. + smt::Expression summary(FunctionDefinition const& _function); //@} /// Solver related. //@{ /// Adds Horn rule to the solver. void addRule(smt::Expression const& _rule, std::string const& _ruleName); - /// @returns true if query is unsatisfiable (safe). - bool query(smt::Expression const& _query, langutil::SourceLocation const& _location); + /// @returns if query is unsatisfiable (safe). + /// @returns otherwise. + std::pair> query(smt::Expression const& _query, langutil::SourceLocation const& _location); + + void addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId); //@} /// Misc. @@ -157,15 +195,29 @@ private: /// Implicit constructor predicate. /// Explicit constructors are handled as functions. - std::unique_ptr m_constructorPredicate; + std::unique_ptr m_implicitConstructorPredicate; + + /// Constructor summary predicate, exists after the constructor + /// (implicit or explicit) and before the interface. + std::unique_ptr m_constructorSummaryPredicate; /// Artificial Interface predicate. /// Single entry block for all functions. - std::unique_ptr m_interfacePredicate; + std::map> m_interfaces; /// Artificial Error predicate. /// Single error block for all assertions. std::unique_ptr m_errorPredicate; + + /// Function predicates. + std::map>> m_summaries; + + smt::SymbolicIntVariable m_error{ + TypeProvider::uint256(), + TypeProvider::uint256(), + "error", + m_context + }; //@} /// Variables. @@ -180,7 +232,12 @@ private: /// Verification targets. //@{ - std::vector m_verificationTargets; + struct CHCVerificationTarget: VerificationTarget + { + smt::Expression errorId; + }; + + std::map m_verificationTargets; /// Assertions proven safe. std::set m_safeAssertions; @@ -190,6 +247,10 @@ private: //@{ FunctionDefinition const* m_currentFunction = nullptr; + std::map, IdCompare> m_callGraph; + + std::map, IdCompare> m_functionAssertions; + /// The current block. smt::Expression m_currentBlock = smt::Expression(true); diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h index 9b75065f6..648f7dc33 100644 --- a/libsolidity/formal/EncodingContext.h +++ b/libsolidity/formal/EncodingContext.h @@ -140,6 +140,7 @@ public: void pushSolver(); void popSolver(); void addAssertion(Expression const& _e); + unsigned solverStackHeigh() { return m_assertions.size(); } const SolverInterface* solver() { solAssert(m_solver, ""); diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index c69849a06..ebc1a8751 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -29,9 +29,9 @@ ModelChecker::ModelChecker( ReadCallback::Callback const& _smtCallback, smt::SMTSolverChoice _enabledSolvers ): + m_context(), m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers), - m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers), - m_context() + m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers) { } diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index ac19ba270..546f2df86 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -62,14 +62,14 @@ public: static smt::SMTSolverChoice availableSolvers(); private: + /// Stores the context of the encoding. + smt::EncodingContext m_context; + /// 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/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h index a6247a541..3791af4c5 100644 --- a/libsolidity/formal/Z3Interface.h +++ b/libsolidity/formal/Z3Interface.h @@ -58,11 +58,11 @@ private: z3::sort z3Sort(smt::Sort const& _sort); z3::sort_vector z3Sort(std::vector const& _sorts); - std::map m_constants; - std::map m_functions; - z3::context m_context; z3::solver m_solver; + + std::map m_constants; + std::map m_functions; }; } diff --git a/test/libsolidity/smtCheckerTests/functions/library_constant.sol b/test/libsolidity/smtCheckerTests/functions/library_constant.sol new file mode 100644 index 000000000..e32b8565b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/library_constant.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; + +library l1 { + + uint private constant TON = 1000; + function f1() public pure { + assert(TON == 1000); + assert(TON == 2000); + } + function f2(uint x, uint y) internal pure returns (uint) { + return x + y; + } +} + +contract C { + function f(uint x) public pure { + uint z = l1.f2(x, 1); + assert(z == x + 1); + } +} +// ---- +// Warning: (136-155): Assertion violation happens here +// Warning: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (300-302): Assertion checker does not yet implement type type(library l1) +// Warning: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (327-332): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/functions/library_constant_2.sol b/test/libsolidity/smtCheckerTests/functions/library_constant_2.sol new file mode 100644 index 000000000..9c04e6f9a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/library_constant_2.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; + +library l1 { + + uint private constant TON = 1000; + function f1() public pure { + assert(TON == 1000); + } +} diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_nested.sol b/test/libsolidity/smtCheckerTests/invariants/loop_nested.sol index 867403b61..1fb380649 100644 --- a/test/libsolidity/smtCheckerTests/invariants/loop_nested.sol +++ b/test/libsolidity/smtCheckerTests/invariants/loop_nested.sol @@ -17,3 +17,8 @@ contract Simple { } // ==== // SMTSolvers: z3 +// ---- +// Warning: (172-187): Error trying to invoke SMT solver. +// Warning: (195-209): Error trying to invoke SMT solver. +// Warning: (172-187): Assertion violation happens here +// Warning: (195-209): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol b/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol index 9cfd4569f..e7fde4d5a 100644 --- a/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol +++ b/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol @@ -14,3 +14,8 @@ contract Simple { } // ==== // SMTSolvers: z3 +// ---- +// Warning: (164-179): Error trying to invoke SMT solver. +// Warning: (187-201): Error trying to invoke SMT solver. +// Warning: (164-179): Assertion violation happens here +// Warning: (187-201): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol index 9e7a83866..0b301505b 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol @@ -12,12 +12,12 @@ contract LoopFor2 { b[i] = i + 1; c[i] = b[i]; } + // This is safe but too hard to solve currently. assert(b[0] == c[0]); assert(a[0] == 900); assert(b[0] == 900); } } -// ==== -// SMTSolvers: z3 // ---- -// Warning: (312-331): Assertion violation happens here +// Warning: (316-336): Assertion violation happens here +// Warning: (363-382): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol index 8146a7f19..333273781 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol @@ -12,13 +12,13 @@ contract LoopFor2 { b[i] = i + 1; c[i] = b[i]; } + // This is safe but too hard to prove currently. assert(b[0] == c[0]); assert(a[0] == 900); assert(b[0] == 900); } } -// ==== -// SMTSolvers: z3 // ---- -// Warning: (290-309): Assertion violation happens here -// Warning: (313-332): Assertion violation happens here +// Warning: (317-337): Assertion violation happens here +// Warning: (341-360): Assertion violation happens here +// Warning: (364-383): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol index 06ef66be9..9cd7de9e6 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol @@ -13,5 +13,5 @@ contract C assert(a[1][1] == 0); } } -// ==== -// SMTSolvers: z3 +// ---- +// Warning: (184-204): Assertion violation happens here