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

Merge pull request #10581 from blishko/issue-10524

Browse Source 
[SMTChecker] Fix handling of function calls where the function identifier is nested in a tuple.
This commit is contained in:
Leonardo 2020-12-14 17:20:18 +01:00 committed by GitHub
commit ccf1626f0d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 41 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsolidity/formal/SMTEncoder.cpp
View File

@ -2547,10 +2547,10 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall cons
FunctionDefinition const* funDef = nullptr; FunctionDefinition const* funDef = nullptr;
Expression const* calledExpr = &_funCall.expression(); Expression const* calledExpr = &_funCall.expression();
if (TupleExpression const* fun = dynamic_cast<TupleExpression const*>(&_funCall.expression())) if (TupleExpression const* fun = dynamic_cast<TupleExpression const*>(calledExpr))
{ {
solAssert(fun->components().size() == 1, ""); solAssert(fun->components().size() == 1, "");
calledExpr = fun->components().front().get(); calledExpr = innermostTuple(*calledExpr);
} }
if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr)) if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr))
@ -2689,6 +2689,7 @@ vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _f
unsigned firstParam = 0; unsigned firstParam = 0;
if (funType->bound()) if (funType->bound())
{ {
calledExpr = innermostTuple(*calledExpr);
auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr); auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
solAssert(boundFunction, ""); solAssert(boundFunction, "");
args.push_back(expr(boundFunction->expression(), functionParams.front()->type())); args.push_back(expr(boundFunction->expression(), functionParams.front()->type()));

15
test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_1.sol Normal file
View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C {
uint x;
function f() public {
x = 0;
((inc))();
assert(x == 1); // should hold
}
function inc() internal returns (uint) {
require(x < 100);
return ++x;
}
}

23
test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_2.sol Normal file
View File

@ -0,0 +1,23 @@
pragma experimental SMTChecker;
library L {
struct S {
uint256[] data;
}
function f(S memory _s) internal pure returns (uint256) {
require(_s.data.length > 0);
return 42;
}
}
contract C {
using L for L.S;
function f() public pure returns (uint256 y) {
L.S memory x;
y = (x.f)();
assert(y == 42); // should hold
}
}
// ----
// Warning 6031: (289-292): Internal error: Expression undefined for SMT solver.
// Warning 6031: (289-292): Internal error: Expression undefined for SMT solver.