Skip to content

crux-mir-comp: Support enums #1990

Open
@RyanGlScott

Description

@RyanGlScott

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    subsystem: crucible-mir-compIssues related to compositional Rust verification with crucible-mir-comp or crux-mir-comptech debtIssues that document or involve technical debttype: enhancementIssues describing an improvement to an existing feature or capability

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions