diff --git a/intTests/test2665/Makefile b/intTests/test2665/Makefile new file mode 100644 index 0000000000..857fbf5dcf --- /dev/null +++ b/intTests/test2665/Makefile @@ -0,0 +1,2 @@ +MIR_SRCS=test +include ../support/mir-blobs.mk diff --git a/intTests/test2665/test.linked-mir.json b/intTests/test2665/test.linked-mir.json new file mode 100644 index 0000000000..897c15ab62 --- /dev/null +++ b/intTests/test2665/test.linked-mir.json @@ -0,0 +1 @@ +{"version":4,"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:13:28: 13:29","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"0"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:13:1: 13:30"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"test/68742182::GLOB_MUT","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:25:20: 25:21","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"0"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:25:1: 25:22"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"test/68742182::GLOB","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"test.rs:4:5: 4:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:5:2: 5:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::RawPtr::1f2b1eadb40cd255"}]},"name":"test/68742182::foo_in_out","return_ty":"ty::RawPtr::1f2b1eadb40cd255","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Copy"}],"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"bb1"],"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::9905745026a87924"},"kind":"Constant"},"kind":"Call","pos":"test.rs:8:10: 8:23"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"}},"pos":"test.rs:8:5: 8:23","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Eq"}}}],"terminator":{"kind":"Return","pos":"test.rs:9:2: 9:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}]},"name":"test/68742182::bar_in_out","return_ty":"ty::bool","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:16:10: 16:27","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/68742182::GLOB_MUT","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"}},"pos":"test.rs:16:5: 16:27","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Eq"}}}],"terminator":{"kind":"Return","pos":"test.rs:17:2: 17:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}]},"name":"test/68742182::foo_in_static_mut","return_ty":"ty::bool","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:28:21: 28:25","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/68742182::GLOB","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"test.rs:28:10: 28:25","rhs":{"kind":"AddressOf","mutbl":{"kind":"Not"},"place":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"}},"pos":"test.rs:28:5: 28:25","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Eq"}}}],"terminator":{"kind":"Return","pos":"test.rs:29:2: 29:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/68742182::foo_in_static","return_ty":"ty::bool","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:32:30: 32:34","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/68742182::GLOB","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"test.rs:32:19: 32:34","rhs":{"kind":"AddressOf","mutbl":{"kind":"Not"},"place":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"}],"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"}},"bb1"],"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::820ad1a721c7d406"},"kind":"Constant"},"kind":"Call","pos":"test.rs:32:5: 32:35"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:33:2: 33:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/68742182::bar_in_static","return_ty":"ty::bool","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:48:16: 48:20","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/68742182::GLOB","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"test.rs:48:5: 48:20","rhs":{"kind":"AddressOf","mutbl":{"kind":"Not"},"place":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}}}}],"terminator":{"kind":"Return","pos":"test.rs:49:2: 49:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/68742182::foo_out_static","return_ty":"ty::RawPtr::1f2b1eadb40cd255","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:38:5: 38:22","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/68742182::GLOB_MUT","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:39:2: 39:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::RawPtr::63e5937014067f41"}]},"name":"test/68742182::foo_out_static_mut","return_ty":"ty::RawPtr::63e5937014067f41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:52:16: 52:20","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/68742182::GLOB","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"pos":"test.rs:52:5: 52:20","rhs":{"kind":"AddressOf","mutbl":{"kind":"Not"},"place":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}}}}],"terminator":{"args":[],"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"bb1"],"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::b231d267d09d3b73"},"kind":"Constant"},"kind":"Call","pos":"test.rs:52:24: 52:40"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"}},"pos":"test.rs:52:5: 52:40","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Eq"}}}],"terminator":{"kind":"Return","pos":"test.rs:53:2: 53:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::1f2b1eadb40cd255"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::1f2b1eadb40cd255"}]},"name":"test/68742182::bar_out_static","return_ty":"ty::bool","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:42:5: 42:22","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/68742182::GLOB_MUT","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}}],"terminator":{"args":[],"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}},"bb1"],"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::a2624092adf7f195"},"kind":"Constant"},"kind":"Call","pos":"test.rs:42:26: 42:46"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"}},"pos":"test.rs:42:5: 42:46","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Eq"}}}],"terminator":{"kind":"Return","pos":"test.rs:43:2: 43:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}]},"name":"test/68742182::bar_out_static_mut","return_ty":"ty::bool","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:20:23: 20:40","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/68742182::GLOB_MUT","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Move"}],"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"}},"bb1"],"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::b28bbe84a45c656e"},"kind":"Constant"},"kind":"Call","pos":"test.rs:20:5: 20:41"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:21:2: 21:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}]},"name":"test/68742182::bar_in_static_mut","return_ty":"ty::bool","spread_arg":null}],"adts":[],"statics":[{"kind":"body","mutable":true,"name":"test/68742182::GLOB_MUT","ty":"ty::u32"},{"kind":"body","mutable":false,"name":"test/68742182::GLOB","ty":"ty::u32"}],"vtables":[],"traits":[],"intrinsics":[{"inst":{"args":[],"def_id":"test/68742182::foo_in_out","kind":"Item"},"name":"test/68742182::foo_in_out"},{"inst":{"args":[],"def_id":"test/68742182::bar_in_out","kind":"Item"},"name":"test/68742182::bar_in_out"},{"inst":{"args":[],"def_id":"test/68742182::foo_in_static_mut","kind":"Item"},"name":"test/68742182::foo_in_static_mut"},{"inst":{"args":[],"def_id":"test/68742182::foo_in_static","kind":"Item"},"name":"test/68742182::foo_in_static"},{"inst":{"args":[],"def_id":"test/68742182::bar_in_static","kind":"Item"},"name":"test/68742182::bar_in_static"},{"inst":{"args":[],"def_id":"test/68742182::foo_out_static","kind":"Item"},"name":"test/68742182::foo_out_static"},{"inst":{"args":[],"def_id":"test/68742182::foo_out_static_mut","kind":"Item"},"name":"test/68742182::foo_out_static_mut"},{"inst":{"args":[],"def_id":"test/68742182::bar_out_static","kind":"Item"},"name":"test/68742182::bar_out_static"},{"inst":{"args":[],"def_id":"test/68742182::bar_out_static_mut","kind":"Item"},"name":"test/68742182::bar_out_static_mut"},{"inst":{"args":[],"def_id":"test/68742182::bar_in_static_mut","kind":"Item"},"name":"test/68742182::bar_in_static_mut"}],"tys":[{"layout":{"align":4,"size":4},"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"layout":{"align":8,"size":8},"name":"ty::RawPtr::1f2b1eadb40cd255","ty":{"kind":"RawPtr","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"layout":{"align":1,"size":1},"name":"ty::bool","ty":{"kind":"Bool"}},{"layout":{"align":1,"size":0},"name":"ty::FnDef::9905745026a87924","ty":{"defid":"test/68742182::foo_in_out","kind":"FnDef"}},{"layout":{"align":8,"size":8},"name":"ty::RawPtr::63e5937014067f41","ty":{"kind":"RawPtr","mutability":{"kind":"Mut"},"ty":"ty::u32"}},{"layout":{"align":8,"size":8},"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"layout":{"align":1,"size":0},"name":"ty::FnDef::820ad1a721c7d406","ty":{"defid":"test/68742182::foo_in_static","kind":"FnDef"}},{"layout":{"align":1,"size":0},"name":"ty::FnDef::b231d267d09d3b73","ty":{"defid":"test/68742182::foo_out_static","kind":"FnDef"}},{"layout":{"align":1,"size":0},"name":"ty::FnDef::a2624092adf7f195","ty":{"defid":"test/68742182::foo_out_static_mut","kind":"FnDef"}},{"layout":{"align":1,"size":0},"name":"ty::FnDef::b28bbe84a45c656e","ty":{"defid":"test/68742182::foo_in_static_mut","kind":"FnDef"}}],"lang_items":[],"roots":["test/68742182::foo_in_out","test/68742182::bar_in_out","test/68742182::foo_in_static_mut","test/68742182::bar_in_static_mut","test/68742182::foo_in_static","test/68742182::bar_in_static","test/68742182::foo_out_static_mut","test/68742182::bar_out_static_mut","test/68742182::foo_out_static","test/68742182::bar_out_static"],"tests":[]} \ No newline at end of file diff --git a/intTests/test2665/test.linked-mir.json.FROM b/intTests/test2665/test.linked-mir.json.FROM new file mode 100644 index 0000000000..ca1a0c4c25 --- /dev/null +++ b/intTests/test2665/test.linked-mir.json.FROM @@ -0,0 +1,7 @@ +versions + rustc 1.86.0-nightly (9cd60bd2c 2025-02-15) + mir-json mtime: Oct 6 02:23:13 2025 + mir-json version from cargo: mir-json v0.1.0 + probable mir-json commit: ce3ab88fd9df99b7c9bff6fd521926c46c62bf25 from Wed Oct 1 15:06:10 2025 and/or Wed Oct 1 15:06:10 2025 +versions-notes + Generated by update-from.sh version 1 diff --git a/intTests/test2665/test.rs b/intTests/test2665/test.rs new file mode 100644 index 0000000000..9addf5f71a --- /dev/null +++ b/intTests/test2665/test.rs @@ -0,0 +1,53 @@ +// Aliasing input and output + +pub fn foo_in_out(x: *const u32) -> *const u32 { + x +} + +pub fn bar_in_out(x: *const u32) -> bool { + x == foo_in_out(x) +} + +// Aliasing input and mutable static + +static mut GLOB_MUT: u32 = 0; + +pub fn foo_in_static_mut(x: *mut u32) -> bool { + x == &raw mut GLOB_MUT +} + +pub fn bar_in_static_mut() -> bool { + foo_in_static_mut(&raw mut GLOB_MUT) +} + +// Aliasing input and immutable static + +static GLOB: u32 = 0; + +pub fn foo_in_static(x: *const u32) -> bool { + x == &raw const GLOB +} + +pub fn bar_in_static() -> bool { + foo_in_static(&raw const GLOB) +} + +// Aliasing output and mutable static + +pub fn foo_out_static_mut() -> *mut u32 { + &raw mut GLOB_MUT +} + +pub fn bar_out_static_mut() -> bool { + &raw mut GLOB_MUT == foo_out_static_mut() +} + +// Aliasing output and immutable static + +pub fn foo_out_static() -> *const u32 { + &raw const GLOB +} + +pub fn bar_out_static() -> bool { + &raw const GLOB == foo_out_static() +} diff --git a/intTests/test2665/test.saw b/intTests/test2665/test.saw new file mode 100644 index 0000000000..51a166b047 --- /dev/null +++ b/intTests/test2665/test.saw @@ -0,0 +1,212 @@ +enable_experimental; + +m <- mir_load_module "test.linked-mir.json"; + +// Aliasing input and output + +let foo_in_out_spec = do { + x <- mir_alloc_raw_ptr_const mir_u32; + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func [x]; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + y <- mir_alloc_raw_ptr_const mir_u32; + mir_return y; +}; + +fails (mir_verify m "test::foo_in_out" [] false foo_in_out_spec z3); + +/* +let bar_in_out_spec0 = do { + x <- mir_alloc_raw_ptr_const mir_u32; + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func [x]; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_return (mir_term {{ False }}); +}; + +mir_verify m "test::bar_in_out" [foo_in_out_ov] false bar_in_out_spec0 z3; + +let bar_in_out_spec1 = do { + x <- mir_alloc_raw_ptr_const mir_u32; + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func [x]; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_return (mir_term {{ True }}); +}; + +mir_verify m "test::bar_in_out" [] false bar_in_out_spec1 z3; +*/ + +// Aliasing input and mutable static + +let foo_in_static_mut_spec = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + x <- mir_alloc_raw_ptr_mut mir_u32; + x_contents <- mir_fresh_var "x" mir_u32; + mir_points_to x (mir_term x_contents); + + mir_execute_func [x]; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_points_to x (mir_term x_contents); + mir_return (mir_term {{ False }}); +}; + +foo_in_static_mut_ov <- mir_verify m "test::foo_in_static_mut" [] false foo_in_static_mut_spec z3; + +let bar_in_static_mut_spec0 = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func []; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_return (mir_term {{ False }}); +}; + +fails (mir_verify m "test::bar_in_static_mut" [foo_in_static_mut_ov] false bar_in_static_mut_spec0 z3); + +let bar_in_static_mut_spec1 = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func []; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_return (mir_term {{ True }}); +}; + +mir_verify m "test::bar_in_static_mut" [] false bar_in_static_mut_spec1 z3; + +// Aliasing input and immutable static + +let foo_in_static_spec = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + x <- mir_alloc_raw_ptr_const mir_u32; + x_contents <- mir_fresh_var "x" mir_u32; + mir_points_to x (mir_term x_contents); + + mir_execute_func [x]; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_return (mir_term {{ False }}); +}; + +foo_in_static_ov <- mir_verify m "test::foo_in_static" [] false foo_in_static_spec z3; + +let bar_in_static_spec0 = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func []; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_return (mir_term {{ False }}); +}; + +fails (mir_verify m "test::bar_in_static" [foo_in_static_ov] false bar_in_static_spec0 z3); + +let bar_in_static_spec1 = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func []; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_return (mir_term {{ True }}); +}; + +mir_verify m "test::bar_in_static" [] false bar_in_static_spec1 z3; + +// Aliasing output and mutable static + +let foo_out_static_mut_spec = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func []; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + y <- mir_alloc_raw_ptr_mut mir_u32; + mir_return y; +}; + +fails (mir_verify m "test::foo_out_static_mut" [] false foo_out_static_mut_spec z3); + +/* +let bar_out_static_mut_spec0 = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func []; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_return (mir_term {{ False }}); +}; + +mir_verify m "test::bar_out_static_mut" [foo_out_static_mut_ov] false bar_out_static_mut_spec0 z3; + +let bar_out_static_mut_spec1 = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func []; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_return (mir_term {{ True }}); +}; + +mir_verify m "test::bar_out_static_mut" [] false bar_out_static_mut_spec1 z3; +*/ + +// Aliasing output and immutable static + +let foo_out_static_spec = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func []; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + y <- mir_alloc_raw_ptr_const mir_u32; + mir_return y; +}; + +fails (mir_verify m "test::foo_out_static" [] false foo_out_static_spec z3); + +/* +let bar_out_static_spec0 = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func []; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_return (mir_term {{ False }}); +}; + +mir_verify m "test::bar_out_static" [foo_out_static_ov] false bar_out_static_spec0 z3; + +let bar_out_static_spec1 = do { + glob_mut_contents <- mir_fresh_var "GLOB_MUT" mir_u32; + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + + mir_execute_func []; + + mir_points_to (mir_static "test::GLOB_MUT") (mir_term glob_mut_contents); + mir_return (mir_term {{ True }}); +}; + +mir_verify m "test::bar_out_static" [] false bar_out_static_spec1 z3; +*/ diff --git a/intTests/test2665/test.sh b/intTests/test2665/test.sh new file mode 100644 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test2665/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs index 9b9170059c..e87e525411 100644 --- a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs +++ b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs @@ -1425,7 +1425,9 @@ verifyPoststate cc mspec env0 globals ret mdMap = matchPost <- io $ runOverrideMatcher sym globals env0 terms0 initialFree poststateLoc $ do matchResult opts sc - learnCond opts sc cc mspec MS.PostState (mspec ^. MS.csPostState) + learnCond opts sc cc mspec MS.PostState + (mspec ^. MS.csPreState . MS.csAllocs) + (mspec ^. MS.csPostState) st <- case matchPost of Left err -> fail (show err) diff --git a/saw-central/src/SAWCentral/Crucible/MIR/Override.hs b/saw-central/src/SAWCentral/Crucible/MIR/Override.hs index b70a4a6207..4843b90118 100644 --- a/saw-central/src/SAWCentral/Crucible/MIR/Override.hs +++ b/saw-central/src/SAWCentral/Crucible/MIR/Override.hs @@ -44,6 +44,7 @@ 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.Classes as PC import qualified Data.Parameterized.Context as Ctx @@ -531,14 +532,27 @@ decodeMIRVal col ty (Crucible.AnyValue repr rv) Just Refl -> Just (MIRVal shp rv) Nothing -> Nothing --- | Generate assertions that all of the memory allocations matched by --- an override's precondition are disjoint. +-- | Generate assertions that all of the memory allocations matched by an +-- override's precondition are disjoint from each other, and from all statics +-- and any extra allocations passed in. enforceDisjointness :: - MIRCrucibleContext -> W4.ProgramLoc -> StateSpec -> OverrideMatcher MIR w () -enforceDisjointness cc loc ss = + MIRCrucibleContext -> + W4.ProgramLoc -> + -- | Additional allocations to check disjointness from (from prestate) + Map AllocIndex (Some MirAllocSpec) -> + StateSpec -> + OverrideMatcher MIR w () +enforceDisjointness cc loc extras ss = do let sym = cc^.mccSym sub <- OM (use setupValueSub) - let mems = Map.elems $ Map.intersectionWith (,) (view MS.csAllocs ss) sub + let mems = Map.elems $ Map.intersection sub (view MS.csAllocs ss) + let mems2 = Map.elems $ Map.intersection sub extras + + let colState = cc ^. mccRustModule . Mir.rmCS + let statics = Map.elems $ + Map.intersectionWith (staticMirPointer sym) + (colState ^. Mir.collection ^. Mir.statics) + (colState ^. Mir.staticMap) let md = MS.ConditionMetadata { MS.conditionLoc = loc @@ -546,15 +560,16 @@ enforceDisjointness cc loc ss = , MS.conditionType = "memory region disjointness" , MS.conditionContext = "" } - -- Ensure that all regions are disjoint from each other. + -- Ensure that all regions are disjoint from each other and extras and + -- statics sequence_ [ do c <- liftIO $ W4.notPred sym =<< equalRefsPred cc p q addAssert c md a | let a = Crucible.SimError loc $ Crucible.AssertFailureSimError "Memory regions not disjoint" "" - , (_, Some p) : ps <- tails mems - , (_, Some q) <- ps + , Some p : ps <- tails mems + , Some q <- ps ++ mems2 ++ statics ] -- | Perform an allocation as indicated by a 'mir_alloc' @@ -948,14 +963,15 @@ learnCond :: MIRCrucibleContext -> CrucibleMethodSpecIR -> MS.PrePost -> + Map AllocIndex (Some MirAllocSpec) -> StateSpec -> OverrideMatcher MIR w () -learnCond opts sc cc cs prepost ss = +learnCond opts sc cc cs prepost extras ss = do let loc = cs ^. MS.csLoc matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos) F.traverse_ (learnSetupCondition opts sc cc cs prepost) (ss ^. MS.csConditions) assertTermEqualities sc cc - enforceDisjointness cc loc ss + enforceDisjointness cc loc extras ss enforceCompleteSubstitution loc ss -- | Process a "mir_equal" statement from the precondition @@ -1768,7 +1784,7 @@ methodSpecHandler_prestate opts sc cc args cs = sequence_ [ matchArg opts sc cc cs MS.PreState md x z | (x, z) <- xs] - learnCond opts sc cc cs MS.PreState (cs ^. MS.csPreState) + learnCond opts sc cc cs MS.PreState Map.empty (cs ^. MS.csPreState) -- | Try to translate the spec\'s 'SetupValue' into a 'MIRVal', pretty-print -- the 'MIRVal'. diff --git a/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs index 939228ee2e..983180387e 100644 --- a/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs +++ b/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs @@ -40,6 +40,7 @@ module SAWCentral.Crucible.MIR.ResolveSetupValue , findStatic , findStaticInitializer , findStaticVar + , staticMirPointer , staticRefMux -- * Enum discriminants , getEnumVariantDiscr @@ -501,15 +502,7 @@ resolveSetupVal mcc env tyenv nameEnv val = mccWithBackend mcc $ \bak -> let sym = backendGetSym bak in case val of - MS.SetupVar i -> do - Some ptr <- pure $ lookupAllocIndex env i - let pointeeType = ptr ^. mpMirType - pure $ MIRVal (RefShape - (ptrKindToTy (ptr ^. mpKind) pointeeType (ptr ^. mpMutbl)) - pointeeType - (ptr ^. mpMutbl) - (ptr ^. mpType)) - (ptr ^. mpRef) + MS.SetupVar i -> pure $ mirPointerToMIRVal $ lookupAllocIndex env i MS.SetupTerm tm -> resolveTypedTerm mcc tm MS.SetupNull empty -> absurd empty MS.SetupStruct adt flds -> @@ -799,11 +792,8 @@ resolveSetupVal mcc env tyenv nameEnv val = MS.SetupUnion empty _ _ -> absurd empty MS.SetupGlobal () name -> do static <- findStatic cs name - Mir.StaticVar gv <- findStaticVar cs (static ^. Mir.sName) - let sMut = staticMutability static - sTy = static ^. Mir.sTy - pure $ MIRVal (RefShape (staticTyRef static) sTy sMut (globalType gv)) - $ staticRefMux sym gv + staticVar <- findStaticVar cs (static ^. Mir.sName) + pure $ mirPointerToMIRVal $ staticMirPointer sym static staticVar MS.SetupGlobalInitializer () name -> do static <- findStatic cs name findStaticInitializer mcc static @@ -836,6 +826,16 @@ resolveSetupVal mcc env tyenv nameEnv val = col = cs ^. Mir.collection iTypes = mcc ^. mccIntrinsicTypes + mirPointerToMIRVal :: Some (MirPointer Sym) -> MIRVal + mirPointerToMIRVal (Some ptr) = + MIRVal (RefShape (ptrKindToTy (ptr ^. mpKind) + (ptr ^. mpMirType) + (ptr ^. mpMutbl)) + (ptr ^. mpMirType) + (ptr ^. mpMutbl) + (ptr ^. mpType)) + (ptr ^. mpRef) + -- Perform a light amount of typechecking on the fields in a struct or enum -- variant. This ensures that the variant receives the expected number of -- types and that the types of each field match. @@ -1824,6 +1824,23 @@ findStaticVar cs staticDefId = Nothing -> X.throwM $ MIRStaticNotFound staticDefId Just sv -> pure sv +-- | Create a 'MirPointer' from the 'Mir.Static' and 'Mir.StaticVar' +-- corresponding to a static. +staticMirPointer :: + W4.IsSymExprBuilder sym => + sym -> + Mir.Static -> + Mir.StaticVar -> + Some (MirPointer sym) +staticMirPointer sym static (Mir.StaticVar gv) = + Some MirPointer + { _mpType = globalType gv + , _mpKind = tyToPtrKind $ staticTyRef static + , _mpMutbl = staticMutability static + , _mpMirType = static ^. Mir.sTy + , _mpRef = staticRefMux sym gv + } + -- | Compute the 'Mir.Mutability' of a 'Mir.Static' value. staticMutability :: Mir.Static -> Mir.Mutability staticMutability static