From 961a199cf5233ebb68db4b2541604117409c15d2 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Fri, 11 Sep 2020 19:28:01 +0100 Subject: [PATCH] [SMTChecker] Support type(T).min and type(T).max --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 21 ++++- .../types/type_meta_unsupported.sol | 19 +++++ .../smtCheckerTests/types/type_minmax.sol | 84 +++++++++++++++++++ 4 files changed, 122 insertions(+), 3 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/types/type_meta_unsupported.sol create mode 100644 test/libsolidity/smtCheckerTests/types/type_minmax.sol diff --git a/Changelog.md b/Changelog.md index 7c710c3c3..6793285dc 100644 --- a/Changelog.md +++ b/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. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index e2f28d3c3..b6bb770af 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -881,16 +881,31 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) auto identifier = dynamic_cast(&_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(exprType); magicType->kind() == MagicType::Kind::MetaType) + { + auto const& memberName = _memberAccess.memberName(); + if (memberName == "min" || memberName == "max") + { + IntegerType const& integerType = dynamic_cast(*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)) diff --git a/test/libsolidity/smtCheckerTests/types/type_meta_unsupported.sol b/test/libsolidity/smtCheckerTests/types/type_meta_unsupported.sol new file mode 100644 index 000000000..bccec79b7 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/types/type_minmax.sol b/test/libsolidity/smtCheckerTests/types/type_minmax.sol new file mode 100644 index 000000000..2a59b7895 --- /dev/null +++ b/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.