mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Refactor cex loop
This commit is contained in:
parent
5241b7b761
commit
11f56861c3
@ -1436,9 +1436,13 @@ The counterexample DAG has the following properties:
|
|||||||
that is, it represents the state of the contract before the function described above was called.
|
that is, it represents the state of the contract before the function described above was called.
|
||||||
3) Interface nodes also have property 2.
|
3) Interface nodes also have property 2.
|
||||||
|
|
||||||
The following algorithm starts collecting function summaries at the root node and repeats
|
We run a BFS on the DAG from the root node collecting the reachable function summaries from the given node.
|
||||||
for each interface node seen.
|
When a function summary is seen, the search continues with that summary as the new root for its subgraph.
|
||||||
Each function summary collected represents a transaction, and the final order is reversed.
|
The result of the search is a callgraph containing:
|
||||||
|
- Functions calls needed to reach the root node, that is, transaction entry points.
|
||||||
|
- Functions called by other functions (internal calls or external calls/internal transactions).
|
||||||
|
The BFS visit order and the shape of the DAG described in the previous paragraph guarantee that the order of
|
||||||
|
the function summaries in the callgraph of the error node is the reverse transaction trace.
|
||||||
|
|
||||||
The first function summary seen contains the values for the state, input and output variables at the
|
The first function summary seen contains the values for the state, input and output variables at the
|
||||||
error point.
|
error point.
|
||||||
@ -1458,51 +1462,28 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
|
|||||||
vector<string> path;
|
vector<string> path;
|
||||||
string localState;
|
string localState;
|
||||||
|
|
||||||
unsigned node = *rootId;
|
auto callGraph = summaryCalls(_graph, *rootId);
|
||||||
/// The first summary node seen in this loop represents the last transaction.
|
|
||||||
bool lastTxSeen = false;
|
bool first = true;
|
||||||
while (_graph.edges.at(node).size() >= 1)
|
for (auto summaryId: callGraph.at(*rootId))
|
||||||
{
|
{
|
||||||
auto const& edges = _graph.edges.at(node);
|
CHCSolverInterface::CexNode const& summaryNode = _graph.nodes.at(summaryId);
|
||||||
solAssert(edges.size() <= 2, "");
|
Predicate const* summaryPredicate = Predicate::predicate(summaryNode.name);
|
||||||
|
auto const& summaryArgs = summaryNode.arguments;
|
||||||
|
|
||||||
unsigned summaryId = edges.at(0);
|
|
||||||
optional<unsigned> interfaceId;
|
|
||||||
if (edges.size() == 2)
|
|
||||||
{
|
|
||||||
interfaceId = edges.at(1);
|
|
||||||
if (!Predicate::predicate(_graph.nodes.at(summaryId).name)->isSummary())
|
|
||||||
swap(summaryId, *interfaceId);
|
|
||||||
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).name);
|
|
||||||
solAssert(summaryPredicate && summaryPredicate->isSummary(), "");
|
|
||||||
/// At this point property 2 from the function description is verified for this node.
|
|
||||||
vector<smtutil::Expression> summaryArgs = _graph.nodes.at(summaryId).arguments;
|
|
||||||
|
|
||||||
FunctionDefinition const* calledFun = summaryPredicate->programFunction();
|
|
||||||
ContractDefinition const* calledContract = summaryPredicate->programContract();
|
|
||||||
|
|
||||||
solAssert((calledFun && !calledContract) || (!calledFun && calledContract), "");
|
|
||||||
auto stateVars = summaryPredicate->stateVariables();
|
auto stateVars = summaryPredicate->stateVariables();
|
||||||
solAssert(stateVars.has_value(), "");
|
solAssert(stateVars.has_value(), "");
|
||||||
auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
|
auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
|
||||||
solAssert(stateValues.size() == stateVars->size(), "");
|
solAssert(stateValues.size() == stateVars->size(), "");
|
||||||
|
|
||||||
/// This summary node is the end of a tx.
|
string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
|
||||||
/// 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,
|
if (first)
|
||||||
/// but not necessarily the summary of the function that contains the error.
|
|
||||||
if (!lastTxSeen)
|
|
||||||
{
|
{
|
||||||
lastTxSeen = true;
|
first = false;
|
||||||
/// Generate counterexample message local to the failed target.
|
/// Generate counterexample message local to the failed target.
|
||||||
localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
|
localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
|
||||||
if (calledFun)
|
if (auto calledFun = summaryPredicate->programFunction())
|
||||||
{
|
{
|
||||||
auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
|
auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
|
||||||
auto const& inParams = calledFun->parameters();
|
auto const& inParams = calledFun->parameters();
|
||||||
@ -1521,20 +1502,30 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
|
|||||||
path.emplace_back("State: " + modelMsg);
|
path.emplace_back("State: " + modelMsg);
|
||||||
}
|
}
|
||||||
|
|
||||||
string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
|
|
||||||
path.emplace_back(txCex);
|
path.emplace_back(txCex);
|
||||||
|
|
||||||
/// Stop when we reach the summary of the analyzed constructor.
|
|
||||||
if (summaryPredicate->type() == PredicateType::ConstructorSummary)
|
|
||||||
break;
|
|
||||||
|
|
||||||
/// Recurse on the next interface node which represents the previous transaction.
|
|
||||||
node = *interfaceId;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n");
|
return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
|
map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph const& _graph, unsigned _root)
|
||||||
|
{
|
||||||
|
map<unsigned, vector<unsigned>> calls;
|
||||||
|
|
||||||
|
solidity::util::BreadthFirstSearch<pair<unsigned, unsigned>>{{{_root, _root}}}.run([&](auto info, auto&& _addChild) {
|
||||||
|
auto [node, root] = info;
|
||||||
|
if (Predicate::predicate(_graph.nodes.at(node).name)->isSummary())
|
||||||
|
{
|
||||||
|
calls[root].push_back(node);
|
||||||
|
root = node;
|
||||||
|
}
|
||||||
|
for (auto v: _graph.edges.at(node))
|
||||||
|
_addChild({v, root});
|
||||||
|
});
|
||||||
|
|
||||||
|
return calls;
|
||||||
|
}
|
||||||
|
|
||||||
string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex)
|
string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex)
|
||||||
{
|
{
|
||||||
string dot = "digraph {\n";
|
string dot = "digraph {\n";
|
||||||
@ -1542,10 +1533,7 @@ string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex)
|
|||||||
auto pred = [&](CHCSolverInterface::CexNode const& _node) {
|
auto pred = [&](CHCSolverInterface::CexNode const& _node) {
|
||||||
vector<string> args = applyMap(
|
vector<string> args = applyMap(
|
||||||
_node.arguments,
|
_node.arguments,
|
||||||
[&](auto const& arg) {
|
[&](auto const& arg) { return arg.name; }
|
||||||
solAssert(arg.arguments.empty(), "");
|
|
||||||
return arg.name;
|
|
||||||
}
|
|
||||||
);
|
);
|
||||||
return "\"" + _node.name + "(" + boost::algorithm::join(args, ", ") + ")\"";
|
return "\"" + _node.name + "(" + boost::algorithm::join(args, ", ") + ")\"";
|
||||||
};
|
};
|
||||||
|
@ -207,6 +207,14 @@ private:
|
|||||||
|
|
||||||
std::optional<std::string> generateCounterexample(smtutil::CHCSolverInterface::CexGraph const& _graph, std::string const& _root);
|
std::optional<std::string> generateCounterexample(smtutil::CHCSolverInterface::CexGraph const& _graph, std::string const& _root);
|
||||||
|
|
||||||
|
/// @returns a call graph for function summaries in the counterexample graph.
|
||||||
|
/// The returned map also contains a key _root, whose value are the
|
||||||
|
/// summaries called by _root.
|
||||||
|
std::map<unsigned, std::vector<unsigned>> summaryCalls(
|
||||||
|
smtutil::CHCSolverInterface::CexGraph const& _graph,
|
||||||
|
unsigned _root
|
||||||
|
);
|
||||||
|
|
||||||
/// @returns a set of pairs _var = _value separated by _separator.
|
/// @returns a set of pairs _var = _value separated by _separator.
|
||||||
template <typename T>
|
template <typename T>
|
||||||
std::string formatVariableModel(std::vector<T> const& _variables, std::vector<std::optional<std::string>> const& _values, std::string const& _separator) const
|
std::string formatVariableModel(std::vector<T> const& _variables, std::vector<std::optional<std::string>> const& _values, std::string const& _separator) const
|
||||||
|
@ -144,6 +144,11 @@ bool Predicate::isSummary() const
|
|||||||
return m_type == PredicateType::ConstructorSummary || m_type == PredicateType::FunctionSummary;
|
return m_type == PredicateType::ConstructorSummary || m_type == PredicateType::FunctionSummary;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
bool Predicate::isConstructorSummary() const
|
||||||
|
{
|
||||||
|
return m_type == PredicateType::ConstructorSummary;
|
||||||
|
}
|
||||||
|
|
||||||
bool Predicate::isInterface() const
|
bool Predicate::isInterface() const
|
||||||
{
|
{
|
||||||
return m_type == PredicateType::Interface;
|
return m_type == PredicateType::Interface;
|
||||||
|
@ -98,6 +98,9 @@ public:
|
|||||||
/// @returns true if this predicate represents a summary.
|
/// @returns true if this predicate represents a summary.
|
||||||
bool isSummary() const;
|
bool isSummary() const;
|
||||||
|
|
||||||
|
/// @returns true if this predicate represents a constructor summary.
|
||||||
|
bool isConstructorSummary() const;
|
||||||
|
|
||||||
/// @returns true if this predicate represents an interface.
|
/// @returns true if this predicate represents an interface.
|
||||||
bool isInterface() const;
|
bool isInterface() const;
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user