From 6edfdff187f070951894da905f661b0ea31082b4 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Thu, 24 Sep 2020 10:32:56 +0100 Subject: [PATCH] [SMTChecker] Do not warn on "abi" as an identifer There is an approprate warning for the function call. --- libsolidity/formal/SMTEncoder.cpp | 7 ++++ .../smtCheckerTests/complex/MerkleProof.sol | 2 - .../complex/slither/external_function.sol | 1 - .../functions/abi_encode_functions.sol | 2 - .../special/abi_decode_memory_v2.sol | 17 ++++----- .../abi_decode_memory_v2_value_types.sol | 24 ++++++------ .../special/abi_decode_simple.sol | 37 +++++++++---------- .../special/abi_encode_slice.sol | 9 +++++ .../types/function_in_tuple_1.sol | 1 - .../types/function_in_tuple_2.sol | 1 - 10 files changed, 52 insertions(+), 49 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index a446e47bf..69435f0a6 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -748,6 +748,13 @@ void SMTEncoder::endVisit(Identifier const& _identifier) defineExpr(_identifier, m_context.state().thisAddress()); m_uninterpretedTerms.insert(&_identifier); } + // Ignore the builtin abi, it is handled in FunctionCall. + // TODO: ignore MagicType in general (abi, block, msg, tx, type) + else if (auto magicType = dynamic_cast(_identifier.annotation().type); magicType && magicType->kind() == MagicType::Kind::ABI) + { + solAssert(_identifier.name() == "abi", ""); + return; + } else createExpr(_identifier); } diff --git a/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol index 5d6d3d3cb..fb0f69ddc 100644 --- a/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol +++ b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol @@ -34,7 +34,5 @@ library MerkleProof { } // ---- -// Warning 8364: (988-991): Assertion checker does not yet implement type abi // Warning 4588: (988-1032): Assertion checker does not yet implement this type of function call. -// Warning 8364: (1175-1178): Assertion checker does not yet implement type abi // Warning 4588: (1175-1219): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol index 885200cf5..daecc82dc 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol @@ -83,7 +83,6 @@ contract InternalCall { // Warning 2018: (1144-1206): Function state mutability can be restricted to pure // Warning 2018: (1212-1274): Function state mutability can be restricted to pure // Warning 2018: (1280-1342): Function state mutability can be restricted to pure -// Warning 8364: (771-774): Assertion checker does not yet implement type abi // Warning 5084: (782-813): Type conversion is not yet fully supported and might yield false positives. // Warning 4588: (771-814): Assertion checker does not yet implement this type of function call. // Warning 5729: (1403-1408): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol b/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol index d03cd4bb5..2cf037ea5 100644 --- a/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol +++ b/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol @@ -5,7 +5,5 @@ contract C { } } // ---- -// Warning 8364: (162-165): Assertion checker does not yet implement type abi // Warning 4588: (162-176): Assertion checker does not yet implement this type of function call. -// Warning 8364: (178-181): Assertion checker does not yet implement type abi // Warning 4588: (178-203): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol index 1e2c354c9..26d17231e 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol @@ -2,14 +2,13 @@ pragma experimental SMTChecker; pragma experimental "ABIEncoderV2"; contract C { - struct S { uint x; uint[] b; } - function f() public pure returns (S memory, bytes memory, uint[][2] memory) { - return abi.decode("abc", (S, bytes, uint[][2])); - } + struct S { uint x; uint[] b; } + function f() public pure returns (S memory, bytes memory, uint[][2] memory) { + return abi.decode("abc", (S, bytes, uint[][2])); + } } // ---- -// Warning 8364: (206-209): Assertion checker does not yet implement type abi -// Warning 8364: (225-226): Assertion checker does not yet implement type type(struct C.S storage pointer) -// Warning 8364: (235-241): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (235-244): Assertion checker does not yet implement type type(uint256[] memory[2] memory) -// Warning 4588: (206-246): Assertion checker does not yet implement this type of function call. +// Warning 8364: (221-222): Assertion checker does not yet implement type type(struct C.S storage pointer) +// Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory) +// Warning 4588: (202-242): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol index 32992ca99..f0c58958b 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol @@ -2,18 +2,16 @@ pragma experimental SMTChecker; pragma experimental "ABIEncoderV2"; contract C { - function f() public pure { - (uint x1, bool b1) = abi.decode("abc", (uint, bool)); - (uint x2, bool b2) = abi.decode("abc", (uint, bool)); - // False positive until abi.* are implemented as uninterpreted functions. - assert(x1 == x2); - } + function f() public pure { + (uint x1, bool b1) = abi.decode("abc", (uint, bool)); + (uint x2, bool b2) = abi.decode("abc", (uint, bool)); + // False positive until abi.* are implemented as uninterpreted functions. + assert(x1 == x2); + } } // ---- -// Warning 2072: (125-132): Unused local variable. -// Warning 2072: (183-190): Unused local variable. -// Warning 6328: (303-319): Assertion violation happens here. -// Warning 8364: (136-139): Assertion checker does not yet implement type abi -// Warning 4588: (136-167): Assertion checker does not yet implement this type of function call. -// Warning 8364: (194-197): Assertion checker does not yet implement type abi -// Warning 4588: (194-225): Assertion checker does not yet implement this type of function call. +// Warning 2072: (122-129): Unused local variable. +// Warning 2072: (178-185): Unused local variable. +// Warning 6328: (300-316): Assertion violation happens here. +// Warning 4588: (133-164): Assertion checker does not yet implement this type of function call. +// Warning 4588: (189-220): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol index 11b97f724..4766d15da 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol @@ -1,24 +1,21 @@ pragma experimental SMTChecker; contract C { - function f() public pure { - (uint a1, bytes32 b1, C c1) = abi.decode("abc", (uint, bytes32, C)); - (uint a2, bytes32 b2, C c2) = abi.decode("abc", (uint, bytes32, C)); - // False positive until abi.* are implemented as uninterpreted functions. - assert(a1 == a2); - assert(a1 != a2); - } - + function f() public pure { + (uint a1, bytes32 b1, C c1) = abi.decode("abc", (uint, bytes32, C)); + (uint a2, bytes32 b2, C c2) = abi.decode("abc", (uint, bytes32, C)); + // False positive until abi.* are implemented as uninterpreted functions. + assert(a1 == a2); + assert(a1 != a2); + } } // ---- -// Warning 2072: (88-98): Unused local variable. -// Warning 2072: (100-104): Unused local variable. -// Warning 2072: (161-171): Unused local variable. -// Warning 2072: (173-177): Unused local variable. -// Warning 6328: (296-312): Assertion violation happens here. -// Warning 6328: (315-331): Assertion violation happens here. -// Warning 8364: (108-111): Assertion checker does not yet implement type abi -// Warning 8364: (142-143): Assertion checker does not yet implement type type(contract C) -// Warning 4588: (108-145): Assertion checker does not yet implement this type of function call. -// Warning 8364: (181-184): Assertion checker does not yet implement type abi -// Warning 8364: (215-216): Assertion checker does not yet implement type type(contract C) -// Warning 4588: (181-218): Assertion checker does not yet implement this type of function call. +// Warning 2072: (85-95): Unused local variable. +// Warning 2072: (97-101): Unused local variable. +// Warning 2072: (156-166): Unused local variable. +// Warning 2072: (168-172): Unused local variable. +// Warning 6328: (293-309): Assertion violation happens here. +// Warning 6328: (313-329): Assertion violation happens here. +// Warning 8364: (139-140): Assertion checker does not yet implement type type(contract C) +// Warning 4588: (105-142): Assertion checker does not yet implement this type of function call. +// Warning 8364: (210-211): Assertion checker does not yet implement type type(contract C) +// Warning 4588: (176-213): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol b/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol new file mode 100644 index 000000000..6a61a2618 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function f(bytes calldata data) external pure returns (bytes memory) { + return abi.encode(bytes(data[:32])); + } +} +// ---- +// Warning 2923: (143-152): Assertion checker does not yet implement this expression. +// Warning 4588: (126-154): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/function_in_tuple_1.sol b/test/libsolidity/smtCheckerTests/types/function_in_tuple_1.sol index 40b0c0b7a..1a41149e9 100644 --- a/test/libsolidity/smtCheckerTests/types/function_in_tuple_1.sol +++ b/test/libsolidity/smtCheckerTests/types/function_in_tuple_1.sol @@ -7,4 +7,3 @@ contract K { } // ---- // Warning 6133: (76-91): Statement has no effect. -// Warning 8364: (77-80): Assertion checker does not yet implement type abi diff --git a/test/libsolidity/smtCheckerTests/types/function_in_tuple_2.sol b/test/libsolidity/smtCheckerTests/types/function_in_tuple_2.sol index cecb9f967..f64311922 100644 --- a/test/libsolidity/smtCheckerTests/types/function_in_tuple_2.sol +++ b/test/libsolidity/smtCheckerTests/types/function_in_tuple_2.sol @@ -7,4 +7,3 @@ contract K { } // ---- // Warning 6133: (76-92): Statement has no effect. -// Warning 8364: (77-80): Assertion checker does not yet implement type abi