diff --git a/libsmtutil/CHCSolverInterface.h b/libsmtutil/CHCSolverInterface.h index 1fe279a8b..c088f3d0f 100644 --- a/libsmtutil/CHCSolverInterface.h +++ b/libsmtutil/CHCSolverInterface.h @@ -44,9 +44,7 @@ public: /// Needs to bound all vars as universally quantified. virtual void addRule(Expression const& _expr, std::string const& _name) = 0; - /// first: predicate name - /// second: predicate arguments - using CexNode = std::pair>; + using CexNode = Expression; struct CexGraph { std::map nodes; diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp index 35b3556d9..e2b933b68 100644 --- a/libsmtutil/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -161,7 +161,7 @@ CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof) proofStack.push(_proof.arg(0)); auto const& root = proofStack.top(); - graph.nodes[root.id()] = {name(fact(root)), arguments(fact(root))}; + graph.nodes.emplace(root.id(), m_z3Interface->fromZ3Expr(fact(root))); set visited; visited.insert(root.id()); @@ -186,7 +186,7 @@ CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof) if (!graph.nodes.count(child.id())) { - graph.nodes[child.id()] = {name(fact(child)), arguments(fact(child))}; + graph.nodes.emplace(child.id(), m_z3Interface->fromZ3Expr(fact(child))); graph.edges[child.id()] = {}; } diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 7bedc8a65..e10785093 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -1306,7 +1306,7 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& { optional rootId; for (auto const& [id, node]: _graph.nodes) - if (node.first == _root) + if (node.name == _root) { rootId = id; break; @@ -1330,18 +1330,18 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& if (edges.size() == 2) { interfaceId = edges.at(1); - if (!Predicate::predicate(_graph.nodes.at(summaryId).first)->isSummary()) + if (!Predicate::predicate(_graph.nodes.at(summaryId).name)->isSummary()) swap(summaryId, *interfaceId); - auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first); + auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).name); solAssert(interfacePredicate && interfacePredicate->isInterface(), ""); } /// The children are unordered, so we need to check which is the summary and /// which is the interface. - Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).first); + Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).name); 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; + vector summaryArgs = _graph.nodes.at(summaryId).arguments; FunctionDefinition const* calledFun = summaryPredicate->programFunction(); ContractDefinition const* calledContract = summaryPredicate->programContract(); @@ -1387,7 +1387,7 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& /// or stop. if (interfaceId) { - Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first); + Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).name); solAssert(interfacePredicate && interfacePredicate->isInterface(), ""); node = *interfaceId; } @@ -1403,7 +1403,14 @@ string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex) string dot = "digraph {\n"; auto pred = [&](CHCSolverInterface::CexNode const& _node) { - return "\"" + _node.first + "(" + boost::algorithm::join(_node.second, ", ") + ")\""; + vector args = applyMap( + _node.arguments, + [&](auto const& arg) { + solAssert(arg.arguments.empty(), ""); + return arg.name; + } + ); + return "\"" + _node.name + "(" + boost::algorithm::join(args, ", ") + ")\""; }; for (auto const& [u, vs]: _cex.edges) diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 0bae37084..8d801ccb8 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -203,7 +203,7 @@ private: /// @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 + std::string formatVariableModel(std::vector const& _variables, std::vector> const& _values, std::string const& _separator) const { solAssert(_variables.size() == _values.size(), ""); @@ -212,7 +212,10 @@ private: { auto var = _variables.at(i); if (var && var->type()->isValueType()) - assignments.emplace_back(var->name() + " = " + _values.at(i)); + { + solAssert(_values.at(i), ""); + assignments.emplace_back(var->name() + " = " + *_values.at(i)); + } } return boost::algorithm::join(assignments, _separator); diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index b1fa9b19d..d3deaa141 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -149,7 +149,7 @@ bool Predicate::isInterface() const return functor().name.rfind("interface", 0) == 0; } -string Predicate::formatSummaryCall(vector const& _args) const +string Predicate::formatSummaryCall(vector const& _args) const { if (programContract()) return "constructor()"; @@ -163,18 +163,22 @@ string Predicate::formatSummaryCall(vector const& _args) const /// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in preInputVars. - vector::const_iterator first = _args.begin() + 5 + static_cast(stateVars->size()); - vector::const_iterator last = first + static_cast(fun->parameters().size()); + auto first = _args.begin() + 5 + static_cast(stateVars->size()); + auto 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); + auto inTypes = FunctionType(*fun).parameterTypes(); + vector> functionArgsCex = formatExpressions(vector(first, last), inTypes); 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]); + { + solAssert(functionArgsCex.at(i), ""); + functionArgs.emplace_back(*functionArgsCex.at(i)); + } else functionArgs.emplace_back(params[i]->name()); @@ -186,7 +190,7 @@ string Predicate::formatSummaryCall(vector const& _args) const } -vector Predicate::summaryStateValues(vector const& _args) const +vector> Predicate::summaryStateValues(vector const& _args) const { /// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// The signature of an implicit constructor summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, postStateVars). @@ -194,8 +198,8 @@ vector Predicate::summaryStateValues(vector const& _args) const auto stateVars = stateVariables(); solAssert(stateVars.has_value(), ""); - vector::const_iterator stateFirst; - vector::const_iterator stateLast; + vector::const_iterator stateFirst; + vector::const_iterator stateLast; if (auto const* function = programFunction()) { stateFirst = _args.begin() + 5 + static_cast(stateVars->size()) + static_cast(function->parameters().size()) + 1; @@ -212,12 +216,13 @@ vector Predicate::summaryStateValues(vector const& _args) const solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), ""); solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), ""); - vector stateArgs(stateFirst, stateLast); + vector stateArgs(stateFirst, stateLast); solAssert(stateArgs.size() == stateVars->size(), ""); - return stateArgs; + auto stateTypes = applyMap(*stateVars, [&](auto const& _var) { return _var->type(); }); + return formatExpressions(stateArgs, stateTypes); } -vector Predicate::summaryPostInputValues(vector const& _args) const +vector> Predicate::summaryPostInputValues(vector const& _args) const { /// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in postInputVars. @@ -229,18 +234,19 @@ vector Predicate::summaryPostInputValues(vector const& _args) co auto const& inParams = function->parameters(); - vector::const_iterator first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; - vector::const_iterator last = first + static_cast(inParams.size()); + auto first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; + auto last = first + static_cast(inParams.size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), ""); - vector inValues(first, last); + vector inValues(first, last); solAssert(inValues.size() == inParams.size(), ""); - return inValues; + auto inTypes = FunctionType(*function).parameterTypes(); + return formatExpressions(inValues, inTypes); } -vector Predicate::summaryPostOutputValues(vector const& _args) const +vector> Predicate::summaryPostOutputValues(vector const& _args) const { /// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in outputVars. @@ -252,11 +258,46 @@ vector Predicate::summaryPostOutputValues(vector const& _args) c auto const& inParams = function->parameters(); - vector::const_iterator first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; + auto first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; solAssert(first >= _args.begin() && first <= _args.end(), ""); - vector outValues(first, _args.end()); + vector outValues(first, _args.end()); solAssert(outValues.size() == function->returnParameters().size(), ""); - return outValues; + auto outTypes = FunctionType(*function).returnParameterTypes(); + return formatExpressions(outValues, outTypes); +} + +vector> Predicate::formatExpressions(vector const& _exprs, vector const& _types) const +{ + solAssert(_exprs.size() == _types.size(), ""); + vector> strExprs; + for (unsigned i = 0; i < _exprs.size(); ++i) + strExprs.push_back(expressionToString(_exprs.at(i), _types.at(i))); + return strExprs; +} + +optional Predicate::expressionToString(smtutil::Expression const& _expr, TypePointer _type) const +{ + if (smt::isNumber(*_type)) + { + solAssert(_expr.sort->kind == Kind::Int, ""); + solAssert(_expr.arguments.empty(), ""); + // TODO assert that _expr.name is a number. + return _expr.name; + } + if (smt::isBool(*_type)) + { + solAssert(_expr.sort->kind == Kind::Bool, ""); + solAssert(_expr.arguments.empty(), ""); + solAssert(_expr.name == "true" || _expr.name == "false", ""); + return _expr.name; + } + if (smt::isFunction(*_type)) + { + solAssert(_expr.arguments.empty(), ""); + return _expr.name; + } + + return {}; } diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index a87e81afa..9a05c3008 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -107,21 +107,27 @@ public: /// @returns a formatted string representing a call to this predicate /// with _args. - std::string formatSummaryCall(std::vector const& _args) const; + 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; + 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; + 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; + std::vector> summaryPostOutputValues(std::vector const& _args) const; private: + /// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants. + std::vector> formatExpressions(std::vector const& _exprs, std::vector const& _types) const; + + /// @returns a string representation of the SMT expression based on a Solidity type. + std::optional expressionToString(smtutil::Expression const& _expr, TypePointer _type) const; + /// The actual SMT expression. smt::SymbolicFunctionVariable m_predicate;