@@ -139,55 +139,76 @@ module type Backward_domain = sig
139
139
140
140
val bot : t
141
141
142
- val compare : t -> t -> int
143
-
144
142
val join : t -> t -> t
145
143
146
144
val less_equal : t -> t -> bool
147
145
146
+ val compare : t -> t -> int
147
+
148
148
val to_string : t -> string
149
149
end
150
150
151
151
module type Backward_transfer = sig
152
152
type domain
153
153
154
- val basic : domain -> exn :domain -> Cfg .basic Cfg .instruction -> domain
154
+ type error
155
+
156
+ val basic :
157
+ domain -> exn :domain -> Cfg .basic Cfg .instruction -> (domain , error ) result
155
158
156
159
val terminator :
157
- domain -> exn :domain -> Cfg .terminator Cfg .instruction -> domain
160
+ domain ->
161
+ exn :domain ->
162
+ Cfg .terminator Cfg .instruction ->
163
+ (domain , error ) result
158
164
159
- val exception_ : domain -> domain
165
+ val exception_ : domain -> ( domain , error ) result
160
166
end
161
167
162
168
module Instr = Numbers. Int
163
169
170
+ module Dataflow_result = struct
171
+ type ('a, 'e) t =
172
+ | Ok of 'a
173
+ | Aborted of 'a * 'e
174
+ | Max_iterations_reached
175
+ end
176
+
164
177
module type Backward_S = sig
165
178
type domain
166
179
180
+ type error
181
+
167
182
type _ map =
168
183
| Block : domain Label.Tbl .t map
169
184
| Instr : domain Instr.Tbl .t map
185
+ | Both : (domain Instr.Tbl .t * domain Label.Tbl .t ) map
170
186
171
187
val run :
172
188
Cfg .t ->
173
189
?max_iteration : int ->
174
190
init :domain ->
175
191
map :'a map ->
176
192
unit ->
177
- ('a , 'a ) Result .t
193
+ ('a , error ) Dataflow_result .t
178
194
end
179
195
180
196
module Backward
181
197
(D : Backward_domain )
182
198
(T : Backward_transfer with type domain = D.t ) :
183
- Backward_S with type domain = D. t = struct
199
+ Backward_S with type domain = D. t and type error = T. error = struct
184
200
(* CR xclerc for xclerc: see what can be shared with `Forward`. *)
185
201
186
202
type domain = D .t
187
203
204
+ type error = T .error
205
+
206
+ exception Dataflow_aborted of error
207
+
188
208
type _ map =
189
209
| Block : domain Label.Tbl .t map
190
210
| Instr : domain Instr.Tbl .t map
211
+ | Both : (domain Instr.Tbl .t * domain Label.Tbl .t ) map
191
212
192
213
module WorkSetElement = struct
193
214
type t =
@@ -204,6 +225,11 @@ module Backward
204
225
205
226
module WorkSet = Set. Make (WorkSetElement )
206
227
228
+ let unwrap_transfer_result value =
229
+ match value with
230
+ | Ok value -> value
231
+ | Error error -> raise (Dataflow_aborted error)
232
+
207
233
let transfer_block :
208
234
domain Instr.Tbl. t option ->
209
235
domain ->
@@ -212,6 +238,7 @@ module Backward
212
238
domain =
213
239
fun tbl value ~exn block ->
214
240
let replace (instr : _ Cfg.instruction ) value =
241
+ let value = unwrap_transfer_result value in
215
242
match tbl with
216
243
| None -> value
217
244
| Some tbl ->
@@ -256,7 +283,7 @@ module Backward
256
283
init :domain ->
257
284
map :a map ->
258
285
unit ->
259
- (a , a ) Result .t =
286
+ (a , error ) Dataflow_result .t =
260
287
fun cfg ?(max_iteration = max_int) ~init ~map () ->
261
288
let res_block, res_instr, work_set = create cfg ~init in
262
289
let iteration = ref 0 in
@@ -265,80 +292,85 @@ module Backward
265
292
Label.Tbl. create (Label.Tbl. length cfg.Cfg. blocks)
266
293
in
267
294
let instr_map : D.t Instr.Tbl.t option =
268
- match map with Block -> None | Instr -> Some res_instr
295
+ match map with Block -> None | Both | Instr -> Some res_instr
269
296
in
270
- while (not (WorkSet. is_empty ! work_set)) && ! iteration < max_iteration do
271
- incr iteration;
272
- let element, block = remove_and_return cfg work_set in
273
- let exn : domain =
274
- Option. map
275
- (fun exceptional_successor ->
276
- Label.Tbl. find_opt handler_map exceptional_successor)
277
- block.exn
278
- |> Option. join
279
- |> Option. value ~default: D. bot
280
- in
281
- let value = transfer_block instr_map element.value ~exn block in
282
- if block.is_trap_handler
283
- then (
284
- let old_value =
285
- Option. value
286
- (Label.Tbl. find_opt handler_map block.start)
287
- ~default: D. bot
297
+ let result : a =
298
+ match map with
299
+ | Block -> res_block
300
+ | Instr -> res_instr
301
+ | Both -> res_instr, res_block
302
+ in
303
+ try
304
+ while (not (WorkSet. is_empty ! work_set)) && ! iteration < max_iteration do
305
+ incr iteration;
306
+ let element, block = remove_and_return cfg work_set in
307
+ let exn : domain =
308
+ Option. map
309
+ (fun exceptional_successor ->
310
+ Label.Tbl. find_opt handler_map exceptional_successor)
311
+ block.exn
312
+ |> Option. join
313
+ |> Option. value ~default: D. bot
288
314
in
289
- let new_value = T. exception_ value in
290
- if not ( D. less_equal new_value old_value)
315
+ let value = transfer_block instr_map element. value ~exn block in
316
+ if block.is_trap_handler
291
317
then (
292
- Label.Tbl. replace handler_map block.start new_value;
318
+ let old_value =
319
+ Option. value
320
+ (Label.Tbl. find_opt handler_map block.start)
321
+ ~default: D. bot
322
+ in
323
+ let new_value = T. exception_ value |> unwrap_transfer_result in
324
+ if not (D. less_equal new_value old_value)
325
+ then (
326
+ Label.Tbl. replace handler_map block.start new_value;
327
+ List. iter
328
+ (fun predecessor_label ->
329
+ let current_value =
330
+ Option. value
331
+ (Label.Tbl. find_opt res_block predecessor_label)
332
+ ~default: D. bot
333
+ in
334
+ work_set
335
+ := WorkSet. add
336
+ { WorkSetElement. label = predecessor_label;
337
+ value = current_value
338
+ }
339
+ ! work_set)
340
+ (Cfg. predecessor_labels block)))
341
+ else
293
342
List. iter
294
343
(fun predecessor_label ->
295
- let current_value =
344
+ let old_value =
296
345
Option. value
297
346
(Label.Tbl. find_opt res_block predecessor_label)
298
347
~default: D. bot
299
348
in
300
- work_set
301
- := WorkSet. add
302
- { WorkSetElement. label = predecessor_label;
303
- value = current_value
304
- }
305
- ! work_set)
306
- (Cfg. predecessor_labels block)))
307
- else
308
- List. iter
309
- (fun predecessor_label ->
310
- let old_value =
311
- Option. value
312
- (Label.Tbl. find_opt res_block predecessor_label)
313
- ~default: D. bot
314
- in
315
- let new_value = D. join old_value value in
316
- if not (D. less_equal new_value old_value)
317
- then (
318
- Label.Tbl. replace res_block predecessor_label new_value;
319
- let already_in_workset = ref false in
320
- work_set
321
- := WorkSet. filter
322
- (fun { WorkSetElement. label; value } ->
323
- if Label. equal label predecessor_label
324
- then (
325
- if D. less_equal new_value value
326
- then already_in_workset := true ;
327
- not (D. less_equal value new_value))
328
- else true )
329
- ! work_set;
330
- if not ! already_in_workset
331
- then
349
+ let new_value = D. join old_value value in
350
+ if not (D. less_equal new_value old_value)
351
+ then (
352
+ Label.Tbl. replace res_block predecessor_label new_value;
353
+ let already_in_workset = ref false in
332
354
work_set
333
- := WorkSet. add
334
- { WorkSetElement. label = predecessor_label;
335
- value = new_value
336
- }
337
- ! work_set))
338
- (Cfg. predecessor_labels block)
339
- done ;
340
- let return x =
341
- if WorkSet. is_empty ! work_set then Result. Ok x else Result. Error x
342
- in
343
- match map with Block -> return res_block | Instr -> return res_instr
355
+ := WorkSet. filter
356
+ (fun { WorkSetElement. label; value } ->
357
+ if Label. equal label predecessor_label
358
+ then (
359
+ if D. less_equal new_value value
360
+ then already_in_workset := true ;
361
+ not (D. less_equal value new_value))
362
+ else true )
363
+ ! work_set;
364
+ if not ! already_in_workset
365
+ then
366
+ work_set
367
+ := WorkSet. add
368
+ { WorkSetElement. label = predecessor_label;
369
+ value = new_value
370
+ }
371
+ ! work_set))
372
+ (Cfg. predecessor_labels block)
373
+ done ;
374
+ if WorkSet. is_empty ! work_set then Ok result else Max_iterations_reached
375
+ with Dataflow_aborted error -> Aborted (result, error)
344
376
end
0 commit comments