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

Merge pull request #10727 from ethereum/smt_cex_internal_calls

Browse Source 
[SMTChecker] Report internal calls in CHC transaction trace
This commit is contained in:
Leonardo
2021-01-12 15:44:12 +01:00
committed by GitHub
parent 99add1e4e5 b3c3836388
commit fa28e48415
386 changed files with 642 additions and 569 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/CHC.cpp
+56 -14
View File
@@ -1072,12 +1072,12 @@ Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType,
return block;
}
Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract, PredicateType _type)
{
return createSymbolicBlock(
functionSort(_function, &_contract, state()),
"summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
PredicateType::FunctionSummary,
_type,
&_function
);
}
@@ -1179,6 +1179,8 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
case PredicateType::ConstructorSummary:
return constructor(_block, m_context);
case PredicateType::FunctionSummary:
case PredicateType::InternalCall:
case PredicateType::ExternalCall:
return smt::function(_block, m_currentContract, m_context);
case PredicateType::FunctionBlock:
solAssert(m_currentFunction, "");
@@ -1250,7 +1252,17 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
args.push_back(currentValue(*var));
}
return (*m_summaries.at(calledContract).at(function))(args);
Predicate const& summary = *m_summaries.at(calledContract).at(function);
auto from = smt::function(summary, calledContract, m_context);
Predicate const& callPredicate = *createSummaryBlock(
*function,
*calledContract,
kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCall
);
auto to = smt::function(callPredicate, calledContract, m_context);
addRule(smtutil::Expression::implies(from, to), to.name);
return callPredicate(args);
}
void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName)
@@ -1506,6 +1518,9 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
auto callGraph = summaryCalls(_graph, *rootId);
auto nodePred = [&](auto _node) { return Predicate::predicate(_graph.nodes.at(_node).name); };
auto nodeArgs = [&](auto _node) { return _graph.nodes.at(_node).arguments; };
bool first = true;
for (auto summaryId: callGraph.at(*rootId))
{
@@ -1518,8 +1533,6 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
solAssert(stateValues.size() == stateVars->size(), "");
string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
if (first)
{
first = false;
@@ -1529,10 +1542,12 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
{
auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
auto const& inParams = calledFun->parameters();
localState += formatVariableModel(inParams, inValues, "\n") + "\n";
if (auto inStr = formatVariableModel(inParams, inValues, "\n"); !inStr.empty())
localState += inStr + "\n";
auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
auto const& outParams = calledFun->returnParameters();
localState += formatVariableModel(outParams, outValues, "\n") + "\n";
if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty())
localState += outStr + "\n";
}
}
else
@@ -1544,7 +1559,23 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
path.emplace_back("State: " + modelMsg);
}
path.emplace_back(txCex);
string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
list<string> calls;
auto dfs = [&](unsigned node, unsigned depth, auto&& _dfs) -> void {
auto pred = nodePred(node);
solAssert(pred && pred->isSummary(), "");
if (!pred->isConstructorSummary())
for (unsigned v: callGraph[node])
_dfs(v, depth + 1, _dfs);
calls.push_front(string(depth * 2, ' ') + pred->formatSummaryCall(nodeArgs(node)));
if (pred->isInternalCall())
calls.front() += " -- internal call";
else if (pred->isExternalCall())
calls.front() += " -- external call";
};
dfs(summaryId, 0, dfs);
path.emplace_back(boost::algorithm::join(calls, "\n"));
}
return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n");
@@ -1554,16 +1585,27 @@ map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph c
{
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())
auto compare = [&](unsigned _a, unsigned _b) {
return _graph.nodes.at(_a).name > _graph.nodes.at(_b).name;
};
queue<pair<unsigned, unsigned>> q;
q.push({_root, _root});
while (!q.empty())
{
auto [node, root] = q.front();
q.pop();
Predicate const* nodePred = Predicate::predicate(_graph.nodes.at(node).name);
if (nodePred->isSummary() && (_root == root || nodePred->isInternalCall() || nodePred->isExternalCall()))
{
calls[root].push_back(node);
root = node;
}
for (auto v: _graph.edges.at(node))
_addChild({v, root});
});
auto const& edges = _graph.edges.at(node);
for (unsigned v: set<unsigned, decltype(compare)>(begin(edges), end(edges), compare))
q.push({v, root});
}
return calls;
}
libsolidity/formal/CHC.h
+7 -1
View File
@@ -147,7 +147,13 @@ private:
Predicate const* createBlock(ASTNode const* _node, PredicateType _predType, std::string const& _prefix = "");
/// Creates a call block for the given function _function from contract _contract.
/// The contract is needed here because of inheritance.
Predicate const* createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract);
/// There are different types of summaries, where the most common is FunctionSummary,
/// but other summaries are also used for internal and external function calls.
Predicate const* createSummaryBlock(
FunctionDefinition const& _function,
ContractDefinition const& _contract,
PredicateType _type = PredicateType::FunctionSummary
);
/// @returns a block related to @a _contract's constructor.
Predicate const* createConstructorBlock(ContractDefinition const& _contract, std::string const& _prefix);
libsolidity/formal/Predicate.cpp
+16 -1
View File
@@ -141,7 +141,22 @@ optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
bool Predicate::isSummary() const
{
return m_type == PredicateType::ConstructorSummary || m_type == PredicateType::FunctionSummary;
return m_type == PredicateType::ConstructorSummary || m_type == PredicateType::FunctionSummary || m_type == PredicateType::InternalCall || m_type == PredicateType::ExternalCall;
}
bool Predicate::isFunctionSummary() const
{
return m_type == PredicateType::FunctionSummary;
}
bool Predicate::isInternalCall() const
{
return m_type == PredicateType::InternalCall;
}
bool Predicate::isExternalCall() const
{
return m_type == PredicateType::ExternalCall;
}
bool Predicate::isConstructorSummary() const
libsolidity/formal/Predicate.h
+11
View File
@@ -37,6 +37,8 @@ enum class PredicateType
ConstructorSummary,
FunctionSummary,
FunctionBlock,
InternalCall,
ExternalCall,
Error,
Custom
};
@@ -98,6 +100,15 @@ public:
/// @returns true if this predicate represents a summary.
bool isSummary() const;
/// @returns true if this predicate represents a function summary.
bool isFunctionSummary() const;
/// @returns true if this predicate represents an internal function call.
bool isInternalCall() const;
/// @returns true if this predicate represents an external function call.
bool isExternalCall() const;
/// @returns true if this predicate represents a constructor summary.
bool isConstructorSummary() const;