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:

kani/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Line 349 in a27905f

BinOp::ShlUnchecked => self.codegen_scalar_binop(&BinOp::Shl, e1, e2),

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

kani/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Line 416 in a27905f

fn check_div_overflow(