Skip to content

Commit cd5641c

Browse files
lqdlqd
committed
book: document naive rules
1 parent d12ac47 commit cd5641c

File tree

1 file changed

+158
-1
lines changed

1 file changed

+158
-1
lines changed

‎book/src/rules/loans.md‎

Lines changed: 158 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,160 @@
11
# Loan analysis
22

3-
**These rules are not yet described.**
3+
Loan analysis is the heart of the borrow checker, and will compute:
4+
- illegal access errors: an action on a loan, that is illegal to perform
5+
- illegal subset relationships errors: missing relationships between placeholder origins
6+
7+
This is done in multiple variants, whose goals are different: performance, readability, tests and validation.
8+
9+
Broadly speaking, the goals of the analysis is 1) to track loans:
10+
- from the point and origin in which they are issued, to the points where they are invalidated
11+
- flowing from origin to origin at a single point, via their `subset` relationships
12+
- flowing from point to point in the CFG, according to the origins' liveness (stopping at points where a loan is killed)
13+
14+
And 2) to track undeclared relationships between placeholder origins.
15+
16+
Any live loan which is invalidated will be an illegal access error, any placeholder which flows into another placeholder unexpectedly will be an illegal subset relationship error.
17+
18+
### Inputs
19+
20+
The input relations will be described below, but the [dedicated page](./relations.md) will have more information about them.
21+
22+
```prolog
23+
// Indicates that the `loan` was "issued" at the given `point`, creating a
24+
// reference with the `origin`. Effectively, `origin` may refer to data from
25+
// `loan` starting at `point` (this is usually the point *after* a borrow rvalue).
26+
.decl loan_issued_at(Origin:origin, Loan:loan, Point:point)
27+
.input loan_issued_at
28+
29+
// When some prefix of the path borrowed at `loan` is assigned at `point`.
30+
// Indicates that the path borrowed by the `loan` has changed in some way that the
31+
// loan no longer needs to be tracked. (In particular, mutations to the path that
32+
// was borrowed no longer invalidate the loan)
33+
.decl loan_killed_at(Loan:loan, Point:point)
34+
.input loan_killed_at
35+
36+
// Indicates that the `loan` is invalidated by some action
37+
// taking place at `point`; if any origin that references this loan is live,
38+
// this is an error.
39+
.decl loan_invalidated_at(Loan:loan, Point:point)
40+
.input loan_invalidated_at
41+
42+
// When we require `origin1@point: origin2@point`.
43+
// Indicates that `origin1 <= origin2` -- i.e., the set of loans in `origin1`
44+
// are a subset of those in `origin2`.
45+
.decl subset_base(Origin1:origin, Origin2:origin, Point:point)
46+
.input subset_base
47+
48+
// Describes a placeholder `origin`, with its associated placeholder `loan`.
49+
.decl placeholder(Origin:origin, Loan:loan)
50+
.input placeholder
51+
52+
// These reflect the `'a: 'b` relations that are either declared by the user on
53+
// function declarations or which are inferred via implied bounds.
54+
// For example: `fn foo<'a, 'b: 'a, 'c>(x: &'c &'a u32)` would have two entries:
55+
// - one for the user-supplied subset `'b: 'a`
56+
// - and one for the `'a: 'c` implied bound from the `x` parameter,
57+
// (note that the transitive relation `'b: 'c` is not necessarily included
58+
// explicitly, but rather inferred by polonius).
59+
.decl known_placeholder_subset(Origin1:origin, Origin2:origin)
60+
.input known_placeholder_subset
61+
```
62+
63+
The datalog rules below are considered the "naive" implementation, as it computes the whole transitive closure of the subset relation, but are easy to describe and explain. They are implemented using the datafrog engine in the [Naive variant](https://github.com/rust-lang/polonius/blob/master/polonius-engine/src/output/naive.rs).
64+
65+
Some trivial differences exist with the implementation:
66+
- the use of the `;` alternative operator in the rules
67+
- the use of worst-case optimal joins in the implementation
68+
69+
### Subsets between origins
70+
71+
The rules below compute the complete graph of subsets between origins: starting from the non-transitive subsets, we close over this relation at a given point in the CFG (regardless of liveness). Liveness is then taken into account to propagate these transitive subsets along the CFG: if an origin flows into another at a given point, and they both are live at the successor points (reminder: placeholder origins are considered live at all points), the relationship is propagated to the successor points.
72+
73+
```prolog
74+
.decl subset(Origin1:origin, Origin2:origin, Point:point)
75+
76+
// R1: the initial subsets are the non-transitive `subset_base` static input
77+
subset(Origin1, Origin2, Point) :-
78+
subset_base(Origin1, Origin2, Point).
79+
80+
// R2: compute the subset transitive closure, at a given point
81+
subset(Origin1, Origin3, Point) :-
82+
subset(Origin1, Origin2, Point),
83+
subset(Origin2, Origin3, Point).
84+
85+
// R3: propagate subsets along the CFG, according to liveness
86+
subset(Origin1, Origin2, TargetPoint) :-
87+
subset(Origin1, Origin2, SourcePoint),
88+
cfg_edge(SourcePoint, TargetPoint),
89+
(origin_live_on_entry(Origin1, TargetPoint); placeholder(Origin1, _)),
90+
(origin_live_on_entry(Origin2, TargetPoint); placeholder(Origin2, _)).
91+
```
92+
93+
### The origins contain loans
94+
95+
The rules below compute what loans are contained in which origins, at given points of the CFG: starting from the "issuing point and origin", a loan is propagated via the subsets computed above, at a given point in the CFG. Liveness is then taken into account to propagate these loans along the CFG: if a loan is contained in an origin at a given point, and that the origin is live at the successor points, the loan is propagated to the successor points. A subtlety here is that there are points in the CFG where a loan can be killed, and that will stop propagation. Rule 6 uses both liveness and kill points to know whether the loan should be propagated further in the CFG.
96+
97+
```prolog
98+
.decl origin_contains_loan_on_entry(Origin:origin, Loan:loan, Point:point)
99+
100+
// R4: the issuing origins are the ones initially containing loans
101+
origin_contains_loan_on_entry(Origin, Loan, Point) :-
102+
loan_issued_at(Origin, Loan, Point).
103+
104+
// R5: propagate loans within origins, at a given point, according to subsets
105+
origin_contains_loan_on_entry(Origin2, Loan, Point) :-
106+
origin_contains_loan_on_entry(Origin1, Loan, Point),
107+
subset(Origin1, Origin2, Point).
108+
109+
// R6: propagate loans along the CFG, according to liveness
110+
origin_contains_loan_on_entry(Origin, Loan, TargetPoint) :-
111+
origin_contains_loan_on_entry(Origin, Loan, SourcePoint),
112+
!loan_killed_at(Loan, SourcePoint),
113+
cfg_edge(SourcePoint, TargetPoint),
114+
(origin_live_on_entry(Origin, TargetPoint); placeholder(Origin, _)).
115+
```
116+
117+
### Loan liveness, and illegal access errors
118+
119+
With the information computed above, we can compute illegal accesses errors. It is an error to invalidate a loan that is live at a given point. A loan is live at a point if it is contained in an origin that is live at that point.
120+
121+
```prolog
122+
.decl loan_live_at(Loan:loan, Point:point)
123+
124+
// R7: compute whether a loan is live at a given point, i.e. whether it is
125+
// contained in a live origin at this point
126+
loan_live_at(Loan, Point) :-
127+
origin_contains_loan_on_entry(Origin, Loan, Point),
128+
(origin_live_on_entry(Origin, Point); placeholder(Origin, _)).
129+
130+
.decl errors(Loan:loan, Point:point)
131+
132+
// R8: compute illegal access errors, i.e. an invalidation of a live loan
133+
errors(Loan, Point) :-
134+
loan_invalidated_at(Loan, Point),
135+
loan_live_at(Loan, Point).
136+
```
137+
138+
### Placeholder subsets, and illegal subset relationships errors
139+
140+
These errors can be computed differently depending on the variant, but the goal is the same: if the analysis detects that a placeholder origin ultimately flows into another placeholder origin, that relationship needs to be declared or it is an error.
141+
142+
The `Naive` rules variant computes the complete subset transitive closure and can more easily detect whether one of these facts links two placeholder origins. The `LocationInsensitive` rules variant does not compute transitive subsets at all, and uses loan propagation to detect these errors (if a placeholder loan flows into a placeholder origin). The `Opt` optimized rules variant only computes the transitive closure of some origins according to their liveness and possible contribution to any error (mostly the ones dying along an edge, and the origins they can reach), and track the transitive subsets of placeholders explicitly.
143+
144+
```prolog
145+
.decl subset_errors(Origin1:origin, Origin2:origin, Point:point)
146+
147+
// R9: compute illegal subset relations errors, i.e. the undeclared subsets
148+
// between two placeholder origins.
149+
subset_errors(Origin1, Origin2, Point) :-
150+
subset(Origin1, Origin2, Point),
151+
placeholder_origin(Origin1),
152+
placeholder_origin(Origin2),
153+
!known_placeholder_subset(Origin1, Origin2).
154+
```
155+
156+
### To be continued
157+
158+
A more detailed description of the rules in the `LocationInsensitive` and `Opt` variants will be added later but they compute the same things described above:
159+
- the `LocationInsensitive` variant tries to quickly find "potential errors" in a path- and flow-insensitive manner: if there are no errors, we don't need to do the full analysis. If there are potential errors, they could be false positives or real errors: the interesting thing is that only these loans and origins need to be checked by the full analysis.
160+
- the `Opt` variant limits where the subset transitive closure is computed: some origins are short-lived, or part of a subsection of the subset graph into which no loan ever flows, etc. These cases don't contribute to errors or loan propagation and are not useful to track.

0 commit comments

Comments
 (0)