From 6e2fe1e340efedb599005507eb0c7f822b1a82cd Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Mon, 6 Sep 2021 23:54:14 +0200 Subject: [PATCH] [SMTChecker] Cleanup spurious messages about TypeTypes --- libsolidity/formal/SMTEncoder.cpp | 18 ++++++++++++++++++ libsolidity/formal/SMTEncoder.h | 1 + .../smtCheckerTests/abi/abi_decode_1_tuple.sol | 2 -- .../smtCheckerTests/abi/abi_decode_array.sol | 14 -------------- .../special/abi_decode_memory_v2.sol | 3 --- .../special/abi_decode_simple.sol | 2 -- .../smtCheckerTests/types/abi_type_type_1.sol | 10 ++++++++++ .../smtCheckerTests/types/abi_type_type_2.sol | 9 +++++++++ 8 files changed, 38 insertions(+), 21 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/types/abi_type_type_1.sol create mode 100644 test/libsolidity/smtCheckerTests/types/abi_type_type_2.sol diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 411fa2757..fdf5db5ca 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -560,6 +560,24 @@ bool SMTEncoder::visit(Conditional const& _op) return false; } +bool SMTEncoder::visit(FunctionCall const& _funCall) +{ + auto functionCallKind = *_funCall.annotation().kind; + if (functionCallKind != FunctionCallKind::FunctionCall) + return true; + + FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); + // We do not want to visit the TypeTypes in the second argument of `abi.decode`. + // Those types are checked/used in SymbolicState::buildABIFunctions. + if (funType.kind() == FunctionType::Kind::ABIDecode) + { + if (auto arg = _funCall.arguments().front()) + arg->accept(*this); + return false; + } + return true; +} + void SMTEncoder::endVisit(FunctionCall const& _funCall) { auto functionCallKind = *_funCall.annotation().kind; diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 28270acc0..a567a0fbf 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -152,6 +152,7 @@ protected: bool visit(BinaryOperation const& _node) override; void endVisit(BinaryOperation const& _node) override; bool visit(Conditional const& _node) override; + bool visit(FunctionCall const& _node) override; void endVisit(FunctionCall const& _node) override; bool visit(ModifierInvocation const& _node) override; void endVisit(Identifier const& _node) override; diff --git a/test/libsolidity/smtCheckerTests/abi/abi_decode_1_tuple.sol b/test/libsolidity/smtCheckerTests/abi/abi_decode_1_tuple.sol index e9c4e2043..d43f11b68 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_decode_1_tuple.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_decode_1_tuple.sol @@ -6,5 +6,3 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 8364: (116-125): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (115-126): Assertion checker does not yet implement type type(uint256[] memory) diff --git a/test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol b/test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol index 998503eb8..3c88329a3 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol @@ -32,20 +32,6 @@ contract C { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (283-289): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (291-297): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (532-538): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (540-546): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (548-554): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (769-775): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (769-777): Assertion checker does not yet implement type type(uint256[] memory[] memory) -// Warning 8364: (779-785): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (779-787): Assertion checker does not yet implement type type(uint256[] memory[] memory) -// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory) -// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory) // Warning 1218: (1009-1037): CHC: Error trying to invoke SMT solver. // Warning 1218: (1056-1084): CHC: Error trying to invoke SMT solver. // Warning 1218: (1103-1131): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol index a2d864b52..b9613a58c 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol @@ -9,6 +9,3 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 8364: (183-189): Assertion checker does not yet implement type type(uint256[] memory) -// Warning 8364: (183-192): Assertion checker does not yet implement type type(uint256[] memory[2] memory) -// Warning 8364: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer) diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol index 641b59440..bb82c659e 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol @@ -13,6 +13,4 @@ contract C { // Warning 2072: (82-86): Unused local variable. // Warning 2072: (140-150): Unused local variable. // Warning 2072: (152-156): Unused local variable. -// Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C) -// Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C) // Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\na1 = 2437\nb1 = 10\nc1 = 9\na2 = 2437\nb2 = 10\nc2 = 9\n\nTransaction trace:\nC.constructor()\nC.f(data) diff --git a/test/libsolidity/smtCheckerTests/types/abi_type_type_1.sol b/test/libsolidity/smtCheckerTests/types/abi_type_type_1.sol new file mode 100644 index 000000000..d4207bc86 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/abi_type_type_1.sol @@ -0,0 +1,10 @@ +contract C { + function f(bytes memory d) public pure { + (bool a, uint x) = abi.decode(d, (bool, uint)); + assert(a == (x == 2)); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (107-128): CHC: Assertion violation happens here.\nCounterexample:\n\na = true\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(d) diff --git a/test/libsolidity/smtCheckerTests/types/abi_type_type_2.sol b/test/libsolidity/smtCheckerTests/types/abi_type_type_2.sol new file mode 100644 index 000000000..e1730fedd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/abi_type_type_2.sol @@ -0,0 +1,9 @@ +contract C { + function f(bytes memory d) public pure { + assert(abi.decode(d, (bool))); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (57-86): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(d)