naive soufflé

.type point
.type region
.type loan

.decl borrow_region(R:region, L:loan, P:point)
.input borrow_region

.decl cfg_edge(P:point, Q:point)
.input cfg_edge

.decl killed(L:loan, P:point)
.input killed

.decl outlives(R1:region, R2:region, P:point)
.input outlives

.decl region_live_at(R:region, P:point)
.input region_live_at

.decl universal_region(R:region)
.input universal_region

.decl subset(R1:region, R2:region, P:point)
subset(R1, R2, P) :- outlives(R1, R2, P).
subset(R1, R3, P) :-
  subset(R1, R2, P),
  subset(R2, R3, P).
subset(R1, R2, Q) :-
  subset(R1, R2, P),
  cfg_edge(P, Q),
  (region_live_at(R1, Q); universal_region(R1)),
  (region_live_at(R2, Q); universal_region(R2)).

.decl requires(R:region, B:loan, P:point)
requires(R, B, P) :- borrow_region(R, B, P).
requires(R2, B, P) :-
  requires(R1, B, P),
  subset(R1, R2, P).
requires(R, B, Q) :-
  requires(R, B, P),
  !killed(B, P),
  cfg_edge(P, Q),
  (region_live_at(R, Q); universal_region(R)).

.decl borrow_live_at(P:point,B:loan)
borrow_live_at(P, B) :- requires(R, B, P), region_live_at(R, P).
borrow_live_at(P, B) :- requires(R, B, P), universal_region(R).

.output borrow_live_at(IO=stdout)

timely-opt soufflé

.type point
.type region
.type loan

.decl borrow_region(R:region, L:loan, P:point)
.input borrow_region

.decl cfg_edge(P:point, Q:point)
.input cfg_edge

.decl killed(L:loan, P:point)
.input killed

.decl outlives(R1:region, R2:region, P:point)
.input outlives

.decl region_live_at(R:region, P:point)
.input region_live_at

.decl universal_region(R:region)
.input universal_region

.decl live_to_dead_regions(R1:region, R2:region, P:point, Q:point)
live_to_dead_regions(R1, R2, P, Q) :-
  subset(R1, R2, P),
  cfg_edge(P, Q),
  (region_live_at(R1, Q); universal_region(R1)),
  !region_live_at(R2, Q),
  !universal_region(R2).

.decl dead_can_reach(R1:region, R2:region, P:point, Q:point)
dead_can_reach(R2, R3, P, Q) :-
  live_to_dead_regions(_R1, R2, P, Q),
  subset(R2, R3, P).
dead_can_reach(R1, R3, P, Q) :-
  dead_can_reach(R1, R2, P, Q),
  !region_live_at(R2, Q),
  !universal_region(R2),
  subset(R2, R3, P).

.decl subset(R1:region, R2:region, P:point)
subset(R1, R2, P) :- outlives(R1, R2, P).
subset(R1, R2, Q) :-
  subset(R1, R2, P),
  cfg_edge(P, Q),
  (region_live_at(R1, Q); universal_region(R1)),
  (region_live_at(R2, Q); universal_region(R2)).
subset(R1, R3, Q) :-
  live_to_dead_regions(R1, R2, P, Q),
  dead_can_reach(R2, R3, P, Q),
  region_live_at(R3, Q).

.decl requires(R:region, B:loan, P:point)
requires(R, B, P) :- borrow_region(R, B, P).
requires(R2, B, P) :-
  requires(R1, B, P),
  subset(R1, R2, P).
requires(R, B, Q) :-
  requires(R, B, P),
  !killed(B, P),
  cfg_edge(P, Q),
  (region_live_at(R, Q); universal_region(R)).

.decl borrow_live_at(P:point, B:loan)
borrow_live_at(P, B) :- requires(R, B, P), region_live_at(R, P).
borrow_live_at(P, B) :- requires(R, B, P), universal_region(R).

.output borrow_live_at(IO=stdout)