MIR enums

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,14 @@ substMethodSpec sc sm ms = do
     goSetupCondition (MS.SetupCond_Ghost loc gg tt) =
         MS.SetupCond_Ghost loc gg <$> goTypedTerm tt
 
+    goSetupEnum (MirSetupEnumVariant adt variant variantIdx svs) =
+      MirSetupEnumVariant adt variant variantIdx <$>
+      mapM goSetupValue svs
+    goSetupEnum (MirSetupEnumSymbolic adt discr variants) =
+      MirSetupEnumSymbolic adt <$>
+      goSetupValue discr <*>
+      mapM (mapM goSetupValue) variants
+
     goSetupSlice (MirSetupSliceRaw ref len) =
       MirSetupSliceRaw <$> goSetupValue ref <*> goSetupValue len
     goSetupSlice (MirSetupSlice arr) =
@@ -742,6 +751,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
@@ -2212,6 +2209,14 @@ internally. The second parameter is the LLVM, Java, or MIR type of the
 variable. The resulting `Term` can be used in various subsequent
 commands.
 
+Note that the second parameter to `{llvm,jvm,mir}_fresh_var` must be a type
+that has a counterpart in Cryptol. (For more information on this, refer to the
+"Cryptol type correspondence" section.) If the type does not have a Cryptol
+counterpart, the function will raise an error. If you do need to create a fresh
+value of a type that cannot be represented in Cryptol, consider using a
+function such as `llvm_fresh_expanded_val` (for LLVM verification) or
+`mir_fresh_expanded_value` (for MIR verification).
+
 LLVM types are built with this set of functions:
 
 * `llvm_int : Int -> LLVMType`
@@ -2306,6 +2311,86 @@ The `llvm_term`, `jvm_term`, and `mir_term` functions create a `SetupValue`,
 * `jvm_term : Term -> JVMValue`
 * `mir_term : Term -> MIRValue`
 
+The value that these functions return will have an LLVM, JVM, or MIR type
+corresponding to the Cryptol type of the `Term` argument. (For more information
+on this, refer to the "Cryptol type correspondence" section.) If the type does
+not have a Cryptol counterpart, the function will raise an error.
+
+### Cryptol type correspondence
+
+The `{llvm,jvm,mir}_fresh_var` functions take an LLVM, JVM, or MIR type as an
+argument and produces a `Term` variable of the corresponding Cryptol type as
+output. Similarly, the `{llvm,jvm,mir}_term` functions take a Cryptol `Term` as
+input and produce a value of the corresponding LLVM, JVM, or MIR type as
+output. This section describes precisely which types can be converted to
+Cryptol types (and vice versa) in this way.
+
+#### LLVM verification
+
+The following LLVM types correspond to Cryptol types:
+
+* `llvm_alias <name>`: Corresponds to the same Cryptol type as the type used
+  in the definition of `<name>`.
+* `llvm_array <n> <ty>`: Corresponds to the Cryptol sequence `[<n>][<cty>]`,
+  where `<cty>` is the Cryptol type corresponding to `<ty>`.
+* `llvm_int <n>`: Corresponds to the Cryptol word `[<n>]`.
+* `llvm_struct [<ty_1>, ..., <ty_n>]` and `llvm_packed_struct [<ty_1>, ..., <ty_n>]`:
+  Corresponds to the Cryptol tuple `(<cty_1>, ..., <cty_n>)`, where `<cty_i>`
+  is the Cryptol type corresponding to `<ty_i>` for each `i` ranging from `1`
+  to `n`.
+
+The following LLVM types do _not_ correspond to Cryptol types:
+
+* `llvm_double`
+* `llvm_float`
+* `llvm_pointer`
+
+#### JVM verification
+
+The following Java types correspond to Cryptol types:
+
+* `java_array <n> <ty>`: Corresponds to the Cryptol sequence `[<n>][<cty>]`,
+  where `<cty>` is the Cryptol type corresponding to `<ty>`.
+* `java_bool`: Corresponds to the Cryptol `Bit` type.
+* `java_byte`: Corresponds to the Cryptol `[8]` type.
+* `java_char`: Corresponds to the Cryptol `[16]` type.
+* `java_int`: Corresponds to the Cryptol `[32]` type.
+* `java_long`: Corresponds to the Cryptol `[64]` type.
+* `java_short`: Corresponds to the Cryptol `[16]` type.
+
+The following Java types do _not_ correspond to Cryptol types:
+
+* `java_class`
+* `java_double`
+* `java_float`
+
+#### MIR verification
+
+The following MIR types correspond to Cryptol types:
+
+* `mir_array <n> <ty>`: Corresponds to the Cryptol sequence `[<n>][<cty>]`,
+  where `<cty>` is the Cryptol type corresponding to `<ty>`.
+* `mir_bool`: Corresponds to the Cryptol `Bit` type.
+* `mir_char`: Corresponds to the Cryptol `[32]` type.
+* `mir_i8` and `mir_u8`: Corresponds to the Cryptol `[8]` type.
+* `mir_i16` and `mir_u16`: Corresponds to the Cryptol `[16]` type.
+* `mir_i32` and `mir_u32`: Corresponds to the Cryptol `[32]` type.
+* `mir_i64` and `mir_u64`: Corresponds to the Cryptol `[64]` type.
+* `mir_i128` and `mir_u128`: Corresponds to the Cryptol `[128]` type.
+* `mir_isize` and `mir_usize`: Corresponds to the Cryptol `[32]` type.
+* `mir_tuple [<ty_1>, ..., <ty_n>]`: Corresponds to the Cryptol tuple
+  `(<cty_1>, ..., <cty_n>)`, where `<cty_i>` is the Cryptol type corresponding
+  to `<ty_i>` for each `i` ranging from `1` to `n`.
+
+The following MIR types do _not_ correspond to Cryptol types:
+
+* `mir_adt`
+* `mir_f32`
+* `mir_f64`
+* `mir_ref` and `mir_ref_mut`
+* `mir_slice`
+* `mir_str`
+
 ## Executing
 
 Once the initial state has been configured, the `{llvm,jvm,mir}_execute_func`
@@ -2926,14 +3011,23 @@ 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 algebraic data types" section (as well as the "Enums"
+  subsection) 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.
 * `mir_struct_value : MIRAdt -> [MIRValue] -> MIRValue` construct a struct
   with the given list of values as elements. The `MIRAdt` argument determines
   what struct type to create.
 
-  See the "Finding MIR alegraic data types" section for more information on how
+  See the "Finding MIR algebraic data types" section for more information on how
   to compute a `MIRAdt` value to pass to `mir_struct_value`.
 * `mir_tuple_value : [MIRValue] -> MIRValue` construct a tuple with the given
   list of values as elements.
@@ -3040,7 +3134,7 @@ SAW's support for slices is currently limited:
 If either of these limitations prevent you from using SAW, please file an issue
 [on GitHub](https://github.com/GaloisInc/saw-script/issues).
 
-### Finding MIR alegraic data types
+### Finding MIR algebraic data types
 
 We collectively refer to MIR `struct`s and `enum`s together as _algebraic data
 types_, or ADTs for short. ADTs have identifiers to tell them apart, and a
@@ -3102,9 +3196,53 @@ 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.
+
+#### Enums
+
+In addition to taking a `MIRAdt` as an argument, `mir_enum_value` 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::Option::None"` or `"core::option::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]);
+};
+~~~~
+
+Note that `mir_enum_value` can only be used to construct a specific variant. If
+you need to construct a symbolic enum value that can range over many potential
+variants, use `mir_fresh_expanded_value` instead.
 
 ### Bitfields
 

intTests/test_mir_fresh_expanded_value_enum/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_fresh_expanded_value_enum/test.linked-mir.json

@@ -0,0 +1 @@
+{"fns":[{"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/b38ac280::f","return_ty":"ty::u32","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":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:13:7: 13:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Copy"}}}],"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":true,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Tuple::e93222e871854c41"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::779a68152b60006a"},"kind":"Constant"},"kind":"Call","pos":"test.rs:13:5: 13:9"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:14:2: 14:2"}},"blockid":"bb1"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":true,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"test/b38ac280::gg","return_ty":"ty::Tuple::e93222e871854c41","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":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:9:7: 9:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Copy"}}}],"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":"Not"},"name":"_2","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::946bbc4c46985e3c"},"kind":"Constant"},"kind":"Call","pos":"test.rs:9:5: 9:9"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:10:2: 10:2"}},"blockid":"bb1"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"test/b38ac280::g","return_ty":"ty::Tuple::e93222e871854c41","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"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/b38ac280::f","kind":"Item","substs":[]},"name":"test/b38ac280::f"},{"inst":{"def_id":"test/b38ac280::gg","kind":"Item","substs":[]},"name":"test/b38ac280::gg"},{"inst":{"def_id":"test/b38ac280::g","kind":"Item","substs":[]},"name":"test/b38ac280::g"}],"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::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::FnDef::779a68152b60006a","ty":{"defid":"test/b38ac280::g","kind":"FnDef"}},{"name":"ty::FnDef::946bbc4c46985e3c","ty":{"defid":"test/b38ac280::f","kind":"FnDef"}}],"roots":["test/b38ac280::f","test/b38ac280::g","test/b38ac280::gg"]}

intTests/test_mir_fresh_expanded_value_enum/test.rs

@@ -0,0 +1,14 @@
+pub fn f(x: Option<u32>) -> u32 {
+    match x {
+        Some(x) => x,
+        None => 27,
+    }
+}
+
+pub fn g(x: Option<u32>) {
+    f(x);
+}
+
+pub fn gg(x: Option<u32>) {
+    g(x);
+}