From c4af4eb24497c9d89211bc1de5457dcc2f83d3df Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Mon, 18 Oct 2021 18:38:07 +0200
Subject: [PATCH] destruction problem solved

---
 examples/lockall_destruct.rs   |  6 ++--
 examples/lockall_soundness2.rs | 53 ++++++++++++++++++++++++++++++++++
 2 files changed, 56 insertions(+), 3 deletions(-)
 create mode 100644 examples/lockall_soundness2.rs

diff --git a/examples/lockall_destruct.rs b/examples/lockall_destruct.rs
index 9add1cefd8..aab25bcef2 100644
--- a/examples/lockall_destruct.rs
+++ b/examples/lockall_destruct.rs
@@ -1,4 +1,4 @@
-//! examples/lockall.rs
+//! examples/lockall_destruct.rs
 
 #![deny(unsafe_code)]
 #![deny(warnings)]
@@ -30,9 +30,9 @@ mod app {
     // when omitted priority is assumed to be `1`
     #[task(shared = [a, b])]
     fn foo(mut c: foo::Context) {
-        c.shared.lock(|Shared { a, b }| {
+        c.shared.lock(|foo::Shared { a, b }| {
             hprintln!("foo: a = {}, b = {}", a, b).ok();
-            *a += 1;
+            **a += 1;
             bar::spawn().unwrap();
             baz::spawn().unwrap();
             hprintln!("still in foo::lock").ok();
diff --git a/examples/lockall_soundness2.rs b/examples/lockall_soundness2.rs
new file mode 100644
index 0000000000..f3d71dd532
--- /dev/null
+++ b/examples/lockall_soundness2.rs
@@ -0,0 +1,53 @@
+//! examples/lockall_soundness2.rs
+
+// #![deny(unsafe_code)]
+#![deny(warnings)]
+#![no_main]
+#![no_std]
+
+use panic_semihosting as _;
+
+#[rtic::app(device = lm3s6965, dispatchers = [GPIOA])]
+mod app {
+    use cortex_m_semihosting::{debug, hprintln};
+
+    #[shared]
+    struct Shared {
+        a: u32,
+        b: i64,
+    }
+
+    #[local]
+    struct Local {}
+
+    #[init]
+    fn init(_: init::Context) -> (Shared, Local, init::Monotonics) {
+        foo::spawn().unwrap();
+
+        (Shared { a: 1, b: 2 }, Local {}, init::Monotonics())
+    }
+
+    // when omitted priority is assumed to be `1`
+    #[task(shared = [a, b])]
+    fn foo(mut c: foo::Context) {
+        static mut X: Option<&'static mut u32> = None;
+        static mut Y: u32 = 0;
+        c.shared.lock(|foo::Shared { a, b }| {
+            hprintln!("s.a = {}, s.b = {}", a, b).ok();
+            **a += 1;
+
+            // soundness check
+            // c.shared.lock(|s| {}); // borrow error
+            // c.shared.a.lock(|s| {}); // borrow error
+
+            unsafe {
+                X = Some(&mut Y);
+                // X = Some(*a); // lifetime issue
+                // X = Some(&mut **a); // lifetime issue
+                // X = Some(&'static mut **a); // not rust
+            }
+            hprintln!("s.a = {}, s.b = {}", a, b).ok();
+        });
+        debug::exit(debug::EXIT_SUCCESS); // Exit QEMU simulator
+    }
+}