10BC0 progress on liveness · nikomatsakis/a-mir-formality-ndm@18fb2a0 · GitHub
[go: up one dir, main page]
Skip to content

Commit 18fb2a0

Browse files
nikomatsakisnikomatsakis
committed
progress on liveness
1 parent dfa463e commit 18fb2a0

File tree

7 files changed

+251
-8
lines changed

7 files changed

+251
-8
lines changed

‎crates/formality-check/src/borrow_check.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1 +1,2 @@
11
pub mod nll;
2+
pub mod liveness;

‎crates/formality-check/src/borrow_check/liveness.rs‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
use formality_core::{
2+
Cons, Fallible, Set, Union, judgment_fn
3+
};
4+
use formality_rust::grammar::minirust::{BasicBlock, BbId, PlaceExpression, Statement, Terminator, ValueExpression};
5+
6+
use crate::mini_rust_check::{TypeckEnv};
7+
8+
pub type LivePlaces = Set<PlaceExpression>;
9+
10+
judgment_fn! {
11+
/// Prove that any loans issued in this statement are respected.
12+
fn places_live_after_basic_block(
13+
env: TypeckEnv,
14+
bb_id: BbId,
15+
) => LivePlaces {
16+
debug(bb_id, env)
17+
18+
(
19+
(let BasicBlock { id: _, statements, terminator } = env.basic_block(bb_id)?)
20+
(places_live_after_statements(&env, statements) => places_after_statements)
21+
(places_live_after_terminator(&env, terminator) => places_after_terminator)
22+
--- ("lookup")
23+
(places_live_after_basic_block(env, bb_id) => Union((&places_after_statements, &places_after_terminator)))
24+
)
25+
}
26+
}
27+
28+
judgment_fn! {
29+
fn places_live_after_statements(
30+
env: TypeckEnv,
31+
statements: Vec<Statement>,
32+
) => LivePlaces {
33+
debug(statements, env)
34+
35+
(
36+
--- ("lookup")
37+
(places_live_after_statements(_env, ()) => LivePlaces::default())
38+
)
39+
40+
(
41+
(places_live_after_statement(&env, head) => places_after_head)
42+
(places_live_after_statements(&env, &tail) => places_after_tail)
43+
--- ("lookup")
44+
(places_live_after_statements(env, Cons(head, tail)) => Union((&places_after_head, &places_after_tail)))
45+
)
46+
}
47+
}
48+
49+
judgment_fn! {
50+
fn places_live_after_statement(
51+
env: TypeckEnv,
52+
statement: Statement,
53+
) => LivePlaces {
54+
debug(statement, env)
55+
56+
// ...
57+
}
58+
}
59+
60+
judgment_fn! {
61+
fn places_live_after_terminator(
62+
env: TypeckEnv,
63+
terminator: Terminator,
64+
) => LivePlaces {
65+
debug(terminator, env)
66+
67+
(
68+
(places_live_after_basic_block(env, bb_id) => places)
69+
--- ("goto")
70+
(places_live_after_terminator(env, Terminator::Goto(bb_id)) => places)
71+
)
72+
}
73+
}
74+
75+
76+
impl TypeckEnv {
77+
fn basic_block(&self, bb_id: BbId) -> Fallible<&BasicBlock> {
78+
Ok(self.blocks.iter()
79+
.find(|bb| bb.id == bb_id)
80+
.ok_or_else(|| anyhow::anyhow!("Basic block {:?} not found", bb_id))?)
81+
}
82+
}

‎crates/formality-check/src/borrow_check/nll.rs‎

Lines changed: 130 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
use formality_core::{
2-
Cons, Fallible, Set, judgment_fn, variable::CoreUniversalVar
2+
Cons, Fallible, Set, judgment_fn, variable::CoreUniversalVar, term
33
};
4-
use formality_rust::grammar::minirust::{BasicBlock, Statement, Terminator, ValueExpression};
4+
use formality_rust::grammar::minirust::{BasicBlock, PlaceExpression, Statement, Terminator, ValueExpression};
55
use formality_types::{
6-
grammar::Wcs,
6+
grammar::{Lt, RefKind, Wcs},
77
rust::FormalityLang,
88
};
99
use formality_prove::combinators::for_all;
1010

11-
use crate::mini_rust_check::{Location, TypeckEnv};
11+
use crate::{borrow_check::liveness::LivePlaces, mini_rust_check::{Location, TypeckEnv}};
1212

1313
/// So what is a lifetime? The NLL answer is that a lifetime corresponds to one of the following:
1414
///
@@ -138,7 +138,7 @@ judgment_fn! {
138138
fn loans_in_basic_block_respected(
139139
env: TypeckEnv,
140140
fn_assumptions: Wcs,
141-
block: BasicBlock
141+
block: BasicBlock,
142142
) => () {
143143
debug(block, fn_assumptions, env)
144144

@@ -150,6 +150,7 @@ judgment_fn! {
150150
)
151151
}
152152
}
153+
153154
judgment_fn! {
154155
/// Prove that any loans issued in this statement are respected.
155156
fn loans_in_statements_respected(
@@ -173,7 +174,6 @@ judgment_fn! {
173174
}
174175
}
175176

176-
177177
judgment_fn! {
178178
/// Prove that any loans issued in this statement are respected.
179179
fn loans_in_terminator_respected(
@@ -238,4 +238,127 @@ judgment_fn! {
238238

239239

240240
}
241-
}
241+
}
242+
243+
pub type Loans = Set<Loan>;
244+
245+
#[term]
246+
247+
struct Loan {
248+
lt: Lt,
249+
place: PlaceExpression,
250+
kind: RefKind,
251+
}
252+
253+
254+
judgment_fn! {
255+
/// Prove that any loans issued in this statement are respected.
256+
fn borrow_check_statement(
257+
env: TypeckEnv,
258+
assumptions: Wcs,
259+
loaned_on_entry: Loans,
260+
live_after: LivePlaces,
261+
statement: Statement,
262+
) => Loans {
263+
debug(statement, loaned_on_entry, live_after, assumptions, env)
264+
265+
(
266+
(place_not_borrowed_by_any(env, assumptions, &loaned, live_after, local_id) => ())
267+
--- ("storage-dead")
268+
(borrow_check_statement(env, assumptions, loaned, live_after, Statement::StorageDead(local_id)) => &loaned)
269+
)
270+
}
271+
}
272+
273+
274+
275+
judgment_fn! {
276+
/// Prove that none of the borrows in `borrowed` does not affect `place`.
277+
fn place_not_borrowed_by_any(
278+
env: TypeckEnv,
279+
assumptions: Wcs,
280+
loaned: Set<Loan>,
281+
live_after: LivePlaces,
282+
accessed_place: PlaceExpression,
283+
) => () {
284+
debug(accessed_place, loaned, live_after, assumptions, env)
285+
286+
(
287+
// Clearly, `place` is not borrowed if nothing has been borrowed.
288+
--- ("no borrows")
289+
(place_not_borrowed_by_any(_env, _assumptions, (), _live_after, _place) => ())
290+
)
291+
292+
(
293+
(place_not_borrowed_by(&env, &assumptions, head, &live_after, &place) => ())
294+
(place_not_borrowed_by_any(&env, &assumptions, &tail, &live_after, &place) => ())
295+
--- ("no borrows")
296+
(place_not_borrowed_by_any(env, assumptions, Cons(head, tail), live_after, place) => ())
297+
)
298+
}
299+
}
300+
301+
judgment_fn! {
302+
/// Prove that the borrow `borrow` does not affect `place`.
303+
fn place_not_borrowed_by(
304+
env: TypeckEnv,
305+
fn_assumptions: Wcs,
306+
loan: Loan,
307+
live_after: LivePlaces,
308+
accessed_place: PlaceExpression,
309+
) => () {
310+
debug(accessed_place, loan, live_after, fn_assumptions, env)
311+
312+
(
313+
(place_disjoint_from_place(loan.place, accessed_place) => ())
314+
--- ("borrows of disjoint places")
315+
(place_not_borrowed_by(< C46B /span>_env, _assumptions, loan, _live_after, accessed_place) => ())
316+
)
317+
318+
(
319+
--- ("borrow not live -- no live places")
320+
(place_not_borrowed_by(_env, _assumptions, _loan, (), _accessed_place) => ())
321+
)
322+
323+
(
324+
(place_not_borrowed_by_live_variable(&env, &assumptions, &head, &loan, &accessed_place) => ())
325+
(place_not_borrowed_by(&env, &assumptions, &loan, &tail, &accessed_place) => ())
326+
--- ("borrow not live -- live place")
327+
(place_not_borrowed_by(env, assumptions, loan, Cons(head, tail), accessed_place) => ())
328+
)
329+
}
330+
}
331+
332+
judgment_fn! {
333+
/// Prove that `accessed_place` can still be accessed even though `live_place` is live and the borrow occurs.
334+
fn place_not_borrowed_by_live_variable(
335+
env: TypeckEnv,
336+
assumptions: Wcs,
337+
live_place: PlaceExpression,
338+
borrowed_place: Loan,
339+
accessed_place: PlaceExpression,
340+
) => () {
341+
debug(accessed_place, borrowed_place, live_place, assumptions, env)
342+
343+
}
344+
}
345+
346+
judgment_fn! {
347+
fn place_disjoint_from_place(
348+
place1: PlaceExpression,
349+
place2: PlaceExpression,
350+
) => () {
351+
debug(place1, place2)
352+
353+
(
354+
(if local1 != local2)
355+
--- ("different locals")
356+
(place_disjoint_from_place(
357+
PlaceExpression::Local(local1),
358+
PlaceExpression::Local(local2),
359+
) => ())
360+
)
361+
362+
// ... fill this in ...
363+
}
364+
}

‎crates/formality-check/src/lib.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ use formality_types::{
1313
grammar::{CrateId, Fallible, Wcs},
1414
rust::Visit,
1515
};
16+
use formality_types::rust::FormalityLang;
1617

1718
mod borrow_check;
1819
mod mini_rust_check;

‎crates/formality-core/src/collections.rs‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -232,6 +232,33 @@ tuple_upcast!(Vec: A, B);
232232
tuple_upcast!(Vec: A, B, C);
233233
tuple_upcast!(Vec: A, B, C, D);
234234

235+
/// This type exists to be used in judgment functions.
236+
/// You can upcast a `Union((a, b))` to a `Set<T>`.
237+
#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
238+
pub struct Union<T>(pub T);
239+
240+
/// Upcast from a tuple of iterable things into a collection.
241+
/// Downcasting doesn't work, because how would we know how many
242+
/// things to put in each collection? But see `Cons` below.
243+
#[allow(non_snake_case)]
244+
impl<A, B, T> UpcastFrom<Union<(A, B)>> for Set<T>
245+
where
246+
A: IntoIterator + Clone,
247+
A::Item: Upcast<T>,
248+
249+
B: IntoIterator + Clone,
250+
B::Item: Upcast<T>,
251+
252+
T: Ord + Clone,
253+
{
254+
fn upcast_from(Union((a, b)): Union<(A, B)>) -> Self {
255+
let c = None.into_iter();
256+
let c = c.chain(a.upcasted());
257+
let c = c.chain(b.upcasted());
258+
c.collect()
259+
}
260+
}
261+
235262
/// This type exists to be used in judgment functions.
236263
/// You can upcast/downcast a `Vec` or `Set` to `Cons(head, tail)`
237264
/// where `head` will be the first item in the collection

‎crates/formality-core/src/lib.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@ pub mod visit;
4141

4242
pub use cast::{Downcast, DowncastFrom, DowncastTo, Downcasted, To, Upcast, UpcastFrom, Upcasted};
4343
pub use collections::Cons;
44+
pub use collections::Union;
4445
pub use collections::Deduplicate;
4546
pub use collections::Map;
4647
pub use collections::Set;

‎crates/formality-rust/src/grammar/minirust.rs‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -271,8 +271,10 @@ impl ConstTypePair {
271271
pub enum PlaceExpression {
272272
#[grammar(local($v0))]
273273
Local(LocalId),
274+ 4755
274275
#[grammar(*($v0))] // TODO: change syntax?
275-
Deref(Arc<ValueExpression>),
276+
Deref(Arc<PlaceExpression>), // XXX: we depart from MiniRust here and require a place
277+
276278
// Project to a field.
277279
#[grammar($v0)]
278280
Field(FieldProjection),
@@ -287,3 +289,9 @@ pub struct FieldProjection {
287289
/// The field to project to.
288290
pub index: usize,
289291
}
292+
293+
impl UpcastFrom<LocalId> for PlaceExpression {
294+
fn upcast_from(term: LocalId) -> Self {
295+
PlaceExpression::Local(term)
296+
}
297+
}

0 commit comments

Comments
 (0)
0