[SMTChecker] Added support for selector when expression's value is known at compile time

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.

libsolidity/formal/SMTEncoder.cpp

@@ -1145,6 +1145,16 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 		}
 		return false;
 	}
+	else if (
+		auto const* functionType = dynamic_cast<FunctionType const*>(exprType);
+		functionType &&
+		_memberAccess.memberName() == "selector" &&
+		functionType->hasDeclaration()
+	)
+	{
+		defineExpr(_memberAccess, functionType->externalIdentifier());
+		return false;
+	}
 	else
 		m_errorReporter.warning(
 			7650_error,

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);
+    }
+}
+// ====

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.

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.

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);
+    }
+}
+// ----

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.

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.