package mopsa

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

Source file alarm.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
(****************************************************************************)
(*                                                                          *)
(* 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/>.    *)
(*                                                                          *)
(****************************************************************************)

open Mopsa_utils
open Lattice
open Location
open Callstack
open Format


(** {1 Checks} *)
(** ********** *)

type check = ..

let check_print_chain : check TypeExt.print_chain =
  TypeExt.mk_print_chain (fun _ _ -> Exceptions.panic "Print of unregistered check")

let pp_check fmt c =
  TypeExt.print check_print_chain fmt c

let compare_check = compare

let register_check f =
  TypeExt.register_print f check_print_chain


(** {1 Alarms} *)
(** ********** *)

type alarm_kind = ..

type alarm_kind += A_generic of check

type alarm = {
  alarm_kind      : alarm_kind;
  alarm_check     : check;
  alarm_range     : range;
  alarm_callstack : callstack;
}

let alarm_compare_chain : alarm_kind TypeExt.compare_chain =
  TypeExt.mk_compare_chain
    (fun a1 a2 ->
       match a1,a2 with
       | A_generic chk1, A_generic chk2 -> compare chk1 chk2
       | _ -> compare a1 a2)

let alarm_print_chain : alarm_kind TypeExt.print_chain =
  TypeExt.mk_print_chain
    (fun fmt -> function
       | A_generic chk -> pp_check fmt chk
       | _ -> Exceptions.panic "Print of unregistered alarm")

let alarm_check_chain : (alarm_kind -> check) ref =
  ref (function
      | A_generic chk -> chk
      | _ -> Exceptions.panic "Check of unregistered alarm")

let alarm_join_chain : (alarm_kind -> alarm_kind -> alarm_kind option) ref =
  ref (fun a1 a2 -> None)

let compare_alarm_kind a1 a2 =
  TypeExt.compare alarm_compare_chain a1 a2

let pp_alarm_kind fmt a =
  TypeExt.print alarm_print_chain fmt a

let join_alarm_kind a1 a2 =
  !alarm_join_chain a1 a2

let compare_alarm a1 a2 =
  Compare.quadruple
    compare_alarm_kind compare_callstack compare_range compare_check
    (a1.alarm_kind,a1.alarm_callstack,a1.alarm_range,a1.alarm_check)
    (a2.alarm_kind,a2.alarm_callstack,a2.alarm_range,a2.alarm_check)

let pp_alarm fmt a =
  pp_alarm_kind fmt a.alarm_kind

let register_alarm_compare f =
  TypeExt.register_compare f alarm_compare_chain

let register_alarm_pp f =
  TypeExt.register_print f alarm_print_chain

let register_alarm_check f =
  alarm_check_chain := f !alarm_check_chain

let register_alarm_join f =
  alarm_join_chain := f !alarm_join_chain

type alarm_info = {
  check : (alarm_kind -> check) -> alarm_kind -> check;
  compare : (alarm_kind -> alarm_kind -> int) -> alarm_kind -> alarm_kind -> int;
  print : (formatter -> alarm_kind -> unit) -> formatter -> alarm_kind -> unit;
  join : (alarm_kind -> alarm_kind -> alarm_kind option) -> alarm_kind -> alarm_kind -> alarm_kind option;
}

let register_alarm info =
  register_alarm_check info.check;
  register_alarm_pp info.print;
  register_alarm_compare info.compare;
  register_alarm_join info.join

let check_of_alarm a = a.alarm_check

let range_of_alarm a = a.alarm_range

let callstack_of_alarm a = a.alarm_callstack

let mk_alarm kind callstack range =
  { alarm_kind      = kind;
    alarm_check     = !alarm_check_chain kind;
    alarm_range     = range;
    alarm_callstack = callstack }


(** {1 Diagnostic} *)
(** ************** *)

module AlarmSet = SetExt.Make(struct type t = alarm let compare = compare_alarm end)

let pp_alarm_set fmt a =
  match AlarmSet.elements a with
  | []  -> pp_print_string fmt "∅"
  | [a] -> pp_alarm fmt a
  | l   ->
    fprintf fmt "@[<v>{ %a }@]"
      (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@,")
         pp_alarm
      ) l

type diagnostic_kind =
  | Warning
  | Safe
  | Error
  | Unreachable

type 'a diagnostic_ = {
  diag_range : range;
  diag_check : check;
  diag_kind : diagnostic_kind;
  diag_alarms : AlarmSet.t;
  diag_callstack : 'a;
}

type diagnostic = callstack diagnostic_
type diagnosticWoCs = unit diagnostic_

let mk_safe_diagnostic check callstack range =
  { diag_range = range;
    diag_check = check;
    diag_kind = Safe;
    diag_alarms = AlarmSet.empty;
    diag_callstack = callstack }

let mk_unreachable_diagnostic check callstack range =
  { diag_range = range;
    diag_check = check;
    diag_kind = Unreachable;
    diag_alarms = AlarmSet.empty;
    diag_callstack = callstack }

let mk_error_diagnostic alarm =
  { diag_range = alarm.alarm_range;
    diag_check = alarm.alarm_check;
    diag_kind = Error;
    diag_alarms = AlarmSet.singleton alarm;
    diag_callstack = alarm.alarm_callstack }

let mk_warning_diagnostic check callstack range =
  { diag_range = range;
    diag_check = check;
    diag_kind = Warning;
    diag_alarms = AlarmSet.empty;
    diag_callstack = callstack }

let pp_diagnostic_kind fmt = function
  | Warning   -> pp_print_string fmt "warning"
  | Safe      -> pp_print_string fmt "safe"
  | Error     -> pp_print_string fmt "error"
  | Unreachable -> pp_print_string fmt "unreachable"

let pp_diagnostic fmt d =
  match d.diag_kind with
  | Safe | Unreachable ->
    pp_diagnostic_kind fmt d.diag_kind
  | Error | Warning ->
    fprintf fmt "%a: %a"
      pp_diagnostic_kind d.diag_kind
      pp_alarm_set d.diag_alarms

let subset_diagnostic_kind s1 s2 =
  if s1 == s2 then true else
  match s1,s2 with
  | Unreachable, _ -> true
  | _, Unreachable -> false
  | _, Warning     -> true
  | Warning, _     -> false
  | Error, Error   -> true
  | Safe, Safe     -> true
  | Error,Safe     -> false
  | Safe,Error     -> false


let subset_diagnostic d1 d2 =
  if d1 == d2 then true else
  subset_diagnostic_kind d1.diag_kind d2.diag_kind
  && AlarmSet.subset d1.diag_alarms d2.diag_alarms
  && compare_callstack d1.diag_callstack d2.diag_callstack = 0

let join_diagnostic_kind s1 s2 =
  if s1 == s2 then s1 else
  match s1,s2 with
  | Unreachable, x | x, Unreachable  -> x
  | Warning, x     | x, Warning      -> Warning
  | Error, Error                     -> Error
  | Safe, Safe                       -> Safe
  | Error, Safe    | Safe, Error     -> Warning


let join_diagnostic d1 d2 =
  if d1 == d2 then d1 else
  if subset_diagnostic d1 d2 then d2 else
  if subset_diagnostic d2 d1 then d1
  else (
    assert(compare_range d1.diag_range d2.diag_range = 0);
    assert(compare_check d1.diag_check d2.diag_check = 0);
    assert(compare_callstack d1.diag_callstack d2.diag_callstack = 0);
    { diag_range = d1.diag_range;
      diag_check = d1.diag_check;
      diag_kind = join_diagnostic_kind d1.diag_kind d2.diag_kind;
      diag_alarms = AlarmSet.union d1.diag_alarms d2.diag_alarms;
      diag_callstack = d1.diag_callstack;
    }
  )

let meet_diagnostic_kind s1 s2 =
  if s1 == s2 then s1 else
  match s1,s2 with
  | Unreachable, _ | _, Unreachable  -> Unreachable
  | Warning, x     | x, Warning      -> x
  | Error, Error                     -> Error
  | Safe, Safe                       -> Safe
  | Error, Safe    | Safe, Error     -> Exceptions.panic "unsound intersection of diagnostics"

let meet_diagnostic d1 d2 =
  if d1 == d2 then d1 else
  if subset_diagnostic d1 d2 then d1 else
  if subset_diagnostic d2 d1 then d2
  else (
    assert(compare_range d1.diag_range d2.diag_range = 0);
    assert(compare_check d1.diag_check d2.diag_check = 0);
    assert(compare_callstack d1.diag_callstack d2.diag_callstack = 0);
    (* It is currently unsound for one domain to remove alarms raised by
       another domain during reduction, because a "safe" check in a domain
       may correspond to a previous instance of the check at the same range
       and there is actually no information for the current instance in
       the domain.
       The current fix is to perform a union instead of an intersection of
       alarms during reduction. It is sound but imprecise.
       See MR!51 for more details.
       FIXME: implement a better fix, performing intersections when sound
     *)
    { diag_range = d1.diag_range;
      diag_check = d1.diag_check;
      diag_kind = meet_diagnostic_kind d1.diag_kind d2.diag_kind;
      diag_alarms = AlarmSet.union d1.diag_alarms d2.diag_alarms;
      diag_callstack = d1.diag_callstack
    }
  )

let add_alarm_to_diagnostic a d =
  assert(compare_callstack d.diag_callstack a.alarm_callstack = 0);
  match d.diag_kind with
  | Error ->
    { d with diag_alarms = AlarmSet.add a d.diag_alarms; }

  | Warning ->
    { d with diag_alarms = AlarmSet.add a d.diag_alarms; }

  | Safe ->
    { d with diag_kind = Error;
             diag_alarms = AlarmSet.singleton a;
    }

  | Unreachable ->
    { d with diag_kind = Error;
             diag_alarms = AlarmSet.singleton a;
    }

let compare_diagnostic d1 d2 =
  Compare.quadruple
    compare_range compare_check compare (Compare.pair AlarmSet.compare compare_callstack)
    (d1.diag_range,d1.diag_check,d1.diag_kind,(d1.diag_alarms,d1.diag_callstack))
    (d2.diag_range,d2.diag_check,d2.diag_kind,(d2.diag_alarms,d2.diag_callstack))

(** {1 Soundness assumption} *)
(** ************************ *)

type assumption_scope =
  | A_local of range
  | A_global

type assumption_kind = ..

type assumption_kind += A_ignore_unsupported_stmt of Ast.Stmt.stmt
type assumption_kind += A_ignore_unsupported_expr of Ast.Expr.expr

type assumption = {
  assumption_scope : assumption_scope;
  assumption_kind  : assumption_kind;
}

let assumption_compare_chain : assumption_kind TypeExt.compare_chain =
  TypeExt.mk_compare_chain
    (fun a1 a2 ->
       match a1,a2 with
       | A_ignore_unsupported_stmt s1, A_ignore_unsupported_stmt s2 ->
         Ast.Stmt.compare_stmt s1 s2

       | A_ignore_unsupported_expr e1, A_ignore_unsupported_expr e2 ->
         Ast.Expr.compare_expr e1 e2

       | _ -> compare a1 a2
    )


let assumption_print_chain : assumption_kind TypeExt.print_chain =
  TypeExt.mk_print_chain
    (fun fmt -> function
       | A_ignore_unsupported_stmt s ->
         Format.fprintf fmt "ignoring unsupported statement '%a'"
           (Debug.bold Ast.Stmt.pp_stmt) s

       | A_ignore_unsupported_expr e ->
         Format.fprintf fmt "ignoring unsupported expression '%a'"
           (Debug.bold Ast.Expr.pp_expr) e

       | _ -> Exceptions.panic "Print of unregistered assumption"
    )

let register_assumption info =
  TypeExt.register info assumption_compare_chain assumption_print_chain

let pp_assumption_kind fmt h =
  TypeExt.print assumption_print_chain fmt h

let pp_assumption fmt h =
  match h.assumption_scope with
  | A_global      -> pp_assumption_kind fmt h.assumption_kind
  | A_local range -> fprintf fmt "%a: %a"
                       pp_relative_range range
                       pp_assumption_kind h.assumption_kind

let compare_assumption_kind h1 h2 =
  TypeExt.compare assumption_compare_chain h1 h2

let compare_assumption h1 h2 =
  Compare.pair
    (fun scope1 scope2 ->
       match scope1, scope2 with
       | A_global, A_global     -> 0
       | A_local r1, A_local r2 -> compare_range r1 r2
       | _ -> compare scope1 scope2 )
    compare_assumption_kind
    (h1.assumption_scope, h1.assumption_kind)
    (h2.assumption_scope, h2.assumption_kind)

let mk_global_assumption kind =
  { assumption_scope = A_global;
    assumption_kind = kind }

let mk_local_assumption kind range =
  { assumption_scope = A_local range;
    assumption_kind = kind }

(** {1 Alarms report} *)
(** ***************** *)

module RangeMap = MapExt.Make(struct
    type t = range
    let compare = compare_range
  end)

module RangeCallStackMap = MapExt.Make(struct type t = range * callstack
    let compare = Compare.pair compare_range compare_callstack end)

module CheckMap = MapExt.Make(struct type t = check let compare = compare end)

module AssumptionSet = SetExt.Make(struct type t = assumption let compare = compare_assumption end)

type report = {
  report_diagnostics : diagnostic CheckMap.t RangeCallStackMap.t;
  report_assumptions : AssumptionSet.t;
}

let empty_report = {
  report_diagnostics = RangeCallStackMap.empty;
  report_assumptions = AssumptionSet.empty;
}

let is_empty_report r = RangeCallStackMap.is_empty r.report_diagnostics

let is_safe_report r =
  RangeCallStackMap.for_all
    (fun range checks ->
       CheckMap.for_all
         (fun check diag ->
            match diag.diag_kind with
            | Safe  | Unreachable  -> true
            | Error | Warning      -> false
         ) checks
    ) r.report_diagnostics

let is_sound_report r =
  AssumptionSet.is_empty r.report_assumptions

let singleton_report alarm =
  let diag = mk_error_diagnostic alarm in
  let checks = CheckMap.singleton alarm.alarm_check diag in
  { report_diagnostics = RangeCallStackMap.singleton (alarm.alarm_range, alarm.alarm_callstack) checks;
    report_assumptions = AssumptionSet.empty; }

let pp_report fmt r =
  fprintf fmt "@[<v>assumptions: @[<v>%a@]@,%a@]"
    (AssumptionSet.fprint
       SetExtSig.{ print_empty = "∅";
                   print_begin = "";
                   print_sep   = "@,";
                   print_end   = ""; }
       pp_assumption
    ) r.report_assumptions
    (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@,")
       (fun fmt ((range, cs),checks) ->
          pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@,")
            (fun fmt (check,diag) ->
               fprintf fmt "@[<hov2>%a(%a): %a:@ @[%a@]@]"
                 pp_relative_range range
                 pp_callstack_short cs
                 pp_check check
                 pp_diagnostic diag
            ) fmt (CheckMap.bindings checks)
       )
    ) (RangeCallStackMap.bindings r.report_diagnostics)

let subset_report r1 r2 =
  (r1 == r2)
  || (AssumptionSet.equal r1.report_assumptions r2.report_assumptions
      && (r1.report_diagnostics == r2.report_diagnostics
          || (RangeCallStackMap.for_all2zo
                (fun _ checks1 -> false)
                (fun _ checks2 -> true)
                (fun _ checks1 checks2 ->
                   CheckMap.for_all2zo
                     (fun _ diag1 -> diag1.diag_kind == Unreachable)
                     (fun _ diag2 -> true)
                     (fun _ diag1 diag2 -> subset_diagnostic diag1 diag2)
                     checks1 checks2
                )
                r1.report_diagnostics r2.report_diagnostics)))

let join_report r1 r2 =
  if r1 == r2 then r1 else
  if subset_report r1 r2 then r2 else
  if subset_report r2 r1 then r1
  else
    { report_assumptions = AssumptionSet.union r1.report_assumptions r2.report_assumptions;
      report_diagnostics =
        RangeCallStackMap.map2zo
          (fun range checks1 -> checks1)
          (fun range checks2 -> checks2)
          (fun range checks1 checks2 ->
             CheckMap.map2zo
               (fun check diag1 -> diag1)
               (fun check diag2 -> diag2)
               (fun _ diag1 diag2 -> join_diagnostic diag1 diag2)
               checks1 checks2
          )
          r1.report_diagnostics r2.report_diagnostics; }

let meet_report r1 r2 =
  if r1 == r2 then r1 else
  if subset_report r1 r2 then r1 else
  if subset_report r2 r1 then r2
  else
    { report_assumptions = AssumptionSet.union r1.report_assumptions r2.report_assumptions;
      report_diagnostics =
        RangeCallStackMap.fold2zo
          (fun (range, _) _ acc -> Exceptions.panic_at range "alarms: unsound meet")
          (fun (range, _) _ acc -> Exceptions.panic_at range "alarms: unsound meet")
          (fun (range, cs) checks1 checks2 acc ->
             let checks =
               CheckMap.fold2zo
                 (fun check diag1 acc -> Exceptions.panic_at range "alarms: unsound meet for check '%a'" pp_check check)
                 (fun check diag2 acc -> Exceptions.panic_at range "alarms: unsound meet for check '%a'" pp_check check)
                 (fun check diag1 diag2 acc -> CheckMap.add check (meet_diagnostic diag1 diag2) acc)
                 checks1 checks2 checks1 in
             RangeCallStackMap.add (range, cs) checks acc
          )
          r1.report_diagnostics r2.report_diagnostics r1.report_diagnostics }

let count_alarms r =
  RangeCallStackMap.fold
    (fun range checks acc ->
       CheckMap.fold
         (fun check diag (errors,warnings) ->
            match diag.diag_kind with
            | Error              -> errors + 1, warnings
            | Warning            -> errors, warnings + 1
            | Safe | Unreachable -> errors, warnings
         ) checks acc
    ) r.report_diagnostics (0,0)

let add_alarm ?(warning=false) alarm r =
  let check = alarm.alarm_check in
  let range = alarm.alarm_range in
  let callstack = alarm.alarm_callstack in
  let checks = try RangeCallStackMap.find (range, alarm.alarm_callstack) r.report_diagnostics with Not_found -> CheckMap.empty in
  let diag = try CheckMap.find check checks with Not_found -> mk_unreachable_diagnostic check callstack range in
  let diag' = add_alarm_to_diagnostic alarm diag in
  let diag'' = if warning && diag'.diag_kind = Error then { diag' with diag_kind = Warning } else diag' in
  { r with report_diagnostics = RangeCallStackMap.add (alarm.alarm_range, alarm.alarm_callstack) (CheckMap.add check diag'' checks) r.report_diagnostics }

let map2zo_report f1 f2 f r1 r2 =
  { report_assumptions = AssumptionSet.union r1.report_assumptions r2.report_assumptions;
    report_diagnostics =
      RangeCallStackMap.map2zo
        (fun range -> CheckMap.map f1)
        (fun range -> CheckMap.map f2)
        (fun range -> CheckMap.map2zo (fun _ -> f1) (fun _ -> f2) (fun _ -> f))
        r1.report_diagnostics r2.report_diagnostics }

let fold2zo_report f1 f2 f r1 r2 init =
  RangeCallStackMap.fold2zo
    (fun range checks1 acc -> CheckMap.fold (fun check -> f1) checks1 acc)
    (fun range checks2 acc -> CheckMap.fold (fun check -> f2) checks2 acc)
    (fun range checks1 checks2 acc ->
       CheckMap.fold2zo
         (fun check diag1 acc -> f1 diag1 acc)
         (fun check diag2 acc -> f2 diag2 acc)
         (fun check diag1 diag2 acc -> f diag1 diag2 acc)
         checks1 checks2 acc
    )
    r1.report_diagnostics r2.report_diagnostics init

let exists2zo_report f1 f2 f r1 r2 =
  RangeCallStackMap.exists2zo
    (fun range checks1 -> CheckMap.exists (fun check -> f1) checks1)
    (fun range checks2 -> CheckMap.exists (fun check -> f2) checks2)
    (fun range checks1 checks2 ->
       CheckMap.exists2zo
         (fun check diag1 -> f1 diag1)
         (fun check diag2 -> f2 diag2)
         (fun check diag1 diag2 -> f diag1 diag2)
         checks1 checks2
    )
    r1.report_diagnostics r2.report_diagnostics

let fold_report f r init =
  RangeCallStackMap.fold
    (fun range checks acc -> CheckMap.fold (fun check -> f) checks acc)
    r.report_diagnostics init

module CallstackSet = SetExt.Make(struct type t = callstack let compare = compare_callstack end)

module RangeDiagnosticWoCsMap = MapExt.Make(
  struct
    type t = range * diagnosticWoCs
    let compare (r1, d1) (r2, d2) =
      Compare.pair
        compare_range 
        (Compare.quadruple
           compare_range compare_check compare AlarmSet.compare)
        (r1, (d1.diag_range,d1.diag_check,d1.diag_kind,d1.diag_alarms))
        (r2, (d2.diag_range,d2.diag_check,d2.diag_kind,d2.diag_alarms))
  end)

let group_diagnostics (rangecs: diagnostic CheckMap.t RangeCallStackMap.t)
  : CallstackSet.t RangeDiagnosticWoCsMap.t =
  RangeCallStackMap.fold (fun (range, cs) cm acc ->
      CheckMap.fold (fun check diagnostic acc ->
          let dWoCs = {diagnostic with diag_callstack = ()} in
          let css =
            try RangeDiagnosticWoCsMap.find (range, dWoCs) acc
            with Not_found -> CallstackSet.empty in
          RangeDiagnosticWoCsMap.add (range, dWoCs) (CallstackSet.add diagnostic.diag_callstack css) acc  
        ) cm acc
    )
    rangecs RangeDiagnosticWoCsMap.empty 

let find_diagnostic rangecs check report =
  RangeCallStackMap.find rangecs report.report_diagnostics |>
  CheckMap.find check

let set_diagnostic diag report =
  let checks =
    try RangeCallStackMap.find (diag.diag_range, diag.diag_callstack) report.report_diagnostics
    with Not_found -> CheckMap.empty
  in
  let checks' = CheckMap.add diag.diag_check diag checks in
  if checks == checks' then report
  else { report with
         report_diagnostics = RangeCallStackMap.add (diag.diag_range, diag.diag_callstack) checks' report.report_diagnostics }

let add_diagnostic diag report =
  let checks =
    try RangeCallStackMap.find (diag.diag_range, diag.diag_callstack) report.report_diagnostics
    with Not_found -> CheckMap.empty in
  try
    let old_diag = CheckMap.find diag.diag_check checks in
    let diag' = join_diagnostic diag old_diag in
    if old_diag == diag' then report
    else
      let checks' = CheckMap.add diag.diag_check diag' checks in
      { report with
        report_diagnostics = RangeCallStackMap.add (diag.diag_range, diag.diag_callstack) checks' report.report_diagnostics }
  with Not_found ->
    let checks' = CheckMap.add diag.diag_check diag checks in
    { report with
      report_diagnostics = RangeCallStackMap.add (diag.diag_range, diag.diag_callstack) checks' report.report_diagnostics }

let remove_diagnostic diag report =
  try
    let checks = RangeCallStackMap.find (diag.diag_range, diag.diag_callstack) report.report_diagnostics in
    let checks' = CheckMap.remove diag.diag_check checks in
    if checks == checks' then report
    else { report with
           report_diagnostics = RangeCallStackMap.add (diag.diag_range, diag.diag_callstack) checks' report.report_diagnostics }
  with Not_found ->
    report

let exists_report f report =
  RangeCallStackMap.exists
    (fun range -> CheckMap.exists (fun _ diag -> f diag))
    report.report_diagnostics

let forall_report f report =
  RangeCallStackMap.exists
    (fun range -> CheckMap.exists (fun _ diag -> f diag))
    report.report_diagnostics

let filter_report f report =
  let diags =
    RangeCallStackMap.fold
      (fun range checks acc ->
         let checks' = CheckMap.filter (fun _ diag -> f diag) checks in
         if checks == checks' then acc else
         if CheckMap.is_empty checks' then RangeCallStackMap.remove range acc
         else RangeCallStackMap.add range checks' acc)
      report.report_diagnostics report.report_diagnostics
  in
  if diags = report.report_diagnostics then report else { report with report_diagnostics = diags }

let alarms_to_report alarms =
  List.fold_left (fun acc alarm ->
      join_report acc (singleton_report alarm)
    ) empty_report alarms

let report_to_alarms report =
  RangeCallStackMap.fold
    (fun range checks acc ->
       CheckMap.fold
         (fun check diag acc ->
            match diag.diag_kind with
            | Error | Warning    -> AlarmSet.elements diag.diag_alarms @ acc
            | Safe | Unreachable -> acc
         ) checks acc
    ) report.report_diagnostics []

let add_assumption a report =
  let assumptions = AssumptionSet.add a report.report_assumptions in
  if assumptions == report.report_assumptions then report
  else { report with report_assumptions = assumptions }

let add_global_assumption kind report =
  let a = mk_global_assumption kind in
  add_assumption a report

let add_local_assumption kind range report =
  let a = mk_local_assumption kind range in
  add_assumption a report
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