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

This commit is contained in:
Alex Beregszaszi 2020-09-11 19:28:01 +01:00
parent 72f8a753a9
commit 961a199cf5
4 changed files with 122 additions and 3 deletions

View File

@ -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.

View File

@ -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))

View File

@ -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.

View File

@ -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.