cerc-io/solidity
16
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

[SMTChecker] Basic support for try-catch in BMC

Browse Source
This commit is contained in:
Martin Blicha 2021-01-07 17:20:13 +01:00
parent 0f3924186e
commit 55589a9eec
2 changed files with 32 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
libsolidity/formal/BMC.cpp
View File

@ -345,6 +345,37 @@ bool BMC::visit(ForStatement const& _node)
return false;
}
bool BMC::visit(TryStatement const& _tryStatement)
{
FunctionCall const* externalCall = dynamic_cast<FunctionCall const*>(&_tryStatement.externalCall());
solAssert(externalCall && externalCall->annotation().tryCall, "");
externalCall->accept(*this);
auto callExpr = expr(*externalCall);
smtutil::Expression clauseId = m_context.newVariable("clause_choice_" + to_string(m_context.newUniqueId()), smtutil::SortProvider::uintSort);
auto const& clauses = _tryStatement.clauses();
solAssert(clauses[0].get() == _tryStatement.successClause(), "First clause of TryStatement should be the success clause");
vector<set<VariableDeclaration const*>> touchedVars;
vector<pair<VariableIndices, smtutil::Expression>> clausesVisitResults;
for (size_t i = 0; i < clauses.size(); ++i)
{
clausesVisitResults.push_back(visitBranch(clauses[i].get(), clauseId == i));
touchedVars.push_back(touchedVariables(*clauses[i]));
}
// merge the information from all clauses
smtutil::Expression pathCondition = clausesVisitResults.front().second;
for (size_t i = 1; i < clauses.size(); ++i)
{
mergeVariables(touchedVars[i - 1] + touchedVars[i], clauseId == (i - 1), clausesVisitResults[i - 1].first, clausesVisitResults[i].first);
pathCondition = pathCondition || clausesVisitResults[i].second;
}
setPathCondition(pathCondition);
return false;
}
void BMC::endVisit(UnaryOperation const& _op)
{
SMTEncoder::endVisit(_op);

1
libsolidity/formal/BMC.h
View File

@ -91,6 +91,7 @@ private:
void endVisit(UnaryOperation const& _node) override;
void endVisit(FunctionCall const& _node) override;
void endVisit(Return const& _node) override;
bool visit(TryStatement const& _node) override;
//@}
/// Visitor helpers.