From f9fa76c9d3177c629c0f94094867f81cbd8f50cc Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Mon, 20 Dec 2021 13:59:30 +0100 Subject: [PATCH] smt encode call --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 11 ++++++++ .../abi/abi_encode_call_simple.sol | 26 ------------------- .../abi/abi_encode_call_simple_1.sol | 22 ++++++++++++++++ .../abi/abi_encode_call_simple_2.sol | 21 +++++++++++++++ .../abi/abi_encode_call_simple_3.sol | 21 +++++++++++++++ .../abi/abi_encode_call_simple_4.sol | 25 ++++++++++++++++++ .../abi/abi_encode_call_simple_5.sol | 25 ++++++++++++++++++ 8 files changed, 126 insertions(+), 26 deletions(-) delete mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_1.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_2.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_3.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_4.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_5.sol diff --git a/Changelog.md b/Changelog.md index 203081823..26ba5965d 100644 --- a/Changelog.md +++ b/Changelog.md @@ -7,6 +7,7 @@ Compiler Features: * Peephole Optimizer: Remove operations without side effects before simple terminations. * Assembly-Json: Export: Include source list in `sourceList` field. * Commandline Interface: option ``--pretty-json`` works also with the following options: ``--abi``, ``--asm-json``, ``--ast-compact-json``, ``--devdoc``, ``--storage-layout``, ``--userdoc``. + * SMTChecker: Support ``abi.encodeCall`` taking into account the called selector. Bugfixes: diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 7cc978d28..8c5dd647e 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -586,6 +586,16 @@ bool SMTEncoder::visit(FunctionCall const& _funCall) arg->accept(*this); return false; } + else if (funType.kind() == FunctionType::Kind::ABIEncodeCall) + { + auto fun = _funCall.arguments().front(); + createExpr(*fun); + auto const* functionType = dynamic_cast(fun->annotation().type); + if (functionType->hasDeclaration()) + defineExpr(*fun, functionType->externalIdentifier()); + return true; + } + // We do not really need to visit the expression in a wrap/unwrap no-op call, // so we just ignore the function call expression to avoid "unsupported" warnings. else if ( @@ -1323,6 +1333,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) auto const& exprType = memberExpr->annotation().type; solAssert(exprType, ""); + if (exprType->category() == Type::Category::Magic) { if (auto const* identifier = dynamic_cast(memberExpr)) diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple.sol deleted file mode 100644 index 72fd4290c..000000000 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple.sol +++ /dev/null @@ -1,26 +0,0 @@ -contract C { - function callMeMaybe(uint a, uint b, uint[] memory c) external {} - - function abiEncodeSimple(uint x, uint y, uint z, uint[] memory a, uint[] memory b) public view { - require(x == y); - bytes memory b1 = abi.encodeCall(this.callMeMaybe, (x, z, a)); - bytes memory b2 = abi.encodeCall(this.callMeMaybe, (y, z, a)); - assert(b1.length == b2.length); - - bytes memory b3 = abi.encodeCall(this.callMeMaybe, (y, z, b)); - assert(b1.length == b3.length); // should fail - } -} -// ==== -// SMTEngine: all -// SMTIgnoreCex: yes -// ---- -// Warning 6031: (233-249): Internal error: Expression undefined for SMT solver. -// Warning 6031: (298-314): Internal error: Expression undefined for SMT solver. -// Warning 6031: (398-414): Internal error: Expression undefined for SMT solver. -// Warning 1218: (330-360): CHC: Error trying to invoke SMT solver. -// Warning 1218: (430-460): CHC: Error trying to invoke SMT solver. -// Warning 6328: (330-360): CHC: Assertion violation might happen here. -// Warning 6328: (430-460): CHC: Assertion violation might happen here. -// Warning 4661: (330-360): BMC: Assertion violation happens here. -// Warning 4661: (430-460): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_1.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_1.sol new file mode 100644 index 000000000..be0bc4769 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_1.sol @@ -0,0 +1,22 @@ +contract C { + function callMeMaybe(uint a, uint b) external {} + + function abiEncodeSimple(uint x, uint y, uint z) public view { + require(x == y); + function (uint, uint) external f = this.callMeMaybe; + bytes memory b1 = abi.encodeCall(f, (x, z)); + bytes memory b2 = abi.encodeCall(f, (y, z)); + assert(b1.length == b2.length); // should hold + assert(b1[0] == b2[0]); // should hold + + bytes memory b3 = abi.encodeCall(this.callMeMaybe, (3, z)); + assert(b1.length == b3.length); // should hold, but we don't encode the length computation precisely + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 6368: (354-359): CHC: Out of bounds access happens here. +// Warning 6368: (363-368): CHC: Out of bounds access happens here. +// Warning 6328: (451-481): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_2.sol new file mode 100644 index 000000000..c6044a8cd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_2.sol @@ -0,0 +1,21 @@ +contract C { + function callMeMaybe(uint a, uint b) external {} + + function abiEncodeSimple(uint x, uint y, uint z) public view { + require(x == y); + bytes memory b1 = abi.encodeCall(this.callMeMaybe, (x, z)); + bytes memory b2 = abi.encodeCall(this.callMeMaybe, (y, z)); + assert(b1.length == b2.length); // should hold + assert(b1[0] == b2[0]); // should hold + + bytes memory b3 = abi.encodeCall(this.callMeMaybe, (3, z)); + assert(b1.length == b3.length); // should hold but we don't compute the length precisely + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 6368: (329-334): CHC: Out of bounds access happens here. +// Warning 6368: (338-343): CHC: Out of bounds access happens here. +// Warning 6328: (426-456): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_3.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_3.sol new file mode 100644 index 000000000..a3b20f7f7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_3.sol @@ -0,0 +1,21 @@ +contract C { + function callMeMaybe(uint a, uint b) external {} + + function abiEncodeSimple(uint x, uint y, uint z) public pure { + require(x == y); + bytes memory b1 = abi.encodeCall(C.callMeMaybe, (x, z)); + bytes memory b2 = abi.encodeCall(C.callMeMaybe, (y, z)); + assert(b1.length == b2.length); // should hold + assert(b1[0] == b2[0]); // should hold + + bytes memory b3 = abi.encodeCall(C.callMeMaybe, (3, z)); + assert(b1.length == b3.length); // should hold but we don't compute the length precisely + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 6368: (323-328): CHC: Out of bounds access happens here. +// Warning 6368: (332-337): CHC: Out of bounds access happens here. +// Warning 6328: (417-447): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_4.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_4.sol new file mode 100644 index 000000000..6f0128f8a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_4.sol @@ -0,0 +1,25 @@ +abstract contract D { + function no(uint a, uint b) external virtual; +} + +contract C { + function callMeMaybe(uint a, uint b) external {} + + function abiEncodeSimple(uint x, uint y, uint z) public pure { + require(x == y); + bytes memory b1 = abi.encodeCall(D.no, (x, z)); + bytes memory b2 = abi.encodeCall(D.no, (y, z)); + assert(b1.length == b2.length); // should hold + assert(b1[0] == b2[0]); // should hold + + bytes memory b3 = abi.encodeCall(D.no, (3, z)); + assert(b1.length == b3.length); // should hold but we don't compute the length precisely + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 6368: (377-382): CHC: Out of bounds access happens here. +// Warning 6368: (386-391): CHC: Out of bounds access happens here. +// Warning 6328: (462-492): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_5.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_5.sol new file mode 100644 index 000000000..98e42ad9f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_5.sol @@ -0,0 +1,25 @@ +abstract contract D { + function no(uint a, uint b) external virtual; +} + +contract C { + function callMeMaybe(uint a, uint b) external {} + + function abiEncodeSimple(D d, uint x, uint y, uint z) public pure { + require(x == y); + bytes memory b1 = abi.encodeCall(d.no, (x, z)); + bytes memory b2 = abi.encodeCall(d.no, (y, z)); + assert(b1.length == b2.length); // should hold + assert(b1[0] == b2[0]); // should hold + + bytes memory b3 = abi.encodeCall(d.no, (3, z)); + assert(b1.length == b3.length); // should hold but we don't compute the length precisely + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 6368: (382-387): CHC: Out of bounds access happens here. +// Warning 6368: (391-396): CHC: Out of bounds access happens here. +// Warning 6328: (467-497): CHC: Assertion violation happens here.