diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 74f4a9a21..5e823d8ee 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -100,6 +100,8 @@ set(sources formal/EncodingContext.h formal/ModelChecker.cpp formal/ModelChecker.h + formal/Predicate.cpp + formal/Predicate.h formal/SMTEncoder.cpp formal/SMTEncoder.h formal/SSAVariable.cpp diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 65df7e203..f6a3b5aae 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -29,7 +29,6 @@ #include #include -#include #include #include @@ -85,11 +84,7 @@ void CHC::analyze(SourceUnit const& _source) resetSourceAnalysis(); - auto genesisSort = make_shared( - vector(), - smtutil::SortProvider::boolSort - ); - m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis"); + m_genesisPredicate = createSymbolicBlock(arity0FunctionSort(), "genesis"); addRule(genesis(), "genesis"); set sources; @@ -118,16 +113,14 @@ bool CHC::visit(ContractDefinition const& _contract) initContract(_contract); - m_stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract); + m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract); m_stateSorts = stateSorts(_contract); clearIndices(&_contract); string suffix = _contract.name() + "_" + to_string(_contract.id()); - m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_" + suffix); - m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix); - m_symbolFunction[m_constructorSummaryPredicate->currentFunctionValue().name] = &_contract; - m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix); + m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix, &_contract); + m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix, &_contract); auto stateExprs = currentStateVariables(); setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs); @@ -233,7 +226,7 @@ void CHC::endVisit(FunctionDefinition const& _function) if (_function.isConstructor()) { string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id()); - auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix); + auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix, m_currentContract); connectBlocks(m_currentBlock, predicate(*constructorExit, currentFunctionVariables(*m_currentContract))); clearIndices(m_currentContract, m_currentFunction); @@ -326,8 +319,8 @@ bool CHC::visit(WhileStatement const& _while) auto outerBreakDest = m_breakDest; auto outerContinueDest = m_continueDest; - m_breakDest = afterLoopBlock.get(); - m_continueDest = loopHeaderBlock.get(); + m_breakDest = afterLoopBlock; + m_continueDest = loopHeaderBlock; if (_while.isDoWhile()) _while.body().accept(*this); @@ -377,8 +370,8 @@ bool CHC::visit(ForStatement const& _for) auto outerBreakDest = m_breakDest; auto outerContinueDest = m_continueDest; - m_breakDest = afterLoopBlock.get(); - m_continueDest = postLoop ? postLoopBlock.get() : loopHeaderBlock.get(); + m_breakDest = afterLoopBlock; + m_continueDest = postLoop ? postLoopBlock : loopHeaderBlock; if (auto init = _for.initializationExpression()) init->accept(*this); @@ -571,7 +564,6 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) m_context.variable(*var)->increaseIndex(); auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables()); - m_symbolFunction[nondet.name] = &_funCall; m_context.addAssertion(nondet); m_context.addAssertion(m_error.currentValue() == 0); @@ -681,7 +673,9 @@ void CHC::resetSourceAnalysis() m_errorIds.clear(); m_callGraph.clear(); m_summaries.clear(); - m_symbolFunction.clear(); + m_interfaces.clear(); + m_nondetInterfaces.clear(); + Predicate::reset(); } void CHC::resetContractAnalysis() @@ -717,7 +711,7 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c } void CHC::setCurrentBlock( - smt::SymbolicFunctionVariable const& _block, + Predicate const& _block, vector const* _arguments ) { @@ -743,24 +737,10 @@ set CHC::transactionAssertions(ASTN return assertions; } -vector CHC::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract) -{ - return fold( - _contract.annotation().linearizedBaseContracts, - vector{}, - [](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); } - ); -} - -vector CHC::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function) -{ - return stateVariablesIncludingInheritedAndPrivate(dynamic_cast(*_function.scope())); -} - vector CHC::stateSorts(ContractDefinition const& _contract) { return applyMap( - stateVariablesIncludingInheritedAndPrivate(_contract), + SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); } ); } @@ -806,7 +786,7 @@ smtutil::SortPointer CHC::nondetInterfaceSort(ContractDefinition const& _contrac ); } -smtutil::SortPointer CHC::arity0FunctionSort() +smtutil::SortPointer CHC::arity0FunctionSort() const { return make_shared( vector(), @@ -853,7 +833,7 @@ smtutil::SortPointer CHC::sort(ASTNode const* _node) smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract) { - auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract); + auto stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract); auto sorts = stateSorts(_contract); auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; @@ -870,14 +850,10 @@ smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, Contr ); } -unique_ptr CHC::createSymbolicBlock(smtutil::SortPointer _sort, string const& _name) +Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, ASTNode const* _node) { - auto block = make_unique( - _sort, - _name, - m_context - ); - m_interface->registerRelation(block->currentFunctionValue()); + auto const* block = Predicate::create(_sort, _name, m_context, _node); + m_interface->registerRelation(block->functor()); return block; } @@ -887,20 +863,24 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) 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); - m_nondetInterfaces[base] = createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix); - - for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base)) + for (auto const* var: SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*base)) if (!m_context.knownVariable(*var)) createVariable(*var); - /// Base nondeterministic interface that allows - /// 0 steps to be taken, used as base for the inductive - /// rule for each function. - auto const& iface = *m_nondetInterfaces.at(base); - auto state0 = stateVariablesAtIndex(0, *base); - addRule(iface(state0 + state0), "base_nondet"); + if (!m_interfaces.count(base)) + { + solAssert(!m_nondetInterfaces.count(base), ""); + string suffix = base->name() + "_" + to_string(base->id()); + m_interfaces.emplace(base, createSymbolicBlock(interfaceSort(*base), "interface_" + suffix, base)); + m_nondetInterfaces.emplace(base, createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix, base)); + + /// Base nondeterministic interface that allows + /// 0 steps to be taken, used as base for the inductive + /// rule for each function. + auto const* iface = m_nondetInterfaces.at(base); + auto state0 = stateVariablesAtIndex(0, *base); + addRule((*iface)(state0 + state0), "base_nondet"); + } for (auto const* function: base->definedFunctions()) { @@ -923,8 +903,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) auto state1 = stateVariablesAtIndex(1, *base); auto state2 = stateVariablesAtIndex(2, *base); - auto nondetPre = iface(state0 + state1); - auto nondetPost = iface(state0 + state2); + auto const* iface = m_nondetInterfaces.at(base); + auto state0 = stateVariablesAtIndex(0, *base); + auto nondetPre = (*iface)(state0 + state1); + auto nondetPost = (*iface)(state0 + state2); vector args{m_error.currentValue()}; args += state1 + @@ -960,7 +942,7 @@ smtutil::Expression CHC::error() smtutil::Expression CHC::error(unsigned _idx) { - return m_errorPredicate->functionValueAtIndex(_idx)({}); + return m_errorPredicate->functor(_idx)({}); } smtutil::Expression CHC::summary(ContractDefinition const& _contract) @@ -994,37 +976,33 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function) return summary(_function, *m_currentContract); } -unique_ptr CHC::createBlock(ASTNode const* _node, string const& _prefix) +Predicate const* CHC::createBlock(ASTNode const* _node, string const& _prefix) { - auto block = createSymbolicBlock(sort(_node), - "block_" + - uniquePrefix() + - "_" + - _prefix + - predicateName(_node)); + auto block = createSymbolicBlock( + sort(_node), + "block_" + uniquePrefix() + "_" + _prefix + predicateName(_node), + _node + ); solAssert(m_currentFunction, ""); - m_symbolFunction[block->currentFunctionValue().name] = m_currentFunction; return block; } -unique_ptr CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract) +Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract) { - auto block = createSymbolicBlock(summarySort(_function, _contract), - "summary_" + - uniquePrefix() + - "_" + - predicateName(&_function, &_contract)); + auto block = createSymbolicBlock( + summarySort(_function, _contract), + "summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract), + &_function + ); - m_symbolFunction[block->currentFunctionValue().name] = &_function; return block; } void CHC::createErrorBlock() { - solAssert(m_errorPredicate, ""); - m_errorPredicate->increaseIndex(); - m_interface->registerRelation(m_errorPredicate->currentFunctionValue()); + m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId())); + m_interface->registerRelation(m_errorPredicate->functor()); } void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints) @@ -1055,7 +1033,7 @@ vector CHC::stateVariablesAtIndex(unsigned _index) vector CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract) { return applyMap( - stateVariablesIncludingInheritedAndPrivate(_contract), + SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [&](auto _var) { return valueAtIndex(*_var, _index); } ); } @@ -1068,7 +1046,7 @@ vector CHC::currentStateVariables() vector CHC::currentStateVariables(ContractDefinition const& _contract) { - return applyMap(stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); }); + return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); }); } vector CHC::currentFunctionVariables() @@ -1128,13 +1106,13 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id()); } -smtutil::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block) +smtutil::Expression CHC::predicate(Predicate const& _block) { return _block(currentBlockVariables()); } smtutil::Expression CHC::predicate( - smt::SymbolicFunctionVariable const& _block, + Predicate const& _block, vector const& _arguments ) { @@ -1425,42 +1403,31 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& solAssert(edges.size() <= 2, ""); unsigned summaryId = edges.at(0); - optional interfaceId; if (edges.size() == 2) { interfaceId = edges.at(1); - if (_graph.nodes.at(summaryId).first.rfind("summary", 0) != 0) + if (!Predicate::predicate(_graph.nodes.at(summaryId).first)->isSummary()) swap(summaryId, *interfaceId); - solAssert(_graph.nodes.at(*interfaceId).first.rfind("interface", 0) == 0, ""); + auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first); + solAssert(interfacePredicate && interfacePredicate->isInterface(), ""); } /// The children are unordered, so we need to check which is the summary and /// which is the interface. - solAssert(_graph.nodes.at(summaryId).first.rfind("summary", 0) == 0, ""); + Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).first); + solAssert(summaryPredicate && summaryPredicate->isSummary(), ""); /// At this point property 2 from the function description is verified for this node. + auto summaryArgs = _graph.nodes.at(summaryId).second; - auto const& summaryNode = _graph.nodes.at(summaryId); - solAssert(m_symbolFunction.count(summaryNode.first), ""); - - FunctionDefinition const* calledFun = nullptr; - ContractDefinition const* calledContract = nullptr; - if (auto const* contract = dynamic_cast(m_symbolFunction.at(summaryNode.first))) - { - if (auto const* constructor = contract->constructor()) - calledFun = constructor; - else - calledContract = contract; - } - else if (auto const* fun = dynamic_cast(m_symbolFunction.at(summaryNode.first))) - calledFun = fun; - else - solAssert(false, ""); + FunctionDefinition const* calledFun = summaryPredicate->programFunction(); + ContractDefinition const* calledContract = summaryPredicate->programContract(); solAssert((calledFun && !calledContract) || (!calledFun && calledContract), ""); - auto const& stateVars = calledFun ? stateVariablesIncludingInheritedAndPrivate(*calledFun) : stateVariablesIncludingInheritedAndPrivate(*calledContract); - /// calledContract != nullptr implies that the constructor of the analyzed contract is implicit and - /// therefore takes no parameters. + auto stateVars = summaryPredicate->stateVariables(); + solAssert(stateVars.has_value(), ""); + auto stateValues = summaryPredicate->summaryStateValues(summaryArgs); + solAssert(stateValues.size() == stateVars->size(), ""); /// This summary node is the end of a tx. /// If it is the first summary node seen in this loop, it is the summary @@ -1470,36 +1437,23 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& { lastTxSeen = true; /// Generate counterexample message local to the failed target. - localState = formatStateCounterexample(stateVars, calledFun, summaryNode.second) + "\n"; + localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n"; if (calledFun) { - /// The signature of a summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars). + auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs); auto const& inParams = calledFun->parameters(); - unsigned initLocals = stateVars.size() * 2 + 1 + inParams.size(); - /// In this loop we are interested in postInputVars. - for (unsigned i = initLocals; i < initLocals + inParams.size(); ++i) - { - auto param = inParams.at(i - initLocals); - if (param->type()->isValueType()) - localState += param->name() + " = " + summaryNode.second.at(i) + "\n"; - } + localState += formatVariableModel(inParams, inValues, "\n") + "\n"; + auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs); auto const& outParams = calledFun->returnParameters(); - initLocals += inParams.size(); - /// In this loop we are interested in outputVars. - for (unsigned i = initLocals; i < initLocals + outParams.size(); ++i) - { - auto param = outParams.at(i - initLocals); - if (param->type()->isValueType()) - localState += param->name() + " = " + summaryNode.second.at(i) + "\n"; - } + localState += formatVariableModel(outParams, outValues, "\n") + "\n"; } } else /// We report the state after every tx in the trace except for the last, which is reported /// first in the code above. - path.emplace_back("State: " + formatStateCounterexample(stateVars, calledFun, summaryNode.second)); + path.emplace_back("State: " + formatVariableModel(*stateVars, stateValues, ", ")); - string txCex = calledContract ? "constructor()" : formatFunctionCallCounterexample(stateVars, *calledFun, summaryNode.second); + string txCex = summaryPredicate->formatSummaryCall(summaryArgs); path.emplace_back(txCex); /// Recurse on the next interface node which represents the previous transaction @@ -1513,66 +1467,6 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n"); } -string CHC::formatStateCounterexample(vector const& _stateVars, FunctionDefinition const* _function, vector const& _summaryValues) -{ - /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars). - /// The signature of an implicit constructor summary predicate is: summary(error, postStateVars). - /// Here we are interested in postStateVars. - vector::const_iterator stateFirst; - vector::const_iterator stateLast; - if (_function) - { - stateFirst = _summaryValues.begin() + 1 + static_cast(_stateVars.size()) + static_cast(_function->parameters().size()); - stateLast = stateFirst + static_cast(_stateVars.size()); - } - else - { - stateFirst = _summaryValues.begin() + 1; - stateLast = stateFirst + static_cast(_stateVars.size()); - } - - solAssert(stateFirst >= _summaryValues.begin() && stateFirst <= _summaryValues.end(), ""); - solAssert(stateLast >= _summaryValues.begin() && stateLast <= _summaryValues.end(), ""); - vector stateArgs(stateFirst, stateLast); - solAssert(stateArgs.size() == _stateVars.size(), ""); - - vector stateCex; - for (unsigned i = 0; i < stateArgs.size(); ++i) - { - auto var = _stateVars.at(i); - if (var->type()->isValueType()) - stateCex.emplace_back(var->name() + " = " + stateArgs.at(i)); - } - - return boost::algorithm::join(stateCex, ", "); -} - -string CHC::formatFunctionCallCounterexample(vector const& _stateVars, FunctionDefinition const& _function, vector const& _summaryValues) -{ - /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars). - /// Here we are interested in preInputVars. - vector::const_iterator first = _summaryValues.begin() + static_cast(_stateVars.size()) + 1; - vector::const_iterator last = first + static_cast(_function.parameters().size()); - solAssert(first >= _summaryValues.begin() && first <= _summaryValues.end(), ""); - solAssert(last >= _summaryValues.begin() && last <= _summaryValues.end(), ""); - vector functionArgsCex(first, last); - vector functionArgs; - - auto const& params = _function.parameters(); - solAssert(params.size() == functionArgsCex.size(), ""); - for (unsigned i = 0; i < params.size(); ++i) - if (params[i]->type()->isValueType()) - functionArgs.emplace_back(functionArgsCex[i]); - else - functionArgs.emplace_back(params[i]->name()); - - string fName = _function.isConstructor() ? "constructor" : - _function.isFallback() ? "fallback" : - _function.isReceive() ? "receive" : - _function.name(); - return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")"; -} - string CHC::cex2dot(smtutil::CHCSolverInterface::CexGraph const& _cex) { string dot = "digraph {\n"; diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index ac1315317..d555f19e7 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -31,12 +31,15 @@ #pragma once +#include #include #include #include +#include + #include #include #include @@ -108,10 +111,8 @@ private: void resetContractAnalysis(); void eraseKnowledge(); void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override; - void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector const* _arguments = nullptr); + void setCurrentBlock(Predicate const& _block, std::vector const* _arguments = nullptr); std::set transactionAssertions(ASTNode const* _txRoot); - static std::vector stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract); - static std::vector stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function); //@} /// Sort helpers. @@ -122,7 +123,7 @@ private: smtutil::SortPointer nondetInterfaceSort(); static smtutil::SortPointer interfaceSort(ContractDefinition const& _const); static smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _const); - smtutil::SortPointer arity0FunctionSort(); + smtutil::SortPointer arity0FunctionSort() const; smtutil::SortPointer sort(FunctionDefinition const& _function); smtutil::SortPointer sort(ASTNode const* _block); /// @returns the sort of a predicate that represents the summary of _function in the scope of _contract. @@ -134,7 +135,7 @@ private: /// Predicate helpers. //@{ /// @returns a new block of given _sort and _name. - std::unique_ptr createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name); + Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, ASTNode const* _node = nullptr); /// Creates summary predicates for all functions of all contracts /// in a given _source. @@ -150,10 +151,10 @@ private: smtutil::Expression error(unsigned _idx); /// Creates a block for the given _node. - std::unique_ptr createBlock(ASTNode const* _node, std::string const& _prefix = ""); + Predicate const* 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); + Predicate const* createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract); /// Creates a new error block to be used by an assertion. /// Also registers the predicate. @@ -184,9 +185,9 @@ private: /// @returns the predicate name for a given node. std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr); /// @returns a predicate application over the current scoped variables. - smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block); + smtutil::Expression predicate(Predicate const& _block); /// @returns a predicate application over @param _arguments. - smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector const& _arguments); + smtutil::Expression predicate(Predicate const& _block, std::vector const& _arguments); /// @returns the summary predicate for the called function. smtutil::Expression predicate(FunctionCall const& _funCall); /// @returns a predicate that defines a constructor summary. @@ -222,15 +223,23 @@ private: ); std::optional generateCounterexample(smtutil::CHCSolverInterface::CexGraph const& _graph, std::string const& _root); - /// @returns values for the _stateVariables after a transaction calling - /// _function was executed. - /// _function = nullptr means the transaction was the deployment of a - /// contract without an explicit constructor. - std::string formatStateCounterexample(std::vector const& _stateVariables, FunctionDefinition const* _function, std::vector const& _summaryValues); - /// @returns a formatted text representing a call to _function - /// with the concrete values for value type parameters and - /// the parameter name for reference types. - std::string formatFunctionCallCounterexample(std::vector const& _stateVariables, FunctionDefinition const& _function, std::vector const& _summaryValues); + + /// @returns a set of pairs _var = _value separated by _separator. + template + std::string formatVariableModel(std::vector const& _variables, std::vector const& _values, std::string const& _separator) const + { + solAssert(_variables.size() == _values.size(), ""); + + std::vector assignments; + for (unsigned i = 0; i < _values.size(); ++i) + { + auto var = _variables.at(i); + if (var && var->type()->isValueType()) + assignments.emplace_back(var->name() + " = " + _values.at(i)); + } + + return boost::algorithm::join(assignments, _separator); + } /// @returns a DAG in the dot format. /// Used for debugging purposes. @@ -251,32 +260,32 @@ private: /// Predicates. //@{ /// Genesis predicate. - std::unique_ptr m_genesisPredicate; + Predicate const* m_genesisPredicate = nullptr; /// Implicit constructor predicate. /// Explicit constructors are handled as functions. - std::unique_ptr m_implicitConstructorPredicate; + Predicate const* m_implicitConstructorPredicate = nullptr; /// Constructor summary predicate, exists after the constructor /// (implicit or explicit) and before the interface. - std::unique_ptr m_constructorSummaryPredicate; + Predicate const* m_constructorSummaryPredicate = nullptr; /// Artificial Interface predicate. /// Single entry block for all functions. - std::map> m_interfaces; + std::map m_interfaces; /// Nondeterministic interfaces. /// These are used when the analyzed contract makes external calls to unknown code, /// which means that the analyzed contract can potentially be called /// nondeterministically. - std::map> m_nondetInterfaces; + std::map m_nondetInterfaces; /// Artificial Error predicate. /// Single error block for all assertions. - std::unique_ptr m_errorPredicate; + Predicate const* m_errorPredicate = nullptr; /// Function predicates. - std::map>> m_summaries; + std::map> m_summaries; smt::SymbolicIntVariable m_error{ TypeProvider::uint256(), @@ -337,9 +346,9 @@ private: bool m_unknownFunctionCallSeen = false; /// Block where a loop break should go to. - smt::SymbolicFunctionVariable const* m_breakDest = nullptr; + Predicate const* m_breakDest; /// Block where a loop continue should go to. - smt::SymbolicFunctionVariable const* m_continueDest = nullptr; + Predicate const* m_continueDest; //@} /// CHC solver. diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp new file mode 100644 index 000000000..9f897d63f --- /dev/null +++ b/libsolidity/formal/Predicate.cpp @@ -0,0 +1,260 @@ +/* + 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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include + +#include + +#include + +#include +#include + +using namespace std; +using namespace solidity; +using namespace solidity::smtutil; +using namespace solidity::frontend; +using namespace solidity::frontend::smt; + +map Predicate::m_predicates; + +Predicate const* Predicate::create( + SortPointer _sort, + string _name, + EncodingContext& _context, + ASTNode const* _node +) +{ + smt::SymbolicFunctionVariable predicate{_sort, move(_name), _context}; + string functorName = predicate.currentName(); + solAssert(!m_predicates.count(functorName), ""); + return &m_predicates.emplace( + std::piecewise_construct, + std::forward_as_tuple(functorName), + std::forward_as_tuple(move(predicate), _node) + ).first->second; +} + +Predicate::Predicate( + smt::SymbolicFunctionVariable&& _predicate, + ASTNode const* _node +): + m_predicate(move(_predicate)), + m_node(_node) +{ +} + +Predicate const* Predicate::predicate(string const& _name) +{ + return &m_predicates.at(_name); +} + +void Predicate::reset() +{ + m_predicates.clear(); +} + +smtutil::Expression Predicate::operator()(vector const& _args) const +{ + return m_predicate(_args); +} + +smtutil::Expression Predicate::functor() const +{ + return m_predicate.currentFunctionValue(); +} + +smtutil::Expression Predicate::functor(unsigned _idx) const +{ + return m_predicate.functionValueAtIndex(_idx); +} + +void Predicate::newFunctor() +{ + m_predicate.increaseIndex(); +} + +ASTNode const* Predicate::programNode() const +{ + return m_node; +} + +ContractDefinition const* Predicate::programContract() const +{ + if (auto const* contract = dynamic_cast(m_node)) + if (!contract->constructor()) + return contract; + + return nullptr; +} + +FunctionDefinition const* Predicate::programFunction() const +{ + if (auto const* contract = dynamic_cast(m_node)) + { + if (contract->constructor()) + return contract->constructor(); + return nullptr; + } + + if (auto const* fun = dynamic_cast(m_node)) + return fun; + + return nullptr; +} + +optional> Predicate::stateVariables() const +{ + if (auto const* fun = programFunction()) + return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun); + if (auto const* contract = programContract()) + return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contract); + + auto const* node = m_node; + while (auto const* scopable = dynamic_cast(node)) + { + node = scopable->scope(); + if (auto const* fun = dynamic_cast(node)) + return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun); + } + + return nullopt; +} + +bool Predicate::isSummary() const +{ + return functor().name.rfind("summary", 0) == 0; +} + +bool Predicate::isInterface() const +{ + return functor().name.rfind("interface", 0) == 0; +} + +string Predicate::formatSummaryCall(vector const& _args) const +{ + if (programContract()) + return "constructor()"; + + solAssert(isSummary(), ""); + + auto stateVars = stateVariables(); + solAssert(stateVars.has_value(), ""); + auto const* fun = programFunction(); + solAssert(fun, ""); + + /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). + /// Here we are interested in preInputVars. + vector::const_iterator first = _args.begin() + static_cast(stateVars->size()) + 1; + vector::const_iterator last = first + static_cast(fun->parameters().size()); + solAssert(first >= _args.begin() && first <= _args.end(), ""); + solAssert(last >= _args.begin() && last <= _args.end(), ""); + vector functionArgsCex(first, last); + vector functionArgs; + + auto const& params = fun->parameters(); + solAssert(params.size() == functionArgsCex.size(), ""); + for (unsigned i = 0; i < params.size(); ++i) + if (params[i]->type()->isValueType()) + functionArgs.emplace_back(functionArgsCex[i]); + else + functionArgs.emplace_back(params[i]->name()); + + string fName = fun->isConstructor() ? "constructor" : + fun->isFallback() ? "fallback" : + fun->isReceive() ? "receive" : + fun->name(); + return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")"; + +} + +vector Predicate::summaryStateValues(vector const& _args) const +{ + /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). + /// The signature of an implicit constructor summary predicate is: summary(error, postStateVars). + /// Here we are interested in postStateVars. + + auto stateVars = stateVariables(); + solAssert(stateVars.has_value(), ""); + + vector::const_iterator stateFirst; + vector::const_iterator stateLast; + if (auto const* function = programFunction()) + { + stateFirst = _args.begin() + 1 + static_cast(stateVars->size()) + static_cast(function->parameters().size()); + stateLast = stateFirst + static_cast(stateVars->size()); + } + else if (programContract()) + { + stateFirst = _args.begin() + 1; + stateLast = stateFirst + static_cast(stateVars->size()); + } + else + solAssert(false, ""); + + solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), ""); + solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), ""); + + vector stateArgs(stateFirst, stateLast); + solAssert(stateArgs.size() == stateVars->size(), ""); + return stateArgs; +} + +vector Predicate::summaryPostInputValues(vector const& _args) const +{ + /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). + /// Here we are interested in postInputVars. + auto const* function = programFunction(); + solAssert(function, ""); + + auto stateVars = stateVariables(); + solAssert(stateVars.has_value(), ""); + + auto const& inParams = function->parameters(); + + vector::const_iterator first = _args.begin() + 1 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()); + vector::const_iterator last = first + static_cast(inParams.size()); + + solAssert(first >= _args.begin() && first <= _args.end(), ""); + solAssert(last >= _args.begin() && last <= _args.end(), ""); + + vector inValues(first, last); + solAssert(inValues.size() == inParams.size(), ""); + return inValues; +} + +vector Predicate::summaryPostOutputValues(vector const& _args) const +{ + /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). + /// Here we are interested in outputVars. + auto const* function = programFunction(); + solAssert(function, ""); + + auto stateVars = stateVariables(); + solAssert(stateVars.has_value(), ""); + + auto const& inParams = function->parameters(); + + vector::const_iterator first = _args.begin() + 1 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2; + + solAssert(first >= _args.begin() && first <= _args.end(), ""); + + vector outValues(first, _args.end()); + solAssert(outValues.size() == function->returnParameters().size(), ""); + return outValues; +} diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h new file mode 100644 index 000000000..3da5ad453 --- /dev/null +++ b/libsolidity/formal/Predicate.h @@ -0,0 +1,120 @@ +/* + 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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#pragma once + +#include +#include + +#include + +#include +#include +#include + +namespace solidity::frontend +{ + +/** + * Represents a predicate used by the CHC engine. + */ +class Predicate +{ +public: + static Predicate const* create( + smtutil::SortPointer _sort, + std::string _name, + smt::EncodingContext& _context, + ASTNode const* _node = nullptr + ); + + Predicate( + smt::SymbolicFunctionVariable&& _predicate, + ASTNode const* _node = nullptr + ); + + /// Predicate should not be copiable. + Predicate(Predicate const&) = delete; + Predicate& operator=(Predicate const&) = delete; + + /// @returns the Predicate associated with _name. + static Predicate const* predicate(std::string const& _name); + + /// Resets all the allocated predicates. + static void reset(); + + /// @returns a function application of the predicate over _args. + smtutil::Expression operator()(std::vector const& _args) const; + + /// @returns the function declaration of the predicate. + smtutil::Expression functor() const; + /// @returns the function declaration of the predicate with index _idx. + smtutil::Expression functor(unsigned _idx) const; + /// Increases the index of the function declaration of the predicate. + void newFunctor(); + + /// @returns the program node this predicate represents. + ASTNode const* programNode() const; + + /// @returns the ContractDefinition that this predicate represents + /// or nullptr otherwise. + ContractDefinition const* programContract() const; + + /// @returns the FunctionDefinition that this predicate represents + /// or nullptr otherwise. + FunctionDefinition const* programFunction() const; + + /// @returns the program state variables in the scope of this predicate. + std::optional> stateVariables() const; + + /// @returns true if this predicate represents a summary. + bool isSummary() const; + + /// @returns true if this predicate represents an interface. + bool isInterface() const; + + /// @returns a formatted string representing a call to this predicate + /// with _args. + std::string formatSummaryCall(std::vector const& _args) const; + + /// @returns the values of the state variables from _args at the point + /// where this summary was reached. + std::vector summaryStateValues(std::vector const& _args) const; + + /// @returns the values of the function input variables from _args at the point + /// where this summary was reached. + std::vector summaryPostInputValues(std::vector const& _args) const; + + /// @returns the values of the function output variables from _args at the point + /// where this summary was reached. + std::vector summaryPostOutputValues(std::vector const& _args) const; + +private: + /// The actual SMT expression. + smt::SymbolicFunctionVariable m_predicate; + + /// The ASTNode that this predicate represents. + /// nullptr if this predicate is not associated with a specific program AST node. + ASTNode const* m_node = nullptr; + + /// Maps the name of the predicate to the actual Predicate. + /// Used in counterexample generation. + static std::map m_predicates; +}; + +} diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 0418de737..644e9200e 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1985,6 +1985,20 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall cons return funDef; } +vector SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract) +{ + return fold( + _contract.annotation().linearizedBaseContracts, + vector{}, + [](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); } + ); +} + +vector SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function) +{ + return stateVariablesIncludingInheritedAndPrivate(dynamic_cast(*_function.scope())); +} + void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) { FunctionDefinition const* funDef = functionCallToDefinition(_funCall); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index fb5dce405..6e7388155 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -62,6 +62,9 @@ public: /// if possible or nullptr. static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall); + static std::vector stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract); + static std::vector stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function); + protected: // TODO: Check that we do not have concurrent reads and writes to a variable, // because the order of expression evaluation is undefined diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol index f543be8db..6f3701d41 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol @@ -21,5 +21,5 @@ contract C } } // ---- -// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 6328: (136-149): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol index f267f0b99..6b09f780d 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol @@ -26,4 +26,4 @@ contract C } } // ---- -// Warning 6328: (400-457): Assertion violation happens here. +// Warning 6328: (400-457): Assertion violation happens here