diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 1d0de3c9da..9b67b98f3e 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -2122,8 +2122,6 @@ some parts of `mir_verify` are not currently implemented, so it is possible that using `mir_verify` on some programs will fail. Features that are not yet implemented include the following: -* MIR specifications that use overrides (i.e., the `[MIRSpec]` argument to - `mir_verify` must always be the empty list at present) * The ability to construct MIR `enum` values in specifications * The ability to specify the layout of slice values @@ -2995,18 +2993,18 @@ the target code. However, in some cases, it can be useful to use a `MethodSpec` to specify some code that either doesn't exist or is hard to prove. The previously-mentioned [`assume_unsat` tactic](#miscellaneous-tactics) omits proof but does not prevent -simulation of the function. To skip simulation altogether, one can use: +simulation of the function. To skip simulation altogether, one can use +one of the following commands: ~~~ llvm_unsafe_assume_spec : LLVMModule -> String -> LLVMSetup () -> TopLevel CrucibleMethodSpec -~~~ - -Or, in the experimental JVM implementation: -~~~ jvm_unsafe_assume_spec : JavaClass -> String -> JVMSetup () -> TopLevel JVMMethodSpec + +mir_unsafe_assume_spec : + MIRModule -> String -> MIRSetup () -> TopLevel MIRSpec ~~~ ## A Heap-Based Example diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index de9ccf68b8..73891254fb 100644 Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ diff --git a/intTests/test_mir_unsafe_assume_spec/Makefile b/intTests/test_mir_unsafe_assume_spec/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_unsafe_assume_spec/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_unsafe_assume_spec/test.linked-mir.json b/intTests/test_mir_unsafe_assume_spec/test.linked-mir.json new file mode 100644 index 0000000000..a5d29a520d --- /dev/null +++ b/intTests/test_mir_unsafe_assume_spec/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:6:7: 6:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::95d37a33656fd654"},"kind":"Constant"},"kind":"Call","pos":"test.rs:6:5: 6:9"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:6:5: 6:25"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:7:2: 7:2"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}]},"name":"test/ca04d5a3::g","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:10:5: 10:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:10:5: 10:22"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:11:2: 11:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}]},"name":"test/ca04d5a3::h","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:22:7: 22:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:22:10: 22:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::d8f5e5d50376e8aa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:22:5: 22:12"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:23:2: 23:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/ca04d5a3::q","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:32:22: 32:23","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::953fce25114368d0"}},"pos":"test.rs:33:17: 33:23","rhs":{"borrowkind":"Mut","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::953fce25114368d0"}},"pos":"test.rs:33:17: 33:23","rhs":{"borrowkind":"Mut","kind":"Ref","refvar":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::953fce25114368d0"}},"region":"unimplement"}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::953fce25114368d0"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::b153432b719d377c"},"kind":"Constant"},"kind":"Call","pos":"test.rs:33:5: 33:24"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::953fce25114368d0"}},"pos":"test.rs:34:17: 34:23","rhs":{"borrowkind":"Mut","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::953fce25114368d0"}},"pos":"test.rs:34:17: 34:23","rhs":{"borrowkind":"Mut","kind":"Ref","refvar":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::953fce25114368d0"}},"region":"unimplement"}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::953fce25114368d0"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::b153432b719d377c"},"kind":"Constant"},"kind":"Call","pos":"test.rs:34:5: 34:24"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:35:2: 35:2"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::953fce25114368d0"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::953fce25114368d0"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::953fce25114368d0"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::953fce25114368d0"}]},"name":"test/ca04d5a3::foo","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::95d37a33656fd654"},"kind":"Constant"},"kind":"Call","pos":"test.rs:14:5: 14:9"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:14:5: 14:25"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:15:2: 15:2"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}]},"name":"test/ca04d5a3::g2","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:18:5: 18:44","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/ca04d5a3286a7930::{{alloc}}[0]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:18:5: 18:44","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:18:5: 18:44","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:18:5: 18:44","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","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":"_23","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"test.rs:18:20: 18:43","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/ca04d5a3286a7930::{{alloc}}[1]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"test.rs:18:20: 18:43","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"test.rs:18:20: 18:43","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Ref::675b2a8049aad652"}},"pos":"test.rs:18:20: 18:43","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","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":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:18:5: 18:44","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/ca04d5a3286a7930::{{alloc}}[2]","kind":"static_ref"},"ty":"ty::Ref::d0bd7bf253977b90"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:18:5: 18:44","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"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:18:5: 18:44","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_19","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:18:5: 18:44","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","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":"_16","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_19","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_15","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:18:5: 18:44"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_14","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:18:5: 18:44","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_15","ty":"ty::Adt::ba5184b53bc36a4d"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:18:5: 18:44","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_14","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","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:18:5: 18:44"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_11","ty":"ty::Array::6167cd8fdeb01e06"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:18:5: 18:44","rhs":{"akind":{"kind":"Array","ty":"ty::Adt::613f1953a8669d14"},"kind":"Aggregate","ops":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::Adt::613f1953a8669d14"}},"kind":"Move"}]}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_10","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:18:5: 18:44","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_11","ty":"ty::Array::6167cd8fdeb01e06"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:18:5: 18:44","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_10","ty":"ty::Ref::41f3f8f95d02c3e9"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:18:5: 18:44","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","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":"_5","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","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:18:5: 18:44"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","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:18:5: 18:44"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":true,"mut":{"kind":"Not"},"name":"_3","ty":"ty::Never::7199a9b06188843c"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_7","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_10","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_11","ty":"ty::Array::6167cd8fdeb01e06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::Adt::613f1953a8669d14"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_14","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_15","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_19","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Ref::c2a5dcbb98af2a61"}]},"name":"test/ca04d5a3::p","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:2:5: 2:45","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/ca04d5a3286a7930::{{alloc}}[3]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:2:5: 2:45","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:2:5: 2:45","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !test.rs:2:5: 2:45","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","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":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"test.rs:2:20: 2:44","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/ca04d5a3286a7930::{{alloc}}[4]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_17","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"test.rs:2:20: 2:44","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":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"test.rs:2:20: 2:44","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_17","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::675b2a8049aad652"}},"pos":"test.rs:2:20: 2:44","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","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::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:45","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/ca04d5a3286a7930::{{alloc}}[2]","kind":"static_ref"},"ty":"ty::Ref::d0bd7bf253977b90"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:45","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:45","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:45","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_19","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":"_15","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_14","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:45"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:45","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_14","ty":"ty::Adt::ba5184b53bc36a4d"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !test.rs:2:5: 2:45","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","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:45"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_10","ty":"ty::Array::6167cd8fdeb01e06"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:2:5: 2:45","rhs":{"akind":{"kind":"Array","ty":"ty::Adt::613f1953a8669d14"},"kind":"Aggregate","ops":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Adt::613f1953a8669d14"}},"kind":"Move"}]}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:2:5: 2:45","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_10","ty":"ty::Array::6167cd8fdeb01e06"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:2:5: 2:45","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Ref::41f3f8f95d02c3e9"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !test.rs:2:5: 2:45","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","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":"_4","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","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:45"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","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:45"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":true,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Never::7199a9b06188843c"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_10","ty":"ty::Array::6167cd8fdeb01e06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Adt::613f1953a8669d14"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_14","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_17","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::c2a5dcbb98af2a61"}]},"name":"test/ca04d5a3::f","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::953fce25114368d0"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:26:18: 26:20","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::953fce25114368d0"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::953fce25114368d0"}},"pos":"test.rs:27:5: 27:11","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"0"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:29:2: 29:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"test/ca04d5a3::side_effect","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::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:13: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1163:10: 1163:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}]},"name":"core/73237d41::num::{impl#9}::wrapping_add","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::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/ca04d5a3286a7930::{{alloc}}[5]","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/ca04d5a3286a7930::{{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":{"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":{"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":{"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::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/ca04d5a3286a7930::{{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/ca04d5a3286a7930::{{alloc}}[1]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[112,32,115,104,111,117,108,100,32,98,101,32,111,118,101,114,114,105,100,101,110]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"},{"kind":"constant","mutable":false,"name":"test/ca04d5a3286a7930::{{alloc}}[2]","rendered":{"element_ty":"ty::Adt::613f1953a8669d14","elements":[],"kind":"array"},"ty":"ty::Array::0e1a52ee2b2d3e97"},{"kind":"constant","mutable":false,"name":"test/ca04d5a3286a7930::{{alloc}}[3]","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/ca04d5a3286a7930::{{alloc}}[4]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[102,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/ca04d5a3286a7930::{{alloc}}[5]","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/ca04d5a3::g","kind":"Item","substs":[]},"name":"test/ca04d5a3::g"},{"inst":{"def_id":"test/ca04d5a3::h","kind":"Item","substs":[]},"name":"test/ca04d5a3::h"},{"inst":{"def_id":"test/ca04d5a3::q","kind":"Item","substs":[]},"name":"test/ca04d5a3::q"},{"inst":{"def_id":"test/ca04d5a3::foo","kind":"Item","substs":[]},"name":"test/ca04d5a3::foo"},{"inst":{"def_id":"test/ca04d5a3::g2","kind":"Item","substs":[]},"name":"test/ca04d5a3::g2"},{"inst":{"def_id":"test/ca04d5a3::p","kind":"Item","substs":[]},"name":"test/ca04d5a3::p"},{"inst":{"def_id":"test/ca04d5a3::f","kind":"Item","substs":[]},"name":"test/ca04d5a3::f"},{"inst":{"def_id":"test/ca04d5a3::side_effect","kind":"Item","substs":[]},"name":"test/ca04d5a3::side_effect"},{"inst":{"def_id":"core/73237d41::panicking::panic_fmt","kind":"Item","substs":[]},"name":"core/73237d41::panicking::panic_fmt"},{"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::num::{impl#9}::wrapping_add","kind":"Item","substs":[]},"name":"core/73237d41::num::{impl#9}::wrapping_add"},{"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::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::95d37a33656fd654","ty":{"defid":"test/ca04d5a3::f","kind":"FnDef"}},{"name":"ty::FnDef::f55acdef755f1aaa","ty":{"defid":"core/73237d41::num::{impl#9}::wrapping_add","kind":"FnDef"}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"name":"ty::FnDef::d8f5e5d50376e8aa","ty":{"defid":"test/ca04d5a3::p","kind":"FnDef"}},{"name":"ty::Ref::953fce25114368d0","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::u32"}},{"name":"ty::FnDef::b153432b719d377c","ty":{"defid":"test/ca04d5a3::side_effect","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::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::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}},{"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/ca04d5a3::f","test/ca04d5a3::g","test/ca04d5a3::h","test/ca04d5a3::g2","test/ca04d5a3::p","test/ca04d5a3::q","test/ca04d5a3::side_effect","test/ca04d5a3::foo"]} \ No newline at end of file diff --git a/intTests/test_mir_unsafe_assume_spec/test.rs b/intTests/test_mir_unsafe_assume_spec/test.rs new file mode 100644 index 0000000000..062ad042ed --- /dev/null +++ b/intTests/test_mir_unsafe_assume_spec/test.rs @@ -0,0 +1,35 @@ +pub fn f(_x: u32) -> u32 { + unimplemented!("f should be overridden"); +} + +pub fn g(x: u32) -> u32 { + f(x).wrapping_add(1) +} + +pub fn h(x: u32) -> u32 { + x.wrapping_add(1) +} + +pub fn g2() -> u32 { + f(2).wrapping_add(1) +} + +pub fn p(_x: &u32, _y: &u32) -> u32 { + unimplemented!("p should be overriden"); +} + +pub fn q(x: &u32, y: &u32) -> u32 { + p(x, y) +} + +pub fn side_effect(a: &mut u32) -> u32 { + let v: u32 = *a; + *a = 0; + v +} + +pub fn foo(x: u32) -> u32 { + let mut b: u32 = x; + side_effect(&mut b); + side_effect(&mut b) +} diff --git a/intTests/test_mir_unsafe_assume_spec/test.saw b/intTests/test_mir_unsafe_assume_spec/test.saw new file mode 100644 index 0000000000..c37e1d645a --- /dev/null +++ b/intTests/test_mir_unsafe_assume_spec/test.saw @@ -0,0 +1,158 @@ +enable_experimental; + +let f_generic_spec (x : Term) = do { + mir_execute_func [mir_term x]; + + mir_return (mir_term x); +}; + +let f_spec = do { + x <- mir_fresh_var "x" mir_u32; + f_generic_spec x; +}; + +let f2_spec = do { + let x = {{ 2 : [32] }}; + f_generic_spec x; +}; + +let f3_spec = do { + let x = {{ 3 : [32] }}; + f_generic_spec x; +}; + +let g_spec = do { + x <- mir_fresh_var "x" mir_u32; + + mir_execute_func [mir_term x]; + + mir_return (mir_term {{ x + 1 }}); +}; + +let g2_spec = do { + mir_execute_func []; + + mir_return (mir_term {{ 3 : [32] }}); +}; + +let h_spec = g_spec; + +let p_spec_1 = do { + x_ptr <- mir_alloc mir_u32; + x <- mir_fresh_var "x" mir_u32; + mir_points_to x_ptr (mir_term x); + + y_ptr <- mir_alloc mir_u32; + y <- mir_fresh_var "y" mir_u32; + mir_points_to y_ptr (mir_term y); + + mir_execute_func [x_ptr, y_ptr]; + + mir_return (mir_term {{ x + y }}); +}; + +let p_spec_2 = do { + x_ptr <- mir_alloc mir_u32; + x <- mir_fresh_var "x" mir_u32; + mir_points_to x_ptr (mir_term x); + + mir_execute_func [x_ptr, x_ptr]; + + mir_return (mir_term {{ 2 * x }}); +}; + +let q_spec = p_spec_1; + +let side_spec_1 = do { + a_ptr <- mir_alloc_mut mir_u32; + a <- mir_fresh_var "a" mir_u32; + mir_points_to a_ptr (mir_term a); + + mir_execute_func [a_ptr]; + + mir_points_to a_ptr (mir_term {{ 0 : [32] }}); + mir_return (mir_term a); +}; + +let side_spec_2 = do { + a_ptr <- mir_alloc_mut mir_u32; + a <- mir_fresh_var "a" mir_u32; + mir_points_to a_ptr (mir_term a); + + mir_execute_func [a_ptr]; + + mir_return (mir_term a); +}; + +let foo_spec = do { + x <- mir_fresh_var "x" mir_u32; + + mir_execute_func [mir_term x]; + + mir_return (mir_term {{ x }}); +}; + +m <- mir_load_module "test.linked-mir.json"; + +//////////// +// Basics // +//////////// + +f_ov <- mir_unsafe_assume_spec m "test::f" f_spec; +f2_ov <- mir_unsafe_assume_spec m "test::f" f2_spec; +f3_ov <- mir_unsafe_assume_spec m "test::f" f3_spec; + +// `g` should fail without an override for `f`... +fails ( + mir_verify m "test::g" [] false g_spec z3 +); +// ...but should succeed with an `f` override. +mir_verify m "test::g" [f_ov] false g_spec z3; +// `h` never calls `f`, but it's still fine to redundantly pass an `f` override +mir_verify m "test::h" [f_ov] false h_spec z3; + +// `g2` will succeed with both a generic `f` override as well as a specialized +// one where the argument and result values are concrete. +mir_verify m "test::g2" [f_ov] false g2_spec z3; +mir_verify m "test::g2" [f2_ov] false g2_spec z3; +mir_verify m "test::g2" [f_ov, f2_ov] false g2_spec z3; + +// Overrides that fail to match. +fails ( + mir_verify m "test::g" [f3_ov] false g_spec z3 +); +fails ( + mir_verify m "test::g2" [f3_ov] false g2_spec z3 +); + +////////////// +// Pointers // +////////////// + +p_ov_1 <- mir_unsafe_assume_spec m "test::p" p_spec_1; +p_ov_2 <- mir_unsafe_assume_spec m "test::p" p_spec_2; + +mir_verify m "test::q" [p_ov_1] false q_spec z3; +fails ( + mir_verify m "test::q" [p_ov_2] false q_spec z3 +); + +/////////////////////// +// Avoid unsoundness // +/////////////////////// + +// https://github.com/GaloisInc/saw-script/issues/30 + +side_ov_1 <- mir_verify m "test::side_effect" [] false side_spec_1 z3; +side_ov_2 <- mir_verify m "test::side_effect" [] false side_spec_2 z3; + +fails ( + mir_verify m "test::foo" [side_ov_1] false foo_spec z3 +); +// TODO: This should not verify, as side_spec_2 underspecifies the mutable +// allocation `a_ptr`. We need to implement a check that catches this. +// fails ( +// mir_verify m "test::foo" [side_ov_2] false foo_spec z3 +// ); + +// TODO: Add similar tests for mutable statics. diff --git a/intTests/test_mir_unsafe_assume_spec/test.sh b/intTests/test_mir_unsafe_assume_spec/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_unsafe_assume_spec/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md index a7e3531764..17f8f73d2e 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -8,6 +8,8 @@ * The `SAW/MIR/verify` command performs verification of a MIR function. * The `SAW/MIR/find ADT` command looks up an algebraic data type (ADT) name in a MIR module. + * The `SAW/MIR/assume` command assumes a specification for a MIR function + without performing any verification. See the [remote API documentation](https://github.com/GaloisInc/saw-script/blob/master/saw-remote-api/docs/SAW.rst#sawmirload-module-command) diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index 6a25dcc327..bb6f462977 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -8,7 +8,8 @@ * The `mir_verify` function performs verification of a MIR function. * The `mir_find_adt` function looks up an algebraic data type (ADT) name in a MIR module. - + * The `mir_assume` function assumes a specification for a MIR function without + performing any verification. * The `saw_client.mir` module contains utility functions for constructing MIR types. diff --git a/saw-remote-api/src/SAWServer/MIRVerify.hs b/saw-remote-api/src/SAWServer/MIRVerify.hs index 09261a2f8c..5106396341 100644 --- a/saw-remote-api/src/SAWServer/MIRVerify.hs +++ b/saw-remote-api/src/SAWServer/MIRVerify.hs @@ -11,7 +11,7 @@ import Prelude hiding (mod) import Control.Lens import SAWScript.Crucible.MIR.Builtins - ( mir_verify ) + ( mir_unsafe_assume_spec, mir_verify ) import SAWScript.Value (rwCryptol) import qualified Argo @@ -61,7 +61,7 @@ mirVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scri proofScript <- interpretProofScript script tl $ mir_verify rm fun lemmas checkSat setup proofScript AssumeContract -> - tl $ error "mir_unsafe_assume_spec not yet supported" + tl $ mir_unsafe_assume_spec rm fun setup dropTask setServerVal lemmaName res ok diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs index e09eba8ac9..48d31e1b66 100644 --- a/src/SAWScript/Crucible/Common/Override.hs +++ b/src/SAWScript/Crucible/Common/Override.hs @@ -78,10 +78,10 @@ import qualified Control.Monad.Fail as Fail import Control.Monad.Trans.Except import Control.Monad.Trans.Class import Control.Monad.IO.Class -import Data.Proxy (Proxy(..)) import qualified Data.Map as Map import Data.Map (Map) import Data.Maybe (fromMaybe) +import Data.Proxy (Proxy(..)) import Data.Set (Set) import Data.Typeable (Typeable) import Data.Void diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index 63d76ac0b3..5a157f1865 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -21,6 +21,7 @@ module SAWScript.Crucible.MIR.Builtins , mir_postcond , mir_precond , mir_return + , mir_unsafe_assume_spec , mir_verify -- ** MIR types , mir_adt @@ -55,11 +56,12 @@ import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Reader (runReaderT) import Control.Monad.State (MonadState(..), StateT(..), execStateT, gets) import Control.Monad.Trans.Class (MonadTrans(..)) -import qualified Data.BitVector.Sized as BV import qualified Data.ByteString.Lazy as BSL import Data.Foldable (for_) import Data.IORef -import qualified Data.List.Extra as List (find, groupOn) +import qualified Data.List as List (find) +import qualified Data.List.NonEmpty as NE +import Data.List.NonEmpty (NonEmpty(..)) import qualified Data.Map as Map import Data.Map (Map) import Data.Maybe (fromMaybe) @@ -123,6 +125,7 @@ import SAWScript.Panic import qualified SAWScript.Position as SS import SAWScript.Proof import SAWScript.Prover.SolverStats +import SAWScript.Utils (neGroupOn) import SAWScript.Value type AssumptionReason = (MS.ConditionMetadata, String) @@ -325,6 +328,22 @@ mir_points_to_check_lhs_validity ref loc = _ -> throwCrucibleSetup loc $ "lhs not a reference type: " ++ show (PP.pretty refTy) +mir_unsafe_assume_spec :: + Mir.RustModule -> + String {- ^ Name of the function -} -> + MIRSetupM () {- ^ Boundary specification -} -> + TopLevel Lemma +mir_unsafe_assume_spec rm nm setup = + do cc <- setupCrucibleContext rm + pos <- getPosition + let loc = SS.toW4Loc "_SAW_assume_spec" pos + fn <- findFn rm nm + let st0 = initialCrucibleSetupState cc fn loc + ms <- (view Setup.csMethodSpec) <$> + execStateT (runReaderT (runMIRSetupM setup) Setup.makeCrucibleSetupRO) st0 + ps <- io (MS.mkProvedSpec MS.SpecAdmitted ms mempty mempty mempty 0) + returnProof ps + mir_verify :: Mir.RustModule -> String {- ^ method name -} -> @@ -345,19 +364,16 @@ mir_verify rm nm lemmas checkSat setup tactic = let sym = cc^.mccSym let globals0 = cc^.mccSymGlobalState + sosp <- rwSingleOverrideSpecialCase <$> getTopLevelRW + let ?singleOverrideSpecialCase = sosp + pos <- getPosition let loc = SS.toW4Loc "_SAW_verify_prestate" pos profFile <- rwProfilingFile <$> getTopLevelRW (writeFinalProfile, pfs) <- io $ setupProfiling sym "mir_verify" profFile - let cs = rm ^. Mir.rmCS - col = cs ^. Mir.collection - crateDisambigs = cs ^. Mir.crateHashesMap - did <- findDefId crateDisambigs (Text.pack nm) - fn <- case Map.lookup did (col ^. Mir.functions) of - Just x -> return x - Nothing -> fail $ "Couldn't find MIR function named: " ++ nm + fn <- findFn rm nm let st0 = initialCrucibleSetupState cc fn loc -- execute commands of the method spec @@ -491,18 +507,22 @@ assertEqualVals cc v1 v2 = toSC sym st =<< equalValsPred cc v1 v2 registerOverride :: + (?singleOverrideSpecialCase :: Bool) => Options -> MIRCrucibleContext -> Crucible.SimContext (SAWCruciblePersonality Sym) Sym MIR -> W4.ProgramLoc -> IORef MetadataMap {- ^ metadata map -} -> - [MethodSpec] -> + NonEmpty MethodSpec -> Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym MIR rtp args ret () -registerOverride _opts cc _ctx _top_loc _mdMap cs = - do let c0 = head cs +registerOverride opts cc _ctx _top_loc mdMap cs = + do let sym = cc^.mccSym + let c0 = NE.head cs let method = c0 ^. MS.csMethod let rm = cc^.mccRustModule + sc <- saw_ctx <$> liftIO (sawCoreState sym) + Crucible.AnyCFG cfg <- lookupDefIdCFG rm method let h = Crucible.cfgHandle cfg let retTy = Crucible.handleReturnType h @@ -512,7 +532,7 @@ registerOverride _opts cc _ctx _top_loc _mdMap cs = $ Crucible.mkOverride' (Crucible.handleName h) retTy - (panic "registerOverride.methodSpecHandler" ["not yet implemented"]) + (methodSpecHandler opts sc cc mdMap cs h) resolveArguments :: MIRCrucibleContext -> @@ -553,46 +573,8 @@ setupPrePointsTos :: [MirPointsTo] -> Crucible.SymGlobalState Sym -> IO (Crucible.SymGlobalState Sym) -setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts - where - tyenv = MS.csAllocations mspec - nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames - - doPointsTo :: - Crucible.SymGlobalState Sym - -> MirPointsTo - -> IO (Crucible.SymGlobalState Sym) - doPointsTo globals (MirPointsTo _ reference referents) = - mccWithBackend cc $ \bak -> do - MIRVal referenceShp referenceVal <- - resolveSetupVal cc env tyenv nameEnv reference - -- By the time we reach here, we have already checked (in mir_points_to) - -- that we are in fact dealing with a reference value, so the call to - -- `testRefShape` below should always succeed. - IsRefShape _ _ _ referenceInnerTy <- - case testRefShape referenceShp of - Just irs -> pure irs - Nothing -> - panic "setupPrePointsTos" - [ "Unexpected non-reference type:" - , show $ PP.pretty $ shapeMirTy referenceShp - ] - referent <- firstPointsToReferent referents - MIRVal referentShp referentVal <- - resolveSetupVal cc env tyenv nameEnv referent - -- By the time we reach here, we have already checked (in mir_points_to) - -- that the type of the reference is compatible with the right-hand side - -- value, so the equality check below should never fail. - Refl <- - case W4.testEquality referenceInnerTy (shapeType referentShp) of - Just r -> pure r - Nothing -> - panic "setupPrePointsTos" - [ "Unexpected type mismatch between reference and referent" - , "Reference type: " ++ show referenceInnerTy - , "Referent type: " ++ show (shapeType referentShp) - ] - Mir.writeMirRefIO bak globals Mir.mirIntrinsicTypes referenceVal referentVal +setupPrePointsTos mspec cc env pts mem0 = + foldM (doPointsTo mspec cc env) mem0 pts -- | Collects boolean terms that should be assumed to be true. setupPrestateConditions :: @@ -793,7 +775,9 @@ verifyPrestate cc mspec globals0 = liftIO $ W4.setCurrentProgramLoc sym prestateLoc (env, globals1) <- runStateT - (traverse (doAlloc cc) (mspec ^. MS.csPreState . MS.csAllocs)) + (traverse + (\alloc -> StateT (\globals -> doAlloc cc globals alloc)) + (mspec ^. MS.csPreState . MS.csAllocs)) globals0 globals2 <- setupPrePointsTos mspec cc env (mspec ^. MS.csPreState . MS.csPointsTos) globals1 @@ -823,6 +807,7 @@ verifyPrestate cc mspec globals0 = -- | Simulate a MIR function with Crucible as part of a 'mir_verify' command, -- making sure to install any overrides that the user supplies. verifySimulate :: + (?singleOverrideSpecialCase :: Bool) => Options -> MIRCrucibleContext -> [Crucible.GenericExecutionFeature Sym] -> @@ -859,7 +844,7 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat m let fnCall = Crucible.regValue <$> Crucible.callCFG methodCfg regmap let overrideSim = do mapM_ (registerOverride opts cc simctx top_loc mdMap) - (List.groupOn (view MS.csMethod) (map (view MS.psSpec) lemmas)) + (neGroupOn (view MS.csMethod) (map (view MS.psSpec) lemmas)) liftIO $ for_ assumes $ \(Crucible.LabeledPred p (md, reason)) -> do expr <- resolveSAWPred cc p @@ -949,41 +934,6 @@ cryptolTypeOfActual mty = baseSizeType Mir.B128 = Just $ Cryptol.tWord $ Cryptol.tNum (128 :: Integer) baseSizeType Mir.USize = Just $ Cryptol.tWord $ Cryptol.tNum $ natValue $ knownNat @Mir.SizeBits --- | Allocate memory for each 'mir_alloc' or 'mir_alloc_mut'. -doAlloc :: - MIRCrucibleContext - -> Some MirAllocSpec - -> StateT (Crucible.SymGlobalState Sym) IO (Some (MirPointer Sym)) -doAlloc cc (Some ma) = - mccWithBackend cc $ \bak -> - do let col = cc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection - let halloc = cc^.mccHandleAllocator - let sym = backendGetSym bak - let iTypes = Mir.mirIntrinsicTypes - Some tpr <- pure $ Mir.tyToRepr col (ma^.maMirType) - - -- Create an uninitialized `MirVector_PartialVector` of length 1 and - -- return a pointer to its element. - ref <- liftIO $ - Mir.newMirRefIO sym halloc (Mir.MirVectorRepr tpr) - - globals <- get - globals' <- liftIO $ do - one <- W4.bvLit sym W4.knownRepr $ BV.mkBV W4.knownRepr 1 - vec <- Mir.mirVector_uninitIO bak one - Mir.writeMirRefIO bak globals iTypes ref vec - put globals' - - ptr <- liftIO $ do - zero <- W4.bvLit sym W4.knownRepr $ BV.mkBV W4.knownRepr 0 - Mir.subindexMirRefIO bak iTypes tpr ref zero - pure $ Some MirPointer - { _mpType = tpr - , _mpMutbl = ma^.maMutbl - , _mpMirType = ma^.maMirType - , _mpRef = ptr - } - -- Find the ADT definition that is monomorphized from `origName` with `substs`. -- This should only be used on types that are known to be present in the crate -- after dead code elimination - for example, because the type appears in the @@ -996,6 +946,20 @@ findAdt col origName substs = where insts = col ^. Mir.adtsOrig . at origName . to (fromMaybe []) +-- | Find the 'Mir.Fn' corresponding to the given function name (supplied as a +-- 'String'). If none can be found or if there are multiple functions +-- corresponding to that name (see the Haddocks for 'findDefId'), then this will +-- fail. +findFn :: Mir.RustModule -> String -> TopLevel Mir.Fn +findFn rm nm = do + let cs = rm ^. Mir.rmCS + col = cs ^. Mir.collection + crateDisambigs = cs ^. Mir.crateHashesMap + did <- findDefId crateDisambigs (Text.pack nm) + case Map.lookup did (col ^. Mir.functions) of + Just x -> return x + Nothing -> fail $ "Couldn't find MIR function named: " ++ nm + getMIRCrucibleContext :: CrucibleSetup MIR MIRCrucibleContext getMIRCrucibleContext = view Setup.csCrucibleContext <$> get diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index ccb4f7fb21..bdc16e255b 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -1,5 +1,10 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} -- | Override matching and application for MIR. @@ -14,18 +19,24 @@ module SAWScript.Crucible.MIR.Override , learnCond , matchArg + , methodSpecHandler , decodeMIRVal ) where import qualified Control.Exception as X import Control.Lens -import Control.Monad (unless) +import Control.Monad (filterM, forM, forM_, unless, zipWithM) import Control.Monad.IO.Class (MonadIO(..)) +import Data.Either (partitionEithers) +import qualified Data.Foldable as F import Data.Foldable (for_, traverse_) import qualified Data.Functor.Product as Functor +import Data.IORef (IORef, modifyIORef) import Data.List (tails) +import qualified Data.List.NonEmpty as NE import qualified Data.Map as Map import Data.Map (Map) +import Data.Maybe (catMaybes) import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Some (Some(..)) import qualified Data.Parameterized.TraversableFC as FC @@ -37,6 +48,8 @@ import qualified Prettyprinter as PP import qualified Cryptol.TypeCheck.AST as Cryptol import qualified Cryptol.Eval.Type as Cryptol (TValue(..), evalType) +import qualified Lang.Crucible.Backend as Crucible +import qualified Lang.Crucible.FunctionHandle as Crucible import qualified Lang.Crucible.Simulator as Crucible import qualified Lang.Crucible.Types as Crucible import qualified Mir.Generator as Mir @@ -46,6 +59,7 @@ import qualified Mir.Mir as Mir import qualified Mir.TransTy as Mir import qualified What4.Expr as W4 import qualified What4.Interface as W4 +import qualified What4.LabeledPred as W4 import qualified What4.ProgramLoc as W4 import Verifier.SAW.Prelude (scEq) @@ -64,7 +78,7 @@ import SAWScript.Crucible.MIR.ResolveSetupValue import SAWScript.Crucible.MIR.TypeShape import SAWScript.Options import SAWScript.Panic (panic) -import SAWScript.Utils (handleException) +import SAWScript.Utils (bullets, handleException) -- A few convenient synonyms type SetupValue = MS.SetupValue MIR @@ -115,6 +129,29 @@ assignTerm sc cc md prepost var val = Just old -> matchTerm sc cc md prepost val old +computeReturnValue :: + Options {- ^ saw script debug and print options -} -> + MIRCrucibleContext {- ^ context of the crucible simulation -} -> + SharedContext {- ^ context for generating saw terms -} -> + MS.CrucibleMethodSpecIR MIR {- ^ method specification -} -> + Crucible.TypeRepr ret {- ^ representation of function return type -} -> + Maybe SetupValue {- ^ optional symbolic return value -} -> + OverrideMatcher MIR md (Crucible.RegValue Sym ret) + {- ^ concrete return value -} +computeReturnValue opts cc sc spec ty mbVal = + case mbVal of + Nothing -> + case ty of + Crucible.UnitRepr -> return () + _ -> fail_ + Just val -> do + MIRVal shp val' <- resolveSetupValueMIR opts cc sc spec val + case W4.testEquality ty (shapeType shp) of + Just Refl -> pure val' + Nothing -> fail_ + where + fail_ = failure (spec ^. MS.csLoc) (BadReturnSpecification (Some ty)) + decodeMIRVal :: Mir.Collection -> Mir.Ty -> Crucible.AnyValue Sym -> Maybe MIRVal decodeMIRVal col ty (Crucible.AnyValue repr rv) | Some shp <- tyToShape col ty @@ -148,6 +185,314 @@ enforceDisjointness cc loc ss = , (_, Some q) <- ps ] +-- | Perform an allocation as indicated by a 'mir_alloc' +-- statement from the postcondition section. +executeAllocation :: + Options -> + MIRCrucibleContext -> + (AllocIndex, Some MirAllocSpec) -> + OverrideMatcher MIR w () +executeAllocation opts cc (var, someAlloc@(Some alloc)) = + do liftIO $ printOutLn opts Debug $ unwords ["executeAllocation:", show var, show alloc] + globals <- OM (use overrideGlobals) + (ptr, globals') <- liftIO $ doAlloc cc globals someAlloc + OM (overrideGlobals .= globals') + assignVar cc (alloc^.maConditionMetadata) var ptr + +-- | Process a "points_to" statement from the postcondition section of +-- the CrucibleSetup block. First we compute the value indicated by +-- 'val', and then write it to the address indicated by 'ptr'. +executePointsTo :: + Options -> + SharedContext -> + MIRCrucibleContext -> + CrucibleMethodSpecIR -> + MirPointsTo -> + OverrideMatcher MIR w () +executePointsTo _opts _sc cc spec pt = do + env <- OM (use setupValueSub) + globals <- OM (use overrideGlobals) + globals' <- liftIO $ doPointsTo spec cc env globals pt + OM (overrideGlobals .= globals') + +-- execute a pre/post condition +executeCond :: + Options -> + SharedContext -> + MIRCrucibleContext -> + CrucibleMethodSpecIR -> + StateSpec -> + OverrideMatcher MIR w () +executeCond opts sc cc cs ss = + do refreshTerms sc ss + traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs)) + -- TODO: We need to do something like this: + {- + checkMutableAllocPostconds opts sc cc cs + -} + -- Which checks that all of the mutable allocations and statics have been + -- specified in the postconditions of overrides. (See the related TODOs + -- in the test_mir_unsafe_assume_spec test case.) + traverse_ (executePointsTo opts sc cc cs) (ss ^. MS.csPointsTos) + traverse_ (executeSetupCondition opts sc cc cs) (ss ^. MS.csConditions) + +-- | Process a "mir_equal" statement from the postcondition +-- section of the CrucibleSetup block. +executeEqual :: + Options -> + SharedContext -> + MIRCrucibleContext -> + CrucibleMethodSpecIR -> + MS.ConditionMetadata -> + SetupValue {- ^ first value to compare -} -> + SetupValue {- ^ second value to compare -} -> + OverrideMatcher MIR w () +executeEqual opts sc cc spec md v1 v2 = + do val1 <- resolveSetupValueMIR opts cc sc spec v1 + val2 <- resolveSetupValueMIR opts cc sc spec v2 + p <- liftIO (equalValsPred cc val1 val2) + addAssume p md + +-- | Process a "mir_postcond" statement from the postcondition +-- section of the CrucibleSetup block. +executePred :: + SharedContext -> + MIRCrucibleContext -> + MS.ConditionMetadata -> + TypedTerm {- ^ the term to assert as a postcondition -} -> + OverrideMatcher MIR w () +executePred sc cc md tt = + do s <- OM (use termSub) + t <- liftIO $ scInstantiateExt sc s (ttTerm tt) + p <- liftIO $ resolveBoolTerm (cc ^. mccSym) t + addAssume p md + +-- | Update the simulator state based on the postconditions from the +-- procedure specification. +executeSetupCondition :: + Options -> + SharedContext -> + 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 + +handleSingleOverrideBranch :: forall rtp args ret. + Options {- ^ output/verbosity options -} -> + SharedContext {- ^ context for constructing SAW terms -} -> + MIRCrucibleContext {- ^ context for interacting with Crucible -} -> + W4.ProgramLoc {- ^ Location of the call site for error reporting -} -> + IORef MetadataMap -> + Crucible.FnHandle args ret {- ^ the handle for this function -} -> + OverrideWithPreconditions MIR -> + Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym MIR rtp args ret + (Crucible.RegValue Sym ret) +handleSingleOverrideBranch opts sc cc call_loc mdMap h (OverrideWithPreconditions preconds cs st) = + mccWithBackend cc $ \bak -> do + let sym = backendGetSym bak + let fnName = cs ^. MS.csMethod + let retTy = Crucible.handleReturnType h + + liftIO $ printOutLn opts Info $ unwords + [ "Found a single potential override for" + , show fnName + ] + + -- First assert the override preconditions + liftIO $ forM_ preconds $ \(md,W4.LabeledPred p r) -> + do (ann,p') <- W4.annotateTerm sym p + let caller = unwords ["Override called from:", show (W4.plSourceLoc call_loc)] + let md' = md{ MS.conditionContext = MS.conditionContext md ++ caller } + modifyIORef mdMap (Map.insert ann md') + Crucible.addAssertion bak (Crucible.LabeledPred p' r) + + g <- Crucible.readGlobals + res <- liftIO $ runOverrideMatcher sym g + (st^.setupValueSub) + (st^.termSub) + (st^.osFree) + (st^.osLocation) + (methodSpecHandler_poststate opts sc cc retTy cs) + case res of + Left (OF loc rsn) -> + -- TODO, better pretty printing for reasons + liftIO + $ Crucible.abortExecBecause + $ Crucible.AssertionFailure + $ Crucible.SimError loc + $ Crucible.AssertFailureSimError "assumed false" (show rsn) + Right (ret,st') -> + do liftIO $ forM_ (st'^.osAssumes) $ \(_md,asum) -> + Crucible.addAssumption bak + $ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum + Crucible.writeGlobals (st'^.overrideGlobals) + Crucible.overrideReturn' (Crucible.RegEntry retTy ret) + +handleOverrideBranches :: forall rtp args ret. + Options {- ^ output/verbosity options -} -> + SharedContext {- ^ context for constructing SAW terms -} -> + MIRCrucibleContext {- ^ context for interacting with Crucible -} -> + W4.ProgramLoc {- ^ Location of the call site for error reporting -} -> + NE.NonEmpty (MS.CrucibleMethodSpecIR MIR) + {- ^ specification for current function override -} -> + Crucible.FnHandle args ret {- ^ the handle for this function -} -> + [OverrideWithPreconditions MIR] -> + ([OverrideWithPreconditions MIR],[OverrideWithPreconditions MIR],[OverrideWithPreconditions MIR]) -> + Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym MIR rtp args ret + (Crucible.RegValue Sym ret) + +handleOverrideBranches opts sc cc call_loc css h branches (true, false, unknown) = + mccWithBackend cc $ \bak -> do + let sym = backendGetSym bak + let fnName = show $ NE.head css ^. MS.csMethod + Crucible.RegMap args <- Crucible.getOverrideArgs + + -- Collapse the preconditions to a single predicate + branches' <- liftIO $ forM (true ++ unknown) $ + \(OverrideWithPreconditions preconds cs st) -> + W4.andAllOf sym (folded . _2 . W4.labeledPred) preconds <&> + \precond -> (precond, cs, st) + + -- Now use crucible's symbolic branching machinery to select between the branches. + -- Essentially, we are doing an n-way if statement on the precondition predicates + -- for each override, and selecting the first one whose preconditions hold. + -- + -- Then, in the body of the branch, we run the poststate handler to update the + -- memory state, compute return values and compute postcondition predicates. + -- + -- For each override branch that doesn't fail outright, we assume the relevant + -- postconditions, update the crucible global variable state, and return the + -- computed return value. + -- + -- We add a final default branch that simply fails unless some previous override + -- branch has already succeeded. + liftIO $ printOutLn opts Info $ unwords + [ "Branching on" + , show (length branches') + , "override variants of" + , fnName + , "..." + ] + let retTy = Crucible.handleReturnType h + res <- Crucible.regValue <$> Crucible.callOverride h + (Crucible.mkOverride' "overrideBranches" retTy + (Crucible.symbolicBranches Crucible.emptyRegMap $ + [ ( precond + , do g <- Crucible.readGlobals + res <- liftIO $ runOverrideMatcher sym g + (st^.setupValueSub) + (st^.termSub) + (st^.osFree) + (st^.osLocation) + (methodSpecHandler_poststate opts sc cc retTy cs) + case res of + Left (OF loc rsn) -> + -- TODO, better pretty printing for reasons + liftIO + $ Crucible.abortExecBecause + $ Crucible.AssertionFailure + $ Crucible.SimError loc + $ Crucible.AssertFailureSimError "assumed false" (show rsn) + Right (ret,st') -> + do liftIO $ forM_ (st'^.osAssumes) $ \(_md,asum) -> + Crucible.addAssumption bak + $ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum + Crucible.writeGlobals (st'^.overrideGlobals) + Crucible.overrideReturn' (Crucible.RegEntry retTy ret) + , Just (W4.plSourceLoc (cs ^. MS.csLoc)) + ) + | (precond, cs, st) <- branches' + ] ++ + [ let e prettyArgs symFalse unsat = show $ PP.vcat $ concat + [ [ PP.pretty $ + "No override specification applies for " ++ fnName ++ "." + ] + , [ "Arguments:" + , bullets '-' prettyArgs + ] + , if | not (null false) -> + [ PP.vcat + [ PP.pretty (unwords + [ "The following overrides had some preconditions" + , "that failed concretely:" + ]) + , bullets '-' (map ppConcreteFailure false) + ] + ] + -- See comment on ppSymbolicFailure: this needs more + -- examination to see if it's useful. + -- - | not (null symFalse) -> + -- [ PP.text (unwords + -- [ "The following overrides had some preconditions " + -- , "that failed symbolically:" + -- ]) PP.<$$> bullets '-' (map ppSymbolicFailure symFalse) + -- ] + + -- Note that we only print these in case no override had + -- individually (concretely or symbolically) false + -- preconditions. + | not (null unsat) && null false && null symFalse -> + [ PP.vcat + [ PP.pretty (unwords + [ "The conjunction of these overrides' preconditions" + , "was unsatisfiable, meaning your override can never" + , "apply. You probably have unintentionally specified" + , "mutually exclusive/inconsistent preconditions." + ]) + , bullets '-' (unsat ^.. each . owpMethodSpec . to MS.ppMethodSpec) + ] + ] + | null false && null symFalse -> + [ PP.pretty (unwords + [ "No overrides had any single concretely or" + , "symbolically failing preconditions." + ]) + ] + | otherwise -> [] + , if | simVerbose opts < 3 -> + [ PP.pretty $ unwords + [ "Run SAW with --sim-verbose=3 to see a description" + , "of each override." + ] + ] + | otherwise -> + [ PP.vcat + [ "Here are the descriptions of each override:" + , bullets '-' + (branches ^.. each . owpMethodSpec . to MS.ppMethodSpec) + ] + ] + ] + in ( W4.truePred sym + , liftIO $ do + -- Now that we're failing, do the additional work of figuring out + -- if any overrides had symbolically false preconditions + symFalse <- catMaybes <$> (forM unknown $ \owp -> + findFalsePreconditions bak owp <&> + \case + [] -> Nothing + ps -> Just (owp, ps)) + + prettyArgs <- + ppArgs sym cc (NE.head css) (Crucible.RegMap args) + + unsat <- + filterM + (unsatPreconditions bak (owpPreconditions . each . _2 . W4.labeledPred)) + branches + + Crucible.addFailedAssertion bak + (Crucible.GenericSimError (e prettyArgs symFalse unsat)) + , Just (W4.plSourceLoc call_loc) + ) + ])) + (Crucible.RegMap args) + liftIO $ printOutLn opts Info $ unwords ["Applied override!", fnName] + return res + instantiateExtResolveSAWPred :: SharedContext -> MIRCrucibleContext -> @@ -198,7 +543,7 @@ learnCond opts sc cc cs prepost ss = enforceDisjointness cc loc ss enforceCompleteSubstitution loc ss --- | Process a "crucible_equal" statement from the precondition +-- | Process a "mir_equal" statement from the precondition -- section of the CrucibleSetup block. learnEqual :: Options -> @@ -253,7 +598,7 @@ learnPointsTo opts sc cc spec prepost (MirPointsTo md reference referents) = matchArg opts sc cc spec prepost md (MIRVal innerShp v) referenceInnerMirTy referentVal --- | Process a "crucible_precond" statement from the precondition +-- | Process a "mir_precond" statement from the precondition -- section of the CrucibleSetup block. learnPred :: SharedContext -> @@ -494,6 +839,160 @@ matchTerm sc cc md prepost real expect = ] 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 +-- specifications that could apply. We want a proof to succeed if _any_ +-- choice of method spec allows the proof to go through, which is a slightly +-- awkward thing to fit into the symbolic simulation framework. +-- +-- The main work of determining the preconditions, postconditions, memory +-- updates and return value for a single specification is done by +-- the @methodSpecHandler_prestate@ and @methodSpecHandler_poststate@ functions. +-- +-- In a first phase, we attempt to apply the precondition portion of each of +-- the given method specifications. Each of them that might apply generate +-- a substitution for the setup variables and a collection of preconditions +-- that guard the specification. We use these preconditions to compute +-- a multiway symbolic branch, one for each override which might apply. +-- +-- In the body of each of the individual branches, we compute the postcondition +-- actions of the corresponding method specification. This will update memory +-- and compute function return values, in addition to assuming postcondition +-- predicates. +methodSpecHandler :: + forall rtp args ret. + (?singleOverrideSpecialCase :: Bool) => + Options {- ^ output/verbosity options -} -> + SharedContext {- ^ context for constructing SAW terms -} -> + MIRCrucibleContext {- ^ context for interacting with Crucible -} -> + IORef MetadataMap -> + NE.NonEmpty (MS.CrucibleMethodSpecIR MIR) + {- ^ specification for current function override -} -> + Crucible.FnHandle args ret {- ^ the handle for this function -} -> + Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym MIR rtp args ret + (Crucible.RegValue Sym ret) +methodSpecHandler opts sc cc mdMap css h = + mccWithBackend cc $ \bak -> do + let sym = backendGetSym bak + let fnName = NE.head css ^. MS.csMethod + call_loc <- liftIO $ W4.getCurrentProgramLoc sym + liftIO $ printOutLn opts Info $ unwords + [ "Matching" + , show (length css) + , "overrides of " + , show fnName + , "..." + ] + Crucible.RegMap args <- Crucible.getOverrideArgs + + -- First, run the precondition matcher phase. Collect together a list of the results. + -- For each override, this will either be an error message, or a matcher state and + -- a method spec. + prestates <- + do g0 <- Crucible.readGlobals + forM css $ \cs -> liftIO $ + let initialFree = Set.fromList (map (ecVarIndex . tecExt) + (view (MS.csPreState . MS.csFreshVars) cs)) + in runOverrideMatcher sym g0 Map.empty Map.empty initialFree (view MS.csLoc cs) + (do methodSpecHandler_prestate opts sc cc args cs + return cs) + + -- Print a failure message if all overrides failed to match. Otherwise, collect + -- all the override states that might apply, and compute the conjunction of all + -- the preconditions. We'll use these to perform symbolic branches between the + -- various overrides. + branches <- + let prettyError methodSpec failureReason = do + prettyArgs <- liftIO $ ppArgs sym cc methodSpec (Crucible.RegMap args) + pure $ + PP.vcat + [ MS.ppMethodSpec methodSpec + , "Arguments:" + , bullets '-' prettyArgs + , ppOverrideFailure failureReason + ] + in + case partitionEithers (F.toList prestates) of + (errs, []) -> do + msgs <- + mapM (\(cs, err) -> + ("*" PP.<>) . PP.indent 2 <$> prettyError cs err) + (zip (F.toList css) errs) + fail $ show $ + PP.vcat ["All overrides failed during structural matching:", PP.vcat msgs] + (_, ss) -> liftIO $ + forM ss $ \(cs,st) -> + return (OverrideWithPreconditions (st^.osAsserts) cs st) + + -- Now we do a second phase of simple compatibility checking: we check to see + -- if any of the preconditions of the various overrides are concretely false. + -- If so, there's no use in branching on them with @symbolicBranches@. + (true, false, unknown) <- liftIO $ partitionOWPsConcrete sym branches + + -- Check if there is only a single override branch that might apply at this + -- point. If so, commit to it and handle that case specially. If there is + -- more than one (or zero) branches that might apply, go to the general case. + case true ++ unknown of + [singleBranch] | ?singleOverrideSpecialCase -> + handleSingleOverrideBranch opts sc cc call_loc mdMap h singleBranch + _ -> handleOverrideBranches opts sc cc call_loc css h branches (true, false, unknown) + +-- | Use a method spec to override the behavior of a function. +-- This function computes the post-state portion of the override, +-- which involves writing values into memory, computing the return value, +-- and computing postcondition predicates. +methodSpecHandler_poststate :: + forall ret w. + 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) +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) + +-- | Use a method spec to override the behavior of a function. +-- This function computes the pre-state portion of the override, +-- which involves reading values from arguments and memory and computing +-- substitutions for the setup value variables, and computing precondition +-- predicates. +methodSpecHandler_prestate :: + forall ctx w. + Options {- ^ output/verbosity options -} -> + SharedContext {- ^ context for constructing SAW terms -} -> + MIRCrucibleContext {- ^ context for interacting with Crucible -} -> + Ctx.Assignment (Crucible.RegEntry Sym) ctx + {- ^ the arguments to the function -} -> + CrucibleMethodSpecIR {- ^ specification for current function override -} -> + OverrideMatcher MIR w () +methodSpecHandler_prestate opts sc cc args cs = + do let expectedArgTypes = Map.elems (cs ^. MS.csArgBindings) + let col = cc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection + let aux :: + (Mir.Ty, SetupValue) -> Crucible.AnyValue Sym -> + IO (MIRVal, Mir.Ty, SetupValue) + aux (argTy, setupVal) val = + case decodeMIRVal col argTy val of + Just val' -> return (val', argTy, setupVal) + Nothing -> fail "unexpected type" + + -- todo: fail if list lengths mismatch + xs <- liftIO (zipWithM aux expectedArgTypes (assignmentToList args)) + + let md = MS.ConditionMetadata + { MS.conditionLoc = cs ^. MS.csLoc + , MS.conditionTags = mempty + , MS.conditionType = "formal argument matching" + , MS.conditionContext = "" + } + + sequence_ [ matchArg opts sc cc cs MS.PreState md x y z | (x, y, z) <- xs] + + learnCond opts sc cc cs MS.PreState (cs ^. MS.csPreState) + -- | Try to translate the spec\'s 'SetupValue' into a 'MIRVal', pretty-print -- the 'MIRVal'. mkStructuralMismatch :: @@ -540,6 +1039,22 @@ notEqual cond opts loc cc sc spec expected actual = do ] pure $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" +-- | Pretty-print the arguments passed to an override +ppArgs :: + forall args ann. + Sym -> + MIRCrucibleContext {- ^ context for interacting with Crucible -} -> + MS.CrucibleMethodSpecIR MIR {- ^ specification for current function override -} -> + Crucible.RegMap Sym args {- ^ arguments from the simulator -} -> + IO [PP.Doc ann] +ppArgs sym cc cs (Crucible.RegMap args) = do + let expectedArgTypes = map fst (Map.elems (cs ^. MS.csArgBindings)) + let col = cc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection + let aux memTy (Crucible.AnyValue tyrep val) = + MIRVal (tyToShapeEq col memTy tyrep) val + let vals = zipWith aux expectedArgTypes (assignmentToList args) + pure $ map (ppMIRVal sym) vals + -- | Resolve a 'SetupValue' into a 'MIRVal' and pretty-print it ppSetupValueAsMIRVal :: Options {- ^ output/verbosity options -} -> diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index fde07c4ce1..05c42facf4 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs @@ -23,6 +23,8 @@ module SAWScript.Crucible.MIR.ResolveSetupValue , equalValsPred , checkCompatibleTys , readMaybeType + , doAlloc + , doPointsTo , firstPointsToReferent , mirAdtToTy , findDefId @@ -64,7 +66,8 @@ import qualified Cryptol.Eval.Type as Cryptol (TValue(..), tValTy, evalValType) import qualified Cryptol.TypeCheck.AST as Cryptol (Type, Schema(..)) import qualified Cryptol.Utils.PP as Cryptol (pp) import Lang.Crucible.Backend (IsSymInterface) -import Lang.Crucible.Simulator (AnyValue(..), GlobalVar(..), RegValue, RegValue'(..)) +import Lang.Crucible.Simulator + ( AnyValue(..), GlobalVar(..), RegValue, RegValue'(..), SymGlobalState ) import Lang.Crucible.Types (MaybeType, TypeRepr(..)) import qualified Mir.DefId as Mir import qualified Mir.FancyMuxTree as Mir @@ -866,6 +869,81 @@ readPartExprMaybe _sym (W4.PE p v) | Just True <- W4.asConstantPred p = Just v | otherwise = Nothing +-- | Allocate memory for each 'mir_alloc' or 'mir_alloc_mut'. +doAlloc :: + MIRCrucibleContext + -> SymGlobalState Sym + -> Some MirAllocSpec + -> IO (Some (MirPointer Sym), SymGlobalState Sym) +doAlloc cc globals (Some ma) = + mccWithBackend cc $ \bak -> + do let col = cc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection + let halloc = cc^.mccHandleAllocator + let sym = backendGetSym bak + let iTypes = Mir.mirIntrinsicTypes + Some tpr <- pure $ Mir.tyToRepr col (ma^.maMirType) + + -- Create an uninitialized `MirVector_PartialVector` of length 1 and + -- return a pointer to its element. + ref <- Mir.newMirRefIO sym halloc (Mir.MirVectorRepr tpr) + + one <- W4.bvLit sym W4.knownRepr $ BV.mkBV W4.knownRepr 1 + vec <- Mir.mirVector_uninitIO bak one + globals' <- Mir.writeMirRefIO bak globals iTypes ref vec + + zero <- W4.bvLit sym W4.knownRepr $ BV.mkBV W4.knownRepr 0 + ptr <- Mir.subindexMirRefIO bak iTypes tpr ref zero + let mirPtr = Some MirPointer + { _mpType = tpr + , _mpMutbl = ma^.maMutbl + , _mpMirType = ma^.maMirType + , _mpRef = ptr + } + + pure (mirPtr, globals') + +doPointsTo :: + MS.CrucibleMethodSpecIR MIR + -> MIRCrucibleContext + -> Map MS.AllocIndex (Some (MirPointer Sym)) + -> SymGlobalState Sym + -> MirPointsTo + -> IO (SymGlobalState Sym) +doPointsTo mspec cc env globals (MirPointsTo _ reference referents) = + mccWithBackend cc $ \bak -> do + MIRVal referenceShp referenceVal <- + resolveSetupVal cc env tyenv nameEnv reference + -- By the time we reach here, we have already checked (in mir_points_to) + -- that we are in fact dealing with a reference value, so the call to + -- `testRefShape` below should always succeed. + IsRefShape _ _ _ referenceInnerTy <- + case testRefShape referenceShp of + Just irs -> pure irs + Nothing -> + panic "doPointsTo" + [ "Unexpected non-reference type:" + , show $ PP.pretty $ shapeMirTy referenceShp + ] + referent <- firstPointsToReferent referents + MIRVal referentShp referentVal <- + resolveSetupVal cc env tyenv nameEnv referent + -- By the time we reach here, we have already checked (in mir_points_to) + -- that the type of the reference is compatible with the right-hand side + -- value, so the equality check below should never fail. + Refl <- + case W4.testEquality referenceInnerTy (shapeType referentShp) of + Just r -> pure r + Nothing -> + panic "doPointsTo" + [ "Unexpected type mismatch between reference and referent" + , "Reference type: " ++ show referenceInnerTy + , "Referent type: " ++ show (shapeType referentShp) + ] + Mir.writeMirRefIO bak globals Mir.mirIntrinsicTypes referenceVal referentVal + where + tyenv = MS.csAllocations mspec + nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames + -- | @mir_points_to@ always creates a 'MirPointsTo' value with exactly one -- referent on the right-hand side. As a result, this function should never -- fail. diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 980aec8d95..bc28517c76 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -4005,6 +4005,14 @@ primitives = Map.fromList , "values as elements." ] + , prim "mir_unsafe_assume_spec" + "MIRModule -> String -> MIRSetup () -> TopLevel MIRSpec" + (pureVal mir_unsafe_assume_spec) + Experimental + [ "Return a MIRSpec corresponding to a MIRSetup block, as would be" + , "returned by mir_verify but without performing any verification." + ] + , prim "mir_verify" "MIRModule -> String -> [MIRSpec] -> Bool -> MIRSetup () -> ProofScript () -> TopLevel MIRSpec" (pureVal mir_verify)