GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
628 stars 42 forks source link

`crucible-mir`: Translation error on `repr(transparent)` enum #1140

Closed RyanGlScott closed 9 months ago

RyanGlScott commented 9 months ago

The following program crashes crux-mir during translation:

#[repr(transparent)]
pub enum E {
    MkE(u32),
}

#[crux::test]
pub fn f() -> E {
    E::MkE(42)
}
test test/1ec90f26::f[0]: [Crux] Attempting to prove verification conditions.
FAILED

failures:

---- test/1ec90f26::f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux]   test.rs:8:5: 8:15: error: in test/1ec90f26::f[0]
[Crux]   Translation error in test/1ec90f26::f[0]: ill-typed assignment of AnyRepr to BVRepr 32 (TyAdt test/1ec90f26::E[0]::_adtb7803c2264daf0ec[0] test/1ec90f26::E[0] (Substs [])) LBase (Var {_varname = "_0", _varmut = Mut, _varty = TyAdt test/1ec90f26::E[0]::_adtb7803c2264daf0ec[0] test/1ec90f26::E[0] (Substs []), _varIsZST = False})

[Crux-MIR] ---- FINAL RESULTS ----
[Crux] Goal status:
[Crux]   Total: 1
[Crux]   Proved: 0
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

Translation suceeds if either (1) the #[repr(transparent)] is removed, or (2) the enum is converted to a struct.