Skip to content

Commit 713c8c1

Browse files
Fix bugs in optimized variant
- Filter reflexive subset relations - Mark placeholder regions as live
1 parent e77e9c9 commit 713c8c1

File tree

1 file changed

+20
-13
lines changed

1 file changed

+20
-13
lines changed

rules/opt.dl

Lines changed: 20 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,12 @@ placeholder_origin(o) :- placeholder(o, _).
5252
.input known_placeholder_subset
5353

5454

55+
.decl origin_live_on_entry_or_placeholder(origin: Origin, point: Node) inline
56+
57+
origin_live_on_entry_or_placeholder(origin, point) :- origin_live_on_entry(origin, point).
58+
origin_live_on_entry_or_placeholder(origin, point) :- placeholder_origin(origin), cfg_node(point).
59+
60+
5561
// The origins `origin1` and `origin2` are "live to dead"
5662
// on the edge `point1 -> point2` if:
5763
//
@@ -65,8 +71,8 @@ placeholder_origin(o) :- placeholder(o, _).
6571
live_to_dying_regions(origin1, origin2, point1, point2) :-
6672
subset(origin1, origin2, point1),
6773
cfg_edge(point1, point2),
68-
origin_live_on_entry(origin1, point2),
69-
!origin_live_on_entry(origin2, point2).
74+
origin_live_on_entry_or_placeholder(origin1, point2),
75+
!origin_live_on_entry_or_placeholder(origin2, point2).
7076

7177

7278
// The `origin` requires `loan`, but the `origin` goes dead
@@ -77,7 +83,7 @@ dying_region_requires(origin, point1, point2, loan) :-
7783
requires(origin, loan, point1),
7884
!loan_killed_at(loan, point1),
7985
cfg_edge(point1, point2),
80-
!origin_live_on_entry(origin, point2).
86+
!origin_live_on_entry_or_placeholder(origin, point2).
8187

8288

8389
// Contains dead origins where we are interested
@@ -106,7 +112,7 @@ dying_can_reach(origin1, origin2, point1, point2) :-
106112
// "intermediate" `origin2` is dead at `point2`.
107113
dying_can_reach(origin1, origin3, point1, point2) :-
108114
dying_can_reach(origin1, origin2, point1, point2),
109-
!origin_live_on_entry(origin2, point2),
115+
!origin_live_on_entry_or_placeholder(origin2, point2),
110116
subset(origin2, origin3, point1).
111117

112118

@@ -119,7 +125,7 @@ dying_can_reach(origin1, origin3, point1, point2) :-
119125

120126
dying_can_reach_live(origin1, origin2, point1, point2) :-
121127
dying_can_reach(origin1, origin2, point1, point2),
122-
origin_live_on_entry(origin2, point2).
128+
origin_live_on_entry_or_placeholder(origin2, point2).
123129

124130

125131
// Indicates a "borrow region" `origin` at `point` which is not live on
@@ -128,7 +134,7 @@ dying_can_reach_live(origin1, origin2, point1, point2) :-
128134

129135
dead_borrow_region_can_reach_root(origin, point, loan) :-
130136
loan_issued_at(origin, loan, point),
131-
!origin_live_on_entry(origin, point).
137+
!origin_live_on_entry_or_placeholder(origin, point).
132138

133139

134140
.decl dead_borrow_region_can_reach_dead(origin: Origin, point: Node, loan: Loan)
@@ -139,7 +145,7 @@ dead_borrow_region_can_reach_dead(origin, point, loan) :-
139145
dead_borrow_region_can_reach_dead(origin2, point, loan) :-
140146
dead_borrow_region_can_reach_dead(origin1, point, loan),
141147
subset(origin1, origin2, point),
142-
!origin_live_on_entry(origin2, point).
148+
!origin_live_on_entry_or_placeholder(origin2, point).
143149

144150

145151
.decl subset(origin1: Origin, origin2: Origin, point: Node)
@@ -152,12 +158,13 @@ subset(origin1, origin2, point) :- subset_base(origin1, origin2, point).
152158
subset(origin1, origin2, point2) :-
153159
subset(origin1, origin2, point1),
154160
cfg_edge(point1, point2),
155-
origin_live_on_entry(origin1, point2),
156-
origin_live_on_entry(origin2, point2).
161+
origin_live_on_entry_or_placeholder(origin1, point2),
162+
origin_live_on_entry_or_placeholder(origin2, point2).
157163

158164
subset(origin1, origin3, point2) :-
159165
live_to_dying_regions(origin1, origin2, point1, point2),
160-
dying_can_reach_live(origin2, origin3, point1, point2).
166+
dying_can_reach_live(origin2, origin3, point1, point2),
167+
origin1 != origin3.
161168

162169

163170
.decl requires(origin: Origin, loan: Loan, point: Node)
@@ -175,19 +182,19 @@ requires(origin, loan, point2) :-
175182
requires(origin, loan, point1),
176183
!loan_killed_at(loan, point1),
177184
cfg_edge(point1, point2),
178-
origin_live_on_entry(origin, point2).
185+
origin_live_on_entry_or_placeholder(origin, point2).
179186

180187

181188
.decl borrow_live_at(loan: Loan, point: Node)
182189

183190
borrow_live_at(loan, point) :-
184191
requires(origin, loan, point),
185-
origin_live_on_entry(origin, point).
192+
origin_live_on_entry_or_placeholder(origin, point).
186193

187194
borrow_live_at(loan, point) :-
188195
dead_borrow_region_can_reach_dead(origin1, point, loan),
189196
subset(origin1, origin2, point),
190-
origin_live_on_entry(origin2, point).
197+
origin_live_on_entry_or_placeholder(origin2, point).
191198

192199

193200
.decl errors(loan: Loan, point: Node)

0 commit comments

Comments
 (0)