Skip to content

Commit

Permalink
change from using flow to using liveness
Browse files Browse the repository at this point in the history 
This also allows us to have less branching!
Awesome!
  • Loading branch information
@nikomatsakis
nikomatsakis committed Feb 16, 2024
1 parent 40ba060 commit 6367654
Show file tree
Hide file tree
Showing 9 changed files with 81 additions and 174 deletions.
1 change: 0 additions & 1 deletion src/type_system/accesses.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,6 @@ judgment_fn! {
debug(access, place, env, flow, live_after)

(
(if !flow.is_moved(&place))
(env_permits_access(env, flow, live_after, access, place) => (env, flow))
-------------------------------- ("access_permitted")
(access_permitted(env, flow, live_after, access, place) => (env, flow))
Expand Down
13 changes: 8 additions & 5 deletions src/type_system/expressions.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,9 +102,9 @@ judgment_fn! {
)

(
(access_permitted(env, flow, live_after, Access::Give, &place) => (env, flow))
(access_permitted(env, flow, &live_after, Access::Give, &place) => (env, flow))
(place_ty(&env, &place) => ty)
(give_place(&env, &flow, &place, &ty) => (env, flow))
(give_place(&env, &flow, &live_after, &place, &ty) => (env, flow))
----------------------------------- ("give place")
(type_expr(env, flow, live_after, PlaceExpr { access: Access::Give, place }) => (env, flow, &ty))
)
Expand Down Expand Up @@ -204,22 +204,25 @@ judgment_fn! {
fn give_place(
env: Env,
flow: Flow,
live_after: LivePlaces,
place: Place,
ty: Ty,
) => (Env, Flow) {
debug(place, ty, env, flow)
debug(place, ty, env, flow, live_after)

(
(if live_after.is_live(&place))!
(is_shared(env, ty) => env)
----------------------------------- ("shared")
(give_place(env, flow, _place, ty) => (env, &flow))
(give_place(env, flow, _live_after, _place, ty) => (env, &flow))
)

(
(if !live_after.is_live(&place))
(let flow = flow.move_place(&place))
(let env = env.with_place_in_flight(&place))
----------------------------------- ("affine")
(give_place(env, flow, place, _ty) => (env, flow))
(give_place(env, flow, live_after, place, _ty) => (env, flow))
)
}
}
Expand Down
6 changes: 6 additions & 0 deletions src/type_system/liveness.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,12 @@ impl LivePlaces {
|| self.traversed.iter().any(|p| place.is_prefix_of(&p))
}

/// True if `v` is live -- i.e., may be accessed after this point.
pub fn place_is_live(&self, p: impl Upcast<Place>) -> bool {
let p: Place = p.upcast();
self.is_live(p.var)
}

/// Compute a new set of live-vars just before `term` has been evaluated.
pub fn before(&self, term: &impl AdjustLiveVars) -> Self {
term.adjust_live_vars(self.clone())
Expand Down
54 changes: 16 additions & 38 deletions src/type_system/tests/fn_calls.rs
View file

Large diffs are not rendered by default.

88 changes: 40 additions & 48 deletions src/type_system/tests/move_check.rs
View file

Large diffs are not rendered by default.

18 changes: 0 additions & 18 deletions src/type_system/tests/move_tracking.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -221,24 +221,6 @@ fn give_while_shared_then_assign_while_shared_then_mutate_new_place() {
judgment `type_statements_with_final_ty { statements: [d = bar . i . give ;, s . give ;, d = new Data () ;, s . give ;, () ;], ty: (), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, bar: Foo, d: Data, foo: Foo, s: shared {bar . i} Data}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {foo} }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "cons" failed at step #2 (src/file.rs:LL:CC) because
judgment `type_statements_with_final_ty { statements: [s . give ;, d = new Data () ;, s . give ;, () ;], ty: (), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, bar: Foo, d: Data, foo: Foo, s: shared {d} Data}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {bar . i, foo} }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "cons" failed at step #2 (src/file.rs:LL:CC) because
judgment `type_statements_with_final_ty { statements: [d = new Data () ;, s . give ;, () ;], ty: shared {d} Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, bar: Foo, d: Data, foo: Foo, s: shared {d} Data}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {bar . i, foo, s} }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `type_statement { statement: d = new Data () ;, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, bar: Foo, d: Data, foo: Foo, s: shared {d} Data}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {bar . i, foo, s} }, live_after: LivePlaces { accessed: {s}, traversed: {} } }` failed at the following rule(s):
the rule "let" failed at step #4 (src/file.rs:LL:CC) because
judgment `env_permits_access { access: lease, place: d, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, @ fresh(0): Data, bar: Foo, d: Data, foo: Foo, s: shared {d} Data}, assumptions: {}, fresh: 1 }, flow: Flow { moved_places: {bar . i, foo, s} }, live_after: LivePlaces { accessed: {s}, traversed: {} } }` failed at the following rule(s):
the rule "env_permits_access" failed at step #1 (src/file.rs:LL:CC) because
judgment `parameters_permit_access { parameters: [shared {d} Data], access: lease, place: d, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, @ fresh(0): Data, bar: Foo, d: Data, foo: Foo, s: shared {d} Data}, assumptions: {}, fresh: 1 }, flow: Flow { moved_places: {bar . i, foo, s} } }` failed at the following rule(s):
the rule "cons" failed at step #0 (src/file.rs:LL:CC) because
judgment `parameter_permits_access { parameter: shared {d} Data, access: lease, place: d, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, @ fresh(0): Data, bar: Foo, d: Data, foo: Foo, s: shared {d} Data}, assumptions: {}, fresh: 1 }, flow: Flow { moved_places: {bar . i, foo, s} } }` failed at the following rule(s):
the rule "parameter" failed at step #1 (src/file.rs:LL:CC) because
judgment `lien_permit_access { lien: shared{d}, access: lease, accessed_place: d, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, @ fresh(0): Data, bar: Foo, d: Data, foo: Foo, s: shared {d} Data}, assumptions: {}, fresh: 1 }, flow: Flow { moved_places: {bar . i, foo, s} } }` failed at the following rule(s):
the rule "our" failed at step #0 (src/file.rs:LL:CC) because
judgment `shared_place_permits_access { shared_place: d, access: lease, accessed_place: d }` failed at the following rule(s):
the rule "share-mutation" failed at step #0 (src/file.rs:LL:CC) because
condition evaluted to false: `place_disjoint_from(&accessed_place, &shared_place)`
&accessed_place = d
&shared_place = d
the rule "cons" failed at step #2 (src/file.rs:LL:CC) because
judgment `type_statements_with_final_ty { statements: [d = new Data () ;, s . give ;, () ;], ty: shared {d} Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, bar: Foo, d: Data, foo: Foo, s: shared {d} Data}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {bar . i, foo} }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
Expand Down
Loading

0 comments on commit 6367654

Please sign in to comment.