diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index ba2f1ccc8b..c8effab421 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -273,8 +273,8 @@ addArg tpr argRef msb = , MS.conditionType = "add argument value" , MS.conditionContext = "" } - msbSpec . MS.csPreState . MS.csPointsTos %= (MirPointsTo md (fr ^. frAlloc) svs :) - msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (fr ^. frAlloc) svs' :) + msbSpec . MS.csPreState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs :) + msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs' :) msbSpec . MS.csArgBindings . at (fromIntegral idx) .= Just (ty, sv) where @@ -318,7 +318,7 @@ setReturn tpr argRef msb = , MS.conditionType = "set return value" , MS.conditionContext = "" } - msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (fr ^. frAlloc) svs :) + msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs :) msbSpec . MS.csRetValue .= Just sv where diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index 831700f8b8..73e8623d2e 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -208,7 +208,8 @@ runSpec cs mh ms = ovrWithBackend $ \bak -> -- to allocation `alloc` before we see the PointsTo for `alloc` itself. -- This ensures we can obtain a MirReference for each PointsTo that we -- see. - forM_ (reverse $ ms ^. MS.csPreState . MS.csPointsTos) $ \(MirPointsTo md alloc svs) -> do + forM_ (reverse $ ms ^. MS.csPreState . MS.csPointsTos) $ \(MirPointsTo md ref svs) -> do + alloc <- setupVarAllocIndex ref allocSub <- use MS.setupValueSub Some ptr <- case Map.lookup alloc allocSub of Just x -> return x @@ -311,7 +312,8 @@ runSpec cs mh ms = ovrWithBackend $ \bak -> -- figuring out which memory is accessible and mutable and thus needs to be -- clobbered, and for adding appropriate fresh variables and `PointsTo`s to -- the post state. - forM_ (ms ^. MS.csPostState . MS.csPointsTos) $ \(MirPointsTo _md alloc svs) -> do + forM_ (ms ^. MS.csPostState . MS.csPointsTos) $ \(MirPointsTo _md ref svs) -> do + alloc <- setupVarAllocIndex ref Some ptr <- case Map.lookup alloc allocMap of Just x -> return x Nothing -> error $ "post PointsTos are out of order: no ref for " ++ show alloc @@ -589,3 +591,20 @@ checkDisjoint bak refs = go refs assert bak disjoint $ GenericSimError $ "references " ++ show alloc ++ " and " ++ show alloc' ++ " must not overlap" go rest + +-- | Take a 'MS.SetupValue' that is assumed to be a bare 'MS.SetupVar' and +-- extract the underlying 'MS.AllocIndex'. If this assumption does not hold, +-- this function will raise an error. +-- +-- This is used in conjunction with 'MirPointsTo' values. With the way that +-- @crucible-mir-comp@ is currently set up, the only sort of 'MS.SetupValue' +-- that will be put into a 'MirPointsTo' value's left-hand side is a +-- 'MS.SetupVar', so we can safely use this function on such 'MS.SetupValue's. +-- Other parts of SAW can break this assumption (e.g., if you wrote something +-- like @mir_points_to (mir_static "X") ...@ in a SAW specification), but these +-- parts of SAW are not used in @crucible-mir-comp@. +setupVarAllocIndex :: Applicative m => MS.SetupValue MIR -> m MS.AllocIndex +setupVarAllocIndex (MS.SetupVar idx) = pure idx +setupVarAllocIndex val = + error $ "setupVarAllocIndex: Expected SetupVar, received: " + ++ show (MS.ppSetupValue val) diff --git a/doc/manual/manual.md b/doc/manual/manual.md index c2e79b6dc1..1d0de3c9da 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -2788,6 +2788,10 @@ them. ## Global variables +SAW supports verifying LLVM and MIR specifications involving global variables. + +### LLVM global variables + Mutable global variables that are accessed in a function must first be allocated by calling `llvm_alloc_global` on the name of the global. @@ -2892,6 +2896,68 @@ point of a call to `f`. This specification also constrains `y` to prevent signed integer overflow resulting from the `x + y` expression in `f`, which is undefined behavior in C. +### MIR static items + +Rust's static items are the MIR version of global variables. A reference to a +static item can be accessed with the `mir_static` function. This function takes +a `String` representing a static item's identifier, and this identifier is +expected to adhere to the naming conventions outlined in the "Running a +MIR-based verification" section: + +* `mir_static : String -> MIRValue` + +References to static values can be initialized with the `mir_points_to` +command, just like with other forms of references. Immutable static items +(e.g., `static X: u8 = 42`) are initialized implicitly in every SAW +specification, so there is no need for users to do so manually. Mutable static +items (e.g., `static mut Y: u8 = 27`), on the other hand, are *not* initialized +implicitly, and users must explicitly pick a value to initialize them with. + +The `mir_static_initializer` function can be used to access the initial value +of a static item in a MIR program. Like with `mir_static`, the `String` +supplied as an argument must be a valid identifier: + +* `mir_static_initializer : String -> MIRValue`. + +As an example of how to use these functions, here is a Rust program involving +static items: + +~~~ .rs +// statics.rs +static S1: u8 = 1; +static mut S2: u8 = 2; + +pub fn f() -> u8 { + // Reading a mutable static item requires an `unsafe` block due to + // concurrency-related concerns. We are only concerned about the behavior + // of this program in a single-threaded context, so this is fine. + let s2 = unsafe { S2 }; + S1 + s2 +} +~~~ + +We can write a specification for `f` like so: + +~~~ +// statics.saw +enable_experimental; + +let f_spec = do { + mir_points_to (mir_static "statics::S2") + (mir_static_initializer "statics::S2"); + // Note that we do not initialize S1, as immutable static items are implicitly + // initialized in every specification. + + mir_execute_func []; + + mir_return (mir_term {{ 3 : [8] }}); +}; + +m <- mir_load_module "statics.linked-mir.json"; + +mir_verify m "statics::f" [] false f_spec z3; +~~~ + ## Preconditions and Postconditions Sometimes a function is only well-defined under certain conditions, or diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index bc02e7609a..de9ccf68b8 100644 Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ diff --git a/intTests/test_mir_statics/Makefile b/intTests/test_mir_statics/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_statics/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_statics/test.linked-mir.json b/intTests/test_mir_statics/test.linked-mir.json new file mode 100644 index 0000000000..27457cc056 --- /dev/null +++ b/intTests/test_mir_statics/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:2:22: 2:23","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:2:1: 2:24"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"test/03613d74::S2","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::u32"}},"pos":"test.rs:3:22: 3:23","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"3"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:3:1: 3:24"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"test/03613d74::S3","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::u32"}},"pos":"test.rs:1:22: 1:23","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:1:1: 1:24"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"test/03613d74::S1","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":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:18:6: 18:8","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/03613d74::S2","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:18:5: 18:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:19:2: 19:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/03613d74::f2","return_ty":"ty::Ref::e028c0f25e8b6323","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::944607c7a6d1ed60"},"kind":"Constant"},"kind":"Call","pos":"test.rs:14:6: 14:14"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:14:5: 14:14","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:15:2: 15:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/03613d74::f1","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":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:10:6: 10:8","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/03613d74::S1","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:10:5: 10:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:11:2: 11:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/03613d74::f1_aux","return_ty":"ty::Ref::e028c0f25e8b6323","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:23:14: 23:16","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/03613d74::S3","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:23:14: 23:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:23:14: 23:32"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:23:9: 23:11","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/03613d74::S3","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:23:9: 23:32","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:24:9: 24:11","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/03613d74::S3","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:24:9: 24:11","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:26:2: 26:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::63e5937014067f41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::63e5937014067f41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::RawPtr::63e5937014067f41"}]},"name":"test/03613d74::f3","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"test.rs:29:18: 29:19","rhs":{"kind":"AddressOf","mutbl":{"kind":"Not"},"place":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:29:22: 29:24","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/03613d74::S1","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:29:21: 29:24","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"test.rs:29:21: 29:24","rhs":{"kind":"AddressOf","mutbl":{"kind":"Not"},"place":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"}}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::1cc207ca586a46de"},"kind":"Constant"},"kind":"Call","pos":"test.rs:29:5: 29:25"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:30:2: 30:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/03613d74::g","return_ty":"ty::bool","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:13: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1163:10: 1163:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}]},"name":"core/73237d41::num::{impl#9}::wrapping_add","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:5: 1828:6","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:5: 1828:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:10: 1828:11","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::1f2b1eadb40cd255"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:10: 1828:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:5: 1828:11","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Eq"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:10: 1828:11","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::1f2b1eadb40cd255"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:10: 1828:11","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1829:2: 1829:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::1f2b1eadb40cd255"}]},"name":"core/73237d41::ptr::eq::_instc5e93708b8ca6e2a[0]","return_ty":"ty::bool","spread_arg":null}],"adts":[],"statics":[{"kind":"body","mutable":false,"name":"test/03613d74::S2","ty":"ty::u32"},{"kind":"body","mutable":true,"name":"test/03613d74::S3","ty":"ty::u32"},{"kind":"body","mutable":false,"name":"test/03613d74::S1","ty":"ty::u32"}],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/03613d74::f2","kind":"Item","substs":[]},"name":"test/03613d74::f2"},{"inst":{"def_id":"test/03613d74::f1","kind":"Item","substs":[]},"name":"test/03613d74::f1"},{"inst":{"def_id":"test/03613d74::f1_aux","kind":"Item","substs":[]},"name":"test/03613d74::f1_aux"},{"inst":{"def_id":"test/03613d74::f3","kind":"Item","substs":[]},"name":"test/03613d74::f3"},{"inst":{"def_id":"test/03613d74::g","kind":"Item","substs":[]},"name":"test/03613d74::g"},{"inst":{"def_id":"core/73237d41::num::{impl#9}::wrapping_add","kind":"Item","substs":[]},"name":"core/73237d41::num::{impl#9}::wrapping_add"},{"inst":{"def_id":"core/73237d41::ptr::eq","kind":"Item","substs":["ty::u32"]},"name":"core/73237d41::ptr::eq::_instc5e93708b8ca6e2a[0]"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"name":"ty::FnDef::944607c7a6d1ed60","ty":{"defid":"test/03613d74::f1_aux","kind":"FnDef"}},{"name":"ty::RawPtr::63e5937014067f41","ty":{"kind":"RawPtr","mutability":{"kind":"Mut"},"ty":"ty::u32"}},{"name":"ty::FnDef::f55acdef755f1aaa","ty":{"defid":"core/73237d41::num::{impl#9}::wrapping_add","kind":"FnDef"}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::RawPtr::1f2b1eadb40cd255","ty":{"kind":"RawPtr","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"name":"ty::FnDef::1cc207ca586a46de","ty":{"defid":"core/73237d41::ptr::eq::_instc5e93708b8ca6e2a[0]","kind":"FnDef"}}],"roots":["test/03613d74::f1_aux","test/03613d74::f1","test/03613d74::f2","test/03613d74::f3","test/03613d74::g"]} \ No newline at end of file diff --git a/intTests/test_mir_statics/test.rs b/intTests/test_mir_statics/test.rs new file mode 100644 index 0000000000..6b8bdf2f5e --- /dev/null +++ b/intTests/test_mir_statics/test.rs @@ -0,0 +1,30 @@ +static S1: u32 = 1; +static S2: u32 = 2; +static mut S3: u32 = 3; + +// rustc is very eager to inline immutable, top-level static values, even on the +// lowest optimization settings. To ensure that S1 isn't inlined, we must +// introduce this extra layer of indirection. +#[inline(never)] +pub fn f1_aux() -> &'static u32 { + &S1 +} + +pub fn f1() -> u32 { + *f1_aux() +} + +pub fn f2() -> &'static u32 { + &S2 +} + +pub fn f3() -> u32 { + unsafe { + S3 = S3.wrapping_add(1); + S3 + } +} + +pub fn g(r: &u32) -> bool { + std::ptr::eq(r, &S1) +} diff --git a/intTests/test_mir_statics/test.saw b/intTests/test_mir_statics/test.saw new file mode 100644 index 0000000000..4b38830c55 --- /dev/null +++ b/intTests/test_mir_statics/test.saw @@ -0,0 +1,115 @@ +enable_experimental; + +// A basic spec that uses the initial value of S1. +let f1_spec = do { + mir_execute_func []; + + mir_return (mir_static_initializer "test::S1"); +}; + +// An alternative spec that uses a different initial value for S1. +let f1_alt_spec = do { + let s1_static = mir_static "test::S1"; + let init = mir_term {{ 42 : [32] }}; + mir_points_to s1_static init; + + mir_execute_func []; + + mir_points_to s1_static init; + mir_return init; +}; + +// A buggy spec that refers to a non-existent static initializer value. +let f1_fail_spec = do { + mir_execute_func []; + + mir_return (mir_static_initializer "test::S1_fake"); +}; + +// A buggy spec that refers to a non-existent static value. +let f1_fail_alt_spec = do { + let s1_static = mir_static "test::S1_fake"; + let init = mir_term {{ 42 : [32] }}; + mir_points_to s1_static init; + + mir_execute_func []; + + mir_points_to s1_static init; + mir_return init; +}; + +// A spec that matches against a static in the return value. +let f2_spec = do { + mir_execute_func []; + + mir_return (mir_static "test::S2"); +}; + +// A basic spec that uses the initial value of S3. +let f3_spec = do { + let s3_static = mir_static "test::S3"; + mir_points_to s3_static (mir_static_initializer "test::S3"); + + mir_execute_func []; + + let ret = mir_term {{ 4 : [32] }}; + mir_points_to s3_static ret; + mir_return ret; +}; + +// An alternative spec that uses a different initial value for S3. +let f3_alt_spec = do { + let s3_static = mir_static "test::S3"; + let init = {{ 42 : [32] }}; + mir_points_to s3_static (mir_term init); + + mir_execute_func []; + + let ret = mir_term {{ init + 1 }}; + mir_points_to s3_static ret; + mir_return ret; +}; + +// A buggy spec that does not initialize S3 (a mutable static value). +let f3_fail_spec = do { + mir_execute_func []; + + mir_return (mir_term {{ 4 : [32] }}); +}; + +// A spec that ensures that fresh allocations do not alias with static +// references. +let g_spec = do { + r_ref <- mir_alloc mir_u32; + + mir_execute_func [r_ref]; + + mir_return (mir_term {{ False }}); +}; + +// g(&S1) should return True. +let g_alt_spec = do { + mir_execute_func [mir_static "test::S1"]; + + mir_return (mir_term {{ True }}); +}; + +m <- mir_load_module "test.linked-mir.json"; + +mir_verify m "test::f1" [] false f1_spec z3; +mir_verify m "test::f1" [] false f1_alt_spec z3; +mir_verify m "test::f2" [] false f2_spec z3; +mir_verify m "test::f3" [] false f3_spec z3; +mir_verify m "test::f3" [] false f3_alt_spec z3; +mir_verify m "test::g" [] false g_spec z3; +mir_verify m "test::g" [] false g_alt_spec z3; + +fails ( + mir_verify m "test::f1" [] false f1_fail_spec z3 +); +fails ( + mir_verify m "test::f1" [] false f1_fail_alt_spec z3 +); +fails ( + mir_verify m "test::f3" [] false f3_fail_spec z3 +); diff --git a/intTests/test_mir_statics/test.sh b/intTests/test_mir_statics/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_statics/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/python/tests/saw/test-files/Makefile b/saw-remote-api/python/tests/saw/test-files/Makefile index acb9f97702..6067fee257 100644 --- a/saw-remote-api/python/tests/saw/test-files/Makefile +++ b/saw-remote-api/python/tests/saw/test-files/Makefile @@ -1,6 +1,7 @@ C_FILES := $(wildcard *.c) BC_FILES := $(C_FILES:.c=.bc) RS_FILES := $(wildcard *.rs) +EXE_FILES := $(RS_FILES:.rs=) JSON_FILES := $(RS_FILES:.rs=.linked-mir.json) all: $(BC_FILES) $(JSON_FILES) @@ -10,7 +11,12 @@ all: $(BC_FILES) $(JSON_FILES) %.linked-mir.json: %.rs saw-rustc $< + $(MAKE) remove-unused-build-artifacts # This test case crucially relies on the use of -O2. llvm_lax_pointer_ordering.bc: llvm_lax_pointer_ordering.c clang -O2 -g -c -emit-llvm -o $@ $< + +PHONY: remove-unused-build-artifacts +remove-unused-build-artifacts: + rm -f test lib*.mir lib*.rlib $(EXE_FILES) diff --git a/saw-remote-api/python/tests/saw/test-files/mir_statics.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/mir_statics.linked-mir.json new file mode 100644 index 0000000000..6bafcfd26a --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_statics.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"mir_statics.rs:2:22: 2:23","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"mir_statics.rs:2:1: 2:24"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"mir_statics/f6d6b500::S2","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::u32"}},"pos":"mir_statics.rs:3:22: 3:23","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"3"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"mir_statics.rs:3:1: 3:24"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"mir_statics/f6d6b500::S3","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::u32"}},"pos":"mir_statics.rs:1:22: 1:23","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"mir_statics.rs:1:1: 1:24"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"mir_statics/f6d6b500::S1","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::d1a77fa11fa71149"},"kind":"Constant"},"kind":"Call","pos":"mir_statics.rs:14:6: 14:14"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"mir_statics.rs:14:5: 14:14","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"mir_statics.rs:15:2: 15:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"mir_statics/f6d6b500::f1","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":"_3","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"mir_statics.rs:23:14: 23:16","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_statics/f6d6b500::S3","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"mir_statics.rs:23:14: 23:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"mir_statics.rs:23:14: 23:32"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"mir_statics.rs:23:9: 23:11","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_statics/f6d6b500::S3","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"mir_statics.rs:23:9: 23:32","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"mir_statics.rs:24:9: 24:11","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_statics/f6d6b500::S3","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"mir_statics.rs:24:9: 24:11","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"mir_statics.rs:26:2: 26:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::63e5937014067f41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::63e5937014067f41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::RawPtr::63e5937014067f41"}]},"name":"mir_statics/f6d6b500::f3","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":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_statics.rs:18:6: 18:8","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_statics/f6d6b500::S2","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_statics.rs:18:5: 18:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"mir_statics.rs:19:2: 19:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"mir_statics/f6d6b500::f2","return_ty":"ty::Ref::e028c0f25e8b6323","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"mir_statics.rs:29:18: 29:19","rhs":{"kind":"AddressOf","mutbl":{"kind":"Not"},"place":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_statics.rs:29:22: 29:24","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_statics/f6d6b500::S1","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_statics.rs:29:21: 29:24","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"mir_statics.rs:29:21: 29:24","rhs":{"kind":"AddressOf","mutbl":{"kind":"Not"},"place":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"}}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::1cc207ca586a46de"},"kind":"Constant"},"kind":"Call","pos":"mir_statics.rs:29:5: 29:25"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_statics.rs:30:2: 30:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"mir_statics/f6d6b500::g","return_ty":"ty::bool","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_statics.rs:10:6: 10:8","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_statics/f6d6b500::S1","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_statics.rs:10:5: 10:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"mir_statics.rs:11:2: 11:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"mir_statics/f6d6b500::f1_aux","return_ty":"ty::Ref::e028c0f25e8b6323","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:13: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1163:10: 1163:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}]},"name":"core/73237d41::num::{impl#9}::wrapping_add","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:5: 1828:6","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:5: 1828:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:10: 1828:11","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::1f2b1eadb40cd255"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:10: 1828:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:5: 1828:11","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Eq"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:10: 1828:11","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::1f2b1eadb40cd255"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1828:10: 1828:11","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/ptr/mod.rs:1829:2: 1829:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::RawPtr::1f2b1eadb40cd255"}]},"name":"core/73237d41::ptr::eq::_instc5e93708b8ca6e2a[0]","return_ty":"ty::bool","spread_arg":null}],"adts":[],"statics":[{"kind":"body","mutable":false,"name":"mir_statics/f6d6b500::S2","ty":"ty::u32"},{"kind":"body","mutable":true,"name":"mir_statics/f6d6b500::S3","ty":"ty::u32"},{"kind":"body","mutable":false,"name":"mir_statics/f6d6b500::S1","ty":"ty::u32"}],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"mir_statics/f6d6b500::f1","kind":"Item","substs":[]},"name":"mir_statics/f6d6b500::f1"},{"inst":{"def_id":"mir_statics/f6d6b500::f3","kind":"Item","substs":[]},"name":"mir_statics/f6d6b500::f3"},{"inst":{"def_id":"mir_statics/f6d6b500::f2","kind":"Item","substs":[]},"name":"mir_statics/f6d6b500::f2"},{"inst":{"def_id":"mir_statics/f6d6b500::g","kind":"Item","substs":[]},"name":"mir_statics/f6d6b500::g"},{"inst":{"def_id":"mir_statics/f6d6b500::f1_aux","kind":"Item","substs":[]},"name":"mir_statics/f6d6b500::f1_aux"},{"inst":{"def_id":"core/73237d41::num::{impl#9}::wrapping_add","kind":"Item","substs":[]},"name":"core/73237d41::num::{impl#9}::wrapping_add"},{"inst":{"def_id":"core/73237d41::ptr::eq","kind":"Item","substs":["ty::u32"]},"name":"core/73237d41::ptr::eq::_instc5e93708b8ca6e2a[0]"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"name":"ty::FnDef::d1a77fa11fa71149","ty":{"defid":"mir_statics/f6d6b500::f1_aux","kind":"FnDef"}},{"name":"ty::RawPtr::63e5937014067f41","ty":{"kind":"RawPtr","mutability":{"kind":"Mut"},"ty":"ty::u32"}},{"name":"ty::FnDef::f55acdef755f1aaa","ty":{"defid":"core/73237d41::num::{impl#9}::wrapping_add","kind":"FnDef"}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::RawPtr::1f2b1eadb40cd255","ty":{"kind":"RawPtr","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"name":"ty::FnDef::1cc207ca586a46de","ty":{"defid":"core/73237d41::ptr::eq::_instc5e93708b8ca6e2a[0]","kind":"FnDef"}}],"roots":["mir_statics/f6d6b500::f1_aux","mir_statics/f6d6b500::f1","mir_statics/f6d6b500::f2","mir_statics/f6d6b500::f3","mir_statics/f6d6b500::g"]} \ No newline at end of file diff --git a/saw-remote-api/python/tests/saw/test-files/mir_statics.rs b/saw-remote-api/python/tests/saw/test-files/mir_statics.rs new file mode 100644 index 0000000000..6b8bdf2f5e --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_statics.rs @@ -0,0 +1,30 @@ +static S1: u32 = 1; +static S2: u32 = 2; +static mut S3: u32 = 3; + +// rustc is very eager to inline immutable, top-level static values, even on the +// lowest optimization settings. To ensure that S1 isn't inlined, we must +// introduce this extra layer of indirection. +#[inline(never)] +pub fn f1_aux() -> &'static u32 { + &S1 +} + +pub fn f1() -> u32 { + *f1_aux() +} + +pub fn f2() -> &'static u32 { + &S2 +} + +pub fn f3() -> u32 { + unsafe { + S3 = S3.wrapping_add(1); + S3 + } +} + +pub fn g(r: &u32) -> bool { + std::ptr::eq(r, &S1) +} diff --git a/saw-remote-api/python/tests/saw/test_mir_statics.py b/saw-remote-api/python/tests/saw/test_mir_statics.py new file mode 100644 index 0000000000..fa739cf6f1 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_mir_statics.py @@ -0,0 +1,106 @@ +import unittest +from pathlib import Path + +from saw_client import * +from saw_client.crucible import cry, cry_f, global_var, global_initializer +from saw_client.mir import Contract, u32 + + +class F1Contract(Contract): + def specification(self) -> None: + self.execute_func() + + self.returns(global_initializer('mir_statics::S1')) + + +class F1AltContract(Contract): + def specification(self) -> None: + s1_static = global_var('mir_statics::S1') + init = cry_f('42 : [32]') + self.points_to(s1_static, init) + + self.execute_func() + + self.points_to(s1_static, init) + self.returns(init) + + +class F2Contract(Contract): + def specification(self) -> None: + self.execute_func() + + self.returns(global_var('mir_statics::S2')) + + +class F3Contract(Contract): + def specification(self) -> None: + s3_static = global_var('mir_statics::S3') + self.points_to(s3_static, global_initializer('mir_statics::S3')) + + self.execute_func() + + ret = cry_f('4 : [32]') + self.points_to(s3_static, ret) + self.returns(ret) + + +class F3AltContract(Contract): + def specification(self) -> None: + s3_static = global_var('mir_statics::S3') + init = cry_f('42 : [32]') + self.points_to(s3_static, init) + + self.execute_func() + + ret = cry_f('{init} + 1 : [32]') + self.points_to(s3_static, ret) + self.returns(ret) + + +class GContract(Contract): + def specification(self) -> None: + r_ref = self.alloc(u32, read_only = True) + + self.execute_func(r_ref) + + self.returns(cry_f('False')) + + +class GAltContract(Contract): + def specification(self) -> None: + self.execute_func(global_var('mir_statics::S1')) + + self.returns(cry_f('True')) + + +class MIRStaticsTest(unittest.TestCase): + def test_mir_statics(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults()) + json_name = str(Path('tests', 'saw', 'test-files', 'mir_statics.linked-mir.json')) + mod = mir_load_module(json_name) + + f1_result = mir_verify(mod, 'mir_statics::f1', F1Contract()) + self.assertIs(f1_result.is_success(), True) + + f1_alt_result = mir_verify(mod, 'mir_statics::f1', F1AltContract()) + self.assertIs(f1_alt_result.is_success(), True) + + f2_result = mir_verify(mod, 'mir_statics::f2', F2Contract()) + self.assertIs(f2_result.is_success(), True) + + f3_result = mir_verify(mod, 'mir_statics::f3', F3Contract()) + self.assertIs(f3_result.is_success(), True) + + f3_alt_result = mir_verify(mod, 'mir_statics::f3', F3AltContract()) + self.assertIs(f3_alt_result.is_success(), True) + + g_result = mir_verify(mod, 'mir_statics::g', GContract()) + self.assertIs(g_result.is_success(), True) + + g_alt_result = mir_verify(mod, 'mir_statics::g', GAltContract()) + self.assertIs(g_alt_result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs index 1db52e72fc..e2b5942741 100644 --- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs @@ -196,6 +196,10 @@ compileMIRContract fileReader bic cenv0 sawenv c = getSetupVal env (TupleValue elems) = do elems' <- mapM (getSetupVal env) elems pure $ MS.SetupTuple () elems' + getSetupVal _ (GlobalInitializer name) = + pure $ MS.SetupGlobalInitializer () name + getSetupVal _ (GlobalLValue name) = + pure $ MS.SetupGlobal () name getSetupVal _ (FieldLValue _ _) = MIRSetupM $ fail "Field l-values unsupported in the MIR API." getSetupVal _ (CastLValue _ _) = @@ -204,10 +208,6 @@ compileMIRContract fileReader bic cenv0 sawenv c = MIRSetupM $ fail "Union l-values unsupported in the MIR API." getSetupVal _ (ElementLValue _ _) = MIRSetupM $ fail "Element l-values unsupported in the MIR API." - getSetupVal _ (GlobalInitializer _) = - MIRSetupM $ fail "Global initializers unsupported in the MIR API." - getSetupVal _ (GlobalLValue _) = - MIRSetupM $ fail "Global l-values unsupported in the MIR API." data MIRLoadModuleParams = MIRLoadModuleParams ServerName FilePath diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index 25c6e1d9e8..3c4f0774f6 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -2,6 +2,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} @@ -56,21 +57,21 @@ import Control.Monad.State (MonadState(..), StateT(..), execStateT, gets) import Control.Monad.Trans.Class (MonadTrans(..)) import qualified Data.BitVector.Sized as BV import qualified Data.ByteString.Lazy as BSL -import qualified Data.Foldable as F import Data.Foldable (for_) import Data.IORef import qualified Data.List.Extra as List (find, groupOn) -import Data.List.NonEmpty (NonEmpty(..)) import qualified Data.Map as Map import Data.Map (Map) import Data.Maybe (fromMaybe) 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.Set as Set import qualified Data.Text as Text import Data.Text (Text) import Data.Time.Clock (diffUTCTime, getCurrentTime) +import Data.Traversable (mapAccumL) import Data.Type.Equality (TestEquality(..)) import Data.Void (absurd) import qualified Prettyprinter as PP @@ -81,8 +82,10 @@ import qualified Cryptol.TypeCheck.Type as Cryptol import qualified Lang.Crucible.Analysis.Postdom as Crucible import qualified Lang.Crucible.Backend as Crucible import qualified Lang.Crucible.CFG.Core as Crucible +import qualified Lang.Crucible.CFG.Extension as Crucible import qualified Lang.Crucible.FunctionHandle as Crucible import qualified Lang.Crucible.Simulator as Crucible +import qualified Lang.Crucible.Simulator.GlobalState as Crucible import qualified Lang.Crucible.Simulator.SimError as Crucible import qualified Mir.DefId as Mir @@ -91,8 +94,8 @@ import qualified Mir.Generator as Mir import Mir.Intrinsics (MIR) import qualified Mir.Intrinsics as Mir import qualified Mir.ParseTranslate as Mir -import qualified Mir.Trans as Mir import Mir.TransCustom (customOps) +import qualified Mir.Trans as Mir import qualified Mir.TransTy as Mir import qualified What4.Config as W4 @@ -129,10 +132,9 @@ type MethodSpec = MS.CrucibleMethodSpecIR MIR type SetupCondition = MS.SetupCondition MIR -- TODO: something useful with the global pair? -ppMIRAbortedResult :: MIRCrucibleContext - -> Crucible.AbortedResult Sym a +ppMIRAbortedResult :: Crucible.AbortedResult Sym a -> PP.Doc ann -ppMIRAbortedResult _cc = ppAbortedResult (\_gp -> mempty) +ppMIRAbortedResult = ppAbortedResult (\_gp -> mempty) ----- -- Commands @@ -218,15 +220,11 @@ mir_load_module inputFile = do b <- io $ BSL.readFile inputFile opts <- getOptions - let ?debug = simVerbose opts - -- For now, we use the same default settings for implicit parameters as in - -- crux-mir. We may want to add options later that allow configuring these. - let ?assertFalseOnError = True - let ?printCrucible = False - halloc <- getHandleAlloc - col <- io $ Mir.parseMIR inputFile b - io $ Mir.translateMIR mempty col halloc + + withImplicitParams opts $ do + col <- io $ Mir.parseMIR inputFile b + io $ Mir.translateMIR mempty col halloc mir_return :: SetupValue -> MIRSetupM () mir_return retVal = @@ -279,11 +277,6 @@ mir_points_to ref val = let env = MS.csAllocations (st ^. Setup.csMethodSpec) nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec) - allocIdx <- - case ref of - MS.SetupVar idx -> pure idx - _ -> X.throwM $ MIRPointsToNonReference ref - referentTy <- mir_points_to_check_lhs_validity ref loc valTy <- typeOfSetupValue cc env nameEnv val unless (checkCompatibleTys referentTy valTy) $ @@ -300,7 +293,7 @@ mir_points_to ref val = , MS.conditionType = "MIR points-to" , MS.conditionContext = "" } - Setup.addPointsTo (MirPointsTo md allocIdx [val]) + Setup.addPointsTo (MirPointsTo md ref [val]) -- | Perform a set of validity checks on the LHS reference value in a -- 'mir_points_to' command. In particular: @@ -320,7 +313,8 @@ mir_points_to_check_lhs_validity ref loc = refTy <- typeOfSetupValue cc env nameEnv ref case refTy of Mir.TyRef referentTy _ -> pure referentTy - _ -> throwCrucibleSetup loc $ "lhs not a reference type: " ++ show refTy + _ -> throwCrucibleSetup loc $ "lhs not a reference type: " + ++ show (PP.pretty refTy) mir_verify :: Mir.RustModule -> @@ -340,6 +334,7 @@ mir_verify rm nm lemmas checkSat setup tactic = cc <- setupCrucibleContext rm SomeOnlineBackend bak <- pure (cc^.mccBackend) let sym = cc^.mccSym + let globals0 = cc^.mccSymGlobalState pos <- getPosition let loc = SS.toW4Loc "_SAW_verify_prestate" pos @@ -367,7 +362,7 @@ mir_verify rm nm lemmas checkSat setup tactic = unwords ["Verifying", show (methodSpec ^. MS.csMethod), "..."] -- construct the initial state for verifications - (args, assumes, env, globals1) <- io $ verifyPrestate cc methodSpec Crucible.emptyGlobals + (args, assumes, env, globals1) <- io $ verifyPrestate cc methodSpec globals0 -- save initial path conditions frameIdent <- io $ Crucible.pushAssumptionFrame bak @@ -558,25 +553,37 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts Crucible.SymGlobalState Sym -> MirPointsTo -> IO (Crucible.SymGlobalState Sym) - doPointsTo globals (MirPointsTo _ allocIdx referents) = + doPointsTo globals (MirPointsTo _ reference referents) = mccWithBackend cc $ \bak -> do + MIRVal referenceShp referenceVal <- + resolveSetupVal cc env tyenv nameEnv reference + -- By the time we reach here, we have already checked (in mir_points_to) + -- that we are in fact dealing with a reference value, so the call to + -- `testRefShape` below should always succeed. + IsRefShape _ _ _ referenceInnerTy <- + case testRefShape referenceShp of + Just irs -> pure irs + Nothing -> + panic "setupPrePointsTos" + [ "Unexpected non-reference type:" + , show $ PP.pretty $ shapeMirTy referenceShp + ] referent <- firstPointsToReferent referents - MIRVal referentTy referentVal <- + MIRVal referentShp referentVal <- resolveSetupVal cc env tyenv nameEnv referent - Some mp <- pure $ lookupAllocIndex env allocIdx -- By the time we reach here, we have already checked (in mir_points_to) -- that the type of the reference is compatible with the right-hand side -- value, so the equality check below should never fail. Refl <- - case W4.testEquality (mp^.mpType) (shapeType referentTy) of + case W4.testEquality referenceInnerTy (shapeType referentShp) of Just r -> pure r Nothing -> panic "setupPrePointsTos" [ "Unexpected type mismatch between reference and referent" - , "Reference type: " ++ show (mp^.mpType) - , "Referent type: " ++ show (shapeType referentTy) + , "Reference type: " ++ show referenceInnerTy + , "Referent type: " ++ show (shapeType referentShp) ] - Mir.writeMirRefIO bak globals Mir.mirIntrinsicTypes (mp^.mpRef) referentVal + Mir.writeMirRefIO bak globals Mir.mirIntrinsicTypes referenceVal referentVal -- | Collects boolean terms that should be assumed to be true. setupPrestateConditions :: @@ -822,28 +829,15 @@ verifySimulate :: verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat mdMap = mccWithBackend cc $ \bak -> do let rm = cc^.mccRustModule - let cfgMap = rm ^. Mir.rmCFGs let cs = rm ^. Mir.rmCS let col = cs ^. Mir.collection let method = mspec ^. MS.csMethod let verbosity = simVerbose opts - let halloc = cc^.mccHandleAllocator + let simctx = cc^.mccSimContext when (verbosity > 2) $ putStrLn "starting executeCrucibleMIR" - -- Translate the static initializer function - let ?debug = simVerbose opts - -- For now, we use the same default settings for implicit parameters as in - -- crux-mir. We may want to add options later that allow configuring these. - let ?assertFalseOnError = True - let ?customOps = customOps - Crucible.AnyCFG staticInitCfg <- Mir.transStatics cs halloc - let staticInitHndl = Crucible.cfgHandle staticInitCfg - Refl <- case testEquality (Crucible.handleArgTypes staticInitHndl) Ctx.Empty of - Just e -> pure e - Nothing -> fail "mir_verify: static initializer should not require arguments" - -- Find and run the target function Crucible.AnyCFG methodCfg <- lookupDefIdCFG rm method let methodHndl = Crucible.cfgHandle methodCfg @@ -851,20 +845,11 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat m let methodRetTy = Crucible.handleReturnType methodHndl regmap <- prepareArgs methodArgTys (map snd args) - res <- + (_, Crucible.GlobalPair retval globals1) <- do let feats = pfs - let simctx = Crucible.initSimContext bak Mir.mirIntrinsicTypes halloc stdout - (Crucible.FnBindings Crucible.emptyHandleMap) Mir.mirExtImpl - SAWCruciblePersonality - let simSt = Crucible.InitialState simctx globals Crucible.defaultAbortHandler methodRetTy let fnCall = Crucible.regValue <$> Crucible.callCFG methodCfg regmap let overrideSim = - do forM_ cfgMap $ \(Crucible.AnyCFG cfg) -> - Crucible.bindFnHandle (Crucible.cfgHandle cfg) $ - Crucible.UseCFG cfg (Crucible.postdomInfo cfg) - _ <- Crucible.callCFG staticInitCfg Crucible.emptyRegMap - - mapM_ (registerOverride opts cc simctx top_loc mdMap) + do mapM_ (registerOverride opts cc simctx top_loc mdMap) (List.groupOn (view MS.csMethod) (map (view MS.psSpec) lemmas)) liftIO $ for_ assumes $ \(Crucible.LabeledPred p (md, reason)) -> @@ -872,36 +857,20 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat m let loc = MS.conditionLoc md Crucible.addAssumption bak (Crucible.GenericAssumption loc reason expr) fnCall - Crucible.executeCrucible (map Crucible.genericToExecutionFeature feats) - (simSt (Crucible.runOverrideSim methodRetTy overrideSim)) - - case res of - Crucible.FinishedResult _ pr -> - do Crucible.GlobalPair retval globals1 <- - case pr of - Crucible.TotalRes gp -> return gp - Crucible.PartialRes _ _ gp _ -> - do printOutLn opts Info "Symbolic simulation completed with side conditions." - return gp - let ret_ty = mspec ^. MS.csRet - retval' <- - case ret_ty of - Nothing -> return Nothing - Just ret_mt -> - case retval of - Crucible.RegEntry ty val -> - case decodeMIRVal col ret_mt (Crucible.AnyValue ty val) of - Nothing -> error $ "FIXME: Unsupported return type: " ++ show ret_ty - Just v -> return (Just (ret_mt, v)) - return (retval', globals1) - - Crucible.AbortedResult _ ar -> - do let resultDoc = ppMIRAbortedResult cc ar - fail $ unlines [ "Symbolic execution failed." - , show resultDoc - ] - - Crucible.TimeoutResult _cxt -> fail "Symbolic execution timed out." + runCrucible opts simctx globals (map Crucible.genericToExecutionFeature feats) + methodRetTy overrideSim + + let ret_ty = mspec ^. MS.csRet + retval' <- + case ret_ty of + Nothing -> return Nothing + Just ret_mt -> + case retval of + Crucible.RegEntry ty val -> + case decodeMIRVal col ret_mt (Crucible.AnyValue ty val) of + Nothing -> error $ "FIXME: Unsupported return type: " ++ show ret_ty + Just v -> return (Just (ret_mt, v)) + return (retval', globals1) where prepareArg :: forall tp. Crucible.TypeRepr tp -> MIRVal -> IO (Crucible.RegValue Sym tp) @@ -1018,46 +987,6 @@ findAdt col origName substs = where insts = col ^. Mir.adtsOrig . at origName . to (fromMaybe []) --- | Given a function name @fnName@, attempt to look up its corresponding --- 'Mir.DefId'. Currently, the following types of function names are permittd: --- --- * @/::: A fully disambiguated name. --- --- * @::: A name without a disambiguator. In this --- case, SAW will attempt to look up a disambiguator from the @crateDisambigs@ --- map. If none can be found, or if there are multiple disambiguators for the --- given @@, then this will fail. -findDefId :: Map Text (NonEmpty Text) -> Text -> TopLevel Mir.DefId -findDefId crateDisambigs fnName = do - (crate, path) <- - case edid of - crate:path -> pure (crate, path) - [] -> fail $ unlines - [ "The function `" ++ fnNameStr ++ "` lacks a crate." - , "Consider providing one, e.g., `::" ++ fnNameStr ++ "`." - ] - let crateStr = Text.unpack crate - case Text.splitOn "/" crate of - [crateNoDisambig, disambig] -> - pure $ Mir.textId $ Text.intercalate "::" - $ (crateNoDisambig <> "/" <> disambig) : path - [_] -> - case Map.lookup crate crateDisambigs of - Just allDisambigs@(disambig :| otherDisambigs) - | F.null otherDisambigs - -> pure $ Mir.textId $ Text.intercalate "::" - $ (crate <> "/" <> disambig) : path - | otherwise - -> fail $ unlines $ - [ "ambiguous crate " ++ crateStr - , "crate disambiguators:" - ] ++ F.toList (Text.unpack <$> allDisambigs) - Nothing -> fail $ "unknown crate " ++ crateStr - _ -> fail $ "Malformed crate name: " ++ show crateStr - where - fnNameStr = Text.unpack fnName - edid = Text.splitOn "::" fnName - getMIRCrucibleContext :: CrucibleSetup MIR MIRCrucibleContext getMIRCrucibleContext = view Setup.csCrucibleContext <$> get @@ -1073,13 +1002,49 @@ lookupDefIdCFG rm method = Just x -> return x Nothing -> fail $ "Couldn't find CFG for MIR function: " ++ show method +-- | Some boilerplate code needed to invoke 'Crucible.executeCrucible' and +-- extract the results. +runCrucible :: + Crucible.IsSyntaxExtension ext => + Options -> + Crucible.SimContext p Sym ext -> + Crucible.SymGlobalState Sym -> + [Crucible.ExecutionFeature p Sym ext (Crucible.RegEntry Sym a)] -> + Crucible.TypeRepr a -> + Crucible.OverrideSim p Sym ext (Crucible.RegEntry Sym a) Crucible.EmptyCtx a (Crucible.RegValue Sym a) -> + IO (Crucible.SimContext p Sym ext, Crucible.GlobalPair Sym (Crucible.RegEntry Sym a)) +runCrucible opts simCtx globals execFeatures ovRetTpr ovSim = do + let initExecState = + Crucible.InitialState simCtx globals Crucible.defaultAbortHandler ovRetTpr $ + Crucible.runOverrideSim ovRetTpr ovSim + res <- Crucible.executeCrucible execFeatures initExecState + case res of + Crucible.FinishedResult simctx pr -> + case pr of + Crucible.TotalRes gp -> return (simctx, gp) + Crucible.PartialRes _ _ gp _ -> + do printOutLn opts Info "Symbolic simulation completed with side conditions." + return (simctx, gp) + + Crucible.AbortedResult _ ar -> do + let resultDoc = ppMIRAbortedResult ar + fail $ unlines [ "Symbolic execution failed." + , show resultDoc + ] + + Crucible.TimeoutResult _cxt -> + fail "Symbolic execution timed out." + setupCrucibleContext :: Mir.RustModule -> TopLevel MIRCrucibleContext setupCrucibleContext rm = do halloc <- getHandleAlloc sc <- getSharedContext pathSatSolver <- gets rwPathSatSolver sym <- io $ newSAWCoreExprBuilder sc - bak <- io $ newSAWCoreBackend pathSatSolver sym + someBak@(SomeOnlineBackend bak) <- io $ newSAWCoreBackend pathSatSolver sym + let cs = rm ^. Mir.rmCS + let col = cs ^. Mir.collection + let cfgMap = rm ^. Mir.rmCFGs opts <- getOptions io $ do let cfg = W4.getConfiguration sym verbSetting <- W4.getOptionSetting W4.verbosity cfg @@ -1089,18 +1054,156 @@ setupCrucibleContext rm = -- TODO! there's a lot of options setup we need to replicate -- from SAWScript.Crucible.LLVM.Builtins + -- There is quite a bit of faff below, all for the sake of translating + -- top-level static values. See Note [Translating MIR statics in SAW] for + -- a high-level description of what this code is doing. + Crucible.AnyCFG staticInitCfg <- + withImplicitParams opts $ io $ Mir.transStatics cs halloc + let staticInitHndl = Crucible.cfgHandle staticInitCfg + let staticInitArgTys = Crucible.handleArgTypes staticInitHndl + let staticInitRetTy = Crucible.handleReturnType staticInitHndl + Refl <- case testEquality staticInitArgTys Ctx.Empty of + Just e -> + pure e + Nothing -> + panic "setupCrucibleContext" + [ "static initializer should not require arguments:" + , show staticInitArgTys + ] + Refl <- case testEquality staticInitRetTy Crucible.UnitRepr of + Just e -> + pure e + Nothing -> + panic "setupCrucibleContext" + [ "static initializer should return ():" + , show staticInitRetTy + ] + + let bindings = Crucible.fnBindingsFromList $ + map (\(Crucible.AnyCFG cfg) -> + Crucible.FnBinding + (Crucible.cfgHandle cfg) + (Crucible.UseCFG cfg (Crucible.postdomInfo cfg))) $ + Map.elems cfgMap + let simctx0 = Crucible.initSimContext bak + Mir.mirIntrinsicTypes halloc stdout + bindings Mir.mirExtImpl + SAWCruciblePersonality + let globals0 = Crucible.emptyGlobals + let setupGlobals = Crucible.regValue <$> Crucible.callCFG staticInitCfg Crucible.emptyRegMap + -- Step (1) in Note [Translating MIR statics in SAW] + (simctx1, gp) <- io $ runCrucible opts simctx0 globals0 [] Crucible.UnitRepr setupGlobals + let globalsAllStatics = gp ^. Crucible.gpGlobals + -- Step (2) in Note [Translating MIR statics in SAW] + let (globalsImmutStaticsOnly, staticInitializerPairs) = + mapAccumL + (\globals (staticDefId, Mir.StaticVar gv) -> + let static = + case Map.lookup staticDefId (col ^. Mir.statics) of + Just static' -> + static' + Nothing -> + panic "setupCrucibleContext" + [ "staticDefId not in statics map:" + , show staticDefId + ] in + case Crucible.lookupGlobal gv globalsAllStatics of + Just rv -> + let pair = MapF.Pair gv (Crucible.RV rv) in + if static ^. Mir.sMutable + then (globals, pair) + else (Crucible.insertGlobal gv rv globals, pair) + Nothing -> + panic "setupCrucibleContext" + [ "Static GlobalVar not in SymGlobalState:" + , show gv + ]) + globals0 + (cs ^. Mir.staticMap . to Map.toList) + let staticInitializerMap = MapF.fromList staticInitializerPairs + return MIRCrucibleContext { _mccRustModule = rm - , _mccBackend = bak - , _mccHandleAllocator = halloc + , _mccBackend = someBak + , _mccSimContext = simctx1 + , _mccSymGlobalState = globalsImmutStaticsOnly + , _mccStaticInitializerMap = staticInitializerMap } +{- +Note [Translating MIR statics in SAW] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Translating top-level static values in the SAW MIR backend requires some care. +This is because we want to treat immutable and mutable static differently: + +* Immutable statics should be implicitly initialized in each specification + without any action required on the user's end. + +* Mutable statics should /not/ be initialized in a specification unless a user + explicitly declares it with `mir_points_to (mir_static ...) ...`. This is + because a mutable static's value can change over the course of a program, so + we require users to be precise about what the value should be before and after + invoking a function. + +This poses a challenge when translating static values in SAW. It is tempting to +only translate the immutable statics and not the mutable statics (similarly to +how the SAW LLVM backend handles translation), but this will not work in +general. Consider this program: + + static mut S1: u32 = 1; + static S2: u32 = unsafe { S1 }; + + pub fn f() { + ... S2 ... + } + +The initial value of S2 (an immutable static) depends on having first translated +the initial value of S1 (a mutable static). If we do not translate mutable +statics in SAW, the translation of S1 will not succeed. + +We solve this problem by doing the following: + +1. Use Crucible to translate all top-level static values (both immutable and + mutable). This produces a SymGlobalState that contains every static's + initializer value. + +2. Consult the updated SymGlobalState to produce the following: + + (a) A subset of the SymGlobalState that only contains the initializer values + for the immutable statics. This will be used later to initialize the + Crucible state when translating the function being verified with + mir_verify. + + (b) A MirStaticInitializerMap mapping all static variables (both immutable + and mutable) to their initializer values. This will be used later to + power the mir_static_initializer function. + +This is a bit clunky, but it's unclear how to do better without significantly +changing how crucible-mir translates top-level static values. +-} + +-- | Define several commonly used implicit parameters in @crucible-mir@ and +-- call a continuation with these parameters. +withImplicitParams :: + Options -> + ( ( ?debug :: Int, ?customOps :: Mir.CustomOpMap + , ?assertFalseOnError :: Bool, ?printCrucible :: Bool + ) => r) -> + r +withImplicitParams opts k = + let ?debug = simVerbose opts in + -- For now, we use the same default settings for implicit parameters as in + -- crux-mir. We may want to add options later that allow configuring these. + let ?assertFalseOnError = True in + let ?customOps = customOps in + let ?printCrucible = False in + k + -------------------------------------------------------------------------------- -- Errors -------------------------------------------------------------------------------- data MIRSetupError = MIRFreshVarInvalidType Mir.Ty - | MIRPointsToNonReference SetupValue | MIRArgTypeMismatch Int Mir.Ty Mir.Ty -- argument position, expected, found | MIRArgNumberWrong Int Int -- number expected, number found | MIRReturnUnexpected Mir.Ty -- found @@ -1115,11 +1218,6 @@ instance Show MIRSetupError where case err of MIRFreshVarInvalidType jty -> "mir_fresh_var: Invalid type: " ++ show jty - MIRPointsToNonReference ptr -> - unlines - [ "mir_points_to: Left-hand side is not a valid reference" - , show (MS.ppSetupValue ptr) - ] MIRArgTypeMismatch i expected found -> unlines [ "mir_execute_func: Argument type mismatch" diff --git a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs index 87e4cc430a..2fa95e2bc1 100644 --- a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs @@ -12,10 +12,16 @@ module SAWScript.Crucible.MIR.MethodSpecIR MIRCrucibleContext(..) , mccRustModule , mccBackend + , mccSimContext + , mccSymGlobalState + , mccStaticInitializerMap , mccHandleAllocator , mccWithBackend , mccSym + -- * @MirStaticInitializerMap@ + , MirStaticInitializerMap + -- * @MirPointsTo@ , MirPointsTo(..) @@ -44,6 +50,8 @@ module SAWScript.Crucible.MIR.MethodSpecIR import Control.Lens (Getter, (^.), to) import qualified Prettyprinter as PP +import Lang.Crucible.FunctionHandle (HandleAllocator) +import Lang.Crucible.Simulator (SimContext(..)) import Mir.Generator import Mir.Intrinsics import qualified Mir.Mir as M @@ -54,6 +62,9 @@ import qualified SAWScript.Crucible.Common.MethodSpec as MS import qualified SAWScript.Crucible.Common.Setup.Type as Setup import SAWScript.Crucible.MIR.Setup.Value +mccHandleAllocator :: Getter MIRCrucibleContext HandleAllocator +mccHandleAllocator = mccSimContext . to simHandleAllocator + mccWithBackend :: MIRCrucibleContext -> (forall solver. OnlineSolver solver => Backend solver -> a) -> @@ -65,8 +76,8 @@ mccSym :: Getter MIRCrucibleContext Sym mccSym = to (\mcc -> mccWithBackend mcc backendGetSym) instance PP.Pretty MirPointsTo where - pretty (MirPointsTo _md alloc sv) = PP.parens $ - PP.pretty (show alloc) PP.<+> "->" PP.<+> PP.list (map MS.ppSetupValue sv) + pretty (MirPointsTo _md ref sv) = PP.parens $ + MS.ppSetupValue ref PP.<+> "->" PP.<+> PP.list (map MS.ppSetupValue sv) type MIRMethodSpec = MS.CrucibleMethodSpecIR MIR diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index e488ecd1a5..a6f9931a16 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -20,6 +20,7 @@ module SAWScript.Crucible.MIR.Override import qualified Control.Exception as X import Control.Lens +import Control.Monad (unless) import Control.Monad.IO.Class (MonadIO(..)) import Data.Foldable (for_, traverse_) import qualified Data.Functor.Product as Functor @@ -30,13 +31,13 @@ import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Some (Some(..)) import qualified Data.Parameterized.TraversableFC as FC import qualified Data.Set as Set +import Data.Set (Set) import qualified Data.Vector as V import Data.Void (absurd) import qualified Prettyprinter as PP import qualified Cryptol.TypeCheck.AST as Cryptol import qualified Cryptol.Eval.Type as Cryptol (TValue(..), evalType) -import qualified Lang.Crucible.Backend as Crucible import qualified Lang.Crucible.Simulator as Crucible import qualified Lang.Crucible.Types as Crucible import qualified Mir.Generator as Mir @@ -46,7 +47,6 @@ import qualified Mir.Mir as Mir import qualified Mir.TransTy as Mir import qualified What4.Expr as W4 import qualified What4.Interface as W4 -import qualified What4.Partial as W4 import qualified What4.ProgramLoc as W4 import Verifier.SAW.Prelude (scEq) @@ -185,12 +185,12 @@ instantiateSetupValue sc s v = 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.SetupNull empty -> absurd empty - MS.SetupGlobal empty _ -> absurd empty + MS.SetupGlobal _ _ -> return v MS.SetupElem _ _ _ -> return v MS.SetupField _ _ _ -> return v MS.SetupCast empty _ -> absurd empty MS.SetupUnion empty _ _ -> absurd empty - MS.SetupGlobalInitializer empty _ -> absurd empty + MS.SetupGlobalInitializer _ _ -> return v where doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t @@ -242,16 +242,29 @@ learnPointsTo :: MS.PrePost -> MirPointsTo -> OverrideMatcher MIR w () -learnPointsTo opts sc cc spec prepost (MirPointsTo md allocIdx referents) = +learnPointsTo opts sc cc spec prepost (MirPointsTo md reference referents) = mccWithBackend cc $ \bak -> do let col = cc ^. mccRustModule . Mir.rmCS ^. Mir.collection globals <- OM (use overrideGlobals) - Some mp <- resolveAllocIndexMIR allocIdx - let mpMirTy = mp^.mpMirType - let mpTpr = tyToShapeEq col mpMirTy (mp^.mpType) - val <- firstPointsToReferent referents - v <- liftIO $ Mir.readMirRefIO bak globals Mir.mirIntrinsicTypes (mp^.mpType) (mp^.mpRef) - matchArg opts sc cc spec prepost md (MIRVal mpTpr v) mpMirTy val + MIRVal referenceShp referenceVal <- + resolveSetupValueMIR opts cc sc spec reference + -- By the time we reach here, we have already checked (in mir_points_to) + -- that we are in fact dealing with a reference value, so the call to + -- `testRefShape` below should always succeed. + IsRefShape _ referenceInnerMirTy _ referenceInnerTpr <- + case testRefShape referenceShp of + Just irs -> pure irs + Nothing -> + panic "learnPointsTo" + [ "Unexpected non-reference type:" + , show $ PP.pretty $ shapeMirTy referenceShp + ] + let innerShp = tyToShapeEq col referenceInnerMirTy referenceInnerTpr + referentVal <- firstPointsToReferent referents + v <- liftIO $ Mir.readMirRefIO bak globals Mir.mirIntrinsicTypes + referenceInnerTpr referenceVal + matchArg opts sc cc spec prepost md (MIRVal innerShp v) + referenceInnerMirTy referentVal -- | Process a "crucible_precond" statement from the precondition -- section of the CrucibleSetup block. @@ -321,8 +334,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = | Mir.MirVector_PartialVector xs' <- xs , V.length xs' == length zs -> - do xs'' <- liftIO $ - traverse (readMaybeType sym "vector element" (shapeType elemShp)) xs' + do let xs'' = V.map (readMaybeType sym "vector element" (shapeType elemShp)) xs' sequence_ [ matchArg opts sc cc cs prepost md (MIRVal elemShp x) y z | (x, z) <- zip (V.toList xs'') zs ] @@ -347,7 +359,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = ReqField shp -> matchArg opts sc cc cs prepost md (MIRVal shp x) y z OptField shp -> do - x' <- liftIO $ readMaybeType sym "field" (shapeType shp) x + 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)) @@ -363,7 +375,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = ReqField shp -> matchArg opts sc cc cs prepost md (MIRVal shp x) y z OptField shp -> do - x' <- liftIO $ readMaybeType sym "field" (shapeType shp) x + 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)) @@ -371,16 +383,37 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = zs ] + (MIRVal (RefShape _ _ _ xTpr) x, Mir.TyRef _ _, MS.SetupGlobal () name) -> do + static <- findStatic colState name + Mir.StaticVar yGlobalVar <- findStaticVar colState (static ^. Mir.sName) + let y = staticRefMux sym yGlobalVar + case W4.testEquality xTpr (Crucible.globalType yGlobalVar) of + Nothing -> fail_ + Just Refl -> do + pred_ <- liftIO $ + Mir.mirRef_eqIO bak x y + addAssert pred_ md =<< notEq + (_, _, MS.SetupGlobalInitializer () name) -> do + static <- findStatic colState name + let staticTy = static ^. Mir.sTy + unless (checkCompatibleTys expectedTy staticTy) fail_ + staticInitMirVal <- findStaticInitializer cc static + pred_ <- liftIO $ equalValsPred cc staticInitMirVal actual + addAssert pred_ md =<< notEq + (_, _, MS.SetupNull empty) -> absurd empty - (_, _, MS.SetupGlobal empty _) -> absurd empty (_, _, MS.SetupCast empty _) -> absurd empty (_, _, MS.SetupUnion empty _ _) -> absurd empty - (_, _, MS.SetupGlobalInitializer empty _) -> absurd empty - _ -> failure (MS.conditionLoc md) =<< - mkStructuralMismatch opts cc sc cs actual expected expectedTy + _ -> fail_ where - col = cc ^. mccRustModule . Mir.rmCS . Mir.collection + colState = cc ^. mccRustModule . Mir.rmCS + col = colState ^. Mir.collection + + 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 -- | For each points-to statement read the memory value through the -- given pointer (lhs) and match the value against the given pattern @@ -423,12 +456,29 @@ matchPointsTos opts sc cc spec prepost = go False [] -- determine if a precondition is ready to be checked checkPointsTo :: MirPointsTo -> OverrideMatcher MIR w Bool - checkPointsTo (MirPointsTo _ allocIdx _) = checkAllocIndex allocIdx + checkPointsTo (MirPointsTo _ ref _) = checkSetupValue ref - checkAllocIndex :: AllocIndex -> OverrideMatcher MIR w Bool - checkAllocIndex i = + checkSetupValue :: SetupValue -> OverrideMatcher MIR w Bool + checkSetupValue v = do m <- OM (use setupValueSub) - return (Map.member i m) + return (all (`Map.member` m) (setupVars v)) + + -- Compute the set of variable identifiers in a 'SetupValue' + setupVars :: SetupValue -> Set AllocIndex + setupVars v = + case v of + MS.SetupVar i -> Set.singleton i + MS.SetupStruct _ xs -> foldMap setupVars xs + MS.SetupTuple _ xs -> foldMap setupVars xs + MS.SetupArray _ xs -> foldMap setupVars xs + MS.SetupElem _ x _ -> setupVars x + MS.SetupField _ x _ -> setupVars x + MS.SetupTerm _ -> Set.empty + MS.SetupGlobal _ _ -> Set.empty + MS.SetupGlobalInitializer _ _ -> Set.empty + MS.SetupCast empty _ -> absurd empty + MS.SetupUnion empty _ _ -> absurd empty + MS.SetupNull empty -> absurd empty matchTerm :: SharedContext {- ^ context for constructing SAW terms -} -> @@ -476,33 +526,44 @@ mkStructuralMismatch _opts cc _sc spec (MIRVal shp _) setupval mty = do (Just setupTy) mty -readMaybeType :: - Crucible.IsSymInterface sym - => sym - -> String - -> Crucible.TypeRepr tp - -> Crucible.RegValue sym (Crucible.MaybeType tp) - -> IO (Crucible.RegValue sym tp) -readMaybeType sym desc tpr rv = - case readPartExprMaybe sym rv of - Just x -> return x - Nothing -> error $ "readMaybeType: accessed possibly-uninitialized " ++ desc ++ - " of type " ++ show tpr - -readPartExprMaybe :: - Crucible.IsSymInterface sym - => sym - -> W4.PartExpr (W4.Pred sym) a - -> Maybe a -readPartExprMaybe _sym W4.Unassigned = Nothing -readPartExprMaybe _sym (W4.PE p v) - | Just True <- W4.asConstantPred p = Just v - | otherwise = Nothing - -resolveAllocIndexMIR :: AllocIndex -> OverrideMatcher MIR w (Some (MirPointer Sym)) -resolveAllocIndexMIR i = - do m <- OM (use setupValueSub) - pure $ lookupAllocIndex m i +-- | Create an error stating that the 'MIRVal' was not equal to the 'SetupValue' +notEqual :: + MS.PrePost -> + Options {- ^ output/verbosity options -} -> + W4.ProgramLoc {- ^ where is the assertion from? -} -> + MIRCrucibleContext -> + SharedContext {- ^ context for constructing SAW terms -} -> + MS.CrucibleMethodSpecIR MIR {- ^ for name and typing environments -} -> + SetupValue {- ^ the value from the spec -} -> + MIRVal {- ^ the value from the simulator -} -> + OverrideMatcher MIR w Crucible.SimError +notEqual cond opts loc cc sc spec expected actual = do + sym <- Ov.getSymInterface + let prettyMIRVal = ppMIRVal sym actual + prettySetupMIRVal <- ppSetupValueAsMIRVal opts cc sc spec expected + let msg = unlines + [ "Equality " ++ MS.stateCond cond + , "Expected value (as a SAW value): " + , show (MS.ppSetupValue expected) + , "Expected value (as a Crucible value): " + , show prettySetupMIRVal + , "Actual value: " + , show prettyMIRVal + ] + pure $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" + +-- | Resolve a 'SetupValue' into a 'MIRVal' and pretty-print it +ppSetupValueAsMIRVal :: + Options {- ^ output/verbosity options -} -> + MIRCrucibleContext -> + SharedContext {- ^ context for constructing SAW terms -} -> + MS.CrucibleMethodSpecIR MIR {- ^ for name and typing environments -} -> + SetupValue -> + OverrideMatcher MIR w (PP.Doc ann) +ppSetupValueAsMIRVal opts cc sc spec setupval = do + sym <- Ov.getSymInterface + mirVal <- resolveSetupValueMIR opts cc sc spec setupval + pure $ ppMIRVal sym mirVal resolveSetupValueMIR :: Options -> @@ -569,8 +630,8 @@ valueToSC sym md failMsg tval (MIRVal shp val) = liftIO (scVectorReduced sc t terms) | Mir.MirVector_PartialVector vals <- val , toInteger (V.length vals) == n - -> do vals' <- liftIO $ V.toList <$> - traverse (readMaybeType sym "vector element" (shapeType arrShp)) vals + -> do let vals' = V.toList $ + V.map (readMaybeType sym "vector element" (shapeType arrShp)) vals terms <- traverse (\v -> valueToSC sym md failMsg cryty (MIRVal arrShp v)) vals' t <- shapeToTerm sc arrShp @@ -591,7 +652,7 @@ valueToSC sym md failMsg tval (MIRVal shp val) = case fldShp of ReqField shp' -> pure $ MIRVal shp' tm - OptField shp' -> do - tm' <- liftIO $ readMaybeType sym "field" (shapeType shp') tm - pure $ MIRVal shp' tm' + OptField shp' -> + pure $ MIRVal shp' + $ readMaybeType sym "field" (shapeType shp') tm valueToSC sym md failMsg ty mirVal diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index f25b17130c..1288c857c6 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs @@ -3,6 +3,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} @@ -10,6 +11,7 @@ -- | Turns 'SetupValue's back into 'MIRVal's. module SAWScript.Crucible.MIR.ResolveSetupValue ( MIRVal(..) + , ppMIRVal , resolveSetupVal , typeOfSetupValue , lookupAllocIndex @@ -20,20 +22,36 @@ module SAWScript.Crucible.MIR.ResolveSetupValue , equalRefsPred , equalValsPred , checkCompatibleTys + , readMaybeType , mirAdtToTy + , findDefId + , findDefIdEither + , findStatic + , findStaticInitializer + , findStaticVar + , staticRefMux , MIRTypeOfError(..) ) where import Control.Lens -import Control.Monad (unless, zipWithM, zipWithM_) +import Control.Monad (guard, unless, zipWithM, zipWithM_) import qualified Control.Monad.Catch as X +import Control.Monad.IO.Class (MonadIO(..)) +import Control.Monad.Trans.Maybe (MaybeT(..)) 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 Data.List.NonEmpty (NonEmpty(..)) import Data.Map (Map) import qualified Data.Map as Map +import Data.Maybe (fromMaybe) import qualified Data.Parameterized.Context as Ctx +import qualified Data.Parameterized.Map as MapF import Data.Parameterized.Some (Some(..)) import qualified Data.Parameterized.TraversableFC as FC +import qualified Data.Parameterized.TraversableFC.WithIndex as FCI +import qualified Data.Text as Text import Data.Text (Text) import qualified Data.Vector as V import Data.Vector (Vector) @@ -44,9 +62,11 @@ import qualified Prettyprinter as PP import qualified Cryptol.Eval.Type as Cryptol (TValue(..), tValTy, evalValType) import qualified Cryptol.TypeCheck.AST as Cryptol (Type, Schema(..)) import qualified Cryptol.Utils.PP as Cryptol (pp) -import Lang.Crucible.Simulator (AnyValue(..), RegValue, RegValue'(..)) -import Lang.Crucible.Types (TypeRepr(..)) +import Lang.Crucible.Backend (IsSymInterface) +import Lang.Crucible.Simulator (AnyValue(..), GlobalVar(..), RegValue, RegValue'(..)) +import Lang.Crucible.Types (MaybeType, TypeRepr(..)) import qualified Mir.DefId as Mir +import qualified Mir.FancyMuxTree as Mir import qualified Mir.Generator as Mir import qualified Mir.Intrinsics as Mir import Mir.Intrinsics (MIR) @@ -78,12 +98,81 @@ import SAWScript.Panic data MIRVal where MIRVal :: TypeShape tp -> RegValue Sym tp -> MIRVal +-- | Pretty-print a 'MIRVal'. +ppMIRVal :: + forall ann. + Sym -> + MIRVal -> + PP.Doc ann +ppMIRVal sym (MIRVal shp val) = + case shp of + UnitShape _ -> + PP.pretty val + PrimShape _ _ -> + W4.printSymExpr val + TupleShape _ _ fldShp -> + PP.parens $ prettyStructOrTuple fldShp val + ArrayShape _ _ shp' -> + case val of + Mir.MirVector_Vector vec -> + PP.brackets $ commaList $ V.toList $ + fmap (\v -> ppMIRVal sym (MIRVal shp' v)) vec + Mir.MirVector_PartialVector vec -> + PP.braces $ commaList $ V.toList $ + fmap (\v -> let v' = readMaybeType sym "vector element" (shapeType shp') v in + ppMIRVal sym (MIRVal shp' v')) vec + Mir.MirVector_Array arr -> + W4.printSymExpr arr + StructShape _ _ fldShp + | AnyValue (StructRepr fldTpr) fldVals <- val + , Just Refl <- W4.testEquality (FC.fmapFC fieldShapeType fldShp) fldTpr + -> PP.braces $ prettyStructOrTuple fldShp fldVals + + | otherwise + -> error "Malformed MIRVal struct" + TransparentShape _ shp' -> + ppMIRVal sym $ MIRVal shp' val + RefShape _ _ _ _ -> + "" + FnPtrShape _ _ _ -> + PP.viaShow val + where + commaList :: [PP.Doc ann] -> PP.Doc ann + commaList [] = PP.emptyDoc + commaList (x:xs) = x PP.<> PP.hcat (map (\y -> PP.comma PP.<+> y) xs) + + prettyStructOrTuple :: + forall ctx. + Ctx.Assignment FieldShape ctx -> + Ctx.Assignment (RegValue' Sym) ctx -> + PP.Doc ann + prettyStructOrTuple fldShp fldVals = + commaList $ + map (\(Some (Functor.Pair shp' (RV v))) -> prettyField shp' v) $ + FC.toListFC Some $ + Ctx.zipWith Functor.Pair fldShp fldVals + + prettyField :: + forall tp. + FieldShape tp -> + RegValue Sym tp -> + PP.Doc ann + prettyField fldShp val' = + case fldShp of + OptField shp' -> + ppMIRVal sym $ MIRVal shp' $ + readMaybeType sym "field" (shapeType shp') val' + ReqField shp' -> + ppMIRVal sym $ MIRVal shp' val' + type SetupValue = MS.SetupValue MIR data MIRTypeOfError = MIRPolymorphicType Cryptol.Schema | MIRNonRepresentableType Cryptol.Type ToMIRTypeErr | MIRInvalidTypedTerm TypedTermType + | MIRInvalidIdentifier String + | MIRStaticNotFound Mir.DefId instance Show MIRTypeOfError where show (MIRPolymorphicType s) = @@ -103,10 +192,22 @@ instance Show MIRTypeOfError where [ "Expected typed term with Cryptol-representable type, but got" , show (MS.ppTypedTermType tp) ] + show (MIRInvalidIdentifier errMsg) = + errMsg + show (MIRStaticNotFound did) = + staticNotFoundErr did + +staticNotFoundErr :: Mir.DefId -> String +staticNotFoundErr did = + unlines + [ "Could not find static named:" + , show did + ] instance X.Exception MIRTypeOfError typeOfSetupValue :: + forall m. X.MonadThrow m => MIRCrucibleContext -> Map AllocIndex (Some MirAllocSpec) -> @@ -135,14 +236,19 @@ typeOfSetupValue mcc env nameEnv val = MS.SetupTuple () vals -> do tys <- traverse (typeOfSetupValue mcc env nameEnv) vals pure $ Mir.TyTuple tys + MS.SetupGlobal () name -> + staticTyRef <$> findStatic cs name + MS.SetupGlobalInitializer () name -> do + static <- findStatic cs name + pure $ static ^. Mir.sTy MS.SetupNull empty -> absurd empty - MS.SetupGlobal empty _ -> absurd empty MS.SetupElem _ _ _ -> panic "typeOfSetupValue" ["elems not yet implemented"] MS.SetupField _ _ _ -> panic "typeOfSetupValue" ["fields not yet implemented"] MS.SetupCast empty _ -> absurd empty MS.SetupUnion empty _ _ -> absurd empty - MS.SetupGlobalInitializer empty _ -> absurd empty + where + cs = mcc ^. mccRustModule . Mir.rmCS lookupAllocIndex :: Map AllocIndex a -> AllocIndex -> a lookupAllocIndex env i = @@ -172,7 +278,6 @@ resolveSetupVal mcc env tyenv nameEnv val = (ptr ^. mpRef) MS.SetupTerm tm -> resolveTypedTerm mcc tm MS.SetupNull empty -> absurd empty - MS.SetupGlobal empty _ -> absurd empty MS.SetupStruct adt flds -> case adt of _ | adt ^. Mir.adtReprTransparent, @@ -251,10 +356,20 @@ resolveSetupVal mcc env tyenv nameEnv val = MS.SetupField _ _ _ -> panic "resolveSetupValue" ["fields not yet implemented"] MS.SetupCast empty _ -> absurd empty MS.SetupUnion empty _ _ -> absurd empty - MS.SetupGlobalInitializer empty _ -> absurd empty + MS.SetupGlobal () name -> do + static <- findStatic cs name + Mir.StaticVar gv <- findStaticVar cs (static ^. Mir.sName) + let sMut = staticMutability static + sTy = static ^. Mir.sTy + pure $ MIRVal (RefShape (staticTyRef static) sTy sMut (globalType gv)) + $ staticRefMux sym gv + MS.SetupGlobalInitializer () name -> do + static <- findStatic cs name + findStaticInitializer mcc static where sym = mcc ^. mccSym - col = mcc ^. mccRustModule . Mir.rmCS . Mir.collection + cs = mcc ^. mccRustModule . Mir.rmCS + col = cs ^. Mir.collection resolveTypedTerm :: MIRCrucibleContext -> @@ -455,12 +570,107 @@ equalRefsPred cc mp1 mp2 = Nothing -> pure $ W4.falsePred sym Just Refl -> Mir.mirRef_eqIO bak (mp1^.mpRef) (mp2^.mpRef) +-- | Check if two 'MIRVal's are equal. equalValsPred :: MIRCrucibleContext -> MIRVal -> MIRVal -> IO (W4.Pred Sym) -equalValsPred = panic "equalValsPred" ["not yet implemented"] +equalValsPred cc mv1 mv2 = + case (mv1, mv2) of + (MIRVal shp1 v1, MIRVal shp2 v2) -> do + mbEq <- runMaybeT $ do + guard $ checkCompatibleTys (shapeMirTy shp1) (shapeMirTy shp2) + Refl <- testEquality shp1 shp2 + goTy shp1 v1 v2 + pure $ fromMaybe (W4.falsePred sym) mbEq + where + sym = cc^.mccSym + + testEquality :: forall k (f :: k -> Type) (a :: k) (b :: k) + . W4.TestEquality f + => f a -> f b -> MaybeT IO (a :~: b) + testEquality v1 v2 = MaybeT $ pure $ W4.testEquality v1 v2 + + goTy :: TypeShape tp + -> RegValue Sym tp + -> RegValue Sym tp + -> MaybeT IO (W4.Pred Sym) + goTy (UnitShape _) () () = + pure $ W4.truePred sym + goTy (PrimShape _ _) v1 v2 = + liftIO $ W4.isEq sym v1 v2 + goTy (TupleShape _ _ fldShp) fldAssn1 fldAssn2 = + goFldAssn fldShp fldAssn1 fldAssn2 + goTy (ArrayShape _ _ shp) vec1 vec2 = + goVec shp vec1 vec2 + goTy (StructShape _ _ fldShp) any1 any2 = + case (any1, any2) of + (AnyValue (StructRepr fldCtx1) fldAssn1, + AnyValue (StructRepr fldCtx2) fldAssn2) -> do + Refl <- testEquality fldCtx1 fldCtx2 + Refl <- testEquality (FC.fmapFC fieldShapeType fldShp) fldCtx1 + goFldAssn fldShp fldAssn1 fldAssn2 + (_, _) -> + pure $ W4.falsePred sym + goTy (TransparentShape _ shp) v1 v2 = + goTy shp v1 v2 + goTy (RefShape _ _ _ _) ref1 ref2 = + mccWithBackend cc $ \bak -> + liftIO $ Mir.mirRef_eqIO bak ref1 ref2 + goTy (FnPtrShape _ _ _) _fh1 _fh2 = + error "Function pointers not currently supported in overrides" + + goVec :: TypeShape tp + -> Mir.MirVector Sym tp + -> Mir.MirVector Sym tp + -> MaybeT IO (W4.Pred Sym) + goVec shp (Mir.MirVector_Vector vec1) + (Mir.MirVector_Vector vec2) = do + eqs <- V.zipWithM (goTy shp) vec1 vec2 + liftIO $ F.foldrM (W4.andPred sym) (W4.truePred sym) eqs + goVec shp (Mir.MirVector_PartialVector vec1) + (Mir.MirVector_PartialVector vec2) = do + eqs <- V.zipWithM + (\v1 v2 -> do + let readElem v = readMaybeType sym "vector element" (shapeType shp) v + let v1' = readElem v1 + let v2' = readElem v2 + goTy shp v1' v2') + vec1 + vec2 + liftIO $ F.foldrM (W4.andPred sym) (W4.truePred sym) eqs + goVec _shp (Mir.MirVector_Array vec1) (Mir.MirVector_Array vec2) = + liftIO $ W4.arrayEq sym vec1 vec2 + goVec _shp _vec1 _vec2 = + pure $ W4.falsePred sym + + goFldAssn :: Ctx.Assignment FieldShape ctx + -> Ctx.Assignment (RegValue' Sym) ctx + -> Ctx.Assignment (RegValue' Sym) ctx + -> MaybeT IO (W4.Pred Sym) + goFldAssn fldShp fldAssn1 fldAssn2 = + FCI.ifoldrMFC + (\idx (Functor.Pair (RV fld1) (RV fld2)) z -> do + let shp = fldShp Ctx.! idx + eq <- goFld shp fld1 fld2 + liftIO $ W4.andPred sym eq z) + (W4.truePred sym) + (Ctx.zipWith Functor.Pair fldAssn1 fldAssn2) + + goFld :: FieldShape tp + -> RegValue Sym tp + -> RegValue Sym tp + -> MaybeT IO (W4.Pred Sym) + goFld shp v1 v2 = + case shp of + ReqField shp' -> + goTy shp' v1 v2 + OptField shp' -> do + let readField v = readMaybeType sym "field" (shapeType shp') v + let v1' = readField v1 + let v2' = readField v2 + goTy shp' v1' v2' -- | Check if two 'Mir.Ty's are compatible in SAW. This is a slightly coarser -- notion of equality to reflect the fact that MIR's type system is richer than @@ -629,7 +839,149 @@ fnSigView :: Mir.FnSig -> FnSigView fnSigView (Mir.FnSig argTys retTy abi spreadarg) = FnSigView (map tyView argTys) (tyView retTy) abi spreadarg +-- | Read the value out of a 'MaybeType' expression that is assumed to be +-- assigned to a value. If this assumption does not hold (i.e., if the value is +-- unassigned), then this function will raise an error. +readMaybeType :: + IsSymInterface sym + => sym + -> String + -> TypeRepr tp + -> RegValue sym (MaybeType tp) + -> RegValue sym tp +readMaybeType sym desc tpr rv = + case readPartExprMaybe sym rv of + Just x -> x + Nothing -> error $ "readMaybeType: accessed possibly-uninitialized " ++ desc ++ + " of type " ++ show tpr + +readPartExprMaybe :: + IsSymInterface sym + => sym + -> W4.PartExpr (W4.Pred sym) a + -> Maybe a +readPartExprMaybe _sym W4.Unassigned = Nothing +readPartExprMaybe _sym (W4.PE p v) + | Just True <- W4.asConstantPred p = Just v + | otherwise = Nothing + -- | Construct an 'Mir.TyAdt' from an 'Mir.Adt'. mirAdtToTy :: Mir.Adt -> Mir.Ty mirAdtToTy adt = Mir.TyAdt (adt ^. Mir.adtname) (adt ^. Mir.adtOrigDefId) (adt ^. Mir.adtOrigSubsts) + +-- | Like 'findDefIdEither', but any errors are thrown with 'fail'. +findDefId :: MonadFail m => Map Text (NonEmpty Text) -> Text -> m Mir.DefId +findDefId crateDisambigs fnName = + either fail pure $ findDefIdEither crateDisambigs fnName + +-- | Given a function name @fnName@, attempt to look up its corresponding +-- 'Mir.DefId'. If successful, return it with 'Right'. Currently, the following +-- types of function names are permittd: +-- +-- * @/::: A fully disambiguated name. +-- +-- * @::: A name without a disambiguator. In this +-- case, SAW will attempt to look up a disambiguator from the @crateDisambigs@ +-- map. If none can be found, or if there are multiple disambiguators for the +-- given @@, then this will return an error message with 'Left'. +findDefIdEither :: Map Text (NonEmpty Text) -> Text -> Either String Mir.DefId +findDefIdEither crateDisambigs fnName = do + (crate, path) <- + case edid of + crate:path -> pure (crate, path) + [] -> Left $ unlines + [ "The function `" ++ fnNameStr ++ "` lacks a crate." + , "Consider providing one, e.g., `::" ++ fnNameStr ++ "`." + ] + let crateStr = Text.unpack crate + case Text.splitOn "/" crate of + [crateNoDisambig, disambig] -> + Right $ Mir.textId $ Text.intercalate "::" + $ (crateNoDisambig <> "/" <> disambig) : path + [_] -> + case Map.lookup crate crateDisambigs of + Just allDisambigs@(disambig :| otherDisambigs) + | F.null otherDisambigs + -> Right $ Mir.textId $ Text.intercalate "::" + $ (crate <> "/" <> disambig) : path + | otherwise + -> Left $ unlines $ + [ "ambiguous crate " ++ crateStr + , "crate disambiguators:" + ] ++ F.toList (Text.unpack <$> allDisambigs) + Nothing -> Left $ "unknown crate " ++ crateStr + _ -> Left $ "Malformed crate name: " ++ show crateStr + where + fnNameStr = Text.unpack fnName + edid = Text.splitOn "::" fnName + +-- | Consult the given 'Mir.CollectionState' to find a 'Mir.Static' with the +-- given 'String' as an identifier. If such a 'Mir.Static' cannot be found, this +-- will raise an error. +findStatic :: X.MonadThrow m => Mir.CollectionState -> String -> m Mir.Static +findStatic cs name = do + did <- case findDefIdEither (cs ^. Mir.crateHashesMap) (Text.pack name) of + Left err -> X.throwM $ MIRInvalidIdentifier err + Right did -> pure did + case Map.lookup did (cs ^. Mir.collection . Mir.statics) of + Nothing -> X.throwM $ MIRStaticNotFound did + Just static -> pure static + +-- | Consult the given 'MIRCrucibleContext' to find the 'MIRVal' used to +-- initialize a 'Mir.Static' value. If such a 'MIRVal' cannot be found, this +-- will raise an error. +findStaticInitializer :: + X.MonadThrow m => + MIRCrucibleContext -> + Mir.Static -> + m MIRVal +findStaticInitializer mcc static = do + Mir.StaticVar gv <- findStaticVar cs staticDefId + let staticShp = tyToShapeEq col (static ^. Mir.sTy) (globalType gv) + case MapF.lookup gv (mcc^.mccStaticInitializerMap) of + Just (RV staticInitVal) -> + pure $ MIRVal staticShp staticInitVal + Nothing -> + X.throwM $ MIRStaticNotFound staticDefId + where + staticDefId = static ^. Mir.sName + cs = mcc ^. mccRustModule . Mir.rmCS + col = cs ^. Mir.collection + +-- | Consult the given 'Mir.CollectionState' to find a 'Mir.StaticVar' with the +-- given 'Mir.DefId'. If such a 'Mir.StaticVar' cannot be found, this will raise +-- an error. +findStaticVar :: + X.MonadThrow m => + Mir.CollectionState -> + Mir.DefId -> + m Mir.StaticVar +findStaticVar cs staticDefId = + case Map.lookup staticDefId (cs ^. Mir.staticMap) of + Nothing -> X.throwM $ MIRStaticNotFound staticDefId + Just sv -> pure sv + +-- | Compute the 'Mir.Mutability' of a 'Mir.Static' value. +staticMutability :: Mir.Static -> Mir.Mutability +staticMutability static + | static ^. Mir.sMutable = Mir.Mut + | otherwise = Mir.Immut + +-- | Compute a 'Mir.MirReferenceMux' pointing to a static value's 'GlobalVar'. +staticRefMux :: + W4.IsSymExprBuilder sym => + sym -> + GlobalVar tp -> + Mir.MirReferenceMux sym tp +staticRefMux sym gv = + Mir.MirReferenceMux $ + Mir.toFancyMuxTree sym $ + Mir.MirReference (Mir.GlobalVar_RefRoot gv) Mir.Empty_RefPath + +-- | Compute the 'Mir.Ty' of a reference to a 'Mir.Static' value. +staticTyRef :: Mir.Static -> Mir.Ty +staticTyRef static = + Mir.TyRef + (static ^. Mir.sTy) + (staticMutability static) diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs index 9aca21d93f..5c592abefb 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -22,7 +22,12 @@ module SAWScript.Crucible.MIR.Setup.Value MIRCrucibleContext(..) , mccRustModule , mccBackend - , mccHandleAllocator + , mccSimContext + , mccSymGlobalState + , mccStaticInitializerMap + + -- * @MirStaticInitializerMap@ + , MirStaticInitializerMap -- * @MirPointsTo@ , MirPointsTo(..) @@ -44,11 +49,12 @@ module SAWScript.Crucible.MIR.Setup.Value import Control.Lens (makeLenses) import Data.Parameterized.Classes +import Data.Parameterized.Map (MapF) import Data.Parameterized.Some import Data.Text (Text) import Data.Void (Void) -import Lang.Crucible.FunctionHandle (HandleAllocator) +import Lang.Crucible.Simulator (GlobalVar, RegValue', SimContext, SymGlobalState) import Lang.Crucible.Types import Mir.DefId import Mir.Generator @@ -59,7 +65,7 @@ import SAWScript.Crucible.Common import qualified SAWScript.Crucible.Common.Setup.Value as MS type instance MS.XSetupNull MIR = Void -type instance MS.XSetupGlobal MIR = Void +type instance MS.XSetupGlobal MIR = () type instance MS.XSetupStruct MIR = M.Adt type instance MS.XSetupTuple MIR = () -- The 'M.Ty' represents the type of array elements. @@ -68,7 +74,7 @@ type instance MS.XSetupElem MIR = () type instance MS.XSetupField MIR = () type instance MS.XSetupCast MIR = Void type instance MS.XSetupUnion MIR = Void -type instance MS.XSetupGlobalInitializer MIR = Void +type instance MS.XSetupGlobalInitializer MIR = () type instance MS.XGhostState MIR = Void @@ -84,22 +90,31 @@ type instance MS.Codebase MIR = CollectionState data MIRCrucibleContext = MIRCrucibleContext - { _mccRustModule :: RustModule - , _mccBackend :: SomeOnlineBackend - , _mccHandleAllocator :: HandleAllocator + { _mccRustModule :: RustModule + , _mccBackend :: SomeOnlineBackend + , _mccSimContext :: SimContext (SAWCruciblePersonality Sym) Sym MIR + , _mccSymGlobalState :: SymGlobalState Sym + , _mccStaticInitializerMap :: MirStaticInitializerMap } type instance MS.CrucibleContext MIR = MIRCrucibleContext type instance MS.Pointer' MIR sym = Some (MirPointer sym) +-- | A 'MirStaticInitializerMap' maps the 'GlobalVar's of each top-level static +-- value in a 'Mir.RustModule' to its initializer value (post-Crucible +-- translation). See @Note [Translating MIR statics in SAW]@ in +-- "SAWScript.Crucible.MIR.Builtins" for more details on how this map is +-- created. +type MirStaticInitializerMap = MapF GlobalVar (RegValue' Sym) + -- | Unlike @LLVMPointsTo@ and @JVMPointsTo@, 'MirPointsTo' contains a /list/ of -- 'MS.SetupValue's on the right-hand side. This is due to how slices are -- represented in @crucible-mir-comp@, which stores the list of values -- referenced by the slice. The @mir_points_to@ command, on the other hand, -- always creates 'MirPointsTo' values with exactly one value in the list (see -- the @firstPointsToReferent@ function in "SAWScript.Crucible.MIR.Override"). -data MirPointsTo = MirPointsTo MS.ConditionMetadata MS.AllocIndex [MS.SetupValue MIR] +data MirPointsTo = MirPointsTo MS.ConditionMetadata (MS.SetupValue MIR) [MS.SetupValue MIR] deriving (Show) data MirAllocSpec tp = MirAllocSpec diff --git a/src/SAWScript/Crucible/MIR/TypeShape.hs b/src/SAWScript/Crucible/MIR/TypeShape.hs index 5fed734473..47e845e01d 100644 --- a/src/SAWScript/Crucible/MIR/TypeShape.hs +++ b/src/SAWScript/Crucible/MIR/TypeShape.hs @@ -18,6 +18,8 @@ module SAWScript.Crucible.MIR.TypeShape , shapeMirTy , fieldShapeMirTy , shapeToTerm + , IsRefShape(..) + , testRefShape ) where import Control.Lens ((^.), (^..), each) @@ -251,6 +253,27 @@ shapeToTerm sc = go goField (OptField shp) = go shp goField (ReqField shp) = go shp +-- | A witness that a 'TypeShape' is equal to a 'RefShape'. +data IsRefShape (tp :: CrucibleType) where + IsRefShape :: M.Ty + -- ^ The reference type + -> M.Ty + -- ^ The pointee type + -> M.Mutability + -- ^ Is the reference mutable or immutable? + -> TypeRepr tp + -- ^ The Crucible representation of the pointee type + -> IsRefShape (MirReferenceType tp) + +-- | Check that a 'TypeShape' is equal to a 'RefShape'. If so, return 'Just' a +-- witness of that equality. Otherwise, return 'Nothing'. +testRefShape :: TypeShape tp -> Maybe (IsRefShape tp) +testRefShape shp = + case shp of + RefShape ty ty' mut shp' + -> Just $ IsRefShape ty ty' mut shp' + _ -> Nothing + $(pure []) instance TestEquality TypeShape where diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 0315b978b7..980aec8d95 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3976,6 +3976,22 @@ primitives = Map.fromList , "create; use `mir_find_adt` to retrieve a MIRAdt value." ] + , prim "mir_static" + "String -> MIRValue" + (pureVal (CMS.SetupGlobal () :: String -> CMS.SetupValue MIR)) + Experimental + [ "Return a MIRValue representing a reference to the named static." + , "The String should be the name of a static value." + ] + + , prim "mir_static_initializer" + "String -> MIRValue" + (pureVal (CMS.SetupGlobalInitializer () :: String -> CMS.SetupValue MIR)) + Experimental + [ "Return a MIRValue representing the value of the initializer of a named" + , "static. The String should be the name of a static value." + ] + , prim "mir_term" "Term -> MIRValue" (pureVal (CMS.SetupTerm :: TypedTerm -> CMS.SetupValue MIR))