-
Notifications
You must be signed in to change notification settings - Fork 1.6k
[red-knot] Combine terminal statement support with statically known branches #15817
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from 34 commits
02c4798
2c0d577
e198806
23b366d
38f3d99
5c1918a
7504fb7
ee6f253
6b53554
bb11cf8
a2ef702
1c42a2b
289c0c6
8b0899f
9cd8e68
1a80f81
f71325c
0e06012
b3b4577
46b1ec2
999188a
0f278da
0fb6a74
c882a95
33db6f1
b49916d
c80f27e
0d50385
c42490c
26f842b
e5b6c4a
00e236f
1d93650
ae83741
f13a6a6
7423de2
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -452,6 +452,9 @@ def raise_in_both_branches(cond: bool): | |
| # Exceptions can occur anywhere, so "before" and "raise" are valid possibilities | ||
| reveal_type(x) # revealed: Literal["before", "raise1", "raise2"] | ||
| else: | ||
| # This branch is unreachable, since all control flows in the `try` clause raise exceptions. | ||
| # As a result, this binding should never be reachable, since new bindings are visibile only | ||
| # when they are reachable. | ||
| x = "unreachable" | ||
| finally: | ||
| # Exceptions can occur anywhere, so "before" and "raise" are valid possibilities | ||
|
|
@@ -623,9 +626,9 @@ def return_from_nested_if(cond1: bool, cond2: bool): | |
|
|
||
| ## Statically known terminal statements | ||
|
|
||
| Terminal statements do not yet interact correctly with statically known bounds. In this example, we | ||
| should see that the `return` statement is always executed, and therefore that the `"b"` assignment | ||
| is not visible to the `reveal_type`. | ||
| We model reachability using the same visibility constraints that we use to model statically known | ||
| bounds. In this example, we see that the `return` statement is always executed, and therefore that | ||
| the `"b"` assignment is not visible to the `reveal_type`. | ||
|
|
||
| ```py | ||
| def _(cond: bool): | ||
|
|
@@ -635,6 +638,23 @@ def _(cond: bool): | |
| if True: | ||
| return | ||
|
|
||
| # TODO: Literal["a"] | ||
| reveal_type(x) # revealed: Literal["a", "b"] | ||
| reveal_type(x) # revealed: Literal["a"] | ||
dcreager marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| ``` | ||
|
|
||
| ## Bindings after a terminal statement are unreachable | ||
|
|
||
| Any bindings introduced after a terminal statement are unreachable, and are considered not visible. | ||
|
||
|
|
||
| ```py | ||
| def f(cond: bool) -> str: | ||
| x = "before" | ||
| if cond: | ||
| reveal_type(x) # revealed: Literal["before"] | ||
| return | ||
| x = "after-return" | ||
| # error: [unresolved-reference] | ||
| reveal_type(x) # revealed: Unknown | ||
| else: | ||
| x = "else" | ||
| reveal_type(x) # revealed: Literal["else"] | ||
| ``` | ||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -478,7 +478,6 @@ impl std::iter::FusedIterator for DeclarationsIterator<'_, '_> {} | |
| pub(super) struct FlowSnapshot { | ||
| symbol_states: IndexVec<ScopedSymbolId, SymbolState>, | ||
| scope_start_visibility: ScopedVisibilityConstraintId, | ||
| reachable: bool, | ||
| } | ||
|
|
||
| #[derive(Debug)] | ||
dcreager marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
@@ -506,8 +505,6 @@ pub(super) struct UseDefMapBuilder<'db> { | |
|
|
||
| /// Currently live bindings and declarations for each symbol. | ||
| symbol_states: IndexVec<ScopedSymbolId, SymbolState>, | ||
|
|
||
| reachable: bool, | ||
carljm marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| } | ||
|
|
||
| impl Default for UseDefMapBuilder<'_> { | ||
|
|
@@ -520,14 +517,13 @@ impl Default for UseDefMapBuilder<'_> { | |
| bindings_by_use: IndexVec::new(), | ||
| definitions_by_definition: FxHashMap::default(), | ||
| symbol_states: IndexVec::new(), | ||
| reachable: true, | ||
| } | ||
| } | ||
| } | ||
|
|
||
| impl<'db> UseDefMapBuilder<'db> { | ||
| pub(super) fn mark_unreachable(&mut self) { | ||
| self.reachable = false; | ||
| self.record_visibility_constraint(ScopedVisibilityConstraintId::ALWAYS_FALSE); | ||
| } | ||
|
|
||
| pub(super) fn add_symbol(&mut self, symbol: ScopedSymbolId) { | ||
|
|
@@ -544,7 +540,7 @@ impl<'db> UseDefMapBuilder<'db> { | |
| binding, | ||
| SymbolDefinitions::Declarations(symbol_state.declarations().clone()), | ||
| ); | ||
| symbol_state.record_binding(def_id); | ||
| symbol_state.record_binding(def_id, self.scope_start_visibility); | ||
carljm marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| } | ||
|
|
||
| pub(super) fn add_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId { | ||
|
|
@@ -596,7 +592,11 @@ impl<'db> UseDefMapBuilder<'db> { | |
| pub(super) fn simplify_visibility_constraints(&mut self, snapshot: FlowSnapshot) { | ||
| debug_assert!(self.symbol_states.len() >= snapshot.symbol_states.len()); | ||
|
|
||
| self.scope_start_visibility = snapshot.scope_start_visibility; | ||
| // If there are any control flow paths that have become unreachable between `snapshot` and | ||
| // now, then it's not valid to simplify any visibility constraints to `snapshot`. | ||
| if self.scope_start_visibility != snapshot.scope_start_visibility { | ||
| return; | ||
| } | ||
carljm marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| // Note that this loop terminates when we reach a symbol not present in the snapshot. | ||
| // This means we keep visibility constraints for all new symbols, which is intended, | ||
|
|
@@ -632,7 +632,7 @@ impl<'db> UseDefMapBuilder<'db> { | |
| let def_id = self.all_definitions.push(Some(definition)); | ||
| let symbol_state = &mut self.symbol_states[symbol]; | ||
| symbol_state.record_declaration(def_id); | ||
| symbol_state.record_binding(def_id); | ||
| symbol_state.record_binding(def_id, self.scope_start_visibility); | ||
| } | ||
|
|
||
| pub(super) fn record_use(&mut self, symbol: ScopedSymbolId, use_id: ScopedUseId) { | ||
|
|
@@ -649,7 +649,6 @@ impl<'db> UseDefMapBuilder<'db> { | |
| FlowSnapshot { | ||
| symbol_states: self.symbol_states.clone(), | ||
| scope_start_visibility: self.scope_start_visibility, | ||
| reachable: self.reachable, | ||
| } | ||
| } | ||
|
|
||
|
|
@@ -672,21 +671,23 @@ impl<'db> UseDefMapBuilder<'db> { | |
| num_symbols, | ||
| SymbolState::undefined(self.scope_start_visibility), | ||
| ); | ||
|
|
||
| self.reachable = snapshot.reachable; | ||
| } | ||
|
|
||
| /// Merge the given snapshot into the current state, reflecting that we might have taken either | ||
| /// path to get here. The new state for each symbol should include definitions from both the | ||
| /// prior state and the snapshot. | ||
| pub(super) fn merge(&mut self, snapshot: FlowSnapshot) { | ||
| // Unreachable snapshots should not be merged: If the current snapshot is unreachable, it | ||
| // should be completely overwritten by the snapshot we're merging in. If the other snapshot | ||
| // is unreachable, we should return without merging. | ||
| if !snapshot.reachable { | ||
| // As an optimization, if we know statically that either of the snapshots is always | ||
|
Member
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Commenting out these two
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. And I verified that we can indeed remove these checks and all tests pass! I'm not seeing a detectable performance improvement in the benchmark from including these lines; perhaps that just suggests conditional terminals aren't common enough for it to show up? It definitely seems like this should be faster in cases where it does apply.
Member
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
I think it might be that the merge step is now faster: if the other snapshot's reachability is To be clear, it's a hunch — I haven't backed any of ☝️ with data! |
||
| // unreachable, we can leave it out of the merged result entirely. Note that we cannot | ||
| // perform any type inference at this point, so this is largely limited to unreachability | ||
| // via terminal statements. If a flow's reachability depends on an expression in the code, | ||
| // we will include the flow in the merged result; the visibility constraints of its | ||
| // bindings will include this reachability condition, so that later during type inference, | ||
| // we can determine whether any particular binding is non-visible due to unreachability. | ||
| if snapshot.scope_start_visibility == ScopedVisibilityConstraintId::ALWAYS_FALSE { | ||
| return; | ||
| } | ||
| if !self.reachable { | ||
| if self.scope_start_visibility == ScopedVisibilityConstraintId::ALWAYS_FALSE { | ||
| self.restore(snapshot); | ||
| return; | ||
| } | ||
|
|
@@ -712,9 +713,6 @@ impl<'db> UseDefMapBuilder<'db> { | |
| self.scope_start_visibility = self | ||
| .visibility_constraints | ||
| .add_or_constraint(self.scope_start_visibility, snapshot.scope_start_visibility); | ||
|
|
||
| // Both of the snapshots are reachable, so the merged result is too. | ||
| self.reachable = true; | ||
| } | ||
|
|
||
| pub(super) fn finish(mut self) -> UseDefMap<'db> { | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The changes in this file are easier to see with "Hide whitespace"