Open
Description
Currently, crux-mir-comp
will simply crash if you write a specification involving enums, as seen in this variant of the spec_struct.rs
test case:
extern crate crucible;
use crucible::*;
use crucible::method_spec::{MethodSpec, MethodSpecBuilder, clobber_globals};
enum S {
MkS(u8, u8)
}
impl Symbolic for S {
fn symbolic(desc: &'static str) -> Self {
S::MkS(u8::symbolic(desc), u8::symbolic(desc))
}
}
fn f(x: S) -> S {
let S::MkS(x0, x1) = x;
S::MkS(x1, x0)
}
#[crux::test]
fn f_test() {
clobber_globals();
let x = <S>::symbolic("x");
let S::MkS(x0, _x1) = x;
crucible_assume!(x0 > 0);
let y = f(x);
let S::MkS(_y0, y1) = y;
crucible_assert!(y1 > 0);
}
fn f_spec() -> MethodSpec {
let x = <S>::symbolic("x");
let S::MkS(x0, _x1) = x;
crucible_assume!(x0 > 0);
let mut msb = MethodSpecBuilder::new(f);
msb.add_arg(&x);
msb.gather_assumes();
let y = <S>::symbolic("result");
let S::MkS(_y0, y1) = y;
crucible_assert!(y1 > 0);
msb.set_return(&y);
msb.gather_asserts();
msb.finish()
}
#[crux::test]
fn use_f() {
f_spec().enable();
let a = u8::symbolic("a");
let b = u8::symbolic("b");
crucible_assume!(0 < a && a < 10);
let S::MkS(c, d) = f(S::MkS(a, b));
crucible_assert!(0 < d);
crucible_assert!(d < 10);
}
$ cabal run exe:crux-mir-comp -- spec_enum.rs
test spec_enum/421e2168::f_test[0]: [Crux] Attempting to prove verification conditions.
ok
tyToShape: AdtKind Enum {_enumDiscrTy = TyInt USize} NYI
CallStack (from HasCallStack):
error, called at src/SAWScript/Crucible/MIR/TypeShape.hs:146:44 in saw-script-1.0.0.99-inplace:SAWScript.Crucible.MIR.TypeShapetest spec_enum/421e2168::use_f[0]:
This ticket exists as a reminder to implement enum support.