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

Fixes handling bitwise operators for z3 model checker

Browse Source
This commit is contained in:
Pawel Gebal 2023-02-03 11:29:58 +01:00
parent 411841cbb5
commit a38549dc19
3 changed files with 19 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -8,6 +8,7 @@ Compiler Features:
Bugfixes: Bugfixes:
* TypeChecker: Also allow external library functions in ``using for``. * TypeChecker: Also allow external library functions in ``using for``.
* SMTChecker: Fix internal error caused by unhandled ``z3`` expressions that come from the solver when bitwise operators are used.
### 0.8.18 (2023-02-01) ### 0.8.18 (2023-02-01)

6
libsmtutil/Z3Interface.cpp
View File

@ -344,6 +344,12 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
return arguments[0] % arguments[1]; return arguments[0] % arguments[1];
else if (kind == Z3_OP_XOR) else if (kind == Z3_OP_XOR)
return arguments[0] ^ arguments[1]; return arguments[0] ^ arguments[1];
else if (kind == Z3_OP_BOR)
return arguments[0] | arguments[1];
else if (kind == Z3_OP_BAND)
return arguments[0] & arguments[1];
else if (kind == Z3_OP_BXOR)
return arguments[0] ^ arguments[1];
else if (kind == Z3_OP_BNOT) else if (kind == Z3_OP_BNOT)
return !arguments[0]; return !arguments[0];
else if (kind == Z3_OP_BSHL) else if (kind == Z3_OP_BSHL)

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

@ -0,0 +1,12 @@
contract C {
// tests that bitwise operators are parsed from z3 answer
function test(uint x, uint y) public pure {
x | y;
x & y;
x ^ y;
assert(true);
}
}
// ====
// SMTEngine: all
// ----