cerc-io/solidity
10
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 #9716 from ethereum/smt_fix_tuple_2

Browse Source 
[SMTChecker] Fix ICE on tuple assignment
This commit is contained in:
Leonardo 2020-09-01 10:44:34 +02:00 committed by GitHub
commit 20b359e5c5
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 27 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -21,6 +21,7 @@ Bugfixes:
* SMTChecker: Fix internal error on array implicit conversion. * SMTChecker: Fix internal error on array implicit conversion.
* SMTChecker: Fix internal error on fixed bytes index access. * SMTChecker: Fix internal error on fixed bytes index access.
* SMTChecker: Fix internal error on lvalue unary operators with tuples. * SMTChecker: Fix internal error on lvalue unary operators with tuples.
* SMTChecker: Fix internal error on tuple assignment.
* SMTChecker: Fix soundness of array ``pop``. * SMTChecker: Fix soundness of array ``pop``.
* References Resolver: Fix internal bug when using constructor for library. * References Resolver: Fix internal bug when using constructor for library.
* Yul Optimizer: Make function inlining order more resilient to whether or not unrelated source files are present. * Yul Optimizer: Make function inlining order more resilient to whether or not unrelated source files are present.

7
libsolidity/formal/SMTEncoder.cpp
View File

@ -1490,13 +1490,14 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
{ {
auto lTuple = dynamic_cast<TupleExpression const*>(innermostTuple(_left)); auto lTuple = dynamic_cast<TupleExpression const*>(innermostTuple(_left));
solAssert(lTuple, ""); solAssert(lTuple, "");
Expression const* right = innermostTuple(_right);
auto const& lComponents = lTuple->components(); auto const& lComponents = lTuple->components();
// If both sides are tuple expressions, we individually and potentially // If both sides are tuple expressions, we individually and potentially
// recursively assign each pair of components. // recursively assign each pair of components.
// This is because of potential type conversion. // This is because of potential type conversion.
if (auto rTuple = dynamic_cast<TupleExpression const*>(&_right)) if (auto rTuple = dynamic_cast<TupleExpression const*>(right))
{ {
auto const& rComponents = rTuple->components(); auto const& rComponents = rTuple->components();
solAssert(lComponents.size() == rComponents.size(), ""); solAssert(lComponents.size() == rComponents.size(), "");
@ -1517,13 +1518,13 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
} }
else else
{ {
auto rType = dynamic_cast<TupleType const*>(_right.annotation().type); auto rType = dynamic_cast<TupleType const*>(right->annotation().type);
solAssert(rType, ""); solAssert(rType, "");
auto const& rComponents = rType->components(); auto const& rComponents = rType->components();
solAssert(lComponents.size() == rComponents.size(), ""); solAssert(lComponents.size() == rComponents.size(), "");
auto symbRight = expr(_right); auto symbRight = expr(*right);
solAssert(symbRight.sort->kind == smtutil::Kind::Tuple, ""); solAssert(symbRight.sort->kind == smtutil::Kind::Tuple, "");
for (unsigned i = 0; i < lComponents.size(); ++i) for (unsigned i = 0; i < lComponents.size(); ++i)

11
test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_1.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
function f() public pure returns(int) {
int a;
(,, a) = ((((((1, 3, (((((2)))))))))));
assert(a == 2);
assert(a == 3);
}
}
// ----
// Warning 6328: (157-171): Assertion violation happens here

11
test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_2.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
function f() public pure returns(int) {
int a;
((,, a)) = ((((((1, 3, (((((2)))))))))));
assert(a == 2);
assert(a == 3);
}
}
// ----
// Warning 6328: (159-173): Assertion violation happens here