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

[SMTChecker] Support address type conversion with literals

Browse Source
This commit is contained in:
Alex Beregszaszi 2020-09-14 20:22:50 +01:00
parent 700cc4c9d3
commit 709d25bd3d
5 changed files with 35 additions and 5 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)
{

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.

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.

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.