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 #9723 from ethereum/smt_fix_rational

Browse Source 
[SMTChecker] Fix rational number short circuit
This commit is contained in:
chriseth 2020-09-01 17:34:56 +02:00 committed by GitHub
commit 3599258d86
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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) void SMTEncoder::endVisit(UnaryOperation const& _op)
{ {
if (TokenTraits::isBitOp(_op.getOperator())) /// We need to shortcut here due to potentially unknown
return bitwiseNotOperation(_op); /// rational number sizes.
if (_op.annotation().type->category() == Type::Category::RationalNumber) if (_op.annotation().type->category() == Type::Category::RationalNumber)
return; return;
if (TokenTraits::isBitOp(_op.getOperator()))
return bitwiseNotOperation(_op);
createExpr(_op); createExpr(_op);
auto const* subExpr = innermostTuple(_op.subExpression()); 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