Verification fails when comparing arrays and string slices.

[bdalrhm]

I tried this code:

fn main() {
    assert!([1, 2, 3] < [1, 3, 4]);
    assert!("World" >= "Hello");
}

using the following command line invocation:

rmc test.rs

with RMC version: 6962a67

I expected to see this happen: verification succeeds.

Instead, this happened: verification failed with the following assertions failures:

[_RNvYSlNtNtCsgWci0eQkB8o_4core3cmp10PartialOrd2ltCs8ZdcvQGSn7l_4test.overflow.1] line 1018 arithmetic overflow on signed - in *((signed char *)((unsigned char *)&var_3 + 0)) - 2: FAILURE
[_RNvYSlNtNtCsgWci0eQkB8o_4core3cmp10PartialOrd2ltCs8ZdcvQGSn7l_4test.overflow.2] line 1018 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)(*((signed char *)((unsigned char *)&var_3 + 0)) - 2): FAILURE
[_RNvYeNtNtCsgWci0eQkB8o_4core3cmp10PartialOrd2geCs8ZdcvQGSn7l_4test.overflow.2] line 1078 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)(*((signed char *)((unsigned char *)&var_3 + 0)) - 2): FAILURE
[main.assertion.1] line 2 assertion failed: [1, 2, 3] < [1, 3, 4]: FAILURE

[zhassan-aws]

This seems to be caused by the usage of a negative value in the std::cmp::Ordering enum: https://github.com/rust-lang/rust/blob/8d8135f003b35c3e109d013b2bed9ee9496da615/library/core/src/cmp.rs#L342

The same failure can be reproduced by the following program:

enum Foo {
    A = -1,
    B = 1,
}

fn main() {
    let a = Some(Foo::A);
    let b = Some(Foo::B);
    let _ = matches!(a, Some(Foo::A));
    let _ = matches!(b, Some(Foo::B));
}

Check 4: main.overflow.1
         - Status: FAILURE
         - Description: "arithmetic overflow on signed to unsigned type conversion"
         - Location: /home/ubuntu/examples/iss356/foo.rs:10:22 in function main

[tedinski]

This does successfully verify, for the record:

#[kani::proof]
fn main() {
    let x: i8 = unsafe { std::mem::transmute([3].cmp(&[4])) };
    assert!(x == -1);
}

But this does NOT verify:

#[kani::proof]
fn main() {
    let x: i8 = unsafe { std::mem::transmute([3].lt(&[4])) };
    assert!(x == 1);
}

So it seems like cmp is successfully returning -1 (Less) but lt is not returning... 1. Or 0. ???

[tedinski]

A possible thread to pull on, and then I need to stop getting nerd sniped by this problem:

cmp is part of Ord while lt is part of PartialOrd so the problem could have its origin in how we codegen partial_cmp which returns the type Option<Ordering>.

Curiously, this succeeds:

#[kani::proof]
fn main() {
    let x: i8 = unsafe { std::mem::transmute([3].partial_cmp(&[4])) };
    assert!(x == -1);
}

After some experimentation, apparently this is a case where None has representation 2. I wonder if we handle this case of the niche optimization? I didn't know it could do this...

It could be that we're codegen'ing partial_cmp correctly, then botching lt handling None