cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #9938 from ethereum/smt-convert

Browse Source 
[SMTChecker] Support all type casts
This commit is contained in:
Leonardo 2020-10-02 13:45:33 +02:00 committed by GitHub
commit 6796ce7947
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
25 changed files with 401 additions and 71 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -3,6 +3,7 @@
Compiler Features:
* SMTChecker: Support ``addmod`` and ``mulmod``.
* SMTChecker: Support array slices.
* SMTChecker: Support type conversions.
* Optimizer: Optimize ``exp`` when base is -1.
* Code generator: Implemented events with function type as one of its indexed parameters.
* General: Option to stop compilation after parsing stage. Can be used with ``solc --stop-after parsing``

146
libsolidity/formal/SMTEncoder.cpp
View File

@ -817,43 +817,125 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
{
solAssert(*_funCall.annotation().kind == FunctionCallKind::TypeConversion, "");
solAssert(_funCall.arguments().size() == 1, "");
auto argument = _funCall.arguments().front();
auto const& argType = argument->annotation().type;
unsigned argSize = argument->annotation().type->storageBytes();
unsigned castSize = _funCall.annotation().type->storageBytes();
auto const& funCallCategory = _funCall.annotation().type->category();
// Allow casting number literals to address.
// TODO: remove the isNegative() check once the type checker disallows this
if (
auto const* numberType = dynamic_cast<RationalNumberType const*>(argument->annotation().type);
numberType && !numberType->isNegative() && (funCallCategory == Type::Category::Address)
)
defineExpr(_funCall, numberType->literalValue(nullptr));
else if (argSize == castSize)
defineExpr(_funCall, expr(*argument));
else
{
m_context.setUnknownValue(*m_context.expression(_funCall));
// TODO: truncating and bytesX needs a different approach because of right padding.
if (funCallCategory == Type::Category::Integer || funCallCategory == Type::Category::Address)
{
if (argSize < castSize)
defineExpr(_funCall, expr(*argument));
else
{
auto const& intType = dynamic_cast<IntegerType const&>(*m_context.expression(_funCall)->type());
defineExpr(_funCall, smtutil::Expression::ite(
expr(*argument) >= smt::minValue(intType) && expr(*argument) <= smt::maxValue(intType),
expr(*argument),
expr(_funCall)
));
}
}
m_errorReporter.warning(
5084_error,
_funCall.location(),
"Type conversion is not yet fully supported and might yield false positives."
auto const& funCallType = _funCall.annotation().type;
// TODO Simplify this whole thing for 0.8.0 where weird casts are disallowed.
auto symbArg = expr(*argument, funCallType);
bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType);
bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType);
optional<smtutil::Expression> symbMin;
optional<smtutil::Expression> symbMax;
if (smt::isNumber(*funCallType))
{
symbMin = smt::minValue(funCallType);
symbMax = smt::maxValue(funCallType);
}
if (argSize == castSize)
{
// If sizes are the same, it's possible that the signs are different.
if (smt::isNumber(*funCallType))
{
solAssert(smt::isNumber(*argType), "");
// castIsSigned && !argIsSigned => might overflow if arg > castType.max
// !castIsSigned && argIsSigned => might underflow if arg < castType.min
// !castIsSigned && !argIsSigned => ok
// castIsSigned && argIsSigned => ok
if (castIsSigned && !argIsSigned)
{
auto wrap = smtutil::Expression::ite(
symbArg > *symbMax,
symbArg - (*symbMax - *symbMin + 1),
symbArg
);
defineExpr(_funCall, wrap);
}
else if (!castIsSigned && argIsSigned)
{
auto wrap = smtutil::Expression::ite(
symbArg < *symbMin,
symbArg + (*symbMax + 1),
symbArg
);
defineExpr(_funCall, wrap);
}
else
defineExpr(_funCall, symbArg);
}
else
defineExpr(_funCall, symbArg);
}
else if (castSize > argSize)
{
solAssert(smt::isNumber(*funCallType), "");
// RationalNumbers have size 32.
solAssert(argType->category() != Type::Category::RationalNumber, "");
// castIsSigned && !argIsSigned => ok
// castIsSigned && argIsSigned => ok
// !castIsSigned && !argIsSigned => ok except for FixedBytesType, need to adjust padding
// !castIsSigned && argIsSigned => might underflow if arg < castType.min
if (!castIsSigned && argIsSigned)
{
auto wrap = smtutil::Expression::ite(
symbArg < *symbMin,
symbArg + (*symbMax + 1),
symbArg
);
defineExpr(_funCall, wrap);
}
else if (!castIsSigned && !argIsSigned)
{
if (auto const* fixedCast = dynamic_cast<FixedBytesType const*>(funCallType))
{
auto const* fixedArg = dynamic_cast<FixedBytesType const*>(argType);
solAssert(fixedArg, "");
auto diff = fixedCast->numBytes() - fixedArg->numBytes();
solAssert(diff > 0, "");
auto bvSize = fixedCast->numBytes() * 8;
defineExpr(
_funCall,
smtutil::Expression::bv2int(smtutil::Expression::int2bv(symbArg, bvSize) << smtutil::Expression::int2bv(diff * 8, bvSize))
);
}
else
defineExpr(_funCall, symbArg);
}
else
defineExpr(_funCall, symbArg);
}
else // castSize < argSize
{
solAssert(smt::isNumber(*funCallType), "");
auto const* fixedCast = dynamic_cast<FixedBytesType const*>(funCallType);
auto const* fixedArg = dynamic_cast<FixedBytesType const*>(argType);
if (fixedCast && fixedArg)
{
createExpr(_funCall);
auto diff = argSize - castSize;
solAssert(fixedArg->numBytes() - fixedCast->numBytes() == diff, "");
auto argValueBV = smtutil::Expression::int2bv(symbArg, argSize * 8);
auto shr = smtutil::Expression::int2bv(diff * 8, argSize * 8);
solAssert(!castIsSigned, "");
defineExpr(_funCall, smtutil::Expression::bv2int(argValueBV >> shr));
}
else
{
auto argValueBV = smtutil::Expression::int2bv(symbArg, castSize * 8);
defineExpr(_funCall, smtutil::Expression::bv2int(argValueBV, castIsSigned));
}
}
}

59
libsolidity/formal/SymbolicTypes.cpp
View File

@ -389,11 +389,47 @@ smtutil::Expression minValue(frontend::IntegerType const& _type)
return smtutil::Expression(_type.minValue());
}
smtutil::Expression minValue(frontend::TypePointer _type)
{
solAssert(isNumber(*_type), "");
if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
return intType->minValue();
if (auto const* fixedType = dynamic_cast<FixedPointType const*>(_type))
return fixedType->minIntegerValue();
if (
dynamic_cast<AddressType const*>(_type) ||
dynamic_cast<ContractType const*>(_type) ||
dynamic_cast<EnumType const*>(_type) ||
dynamic_cast<FixedBytesType const*>(_type)
)
return 0;
solAssert(false, "");
}
smtutil::Expression maxValue(frontend::IntegerType const& _type)
{
return smtutil::Expression(_type.maxValue());
}
smtutil::Expression maxValue(frontend::TypePointer _type)
{
solAssert(isNumber(*_type), "");
if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
return intType->maxValue();
if (auto const* fixedType = dynamic_cast<FixedPointType const*>(_type))
return fixedType->maxIntegerValue();
if (
dynamic_cast<AddressType const*>(_type) ||
dynamic_cast<ContractType const*>(_type)
)
return TypeProvider::uint(160)->maxValue();
if (auto const* enumType = dynamic_cast<EnumType const*>(_type))
return enumType->numberOfMembers();
if (auto const* bytesType = dynamic_cast<FixedBytesType const*>(_type))
return TypeProvider::uint(bytesType->numBytes() * 8)->maxValue();
solAssert(false, "");
}
void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context)
{
setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _context);
@ -458,6 +494,29 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type)
return 0;
}
bool isSigned(TypePointer const& _type)
{
solAssert(smt::isNumber(*_type), "");
bool isSigned = false;
if (auto const* numberType = dynamic_cast<RationalNumberType const*>(_type))
isSigned |= numberType->isNegative();
else if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
isSigned |= intType->isSigned();
else if (auto const* fixedType = dynamic_cast<FixedPointType const*>(_type))
isSigned |= fixedType->isSigned();
else if (
dynamic_cast<AddressType const*>(_type) ||
dynamic_cast<ContractType const*>(_type) ||
dynamic_cast<EnumType const*>(_type) ||
dynamic_cast<FixedBytesType const*>(_type)
)
return false;
else
solAssert(false, "");
return isSigned;
}
pair<unsigned, bool> typeBvSizeAndSignedness(frontend::TypePointer const& _type)
{
if (auto const* intType = dynamic_cast<IntegerType const*>(_type))

3
libsolidity/formal/SymbolicTypes.h
View File

@ -65,8 +65,11 @@ bool isNonRecursiveStruct(frontend::Type const& _type);
std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(frontend::Type const& _type, std::string const& _uniqueName, EncodingContext& _context);
smtutil::Expression minValue(frontend::IntegerType const& _type);
smtutil::Expression minValue(frontend::TypePointer _type);
smtutil::Expression maxValue(frontend::IntegerType const& _type);
smtutil::Expression maxValue(frontend::TypePointer _type);
smtutil::Expression zeroValue(frontend::TypePointer const& _type);
bool isSigned(frontend::TypePointer const& _type);
std::pair<unsigned, bool> typeBvSizeAndSignedness(frontend::TypePointer const& type);

1
test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
View File

@ -83,6 +83,5 @@ contract InternalCall {
// Warning 2018: (1144-1206): Function state mutability can be restricted to pure
// Warning 2018: (1212-1274): Function state mutability can be restricted to pure
// Warning 2018: (1280-1342): Function state mutability can be restricted to pure
// Warning 5084: (782-813): Type conversion is not yet fully supported and might yield false positives.
// Warning 4588: (771-814): Assertion checker does not yet implement this type of function call.
// Warning 5729: (1403-1408): Assertion checker does not yet implement this type of function call.

1
test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol
View File

@ -5,4 +5,3 @@ contract C {
}
}
// ----
// Warning 5084: (106-114): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol
View File

@ -5,4 +5,3 @@ contract C {
}
}
// ----
// Warning 5084: (101-109): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol
View File

@ -5,4 +5,3 @@ contract C {
}
}
// ----
// Warning 5084: (102-112): Type conversion is not yet fully supported and might yield false positives.

2
test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol
View File

@ -5,5 +5,3 @@ contract C {
}
}
// ----
// Warning 5084: (101-111): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (115-125): Type conversion is not yet fully supported and might yield false positives.

2
test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol
View File

@ -3,10 +3,8 @@ pragma experimental SMTChecker;
contract C {
function f() public pure {
uint x = uint(~1);
// This assertion fails because type conversion is still unsupported.
assert(x == 2**256 - 2);
assert(~1 == -2);
}
}
// ----
// Warning 6328: (169-192): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol
View File

@ -6,6 +6,3 @@ contract test {
}
// ----
// Warning 2072: (80-88): Unused local variable.
// Warning 4984: (91-112): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 5084: (91-100): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (103-112): Type conversion is not yet fully supported and might yield false positives.

10
test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol
View File

@ -7,20 +7,10 @@ contract C
uint32 b = uint16(a); // b will be 0x00001234
assert(b == 0x1234);
uint32 c = uint32(bytes4(a)); // c will be 0x12340000
// This fails because right padding is not supported.
assert(c == 0x12340000);
uint8 d = uint8(uint16(a)); // d will be 0x34
// False positive since truncating is not supported yet.
assert(d == 0x34);
uint8 e = uint8(bytes1(a)); // e will be 0x12
// False positive since truncating is not supported yet.
assert(e == 0x12);
}
}
// ----
// Warning 6328: (280-303): CHC: Assertion violation happens here.
// Warning 6328: (414-431): CHC: Assertion violation happens here.
// Warning 6328: (542-559): CHC: Assertion violation happens here.
// Warning 5084: (186-195): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (317-333): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (451-460): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol
View File

@ -9,4 +9,3 @@ contract C
}
}
// ----
// Warning 5084: (94-103): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol
View File

@ -10,4 +10,3 @@ contract C
}
}
// ----
// Warning 5084: (108-117): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol
View File

@ -10,4 +10,3 @@ contract C
}
// ----
// Warning 6328: (149-163): CHC: Assertion violation happens here.
// Warning 5084: (108-117): Type conversion is not yet fully supported and might yield false positives.

2
test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol
View File

@ -12,6 +12,4 @@ contract C
}
}
// ----
// Warning 6328: (207-230): CHC: Assertion violation happens here.
// Warning 6328: (273-287): CHC: Assertion violation happens here.
// Warning 5084: (108-117): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol
View File

@ -9,4 +9,3 @@ contract C
}
}
// ----
// Warning 5084: (94-102): Type conversion is not yet fully supported and might yield false positives.

4
test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol
View File

@ -5,10 +5,6 @@ contract C
function f() public pure {
uint32 a = 0x12345678;
uint16 b = uint16(a); // b will be 0x5678 now
// False positive since truncation is not supported yet.
assert(b == 0x5678);
}
}
// ----
// Warning 6328: (208-227): CHC: Assertion violation happens here.
// Warning 5084: (112-121): Type conversion is not yet fully supported and might yield false positives.

4
test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol
View File

@ -5,10 +5,6 @@ contract C
function f() public pure {
bytes2 a = 0x1234;
bytes1 b = bytes1(a); // b will be 0x12
// False positive since truncation is not supported yet.
assert(b == 0x12);
}
}
// ----
// Warning 6328: (198-215): CHC: Assertion violation happens here.
// Warning 5084: (108-117): Type conversion is not yet fully supported and might yield false positives.

48
test/libsolidity/smtCheckerTests/typecast/downcast.sol Normal file
View File

@ -0,0 +1,48 @@
pragma experimental SMTChecker;
contract C {
function f1() public pure {
// signed <- signed
int8 z = int8(-1);
assert(z == -1);
z = int8(0xf0ff);
assert(z == -1);
z = int8(0xcafecafef0ff);
assert(z == -1);
z = int8(0xcafecafe);
assert(z == -2);
z = int8(255);
assert(z == -1);
// unsigned <= unsigned
uint8 x = uint8(uint16(-1));
assert(x == 255);
x = uint8(uint256(-1));
assert(x == 255);
// signed <- unsigned
int8 y = int8(uint16(-1));
assert(y == -1);
y = int8(uint16(100));
assert(y == 100);
y = int8(uint16(200));
assert(y == -56);
// unsigned <- signed
uint8 v = uint8(int16(-1));
assert(v == 255);
v = uint8(int16(300));
assert(v == 44);
v = uint8(int16(200));
assert(v == 200);
// fixed bytes
bytes2 b = bytes2(bytes4(0xcafeffff));
assert(b == 0xcafe);
b = bytes2(bytes4(bytes8(0xaaaabbbbccccdddd)));
assert(b == 0xaaaa);
b = bytes2(bytes8(0xaaaabbbbccccdddd));
assert(b == 0xaaaa);
}
}
// ----

2
test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol
View File

@ -10,6 +10,4 @@ contract C
}
}
// ----
// Warning 6328: (140-160): CHC: Assertion violation happens here.
// Warning 8364: (132-133): Assertion checker does not yet implement type type(enum C.D)
// Warning 5084: (132-136): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/typecast/enum_to_uint_max_value.sol
View File

@ -9,4 +9,3 @@ contract C
}
}
// ----
// Warning 5084: (113-121): Type conversion is not yet fully supported and might yield false positives.

31
test/libsolidity/smtCheckerTests/typecast/number_literal.sol Normal file
View File

@ -0,0 +1,31 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
uint x = 1234;
uint y = 0;
assert(x != y);
assert(x == uint(1234));
assert(y == uint(0));
}
function g() public pure {
uint a = uint(0);
uint b = uint(-1);
uint c = 115792089237316195423570985008687907853269984665640564039457584007913129639935;
int d = -1;
uint e = uint(d);
assert(a != b);
assert(b == c);
assert(b == e);
}
function h() public pure {
uint32 a = uint32(0);
uint32 b = uint32(-1);
uint32 c = 4294967295;
int32 d = -1;
uint32 e = uint32(d);
assert(a != b);
assert(b == c);
assert(b == e);
}
}

74
test/libsolidity/smtCheckerTests/typecast/same_size.sol Normal file
View File

@ -0,0 +1,74 @@
pragma experimental SMTChecker;
abstract contract D {}
enum E {A, B}
contract C {
function f1() public pure {
// signed <- unsigned
int8 x = int8(uint8(200));
assert(x == -56);
int256 y = int256(uint256(2**255 + 10));
assert(y == -(2**255) + 10);
int256 z = int256(2**255 + 10);
assert(z == -(2**255) + 10);
int256 t = int256(bytes32(uint256(200)));
assert(t == 200);
int256 v = int256(bytes32(uint256(2**255 + 10)));
assert(v == -(2**255) + 10);
int160 a = int160(address(-1));
assert(a == -1);
int160 b = int160(address(2**159 + 10));
assert(b == -(2**159) + 10);
D d;
int160 e = int160(address(d));
assert(e == 0);
}
function f2() public pure {
// unsigned <- signed
uint8 x = uint8(int8(100));
assert(x == 100);
uint8 y = uint8(int8(200));
assert(y == 200);
uint8 z = uint8(int8(-100));
assert(z == 156);
uint8 t = uint8(int8(-200));
assert(t == 56);
uint256 v = uint256(int256(-200));
assert(v == 2**256 - 200);
uint256 w = uint256(-2);
assert(w == 2**256 - 2);
bytes4 b = bytes4(uint32(-2));
assert(uint32(b) == uint32(2**32 - 2));
address a = address(-1);
assert(uint160(a) == uint160(2**160 - 1));
address c = address(0);
assert(uint160(c) == 0);
D d;
address e = address(d);
assert(uint160(e) == 0);
E f = E(1);
assert(uint(f) == 1);
}
function f3() public pure {
// unsigned <- unsigned
uint8 x = uint8(bytes1(uint8(100)));
assert(x == 100);
address a = address(0);
assert(a == address(uint160(0)));
D d;
assert(a == address(d));
}
function f4() public pure {
// signed <- signed
int8 x = -10;
int8 y = int8(x);
assert(y == -10);
}
}
// ----
// Warning 8364: (1304-1305): Assertion checker does not yet implement type type(enum E)

70
test/libsolidity/smtCheckerTests/typecast/upcast.sol Normal file
View File

@ -0,0 +1,70 @@
pragma experimental SMTChecker;
abstract contract D {}
contract C {
function f1() public pure {
// unsigned <- signed
uint16 x = uint16(-1);
assert(x == 65535);
int8 i = int8(-1);
assert(i == -1);
x = uint16(int8(-1));
assert(x == 65535);
x = uint16(int16(i));
assert(x == 65535);
uint z = uint(i);
assert(z == 2**256 - 1);
}
function f2() public pure {
// signed <- unsigned
int16 y = int16(uint8(65535));
assert(y == 255);
int z = int(uint8(-1));
assert(z == 255);
z = int(uint8(255));
assert(z == 255);
}
function f3() public pure {
// signed <- signed
int16 y = int16(int8(65535));
assert(y == -1);
int z = int(int8(-1));
assert(z == -1);
z = int(int8(255));
assert(z == -1);
z = int(int16(5000));
assert(z == 5000);
}
function f4() public pure {
// unsigned <- unsigned
uint x = uint(uint8(-1));
assert(x == 255);
x = uint(uint16(-1));
assert(x == 65535);
x = uint(uint16(5000));
assert(x == 5000);
uint16 y = uint16(-1);
assert(y == 65535);
y = uint16(uint8(-1));
assert(y == 255);
address a = address(uint8(0));
assert(a == address(0));
D d = D(uint8(0));
assert(a == address(d));
bytes2 b1 = 0xcafe;
bytes4 b2 = bytes4(b1);
assert(b2 == 0xcafe0000);
bytes16 b3 = bytes16(b1);
assert(b3 == 0xcafe0000000000000000000000000000);
bytes4 b4 = bytes4(uint32(0xcafe));
assert(b4 == 0x0000cafe);
bytes4 b5 = bytes4(uint32(0xcafe0000));
assert(b5 == 0xcafe0000);
}
}
// ----
// Warning 8364: (1144-1145): Assertion checker does not yet implement type type(contract D)