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 #9858 from ethereum/smt-address

Browse Source 
[SMTChecker] Support address type conversion with literals
This commit is contained in:
Leonardo 2020-09-23 11:24:07 +02:00 committed by GitHub
commit cfff24a2ae
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
20 changed files with 35 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -10,6 +10,7 @@ Compiler Features:
* SMTChecker: Support shifts.
* SMTChecker: Support structs.
* SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``.
* SMTChecker: Support ``address`` type conversion with literals, e.g. ``address(0)``.
* Yul Optimizer: Prune unused parameters in functions.
* Yul Optimizer: Inline into functions further down in the call graph first.
* Yul Optimizer: Try to simplify function names.

11
libsolidity/formal/SMTEncoder.cpp
View File

@ -792,12 +792,19 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
auto argument = _funCall.arguments().front();
unsigned argSize = argument->annotation().type->storageBytes();
unsigned castSize = _funCall.annotation().type->storageBytes();
if (argSize == castSize)
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));
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)
{

3
test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch.sol
View File

@ -15,6 +15,3 @@ contract C
}
}
// ----
// Warning 5084: (208-218): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (123-133): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (208-218): Type conversion is not yet fully supported and might yield false positives.

5
test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_2.sol
View File

@ -20,8 +20,3 @@ contract C
}
}
// ----
// Warning 5084: (271-281): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (123-133): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (271-281): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (186-196): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (271-281): Type conversion is not yet fully supported and might yield false positives.

5
test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_3.sol
View File

@ -20,8 +20,3 @@ contract C
}
}
// ----
// Warning 5084: (275-285): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (123-133): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (275-285): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (189-199): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (275-285): Type conversion is not yet fully supported and might yield false positives.

4
test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_4.sol
View File

@ -25,7 +25,3 @@ contract C
}
// ----
// Warning 5084: (275-285): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (123-133): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (189-199): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (275-285): Type conversion is not yet fully supported and might yield false positives.

3
test/libsolidity/smtCheckerTests/control_flow/function_call_inside_else_branch.sol
View File

@ -16,6 +16,3 @@ contract C
}
}
// ----
// Warning 5084: (219-229): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (134-144): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (219-229): Type conversion is not yet fully supported and might yield false positives.

3
test/libsolidity/smtCheckerTests/control_flow/function_call_inside_modifier_branch.sol
View File

@ -19,6 +19,3 @@ contract C
}
}
// ----
// Warning 5084: (249-259): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (118-128): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (249-259): Type conversion is not yet fully supported and might yield false positives.

3
test/libsolidity/smtCheckerTests/control_flow/function_call_inside_placeholder_inside_modifier_branch.sol
View File

@ -20,6 +20,3 @@ contract C
}
}
// ----
// Warning 5084: (247-257): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (162-172): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (247-257): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol
View File

@ -35,4 +35,3 @@ contract C {
}
// ----
// Warning 6328: (528-565): Assertion violation happens here.
// Warning 5084: (544-554): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol
View File

@ -44,4 +44,3 @@ contract C {
// ----
// Warning 6328: (452-466): Assertion violation happens here.
// Warning 6328: (470-496): Assertion violation happens here.
// Warning 5084: (92-102): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol
View File

@ -36,4 +36,3 @@ contract C {
// ----
// Warning 6328: (381-395): Assertion violation happens here.
// Warning 6328: (399-425): Assertion violation happens here.
// Warning 5084: (116-126): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol
View File

@ -40,4 +40,3 @@ contract C {
// ----
// Warning 6328: (435-461): Assertion violation happens here.
// Warning 6328: (594-631): Assertion violation happens here.
// Warning 5084: (610-620): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/functions/function_external_call_should_not_inline_1.sol
View File

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

1
test/libsolidity/smtCheckerTests/functions/function_external_call_should_not_inline_2.sol
View File

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

2
test/libsolidity/smtCheckerTests/modifiers/modifier_inline_function_inside_branch.sol
View File

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

1
test/libsolidity/smtCheckerTests/special/msg_sender_2.sol
View File

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

25
test/libsolidity/smtCheckerTests/typecast/address_literal.sol Normal file
View File

@ -0,0 +1,25 @@
pragma experimental SMTChecker;
contract C {
address x; // We know that this is "zero initialised".
function f() public view {
address a = address(0);
assert(x == address(0));
assert(x == a);
}
function g() public pure {
address a = address(0);
address b = address(1);
address c = address(0);
address d = a;
address e = address(0x12345678);
assert(c == d);
assert(a == c);
assert(e == address(305419896));
// This is untrue.
assert(a == b);
}
}
// ----
// Warning 6328: (487-501): Assertion violation happens here.

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

@ -8,5 +8,3 @@ contract C
}
}
// ----
// Warning 5084: (98-108): Type conversion is not yet fully supported and might yield false positives.
// Warning 5084: (125-135): Type conversion is not yet fully supported and might yield false positives.

1
test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol
View File

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