From ade3b9951c4681e20d24bb3ed8f29dcab605ff6f Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Wed, 21 Oct 2020 17:57:34 +0200 Subject: [PATCH] [SMTChecker] Added support for selector when expression's value is known at compile time --- Changelog.md | 2 + libsolidity/formal/SMTEncoder.cpp | 10 ++++ .../function_selector_via_contract_name.sol | 20 ++++++++ .../function_selector/function_types_sig.sol | 31 +++++++++++++ .../function_selector/homer.sol | 46 +++++++++++++++++++ .../function_selector/selector.sol | 8 ++++ .../function_selector/selector_2.sol | 12 +++++ .../function_selector/selector_3.sol | 14 ++++++ 8 files changed, 143 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/function_selector/function_selector_via_contract_name.sol create mode 100644 test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol create mode 100644 test/libsolidity/smtCheckerTests/function_selector/homer.sol create mode 100644 test/libsolidity/smtCheckerTests/function_selector/selector.sol create mode 100644 test/libsolidity/smtCheckerTests/function_selector/selector_2.sol create mode 100644 test/libsolidity/smtCheckerTests/function_selector/selector_3.sol diff --git a/Changelog.md b/Changelog.md index 176137b31..9c5ea16ea 100644 --- a/Changelog.md +++ b/Changelog.md @@ -2,6 +2,8 @@ Compiler Features: * SMTChecker: Add division by zero checks in the CHC engine. + * SMTChecker: Support ``selector`` for expressions with value known at compile-time. + Bugfixes: * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 4e338ab5d..efd712644 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1145,6 +1145,16 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) } return false; } + else if ( + auto const* functionType = dynamic_cast(exprType); + functionType && + _memberAccess.memberName() == "selector" && + functionType->hasDeclaration() + ) + { + defineExpr(_memberAccess, functionType->externalIdentifier()); + return false; + } else m_errorReporter.warning( 7650_error, diff --git a/test/libsolidity/smtCheckerTests/function_selector/function_selector_via_contract_name.sol b/test/libsolidity/smtCheckerTests/function_selector/function_selector_via_contract_name.sol new file mode 100644 index 000000000..a1690519d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/function_selector/function_selector_via_contract_name.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; + +contract A { + function f() external {} + function g(uint256) external {} +} +contract B { + function f() external returns (uint256) {} + function g(uint256) external returns (uint256) {} +} +contract C { + function test1() external pure returns(bytes4, bytes4, bytes4, bytes4) { + return (A.f.selector, A.g.selector, B.f.selector, B.g.selector); + } + function test2() external pure returns(bytes4, bytes4, bytes4, bytes4) { + A a; B b; + return (a.f.selector, a.g.selector, b.f.selector, b.g.selector); + } +} +// ==== diff --git a/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol b/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol new file mode 100644 index 000000000..b49c3ac51 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol @@ -0,0 +1,31 @@ +pragma experimental SMTChecker; + +contract C { + uint256 public x; + + function f() public pure returns (bytes4) { + return this.f.selector; + } + + function g() public view returns (bytes4) { + function () pure external returns (bytes4) fun = this.f; + return fun.selector; + } + + function i() public pure returns (bytes4) { + return this.x.selector; + } + + function check() public view { + assert(f() == 0x26121ff0); + assert(g() == 0x26121ff0); + assert(i() == 0x0c55699c); + assert(i() == 0x26121ff0); + } +} +// ---- +// Warning 6328: (470-495): CHC: Assertion violation happens here. +// Warning 6328: (540-565): CHC: Assertion violation happens here. +// Warning 6031: (261-267): Internal error: Expression undefined for SMT solver. +// Warning 7650: (284-296): Assertion checker does not yet support this expression. +// Warning 7650: (284-296): Assertion checker does not yet support this expression. diff --git a/test/libsolidity/smtCheckerTests/function_selector/homer.sol b/test/libsolidity/smtCheckerTests/function_selector/homer.sol new file mode 100644 index 000000000..a858a7714 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/function_selector/homer.sol @@ -0,0 +1,46 @@ +pragma experimental SMTChecker; + +interface ERC165 { + /// @notice Query if a contract implements an interface + /// @param interfaceID The interface identifier, as specified in ERC-165 + /// @dev Interface identification is specified in ERC-165. This function + /// uses less than 30,000 gas. + /// @return `true` if the contract implements `interfaceID` and + /// `interfaceID` is not 0xffffffff, `false` otherwise + function supportsInterface(bytes4 interfaceID) external view returns (bool); +} + +interface Simpson { + function is2D() external returns (bool); + function skinColor() external returns (string memory); +} + +interface PeaceMaker { + function achieveWorldPeace() external; +} + +contract Homer is ERC165, Simpson { + function supportsInterface(bytes4 interfaceID) public pure override returns (bool) { + return + interfaceID == this.supportsInterface.selector || // ERC165 + interfaceID == this.is2D.selector ^ this.skinColor.selector; // Simpson + } + + function is2D() external pure override returns (bool) { + return true; + } + + function skinColor() external pure override returns (string memory) { + return "yellow"; + } + + function check() public pure { + assert(supportsInterface(type(Simpson).interfaceId)); + assert(supportsInterface(type(ERC165).interfaceId)); + assert(supportsInterface(type(PeaceMaker).interfaceId)); + } +} + + +// ---- +// Warning 6328: (1373-1428): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/function_selector/selector.sol b/test/libsolidity/smtCheckerTests/function_selector/selector.sol new file mode 100644 index 000000000..b1339ed54 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/function_selector/selector.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + assert(msg.sig == this.f.selector); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/function_selector/selector_2.sol b/test/libsolidity/smtCheckerTests/function_selector/selector_2.sol new file mode 100644 index 000000000..beaf88465 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/function_selector/selector_2.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + function g() external pure { + } + + function f() public pure { + assert(msg.sig == this.g.selector); + } +} +// ---- +// Warning 6328: (125-159): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/function_selector/selector_3.sol b/test/libsolidity/smtCheckerTests/function_selector/selector_3.sol new file mode 100644 index 000000000..072113553 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/function_selector/selector_3.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + + +contract C { + int public x; + int public y; + + function f() public pure { + assert(this.x.selector != this.y.selector); + assert(this.x.selector == this.y.selector); + } +} +// ---- +// Warning 6328: (175-217): CHC: Assertion violation happens here.