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

[SMTChecker] CHC create function return variables

Browse Source
This commit is contained in:
Leonardo Alt
2019-08-05 12:36:51 +02:00
parent 11632966c9
commit 369f8cd97f
6 changed files with 67 additions and 20 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+36 -5
View File
@@ -643,13 +643,15 @@ void SMTEncoder::endVisit(Return const& _return)
auto returnParams = m_callStack.back().first->returnParameters();
if (returnParams.size() > 1)
{
auto tuple = dynamic_cast<TupleExpression const*>(_return.expression());
solAssert(tuple, "");
auto const& components = tuple->components();
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*_return.expression()));
solAssert(symbTuple, "");
auto const& components = symbTuple->components();
solAssert(components.size() == returnParams.size(), "");
for (unsigned i = 0; i < returnParams.size(); ++i)
if (components.at(i))
m_context.addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i)));
{
solAssert(components.at(i), "");
m_context.addAssertion(components.at(i)->currentValue() == m_context.newValue(*returnParams.at(i)));
}
}
else if (returnParams.size() == 1)
m_context.addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
@@ -1411,3 +1413,32 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall cons
return funDef;
}
void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
{
FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
if (!funDef)
return;
auto const& returnParams = funDef->returnParameters();
for (auto param: returnParams)
createVariable(*param);
if (returnParams.size() > 1)
{
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
solAssert(symbTuple, "");
if (symbTuple->components().empty())
{
vector<shared_ptr<smt::SymbolicVariable>> components;
for (auto param: returnParams)
{
solAssert(m_context.knownVariable(*param), "");
components.push_back(m_context.variable(*param));
}
symbTuple->setComponents(move(components));
}
}
else if (returnParams.size() == 1)
defineExpr(_funCall, currentValue(*returnParams.front()));
}