diff --git a/CHANGES.md b/CHANGES.md index dbf13e439f..d722ae64cb 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -17,6 +17,13 @@ generating LLVM setup scripts for Cryptol FFI functions with the `llvm_ffi_setup` command. For more information, see the [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#verifying-cryptol-ffi-functions). +* Ghost state is now supported with the JVM and MIR language backends: + * The `llvm_declare_ghost_state` command is now deprecated in favor of the + new `declare_ghost_state` command, as nothing about this command is + LLVM-specific. + * Add `jvm_ghost_value` and `mir_ghost_value` commands in addition to the + existing `llvm_ghost_value` command. + # Version 1.0 -- 2023-06-26 ## New Features diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index 0e77b644b7..b8271368d6 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -641,8 +641,8 @@ substMethodSpec sc sm ms = do MS.SetupCond_Equal loc <$> goSetupValue sv1 <*> goSetupValue sv2 goSetupCondition (MS.SetupCond_Pred loc tt) = MS.SetupCond_Pred loc <$> goTypedTerm tt - goSetupCondition (MS.SetupCond_Ghost b loc gg tt) = - MS.SetupCond_Ghost b loc gg <$> goTypedTerm tt + goSetupCondition (MS.SetupCond_Ghost loc gg tt) = + MS.SetupCond_Ghost loc gg <$> goTypedTerm tt goSetupSlice (MirSetupSliceRaw ref len) = MirSetupSliceRaw <$> goSetupValue ref <*> goSetupValue len diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index da5d4ce55e..ea63c2122f 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -581,7 +581,7 @@ condTerm sc (MS.SetupCond_Pred md tt) = do sub <- use MS.termSub t' <- liftIO $ SAW.scInstantiateExt sc sub $ SAW.ttTerm tt return (md, t') -condTerm _ (MS.SetupCond_Ghost _ _ _ _) = do +condTerm _ (MS.SetupCond_Ghost _ _ _) = do error $ "learnCond: SetupCond_Ghost is not supported" diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 9fb91a2d73..b6e5beb656 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -3541,18 +3541,19 @@ thought of as additional global state that is visible only to the verifier. Ghost state with a given name can be declared at the top level with the following function: -* `llvm_declare_ghost_state : String -> TopLevel Ghost` +* `declare_ghost_state : String -> TopLevel Ghost` Ghost state variables do not initially have any particluar type, and can store data of any type. Given an existing ghost variable the following -function can be used to specify its value: +functions can be used to specify its value: * `llvm_ghost_value : Ghost -> Term -> LLVMSetup ()` +* `jvm_ghost_value : Ghost -> Term -> JVMSetup ()` +* `mir_ghost_value : Ghost -> Term -> MIRSetup ()` -Currently, this function can only be used for LLVM verification, though -that will likely be generalized in the future. It can be used in either -the pre state or the post state, to specify the value of ghost state -either before or after the execution of the function, respectively. +These can be used in either the pre state or the post state, to specify the +value of ghost state either before or after the execution of the function, +respectively. ## An Extended Example diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index 80e0c8ad8c..67f1cbdc2d 100644 Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ diff --git a/examples/ghost/ghost.saw b/examples/ghost/ghost.saw index 3e1dba3071..685ed46c45 100644 --- a/examples/ghost/ghost.saw +++ b/examples/ghost/ghost.saw @@ -16,7 +16,7 @@ let example_spec counter : CrucibleSetup () = do { }; let main : TopLevel () = do { - counter <- llvm_declare_ghost_state "ctr"; + counter <- declare_ghost_state "ctr"; m <- llvm_load_module "simple.bc"; next <- llvm_unsafe_assume_spec m "next" (next_spec counter); diff --git a/intTests/test_ghost/test.saw b/intTests/test_ghost/test.saw index 24b38a02dd..951a09423d 100644 --- a/intTests/test_ghost/test.saw +++ b/intTests/test_ghost/test.saw @@ -26,7 +26,7 @@ let f_spec (counter : Ghost) : CrucibleSetup () = do { }; let main : TopLevel () = do { - counter <- llvm_declare_ghost_state "counter"; + counter <- declare_ghost_state "counter"; m <- llvm_load_module "test.bc"; get_and_increment_ov <- llvm_unsafe_assume_spec m "get_and_increment" (get_and_increment_spec counter); diff --git a/intTests/test_ghost_branch_00/test.saw b/intTests/test_ghost_branch_00/test.saw index 78d1b77983..3fa4841445 100644 --- a/intTests/test_ghost_branch_00/test.saw +++ b/intTests/test_ghost_branch_00/test.saw @@ -25,7 +25,7 @@ let g_spec : CrucibleSetup () = do { }; let main : TopLevel () = do { - x <- llvm_declare_ghost_state "x"; + x <- declare_ghost_state "x"; m <- llvm_load_module "test.bc"; f_lt_ov <- llvm_unsafe_assume_spec m "f" (f_lt_spec x); f_ge_ov <- llvm_unsafe_assume_spec m "f" (f_ge_spec x); diff --git a/intTests/test_ghost_branch_01/test.saw b/intTests/test_ghost_branch_01/test.saw index 6d41b68b25..87b13e5ec1 100644 --- a/intTests/test_ghost_branch_01/test.saw +++ b/intTests/test_ghost_branch_01/test.saw @@ -28,7 +28,7 @@ let h_spec : CrucibleSetup () = do { }; let main : TopLevel () = do { - x <- llvm_declare_ghost_state "x"; + x <- declare_ghost_state "x"; m <- llvm_load_module "test.bc"; get_ov <- llvm_unsafe_assume_spec m "get" (get_spec x); f_ov <- llvm_unsafe_assume_spec m "f" (f_spec x); diff --git a/intTests/test_ghost_branch_02/test.saw b/intTests/test_ghost_branch_02/test.saw index 55f5eb8047..3efffb984d 100644 --- a/intTests/test_ghost_branch_02/test.saw +++ b/intTests/test_ghost_branch_02/test.saw @@ -21,7 +21,7 @@ let g_spec : CrucibleSetup () = do { }; let main : TopLevel () = do { - x <- llvm_declare_ghost_state "x"; + x <- declare_ghost_state "x"; m <- llvm_load_module "test.bc"; f_lt_ov <- llvm_unsafe_assume_spec m "f" (f_lt_spec x); f_ge_ov <- llvm_unsafe_assume_spec m "f" (f_ge_spec x); diff --git a/intTests/test_ghost_branch_03/test.saw b/intTests/test_ghost_branch_03/test.saw index 30f7373e5f..3f6bfd5393 100644 --- a/intTests/test_ghost_branch_03/test.saw +++ b/intTests/test_ghost_branch_03/test.saw @@ -28,7 +28,7 @@ let h_spec : CrucibleSetup () = do { }; let main : TopLevel () = do { - x <- llvm_declare_ghost_state "x"; + x <- declare_ghost_state "x"; m <- llvm_load_module "test.bc"; get_ov <- llvm_unsafe_assume_spec m "get" (get_spec x); f_ov <- llvm_unsafe_assume_spec m "f" (f_spec x); diff --git a/intTests/test_ghost_types_00/test.saw b/intTests/test_ghost_types_00/test.saw index f88faaef10..fc61fe0a86 100644 --- a/intTests/test_ghost_types_00/test.saw +++ b/intTests/test_ghost_types_00/test.saw @@ -23,7 +23,7 @@ let h_spec : CrucibleSetup () = do { }; let main : TopLevel () = do { - x <- llvm_declare_ghost_state "x"; + x <- declare_ghost_state "x"; m <- llvm_load_module "test.bc"; f_ov <- llvm_unsafe_assume_spec m "f" (f_spec x); // This spec should probably use a different variable, but doesn't: diff --git a/intTests/test_mir_ghost/Makefile b/intTests/test_mir_ghost/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_ghost/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_ghost/test.linked-mir.json b/intTests/test_mir_ghost/test.linked-mir.json new file mode 100644 index 0000000000..238971f5f7 --- /dev/null +++ b/intTests/test_mir_ghost/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::53e788cd45991c87"},"kind":"Constant"},"kind":"Call","pos":"test.rs:6:5: 6:11"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::53e788cd45991c87"},"kind":"Constant"},"kind":"Call","pos":"test.rs:7:5: 7:11"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::53e788cd45991c87"},"kind":"Constant"},"kind":"Call","pos":"test.rs:8:5: 8:11"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:9:2: 9:2"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}]},"name":"test/9f9d7d4c::example","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":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/9f9d7d4c190de41a::{{alloc}}[0]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"test.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/9f9d7d4c190de41a::{{alloc}}[1]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"test.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"test.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"}},"pos":"test.rs:2:20: 2:47","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/9f9d7d4c190de41a::{{alloc}}[2]","kind":"static_ref"},"ty":"ty::Ref::d0bd7bf253977b90"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:48"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:48","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::72bf0f6662028c6a"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:48"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:2:5: 2:48","rhs":{"akind":{"kind":"Array","ty":"ty::Adt::613f1953a8669d14"},"kind":"Aggregate","ops":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"}},"kind":"Move"}]}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:2:5: 2:48","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:2:5: 2:48"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"}},"kind":"Move"}],"cleanup":null,"destination":null,"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::906e67453a1bbab9"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !test.rs:2:5: 2:48"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":true,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Never::7199a9b06188843c"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}]},"name":"test/9f9d7d4c::next","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:23: 400:24","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Lt"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},"kind":"Move"},"discr_span":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","kind":"SwitchInt","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","switch_ty":"ty::bool","targets":["bb2","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"bool","size":1,"val":"1"},"ty":"ty::bool"},"kind":"Constant"}}}],"terminator":{"kind":"Goto","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","target":"bb3"}},"blockid":"bb1"},{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:52: 400:53","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:65: 400:66","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:70","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:70","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Gt"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"kind":"Move"}}}],"terminator":{"kind":"Goto","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","target":"bb3"}},"blockid":"bb2"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"kind":"Move"},"discr_span":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","kind":"SwitchInt","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","switch_ty":"ty::bool","targets":["bb6","bb4"],"values":["0"]}},"blockid":"bb3"},{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":true,"mut":{"kind":"Not"},"name":"_15","ty":"ty::Never::7199a9b06188843c"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/9f9d7d4c190de41a::{{alloc}}[3]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:33: 401:34","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/9f9d7d4c190de41a::{{alloc}}[2]","kind":"static_ref"},"ty":"ty::Ref::d0bd7bf253977b90"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb5"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35"}},"blockid":"bb4"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},"kind":"Move"}],"cleanup":null,"destination":null,"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::906e67453a1bbab9"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35"}},"blockid":"bb5"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:402:9: 402:10","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:21: 403:27","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:21: 403:27","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38","variant_index":0},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:40: 403:44","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:40: 403:44","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::675b2a8049aad652"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::Adt::45883e75bd5c5ca5"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":2,"kind":"Field","ty":"ty::Ref::913e2ff5487f7787"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:404:6: 404:6"}},"blockid":"bb6"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":true,"mut":{"kind":"Not"},"name":"_15","ty":"ty::Never::7199a9b06188843c"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}]},"name":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]","return_ty":"ty::Adt::ba5184b53bc36a4d","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::bf4d6d337c623aee"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:23: 328:24 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:23: 328:24 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:26: 328:33 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:26: 328:33 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Cast","op":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::b30b83d63051810b"},"kind":"Constant"},"ty":"ty::FnPtr::07cd89921cc84271","type":{"kind":"Pointer(ReifyFnPointer)"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:42: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:57: 347:58 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:57: 347:58 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::788a983faed72be6"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:42: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb0"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:58: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:68: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:83: 347:84 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:83: 347:84 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f532a620418c4246"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:68: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb1"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:84: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::4e8e6a61a1ceb622"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},"kind":"Move"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:86: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:86: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:33: 328:34 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:33: 328:34 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:329:10: 329:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}]},"name":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]","return_ty":"ty::Adt::613f1953a8669d14","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Arguments::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Arguments","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":48,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::Arguments::pieces","ty":"ty::Ref::675b2a8049aad652"},{"name":"core/73237d41::fmt::Arguments::fmt","ty":"ty::Adt::45883e75bd5c5ca5"},{"name":"core/73237d41::fmt::Arguments::args","ty":"ty::Ref::913e2ff5487f7787"}],"inhabited":true,"name":"core/73237d41::fmt::Arguments"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::ArgumentV1::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::ArgumentV1","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::ArgumentV1::value","ty":"ty::Ref::4e8e6a61a1ceb622"},{"name":"core/73237d41::fmt::ArgumentV1::formatter","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}],"inhabited":true,"name":"core/73237d41::fmt::ArgumentV1"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::rt::v1::Argument::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Argument","orig_substs":[],"repr_transparent":false,"size":56,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::rt::v1::Argument::position","ty":"ty::usize"},{"name":"core/73237d41::fmt::rt::v1::Argument::format","ty":"ty::Adt::ed8948c5d0b3a39f"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Argument"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::result::Result::_adt0f6d5765b4e92fb6[0]","orig_def_id":"core/73237d41::result::Result","orig_substs":["ty::Tuple::e93222e871854c41","ty::Adt::8d47b311e48cbf8f"],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[{"name":"core/73237d41::result::Result::Ok::0","ty":"ty::Tuple::e93222e871854c41"}],"inhabited":true,"name":"core/73237d41::result::Result::Ok"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::result::Result::Err::0","ty":"ty::Adt::8d47b311e48cbf8f"}],"inhabited":true,"name":"core/73237d41::result::Result::Err"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Formatter::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Formatter","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":64,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::Formatter::flags","ty":"ty::u32"},{"name":"core/73237d41::fmt::Formatter::fill","ty":"ty::char"},{"name":"core/73237d41::fmt::Formatter::align","ty":"ty::Adt::c4745d1cf6b33a46"},{"name":"core/73237d41::fmt::Formatter::width","ty":"ty::Adt::ba42a94c73933868"},{"name":"core/73237d41::fmt::Formatter::precision","ty":"ty::Adt::ba42a94c73933868"},{"name":"core/73237d41::fmt::Formatter::buf","ty":"ty::Ref::0cd866b4eb1c792b"}],"inhabited":true,"name":"core/73237d41::fmt::Formatter"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adta9d03177c2d4a99f[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::Ref::5f3877d5405402c5"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::Ref::5f3877d5405402c5"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Error::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::Error","orig_substs":[],"repr_transparent":false,"size":0,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[],"inhabited":true,"name":"core/73237d41::fmt::Error"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adtaffa7a8b1157c078[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::usize"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::rt::v1::FormatSpec::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::FormatSpec","orig_substs":[],"repr_transparent":false,"size":48,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::rt::v1::FormatSpec::fill","ty":"ty::char"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::align","ty":"ty::Adt::c4745d1cf6b33a46"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::flags","ty":"ty::u32"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::precision","ty":"ty::Adt::389b970f3565f26b"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::width","ty":"ty::Adt::389b970f3565f26b"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::FormatSpec"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::fmt::rt::v1::Alignment::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Alignment","orig_substs":[],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Left"},{"ctor_kind":{"kind":"Const"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Right"},{"ctor_kind":{"kind":"Const"},"discr":{"index":2,"kind":"Relative"},"discr_value":"2","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Center"},{"ctor_kind":{"kind":"Const"},"discr":{"index":3,"kind":"Relative"},"discr_value":"3","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Unknown"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::fmt::rt::v1::Count::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Count","orig_substs":[],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[{"name":"core/73237d41::fmt::rt::v1::Count::Is::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Is"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::fmt::rt::v1::Count::Param::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Param"},{"ctor_kind":{"kind":"Const"},"discr":{"index":2,"kind":"Relative"},"discr_value":"2","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Implied"}]}],"statics":[{"kind":"constant","mutable":false,"name":"test/9f9d7d4c190de41a::{{alloc}}[0]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[110,111,116,32,105,109,112,108,101,109,101,110,116,101,100,58,32]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"},{"kind":"constant","mutable":false,"name":"test/9f9d7d4c190de41a::{{alloc}}[1]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[84,104,105,115,32,115,104,111,117,108,100,32,98,101,32,111,118,101,114,114,105,100,100,101,110]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"},{"kind":"constant","mutable":false,"name":"test/9f9d7d4c190de41a::{{alloc}}[2]","rendered":{"element_ty":"ty::Adt::613f1953a8669d14","elements":[],"kind":"array"},"ty":"ty::Array::0e1a52ee2b2d3e97"},{"kind":"constant","mutable":false,"name":"test/9f9d7d4c190de41a::{{alloc}}[3]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[105,110,118,97,108,105,100,32,97,114,103,115]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"}],"vtables":[],"traits":[{"items":[{"item_id":"core/73237d41::fmt::Write::write_str","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::Ref::fb1cfdc5725cd03b"],"output":"ty::Adt::30ed5848b4f625b6"}},{"item_id":"core/73237d41::fmt::Write::write_char","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::char"],"output":"ty::Adt::30ed5848b4f625b6"}},{"item_id":"core/73237d41::fmt::Write::write_fmt","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::Adt::ba5184b53bc36a4d"],"output":"ty::Adt::30ed5848b4f625b6"}}],"name":"core/73237d41::fmt::Write::_trait3e5b0354795cc029[0]"}],"intrinsics":[{"inst":{"def_id":"test/9f9d7d4c::example","kind":"Item","substs":[]},"name":"test/9f9d7d4c::example"},{"inst":{"def_id":"test/9f9d7d4c::next","kind":"Item","substs":[]},"name":"test/9f9d7d4c::next"},{"inst":{"def_id":"core/73237d41::fmt::{impl#4}::new_v1","kind":"Item","substs":["nonty::Lifetime"]},"name":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]"},{"inst":{"def_id":"core/73237d41::fmt::{impl#3}::new_display","kind":"Item","substs":["nonty::Lifetime","ty::Adt::ba5184b53bc36a4d"]},"name":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]"},{"inst":{"def_id":"core/73237d41::panicking::panic_fmt","kind":"Item","substs":[]},"name":"core/73237d41::panicking::panic_fmt"},{"inst":{"def_id":"core/73237d41::intrinsics::{extern#0}::transmute","kind":"Intrinsic","substs":["ty::FnPtr::07cd89921cc84271","ty::FnPtr::bd6bee7b1f95b7bf"]},"name":"core/73237d41::intrinsics::{extern#0}::transmute::_inst82602b44b15ef1cb[0]"},{"inst":{"def_id":"core/73237d41::fmt::{impl#7}::fmt","kind":"Item","substs":["nonty::Lifetime"]},"name":"core/73237d41::fmt::{impl#7}::fmt::_instbd21306cbe4f0b9b[0]"},{"inst":{"def_id":"core/73237d41::intrinsics::{extern#0}::transmute","kind":"Intrinsic","substs":["ty::Ref::bf4d6d337c623aee","ty::Ref::4e8e6a61a1ceb622"]},"name":"core/73237d41::intrinsics::{extern#0}::transmute::_inst79e1dbb43599bccf[0]"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::FnDef::53e788cd45991c87","ty":{"defid":"test/9f9d7d4c::next","kind":"FnDef"}},{"name":"ty::Never::7199a9b06188843c","ty":{"kind":"Never"}},{"name":"ty::Adt::ba5184b53bc36a4d","ty":{"kind":"Adt","name":"core/73237d41::fmt::Arguments::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Arguments","substs":["nonty::Lifetime"]}},{"name":"ty::str","ty":{"kind":"Str"}},{"name":"ty::Ref::fb1cfdc5725cd03b","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::str"}},{"name":"ty::Slice::563a94fdd2fd2b33","ty":{"kind":"Slice","ty":"ty::Ref::fb1cfdc5725cd03b"}},{"name":"ty::Ref::675b2a8049aad652","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::563a94fdd2fd2b33"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::e5bd840a2dafa04a","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"ty":"ty::Ref::fb1cfdc5725cd03b"}},{"name":"ty::Ref::c2a5dcbb98af2a61","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::e5bd840a2dafa04a"}},{"name":"ty::Adt::613f1953a8669d14","ty":{"kind":"Adt","name":"core/73237d41::fmt::ArgumentV1::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::ArgumentV1","substs":["nonty::Lifetime"]}},{"name":"ty::Slice::818a2c6d5f962f99","ty":{"kind":"Slice","ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::913e2ff5487f7787","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::818a2c6d5f962f99"}},{"name":"ty::Array::6167cd8fdeb01e06","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::41f3f8f95d02c3e9","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::6167cd8fdeb01e06"}},{"name":"ty::Ref::bf4d6d337c623aee","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Adt::ba5184b53bc36a4d"}},{"name":"ty::Array::0e1a52ee2b2d3e97","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::d0bd7bf253977b90","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::0e1a52ee2b2d3e97"}},{"name":"ty::FnDef::76afb566734aff77","ty":{"defid":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]","kind":"FnDef"}},{"name":"ty::FnDef::72bf0f6662028c6a","ty":{"defid":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]","kind":"FnDef"}},{"name":"ty::FnDef::906e67453a1bbab9","ty":{"defid":"core/73237d41::panicking::panic_fmt","kind":"FnDef"}},{"name":"ty::Adt::afb4c9f4ce8cdadf","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Argument::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Argument","substs":[]}},{"name":"ty::Slice::26b8a0a5e2b22aa9","ty":{"kind":"Slice","ty":"ty::Adt::afb4c9f4ce8cdadf"}},{"name":"ty::Ref::5f3877d5405402c5","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::26b8a0a5e2b22aa9"}},{"name":"ty::Adt::45883e75bd5c5ca5","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adta9d03177c2d4a99f[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::Ref::5f3877d5405402c5"]}},{"name":"ty::Foreign::66d9923797cfc204","ty":{"kind":"Foreign"}},{"name":"ty::Ref::4e8e6a61a1ceb622","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Foreign::66d9923797cfc204"}},{"name":"ty::Adt::ad5a554022507816","ty":{"kind":"Adt","name":"core/73237d41::fmt::Formatter::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Formatter","substs":["nonty::Lifetime"]}},{"name":"ty::Ref::7984c7d8fa40d865","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::Adt::ad5a554022507816"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::Adt::8d47b311e48cbf8f","ty":{"kind":"Adt","name":"core/73237d41::fmt::Error::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::Error","substs":[]}},{"name":"ty::Adt::30ed5848b4f625b6","ty":{"kind":"Adt","name":"core/73237d41::result::Result::_adt0f6d5765b4e92fb6[0]","orig_def_id":"core/73237d41::result::Result","substs":["ty::Tuple::e93222e871854c41","ty::Adt::8d47b311e48cbf8f"]}},{"name":"ty::FnPtr::bd6bee7b1f95b7bf","ty":{"kind":"FnPtr","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::4e8e6a61a1ceb622","ty::Ref::7984c7d8fa40d865"],"output":"ty::Adt::30ed5848b4f625b6"}}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::FnPtr::07cd89921cc84271","ty":{"kind":"FnPtr","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::bf4d6d337c623aee","ty::Ref::7984c7d8fa40d865"],"output":"ty::Adt::30ed5848b4f625b6"}}},{"name":"ty::FnDef::b30b83d63051810b","ty":{"defid":"core/73237d41::fmt::{impl#7}::fmt::_instbd21306cbe4f0b9b[0]","kind":"FnDef"}},{"name":"ty::FnDef::788a983faed72be6","ty":{"defid":"core/73237d41::intrinsics::{extern#0}::transmute::_inst82602b44b15ef1cb[0]","kind":"FnDef"}},{"name":"ty::FnDef::f532a620418c4246","ty":{"defid":"core/73237d41::intrinsics::{extern#0}::transmute::_inst79e1dbb43599bccf[0]","kind":"FnDef"}},{"name":"ty::Adt::ed8948c5d0b3a39f","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::FormatSpec::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::FormatSpec","substs":[]}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}},{"name":"ty::char","ty":{"kind":"Char"}},{"name":"ty::Adt::c4745d1cf6b33a46","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Alignment::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Alignment","substs":[]}},{"name":"ty::Adt::ba42a94c73933868","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adtaffa7a8b1157c078[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::usize"]}},{"name":"ty::Dynamic::08a22e65af9638be","ty":{"kind":"Dynamic","predicates":[{"kind":"Trait","substs":[],"trait":"core/73237d41::fmt::Write"}],"trait_id":"core/73237d41::fmt::Write::_trait3e5b0354795cc029[0]"}},{"name":"ty::Ref::0cd866b4eb1c792b","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::Dynamic::08a22e65af9638be"}},{"name":"ty::Adt::389b970f3565f26b","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Count::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Count","substs":[]}}],"roots":["test/9f9d7d4c::next","test/9f9d7d4c::example"]} \ No newline at end of file diff --git a/intTests/test_mir_ghost/test.rs b/intTests/test_mir_ghost/test.rs new file mode 100644 index 0000000000..fafa13669c --- /dev/null +++ b/intTests/test_mir_ghost/test.rs @@ -0,0 +1,9 @@ +pub fn next() -> u32 { + unimplemented!("This should be overridden") +} + +pub fn example() -> u32 { + next(); + next(); + next() +} diff --git a/intTests/test_mir_ghost/test.saw b/intTests/test_mir_ghost/test.saw new file mode 100644 index 0000000000..01046b4bcc --- /dev/null +++ b/intTests/test_mir_ghost/test.saw @@ -0,0 +1,28 @@ +enable_experimental; + +let next_spec counter = do { + n <- mir_fresh_var "n" mir_u32; + mir_ghost_value counter n; + + mir_execute_func []; + + mir_ghost_value counter {{n+1}}; + mir_return (mir_term {{n}}); +}; + +let example_spec counter = do { + n <- mir_fresh_var "nm" mir_u32; + mir_precond {{n < 2}}; + mir_ghost_value counter n; + + mir_execute_func []; + + mir_ghost_value counter {{n+3}}; + mir_return (mir_term {{n+2}}); +}; + +counter <- declare_ghost_state "ctr"; +m <- mir_load_module "test.linked-mir.json"; + +next <- mir_unsafe_assume_spec m "test::next" (next_spec counter); +mir_verify m "test::example" [next] false (example_spec counter) z3; diff --git a/intTests/test_mir_ghost/test.sh b/intTests/test_mir_ghost/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_ghost/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/intTests/test_mir_ghost_symbolic_branch/Makefile b/intTests/test_mir_ghost_symbolic_branch/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_ghost_symbolic_branch/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_ghost_symbolic_branch/test.linked-mir.json b/intTests/test_mir_ghost_symbolic_branch/test.linked-mir.json new file mode 100644 index 0000000000..deea148368 --- /dev/null +++ b/intTests/test_mir_ghost_symbolic_branch/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"pos":"test.rs:5:8: 5:9","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}},"kind":"Copy"}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"kind":"Move"},"discr_span":"test.rs:5:8: 5:9 !test.rs:5:8: 5:9","kind":"SwitchInt","pos":"test.rs:5:8: 5:9 !test.rs:5:8: 5:9","switch_ty":"ty::bool","targets":["bb2","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"args":[{"data":{"rendered":{"kind":"uint","size":4,"val":"27"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::140cf1f14525dfe1"},"kind":"Constant"},"kind":"Call","pos":"test.rs:6:9: 6:14"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"args":[{"data":{"rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::140cf1f14525dfe1"},"kind":"Constant"},"kind":"Call","pos":"test.rs:8:9: 8:14"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:10:2: 10:2"}},"blockid":"bb3"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}]},"name":"test/2c9d3c4c::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:2:21: 2:21"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/2c9d3c4c::f","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/2c9d3c4c::g","kind":"Item","substs":[]},"name":"test/2c9d3c4c::g"},{"inst":{"def_id":"test/2c9d3c4c::f","kind":"Item","substs":[]},"name":"test/2c9d3c4c::f"}],"tys":[{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::FnDef::140cf1f14525dfe1","ty":{"defid":"test/2c9d3c4c::f","kind":"FnDef"}},{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}}],"roots":["test/2c9d3c4c::f","test/2c9d3c4c::g"]} \ No newline at end of file diff --git a/intTests/test_mir_ghost_symbolic_branch/test.rs b/intTests/test_mir_ghost_symbolic_branch/test.rs new file mode 100644 index 0000000000..6a3d06e7fd --- /dev/null +++ b/intTests/test_mir_ghost_symbolic_branch/test.rs @@ -0,0 +1,10 @@ +// Meant to be overridden +pub fn f(_x: u32) {} + +pub fn g(b: bool) { + if b { + f(27) + } else { + f(42) + } +} diff --git a/intTests/test_mir_ghost_symbolic_branch/test.saw b/intTests/test_mir_ghost_symbolic_branch/test.saw new file mode 100644 index 0000000000..e35b0652cc --- /dev/null +++ b/intTests/test_mir_ghost_symbolic_branch/test.saw @@ -0,0 +1,24 @@ +enable_experimental; + +m <- mir_load_module "test.linked-mir.json"; + +g <- declare_ghost_state "g"; + +let f_spec = do { + x <- mir_fresh_var "x" mir_u32; + + mir_execute_func [mir_term x]; + + mir_ghost_value g x; +}; + +let g_spec = do { + b <- mir_fresh_var "b" mir_bool; + + mir_execute_func [mir_term b]; + + mir_ghost_value g ({{ if b then 27 else 42 : [32] }}); +}; + +f_ov <- mir_unsafe_assume_spec m "test::f" f_spec; +mir_verify m "test::g" [f_ov] false g_spec z3; diff --git a/intTests/test_mir_ghost_symbolic_branch/test.sh b/intTests/test_mir_ghost_symbolic_branch/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_ghost_symbolic_branch/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md index 1316e3e6ba..8aafd8075b 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -35,6 +35,8 @@ * Add `"slice"` and `"slice range"` `setup value`s representing slices in MIR verification. Attempting to use these in LLVM or JVM verification will raise an error. +* The `SAW/create ghost variable` command and the associated + `ghost variable value` value are now supported with JVM and MIR verification. ## 1.0.0 -- 2023-06-26 diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index 4892e5c863..b2434fd8fc 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -38,6 +38,8 @@ variable. This function is currently only supported with LLVM and MIR verification, and using this function with JVM verification will raise an error. +* The `create_ghost_variable()` and `ghost_value()` functions are now supported + with JVM and MIR verification. ## 1.0.1 -- YYYY-MM-DD diff --git a/saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json new file mode 100644 index 0000000000..f09a6a8147 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::ae5488df1dc4e585"},"kind":"Constant"},"kind":"Call","pos":"mir_ghost.rs:6:5: 6:11"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::ae5488df1dc4e585"},"kind":"Constant"},"kind":"Call","pos":"mir_ghost.rs:7:5: 7:11"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::ae5488df1dc4e585"},"kind":"Constant"},"kind":"Call","pos":"mir_ghost.rs:8:5: 8:11"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_ghost.rs:9:2: 9:2"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}]},"name":"mir_ghost/150ed446::example","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":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[0]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[1]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[2]","kind":"static_ref"},"ty":"ty::Ref::d0bd7bf253977b90"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::72bf0f6662028c6a"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"akind":{"kind":"Array","ty":"ty::Adt::613f1953a8669d14"},"kind":"Aggregate","ops":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"}},"kind":"Move"}]}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"}},"kind":"Move"}],"cleanup":null,"destination":null,"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::906e67453a1bbab9"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":true,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Never::7199a9b06188843c"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}]},"name":"mir_ghost/150ed446::next","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::bf4d6d337c623aee"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:23: 328:24 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:23: 328:24 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:26: 328:33 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:26: 328:33 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Cast","op":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::b30b83d63051810b"},"kind":"Constant"},"ty":"ty::FnPtr::07cd89921cc84271","type":{"kind":"Pointer(ReifyFnPointer)"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:42: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:57: 347:58 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:57: 347:58 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::788a983faed72be6"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:42: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb0"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:58: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:68: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:83: 347:84 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:83: 347:84 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f532a620418c4246"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:68: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb1"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:84: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::4e8e6a61a1ceb622"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},"kind":"Move"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:86: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:86: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:33: 328:34 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:33: 328:34 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:329:10: 329:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}]},"name":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]","return_ty":"ty::Adt::613f1953a8669d14","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:23: 400:24","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Lt"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},"kind":"Move"},"discr_span":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","kind":"SwitchInt","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","switch_ty":"ty::bool","targets":["bb2","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"bool","size":1,"val":"1"},"ty":"ty::bool"},"kind":"Constant"}}}],"terminator":{"kind":"Goto","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","target":"bb3"}},"blockid":"bb1"},{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:52: 400:53","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:65: 400:66","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:70","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:70","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Gt"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"kind":"Move"}}}],"terminator":{"kind":"Goto","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","target":"bb3"}},"blockid":"bb2"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"kind":"Move"},"discr_span":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","kind":"SwitchInt","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","switch_ty":"ty::bool","targets":["bb6","bb4"],"values":["0"]}},"blockid":"bb3"},{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":true,"mut":{"kind":"Not"},"name":"_15","ty":"ty::Never::7199a9b06188843c"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[3]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:33: 401:34","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[2]","kind":"static_ref"},"ty":"ty::Ref::d0bd7bf253977b90"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb5"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35"}},"blockid":"bb4"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},"kind":"Move"}],"cleanup":null,"destination":null,"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::906e67453a1bbab9"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35"}},"blockid":"bb5"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:402:9: 402:10","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:21: 403:27","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:21: 403:27","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38","variant_index":0},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:40: 403:44","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:40: 403:44","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::675b2a8049aad652"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::Adt::45883e75bd5c5ca5"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":2,"kind":"Field","ty":"ty::Ref::913e2ff5487f7787"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:404:6: 404:6"}},"blockid":"bb6"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":true,"mut":{"kind":"Not"},"name":"_15","ty":"ty::Never::7199a9b06188843c"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}]},"name":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]","return_ty":"ty::Adt::ba5184b53bc36a4d","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Arguments::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Arguments","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":48,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::Arguments::pieces","ty":"ty::Ref::675b2a8049aad652"},{"name":"core/73237d41::fmt::Arguments::fmt","ty":"ty::Adt::45883e75bd5c5ca5"},{"name":"core/73237d41::fmt::Arguments::args","ty":"ty::Ref::913e2ff5487f7787"}],"inhabited":true,"name":"core/73237d41::fmt::Arguments"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::ArgumentV1::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::ArgumentV1","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::ArgumentV1::value","ty":"ty::Ref::4e8e6a61a1ceb622"},{"name":"core/73237d41::fmt::ArgumentV1::formatter","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}],"inhabited":true,"name":"core/73237d41::fmt::ArgumentV1"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adta9d03177c2d4a99f[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::Ref::5f3877d5405402c5"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::Ref::5f3877d5405402c5"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Error::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::Error","orig_substs":[],"repr_transparent":false,"size":0,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[],"inhabited":true,"name":"core/73237d41::fmt::Error"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::result::Result::_adt0f6d5765b4e92fb6[0]","orig_def_id":"core/73237d41::result::Result","orig_substs":["ty::Tuple::e93222e871854c41","ty::Adt::8d47b311e48cbf8f"],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[{"name":"core/73237d41::result::Result::Ok::0","ty":"ty::Tuple::e93222e871854c41"}],"inhabited":true,"name":"core/73237d41::result::Result::Ok"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::result::Result::Err::0","ty":"ty::Adt::8d47b311e48cbf8f"}],"inhabited":true,"name":"core/73237d41::result::Result::Err"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::rt::v1::Argument::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Argument","orig_substs":[],"repr_transparent":false,"size":56,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::rt::v1::Argument::position","ty":"ty::usize"},{"name":"core/73237d41::fmt::rt::v1::Argument::format","ty":"ty::Adt::ed8948c5d0b3a39f"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Argument"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Formatter::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Formatter","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":64,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::Formatter::flags","ty":"ty::u32"},{"name":"core/73237d41::fmt::Formatter::fill","ty":"ty::char"},{"name":"core/73237d41::fmt::Formatter::align","ty":"ty::Adt::c4745d1cf6b33a46"},{"name":"core/73237d41::fmt::Formatter::width","ty":"ty::Adt::ba42a94c73933868"},{"name":"core/73237d41::fmt::Formatter::precision","ty":"ty::Adt::ba42a94c73933868"},{"name":"core/73237d41::fmt::Formatter::buf","ty":"ty::Ref::0cd866b4eb1c792b"}],"inhabited":true,"name":"core/73237d41::fmt::Formatter"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::rt::v1::FormatSpec::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::FormatSpec","orig_substs":[],"repr_transparent":false,"size":48,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::rt::v1::FormatSpec::fill","ty":"ty::char"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::align","ty":"ty::Adt::c4745d1cf6b33a46"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::flags","ty":"ty::u32"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::precision","ty":"ty::Adt::389b970f3565f26b"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::width","ty":"ty::Adt::389b970f3565f26b"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::FormatSpec"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::fmt::rt::v1::Alignment::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Alignment","orig_substs":[],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Left"},{"ctor_kind":{"kind":"Const"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Right"},{"ctor_kind":{"kind":"Const"},"discr":{"index":2,"kind":"Relative"},"discr_value":"2","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Center"},{"ctor_kind":{"kind":"Const"},"discr":{"index":3,"kind":"Relative"},"discr_value":"3","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Unknown"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adtaffa7a8b1157c078[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::usize"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::fmt::rt::v1::Count::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Count","orig_substs":[],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[{"name":"core/73237d41::fmt::rt::v1::Count::Is::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Is"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::fmt::rt::v1::Count::Param::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Param"},{"ctor_kind":{"kind":"Const"},"discr":{"index":2,"kind":"Relative"},"discr_value":"2","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Implied"}]}],"statics":[{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[0]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[110,111,116,32,105,109,112,108,101,109,101,110,116,101,100,58,32]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"},{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[1]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[84,104,105,115,32,115,104,111,117,108,100,32,98,101,32,111,118,101,114,114,105,100,100,101,110]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"},{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[2]","rendered":{"element_ty":"ty::Adt::613f1953a8669d14","elements":[],"kind":"array"},"ty":"ty::Array::0e1a52ee2b2d3e97"},{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[3]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[105,110,118,97,108,105,100,32,97,114,103,115]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"}],"vtables":[],"traits":[{"items":[{"item_id":"core/73237d41::fmt::Write::write_str","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::Ref::fb1cfdc5725cd03b"],"output":"ty::Adt::30ed5848b4f625b6"}},{"item_id":"core/73237d41::fmt::Write::write_char","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::char"],"output":"ty::Adt::30ed5848b4f625b6"}},{"item_id":"core/73237d41::fmt::Write::write_fmt","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::Adt::ba5184b53bc36a4d"],"output":"ty::Adt::30ed5848b4f625b6"}}],"name":"core/73237d41::fmt::Write::_trait3e5b0354795cc029[0]"}],"intrinsics":[{"inst":{"def_id":"mir_ghost/150ed446::example","kind":"Item","substs":[]},"name":"mir_ghost/150ed446::example"},{"inst":{"def_id":"mir_ghost/150ed446::next","kind":"Item","substs":[]},"name":"mir_ghost/150ed446::next"},{"inst":{"def_id":"core/73237d41::fmt::{impl#3}::new_display","kind":"Item","substs":["nonty::Lifetime","ty::Adt::ba5184b53bc36a4d"]},"name":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]"},{"inst":{"def_id":"core/73237d41::fmt::{impl#4}::new_v1","kind":"Item","substs":["nonty::Lifetime"]},"name":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]"},{"inst":{"def_id":"core/73237d41::panicking::panic_fmt","kind":"Item","substs":[]},"name":"core/73237d41::panicking::panic_fmt"},{"inst":{"def_id":"core/73237d41::intrinsics::{extern#0}::transmute","kind":"Intrinsic","substs":["ty::Ref::bf4d6d337c623aee","ty::Ref::4e8e6a61a1ceb622"]},"name":"core/73237d41::intrinsics::{extern#0}::transmute::_inst79e1dbb43599bccf[0]"},{"inst":{"def_id":"core/73237d41::intrinsics::{extern#0}::transmute","kind":"Intrinsic","substs":["ty::FnPtr::07cd89921cc84271","ty::FnPtr::bd6bee7b1f95b7bf"]},"name":"core/73237d41::intrinsics::{extern#0}::transmute::_inst82602b44b15ef1cb[0]"},{"inst":{"def_id":"core/73237d41::fmt::{impl#7}::fmt","kind":"Item","substs":["nonty::Lifetime"]},"name":"core/73237d41::fmt::{impl#7}::fmt::_instbd21306cbe4f0b9b[0]"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::FnDef::ae5488df1dc4e585","ty":{"defid":"mir_ghost/150ed446::next","kind":"FnDef"}},{"name":"ty::Never::7199a9b06188843c","ty":{"kind":"Never"}},{"name":"ty::Adt::ba5184b53bc36a4d","ty":{"kind":"Adt","name":"core/73237d41::fmt::Arguments::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Arguments","substs":["nonty::Lifetime"]}},{"name":"ty::str","ty":{"kind":"Str"}},{"name":"ty::Ref::fb1cfdc5725cd03b","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::str"}},{"name":"ty::Slice::563a94fdd2fd2b33","ty":{"kind":"Slice","ty":"ty::Ref::fb1cfdc5725cd03b"}},{"name":"ty::Ref::675b2a8049aad652","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::563a94fdd2fd2b33"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::e5bd840a2dafa04a","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"ty":"ty::Ref::fb1cfdc5725cd03b"}},{"name":"ty::Ref::c2a5dcbb98af2a61","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::e5bd840a2dafa04a"}},{"name":"ty::Adt::613f1953a8669d14","ty":{"kind":"Adt","name":"core/73237d41::fmt::ArgumentV1::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::ArgumentV1","substs":["nonty::Lifetime"]}},{"name":"ty::Slice::818a2c6d5f962f99","ty":{"kind":"Slice","ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::913e2ff5487f7787","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::818a2c6d5f962f99"}},{"name":"ty::Array::6167cd8fdeb01e06","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::41f3f8f95d02c3e9","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::6167cd8fdeb01e06"}},{"name":"ty::Ref::bf4d6d337c623aee","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Adt::ba5184b53bc36a4d"}},{"name":"ty::Array::0e1a52ee2b2d3e97","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::d0bd7bf253977b90","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::0e1a52ee2b2d3e97"}},{"name":"ty::FnDef::76afb566734aff77","ty":{"defid":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]","kind":"FnDef"}},{"name":"ty::FnDef::72bf0f6662028c6a","ty":{"defid":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]","kind":"FnDef"}},{"name":"ty::FnDef::906e67453a1bbab9","ty":{"defid":"core/73237d41::panicking::panic_fmt","kind":"FnDef"}},{"name":"ty::Adt::afb4c9f4ce8cdadf","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Argument::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Argument","substs":[]}},{"name":"ty::Slice::26b8a0a5e2b22aa9","ty":{"kind":"Slice","ty":"ty::Adt::afb4c9f4ce8cdadf"}},{"name":"ty::Ref::5f3877d5405402c5","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::26b8a0a5e2b22aa9"}},{"name":"ty::Adt::45883e75bd5c5ca5","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adta9d03177c2d4a99f[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::Ref::5f3877d5405402c5"]}},{"name":"ty::Foreign::66d9923797cfc204","ty":{"kind":"Foreign"}},{"name":"ty::Ref::4e8e6a61a1ceb622","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Foreign::66d9923797cfc204"}},{"name":"ty::Adt::ad5a554022507816","ty":{"kind":"Adt","name":"core/73237d41::fmt::Formatter::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Formatter","substs":["nonty::Lifetime"]}},{"name":"ty::Ref::7984c7d8fa40d865","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::Adt::ad5a554022507816"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::Adt::8d47b311e48cbf8f","ty":{"kind":"Adt","name":"core/73237d41::fmt::Error::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::Error","substs":[]}},{"name":"ty::Adt::30ed5848b4f625b6","ty":{"kind":"Adt","name":"core/73237d41::result::Result::_adt0f6d5765b4e92fb6[0]","orig_def_id":"core/73237d41::result::Result","substs":["ty::Tuple::e93222e871854c41","ty::Adt::8d47b311e48cbf8f"]}},{"name":"ty::FnPtr::bd6bee7b1f95b7bf","ty":{"kind":"FnPtr","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::4e8e6a61a1ceb622","ty::Ref::7984c7d8fa40d865"],"output":"ty::Adt::30ed5848b4f625b6"}}},{"name":"ty::FnPtr::07cd89921cc84271","ty":{"kind":"FnPtr","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::bf4d6d337c623aee","ty::Ref::7984c7d8fa40d865"],"output":"ty::Adt::30ed5848b4f625b6"}}},{"name":"ty::FnDef::b30b83d63051810b","ty":{"defid":"core/73237d41::fmt::{impl#7}::fmt::_instbd21306cbe4f0b9b[0]","kind":"FnDef"}},{"name":"ty::FnDef::788a983faed72be6","ty":{"defid":"core/73237d41::intrinsics::{extern#0}::transmute::_inst82602b44b15ef1cb[0]","kind":"FnDef"}},{"name":"ty::FnDef::f532a620418c4246","ty":{"defid":"core/73237d41::intrinsics::{extern#0}::transmute::_inst79e1dbb43599bccf[0]","kind":"FnDef"}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}},{"name":"ty::Adt::ed8948c5d0b3a39f","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::FormatSpec::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::FormatSpec","substs":[]}},{"name":"ty::char","ty":{"kind":"Char"}},{"name":"ty::Adt::c4745d1cf6b33a46","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Alignment::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Alignment","substs":[]}},{"name":"ty::Adt::ba42a94c73933868","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adtaffa7a8b1157c078[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::usize"]}},{"name":"ty::Dynamic::08a22e65af9638be","ty":{"kind":"Dynamic","predicates":[{"kind":"Trait","substs":[],"trait":"core/73237d41::fmt::Write"}],"trait_id":"core/73237d41::fmt::Write::_trait3e5b0354795cc029[0]"}},{"name":"ty::Ref::0cd866b4eb1c792b","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::Dynamic::08a22e65af9638be"}},{"name":"ty::Adt::389b970f3565f26b","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Count::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Count","substs":[]}}],"roots":["mir_ghost/150ed446::next","mir_ghost/150ed446::example"]} \ No newline at end of file diff --git a/saw-remote-api/python/tests/saw/test-files/mir_ghost.rs b/saw-remote-api/python/tests/saw/test-files/mir_ghost.rs new file mode 100644 index 0000000000..fafa13669c --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_ghost.rs @@ -0,0 +1,9 @@ +pub fn next() -> u32 { + unimplemented!("This should be overridden") +} + +pub fn example() -> u32 { + next(); + next(); + next() +} diff --git a/saw-remote-api/python/tests/saw/test_mir_ghost.py b/saw-remote-api/python/tests/saw/test_mir_ghost.py new file mode 100644 index 0000000000..3d4e388cad --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_mir_ghost.py @@ -0,0 +1,53 @@ +import unittest +from pathlib import Path + +from saw_client import * +from saw_client.crucible import cry_f +from saw_client.mir import Contract, GhostVariable, u32 + + +class NextContract(Contract): + def __init__(self, counter: GhostVariable) -> None: + super().__init__() + self.counter = counter + + def specification(self) -> None: + n = self.fresh_var(u32, 'n') + self.ghost_value(self.counter, n) + + self.execute_func() + + self.ghost_value(self.counter, cry_f('{n} + 1')) + self.returns(n) + + +class ExampleContract(Contract): + def __init__(self, counter: GhostVariable) -> None: + super().__init__() + self.counter = counter + + def specification(self) -> None: + n = self.fresh_var(u32, 'n') + self.precondition_f('{n} < 2') + self.ghost_value(self.counter, n) + + self.execute_func() + self.ghost_value(self.counter, cry_f('{n} + 3')) + self.returns_f('{n} + 2') + + +class MIRGhostTest(unittest.TestCase): + def test_mir_ghost(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults()) + json_name = str(Path('tests', 'saw', 'test-files', 'mir_ghost.linked-mir.json')) + mod = mir_load_module(json_name) + + counter = create_ghost_variable('ctr'); + next_ov = mir_assume(mod, 'mir_ghost::next', NextContract(counter)) + example_result = mir_verify(mod, 'mir_ghost::example', ExampleContract(counter), lemmas=[next_ov]) + self.assertIs(example_result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index c601974f4a..8262e46c81 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -26,7 +26,7 @@ import qualified Data.Map as Map import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) import qualified Lang.Crucible.JVM as CJ -import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) +import qualified SAWScript.Crucible.Common.MethodSpec as MS import SAWScript.Crucible.JVM.Builtins ( jvm_alloc_array, jvm_alloc_object, @@ -35,6 +35,7 @@ import SAWScript.Crucible.JVM.Builtins jvm_static_field_is, jvm_execute_func, jvm_fresh_var, + jvm_ghost_value, jvm_postcond, jvm_precond, jvm_return ) @@ -56,10 +57,11 @@ import SAWServer import SAWServer.Data.Contract ( PointsTo(PointsTo), PointsToBitfield, + GhostValue(GhostValue), Allocated(Allocated), ContractVar(ContractVar), - Contract(preVars, preConds, preAllocated, prePointsTos, prePointsToBitfields, - argumentVals, postVars, postConds, postAllocated, postPointsTos, postPointsToBitfields, + Contract(preVars, preConds, preAllocated, preGhostValues, prePointsTos, prePointsToBitfields, + argumentVals, postVars, postConds, postAllocated, postGhostValues, postPointsTos, postPointsToBitfields, returnVal) ) import SAWServer.Data.SetupValue () import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp) @@ -82,28 +84,29 @@ instance Doc.DescribedMethod StartJVMSetupParams OK where ] resultFieldDescription = [] -newtype ServerSetupVal = Val (SetupValue CJ.JVM) +newtype ServerSetupVal = Val (MS.SetupValue CJ.JVM) compileJVMContract :: (FilePath -> IO ByteString) -> BuiltinContext -> + Map ServerName MS.GhostGlobal -> CryptolEnv -> Contract JavaType (P.Expr P.PName) -> JVMSetupM () -compileJVMContract fileReader bic cenv0 c = +compileJVMContract fileReader bic ghostEnv cenv0 c = do allocsPre <- mapM setupAlloc (preAllocated c) (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) mapM_ (\p -> getTypedTerm cenvPre p >>= jvm_precond) (preConds c) mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) mapM_ setupPointsToBitfields (prePointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= jvm_execute_func allocsPost <- mapM setupAlloc (postAllocated c) (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) mapM_ (\p -> getTypedTerm cenvPost p >>= jvm_postcond) (postConds c) mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) mapM_ setupPointsToBitfields (postPointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) case returnVal c of Just v -> getSetupVal (envPost, cenvPost) v >>= jvm_return Nothing -> return () @@ -149,7 +152,10 @@ compileJVMContract fileReader bic cenv0 c = setupPointsToBitfields _ = JVMSetupM $ fail "Points-to-bitfield not supported in JVM API." - --setupGhostValue _ _ _ = fail "Ghost values not supported yet in JVM API." + setupGhostValue genv cenv (GhostValue serverName e) = + do g <- resolve genv serverName + t <- getTypedTerm cenv e + jvm_ghost_value g t resolve :: Map ServerName a -> ServerName -> JVMSetupM a resolve env name = diff --git a/saw-remote-api/src/SAWServer/JVMVerify.hs b/saw-remote-api/src/SAWServer/JVMVerify.hs index f7c97654ed..293d424e79 100644 --- a/saw-remote-api/src/SAWServer/JVMVerify.hs +++ b/saw-remote-api/src/SAWServer/JVMVerify.hs @@ -9,6 +9,7 @@ module SAWServer.JVMVerify import Prelude hiding (mod) import Control.Lens +import qualified Data.Map as Map import SAWScript.Crucible.JVM.Builtins ( jvm_unsafe_assume_spec, jvm_verify ) @@ -26,6 +27,7 @@ import SAWServer pushTask, dropTask, setServerVal, + getGhosts, getJVMClass, getJVMMethodSpecIR ) import SAWServer.CryptolExpression (getCryptolExpr) @@ -51,7 +53,8 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc let bic = view sawBIC state cenv = rwCryptol (view sawTopLevelRW state) fileReader <- Argo.getFileReader - setup <- compileJVMContract fileReader bic cenv <$> traverse getCryptolExpr contract + ghostEnv <- Map.fromList <$> getGhosts + setup <- compileJVMContract fileReader bic ghostEnv cenv <$> traverse getCryptolExpr contract res <- case mode of VerifyContract -> do lemmas <- mapM getJVMMethodSpecIR lemmaNames diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs index a1ce2f07d3..b6cf3555df 100644 --- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs @@ -31,6 +31,7 @@ import SAWScript.Crucible.MIR.Builtins mir_fresh_expanded_value, mir_fresh_var, mir_execute_func, + mir_ghost_value, mir_load_module, mir_points_to, mir_postcond, @@ -58,10 +59,11 @@ import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCE import SAWServer.Data.Contract ( PointsTo(PointsTo), PointsToBitfield, + GhostValue(GhostValue), Allocated(Allocated), ContractVar(ContractVar), - Contract(preVars, preConds, preAllocated, prePointsTos, prePointsToBitfields, - argumentVals, postVars, postConds, postAllocated, postPointsTos, postPointsToBitfields, + Contract(preVars, preConds, preAllocated, preGhostValues, prePointsTos, prePointsToBitfields, + argumentVals, postVars, postConds, postAllocated, postGhostValues, postPointsTos, postPointsToBitfields, returnVal) ) import SAWServer.Data.MIRType (JSONMIRType, mirType) import SAWServer.Exceptions ( notAtTopLevel ) @@ -74,24 +76,25 @@ newtype ServerSetupVal = Val (MS.SetupValue MIR) compileMIRContract :: (FilePath -> IO ByteString) -> BuiltinContext -> + Map ServerName MS.GhostGlobal -> CryptolEnv -> SAWEnv -> Contract JSONMIRType (P.Expr P.PName) -> MIRSetupM () -compileMIRContract fileReader bic cenv0 sawenv c = +compileMIRContract fileReader bic ghostEnv cenv0 sawenv c = do allocsPre <- mapM setupAlloc (preAllocated c) (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) mapM_ (\p -> getTypedTerm cenvPre p >>= mir_precond) (preConds c) mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) mapM_ setupPointsToBitfields (prePointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= mir_execute_func allocsPost <- mapM setupAlloc (postAllocated c) (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) mapM_ (\p -> getTypedTerm cenvPost p >>= mir_postcond) (postConds c) mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) mapM_ setupPointsToBitfields (postPointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) case returnVal c of Just v -> getSetupVal (envPost, cenvPost) v >>= mir_return Nothing -> return () @@ -136,7 +139,10 @@ compileMIRContract fileReader bic cenv0 sawenv c = setupPointsToBitfields _ = MIRSetupM $ fail "Points-to-bitfield not supported in the MIR API." - --setupGhostValue _ _ _ = fail "Ghost values not supported yet in the MIR API." + setupGhostValue genv cenv (GhostValue serverName e) = + do g <- resolve genv serverName + t <- getTypedTerm cenv e + mir_ghost_value g t resolve :: Map ServerName a -> ServerName -> MIRSetupM a resolve env name = diff --git a/saw-remote-api/src/SAWServer/MIRVerify.hs b/saw-remote-api/src/SAWServer/MIRVerify.hs index 5106396341..f3bf31e447 100644 --- a/saw-remote-api/src/SAWServer/MIRVerify.hs +++ b/saw-remote-api/src/SAWServer/MIRVerify.hs @@ -9,6 +9,7 @@ module SAWServer.MIRVerify import Prelude hiding (mod) import Control.Lens +import qualified Data.Map as Map import SAWScript.Crucible.MIR.Builtins ( mir_unsafe_assume_spec, mir_verify ) @@ -26,6 +27,7 @@ import SAWServer pushTask, dropTask, setServerVal, + getGhosts, getMIRModule, getMIRMethodSpecIR ) import SAWServer.CryptolExpression (getCryptolExpr) @@ -53,7 +55,8 @@ mirVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scri cenv = rwCryptol (view sawTopLevelRW state) sawenv = view sawEnv state fileReader <- Argo.getFileReader - setup <- compileMIRContract fileReader bic cenv sawenv <$> + ghostEnv <- Map.fromList <$> getGhosts + setup <- compileMIRContract fileReader bic ghostEnv cenv sawenv <$> traverse getCryptolExpr contract res <- case mode of VerifyContract -> do diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index fe52a42fb1..dc41073628 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -27,6 +27,7 @@ import Data.Functor import Control.Applicative import Data.Monoid #endif +import Control.Lens (view) import Control.Monad (foldM, forM, unless, when) import Control.Monad.Except (MonadError(..)) import Control.Monad.IO.Class (MonadIO(..)) @@ -42,6 +43,7 @@ import Data.IORef import Data.List (isPrefixOf, isInfixOf, sort) import qualified Data.Map as Map import Data.Maybe (fromMaybe) +import Data.Parameterized.Classes (KnownRepr(..)) import Data.Set (Set) import qualified Data.Set as Set import Data.Text (Text) @@ -118,6 +120,9 @@ import qualified Cryptol.Utils.Ident as C (mkIdent, packModName, textToModName, PrimIdent(..)) import qualified Cryptol.Utils.RecordMap as C (recordFromFields) +-- crucible +import Lang.Crucible.CFG.Common (freshGlobalVar) + import qualified SAWScript.SBVParser as SBV import SAWScript.ImportAIG @@ -131,7 +136,8 @@ import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork) import SAWScript.SolverCache import SAWScript.SolverVersions -import SAWScript.Crucible.Common.MethodSpec (ppTypedTermType) +import qualified SAWScript.Crucible.Common.MethodSpec as MS +import SAWScript.Crucible.Common.Setup.Type (addCondition, croTags) import SAWScript.Prover.Util(checkBooleanSchema) import SAWScript.Prover.SolverStats import qualified SAWScript.Prover.SBV as Prover @@ -157,7 +163,7 @@ definePrim name (TypedTerm (TypedTermSchema schema) rhs) = definePrim _name (TypedTerm tp _) = fail $ unlines [ "Expected term with Cryptol schema type, but got" - , show (ppTypedTermType tp) + , show (MS.ppTypedTermType tp) ] sbvUninterpreted :: String -> Term -> TopLevel Uninterp @@ -695,7 +701,7 @@ term_type tt = TypedTermSchema sch -> pure sch tp -> fail $ unlines [ "Term does not have a Cryptol type" - , show (ppTypedTermType tp) + , show (MS.ppTypedTermType tp) ] goal_eval :: [String] -> ProofScript () @@ -2465,3 +2471,26 @@ writeVerificationSummary = do JSON -> jsonVerificationSummary Pretty -> prettyVerificationSummary ppOpts nenv in io $ writeFile f' $ formatSummary summary + +declare_ghost_state :: + String -> + TopLevel SV.Value +declare_ghost_state name = + do allocator <- getHandleAlloc + global <- liftIO (freshGlobalVar allocator (Text.pack name) knownRepr) + return (SV.VGhostVar global) + +ghost_value :: + MS.GhostGlobal -> + TypedTerm -> + SV.CrucibleSetup ext () +ghost_value ghost val = + do loc <- SV.getW4Position "ghost_value" + tags <- view croTags + let md = MS.ConditionMetadata + { MS.conditionLoc = loc + , MS.conditionTags = tags + , MS.conditionType = "ghost value" + , MS.conditionContext = "" + } + addCondition (MS.SetupCond_Ghost md ghost val) diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index e8ce39d657..acba975084 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -13,8 +13,10 @@ Grow\", and is prevalent across the Crucible codebase. {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} @@ -22,6 +24,7 @@ Grow\", and is prevalent across the Crucible codebase. {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} module SAWScript.Crucible.Common.MethodSpec ( AllocIndex(..) @@ -62,7 +65,6 @@ module SAWScript.Crucible.Common.MethodSpec , setupToTypedTerm , setupToTerm - , XGhostState , GhostValue , GhostType , GhostGlobal @@ -118,6 +120,7 @@ import Data.Set (Set) import Data.Time.Clock import Data.Void (absurd) +import Control.Monad (when) import Control.Monad.Trans.Maybe import Control.Monad.Trans (lift) import Control.Lens @@ -132,13 +135,17 @@ import Lang.Crucible.JVM (JVM) import qualified Lang.Crucible.Types as Crucible (IntrinsicType, EmptyCtx) import qualified Lang.Crucible.CFG.Common as Crucible (GlobalVar) +import qualified Lang.Crucible.Simulator.Intrinsics as Crucible import Mir.Intrinsics (MIR) +import qualified Cryptol.TypeCheck.Type as Cryptol (Schema) import qualified Cryptol.Utils.PP as Cryptol import Verifier.SAW.TypedTerm as SAWVerifier import Verifier.SAW.SharedTerm as SAWVerifier +import Verifier.SAW.Simulator.What4.ReturnTrip as SAWVerifier +import SAWScript.Crucible.Common (Sym, sawCoreState) import SAWScript.Crucible.Common.Setup.Value import SAWScript.Crucible.LLVM.Setup.Value (LLVM) import SAWScript.Crucible.JVM.Setup.Value () @@ -344,21 +351,33 @@ type GhostValue = "GhostValue" type GhostType = Crucible.IntrinsicType GhostValue Crucible.EmptyCtx type GhostGlobal = Crucible.GlobalVar GhostType +instance Crucible.IntrinsicClass Sym GhostValue where + type Intrinsic Sym GhostValue ctx = (Cryptol.Schema, Term) + muxIntrinsic sym _ _namerep _ctx prd (thnSch,thn) (elsSch,els) = + do when (thnSch /= elsSch) $ fail $ unlines $ + [ "Attempted to mux ghost variables of different types:" + , show (Cryptol.pp thnSch) + , show (Cryptol.pp elsSch) + ] + st <- sawCoreState sym + let sc = saw_ctx st + prd' <- toSC sym st prd + typ <- scTypeOf sc thn + res <- scIte sc typ prd' thn els + return (thnSch, res) + -------------------------------------------------------------------------------- -- *** StateSpec data SetupCondition ext where SetupCond_Equal :: ConditionMetadata -> SetupValue ext -> SetupValue ext -> SetupCondition ext SetupCond_Pred :: ConditionMetadata -> TypedTerm -> SetupCondition ext - SetupCond_Ghost :: XGhostState ext -> - ConditionMetadata -> + SetupCond_Ghost :: ConditionMetadata -> GhostGlobal -> TypedTerm -> SetupCondition ext -deriving instance ( SetupValueHas Show ext - , Show (XGhostState ext) - ) => Show (SetupCondition ext) +deriving instance SetupValueHas Show ext => Show (SetupCondition ext) -- | Verification state (either pre- or post-) specification data StateSpec ext = StateSpec diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs index 48d31e1b66..fac57dcb20 100644 --- a/src/SAWScript/Crucible/Common/Override.hs +++ b/src/SAWScript/Crucible/Common/Override.hs @@ -65,11 +65,16 @@ module SAWScript.Crucible.Common.Override -- , assignmentToList , MetadataMap + -- + , learnGhost + , executeGhost + , instantiateExtMatchTerm + , matchTerm ) where import qualified Control.Exception as X import Control.Lens -import Control.Monad (foldM, unless) +import Control.Monad (foldM, unless, when) import Control.Monad.Trans.State hiding (get, put) import Control.Monad.State.Class (MonadState(..)) import Control.Monad.Error.Class (MonadError) @@ -82,6 +87,7 @@ import qualified Data.Map as Map import Data.Map (Map) import Data.Maybe (fromMaybe) import Data.Proxy (Proxy(..)) +import qualified Data.Set as Set import Data.Set (Set) import Data.Typeable (Typeable) import Data.Void @@ -92,10 +98,13 @@ import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Some (Some) import Data.Parameterized.TraversableFC (toListFC) +import Verifier.SAW.Prelude as SAWVerifier (scEq) import Verifier.SAW.SharedTerm as SAWVerifier import Verifier.SAW.TypedAST as SAWVerifier import Verifier.SAW.TypedTerm as SAWVerifier +import qualified Cryptol.Utils.PP as Cryptol (pp) + import qualified Lang.Crucible.Backend as Crucible import qualified Lang.Crucible.Backend.Online as Crucible import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr, GlobalVar) @@ -529,3 +538,102 @@ assignmentToList :: Ctx.Assignment (Crucible.RegEntry sym) ctx -> [Crucible.AnyValue sym] assignmentToList = toListFC (\(Crucible.RegEntry x y) -> Crucible.AnyValue x y) + +------------------------------------------------------------------------ + +learnGhost :: + SharedContext -> + MS.ConditionMetadata -> + PrePost -> + MS.GhostGlobal -> + TypedTerm -> + OverrideMatcher ext md () +learnGhost sc md prepost var (TypedTerm (TypedTermSchema schEx) tmEx) = + do (sch,tm) <- readGlobal var + when (sch /= schEx) $ fail $ unlines $ + [ "Ghost variable had the wrong type:" + , "- Expected: " ++ show (Cryptol.pp schEx) + , "- Actual: " ++ show (Cryptol.pp sch) + ] + instantiateExtMatchTerm sc md prepost tm tmEx +learnGhost _sc _md _prepost _var (TypedTerm tp _) + = fail $ unlines + [ "Ghost variable expected value has improper type" + , "expected Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] + +executeGhost :: + SharedContext -> + MS.ConditionMetadata -> + MS.GhostGlobal -> + TypedTerm -> + OverrideMatcher ext RW () +executeGhost sc _md var (TypedTerm (TypedTermSchema sch) tm) = + do s <- OM (use termSub) + tm' <- liftIO (scInstantiateExt sc s tm) + writeGlobal var (sch,tm') +executeGhost _sc _md _var (TypedTerm tp _) = + fail $ unlines + [ "executeGhost: improper value type" + , "expected Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] + +-- | NOTE: The two 'Term' arguments must have the same type. +instantiateExtMatchTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + Term {- ^ exported concrete term -} -> + Term {- ^ expected specification term -} -> + OverrideMatcher ext md () +instantiateExtMatchTerm sc md prepost actual expected = do + sub <- OM (use termSub) + matchTerm sc md prepost actual =<< liftIO (scInstantiateExt sc sub expected) + +matchTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + Term {- ^ exported concrete term -} -> + Term {- ^ expected specification term -} -> + OverrideMatcher ext md () + +matchTerm _ _ _ real expect | real == expect = return () +matchTerm sc md prepost real expect = + do let loc = MS.conditionLoc md + free <- OM (use osFree) + case unwrapTermF expect of + FTermF (ExtCns ec) + | Set.member (ecVarIndex ec) free -> + do assignTerm sc md prepost (ecVarIndex ec) real + + _ -> + do t <- liftIO $ scEq sc real expect + let msg = unlines $ + [ "Literal equality " ++ MS.stateCond prepost +-- , "Expected term: " ++ prettyTerm expect +-- , "Actual term: " ++ prettyTerm real + ] + addTermEq t md $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" +-- where prettyTerm = show . ppTermDepth 20 + +assignTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + VarIndex {- ^ external constant index -} -> + Term {- ^ value -} -> + OverrideMatcher ext md () + +assignTerm sc md prepost var val = + do mb <- OM (use (termSub . at var)) + case mb of + Nothing -> OM (termSub . at var ?= val) + Just old -> + matchTerm sc md prepost val old + +-- do t <- liftIO $ scEq sc old val +-- p <- liftIO $ resolveSAWPred cc t +-- addAssert p (Crucible.AssertFailureSimError ("literal equality " ++ MS.stateCond prepost)) diff --git a/src/SAWScript/Crucible/Common/Setup/Value.hs b/src/SAWScript/Crucible/Common/Setup/Value.hs index 505acce1c9..b9fa6ebcde 100644 --- a/src/SAWScript/Crucible/Common/Setup/Value.hs +++ b/src/SAWScript/Crucible/Common/Setup/Value.hs @@ -51,8 +51,6 @@ module SAWScript.Crucible.Common.Setup.Value , SetupValue(..) , SetupValueHas - , XGhostState - , ConditionMetadata(..) , MethodId @@ -185,15 +183,6 @@ deriving instance (SetupValueHas Show ext) => Show (SetupValue ext) -- deriving instance (SetupValueHas Eq ext) => Eq (SetupValue ext) -- deriving instance (SetupValueHas Ord ext) => Ord (SetupValue ext) --------------------------------------------------------------------------------- --- ** Ghost state - --- | This extension field controls whether ghost state is enabled for a --- particular language backend. At the moment, ghost state is only enabled for --- the LLVM backend, but we want to expand this to cover other language backends --- in the future. See . -type family XGhostState ext - -------------------------------------------------------------------------------- -- ** Pre- and post-conditions diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index 77c5d99dd6..f2a55d93b4 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -44,6 +44,7 @@ module SAWScript.Crucible.JVM.Builtins , jvm_alloc_object , jvm_alloc_array , jvm_setup_with_tag + , jvm_ghost_value ) where import Control.Lens @@ -70,7 +71,6 @@ import Data.Text (Text) import qualified Data.Text as Text import Data.Time.Clock (getCurrentTime, diffUTCTime) import qualified Data.Vector as V -import Data.Void (absurd) import Prettyprinter import System.IO @@ -112,6 +112,7 @@ import Verifier.SAW.TypedTerm import Verifier.SAW.Simulator.What4.ReturnTrip +import SAWScript.Builtins (ghost_value) import SAWScript.Exceptions import SAWScript.Panic import SAWScript.Proof @@ -415,7 +416,8 @@ verifyPrestate cc mspec globals0 = (env, globals1) <- runStateT (Map.traverseWithKey doAlloc preallocs) globals0' globals2 <- setupPrePointsTos mspec cc env (mspec ^. MS.csPreState . MS.csPointsTos) globals1 - cs <- setupPrestateConditions mspec cc env (mspec ^. MS.csPreState . MS.csConditions) + (globals3, cs) <- + setupPrestateConditions mspec cc env globals2 (mspec ^. MS.csPreState . MS.csConditions) args <- resolveArguments cc mspec env -- Check the type of the return setup value @@ -435,7 +437,7 @@ verifyPrestate cc mspec globals0 = ] (Nothing, _) -> return () - return (args, cs, env, globals2) + return (args, cs, env, globals3) -- | Check two Types for register compatibility. registerCompatible :: J.Type -> J.Type -> Bool @@ -540,32 +542,43 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts _ -> panic "setupPrePointsTo" ["invalid invariant", "jvm_modifies in pre-state"] --- | Collects boolean terms that should be assumed to be true. +-- | Sets up globals (ghost variable), and collects boolean terms +-- that should be assumed to be true. setupPrestateConditions :: MethodSpec -> JVMCrucibleContext -> Map AllocIndex JVMRefVal -> + Crucible.SymGlobalState Sym -> [SetupCondition] -> - IO [Crucible.LabeledPred Term AssumptionReason] + IO ( Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term AssumptionReason] + ) setupPrestateConditions mspec cc env = aux [] where tyenv = MS.csAllocations mspec nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames - aux acc [] = return acc + aux acc globals [] = return (globals, acc) - aux acc (MS.SetupCond_Equal loc val1 val2 : xs) = + aux acc globals (MS.SetupCond_Equal loc val1 val2 : xs) = do val1' <- resolveSetupVal cc env tyenv nameEnv val1 val2' <- resolveSetupVal cc env tyenv nameEnv val2 t <- assertEqualVals cc val1' val2' let lp = Crucible.LabeledPred t (loc, "equality precondition") - aux (lp:acc) xs + aux (lp:acc) globals xs - aux acc (MS.SetupCond_Pred loc tm : xs) = + aux acc globals (MS.SetupCond_Pred loc tm : xs) = let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in - aux (lp:acc) xs - - aux _ (MS.SetupCond_Ghost empty_ _ _ _ : _) = absurd empty_ + aux (lp:acc) globals xs + + aux acc globals (MS.SetupCond_Ghost _md var val : xs) = + case val of + TypedTerm (TypedTermSchema sch) tm -> + aux acc (Crucible.insertGlobal var (sch,tm) globals) xs + TypedTerm tp _ -> + fail $ unlines + [ "Setup term for global variable expected to have Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] -------------------------------------------------------------------------------- @@ -660,7 +673,13 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat m regmap <- prepareArgs (Crucible.handleArgTypes h) (map snd args) res <- do let feats = pfs - let simctx = CJ.jvmSimContext bak halloc stdout jc verbosity SAWCruciblePersonality + -- TODO: Use crucible-jvm's jvmSimContext here (instead of manually + -- calling mkDelayedBindings/initSimContext), once + -- https://github.com/GaloisInc/crucible/issues/1128 has been fixed + -- upstream. + let bindings = CJ.mkDelayedBindings jc verbosity + let simctx = Crucible.initSimContext bak intrinsics halloc stdout + bindings CJ.jvmExtensionImpl SAWCruciblePersonality let simSt = Crucible.InitialState simctx globals Crucible.defaultAbortHandler (Crucible.handleReturnType h) let fnCall = Crucible.regValue <$> Crucible.callFnVal (Crucible.HandleFnVal h) regmap let overrideSim = @@ -1421,6 +1440,13 @@ jvm_setup_with_tag :: jvm_setup_with_tag tag m = JVMSetupM (Setup.setupWithTag tag (runJVMSetupM m)) +jvm_ghost_value :: + MS.GhostGlobal -> + TypedTerm -> + JVMSetupM () +jvm_ghost_value ghost val = JVMSetupM $ + ghost_value ghost val + -------------------------------------------------------------------------------- -- | Sort a list of things and group them into equivalence classes. diff --git a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs index bc9e40a9f6..1e3cd413f8 100644 --- a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs @@ -53,9 +53,13 @@ module SAWScript.Crucible.JVM.MethodSpecIR , initialDefCrucibleMethodSpecIR , initialCrucibleSetupState + + , intrinsics ) where import Control.Lens +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.SymbolRepr (SymbolRepr, knownSymbol) import qualified Prettyprinter as PPL -- what4 @@ -63,6 +67,8 @@ import What4.ProgramLoc (ProgramLoc) -- crucible-jvm import qualified Lang.Crucible.JVM as CJ +import qualified Lang.Crucible.Simulator.Intrinsics as CS + (IntrinsicMuxFn(IntrinsicMuxFn)) import qualified Lang.JVM.Codebase as CB -- jvm-parser @@ -184,6 +190,16 @@ initialCrucibleSetupState cc (cls, method) loc = (J.className cls) method loc +-------------------------------------------------------------------------------- + +-- | The default JVM intrinsics extended with the 'MS.GhostValue' intrinsic, +-- which powers ghost state. +intrinsics :: MapF.MapF SymbolRepr (CS.IntrinsicMuxFn Sym) +intrinsics = + MapF.insert + (knownSymbol :: SymbolRepr MS.GhostValue) + CS.IntrinsicMuxFn + CJ.jvmIntrinsicTypes -------------------------------------------------------------------------------- diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 258249647c..680686ac8c 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -92,8 +92,6 @@ import Data.Parameterized.Some (Some(Some)) -- saw-core import Verifier.SAW.SharedTerm -import Verifier.SAW.Prelude (scEq) -import Verifier.SAW.TypedAST import Verifier.SAW.TypedTerm import Verifier.SAW.Simulator.What4.ReturnTrip (toSC) @@ -326,13 +324,13 @@ methodSpecHandler_prestate opts sc cc args cs = -- which involves writing values into memory, computing the return value, -- and computing postcondition predicates. methodSpecHandler_poststate :: - forall ret w. + forall ret. Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> JVMCrucibleContext {- ^ context for interacting with Crucible -} -> Crucible.TypeRepr ret {- ^ type representation of function return value -} -> CrucibleMethodSpecIR {- ^ specification for current function override -} -> - OverrideMatcher CJ.JVM w (Crucible.RegValue Sym ret) + OverrideMatcher CJ.JVM RW (Crucible.RegValue Sym ret) methodSpecHandler_poststate opts sc cc retTy cs = do executeCond opts sc cc cs (cs ^. MS.csPostState) computeReturnValue opts cc sc cs retTy (cs ^. MS.csRetValue) @@ -350,10 +348,22 @@ learnCond opts sc cc cs prepost ss = do let loc = cs ^. MS.csLoc matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos) traverse_ (learnSetupCondition opts sc cc cs prepost) (ss ^. MS.csConditions) + assertTermEqualities sc cc enforceDisjointness cc loc ss enforceCompleteSubstitution loc ss +assertTermEqualities :: + SharedContext -> + JVMCrucibleContext -> + OverrideMatcher CJ.JVM md () +assertTermEqualities sc cc = do + let assertTermEquality (t, md, e) = do + p <- instantiateExtResolveSAWPred sc cc t + addAssert p md e + traverse_ assertTermEquality =<< OM (use termEqs) + + -- execute a pre/post condition executeCond :: Options -> @@ -361,7 +371,7 @@ executeCond :: JVMCrucibleContext -> CrucibleMethodSpecIR -> StateSpec -> - OverrideMatcher CJ.JVM w () + OverrideMatcher CJ.JVM RW () executeCond opts sc cc cs ss = do refreshTerms sc ss traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs)) @@ -508,26 +518,6 @@ assignVar cc md var ref = ------------------------------------------------------------------------ - -assignTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - JVMCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - VarIndex {- ^ external constant index -} -> - Term {- ^ value -} -> - OverrideMatcher CJ.JVM w () - -assignTerm sc cc md prepost var val = - do mb <- OM (use (termSub . at var)) - case mb of - Nothing -> OM (termSub . at var ?= val) - Just old -> - matchTerm sc cc md prepost val old - - ------------------------------------------------------------------------- - -- | Match the value of a function argument with a symbolic 'SetupValue'. matchArg :: Options {- ^ saw script print out opts -} -> @@ -547,7 +537,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected@(MS.SetupTerm expec = do sym <- Ov.getSymInterface failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy realTerm <- valueToSC sym md failMsg tval actual - matchTerm sc cc md prepost realTerm (ttTerm expectedTT) + matchTerm sc md prepost realTerm (ttTerm expectedTT) matchArg opts sc cc cs prepost md actual@(RVal ref) expectedTy setupval = case setupval of @@ -606,32 +596,6 @@ valueToSC _sym md failMsg _tval _val = ------------------------------------------------------------------------ --- | NOTE: The two 'Term' arguments must have the same type. -matchTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - JVMCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - Term {- ^ exported concrete term -} -> - Term {- ^ expected specification term -} -> - OverrideMatcher CJ.JVM w () - -matchTerm _ _ _ _ real expect | real == expect = return () -matchTerm sc cc md prepost real expect = - do free <- OM (use osFree) - let loc = MS.conditionLoc md - case unwrapTermF expect of - FTermF (ExtCns ec) - | Set.member (ecVarIndex ec) free -> - do assignTerm sc cc md prepost (ecVarIndex ec) real - - _ -> - do t <- liftIO $ scEq sc real expect - p <- liftIO $ resolveBoolTerm (cc ^. jccSym) t - addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError ("literal equality " ++ MS.stateCond prepost) "")) - ------------------------------------------------------------------------- - -- | Use the current state to learn about variable assignments based on -- preconditions for a procedure specification. learnSetupCondition :: @@ -642,9 +606,11 @@ learnSetupCondition :: PrePost -> SetupCondition -> OverrideMatcher CJ.JVM w () -learnSetupCondition opts sc cc spec prepost (MS.SetupCond_Equal md val1 val2) = learnEqual opts sc cc spec md prepost val1 val2 -learnSetupCondition _opts sc cc _ prepost (MS.SetupCond_Pred md tm) = learnPred sc cc md prepost (ttTerm tm) -learnSetupCondition _opts _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty +learnSetupCondition opts sc cc spec prepost cond = + case cond of + MS.SetupCond_Equal md val1 val2 -> learnEqual opts sc cc spec md prepost val1 val2 + MS.SetupCond_Pred md tm -> learnPred sc cc md prepost (ttTerm tm) + MS.SetupCond_Ghost md var val -> learnGhost sc md prepost var val ------------------------------------------------------------------------ @@ -717,7 +683,7 @@ learnPointsTo opts sc cc spec prepost pt = ety_tm <- liftIO $ Cryptol.importType sc Cryptol.emptyEnv ety ts <- traverse load [0 .. fromInteger len - 1] realTerm <- liftIO $ scVector sc ety_tm ts - matchTerm sc cc md prepost realTerm (ttTerm tt) + matchTerm sc md prepost realTerm (ttTerm tt) -- If the right-hand-side is 'Nothing', this is indicates a "modifies" declaration, -- which should probably not appear in the pre-state section, and has no effect. @@ -761,6 +727,15 @@ learnPred sc cc md prepost t = let loc = MS.conditionLoc md addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) "")) +instantiateExtResolveSAWPred :: + SharedContext -> + JVMCrucibleContext -> + Term -> + OverrideMatcher CJ.JVM md (W4.Pred Sym) +instantiateExtResolveSAWPred sc cc cond = do + sub <- OM (use termSub) + liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond + ------------------------------------------------------------------------ -- TODO: replace (W4.ProgramLoc, J.Type) by some allocation datatype @@ -800,10 +775,13 @@ executeSetupCondition :: JVMCrucibleContext -> CrucibleMethodSpecIR -> SetupCondition -> - OverrideMatcher CJ.JVM w () -executeSetupCondition opts sc cc spec (MS.SetupCond_Equal md val1 val2) = executeEqual opts sc cc spec md val1 val2 -executeSetupCondition _opts sc cc _ (MS.SetupCond_Pred md tm) = executePred sc cc md tm -executeSetupCondition _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty + OverrideMatcher CJ.JVM RW () +executeSetupCondition opts sc cc spec = + \case + MS.SetupCond_Equal md val1 val2 -> + executeEqual opts sc cc spec md val1 val2 + MS.SetupCond_Pred md tm -> executePred sc cc md tm + MS.SetupCond_Ghost md var val -> executeGhost sc md var val ------------------------------------------------------------------------ diff --git a/src/SAWScript/Crucible/JVM/Setup/Value.hs b/src/SAWScript/Crucible/JVM/Setup/Value.hs index 8286704750..a69e29ec05 100644 --- a/src/SAWScript/Crucible/JVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/JVM/Setup/Value.hs @@ -87,8 +87,6 @@ type instance MS.XSetupCast CJ.JVM = Void type instance MS.XSetupUnion CJ.JVM = Void type instance MS.XSetupGlobalInitializer CJ.JVM = Void -type instance MS.XGhostState CJ.JVM = Void - type JIdent = String -- FIXME(huffman): what to put here? type instance MS.TypeName CJ.JVM = JIdent diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index e7fa7c7892..625e0db955 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -43,7 +43,6 @@ module SAWScript.Crucible.LLVM.Builtins , llvm_spec_size , llvm_spec_solvers , llvm_ghost_value - , llvm_declare_ghost_state , llvm_equal , llvm_points_to , llvm_conditional_points_to @@ -189,6 +188,7 @@ import Verifier.SAW.TypedTerm -- saw-script import SAWScript.AST (Located(..)) +import SAWScript.Builtins (ghost_value) import SAWScript.Proof import SAWScript.Prover.SolverStats import SAWScript.Prover.Versions @@ -1206,7 +1206,7 @@ setupPrestateConditions mspec cc mem env = aux [] let lp = Crucible.LabeledPred (ttTerm tm) (md, "precondition") in aux (lp:acc) globals xs - aux acc globals (MS.SetupCond_Ghost () _md var val : xs) = + aux acc globals (MS.SetupCond_Ghost _md var val : xs) = case val of TypedTerm (TypedTermSchema sch) tm -> aux acc (Crucible.insertGlobal var (sch,tm) globals) xs @@ -2795,28 +2795,12 @@ llvm_equal (getAllLLVM -> val1) (getAllLLVM -> val2) = } Setup.addCondition (MS.SetupCond_Equal md val1 val2) -llvm_declare_ghost_state :: - String -> - TopLevel Value -llvm_declare_ghost_state name = - do allocator <- getHandleAlloc - global <- liftIO (Crucible.freshGlobalVar allocator (Text.pack name) knownRepr) - return (VGhostVar global) - llvm_ghost_value :: MS.GhostGlobal -> TypedTerm -> LLVMCrucibleSetupM () llvm_ghost_value ghost val = LLVMCrucibleSetupM $ - do loc <- getW4Position "llvm_ghost_value" - tags <- view Setup.croTags - let md = MS.ConditionMetadata - { MS.conditionLoc = loc - , MS.conditionTags = tags - , MS.conditionType = "ghost value" - , MS.conditionContext = "" - } - Setup.addCondition (MS.SetupCond_Ghost () md ghost val) + ghost_value ghost val llvm_spec_solvers :: SomeLLVM MS.ProvedSpec -> [String] llvm_spec_solvers (SomeLLVM ps) = diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index 2ed66092e3..f627d36508 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -12,11 +12,9 @@ Stability : provisional {-# LANGUAGE DoAndIfThenElse #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternSynonyms #-} @@ -119,16 +117,12 @@ module SAWScript.Crucible.LLVM.MethodSpecIR ) where import Control.Lens -import Control.Monad (when) import Data.Functor.Compose (Compose(..)) import qualified Data.Map as Map import qualified Prettyprinter as PPL import qualified Text.LLVM.AST as L import qualified Text.LLVM.PP as L -import qualified Cryptol.TypeCheck.AST as Cryptol -import qualified Cryptol.Utils.PP as Cryptol (pp) - import Data.Parameterized.All (All(All)) import Data.Parameterized.Some (Some(Some)) import qualified Data.Parameterized.Map as MapF @@ -137,7 +131,7 @@ import What4.ProgramLoc (ProgramLoc) import qualified Lang.Crucible.Types as Crucible (SymbolRepr, knownSymbol) import qualified Lang.Crucible.Simulator.Intrinsics as Crucible - (IntrinsicClass(Intrinsic, muxIntrinsic), IntrinsicMuxFn(IntrinsicMuxFn)) + (IntrinsicMuxFn(IntrinsicMuxFn)) import SAWScript.Crucible.Common import qualified SAWScript.Crucible.Common.MethodSpec as MS @@ -146,9 +140,6 @@ import qualified SAWScript.Crucible.Common.Setup.Type as Setup import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL import SAWScript.Crucible.LLVM.Setup.Value -import Verifier.SAW.Simulator.What4.ReturnTrip ( toSC, saw_ctx ) - -import Verifier.SAW.SharedTerm import Verifier.SAW.TypedTerm @@ -177,24 +168,6 @@ mutIso = isMut :: Lens' LLVMAllocSpec Bool isMut = allocSpecMut . mutIso --------------------------------------------------------------------------------- --- ** Ghost state - -instance Crucible.IntrinsicClass Sym MS.GhostValue where - type Intrinsic Sym MS.GhostValue ctx = (Cryptol.Schema, Term) - muxIntrinsic sym _ _namerep _ctx prd (thnSch,thn) (elsSch,els) = - do when (thnSch /= elsSch) $ fail $ unlines $ - [ "Attempted to mux ghost variables of different types:" - , show (Cryptol.pp thnSch) - , show (Cryptol.pp elsSch) - ] - st <- sawCoreState sym - let sc = saw_ctx st - prd' <- toSC sym st prd - typ <- scTypeOf sc thn - res <- scIte sc typ prd' thn els - return (thnSch, res) - -------------------------------------------------------------------------------- -- ** CrucibleContext @@ -249,8 +222,10 @@ instance PPL.Pretty (LLVMPointsToValue arch) where MS.ppTypedTerm arr PPL.<+> PPL.pretty "[" PPL.<+> MS.ppTypedTerm sz PPL.<+> PPL.pretty "]" -------------------------------------------------------------------------------- --- ** ??? +-- ** SAW LLVM intrinsics +-- | The default LLVM intrinsics extended with the 'MS.GhostValue' intrinsic, +-- which powers ghost state. intrinsics :: MapF.MapF Crucible.SymbolRepr (Crucible.IntrinsicMuxFn Sym) intrinsics = MapF.insert diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index f28768f11b..44dc4f89e4 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -64,7 +64,7 @@ import Control.Lens.Getter import Control.Lens.Lens import Control.Lens.Setter import Control.Exception as X -import Control.Monad (filterM, foldM, forM, forM_, when, zipWithM) +import Control.Monad (filterM, foldM, forM, forM_, zipWithM) import Control.Monad.Except (runExcept) import Control.Monad.IO.Class (MonadIO(..)) import Data.Either (partitionEithers) @@ -87,7 +87,6 @@ import qualified Text.LLVM.AST as L import qualified Cryptol.TypeCheck.AST as Cryptol (Schema(..)) import qualified Cryptol.Eval.Type as Cryptol (TValue(..), evalType) -import qualified Cryptol.Utils.PP as Cryptol (pp) import qualified Lang.Crucible.Backend as Crucible import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr(UnitRepr)) @@ -117,9 +116,7 @@ import Data.Parameterized.NatRepr import Data.Parameterized.Some (Some(..)) import qualified Data.BitVector.Sized as BV -import Verifier.SAW.Prelude (scEq) import Verifier.SAW.SharedTerm -import Verifier.SAW.TypedAST import Verifier.SAW.Recognizer import Verifier.SAW.TypedTerm import Verifier.SAW.Simulator.What4.ReturnTrip (SAWCoreState(..), toSC, bindSAWTerm) @@ -1073,29 +1070,6 @@ assignVar cc md var val = ------------------------------------------------------------------------ - -assignTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - VarIndex {- ^ external constant index -} -> - Term {- ^ value -} -> - OverrideMatcher (LLVM arch) md () - -assignTerm sc cc md prepost var val = - do mb <- OM (use (termSub . at var)) - case mb of - Nothing -> OM (termSub . at var ?= val) - Just old -> - matchTerm sc cc md prepost val old - --- do t <- liftIO $ scEq sc old val --- p <- liftIO $ resolveSAWPred cc t --- addAssert p (Crucible.AssertFailureSimError ("literal equality " ++ MS.stateCond prepost)) - ------------------------------------------------------------------------- - diffMemTypes :: Crucible.HasPtrWidth wptr => Crucible.MemType -> @@ -1176,7 +1150,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = , Right tval <- Cryptol.evalType mempty tyexpr -> do failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy realTerm <- valueToSC sym md failMsg tval actual - instantiateExtMatchTerm sc cc md prepost realTerm (ttTerm expectedTT) + instantiateExtMatchTerm sc md prepost realTerm (ttTerm expectedTT) -- match arrays point-wise (Crucible.LLVMValArray _ xs, Crucible.ArrayType _len y, SetupArray () zs) @@ -1346,50 +1320,6 @@ typeToSC sc t = do fields' <- V.toList <$> traverse (typeToSC sc . view Crucible.fieldVal) fields scTupleType sc fields' ------------------------------------------------------------------------- - --- | NOTE: The two 'Term' arguments must have the same type. -instantiateExtMatchTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - Term {- ^ exported concrete term -} -> - Term {- ^ expected specification term -} -> - OverrideMatcher (LLVM arch) md () -instantiateExtMatchTerm sc cc md prepost actual expected = do - sub <- OM (use termSub) - matchTerm sc cc md prepost actual =<< liftIO (scInstantiateExt sc sub expected) - -matchTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - Term {- ^ exported concrete term -} -> - Term {- ^ expected specification term -} -> - OverrideMatcher (LLVM arch) md () - -matchTerm _ _ _ _ real expect | real == expect = return () -matchTerm sc cc md prepost real expect = - do let loc = MS.conditionLoc md - free <- OM (use osFree) - case unwrapTermF expect of - FTermF (ExtCns ec) - | Set.member (ecVarIndex ec) free -> - do assignTerm sc cc md prepost (ecVarIndex ec) real - - _ -> - do t <- liftIO $ scEq sc real expect - let msg = unlines $ - [ "Literal equality " ++ MS.stateCond prepost --- , "Expected term: " ++ prettyTerm expect --- , "Actual term: " ++ prettyTerm real - ] - addTermEq t md $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" --- where prettyTerm = show . ppTermDepth 20 - - ------------------------------------------------------------------------ -- | Use the current state to learn about variable assignments based on @@ -1405,36 +1335,10 @@ learnSetupCondition :: OverrideMatcher (LLVM arch) md () learnSetupCondition opts sc cc spec prepost cond = case cond of - MS.SetupCond_Equal md val1 val2 -> learnEqual opts sc cc spec md prepost val1 val2 - MS.SetupCond_Pred md tm -> learnPred sc cc md prepost (ttTerm tm) - MS.SetupCond_Ghost () md var val -> learnGhost sc cc md prepost var val - - ------------------------------------------------------------------------- + MS.SetupCond_Equal md val1 val2 -> learnEqual opts sc cc spec md prepost val1 val2 + MS.SetupCond_Pred md tm -> learnPred sc cc md prepost (ttTerm tm) + MS.SetupCond_Ghost md var val -> learnGhost sc md prepost var val --- TODO(lb): make this language-independent! -learnGhost :: - SharedContext -> - LLVMCrucibleContext arch -> - MS.ConditionMetadata -> - PrePost -> - MS.GhostGlobal -> - TypedTerm -> - OverrideMatcher (LLVM arch) md () -learnGhost sc cc md prepost var (TypedTerm (TypedTermSchema schEx) tmEx) = - do (sch,tm) <- readGlobal var - when (sch /= schEx) $ fail $ unlines $ - [ "Ghost variable had the wrong type:" - , "- Expected: " ++ show (Cryptol.pp schEx) - , "- Actual: " ++ show (Cryptol.pp sch) - ] - instantiateExtMatchTerm sc cc md prepost tm tmEx -learnGhost _sc _cc _md _prepost _var (TypedTerm tp _) - = fail $ unlines - [ "Ghost variable expected value has improper type" - , "expected Cryptol schema type, but got" - , show (MS.ppTypedTermType tp) - ] ------------------------------------------------------------------------ @@ -1553,7 +1457,7 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val = off_tm -- src offset instantiated_expected_sz_tm -- length - instantiateExtMatchTerm sc cc md prepost arr_tm $ ttTerm expected_arr_tm + instantiateExtMatchTerm sc md prepost arr_tm $ ttTerm expected_arr_tm sz_tm <- liftIO $ toSC sym st sz expected_end_off_tm <- liftIO $ scBvAdd sc ptr_width_tm off_tm $ ttTerm expected_sz_tm @@ -1979,27 +1883,7 @@ executeSetupCondition opts sc cc spec = MS.SetupCond_Equal md val1 val2 -> executeEqual opts sc cc spec md val1 val2 MS.SetupCond_Pred md tm -> executePred sc cc md tm - MS.SetupCond_Ghost () md var val -> executeGhost sc md var val - ------------------------------------------------------------------------- - --- TODO(lb): make this language independent! -executeGhost :: - SharedContext -> - MS.ConditionMetadata -> - MS.GhostGlobal -> - TypedTerm -> - OverrideMatcher (LLVM arch) RW () -executeGhost sc _md var (TypedTerm (TypedTermSchema sch) tm) = - do s <- OM (use termSub) - tm' <- liftIO (scInstantiateExt sc s tm) - writeGlobal var (sch,tm') -executeGhost _sc _md _var (TypedTerm tp _) = - fail $ unlines - [ "executeGhost: improper value type" - , "expected Cryptol schema type, but got" - , show (MS.ppTypedTermType tp) - ] + MS.SetupCond_Ghost md var val -> executeGhost sc md var val ------------------------------------------------------------------------ diff --git a/src/SAWScript/Crucible/LLVM/Setup/Value.hs b/src/SAWScript/Crucible/LLVM/Setup/Value.hs index ac5baba510..9f301187f7 100644 --- a/src/SAWScript/Crucible/LLVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/LLVM/Setup/Value.hs @@ -130,8 +130,6 @@ type instance Setup.XSetupUnion (LLVM _) = () type instance Setup.XSetupGlobal (LLVM _) = () type instance Setup.XSetupGlobalInitializer (LLVM _) = () -type instance Setup.XGhostState (LLVM _) = () - type instance Setup.TypeName (LLVM arch) = CL.Ident type instance Setup.ExtType (LLVM arch) = CL.MemType diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index 341e6dac0c..c81a39546d 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -18,6 +18,7 @@ module SAWScript.Crucible.MIR.Builtins , mir_fresh_cryptol_var , mir_fresh_expanded_value , mir_fresh_var + , mir_ghost_value , mir_load_module , mir_points_to , mir_postcond @@ -81,7 +82,6 @@ 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 import System.IO (stdout) @@ -116,6 +116,7 @@ import Verifier.SAW.SharedTerm import Verifier.SAW.Simulator.What4.ReturnTrip import Verifier.SAW.TypedTerm +import SAWScript.Builtins (ghost_value) import SAWScript.Crucible.Common import qualified SAWScript.Crucible.Common.MethodSpec as MS import SAWScript.Crucible.Common.Override @@ -395,6 +396,13 @@ mir_fresh_var name mty = Nothing -> X.throwM $ MIRFreshVarInvalidType mty Just cty -> Setup.freshVariable sc name cty +mir_ghost_value :: + MS.GhostGlobal -> + TypedTerm -> + MIRSetupM () +mir_ghost_value ghost val = MIRSetupM $ + ghost_value ghost val + -- | Load a MIR JSON file and return a handle to it. mir_load_module :: String -> TopLevel Mir.RustModule mir_load_module inputFile = do @@ -757,32 +765,43 @@ setupPrePointsTos :: setupPrePointsTos mspec cc env pts mem0 = foldM (doPointsTo mspec cc env) mem0 pts --- | Collects boolean terms that should be assumed to be true. +-- | Sets up globals (ghost variable), and collects boolean terms +-- that should be assumed to be true. setupPrestateConditions :: MethodSpec -> MIRCrucibleContext -> Map MS.AllocIndex (Some (MirPointer Sym)) -> + Crucible.SymGlobalState Sym -> [SetupCondition] -> - IO [Crucible.LabeledPred Term AssumptionReason] + IO ( Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term AssumptionReason] + ) setupPrestateConditions mspec cc env = aux [] where tyenv = MS.csAllocations mspec nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames - aux acc [] = return acc + aux acc globals [] = return (globals, acc) - aux acc (MS.SetupCond_Equal loc val1 val2 : xs) = + aux acc globals (MS.SetupCond_Equal loc val1 val2 : xs) = do val1' <- resolveSetupVal cc env tyenv nameEnv val1 val2' <- resolveSetupVal cc env tyenv nameEnv val2 t <- assertEqualVals cc val1' val2' let lp = Crucible.LabeledPred t (loc, "equality precondition") - aux (lp:acc) xs + aux (lp:acc) globals xs - aux acc (MS.SetupCond_Pred loc tm : xs) = + aux acc globals (MS.SetupCond_Pred loc tm : xs) = let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in - aux (lp:acc) xs - - aux _ (MS.SetupCond_Ghost empty_ _ _ _ : _) = absurd empty_ + aux (lp:acc) globals xs + + aux acc globals (MS.SetupCond_Ghost _md var val : xs) = + case val of + TypedTerm (TypedTermSchema sch) tm -> + aux acc (Crucible.insertGlobal var (sch,tm) globals) xs + TypedTerm tp _ -> + fail $ unlines + [ "Setup term for global variable expected to have Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] verifyObligations :: MIRCrucibleContext -> @@ -962,7 +981,8 @@ verifyPrestate cc mspec globals0 = globals0 globals2 <- setupPrePointsTos mspec cc env (mspec ^. MS.csPreState . MS.csPointsTos) globals1 - cs <- setupPrestateConditions mspec cc env (mspec ^. MS.csPreState . MS.csConditions) + (globals3, cs) <- + setupPrestateConditions mspec cc env globals2 (mspec ^. MS.csPreState . MS.csConditions) args <- resolveArguments cc mspec env -- Check the type of the return setup value @@ -983,7 +1003,7 @@ verifyPrestate cc mspec globals0 = ] (Nothing, _) -> return () - return (args, cs, env, globals2) + return (args, cs, env, globals3) -- | Simulate a MIR function with Crucible as part of a 'mir_verify' command, -- making sure to install any overrides that the user supplies. @@ -1240,7 +1260,7 @@ setupCrucibleContext rm = (Crucible.UseCFG cfg (Crucible.postdomInfo cfg))) $ Map.elems cfgMap let simctx0 = Crucible.initSimContext bak - Mir.mirIntrinsicTypes halloc stdout + intrinsics halloc stdout bindings Mir.mirExtImpl SAWCruciblePersonality let globals0 = Crucible.emptyGlobals diff --git a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs index b66b3cc02a..c52292ea43 100644 --- a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs @@ -17,6 +17,7 @@ module SAWScript.Crucible.MIR.MethodSpecIR , mccSymGlobalState , mccStaticInitializerMap , mccHandleAllocator + , mccIntrinsicTypes , mccWithBackend , mccSym @@ -53,13 +54,20 @@ module SAWScript.Crucible.MIR.MethodSpecIR -- * Initial CrucibleSetupMethodSpec , initialDefCrucibleMethodSpecIR , initialCrucibleSetupState + + -- * Intrinsics + , intrinsics ) where import Control.Lens (Getter, Iso', Lens', (^.), iso, to) +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.SymbolRepr (SymbolRepr, knownSymbol) import qualified Prettyprinter as PP import Lang.Crucible.FunctionHandle (HandleAllocator) import Lang.Crucible.Simulator (SimContext(..)) +import Lang.Crucible.Simulator.Intrinsics + (IntrinsicMuxFn(IntrinsicMuxFn), IntrinsicTypes) import Mir.Generator import Mir.Intrinsics import qualified Mir.Mir as M @@ -73,6 +81,9 @@ import SAWScript.Crucible.MIR.Setup.Value mccHandleAllocator :: Getter MIRCrucibleContext HandleAllocator mccHandleAllocator = mccSimContext . to simHandleAllocator +mccIntrinsicTypes :: Getter MIRCrucibleContext (IntrinsicTypes Sym) +mccIntrinsicTypes = mccSimContext . to ctxIntrinsicTypes + mccWithBackend :: MIRCrucibleContext -> (forall solver. OnlineSolver solver => Backend solver -> a) -> @@ -127,3 +138,12 @@ initialCrucibleSetupState cc fn loc = (cc ^. mccRustModule ^. rmCS) fn loc + +-- | The default MIR intrinsics extended with the 'MS.GhostValue' intrinsic, +-- which powers ghost state. +intrinsics :: MapF.MapF SymbolRepr (IntrinsicMuxFn Sym) +intrinsics = + MapF.insert + (knownSymbol :: SymbolRepr MS.GhostValue) + IntrinsicMuxFn + mirIntrinsicTypes diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index bea3d78edf..0cee024cc5 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -69,10 +69,8 @@ import qualified What4.Interface as W4 import qualified What4.LabeledPred as W4 import qualified What4.ProgramLoc as W4 -import Verifier.SAW.Prelude (scEq) import Verifier.SAW.SharedTerm import Verifier.SAW.Simulator.What4.ReturnTrip (saw_ctx, toSC) -import Verifier.SAW.TypedAST import Verifier.SAW.TypedTerm import SAWScript.Crucible.Common @@ -120,22 +118,6 @@ assignVar cc md var sref@(Some ref) = do p <- liftIO (equalRefsPred cc ref ref') addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError "equality of aliased references" "")) -assignTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - MIRCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - MS.PrePost -> - VarIndex {- ^ external constant index -} -> - Term {- ^ value -} -> - OverrideMatcher MIR w () - -assignTerm sc cc md prepost var val = - do mb <- OM (use (termSub . at var)) - case mb of - Nothing -> OM (termSub . at var ?= val) - Just old -> - matchTerm sc cc md prepost val old - -- | When a specification is used as a composition override, this function -- checks that the postconditions of the specification fully specify (via -- @mir_points_to@ statements) the values of all local mutable allocations @@ -607,7 +589,7 @@ executeCond :: MIRCrucibleContext -> CrucibleMethodSpecIR -> StateSpec -> - OverrideMatcher MIR w () + OverrideMatcher MIR RW () executeCond opts sc cc cs ss = do refreshTerms sc ss F.traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs)) @@ -654,10 +636,13 @@ executeSetupCondition :: MIRCrucibleContext -> CrucibleMethodSpecIR -> SetupCondition -> - OverrideMatcher MIR w () -executeSetupCondition opts sc cc spec (MS.SetupCond_Equal md val1 val2) = executeEqual opts sc cc spec md val1 val2 -executeSetupCondition _ sc cc _ (MS.SetupCond_Pred md tm) = executePred sc cc md tm -executeSetupCondition _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty + OverrideMatcher MIR RW () +executeSetupCondition opts sc cc spec = + \case + MS.SetupCond_Equal md val1 val2 -> + executeEqual opts sc cc spec md val1 val2 + MS.SetupCond_Pred md tm -> executePred sc cc md tm + MS.SetupCond_Ghost md var val -> executeGhost sc md var val handleSingleOverrideBranch :: forall rtp args ret. Options {- ^ output/verbosity options -} -> @@ -995,10 +980,12 @@ learnPointsTo opts sc cc spec prepost (MirPointsTo md reference referents) = ] let innerShp = tyToShapeEq col referenceInnerMirTy referenceInnerTpr referentVal <- firstPointsToReferent referents - v <- liftIO $ Mir.readMirRefIO bak globals Mir.mirIntrinsicTypes + v <- liftIO $ Mir.readMirRefIO bak globals iTypes referenceInnerTpr referenceVal matchArg opts sc cc spec prepost md (MIRVal innerShp v) referenceInnerMirTy referentVal + where + iTypes = cc ^. mccIntrinsicTypes -- | Process a "mir_precond" statement from the precondition -- section of the CrucibleSetup block. @@ -1026,9 +1013,11 @@ learnSetupCondition :: MS.PrePost -> SetupCondition -> OverrideMatcher MIR w () -learnSetupCondition opts sc cc spec prepost (MS.SetupCond_Equal md val1 val2) = learnEqual opts sc cc spec md prepost val1 val2 -learnSetupCondition _opts sc cc _ prepost (MS.SetupCond_Pred md tm) = learnPred sc cc md prepost (ttTerm tm) -learnSetupCondition _opts _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty +learnSetupCondition opts sc cc spec prepost cond = + case cond of + MS.SetupCond_Equal md val1 val2 -> learnEqual opts sc cc spec md prepost val1 val2 + MS.SetupCond_Pred md tm -> learnPred sc cc md prepost (ttTerm tm) + MS.SetupCond_Ghost md var val -> learnGhost sc md prepost var val -- | Match the value of a function argument with a symbolic 'SetupValue'. matchArg :: @@ -1049,7 +1038,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected@(MS.SetupTerm expec = do sym <- Ov.getSymInterface failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy realTerm <- valueToSC sym md failMsg tval actual - matchTerm sc cc md prepost realTerm (ttTerm expectedTT) + matchTerm sc md prepost realTerm (ttTerm expectedTT) matchArg opts sc cc cs prepost md actual expectedTy expected = mccWithBackend cc $ \bak -> do @@ -1186,6 +1175,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = where colState = cc ^. mccRustModule . Mir.rmCS col = colState ^. Mir.collection + iTypes = cc ^. mccIntrinsicTypes tyenv = MS.csAllocations cs nameEnv = MS.csTypeNames cs @@ -1194,9 +1184,6 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = mkStructuralMismatch opts cc sc cs actual expected expectedTy notEq = notEqual prepost opts loc cc sc cs expected actual - iTypes :: Crucible.IntrinsicTypes Sym - iTypes = Mir.mirIntrinsicTypes - -- | For each points-to statement read the memory value through the -- given pointer (lhs) and match the value against the given pattern -- (rhs). Statements are processed in dependency order: a points-to @@ -1272,33 +1259,6 @@ matchPointsTos opts sc cc spec prepost = go False [] setupSlice (MirSetupSliceRange arr _start _end) = setupVars arr -matchTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - MIRCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - MS.PrePost -> - Term {- ^ exported concrete term -} -> - Term {- ^ expected specification term -} -> - OverrideMatcher MIR md () - -matchTerm _ _ _ _ real expect | real == expect = return () -matchTerm sc cc md prepost real expect = - do let loc = MS.conditionLoc md - free <- OM (use osFree) - case unwrapTermF expect of - FTermF (ExtCns ec) - | Set.member (ecVarIndex ec) free -> - do assignTerm sc cc md prepost (ecVarIndex ec) real - - _ -> - do t <- liftIO $ scEq sc real expect - let msg = unlines $ - [ "Literal equality " ++ MS.stateCond prepost --- , "Expected term: " ++ prettyTerm expect --- , "Actual term: " ++ prettyTerm real - ] - addTermEq t md $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" - -- | This function is responsible for implementing the \"override\" behavior -- of method specifications. The main work done in this function to manage -- the process of selecting between several possible different override @@ -1403,13 +1363,13 @@ methodSpecHandler opts sc cc mdMap css h = -- which involves writing values into memory, computing the return value, -- and computing postcondition predicates. methodSpecHandler_poststate :: - forall ret w. + forall ret. Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> MIRCrucibleContext {- ^ context for interacting with Crucible -} -> Crucible.TypeRepr ret {- ^ type representation of function return value -} -> CrucibleMethodSpecIR {- ^ specification for current function override -} -> - OverrideMatcher MIR w (Crucible.RegValue Sym ret) + OverrideMatcher MIR RW (Crucible.RegValue Sym ret) methodSpecHandler_poststate opts sc cc retTy cs = do executeCond opts sc cc cs (cs ^. MS.csPostState) computeReturnValue opts cc sc cs retTy (cs ^. MS.csRetValue) diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index 1426e62f02..4727199da3 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs @@ -422,7 +422,7 @@ resolveSetupVal mcc env tyenv nameEnv val = where cs = mcc ^. mccRustModule . Mir.rmCS col = cs ^. Mir.collection - iTypes = Mir.mirIntrinsicTypes + iTypes = mcc ^. mccIntrinsicTypes usizeBvLit :: Sym -> Int -> IO (W4.SymBV Sym Mir.SizeBits) usizeBvLit sym = W4.bvLit sym W4.knownNat . BV.mkBV W4.knownNat . toInteger @@ -967,7 +967,7 @@ doAlloc cc globals (Some ma) = do let col = cc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection let halloc = cc^.mccHandleAllocator let sym = backendGetSym bak - let iTypes = Mir.mirIntrinsicTypes + let iTypes = cc^.mccIntrinsicTypes Some tpr <- pure $ Mir.tyToRepr col (ma^.maMirType) -- Create an uninitialized `MirVector_PartialVector` of length 1 and @@ -1026,8 +1026,9 @@ doPointsTo mspec cc env globals (MirPointsTo _ reference referents) = , "Reference type: " ++ show referenceInnerTy , "Referent type: " ++ show (shapeType referentShp) ] - Mir.writeMirRefIO bak globals Mir.mirIntrinsicTypes referenceVal referentVal + Mir.writeMirRefIO bak globals iTypes referenceVal referentVal where + iTypes = cc ^. mccIntrinsicTypes tyenv = MS.csAllocations mspec nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs index f764de1f17..bbdfbd85a9 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -81,8 +81,6 @@ type instance MS.XSetupCast MIR = Void type instance MS.XSetupUnion MIR = Void type instance MS.XSetupGlobalInitializer MIR = () -type instance MS.XGhostState MIR = Void - type instance MS.TypeName MIR = Text type instance MS.ExtType MIR = M.Ty diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 9f4830e4a0..34a021d769 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3605,16 +3605,21 @@ primitives = Map.fromList ] -- Ghost state support - , prim "llvm_declare_ghost_state" + , prim "declare_ghost_state" "String -> TopLevel Ghost" - (pureVal llvm_declare_ghost_state) + (pureVal declare_ghost_state) Current [ "Allocates a unique ghost variable." ] + , prim "llvm_declare_ghost_state" + "String -> TopLevel Ghost" + (pureVal declare_ghost_state) + Current + [ "Legacy alternative name for `declare_ghost_state`." ] , prim "crucible_declare_ghost_state" "String -> TopLevel Ghost" - (pureVal llvm_declare_ghost_state) + (pureVal declare_ghost_state) Current - [ "Legacy alternative name for `llvm_declare_ghost_state`." ] + [ "Legacy alternative name for `declare_ghost_state`." ] , prim "llvm_ghost_value" "Ghost -> Term -> LLVMSetup ()" @@ -3628,6 +3633,20 @@ primitives = Map.fromList Current [ "Legacy alternative name for `llvm_ghost_value`."] + , prim "jvm_ghost_value" + "Ghost -> Term -> JVMSetup ()" + (pureVal jvm_ghost_value) + Current + [ "Specifies the value of a ghost variable. This can be used" + , "in the pre- and post- conditions of a setup block."] + + , prim "mir_ghost_value" + "Ghost -> Term -> MIRSetup ()" + (pureVal mir_ghost_value) + Current + [ "Specifies the value of a ghost variable. This can be used" + , "in the pre- and post- conditions of a setup block."] + , prim "llvm_spec_solvers" "LLVMSpec -> [String]" (\_ _ -> toValue llvm_spec_solvers) Current