diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index b8271368d6..c3009850e7 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/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" diff --git a/crucible-mir-comp/src/Mir/Compositional/Clobber.hs b/crucible-mir-comp/src/Mir/Compositional/Clobber.hs index f9bebc062d..e2288de83c 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Clobber.hs +++ b/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" diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index ea63c2122f..e83d18eea6 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/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) ++ diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 08bf240b29..df09f9b4dc 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/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 diff --git a/doc/manual/manual.md b/doc/manual/manual.md index b6e5beb656..3c7be03800 100644 --- a/doc/manual/manual.md +++ b/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 `: Corresponds to the same Cryptol type as the type used + in the definition of ``. +* `llvm_array `: Corresponds to the Cryptol sequence `[][]`, + where `` is the Cryptol type corresponding to ``. +* `llvm_int `: Corresponds to the Cryptol word `[]`. +* `llvm_struct [, ..., ]` and `llvm_packed_struct [, ..., ]`: + Corresponds to the Cryptol tuple `(, ..., )`, where `` + is the Cryptol type corresponding to `` 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 `: Corresponds to the Cryptol sequence `[][]`, + where `` is the Cryptol type corresponding to ``. +* `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 `: Corresponds to the Cryptol sequence `[][]`, + where `` is the Cryptol type corresponding to ``. +* `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 [, ..., ]`: Corresponds to the Cryptol tuple + `(, ..., )`, where `` is the Cryptol type corresponding + to `` 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,6 +3011,15 @@ 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. @@ -2933,7 +3027,7 @@ construct compound values: 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 { + None +} + +pub fn s(x: u32) -> Option { + 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 diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index 67f1cbdc2d..0a1a4b2830 100644 Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ diff --git a/intTests/test_mir_fresh_expanded_value_enum/Makefile b/intTests/test_mir_fresh_expanded_value_enum/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/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 diff --git a/intTests/test_mir_fresh_expanded_value_enum/test.linked-mir.json b/intTests/test_mir_fresh_expanded_value_enum/test.linked-mir.json new file mode 100644 index 0000000000..7b202fff9e --- /dev/null +++ b/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"]} \ No newline at end of file diff --git a/intTests/test_mir_fresh_expanded_value_enum/test.rs b/intTests/test_mir_fresh_expanded_value_enum/test.rs new file mode 100644 index 0000000000..86f7563545 --- /dev/null +++ b/intTests/test_mir_fresh_expanded_value_enum/test.rs @@ -0,0 +1,14 @@ +pub fn f(x: Option) -> u32 { + match x { + Some(x) => x, + None => 27, + } +} + +pub fn g(x: Option) { + f(x); +} + +pub fn gg(x: Option) { + g(x); +} diff --git a/intTests/test_mir_fresh_expanded_value_enum/test.saw b/intTests/test_mir_fresh_expanded_value_enum/test.saw new file mode 100644 index 0000000000..d3c9712f2c --- /dev/null +++ b/intTests/test_mir_fresh_expanded_value_enum/test.saw @@ -0,0 +1,43 @@ +enable_experimental; + +m <- mir_load_module "test.linked-mir.json"; + +let option_u32_adt = mir_find_adt m "core::option::Option" [mir_u32]; + +let f_none_spec = do { + let x = mir_enum_value option_u32_adt "None" []; + + mir_execute_func [x]; + + mir_return (mir_term {{ 27 : [32] }}); +}; + +let f_some_spec = do { + ret <- mir_fresh_var "ret" mir_u32; + let x = mir_enum_value option_u32_adt "Some" [mir_term ret]; + + mir_execute_func [x]; + + mir_return (mir_term ret); +}; + +let g_spec = do { + x <- mir_fresh_expanded_value "x" (mir_adt option_u32_adt); + + mir_execute_func [x]; +}; + +let gg_spec = do { + xx <- mir_fresh_expanded_value "xx" (mir_adt option_u32_adt); + + mir_execute_func [xx]; +}; + +f_none_ov <- mir_verify m "test::f" [] false f_none_spec z3; +f_some_ov <- mir_verify m "test::f" [] false f_some_spec z3; + +mir_verify m "test::g" [] false g_spec z3; +g_ov <- mir_verify m "test::g" [f_none_ov, f_some_ov] false g_spec z3; + +mir_verify m "test::gg" [] false gg_spec z3; +mir_verify m "test::gg" [g_ov] false gg_spec z3; diff --git a/intTests/test_mir_fresh_expanded_value_enum/test.sh b/intTests/test_mir_fresh_expanded_value_enum/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_fresh_expanded_value_enum/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/intTests/test_mir_verify_enums/Makefile b/intTests/test_mir_verify_enums/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/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 diff --git a/intTests/test_mir_verify_enums/test.linked-mir.json b/intTests/test_mir_verify_enums/test.linked-mir.json new file mode 100644 index 0000000000..0b503737b6 --- /dev/null +++ b/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"]} \ No newline at end of file diff --git a/intTests/test_mir_verify_enums/test.rs b/intTests/test_mir_verify_enums/test.rs new file mode 100644 index 0000000000..e4f25f1e2c --- /dev/null +++ b/intTests/test_mir_verify_enums/test.rs @@ -0,0 +1,35 @@ +pub fn f(x: Option) -> 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 { + None +} + +pub fn h_some(x: u32) -> Option { + Some(x) +} + +pub enum I { + I42 = 42, + I43, +} + +pub fn i42() -> I { + I::I42 +} + +pub fn i43() -> I { + I::I43 +} diff --git a/intTests/test_mir_verify_enums/test.saw b/intTests/test_mir_verify_enums/test.saw new file mode 100644 index 0000000000..aa5b84def5 --- /dev/null +++ b/intTests/test_mir_verify_enums/test.saw @@ -0,0 +1,78 @@ +enable_experimental; + +m <- mir_load_module "test.linked-mir.json"; + +let option_u32_adt = mir_find_adt m "core::option::Option" [mir_u32]; +let i_adt = mir_find_adt m "test::I" []; + +let f_none_spec = do { + let x = mir_enum_value option_u32_adt "None" []; + + mir_execute_func [x]; + + mir_return (mir_term {{ 27 : [32] }}); +}; + +let f_some_spec = do { + let ret = mir_term {{ 42 : [32] }}; + let x = mir_enum_value option_u32_adt "Some" [ret]; + + mir_execute_func [x]; + + mir_return ret; +}; + +let g_spec = do { + b <- mir_fresh_var "b" mir_bool; + + mir_execute_func [mir_term b]; + + mir_return (mir_term {{ if b then 27 else 42 : [32] }}); +}; + +let h_none_spec = do { + mir_execute_func []; + + mir_return (mir_enum_value option_u32_adt "None" []); +}; + +let h_some_spec = do { + x <- mir_fresh_var "x" mir_u32; + + mir_execute_func [mir_term x]; + + mir_return (mir_enum_value option_u32_adt "Some" [mir_term x]); +}; + +let i42_spec = do { + mir_execute_func []; + + mir_return (mir_enum_value i_adt "I42" []); +}; + +let i43_spec = do { + mir_execute_func []; + + mir_return (mir_enum_value i_adt "I43" []); +}; + +// `mir_enum_value` should error if it cannot find a variant name. +let i43_bad_spec = do { + mir_execute_func []; + + mir_return (mir_enum_value i_adt "I44" []); +}; + +f_none_ov <- mir_verify m "test::f" [] false f_none_spec z3; +f_some_ov <- mir_verify m "test::f" [] false f_some_spec z3; + +mir_verify m "test::g" [f_none_ov, f_some_ov] false g_spec z3; + +mir_verify m "test::h_none" [] false h_none_spec z3; +mir_verify m "test::h_some" [] false h_some_spec z3; + +mir_verify m "test::i42" [] false i42_spec z3; +mir_verify m "test::i43" [] false i43_spec z3; +fails ( + mir_verify m "test::i43" [] false i43_bad_spec z3 +); diff --git a/intTests/test_mir_verify_enums/test.sh b/intTests/test_mir_verify_enums/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_verify_enums/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md index 8aafd8075b..c404cbe6d4 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -35,6 +35,7 @@ * Add `"slice"` and `"slice range"` `setup value`s representing slices in MIR verification. Attempting to use these in LLVM or JVM verification will raise an error. +* Add `"enum"` `setup value`s representing enums in MIR verification. * The `SAW/create ghost variable` command and the associated `ghost variable value` value are now supported with JVM and MIR verification. diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index b2434fd8fc..53c757fbf8 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -38,6 +38,7 @@ variable. This function is currently only supported with LLVM and MIR verification, and using this function with JVM verification will raise an error. +* Add an `enum()` function for constructing MIR enum values. * The `create_ghost_variable()` and `ghost_value()` functions are now supported with JVM and MIR verification. diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py index 984d79cc62..93f9827310 100644 --- a/saw-remote-api/python/saw_client/crucible.py +++ b/saw-remote-api/python/saw_client/crucible.py @@ -154,6 +154,22 @@ def to_json(self) -> JSON: 'elements': [fld.to_json() for fld in self.fields], 'MIR ADT server name': self.mir_adt.server_name if self.mir_adt is not None else None} +class EnumVal(SetupVal): + adt : MIRAdt + variant_name : str + fields : List[SetupVal] + + def __init__(self, adt : MIRAdt, variant_name : str, fields : List[SetupVal]) -> None: + self.adt = adt + self.variant_name = variant_name + self.fields = fields + + def to_json(self) -> JSON: + return {'setup value': 'enum', + 'MIR ADT server name': self.adt.server_name, + 'variant name': self.variant_name, + 'elements': [fld.to_json() for fld in self.fields]} + class TupleVal(SetupVal): fields : List[SetupVal] @@ -766,6 +782,19 @@ def elem(base: SetupVal, index: int) -> SetupVal: raise ValueError('elem expected an int, but got {index!r}') return ElemVal(base, index) +def enum(adt : MIRAdt, variant_name : str, *fields : SetupVal) -> SetupVal: + """Returns a MIR enum value (i.e., an ``EnumVal``) whose type corresponds to + the given ``adt``, whose variant corresponds to the given ``variant_name``, + and whose field values correspond to the given ``fields``. + + At present, this is only supported with MIR verification. Using this + function with LLVM or JVM verification will raise an error. + """ + for field in fields: + if not isinstance(field, SetupVal): + raise ValueError('enum expected a SetupVal, but got {field!r}') + return EnumVal(adt, variant_name, list(fields)) + def field(base : SetupVal, field_name : str) -> SetupVal: """Returns the value of struct ``base``'s field ``field_name`` (i.e., a ``FieldVal``). diff --git a/saw-remote-api/python/tests/saw/test-files/mir_enums.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/mir_enums.linked-mir.json new file mode 100644 index 0000000000..d2a9e3e66c --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_enums.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"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":"mir_enums.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":"mir_enums.rs:9:8: 9:9 !mir_enums.rs:9:8: 9:9","kind":"SwitchInt","pos":"mir_enums.rs:9:8: 9:9 !mir_enums.rs:9:8: 9:9","switch_ty":"ty::bool","targets":["bb2","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Deinit","pos":"mir_enums.rs:10:11: 10:15"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"mir_enums.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::be69c9ad94113883"},"kind":"Constant"},"kind":"Call","pos":"mir_enums.rs:10:9: 10:16"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Deinit","pos":"mir_enums.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":"mir_enums.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":"mir_enums.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::be69c9ad94113883"},"kind":"Constant"},"kind":"Call","pos":"mir_enums.rs:12:9: 12:20"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_enums.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":"mir_enums/284a9f79::g","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"mir_enums.rs:34:5: 34:11"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::d1797ca6daa8927f"}},"pos":"mir_enums.rs:34:5: 34:11","variant_index":1}],"terminator":{"kind":"Return","pos":"mir_enums.rs:35:2: 35:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::d1797ca6daa8927f"}]},"name":"mir_enums/284a9f79::i43","return_ty":"ty::Adt::d1797ca6daa8927f","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"mir_enums.rs:17:5: 17:9"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"mir_enums.rs:17:5: 17:9","variant_index":0}],"terminator":{"kind":"Return","pos":"mir_enums.rs:18:2: 18:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"mir_enums/284a9f79::h_none","return_ty":"ty::Adt::3fa7c2d95c7fce06","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"mir_enums.rs:30:5: 30:11"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::d1797ca6daa8927f"}},"pos":"mir_enums.rs:30:5: 30:11","variant_index":0}],"terminator":{"kind":"Return","pos":"mir_enums.rs:31:2: 31:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::d1797ca6daa8927f"}]},"name":"mir_enums/284a9f79::i42","return_ty":"ty::Adt::d1797ca6daa8927f","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":"mir_enums.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":"mir_enums.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":"mir_enums.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":"mir_enums.rs:21:5: 21:12","variant_index":1}],"terminator":{"kind":"Return","pos":"mir_enums.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":"mir_enums/284a9f79::h_some","return_ty":"ty::Adt::3fa7c2d95c7fce06","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":"mir_enums.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":"mir_enums.rs:3:9: 3:16","kind":"SwitchInt","pos":"mir_enums.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":"mir_enums.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":"mir_enums.rs:4:17: 4:19","target":"bb4"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Unreachable","pos":"mir_enums.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":"mir_enums.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":"mir_enums.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":"mir_enums.rs:3:20: 3:21","target":"bb4"}},"blockid":"bb3"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_enums.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":"mir_enums/284a9f79::f","return_ty":"ty::u32","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":"mir_enums.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":"mir_enums.rs:25:11: 25:13"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::isize"}]},"name":"mir_enums/284a9f79::I::I42::{constant#0}","return_ty":"ty::isize","spread_arg":null}],"adts":[{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"mir_enums/284a9f79::I::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_enums/284a9f79::I","orig_substs":[],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"kind":"Explicit","name":"mir_enums/284a9f79::I::I42::{constant#0}"},"discr_value":"42","fields":[],"inhabited":true,"name":"mir_enums/284a9f79::I::I42"},{"ctor_kind":{"kind":"Const"},"discr":{"index":1,"kind":"Relative"},"discr_value":"43","fields":[],"inhabited":true,"name":"mir_enums/284a9f79::I::I43"}]},{"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":"mir_enums/284a9f79::g","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::g"},{"inst":{"def_id":"mir_enums/284a9f79::i43","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::i43"},{"inst":{"def_id":"mir_enums/284a9f79::h_none","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::h_none"},{"inst":{"def_id":"mir_enums/284a9f79::i42","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::i42"},{"inst":{"def_id":"mir_enums/284a9f79::h_some","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::h_some"},{"inst":{"def_id":"mir_enums/284a9f79::f","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::f"},{"inst":{"def_id":"mir_enums/284a9f79::I::I42::{constant#0}","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::I::I42::{constant#0}"}],"tys":[{"name":"ty::bool","ty":{"kind":"Bool"}},{"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::FnDef::be69c9ad94113883","ty":{"defid":"mir_enums/284a9f79::f","kind":"FnDef"}},{"name":"ty::Adt::d1797ca6daa8927f","ty":{"kind":"Adt","name":"mir_enums/284a9f79::I::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_enums/284a9f79::I","substs":[]}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}}],"roots":["mir_enums/284a9f79::f","mir_enums/284a9f79::g","mir_enums/284a9f79::h_none","mir_enums/284a9f79::h_some","mir_enums/284a9f79::i42","mir_enums/284a9f79::i43"]} \ No newline at end of file diff --git a/saw-remote-api/python/tests/saw/test-files/mir_enums.rs b/saw-remote-api/python/tests/saw/test-files/mir_enums.rs new file mode 100644 index 0000000000..e4f25f1e2c --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_enums.rs @@ -0,0 +1,35 @@ +pub fn f(x: Option) -> 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 { + None +} + +pub fn h_some(x: u32) -> Option { + Some(x) +} + +pub enum I { + I42 = 42, + I43, +} + +pub fn i42() -> I { + I::I42 +} + +pub fn i43() -> I { + I::I43 +} diff --git a/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value_enum.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value_enum.linked-mir.json new file mode 100644 index 0000000000..cbd60459f8 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value_enum.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":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"mir_fresh_expanded_value_enum.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::4ca1625b83958a06"},"kind":"Constant"},"kind":"Call","pos":"mir_fresh_expanded_value_enum.rs:13:5: 13:9"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_fresh_expanded_value_enum.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":"mir_fresh_expanded_value_enum/b7d178bc::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":"_2","ty":"ty::isize"}},"pos":"mir_fresh_expanded_value_enum.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":"mir_fresh_expanded_value_enum.rs:3:9: 3:16","kind":"SwitchInt","pos":"mir_fresh_expanded_value_enum.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":"mir_fresh_expanded_value_enum.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":"mir_fresh_expanded_value_enum.rs:4:17: 4:19","target":"bb4"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Unreachable","pos":"mir_fresh_expanded_value_enum.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":"mir_fresh_expanded_value_enum.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":"mir_fresh_expanded_value_enum.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":"mir_fresh_expanded_value_enum.rs:3:20: 3:21","target":"bb4"}},"blockid":"bb3"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_fresh_expanded_value_enum.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":"mir_fresh_expanded_value_enum/b7d178bc::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":"mir_fresh_expanded_value_enum.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::4c1263d320af70d4"},"kind":"Constant"},"kind":"Call","pos":"mir_fresh_expanded_value_enum.rs:9:5: 9:9"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_fresh_expanded_value_enum.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":"mir_fresh_expanded_value_enum/b7d178bc::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":"mir_fresh_expanded_value_enum/b7d178bc::gg","kind":"Item","substs":[]},"name":"mir_fresh_expanded_value_enum/b7d178bc::gg"},{"inst":{"def_id":"mir_fresh_expanded_value_enum/b7d178bc::f","kind":"Item","substs":[]},"name":"mir_fresh_expanded_value_enum/b7d178bc::f"},{"inst":{"def_id":"mir_fresh_expanded_value_enum/b7d178bc::g","kind":"Item","substs":[]},"name":"mir_fresh_expanded_value_enum/b7d178bc::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::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::FnDef::4ca1625b83958a06","ty":{"defid":"mir_fresh_expanded_value_enum/b7d178bc::g","kind":"FnDef"}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}},{"name":"ty::FnDef::4c1263d320af70d4","ty":{"defid":"mir_fresh_expanded_value_enum/b7d178bc::f","kind":"FnDef"}}],"roots":["mir_fresh_expanded_value_enum/b7d178bc::f","mir_fresh_expanded_value_enum/b7d178bc::g","mir_fresh_expanded_value_enum/b7d178bc::gg"]} \ No newline at end of file diff --git a/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value_enum.rs b/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value_enum.rs new file mode 100644 index 0000000000..86f7563545 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value_enum.rs @@ -0,0 +1,14 @@ +pub fn f(x: Option) -> u32 { + match x { + Some(x) => x, + None => 27, + } +} + +pub fn g(x: Option) { + f(x); +} + +pub fn gg(x: Option) { + g(x); +} diff --git a/saw-remote-api/python/tests/saw/test_mir_enums.py b/saw-remote-api/python/tests/saw/test_mir_enums.py new file mode 100644 index 0000000000..490832140c --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_mir_enums.py @@ -0,0 +1,136 @@ +import unittest +from pathlib import Path + +from saw_client import * +from saw_client.crucible import cry_f, enum +from saw_client.mir import Contract, MIRAdt, adt_ty, bool_ty, u32 + + +class FNoneContract(Contract): + adt: MIRAdt + + def __init__(self, adt: MIRAdt): + super().__init__() + self.adt = adt + + def specification(self) -> None: + x = enum(self.adt, 'None') + + self.execute_func(x) + + self.returns_f('27 : [32]') + + +class FSomeContract(Contract): + adt: MIRAdt + + def __init__(self, adt: MIRAdt): + super().__init__() + self.adt = adt + + def specification(self) -> None: + ret = cry_f('42 : [32]') + x = enum(self.adt, 'Some', ret) + + self.execute_func(x) + + self.returns(ret) + + +class GContract(Contract): + def specification(self) -> None: + b = self.fresh_var(bool_ty, 'b') + + self.execute_func(b) + + self.returns_f('if {b} then 27 else 42 : [32]') + + +class HNoneContract(Contract): + adt: MIRAdt + + def __init__(self, adt: MIRAdt): + super().__init__() + self.adt = adt + + def specification(self) -> None: + self.execute_func() + + self.returns(enum(self.adt, 'None')) + + +class HSomeContract(Contract): + adt: MIRAdt + + def __init__(self, adt: MIRAdt): + super().__init__() + self.adt = adt + + def specification(self) -> None: + x = self.fresh_var(u32, 'x') + + self.execute_func(x) + + self.returns(enum(self.adt, 'Some', x)) + + +class I42Contract(Contract): + adt: MIRAdt + + def __init__(self, adt: MIRAdt): + super().__init__() + self.adt = adt + + def specification(self) -> None: + self.execute_func() + + self.returns(enum(self.adt, 'I42')) + + +class I43Contract(Contract): + adt: MIRAdt + + def __init__(self, adt: MIRAdt): + super().__init__() + self.adt = adt + + def specification(self) -> None: + self.execute_func() + + self.returns(enum(self.adt, 'I43')) + + +class MIRStructsTest(unittest.TestCase): + def test_mir_points_to(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults()) + json_name = str(Path('tests', 'saw', 'test-files', 'mir_enums.linked-mir.json')) + mod = mir_load_module(json_name) + + option_adt = mir_find_adt(mod, 'core::option::Option', u32) + i_adt = mir_find_adt(mod, "mir_enums::I") + + f_none_ov = mir_verify(mod, 'mir_enums::f', FNoneContract(option_adt)) + self.assertIs(f_none_ov.is_success(), True) + + f_some_ov = mir_verify(mod, 'mir_enums::f', FSomeContract(option_adt)) + self.assertIs(f_some_ov.is_success(), True) + + g_result = mir_verify(mod, 'mir_enums::g', GContract(), lemmas=[f_none_ov, f_some_ov]) + self.assertIs(g_result.is_success(), True) + + h_none_result = mir_verify(mod, 'mir_enums::h_none', HNoneContract(option_adt)) + self.assertIs(h_none_result.is_success(), True) + + h_some_result = mir_verify(mod, 'mir_enums::h_some', HSomeContract(option_adt)) + self.assertIs(h_some_result.is_success(), True) + + i42_result = mir_verify(mod, 'mir_enums::i42', I42Contract(i_adt)) + self.assertIs(i42_result.is_success(), True) + + i43_result = mir_verify(mod, 'mir_enums::i43', I43Contract(i_adt)) + self.assertIs(i43_result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/python/tests/saw/test_mir_fresh_expanded_value_enum.py b/saw-remote-api/python/tests/saw/test_mir_fresh_expanded_value_enum.py new file mode 100644 index 0000000000..341046ce15 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_mir_fresh_expanded_value_enum.py @@ -0,0 +1,99 @@ +import unittest +from pathlib import Path + +from saw_client import * +from saw_client.crucible import fresh_expanded +from saw_client.mir import Contract, MIRAdt, adt_ty, enum, u32, void + + +class FNoneContract(Contract): + adt: MIRAdt + + def __init__(self, adt: MIRAdt): + super().__init__() + self.adt = adt + + def specification(self) -> None: + x = enum(self.adt, 'None') + + self.execute_func(x) + + self.returns_f('27 : [32]') + + +class FSomeContract(Contract): + adt: MIRAdt + + def __init__(self, adt: MIRAdt): + super().__init__() + self.adt = adt + + def specification(self) -> None: + ret = self.fresh_var(u32, 'ret') + x = enum(self.adt, 'Some', ret) + + self.execute_func(x) + + self.returns(ret) + + +class GContract(Contract): + adt: MIRAdt + + def __init__(self, adt: MIRAdt): + super().__init__() + self.adt = adt + + def specification(self) -> None: + x = fresh_expanded('x', adt_ty(self.adt)) + + self.execute_func(x) + + self.returns(void) + + +class GGContract(Contract): + adt: MIRAdt + + def __init__(self, adt: MIRAdt): + super().__init__() + self.adt = adt + + def specification(self) -> None: + x = fresh_expanded('x', adt_ty(self.adt)) + + self.execute_func(x) + + self.returns(void) + + +class MIRFreshExpandedValueTest(unittest.TestCase): + def test_mir_fresh_expanded_value(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults()) + json_name = str(Path('tests', 'saw', 'test-files', 'mir_fresh_expanded_value_enum.linked-mir.json')) + mod = mir_load_module(json_name) + + option_u32_adt = mir_find_adt(mod, 'core::option::Option', u32) + + f_none_ov = mir_verify(mod, 'mir_fresh_expanded_value_enum::f', FNoneContract(option_u32_adt)) + self.assertIs(f_none_ov.is_success(), True) + + f_some_ov = mir_verify(mod, 'mir_fresh_expanded_value_enum::f', FSomeContract(option_u32_adt)) + self.assertIs(f_some_ov.is_success(), True) + + g_ov_1 = mir_verify(mod, 'mir_fresh_expanded_value_enum::g', GContract(option_u32_adt)) + self.assertIs(g_ov_1.is_success(), True) + + g_ov_2 = mir_verify(mod, 'mir_fresh_expanded_value_enum::g', GContract(option_u32_adt), lemmas=[f_none_ov, f_some_ov]) + self.assertIs(g_ov_2.is_success(), True) + + gg_ov_1 = mir_verify(mod, 'mir_fresh_expanded_value_enum::gg', GGContract(option_u32_adt)) + self.assertIs(gg_ov_1.is_success(), True) + + gg_ov_2 = mir_verify(mod, 'mir_fresh_expanded_value_enum::gg', GGContract(option_u32_adt), lemmas=[g_ov_2]) + self.assertIs(gg_ov_2.is_success(), True) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index d7b2f2942b..76a5600590 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -112,6 +112,7 @@ data CrucibleSetupVal ty e -- ^ The @'Maybe' 'ServerName'@ value represents a possible MIR -- ADT. This should always be 'Just' with MIR verification and -- 'Nothing' with LLVM or JVM verification. + | EnumValue ServerName String [CrucibleSetupVal ty e] | TupleValue [CrucibleSetupVal ty e] | SliceValue (CrucibleSetupVal ty e) | SliceRangeValue (CrucibleSetupVal ty e) Int Int diff --git a/saw-remote-api/src/SAWServer/Data/SetupValue.hs b/saw-remote-api/src/SAWServer/Data/SetupValue.hs index 13ae0bedbd..04cc3f0a25 100644 --- a/saw-remote-api/src/SAWServer/Data/SetupValue.hs +++ b/saw-remote-api/src/SAWServer/Data/SetupValue.hs @@ -14,6 +14,7 @@ data SetupValTag | TagCryptol | TagArrayValue | TagStructValue + | TagEnumValue | TagTupleValue | TagSliceValue | TagSliceRangeValue @@ -34,6 +35,7 @@ instance FromJSON SetupValTag where "Cryptol" -> pure TagCryptol "array" -> pure TagArrayValue "struct" -> pure TagStructValue + "enum" -> pure TagEnumValue "tuple" -> pure TagTupleValue "slice" -> pure TagSliceValue "slice range" -> pure TagSliceRangeValue @@ -57,6 +59,7 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cr TagCryptol -> CryptolExpr <$> o .: "expression" TagArrayValue -> ArrayValue <$> o .:? "element type" <*> o .: "elements" TagStructValue -> StructValue <$> o .:? "MIR ADT server name" <*> o .: "elements" + TagEnumValue -> EnumValue <$> o .: "MIR ADT server name" <*> o .: "variant name" <*> o .: "elements" TagTupleValue -> TupleValue <$> o .: "elements" TagSliceValue -> SliceValue <$> o .: "base" TagSliceRangeValue -> SliceRangeValue <$> o .: "base" <*> o .: "start" <*> o .: "end" diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index 8262e46c81..e3befb64cd 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -190,6 +190,8 @@ compileJVMContract fileReader bic ghostEnv cenv0 c = JVMSetupM $ fail "Array setup values unsupported in JVM API." getSetupVal _ (StructValue _ _) = JVMSetupM $ fail "Struct setup values unsupported in JVM API." + getSetupVal _ (EnumValue _ _ _) = + JVMSetupM $ fail "Enum setup values unsupported in JVM API." getSetupVal _ (TupleValue _) = JVMSetupM $ fail "Tuple setup values unsupported in JVM API." getSetupVal _ (SliceValue _) = diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs index 6b05fe1d65..c091d0f029 100644 --- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs @@ -190,6 +190,8 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c = LLVMCrucibleSetupM $ fail "Tuple setup values unsupported in the LLVM API." getSetupVal _ (SliceValue _) = LLVMCrucibleSetupM $ fail "Slice setup values unsupported in the LLVM API." + getSetupVal _ (EnumValue _ _ _) = + LLVMCrucibleSetupM $ fail "Enum setup values unsupported in the LLVM API." getSetupVal _ (SliceRangeValue _ _ _) = LLVMCrucibleSetupM $ fail "Slice range setup values unsupported in the LLVM API." getSetupVal env (FieldLValue base fld) = diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs index b6cf3555df..35ce5bb6e4 100644 --- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs @@ -19,6 +19,7 @@ import Data.Map (Map) import qualified Data.Map as Map import Mir.Intrinsics (MIR) +import qualified Mir.Mir as Mir import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) @@ -30,6 +31,7 @@ import SAWScript.Crucible.MIR.Builtins mir_alloc_mut, mir_fresh_expanded_value, mir_fresh_var, + mir_enum_value, mir_execute_func, mir_ghost_value, mir_load_module, @@ -194,14 +196,14 @@ compileMIRContract fileReader bic ghostEnv cenv0 sawenv c = return $ MS.SetupArray ty' (elt':eltss') getSetupVal _ (StructValue Nothing _) = MIRSetupM $ fail "MIR struct without a corresponding ADT." - getSetupVal env (StructValue (Just adtServerName) elts) = - -- First, we look up the MIR ADT from its ServerName. If we find it, - -- proceed to handle the struct field types. Otherwise, raise an error. - case getMIRAdtEither sawenv adtServerName of - Left ex -> throw ex - Right adt -> do - elts' <- mapM (getSetupVal env) elts - pure $ MS.SetupStruct adt elts' + getSetupVal env (StructValue (Just adtServerName) elts) = do + adt <- getMirAdt adtServerName + elts' <- mapM (getSetupVal env) elts + pure $ MS.SetupStruct adt elts' + getSetupVal env (EnumValue adtServerName variantName elts) = do + adt <- getMirAdt adtServerName + elts' <- mapM (getSetupVal env) elts + MIRSetupM $ mir_enum_value adt variantName elts' getSetupVal env (TupleValue elems) = do elems' <- mapM (getSetupVal env) elems pure $ MS.SetupTuple () elems' @@ -227,6 +229,10 @@ compileMIRContract fileReader bic ghostEnv cenv0 sawenv c = getSetupVal _ (ElementLValue _ _) = MIRSetupM $ fail "Element l-values unsupported in the MIR API." + getMirAdt :: ServerName -> MIRSetupM Mir.Adt + getMirAdt adtServerName = + either throw pure $ getMIRAdtEither sawenv adtServerName + data MIRLoadModuleParams = MIRLoadModuleParams ServerName FilePath diff --git a/saw-script.cabal b/saw-script.cabal index 2b52c55716..7804376543 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -54,6 +54,7 @@ library , haskeline , heapster-saw , hobbits >= 1.3.1 + , indexed-traversable , galois-dwarf >= 0.2.2 , IfElse , jvm-parser diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index acba975084..6884eaf8d4 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -149,7 +149,8 @@ import SAWScript.Crucible.Common (Sym, sawCoreState) import SAWScript.Crucible.Common.Setup.Value import SAWScript.Crucible.LLVM.Setup.Value (LLVM) import SAWScript.Crucible.JVM.Setup.Value () -import SAWScript.Crucible.MIR.Setup.Value (MirSetupSlice(..)) +import SAWScript.Crucible.MIR.Setup.Value + (MirSetupEnum(..), MirSetupSlice(..)) import SAWScript.Options import SAWScript.Prover.SolverStats import SAWScript.Utils (bullets) @@ -203,6 +204,14 @@ ppSetupValue setupval = case setupval of absurd empty (MIRExt, _defId) -> ppSetupStructDefault vs + SetupEnum x -> + case (ext, x) of + (LLVMExt, empty) -> + absurd empty + (JVMExt, empty) -> + absurd empty + (MIRExt, enum_) -> + ppMirSetupEnum enum_ SetupTuple x vs -> case (ext, x) of (LLVMExt, empty) -> @@ -249,12 +258,18 @@ ppSetupValue setupval = case setupval of | packed = PP.angles (ppSetupStructDefault vs) | otherwise = ppSetupStructDefault vs - ppSetupStructDefault :: [SetupValue ext] -> PP.Doc ann + ppSetupStructDefault :: forall ext'. IsExt ext' => [SetupValue ext'] -> PP.Doc ann ppSetupStructDefault vs = PP.braces (commaList (map ppSetupValue vs)) ppSetupTuple :: [SetupValue MIR] -> PP.Doc ann ppSetupTuple vs = PP.parens (commaList (map ppSetupValue vs)) + ppMirSetupEnum :: MirSetupEnum -> PP.Doc ann + ppMirSetupEnum (MirSetupEnumVariant _defId variantName _varIdx fields) = + PP.pretty variantName PP.<+> ppSetupStructDefault fields + ppMirSetupEnum (MirSetupEnumSymbolic _defId _discr _variants) = + PP.pretty "" + ppMirSetupSlice :: MirSetupSlice -> PP.Doc ann ppMirSetupSlice (MirSetupSliceRaw ref len) = PP.pretty "SliceRaw" <> ppSetupTuple [ref, len] diff --git a/src/SAWScript/Crucible/Common/Setup/Value.hs b/src/SAWScript/Crucible/Common/Setup/Value.hs index b9fa6ebcde..1b1153104e 100644 --- a/src/SAWScript/Crucible/Common/Setup/Value.hs +++ b/src/SAWScript/Crucible/Common/Setup/Value.hs @@ -38,6 +38,7 @@ module SAWScript.Crucible.Common.Setup.Value , XSetupNull , XSetupStruct + , XSetupEnum , XSetupTuple , XSetupSlice , XSetupArray @@ -121,6 +122,7 @@ type family ResolvedState ext :: Type type family XSetupNull ext type family XSetupStruct ext +type family XSetupEnum ext type family XSetupTuple ext type family XSetupSlice ext type family XSetupArray ext @@ -151,6 +153,9 @@ data SetupValue ext where -- | A slice value. At the moment, this is only ever used for MIR -- verification. SetupSlice :: XSetupSlice ext -> SetupValue ext + -- | An enumeration value. At the moment, this is only ever used for MIR + -- verification. + SetupEnum :: XSetupEnum ext -> SetupValue ext -- | A pointer to a global variable SetupGlobal :: XSetupGlobal ext -> String -> SetupValue ext @@ -166,6 +171,7 @@ data SetupValue ext where type SetupValueHas (c :: Type -> Constraint) ext = ( c (XSetupNull ext) , c (XSetupStruct ext) + , c (XSetupEnum ext) , c (XSetupTuple ext) , c (XSetupSlice ext) , c (XSetupArray ext) diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 1bf1777e67..4ab53ab60f 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -552,6 +552,7 @@ matchArg opts sc cc cs prepost md actual@(RVal ref) expectedTy setupval = addAssert p md (Crucible.SimError (cs ^. MS.csLoc) (Crucible.AssertFailureSimError ("null-equality " ++ MS.stateCond prepost) "")) MS.SetupGlobal empty _ -> absurd empty + MS.SetupEnum empty -> absurd empty MS.SetupTuple empty _ -> absurd empty MS.SetupSlice empty -> absurd empty @@ -932,6 +933,7 @@ instantiateSetupValue sc s v = MS.SetupNull () -> return v MS.SetupGlobal empty _ -> absurd empty MS.SetupStruct empty _ -> absurd empty + MS.SetupEnum empty -> absurd empty MS.SetupTuple empty _ -> absurd empty MS.SetupSlice empty -> absurd empty MS.SetupArray empty _ -> absurd empty diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs index 9364b7716c..98f38a0d14 100644 --- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs @@ -140,6 +140,7 @@ typeOfSetupValue _cc env _nameEnv val = return (J.ClassType (J.mkClassName "java/lang/Object")) MS.SetupGlobal empty _ -> absurd empty MS.SetupStruct empty _ -> absurd empty + MS.SetupEnum empty -> absurd empty MS.SetupTuple empty _ -> absurd empty MS.SetupSlice empty -> absurd empty MS.SetupArray empty _ -> absurd empty @@ -173,6 +174,7 @@ resolveSetupVal cc env _tyenv _nameEnv val = return (RVal (W4.maybePartExpr sym Nothing)) MS.SetupGlobal empty _ -> absurd empty MS.SetupStruct empty _ -> absurd empty + MS.SetupEnum empty -> absurd empty MS.SetupTuple empty _ -> absurd empty MS.SetupSlice empty -> absurd empty MS.SetupArray empty _ -> absurd empty diff --git a/src/SAWScript/Crucible/JVM/Setup/Value.hs b/src/SAWScript/Crucible/JVM/Setup/Value.hs index a69e29ec05..9bd3ec97f3 100644 --- a/src/SAWScript/Crucible/JVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/JVM/Setup/Value.hs @@ -78,6 +78,7 @@ import qualified SAWScript.Crucible.Common.Setup.Value as MS type instance MS.XSetupNull CJ.JVM = () type instance MS.XSetupGlobal CJ.JVM = Void type instance MS.XSetupStruct CJ.JVM = Void +type instance MS.XSetupEnum CJ.JVM = Void type instance MS.XSetupTuple CJ.JVM = Void type instance MS.XSetupSlice CJ.JVM = Void type instance MS.XSetupArray CJ.JVM = Void diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 8174385b8a..b31867ca9d 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1009,6 +1009,7 @@ matchPointsTos opts sc cc spec prepost = go False [] case v of SetupVar i -> Set.singleton i SetupStruct _ xs -> foldMap setupVars xs + SetupEnum empty -> absurd empty SetupTuple empty _ -> absurd empty SetupSlice empty -> absurd empty SetupArray _ xs -> foldMap setupVars xs @@ -1169,6 +1170,8 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = (V.toList (Crucible.fiType <$> Crucible.siFields fields)) zs ] + (_, _, SetupEnum empty) -> + absurd empty (_, _, SetupTuple empty _) -> absurd empty (_, _, SetupSlice empty) -> @@ -2280,6 +2283,7 @@ instantiateSetupValue sc s v = SetupNull{} -> return v SetupGlobal{} -> return v SetupGlobalInitializer{} -> return v + SetupEnum empty -> absurd empty SetupTuple empty _ -> absurd empty SetupSlice empty -> absurd empty where diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 84b29b9784..b5fd1bdbf6 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -451,6 +451,8 @@ typeOfSetupValue cc env nameEnv val = let si = Crucible.mkStructInfo dl packed memTys return (Crucible.StructType si) + SetupEnum empty -> + absurd empty SetupTuple empty _ -> absurd empty SetupSlice empty -> @@ -632,6 +634,8 @@ resolveSetupVal cc mem env tyenv nameEnv val = Crucible.Struct v -> v _ -> error "impossible" return $ Crucible.LLVMValStruct (V.zip flds (V.fromList vals)) + SetupEnum empty -> + absurd empty SetupTuple empty _ -> absurd empty SetupSlice empty -> diff --git a/src/SAWScript/Crucible/LLVM/Setup/Value.hs b/src/SAWScript/Crucible/LLVM/Setup/Value.hs index 9f301187f7..2f9133e03f 100644 --- a/src/SAWScript/Crucible/LLVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/LLVM/Setup/Value.hs @@ -120,6 +120,7 @@ data LLVM (arch :: CL.LLVMArch) type instance Setup.XSetupNull (LLVM _) = () -- 'True' if this is an LLVM packed struct, 'False' otherwise. type instance Setup.XSetupStruct (LLVM _) = Bool +type instance Setup.XSetupEnum (LLVM _) = Void type instance Setup.XSetupTuple (LLVM _) = Void type instance Setup.XSetupSlice (LLVM _) = Void type instance Setup.XSetupArray (LLVM _) = () diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index c81a39546d..0030c90481 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -26,6 +26,8 @@ module SAWScript.Crucible.MIR.Builtins , mir_return , mir_unsafe_assume_spec , mir_verify + -- ** MIR enums + , mir_enum_value -- ** MIR slices , mir_slice_value , mir_slice_range_value @@ -56,7 +58,7 @@ module SAWScript.Crucible.MIR.Builtins ) where import Control.Lens -import Control.Monad (foldM, forM, forM_, unless, when) +import Control.Monad (foldM, forM, forM_, unless, when, zipWithM) import qualified Control.Monad.Catch as X import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Reader (runReaderT) @@ -64,8 +66,9 @@ import Control.Monad.State (MonadState(..), StateT(..), execStateT, gets) import Control.Monad.Trans.Class (MonadTrans(..)) import qualified Data.ByteString.Lazy as BSL import Data.Foldable (for_) +import qualified Data.Foldable.WithIndex as FWI import Data.IORef -import qualified Data.List as List (find) +import qualified Data.List.Extra as List (find, unsnoc) import qualified Data.List.NonEmpty as NE import Data.List.NonEmpty (NonEmpty(..)) import qualified Data.Map as Map @@ -75,6 +78,7 @@ import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.Map as MapF import Data.Parameterized.NatRepr (knownNat, natValue) import Data.Parameterized.Some (Some(..)) +import qualified Data.Parameterized.TraversableFC as FC import qualified Data.Parameterized.TraversableFC.WithIndex as FCI import qualified Data.Set as Set import qualified Data.Text as Text @@ -288,13 +292,9 @@ constructExpandedSetupValue cc sc = go case shp of UnitShape _ -> pure $ MS.SetupTuple () [] - PrimShape ty _ -> - case cryptolTypeOfActual ty of - Nothing -> - X.throwM $ MIRFreshExpandedValueUnsupportedType ty - Just cty -> do - fv <- Setup.freshVariable sc pfx cty - pure $ MS.SetupTerm fv + PrimShape ty _ -> do + fv <- freshPrimVariable pfx ty + pure $ MS.SetupTerm fv TupleShape _ _ fldShps -> do flds <- goFlds pfx fldShps pure $ MS.SetupTuple () flds @@ -303,7 +303,7 @@ constructExpandedSetupValue cc sc = go Mir.TyArray _ n -> do elems <- traverse - (\i -> go (pfx <> "." <> Text.pack (show i)) elemShp) + (\i -> go (pfx <> "_" <> Text.pack (show i)) elemShp) [0..n-1] pure $ MS.SetupArray elemTy elems _ -> @@ -329,17 +329,48 @@ constructExpandedSetupValue cc sc = go adt_not_found_panic "StructShape" adtName _ -> non_adt_type_panic "StructShape" ty + EnumShape ty _ variantShps _ discrShp -> + case ty of + Mir.TyAdt adtName _ _ -> + case col ^. Mir.adts . at adtName of + Just adt@(Mir.Adt _ kind _ _ _ _ _) -> + case kind of + Mir.Enum _ -> + MS.SetupEnum <$> goEnum pfx adt discrShp variantShps + Mir.Struct -> + panic "constructExpandedSetupValue" + ["Expected enum, encountered struct"] + Mir.Union -> + panic "constructExpandedSetupValue" + ["Expected enum, encountered union"] + Nothing -> + adt_not_found_panic "EnumShape" adtName + _ -> + non_adt_type_panic "EnumShape" ty TransparentShape ty shp' -> case ty of Mir.TyAdt adtName _ _ -> do case col ^. Mir.adts . at adtName of - Just adt@(Mir.Adt _ kind _ _ _ _ _) -> + Just adt@(Mir.Adt adtNm kind variants _ _ _ _) -> case kind of Mir.Struct -> do val <- go pfx shp' pure $ MS.SetupStruct adt [val] - Mir.Enum{} -> - fail "`repr(transparent)` enums not currently supported" + Mir.Enum{} + -- `repr(transparent)` enum values use MirSetupEnumVariant + -- rather than MirSetupEnumSymbolic. See the Haddocks for + -- MirSetupEnumSymbolic for an explanation. + | [variant] <- variants + -> do val <- go pfx shp' + pure $ MS.SetupEnum + $ MirSetupEnumVariant adt variant 0 [val] + + | otherwise + -> panic "constructExpandedSetupValue" + [ "`repr(transparent)` enum that doesn't have exactly one variant" + , "Enum: " ++ show adtNm + , "Number of variants: " ++ show (length variants) + ] Mir.Union -> panic "constructExpandedSetupValue" [ "Unexpected `repr(transparent)` union:" @@ -356,6 +387,73 @@ constructExpandedSetupValue cc sc = go FnPtrShape ty _ _ -> X.throwM $ MIRFreshExpandedValueUnsupportedType ty + -- Create a fresh symbolic enum value, as described in + -- Note [Symbolic enums] in SAWScript.Crucible.MIR.Setup.Value. + goEnum :: + forall discrShp variantCtx. + Text -> + Mir.Adt -> + TypeShape discrShp -> + Ctx.Assignment VariantShape variantCtx -> + CrucibleSetup MIR MirSetupEnum + goEnum pfx adt@(Mir.Adt _ _ variants _ _ _ _) discrShp variantShps = + mccWithBackend cc $ \bak -> + do -- First, create a symbolic discriminant value. + IsBVShape discrTy discrW <- pure $ testDiscriminantIsBV discrShp + let discrPfx = pfx <> "_discr" + discrVar <- freshPrimVariable discrPfx discrTy + let discrVal = MS.SetupTerm discrVar + + -- Next, add Crucible assumptions that constraint the discriminant + -- to be equal to one of the possible variants' discriminant values. + -- This assumption will be of the form: + -- + -- (discr == 0) \/ (discr == 1) \/ ... + -- + -- It's tempting to simplify this assumption to just + -- `discr < num_variants`, but this will not work in the event that + -- the enum uses explicit discriminants for some variants, e.g., + -- + -- enum E { + -- E0 = 42, + -- E1, + -- } + discrWNat <- liftIO $ scNat sc $ natValue discrW + possibleDiscrTerms <- liftIO $ + traverse (\discr -> do + discrNat <- scNat sc $ fromInteger discr + scBvNat sc discrWNat discrNat) + (map getEnumVariantDiscr variants) + scFalse <- liftIO $ scBool sc False + possibleDiscrPredTerm <- liftIO $ + foldM + (\z possibleDiscrTerm -> do + p <- scBvEq sc discrWNat (ttTerm discrVar) possibleDiscrTerm + scOr sc p z) + scFalse + possibleDiscrTerms + possibleDiscrPred <- liftIO $ resolveSAWPred cc possibleDiscrPredTerm + loc <- SS.toW4Loc "mir_fresh_expanded_value" <$> lift (lift getPosition) + liftIO $ Crucible.addAssumption bak $ + Crucible.GenericAssumption + loc "Symbolic enum discriminant constraints" possibleDiscrPred + + -- Finally, create symbolic fields for each of the possible variants. + let variantAssns :: [Some (Ctx.Assignment FieldShape)] + variantAssns = + FC.toListFC + (\(VariantShape fldShps) -> Some fldShps) + variantShps + variantVals <- + zipWithM + (\variant (Some fldShps) -> + let variantPfx = pfx <> "_" <> getEnumVariantShortName variant in + goFlds variantPfx fldShps) + variants + variantAssns + + pure $ MirSetupEnumSymbolic adt discrVal variantVals + goFlds :: forall ctx. Text -> Ctx.Assignment FieldShape ctx -> @@ -363,12 +461,25 @@ constructExpandedSetupValue cc sc = go goFlds pfx fldShps = sequenceA $ FCI.itoListFC (\idx fldShp -> - let pfx' = pfx <> "." <> Text.pack (show idx) in + let pfx' = pfx <> "_" <> Text.pack (show idx) in case fldShp of ReqField shp' -> go pfx' shp' OptField shp' -> go pfx' shp') fldShps + -- Create a fresh variable of a primitive MIR type (where \"primitive\" + -- is defined by the @cryptolTypeOfActual@ function). + freshPrimVariable :: + Text -> + Mir.Ty -> + CrucibleSetup MIR TypedTerm + freshPrimVariable pfx ty = + case cryptolTypeOfActual ty of + Nothing -> + X.throwM $ MIRFreshExpandedValueUnsupportedType ty + Just cty -> + Setup.freshVariable sc pfx cty + adt_not_found_panic :: String -> Mir.DefId -> a adt_not_found_panic shapeName adtName = panic "constructExpandedSetupValue" @@ -595,6 +706,45 @@ mir_verify rm nm lemmas checkSat setup tactic = ps <- io (MS.mkProvedSpec MS.SpecProved methodSpec stats vcstats lemmaSet diff) returnProof ps +----- +-- MIR enums +----- + +-- | Construct a specific enum variant. This does a light amount of validity +-- checking, which is the only reason that this function is monadic. +mir_enum_value :: + X.MonadThrow m => + Mir.Adt -> + String -> + [MS.SetupValue MIR] -> + m (MS.SetupValue MIR) +mir_enum_value adt variantNm vs = + case adt of + Mir.Adt adtNm (Mir.Enum _) variants _ _ _ _ -> do + (variantIdx, variant) <- + case FWI.ifind (\_ v -> variantDefIdMatches v) variants of + Just iv -> + pure iv + Nothing -> + X.throwM $ MIREnumValueVariantNotFound adtNm variantNm + pure $ MS.SetupEnum $ MirSetupEnumVariant adt variant variantIdx vs + Mir.Adt adtNm Mir.Struct _ _ _ _ _ -> + X.throwM $ MIREnumValueNonEnum adtNm "struct" + Mir.Adt adtNm Mir.Union _ _ _ _ _ -> + X.throwM $ MIREnumValueNonEnum adtNm "union" + where + variantNmText :: Text + variantNmText = Text.pack variantNm + + -- Check if the user-supplied String argument matches the name of the given + -- variant's DefId. For instance, the variant DefId might be named + -- @core::option[0]::Option[0]::Some[0]@, but the user will simply write + -- @Some@, so we must strip off the other parts of the DefId before checking + -- if the two are the same. + variantDefIdMatches :: Mir.Variant -> Bool + variantDefIdMatches variant = + getEnumVariantShortName variant == variantNmText + ----- -- MIR slices ----- @@ -1161,6 +1311,20 @@ findFn rm nm = do Just x -> return x Nothing -> fail $ "Couldn't find MIR function named: " ++ nm +-- | Given a full enum variant identifier (e.g., +-- @core::option[0]::Option[0]::Some[0]@, retrieve the part of the identifier +-- that corresponds to the variant's shorthand name (e.g., @Some@). +getEnumVariantShortName :: Mir.Variant -> Text +getEnumVariantShortName variant + | Just (_, (variantNm, _)) <- List.unsnoc (variant ^. Mir.vname . Mir.didPath) + = variantNm + + | otherwise + = panic "getEnumVariantShortName" + [ "Malformed enum variant identifier" + , show $ variant ^. Mir.vname + ] + getMIRCrucibleContext :: CrucibleSetup MIR MIRCrucibleContext getMIRCrucibleContext = view Setup.csCrucibleContext <$> get @@ -1383,6 +1547,8 @@ data MIRSetupError | MIRArgNumberWrong Int Int -- number expected, number found | MIRReturnUnexpected Mir.Ty -- found | MIRReturnTypeMismatch Mir.Ty Mir.Ty -- expected, found + | MIREnumValueVariantNotFound Mir.DefId String + | MIREnumValueNonEnum Mir.DefId String -- The String is either \"struct\" or \"union\" instance X.Exception MIRSetupError where toException = topLevelExceptionToException @@ -1420,3 +1586,13 @@ instance Show MIRSetupError where , "Expected type: " ++ show (PP.pretty expected) , "Given type: " ++ show (PP.pretty found) ] + MIREnumValueVariantNotFound adtNm variantNm -> + unlines + [ "mir_enum_value: Could not find a variant named `" ++ variantNm ++ "`" + , "in the enum " ++ show adtNm + ] + MIREnumValueNonEnum adtNm what -> + unlines + [ "mir_enum_value: Expected enum, received " ++ what + , show adtNm + ] diff --git a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs index c52292ea43..a05c2d6ebc 100644 --- a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs @@ -48,6 +48,9 @@ module SAWScript.Crucible.MIR.MethodSpecIR -- * @MIRMethodSpec@ , MIRMethodSpec + -- * @MirSetupEnum@ + , MirSetupEnum(..) + -- * @MirSetupSlice@ , MirSetupSlice(..) diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index 666fcec74c..121e7ebaab 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -7,6 +7,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} @@ -67,6 +68,7 @@ import qualified Mir.TransTy as Mir import qualified What4.Expr as W4 import qualified What4.Interface as W4 import qualified What4.LabeledPred as W4 +import qualified What4.Partial as W4 import qualified What4.ProgramLoc as W4 import Verifier.SAW.SharedTerm @@ -892,6 +894,7 @@ instantiateSetupValue sc s v = MS.SetupTerm tt -> MS.SetupTerm <$> doTerm tt MS.SetupArray elemTy vs -> MS.SetupArray elemTy <$> mapM (instantiateSetupValue sc s) vs MS.SetupStruct did vs -> MS.SetupStruct did <$> mapM (instantiateSetupValue sc s) vs + MS.SetupEnum enum_ -> MS.SetupEnum <$> instantiateSetupEnum enum_ MS.SetupTuple x vs -> MS.SetupTuple x <$> mapM (instantiateSetupValue sc s) vs MS.SetupSlice slice -> MS.SetupSlice <$> instantiateSetupSlice slice MS.SetupNull empty -> absurd empty @@ -904,6 +907,14 @@ instantiateSetupValue sc s v = where doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t + instantiateSetupEnum :: MirSetupEnum -> IO MirSetupEnum + instantiateSetupEnum (MirSetupEnumVariant adt variant variantIdx vs) = + MirSetupEnumVariant adt variant variantIdx <$> + mapM (instantiateSetupValue sc s) vs + instantiateSetupEnum (MirSetupEnumSymbolic adt discr variants) = + MirSetupEnumSymbolic adt discr <$> + mapM (mapM (instantiateSetupValue sc s)) variants + instantiateSetupSlice :: MirSetupSlice -> IO MirSetupSlice instantiateSetupSlice (MirSetupSliceRaw ref len) = MirSetupSliceRaw @@ -1023,6 +1034,7 @@ learnSetupCondition opts sc cc spec prepost cond = -- | Match the value of a function argument with a symbolic 'SetupValue'. matchArg :: + forall w. Options {- ^ saw script print out opts -} -> SharedContext {- ^ context for constructing SAW terms -} -> MIRCrucibleContext {- ^ context for interacting with Crucible -} -> @@ -1073,40 +1085,120 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = (MIRVal (StructShape _ _ xsFldShps) (Crucible.AnyValue tpr@(Crucible.StructRepr _) xs), Mir.TyAdt _ _ _, MS.SetupStruct adt zs) - | Ctx.sizeInt (Ctx.size xs) == length zs - , let xsTpr = Crucible.StructRepr (FC.fmapFC fieldShapeType xsFldShps) - , Just Refl <- W4.testEquality tpr xsTpr -> - case adt of - Mir.Adt _ Mir.Struct [v] _ _ _ _ -> - let ys = v ^.. Mir.vfields . each . Mir.fty in - sequence_ - [ case xFldShp of - ReqField shp -> - matchArg opts sc cc cs prepost md (MIRVal shp x) y z - OptField shp -> do - let x' = readMaybeType sym "field" (shapeType shp) x - matchArg opts sc cc cs prepost md (MIRVal shp x') y z - | (Some (Functor.Pair xFldShp (Crucible.RV x)), y, z) <- - zip3 (FC.toListFC Some (Ctx.zipWith Functor.Pair xsFldShps xs)) - ys - zs ] - Mir.Adt _ ak _ _ _ _ _ -> - panic "matchArg" ["AdtKind " ++ show ak ++ " not yet implemented"] + | let xsTpr = Crucible.StructRepr (FC.fmapFC fieldShapeType xsFldShps) + , Just Refl <- W4.testEquality tpr xsTpr -> do + let variants = adt ^. Mir.adtvariants + variant <- + case variants of + [variant] -> + pure variant + _ -> + panic "matchArg" + [ "Encountered struct Adt with " ++ + show (length variants) ++ + " variants:" + , show $ adt ^. Mir.adtname + ] + let ys = variant ^.. Mir.vfields . each . Mir.fty + matchFields sym xsFldShps xs ys zs + + -- In order to match an enum value, we first check to see if the expected + -- value is a specific enum variant or a symbolic enum... + (MIRVal (EnumShape _ _ variantShps _ discrShp) + (Crucible.AnyValue + (Mir.RustEnumRepr discrTpr variantCtx) + (Ctx.Empty + Ctx.:> Crucible.RV actualDiscr + Ctx.:> Crucible.RV variantAssn)), + _, + MS.SetupEnum enum_) + | Just Refl <- W4.testEquality (shapeType discrShp) discrTpr + , Just Refl <- W4.testEquality (FC.fmapFC variantShapeType variantShps) variantCtx -> + case enum_ of + -- ...if the expected value is a specific enum variant, then we must: + -- + -- - Ensure that the discriminant values match + -- - Ensure that the predicate in the variant's VariantBranch holds. + -- This should always succeed if the discriminant values match. + -- - Match the fields of the VariantBranch's payload point-wise. + MirSetupEnumVariant adt variant variantIdxInt zs -> do + Some variantIdx <- pure $ + variantIntIndex (adt ^. Mir.adtname) variantIdxInt (Ctx.size variantAssn) + VariantShape xsFldShps <- pure $ variantShps Ctx.! variantIdx + let Crucible.VB expectedVariant = variantAssn Ctx.! variantIdx + let ys = variant ^.. Mir.vfields . each . Mir.fty + + -- Ensure that the discriminant values match. + IsBVShape _ discrW <- pure $ testDiscriminantIsBV discrShp + let discr = getEnumVariantDiscr variant + expectedDiscr <- liftIO $ + W4.bvLit sym discrW $ BV.mkBV discrW discr + discrEq <- liftIO $ + W4.bvEq sym expectedDiscr actualDiscr + addAssert discrEq md =<< notEq + + case expectedVariant of + W4.PE xsPred xs -> do + -- Ensure that the variant is defined, i.e., that the predicate + -- in the underlying PartialExpr holds. Due to the way that we + -- construct specific enum values, this should always hold if + -- the discriminant values match, but we check it anyway to be + -- on the safe side. + addAssert xsPred md =<< notEq + -- Finally, ensure that the fields match point-wise. + matchFields sym xsFldShps xs ys zs + W4.Unassigned -> + -- If we see `Unassigned`, we immediately know that the variant + -- should not be defined. Because we know in advance that this + -- VariantBranch's predicate *should* hold, the overall match + -- will fail. + fail_ + + -- ...if the expected value is a symbolic enum (see + -- Note [Symbolic enums] in SAWScript.Crucible.MIR.Setup.Value), then + -- we employ a more general version of the `MirSetupEnumVariant` case + -- above: + -- + -- - Ensure that the discriminant values match + -- - For each possible variant, match the fields of the + -- VariantBranch's payload point-wise under the assumption that + -- the VariantBranch's predicate holds. + -- + -- The `MirSetupEnumVariant` case can be seen as a special case of + -- this approach where we already know that one specific + -- VariantBranch's predicate should hold, and the predicates in all + -- other VariantBranches should be false. + MirSetupEnumSymbolic adt expectedDiscr variantFlds -> do + -- Ensure that the discriminant values match. + let discrTp = shapeMirTy discrShp + matchArg opts sc cc cs prepost md (MIRVal discrShp actualDiscr) discrTp expectedDiscr + + sequence_ @_ @_ @() + [ case xPE of + W4.PE xsPred xs -> + -- For each variant, check that the fields of the variant + -- (xs) match point-wise under the assumption that the + -- VariantBranch's predicate (xsPred) holds. + withConditionalPred xsPred $ + matchFields sym xsFldShps xs ys zs + W4.Unassigned -> + -- If we see `Unassigned`, then we immediately know that the + -- variant should not defined. We can skip checking anything + -- in this case, since we know that the fields of the + -- variant cannot match. (Note that we do not fail outright, + -- as it is still possible that other variants might + -- match.) + pure () + | (Some (Functor.Pair (VariantShape xsFldShps) (Crucible.VB xPE)), ys, zs) <- + zip3 + (FC.toListFC Some (Ctx.zipWith Functor.Pair variantShps variantAssn)) + (map (\v -> v ^.. Mir.vfields . each . Mir.fty) (adt ^. Mir.adtvariants)) + variantFlds + ] -- match the fields of a tuple point-wise (MIRVal (TupleShape _ _ xsFldShps) xs, Mir.TyTuple ys, MS.SetupTuple () zs) -> - sequence_ - [ case xFldShp of - ReqField shp -> - matchArg opts sc cc cs prepost md (MIRVal shp x) y z - OptField shp -> do - let x' = readMaybeType sym "field" (shapeType shp) x - matchArg opts sc cc cs prepost md (MIRVal shp x') y z - | (Some (Functor.Pair xFldShp (Crucible.RV x)), y, z) <- - zip3 (FC.toListFC Some (Ctx.zipWith Functor.Pair xsFldShps xs)) - ys - zs - ] + matchFields sym xsFldShps xs ys zs -- Match the parts of a slice point-wise (MIRVal (SliceShape _ actualElemTy actualMutbl actualElemTpr) @@ -1182,8 +1274,36 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = nameEnv = MS.csTypeNames cs loc = MS.conditionLoc md + + fail_ :: OverrideMatcher MIR w a fail_ = failure loc =<< mkStructuralMismatch opts cc sc cs actual expected expectedTy + + -- Match the fields (point-wise) in a tuple, a struct, or enum variant. + matchFields :: + Sym -> + Ctx.Assignment FieldShape ctx -> + Ctx.Assignment (Crucible.RegValue' Sym) ctx -> + [Mir.Ty] -> + [SetupValue] -> + OverrideMatcher MIR w () + matchFields sym xsFldShps xs ys zs = do + -- As a sanity check, first ensure that the number of fields matches + -- what is expected. + unless (Ctx.sizeInt (Ctx.size xs) == length zs) fail_ + -- Then match the fields point-wise. + sequence_ + [ case xFldShp of + ReqField shp -> + matchArg opts sc cc cs prepost md (MIRVal shp x) y z + OptField shp -> do + let x' = readMaybeType sym "field" (shapeType shp) x + matchArg opts sc cc cs prepost md (MIRVal shp x') y z + | (Some (Functor.Pair xFldShp (Crucible.RV x)), y, z) <- + zip3 (FC.toListFC Some (Ctx.zipWith Functor.Pair xsFldShps xs)) + ys + zs ] + notEq = notEqual prepost opts loc cc sc cs expected actual -- | For each points-to statement read the memory value through the @@ -1240,6 +1360,7 @@ matchPointsTos opts sc cc spec prepost = go False [] case v of MS.SetupVar i -> Set.singleton i MS.SetupStruct _ xs -> foldMap setupVars xs + MS.SetupEnum enum_ -> setupEnum enum_ MS.SetupTuple _ xs -> foldMap setupVars xs MS.SetupSlice slice -> setupSlice slice MS.SetupArray _ xs -> foldMap setupVars xs @@ -1252,6 +1373,13 @@ matchPointsTos opts sc cc spec prepost = go False [] MS.SetupUnion empty _ _ -> absurd empty MS.SetupNull empty -> absurd empty + -- Compute the set of variable identifiers in a 'MirSetupEnum' + setupEnum :: MirSetupEnum -> Set AllocIndex + setupEnum (MirSetupEnumVariant _ _ _ xs) = + foldMap setupVars xs + setupEnum (MirSetupEnumSymbolic _ _ variants) = + foldMap (foldMap setupVars) variants + -- Compute the set of variable identifiers in a 'MirSetupSlice' setupSlice :: MirSetupSlice -> Set AllocIndex setupSlice (MirSetupSliceRaw ref len) = diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index 4727199da3..57ce46397d 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs @@ -29,10 +29,16 @@ module SAWScript.Crucible.MIR.ResolveSetupValue , mirAdtToTy , findDefId , findDefIdEither + -- * Static items , findStatic , findStaticInitializer , findStaticVar , staticRefMux + -- * Enum discriminants + , getEnumVariantDiscr + , testDiscriminantIsBV + , variantIntIndex + -- * Types of errors , MIRTypeOfError(..) ) where @@ -45,6 +51,7 @@ import qualified Data.BitVector.Sized as BV import qualified Data.Foldable as F import qualified Data.Functor.Product as Functor import Data.Kind (Type) +import qualified Data.List.Extra as List (firstJust) import Data.List.NonEmpty (NonEmpty(..)) import Data.Map (Map) import qualified Data.Map as Map @@ -67,8 +74,10 @@ import qualified Cryptol.TypeCheck.AST as Cryptol (Type, Schema(..)) import qualified Cryptol.Utils.PP as Cryptol (pp) import Lang.Crucible.Backend (IsSymInterface) import Lang.Crucible.Simulator - ( AnyValue(..), GlobalVar(..), RegValue, RegValue'(..), SymGlobalState ) -import Lang.Crucible.Types (MaybeType, TypeRepr(..)) + ( AnyValue(..), GlobalVar(..), RegValue, RegValue'(..), SymGlobalState + , VariantBranch(..), injectVariant + ) +import Lang.Crucible.Types (AnyType, MaybeType, TypeRepr(..)) import qualified Mir.DefId as Mir import qualified Mir.FancyMuxTree as Mir import qualified Mir.Generator as Mir @@ -115,7 +124,7 @@ ppMIRVal sym (MIRVal shp val) = PrimShape _ _ -> W4.printSymExpr val TupleShape _ _ fldShp -> - PP.parens $ prettyStructOrTuple fldShp val + PP.parens $ prettyAdtOrTuple fldShp val ArrayShape _ _ shp' -> case val of Mir.MirVector_Vector vec -> @@ -130,10 +139,22 @@ ppMIRVal sym (MIRVal shp val) = StructShape _ _ fldShp | AnyValue (StructRepr fldTpr) fldVals <- val , Just Refl <- W4.testEquality (FC.fmapFC fieldShapeType fldShp) fldTpr - -> PP.braces $ prettyStructOrTuple fldShp fldVals + -> PP.braces $ prettyAdtOrTuple fldShp fldVals | otherwise -> error "Malformed MIRVal struct" + EnumShape _ _ variantShps _ _ + | AnyValue (Mir.RustEnumRepr _ variantCtx) + (Ctx.Empty Ctx.:> RV _ Ctx.:> RV variants) <- val + , Just Refl <- W4.testEquality (FC.fmapFC variantShapeType variantShps) variantCtx + -> case firstConcreteVariant variantShps variants of + Just (Some (Functor.Pair fldShps fldVals)) -> + PP.braces $ prettyAdtOrTuple fldShps fldVals + Nothing -> + "" + + | otherwise + -> error "Malformed MIRVal enum" TransparentShape _ shp' -> ppMIRVal sym $ MIRVal shp' val RefShape _ _ _ _ -> @@ -147,12 +168,35 @@ ppMIRVal sym (MIRVal shp val) = commaList [] = PP.emptyDoc commaList (x:xs) = x PP.<> PP.hcat (map (\y -> PP.comma PP.<+> y) xs) - prettyStructOrTuple :: + -- Return Just the first VariantBranch whose predicate is concretely equal + -- to True. If none of the VariantBranches satisfy this property, then + -- return Nothing. + firstConcreteVariant :: + Ctx.Assignment VariantShape ctx -> + Ctx.Assignment (VariantBranch Sym) ctx -> + Maybe (Some (Functor.Product + (Ctx.Assignment FieldShape) + (Ctx.Assignment (RegValue' Sym)))) + firstConcreteVariant variantShapes variantBranches = + List.firstJust + (\(Some (Functor.Pair (VariantShape fldShps) (VB branch))) -> + case branch of + W4.PE fldPred fldVals + | W4.asConstantPred fldPred == Just True + -> Just $ Some $ Functor.Pair fldShps fldVals + | otherwise + -> Nothing + W4.Unassigned -> + Nothing) $ + FC.toListFC Some $ + Ctx.zipWith Functor.Pair variantShapes variantBranches + + prettyAdtOrTuple :: forall ctx. Ctx.Assignment FieldShape ctx -> Ctx.Assignment (RegValue' Sym) ctx -> PP.Doc ann - prettyStructOrTuple fldShp fldVals = + prettyAdtOrTuple fldShp fldVals = commaList $ map (\(Some (Functor.Pair shp' (RV v))) -> prettyField shp' v) $ FC.toListFC Some $ @@ -245,6 +289,12 @@ typeOfSetupValue mcc env nameEnv val = pure $ Mir.TyArray elemTy (length vs) MS.SetupStruct adt _ -> pure $ mirAdtToTy adt + MS.SetupEnum enum_ -> + case enum_ of + MirSetupEnumVariant adt _ _ _ -> + pure $ mirAdtToTy adt + MirSetupEnumSymbolic adt _ _ -> + pure $ mirAdtToTy adt MS.SetupTuple () vals -> do tys <- traverse (typeOfSetupValue mcc env nameEnv) vals pure $ Mir.TyTuple tys @@ -312,48 +362,206 @@ resolveSetupVal mcc env tyenv nameEnv val = MS.SetupStruct adt flds -> case adt of _ | adt ^. Mir.adtReprTransparent, - [fld] <- flds -> do - MIRVal shp fld' <- resolveSetupVal mcc env tyenv nameEnv fld - pure $ MIRVal (TransparentShape (mirAdtToTy adt) shp) fld' - Mir.Adt nm Mir.Struct [variant] _ _ _ _ -> do + [fld] <- flds -> + resolveTransparentSetupVal adt fld + Mir.Adt nm Mir.Struct variants _ _ _ _ -> do + -- First, retrieve the struct variant. + variant <- + case variants of + [variant] -> + pure variant + _ -> + panic "resolveSetupVal" + [ "Encountered struct Adt with " ++ + show (length variants) ++ + " variants:" + , show nm + ] + + -- Next, resolve the field values and check that they have the + -- expected types. flds' <- traverse (resolveSetupVal mcc env tyenv nameEnv) flds let expectedFlds = variant ^. Mir.vfields - let expectedFldsNum = length expectedFlds let actualFldTys = map (\(MIRVal shp _) -> shapeMirTy shp) flds' - let actualFldsNum = length actualFldTys - unless (expectedFldsNum == actualFldsNum) $ - fail $ unlines - [ "Mismatch in number of struct fields" - , "Struct name: " ++ show nm - , "Expected number of fields: " ++ show expectedFldsNum - , "Actual number of fields: " ++ show actualFldsNum - ] - zipWithM_ - (\expectedFld actualFldTy -> - let expectedFldTy = expectedFld ^. Mir.fty in - let expectedFldName = expectedFld ^. Mir.fName in - unless (checkCompatibleTys expectedFldTy actualFldTy) $ - fail $ unlines - [ "Struct field type mismatch" - , "Field name: " ++ show expectedFldName - , "Expected type: " ++ show (PP.pretty expectedFldTy) - , "Given type: " ++ show (PP.pretty actualFldTy) - ]) - expectedFlds - actualFldTys - Some fldAssn <- - pure $ Ctx.fromList $ - map (\(MIRVal shp v) -> - if Mir.canInitialize col (shapeMirTy shp) - then Some $ Functor.Pair (ReqField shp) (RV v) - else Some $ Functor.Pair (OptField shp) (RV (W4.justPartExpr sym v))) - flds' - let (fldShpAssn, valAssn) = Ctx.unzip fldAssn + checkFields nm "Struct" "struct fields" expectedFlds actualFldTys + + -- Finally, construct a MIRVal of the appropriate shape. + Some (Functor.Pair fldShpAssn valAssn) <- + pure $ variantFieldsToAssns sym flds' let structShp = StructShape (mirAdtToTy adt) actualFldTys fldShpAssn let structTpr = StructRepr (FC.fmapFC fieldShapeType fldShpAssn) pure $ MIRVal structShp (AnyValue structTpr valAssn) - Mir.Adt _ ak _ _ _ _ _ -> - panic "resolveSetupVal" ["AdtKind " ++ show ak ++ " not yet implemented"] + Mir.Adt nm (Mir.Enum _) _ _ _ _ _ -> + panic "resolveSetupVal" + [ "Expected struct type, received enum:" + , show nm + ] + Mir.Adt nm Mir.Union _ _ _ _ _ -> + panic "resolveSetupVal" + [ "Expected struct type, received union:" + , show nm + ] + MS.SetupEnum enum_ -> + case enum_ of + MirSetupEnumVariant adt variant variantIdxInt flds -> + case adt of + _ | adt ^. Mir.adtReprTransparent, + [fld] <- flds -> do + resolveTransparentSetupVal adt fld + Mir.Adt nm (Mir.Enum discrTp) variants _ _ _ _ -> do + -- Resolve the field values and check that they have the expected + -- types. + flds' <- traverse (resolveSetupVal mcc env tyenv nameEnv) flds + let expectedFlds = variant ^. Mir.vfields + let actualFldTys = map (\(MIRVal shp _) -> shapeMirTy shp) flds' + checkFields + nm + "Enum" + ("fields in enum variant " ++ show (variant ^. Mir.vname)) + expectedFlds + actualFldTys + + -- Ensure that the discriminant has an integral type and build + -- a symbolic bitvector from it. + Some discrTpr <- pure $ Mir.tyToRepr col discrTp + let discrShp = tyToShapeEq col discrTp discrTpr + IsBVShape _ discrW <- pure $ testDiscriminantIsBV discrShp + let discr = getEnumVariantDiscr variant + discrVal <- W4.bvLit sym discrW $ BV.mkBV discrW discr + + -- Construct an EnumShape and RustEnumRepr. This requires + -- processing /all/ variants, not just the particular variant that + -- we are building. + (enumShp, Some expectedVariantShps) <- pure $ + enumShapes adt discrTp discrShp variants + let variantTprs = + FC.fmapFC variantShapeType expectedVariantShps + let enumTpr = Mir.RustEnumRepr + discrTpr + variantTprs + + -- Construct the VariantShape of the particular variant that we + -- are building. + Some variantIdx <- pure $ + variantIntIndex nm variantIdxInt $ + Ctx.size expectedVariantShps + VariantShape expectedFldAssn <- + pure $ expectedVariantShps Ctx.! variantIdx + + -- Check that the actual field values match the expected types. + Some (Functor.Pair actualFldAssn actualValAssn) <- + pure $ variantFieldsToAssns sym flds' + Refl <- + case W4.testEquality expectedFldAssn actualFldAssn of + Just r -> pure r + Nothing -> + panic "resolveSetupVal" + [ "Enum field shape mismatch" + , "Expected: " ++ show expectedFldAssn + , "Actual: " ++ show actualFldAssn + ] + + -- Finally, construct a MIRVal. + let enumVal = + Ctx.empty + Ctx.:> RV discrVal + Ctx.:> RV (injectVariant sym variantTprs variantIdx actualValAssn) + pure $ MIRVal enumShp $ AnyValue enumTpr enumVal + Mir.Adt nm Mir.Struct _ _ _ _ _ -> + panic "resolveSetupVal" + [ "Expected enum type, received struct:" + , show nm + ] + Mir.Adt nm Mir.Union _ _ _ _ _ -> + panic "resolveSetupVal" + [ "Expected enum type, received union:" + , show nm + ] + -- See Note [Symbolic enums] in SAWScript.Crucible.MIR.Setup.Value for + -- more information on the approach used to resolve symbolic enum + -- values. + MirSetupEnumSymbolic adt discr variantFlds -> + case adt of + _ | adt ^. Mir.adtReprTransparent -> + -- `repr(transparent)` enum values use MirSetupEnumVariant rather + -- than MirSetupEnumSymbolic. See the Haddocks for + -- MirSetupEnumSymbolic for an explanation. + panic "resolveSetupVal" + [ "Symbolic enum of type " ++ show (adt ^. Mir.adtname) + , "that uses MirSetupEnumSymbolic rather than MirSetupEnumVarianr" + ] + Mir.Adt nm (Mir.Enum discrTp) variants _ _ _ _ -> do + -- Resolve the discriminant value and ensure that it has an + -- integral type. + MIRVal discrShp discrVal <- resolveSetupVal mcc env tyenv nameEnv discr + IsBVShape _ discrW <- pure $ testDiscriminantIsBV discrShp + let discrTpr = shapeType discrShp + + -- Resolve the field values in each possible variant and check + -- that they have the expected types. + variantFlds' <- + zipWithM + (\variant flds -> do + let variantDiscr = getEnumVariantDiscr variant + variantDiscrBV <- W4.bvLit sym discrW $ BV.mkBV discrW variantDiscr + branch <- W4.bvEq sym variantDiscrBV discrVal + flds' <- traverse (resolveSetupVal mcc env tyenv nameEnv) flds + let expectedFlds = variant ^. Mir.vfields + let actualFldTys = map (\(MIRVal shp _) -> shapeMirTy shp) flds' + checkFields + nm + "Enum" + ("fields in enum variant " ++ show (variant ^. Mir.vname)) + expectedFlds + actualFldTys + Some (Functor.Pair fldShpAssn valAssn) <- + pure $ variantFieldsToAssns sym flds' + pure $ Some + $ Functor.Pair + (VariantShape fldShpAssn) + (VB (W4.PE branch valAssn))) + variants + variantFlds + Some variantBranchAssn <- pure $ Ctx.fromList variantFlds' + let (actualVariantShps, branchAssn) = + Ctx.unzip variantBranchAssn + + -- Construct an EnumShape and RustEnumRepr. + (enumShp, Some expectedVariantShps) <- pure $ + enumShapes adt discrTp discrShp variants + let variantTprs = + FC.fmapFC variantShapeType expectedVariantShps + let enumTpr = Mir.RustEnumRepr + discrTpr + variantTprs + + -- Check that the actual variant types match the expected types. + Refl <- + case W4.testEquality expectedVariantShps actualVariantShps of + Just r -> pure r + Nothing -> + panic "resolveSetupVal" + [ "Enum variant shape mismatch" + , "Expected: " ++ show expectedVariantShps + , "Actual: " ++ show actualVariantShps + ] + + -- Finally, construct a MIRVal. + let enumVal = + Ctx.empty + Ctx.:> RV discrVal + Ctx.:> RV branchAssn + pure $ MIRVal enumShp $ AnyValue enumTpr enumVal + Mir.Adt nm Mir.Struct _ _ _ _ _ -> + panic "resolveSetupVal" + [ "Expected enum type, received struct:" + , show nm + ] + Mir.Adt nm Mir.Union _ _ _ _ _ -> + panic "resolveSetupVal" + [ "Expected enum type, received union:" + , show nm + ] MS.SetupTuple () flds -> do flds' <- traverse (resolveSetupVal mcc env tyenv nameEnv) flds let fldMirTys = map (\(MIRVal shp _) -> shapeMirTy shp) flds' @@ -427,6 +635,72 @@ resolveSetupVal mcc env tyenv nameEnv val = usizeBvLit :: Sym -> Int -> IO (W4.SymBV Sym Mir.SizeBits) usizeBvLit sym = W4.bvLit sym W4.knownNat . BV.mkBV W4.knownNat . toInteger + -- Perform a light amount of typechecking on the fields in a struct or enum + -- variant. This ensures that the variant receives the expected number of + -- types and that the types of each field match. + checkFields :: + Mir.DefId {- The struct or enum name. (Only used for error messages.) -} -> + String {- "Struct" or "Enum". (Only used for error messages.) -} -> + String {- What type of fields are we checking? + (Only used for error messages.) -} -> + [Mir.Field] {- The expected fields. -} -> + [Mir.Ty] {- The actual field types. -} -> + IO () + checkFields adtNm what fieldDiscr expectedFlds actualFldTys = do + let expectedFldsNum = length expectedFlds + let actualFldsNum = length actualFldTys + unless (expectedFldsNum == actualFldsNum) $ + fail $ unlines + [ "Mismatch in number of " ++ fieldDiscr + , what ++ " name: " ++ show adtNm + , "Expected number of fields: " ++ show expectedFldsNum + , "Actual number of fields: " ++ show actualFldsNum + ] + zipWithM_ + (\expectedFld actualFldTy -> + let expectedFldTy = expectedFld ^. Mir.fty in + let expectedFldName = expectedFld ^. Mir.fName in + unless (checkCompatibleTys expectedFldTy actualFldTy) $ + fail $ unlines + [ what ++ " field type mismatch" + , "Field name: " ++ show expectedFldName + , "Expected type: " ++ show (PP.pretty expectedFldTy) + , "Given type: " ++ show (PP.pretty actualFldTy) + ]) + expectedFlds + actualFldTys + + -- Construct the 'TypeShape' for an enum, along with the 'VariantShape's for + -- the enum's variants. + enumShapes :: + Mir.Adt {- The enum type -} -> + Mir.Ty {- The discriminant's MIR type -} -> + TypeShape discrShp {- The discriminant's TypeShape -} -> + [Mir.Variant] {- The enum's variants -} -> + (TypeShape AnyType, Some (Ctx.Assignment VariantShape)) + enumShapes adt discrTp discrShp variants + | let variantTys = + map (\v -> v ^.. Mir.vfields . each . Mir.fty) variants + , Some variantShps <- + Ctx.fromList $ + map (\fldTys -> + case Ctx.fromList $ + map + (\ty -> + case tyToShape col ty of + Some shp -> + if Mir.canInitialize col ty + then Some $ ReqField shp + else Some $ OptField shp) + fldTys of + Some fldAssn -> Some $ VariantShape fldAssn) + variantTys + , let enumShp = + EnumShape + (mirAdtToTy adt) variantTys + variantShps discrTp discrShp + = (enumShp, Some variantShps) + -- Resolve parts of a slice that are shared in common between -- 'MirSetupSlice' and 'MirSetupSliceRange'. resolveSetupSliceFromArray :: @@ -445,6 +719,36 @@ resolveSetupVal mcc env tyenv nameEnv val = pure $ SetupSliceFromArray elemTpr sliceShp refVal len _ -> X.throwM $ MIRSliceNonArrayReference $ shapeMirTy arrRefShp + -- Resolve a transparent struct or enum value. + resolveTransparentSetupVal :: Mir.Adt -> SetupValue -> IO MIRVal + resolveTransparentSetupVal adt fld = do + MIRVal shp fld' <- resolveSetupVal mcc env tyenv nameEnv fld + pure $ MIRVal (TransparentShape (mirAdtToTy adt) shp) fld' + + -- Given the list of fields in a struct or enum variant, construct two + -- Assignments, where the first Assignment consists of each field's type, + -- and the second assignment consists of each field's value. + variantFieldsToAssns :: + Sym -> + [MIRVal] -> + Some (Functor.Product + (Ctx.Assignment FieldShape) + (Ctx.Assignment (RegValue' Sym))) + variantFieldsToAssns sym flds + | Some fldValAssn <- someFldValAssn + , (fldAssn, valAssn) <- Ctx.unzip fldValAssn + = Some $ Functor.Pair fldAssn valAssn + where + someFldValAssn :: + Some (Ctx.Assignment (Functor.Product FieldShape (RegValue' Sym))) + someFldValAssn = + Ctx.fromList $ + map (\(MIRVal shp v) -> + if Mir.canInitialize col (shapeMirTy shp) + then Some $ Functor.Pair (ReqField shp) (RV v) + else Some $ Functor.Pair (OptField shp) (RV (W4.justPartExpr sym v))) + flds + -- | An intermediate data structure that is only used by -- 'resolveSetupSliceFromArray'. data SetupSliceFromArray where @@ -697,6 +1001,21 @@ equalValsPred cc mv1 mv2 = goFldAssn fldShp fldAssn1 fldAssn2 (_, _) -> pure $ W4.falsePred sym + goTy (EnumShape _ _ variantShp _ discrShp) any1 any2 = + case (any1, any2) of + (AnyValue (Mir.RustEnumRepr discrTpr1 variantCtx1) + (Ctx.Empty Ctx.:> RV discr1 Ctx.:> RV variant1), + AnyValue (Mir.RustEnumRepr discrTpr2 variantCtx2) + (Ctx.Empty Ctx.:> RV discr2 Ctx.:> RV variant2)) -> do + Refl <- testEquality discrTpr1 discrTpr2 + Refl <- testEquality (shapeType discrShp) discrTpr1 + Refl <- testEquality variantCtx1 variantCtx2 + Refl <- testEquality (FC.fmapFC variantShapeType variantShp) variantCtx1 + discrPred <- goTy discrShp discr1 discr2 + variantPred <- goVariantAssn variantShp variant1 variant2 + liftIO $ W4.andPred sym discrPred variantPred + (_, _) -> + pure $ W4.falsePred sym goTy (TransparentShape _ shp) v1 v2 = goTy shp v1 v2 goTy (RefShape _ _ _ _) ref1 ref2 = @@ -749,6 +1068,34 @@ equalValsPred cc mv1 mv2 = (W4.truePred sym) (Ctx.zipWith Functor.Pair fldAssn1 fldAssn2) + goVariantAssn :: Ctx.Assignment VariantShape ctx + -> Ctx.Assignment (VariantBranch Sym) ctx + -> Ctx.Assignment (VariantBranch Sym) ctx + -> MaybeT IO (W4.Pred Sym) + goVariantAssn variantShp vbAssn1 vbAssn2 = + FCI.ifoldrMFC + (\idx (Functor.Pair (VB var1) (VB var2)) z -> do + VariantShape fldShp <- pure $ variantShp Ctx.! idx + varPred <- goVariantFlds fldShp var1 var2 + liftIO $ W4.andPred sym varPred z) + (W4.truePred sym) + (Ctx.zipWith Functor.Pair vbAssn1 vbAssn2) + + goVariantFlds :: Ctx.Assignment FieldShape ctx + -> W4.PartExpr (W4.Pred Sym) (Ctx.Assignment (RegValue' Sym) ctx) + -> W4.PartExpr (W4.Pred Sym) (Ctx.Assignment (RegValue' Sym) ctx) + -> MaybeT IO (W4.Pred Sym) + goVariantFlds fldShp (W4.PE p1 fldAssn1) (W4.PE p2 fldAssn2) = do + pPred <- liftIO $ W4.eqPred sym p1 p2 + fldPred <- goFldAssn fldShp fldAssn1 fldAssn2 + liftIO $ W4.andPred sym pPred fldPred + goVariantFlds _ W4.Unassigned W4.Unassigned = + pure $ W4.truePred sym + goVariantFlds _ (W4.PE{}) W4.Unassigned = + pure $ W4.falsePred sym + goVariantFlds _ W4.Unassigned (W4.PE{}) = + pure $ W4.falsePred sym + goFld :: FieldShape tp -> RegValue Sym tp -> RegValue Sym tp @@ -1164,3 +1511,48 @@ staticTyRef static = Mir.TyRef (static ^. Mir.sTy) (staticMutability static) + +-- | Retrieve the discriminant corresponding to an enum variant. This function +-- will panic if the variant does not contain a discriminant. +getEnumVariantDiscr :: Mir.Variant -> Integer +getEnumVariantDiscr variant = + case variant ^. Mir.discrval of + Just discr -> + discr + Nothing -> + panic "getEnumVariantDiscr" + [ "discrval not set for variant:" + , show (variant ^. Mir.vname) + ] + +-- | An enum's discriminant should have an integral type such as @isize@ or +-- @i8@, which this function checks. If this is not the case, this function will +-- panic. +testDiscriminantIsBV :: TypeShape shp -> IsBVShape shp +testDiscriminantIsBV discrShp = + case testBVShape discrShp of + Just ibvs -> ibvs + Nothing -> + panic "testDiscriminantIsBV" + [ "Unexpected non-integral discriminant type:" + , show $ PP.pretty $ shapeMirTy discrShp + ] + +-- | Compute the index of a variant as an 'Ctx.Index'. If the index is out of +-- range, this function will panic. +variantIntIndex :: + Mir.DefId {-^ The enum identifier. (Only used for error messages.) -} -> + Int {-^ The index of the variant as an 'Int'. -} -> + Ctx.Size ctx {-^ The number of variants as a 'Ctx.Size'. -} -> + Some (Ctx.Index ctx) +variantIntIndex adtNm variantIdx variantsSize = + case Ctx.intIndex variantIdx variantsSize of + Just someIdx -> + someIdx + Nothing -> + panic "variantIntIndex" + [ "Enum variant index out of range" + , "Enum: " ++ show adtNm + , "Index: " ++ show variantIdx + , "Number of variants: " ++ show variantsSize + ] diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs index bbdfbd85a9..04239058f8 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -12,10 +12,13 @@ module, plus additional functionality) instead. -} {-# Language DataKinds #-} +{-# Language GADTs #-} {-# Language OverloadedStrings #-} {-# Language RankNTypes #-} +{-# Language StandaloneDeriving #-} {-# Language TemplateHaskell #-} {-# Language TypeFamilies #-} +{-# Language TypeOperators #-} module SAWScript.Crucible.MIR.Setup.Value ( -- * @MIRCrucibleContext@ @@ -47,6 +50,9 @@ module SAWScript.Crucible.MIR.Setup.Value , mpMirType , mpRef + -- * @MirSetupEnum@ + , MirSetupEnum(..) + -- * @MirSetupSlice@ , MirSetupSlice(..) ) where @@ -71,6 +77,7 @@ import qualified SAWScript.Crucible.Common.Setup.Value as MS type instance MS.XSetupNull MIR = Void type instance MS.XSetupGlobal MIR = () type instance MS.XSetupStruct MIR = M.Adt +type instance MS.XSetupEnum MIR = MirSetupEnum type instance MS.XSetupTuple MIR = () type instance MS.XSetupSlice MIR = MirSetupSlice -- The 'M.Ty' represents the type of array elements. @@ -138,6 +145,77 @@ data MirPointer sym tp = MirPointer , _mpRef :: MirReferenceMux sym tp } +-- | A enum-related MIR 'SetupValue'. +data MirSetupEnum where + -- | A specific variant of an enum. + MirSetupEnumVariant :: + M.Adt + -- ^ The enum type. + -> M.Variant + -- ^ The variant to use. + -> Int + -- ^ The index of the variant within the list of all the enum's variants. + -- In most circumstances, this index will be the same as the discriminant + -- value, but the index can be different if a variant uses an explicit + -- value. For instance, in this example: + -- + -- @ + -- enum A { + -- A0, + -- A1, + -- } + -- + -- enum B { + -- B0 = 42, + -- B1, + -- } + -- @ + -- + -- The indexes for @A0@ and @B0@ are both @0@, and the indexes for @A1@ + -- and @B1@ are both @1@. The discriminant values are different, however. + -- The discriminants for @A0@ and @A1@ are @0@ and @1@, respectively, + -- while the discriminants for @B0@ and @B1@ are @42@ and @43@, + -- respectively. + -- + -- Note that the index is accessible within the 'M.Variant' argument, but + -- retrieving the information is somewhat involved. (See the + -- implementation of @mir_enum_value@.) For this reason, we store this + -- information separately in 'MirSetupEnumVariant' to make it easier to + -- look up later. + -> [MS.SetupValue MIR] + -- ^ The values of the variant's fields. + -> MirSetupEnum + + -- | A symbolic enum value, where the 'M.Adt' represents the enum type. + -- This is only used in the implementation of @mir_fresh_expanded_value@. + -- See @Note [Symbolic enums]@ for a more detailed explanation. + -- + -- Note that @repr(transparent)@ enums never use 'MirSetupEnumSymbolic'. + -- Instead, they are represented as a 'MirSetupEnumVariant' where the + -- underlying variant field is symbolic. This makes it simpler to ensure that + -- resolving a @repr(transparent@ enum value will yield a 'MIRVal' whose + -- 'TypeShape' is 'TransparentShape'. + MirSetupEnumSymbolic :: + M.Adt + -- ^ The enum type. + -> MS.SetupValue MIR + -- ^ The symbolic discriminant value. + -> [[MS.SetupValue MIR]] + -- ^ The symbolic values that are used for the fields in each variant. + -- For instance, if one created a symbolic value of this type: + -- + -- @ + -- enum E { + -- E1(u16), + -- E2(u32, u32), + -- @ + -- + -- Then the list of fields would be @[[x], [y, z]]@, where @x: u16@ + -- are the fields of @E1@, and @y: u32@ and @z: u32@ are the fields of + -- @E2@. + -> MirSetupEnum + deriving Show + -- | A slice-related MIR 'SetupValue'. data MirSetupSlice = MirSetupSliceRaw (MS.SetupValue MIR) (MS.SetupValue MIR) @@ -157,3 +235,137 @@ data MirSetupSlice makeLenses ''MIRCrucibleContext makeLenses ''MirAllocSpec makeLenses ''MirPointer + +{- +Note [Symbolic enums] +~~~~~~~~~~~~~~~~~~~~~ +Creating a symbolic MIR enum value is not quite as straightforward as creating +symbolic versions of other compound types, mostly due to the atypical Crucible +representation that enums use. To recap, if we have an enum like this: + + enum E { + E1(u16), + E2(u32, u32), + } + +Then this will be implemented using (roughly) the following Crucible `Type` +under the hood: + + (BVType 64, VariantType [StructType [BVType 16], StructType [BVType 32, BVType 32]]) + +Where: + +* The `BVType 64` is a /discriminant/, whose value indicates which variant is + in use. For instance, a discriminant value of `0` indicates that the `E1` + variant is in use, and a discriminant value of `1` indicates that the `E2` + variant is in use. +* The `VariantType ...` indicates that there are two variants in this enum, + where each variant is represented as a struct with the corresponding fields + in that variant. + +At simulation time, VariantTypes are represented as a sequence of +VariantBranches, where a VariantBranch is (roughly) a pair of: + +* A (possibly symbolic) predicate indicating if that variant is being used, and +* A payload representing the fields of the enum. If the predicate does not + hold, then the payload will likely be symbolic, since it does not matter what + the payload value is in that case. + +OK, recap over. Let's get back to the original question: how do we make a +symbolic value of this type? A naïve first attempt is to generate fresh +symbolic values for everything. That is, a symbolic discriminant, as well as a +symbolic predicate and payload for each VariantBranch. While tempting, this +approach won't work. To see why, consider what happens when one pattern matches +on a symbolic enum value. For example, the `match` expression in this function: + + fn foo(x: E) -> u32 { + match x { + E::E1(a) => bar(y), + E::E2(b, c) => baz(b, c), + } + } + +Would turn into the (roughly) following MIR: + + fn foo(x : E) -> u32 { + start_block: { + discr = Discriminant(x, isize); + switchint discr :isize [0, 1] -> [e1_block, e2_block, fallthrough_block] + } + e1_block: { + ... call bar() ... + } + e2_block: { + ... call baz() ... + } + fallthrough_block: { + unreachable; + } + ... + } + +Here, the `switchint discr` statement will check the value of `discr` (the +discriminant), and if it equals `0`, go to `e1_block`; if it equals `1`, go to +`e2_block`; and if it equals something else, go to `fallthrough_block`. In +normal circumstances, `discr` should only ever be equal to `0` or `1`, which +implies that `fallthrough_block` should never be accessible (as indicated by +its `unreachable` instruction). + +Now consider what would happen if the discriminant were an unconstrained, +symbolic value. While a symbolic discriminant could be equal to `0` or `1`, it +could also be equal to any other value! This would spell disaster if Crucible +tried to perform a symbolic branch on, say, `discr == 2`, since that would +cause execution to reach `fallthrough_block` and crash. We want a symbolic +discriminant, but we don't want it to be /that/ symbolic! + +For this reason, after we create a symbolic discriminant value, we also add a +Crucible assumption that the discriminant must be equal to one of the possible +enum variants' discriminants. In the example above, this means that we would +assume assume the following: + + (discr == 0) \/ (discr == 1) + +This way, symbolic execution will never reach `fallthrough_block`. This +Crucible assumption is created in +SAWScript.Crucible.MIR.Builtins.constructExpandedSetupValue.goEnum`. + +Similarly, we cannot make the VariantBranch predicates completely symbolic, as +whether a predicate holds or not depends on the value of the discriminant. For +this reason, we do not create fresh variables for each predicate, but instead +make each predicate the result of checking the discriminant against particular +values. For instance, the predicate for the `E1` VariantBranch is defined to be +`discr == 0`, and the predicate for the `E2` VariantBranch is defined to be +`discr == 1`. These predicates are defined in +`SAWScript.Crucible.MIR.ResolveSetupValue.resolveSetupValue`, along with the +fields in the associated payloads. + +Lastly, there are the payloads (i.e., the fields of each variant) in each +VariantBranch. These are created as completely symbolic values—the trick is to +only access the fields when the corresponding predicate holds. For example, +`SAWScript.Crucible.MIR.Override.matchArg` (in the `MirSetupEnumSymbolic` case) +must be able to match two possibly symbolic enum values together, but it must +be careful to only match the fields in a variant if that VariantBranch's +predicate holds. + +To make this a bit more specific, suppose we have two symbolic enum values +`enumA` and `enumA`, where: + +* `enumA` has the discriminant value `discrA`, and + `enumB` has the discriminant value `discrB`. +* `enumA` has the VariantBranches [(e1_pred_a, [e1_fld1_a]), (e2_pred_a, [e2_fld1_a, e2_fld2_a])], and + `enumB` has the VariantBranches [(e1_pred_b, [e1_fld1_b]), (e2_pred_b, [e2_fld1_b, e2_fld2_b])]. + +We only want to match `e1_fld1_a` against `e1_fld1_b` if both enums are using +the `E1` variant, that is, if `e1_pred_a` and `e_pred_b` hold. To this end, the +`matchArg` function checks this by generating (roughly) the following +assertion: + + (discrA == discrB) /\ + (e1_pred_a ==> (e1_fld1_a == e1_fld1_b)) + +(Note that instead of `e1_pred_a ==> ...`, we could have alternatively used +`e1_pred_b ==> ...`, `(discrA == 0) ==> ...`, or `(discrB == 0) ==> ...`. All +formulations are equivalent.) + +Phew! Enums are surprisingly tricky. +-} diff --git a/src/SAWScript/Crucible/MIR/TypeShape.hs b/src/SAWScript/Crucible/MIR/TypeShape.hs index f24d372ea8..92aa2f80c8 100644 --- a/src/SAWScript/Crucible/MIR/TypeShape.hs +++ b/src/SAWScript/Crucible/MIR/TypeShape.hs @@ -6,18 +6,23 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} -- | The 'TypeShape' data type and related utilities. module SAWScript.Crucible.MIR.TypeShape ( TypeShape(..) , FieldShape(..) + , VariantShape(..) , tyToShape , tyToShapeEq , shapeType , fieldShapeType + , variantShapeType , shapeMirTy , fieldShapeMirTy , shapeToTerm + , IsBVShape(..) + , testBVShape , IsRefShape(..) , testRefShape , sliceShapeParts @@ -95,6 +100,21 @@ data TypeShape (tp :: CrucibleType) where -> TypeRepr tp -- ^ The Crucible representation of @T@. -> TypeShape (MirSlice tp) + -- | A shape for an enum type. Like 'StructShape', this is indexed by + -- 'AnyType', so code that matches on 'EnumShape' may need to further match + -- on the 'VariantShape's in order to bring additional type information into + -- scope. + EnumShape :: M.Ty + -- ^ The overall enum type. + -> [[M.Ty]] + -- ^ The field types in each of the enum's variants. + -> Assignment VariantShape ctx + -- ^ The shapes of the enum type's variants. + -> M.Ty + -- ^ The discriminant type. + -> TypeShape discrTp + -- ^ The shape of the discriminant type. + -> TypeShape AnyType -- | Note that 'FnPtrShape' contains only 'TypeRepr's for the argument and -- result types, not 'TypeShape's, as none of our operations need to recurse -- inside them. @@ -121,6 +141,25 @@ instance PP.Pretty (FieldShape tp) where deriving instance Show (FieldShape tp) instance ShowF FieldShape +-- | The 'TypeShape' of an enum variant, which consists of some number of field +-- types. +-- +-- This is indexed by a 'StructType', but that is simply an artifact of the +-- particular way that @crucible-mir@ encodes enum types. Despite the use of +-- 'StructType' as a type index, we only use 'VariantShape' for enums, not +-- structs. +data VariantShape (tp :: CrucibleType) where + VariantShape :: Assignment FieldShape ctx + -- ^ The shapes of the variant's field types. + -> VariantShape (StructType ctx) + +-- TODO: Improve? +instance PP.Pretty (VariantShape tp) where + pretty = PP.viaShow + +deriving instance Show (VariantShape tp) +instance ShowF VariantShape + -- | Return the `TypeShape` of `ty`. -- -- It is guaranteed that the `tp :: CrucibleType` index of the resulting @@ -142,8 +181,16 @@ tyToShape col = go M.TyAdt nm _ _ -> case Map.lookup nm (col ^. M.adts) of Just adt | Just ty' <- reprTransparentFieldTy col adt -> mapSome (TransparentShape ty) $ go ty' - Just (M.Adt _ M.Struct [v] _ _ _ _) -> goStruct ty (v ^.. M.vfields . each . M.fty) - Just (M.Adt _ ak _ _ _ _ _) -> error $ "tyToShape: AdtKind " ++ show ak ++ " NYI" + Just (M.Adt _ kind vs _ _ _ _) -> + case kind of + M.Struct + | [v] <- vs + -> goStruct ty (variantFieldTys v) + | otherwise + -> error $ "tyToShape: Unexpected struct with multiple variants: " + ++ show (PP.pretty vs) + M.Enum discrTy -> goEnum ty discrTy vs + M.Union -> error "tyToShape: Union types NYI" Nothing -> error $ "tyToShape: bad adt: " ++ show ty M.TyRef ty' mutbl -> goRef ty ty' mutbl M.TyRawPtr ty' mutbl -> goRef ty ty' mutbl @@ -167,7 +214,38 @@ tyToShape col = go loop (ty':tys') flds | Some fld <- go ty' = loop tys' (flds :> OptField fld) goStruct :: M.Ty -> [M.Ty] -> Some TypeShape - goStruct ty tys | Some flds <- loop tys Empty = Some $ StructShape ty tys flds + goStruct ty tys | Some flds <- goFields tys = Some $ StructShape ty tys flds + + -- The first Ty is the overall enum type, and the second Ty is the + -- discriminant type. + goEnum :: M.Ty -> M.Ty -> [M.Variant] -> Some TypeShape + goEnum ty discrTy vs + | Some discrShp <- go discrTy + , Some variants <- loop vs Empty + = Some $ EnumShape ty variantTys variants discrTy discrShp + where + variantTys = map variantFieldTys vs + + loop :: + forall ctx. + [M.Variant] -> + Assignment VariantShape ctx -> + Some (Assignment VariantShape) + loop [] variants = Some variants + loop (v':vs') variants + | Some variant <- goVariant v' + = loop vs' (variants :> variant) + + -- Process a single Variant in an enum type. + goVariant :: M.Variant -> Some VariantShape + goVariant v + | Some flds <- goFields tys + = Some $ VariantShape flds + where + tys = variantFieldTys v + + goFields :: [M.Ty] -> Some (Assignment FieldShape) + goFields tys = loop tys Empty where loop :: forall ctx. [M.Ty] -> Assignment FieldShape ctx -> Some (Assignment FieldShape) loop [] flds = Some flds @@ -195,6 +273,11 @@ tyToShape col = go tyToReprCont col ret $ \retr -> Some (FnPtrShape ty argsr retr) + -- Retrieve the field types in a variant. This used for both struct and enum + -- variants. + variantFieldTys :: M.Variant -> [M.Ty] + variantFieldTys v = v ^.. M.vfields . each . M.fty + -- | Given a `Ty` and the result of `tyToRepr ty`, produce a `TypeShape` with -- the same index `tp`. Raises an `error` if the `TypeRepr` doesn't match -- `tyToRepr ty`. @@ -215,6 +298,7 @@ shapeType = go go (TupleShape _ _ flds) = StructRepr $ fmapFC fieldShapeType flds go (ArrayShape _ _ shp) = MirVectorRepr $ shapeType shp go (StructShape _ _ _flds) = AnyRepr + go (EnumShape _ _ _ _ _variants) = AnyRepr go (TransparentShape _ shp) = go shp go (RefShape _ _ _ tpr) = MirReferenceRepr tpr go (SliceShape _ _ _ tpr) = MirSliceRepr tpr @@ -224,12 +308,17 @@ fieldShapeType :: FieldShape tp -> TypeRepr tp fieldShapeType (ReqField shp) = shapeType shp fieldShapeType (OptField shp) = MaybeRepr $ shapeType shp +variantShapeType :: VariantShape tp -> TypeRepr tp +variantShapeType (VariantShape flds) = + StructRepr $ fmapFC fieldShapeType flds + shapeMirTy :: TypeShape tp -> M.Ty shapeMirTy (UnitShape ty) = ty shapeMirTy (PrimShape ty _) = ty shapeMirTy (TupleShape ty _ _) = ty shapeMirTy (ArrayShape ty _ _) = ty shapeMirTy (StructShape ty _ _) = ty +shapeMirTy (EnumShape ty _ _ _ _) = ty shapeMirTy (TransparentShape ty _) = ty shapeMirTy (RefShape ty _ _ _) = ty shapeMirTy (SliceShape ty _ _ _) = ty @@ -263,6 +352,24 @@ shapeToTerm sc = go goField (OptField shp) = go shp goField (ReqField shp) = go shp +-- | A witness that a 'TypeShape' is equal to a 'PrimShape' that characterizes +-- a bitvector. +data IsBVShape (tp :: CrucibleType) where + IsBVShape :: (1 <= w) + => M.Ty + -> NatRepr w + -> IsBVShape (BVType w) + +-- | Check that a 'TypeShape' is equal to a 'PrimShape' that characterizes a +-- bitvector. If so, return 'Just' a witness of that equality. Otherwise, return +-- 'Nothing'. +testBVShape :: TypeShape tp -> Maybe (IsBVShape tp) +testBVShape shp = + case shp of + PrimShape ty (BaseBVRepr w) + -> Just $ IsBVShape ty w + _ -> Nothing + -- | A witness that a 'TypeShape' is equal to a 'RefShape'. data IsRefShape (tp :: CrucibleType) where IsRefShape :: M.Ty @@ -313,6 +420,13 @@ instance TestEquality TypeShape where , (TypeApp (ConType [t|CtxRepr|]) AnyType, [|testEquality|]) ]) +instance TestEquality VariantShape where + testEquality = + $(structuralTypeEquality + [t|VariantShape|] + [ (TypeApp (TypeApp (ConType [t|Assignment|]) AnyType) AnyType, [|testEquality|]) + ]) + instance TestEquality FieldShape where testEquality = $(structuralTypeEquality diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 34a021d769..c8e360f3e6 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3936,6 +3936,15 @@ primitives = Map.fromList , "it appears (i.e., before or after `mir_execute_func`)." ] + , prim "mir_enum_value" "MIRAdt -> String -> [MIRValue] -> MIRValue" + (funVal3 mir_enum_value) + Experimental + [ "Create a MIRValue representing a variant of a MIR enum with the given" + , "list of values as elements. The MIRAdt argument determines what enum" + , "type to create; use `mir_find_adt` to retrieve a MIRAdt value. The" + , "String argument represents the variant name." + ] + , prim "mir_execute_func" "[MIRValue] -> MIRSetup ()" (pureVal mir_execute_func) Experimental