cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Adjust counterexamples for synthesized calls to external contracts that are state variables in the analyzed contract

Browse Source
This commit is contained in:
Leo Alt 2021-10-12 11:28:40 +02:00
parent a66ba81dad
commit d4e4189a85
3 changed files with 72 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

106
libsolidity/formal/CHC.cpp
View File

@ -2053,60 +2053,63 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
Predicate const* summaryPredicate = Predicate::predicate(summaryNode.name);
auto const& summaryArgs = summaryNode.arguments;
auto stateVars = summaryPredicate->stateVariables();
solAssert(stateVars.has_value(), "");
auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
solAssert(stateValues.size() == stateVars->size(), "");
if (first)
if (!summaryPredicate->programVariable())
{
first = false;
/// Generate counterexample message local to the failed target.
localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
auto stateVars = summaryPredicate->stateVariables();
solAssert(stateVars.has_value(), "");
auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
solAssert(stateValues.size() == stateVars->size(), "");
if (auto calledFun = summaryPredicate->programFunction())
if (first)
{
auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
auto const& inParams = calledFun->parameters();
if (auto inStr = formatVariableModel(inParams, inValues, "\n"); !inStr.empty())
localState += inStr + "\n";
auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
auto const& outParams = calledFun->returnParameters();
if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty())
localState += outStr + "\n";
first = false;
/// Generate counterexample message local to the failed target.
localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
optional<unsigned> localErrorId;
solidity::util::BreadthFirstSearch<unsigned> bfs{{summaryId}};
bfs.run([&](auto _nodeId, auto&& _addChild) {
auto const& children = _graph.edges.at(_nodeId);
if (
children.size() == 1 &&
nodePred(children.front())->isFunctionErrorBlock()
)
{
localErrorId = children.front();
bfs.abort();
}
ranges::for_each(children, _addChild);
});
if (localErrorId.has_value())
if (auto calledFun = summaryPredicate->programFunction())
{
auto const* localError = nodePred(*localErrorId);
solAssert(localError && localError->isFunctionErrorBlock(), "");
auto const [localValues, localVars] = localError->localVariableValues(nodeArgs(*localErrorId));
if (auto localStr = formatVariableModel(localVars, localValues, "\n"); !localStr.empty())
localState += localStr + "\n";
auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
auto const& inParams = calledFun->parameters();
if (auto inStr = formatVariableModel(inParams, inValues, "\n"); !inStr.empty())
localState += inStr + "\n";
auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
auto const& outParams = calledFun->returnParameters();
if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty())
localState += outStr + "\n";
optional<unsigned> localErrorId;
solidity::util::BreadthFirstSearch<unsigned> bfs{{summaryId}};
bfs.run([&](auto _nodeId, auto&& _addChild) {
auto const& children = _graph.edges.at(_nodeId);
if (
children.size() == 1 &&
nodePred(children.front())->isFunctionErrorBlock()
)
{
localErrorId = children.front();
bfs.abort();
}
ranges::for_each(children, _addChild);
});
if (localErrorId.has_value())
{
auto const* localError = nodePred(*localErrorId);
solAssert(localError && localError->isFunctionErrorBlock(), "");
auto const [localValues, localVars] = localError->localVariableValues(nodeArgs(*localErrorId));
if (auto localStr = formatVariableModel(localVars, localValues, "\n"); !localStr.empty())
localState += localStr + "\n";
}
}
}
}
else
{
auto modelMsg = formatVariableModel(*stateVars, stateValues, ", ");
/// We report the state after every tx in the trace except for the last, which is reported
/// first in the code above.
if (!modelMsg.empty())
path.emplace_back("State: " + modelMsg);
else
{
auto modelMsg = formatVariableModel(*stateVars, stateValues, ", ");
/// We report the state after every tx in the trace except for the last, which is reported
/// first in the code above.
if (!modelMsg.empty())
path.emplace_back("State: " + modelMsg);
}
}
string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider);
@ -2135,6 +2138,12 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
if (calls.size() > callTraceSize + 1)
calls.front() += ", synthesized as:";
}
else if (pred->programVariable())
{
calls.front() += "-- action on external contract in state variable \"" + pred->programVariable()->name() + "\"";
if (calls.size() > callTraceSize + 1)
calls.front() += ", synthesized as:";
}
else if (pred->isFunctionSummary() && parentPred->isExternalCallUntrusted())
calls.front() += " -- reentrant call";
};
@ -2190,7 +2199,8 @@ map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph c
nodePred->isInternalCall() ||
nodePred->isExternalCallTrusted() ||
nodePred->isExternalCallUntrusted() ||
rootPred->isExternalCallUntrusted()
rootPred->isExternalCallUntrusted() ||
rootPred->programVariable()
))
{
calls[root].push_back(node);

10
libsolidity/formal/Predicate.cpp
View File

@ -144,6 +144,11 @@ FunctionCall const* Predicate::programFunctionCall() const
return dynamic_cast<FunctionCall const*>(m_node);
}
VariableDeclaration const* Predicate::programVariable() const
{
return dynamic_cast<VariableDeclaration const*>(m_node);
}
optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
{
if (m_contractContext)
@ -214,6 +219,9 @@ string Predicate::formatSummaryCall(
{
solAssert(isSummary(), "");
if (programVariable())
return {};
if (auto funCall = programFunctionCall())
{
if (funCall->location().hasText())
@ -342,6 +350,8 @@ vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
stateFirst = _args.begin() + 7 + static_cast<int>(stateVars->size());
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else if (programVariable())
return {};
else
solAssert(false, "");

4
libsolidity/formal/Predicate.h
View File

@ -115,6 +115,10 @@ public:
/// or nullptr otherwise.
FunctionCall const* programFunctionCall() const;
/// @returns the VariableDeclaration that this predicate represents
/// or nullptr otherwise.
VariableDeclaration const* programVariable() const;
/// @returns the program state variables in the scope of this predicate.
std::optional<std::vector<VariableDeclaration const*>> stateVariables() const;