From 5440a53d4da3bb06a02774cf5c2d03c3569e4375 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 30 Apr 2019 08:58:08 +0200 Subject: [PATCH] [SMTChecker] Support tuples as function calls with multiple return values --- Changelog.md | 2 +- libsolidity/formal/SMTChecker.cpp | 64 +++++++++++-------- .../types/tuple_assignment.sol | 1 + .../smtCheckerTests/types/tuple_function.sol | 17 +++++ .../types/tuple_function_2.sol | 17 +++++ .../types/tuple_function_3.sol | 19 ++++++ .../smtCheckerTestsJSON/multi.json | 6 +- .../smtCheckerTestsJSON/simple.json | 2 +- 8 files changed, 96 insertions(+), 32 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/types/tuple_function.sol create mode 100644 test/libsolidity/smtCheckerTests/types/tuple_function_2.sol create mode 100644 test/libsolidity/smtCheckerTests/types/tuple_function_3.sol diff --git a/Changelog.md b/Changelog.md index 25c179c11..b0a612ec4 100644 --- a/Changelog.md +++ b/Changelog.md @@ -6,7 +6,7 @@ Language Features: Compiler Features: * SMTChecker: Support inherited state variables. - * SMTChecker: Support tuple assignments. + * SMTChecker: Support tuple assignments and function calls with multiple return values. Bugfixes: diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 83536bac1..588faa338 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -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(calledExpr->annotation().type); solAssert(funType, ""); + if (funType->bound()) { auto const& boundFunction = dynamic_cast(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> components; + for (auto param: returnParams) + { + solAssert(m_variables[param.get()], ""); + components.push_back(m_variables[param.get()]); + } + auto const& symbTuple = dynamic_pointer_cast(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(*_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(_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())); } } diff --git a/test/libsolidity/smtCheckerTests/types/tuple_assignment.sol b/test/libsolidity/smtCheckerTests/types/tuple_assignment.sol index 524e5e6ef..b6f9e2bf4 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_assignment.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_assignment.sol @@ -10,3 +10,4 @@ contract C assert(y == 4); } } +// ---- diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function.sol b/test/libsolidity/smtCheckerTests/types/tuple_function.sol new file mode 100644 index 000000000..53b197395 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/tuple_function.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() internal pure returns (uint, uint) { + return (2, 3); + } + function g() public pure { + uint x; + uint y; + (x,y) = f(); + assert(x == 1); + assert(y == 4); + } +} +// ---- +// Warning: (182-196): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol new file mode 100644 index 000000000..54223bea0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() internal pure returns (uint, uint) { + return (2, 3); + } + function g() public pure { + uint x; + uint y; + (x,) = f(); + assert(x == 2); + assert(y == 4); + } +} +// ---- +// Warning: (199-213): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol b/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol new file mode 100644 index 000000000..1e548403d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() internal pure returns (uint, bool, uint) { + return (2, false, 3); + } + function g() public pure { + uint x; + uint y; + bool b; + (,b,) = f(); + assert(x == 2); + assert(y == 4); + assert(!b); + } +} +// ---- +// Warning: (205-219): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json index c005382be..ba4cf2637 100644 --- a/test/libsolidity/smtCheckerTestsJSON/multi.json +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -3,9 +3,9 @@ { "smtlib2responses": { - "0x47a038dd9021ecb218726ea6bf1f75c215a50b1981bae4341e89c9f2b7ac5db7": "sat\n((|EVALEXPR_0| 1))\n", - "0xf057b272f2ceb99a2f714cb132960babdeedfb84ff8ffb96106a58bc0c2060cb": "sat\n((|EVALEXPR_0| 0))\n", - "0xf49b9d0eb7b6d2f2ac9e1604288e52ee1a08cda57058e26d7843ed109ca6d7c9": "unsat\n" + "0x092d52dc5c2b54c1909592f7b3c8efedfd87afc0223ce421a24a1cc7905006b4": "sat\n((|EVALEXPR_0| 1))\n", + "0x8faacfc008b6f2278b5927ff22d76832956dfb46b3c21a64fab96583c241b88f": "unsat\n", + "0xa66d08de30c873ca7d0e7e9e426f278640e0ee463a1aed2e4e80baee916b6869": "sat\n((|EVALEXPR_0| 0))\n" } } } diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json index f9935ab01..5c9c3872a 100644 --- a/test/libsolidity/smtCheckerTestsJSON/simple.json +++ b/test/libsolidity/smtCheckerTestsJSON/simple.json @@ -3,7 +3,7 @@ { "smtlib2responses": { - "0xf057b272f2ceb99a2f714cb132960babdeedfb84ff8ffb96106a58bc0c2060cb": "sat\n((|EVALEXPR_0| 0))\n" + "0xa66d08de30c873ca7d0e7e9e426f278640e0ee463a1aed2e4e80baee916b6869": "sat\n((|EVALEXPR_0| 0))\n" } } }