diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 79d42555d..130d239b2 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -29,6 +29,9 @@ #include #include +#include +#include + using namespace std; using namespace solidity; using namespace solidity::util; @@ -122,6 +125,7 @@ bool CHC::visit(ContractDefinition const& _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); auto stateExprs = currentStateVariables(); setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs); @@ -614,6 +618,7 @@ void CHC::resetSourceAnalysis() m_errorIds.clear(); m_callGraph.clear(); m_summaries.clear(); + m_symbolFunction.clear(); } void CHC::resetContractAnalysis() @@ -684,6 +689,11 @@ vector CHC::stateVariablesIncludingInheritedAndPriva ); } +vector CHC::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function) +{ + return stateVariablesIncludingInheritedAndPrivate(dynamic_cast(*_function.scope())); +} + vector CHC::stateSorts(ContractDefinition const& _contract) { return applyMap( @@ -841,10 +851,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract)); if ( + !function->isConstructor() && function->isPublic() && !base->isLibrary() && - !base->isInterface() && - !function->isConstructor() + !base->isInterface() ) { auto state1 = stateVariablesAtIndex(1, *base); @@ -923,21 +933,28 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function) unique_ptr CHC::createBlock(ASTNode const* _node, string const& _prefix) { - return createSymbolicBlock(sort(_node), + auto block = createSymbolicBlock(sort(_node), "block_" + uniquePrefix() + "_" + _prefix + predicateName(_node)); + + solAssert(m_currentFunction, ""); + m_symbolFunction[block->currentFunctionValue().name] = m_currentFunction; + return block; } unique_ptr CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract) { - return createSymbolicBlock(summarySort(_function, _contract), + auto block = createSymbolicBlock(summarySort(_function, _contract), "summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract)); + + m_symbolFunction[block->currentFunctionValue().name] = &_function; + return block; } void CHC::createErrorBlock() @@ -1167,19 +1184,21 @@ void CHC::checkVerificationTargets() { string satMsg; string unknownMsg; + ErrorId errorReporterId; if (target.type == VerificationTarget::Type::PopEmptyArray) { solAssert(dynamic_cast(scope), ""); - satMsg = "Empty array \"pop\" detected here."; + satMsg = "Empty array \"pop\" detected here"; unknownMsg = "Empty array \"pop\" might happen here."; + errorReporterId = 2529_error; } else solAssert(false, ""); auto it = m_errorIds.find(scope->id()); solAssert(it != m_errorIds.end(), ""); - checkAndReportTarget(scope, target, it->second, satMsg, unknownMsg); + checkAndReportTarget(scope, target, it->second, errorReporterId, satMsg, unknownMsg); } } } @@ -1194,13 +1213,7 @@ void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& solAssert(it != m_errorIds.end(), ""); unsigned errorId = it->second; - createErrorBlock(); - connectBlocks(_target.value, error(), _target.constraints && (_target.errorId == errorId)); - auto [result, model] = query(error(), assertion->location()); - // This should be fine but it's a bug in the old compiler - (void)model; - if (result == smtutil::CheckResult::UNSATISFIABLE) - m_safeTargets[assertion].insert(_target.type); + checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here"); } } @@ -1208,35 +1221,228 @@ void CHC::checkAndReportTarget( ASTNode const* _scope, CHCVerificationTarget const& _target, unsigned _errorId, + ErrorId _errorReporterId, string _satMsg, string _unknownMsg ) { + if (m_unsafeTargets.count(_scope) && m_unsafeTargets.at(_scope).count(_target.type)) + return; + createErrorBlock(); connectBlocks(_target.value, error(), _target.constraints && (_target.errorId == _errorId)); - auto [result, model] = query(error(), _scope->location()); - // This should be fine but it's a bug in the old compiler - (void)model; + auto const& [result, model] = query(error(), _scope->location()); if (result == smtutil::CheckResult::UNSATISFIABLE) m_safeTargets[_scope].insert(_target.type); else if (result == smtutil::CheckResult::SATISFIABLE) { solAssert(!_satMsg.empty(), ""); m_unsafeTargets[_scope].insert(_target.type); - m_outerErrorReporter.warning( - 2529_error, - _scope->location(), - _satMsg - ); + auto cex = generateCounterexample(model, error().name); + if (cex) + m_outerErrorReporter.warning( + _errorReporterId, + _scope->location(), + _satMsg, + SecondarySourceLocation().append(" for:\n" + *cex, SourceLocation{}) + ); + else + m_outerErrorReporter.warning( + _errorReporterId, + _scope->location(), + _satMsg + "." + ); } else if (!_unknownMsg.empty()) m_outerErrorReporter.warning( - 1147_error, + _errorReporterId, _scope->location(), _unknownMsg ); } +/** +The counterexample DAG has the following properties: +1) The root node represents the reachable error predicate. +2) The root node has 1 or 2 children: + - One of them is the summary of the function that was called and led to that node. + If this is the only child, this function must be the constructor. + - If it has 2 children, the function is not the constructor and the other child is the interface node, + that is, it represents the state of the contract before the function described above was called. +3) Interface nodes also have property 2. + +The following algorithm starts collecting function summaries at the root node and repeats +for each interface node seen. +Each function summary collected represents a transaction, and the final order is reversed. + +The first function summary seen contains the values for the state, input and output variables at the +error point. +*/ +optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& _graph, string const& _root) +{ + optional rootId; + for (auto const& [id, node]: _graph.nodes) + if (node.first == _root) + { + rootId = id; + break; + } + if (!rootId) + return {}; + + vector path; + string localState; + + unsigned node = *rootId; + optional lastTxSeen; + while (_graph.edges.at(node).size() >= 1) + { + auto const& edges = _graph.edges.at(node); + 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) + swap(summaryId, *interfaceId); + solAssert(_graph.nodes.at(*interfaceId).first.rfind("interface", 0) == 0, ""); + } + + solAssert(_graph.nodes.at(summaryId).first.rfind("summary", 0) == 0, ""); + /// At this point property 2 from the function description is verified for this node. + + 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, ""); + + 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. + + /// This summary node is the end of a tx. + /// If it is the first summary node seen in this loop, it is the summary + /// of the public/external function that was called when the error was reached, + /// but not necessarily the summary of the function that contains the error. + if (!lastTxSeen) + { + lastTxSeen = summaryNode.first; + /// Generate counterexample message local to the failed target. + localState = generatePostStateCounterexample(stateVars, calledFun, summaryNode.second) + "\n"; + if (calledFun) + { + /// The signature of a summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars). + 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"; + } + 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"; + } + } + } + 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: " + generatePostStateCounterexample(stateVars, calledFun, summaryNode.second)); + + string txCex = calledContract ? "constructor()" : generatePreTxCounterexample(stateVars, *calledFun, summaryNode.second); + path.emplace_back(txCex); + + /// Recurse on the next interface node which represents the previous transaction + /// or stop. + if (interfaceId) + node = *interfaceId; + else + break; + } + + return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n"); +} + +string CHC::generatePostStateCounterexample(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()); + } + + 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::generatePreTxCounterexample(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()); + 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::uniquePrefix() { return to_string(m_blockCounter++); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index ca29d046b..3334a45e4 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -38,6 +38,7 @@ #include #include +#include #include namespace solidity::frontend @@ -102,6 +103,7 @@ private: void setCurrentBlock(smt::SymbolicFunctionVariable 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. @@ -206,9 +208,21 @@ private: ASTNode const* _scope, CHCVerificationTarget const& _target, unsigned _errorId, + langutil::ErrorId _errorReporterId, std::string _satMsg, - std::string _unknownMsg + std::string _unknownMsg = "" ); + + 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 generatePostStateCounterexample(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 generatePreTxCounterexample(std::vector const& _stateVariables, FunctionDefinition const& _function, std::vector const& _summaryValues); //@} /// Misc. @@ -258,6 +272,9 @@ private: "error", m_context }; + + /// Maps predicate names to the ASTNodes they came from. + std::map m_symbolFunction; //@} /// Variables.