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 #6652 from ethereum/smt_tuple_function

Browse Source 
[SMTChecker] Support tuples as function calls with multiple return values
This commit is contained in:
Leonardo
2019-05-06 15:19:24 +02:00
committed by GitHub
parent 442742e497 5440a53d4d
commit e99efec085
8 changed files with 96 additions and 32 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTChecker.cpp
+37 -27
View File
@@ -705,8 +705,8 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
{
FunctionDefinition const* _funDef = inlinedFunctionCallToDefinition(_funCall);
if (!_funDef)
FunctionDefinition const* funDef = inlinedFunctionCallToDefinition(_funCall);
if (!funDef)
{
m_errorReporter.warning(
_funCall.location(),
@@ -715,11 +715,11 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
return;
}
if (visitedFunction(_funDef))
if (visitedFunction(funDef))
m_errorReporter.warning(
_funCall.location(),
"Assertion checker does not support recursive function calls.",
SecondarySourceLocation().append("Starting from function:", _funDef->location())
SecondarySourceLocation().append("Starting from function:", funDef->location())
);
else
{
@@ -727,27 +727,36 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
Expression const* calledExpr = &_funCall.expression();
auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
solAssert(funType, "");
if (funType->bound())
{
auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
solAssert(boundFunction, "");
funArgs.push_back(expr(boundFunction->expression()));
}
for (auto arg: _funCall.arguments())
funArgs.push_back(expr(*arg));
initializeFunctionCallParameters(*_funDef, funArgs);
_funDef->accept(*this);
auto const& returnParams = _funDef->returnParameters();
if (_funDef->returnParameters().size())
initializeFunctionCallParameters(*funDef, funArgs);
funDef->accept(*this);
createExpr(_funCall);
auto const& returnParams = funDef->returnParameters();
if (returnParams.size() > 1)
{
if (returnParams.size() > 1)
m_errorReporter.warning(
_funCall.location(),
"Assertion checker does not yet support calls to functions that return more than one value."
);
else
defineExpr(_funCall, currentValue(*returnParams[0]));
vector<shared_ptr<SymbolicVariable>> components;
for (auto param: returnParams)
{
solAssert(m_variables[param.get()], "");
components.push_back(m_variables[param.get()]);
}
auto const& symbTuple = dynamic_pointer_cast<SymbolicTupleVariable>(m_expressions[&_funCall]);
solAssert(symbTuple, "");
symbTuple->setComponents(move(components));
}
else if (returnParams.size() == 1)
defineExpr(_funCall, currentValue(*returnParams.front()));
}
}
@@ -829,15 +838,11 @@ void SMTChecker::visitTypeConversion(FunctionCall const& _funCall)
void SMTChecker::visitFunctionIdentifier(Identifier const& _identifier)
{
auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type);
if (fType.returnParameterTypes().size() > 1)
if (fType.returnParameterTypes().size() == 1)
{
m_errorReporter.warning(
_identifier.location(),
"Assertion checker does not yet support functions with more than one return parameter."
);
defineGlobalFunction(fType.richIdentifier(), _identifier);
m_expressions.emplace(&_identifier, m_globalContext.at(fType.richIdentifier()));
}
defineGlobalFunction(fType.richIdentifier(), _identifier);
m_expressions.emplace(&_identifier, m_globalContext.at(fType.richIdentifier()));
}
void SMTChecker::endVisit(Literal const& _literal)
@@ -873,12 +878,17 @@ void SMTChecker::endVisit(Return const& _return)
{
auto returnParams = m_functionPath.back()->returnParameters();
if (returnParams.size() > 1)
m_errorReporter.warning(
_return.location(),
"Assertion checker does not yet support more than one return value."
);
{
auto tuple = dynamic_cast<TupleExpression const*>(_return.expression());
solAssert(tuple, "");
auto const& components = tuple->components();
solAssert(components.size() == returnParams.size(), "");
for (unsigned i = 0; i < returnParams.size(); ++i)
if (components.at(i))
m_interface->addAssertion(expr(*components.at(i)) == newValue(*returnParams.at(i)));
}
else if (returnParams.size() == 1)
m_interface->addAssertion(expr(*_return.expression()) == newValue(*returnParams[0]));
m_interface->addAssertion(expr(*_return.expression()) == newValue(*returnParams.front()));
}
}