package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file cases.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
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
(****************************************************************************)
(*                                                                          *)
(* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *)
(*                                                                          *)
(* Copyright (C) 2017-2019 The MOPSA Project.                               *)
(*                                                                          *)
(* This program is free software: you can redistribute it and/or modify     *)
(* it under the terms of the GNU Lesser General Public License as published *)
(* by the Free Software Foundation, either version 3 of the License, or     *)
(* (at your option) any later version.                                      *)
(*                                                                          *)
(* This program is distributed in the hope that it will be useful,          *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of           *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the            *)
(* GNU Lesser General Public License for more details.                      *)
(*                                                                          *)
(* You should have received a copy of the GNU Lesser General Public License *)
(* along with this program.  If not, see <http://www.gnu.org/licenses/>.    *)
(*                                                                          *)
(****************************************************************************)


(** Cases - Encoding of results returned by transfer functions. *)


open Mopsa_utils
open Ast.Stmt
open Flow
open Token
open Change
open Context
open Alarm
open Lattice

type cleaners = StmtSet.t

(** Single case of a computation *)
type 'r case =
  | Result of 'r * change_map * cleaners
  | Empty
  | NotHandled

(** Multiple cases of a computation, encoded as a DNF *)
type ('a,'r) cases = {cases: ('r case * 'a flow) Dnf.t;
                      ctx: 'a ctx}

let case (case:'r case) flow : ('a,'r) cases = {cases=Dnf.singleton (case,flow);
                                                ctx = Flow.get_ctx flow}

let return ?(changes=empty_change_map) ?(cleaners=[]) (res:'r) (flow:'a flow) =
  case (Result (res,changes,StmtSet.of_list cleaners)) flow

let singleton = return

let empty (flow:'a flow) : ('a,'r) cases =
  let flow = Flow.remove T_cur flow in
  case Empty flow

let not_handled (flow:'a flow) : ('a,'r) cases =
  case NotHandled flow


let opt_clean_cur_only = ref false


let get_ctx cases = cases.ctx

let set_ctx ctx cases =
  if ctx == get_ctx cases then
    cases
  else
    {cases=Dnf.map
      (fun (case,flow) -> (case, Flow.set_ctx ctx flow))
      cases.cases;
     ctx}

let copy_ctx src dst =
  set_ctx (get_ctx src) dst

let get_most_recent_ctx cases =
  Dnf.fold
    (fun acc (case,flow) -> most_recent_ctx acc (Flow.get_ctx flow))
    (get_ctx cases) cases.cases

let normalize_ctx cases =
  let ctx = get_most_recent_ctx cases in
  set_ctx ctx cases

let get_callstack r =
  get_ctx r |>
  find_ctx Context.callstack_ctx_key

let set_callstack cs r =
  set_ctx (
    get_ctx r |>
    add_ctx Context.callstack_ctx_key cs
  ) r

let get_case_cleaners (case:'r case) : StmtSet.t =
  match case with
  | Result(_,_,cleaners) -> cleaners
  | Empty | NotHandled   -> StmtSet.empty

let set_case_cleaners (cleaners:StmtSet.t) (case:'r case) : 'r case =
  match case with
  | Result(r,changes,_) -> Result(r,changes,cleaners)
  | _ -> case

let get_case_changes (case:'r case) : change_map =
  match case with
  | Result(_,changes,_)    -> changes
  | Empty | NotHandled -> empty_change_map

let set_case_changes (changes:change_map) (case:'r case) : 'r case =
  match case with
  | Result(r,old,cleaners) -> if old == changes then case else Result(r,changes,cleaners)
  | _ -> case


let is_singleton cases =
  match Dnf.to_list cases.cases with
  | [[_]] -> true
  | _ -> false

let choose cases =
  match Dnf.choose cases.cases with
  | Some (case, flow) -> case, flow
  | None -> invalid_arg "Cases.choose"

let choose_result cases =
  let case, flow = choose cases in
  match case with
  | Result(r, _, _) -> r, flow
  | _               -> invalid_arg "Cases.choose_result"

let map
    (f:'r case -> 'a flow -> 's case * 'a flow)
    (cases:('a,'r) cases)
  : ('a,'s) cases =
  {cases=Dnf.map (fun (case,flow) -> f case flow) cases.cases; ctx=cases.ctx} |>
  normalize_ctx


let map_result
    (f:'r->'s)
    (cases:('a,'r) cases)
  : ('a,'s) cases =
  map (fun case flow ->
      let case' =
        match case with
        | Result (r,changes,cleaners) -> Result (f r,changes,cleaners)
        | Empty                   -> Empty
        | NotHandled              -> NotHandled
      in
      (case',flow)
    ) cases

let map_conjunction
    (f:('r case * 'a flow) list -> ('s case * 'a flow) list)
    (cases:('a,'r) cases)
  : ('a,'s) cases =
  {cases=Dnf.map_conjunction f cases.cases; ctx=cases.ctx} |>
  normalize_ctx

let map_disjunction
    (f:('r case * 'a flow) list -> ('s case * 'a flow) list)
    (cases:('a,'r) cases)
  : ('a,'s) cases =
  {cases=Dnf.map_disjunction f cases.cases; ctx=cases.ctx} |>
  normalize_ctx


let reduce
    (f:'r case -> 'a flow -> 'b)
    ~(join:'b -> 'b -> 'b)
    ~(meet:'b -> 'b -> 'b)
    (cases:('a,'r) cases)
  : 'b =
  Dnf.reduce (fun (case,flow) -> f case flow) ~join ~meet cases.cases

let reduce_result
    (f:'r -> 'a flow -> 'b)
    ~(join:'b -> 'b -> 'b)
    ~(meet:'b -> 'b -> 'b)
    ~(bottom:unit -> 'b)
    (cases:('a,'r) cases)
  : 'b =
  reduce
    (fun case flow ->
       match case with
       | Result (r,changes,cleaners) -> f r flow
       | Empty | NotHandled      -> bottom ()
    ) ~join ~meet cases


let print pp fmt cases =
  Dnf.print (fun fmt (case,flow) -> pp fmt case flow) fmt cases.cases


let print_result pp fmt cases =
  print (fun fmt case flow ->
      match case with
      | Result (r,_,_) -> pp fmt r flow
      | Empty          -> Format.fprintf fmt "ε"
      | NotHandled     -> Format.fprintf fmt "✗"
    )
    fmt cases


let map_changes
    (f:change_map -> 'a flow -> change_map)
    (cases:('a,'r) cases)
  : ('a,'r) cases =
  map
    (fun case flow ->
       match case with
       | Result(r,changes,cleaners) ->
         let changes' = f changes flow in
         Result(r,changes',cleaners), flow
       | _ -> case, flow
    ) cases

let set_changes
    (changes:change_map)
    (cases:('a,'r) cases)
  : ('a,'r) cases =
  map
    (fun case flow ->
       match case with
       | Result(r,old,cleaners) -> if old == changes then (case,flow) else (Result(r,changes,cleaners), flow)
       | _                      -> case, flow
    ) cases

let set_cleaners
    (cleaners:stmt list)
    (cases:('a,'r) cases)
  : ('a,'r) cases =
  let cleaners = StmtSet.of_list cleaners in
  map
    (fun case flow ->
       match case with
       | Result(r,changes,_) -> Result(r,changes,cleaners), flow
       | _                  -> case, flow
    ) cases


let concat_changes
    (old:change_map)
    (cases:('a,'r) cases)
  : ('a,'r) cases =
  map
    (fun case flow ->
       match case with
       | Result(r,recent,cleaners) ->
         (* Add changes of non-empty environments only *)
         (* FIXME: Since are always called from the binders, we can't
              require having the lattice manager. So we can't test if
              T_cur is ⊥ or not! For the moment, we rely on empty flow
              maps, but this is not always sufficient.
         *)
         if Flow.mem T_cur flow then
           Result(r, concat_change_map old recent, cleaners), flow
         else
           case, flow
       | _ -> case, flow
    ) cases

let add_cleaners
    (cleaners:stmt list)
    (cases:('a,'r) cases)
  : ('a,'r) cases =
  let cleaners = StmtSet.of_list cleaners in
  map
    (fun case flow ->
       match case with
       | Result(r,changes,cleaners') -> Result(r,changes,StmtSet.union cleaners' cleaners), flow
       | _ -> case, flow
    ) cases

let fold
    (f:'b -> 'r case -> 'a flow -> 'b)
    (init:'b)
    (cases:('a,'r) cases)
  : 'b =
  Dnf.fold (fun acc (case,flow) -> f acc case flow) init cases.cases


let fold_result
    (f:'b -> 'r -> 'a flow -> 'b)
    (init:'b)
    (cases:('a,'r) cases)
  : 'b =
  fold
    (fun acc case flow ->
       match case with
       | Result (r,_,_)     -> f acc r flow
       | Empty | NotHandled -> acc
    ) init cases

let iter
    (f:'r case -> 'a flow -> unit)
    (cases:('a,'r) cases)
  : unit =
  Dnf.iter (fun (case,flow) -> f case flow) cases.cases


let iter_result
    (f:'r -> 'a flow -> unit)
    (cases:('a,'r) cases)
  : unit =
  iter
    (fun case flow ->
       match case with
       | Result (r,_,_)     -> f r flow
       | Empty | NotHandled -> ()
    ) cases

let partition
    (f:'r case -> 'a flow -> bool)
    (cases:('a,'r) cases)
  : ('a,'r) cases option * ('a,'r) cases option =
  let oc1, oc2 = Dnf.partition (fun (case,flow) -> f case flow) cases.cases in
  OptionExt.lift (fun c -> {cases=c; ctx=cases.ctx}) oc1,
  OptionExt.lift (fun c -> {cases=c; ctx=cases.ctx}) oc2

let flatten (cases:('a,'r) cases) : ('r case * 'a flow) list =
  Dnf.to_list cases.cases |>
  List.flatten

let for_all
    (f:'r case -> 'a flow -> bool)
    (cases:('a,'r) cases)
  : bool =
  flatten cases |>
  List.for_all (fun (case,flow) -> f case flow)

let for_all_result
    (f:'r -> 'a flow -> bool)
    (cases:('a,'r) cases)
  : bool =
  for_all
    (fun case flow ->
      match case with
      | Result (r,_,_)     -> f r flow
      | Empty | NotHandled -> true
    ) cases


let exists
    (f:'r case -> 'a flow -> bool)
    (cases:('a,'r) cases)
  : bool =
  flatten cases |>
  List.exists (fun (case,flow) -> f case flow)

let exists_result
    (f:'r -> 'a flow -> bool)
    (cases:('a,'r) cases)
  : bool =
  exists
    (fun case flow ->
      match case with
      | Result (r,_,_)     -> f r flow
      | Empty | NotHandled -> false
    ) cases


(** Join two results *)
let join (cases1:('a,'r) cases) (cases2:('a,'r) cases) : ('a,'r) cases =
  if cases1 == cases2 then cases1 else
  if for_all (fun _ flow -> Flow.is_empty flow) cases1 then cases2 else
  if for_all (fun _ flow -> Flow.is_empty flow) cases2 then cases1
  else
    {cases=Dnf.mk_or cases1.cases cases2.cases; ctx=cases1.ctx} |>
    normalize_ctx

(** Meet two results *)
let meet (cases1:('a,'r) cases) (cases2:('a,'r) cases) : ('a,'r) cases =
  {cases=Dnf.mk_and cases1.cases cases2.cases; ctx=cases1.ctx} |>
  normalize_ctx


(** Join a list of results *)
let join_list ~empty (l: ('a,'r) cases list) : ('a,'r) cases =
  match l with
  | [] -> empty ()
  | hd :: tl -> List.fold_left join hd tl


(** Meet a list of results *)
let meet_list ~empty (l: ('a,'r) cases list) : ('a,'r) cases =
  match l with
  | [] -> empty ()
  | hd :: tl -> List.fold_left meet hd tl


let equal_case c1 c2 =
  c1 == c2 ||
  match c1, c2 with
  | Result(r1, _, _), Result(r2, _, _) -> r1 == r2
  | Empty, Empty -> true
  | NotHandled, NotHandled -> true
  | _ -> false

let remove_duplicates ?(equal=equal_case) (lattice: 'a Lattice.lattice) (cases: ('a, 'r) cases): ('a, 'r) cases =
  (* Remove duplicates of a case in a conjunction *)
  let rec remove_case_duplicates_in_conj case flow conj =
    match conj with
    | [] -> case, flow, []
    | (case',flow') :: tl' ->
      let case'', flow'', tl'' = remove_case_duplicates_in_conj case flow tl' in
      if equal case case' then
        let flow = Flow.meet lattice flow' flow'' in
        let case =
          match case, case' with
          | Empty, Empty
          | NotHandled, NotHandled
          | Empty, NotHandled
          | NotHandled, Empty ->
            case

          | Result _, Empty
          | Result _, NotHandled ->
            case

          | Empty, Result _
          | NotHandled, Result _ ->
            case'

          | Result(r, changes, cleaners), Result(r', changes', cleaners') ->
            let cleaners = StmtSet.union cleaners cleaners' in
            let changes = meet_change_map changes changes' in
            Result(r, changes, cleaners)
        in
        case,flow,tl''
      else
        case'', flow'', (case',flow')::tl''
  in
  (* Remove all duplicates in a conjunction *)
  let rec remove_duplicates_in_conj conj =
    match conj with
    | [] -> []
    | [(case,flow)] -> conj
    | (case,flow) :: tl ->
      (* Remove duplicates of case from tl *)
      let case', flow', tl' = remove_case_duplicates_in_conj case flow tl in
      (case',flow') :: remove_duplicates_in_conj tl'
  in
  (* Remove duplicates of a conjunction in a disjunction *)
  let rec remove_conj_duplicates_in_disj conj disj =
    match disj with
    | [] -> conj, []
    | conj'::tl ->
      let conj'', tl' = remove_conj_duplicates_in_disj conj tl in
      if List.equal (fun (c,_) (c',_) -> equal c c') conj' conj'' then
        let conj =
          List.combine conj' conj'' |>
          List.map
            (fun ((case,flow), (case',flow')) ->
               let flow = Flow.join lattice flow flow' in
               match case, case' with
               | Empty, Empty
               | NotHandled, NotHandled
               | Empty, NotHandled
               | NotHandled, Empty ->
                 case, flow
                 
               | Result _, Empty
               | Result _, NotHandled ->
                 case, flow

               | Empty, Result _
               | NotHandled, Result _ ->
                 case', flow

               | Result(r, changes, cleaners), Result(r', changes', cleaners') ->
                 let cleaners = StmtSet.union cleaners cleaners' in
                 let changes = join_change_map changes changes' in
                 let case = Result(r, changes, cleaners) in
                 case, flow
            )
        in
        conj,tl'
      else
        conj'',conj'::tl'
  in
  let rec remove_duplicates_in_disj = function
    | [] -> []
    | [[e]] as x -> x
    | [conj] -> [remove_duplicates_in_conj conj]
    | conj::tl ->
      let conj = remove_duplicates_in_conj conj in
      let conj',tl' = remove_conj_duplicates_in_disj conj tl in
      conj'::remove_duplicates_in_disj tl'
  in
  let cases' = Dnf.from_list (remove_duplicates_in_disj (Dnf.to_list cases.cases)) in
  {cases with cases=cases'}

let remove_duplicate_results ?(equal=(==)) lattice cases =
  remove_duplicates
    ~equal:(fun case case' ->
       match case, case' with
       | Result(r,_,_), Result(r',_,_) -> equal r r'
       | _                             -> compare case case' = 0
    ) lattice cases


let cardinal cases = Dnf.cardinal cases.cases


(****************************************************************************)
(**                        {2 Monadic binders}                              *)
(****************************************************************************)

let bind_opt
    (f: 'r case -> 'a flow -> ('a,'s) cases option )
    (cases: ('a,'r) cases)
  : ('a,'s) cases option =
  match Dnf.to_list cases.cases with
  | [[Result(_, changes, cleaners) as case, flow]]
    when StmtSet.is_empty cleaners && 
         (not (is_change_tracker_enabled ()) || is_empty_change_map changes) ->
    f case flow

  | [[case, flow]] -> (
      match f case flow with
      | None -> None
      | Some cases' ->
        add_cleaners (get_case_cleaners case |> StmtSet.elements) cases' |>
        concat_changes (get_case_changes case) |>
        Option.some
    )
  
  | _ ->
    let (ctx,handled),ret =
      Dnf.fold_bind
        (fun (ctx,handled) (case,flow) ->
           let flow = Flow.set_ctx ctx flow in
           let cases', handled' =
             match f case flow with
             | None   -> not_handled flow, handled
             | Some c -> c, true
           in
           let ctx' = get_ctx cases' in
           let cases'' = add_cleaners (get_case_cleaners case |> StmtSet.elements) cases' |>
                         concat_changes (get_case_changes case) in
           (ctx',handled'), cases''.cases
        )
        (get_ctx cases,false) cases.cases in
    if handled then
      set_ctx ctx {cases with cases = ret} |>
      OptionExt.return
    else
      None


let (>>=?) cases f = bind_opt f cases

let bind f cases =
  match Dnf.to_list cases.cases with
  | [[Result(_, changes, cleaners) as case, flow]]
    when StmtSet.is_empty cleaners && 
         (not (is_change_tracker_enabled ()) || is_empty_change_map changes) ->
    f case flow

  | [[case, flow]] ->
    let cases' = f case flow in
    add_cleaners (get_case_cleaners case |> StmtSet.elements) cases' |>
    concat_changes (get_case_changes case)
  
  | _ ->
    bind_opt (fun case flow -> Some (f case flow)) cases |>
    OptionExt.none_to_exn

let (>>=) cases f = bind f cases


let bind_result_opt
    (f:'r -> 'a flow -> ('a,'s) cases option)
    (cases:('a,'r) cases)
  : ('a,'s) cases option
  =
  match Dnf.to_list cases.cases with
  | [[Result(r, changes, cleaners), flow]]
    when StmtSet.is_empty cleaners && 
         (not (is_change_tracker_enabled ()) || is_empty_change_map changes) ->
    f r flow

  | [[Result(r, changes, cleaners), flow]] -> (
      match f r flow with
      | None -> None
      | Some cases' ->
        add_cleaners (StmtSet.elements cleaners) cases' |>
        concat_changes changes |>
        Option.some
    )
  
  | _ ->
    bind_opt
      (fun case flow ->
         match case with
         | Result (r,_,_)   -> f r flow
         | Empty            -> Some (empty flow)
         | NotHandled       -> Some (not_handled flow)
      ) cases


let (>>$?) r f = bind_result_opt f r


let bind_result
    (f:'r -> 'a flow -> ('a,'s) cases)
    (cases:('a,'r) cases)
  : ('a,'s) cases
  =
  match Dnf.to_list cases.cases with
  | [[Result(r, changes, cleaners), flow]]
    when StmtSet.is_empty cleaners && 
         (not (is_change_tracker_enabled ()) || is_empty_change_map changes) ->
    f r flow

  | [[Result(r, changes, cleaners), flow]] ->
    let cases' = f r flow in
    add_cleaners (StmtSet.elements cleaners) cases' |>
    concat_changes changes
  
  | _ ->
    bind_result_opt (fun r flow -> Some (f r flow)) cases |>
    OptionExt.none_to_exn


let (>>$) r f = bind_result f r
let ( let* ) r f = bind_result f r

let bind_conjunction
    (f:('r case * 'a flow) list -> ('a,'s) cases)
    (cases:('a,'r) cases)
  : ('a,'s) cases =
  let ctx,ret =
    Dnf.fold_bind_conjunction
      (fun ctx conj ->
         let conj' = List.map (fun (case,flow) -> (case,Flow.set_ctx ctx flow)) conj in
         let cases' = f conj' in
         let ctx' = get_ctx cases' in
         ctx',cases'.cases
      ) (get_ctx cases) cases.cases in
  set_ctx ctx {cases with cases=ret}

let bind_conjunction_result
    (f:'r list -> 'a flow -> ('a,'s) cases)
    (lattice:'a lattice)
    (cases:('a,'r) cases)
  : ('a,'s) cases =
  bind_conjunction
    (fun conj ->
       (* Separate cases actual results from empty and not-handled cases *)
       let handled,others = List.partition (fun (case,flow) -> match case with Result _ -> true | _ -> false) conj in
       (* This is a hack to change the type of others from 'r case to 's case *)
       let others = List.map (fun (case,flow) -> match case with NotHandled -> NotHandled,flow | Empty -> Empty,flow | _ -> assert false) others in
       if handled = [] then
         meet_list (List.map (fun (c,flow) -> case c flow) others) ~empty:(fun () -> assert false)
       else
         let cl,fl = List.split handled in
         let flow = List.fold_left (Flow.meet lattice) (List.hd fl) (List.tl fl) in
         let rl,changes,cleaners =
           List.fold_left
             (fun (acc1,acc2,acc3) case ->
                match case with
                | Result(r,changes,cleaners) -> r::acc1,meet_change_map acc2 changes,StmtSet.union acc3 cleaners
                | _ -> assert false
             ) ([],empty_change_map,StmtSet.empty) cl in
         let handled_res = f rl flow |>
                           add_cleaners (StmtSet.elements cleaners) |>
                           concat_changes changes in
         if others = [] then
           handled_res
         else
           meet_list (List.map (fun (c,flow) -> case c flow) others) ~empty:(fun () -> assert false) |>
           meet handled_res
    ) cases

let bind_disjunction
    (f:('r case * 'a flow) list -> ('a,'s) cases)
    (cases:('a,'r) cases)
  : ('a,'s) cases =
  let ctx,ret =
    Dnf.fold_bind_disjunction
      (fun ctx disj ->
         let disj' = List.map (fun (case,flow) -> (case,Flow.set_ctx ctx flow)) disj in
         let cases' = f disj' in
         let ctx' = get_ctx cases' in
         ctx',cases'.cases
      ) (get_ctx cases) cases.cases in
  set_ctx ctx {cases with cases=ret}

let bind_disjunction_result
    (f:'r list -> 'a flow -> ('a,'s) cases)
    (lattice:'a lattice)
    (cases:('a,'r) cases)
  : ('a,'s) cases =
  bind_disjunction
    (fun disj ->
       (* Separate cases actual results from empty and not-handled cases *)
       let handled,others = List.partition (fun (case,flow) -> match case with Result _ -> true | _ -> false) disj in
       (* This is a hack to change the type of others from 'r case to 's case *)
       let others = List.map (fun (case,flow) -> match case with NotHandled -> NotHandled,flow | Empty -> Empty,flow | _ -> assert false) others in
       if handled = [] then
         join_list (List.map (fun (c,flow) -> case c flow) others) ~empty:(fun () -> assert false)
       else
         let cl,fl = List.split handled in
         let flow = List.fold_left (Flow.join lattice) (List.hd fl) (List.tl fl) in
         let rl,changes,cleaners =
           List.fold_left
             (fun (acc1,acc2,acc3) case ->
                match case with
                | Result(r,changes,cleaners) -> r::acc1,join_change_map acc2 changes,StmtSet.union acc3 cleaners
                | _ -> assert false
             ) ([],empty_change_map,StmtSet.empty) cl in
         let handled_res = f rl flow |>
                           add_cleaners (StmtSet.elements cleaners) |>
                           concat_changes changes in
         if others = [] then
           handled_res
         else
           join_list (List.map (fun (c,flow) -> case c flow) others) ~empty:(fun () -> assert false) |>
           join handled_res
    ) cases


let bind_list_opt
    (l:'r list)
    (f:'r -> 'a flow -> ('a,'s) cases option)
    (flow:'a flow)
  : ('a, 's list) cases option
  =
  let rec aux l flow =
    match l with
    | e :: tl ->
      f e flow |>
      OptionExt.absorb @@ bind_result_opt @@ fun e' flow ->
      aux tl flow |>
      OptionExt.lift @@ bind_result @@ fun tl' flow ->
      return (e'::tl') flow


    | [] ->
      return [] flow |>
      OptionExt.return
  in
  aux l flow


let bind_list l f flow =
  bind_list_opt l (fun e flow -> Some (f e flow)) flow |>
  OptionExt.none_to_exn
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct