fix: reject missing return values - #444
Conversation
|
Thanks for contributing to formality! :) |
| label: label.clone(), | ||
| state: this.current.clone(), | ||
| }); | ||
| if !this.diverged { |
There was a problem hiding this comment.
This is interesting. We could probably make a good borrow checker test here too, something like
let mut a = 1;
let mut b = 2;
let mut p = &a;
loop {
break;
p = &b;
break;
}
b += 1;
use(p);I think that before your changes, we would reject this -- but not after.
There was a problem hiding this comment.
I'm not sure if this is a good thing or bad that it has changed. But I'll rework the whole approach and preserve the desired behavior.
| label: label.clone(), | ||
| state: this.current.clone(), | ||
| }); | ||
| if !this.diverged { |
There was a problem hiding this comment.
we can make a similar test here, I didn't see any test for this
| .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(); |
There was a problem hiding this comment.
This condition doesn't seem quite right to me. For example
fn foo() {
let mut x = 1;
let mut y = 1;
let mut p = &x;
'b: {
'a: {
break 'b;
}
// I think we would conclude "diverged = false" here
p = &y;
}
y += 1; // ...and hence incorrectly report an error here
use(p);
}There was a problem hiding this comment.
This made me rethink the entire approach. Take a look and tell me whether it does still fail for this case. Happy to keep iterating.
This comment has been minimized.
This comment has been minimized.
Track divergent flow across branches and loops. Validate implicit `()` against fn output on fallthrough. fixes rust-lang#392.
|
This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
This comment has been minimized.
This comment has been minimized.
- 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.
- classify expression, print, and let statements as fallthrough - add focused tests for each statement outcome
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.
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.
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.
caad6e5 to
5297bcb
Compare
Remove unused directive
3 participants
What does this PR do?
closes #392
Adds return validation that rejects non-unit functions whose bodies can reach end without them returning a value.
How does it work, what questions do you have?
This PR introduces a control flow summary containing:
break.continueThe return checker sequentially analyzes statements and blocks:
then.join.For functions returning
(), falling through remains valid. For non-unit functions, validation succeeds only when the function body cannot reach its end. This includes functions where every reachable path returns, as well as loops that cannot exit.Q: Did this implementation halfway solve what this issue needs? #209
AI disclosure