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

fixing try/catch encoding for BMC, refactoring

Browse Source
This commit is contained in:
Martin Blicha 2021-01-09 16:35:21 +01:00
parent 064e9a5de6
commit dd43ce1578
4 changed files with 33 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsolidity/formal/BMC.cpp
View File

@ -352,23 +352,29 @@ bool BMC::visit(TryStatement const& _tryStatement)
externalCall->accept(*this);
auto callExpr = expr(*externalCall);
smtutil::Expression clauseId = m_context.newVariable("clause_choice_" + to_string(m_context.newUniqueId()), smtutil::SortProvider::uintSort);
if (_tryStatement.successClause()->parameters())
tryCatchAssignment(
_tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall));
smtutil::Expression clauseId = m_context.newVariable("clause_choice_" + to_string(m_context.newUniqueId()), smtutil::SortProvider::uintSort);
auto const& clauses = _tryStatement.clauses();
m_context.addAssertion(clauseId >= 0 && clauseId < clauses.size());
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));
clausesVisitResults.push_back(visitBranch(clauses[i].get()));
touchedVars.push_back(touchedVariables(*clauses[i]));
}
// merge the information from all clauses
smtutil::Expression pathCondition = clausesVisitResults.front().second;
auto currentIndices = clausesVisitResults[0].first;
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);
mergeVariables(touchedVars[i - 1] + touchedVars[i], clauseId == i, clausesVisitResults[i].first, currentIndices);
currentIndices = copyVariableIndices();
pathCondition = pathCondition || clausesVisitResults[i].second;
}
setPathCondition(pathCondition);

21
libsolidity/formal/CHC.cpp
View File

@ -563,25 +563,8 @@ bool CHC::visit(TryStatement const& _tryStatement)
endVisit(*externalCall);
if (_tryStatement.successClause()->parameters())
{
auto const& params = _tryStatement.successClause()->parameters()->parameters();
if (params.size() > 1)
{
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*externalCall));
solAssert(symbTuple, "");
auto const& symbComponents = symbTuple->components();
solAssert(symbComponents.size() == params.size(), "");
for (unsigned i = 0; i < symbComponents.size(); ++i)
{
auto param = params.at(i);
solAssert(param, "");
solAssert(m_context.knownVariable(*param), "");
assignment(*param, symbTuple->component(i));
}
}
else if (params.size() == 1)
assignment(*params.front(), expr(*externalCall));
}
tryCatchAssignment(
_tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall));
connectBlocks(m_currentBlock, predicate(*tryAfterCallSuccessBlock));

20
libsolidity/formal/SMTEncoder.cpp
View File

@ -2107,6 +2107,26 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
return values.first;
}
void SMTEncoder::tryCatchAssignment(vector<shared_ptr<VariableDeclaration>> const& _variables, smt::SymbolicVariable const& _rhs)
{
if (_variables.size() > 1)
{
auto const* symbTuple = dynamic_cast<smt::SymbolicTupleVariable const*>(&_rhs);
solAssert(symbTuple, "");
auto const& symbComponents = symbTuple->components();
solAssert(symbComponents.size() == _variables.size(), "");
for (unsigned i = 0; i < symbComponents.size(); ++i)
{
auto param = _variables.at(i);
solAssert(param, "");
solAssert(m_context.knownVariable(*param), "");
assignment(*param, symbTuple->component(i));
}
}
else if (_variables.size() == 1)
assignment(*_variables.front(), _rhs.currentValue());
}
void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value)
{
// In general, at this point, the SMT sorts of _variable and _value are the same,

2
libsolidity/formal/SMTEncoder.h
View File

@ -238,6 +238,8 @@ protected:
void tupleAssignment(Expression const& _left, Expression const& _right);
/// Computes the right hand side of a compound assignment.
smtutil::Expression compoundAssignment(Assignment const& _assignment);
/// Handles assignment of the result of external call in try statement to the parameters of success clause
void tryCatchAssignment(std::vector<std::shared_ptr<VariableDeclaration>> const& _variables, smt::SymbolicVariable const& rhs);
/// Maps a variable to an SSA index.
using VariableIndices = std::unordered_map<VariableDeclaration const*, int>;