Unexpected failed check for negative left shift operand

[reisnera]

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:

fn main() {}

#[cfg(kani)]
#[kani::proof]
fn proof() {
    let n: i32 = -16;
    let s: u8 = kani::any();
    kani::assume(s == 1);
    let _ = n << s;
}

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"

[celinval]

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):

This results in undefined behavior if rhs is larger than or equal to the number of bits in self, i.e. when checked_shl would return None.

or the intrinsic (https://doc.rust-lang.org/std/intrinsics/fn.unchecked_shl.html):

resulting in undefined behavior when y < 0 or y >= N, where N is the width of T in bits.

Just to double check, the Rust compiler emits a shl instruction without nuw (No Unsigned Wrap), so the UB definition is only for overflow:

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
}

[celinval]

Note: We should probably disable the CBMC flag --undefined-shift-check and implement the intrinsic safety check.

[reisnera]

@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?

[zhassan-aws]

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?

[zhassan-aws]

This is the output with latest Kani version:

$ kani --version
kani 0.32.0
$ kani iss2374.rs 
warning: function `main` is never used
 --> iss2374.rs:1:4
  |
1 | fn main() {}
  |    ^^^^
  |
  = note: `#[warn(dead_code)]` on by default

warning: 1 warning emitted

Checking harness proof...
CBMC 5.88.0 (cbmc-5.88.0)
CBMC version 5.88.0 (cbmc-5.88.0) 64-bit x86_64 linux
Reading GOTO program from file /home/ubuntu/examples/iss2374/iss2374__RNvCsdGhiXr5gtK7_7iss23745proof.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.000965481s
size of program expression: 53 steps
slicing removed 21 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 2.5081e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000101063s
Running propositional reduction
Post-processing
Runtime Post-process: 5.56e-06s
Solving with MiniSAT 2.2.1 with simplifier
20 variables, 34 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 5.7251e-05s
Runtime decision procedure: 0.000201634s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
20 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 1.015e-05s
Runtime decision procedure: 2.0421e-05s

RESULTS:
Check 1: proof.assertion.1
         - Status: SUCCESS
         - Description: "attempt to shift left with overflow"
         - Location: iss2374.rs:9:13 in function proof

SUMMARY:
 ** 0 of 1 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.018046124s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

[zhassan-aws]

Never mind: naming the variable brings back the issue:

$ diff iss2374.rs iss2374_mod.rs 
9c9
<     let _ = n << s;
---
>     let x = n << s;

$ kani iss2374_mod.rs
...
RESULTS:
Check 1: proof.assertion.1
         - Status: SUCCESS
         - Description: "attempt to shift left with overflow"
         - Location: iss2374_mod.rs:9:13 in function proof

Check 2: proof.undefined-shift.1
         - Status: SUCCESS
         - Description: "shift distance too large"
         - Location: iss2374_mod.rs:9:13 in function proof

Check 3: proof.undefined-shift.2
         - Status: FAILURE
         - Description: "shift operand is negative"
         - Location: iss2374_mod.rs:9:13 in function proof

SUMMARY:
 ** 1 of 3 failed
Failed Checks: shift operand is negative
 File: "/home/ubuntu/examples/iss2374/iss2374_mod.rs", line 9, in proof

VERIFICATION:- FAILED
Verification Time: 0.020628411s

[zhassan-aws]

With that said, if you'd like to try implementing this (thanks for offering!), the entry point should be this line of code:

https://github.com/model-checking/kani/blob/a27905f2e275ea7fb929d7567c2c62d7fefd02d7/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs#L349

The overflow checks should be implemented there. You can take a look at how other overflow checks are implemented, e.g.

https://github.com/model-checking/kani/blob/a27905f2e275ea7fb929d7567c2c62d7fefd02d7/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs#L416

[celinval]

@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?

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.

[reisnera]

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:

1. I'm using PropertyClass::ArithmeticOverflow for the excessive shift distance checks, but should the check for negative shift distance use that or PropertyClass::SafetyCheck?
2. Should I be using codegen_assert_assume for all these checks? That's what I did but I also know that codegen_assert is an option.

I feel pretty good about the binop but I'm curious if the way I implemented the simd shift intrinsic checks is correct.

[reisnera]

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!

[celinval]

1. I'm using PropertyClass::ArithmeticOverflow for the excessive shift distance checks, but should the check for negative shift distance use that or PropertyClass::SafetyCheck?

Tbh, both would be correct. ArithmeticOverflow is the most precise, so I would also use that.

2. Should I be using codegen_assert_assume for all these checks? That's what I did but I also know that codegen_assert is an option.

Yes!

I feel pretty good about the binop but I'm curious if the way I implemented the simd shift intrinsic checks is correct.

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.

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!

Yes, the fixme tests only depend on the name of the rust file. :)

[celinval]

@reisnera you might want to check if your changes will also fix: https://github.com/model-checking/kani/issues/1963

Thanks!