-
Notifications
You must be signed in to change notification settings - Fork 86
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Unexpected failed check for negative left shift operand #2374
Comments
Hi @reisnera, thank you for reporting this issue. I believe you are correct, and that is not a UB in Rust, not even for the unsafe version (https://doc.rust-lang.org/std/primitive.i8.html#method.unchecked_shl):
or the intrinsic (https://doc.rust-lang.org/std/intrinsics/fn.unchecked_shl.html):
Just to double check, the Rust compiler emits a unsafe { n.unchecked_shl(s) } Becomes: start:
%_6 = icmp ult i32 %s, 128
%_8 = trunc i32 %s to i8
tail call void @llvm.assume(i1 %_6)
%0 = shl i8 %n, %_8
ret i8 %0
} |
Note: We should probably disable the |
@celinval I'd love to take a crack at fixing this if someone could point me in the right direction! I can see where the CBMC flag comes into play, but I took a look and wasn't able to figure out where an intrinsic safety check would be implemented. I don't know if someone would be willing to mentor me on this a bit? |
Hi @reisnera. Apparently, this no longer fails starting Kani version 0.28.0 (most likely due to the rust toolchain update). Can you confirm, and if so close the issue? |
This is the output with latest Kani version:
|
Never mind: naming the variable brings back the issue: $ diff iss2374.rs iss2374_mod.rs
9c9
< let _ = n << s;
---
> let x = n << s;
|
With that said, if you'd like to try implementing this (thanks for offering!), the entry point should be this line of code:
The overflow checks should be implemented there. You can take a look at how other overflow checks are implemented, e.g.
|
Sweet! I can help you. As @zhassan-aws mentioned, you can start looking into where we translate BinOps. Btw, this used to show up as an intrinsic, but the compiler changed that. The idea would be to implement all the UB checks for shift first then we should be able to disable cbmc checks. |
So I've been working on this and I think I've accomplished it. I did have to also implement checks for the simd shift intrinsics as well because that broke when I removed the CBMC flag. I'm just updating/adding some tests now but should have a pull request ready in the near future. I do have a couple random questions:
I feel pretty good about the binop but I'm curious if the way I implemented the simd shift intrinsic checks is correct. |
Ok actually another question related to tests: there's a fixme test related to SIMD, however the kani-fixme folder appears to just symlink to the kani subfolder of tests so now I'm confused... Edit: actually nevermind, I think the fixme testing only depends on the filename, but correct me if I'm wrong! |
Tbh, both would be correct. ArithmeticOverflow is the most precise, so I would also use that.
Yes!
It's probably easier to discuss this once you have a PR out. If you are not confident, maybe add a few tests to ensure it behaves as expected.
Yes, the fixme tests only depend on the name of the rust file. :) |
Apologies in advance if this is intended behavior! I couldn't find any previous discussion of this.
I was playing around with Kani and the chrono crate when I encountered "Failed Checks: shift operand is negative". It seems chono's internals use a packed representation for dates that involves left shifting i32 years.
I tried this code in a blank project:
using the following command line invocation:
cargo kani
with Kani version: 0.25.0
I expected to see this happen: My understanding is that left shifting a negative integer is well-defined safe behavior in Rust. I wouldn't expect there to be any failed checks (at least not without an overflow).
Instead, this happened: "Failed Checks: shift operand is negative"
The text was updated successfully, but these errors were encountered: