Bit-vector basic operators #24
Conversation
| if let TypX::Int(IntRange::U(size)) = &**et { | ||
| return Some(*size); | ||
| } | ||
| if let TypX::Int(IntRange::I(size)) = &**et { |
There was a problem hiding this comment.
We should probably not have this case, since we don't yet have support for signed bitvector.
source/air/src/printer.rs
Outdated
| BinaryOp::BitAdd => "bvadd", | ||
| BinaryOp::BitSub => "bvsub", | ||
| BinaryOp::BitMul => "bvmul", | ||
| BinaryOp::BitDiv => "bvudiv", // unsigned |
There was a problem hiding this comment.
In case we forget, we should to make sure these operations in the original context have unsigned operands.
There was a problem hiding this comment.
I learned that Rust blocks mixed types(signed and unsigned) for %, /, <, >. One strange thing is that Rust allows having mixed types for shifting. In case that both operands are signed integers, % and / are blocked in 'main' branch.
I made commit that forces bitvector reasoning to only have unsigned integers on a separate branch.
8fdd72f
| } | ||
|
|
||
| // return bool type if it is comparision op | ||
| if f_name.eq("bvlt") || f_name.eq("bvgt") || f_name.eq("bvle") || f_name.eq("bvge") { |
There was a problem hiding this comment.
I think it's better to match on BinaryOp here than to use string comparisons.
There was a problem hiding this comment.
Sure, I will make that change.
| assert_bit_vector( (b << 2) >> 2 == b); // FAILS | ||
| } | ||
| } => Err(err) => assert_one_fails(err) | ||
| } |
There was a problem hiding this comment.
It would be good to add a failing test where the assert_bit_vector succeeds but the subsequent assert about integers fails (because it doesn't match the assert_bit_vector).
It might also be good to add a failing test to check that signed integers don't accidentally use the unsigned integer reasoning.
There was a problem hiding this comment.
I agree that those tests are great to have.
About banning signed integers, I will make a few more commits to make sure of that before merging this into main.
|
Made a new pull request ( #32 ) with a few commits addressing Chris and Yi's comment. |
This pull request implements
assert_bit_vector, supporting basic operators such as shift/and/xor/add/less than/etc. Every bit-vector variable/constant/operation are treated as unsigned.asssert_bit_vectormakes a separate z3 query, and the main query assumes its corresponding integer properties. When making the corresponding property, bit operators that are not existing at the integer level (namely <<, >>, &, ^, | ) are translated as uninterpreted functions.Function level bit vector reasoning is not supported yet, although it can be annotated with
#[verifier(bit_vector)]