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

[SMTChecker] Support tuples as function calls with multiple return values

Browse Source
This commit is contained in:
Leonardo Alt 2019-04-30 08:58:08 +02:00
parent befadea0c6
commit 5440a53d4d
8 changed files with 96 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -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:

64
libsolidity/formal/SMTChecker.cpp
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()));
}
}

1
test/libsolidity/smtCheckerTests/types/tuple_assignment.sol
View File

@ -10,3 +10,4 @@ contract C
assert(y == 4);
}
}
// ----

17
test/libsolidity/smtCheckerTests/types/tuple_function.sol Normal file
View File

@ -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

17
test/libsolidity/smtCheckerTests/types/tuple_function_2.sol Normal file
View File

@ -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

19
test/libsolidity/smtCheckerTests/types/tuple_function_3.sol Normal file
View File

@ -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

6
test/libsolidity/smtCheckerTestsJSON/multi.json
View File

@ -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"
}
}
}

2
test/libsolidity/smtCheckerTestsJSON/simple.json
View File

@ -3,7 +3,7 @@
{
"smtlib2responses":
{
"0xf057b272f2ceb99a2f714cb132960babdeedfb84ff8ffb96106a58bc0c2060cb": "sat\n((|EVALEXPR_0| 0))\n"
"0xa66d08de30c873ca7d0e7e9e426f278640e0ee463a1aed2e4e80baee916b6869": "sat\n((|EVALEXPR_0| 0))\n"
}
}
}