From 2c93278719d31f248ba4833f6dc1cc7829327b27 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 17 Jul 2020 10:00:25 +0200 Subject: [PATCH] Fix push().push() --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 24 ++++++++++++++++++- .../array_members/push_push_no_args_1.sol | 9 +++++++ .../push_push_no_args_1_fail.sol | 12 ++++++++++ .../array_members/push_push_no_args_2.sol | 11 +++++++++ .../push_push_no_args_2_fail.sol | 15 ++++++++++++ .../array_members/storage_pointer_push_1.sol | 18 ++++++++++++++ .../storage_pointer_push_1_safe.sol | 15 ++++++++++++ 8 files changed, 104 insertions(+), 1 deletion(-) create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1_safe.sol diff --git a/Changelog.md b/Changelog.md index e0987a919..134bd5df8 100644 --- a/Changelog.md +++ b/Changelog.md @@ -12,6 +12,7 @@ Bugfixes: * SMTChecker: Fix internal error when using bitwise operators on fixed bytes type. * SMTChecker: Fix internal error when using compound bitwise operator assignments on array indices inside branches. * SMTChecker: Fix error in events with indices of type static array. + * SMTChecker: Fix internal error in sequential storage array pushes (``push().push()`). * Type Checker: Fix overload resolution in combination with ``{value: ...}``. * Type Checker: Fix internal compiler error related to oversized types. * Code Generator: Avoid double cleanup when copying to memory. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index e3f16b2ef..417a16921 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1077,7 +1077,7 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall) m_context.addAssertion(symbArray->length() == oldLength + 1); if (arguments.empty()) - defineExpr(_funCall, element); + defineExpr(_funCall, smtutil::Expression::select(symbArray->elements(), oldLength)); arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue()); } @@ -1119,6 +1119,28 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression } else if (auto const* indexAccess = dynamic_cast(&_expr)) arrayIndexAssignment(*indexAccess, _array); + else if (auto const* funCall = dynamic_cast(&_expr)) + { + FunctionType const& funType = dynamic_cast(*funCall->expression().annotation().type); + if (funType.kind() == FunctionType::Kind::ArrayPush) + { + auto memberAccess = dynamic_cast(&funCall->expression()); + solAssert(memberAccess, ""); + auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); + solAssert(symbArray, ""); + + auto oldLength = symbArray->length(); + auto store = smtutil::Expression::store( + symbArray->elements(), + symbArray->length() - 1, + _array + ); + symbArray->increaseIndex(); + m_context.addAssertion(symbArray->elements() == store); + m_context.addAssertion(symbArray->length() == oldLength); + arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue()); + } + } else if (dynamic_cast(&_expr)) m_errorReporter.warning( 9599_error, diff --git a/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1.sol b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1.sol new file mode 100644 index 000000000..8acd7998a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + int[][] array2d; + function l() public { + array2d.push().push(); + assert(array2d.length > 0); + assert(array2d[array2d.length - 1].length > 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1_fail.sol b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1_fail.sol new file mode 100644 index 000000000..a85638189 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1_fail.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + int[][] array2d; + function l() public { + array2d.push().push(); + assert(array2d.length > 2); + assert(array2d[array2d.length - 1].length > 3); + } +} +// ---- +// Warning 4661: (113-139): Assertion violation happens here +// Warning 4661: (143-189): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2.sol b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2.sol new file mode 100644 index 000000000..b6fd8e8c9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +contract C { + int[][][] array2d; + function l() public { + array2d.push().push().push(); + assert(array2d.length > 0); + uint last = array2d[array2d.length - 1].length; + assert(last > 0); + assert(array2d[array2d.length - 1][last - 1].length > 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol new file mode 100644 index 000000000..3d22b862a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract C { + int[][][] array2d; + function l() public { + array2d.push().push().push(); + assert(array2d.length > 2); + uint last = array2d[array2d.length - 1].length; + assert(last > 3); + assert(array2d[array2d.length - 1][last - 1].length > 4); + } +} +// ---- +// Warning 4661: (122-148): Assertion violation happens here +// Warning 4661: (202-218): Assertion violation happens here +// Warning 4661: (222-278): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol b/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol new file mode 100644 index 000000000..527d06534 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; +contract C { + int[][] array2d; + function l() public { + s().push(); + // False positive. + // Knowledge is erased because `s()` is a storage pointer. + assert(array2d[2].length > 0); + } + function s() internal returns (int[] storage) { + array2d.push(); + array2d.push(); + array2d.push(); + return array2d[2]; + } +} +// ---- +// Warning 4661: (184-213): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1_safe.sol b/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1_safe.sol new file mode 100644 index 000000000..843b46b16 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1_safe.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract C { + int[][] array2d; + function l() public { + s(); + array2d[2].push(); + assert(array2d[2].length > 0); + } + function s() internal returns (int[] storage) { + array2d.push(); + array2d.push(); + array2d.push(); + return array2d[2]; + } +}