Enums that are #[repr(u8)] are slower than u8

[jsalzbergedu]

The following code:

#[allow(non_upper_case_globals)]
struct DrSeuss;
impl DrSeuss {
    const Thing1: u8 = 0;
    const Thing2: u8 = 1;
}

#[kani::proof]
fn main() {
    let mut haystack = [DrSeuss::Thing1; 100];
    let needle = DrSeuss::Thing2;
    haystack[kani::any_where(|idx: &usize| *idx < 100)] = needle;
    let mut i = 0;
    let mut count = 0;
    while i < 100 {
        if haystack[i] == needle {
            count += 1;
        }
        assert!(count < 2);
        i += 1;
    }
}

Is faster than the following code:

#[repr(u8)]
#[derive(Copy, Clone, Eq, PartialEq)]
enum DrSeuss {
    Thing1,
    Thing2,
}

#[kani::proof]
fn main() {
    let mut haystack = [DrSeuss::Thing1; 100];
    let needle = DrSeuss::Thing2;
    haystack[kani::any_where(|idx: &usize| *idx < 100)] = needle;
    let mut i = 0;
    let mut count = 0;
    while i < 100 {
        if haystack[i] == needle {
            count += 1;
        }
        assert!(count < 2);
        i += 1;
    }
}

This difference scales, and if you add an extra 0, it is 2 seconds difference on my machine.

It appears that the generated code, which I'm looking at through --gen-c, keeps a "struct" and never uses the u8 layout.

Kani version: 0.54.0

[tautschnig]

The first code snippet appears to have some copy&paste problem, can you please check the first line?

[jsalzbergedu]

@tautschnig fixed