vir: catch delayed-init reassignment for ghost/tracked locals

examples/atomic_increment.rs

@@ -30,7 +30,7 @@ pub fn increment_bad(var: &PAtomicU64, Tracked(perm): Tracked<&mut PermissionU64
 ////////////////////////////////////////////////////////////////////////////////
 
 fn call_increment_bad() {
-    let (var, Tracked(perm)) = PAtomicU64::new(6);
+    let (var, Tracked(mut perm)) = PAtomicU64::new(6);
     increment_bad(&var, Tracked(&mut perm));
 }
 

examples/basic_lock1.rs

@@ -64,7 +64,7 @@ impl<T> Lock<T> {
         loop
             invariant self.wf(),
         {
-            let tracked points_to_opt = None;
+            let tracked mut points_to_opt = None;
             let res;
             open_atomic_invariant!(self.inv.borrow() => ghost_stuff => {
                 let tracked (mut atomic_permission, mut points_to_inv) = ghost_stuff;

examples/cuckoo_hash_table/cuckoo.rs

@@ -729,7 +729,7 @@ impl MyHashMap {
         let h1x = if l1 < l2 { h1 } else { h2 };
         let h2x = if l1 < l2 { h2 } else { h1 };
 
-        let (Tracked(lock1x), handle1x) = self.locks[l1x].acquire_write();
+        let (Tracked(mut lock1x), handle1x) = self.locks[l1x].acquire_write();
 
         let mut i: usize = 0;
         while i < WIDTH
@@ -770,7 +770,7 @@ impl MyHashMap {
             i += 1;
         }
 
-        let (Tracked(lock2x), handle2x) = self.locks[l2x].acquire_write();
+        let (Tracked(mut lock2x), handle2x) = self.locks[l2x].acquire_write();
 
         let mut i: usize = 0;
         while i < WIDTH
@@ -862,7 +862,7 @@ impl MyHashMap {
         let h2x = if l1 < l2 { h2 } else { h1 };
 
         let (Tracked(_unused), main_handle) = self.main_write_lock.acquire_write();
-        let (Tracked(lock1x), handle1x) = self.locks[l1x].acquire_write();
+        let (Tracked(mut lock1x), handle1x) = self.locks[l1x].acquire_write();
 
         // Update the key, value pair if it already exists
 
@@ -906,7 +906,7 @@ impl MyHashMap {
             i += 1;
         }
 
-        let (Tracked(lock2x), handle2x) = self.locks[l2x].acquire_write();
+        let (Tracked(mut lock2x), handle2x) = self.locks[l2x].acquire_write();
 
         let mut i: usize = 0;
         while i < WIDTH
@@ -1157,7 +1157,7 @@ impl MyHashMap {
         // to prove that correct, instead I'm just going to repeat the code from the beginning
         // of the function.
 
-        let (Tracked(lock1x), handle1x) = self.locks[l1x].acquire_write();
+        let (Tracked(mut lock1x), handle1x) = self.locks[l1x].acquire_write();
 
         // Update the key, value pair if it already exists
 
@@ -1201,7 +1201,7 @@ impl MyHashMap {
             i += 1;
         }
 
-        let (Tracked(lock2x), handle2x) = self.locks[l2x].acquire_write();
+        let (Tracked(mut lock2x), handle2x) = self.locks[l2x].acquire_write();
 
         let mut i: usize = 0;
         while i < WIDTH
@@ -1394,8 +1394,8 @@ impl MyHashMap {
         let l1x = if l1 < l2 { l1 } else { l2 };
         let l2x = if l1 < l2 { l2 } else { l1 };
 
-        let (Tracked(lock1x), handle1x) = self.locks[l1x].acquire_write();
-        let (Tracked(lock2x), handle2x) = self.locks[l2x].acquire_write();
+        let (Tracked(mut lock1x), handle1x) = self.locks[l1x].acquire_write();
+        let (Tracked(mut lock2x), handle2x) = self.locks[l2x].acquire_write();
 
         let tracked mut lock1;
         let tracked mut lock2;

examples/cuckoo_hash_table/main.rs

@@ -23,25 +23,25 @@ fn runtime_assert(b: bool)
 fn main() {
     let (hm, Tracked(mut pt_map)) = cuckoo::MyHashMap::new();
 
-    let tracked pt1 = Some(pt_map.remove(1));
+    let tracked mut pt1 = Some(pt_map.remove(1));
     let tracked pt2 = Some(pt_map.remove(2));
     let tracked pt3 = Some(pt_map.remove(3));
 
-    let tracked pt1_a: Option<MPointsTo> = None;
+    let tracked mut pt1_a: Option<MPointsTo> = None;
     let r = hm.read(1) atomically |upd| -> ReadAU {
         pt1_a = Some(upd(pt1.tracked_take()).get());
     };
 
-    let tracked pt1 = pt1_a;
+    let tracked mut pt1 = pt1_a;
     assert(r === None);
     print(r);
 
-    let tracked pt1_a: Option<MPointsTo> = None;
+    let tracked mut pt1_a: Option<MPointsTo> = None;
     let success = hm.insert(1, 17) atomically |upd| -> InsertAU {
         pt1_a = Some(upd(pt1.tracked_take()).get());
     };
 
-    let tracked pt1 = pt1_a;
+    let tracked mut pt1 = pt1_a;
 
     runtime_assert(success);
 
@@ -52,12 +52,12 @@ fn main() {
     assert(r === Some(17));
     print(r);
 
-    let tracked pt1_a: Option<MPointsTo> = None;
+    let tracked mut pt1_a: Option<MPointsTo> = None;
     let success = hm.delete(1) atomically |upd| -> DeleteAU {
         pt1_a = Some(upd(pt1.tracked_take()).get());
     };
 
-    let tracked pt1 = pt1_a;
+    let tracked mut pt1 = pt1_a;
 
     let r = hm.read(1) atomically |upd| -> ReadAU {
         pt1 = Some(upd(pt1.tracked_take()).get());

examples/logatom_lib.rs

@@ -155,7 +155,7 @@ pub exec fn increment_seq(var: &MyPAtomicU64, Tracked(my_perm): Tracked<&mut MyP
 
     let next = curr.wrapping_add(1);
     open_atomic_invariant!(var.inv.borrow() => v => {
-        let tracked V { perm, auth } = v;
+        let tracked V { mut perm, mut auth } = v;
         var.inner.store(Tracked(&mut perm), next);
         proof {
             auth.update(&mut my_perm.inner, next);
@@ -193,7 +193,7 @@ pub fn increment_perm(var: &MyPAtomicU64, Tracked(my_perm): Tracked<&mut MyPermi
         let res;
 
         open_atomic_invariant!(inv => v => {
-            let tracked V { perm, auth } = v;
+            let tracked V { mut perm, mut auth } = v;
             let ghost prev: u64 = perm@.value;
 
             res = var.inner.compare_exchange_weak(Tracked(&mut perm), curr, next);
@@ -325,7 +325,7 @@ pub fn increment<Carrier>(var: &MyPAtomicU64, Tracked(carrier): Tracked<Carrier>
         let res;
 
         open_atomic_invariant!(inv => v => {
-            let tracked V { perm, auth } = v;
+            let tracked V { mut perm, auth } = v;
             let ghost prev: u64 = perm@.value;
 
             res = var.inner.compare_exchange_weak(Tracked(&mut perm), curr, next);

examples/resource/agreement.rs

@@ -91,7 +91,7 @@ impl<T> AgreementResource<T> {
 pub fn main() {
     let tracked r1 = AgreementResource::<int>::alloc(72);
     assert(r1@ == 72);
-    let tracked r2 = r1.duplicate();
+    let tracked mut r2 = r1.duplicate();
     assert(r2@ == r1@);
     proof {
         r1.lemma_agreement(&mut r2);

examples/resource/log.rs

@@ -275,7 +275,7 @@ impl<T> LogResource<T> {
 }
 
 pub fn main() {
-    let tracked full_auth = LogResource::<int>::alloc();
+    let tracked mut full_auth = LogResource::<int>::alloc();
     assert(full_auth@ is FullAuthority);
     assert(full_auth@.log().len() == 0);
     proof {
@@ -287,7 +287,7 @@ pub fn main() {
     assert(full_auth@.log().len() == 2);
     assert(full_auth@.log()[0] == 42);
     assert(full_auth@.log()[1] == 86);
-    let tracked (half_auth1, half_auth2) = full_auth.split();
+    let tracked (mut half_auth1, mut half_auth2) = full_auth.split();
     assert(half_auth1@ == half_auth2@);
     assert(half_auth1@ is HalfAuthority);
     proof {

examples/resource/monotonic_counter.rs

@@ -325,13 +325,13 @@ impl MonotonicCounterResource {
 
 // This example illustrates some uses of the monotonic counter.
 fn main() {
-    let tracked full = MonotonicCounterResource::alloc();
+    let tracked mut full = MonotonicCounterResource::alloc();
     proof {
         full.increment();
     }
     assert(full@.n() == 1);
     let tracked full = MonotonicCounterResource::alloc();
-    let tracked zero_lower_bound = full.extract_lower_bound();
+    let tracked mut zero_lower_bound = full.extract_lower_bound();
     let tracked (mut half1, mut half2) = full.split();
     assert(half1.id() == half2.id());
     assert(half1@.n() == 0);

examples/resource/oneshot.rs

@@ -425,7 +425,7 @@ impl<T> OneShotResource2<T> {
 
 // This example illustrates some uses of the one-shot functions.
 fn test_manual() {
-    let tracked full = OneShotResource::alloc();
+    let tracked mut full = OneShotResource::alloc();
     proof {
         full.perform();
     }
@@ -450,7 +450,7 @@ fn test_manual() {
 }
 
 fn test_combinator() {
-    let tracked full = OneShotResource2::<int>::alloc();
+    let tracked mut full = OneShotResource2::<int>::alloc();
     proof {
         full.shoot(2);
     }

examples/state_machines/tutorial/counting_to_n.rs

@@ -114,8 +114,8 @@ fn do_count(num_threads: u32) {
     let tracked (
         Tracked(instance),
         Tracked(counter_token),
-        Tracked(unstamped_tokens),
-        Tracked(stamped_tokens),
+        Tracked(mut unstamped_tokens),
+        Tracked(mut stamped_tokens),
     ) = X::Instance::initialize(num_threads as nat);
     // Initialize the counter
     let tracked_instance = Tracked(instance.clone());

examples/state_machines/tutorial/ref_cell.rs

@@ -240,7 +240,7 @@ impl<S> RefCell<S> {
     {
         let (rc_cell, Tracked(rc_perm)) = cell::PCell::new(0);
         let (value_cell, Tracked(value_perm)) = cell::PCell::new(s);
-        let tracked (Tracked(inst), Tracked(flag), _, Tracked(writer)) = RefCounter::Instance::<
+        let tracked (Tracked(inst), Tracked(mut flag), _, Tracked(writer)) = RefCounter::Instance::<
             S,
         >::initialize_empty(value_cell.id(), None);
         proof {

source/builtin_macros/src/syntax.rs

@@ -1573,17 +1573,18 @@ impl VisitMut for ExecGhostPatVisitor {
                     let mut x = id.clone();
                     x.mutability = None;
                     let span = id.span();
+                    let mutability = id.mutability;
                     let decl = if path_is_ident(&pts.path, "Tracked") {
                         if self.inside_ghost == 0 {
-                            parse_quote_spanned!(span => #[verus::internal(proof)] let mut #x;)
+                            parse_quote_spanned!(span => #[verus::internal(proof)] let #mutability #x;)
                         } else if id.mutability.is_some() {
                             parse_quote_spanned!(span => #[verus::internal(proof)] let mut #x = #tmp_x.get();)
                         } else {
                             parse_quote_spanned!(span => #[verus::internal(proof)] let #x = #tmp_x.get();)
                         }
                     } else {
                         if self.inside_ghost == 0 {
-                            parse_quote_spanned!(span => #[verus::internal(spec)] #[verus::internal(infer_proph)] let mut #x;)
+                            parse_quote_spanned!(span => #[verus::internal(spec)] #[verus::internal(infer_proph)] let #mutability #x;)
                         } else if id.mutability.is_some() {
                             parse_quote_spanned!(span => #[verus::internal(spec)] let mut #x = #tmp_x.view();)
                         } else {
@@ -1629,12 +1630,13 @@ impl VisitMut for ExecGhostPatVisitor {
                 }
                 let tmp_x = mk_ident_tmp(&id.ident);
                 let mut x = id.clone();
+                let mutability = x.mutability;
                 x.mutability = None;
                 let span = id.span();
                 let decl = if self.ghost.is_some() {
-                    parse_quote_spanned!(span => #[verus::internal(spec)] #[verus::internal(infer_proph)] let mut #x;)
+                    parse_quote_spanned!(span => #[verus::internal(spec)] #[verus::internal(infer_proph)] let #mutability #x;)
                 } else {
-                    parse_quote_spanned!(span => #[verus::internal(infer_mode)] let mut #x;)
+                    parse_quote_spanned!(span => #[verus::internal(infer_mode)] let #mutability #x;)
                 };
                 let assign = quote_spanned!(span => #x = #tmp_x);
                 id.ident = tmp_x;

source/rust_verify_test/tests/cell_lib.rs

@@ -361,7 +361,7 @@ test_verify_one_file_with_options! {
         verus!{
 
         fn cell_test() {
-            let (c, Tracked(points_to)) = PCell::<u64>::new(0);
+            let (c, Tracked(mut points_to)) = PCell::<u64>::new(0);
 
             let r = c.borrow_mut(Tracked(&mut points_to));
             *r = 20;
@@ -371,7 +371,7 @@ test_verify_one_file_with_options! {
         }
 
         fn cell_test2() {
-            let (c, Tracked(points_to)) = PCell::<u64>::new(0);
+            let (c, Tracked(mut points_to)) = PCell::<u64>::new(0);
 
             *c.borrow_mut(Tracked(&mut points_to)) = 20;
 
@@ -380,7 +380,7 @@ test_verify_one_file_with_options! {
         }
 
         fn fails_cell_test() {
-            let (c, Tracked(points_to)) = PCell::<u64>::new(0);
+            let (c, Tracked(mut points_to)) = PCell::<u64>::new(0);
 
             let r = c.borrow_mut(Tracked(&mut points_to));
             *r = 20;
@@ -391,7 +391,7 @@ test_verify_one_file_with_options! {
         }
 
         fn fails_cell_test2() {
-            let (c, Tracked(points_to)) = PCell::<u64>::new(0);
+            let (c, Tracked(mut points_to)) = PCell::<u64>::new(0);
 
             *c.borrow_mut(Tracked(&mut points_to)) = 20;
 

source/rust_verify_test/tests/lifetime.rs

@@ -552,15 +552,15 @@ test_verify_one_file! {
 
 test_verify_one_file_with_options! {
     #[test] assign_twice_no_lifetime ["--no-lifetime"] => verus_code! {
-        // It's fine to accept this because --no-lifetime means we don't
-        // have any real guarantees. It would also be fine to error here.
+        // With --no-lifetime, real rustc borrowck doesn't run, so this now relies
+        // on the same internal check as test_no_lifetime_mut_check above.
         fn test() {
             let x: u8;
             x = 5;
             x = 7;
-            assert(false); // FAILS
+            assert(false);
         }
-    } => Err(err) => assert_fails(err, 1)
+    } => Err(err) => assert_vir_error_msg(err, "variable `x` is not marked mutable")
 }
 
 test_verify_one_file! {
@@ -578,7 +578,7 @@ test_verify_one_file! {
     #[test] tracked_new_issue870 verus_code! {
         use vstd::simple_pptr::*;
         fn test() {
-            let (pptr, Tracked(perm)) = PPtr::<u64>::empty();
+            let (pptr, Tracked(mut perm)) = PPtr::<u64>::empty();
             pptr.put(Tracked(&mut perm), 5);
             let x: &u64 = pptr.borrow(Tracked(&perm)); // should tie x's lifetime to the perm borrow
             assert(x == 5);
@@ -592,7 +592,7 @@ test_verify_one_file! {
     #[test] tracked_new2_issue870 verus_code! {
         use vstd::simple_pptr::*;
         fn test() {
-            let (pptr, Tracked(perm)) = PPtr::<u64>::empty();
+            let (pptr, Tracked(mut perm)) = PPtr::<u64>::empty();
             pptr.put(Tracked(&mut perm), 5);
             let x: &u64 = pptr.borrow(Tracked(&perm)); // should tie x's lifetime to the perm borrow
             assert(x == 5);

source/rust_verify_test/tests/modes.rs

@@ -378,22 +378,22 @@ test_verify_one_file_with_options! {
             #[verifier::spec] let x: u64;
             x = 2;
             x = 3;
-            verus_builtin::assert_(false); // FAILS
+            verus_builtin::assert_(false);
         }
-    } => Err(err) => assert_fails(err, 1)
+    } => Err(err) => assert_vir_error_msg(err, "variable `x` is not marked mutable")
 }
 
 test_verify_one_file! {
     #[test] decl_init_let_spec_fail2 verus_code! {
         fn test1() {
-            let ghost x: u64; // TODO should probably require this to be mut
+            let ghost x: u64;
             proof {
                 x = 2;
                 x = 3;
             }
-            assert(false); // FAILS
+            assert(false);
         }
-    } => Err(err) => assert_fails(err, 1)
+    } => Err(err) => assert_vir_error_msg(err, "variable `x` is not marked mutable")
 }
 
 test_verify_one_file! {
@@ -402,9 +402,9 @@ test_verify_one_file! {
             let x: u64;
             x = 2;
             x = 3;
-            assert(false); // FAILS
+            assert(false);
         }
-    } => Err(err) => assert_fails(err, 1)
+    } => Err(err) => assert_vir_error_msg(err, "variable `x` is not marked mutable")
 }
 
 const FIELD_UPDATE: &str = code_str! {