Merge pull request #2146 from GaloisInc/1960-test-mir-unsound-global

Add a test_mir_unsound_global

intTests/test_mir_unsound_global/Makefile

@@ -0,0 +1,17 @@
+# The current checked-in linked-mir.json file was generated by:
+#    rustc 1.69.0-nightly (5e37043d6 2023-01-22)
+#    mir-json c52b16bf26af2f5b98157ebf9975aa0021982bbc from 2024-09-11
+
+all: unsound_global.linked-mir.json
+
+unsound_global.linked-mir.json: unsound_global.rs
+	saw-rustc $<
+	$(MAKE) remove-unused-build-artifacts
+
+.PHONY: remove-unused-build-artifacts
+remove-unused-build-artifacts:
+	rm -f unsound_global libunsound_global.mir libunsound_global.rlib
+
+.PHONY: clean
+clean: remove-unused-build-artifacts
+	rm -f unsound_global.linked-mir.json

intTests/test_mir_unsound_global/test.sh

@@ -0,0 +1,6 @@
+# this is supposed to fail
+if ! $SAW unsound_global.saw ; then
+    exit 0
+else
+    exit 1
+fi

intTests/test_mir_unsound_global/unsound_global.linked-mir.json

@@ -0,0 +1 @@
+{"version":1,"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"unsound_global.rs:6:24: 6:25","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"unsound_global.rs:6:1: 6:26"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"unsound_global/0420abd1::TEST","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":"unsound_global.rs:14:26: 14:27","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"0"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"unsound_global.rs:14:1: 14:28"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"unsound_global/0420abd1::GLOBAL","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":"_1","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"unsound_global.rs:23:13: 23:17","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"unsound_global/0420abd1::TEST","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"unsound_global.rs:23:13: 23:22","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"unsound_global.rs:25:13: 25:19","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"unsound_global/0420abd1::GLOBAL","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"unsound_global.rs:25:13: 25:23","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"0"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"args":[{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"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::2a16ab277373257f"},"kind":"Constant"},"kind":"Call","pos":"unsound_global.rs:26:19: 26:25"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"unsound_global.rs:34:4: 34:7","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"unsound_global.rs:34:19: 34:25","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"unsound_global/0420abd1::GLOBAL","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"unsound_global.rs:34:19: 34:25","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"unsound_global.rs:34:4: 34:27","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Copy"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _4 + move _5`, which would overflow","pos":"unsound_global.rs:34:4: 34:27","target":"bb2"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"unsound_global.rs:34:4: 34:27","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"unsound_global.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":"_1","ty":"ty::RawPtr::63e5937014067f41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::RawPtr::63e5937014067f41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Tuple::7063e33f0dbc8a58"}]},"name":"unsound_global/0420abd1::bar","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":"unsound_global.rs:18:22: 18: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":"_3","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"unsound_global.rs:18:13: 18:19","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"unsound_global/0420abd1::GLOBAL","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"unsound_global.rs:18:13: 18:23","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"unsound_global.rs:19:4: 19:5","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::Tuple::7063e33f0dbc8a58"}},"pos":"unsound_global.rs:19:4: 19:9","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _4 + const 1_u32`, which would overflow","pos":"unsound_global.rs:19:4: 19:9","target":"bb1"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"unsound_global.rs:19:4: 19:9","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"unsound_global.rs:20:2: 20: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"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::RawPtr::63e5937014067f41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Tuple::7063e33f0dbc8a58"}]},"name":"unsound_global/0420abd1::foo","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[{"kind":"body","mutable":true,"name":"unsound_global/0420abd1::TEST","ty":"ty::u32"},{"kind":"body","mutable":true,"name":"unsound_global/0420abd1::GLOBAL","ty":"ty::u32"}],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"unsound_global/0420abd1::bar","kind":"Item","substs":[]},"name":"unsound_global/0420abd1::bar"},{"inst":{"def_id":"unsound_global/0420abd1::foo","kind":"Item","substs":[]},"name":"unsound_global/0420abd1::foo"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::RawPtr::63e5937014067f41","ty":{"kind":"RawPtr","mutability":{"kind":"Mut"},"ty":"ty::u32"}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::7063e33f0dbc8a58","ty":{"kind":"Tuple","tys":["ty::u32","ty::bool"]}},{"name":"ty::FnDef::2a16ab277373257f","ty":{"defid":"unsound_global/0420abd1::foo","kind":"FnDef"}}],"roots":["unsound_global/0420abd1::foo","unsound_global/0420abd1::bar"]}

intTests/test_mir_unsound_global/unsound_global.rs

@@ -0,0 +1,33 @@
+// unsound_global.rs
+//
+// (this is essentially the same as unsound_global.c from
+// test_llvm_unsound_global)
+
+static mut TEST: u32 = 1;
+
+// the C version uses an array, but that currently causes extra
+// complications here (you can't successfully assign GLOBAL[1] without
+// initializing GLOBAL[0], and that requires also initializing
+// GLOBAL[1], and that changes the meaning of the test, so for now
+// just use a scalar.
+//static mut GLOBAL: [u32; 2] = [0, 0];
+static mut GLOBAL: u32 = 0;
+
+pub fn foo(x: u32) -> u32 {
+   //unsafe { GLOBAL[1] = x };
+   unsafe { GLOBAL = x };
+   x + 1
+}
+
+pub fn bar() -> u32 {
+   unsafe { TEST = 42 };
+   //unsafe { GLOBAL[1] = 0 };
+   unsafe { GLOBAL = 0 };
+   let val: u32 = foo(1);
+   // this does not go, not entirely sure why
+   //println!("{}", unsafe { TEST } );
+   // unsafe { GLOBAL[1] = 0 };
+   // unsafe { GLOBAL = 0 };
+   //val + unsafe { GLOBAL[1] }
+   val + unsafe { GLOBAL }
+}

intTests/test_mir_unsound_global/unsound_global.saw

@@ -0,0 +1,28 @@
+enable_experimental;
+
+MODULE <- mir_load_module "unsound_global.linked-mir.json";
+
+let foo_setup = do {
+  //mir_alloc_global "GLOBAL";
+  x <- mir_fresh_var "x" mir_u32;
+  mir_assert {{ x < 0x10000000 }};
+  mir_execute_func [mir_term x];
+  mir_return (mir_term {{ x + 1 : [32] }});
+  // mir_points_to (mir_elem (mir_static "GLOBAL") 1) (mir_term x);
+};
+foo_spec <- mir_verify MODULE "unsound_global::foo" [] false foo_setup z3;
+
+let bar_setup = do {
+  //mir_alloc_global "GLOBAL";
+  //mir_alloc_global "TEST";
+  mir_execute_func [];
+  mir_return (mir_term {{ 2 : [32] }});
+};
+
+// the below line (without override) correctly fails
+// mir_verify MODULE "unsound_global::bar" [] false bar_setup z3;
+
+// this also correctly fails these days
+mir_verify MODULE "unsound_global::bar" [foo_spec] false bar_setup z3;
+
+print "Should not have succeeded - unsound!";