MIR enums

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.

crucible-mir-comp/src/Mir/Compositional/Builder.hs

@@ -629,6 +629,7 @@ substMethodSpec sc sm ms = do
         MS.SetupStruct b svs -> MS.SetupStruct b <$> mapM goSetupValue svs
         MS.SetupTuple b svs -> MS.SetupTuple b <$> mapM goSetupValue svs
         MS.SetupSlice slice -> MS.SetupSlice <$> goSetupSlice slice
+        MS.SetupEnum enum_ -> MS.SetupEnum <$> goSetupEnum enum_
         MS.SetupArray b svs -> MS.SetupArray b <$> mapM goSetupValue svs
         MS.SetupElem b sv idx -> MS.SetupElem b <$> goSetupValue sv <*> pure idx
         MS.SetupField b sv name -> MS.SetupField b <$> goSetupValue sv <*> pure name
@@ -644,6 +645,11 @@ substMethodSpec sc sm ms = do
     goSetupCondition (MS.SetupCond_Ghost b loc gg tt) =
         MS.SetupCond_Ghost b loc gg <$> goTypedTerm tt
 
+    goSetupEnum (MirSetupEnumVariant adt variantNm svs) =
+      MirSetupEnumVariant adt variantNm <$> mapM goSetupValue svs
+    goSetupEnum sv@(MirSetupEnumSymbolic _) =
+      return sv
+
     goSetupSlice (MirSetupSliceRaw ref len) =
       MirSetupSliceRaw <$> goSetupValue ref <*> goSetupValue len
     goSetupSlice (MirSetupSlice arr) =
@@ -742,6 +748,8 @@ regToSetup bak p eval shp rv = go shp rv
         refSV <- go refShp refRV
         lenSV <- go lenShp lenRV
         pure $ MS.SetupSlice $ MirSetupSliceRaw refSV lenSV
+    go (EnumShape _ _ _ _) _ =
+      error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _ =
         error "Function pointers not currently supported in overrides"
 

crucible-mir-comp/src/Mir/Compositional/Clobber.hs

@@ -62,6 +62,8 @@ clobberSymbolic sym loc nameStr shp rv = go shp rv
         ", but got Any wrapping " ++ show tpr
       where shpTpr = StructRepr $ fmapFC fieldShapeType flds
     go (TransparentShape _ shp) rv = go shp rv
+    go (EnumShape _ _ _ _) _rv =
+      error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _rv =
         error "Function pointers not currently supported in overrides"
     go (RefShape _ _ _ _) _rv = error "clobberSymbolic: RefShape NYI"
@@ -120,6 +122,8 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv
         ref' <- go refShp ref
         len' <- go lenShp len
         pure $ Ctx.Empty Ctx.:> RV ref' Ctx.:> RV len'
+    go (EnumShape _ _ _ _) _rv =
+      error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _rv =
         error "Function pointers not currently supported in overrides"
 

crucible-mir-comp/src/Mir/Compositional/Override.hs

@@ -544,6 +544,8 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
         refRV <- go refShp refSV
         lenRV <- go lenShp lenSV
         pure $ Ctx.Empty Ctx.:> RV refRV Ctx.:> RV lenRV
+    go (EnumShape _ _ _ _) _ =
+      error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _ =
         error "Function pointers not currently supported in overrides"
     go shp sv = error $ "setupToReg: type error: bad SetupValue for " ++ show (shapeType shp) ++

crux-mir-comp/src/Mir/Cryptol.hs

@@ -337,6 +337,8 @@ munge sym shp rv = do
                 AnyValue tpr <$> goFields flds rvs
             | otherwise = error $  "munge: StructShape AnyValue with NYI TypeRepr " ++ show tpr
         go (TransparentShape _ shp) rv = go shp rv
+        go (EnumShape _ _ _ _) _ =
+            error "Enums not currently supported in overrides"
         go (FnPtrShape _ _ _) _ =
             error "Function pointers not currently supported in overrides"
         -- TODO: RefShape

doc/manual/manual.md

@@ -2117,12 +2117,9 @@ mir_verify :
 
 ### Running a MIR-based verification
 
-`mir_verify` requires `enable_experimental` in order to be used.  Moreover,
-some parts of `mir_verify` are not currently implemented, so it is possible
-that using `mir_verify` on some programs will fail. Features that are not yet
-implemented include the following:
-
-* The ability to construct MIR `enum` values in specifications
+(Note: API functions involving MIR verification require `enable_experimental`
+in order to be used. As such, some parts of this API may change before being
+finalized.)
 
 The `String` supplied as an argument to `mir_verify` is expected to be a
 function _identifier_. An identifier is expected adhere to one of the following
@@ -2926,6 +2923,14 @@ construct compound values:
 * `mir_array_value : MIRType -> [MIRValue] -> MIRValue` constructs an array
   of the given type whose elements consist of the given values. Supplying the
   element type is necessary to support length-0 arrays.
+* `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue` constructs an
+  enum using a particular enum variant. The `MIRAdt` arguments determines what
+  enum type to create, the `String` value determines the name of the variant to
+  use, and the `[MIRValue]` list are the values to use as elements in the
+  variant.
+
+  See the "Finding MIR alegraic data types" section for more information on how
+  to compute a `MIRAdt` value to pass to `mir_enum_value`.
 * `mir_slice_value : MIRValue -> MIRValue`: see the "MIR slices" section below.
 * `mir_slice_range_value : MIRValue -> Int -> Int -> MIRValue`: see the
   "MIR slices" section below.
@@ -3102,9 +3107,46 @@ s_8_16  <- mir_find_adt m "example::S" [mir_u8,  mir_u16];
 s_32_64 <- mir_find_adt m "example::S" [mir_u32, mir_u64];
 ~~~~
 
-The `mir_adt` command (for constructing a struct type) and `mir_struct_value`
-(for constructing a struct value) commands in turn take a `MIRAdt` as an
-argument.
+The `mir_adt` command (for constructing a struct type), `mir_struct_value` (for
+constructing a struct value), and `mir_enum_value` (for constructing an enum
+value) commands in turn take a `MIRAdt` as an argument.
+
+In addition to taking a `MIRAdt` as an argument, `mir_enum_variant` also takes
+a `String` representing the name of the variant to construct. The variant name
+should be a short name such as `"None"` or `"Some"`, and not a full identifier
+such as `"core::option::None"` or `"core::option::Some"`. This is because the
+`MIRAdt` already contains the full identifiers for all of an enum's variants,
+so SAW will use this information to look up a variant's identifier from a short
+name. Here is an example of using `mir_enum_value` in practice:
+
+~~~~ .rs
+pub fn n() -> Option<u32> {
+    None
+}
+
+pub fn s(x: u32) -> Option<u32> {
+    Some(x)
+}
+~~~~
+~~~~
+m <- mir_load_module "example.linked-mir.json";
+
+option_u32 <- mir_find_adt m "core::option::Option" [mir_u32];
+
+let n_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_enum_value option_u32 "None" []);
+};
+
+let s_spec = do {
+  x <- mir_fresh_var "x" mir_u32;
+
+  mir_execute_func [mir_term x];
+
+  mir_return (mir_enum_value option_u32 "Some" [mir_term x]);
+};
+~~~~
 
 ### Bitfields
 

intTests/test_mir_verify_enums/Makefile

@@ -0,0 +1,13 @@
+all: test.linked-mir.json
+
+test.linked-mir.json: test.rs
+	saw-rustc $<
+	$(MAKE) remove-unused-build-artifacts
+
+.PHONY: remove-unused-build-artifacts
+remove-unused-build-artifacts:
+	rm -f test libtest.mir libtest.rlib
+
+.PHONY: clean
+clean: remove-unused-build-artifacts
+	rm -f test.linked-mir.json

intTests/test_mir_verify_enums/test.linked-mir.json

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"test.rs:17:5: 17:9"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:17:5: 17:9","variant_index":0}],"terminator":{"kind":"Return","pos":"test.rs:18:2: 18:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"test/f696fd3c::h_none","return_ty":"ty::Adt::3fa7c2d95c7fce06","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"test.rs:30:5: 30:11"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::7746688b48f54a60"}},"pos":"test.rs:30:5: 30:11","variant_index":0}],"terminator":{"kind":"Return","pos":"test.rs:31:2: 31:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::7746688b48f54a60"}]},"name":"test/f696fd3c::i42","return_ty":"ty::Adt::7746688b48f54a60","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"pos":"test.rs:9:8: 9:9","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}},"kind":"Copy"}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"kind":"Move"},"discr_span":"test.rs:9:8: 9:9 !test.rs:9:8: 9:9","kind":"SwitchInt","pos":"test.rs:9:8: 9:9 !test.rs:9:8: 9:9","switch_ty":"ty::bool","targets":["bb2","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Deinit","pos":"test.rs:10:11: 10:15"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:10:11: 10:15","variant_index":0}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::935b79106a1ed847"},"kind":"Constant"},"kind":"Call","pos":"test.rs:10:9: 10:16"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Deinit","pos":"test.rs:12:11: 12:19"},{"kind":"Assign","lhs":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:12:11: 12:19","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"},"kind":"Constant"}}},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:12:11: 12:19","variant_index":1}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::935b79106a1ed847"},"kind":"Constant"},"kind":"Call","pos":"test.rs:12:9: 12:20"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:14:2: 14:2"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"test/f696fd3c::g","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"test.rs:34:5: 34:11"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::7746688b48f54a60"}},"pos":"test.rs:34:5: 34:11","variant_index":1}],"terminator":{"kind":"Return","pos":"test.rs:35:2: 35:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::7746688b48f54a60"}]},"name":"test/f696fd3c::i43","return_ty":"ty::Adt::7746688b48f54a60","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"}},"pos":"test.rs:2:11: 2:12","rhs":{"kind":"Discriminant","ty":"ty::isize","val":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"}},"kind":"Move"},"discr_span":"test.rs:3:9: 3:16","kind":"SwitchInt","pos":"test.rs:2:5: 2:12","switch_ty":"ty::isize","targets":["bb1","bb3","bb2"],"values":["0","1"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:4:17: 4:19","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"27"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Goto","pos":"test.rs:4:17: 4:19","target":"bb4"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Unreachable","pos":"test.rs:2:11: 2:12"}},"blockid":"bb2"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:3:14: 3:15","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:3:20: 3:21","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"kind":"Goto","pos":"test.rs:3:20: 3:21","target":"bb4"}},"blockid":"bb3"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:6:2: 6:2"}},"blockid":"bb4"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}]},"name":"test/f696fd3c::f","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:21:10: 21:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"test.rs:21:5: 21:12"},{"kind":"Assign","lhs":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:21:5: 21:12","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:21:5: 21:12","variant_index":1}],"terminator":{"kind":"Return","pos":"test.rs:22:2: 22:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}]},"name":"test/f696fd3c::h_some","return_ty":"ty::Adt::3fa7c2d95c7fce06","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::isize"}},"pos":"test.rs:25:11: 25:13","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"isize","size":8,"val":"42"},"ty":"ty::isize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:25:11: 25:13"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::isize"}]},"name":"test/f696fd3c::I::I42::{constant#0}","return_ty":"ty::isize","spread_arg":null}],"adts":[{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::u32"],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::u32"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"test/f696fd3c::I::_adtb7803c2264daf0ec[0]","orig_def_id":"test/f696fd3c::I","orig_substs":[],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"kind":"Explicit","name":"test/f696fd3c::I::I42::{constant#0}"},"discr_value":"42","fields":[],"inhabited":true,"name":"test/f696fd3c::I::I42"},{"ctor_kind":{"kind":"Const"},"discr":{"index":1,"kind":"Relative"},"discr_value":"43","fields":[],"inhabited":true,"name":"test/f696fd3c::I::I43"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/f696fd3c::h_none","kind":"Item","substs":[]},"name":"test/f696fd3c::h_none"},{"inst":{"def_id":"test/f696fd3c::i42","kind":"Item","substs":[]},"name":"test/f696fd3c::i42"},{"inst":{"def_id":"test/f696fd3c::g","kind":"Item","substs":[]},"name":"test/f696fd3c::g"},{"inst":{"def_id":"test/f696fd3c::i43","kind":"Item","substs":[]},"name":"test/f696fd3c::i43"},{"inst":{"def_id":"test/f696fd3c::f","kind":"Item","substs":[]},"name":"test/f696fd3c::f"},{"inst":{"def_id":"test/f696fd3c::h_some","kind":"Item","substs":[]},"name":"test/f696fd3c::h_some"},{"inst":{"def_id":"test/f696fd3c::I::I42::{constant#0}","kind":"Item","substs":[]},"name":"test/f696fd3c::I::I42::{constant#0}"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Adt::3fa7c2d95c7fce06","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::u32"]}},{"name":"ty::Adt::7746688b48f54a60","ty":{"kind":"Adt","name":"test/f696fd3c::I::_adtb7803c2264daf0ec[0]","orig_def_id":"test/f696fd3c::I","substs":[]}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::FnDef::935b79106a1ed847","ty":{"defid":"test/f696fd3c::f","kind":"FnDef"}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}}],"roots":["test/f696fd3c::f","test/f696fd3c::g","test/f696fd3c::h_none","test/f696fd3c::h_some","test/f696fd3c::i42","test/f696fd3c::i43"]}

intTests/test_mir_verify_enums/test.rs

@@ -0,0 +1,35 @@
+pub fn f(x: Option<u32>) -> u32 {
+    match x {
+        Some(x) => x,
+        None => 27,
+    }
+}
+
+pub fn g(b: bool) -> u32 {
+    if b {
+        f(None)
+    } else {
+        f(Some(42))
+    }
+}
+
+pub fn h_none() -> Option<u32> {
+    None
+}
+
+pub fn h_some(x: u32) -> Option<u32> {
+    Some(x)
+}
+
+pub enum I {
+    I42 = 42,
+    I43,
+}
+
+pub fn i42() -> I {
+    I::I42
+}
+
+pub fn i43() -> I {
+    I::I43
+}