diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index c8effab421..079c654749 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -637,6 +637,7 @@ substMethodSpec sc sm ms = do MS.SetupNull _ -> return sv 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.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 @@ -652,6 +653,14 @@ substMethodSpec sc sm ms = do goSetupCondition (MS.SetupCond_Ghost b loc gg tt) = MS.SetupCond_Ghost b loc gg <$> goTypedTerm tt + goSetupSlice (MirSetupSliceRaw ref len) = + MirSetupSliceRaw <$> goSetupValue ref <*> goSetupValue len + goSetupSlice (MirSetupSlice arr) = + MirSetupSlice <$> goSetupValue arr + goSetupSlice (MirSetupSliceRange arr start end) = do + arr' <- goSetupValue arr + pure $ MirSetupSliceRange arr' start end + goTypedTerm tt = do term' <- goTerm $ SAW.ttTerm tt return $ tt { SAW.ttTerm = term' } @@ -737,6 +746,11 @@ regToSetup bak p eval shp rv = go shp rv alloc <- refToAlloc bak p mutbl ty' tpr startRef len let offsetSv idx sv = if idx == 0 then sv else MS.SetupElem () sv idx return $ offsetSv idx $ MS.SetupVar alloc + go (SliceShape _ ty mutbl tpr) (Empty :> RV refRV :> RV lenRV) = do + let (refShp, lenShp) = sliceShapeParts ty mutbl tpr + refSV <- go refShp refRV + lenSV <- go lenShp lenRV + pure $ MS.SetupSlice $ MirSetupSliceRaw refSV lenSV 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 151d025b98..0f71c5cc09 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Clobber.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Clobber.hs @@ -63,7 +63,12 @@ clobberSymbolic sym loc nameStr shp rv = go shp rv go (TransparentShape _ shp) rv = go shp rv go (FnPtrShape _ _ _) _rv = error "Function pointers not currently supported in overrides" - go shp _rv = error $ "clobberSymbolic: " ++ show (shapeType shp) ++ " NYI" + go (RefShape _ _ _ _) _rv = error "clobberSymbolic: RefShape NYI" + go (SliceShape _ ty mutbl tpr) (Ctx.Empty Ctx.:> RV ref Ctx.:> RV len) = do + let (refShp, lenShp) = sliceShapeParts ty mutbl tpr + ref' <- go refShp ref + len' <- go lenShp len + pure $ Ctx.Empty Ctx.:> RV ref' Ctx.:> RV len' goField :: forall tp. FieldShape tp -> RegValue' sym tp -> OverrideSim (p sym) sym MIR rtp args ret (RegValue' sym tp) @@ -109,6 +114,11 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv -- Since this ref is in immutable memory, whatever behavior we're -- approximating with this clobber can't possibly modify it. go (RefShape _ _ _ _tpr) rv = return rv + go (SliceShape _ ty mutbl tpr) (Ctx.Empty Ctx.:> RV ref Ctx.:> RV len) = do + let (refShp, lenShp) = sliceShapeParts ty mutbl tpr + ref' <- go refShp ref + len' <- go lenShp len + pure $ Ctx.Empty Ctx.:> RV ref' Ctx.:> RV len' 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 73e8623d2e..da5d4ce55e 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -409,6 +409,11 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv goRef refTy pointeeTy mutbl tpr ref alloc 0 go (RefShape refTy pointeeTy mutbl tpr) ref (MS.SetupElem () (MS.SetupVar alloc) idx) = goRef refTy pointeeTy mutbl tpr ref alloc idx + go (SliceShape _ ty mutbl tpr) (Ctx.Empty Ctx.:> RV ref Ctx.:> RV len) + (MS.SetupSlice (MirSetupSliceRaw refSV lenSV)) = do + let (refShp, lenShp) = sliceShapeParts ty mutbl tpr + go refShp ref refSV + go lenShp len lenSV go (FnPtrShape _ _ _) _ _ = error "Function pointers not currently supported in overrides" go shp _ sv = error $ "matchArg: type error: bad SetupValue " ++ @@ -534,6 +539,11 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv Nothing -> error $ "setupToReg: type error: bad reference type for " ++ show alloc ++ ": got " ++ show (ptr ^. mpType) ++ " but expected " ++ show tpr Nothing -> error $ "setupToReg: no definition for " ++ show alloc + go (SliceShape _ ty mutbl tpr) (MS.SetupSlice (MirSetupSliceRaw refSV lenSV)) = do + let (refShp, lenShp) = sliceShapeParts ty mutbl tpr + refRV <- go refShp refSV + lenRV <- go lenShp lenSV + pure $ Ctx.Empty Ctx.:> RV refRV Ctx.:> RV lenRV 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 ccc45ba518..08bf240b29 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -340,6 +340,11 @@ munge sym shp rv = do go (FnPtrShape _ _ _) _ = error "Function pointers not currently supported in overrides" -- TODO: RefShape + go (SliceShape _ ty mutbl tpr) (Ctx.Empty Ctx.:> RV ref Ctx.:> RV len) = do + let (refShp, lenShp) = sliceShapeParts ty mutbl tpr + ref' <- go refShp ref + len' <- go lenShp len + pure $ Ctx.Empty Ctx.:> RV ref' Ctx.:> RV len' go shp _ = error $ "munge: " ++ show (shapeType shp) ++ " NYI" goFields :: forall ctx. diff --git a/deps/crucible b/deps/crucible index c19fc2c538..602cb8f04e 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit c19fc2c53851cdd162ae1ccca14032467e3c2fd1 +Subproject commit 602cb8f04ec5f42e76a2ba0833f7e91a95d7109c diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 1d0de3c9da..cb8556d8c7 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -2125,7 +2125,6 @@ implemented include the following: * MIR specifications that use overrides (i.e., the `[MIRSpec]` argument to `mir_verify` must always be the empty list at present) * The ability to construct MIR `enum` values in specifications -* The ability to specify the layout of slice values 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 @@ -2639,6 +2638,9 @@ 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_slice_value : MIRValue -> MIRValue`: see the "MIR slices" section below. +* `mir_slice_range_value : MIRValue -> Int -> Int -> MIRValue`: see the + "MIR slices" section below. * `mir_struct_value : MIRAdt -> [MIRValue] -> MIRValue` construct a struct with the given list of values as elements. The `MIRAdt` argument determines what struct type to create. @@ -2648,6 +2650,88 @@ construct compound values: * `mir_tuple_value : [MIRValue] -> MIRValue` construct a tuple with the given list of values as elements. +### MIR slices + +Slices are a unique form of compound type that is currently only used during +MIR verification. Unlike other forms of compound values, such as arrays, it is +not possible to directly construct a slice. Instead, one must take a slice of +an existing reference value that points to the thing being sliced. The +following commands are used to construct slices: + +* `mir_slice_value : MIRValue -> MIRValue`: the SAWScript expression + `mir_slice_value base` is equivalent to the Rust expression `base[..]`, + i.e., a slice of the entirety of `base`. `base` must be a reference to + an array value. +* `mir_slice_range_value : MIRValue -> Int -> Int -> MIRValue`: the SAWScript + expression `mir_slice_range_value base start end` is equivalent to the Rust + expression `base[start..end]`, i.e., a slice over a part of `base` which + ranges from `start` to `end`. `base` must be a reference to an array value, + and `start` and `end` are assumed to be zero-indexed. `start` must not exceed + `end`, and `end` must be strictly less than the length of the array that + `base` points to. + +As an example of how to use these functions, consider this Rust function, which +accepts an arbitrary slice as an argument: + +~~~~ .rs +pub fn f(s: &[u32]) -> u32 { + s[0] + s[1] +} +~~~~ + +We can write a specification that passes a slice to the array `[1, 2, 3, 4, 5]` +as an argument to `f`: + +~~~~ +let f_spec_1 = do { + a <- mir_alloc (mir_array 5 mir_u32); + mir_points_to a (mir_term {{ [1, 2, 3, 4, 5] : [5][32] }}); + + mir_execute_func [mir_slice_value a]; + + mir_return (mir_term {{ 3 : [32] }}); +}; +~~~~ + +Alternatively, we can write a specification that passes a part of this array +which ranges from second element to the fourth. + +~~~~ +let f_spec_2 = do { + a <- mir_alloc (mir_array 5 mir_u32); + mir_points_to a (mir_term {{ [1, 2, 3, 4, 5] : [5][32] }}); + + mir_execute_func [mir_slice_range_value a 1 3]; + + mir_return (mir_term {{ 5 : [32] }}); +}; +~~~~ + +Note that we are passing _references_ of arrays to `mir_slice_value` and +`mir_slice_range_value`. It would be an error to pass a bare array to these +functions, so the following specification would be invalid: + +~~~~ +let f_fail_spec_ = do { + let arr = mir_term {{ [1, 2, 3, 4, 5] : [5][32] }}; + + mir_execute_func [mir_slice_value arr]; // BAD: `arr` is not a reference + + mir_return (mir_term {{ 3 : [32] }}); +}; +~~~~ + +SAW's support for slices is currently limited: + +* SAW specifications cannot say anything about `&str` slice arguments or return + values at present. +* The `mir_slice_range_value` function must accept bare `Int` arguments to + specify the lower and upper bounds of the range. A consequence of this design + is that it is not possible to create a slice with a symbolic length. + +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 We collectively refer to MIR `struct`s and `enum`s together as _algebraic data diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index de9ccf68b8..bdf584c2be 100644 Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ diff --git a/intTests/test_mir_verify_slices/Makefile b/intTests/test_mir_verify_slices/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_verify_slices/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_slices/test.linked-mir.json b/intTests/test_mir_verify_slices/test.linked-mir.json new file mode 100644 index 0000000000..f64340091b --- /dev/null +++ b/intTests/test_mir_verify_slices/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"pos":"test.rs:2:7: 2:8","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"}},"pos":"test.rs:2:5: 2:9","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"}},"pos":"test.rs:2:5: 2:9","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"}},"kind":"Copy"},"kind":"BinaryOp","op":{"kind":"Lt"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"}},"kind":"Move"},"expected":true,"kind":"Assert","msg":"index out of bounds: the length is move _4 but the index is _3","pos":"test.rs:2:5: 2:9","target":"bb1"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:2:5: 2:9","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"}},"pos":"test.rs:2:14: 2:15","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::usize"}},"pos":"test.rs:2:12: 2:16","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"pos":"test.rs:2:12: 2:16","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::usize"}},"kind":"Copy"},"kind":"BinaryOp","op":{"kind":"Lt"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"kind":"Move"},"expected":true,"kind":"Assert","msg":"index out of bounds: the length is move _8 but the index is _7","pos":"test.rs:2:12: 2:16","target":"bb2"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"pos":"test.rs:2:12: 2:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:2:5: 2:16","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"kind":"Copy"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _2 + move _6`, which would overflow","pos":"test.rs:2:5: 2:16","target":"bb3"}},"blockid":"bb2"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:2:5: 2:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:3:2: 3: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::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}]},"name":"test/91ae4be1::f","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::fb1cfdc5725cd03b"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:5:21: 5:21"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/91ae4be1::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/91ae4be1::f","kind":"Item","substs":[]},"name":"test/91ae4be1::f"},{"inst":{"def_id":"test/91ae4be1::g","kind":"Item","substs":[]},"name":"test/91ae4be1::g"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Slice::f7eb0deb10702a2f","ty":{"kind":"Slice","ty":"ty::u32"}},{"name":"ty::Ref::2829f685526f8473","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::f7eb0deb10702a2f"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::7063e33f0dbc8a58","ty":{"kind":"Tuple","tys":["ty::u32","ty::bool"]}},{"name":"ty::str","ty":{"kind":"Str"}},{"name":"ty::Ref::fb1cfdc5725cd03b","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::str"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}}],"roots":["test/91ae4be1::f","test/91ae4be1::g"]} \ No newline at end of file diff --git a/intTests/test_mir_verify_slices/test.rs b/intTests/test_mir_verify_slices/test.rs new file mode 100644 index 0000000000..e8285e44c0 --- /dev/null +++ b/intTests/test_mir_verify_slices/test.rs @@ -0,0 +1,5 @@ +pub fn f(s: &[u32]) -> u32 { + s[0] + s[1] +} + +pub fn g(_: &str) {} diff --git a/intTests/test_mir_verify_slices/test.saw b/intTests/test_mir_verify_slices/test.saw new file mode 100644 index 0000000000..ae391c13d7 --- /dev/null +++ b/intTests/test_mir_verify_slices/test.saw @@ -0,0 +1,115 @@ +enable_experimental; + +let oneThroughFive = mir_term {{ [1, 2, 3, 4, 5] : [5][32] }}; + +let f_spec_1 = do { + a <- mir_alloc (mir_array 5 mir_u32); + mir_points_to a oneThroughFive; + + mir_execute_func [mir_slice_value a]; + + mir_return (mir_term {{ 3 : [32] }}); +}; + +let f_spec_2 = do { + a <- mir_alloc (mir_array 5 mir_u32); + mir_points_to a oneThroughFive; + + mir_execute_func [mir_slice_range_value a 1 3]; + + mir_return (mir_term {{ 5 : [32] }}); +}; + +// mir_slice_value must take an array reference as an argument. +// Passing a bare array constitutes a type error. +let f_fail_spec_1 = do { + let arr = mir_array_value mir_u32 [mir_term {{ 1 : [32] }}]; + mir_execute_func [mir_slice_value arr]; + + mir_return (mir_term {{ 0 : [32] }}); +}; + +// The end value of the range given to mir_slice_range_value must be less +// than the length of the slice. +let f_fail_spec_2 = do { + a <- mir_alloc (mir_array 5 mir_u32); + mir_points_to a oneThroughFive; + + mir_execute_func [mir_slice_range_value a 0 5]; + + mir_return (mir_term {{ 0 : [32] }}); +}; + +// The start value of the range given to mir_slice_range_value must not +// exceed the end value. +let f_fail_spec_3 = do { + a <- mir_alloc (mir_array 5 mir_u32); + mir_points_to a oneThroughFive; + + mir_execute_func [mir_slice_range_value a 6 5]; + + mir_return (mir_term {{ 0 : [32] }}); +}; + +// Indexing into a length-0 slice is disallowed. +let f_fail_spec_4 = do { + a <- mir_alloc (mir_array 5 mir_u32); + mir_points_to a oneThroughFive; + + mir_execute_func [mir_slice_range_value a 0 0]; + + mir_return (mir_term {{ 0 : [32] }}); +}; + +// f requires a slice of length at least two. +let f_fail_spec_5 = do { + a <- mir_alloc (mir_array 5 mir_u32); + mir_points_to a oneThroughFive; + + mir_execute_func [mir_slice_range_value a 0 1]; + + mir_return (mir_term {{ 0 : [32] }}); +}; + +// mir_alloc cannot be used to allocate slice references. +let f_fail_spec_6 = do { + s <- mir_alloc (mir_slice mir_u32); + + mir_execute_func [s]; + + mir_return (mir_term {{ 0 : [32] }}); +}; + +// mir_alloc cannot be used to allocate str references. +let g_fail_spec = do { + s <- mir_alloc mir_str; + + mir_execute_func [s]; +}; + +m <- mir_load_module "test.linked-mir.json"; + +mir_verify m "test::f" [] false f_spec_1 z3; +mir_verify m "test::f" [] false f_spec_2 z3; + +fails ( + mir_verify m "test::f" [] false f_fail_spec_1 z3 +); +fails ( + mir_verify m "test::f" [] false f_fail_spec_2 z3 +); +fails ( + mir_verify m "test::f" [] false f_fail_spec_3 z3 +); +fails ( + mir_verify m "test::f" [] false f_fail_spec_4 z3 +); +fails ( + mir_verify m "test::f" [] false f_fail_spec_5 z3 +); +fails ( + mir_verify m "test::f" [] false f_fail_spec_6 z3 +); +fails ( + mir_verify m "test::g" [] false g_fail_spec z3 +); diff --git a/intTests/test_mir_verify_slices/test.sh b/intTests/test_mir_verify_slices/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_verify_slices/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 a7e3531764..954e6dbdf3 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -25,6 +25,9 @@ * The API for `"struct"` `setup value`s now has a `"MIR ADT"` field. For MIR verification, this field is required. For LLVM and JVM verification, this field must be `null`, or else an error will be raised. +* 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. ## 1.0.0 -- 2023-06-26 diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index 6a25dcc327..d86cc7807b 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -24,6 +24,8 @@ an error. * Add a `tuple_value()` function for constructing MIR tuples. Using this function with LLVM or JVM verification will raise an error. +* Add `slice_value()` and `slice_range()` functions for constructing MIR slices. + Using these functions with LLVM or JVM verification will raise an error. * The `proclaim` function (which is the Python counterpart to to `{llvm,jvm,mir}_assert` in SAWScript) is no longer deprecated. * Add a `proclaim_f` function. This behaves like the `proclaim` function, except diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py index d6ad9c1944..3baef1605e 100644 --- a/saw-remote-api/python/saw_client/crucible.py +++ b/saw-remote-api/python/saw_client/crucible.py @@ -163,6 +163,32 @@ def __init__(self, fields : List[SetupVal]) -> None: def to_json(self) -> JSON: return {'setup value': 'tuple', 'elements': [fld.to_json() for fld in self.fields]} +class SliceVal(SetupVal): + base : SetupVal + + def __init__(self, base : SetupVal) -> None: + self.base = base + + def to_json(self) -> JSON: + return {'setup value': 'slice', + 'base': self.base.to_json()} + +class SliceRangeVal(SetupVal): + base : SetupVal + start : int + end : int + + def __init__(self, base : SetupVal, start : int, end : int) -> None: + self.base = base + self.start = start + self.end = end + + def to_json(self) -> JSON: + return {'setup value': 'slice range', + 'base': self.base.to_json(), + 'start': self.start, + 'end': self.end} + class ElemVal(SetupVal): base : SetupVal index : int @@ -747,6 +773,24 @@ def null() -> SetupVal: """Returns a null pointer value (i.e., a ``NullVal``).""" return NullVal() +def slice_value(base : SetupVal) -> SetupVal: + """Returns a MIR value representing a slice of ``base``, where ``base`` + must be a reference to an array. Using this function with LLVM or JVM + verification will raise an error. + + Unlike most other functions in saw_client.crucible, this has a ``_value`` + suffix so as not to clash with the built-in ``slice()`` function in Python. + """ + return SliceVal(base) + +def slice_range(base : SetupVal, start : int, end : int) -> SetupVal: + """Returns a MIR value representing a slice of ``base`` over a given range, + where ``base`` must be a reference to an array, and ``start`` and ``end`` + delimit the range of values in the slice. Using this function with LLVM or + JVM verification will raise an error. + """ + return SliceRangeVal(base, start, end) + def struct(*fields : SetupVal, mir_adt : Optional[MIRAdt] = None) -> SetupVal: """Returns a structure value with the given ``fields`` (i.e., a ``StructVal``). For MIR structures, it is required to also pass a ``mir_adt`` representing diff --git a/saw-remote-api/python/tests/saw/test-files/mir_slices.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/mir_slices.linked-mir.json new file mode 100644 index 0000000000..fb28f57592 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_slices.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"pos":"mir_slices.rs:2:7: 2:8","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"}},"pos":"mir_slices.rs:2:5: 2:9","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"}},"pos":"mir_slices.rs:2:5: 2:9","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"}},"kind":"Copy"},"kind":"BinaryOp","op":{"kind":"Lt"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"}},"kind":"Move"},"expected":true,"kind":"Assert","msg":"index out of bounds: the length is move _4 but the index is _3","pos":"mir_slices.rs:2:5: 2:9","target":"bb1"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"mir_slices.rs:2:5: 2:9","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"}},"pos":"mir_slices.rs:2:14: 2:15","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::usize"}},"pos":"mir_slices.rs:2:12: 2:16","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"pos":"mir_slices.rs:2:12: 2:16","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::usize"}},"kind":"Copy"},"kind":"BinaryOp","op":{"kind":"Lt"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"kind":"Move"},"expected":true,"kind":"Assert","msg":"index out of bounds: the length is move _8 but the index is _7","pos":"mir_slices.rs:2:12: 2:16","target":"bb2"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"pos":"mir_slices.rs:2:12: 2:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::2829f685526f8473"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"mir_slices.rs:2:5: 2:16","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"kind":"Copy"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _2 + move _6`, which would overflow","pos":"mir_slices.rs:2:5: 2:16","target":"bb3"}},"blockid":"bb2"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"mir_slices.rs:2:5: 2:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"mir_slices.rs:3:2: 3: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::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Tuple::7063e33f0dbc8a58"}]},"name":"mir_slices/4fb0b98c::f","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"mir_slices/4fb0b98c::f","kind":"Item","substs":[]},"name":"mir_slices/4fb0b98c::f"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Slice::f7eb0deb10702a2f","ty":{"kind":"Slice","ty":"ty::u32"}},{"name":"ty::Ref::2829f685526f8473","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::f7eb0deb10702a2f"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::7063e33f0dbc8a58","ty":{"kind":"Tuple","tys":["ty::u32","ty::bool"]}}],"roots":["mir_slices/4fb0b98c::f"]} \ No newline at end of file diff --git a/saw-remote-api/python/tests/saw/test-files/mir_slices.rs b/saw-remote-api/python/tests/saw/test-files/mir_slices.rs new file mode 100644 index 0000000000..f4049ef951 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_slices.rs @@ -0,0 +1,3 @@ +pub fn f(s: &[u32]) -> u32 { + s[0] + s[1] +} diff --git a/saw-remote-api/python/tests/saw/test_mir_slices.py b/saw-remote-api/python/tests/saw/test_mir_slices.py new file mode 100644 index 0000000000..bd0567608f --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_mir_slices.py @@ -0,0 +1,45 @@ +import unittest +from pathlib import Path + +from saw_client import * +from saw_client.crucible import cry_f, slice_range, slice_value +from saw_client.mir import Contract, array_ty, u32 + + +one_through_five = cry_f('[1, 2, 3, 4, 5] : [5][32]') + + +class F1Contract(Contract): + def specification(self) -> None: + a = self.alloc(array_ty(5, u32), points_to=one_through_five, read_only=True) + + self.execute_func(slice_value(a)) + + self.returns(cry_f('3 : [32]')) + + +class F2Contract(Contract): + def specification(self) -> None: + a = self.alloc(array_ty(5, u32), points_to=one_through_five, read_only=True) + + self.execute_func(slice_range(a, 1, 3)) + + self.returns(cry_f('5 : [32]')) + + +class MIRSlicesTest(unittest.TestCase): + def test_mir_slices(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults()) + json_name = str(Path('tests', 'saw', 'test-files', 'mir_slices.linked-mir.json')) + mod = mir_load_module(json_name) + + f1_result = mir_verify(mod, 'mir_slices::f', F1Contract()) + self.assertIs(f1_result.is_success(), True) + + f2_result = mir_verify(mod, 'mir_slices::f', F2Contract()) + self.assertIs(f2_result.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 4523612af0..05163feff6 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -113,6 +113,8 @@ data CrucibleSetupVal ty e -- ADT. This should always be 'Just' with MIR verification and -- 'Nothing' with LLVM or JVM verification. | TupleValue [CrucibleSetupVal ty e] + | SliceValue (CrucibleSetupVal ty e) + | SliceRangeValue (CrucibleSetupVal ty e) Int Int -- | RecordValue [(String, CrucibleSetupVal e)] | FieldLValue (CrucibleSetupVal ty e) String | CastLValue (CrucibleSetupVal ty e) ty diff --git a/saw-remote-api/src/SAWServer/Data/SetupValue.hs b/saw-remote-api/src/SAWServer/Data/SetupValue.hs index 22a329943f..4b784109f1 100644 --- a/saw-remote-api/src/SAWServer/Data/SetupValue.hs +++ b/saw-remote-api/src/SAWServer/Data/SetupValue.hs @@ -15,6 +15,8 @@ data SetupValTag | TagArrayValue | TagStructValue | TagTupleValue + | TagSliceValue + | TagSliceRangeValue | TagFieldLValue | TagCastLValue | TagUnionLValue @@ -32,6 +34,8 @@ instance FromJSON SetupValTag where "array" -> pure TagArrayValue "struct" -> pure TagStructValue "tuple" -> pure TagTupleValue + "slice" -> pure TagSliceValue + "slice range" -> pure TagSliceRangeValue "field" -> pure TagFieldLValue "cast" -> pure TagCastLValue "union" -> pure TagUnionLValue @@ -52,6 +56,8 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cr TagArrayValue -> ArrayValue <$> o .:? "element type" <*> o .: "elements" TagStructValue -> StructValue <$> o .:? "MIR ADT server name" <*> o .: "elements" TagTupleValue -> TupleValue <$> o .: "elements" + TagSliceValue -> SliceValue <$> o .: "base" + TagSliceRangeValue -> SliceRangeValue <$> o .: "base" <*> o .: "start" <*> o .: "end" TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field" TagCastLValue -> CastLValue <$> o .: "base" <*> o .: "type" TagUnionLValue -> UnionLValue <$> o .: "base" <*> o .: "field" diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index 7f051c5fe0..7dd5a4b71f 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -186,6 +186,10 @@ compileJVMContract fileReader bic cenv0 c = JVMSetupM $ fail "Struct setup values unsupported in JVM API." getSetupVal _ (TupleValue _) = JVMSetupM $ fail "Tuple setup values unsupported in JVM API." + getSetupVal _ (SliceValue _) = + JVMSetupM $ fail "Slice setup values unsupported in JVM API." + getSetupVal _ (SliceRangeValue _ _ _) = + JVMSetupM $ fail "Slice range setup values unsupported in JVM API." getSetupVal _ (FieldLValue _ _) = JVMSetupM $ fail "Field l-values unsupported in JVM API." getSetupVal _ (CastLValue _ _) = diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs index 0b9a70066b..35bb922f3f 100644 --- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs @@ -187,6 +187,10 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c = LLVMCrucibleSetupM $ return $ CMS.anySetupStruct False elts' getSetupVal _ (TupleValue _) = LLVMCrucibleSetupM $ fail "Tuple setup values unsupported in the LLVM API." + getSetupVal _ (SliceValue _) = + LLVMCrucibleSetupM $ fail "Slice 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) = do base' <- getSetupVal env base LLVMCrucibleSetupM $ return $ CMS.anySetupField base' fld diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs index e2b5942741..87f904386a 100644 --- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs @@ -34,7 +34,9 @@ import SAWScript.Crucible.MIR.Builtins mir_points_to, mir_postcond, mir_precond, - mir_return ) + mir_return, + mir_slice_value, + mir_slice_range_value ) import SAWScript.Crucible.MIR.ResolveSetupValue (typeOfSetupValue) import SAWScript.Value (BuiltinContext, MIRSetupM(..), biSharedContext) import qualified Verifier.SAW.CryptolEnv as CEnv @@ -200,6 +202,12 @@ compileMIRContract fileReader bic cenv0 sawenv c = pure $ MS.SetupGlobalInitializer () name getSetupVal _ (GlobalLValue name) = pure $ MS.SetupGlobal () name + getSetupVal env (SliceValue base) = do + base' <- getSetupVal env base + pure $ mir_slice_value base' + getSetupVal env (SliceRangeValue base start end) = do + base' <- getSetupVal env base + pure $ mir_slice_range_value base' start end getSetupVal _ (FieldLValue _ _) = MIRSetupM $ fail "Field l-values unsupported in the MIR API." getSetupVal _ (CastLValue _ _) = diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index 3f78ae8d85..e8ce39d657 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -41,6 +41,7 @@ module SAWScript.Crucible.Common.MethodSpec , XSetupNull , XSetupStruct , XSetupTuple + , XSetupSlice , XSetupArray , XSetupElem , XSetupField @@ -141,7 +142,7 @@ import Verifier.SAW.SharedTerm as SAWVerifier 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 () +import SAWScript.Crucible.MIR.Setup.Value (MirSetupSlice(..)) import SAWScript.Options import SAWScript.Prover.SolverStats import SAWScript.Utils (bullets) @@ -202,7 +203,15 @@ ppSetupValue setupval = case setupval of (JVMExt, empty) -> absurd empty (MIRExt, ()) -> - PP.parens (commaList (map ppSetupValue vs)) + ppSetupTuple vs + SetupSlice x -> + case (ext, x) of + (LLVMExt, empty) -> + absurd empty + (JVMExt, empty) -> + absurd empty + (MIRExt, slice) -> + ppMirSetupSlice slice SetupArray _ vs -> PP.brackets (commaList (map ppSetupValue vs)) SetupElem _ v i -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ show i) SetupField _ v f -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ f) @@ -236,6 +245,18 @@ ppSetupValue setupval = case setupval of ppSetupStructDefault :: [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)) + + ppMirSetupSlice :: MirSetupSlice -> PP.Doc ann + ppMirSetupSlice (MirSetupSliceRaw ref len) = + PP.pretty "SliceRaw" <> ppSetupTuple [ref, len] + ppMirSetupSlice (MirSetupSlice arr) = + ppSetupValue arr <> PP.pretty "[..]" + ppMirSetupSlice (MirSetupSliceRange arr start end) = + ppSetupValue arr <> PP.pretty "[" <> PP.pretty start <> + PP.pretty ".." <> PP.pretty end <> PP.pretty "]" + ppAllocIndex :: AllocIndex -> PP.Doc ann ppAllocIndex i = PP.pretty '@' <> PP.viaShow i diff --git a/src/SAWScript/Crucible/Common/Setup/Value.hs b/src/SAWScript/Crucible/Common/Setup/Value.hs index b96b9b2ad8..505acce1c9 100644 --- a/src/SAWScript/Crucible/Common/Setup/Value.hs +++ b/src/SAWScript/Crucible/Common/Setup/Value.hs @@ -39,6 +39,7 @@ module SAWScript.Crucible.Common.Setup.Value , XSetupNull , XSetupStruct , XSetupTuple + , XSetupSlice , XSetupArray , XSetupElem , XSetupField @@ -123,6 +124,7 @@ type family ResolvedState ext :: Type type family XSetupNull ext type family XSetupStruct ext type family XSetupTuple ext +type family XSetupSlice ext type family XSetupArray ext type family XSetupElem ext type family XSetupField ext @@ -139,13 +141,19 @@ data SetupValue ext where SetupTerm :: TypedTerm -> SetupValue ext SetupNull :: XSetupNull ext -> SetupValue ext SetupStruct :: XSetupStruct ext -> [SetupValue ext] -> SetupValue ext - SetupTuple :: XSetupTuple ext -> [SetupValue ext] -> SetupValue ext SetupArray :: XSetupArray ext -> [SetupValue ext] -> SetupValue ext SetupElem :: XSetupElem ext -> SetupValue ext -> Int -> SetupValue ext SetupField :: XSetupField ext -> SetupValue ext -> String -> SetupValue ext SetupCast :: XSetupCast ext -> SetupValue ext -> SetupValue ext SetupUnion :: XSetupUnion ext -> SetupValue ext -> String -> SetupValue ext + -- | A tuple value. At the moment, this is only ever used for MIR + -- verification. + SetupTuple :: XSetupTuple ext -> [SetupValue ext] -> SetupValue ext + -- | A slice value. At the moment, this is only ever used for MIR + -- verification. + SetupSlice :: XSetupSlice ext -> SetupValue ext + -- | A pointer to a global variable SetupGlobal :: XSetupGlobal ext -> String -> SetupValue ext -- | This represents the value of a global's initializer. @@ -161,6 +169,7 @@ type SetupValueHas (c :: Type -> Constraint) ext = ( c (XSetupNull ext) , c (XSetupStruct ext) , c (XSetupTuple ext) + , c (XSetupSlice ext) , c (XSetupArray ext) , c (XSetupElem ext) , c (XSetupField ext) diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 5ba395b742..231338987e 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -576,6 +576,7 @@ matchArg opts sc cc cs prepost md actual@(RVal ref) expectedTy setupval = MS.SetupGlobal empty _ -> absurd empty MS.SetupTuple empty _ -> absurd empty + MS.SetupSlice empty -> absurd empty _ -> failure (cs ^. MS.csLoc) =<< mkStructuralMismatch opts cc sc cs actual setupval expectedTy @@ -967,6 +968,7 @@ instantiateSetupValue sc s v = MS.SetupGlobal empty _ -> absurd empty MS.SetupStruct empty _ -> absurd empty MS.SetupTuple empty _ -> absurd empty + MS.SetupSlice empty -> absurd empty MS.SetupArray empty _ -> absurd empty MS.SetupElem empty _ _ -> absurd empty MS.SetupField empty _ _ -> absurd empty diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs index 6a3863685e..9364b7716c 100644 --- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs @@ -141,6 +141,7 @@ typeOfSetupValue _cc env _nameEnv val = MS.SetupGlobal empty _ -> absurd empty MS.SetupStruct empty _ -> absurd empty MS.SetupTuple empty _ -> absurd empty + MS.SetupSlice empty -> absurd empty MS.SetupArray empty _ -> absurd empty MS.SetupElem empty _ _ -> absurd empty MS.SetupField empty _ _ -> absurd empty @@ -173,6 +174,7 @@ resolveSetupVal cc env _tyenv _nameEnv val = MS.SetupGlobal empty _ -> absurd empty MS.SetupStruct empty _ -> absurd empty MS.SetupTuple empty _ -> absurd empty + MS.SetupSlice empty -> absurd empty MS.SetupArray empty _ -> absurd empty MS.SetupElem empty _ _ -> absurd empty MS.SetupField empty _ _ -> absurd empty diff --git a/src/SAWScript/Crucible/JVM/Setup/Value.hs b/src/SAWScript/Crucible/JVM/Setup/Value.hs index edf3c80581..8286704750 100644 --- a/src/SAWScript/Crucible/JVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/JVM/Setup/Value.hs @@ -79,6 +79,7 @@ type instance MS.XSetupNull CJ.JVM = () type instance MS.XSetupGlobal CJ.JVM = Void type instance MS.XSetupStruct CJ.JVM = Void type instance MS.XSetupTuple CJ.JVM = Void +type instance MS.XSetupSlice CJ.JVM = Void type instance MS.XSetupArray CJ.JVM = Void type instance MS.XSetupElem CJ.JVM = Void type instance MS.XSetupField CJ.JVM = Void diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index f9b258952e..27b11aed0c 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1119,6 +1119,7 @@ matchPointsTos opts sc cc spec prepost = go False [] SetupVar i -> Set.singleton i SetupStruct _ xs -> foldMap setupVars xs SetupTuple empty _ -> absurd empty + SetupSlice empty -> absurd empty SetupArray _ xs -> foldMap setupVars xs SetupElem _ x _ -> setupVars x SetupField _ x _ -> setupVars x @@ -1302,6 +1303,8 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = (_, _, SetupTuple empty _) -> absurd empty + (_, _, SetupSlice empty) -> + absurd empty (Crucible.LLVMValInt blk off, _, SetupElem () v i) | Crucible.isPointerMemType expectedTy -> do let tyenv = MS.csAllocations cs @@ -2486,6 +2489,7 @@ instantiateSetupValue sc s v = SetupGlobal{} -> return v SetupGlobalInitializer{} -> return v SetupTuple empty _ -> absurd empty + SetupSlice empty -> absurd empty where doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 11b102b4ac..84b29b9784 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -453,6 +453,8 @@ typeOfSetupValue cc env nameEnv val = SetupTuple empty _ -> absurd empty + SetupSlice empty -> + absurd empty SetupArray () [] -> throwError "typeOfSetupValue: invalid empty llvm_array_value" SetupArray () (v : vs) -> @@ -632,6 +634,8 @@ resolveSetupVal cc mem env tyenv nameEnv val = return $ Crucible.LLVMValStruct (V.zip flds (V.fromList vals)) SetupTuple empty _ -> absurd empty + SetupSlice empty -> + absurd empty SetupArray () [] -> fail "resolveSetupVal: invalid empty array" SetupArray () vs -> do vals <- V.mapM (resolveSetupVal cc mem env tyenv nameEnv) (V.fromList vs) diff --git a/src/SAWScript/Crucible/LLVM/Setup/Value.hs b/src/SAWScript/Crucible/LLVM/Setup/Value.hs index de4b0ff143..ac5baba510 100644 --- a/src/SAWScript/Crucible/LLVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/LLVM/Setup/Value.hs @@ -121,6 +121,7 @@ type instance Setup.XSetupNull (LLVM _) = () -- 'True' if this is an LLVM packed struct, 'False' otherwise. type instance Setup.XSetupStruct (LLVM _) = Bool type instance Setup.XSetupTuple (LLVM _) = Void +type instance Setup.XSetupSlice (LLVM _) = Void type instance Setup.XSetupArray (LLVM _) = () type instance Setup.XSetupElem (LLVM _) = () type instance Setup.XSetupField (LLVM _) = () diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index 3c4f0774f6..5d0592ea36 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -22,6 +22,9 @@ module SAWScript.Crucible.MIR.Builtins , mir_precond , mir_return , mir_verify + -- ** MIR slices + , mir_slice_value + , mir_slice_range_value -- ** MIR types , mir_adt , mir_array @@ -153,6 +156,21 @@ mir_alloc_internal mut mty = do st <- get let mcc = st ^. Setup.csCrucibleContext let col = mcc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection + + -- We disallow creating slice references (e.g., &[u8] or &str) using + -- mir_alloc, as it is unclear what length to give the resulting slice + -- value. + case mty of + Mir.TySlice _ -> + fail $ unlines + [ "mir_alloc and mir_alloc_mut cannot be used to create slice references." + , "Use the mir_slice_value or mir_slice_range_value functions instead." + ] + Mir.TyStr -> + fail "mir_alloc and mir_alloc_mut cannot be used to create str references." + _ -> + pure () + Some tpr <- pure $ Mir.tyToRepr col mty n <- Setup.csVarCounter <<%= MS.nextAllocIndex Setup.currentState . MS.csAllocs . at n ?= @@ -393,6 +411,18 @@ mir_verify rm nm lemmas checkSat setup tactic = ps <- io (MS.mkProvedSpec MS.SpecProved methodSpec stats vcstats lemmaSet diff) returnProof ps +----- +-- MIR slices +----- + +mir_slice_value :: MS.SetupValue MIR -> MS.SetupValue MIR +mir_slice_value arrRef = MS.SetupSlice (MirSetupSlice arrRef) + +mir_slice_range_value :: + MS.SetupValue MIR -> Int -> Int -> MS.SetupValue MIR +mir_slice_range_value arrRef start end = + MS.SetupSlice (MirSetupSliceRange arrRef start end) + ----- -- Mir.Types ----- diff --git a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs index 2fa95e2bc1..74995675b4 100644 --- a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs @@ -42,6 +42,9 @@ module SAWScript.Crucible.MIR.MethodSpecIR -- * @MIRMethodSpec@ , MIRMethodSpec + -- * @MirSetupSlice@ + , MirSetupSlice(..) + -- * Initial CrucibleSetupMethodSpec , initialDefCrucibleMethodSpecIR , initialCrucibleSetupState diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index a6f9931a16..5d957ddf68 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -22,6 +22,7 @@ import qualified Control.Exception as X import Control.Lens import Control.Monad (unless) import Control.Monad.IO.Class (MonadIO(..)) +import qualified Data.BitVector.Sized as BV import Data.Foldable (for_, traverse_) import qualified Data.Functor.Product as Functor import Data.List (tails) @@ -184,6 +185,7 @@ instantiateSetupValue sc s v = 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.SetupTuple x vs -> MS.SetupTuple x <$> mapM (instantiateSetupValue sc s) vs + MS.SetupSlice slice -> MS.SetupSlice <$> instantiateSetupSlice slice MS.SetupNull empty -> absurd empty MS.SetupGlobal _ _ -> return v MS.SetupElem _ _ _ -> return v @@ -194,6 +196,17 @@ instantiateSetupValue sc s v = where doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t + instantiateSetupSlice :: MirSetupSlice -> IO MirSetupSlice + instantiateSetupSlice (MirSetupSliceRaw ref len) = + MirSetupSliceRaw + <$> instantiateSetupValue sc s ref + <*> instantiateSetupValue sc s len + instantiateSetupSlice (MirSetupSlice arr) = + MirSetupSlice <$> instantiateSetupValue sc s arr + instantiateSetupSlice (MirSetupSliceRange arr start end) = do + arr' <- instantiateSetupValue sc s arr + pure $ MirSetupSliceRange arr' start end + -- learn pre/post condition learnCond :: Options -> @@ -383,6 +396,49 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = zs ] + -- Match the parts of a slice point-wise + (MIRVal (SliceShape _ actualElemTy actualMutbl actualElemTpr) + (Ctx.Empty Ctx.:> Crucible.RV actualRef Ctx.:> Crucible.RV actualLen), + Mir.TyRef (Mir.TySlice expectedElemTy) expectedMutbl, + MS.SetupSlice slice) -> + case slice of + MirSetupSliceRaw{} -> + panic "matchArg" ["SliceRaw not yet implemented"] + + MirSetupSlice expectedRef -> do + actualRefTy <- typeOfSetupValue cc tyenv nameEnv expectedRef + case actualRefTy of + Mir.TyRef (Mir.TyArray _ expectedLen) _ + | Just actualLenBV <- W4.asBV actualLen + , BV.asUnsigned actualLenBV == toInteger expectedLen + -> do let (actualRefShp, _actualLenShp) = + sliceShapeParts actualElemTy actualMutbl actualElemTpr + matchArg opts sc cc cs prepost md + (MIRVal actualRefShp actualRef) + (Mir.TyRef expectedElemTy expectedMutbl) + expectedRef + + _ -> fail_ + + MirSetupSliceRange expectedRef expectedStart expectedEnd + | Just actualLenBV <- W4.asBV actualLen + , BV.asUnsigned actualLenBV == toInteger (expectedEnd - expectedStart) + -> do startBV <- liftIO $ + W4.bvLit sym W4.knownNat $ + BV.mkBV W4.knownNat $ + toInteger expectedStart + actualRef' <- liftIO $ + Mir.mirRef_offsetIO bak iTypes actualElemTpr actualRef startBV + let (actualRefShp, _actualLenShp) = + sliceShapeParts actualElemTy actualMutbl actualElemTpr + matchArg opts sc cc cs prepost md + (MIRVal actualRefShp actualRef') + (Mir.TyRef expectedElemTy expectedMutbl) + expectedRef + + | otherwise + -> fail_ + (MIRVal (RefShape _ _ _ xTpr) x, Mir.TyRef _ _, MS.SetupGlobal () name) -> do static <- findStatic colState name Mir.StaticVar yGlobalVar <- findStaticVar colState (static ^. Mir.sName) @@ -409,12 +465,17 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = where colState = cc ^. mccRustModule . Mir.rmCS col = colState ^. Mir.collection + tyenv = MS.csAllocations cs + nameEnv = MS.csTypeNames cs loc = MS.conditionLoc md fail_ = failure loc =<< mkStructuralMismatch opts cc sc cs actual expected expectedTy notEq = notEqual prepost opts loc cc sc cs expected actual + iTypes :: Crucible.IntrinsicTypes Sym + iTypes = Mir.mirIntrinsicTypes + -- | For each points-to statement read the memory value through the -- given pointer (lhs) and match the value against the given pattern -- (rhs). Statements are processed in dependency order: a points-to @@ -470,6 +531,7 @@ matchPointsTos opts sc cc spec prepost = go False [] MS.SetupVar i -> Set.singleton i MS.SetupStruct _ xs -> foldMap setupVars xs MS.SetupTuple _ xs -> foldMap setupVars xs + MS.SetupSlice slice -> setupSlice slice MS.SetupArray _ xs -> foldMap setupVars xs MS.SetupElem _ x _ -> setupVars x MS.SetupField _ x _ -> setupVars x @@ -480,6 +542,15 @@ 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 'MirSetupSlice' + setupSlice :: MirSetupSlice -> Set AllocIndex + setupSlice (MirSetupSliceRaw ref len) = + setupVars ref <> setupVars len + setupSlice (MirSetupSlice arr) = + setupVars arr + setupSlice (MirSetupSliceRange arr _start _end) = + setupVars arr + matchTerm :: SharedContext {- ^ context for constructing SAW terms -} -> MIRCrucibleContext {- ^ context for interacting with Crucible -} -> diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index 1288c857c6..08568faf87 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs @@ -134,6 +134,8 @@ ppMIRVal sym (MIRVal shp val) = ppMIRVal sym $ MIRVal shp' val RefShape _ _ _ _ -> "" + SliceShape _ _ _ _ -> + "" FnPtrShape _ _ _ -> PP.viaShow val where @@ -173,6 +175,7 @@ data MIRTypeOfError | MIRInvalidTypedTerm TypedTermType | MIRInvalidIdentifier String | MIRStaticNotFound Mir.DefId + | MIRSliceNonArrayReference Mir.Ty instance Show MIRTypeOfError where show (MIRPolymorphicType s) = @@ -196,6 +199,11 @@ instance Show MIRTypeOfError where errMsg show (MIRStaticNotFound did) = staticNotFoundErr did + show (MIRSliceNonArrayReference ty) = + unlines + [ "Expected a reference to an array, but got" + , show (PP.pretty ty) + ] staticNotFoundErr :: Mir.DefId -> String staticNotFoundErr did = @@ -241,6 +249,14 @@ typeOfSetupValue mcc env nameEnv val = MS.SetupGlobalInitializer () name -> do static <- findStatic cs name pure $ static ^. Mir.sTy + MS.SetupSlice slice -> + case slice of + MirSetupSliceRaw{} -> + panic "typeOfSetupValue" ["MirSetupSliceRaw not yet implemented"] + MirSetupSlice arr -> + typeOfSliceFromArray arr + MirSetupSliceRange arr _ _ -> + typeOfSliceFromArray arr MS.SetupNull empty -> absurd empty MS.SetupElem _ _ _ -> panic "typeOfSetupValue" ["elems not yet implemented"] @@ -250,6 +266,15 @@ typeOfSetupValue mcc env nameEnv val = where cs = mcc ^. mccRustModule . Mir.rmCS + typeOfSliceFromArray :: SetupValue -> m Mir.Ty + typeOfSliceFromArray arr = do + arrTy <- typeOfSetupValue mcc env nameEnv arr + case arrTy of + Mir.TyRef (Mir.TyArray ty _) mut -> + pure $ Mir.TyRef (Mir.TySlice ty) mut + _ -> + X.throwM $ MIRSliceNonArrayReference arrTy + lookupAllocIndex :: Map AllocIndex a -> AllocIndex -> a lookupAllocIndex env i = case Map.lookup i env of @@ -266,6 +291,8 @@ resolveSetupVal :: SetupValue -> IO MIRVal resolveSetupVal mcc env tyenv nameEnv val = + mccWithBackend mcc $ \bak -> + let sym = backendGetSym bak in case val of MS.SetupVar i -> do Some ptr <- pure $ lookupAllocIndex env i @@ -334,6 +361,28 @@ resolveSetupVal mcc env tyenv nameEnv val = let (fldShpAssn, valAssn) = Ctx.unzip fldAssn let tupleShp = TupleShape (Mir.TyTuple fldMirTys) fldMirTys fldShpAssn pure $ MIRVal tupleShp valAssn + MS.SetupSlice slice -> + case slice of + MirSetupSliceRaw{} -> + panic "resolveSetupVal" ["MirSetupSliceRaw not yet implemented"] + MirSetupSlice arrRef -> do + SetupSliceFromArray _elemTpr sliceShp refVal len <- + resolveSetupSliceFromArray bak arrRef + lenVal <- usizeBvLit sym len + pure $ MIRVal sliceShp (Ctx.Empty Ctx.:> RV refVal Ctx.:> RV lenVal) + MirSetupSliceRange arrRef start end -> do + unless (start <= end) $ + fail $ "slice index starts at " ++ show start + ++ " but ends at " ++ show end + SetupSliceFromArray elemTpr sliceShp refVal0 len <- + resolveSetupSliceFromArray bak arrRef + unless (end < len) $ + fail $ "range end index " ++ show end + ++ " out of range for slice of length " ++ show len + startBV <- usizeBvLit sym start + refVal1 <- Mir.mirRef_offsetIO bak iTypes elemTpr refVal0 startBV + lenVal <- usizeBvLit sym $ end - start + pure $ MIRVal sliceShp (Ctx.Empty Ctx.:> RV refVal1 Ctx.:> RV lenVal) MS.SetupArray elemTy vs -> do vals <- V.mapM (resolveSetupVal mcc env tyenv nameEnv) (V.fromList vs) @@ -367,9 +416,40 @@ resolveSetupVal mcc env tyenv nameEnv val = static <- findStatic cs name findStaticInitializer mcc static where - sym = mcc ^. mccSym cs = mcc ^. mccRustModule . Mir.rmCS col = cs ^. Mir.collection + iTypes = Mir.mirIntrinsicTypes + + usizeBvLit :: Sym -> Int -> IO (W4.SymBV Sym Mir.SizeBits) + usizeBvLit sym = W4.bvLit sym W4.knownNat . BV.mkBV W4.knownNat . toInteger + + -- Resolve parts of a slice that are shared in common between + -- 'MirSetupSlice' and 'MirSetupSliceRange'. + resolveSetupSliceFromArray :: + OnlineSolver solver => + Backend solver -> + SetupValue -> + IO SetupSliceFromArray + resolveSetupSliceFromArray bak arrRef = do + let sym = backendGetSym bak + MIRVal arrRefShp arrRefVal <- resolveSetupVal mcc env tyenv nameEnv arrRef + case arrRefShp of + RefShape _ (Mir.TyArray elemTy len) mut (Mir.MirVectorRepr elemTpr) -> do + zeroBV <- usizeBvLit sym 0 + refVal <- Mir.subindexMirRefIO bak iTypes elemTpr arrRefVal zeroBV + let sliceShp = SliceShape (Mir.TySlice elemTy) elemTy mut elemTpr + pure $ SetupSliceFromArray elemTpr sliceShp refVal len + _ -> X.throwM $ MIRSliceNonArrayReference $ shapeMirTy arrRefShp + +-- | An intermediate data structure that is only used by +-- 'resolveSetupSliceFromArray'. +data SetupSliceFromArray where + SetupSliceFromArray :: + TypeRepr tp {- ^ The array's element type -} -> + TypeShape (Mir.MirSlice tp) {- ^ The overall shape of the slice -} -> + Mir.MirReferenceMux Sym tp {- ^ The reference to the array -} -> + Int {- ^ The array length -} -> + SetupSliceFromArray resolveTypedTerm :: MIRCrucibleContext -> @@ -618,6 +698,13 @@ equalValsPred cc mv1 mv2 = goTy (RefShape _ _ _ _) ref1 ref2 = mccWithBackend cc $ \bak -> liftIO $ Mir.mirRef_eqIO bak ref1 ref2 + goTy (SliceShape _ ty mut tpr) + (Ctx.Empty Ctx.:> RV ref1 Ctx.:> RV len1) + (Ctx.Empty Ctx.:> RV ref2 Ctx.:> RV len2) = do + let (refShp, lenShp) = sliceShapeParts ty mut tpr + refPred <- goTy refShp ref1 ref2 + lenPred <- goTy lenShp len1 len2 + liftIO $ W4.andPred sym refPred lenPred goTy (FnPtrShape _ _ _) _fh1 _fh2 = error "Function pointers not currently supported in overrides" diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs index 5c592abefb..c3c2857345 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -45,6 +45,9 @@ module SAWScript.Crucible.MIR.Setup.Value , mpMutbl , mpMirType , mpRef + + -- * @MirSetupSlice@ + , MirSetupSlice(..) ) where import Control.Lens (makeLenses) @@ -68,6 +71,7 @@ type instance MS.XSetupNull MIR = Void type instance MS.XSetupGlobal MIR = () type instance MS.XSetupStruct MIR = M.Adt type instance MS.XSetupTuple MIR = () +type instance MS.XSetupSlice MIR = MirSetupSlice -- The 'M.Ty' represents the type of array elements. type instance MS.XSetupArray MIR = M.Ty type instance MS.XSetupElem MIR = () @@ -134,6 +138,22 @@ data MirPointer sym tp = MirPointer , _mpRef :: MirReferenceMux sym tp } +-- | A slice-related MIR 'SetupValue'. +data MirSetupSlice + = MirSetupSliceRaw (MS.SetupValue MIR) (MS.SetupValue MIR) + -- ^ A \"raw\" slice constructed directly from a pointer and a length. + -- Currently, this is only used by @crucible-mir-comp@. SAWScript offers no + -- way to use this, although we may consider doing so in the future. + | MirSetupSlice (MS.SetupValue MIR) + -- ^ A slice of a reference to a contiguous sequence 'SetupValue'. + -- Currently, this only supports references to arrays. + | MirSetupSliceRange (MS.SetupValue MIR) Int Int + -- ^ A slice of a reference to a contiguous sequence 'SetupValue', where the + -- slice only covers the range specified by the given start and end values + -- (the first and second 'Int', respectively). Currently, this only + -- supports references to arrays, and it only supports concrete ranges. + deriving Show + makeLenses ''MIRCrucibleContext makeLenses ''MirAllocSpec makeLenses ''MirPointer diff --git a/src/SAWScript/Crucible/MIR/TypeShape.hs b/src/SAWScript/Crucible/MIR/TypeShape.hs index 47e845e01d..f24d372ea8 100644 --- a/src/SAWScript/Crucible/MIR/TypeShape.hs +++ b/src/SAWScript/Crucible/MIR/TypeShape.hs @@ -20,6 +20,7 @@ module SAWScript.Crucible.MIR.TypeShape , shapeToTerm , IsRefShape(..) , testRefShape + , sliceShapeParts ) where import Control.Lens ((^.), (^..), each) @@ -74,6 +75,26 @@ data TypeShape (tp :: CrucibleType) where -> TypeRepr tp -- ^ The Crucible representation of the pointee type -> TypeShape (MirReferenceType tp) + -- | A shape for a slice reference (e.g., @&[T]@), which is represented in + -- @crucible-mir@ as a 'MirSlice', i.e., a 'StructType' where the first type + -- in the struct is a reference to @T@, and the second type in the struct is + -- the length of the slice. The @crucible-mir@ representations for tuples + -- and slices are almost, but not quite, the same, as tuples can wrap their + -- fields in 'MaybeType's (see 'FieldShape') but slices never do this. + -- Nevertheless, many places in the code effectively treat tuples and slices + -- identically (modulo 'MaybeType's). + -- + -- To make it easier to recurse on the 'TypeShape's for the slice's + -- reference and length types, we provide the 'sliceShapeParts' function. + SliceShape :: M.Ty + -- ^ The type of @&[T]@. + -> M.Ty + -- ^ The type of @T@. + -> M.Mutability + -- ^ Is the reference mutable or immutable? + -> TypeRepr tp + -- ^ The Crucible representation of @T@. + -> TypeShape (MirSlice tp) -- | 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. @@ -161,22 +182,9 @@ tyToShape col = go goRef ty ty' mutbl | M.TySlice slicedTy <- ty' , Some tpr <- tyToRepr col slicedTy - = Some $ - TupleShape ty [refTy, usizeTy] - (Empty - :> ReqField (RefShape refTy slicedTy mutbl tpr) - :> ReqField (PrimShape usizeTy BaseUsizeRepr)) + = Some $ SliceShape ty slicedTy mutbl tpr | M.TyStr <- ty' - = Some $ - TupleShape ty [refTy, usizeTy] - (Empty - :> ReqField (RefShape refTy (M.TyUint M.B8) mutbl (BVRepr (knownNat @8))) - :> ReqField (PrimShape usizeTy BaseUsizeRepr)) - where - -- We use a ref (of the same mutability as `ty`) when possible, to - -- avoid unnecessary clobbering. - refTy = M.TyRef ty' mutbl - usizeTy = M.TyUint M.USize + = Some $ SliceShape ty (M.TyUint M.B8) mutbl (BVRepr (knownNat @8)) goRef ty ty' _ | isUnsized ty' = error $ "tyToShape: fat pointer " ++ show ty ++ " NYI" goRef ty ty' mutbl | Some tpr <- tyToRepr col ty' = Some $ RefShape ty ty' mutbl tpr @@ -209,6 +217,7 @@ shapeType = go go (StructShape _ _ _flds) = AnyRepr go (TransparentShape _ shp) = go shp go (RefShape _ _ _ tpr) = MirReferenceRepr tpr + go (SliceShape _ _ _ tpr) = MirSliceRepr tpr go (FnPtrShape _ args ret) = FunctionHandleRepr args ret fieldShapeType :: FieldShape tp -> TypeRepr tp @@ -223,6 +232,7 @@ shapeMirTy (ArrayShape ty _ _) = ty shapeMirTy (StructShape ty _ _) = ty shapeMirTy (TransparentShape ty _) = ty shapeMirTy (RefShape ty _ _ _) = ty +shapeMirTy (SliceShape ty _ _ _) = ty shapeMirTy (FnPtrShape ty _ _) = ty fieldShapeMirTy :: FieldShape tp -> M.Ty @@ -274,6 +284,22 @@ testRefShape shp = -> Just $ IsRefShape ty ty' mut shp' _ -> Nothing +-- | Construct the 'TypeShape's for a slice's reference and length types. +sliceShapeParts :: + M.Ty -> + M.Mutability -> + TypeRepr tp -> + (TypeShape (MirReferenceType tp), TypeShape UsizeType) +sliceShapeParts referentTy refMutbl referentTpr = + ( RefShape refTy referentTy refMutbl referentTpr + , PrimShape usizeTy BaseUsizeRepr + ) + where + -- We use a ref (of the same mutability as `ty`) when possible, to + -- avoid unnecessary clobbering. + refTy = M.TyRef referentTy refMutbl + usizeTy = M.TyUint M.USize + $(pure []) instance TestEquality TypeShape where diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 980aec8d95..299d6c6839 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3875,6 +3875,10 @@ primitives = Map.fromList , "the function expects the object to be allocated before it runs." , "After `mir_execute_func`, it states that the function being" , "verified is expected to perform the allocation." + , "" + , "This command will raise an error if a `mir_slice` or `mir_str` type is" + , "passed as an argument. To create slice reference, use the" + , "`mir_slice_value` or `mir_slice_range_value` functions instead." ] , prim "mir_alloc_mut" "MIRType -> MIRSetup MIRValue" @@ -3885,6 +3889,10 @@ primitives = Map.fromList , "the function expects the object to be allocated before it runs." , "After `mir_execute_func`, it states that the function being" , "verified is expected to perform the allocation." + , "" + , "This command will raise an error if a `mir_slice` or `mir_str` type is" + , "passed as an argument. To create slice reference, use the" + , "`mir_slice_value` or `mir_slice_range_value` functions instead." ] , prim "mir_array_value" "MIRType -> [MIRValue] -> MIRValue" @@ -3968,6 +3976,23 @@ primitives = Map.fromList , "mir_return statement is required if and only if the method" , "has a non-() return type." ] + , prim "mir_slice_value" "MIRValue -> MIRValue" + (pureVal mir_slice_value) + Experimental + [ "Create a MIRValue representing a slice. The argument must be a" + , "reference to an array value." + ] + + , prim "mir_slice_range_value" "MIRValue -> Int -> Int -> MIRValue" + (pureVal mir_slice_range_value) + Experimental + [ "Create a MIRValue representing a slice over a given range. The first" + , "argument must be a reference to an array value. The second and third" + , "arguments represent the start and end of the range. The start must not" + , "exceed the end, and the end must be strictly less than the length of the" + , "reference's array." + ] + , prim "mir_struct_value" "MIRAdt -> [MIRValue] -> MIRValue" (pureVal (CMS.SetupStruct :: Mir.Adt -> [CMS.SetupValue MIR] -> CMS.SetupValue MIR)) Experimental