Skip to content

[flow analysis] Rework demotion and type of interest promotion. #4370

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.

Sign up for GitHub

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

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
+103 −40
Open

[flow analysis] Rework demotion and type of interest promotion. #4370

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
f4ff6c8
[flow analysis] Rework demotion and type of interest promotion.
stereotype441 May 9, 2025
23bafd3
Address review comments
stereotype441 May 13, 2025
2647c82
Address further review comments
stereotype441 May 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
143 changes: 103 additions & 40 deletions resources/type-system/flow-analysis.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,14 @@ that assignment).
`b`.
- We use the notation `[...l, a]` where `l` is a list to denote a list
beginning with all the elements of `l` and followed by `a`.
- A list of types `p` is called a _promotion chain_ iff, for all `i < j`,
`p[i] <: p[j]`. _Note that since the subtyping relation is transitive, in
order to establish that `p` is a promotion chain, it is sufficient to check
the `p[i] <: p[j]` relation for each adjacent pair of types._
- A promotion chain `p` is said to be _valid for declared type `T`_ iff every
type in `p` is a subtype of `T`. _Note that since the subtyping relation is
transitive, in order to establish that `p` is valid for declared type `T`,
it is sufficient to check that the first type in `p` is a subtype of `T`._

- Stacks
- We use the notation `push(s, x)` to mean pushing `x` onto the top of the
Expand All @@ -123,18 +131,18 @@ that assignment).

### Models

A *variable model*, denoted `VariableModel(declaredType, promotedTypes,
A *variable model*, denoted `VariableModel(declaredType, promotionChain,
tested, assigned, unassigned, writeCaptured)`, represents what is statically
known to the flow analysis about the state of a variable at a given point in the
source code.

- `declaredType` is the type assigned to the variable at its declaration site
(either explicitly or by type inference).

- `promotedTypes` is a list of types that the variable has been promoted to,
with the final type in the list being the current promoted type of the
variable. Note that each type in the list must be a subtype of all previous
types, and of the declared type.
- `promotionChain` is the variable's promotion chain. This is a list of types
that the variable has been promoted to, with the final type in the list being
the current promoted type of the variable. It must always be a valid promotion
chain for declared type `declaredType`.

- `tested` is a set of types which are considered "of interest" for the purposes
of promotion, generally because the variable in question has been tested
Expand Down Expand Up @@ -397,8 +405,8 @@ We also make use of the following auxiliary functions:
Promotion policy is defined by the following operations on flow models.

We say that the **current type** of a variable `x` in variable model `VM` is `S` where:
- `VM = VariableModel(declared, promoted, tested, assigned, unassigned, captured)`
- `promoted = [...l, S]` or (`promoted = []` and `declared = S`)
- `VM = VariableModel(declared, promotionChain, tested, assigned, unassigned, captured)`
- `promotionChain = [...l, S]` or (`promotionChain = []` and `declared = S`)

Policy:
- We say that at type `T` is a type of interest for a variable `x` in a set of
Expand All @@ -407,46 +415,91 @@ Policy:

- We say that a variable `x` is promotable via type test with type `T` given
variable model `VM` if
- `VM = VariableModel(declared, promoted, tested, assigned, unassigned, captured)`
- `VM = VariableModel(declared, promotionChain, tested, assigned, unassigned, captured)`
- and `captured` is false
- and `S` is the current type of `x` in `VM`
- and not `S <: T`
- and `T <: S` or (`S` is `X extends R` and `T <: R`) or (`S` is `X & R` and
`T <: R`)

- We say that a variable `x` is promotable via assignment of an expression of
type `T` given variable model `VM` if
- `VM = VariableModel(declared, promoted, tested, assigned, unassigned, captured)`
- and `captured` is false
- and `S` is the current type of `x` in `VM`
- and `T <: S` and not `S <: T`
- and `T` is a type of interest for `x` in `tested`

- We say that a variable `x` is demotable via assignment of an expression of
type `T` given variable model `VM` if
- `VM = VariableModel(declared, promoted, tested, assigned, unassigned, captured)`
- and `captured` is false
- and [...promoted, declared] contains a type `S` such that `T` is `S` or
`T` is **NonNull(`S`)**.

Definitions:

- `demote(promotionChain, written)`, is a promotion chain obtained by deleting
any elements from `promotionChain` that do not satisfy `written <: T`. _In
effect, this removes any type promotions that are no longer valid after the
assignment of a value of type `written`._
- _Note that if `promotionChain` is valid for declared type `T`, it follows
that `demote(promotionChain, written)` is also valid for declared type `T`._

- `toi_promote(declared, promotionChain, tested, written)`, where `declared` and
`written` are types satisfying `written <: declared`, `promotionChain` is
valid for declared type `declared`, and all types `T` in `promotionChain`
satisfy `written <: T`, is the promotion chain `newPromotionChain`, defined as
follows. _("toi" stands for "type of interest".)_
- Let `provisionalType` be the last type in `promotionChain`, or `declared` if
`promotionChain` is empty. _(This is the type of the variable after
demotions, but before type of interest promotion.)_
- _Since the last type in a promotion chain is a subtype of all the others,
it follows that all types `T` in `promotionChain` satisfy `provisionalType
<: T`._
- If `written` and `provisionalType` are the same type, then
`newPromotionChain` is `promotionChain`. _(No type of interest promotion is
necessary in this case.)_
- Otherwise _(when `written` is not `provisionalType`)_, let `p1` be a set
containing the following types:
- **NonNull**(`declared`), if it is not the same as `declared`.
- For each type `T` in the `tested` list:
- `T`
- **NonNull**(`T`)

_The types in `p1` are known as the types of interest._
- Let `p2` be the set `p1 \ { provisionalType }` _(where `\` denotes set
difference)_.
- If the `written` type is in `p2`, and `written <: provisionalType`, then
`newPromotionChain` is `[...promotionChain, written]`. _Writing a value
whose static type is a type of interest promotes to that type._
- _By precondition, `written <: declared` and `written <: T` for all types
in `promotionChain`. Therefore, `newPromotionChain` satisfies the
definition of a promotion chain, and is valid for declared type
`declared`._
- Otherwise _(when `written` is not in `p2`)_:
- Let `p3` be the set of all types `T` in `p2` such that `written <: T <:
provisionalType`.
- If `p3` contains exactly one type `T` that is a subtype of all the others,
then `promoted` is `[...promotionChain, T]`. _Writing a value whose static
type is a subtype of a type of interest promotes to that type of interest,
provided there is a single "best" type of interest available to promote
to._
- _Since `T <: provisionalType <: declared`, and all types `U` in
`promotionChain` satisfy `provisionalType <: U`, it follows that all
types `U` in `promotionChain` satisfy `T <: U`. Therefore
`newPromotionChain` satisfies the definition of a promotion chain, and
is valid for declared type `declared`._
- Otherwise, `newPromotionChain` is `promotionChain`. _If there is no single
"best" type of interest to promote to, then no type of interest promotion
is done._

- `assign(x, E, M)` where `x` is a local variable, `E` is an expression of
inferred type `T`, and `M = FlowModel(r, VI)` is the flow model for `E` is
defined to be `FlowModel(r, VI[x -> VM])` where:
- `VI(x) = VariableModel(declared, promoted, tested, assigned, unassigned, captured)`
- if `captured` is true then:
- `VM = VariableModel(declared, promoted, tested, true, false, captured)`.
- otherwise if `x` is promotable via assignment of `E` given `VM`
- `VM = VariableModel(declared, [...promoted, T], tested, true, false,
captured)`.
- otherwise if `x` is demotable via assignment of `E` given `VM`
- `VM = VariableModel(declared, demoted, tested, true, false, captured)`.
- where `previous` is the prefix of `promoted` ending with the first type
`S` such that `T <: S`, and:
- if `S` is nullable and if `T <: Q` where `Q` is **NonNull(`S`)** then
`demoted` is `[...previous, Q]`
- otherwise `demoted` is `previous`
inferred type `T` (which must be a subtype of `x`'s declared type), and `M =
FlowModel(r, VI)` is the flow model for `E` is defined to be `FlowModel(r,
VI[x -> VM])` where:
- `VI(x) = VariableModel(declared, promoted, tested, assigned, unassigned,
captured)`
- If `captured` is true then:
- `VM = VariableModel(declared, promotionChain, tested, true, false, captured)`.
- Otherwise:
- Let `written = T`.
- Let `promotionChain' = demote(promotionChain, written)`.
- Let `promotionChain'' = toi_promote(declared, promotionChain', tested,
written)`.
- _The preconditions for `toi_promote` are satisfied because:_
- _`demote` deletes any elements from `promotionChain` that do not
satisfy `written <: T`, therefore every element of `promotionChain'`
satisfies `written <: T`._
- _`written = T` and `T` is a subtype of `x`'s declared type, therefore
`written <: declared`._
- Then `VM = VariableModel(declared, promotionChain'', tested, true, false,
captured)`.

- `stripParens(E1)`, where `E1` is an expression, is the result of stripping
outer parentheses from the expression `E1`. It is defined to be the
Expand Down Expand Up @@ -551,7 +604,12 @@ then they are all assigned the same value as `after(N)`.
- **Local-variable assignment**: If `N` is an expression of the form `x = E1`
where `x` is a local variable, then:
- Let `before(E1) = before(N)`.
- Let `after(N) = assign(x, E1, after(E1))`.
- Let `E1'` be the result of applying type coercion to `E1`, to coerce it to
the declared type of `x`.
- Let `after(N) = assign(x, E1', after(E1))`.
- _Since type coercion to type `T` produces an expression whose static type
is a subtype of `T`, the precondition of `assign` is satisfied, namely
that the static type of `E1'` must be a subtype of `x`'s declared type._

- **operator==** If `N` is an expression of the form `E1 == E2`, where the
static type of `E1` is `T1` and the static type of `E2` is `T2`, then:
Expand Down Expand Up @@ -617,7 +675,12 @@ then they are all assigned the same value as `after(N)`.
- **Local variable conditional assignment**: If `N` is an expression of the form
`x ??= E1` where `x` is a local variable, then:
- Let `before(E1) = split(promote(x, Null, before(N)))`.
- Let `M1 = assign(x, E1, after(E1))`
- Let `E1'` be the result of applying type coercion to `E1`, to coerce it to
the declared type of `x`.
- Let `M1 = assign(x, E1', after(E1))`
- _Since type coercion to type `T` produces an expression whose static type
is a subtype of `T`, the precondition of `assign` is satisfied, namely
that the static type of `E1'` must be a subtype of `x`'s declared type._
- Let `M2 = split(promoteToNonNull(x, before(N)))`
- Let `after(N) = merge(M1, M2)`

Expand Down