From 9757217934d4d1edc3927422ccab3e9c0ba8c874 Mon Sep 17 00:00:00 2001 From: Awesome Rustacean Date: Mon, 27 Jul 2026 21:12:50 +0300 Subject: [PATCH 1/8] fix: reject missing return values Track divergent flow across branches and loops. Validate implicit `()` against fn output on fallthrough. fixes #392. --- .../src/check/borrow_check/flow_state.rs | 44 +++++++++----- .../src/check/borrow_check/nll.rs | 36 ++++++++++-- tests/borrowck.rs | 16 ++--- tests/mir_typeck.rs | 4 +- tests/return_validation.rs | 58 +++++++++++++++---- 5 files changed, 118 insertions(+), 40 deletions(-) diff --git a/crates/formality-rust/src/check/borrow_check/flow_state.rs b/crates/formality-rust/src/check/borrow_check/flow_state.rs index 9f24e44b9..0c68e0a25 100644 --- a/crates/formality-rust/src/check/borrow_check/flow_state.rs +++ b/crates/formality-rust/src/check/borrow_check/flow_state.rs @@ -145,6 +145,7 @@ where let Union((a, b)) = term; let a: FlowState = a.upcast(); let b: FlowState = b.upcast(); + let diverged = a.diverged && b.diverged; // At join points, locals (for name resolution) must be identical on both sides. // Only drop_locals may differ (due to `let 'a: x = ...` in one branch). @@ -164,6 +165,8 @@ where continues: Union((a.continues, b.continues)).upcast(), all_outlives: Union((a.all_outlives, b.all_outlives)).upcast(), scopes, + // A join point is unreachable only if both incoming edges are. + diverged, } } } @@ -196,6 +199,9 @@ pub struct FlowState { pub continues: Set, pub all_outlives: Set, + + /// If true, this program point is unreachable (all paths returned, broke, or continued). + pub diverged: bool, } impl FlowState { @@ -225,20 +231,15 @@ impl FlowState { pub fn with_loan(&self, loan: Loan) -> Self { Self { current: self.current.with_loan(loan), - breaks: self.breaks.clone(), - continues: self.continues.clone(), - scopes: self.scopes.clone(), - all_outlives: self.all_outlives.clone(), + ..self.clone() } } pub fn with_outlives(&self, outlives: &Set) -> Self { Self { current: self.current.with_outlives(outlives), - breaks: self.breaks.clone(), - continues: self.continues.clone(), - scopes: self.scopes.clone(), all_outlives: Union((&self.all_outlives, outlives)).upcast(), + ..self.clone() } } @@ -261,25 +262,30 @@ impl FlowState { pub fn diverges(&self) -> Self { Self { current: PointFlowState::default(), + diverged: true, ..self.clone() } } pub fn with_break(&self, label: &LabelId) -> Self { let mut this = self.clone(); - this.breaks.insert(LabeledFlowState { - label: label.clone(), - state: this.current.clone(), - }); + if !this.diverged { + this.breaks.insert(LabeledFlowState { + label: label.clone(), + state: this.current.clone(), + }); + } this } pub fn with_continue(&self, label: &LabelId) -> Self { let mut this = self.clone(); - this.continues.insert(LabeledFlowState { - label: label.clone(), - state: this.current.clone(), - }); + if !this.diverged { + this.continues.insert(LabeledFlowState { + label: label.clone(), + state: this.current.clone(), + }); + } this } @@ -473,6 +479,7 @@ impl FlowState { breaks, continues, all_outlives, + diverged, } = self.clone(); // Pop and destructure the top scope. @@ -501,6 +508,8 @@ impl FlowState { .into_iter() .partition(|lfs| Some(&lfs.label) == scope_label.as_ref()); let mut successor = current; + // A break targeting this scope is live control arriving after it. + let diverged = diverged && this_label.is_empty(); for lfs in this_label { successor = Union((successor, lfs.state)).upcast(); } @@ -516,6 +525,7 @@ impl FlowState { breaks: other_labels, continues, all_outlives, + diverged, } } @@ -530,6 +540,7 @@ impl FlowState { breaks, continues, all_outlives, + diverged, } = self.clone(); let (this_label, other_labels): (Set, Set) = @@ -545,6 +556,7 @@ impl FlowState { breaks, continues: other_labels, all_outlives, + diverged, } } @@ -631,6 +643,8 @@ impl FlowState { breaks: self.breaks.clone(), continues: self.continues.clone(), all_outlives, + // The rerun starts from the entry state, so it inherits its reachability. + diverged: self.diverged, } } } diff --git a/crates/formality-rust/src/check/borrow_check/nll.rs b/crates/formality-rust/src/check/borrow_check/nll.rs index ccb465716..1c5cab683 100644 --- a/crates/formality-rust/src/check/borrow_check/nll.rs +++ b/crates/formality-rust/src/check/borrow_check/nll.rs @@ -135,7 +135,9 @@ judgment_fn! { debug(assumptions, env, state, block) ( - (borrow_check_block(env, assumptions, state, block, LivePlaces::default()) => _state) + (borrow_check_block(env, assumptions, state, block, LivePlaces::default()) => state) + (for_all(output_ty in env.output_ty.iter()) + (fall_through_permitted(env, assumptions, state, output_ty) => ())) ------------------------------------------------------------ ("borrow_check") (borrow_check(env, assumptions, state, block) => ()) ) @@ -245,6 +247,8 @@ judgment_fn! { (let continue_live = Stmt::loop_(label, body).live_before(&env, &state, places_live_on_exit)) (let state = state.push_continue_scope(&env.env, label, places_live_on_exit, continue_live)?) (borrow_check_loop(env, assumptions, state, body, places_live_on_exit) => state) + // The loop exit is reachable only via `break` (revived in `pop_scope`). + (let state = state.diverges()) (let state = state.pop_scope(label)) ------------------------------------------------------------ ("loop") (borrow_check_statement(env, assumptions, state, Stmt::Loop { label, body }, places_live_on_exit) => (env, state)) @@ -764,11 +768,8 @@ fn kill_loans(overwritten_place: &TypedPlaceExpr, state: &FlowState) -> FlowStat .retain(|loan| !overwritten_place.is_prefix_of(&loan.place)); FlowState { - scopes: state.scopes.clone(), current, - breaks: state.breaks.clone(), - continues: state.continues.clone(), - all_outlives: state.all_outlives.clone(), + ..state.clone() } } @@ -1064,6 +1065,31 @@ judgment_fn! { } } +judgment_fn! { + /// Control that falls off the end of a fn body implicitly returns `()`; + /// permitted if the end is unreachable or `()` is assignable to the declared output type. + fn fall_through_permitted( + env: TypeckEnv, + assumptions: Wcs, + state: FlowState, + output_ty: Ty, + ) => () { + debug(state, output_ty, assumptions, env) + ( + (if state.diverged)! + ------------------------------------------------------------- ("end of body unreachable") + (fall_through_permitted(_env, _assumptions, state, _output_ty) => ()) + ) + + ( + (if !state.diverged) + (prove_assignable(env, assumptions, state, Ty::unit(), output_ty) => _state) + -------------------------------------------------------------- ("implicit unit return") + (fall_through_permitted(_env, _assumptions, state, output_ty) => ()) + ) + } +} + judgment_fn! { /// Prove that `a` is assignable to `b`. fn prove_assignable( diff --git a/tests/borrowck.rs b/tests/borrowck.rs index d1076ca34..3dc3f42f1 100644 --- a/tests/borrowck.rs +++ b/tests/borrowck.rs @@ -4047,8 +4047,8 @@ fn issue_57165_conditional() { .err(expect_test::expect![[r#" the rule "fixed-point" at (nll.rs) failed because condition evaluated to false: `state0 == state1` - state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)}) - state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}) + state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)}, false) + state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, false) the rule "borrow of disjoint places" at (nll.rs) failed because condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` @@ -4094,8 +4094,8 @@ fn issue_57165_conditional() { .err(expect_test::expect![[r#" the rule "fixed-point" at (nll.rs) failed because condition evaluated to false: `state0 == state1` - state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)}) - state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}) + state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)}, false) + state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, false) the rule "borrow of disjoint places" at (nll.rs) failed because condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` @@ -4446,8 +4446,8 @@ fn issue_46859_decoder_next() { .err(expect_test::expect![[r#" the rule "fixed-point" at (nll.rs) failed because condition evaluated to false: `state0 == state1` - state0 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}) - state1 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}) + state0 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, false) + state1 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, false) the rule "borrow of disjoint places" at (nll.rs) failed because condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` @@ -4588,8 +4588,8 @@ fn issue_92985_filtering_lending_iterator() { .err(expect_test::expect![[r#" the rule "fixed-point" at (nll.rs) failed because condition evaluated to false: `state0 == state1` - state0 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}) - state1 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}) + state0 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, false) + state1 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, false) the rule "borrow of disjoint places" at (nll.rs) failed because condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` diff --git a/tests/mir_typeck.rs b/tests/mir_typeck.rs index e6753ceca..c85a7f29b 100644 --- a/tests/mir_typeck.rs +++ b/tests/mir_typeck.rs @@ -819,7 +819,7 @@ fn test_field_projection_root_non_adt() { "#]]) .err(expect_test::expect![[r#" the rule "struct field" at (nll.rs) failed because - pattern `(RigidTy { name: RigidName::AdtId(adt_id), parameters }, state)` did not match value `(u32, flow_state([scope(none, None, {}, None, [(v1, u32)], [v1 : u32]), scope(none, None, {}, None, [(v2, Dummy)], [v2 : Dummy])], point_flow_state({}, {}, {}), {}, {}, {}))`"#]]) + pattern `(RigidTy { name: RigidName::AdtId(adt_id), parameters }, state)` did not match value `(u32, flow_state([scope(none, None, {}, None, [(v1, u32)], [v1 : u32]), scope(none, None, {}, None, [(v2, Dummy)], [v2 : Dummy])], point_flow_state({}, {}, {}), {}, {}, {}, false))`"#]]) } /// Test the behaviour of initialising the struct with wrong type. @@ -1020,7 +1020,7 @@ fn test_break_nonexistent_label() { .err(expect_test::expect![[r#" crates/formality-rust/src/check/borrow_check/nll.rs:177:1: no applicable rules for borrow_check_statement { state: flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(none, None, {}, Some({}), [], []), scope(none, None, {}, None, [], [])], point_flow_state({}, {}, {}), {}, {}, {}), statement: break 'nonexistent ;, places_live_on_exit: {}, assumptions: {}, env: TypeckEnv { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: Some(u32) } } - crates/formality-rust/src/check/borrow_check/nll.rs:177:1: no applicable rules for borrow_check_statement { state: flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(none, None, {}, Some({}), [], []), scope(none, None, {}, None, [], [])], point_flow_state({}, {}, {}), {}, {}, {}), statement: break 'nonexistent ;, places_live_on_exit: {}, assumptions: {}, env: TypeckEnv { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: Some(u32) } }"#]]) + crates/formality-rust/src/check/borrow_check/nll.rs:179:1: no applicable rules for borrow_check_statement { state: flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(none, None, {}, Some({}), [], []), scope(none, None, {}, None, [], [])], point_flow_state({}, {}, {}), {}, {}, {}, false), statement: break 'nonexistent ;, places_live_on_exit: {}, assumptions: {}, env: TypeckEnv { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: Some(u32) } }"#]]) } /// `continue` targeting a valid loop label should pass. diff --git a/tests/return_validation.rs b/tests/return_validation.rs index c919ca2d3..bf9ebd18a 100644 --- a/tests/return_validation.rs +++ b/tests/return_validation.rs @@ -1,6 +1,6 @@ use a_mir_formality::{crates, FormalityTest}; -/// Tests for issue #209: ensuring functions return a value on all paths. +/// Tests for issues #209 and #392: ensuring functions return a value on all paths. /// /// These tests verify that a-mir-formality matches rustc's behavior /// for return validation. All error cases have been verified against @@ -10,14 +10,15 @@ use a_mir_formality::{crates, FormalityTest}; /// should be an error — no value is returned. /// rustc: "implicitly returns `()` as its body has no tail or `return` expression" #[test] -#[ignore = "needs return validation (#209)"] fn empty_body_non_unit_return() { FormalityTest::new(crates![crate Foo { fn foo() -> u32 { } }]) - .rustc_err(expect_test::expect![[r#""#]]) - .err(expect_test::expect![[r#"function may not return a value"#]]) + .err(expect_test::expect![[r#" + crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: (), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } } + + crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } }"#]]) } /// A function returning () with an empty body is fine — unit is implicit. @@ -55,7 +56,6 @@ fn if_else_both_branches_return() { /// without returning, so this should be an error. /// rustc: "expected `u32`, found `()`" #[test] -#[ignore = "needs return validation (#209)"] fn if_else_one_branch_returns() { FormalityTest::new(crates![crate Foo { fn foo(b: bool) -> u32 { @@ -65,8 +65,10 @@ fn if_else_one_branch_returns() { } } }]) - .rustc_err(expect_test::expect![[r#""#]]) - .err(expect_test::expect![[r#"function may not return a value"#]]) + .err(expect_test::expect![[r#" + crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: (), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } } + + crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } }"#]]) } /// An infinite loop never terminates, so it never needs to return. @@ -88,7 +90,6 @@ fn infinite_loop_no_return_needed() { /// This should be an error. /// rustc: "expected `u32`, found `()`" #[test] -#[ignore = "needs return validation (#209)"] fn loop_with_break_no_return() { FormalityTest::new(crates![crate Foo { fn foo() -> u32 { @@ -97,8 +98,10 @@ fn loop_with_break_no_return() { } } }]) - .rustc_err(expect_test::expect![[r#""#]]) - .err(expect_test::expect![[r#"function may not return a value"#]]) + .err(expect_test::expect![[r#" + crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: (), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } } + + crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } }"#]]) } /// A loop with break followed by a return is fine — all paths return. @@ -131,3 +134,38 @@ fn simple_return() { .rustc_ok() .ok() } + +/// A break in dead code must not make the loop exit reachable. +#[test] +fn unreachable_break_after_return_does_not_revive_loop_exit() { + FormalityTest::new(crates![crate Foo { + fn foo() -> u32 { + 'a: loop { + return 1_u32; + break 'a; + } + } + }]) + .skip_execute() + .ok() +} + +/// A reachable break on one branch means the loop can fall through. +#[test] +fn loop_with_conditional_break_can_fall_through() { + FormalityTest::new(crates![crate Foo { + fn foo(b: bool) -> u32 { + 'a: loop { + if b { + return 1_u32; + } else { + break 'a; + } + } + } + }]) + .err(expect_test::expect![[r#" + crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: (), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } } + + crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } }"#]]) +} From 36e948d2b33b38394db3c72531ced7369ded18ea Mon Sep 17 00:00:00 2001 From: Awesome Rustacean Date: Thu, 6 Aug 2026 21:50:08 +0300 Subject: [PATCH 2/8] feat: add control-flow model for return validation - track fallthrough, break, and continue outcomes - compose sequential and branching control flow - model block and loop exits - add initial return, break, and continue statement rules and unit tests. --- crates/formality-rust/src/check/mod.rs | 1 + .../formality-rust/src/check/return_check.rs | 381 ++++++++++++++++++ 2 files changed, 382 insertions(+) create mode 100644 crates/formality-rust/src/check/return_check.rs diff --git a/crates/formality-rust/src/check/mod.rs b/crates/formality-rust/src/check/mod.rs index a45d7a3b8..5a815a1b9 100644 --- a/crates/formality-rust/src/check/mod.rs +++ b/crates/formality-rust/src/check/mod.rs @@ -26,6 +26,7 @@ mod coherence; mod core_crate; mod fns; mod impls; +mod return_check; mod traits; mod where_clauses; diff --git a/crates/formality-rust/src/check/return_check.rs b/crates/formality-rust/src/check/return_check.rs new file mode 100644 index 000000000..88fb9421a --- /dev/null +++ b/crates/formality-rust/src/check/return_check.rs @@ -0,0 +1,381 @@ +#![allow(unused)] +use crate::grammar::{ + expr::{Block, LabelId, Stmt}, + Ty, +}; +use formality_core::{judgment_fn, term, Set}; + +/// Computes the control flow that can emerge from a statement. +#[term] +struct ControlFlow { + can_fall_through: bool, + breaks: Set, + continues: Set, +} + +impl ControlFlow { + fn fallthrough() -> Self { + Self { + can_fall_through: true, + breaks: Set::new(), + continues: Set::new(), + } + } + + fn returns() -> Self { + Self { + can_fall_through: false, + breaks: Set::new(), + continues: Set::new(), + } + } + + fn break_to(label: LabelId) -> Self { + let mut breaks = Set::new(); + breaks.insert(label); + + Self { + can_fall_through: false, + breaks, + continues: Set::new(), + } + } + + fn continue_to(label: LabelId) -> Self { + let mut continues = Set::new(); + continues.insert(label); + + Self { + can_fall_through: false, + breaks: Set::new(), + continues, + } + } + + fn then(&self, next: &Self) -> Self { + if !self.can_fall_through { + return self.clone(); + } + + Self { + can_fall_through: next.can_fall_through, + breaks: self.breaks.union(&next.breaks).cloned().collect(), + continues: self.continues.union(&next.continues).cloned().collect(), + } + } + + fn join(&self, other: &Self) -> Self { + Self { + can_fall_through: self.can_fall_through || other.can_fall_through, + breaks: self.breaks.union(&other.breaks).cloned().collect(), + continues: self.continues.union(&other.continues).cloned().collect(), + } + } + + fn exit_block(&self, label: Option<&LabelId>) -> Self { + let mut breaks = self.breaks.clone(); + let matching_break = label.is_some_and(|label| breaks.remove(label)); + + Self { + can_fall_through: self.can_fall_through || matching_break, + breaks, + continues: self.continues.clone(), + } + } + + fn exit_loop(&self, label: Option<&LabelId>) -> Self { + let mut breaks = self.breaks.clone(); + let mut continues = self.continues.clone(); + + let matching_break = if let Some(label) = label { + let matching_breaks = breaks.remove(label); + continues.remove(label); + + matching_breaks + } else { + false + }; + + Self { + can_fall_through: matching_break, + breaks, + continues, + } + } +} + +// judgment_fn! { +// /// Entry point: This answers the question: "Is this function allowed to end?". +// pub(crate) fn check_fn_returns( +// output_ty: Ty, +// block: Block) => () { +// debug(output_ty, block) + +// ( +// // Rules goes here. +// // 1. Unit returning function +// // +// // (output_ty == ()) +// // ---------------------- ("unit return") +// // (check_fn_returns(output_ty, block) => ()) +// // +// // 2. Non-unit returning functions. +// // +// // (output_ty != ()) +// // (control_flow_block(block) => flow) +// // -------------------- ("non-unit returns") +// // (check_fn_returns(output_ty, block) => ()) +// // +// ) +// } +// } + +// judgment_fn! { +// /// This answers the question: "What control flow can emerge from this block?". +// fn control_flow_block( +// block: Block) => ControlFlow { +// debug(block) + +// ( +// // Rules goes here. +// ) +// } +// } + +judgment_fn! { + /// This answers the question: "What control flow can emerge from this one statement.?" + fn control_flow_stmt( + stmt: Stmt) => ControlFlow { + debug(stmt) + + ( + (let flow = ControlFlow::returns()) + --- ("return") + (control_flow_stmt(Stmt::Return {expr: _ }) => flow) + ) + + ( + (let flow = ControlFlow::break_to(label.clone())) + --- ("break") + (control_flow_stmt(Stmt::Break { label }) => flow) + ) + + ( + (let flow = ControlFlow::continue_to(label.clone())) + --- ("continue") + (control_flow_stmt(Stmt::Continue { label }) => flow) + ) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn then_ignores_unreachable_breaks() { + let returned = ControlFlow::returns(); + let unreachable_break = ControlFlow::break_to(LabelId::new("'break")); + + let result = returned.then(&unreachable_break); + + assert!(!result.can_fall_through); + assert!(result.breaks.is_empty()); + assert!(result.continues.is_empty()); + } + + #[test] + fn then_preserves_reachable_breaks() { + let label = LabelId::new("'rb"); + let fallthrough = ControlFlow::fallthrough(); + let break_flow = ControlFlow::break_to(label.clone()); + + let result = fallthrough.then(&break_flow); + + assert!(!result.can_fall_through); + assert!(result.breaks.contains(&label)); + assert!(result.continues.is_empty()); + } + + #[test] + fn then_ignores_unreachable_continues() { + let returned = ControlFlow::returns(); + let unreachable_continue = ControlFlow::continue_to(LabelId::new("'cont")); + + let result = returned.then(&unreachable_continue); + + assert!(!result.can_fall_through); + assert!(result.breaks.is_empty()); + assert!(result.continues.is_empty()); + } + + #[test] + fn join_unions_break_and_continue_targets_from_both_branches() { + let break_label = LabelId::new("'bl"); + let break_flow = ControlFlow::break_to(break_label.clone()); + let continue_label = LabelId::new("'cl"); + let continue_flow = ControlFlow::continue_to(continue_label.clone()); + + let result = break_flow.join(&continue_flow); + + assert!(!result.can_fall_through); + assert!(result.breaks.contains(&break_label)); + assert!(result.continues.contains(&continue_label)); + } + + #[test] + fn join_allows_fallthrough_when_either_branch_falls_through() { + let label = LabelId::new("'jb"); + let break_flow = ControlFlow::break_to(label.clone()); + let fallthrough = ControlFlow::fallthrough(); + + let result = fallthrough.join(&break_flow); + + assert!(result.can_fall_through); + assert!(result.breaks.contains(&label)); + assert!(result.continues.is_empty()); + } + + #[test] + fn matching_break_exits_block() { + let break_label = LabelId::new("'bl"); + let break_flow = ControlFlow::break_to(break_label.clone()); + + let result = break_flow.exit_block(Some(&break_label)); + + assert!(result.can_fall_through); + assert!(result.breaks.is_empty()); + assert!(result.continues.is_empty()); + } + + #[test] + fn continues_propagate_through_block() { + let block_label = LabelId::new("'inner"); + let continue_label = LabelId::new("'outer"); + let continue_flow = ControlFlow::continue_to(continue_label.clone()); + + let result = continue_flow.exit_block(Some(&block_label)); + + assert!(!result.can_fall_through); + assert!(result.breaks.is_empty()); + assert!(result.continues.contains(&continue_label)); + } + + #[test] + fn matching_break_does_exit_loop() { + let break_label = LabelId::new("'bl"); + let break_flow = ControlFlow::break_to(break_label.clone()); + + let result = break_flow.exit_loop(Some(&break_label)); + + assert!(result.can_fall_through); + assert!(result.breaks.is_empty()); + assert!(result.continues.is_empty()); + } + + #[test] + fn matching_continue_does_not_exit_loop() { + let loop_label = LabelId::new("'inner"); + let continue_flow = ControlFlow::continue_to(loop_label.clone()); + + let result = continue_flow.exit_loop(Some(&loop_label)); + + assert!(!result.can_fall_through); + assert!(result.breaks.is_empty()); + assert!(result.continues.is_empty()); + } + + #[test] + fn non_matching_break_propagates_through_blocks() { + let block_label = LabelId::new("'inner"); + let break_label = LabelId::new("'outer"); + let break_flow = ControlFlow::break_to(break_label.clone()); + + let result = break_flow.exit_block(Some(&block_label)); + + assert!(!result.can_fall_through); + assert!(result.breaks.contains(&break_label)); + assert!(result.continues.is_empty()); + } + + #[test] + fn body_fallthrough_does_not_exit_loop() { + let block_label = LabelId::new("'loop"); + let fallthrough = ControlFlow::fallthrough(); + + let result = fallthrough.exit_loop(Some(&block_label)); + + assert!(!result.can_fall_through); + assert!(result.breaks.is_empty()); + assert!(result.continues.is_empty()); + } + + #[test] + fn break_targeting_outer_label_propagates_through_inner_loop() { + let loop_label = LabelId::new("'inner"); + let break_label = LabelId::new("'outer"); + let break_flow = ControlFlow::break_to(break_label.clone()); + + let result = break_flow.exit_loop(Some(&loop_label)); + + assert!(!result.can_fall_through); + assert!(result.breaks.contains(&break_label)); + assert!(result.continues.is_empty()); + } + + #[test] + fn continues_targeting_outer_label_propagates_through_inner_loop() { + let loop_label = LabelId::new("'inner"); + let continue_label = LabelId::new("'outer"); + let continue_flow = ControlFlow::continue_to(continue_label.clone()); + + let result = continue_flow.exit_loop(Some(&loop_label)); + + assert!(!result.can_fall_through); + assert!(result.breaks.is_empty()); + assert!(result.continues.contains(&continue_label)); + } + + #[test] + fn return_statement_does_not_fall_through() { + let stmt = Stmt::Return { + expr: crate::grammar::expr::Expr::True, + }; + + let (flow, _) = control_flow_stmt(stmt).into_singleton().expect("return statement should produce one control flow"); + + assert!(!flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } + + #[test] + fn break_statement_records_its_target() { + let label = LabelId::new("'block"); + let stmt = Stmt::Break { + label: label.clone() + }; + + let (flow, _) = control_flow_stmt(stmt).into_singleton().expect("break statement should produce one control flow"); + + assert!(!flow.can_fall_through); + assert_eq!(flow.breaks.len(), 1); + assert!(flow.breaks.contains(&label)); + assert!(flow.continues.is_empty()); + } + + #[test] + fn continue_statement_records_its_target() { + let label = LabelId::new("'block"); + let stmt = Stmt::Continue { + label: label.clone(), + }; + + let (flow, _) = control_flow_stmt(stmt).into_singleton().expect("continue statement should produce one control flow"); + + assert!(!flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert_eq!(flow.continues.len(), 1); + assert!(flow.continues.contains(&label)); + } +} From b17942af13ab0265ce379b06ea5f6d09e26e18b6 Mon Sep 17 00:00:00 2001 From: Awesome Rustacean Date: Thu, 6 Aug 2026 23:01:49 +0300 Subject: [PATCH 3/8] feat: handle fallthrough statements in return analysis - classify expression, print, and let statements as fallthrough - add focused tests for each statement outcome --- .../formality-rust/src/check/return_check.rs | 109 ++++++++++++++---- 1 file changed, 88 insertions(+), 21 deletions(-) diff --git a/crates/formality-rust/src/check/return_check.rs b/crates/formality-rust/src/check/return_check.rs index 88fb9421a..b009b221d 100644 --- a/crates/formality-rust/src/check/return_check.rs +++ b/crates/formality-rust/src/check/return_check.rs @@ -151,7 +151,7 @@ judgment_fn! { ( (let flow = ControlFlow::returns()) --- ("return") - (control_flow_stmt(Stmt::Return {expr: _ }) => flow) + (control_flow_stmt(Stmt::Return { expr: _ }) => flow) ) ( @@ -165,6 +165,24 @@ judgment_fn! { --- ("continue") (control_flow_stmt(Stmt::Continue { label }) => flow) ) + + ( + (let flow = ControlFlow::fallthrough()) + --- ("expression") + (control_flow_stmt(Stmt::Expr { expr: _ }) => flow) + ) + + ( + (let flow = ControlFlow::fallthrough()) + --- ("print") + (control_flow_stmt(Stmt::Print { expr: _ }) => flow) + ) + + ( + (let flow = ControlFlow::fallthrough()) + --- ("let") + (control_flow_stmt(Stmt::Let { label: _, id: _, ty: _, init: _ }) => flow) + ) } } @@ -342,40 +360,89 @@ mod tests { expr: crate::grammar::expr::Expr::True, }; - let (flow, _) = control_flow_stmt(stmt).into_singleton().expect("return statement should produce one control flow"); + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("return statement should produce one control flow"); assert!(!flow.can_fall_through); assert!(flow.breaks.is_empty()); assert!(flow.continues.is_empty()); } - + #[test] fn break_statement_records_its_target() { - let label = LabelId::new("'block"); - let stmt = Stmt::Break { - label: label.clone() - }; + let label = LabelId::new("'block"); + let stmt = Stmt::Break { + label: label.clone(), + }; - let (flow, _) = control_flow_stmt(stmt).into_singleton().expect("break statement should produce one control flow"); + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("break statement should produce one control flow"); - assert!(!flow.can_fall_through); - assert_eq!(flow.breaks.len(), 1); - assert!(flow.breaks.contains(&label)); - assert!(flow.continues.is_empty()); + assert!(!flow.can_fall_through); + assert_eq!(flow.breaks.len(), 1); + assert!(flow.breaks.contains(&label)); + assert!(flow.continues.is_empty()); } #[test] fn continue_statement_records_its_target() { - let label = LabelId::new("'block"); - let stmt = Stmt::Continue { - label: label.clone(), - }; + let label = LabelId::new("'block"); + let stmt = Stmt::Continue { + label: label.clone(), + }; - let (flow, _) = control_flow_stmt(stmt).into_singleton().expect("continue statement should produce one control flow"); + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("continue statement should produce one control flow"); + + assert!(!flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert_eq!(flow.continues.len(), 1); + assert!(flow.continues.contains(&label)); + } - assert!(!flow.can_fall_through); - assert!(flow.breaks.is_empty()); - assert_eq!(flow.continues.len(), 1); - assert!(flow.continues.contains(&label)); + #[test] + fn expression_statement_can_fall_through() { + let stmt = Stmt::Expr { + expr: crate::grammar::expr::Expr::True, + }; + + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("expression statements should produce one control-flow result"); + + assert!(flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } + + #[test] + fn print_statement_can_fall_through() { + let stmt = Stmt::Print { + expr: crate::grammar::expr::Expr::True, + }; + + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("print statements should produce one control-flow result"); + + assert!(flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } + + #[test] + fn let_statement_can_fall_through() { + let stmt: Stmt = crate::rust::term("let x: bool;"); + + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("let statements should produce one control-flow result"); + + assert!(flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); } } From b172fdd6f4597b47be4c81c5f19108dd541db5c7 Mon Sep 17 00:00:00 2001 From: Awesome Rustacean Date: Fri, 7 Aug 2026 01:29:22 +0300 Subject: [PATCH 4/8] feat: analyze control flow through compound statements Propagate fallthrough, break, and continue information through blocks, conditionals, loops, and existential blocks. Add tests covering block sequencing, branch joins, loop exists, nested control flow, and ignoring unreachable control-flow transfers. --- .../formality-rust/src/check/return_check.rs | 236 ++++++++++++++++-- 1 file changed, 209 insertions(+), 27 deletions(-) diff --git a/crates/formality-rust/src/check/return_check.rs b/crates/formality-rust/src/check/return_check.rs index b009b221d..4c6e05341 100644 --- a/crates/formality-rust/src/check/return_check.rs +++ b/crates/formality-rust/src/check/return_check.rs @@ -5,7 +5,6 @@ use crate::grammar::{ }; use formality_core::{judgment_fn, term, Set}; -/// Computes the control flow that can emerge from a statement. #[term] struct ControlFlow { can_fall_through: bool, @@ -130,65 +129,100 @@ impl ControlFlow { // } // } -// judgment_fn! { -// /// This answers the question: "What control flow can emerge from this block?". -// fn control_flow_block( -// block: Block) => ControlFlow { -// debug(block) +judgment_fn! { + /// Computes the control flow that can emerge from a block. + fn control_flow_block( + block: Block) => ControlFlow { + debug(block) -// ( -// // Rules goes here. -// ) -// } -// } + ( + (let flow = ControlFlow::fallthrough()) + (for_all(i in 0..stmts.len()) with(flow) + (control_flow_stmt(&stmts[i]) => statement_flow) + (let flow = flow.then(&statement_flow))) + (let flow = flow.exit_block(label.as_ref().map(|label| &label.id))) + ----------------------------------------------------- ("block") + (control_flow_block(Block { label, stmts }) => flow) + ) + } +} judgment_fn! { - /// This answers the question: "What control flow can emerge from this one statement.?" + /// Computes the control flow that can emerge from a statement. fn control_flow_stmt( stmt: Stmt) => ControlFlow { debug(stmt) ( (let flow = ControlFlow::returns()) - --- ("return") + ----------------------------------------------------- ("return") (control_flow_stmt(Stmt::Return { expr: _ }) => flow) ) ( (let flow = ControlFlow::break_to(label.clone())) - --- ("break") + ----------------------------------------------------- ("break") (control_flow_stmt(Stmt::Break { label }) => flow) ) ( (let flow = ControlFlow::continue_to(label.clone())) - --- ("continue") + ----------------------------------------------------- ("continue") (control_flow_stmt(Stmt::Continue { label }) => flow) ) ( (let flow = ControlFlow::fallthrough()) - --- ("expression") + ----------------------------------------------------- ("expression") (control_flow_stmt(Stmt::Expr { expr: _ }) => flow) ) ( (let flow = ControlFlow::fallthrough()) - --- ("print") + ----------------------------------------------------- ("print") (control_flow_stmt(Stmt::Print { expr: _ }) => flow) ) ( (let flow = ControlFlow::fallthrough()) - --- ("let") + ----------------------------------------------------- ("let") (control_flow_stmt(Stmt::Let { label: _, id: _, ty: _, init: _ }) => flow) ) + + ( + (control_flow_block(block) => flow) + ----------------------------------------------------- ("block") + (control_flow_stmt(Stmt::Block(block)) => flow) + ) + + ( + (control_flow_block(then_block) => then_flow) + (control_flow_block(&else_block.block) => else_flow) + (let flow = then_flow.join(else_flow)) + ----------------------------------------------------- ("if") + (control_flow_stmt(Stmt::If { condition: _, then_block, else_block }) => flow) + ) + + ( + (control_flow_block(body) => body_flow) + (let flow = body_flow.exit_loop(label.as_ref().map(|label| &label.id))) + ----------------------------------------------------- ("loop") + (control_flow_stmt(Stmt::Loop { label, body}) => flow) + ) + + ( + (let block = binder.peek()) + (control_flow_block(block) => flow) + ----------------------------------------------------- ("exists") + (control_flow_stmt(Stmt::Exists { binder }) => flow) + ) } } #[cfg(test)] mod tests { use super::*; + use crate::grammar::expr::Expr; #[test] fn then_ignores_unreachable_breaks() { @@ -356,9 +390,7 @@ mod tests { #[test] fn return_statement_does_not_fall_through() { - let stmt = Stmt::Return { - expr: crate::grammar::expr::Expr::True, - }; + let stmt = Stmt::Return { expr: Expr::True }; let (flow, _) = control_flow_stmt(stmt) .into_singleton() @@ -405,9 +437,7 @@ mod tests { #[test] fn expression_statement_can_fall_through() { - let stmt = Stmt::Expr { - expr: crate::grammar::expr::Expr::True, - }; + let stmt = Stmt::Expr { expr: Expr::True }; let (flow, _) = control_flow_stmt(stmt) .into_singleton() @@ -420,9 +450,7 @@ mod tests { #[test] fn print_statement_can_fall_through() { - let stmt = Stmt::Print { - expr: crate::grammar::expr::Expr::True, - }; + let stmt = Stmt::Print { expr: Expr::True }; let (flow, _) = control_flow_stmt(stmt) .into_singleton() @@ -445,4 +473,158 @@ mod tests { assert!(flow.breaks.is_empty()); assert!(flow.continues.is_empty()); } + + #[test] + fn empty_block_can_fall_through() { + let (flow, _) = control_flow_block(Block::empty()) + .into_singleton() + .expect("empty block should produce one control-flow result"); + + assert!(flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } + + #[test] + fn return_after_fall_through_prevents_block_fall_through() { + let block = Block { + label: None, + stmts: vec![ + Stmt::Expr { expr: Expr::True }, + Stmt::Return { expr: Expr::True }, + Stmt::Break { + label: LabelId::new("'test"), + }, + ], + }; + + let (flow, _) = control_flow_block(block) + .into_singleton() + .expect("block should produce one control-flow result"); + + assert!(!flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } + + #[test] + fn matching_break_makes_labeled_block_fall_through() { + let block: Block = crate::rust::term( + "'block: { + break 'block; + }", + ); + + let (flow, _) = control_flow_block(block) + .into_singleton() + .expect("labeled block should produce one control-flow result"); + + assert!(flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } + + #[test] + fn nested_block_propagates_return_flow() { + let stmt = Stmt::Block(Block { + label: None, + stmts: vec![Stmt::Return { expr: Expr::True }], + }); + + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("nested block should produce one control-flow result"); + + assert!(!flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } + + #[test] + fn if_with_two_returning_branches_does_not_fall_through() { + let stmt: Stmt = crate::rust::term( + " if true { + return true; + } else { + return false; + } + ", + ); + + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("if statement should produce one control-flow result"); + + assert!(!flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } + + #[test] + fn if_without_an_else_branch_fall_through() { + let stmt: Stmt = crate::rust::term( + "if true { + return true; + }", + ); + + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("if statement should produce one control-flow result"); + + assert!(flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } + + #[test] + fn loop_with_fallthrough_body_does_not_fall_through() { + let stmt: Stmt = crate::rust::term( + "loop { + true; + }", + ); + + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("loop statement should produce one control-flow result"); + + assert!(!flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } + + #[test] + fn matching_break_makes_loop_fall_through() { + let stmt: Stmt = crate::rust::term( + "'outer: loop { + break 'outer; + }", + ); + + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("loop statement should produce one control-flow result"); + + assert!(flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } + + #[test] + fn exists_statement_propagates_inner_return() { + let stmt: Stmt = crate::rust::term( + "exists<'r> { + return true; + }", + ); + + let (flow, _) = control_flow_stmt(stmt) + .into_singleton() + .expect("exists statement should produce one control-flow result"); + + assert!(!flow.can_fall_through); + assert!(flow.breaks.is_empty()); + assert!(flow.continues.is_empty()); + } } From d69ffd5563c1570393b629bf414bd19032461d51 Mon Sep 17 00:00:00 2001 From: Awesome Rustacean Date: Fri, 7 Aug 2026 02:57:55 +0300 Subject: [PATCH 5/8] feat: validate function returns on all paths Add a return-check judgment that permits unit functions to fall through and rejects non-unit functions when any path reaches the end of the body. Run return validation before borrow checking and add coverage for accepted and rejected function bodies. --- crates/formality-rust/src/check/fns.rs | 2 + .../formality-rust/src/check/return_check.rs | 89 +++++++++++++------ 2 files changed, 62 insertions(+), 29 deletions(-) diff --git a/crates/formality-rust/src/check/fns.rs b/crates/formality-rust/src/check/fns.rs index a790c7e91..9c015634e 100644 --- a/crates/formality-rust/src/check/fns.rs +++ b/crates/formality-rust/src/check/fns.rs @@ -2,6 +2,7 @@ use crate::check::borrow_check::env::TypeckEnv; use crate::check::borrow_check::flow_state::FlowState; use crate::check::borrow_check::nll::borrow_check; use crate::check::prove_goal; +use crate::check::return_check::check_fn_returns; use crate::check::where_clauses::prove_where_clauses_well_formed; use crate::grammar::{CrateId, FnBody, MaybeFnBody, Relation, Wcs}; use crate::prove::{Env, Program}; @@ -84,6 +85,7 @@ judgment_fn! { ) ( + (check_fn_returns(output_ty, block) => ()) // Type-check an expression body via the borrow checker. (let typeck_env = TypeckEnv::for_fn_body(env, program, output_ty)) (let initial_state = FlowState::for_fn_body(env, input_args)?) diff --git a/crates/formality-rust/src/check/return_check.rs b/crates/formality-rust/src/check/return_check.rs index 4c6e05341..0511c61e3 100644 --- a/crates/formality-rust/src/check/return_check.rs +++ b/crates/formality-rust/src/check/return_check.rs @@ -1,8 +1,11 @@ #![allow(unused)] +use crate::grammar::Fallible; use crate::grammar::{ expr::{Block, LabelId, Stmt}, Ty, }; +use anyhow::bail; +use formality_core::judgment::ProofTree; use formality_core::{judgment_fn, term, Set}; #[term] @@ -103,36 +106,38 @@ impl ControlFlow { } } -// judgment_fn! { -// /// Entry point: This answers the question: "Is this function allowed to end?". -// pub(crate) fn check_fn_returns( -// output_ty: Ty, -// block: Block) => () { -// debug(output_ty, block) - -// ( -// // Rules goes here. -// // 1. Unit returning function -// // -// // (output_ty == ()) -// // ---------------------- ("unit return") -// // (check_fn_returns(output_ty, block) => ()) -// // -// // 2. Non-unit returning functions. -// // -// // (output_ty != ()) -// // (control_flow_block(block) => flow) -// // -------------------- ("non-unit returns") -// // (check_fn_returns(output_ty, block) => ()) -// // -// ) -// } -// } +fn check_no_fallthrough(flow: &ControlFlow) -> Fallible { + if flow.can_fall_through { + bail!("function may not return a value"); + } + + Ok(ProofTree::leaf("function does not fall through")) +} + +judgment_fn! { + /// Checks whether every required path through a function returns a value. + pub(crate) fn check_fn_returns( output_ty: Ty, block: Block) => () { + debug(output_ty, block) + + ( + (if output_ty == &Ty::unit()) + ---------------------------------------------------- ("unit") + (check_fn_returns(output_ty, block) => ()) + ) + + ( + (if output_ty != &Ty::unit()) + (control_flow_block(block) => flow) + (check_no_fallthrough(flow) => ()) + ---------------------------------------------------- ("non-unit return") + (check_fn_returns(output_ty, block) => ()) + ) + } +} judgment_fn! { /// Computes the control flow that can emerge from a block. - fn control_flow_block( - block: Block) => ControlFlow { + fn control_flow_block( block: Block) => ControlFlow { debug(block) ( @@ -149,8 +154,7 @@ judgment_fn! { judgment_fn! { /// Computes the control flow that can emerge from a statement. - fn control_flow_stmt( - stmt: Stmt) => ControlFlow { + fn control_flow_stmt( stmt: Stmt) => ControlFlow { debug(stmt) ( @@ -627,4 +631,31 @@ mod tests { assert!(flow.breaks.is_empty()); assert!(flow.continues.is_empty()); } + + #[test] + fn unit_returning_function_may_fall_through() { + check_fn_returns(Ty::unit(), Block::empty()) + .into_singleton() + .expect("unit-returning functions should be allowed to fall through"); + } + + #[test] + fn non_unit_function_with_return_is_accepted() { + let block: Block = crate::rust::term( + " { + return true; + }", + ); + + check_fn_returns(Ty::bool(), block) + .into_singleton() + .expect("non-unit returning functions should not be allowed to fall through"); + } + + #[test] + fn non_unit_function_that_can_fall_through_is_rejected() { + check_fn_returns(Ty::bool(), Block::empty()) + .into_singleton() + .expect_err("non-unit returning function that can fall through should be rejected."); + } } From e04811eae1c5b6e9b6d4007510cf6f34e2d5439b Mon Sep 17 00:00:00 2001 From: Awesome Rustacean Date: Fri, 7 Aug 2026 03:51:53 +0300 Subject: [PATCH 6/8] refactor: remove return tracking from borrow checker Use the dedicated return-validation pass to detect function fallthrough instead of tracking divergence in borrow-checker flow state. Update return-validation diagnostics and add integration coverage for branches, loops, labels, continues, and existential blocks. --- .../src/check/borrow_check/flow_state.rs | 44 ++++-------- .../src/check/borrow_check/nll.rs | 36 ++-------- tests/borrowck.rs | 16 ++--- tests/mir_typeck.rs | 4 +- tests/return_validation.rs | 72 +++++++++++++++---- 5 files changed, 87 insertions(+), 85 deletions(-) diff --git a/crates/formality-rust/src/check/borrow_check/flow_state.rs b/crates/formality-rust/src/check/borrow_check/flow_state.rs index 0c68e0a25..9f24e44b9 100644 --- a/crates/formality-rust/src/check/borrow_check/flow_state.rs +++ b/crates/formality-rust/src/check/borrow_check/flow_state.rs @@ -145,7 +145,6 @@ where let Union((a, b)) = term; let a: FlowState = a.upcast(); let b: FlowState = b.upcast(); - let diverged = a.diverged && b.diverged; // At join points, locals (for name resolution) must be identical on both sides. // Only drop_locals may differ (due to `let 'a: x = ...` in one branch). @@ -165,8 +164,6 @@ where continues: Union((a.continues, b.continues)).upcast(), all_outlives: Union((a.all_outlives, b.all_outlives)).upcast(), scopes, - // A join point is unreachable only if both incoming edges are. - diverged, } } } @@ -199,9 +196,6 @@ pub struct FlowState { pub continues: Set, pub all_outlives: Set, - - /// If true, this program point is unreachable (all paths returned, broke, or continued). - pub diverged: bool, } impl FlowState { @@ -231,15 +225,20 @@ impl FlowState { pub fn with_loan(&self, loan: Loan) -> Self { Self { current: self.current.with_loan(loan), - ..self.clone() + breaks: self.breaks.clone(), + continues: self.continues.clone(), + scopes: self.scopes.clone(), + all_outlives: self.all_outlives.clone(), } } pub fn with_outlives(&self, outlives: &Set) -> Self { Self { current: self.current.with_outlives(outlives), + breaks: self.breaks.clone(), + continues: self.continues.clone(), + scopes: self.scopes.clone(), all_outlives: Union((&self.all_outlives, outlives)).upcast(), - ..self.clone() } } @@ -262,30 +261,25 @@ impl FlowState { pub fn diverges(&self) -> Self { Self { current: PointFlowState::default(), - diverged: true, ..self.clone() } } pub fn with_break(&self, label: &LabelId) -> Self { let mut this = self.clone(); - if !this.diverged { - this.breaks.insert(LabeledFlowState { - label: label.clone(), - state: this.current.clone(), - }); - } + this.breaks.insert(LabeledFlowState { + label: label.clone(), + state: this.current.clone(), + }); this } pub fn with_continue(&self, label: &LabelId) -> Self { let mut this = self.clone(); - if !this.diverged { - this.continues.insert(LabeledFlowState { - label: label.clone(), - state: this.current.clone(), - }); - } + this.continues.insert(LabeledFlowState { + label: label.clone(), + state: this.current.clone(), + }); this } @@ -479,7 +473,6 @@ impl FlowState { breaks, continues, all_outlives, - diverged, } = self.clone(); // Pop and destructure the top scope. @@ -508,8 +501,6 @@ impl FlowState { .into_iter() .partition(|lfs| Some(&lfs.label) == scope_label.as_ref()); let mut successor = current; - // A break targeting this scope is live control arriving after it. - let diverged = diverged && this_label.is_empty(); for lfs in this_label { successor = Union((successor, lfs.state)).upcast(); } @@ -525,7 +516,6 @@ impl FlowState { breaks: other_labels, continues, all_outlives, - diverged, } } @@ -540,7 +530,6 @@ impl FlowState { breaks, continues, all_outlives, - diverged, } = self.clone(); let (this_label, other_labels): (Set, Set) = @@ -556,7 +545,6 @@ impl FlowState { breaks, continues: other_labels, all_outlives, - diverged, } } @@ -643,8 +631,6 @@ impl FlowState { breaks: self.breaks.clone(), continues: self.continues.clone(), all_outlives, - // The rerun starts from the entry state, so it inherits its reachability. - diverged: self.diverged, } } } diff --git a/crates/formality-rust/src/check/borrow_check/nll.rs b/crates/formality-rust/src/check/borrow_check/nll.rs index 1c5cab683..ccb465716 100644 --- a/crates/formality-rust/src/check/borrow_check/nll.rs +++ b/crates/formality-rust/src/check/borrow_check/nll.rs @@ -135,9 +135,7 @@ judgment_fn! { debug(assumptions, env, state, block) ( - (borrow_check_block(env, assumptions, state, block, LivePlaces::default()) => state) - (for_all(output_ty in env.output_ty.iter()) - (fall_through_permitted(env, assumptions, state, output_ty) => ())) + (borrow_check_block(env, assumptions, state, block, LivePlaces::default()) => _state) ------------------------------------------------------------ ("borrow_check") (borrow_check(env, assumptions, state, block) => ()) ) @@ -247,8 +245,6 @@ judgment_fn! { (let continue_live = Stmt::loop_(label, body).live_before(&env, &state, places_live_on_exit)) (let state = state.push_continue_scope(&env.env, label, places_live_on_exit, continue_live)?) (borrow_check_loop(env, assumptions, state, body, places_live_on_exit) => state) - // The loop exit is reachable only via `break` (revived in `pop_scope`). - (let state = state.diverges()) (let state = state.pop_scope(label)) ------------------------------------------------------------ ("loop") (borrow_check_statement(env, assumptions, state, Stmt::Loop { label, body }, places_live_on_exit) => (env, state)) @@ -768,8 +764,11 @@ fn kill_loans(overwritten_place: &TypedPlaceExpr, state: &FlowState) -> FlowStat .retain(|loan| !overwritten_place.is_prefix_of(&loan.place)); FlowState { + scopes: state.scopes.clone(), current, - ..state.clone() + breaks: state.breaks.clone(), + continues: state.continues.clone(), + all_outlives: state.all_outlives.clone(), } } @@ -1065,31 +1064,6 @@ judgment_fn! { } } -judgment_fn! { - /// Control that falls off the end of a fn body implicitly returns `()`; - /// permitted if the end is unreachable or `()` is assignable to the declared output type. - fn fall_through_permitted( - env: TypeckEnv, - assumptions: Wcs, - state: FlowState, - output_ty: Ty, - ) => () { - debug(state, output_ty, assumptions, env) - ( - (if state.diverged)! - ------------------------------------------------------------- ("end of body unreachable") - (fall_through_permitted(_env, _assumptions, state, _output_ty) => ()) - ) - - ( - (if !state.diverged) - (prove_assignable(env, assumptions, state, Ty::unit(), output_ty) => _state) - -------------------------------------------------------------- ("implicit unit return") - (fall_through_permitted(_env, _assumptions, state, output_ty) => ()) - ) - } -} - judgment_fn! { /// Prove that `a` is assignable to `b`. fn prove_assignable( diff --git a/tests/borrowck.rs b/tests/borrowck.rs index 3dc3f42f1..d1076ca34 100644 --- a/tests/borrowck.rs +++ b/tests/borrowck.rs @@ -4047,8 +4047,8 @@ fn issue_57165_conditional() { .err(expect_test::expect![[r#" the rule "fixed-point" at (nll.rs) failed because condition evaluated to false: `state0 == state1` - state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)}, false) - state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, false) + state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)}) + state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}) the rule "borrow of disjoint places" at (nll.rs) failed because condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` @@ -4094,8 +4094,8 @@ fn issue_57165_conditional() { .err(expect_test::expect![[r#" the rule "fixed-point" at (nll.rs) failed because condition evaluated to false: `state0 == state1` - state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)}, false) - state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, false) + state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)}) + state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}) the rule "borrow of disjoint places" at (nll.rs) failed because condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` @@ -4446,8 +4446,8 @@ fn issue_46859_decoder_next() { .err(expect_test::expect![[r#" the rule "fixed-point" at (nll.rs) failed because condition evaluated to false: `state0 == state1` - state0 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, false) - state1 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, false) + state0 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}) + state1 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}) the rule "borrow of disjoint places" at (nll.rs) failed because condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` @@ -4588,8 +4588,8 @@ fn issue_92985_filtering_lending_iterator() { .err(expect_test::expect![[r#" the rule "fixed-point" at (nll.rs) failed because condition evaluated to false: `state0 == state1` - state0 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, false) - state1 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, false) + state0 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}) + state1 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}) the rule "borrow of disjoint places" at (nll.rs) failed because condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` diff --git a/tests/mir_typeck.rs b/tests/mir_typeck.rs index c85a7f29b..e6753ceca 100644 --- a/tests/mir_typeck.rs +++ b/tests/mir_typeck.rs @@ -819,7 +819,7 @@ fn test_field_projection_root_non_adt() { "#]]) .err(expect_test::expect![[r#" the rule "struct field" at (nll.rs) failed because - pattern `(RigidTy { name: RigidName::AdtId(adt_id), parameters }, state)` did not match value `(u32, flow_state([scope(none, None, {}, None, [(v1, u32)], [v1 : u32]), scope(none, None, {}, None, [(v2, Dummy)], [v2 : Dummy])], point_flow_state({}, {}, {}), {}, {}, {}, false))`"#]]) + pattern `(RigidTy { name: RigidName::AdtId(adt_id), parameters }, state)` did not match value `(u32, flow_state([scope(none, None, {}, None, [(v1, u32)], [v1 : u32]), scope(none, None, {}, None, [(v2, Dummy)], [v2 : Dummy])], point_flow_state({}, {}, {}), {}, {}, {}))`"#]]) } /// Test the behaviour of initialising the struct with wrong type. @@ -1020,7 +1020,7 @@ fn test_break_nonexistent_label() { .err(expect_test::expect![[r#" crates/formality-rust/src/check/borrow_check/nll.rs:177:1: no applicable rules for borrow_check_statement { state: flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(none, None, {}, Some({}), [], []), scope(none, None, {}, None, [], [])], point_flow_state({}, {}, {}), {}, {}, {}), statement: break 'nonexistent ;, places_live_on_exit: {}, assumptions: {}, env: TypeckEnv { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: Some(u32) } } - crates/formality-rust/src/check/borrow_check/nll.rs:179:1: no applicable rules for borrow_check_statement { state: flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(none, None, {}, Some({}), [], []), scope(none, None, {}, None, [], [])], point_flow_state({}, {}, {}), {}, {}, {}, false), statement: break 'nonexistent ;, places_live_on_exit: {}, assumptions: {}, env: TypeckEnv { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: Some(u32) } }"#]]) + crates/formality-rust/src/check/borrow_check/nll.rs:177:1: no applicable rules for borrow_check_statement { state: flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(none, None, {}, Some({}), [], []), scope(none, None, {}, None, [], [])], point_flow_state({}, {}, {}), {}, {}, {}), statement: break 'nonexistent ;, places_live_on_exit: {}, assumptions: {}, env: TypeckEnv { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: Some(u32) } }"#]]) } /// `continue` targeting a valid loop label should pass. diff --git a/tests/return_validation.rs b/tests/return_validation.rs index bf9ebd18a..e034e737b 100644 --- a/tests/return_validation.rs +++ b/tests/return_validation.rs @@ -15,10 +15,7 @@ fn empty_body_non_unit_return() { fn foo() -> u32 { } }]) - .err(expect_test::expect![[r#" - crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: (), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } } - - crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } }"#]]) + .err(expect_test::expect![[r#"function may not return a value"#]]) } /// A function returning () with an empty body is fine — unit is implicit. @@ -65,10 +62,7 @@ fn if_else_one_branch_returns() { } } }]) - .err(expect_test::expect![[r#" - crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: (), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } } - - crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } }"#]]) + .err(expect_test::expect![[r#"function may not return a value"#]]) } /// An infinite loop never terminates, so it never needs to return. @@ -98,10 +92,7 @@ fn loop_with_break_no_return() { } } }]) - .err(expect_test::expect![[r#" - crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: (), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } } - - crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } }"#]]) + .err(expect_test::expect![[r#"function may not return a value"#]]) } /// A loop with break followed by a return is fine — all paths return. @@ -164,8 +155,59 @@ fn loop_with_conditional_break_can_fall_through() { } } }]) - .err(expect_test::expect![[r#" - crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: (), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } } + .err(expect_test::expect![[r#"function may not return a value"#]]) +} - crates/formality-rust/src/prove/prove_normalize.rs:20:1: no applicable rules for prove_normalize { p: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: true } }"#]]) +#[test] +fn if_without_else_is_rejected_for_non_unit_function() { + FormalityTest::new(crates![crate Foo { + fn foo(a: bool) -> u32 { + if a { + return 1_u32 + } + } + }]) + .err(expect_test::expect![[r#"function may not return a value"#]]) +} + +#[test] +fn loop_with_matching_continue_does_not_fall_through() { + FormalityTest::new(crates![crate Foo { + fn foo(a: bool) { + 'a: loop { + continue 'a; + } + } + }]) + .skip_execute() + .rustc_ok() + .ok(); +} + +/// A break targeting an outer block propagates through the inner loop +/// and makes execution continue after the outer block. +#[test] +fn break_targeting_outer_block_makes_fall_through() { + FormalityTest::new(crates![crate Foo { + fn foo() -> u32 { + 'outer { + 'inner: loop { + break 'outer; + } + } + } + }]) + .err(expect_test::expect![[r#"function may not return a value"#]]) +} + +#[test] +fn exists_with_return_is_accepted() { + FormalityTest::new(crates![crate Foo { + exists<'a> { + return 1_i32; + } + }]) + .skip_execute() + .rustc_ok() + .ok(); } From 5297bcbab5fbcd9d16bbdd17fe8f4c2d50d5d737 Mon Sep 17 00:00:00 2001 From: Awesome Rustacean Date: Fri, 7 Aug 2026 04:37:45 +0300 Subject: [PATCH 7/8] fix: update failing tests snapshots plus minor fixes. --- tests/return_validation.rs | 57 ++++++++++++++++++++++++++++++-------- 1 file changed, 45 insertions(+), 12 deletions(-) diff --git a/tests/return_validation.rs b/tests/return_validation.rs index e034e737b..814143d94 100644 --- a/tests/return_validation.rs +++ b/tests/return_validation.rs @@ -15,7 +15,12 @@ fn empty_body_non_unit_return() { fn foo() -> u32 { } }]) - .err(expect_test::expect![[r#"function may not return a value"#]]) + .err(expect_test::expect![[r#" + the rule "non-unit return" at (return_check.rs) failed because + function may not return a value + + the rule "unit" at (return_check.rs) failed because + condition evaluated to false: `output_ty == &Ty::unit()`"#]]) } /// A function returning () with an empty body is fine — unit is implicit. @@ -62,7 +67,12 @@ fn if_else_one_branch_returns() { } } }]) - .err(expect_test::expect![[r#"function may not return a value"#]]) + .err(expect_test::expect![[r#" + the rule "non-unit return" at (return_check.rs) failed because + function may not return a value + + the rule "unit" at (return_check.rs) failed because + condition evaluated to false: `output_ty == &Ty::unit()`"#]]) } /// An infinite loop never terminates, so it never needs to return. @@ -92,7 +102,12 @@ fn loop_with_break_no_return() { } } }]) - .err(expect_test::expect![[r#"function may not return a value"#]]) + .err(expect_test::expect![[r#" + the rule "non-unit return" at (return_check.rs) failed because + function may not return a value + + the rule "unit" at (return_check.rs) failed because + condition evaluated to false: `output_ty == &Ty::unit()`"#]]) } /// A loop with break followed by a return is fine — all paths return. @@ -155,7 +170,12 @@ fn loop_with_conditional_break_can_fall_through() { } } }]) - .err(expect_test::expect![[r#"function may not return a value"#]]) + .err(expect_test::expect![[r#" + the rule "non-unit return" at (return_check.rs) failed because + function may not return a value + + the rule "unit" at (return_check.rs) failed because + condition evaluated to false: `output_ty == &Ty::unit()`"#]]) } #[test] @@ -163,17 +183,22 @@ fn if_without_else_is_rejected_for_non_unit_function() { FormalityTest::new(crates![crate Foo { fn foo(a: bool) -> u32 { if a { - return 1_u32 + return 1_u32; } } }]) - .err(expect_test::expect![[r#"function may not return a value"#]]) + .err(expect_test::expect![[r#" + the rule "non-unit return" at (return_check.rs) failed because + function may not return a value + + the rule "unit" at (return_check.rs) failed because + condition evaluated to false: `output_ty == &Ty::unit()`"#]]) } #[test] fn loop_with_matching_continue_does_not_fall_through() { FormalityTest::new(crates![crate Foo { - fn foo(a: bool) { + fn foo(a: bool) -> u32 { 'a: loop { continue 'a; } @@ -190,22 +215,30 @@ fn loop_with_matching_continue_does_not_fall_through() { fn break_targeting_outer_block_makes_fall_through() { FormalityTest::new(crates![crate Foo { fn foo() -> u32 { - 'outer { + 'outer: { 'inner: loop { break 'outer; } } } }]) - .err(expect_test::expect![[r#"function may not return a value"#]]) + .err(expect_test::expect![[r#" + the rule "non-unit return" at (return_check.rs) failed because + function may not return a value + + the rule "unit" at (return_check.rs) failed because + condition evaluated to false: `output_ty == &Ty::unit()`"#]]) } #[test] fn exists_with_return_is_accepted() { FormalityTest::new(crates![crate Foo { - exists<'a> { - return 1_i32; - } + fn foo() -> i32 { + + exists<'a> { + return 1_i32; + } + } }]) .skip_execute() .rustc_ok() From 3d801025fc07c71c7772ea705837d440c64301a8 Mon Sep 17 00:00:00 2001 From: James Muriuki Date: Fri, 7 Aug 2026 16:19:50 +0300 Subject: [PATCH 8/8] Update return_check.rs Remove unused directive --- crates/formality-rust/src/check/return_check.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/crates/formality-rust/src/check/return_check.rs b/crates/formality-rust/src/check/return_check.rs index 0511c61e3..8923c8dcf 100644 --- a/crates/formality-rust/src/check/return_check.rs +++ b/crates/formality-rust/src/check/return_check.rs @@ -1,4 +1,3 @@ -#![allow(unused)] use crate::grammar::Fallible; use crate::grammar::{ expr::{Block, LabelId, Stmt},