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 #6764 from ethereum/smt_fix_tuple_ice

Browse Source 
[SMTChecker] Fix ICE in unsupported function calls with multi return values
This commit is contained in:
chriseth
2019-05-20 15:18:11 +02:00
committed by GitHub
parent bbf45c4af1 60a4f03d3d
commit e08f521b7e
10 changed files with 69 additions and 27 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTChecker.cpp
+14 -16
View File
@@ -334,7 +334,9 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
solAssert(symbTuple, "");
auto const& components = symbTuple->components();
auto const& declarations = _varDecl.declarations();
if (components.size() == declarations.size())
if (!components.empty())
{
solAssert(components.size() == declarations.size(), "");
for (unsigned i = 0; i < declarations.size(); ++i)
if (
components.at(i) &&
@@ -342,6 +344,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
m_context.knownVariable(*declarations.at(i))
)
assignment(*declarations.at(i), components.at(i)->currentValue(), declarations.at(i)->location());
}
}
}
else if (m_context.knownVariable(*_varDecl.declarations().front()))
@@ -632,6 +635,7 @@ void SMTChecker::endVisit(BinaryOperation const& _op)
void SMTChecker::endVisit(FunctionCall const& _funCall)
{
solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, "");
createExpr(_funCall);
if (_funCall.annotation().kind == FunctionCallKind::StructConstructorCall)
{
m_errorReporter.warning(
@@ -693,7 +697,6 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
checkCondition(thisBalance < expr(*value), _funCall.location(), "Insufficient funds", "address(this).balance", &thisBalance);
m_context.transfer(m_context.thisAddress(), expr(address), expr(*value));
createExpr(_funCall);
break;
}
default:
@@ -740,14 +743,8 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
{
FunctionDefinition const* funDef = inlinedFunctionCallToDefinition(_funCall);
if (!funDef)
{
m_errorReporter.warning(
_funCall.location(),
"Assertion checker does not yet implement this type of function call."
);
}
else if (visitedFunction(funDef))
solAssert(funDef, "");
if (visitedFunction(funDef))
m_errorReporter.warning(
_funCall.location(),
"Assertion checker does not support recursive function calls.",
@@ -778,7 +775,6 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
// The callstack entry is popped only in endVisit(FunctionDefinition) instead of here
// as well to avoid code duplication (not all entries are from inlined function calls).
createExpr(_funCall);
auto const& returnParams = funDef->returnParameters();
if (returnParams.size() > 1)
{
@@ -865,7 +861,6 @@ void SMTChecker::visitTypeConversion(FunctionCall const& _funCall)
defineExpr(_funCall, expr(*argument));
else
{
createExpr(_funCall);
m_context.setUnknownValue(*m_context.expression(_funCall));
auto const& funCallCategory = _funCall.annotation().type->category();
// TODO: truncating and bytesX needs a different approach because of right padding.
@@ -1348,10 +1343,13 @@ void SMTChecker::assignment(
else if (auto tuple = dynamic_cast<TupleExpression const*>(&_left))
{
auto const& components = tuple->components();
solAssert(_right.size() == components.size(), "");
for (unsigned i = 0; i < _right.size(); ++i)
if (auto component = components.at(i))
assignment(*component, {_right.at(i)}, component->annotation().type, component->location());
if (!_right.empty())
{
solAssert(_right.size() == components.size(), "");
for (unsigned i = 0; i < _right.size(); ++i)
if (auto component = components.at(i))
assignment(*component, {_right.at(i)}, component->annotation().type, component->location());
}
}
else
m_errorReporter.warning(