Spurious failure for enum with array data

[zhassan-aws]

I tried this code:

#[derive(Clone, PartialEq, Eq)]
enum Foo {
    A,
    B([u8; 65])
}

#[kani::proof]
fn main() {
    let x: Foo = Foo::B(kani::any());
    let b = x.clone();
    assert_eq!(b, x);
}

using the following command line invocation:

kani test.rs

with Kani version:

I expected to see this happen: Verification successful

Instead, this happened: Verification failed:

SUMMARY:
 ** 1 of 52 failed
Failed Checks: assertion failed: b == x
 File: "/home/ubuntu/examples/enum_bug/test.rs", line 11, in main

VERIFICATION:- FAILED

Weird enough, this only happens if the array size is 65 or larger! If I make the array size 64 or less, verification passes!

SUMMARY:
 ** 0 of 52 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.27921867s

[celinval]

I created a similar test with unions and I get the same failure:

union Foo {
    buf: [u8; 65],
}

#[kani::proof]
unsafe fn main() {
    let buf = [0; 65];
    let x: Foo = Foo { buf };
    unsafe { assert_eq!(x.buf, buf) };
}

I could not reproduce the failure with other integer types (not even i8). The error also doesn't happen with an intermediate read:

#[kani::proof]
unsafe fn main() {
    let buf = [0; 65];
    let x: Foo = Foo { buf };
    let buf2 = unsafe { x.buf };
    assert_eq!(buf2, buf);             // --> SUCCESS
    unsafe { assert_eq!(x.buf, buf) }; // --> FAILURE
}

[tautschnig]

I'll review this issue on the CBMC side: running Kani with the additional options -Z unstable-options --cbmc-args --max-field-sensitivity-array-size 128 makes the above examples (both enum and union) pass.

[zhassan-aws]

Simplifying the original test to:

#[derive(PartialEq, Eq)]
enum Foo {
    A,
    B([u8; 65])
}

#[kani::proof]
fn main() {
    let x: Foo = Foo::B([42; 65]);
    let y: Foo = Foo::B([42; 65]);
    assert!(x == y);
}

SUMMARY:
 ** 1 of 52 failed
Failed Checks: assertion failed: x == y
 File: "iss2416.rs", line 11, in main

VERIFICATION:- FAILED`

[zhassan-aws]

Interestingly, I don't get the failure if I unwrap the objects and compare the arrays directly:

#[derive(PartialEq, Eq)]
enum Foo {
    A,
    B([u8; 65])
}

#[kani::proof]
fn main() {
    let x: Foo = Foo::B([42; 65]);
    let y: Foo = Foo::B([42; 65]);
    let Foo::B(x_arr) = x else { unreachable!() };
    let Foo::B(y_arr) = y else { unreachable!() };
    assert!(x_arr == y_arr);
}

SUMMARY:
 ** 0 of 31 failed

VERIFICATION:- SUCCESSFUL

[tautschnig]

Here is a minimal C reproducer (confirming this is a CBMC bug):

union U
{
  unsigned char buf[65];
} s;

int main()
{
  __CPROVER_assert(s.buf[0] == 0, "");
}

[tautschnig]

Bug-fixing PR published at diffblue/cbmc#8579.