From a10db051de404f9f049ad3a951c3b5a9de571697 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 20 Dec 2018 13:20:07 +0100 Subject: [PATCH] [SMTChecker] Support basic typecast --- Changelog.md | 1 + libsolidity/formal/SMTChecker.cpp | 45 ++++++++++++++++++- libsolidity/formal/SMTChecker.h | 1 + .../complex/warn_on_typecast.sol | 2 +- .../smtCheckerTests/special/msg_sender_2.sol | 3 +- .../typecast/cast_address_1.sol | 12 +++++ .../typecast/cast_different_size_1.sol | 26 +++++++++++ .../typecast/cast_larger_1.sol | 12 +++++ .../typecast/cast_larger_2.sol | 13 ++++++ .../typecast/cast_larger_2_fail.sol | 13 ++++++ .../typecast/cast_larger_3.sol | 17 +++++++ .../typecast/cast_smaller_1.sol | 12 +++++ .../typecast/cast_smaller_2.sol | 14 ++++++ .../typecast/cast_smaller_3.sol | 14 ++++++ 14 files changed, 181 insertions(+), 4 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/typecast/cast_address_1.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol diff --git a/Changelog.md b/Changelog.md index bb7b191f8..614acacc7 100644 --- a/Changelog.md +++ b/Changelog.md @@ -5,6 +5,7 @@ Language Features: Compiler Features: * Control Flow Graph: Warn about unreachable code. + * SMTChecker: Support basic typecasts without truncation. Bugfixes: diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 35c1e2f10..387152890 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -386,7 +386,7 @@ void SMTChecker::endVisit(BinaryOperation const& _op) void SMTChecker::endVisit(FunctionCall const& _funCall) { solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, ""); - if (_funCall.annotation().kind != FunctionCallKind::FunctionCall) + if (_funCall.annotation().kind == FunctionCallKind::StructConstructorCall) { m_errorReporter.warning( _funCall.location(), @@ -395,6 +395,12 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) return; } + if (_funCall.annotation().kind == FunctionCallKind::TypeConversion) + { + visitTypeConversion(_funCall); + return; + } + FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); std::vector> const args = _funCall.arguments(); @@ -571,6 +577,43 @@ void SMTChecker::endVisit(Identifier const& _identifier) } } +void SMTChecker::visitTypeConversion(FunctionCall const& _funCall) +{ + solAssert(_funCall.annotation().kind == FunctionCallKind::TypeConversion, ""); + solAssert(_funCall.arguments().size() == 1, ""); + auto argument = _funCall.arguments().at(0); + unsigned argSize = argument->annotation().type->storageBytes(); + unsigned castSize = _funCall.annotation().type->storageBytes(); + if (argSize == castSize) + defineExpr(_funCall, expr(*argument)); + else + { + createExpr(_funCall); + setUnknownValue(*m_expressions.at(&_funCall)); + auto const& funCallCategory = _funCall.annotation().type->category(); + // 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(*m_expressions.at(&_funCall)->type()); + defineExpr(_funCall, smt::Expression::ite( + expr(*argument) >= minValue(intType) && expr(*argument) <= maxValue(intType), + expr(*argument), + expr(_funCall) + )); + } + } + + m_errorReporter.warning( + _funCall.location(), + "Type conversion is not yet fully supported and might yield false positives." + ); + } +} + void SMTChecker::visitFunctionIdentifier(Identifier const& _identifier) { auto const& fType = dynamic_cast(*_identifier.annotation().type); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index f14d2ac08..caa837647 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -86,6 +86,7 @@ private: void visitAssert(FunctionCall const& _funCall); void visitRequire(FunctionCall const& _funCall); void visitGasLeft(FunctionCall const& _funCall); + void visitTypeConversion(FunctionCall const& _funCall); /// Visits the FunctionDefinition of the called function /// if available and inlines the return value. void inlineFunctionCall(FunctionCall const& _funCall); diff --git a/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol b/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol index be7854146..8ecfe41e0 100644 --- a/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol +++ b/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol @@ -5,4 +5,4 @@ contract C { } } // ---- -// Warning: (106-114): Assertion checker does not yet implement this expression. +// Warning: (106-114): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol index ad45d0761..f122f4f23 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol @@ -10,5 +10,4 @@ contract C } } // ---- -// Warning: (98-108): Assertion checker does not yet implement this expression. -// Warning: (98-108): Internal error: Expression undefined for SMT solver. +// Warning: (98-108): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_address_1.sol b/test/libsolidity/smtCheckerTests/typecast/cast_address_1.sol new file mode 100644 index 000000000..885118a5b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/cast_address_1.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(address a) public pure { + require(a != address(0)); + assert(a != address(0)); + } +} +// ---- +// Warning: (98-108): Type conversion is not yet fully supported and might yield false positives. +// Warning: (125-135): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol b/test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol new file mode 100644 index 000000000..baacaef15 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + bytes2 a = 0x1234; + 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: (186-195): Type conversion is not yet fully supported and might yield false positives. +// Warning: (280-303): Assertion violation happens here +// Warning: (317-333): Type conversion is not yet fully supported and might yield false positives. +// Warning: (414-431): Assertion violation happens here +// Warning: (451-460): Type conversion is not yet fully supported and might yield false positives. +// Warning: (542-559): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol new file mode 100644 index 000000000..4b0f42e7e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint8 x) public pure { + uint16 y = uint16(x); + // True because of x's type + assert(y < 300); + } +} +// ---- +// Warning: (94-103): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol new file mode 100644 index 000000000..1f981c8c7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + uint16 a = 0x1234; + uint32 b = uint32(a); // b will be 0x00001234 now + // This is correct (left padding). + assert(a == b); + } +} +// ---- +// Warning: (108-117): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol new file mode 100644 index 000000000..7f7073816 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + uint16 a = 0x1234; + uint32 b = uint32(a); // b will be 0x00001234 now + assert(a != b); + } +} +// ---- +// Warning: (108-117): Type conversion is not yet fully supported and might yield false positives. +// Warning: (149-163): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol new file mode 100644 index 000000000..cc51639ed --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + bytes2 a = 0x1234; + bytes4 b = bytes4(a); // b will be 0x12340000 + // False positive since right padding is not supported yet. + assert(b == 0x12340000); + // This should fail (right padding). + assert(a == b); + } +} +// ---- +// Warning: (108-117): Type conversion is not yet fully supported and might yield false positives. +// Warning: (207-230): Assertion violation happens here +// Warning: (273-287): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol new file mode 100644 index 000000000..3e964dfd7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint16 x) public pure { + uint8 y = uint8(x); + // True because of y's type + assert(y < 300); + } +} +// ---- +// Warning: (94-102): Type conversion is not yet fully supported and might yield false positives. diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol new file mode 100644 index 000000000..252701086 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +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: (112-121): Type conversion is not yet fully supported and might yield false positives. +// Warning: (208-227): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol new file mode 100644 index 000000000..1c9ea545a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +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: (108-117): Type conversion is not yet fully supported and might yield false positives. +// Warning: (198-215): Assertion violation happens here