[SMTChecker] Support type(I).interfaceId

Changelog.md

@@ -6,7 +6,7 @@ Language Features:
 Compiler Features:
  * SMTChecker: Support shifts.
  * SMTChecker: Support structs.
- * SMTChecker: Support ``type(T).min`` and ``type(T).max``.
+ * SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``.
  * Yul Optimizer: Prune unused parameters in functions.
  * Yul Optimizer: Inline into functions further down in the call graph first.
  * Yul Optimizer: Try to simplify function names.

libsolidity/formal/SMTEncoder.cpp

@@ -888,6 +888,15 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 				IntegerType const& integerType = dynamic_cast<IntegerType const&>(*magicType->typeArgument());
 				defineExpr(_memberAccess, memberName == "min" ? integerType.minValue() : integerType.maxValue());
 			}
+			else if (memberName == "interfaceId")
+			{
+				// TODO: move this calculation into ContractDefinition and share with ExpressionCompiler
+				ContractDefinition const& contract = dynamic_cast<ContractType const&>(*magicType->typeArgument()).contractDefinition();
+				uint64_t result{0};
+				for (auto const& function: contract.interfaceFunctionList(false))
+					result ^= fromBigEndian<uint64_t>(function.first.ref());
+				defineExpr(_memberAccess, result);
+			}
 			else
 				// NOTE: supporting name, creationCode, runtimeCode would be easy enough, but the bytes/string they return are not
 				//       at all useable in the SMT checker currently

test/libsolidity/smtCheckerTests/types/type_interfaceid.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+interface I1 {
+}
+
+interface I2 {
+	function f() external;
+}
+
+interface I3 {
+	function f() external;
+	function g(uint, address) external;
+}
+
+contract C {
+	function f() public pure {
+		assert(type(I1).interfaceId == 0);
+		assert(type(I2).interfaceId != 0);
+		assert(type(I2).interfaceId == 0x26121ff0);
+		assert(type(I2).interfaceId != 0);
+		assert(type(I3).interfaceId == 0x822b51c6);
+	}
+	function g() public pure {
+		assert(type(I1).interfaceId == type(I2).interfaceId);
+	}
+	function h() public pure {
+		assert(type(I2).interfaceId == type(I3).interfaceId);
+	}
+}
+// ----
+// Warning 6328: (449-501): Assertion violation happens here.
+// Warning 6328: (536-588): Assertion violation happens here.