Merge pull request #9780 from ethereum/smt-type-minmax

[SMTChecker] Support type(T).min and type(T).max

Changelog.md

@@ -6,6 +6,7 @@ Language Features:
 Compiler Features:
  * SMTChecker: Support shifts.
  * SMTChecker: Support structs.
+ * SMTChecker: Support ``type(T).min`` and ``type(T).max``.
  * Yul Optimizer: Prune unused parameters in functions.
  * Yul Optimizer: Try to simplify function names.
 

libsolidity/formal/SMTEncoder.cpp

@@ -881,16 +881,31 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 	auto identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression());
 	if (exprType->category() == Type::Category::Magic)
 	{
-		string accessedName;
 		if (identifier)
-			accessedName = identifier->name();
+			defineGlobalVariable(identifier->name() + "." + _memberAccess.memberName(), _memberAccess);
+		else if (auto magicType = dynamic_cast<MagicType const*>(exprType); magicType->kind() == MagicType::Kind::MetaType)
+		{
+			auto const& memberName = _memberAccess.memberName();
+			if (memberName == "min" || memberName == "max")
+			{
+				IntegerType const& integerType = dynamic_cast<IntegerType const&>(*magicType->typeArgument());
+				defineExpr(_memberAccess, memberName == "min" ? integerType.minValue() : integerType.maxValue());
+			}
+			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
+				m_errorReporter.warning(
+					7507_error,
+					_memberAccess.location(),
+					"Assertion checker does not yet support this expression."
+				);
+		}
 		else
 			m_errorReporter.warning(
 				9551_error,
 				_memberAccess.location(),
 				"Assertion checker does not yet support this expression."
 			);
-		defineGlobalVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
 		return false;
 	}
 	else if (smt::isNonRecursiveStruct(*exprType))

test/libsolidity/smtCheckerTests/types/type_meta_unsupported.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract A {
+}
+
+contract C {
+	function f() public pure {
+		assert(bytes(type(C).name).length != 0);
+		assert(type(A).creationCode.length != 0);
+		assert(type(A).runtimeCode.length != 0);
+	}
+}
+// ----
+// Warning 6328: (92-131): Assertion violation happens here.
+// Warning 6328: (135-175): Assertion violation happens here.
+// Warning 6328: (179-218): Assertion violation happens here.
+// Warning 7507: (105-117): Assertion checker does not yet support this expression.
+// Warning 7507: (142-162): Assertion checker does not yet support this expression.
+// Warning 7507: (186-205): Assertion checker does not yet support this expression.

test/libsolidity/smtCheckerTests/types/type_minmax.sol

@@ -0,0 +1,84 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(uint a) public pure {
+		assert(a <= type(uint).max);
+		assert(a >= type(uint).min);
+		require(a <= type(uint64).max);
+		assert(a <= type(uint64).max);
+		assert(a <= type(uint32).max);
+	}
+
+	function int_min() public pure {
+		int8 int8_min = type(int8).min;
+		assert(int8_min == -2**7);
+
+		int16 int16_min = type(int16).min;
+		assert(int16_min == -2**15);
+
+		int24 int24_min = type(int24).min;
+		assert(int24_min == -2**23);
+
+		int32 int32_min = type(int32).min;
+		assert(int32_min == -2**31);
+
+		int64 int64_min = type(int64).min;
+		assert(int64_min == -2**63);
+
+		int256 int256_min = type(int256).min;
+		assert(int256_min == -2**255);
+	}
+
+	function int_max() public pure {
+		int8 int8_max = type(int8).max;
+		assert(int8_max == 2**7-1);
+
+		int16 int16_max = type(int16).max;
+		assert(int16_max == 2**15-1);
+
+		int24 int24_max = type(int24).max;
+		assert(int24_max == 2**23-1);
+
+		int32 int32_max = type(int32).max;
+		assert(int32_max == 2**31-1);
+
+		int256 int256_max = type(int256).max;
+		assert(int256_max == 2**255-1);
+	}
+
+	function uint_min() public pure {
+		uint8 uint8_min = type(uint8).min;
+		assert(uint8_min == 0);
+
+		uint16 uint16_min = type(uint16).min;
+		assert(uint16_min == 0);
+
+		uint24 uint24_min = type(uint24).min;
+		assert(uint24_min == 0);
+
+		uint32 uint32_min = type(uint32).min;
+		assert(uint32_min == 0);
+
+		uint256 uint256_min = type(uint256).min;
+		assert(uint256_min == 0);
+	}
+
+	function uint_max() public pure {
+		uint8 uint8_max = type(uint8).max;
+		assert(uint8_max == 2**8-1);
+
+		uint16 uint16_max = type(uint16).max;
+		assert(uint16_max == 2**16-1);
+
+		uint24 uint24_max = type(uint24).max;
+		assert(uint24_max == 2**24-1);
+
+		uint32 uint32_max = type(uint32).max;
+		assert(uint32_max == 2**32-1);
+
+		uint256 uint256_max = type(uint256).max;
+		assert(uint256_max == 2**256-1);
+	}
+}
+// ----
+// Warning 6328: (211-240): Assertion violation happens here.