Source file product.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
(** Reduced product combiner with n-ary reduction rules *)
open Mopsa_utils
open Core.All
open Sig.Reduction.Exec
open Sig.Reduction.Eval
open Sig.Combiner.Stacked
open Common
open Location
(** Signature of a pool of domains with pointwise transfer functions *)
module type POOL =
sig
include STACKED_COMBINER
val checks : check list list
val members : DomainSet.t list
val exec : DomainSet.t option -> stmt -> ('a,t) man -> 'a flow -> 'a post option list
val eval : DomainSet.t option -> expr -> ('a,t) man -> 'a flow -> 'a eval option list
end
(** Empty pool *)
module EmptyPool : POOL =
struct
type t = unit
let id = C_empty
let name = "()"
let domains = DomainSet.empty
let members = []
let semantics = SemanticSet.empty
let routing_table = empty_routing_table
let checks = [[]]
let bottom = ()
let top = ()
let is_bottom _ = false
let subset _ _ ((),s) ((),s') = true,s,s'
let join _ _ ((),s) ((),s') = (),s,s'
let meet _ _ ((),s) ((),s') = (),s,s'
let widen _ _ ((),s) ((),s') = (),s,s',true
let merge _ _ _ _ = ()
let init _ _ flow = None
let exec _ _ _ flow = []
let eval _ _ _ flow = []
let ask _ _ _ _ = None
let print_state _ _ () = ()
let print_expr _ _ _ _ _ = ()
end
(** Add a domain to a pool *)
module MakePairPool(S:STACKED_COMBINER)(P:POOL) : POOL with type t = S.t * P.t =
struct
type t = S.t * P.t
let id = C_pair(Product,S.id,P.id)
let domains = DomainSet.union S.domains P.domains
let members = S.domains :: P.members
let semantics = SemanticSet.union S.semantics P.semantics
let routing_table = join_routing_table S.routing_table P.routing_table
let checks = S.checks :: P.checks
let name = S.name ^ " ∧ " ^ P.name
let bottom = S.bottom, P.bottom
let top = S.top, P.top
let is_bottom (s,p) = S.is_bottom s || P.is_bottom p
let subset man ctx ((a1,a2),s) ((a1',a2'),s') =
let b1, s, s' = S.subset (fst_pair_man man) ctx (a1,s) (a1',s') in
let b2, s, s' = P.subset (snd_pair_man man) ctx (a2,s) (a2',s') in
b1 && b2, s, s'
let join man ctx ((a1,a2),s) ((a1',a2'),s') =
let aa1, s, s' = S.join (fst_pair_man man) ctx (a1,s) (a1',s') in
let aa2, s, s' = P.join (snd_pair_man man) ctx (a2,s) (a2',s') in
(aa1,aa2), s, s'
let meet man ctx ((a1,a2),s) ((a1',a2'),s') =
let aa1, s, s' = S.meet (fst_pair_man man) ctx (a1,s) (a1',s') in
let aa2, s, s' = P.meet (snd_pair_man man) ctx (a2,s) (a2',s') in
(aa1,aa2), s, s'
let widen man ctx ((a1,a2),s) ((a1',a2'),s') =
let aa1, s, s', stable1 = S.widen (fst_pair_man man) ctx (a1,s) (a1',s') in
let aa2, s, s', stable2 = P.widen (snd_pair_man man) ctx (a2,s) (a2',s') in
(aa1,aa2), s, s', stable1 && stable2
let merge path (pre1,pre2) ((a1,a2), te) ((a1',a2'), te') =
S.merge (Ax_pair_left::path) pre1 (a1, te) (a1', te'),
P.merge (Ax_pair_right::path) pre2 (a2, te) (a2', te')
let init prog man flow = broadcast_init S.init P.init prog man flow
let exec targets =
let f2 = P.exec targets in
if not (sat_targets ~targets ~domains:S.domains) then
(fun stmt man flow ->
None :: f2 stmt (snd_pair_man man) flow
)
else
let f1 = S.exec targets in
(fun stmt man flow ->
let post = f1 stmt (fst_pair_man man) flow in
let ctx = OptionExt.apply Cases.get_ctx (Flow.get_ctx flow) post in
let flow = Flow.set_ctx ctx flow in
post :: f2 stmt (snd_pair_man man) flow
)
let eval targets =
let f2 = P.eval targets in
if not (sat_targets ~targets ~domains:S.domains) then
(fun exp man flow ->
None :: f2 exp (snd_pair_man man) flow
)
else
let f1 = S.eval targets in
(fun exp man flow ->
let eval = f1 exp (fst_pair_man man) flow in
let ctx = OptionExt.apply Cases.get_ctx (Flow.get_ctx flow) eval in
let flow = Flow.set_ctx ctx flow in
eval :: f2 exp (snd_pair_man man) flow
)
let ask targets =
let f2 = P.ask targets in
if not (sat_targets ~targets ~domains:S.domains) then
(fun query man flow ->
f2 query (snd_pair_man man) flow
)
else
let f1 = S.ask targets in
(fun query man flow ->
OptionExt.neutral2
Cases.meet
(f1 query (fst_pair_man man) flow)
(f2 query (snd_pair_man man) flow))
let print_state targets =
let f2 = P.print_state targets in
if not (sat_targets ~targets ~domains:S.domains) then
(fun printer (s,p) ->
f2 printer p
)
else
let f1 = S.print_state targets in
(fun printer (s,p) ->
f1 printer s;
f2 printer p
)
let print_expr targets =
let f2 = P.print_expr targets in
if not (sat_targets ~targets ~domains:S.domains) then
(fun man flow printer e ->
f2 (snd_pair_man man) flow printer e
)
else
let f1 = S.print_expr targets in
(fun man flow printer e ->
f1 (fst_pair_man man) flow printer e;
f2 (snd_pair_man man) flow printer e
)
end
(** Create a reduced product over a pool and a list of reduction rules *)
module Make
(Pool:POOL)
(Rules:sig
val erules: (module EVAL_REDUCTION) list
val srules: (module EXEC_REDUCTION) list
end) : STACKED_COMBINER with type t = Pool.t =
struct
include Pool
let checks = List.flatten Pool.checks
let debug fmt = Debug.debug ~channel:"framework.combiners.domain.product" fmt
(** {2 Merging functions} *)
(** ********************* *)
let merge_report checks1 checks2 report1 report2 =
map2zo_report
(fun diag1 ->
if List.mem diag1.diag_check checks2 then
Exceptions.panic "%a: check %a is unsound"
pp_relative_range diag1.diag_range
pp_check diag1.diag_check
else diag1
)
(fun diag2 ->
if List.mem diag2.diag_check checks1 then
Exceptions.panic "%a: check %a is unsound"
pp_relative_range diag2.diag_range
pp_check diag2.diag_check
else diag2
)
(fun diag1 diag2 ->
match List.mem diag2.diag_check checks1, List.mem diag1.diag_check checks2 with
| true, true -> meet_diagnostic diag1 diag2
| true, false -> diag1
| false, true -> diag2
| false, false -> join_diagnostic diag1 diag2
) report1 report2
(** Merge the conflicts between distinct domains.
These conflicts arise from two situations:
1. When a domain changes its local state, this change is not present in
the post-state of the other domains. In this case, we need to put the new
local state of every domain in all other post-states.
2. When two domains change (independently) the state of a shared sub-abstraction.
In this case, we use chages to merge the two diverging states.
*)
let merge_inter_conflicts man pre range (pointwise:('a,'r) cases option list) : ('a,'r option list) cases =
let rec aux : type t. t id -> ('a,t) man -> ('a,'r) cases option list -> check list list -> ('a,'r option list) cases =
fun id man pointwise checks ->
match pointwise, id, checks with
| [None], C_pair(_, s, _), _ ->
Cases.return [None] pre
| [Some r], C_pair(_, s, _), _ ->
r >>= fun case flow ->
begin match case with
| Result(res,_,_) -> Cases.return [Some res] flow
| Empty -> Cases.empty flow
| NotHandled -> Cases.return [None] flow
end
| None :: tl, C_pair(_,s,pid), _::tlchecks ->
aux pid (snd_pair_man man) tl tlchecks >>$ fun after flow ->
Cases.return (None :: after) flow
| Some r :: tl, C_pair(_,s,pid), hdchecks::tlchecks ->
aux pid (snd_pair_man man) tl tlchecks >>= fun after_case after_flow ->
r >>= fun case flow ->
begin match case, after_case with
| Empty, _ | _, Empty ->
let report = merge_report hdchecks (List.flatten tlchecks) (Flow.get_report flow) (Flow.get_report after_flow) in
let flow = Flow.set_report report flow in
let after_flow = Flow.set_report report flow in
Cases.empty (Flow.meet man.lattice flow after_flow)
| NotHandled, Result(after_res,_,_) ->
Cases.return (None :: after_res) after_flow
| Result (res,changes,cleaners), Result(after_res,after_changes,after_cleaners) ->
if after_res |> List.exists (function Some _ -> true | None -> false) then
let post =
let fst_pair_man = fst_pair_man man in
fst_pair_man.get T_cur flow >>$ fun env flow ->
let partitions =
ask_and_reduce man.ask (Sig.Abstraction.Partitioning.Q_partition_predicate range) flow
~bottom:(fun () -> mk_constant (C_bool true) range ~etyp:T_bool)
in
man.exec (mk_assume partitions dummy_range) after_flow >>%
fst_pair_man.set T_cur env
in
Post.remove_duplicates man.lattice post >>% fun after_flow ->
let flow = Flow.merge ~merge_report:(merge_report hdchecks (List.flatten tlchecks)) man.lattice pre (flow,changes) (after_flow,after_changes) in
let changes = meet_change_map changes after_changes in
let cleaners = StmtSet.union cleaners after_cleaners in
Cases.case (Result (Some res :: after_res, changes, cleaners)) flow
else
let report = merge_report hdchecks (List.flatten tlchecks) (Flow.get_report flow) (Flow.get_report after_flow) in
let flow = Flow.set_report report flow in
Cases.case (Result (Some res :: after_res, changes, cleaners)) flow
| _ -> assert false
end
| _ -> assert false
in
aux Pool.id man pointwise Pool.checks
(** Merge the conflicts emerging from the same domain.
This kind of conflicts arises when the same domain produces a conjunction of
post-states. Since these conjunctions are from the same domain, there is
no need to merge its local state; we just merge any shared sub-abstraction.
*)
let merge_intra_conflicts man pre (r:('a,'r) cases) : ('a,'r) cases =
Cases.map_conjunction
(fun conj ->
let rec iter = function
| [] -> assert false
| [case,flow] -> Cases.get_case_changes case, Cases.get_case_cleaners case, flow
| (case,flow)::tl ->
let changes',cleaners',flow' = iter tl in
let changes,cleaners = Cases.get_case_changes case, Cases.get_case_cleaners case in
let flow'' = Flow.merge man.lattice ~merge_report:meet_report pre (flow,changes) (flow',changes') in
meet_change_map changes changes', StmtSet.union cleaners cleaners', flow''
in
let changes,cleaners,flow = iter conj in
List.map
(fun (case,_) ->
let case = Cases.set_case_changes changes case |>
Cases.set_case_cleaners cleaners in
case,flow
) conj
) r
(** {2 Generic pointwise processing of transfer functions *)
(** ***************************************************** *)
(** The successor domain is the domain below the reduced
product. Since all member domains in the reduced product are at the
same level, we can pick any one of them *)
let successor =
let member =
List.find (fun domains -> DomainSet.cardinal domains = 1) Pool.members |>
DomainSet.choose in
Below member
(** Get the context of a pointwise result *)
let rec get_pointwise_ctx ~default pointwise =
match pointwise with
| [] -> default
| None::tl -> get_pointwise_ctx ~default tl
| Some cases :: tl -> most_recent_ctx
(Cases.get_ctx cases)
(get_pointwise_ctx ~default tl)
(** Set the context of a pointwise result *)
let rec set_pointwise_ctx ctx pointwise =
match pointwise with
| [] -> []
| None :: tl -> None :: set_pointwise_ctx ctx tl
| Some cases :: tl -> Some (Cases.set_ctx ctx cases) :: set_pointwise_ctx ctx tl
(** Apply transfer function [f] pointwise over all domains *)
let apply_pointwise f arg remove_duplicates man flow =
let pointwise = f arg man flow in
let pointwise = List.map (function
| None -> None
| Some r -> Some (remove_duplicates man.lattice r)
) pointwise
in
if List.exists (function Some _ -> true | None -> false) pointwise
then
let ctx = get_pointwise_ctx pointwise ~default:(Flow.get_ctx flow) in
Some (set_pointwise_ctx ctx pointwise)
else None
(** Replace missing pointwise results by calling the successor
domain. Missing results are functions returning [None] or
[NotHandled] cases. *)
let add_missing_pointwise_results fsuccessor arg pointwise remove_duplicates man flow =
let handled_pointwise, not_handled =
List.fold_left
(fun (acc1,acc2) -> function
| None -> (None,true)::acc1,acc2
| Some r ->
let h,nh = Cases.partition (fun c _ -> match c with NotHandled -> false | _ -> true) r in
let acc1' = (h,(if nh = None then false else true))::acc1 in
let acc2' = OptionExt.neutral2 Cases.join nh acc2 in
acc1',acc2'
) ([],None) pointwise
in
let handled_pointwise = List.rev handled_pointwise in
let not_handled =
if List.exists (function None -> true | _ -> false) pointwise
then
OptionExt.neutral2 Cases.join not_handled (Some (Cases.not_handled flow))
else
not_handled
in
match not_handled with
| None -> pointwise
| Some cases ->
let successor_res =
remove_duplicates man.lattice cases >>= fun _ flow ->
fsuccessor arg flow |>
remove_duplicates man.lattice
in
let pointwise' =
List.map
(fun (r,has_not_handled_cases) ->
match r with
| None -> Some successor_res
| Some rr when not has_not_handled_cases -> Some rr
| Some rr -> Some (Cases.join rr successor_res)
) handled_pointwise
in
set_pointwise_ctx (Cases.get_ctx successor_res) pointwise'
(** {2 Abstract transformer} *)
(** ************************ *)
(** Manager used by reductions *)
let exec_reduction_man (man:('a, t) man) : 'a exec_reduction_man = {
get_man = (fun id -> find_domain_man ~target:id ~tree:Pool.id man);
}
(** Simplify a pointwise post-state by changing lists of unit into unit *)
let simplify_pointwise_post (pointwise:('a,unit option list) cases) : 'a post =
Cases.map_result (fun _ -> ()) pointwise
(** Apply reduction rules on a post-conditions *)
let reduce_post stmt man pre post =
let rman = exec_reduction_man man in
post |> Cases.bind @@ fun case flow ->
match case with
| Empty -> Cases.empty flow
| NotHandled -> Cases.not_handled flow
| Result((),changes,_) ->
let rec iter = function
| [] -> Post.return flow
| rule::tl ->
let module R = (val rule : EXEC_REDUCTION) in
match R.reduce stmt man rman pre flow changes with
| None -> iter tl
| Some post -> post
in
iter Rules.srules
(** Entry point of abstract transformers *)
let exec targets =
let f = Pool.exec targets in
(fun stmt man flow ->
with_change_tracker
(fun () ->
apply_pointwise f stmt Post.remove_duplicates man flow |>
OptionExt.lift @@ fun pointwise ->
add_missing_pointwise_results (man.exec ~route:successor) stmt pointwise Post.remove_duplicates man flow |>
merge_inter_conflicts man flow stmt.srange |>
simplify_pointwise_post |>
merge_intra_conflicts man flow |>
reduce_post stmt man flow
)
)
(** {2 Abstract evaluations} *)
(** ************************ *)
(** Manager used by reductions *)
let eval_reduction_man (man:('a, t) man) : 'a eval_reduction_man = {
get_man = (fun id -> find_domain_man ~target:id ~tree:Pool.id man);
}
(** Apply reduction rules on a pointwise evaluation *)
let reduce_pointwise_eval exp man input (pointwise:('a, expr option list) cases) : 'a eval =
pointwise >>$ fun el flow ->
let el' = List.filter (function Some _ -> true | _ -> false) el |>
List.map (function Some e -> e | _ -> assert false) |>
List.sort_uniq compare_expr
in
if el' = [] then Eval.empty flow
else
let rman = eval_reduction_man man in
let rec iter = function
| [] ->
Eval.singleton (List.hd el') flow
| rule::tl ->
let module R = (val rule : EVAL_REDUCTION) in
match R.reduce exp man rman input el' flow with
| None -> iter tl
| Some evl -> evl
in
iter Rules.erules
(** Entry point of abstract evaluations *)
let eval targets =
let f = Pool.eval targets in
(fun exp man flow ->
with_change_tracker
(fun () ->
apply_pointwise f exp Eval.remove_duplicates man flow |>
OptionExt.lift @@ fun pointwise ->
add_missing_pointwise_results (man.eval ~route:successor) exp pointwise Eval.remove_duplicates man flow |>
merge_inter_conflicts man flow exp.erange |>
reduce_pointwise_eval exp man flow |>
Eval.remove_duplicates man.lattice |>
merge_intra_conflicts man flow
)
)
end
let rec make_pool : (module STACKED_COMBINER) list -> (module POOL) = function
| [] -> (module EmptyPool)
| hd :: tl ->
let module S = (val hd) in
let p = make_pool tl in
(module MakePairPool(S)(val p))
let make
(domains: (module STACKED_COMBINER) list)
~(eval_rules: (module EVAL_REDUCTION) list)
~(exec_rules: (module EXEC_REDUCTION) list)
: (module STACKED_COMBINER) =
let p = make_pool domains in
(module Make(val p)
(struct
let erules = eval_rules
let srules = exec_rules
end)
)