cerc-io/solidity
10
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] Fix rational number short circuit

Browse Source
This commit is contained in:
Leonardo Alt 2020-09-01 11:35:25 +02:00
parent e582731aab
commit 49d3804de4
3 changed files with 32 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libsolidity/formal/SMTEncoder.cpp
View File

@ -452,11 +452,14 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
void SMTEncoder::endVisit(UnaryOperation const& _op)
{
if (TokenTraits::isBitOp(_op.getOperator()))
return bitwiseNotOperation(_op);
/// We need to shortcut here due to potentially unknown
/// rational number sizes.
if (_op.annotation().type->category() == Type::Category::RationalNumber)
return;
if (TokenTraits::isBitOp(_op.getOperator()))
return bitwiseNotOperation(_op);
createExpr(_op);
auto const* subExpr = innermostTuple(_op.subExpression());

12
test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol Normal file
View File

@ -0,0 +1,12 @@
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): Assertion violation happens here

15
test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol Normal file
View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
assert(~1 | (~0xff & 0) == -2);
int x = ~1 | (~0xff ^ 0);
/// Result is negative, assertion fails.
assert(x > 0);
int y = ~x | (0xff & 1);
assert(y > 0);
assert(y & (0xffffffffffffffffff & 1) == 1);
}
}
// ----
// Warning 6328: (181-194): Assertion violation happens here