Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

crux-mir-comp: Support enums #1990

Open
RyanGlScott opened this issue Nov 22, 2023 · 0 comments
Open

crux-mir-comp: Support enums #1990

RyanGlScott opened this issue Nov 22, 2023 · 0 comments
Labels
subsystem: crucible-mir-comp Issues related to compositional Rust verification with crucible-mir-comp or crux-mir-comp tech debt Issues that document or involve technical debt type: enhancement Issues describing an improvement to an existing feature or capability
Milestone

Comments

@RyanGlScott
Copy link
Contributor

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.

@RyanGlScott RyanGlScott added type: enhancement Issues describing an improvement to an existing feature or capability subsystem: crucible-mir-comp Issues related to compositional Rust verification with crucible-mir-comp or crux-mir-comp labels Nov 22, 2023
RyanGlScott added a commit that referenced this issue Nov 27, 2023
This adds basic support for enums in the MIR backend. In particular:

* There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue`
  function that constructs a value representing a specific enum variant, where
  the `String` indicates which variant to use.
* The `mir_fresh_expanded_value` command can now create symbolic enum values.

Implementation-wise, much of the complexity in this patch arises from the fact
that MIR enums are represented with `VariantType`s at the Crucible level, which
are a fair bit more involved than the `StructType`s used to power MIR structs.
Some highlights of the implementation are:

* There is now a new `EnumShape` constructor for `TypeShape`, which is in turn
  defined in terms of a new `VariantShape` data type that characterizes the
  shapes of all the fields in an enum variant.
* There is a `MirSetupEnum` data type (exported by
  `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms
  of enum `MIRValue`s that one can construct. Currently, there is
  `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and
  `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns
  when it creates a fresh enum value).
* TODO RGS: Say something about symbolic enums
* For now, there is no `crux-mir-comp` support for enums. We could conceivable
  add support, but there is not a pressing need to do so right now. I have
  opened #1990 as a reminder to
  do this later.

This checks off one box in #1859.
@RyanGlScott RyanGlScott mentioned this issue Nov 27, 2023
RyanGlScott added a commit that referenced this issue Nov 27, 2023
This adds basic support for enums in the MIR backend. In particular:

* There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue`
  function that constructs a value representing a specific enum variant, where
  the `String` indicates which variant to use.
* The `mir_fresh_expanded_value` command can now create symbolic enum values.

Implementation-wise, much of the complexity in this patch arises from the fact
that MIR enums are represented with `VariantType`s at the Crucible level, which
are a fair bit more involved than the `StructType`s used to power MIR structs.
Some highlights of the implementation are:

* There is now a new `EnumShape` constructor for `TypeShape`, which is in turn
  defined in terms of a new `VariantShape` data type that characterizes the
  shapes of all the fields in an enum variant.
* There is a `MirSetupEnum` data type (exported by
  `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms
  of enum `MIRValue`s that one can construct. Currently, there is
  `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and
  `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns
  when it creates a fresh enum value).
* TODO RGS: Say something about symbolic enums
* For now, there is no `crux-mir-comp` support for enums. We could conceivable
  add support, but there is not a pressing need to do so right now. I have
  opened #1990 as a reminder to
  do this later.

This checks off one box in #1859.
RyanGlScott added a commit that referenced this issue Nov 29, 2023
This adds basic support for enums in the MIR backend. In particular:

* There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue`
  function that constructs a value representing a specific enum variant, where
  the `String` indicates which variant to use.
* The `mir_fresh_expanded_value` command can now create symbolic enum values.

Implementation-wise, much of the complexity in this patch arises from the fact
that MIR enums are represented with `VariantType`s at the Crucible level, which
are a fair bit more involved than the `StructType`s used to power MIR structs.
Some highlights of the implementation are:

* There is now a new `EnumShape` constructor for `TypeShape`, which is in turn
  defined in terms of a new `VariantShape` data type that characterizes the
  shapes of all the fields in an enum variant.
* There is a `MirSetupEnum` data type (exported by
  `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms
  of enum `MIRValue`s that one can construct. Currently, there is
  `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and
  `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns
  when it creates a fresh enum value).
* TODO RGS: Say something about symbolic enums
* For now, there is no `crux-mir-comp` support for enums. We could conceivable
  add support, but there is not a pressing need to do so right now. I have
  opened #1990 as a reminder to
  do this later.

This checks off one box in #1859.
RyanGlScott added a commit that referenced this issue Dec 6, 2023
This adds basic support for enums in the MIR backend. In particular:

* There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue`
  function that constructs a value representing a specific enum variant, where
  the `String` indicates which variant to use.
* The `mir_fresh_expanded_value` command can now create symbolic enum values.

Implementation-wise, much of the complexity in this patch arises from the fact
that MIR enums are represented with `VariantType`s at the Crucible level, which
are a fair bit more involved than the `StructType`s used to power MIR structs.
Some highlights of the implementation are:

* There is now a new `EnumShape` constructor for `TypeShape`, which is in turn
  defined in terms of a new `VariantShape` data type that characterizes the
  shapes of all the fields in an enum variant.
* There is a `MirSetupEnum` data type (exported by
  `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms
  of enum `MIRValue`s that one can construct. Currently, there is
  `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and
  `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns
  when it creates a fresh enum value).
* The implementation of symbolic enum values in particular is somewhat
  complicated. I have written `Note [Symbolic enums]` to go over the general
  approach and highlight some potential pitfalls in implementing them.
* For now, there is no `crux-mir-comp` support for enums. We could conceivable
  add support, but there is not a pressing need to do so right now. I have
  opened #1990 as a reminder to
  do this later.

This checks off one box in #1859.
RyanGlScott added a commit that referenced this issue Dec 15, 2023
This adds basic support for enums in the MIR backend. In particular:

* There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue`
  function that constructs a value representing a specific enum variant, where
  the `String` indicates which variant to use.
* The `mir_fresh_expanded_value` command can now create symbolic enum values.

Implementation-wise, much of the complexity in this patch arises from the fact
that MIR enums are represented with `VariantType`s at the Crucible level, which
are a fair bit more involved than the `StructType`s used to power MIR structs.
Some highlights of the implementation are:

* There is now a new `EnumShape` constructor for `TypeShape`, which is in turn
  defined in terms of a new `VariantShape` data type that characterizes the
  shapes of all the fields in an enum variant.
* There is a `MirSetupEnum` data type (exported by
  `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms
  of enum `MIRValue`s that one can construct. Currently, there is
  `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and
  `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns
  when it creates a fresh enum value).
* The implementation of symbolic enum values in particular is somewhat
  complicated. I have written `Note [Symbolic enums]` to go over the general
  approach and highlight some potential pitfalls in implementing them.
* For now, there is no `crux-mir-comp` support for enums. We could conceivable
  add support, but there is not a pressing need to do so right now. I have
  opened #1990 as a reminder to
  do this later.

This checks off one box in #1859.
@sauclovian-g sauclovian-g added this to the Someday milestone Nov 8, 2024
@sauclovian-g sauclovian-g added the tech debt Issues that document or involve technical debt label Nov 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-mir-comp Issues related to compositional Rust verification with crucible-mir-comp or crux-mir-comp tech debt Issues that document or involve technical debt type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Development

No branches or pull requests

3 participants