Enable test for bitreverse intrinsic
#926
Conversation
| let n: usize = kani::any(); | ||
| kani::assume(n < len); | ||
| assert!($get_bit_name(a, n) == $get_bit_name(b, (len - 1) - n)); |
| // Note: Support for `__builtin_bitreverse` in CBMC is being added in | ||
| // https://github.com/diffblue/cbmc/pull/6581 | ||
| // Tracking issue: https://github.com/model-checking/kani/issues/778 |
There was a problem hiding this comment.
I guess this might not belong in this test case if there's nothing to change here, but this work remains to be done, right?
There was a problem hiding this comment.
Not sure what you mean, we are enabling this test because support for __builtin_bitreverse is now available in CBMC. The Kani issue will be resolved by this PR, note that most of the work on Kani's end was added in #779
There was a problem hiding this comment.
we are enabling this test because support for __builtin_bitreverse is now available in CBMC.
Ah, that's what I was missing. ok.
| // `reverse_bits` is also defined for signed integer types by casting the | ||
| // number into the corresponding unsigned type and then casting the result | ||
| // into the original signed type. This causes overflows unless we restrict | ||
| // their values considerably, making the signed versions not very | ||
| // interesting to test here. |
There was a problem hiding this comment.
If bit reverse works on signed types in rust... shouldn't we test that we translate it correctly still?
There was a problem hiding this comment.
Well, the translation is the same. Just to be clear, this is how it is defined: https://github.com/rust-lang/rust/blob/master/library/core/src/num/int_macros.rs#L277-L279
Would you be happy if we add a test like this for each integer type?
assert!((0 as i8).reverse_bits() == 0);There was a problem hiding this comment.
Sure, but a test is meant to defend us against changes in the implementation, and there's certainly room for confusing bugs to show up here when converting between signed/unsigned.
Plus... it's not clear to me we should be issuing overflows on this operation on a signed integer. Those cases failing might actually be indicating unwanted behavior from our translation here.
BUT, this does seem like a huge corner case, people probably just don't reverse bits on signed integers much. I'll approve but maybe we should have an issue open about what reversing on signed integers?
|
I think is was ready, and the test taking a long time is bugging me, so merging! |
Description of changes:
Enables the "fixme" test we prepared for
bitreverseafter some modifications (use nondeterministic index, remove tests for signed integer types).Resolved issues:
Resolves #778
Testing:
How is this change tested? Existing regression + this new test.
Is this a refactor change? No.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.