diff --git a/examples/atomic_increment.rs b/examples/atomic_increment.rs index a4227ec331..338dfbef0d 100644 --- a/examples/atomic_increment.rs +++ b/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)); } diff --git a/examples/basic_lock1.rs b/examples/basic_lock1.rs index 077befe596..dd89d24615 100644 --- a/examples/basic_lock1.rs +++ b/examples/basic_lock1.rs @@ -64,7 +64,7 @@ impl Lock { 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; diff --git a/examples/cuckoo_hash_table/cuckoo.rs b/examples/cuckoo_hash_table/cuckoo.rs index 8d55accd4d..966914bd4c 100644 --- a/examples/cuckoo_hash_table/cuckoo.rs +++ b/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; diff --git a/examples/cuckoo_hash_table/main.rs b/examples/cuckoo_hash_table/main.rs index 29221e7a1c..aec25a08b9 100644 --- a/examples/cuckoo_hash_table/main.rs +++ b/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 = None; + let tracked mut pt1_a: Option = 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 = None; + let tracked mut pt1_a: Option = 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 = None; + let tracked mut pt1_a: Option = 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()); diff --git a/examples/logatom_lib.rs b/examples/logatom_lib.rs index 57c0054809..0da8eda9ab 100644 --- a/examples/logatom_lib.rs +++ b/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(var: &MyPAtomicU64, Tracked(carrier): Tracked 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); diff --git a/examples/resource/agreement.rs b/examples/resource/agreement.rs index 6b0dc37537..d3ab00b33c 100644 --- a/examples/resource/agreement.rs +++ b/examples/resource/agreement.rs @@ -91,7 +91,7 @@ impl AgreementResource { pub fn main() { let tracked r1 = AgreementResource::::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); diff --git a/examples/resource/log.rs b/examples/resource/log.rs index 0c3ed03cf8..a590425892 100644 --- a/examples/resource/log.rs +++ b/examples/resource/log.rs @@ -275,7 +275,7 @@ impl LogResource { } pub fn main() { - let tracked full_auth = LogResource::::alloc(); + let tracked mut full_auth = LogResource::::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 { diff --git a/examples/resource/monotonic_counter.rs b/examples/resource/monotonic_counter.rs index 0be8e62946..e1f7c85753 100644 --- a/examples/resource/monotonic_counter.rs +++ b/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); diff --git a/examples/resource/oneshot.rs b/examples/resource/oneshot.rs index 94db46d55d..34e6d5c5f0 100644 --- a/examples/resource/oneshot.rs +++ b/examples/resource/oneshot.rs @@ -425,7 +425,7 @@ impl OneShotResource2 { // 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::::alloc(); + let tracked mut full = OneShotResource2::::alloc(); proof { full.shoot(2); } diff --git a/examples/state_machines/tutorial/counting_to_n.rs b/examples/state_machines/tutorial/counting_to_n.rs index fab0f816c4..4088d6e809 100644 --- a/examples/state_machines/tutorial/counting_to_n.rs +++ b/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()); diff --git a/examples/state_machines/tutorial/ref_cell.rs b/examples/state_machines/tutorial/ref_cell.rs index c350113882..0d1488c462 100644 --- a/examples/state_machines/tutorial/ref_cell.rs +++ b/examples/state_machines/tutorial/ref_cell.rs @@ -240,7 +240,7 @@ impl RefCell { { 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 { diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs index 27480d7545..27c72554a9 100644 --- a/source/builtin_macros/src/syntax.rs +++ b/source/builtin_macros/src/syntax.rs @@ -1573,9 +1573,10 @@ 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 { @@ -1583,7 +1584,7 @@ impl VisitMut for ExecGhostPatVisitor { } } 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; diff --git a/source/rust_verify_test/tests/cell_lib.rs b/source/rust_verify_test/tests/cell_lib.rs index b2d9ccdbea..dd2a20e973 100644 --- a/source/rust_verify_test/tests/cell_lib.rs +++ b/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::::new(0); + let (c, Tracked(mut points_to)) = PCell::::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::::new(0); + let (c, Tracked(mut points_to)) = PCell::::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::::new(0); + let (c, Tracked(mut points_to)) = PCell::::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::::new(0); + let (c, Tracked(mut points_to)) = PCell::::new(0); *c.borrow_mut(Tracked(&mut points_to)) = 20; diff --git a/source/rust_verify_test/tests/lifetime.rs b/source/rust_verify_test/tests/lifetime.rs index 453239a047..ae9d3e72f6 100644 --- a/source/rust_verify_test/tests/lifetime.rs +++ b/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::::empty(); + let (pptr, Tracked(mut perm)) = PPtr::::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::::empty(); + let (pptr, Tracked(mut perm)) = PPtr::::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); diff --git a/source/rust_verify_test/tests/modes.rs b/source/rust_verify_test/tests/modes.rs index 88628aea96..c1177b244e 100644 --- a/source/rust_verify_test/tests/modes.rs +++ b/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! { diff --git a/source/rust_verify_test/tests/mut_refs_modes.rs b/source/rust_verify_test/tests/mut_refs_modes.rs index c8db92beea..df3877953d 100644 --- a/source/rust_verify_test/tests/mut_refs_modes.rs +++ b/source/rust_verify_test/tests/mut_refs_modes.rs @@ -56,7 +56,7 @@ test_verify_one_file_with_options! { #[test] mut_borrow_of_tracked_local_in_proof_block_to_ghost [] => verus_code! { struct X { } fn test() { - let tracked x = X { }; + let tracked mut x = X { }; proof { let tracked mut_ret = &mut x; } @@ -64,6 +64,21 @@ test_verify_one_file_with_options! { } => Ok(()) } +test_verify_one_file_with_options! { + // issue 1169: a `tracked` local declared without `mut` at exec-fn top level must + // still be rejected when mutably borrowed in a nested proof block, just like a + // missing `mut` on an ordinary exec-mode local. + #[test] mut_borrow_of_tracked_local_missing_mut_issue1169 [] => verus_code! { + struct X { } + fn test() { + let tracked x = X { }; + proof { + let tracked mut_ret = &mut x; + } + } + } => Err(err) => assert_rust_error_msg(err, "cannot borrow `x` as mutable, as it is not declared as mutable") +} + test_verify_one_file_with_options! { #[test] mut_borrow_of_exec_local_in_proof_block_to_tracked [] => verus_code! { struct X { } diff --git a/source/vir/src/ast_simplify.rs b/source/vir/src/ast_simplify.rs index 0dfa039384..885186a779 100644 --- a/source/vir/src/ast_simplify.rs +++ b/source/vir/src/ast_simplify.rs @@ -19,7 +19,7 @@ use crate::ast_util::{ conjoin, mk_eq, mk_implies, place_to_spec_expr, typ_args_for_datatype_typ, undecorate_typ, unit_typ, wrap_in_trigger, }; -use crate::ast_visitor::VisitorScopeMap; +use crate::ast_visitor::{AstVisitor, VisitorScopeMap}; use crate::context::GlobalCtx; use crate::def::dummy_param_name; use crate::def::is_dummy_param_name; @@ -31,6 +31,7 @@ use crate::messages::Span; use crate::messages::{error, internal_error}; use crate::sst_util::subst_typ_for_datatype; use crate::util::vec_map_result; +use crate::visitor::Walk; use air::ast_util::ident_binder; use air::scope_map::ScopeMap; use std::collections::{HashMap, HashSet}; @@ -1196,11 +1197,120 @@ fn add_fndef_axioms_to_function( Ok((Spanned::new(function.span.clone(), functionx), trait_impls_out, assoc_type_impl)) } +/// Catches a real reassignment of a no-initializer ghost/tracked declaration +/// (`let ghost x;`/`let tracked x;`, how exec-top-level bindings desugar - see +/// #2865) that simplify_one_expr's check can't see, since it only tracks a static +/// "declaration had an initializer" flag, not how many times the variable's +/// actually been assigned. Runs as its own walk (not part of simplify_one_expr) so +/// it can be control-flow aware - see the `if`/`match`/`loop` cases below. +struct DelayedInitChecker { + scope_map: VisitorScopeMap, + assigned: HashSet, +} + +impl DelayedInitChecker { + fn check_assign_target(&mut self, expr: &Expr, place: &Place) -> Result<(), VirErr> { + if !crate::ast_util::place_has_deref_mut(place) + && let Some(local) = crate::ast_util::place_get_local(place) + && let PlaceX::Local(x) = &local.x + && let Some(entry) = self.scope_map.get(x) + && entry.user_mut == Some(false) + && !entry.init + && !self.assigned.insert(x.clone()) + { + let name = user_local_name(x); + return Err(error(&expr.span, format!("variable `{name:}` is not marked mutable"))); + } + Ok(()) + } +} + +impl AstVisitor for DelayedInitChecker { + fn scoper(&mut self) -> Option<&mut VisitorScopeMap> { + Some(&mut self.scope_map) + } + + fn visit_typ(&mut self, _typ: &Typ) -> Result<(), VirErr> { + Ok(()) + } + + fn visit_stmt(&mut self, stmt: &Stmt) -> Result<(), VirErr> { + self.visit_stmt_rec(stmt) + } + + fn visit_place(&mut self, place: &Place) -> Result<(), VirErr> { + self.visit_place_rec(place) + } + + fn visit_pattern(&mut self, pattern: &Pattern) -> Result<(), VirErr> { + self.visit_pattern_rec(pattern) + } + + fn visit_expr(&mut self, expr: &Expr) -> Result<(), VirErr> { + match &expr.x { + ExprX::Assign { place, .. } + | ExprX::BorrowMut(place) + | ExprX::TwoPhaseBorrowMut(place) + | ExprX::BorrowMutTracked(place) => { + self.check_assign_target(expr, place)?; + self.visit_expr_rec(expr) + } + // Each branch gets a fresh, empty set, not a copy of the pre-conditional + // state: branches are alternatives, so assigning once per branch (e.g. + // resolving a prophecy variable) is fine even if an earlier assignment on + // the path into the conditional already used up the free slot. + ExprX::If(cond, thn, els) => { + self.visit_expr(cond)?; + let saved = std::mem::take(&mut self.assigned); + self.visit_expr(thn)?; + self.assigned = HashSet::new(); + if let Some(els) = els { + self.visit_expr(els)?; + } + self.assigned = saved; + Ok(()) + } + ExprX::Match(place, arms, _) => { + self.visit_place(place)?; + let saved = std::mem::take(&mut self.assigned); + for arm in arms.iter() { + self.assigned = HashSet::new(); + self.visit_arm(arm)?; + } + self.assigned = saved; + Ok(()) + } + ExprX::Loop { cond, body, invs, decrease, .. } => { + if let Some(cond) = cond { + self.visit_expr(cond)?; + } + let saved = std::mem::take(&mut self.assigned); + self.visit_expr(body)?; + self.assigned = saved; + self.visit_loop_invariants(invs)?; + for e in decrease.iter() { + self.visit_expr(e)?; + } + Ok(()) + } + _ => self.visit_expr_rec(expr), + } + } +} + +fn check_delayed_init_reassignment(function: &Function) -> Result<(), VirErr> { + let mut checker = DelayedInitChecker { scope_map: ScopeMap::new(), assigned: HashSet::new() }; + checker.visit_function(function)?; + Ok(()) +} + fn simplify_function( ctx: &GlobalCtx, state: &mut State, function: &Function, ) -> Result { + check_delayed_init_reassignment(function)?; + state.reset_for_function(); let mut functionx = function.x.clone();