package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file abstract_state.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
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  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, version 2.1.                                              *)
(*                                                                        *)
(*  It 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.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Cil_datatype

open Simplified

module EdgeLabel = struct
  type t =
    | Pointer (* represents dereferentiation of pointers as well as arrays *)
    | Field of fieldinfo
  let compare l r = match l, r with
    | Pointer, Pointer -> 0
    | Pointer, Field _ -> -1
    | Field lv, Field rv -> Fieldinfo.compare lv rv
    | Field _, Pointer -> 1
  let default = Pointer
  let is_pointer = function Pointer -> true | _ -> false
  let is_field = function Field _ -> true | _ -> false
  let pretty fmt = function
    | Pointer -> ()
    | Field f -> Format.fprintf fmt "-%s" f.fname
end

module G = struct
  include Graph.Persistent.Digraph.ConcreteBidirectionalLabeled (Datatype.Int) (EdgeLabel)

  let psucc g v =
    let only_pointer_succ e =
      if EdgeLabel.is_pointer (E.label e) then Some (E.dst e) else None
    in
    List.filter_map only_pointer_succ (succ_e g v)

  let ppred g v =
    let p e = match E.label e with Pointer -> Some (E.src e) | _ -> None in
    List.filter_map p (pred_e g v)

  let fsucc_opt g v f =
    assert (List.for_all (fun e -> EdgeLabel.is_field @@ E.label e) @@ succ_e g v);
    let is_field_f e = match E.label e with
      | Field f' -> Fieldinfo.equal f f'
      | _ -> false
    in
    let edges = succ_e g v in
    assert (List.length (List.filter is_field_f edges) <= 1);
    Option.map E.dst @@ List.find_opt is_field_f edges

  let psucc_opt g v = match psucc g v with
    | [] -> None
    | [v] -> Some v
    | _ -> Options.fatal "Invariant violated: more than one successor"
end

type v = G.V.t

module V = G.V
module E = struct
  include G.E
  include EdgeLabel
  module Map = Stdlib.Map.Make (struct
      type t = EdgeLabel.t
      let compare = EdgeLabel.compare
    end)
end

module VMap = Datatype.Int.Map
module VSet = Datatype.Int.Set
module LSet = Cil_datatype.LvalStructEq.Set
module VarSet = Cil_datatype.Varinfo.Set

module VarMap = struct
  include Cil_datatype.Varinfo.Map

  let intersect = merge @@ fun _ l r -> match l,r with
    | Some l, Some r -> Some (l,r)
    | _ -> None

  let pretty = let module M = Make (Datatype.Int) in M.pretty
end

type state =
  {graph : G.t;
   vmap : VarSet.t VMap.t; (* associate with each node a set of variables *)
   varmap : V.t VarMap.t (* reverse of varmap *)}

let node_counter = ref 0
let fresh_node_id () =
  let id = !node_counter in
  node_counter := !node_counter + 1;
  id

let get_vars v s : VarSet.t =
  try VMap.find v s.vmap with Not_found -> VarSet.empty

(* raises Not_found *)
let rec find_lval_vertex ((lhost, offset) : lval) s : V.t =
  let find_psucc v = match G.psucc_opt s.graph v with Some v -> v | _ -> raise Not_found in
  let find_fsucc v fname = match G.fsucc_opt s.graph v fname with Some v -> v | _ -> raise Not_found in
  let find_lhost = function
    | Var var -> VarMap.find var s.varmap
    | Mem e ->
      match LvalOrRef.from_exp e with
      | None -> Options.fatal "unexpected result: Lval.from (%a) = None" Exp.pretty e
      | Some (LvalOrRef.Ref lv1) -> find_lval_vertex lv1 s
      | Some (LvalOrRef.Lval lv1) ->
        let v1 = find_lval_vertex lv1 s in
        find_psucc v1
  in
  let rec find_offset v = function
    | NoOffset -> v
    | Index (_, o) ->
      let v' = find_psucc v in
      find_offset v' o
    | Field (f, o) ->
      let v' = find_fsucc v f in
      find_offset v' o
  in
  let hv = find_lhost lhost in
  find_offset hv offset


module Readout = struct

  (* Reconstruct all lvals that are represented by the given node.
     Nodes only carry varinfos. In order to obtain lvals we recursively walk
     backwards in the graph inductively constructing lvals from scratch.
     - The lvals of the current node are the stored varinfos themselves.
     - After gathering the lvals for the predecessor, the lvals are
       modified according to the edge type used:
       * Pointer: add a star (x → *x)
       * Field f: add an offset (x -> x.f) *)
  let get_lval_set v s : LSet.t =
    assert (G.mem_vertex s.graph v);
    (* cycles can occur with unsafe casts such as: x->f = (int* ) x; *)
    let rec checking_for_cycles s visited v =
      if VSet.mem v visited then
        let () =
          Options.warning ~once:true ~wkey:Options.Warn.incoherent
            "cycle during readout of vertex %d, \
             (following unsafe cast?); analysis may be unsound" v
        in LSet.empty
      else
        let visited = VSet.add v visited in
        let modified_predecessors = List.map
            (fun e ->
               let pred_lvals = checking_for_cycles s visited @@ E.src e in
               let modify_lval lv = match E.label e with
                 | Field f -> Cil.addOffsetLval (Field (f, NoOffset)) lv
                 | Pointer ->
                   (* TODO: This Cil.typeOfLval may crash with a fatal kernel
                      error for certain reconstructed lvals involving a union
                      type. See tests/known_bugs/union_readback.c *)
                   let ty = Cil.typeOfLval lv in
                   if Cil.isArrayType ty then
                     Cil.addOffsetLval (Index (Simplified.nul_exp, NoOffset)) lv
                   else
                     let () = if not @@ Cil.isPointerType ty then
                         Options.debug "unexpected type: %a" Printer.pp_typ ty
                     in
                     Mem (Cil.dummy_exp @@ Lval lv), NoOffset
               in
               LSet.map modify_lval pred_lvals
            )
            (G.pred_e s.graph v)
        in
        let lvals_of_v =
          let mk_lval var = (Var var), NoOffset in
          LSet.of_seq @@ Seq.map mk_lval @@ VarSet.to_seq @@ get_vars v s
        in
        List.fold_left LSet.union lvals_of_v modified_predecessors
    in
    checking_for_cycles s VSet.empty v

  let lvals_pointing_to_vertex v s : LSet.t =
    assert (G.mem_vertex s.graph v);
    let list_pred = List.map (fun b -> get_lval_set b s) (G.ppred s.graph v) in
    List.fold_left LSet.union LSet.empty list_pred

  let vars_pointing_to_vertex v s : VarSet.t =
    let preds = G.ppred s.graph v in
    let pred_vars = List.map (fun p -> get_vars p s) preds in
    List.fold_left VarSet.union VarSet.empty pred_vars

  let find_vars lv s =
    let lv = Lval.simplify lv in
    try let v = find_lval_vertex lv s in get_vars v s
    with Not_found -> VarSet.empty

  let find_synonyms lv s =
    let lv = Lval.simplify lv in
    try let v = find_lval_vertex lv s in get_lval_set v s
    with Not_found -> LSet.empty

  let alias_vars lv s : VarSet.t =
    try
      let v = find_lval_vertex lv s in
      List.fold_left
        (fun acc succ -> VarSet.union acc @@ vars_pointing_to_vertex succ s)
        VarSet.empty
        (G.psucc s.graph v)
    with Not_found -> VarSet.empty

  let alias_lvals lv s : LSet.t =
    let v_opt = try Some (find_lval_vertex lv s) with Not_found -> None in
    match Option.bind v_opt @@ G.psucc_opt s.graph with
    | None -> LSet.empty
    | Some succ -> lvals_pointing_to_vertex succ s

  let points_to_vars lv s : VarSet.t =
    let succ = try G.psucc_opt s.graph @@ find_lval_vertex lv s with Not_found -> None in
    match succ with
    | None -> VarSet.empty
    | Some succ_v -> get_vars succ_v s

  let points_to_lvals lv s : LSet.t =
    let succ = try G.psucc_opt s.graph @@ find_lval_vertex lv s with Not_found -> None in
    match succ with
    | None -> LSet.empty
    | Some succ_v -> get_lval_set succ_v s

  let alias_sets_vars s =
    let alias_set_of_vertex (i, _) =
      let aliases = vars_pointing_to_vertex i s in
      if VarSet.cardinal aliases >= 2 then Some aliases else None
    in
    List.filter_map alias_set_of_vertex @@ VMap.bindings s.vmap

  let alias_sets_lvals s =
    let alias_set_of_vertex (i, _) =
      let aliases = lvals_pointing_to_vertex i s in
      if LSet.cardinal aliases >= 2 then Some aliases else None
    in
    List.filter_map alias_set_of_vertex @@ VMap.bindings s.vmap

end


module Pretty = struct
  let pp_debug fmt s =
    Format.fprintf fmt "@[<v>";
    Format.fprintf fmt "@[Edges:";
    G.iter_edges_e
      (fun e ->
         Format.fprintf fmt "@;<3 2>@[%d@ @[%a→@]@ %d@]"
           (E.src e) E.pretty (E.label e) (E.dst e))
      s.graph;
    Format.fprintf fmt "@]@;<6>";
    Format.fprintf fmt "@[VarMap:@;<3 2>";
    VarMap.pretty fmt s.varmap;
    Format.fprintf fmt "@]@;<6>";
    Format.fprintf fmt "@[VMap:@;<2>";
    VMap.iter (fun v ls -> Format.fprintf fmt "@;<2 2>@[%d:%a@]" v VarSet.pretty ls) s.vmap;
    Format.fprintf fmt "@]";
    Format.fprintf fmt "@]"

  let pp_graph fmt s =
    let is_first = ref true in
    let pp_node v fmt lset = Format.fprintf fmt "%d:%a" v VarSet.pretty lset in
    let pp_edge e =
      let v1 = E.src e and v2 = E.dst e in
      if !is_first then is_first := false else Format.fprintf fmt "@;<3>";
      Format.fprintf fmt "@[%a@] %a→ @[%a@]"
        (pp_node v1) (VMap.find v1 s.vmap)
        E.pretty (E.label e)
        (pp_node v2) (VMap.find v2 s.vmap)
    in
    let pp_unconnected_vertex v =
      if G.in_degree s.graph v = 0 && G.out_degree s.graph v = 0 then begin
        if !is_first then is_first := false else Format.fprintf fmt "@;<3>";
        pp_node v fmt (VMap.find v s.vmap)
      end
    in
    if G.nb_vertex s.graph = 0
    then Format.fprintf fmt "<empty>"
    else (G.iter_edges_e pp_edge s.graph;
          G.iter_vertex pp_unconnected_vertex s.graph)

  let pp_aliases fmt s =
    let alias_sets = Readout.alias_sets_lvals s in
    Pretty_utils.pp_list ~empty:"<none>" ~sep:"@;<2>" LSet.pretty fmt alias_sets
end

(* invariants of type t must be true before and after each functon call *)
let assert_invariants s : unit =
  (* check that all vertex of the graph have entries in vmap,
     and are integer between 0 and node_counter, and have at most 1 successor *)
  assert (!node_counter >= 0);
  let assert_vertex v =
    Options.debug ~level:11 "checking coherence of vertex %d" v;
    assert (v >= 0);
    assert (v < !node_counter);
    assert (VMap.mem v s.vmap);
    let succ_e = G.succ_e s.graph v in
    let is_pointer_vertex =
      List.exists (fun e -> E.is_pointer @@ E.label e) succ_e
    and is_struct_vertex =
      List.exists (fun e -> E.is_field @@ E.label e) succ_e
    in
    assert (not (is_pointer_vertex && is_struct_vertex));
    assert (not is_pointer_vertex || List.length (G.succ s.graph v) <= 1);
  in
  G.iter_vertex assert_vertex s.graph;
  let assert_edge v1 v2 =
    Options.debug ~level:11 "checking coherence of edge %d → %d" v1 v2;
    if v1 = v2 then
      Options.warning ~once:true ~wkey:Options.Warn.incoherent
        "loop on vertex %d (following unsafe cast?); analysis may be unsound" v1;
    assert (G.mem_vertex s.graph v1);
    assert (G.mem_vertex s.graph v2)
  in
  G.iter_edges assert_edge s.graph;
  let assert_varmap (var : varinfo) v =
    assert (G.mem_vertex s.graph v);
    assert (VarSet.mem var (VMap.find v s.vmap))
  in
  VarMap.iter assert_varmap s.varmap;
  let assert_vmap v (ls:VarSet.t) =
    assert (G.mem_vertex s.graph v);
    (* TODO: we removed the invariant because of OSCS*)
    (* if not (VarSet.is_empty ls)
     * then
     *   begin
     *     let lv = VarSet.choose ls in
     *     let is_ptr_lv = Lval.is_pointer lv in
     *     assert (VarSet.for_all (fun x -> Lval.is_pointer x = is_ptr_lv) ls)
     *   end; *)
    assert (VarSet.fold (fun lv acc -> acc && V.equal (VarMap.find lv s.varmap) v) ls true)
  in
  VMap.iter assert_vmap s.vmap

(* Ensure that assert_invariants is not executed if the -noassert flag is supplied. *)
let assert_invariants s =
  try assert (assert_invariants s; true)
  with Assert_failure _ as exn ->
    let bt = Printexc.get_raw_backtrace () in
    Options.debug "incoherent graph:@ @[%a@]" Pretty.pp_debug s;
    Options.debug "incoherent graph:@ @[%a@]" Pretty.pp_graph s;
    Printexc.raise_with_backtrace exn bt

let asserting_invariants s = assert_invariants s; s

let pretty ?(debug = false) fmt s =
  assert_invariants s;
  if debug then Pretty.pp_graph fmt s
  else Pretty.pp_aliases fmt s

(* NOTE on "constant vertex": a constant vertex represents an unamed
   scalar value (type bottom in steensgaard's paper), or the address
   of a variable. It means that in [vmap], its associated VarSet is
   empty.  By definition, constant vertex cannot be associated to a
   lval in [varmap] *)
let create_empty_vertex s : V.t * state =
  let new_v = fresh_node_id () in
  new_v, {graph = G.add_vertex s.graph new_v;
          varmap = s.varmap;
          vmap = VMap.add new_v VarSet.empty s.vmap}

let create_var_vertex var s =
  assert (not @@ VarMap.mem var s.varmap);
  let v = fresh_node_id () in
  let s = {graph = G.add_vertex s.graph v;
           varmap = VarMap.add var v s.varmap;
           vmap = VMap.add v (VarSet.singleton var) s.vmap} in
  let rec create_typ_vertex s v ty = match ty with
    | TArray (ty, _, _) | TPtr (ty, _) ->
      (* create more vertices for each level of dereferentiation *)
      let v', s = create_empty_vertex s in
      let s = {s with graph = G.add_edge s.graph v v'} in
      create_typ_vertex s v' ty
    | _ -> s (* until the type becomes scalar *)
  in
  v, create_typ_vertex s v var.vtype

let find_or_create_var_vertex (var : varinfo) s =
  try VarMap.find var s.varmap, s
  with Not_found -> create_var_vertex var s

let rec find_or_create_lval_vertex ((lhost, offset) : lval) s : V.t * state =
  let find_or_create_psucc v s =
    match G.psucc_opt s.graph v with
    | None ->
      let v', s = create_empty_vertex s in
      (* finally add a points-to edge between v and v' *)
      let new_graph = G.add_edge s.graph v v' in
      v', {s with graph = new_graph}
    | Some v' -> v', s
  in
  let find_or_create_fsucc v s f =
    match G.fsucc_opt s.graph v f with
    | None ->
      let v', s = create_empty_vertex s in
      (* finally add a points-to edge between v and v' *)
      let new_graph = G.add_edge_e s.graph @@ E.create v (Field f) v' in
      v', {s with graph = new_graph}
    | Some v' -> v', s
  in
  let find_or_create_lhost s = function
    | Var var -> find_or_create_var_vertex var s
    | Mem e ->
      match LvalOrRef.from_exp e with
      | None -> Options.fatal "unexpected result: Lval.from (%a) = None" Exp.pretty e
      | Some (LvalOrRef.Ref lv1) -> find_or_create_lval_vertex lv1 s
      | Some (LvalOrRef.Lval lv1) ->
        let v1, s = find_or_create_lval_vertex lv1 s in
        find_or_create_psucc v1 s
  in
  let rec find_or_create_offset v s = function
    | NoOffset -> v, s
    | Index (_, o) ->
      let v', s = find_or_create_psucc v s in
      find_or_create_offset v' s o
    | Field (f, o) ->
      let v', s = find_or_create_fsucc v s f in
      find_or_create_offset v' s o
  in
  let hv, s = find_or_create_lhost s lhost in
  let v, s = find_or_create_offset hv s offset in
  Options.debug ~level:7 "graph after find_or_create_lval_vertex @[%a@] (%d):@ %a"
    Printer.pp_lval (lhost, offset) v Pretty.pp_graph s;
  v, s

and find_or_create_ref_vertex lv s : V.t * state =
  let v1, s = find_or_create_lval_vertex lv s in
  let va, s = create_empty_vertex s in
  let s = {s with graph = G.add_edge s.graph va v1} in
  Options.debug ~level:7 "graph after find_or_create_ref_vertex @[%a@] (%d):@ %a"
    LvalOrRef.pretty (LvalOrRef.Ref lv) va Pretty.pp_graph s;
  va, s

and find_or_create_lval_or_ref_vertex (lv : LvalOrRef.t) s : V.t * state =
  match lv with
  | LvalOrRef.Lval lv -> find_or_create_lval_vertex lv s
  | LvalOrRef.Ref lv -> find_or_create_ref_vertex lv s

(* TODO is there a better way to do it ? *)
let find_vertex lv s =
  let lv = Lval.simplify lv in
  let v,x1 = find_or_create_lval_vertex lv s in
  if s == x1
  then v (* if s has not been modified, then the vertex was found, not created *)
  else raise Not_found

(* merge of two vertices; the first vertex carries both sets, the second is
   removed from the graph and from varmap and vmap *)
let merge s v1 v2 =
  if V.equal v1 v2 || not (G.mem_vertex s.graph v1) || not (G.mem_vertex s.graph v2)
  then s
  else
    (* update varmap : every lval in v2 must now be associated with v1 *)
    let new_varmap = VarSet.fold (fun lv2 -> VarMap.add lv2 v1) (get_vars v2 s) s.varmap in
    let new_vmap =
      let new_set = VarSet.union (get_vars v1 s) (get_vars v2 s) in
      VMap.add v1 new_set @@ VMap.remove v2 s.vmap
    in
    let new_graph = (* update the graph *)
      let f_fold_succ e g : G.t =
        G.add_edge_e g @@ E.create v1 (E.label e) (E.dst e)
      and f_fold_pred e g : G.t =
        G.add_edge_e g @@ E.create (E.src e) (E.label e) v1
      in
      let g = s.graph in
      (* add all new edges *)
      let g = G.fold_succ_e f_fold_succ g v2 g in
      let g = G.fold_pred_e f_fold_pred g v2 g in
      G.remove_vertex g v2 (* remove v2 *)
    in
    {graph = new_graph; varmap = new_varmap; vmap = new_vmap}

(* functions join and unify-pointer of steensgaard's paper *)
(* join_without_check may break the invariants *)
let rec join_without_check s v1 v2 : state =
  if V.equal v1 v2 || not (G.mem_vertex s.graph v1 && G.mem_vertex s.graph v2)
  then s
  else
    let mk_edge_map succs =
      let mk_succ e = E.label e, E.dst e in
      E.Map.of_seq @@ Seq.map mk_succ @@ List.to_seq succs
    in
    let succs1 = mk_edge_map @@ G.succ_e s.graph v1 in
    let succs2 = mk_edge_map @@ G.succ_e s.graph v2 in
    let succ_pairs =
      let mk_pair _ succ1 succ2 = match succ1, succ2 with
        | Some s1, Some s2 -> Some (s1, s2)
        | _ -> None
      in
      E.Map.merge mk_pair succs1 succs2
    in
    let s = merge s v1 v2 in
    assert (not (G.mem_vertex s.graph v2));
    let merge_succs _ (succ1, succ2) s =
      assert (succ1 <> v2);
      assert (succ2 <> v1);
      join_without_check s succ1 succ2
    in
    E.Map.fold merge_succs succ_pairs s

let join s v1 v2 : state =
  Options.debug ~level:6 "graph before join(%d,%d):@;<2>@[%a@]" v1 v2 Pretty.pp_graph s;
  assert_invariants s;
  let res = join_without_check s v1 v2 in
  Options.debug ~level:6 "graph after join(%d,%d):@;<2>@[%a@]" v1 v2 Pretty.pp_graph res;
  begin try assert_invariants res
    with Assert_failure _ ->
      Options.debug "join(%d,%d) failed" v1 v2;
      Options.debug "graph before join(%d,%d):@;<2>@[%a@]" v1 v2 Pretty.pp_debug s;
      Options.debug "graph after join(%d,%d):@;<2>@[ %a@]" v1 v2 Pretty.pp_debug res;
      assert_invariants res
  end;
  res

let merge_set s (vs:VSet.t) : V.t * state =
  let v0 = VSet.choose vs in
  if VSet.cardinal vs < 2 then v0, s else begin
    Options.debug ~level:6 "graph before merge_set %a:@;<2>@[%a@]"
      VSet.pretty vs Pretty.pp_debug s;
    assert (G.mem_vertex s.graph v0);
    let result = VSet.fold (fun v acc -> merge acc v0 v) vs s in
    Options.debug ~level:6 "graph after merge_set %a:@;<2>@[%a@]"
      VSet.pretty vs Pretty.pp_debug result;
    v0, result
  end

(* may operate on an unsound state, where nodes may have multiple successors
   of the same edge type *)
let rec join_succs s v =
  Options.debug ~level:8 "joining successors of %d" v;
  if not @@ G.mem_vertex s.graph v then s else
    let edge_map =
      List.fold_left (fun m e ->
          let add_dst = function
            | None -> Some (VSet.singleton @@ E.dst e)
            | Some vs -> Some (VSet.add (E.dst e) vs)
          in
          E.Map.update (E.label e) add_dst m
        )
        E.Map.empty
        (G.succ_e s.graph v)
    in
    let merge_vset _e vs s =
      if VSet.cardinal vs < 2
      then s
      else let v0, s = merge_set s vs in join_succs s v0
    in
    E.Map.fold merge_vset edge_map s

(* in Steensgard's paper, this is written settype(v1,ref(v2,bot)) *)
let set_type s v1 v2 : state =
  assert_invariants s;
  (* if v1 points to another node, suppress current outgoing edge (and the node if it is a constant node) *)
  let g, new_vmap =
    match G.psucc_opt s.graph v1 with
    | None -> s.graph, s.vmap
    | Some v2 ->
      (* if v2 is a constant node supress it directly *)
      if VarSet.is_empty (VMap.find v2 s.vmap)
      then G.remove_vertex s.graph v2, VMap.remove v2 s.vmap
      else G.remove_edge s.graph v1 v2, s.vmap
  in
  let new_g = G.add_edge g v1 v2 in
  asserting_invariants {s with graph = new_g; vmap = new_vmap}

let assignment s lv (e:exp) : state =
  assert_invariants s;
  match Cil.isPointerType (Cil.typeOf e), LvalOrRef.from_exp e with
  | false, _ | _, None -> s
  | true, Some y ->
    let v1, s = find_or_create_lval_vertex (Lval.simplify lv) s in
    let v2, s = find_or_create_lval_or_ref_vertex y s in
    if List.mem v2 (G.psucc s.graph v1) || List.mem v1 (G.psucc s.graph v2)
    then
      let () =
        Options.warning ~source:(fst e.eloc)
          "ignoring assignment of the form: %a = %a"
          Printer.pp_lval lv Printer.pp_exp e;
      in s
    else asserting_invariants @@ join s v1 v2

(* assignment x = allocate(y) *)
let assignment_x_allocate_y s lv : state =
  assert_invariants s;
  let v1, s = find_or_create_lval_vertex (Lval.simplify lv) s in
  match G.psucc_opt s.graph v1 with
  | None ->
    let v2, s = create_empty_vertex s in
    set_type s v1 v2
  | Some _ -> s

let is_included s s' =
  (* tests if s is included in s', at least as the nodes with lval *)
  assert_invariants s;
  assert_invariants s';
  Options.debug ~level:8 "testing equal %a AND à.%a"
    Pretty.pp_graph s (pretty ~debug:true) s';
  let exception Not_included in
  try
    let iter_varmap (var : varinfo) v : unit =
      let v' = try VarMap.find var s'.varmap with Not_found -> raise Not_included in
      (* TODO: render correct for structs *)
      let succs =
        E.Map.of_seq @@ Seq.map (fun e -> E.label e, E.dst e) @@ List.to_seq @@ G.succ_e s.graph v
      and succs' =
        E.Map.of_seq @@ Seq.map (fun e -> E.label e, E.dst e) @@ List.to_seq @@ G.succ_e s'.graph v'
      in
      let check_succs _ succ1 succ2 = match succ1, succ2 with
        | None, _ -> None
        | Some _, None -> raise Not_included
        | Some v1p, Some v2p ->
          if VarSet.subset (VMap.find v1p s.vmap) (VMap.find v2p s'.vmap)
          then None
          else raise Not_included
      in
      ignore @@ E.Map.merge check_succs succs succs'
    in
    VarMap.iter iter_varmap s.varmap; true
  with Not_included -> false

let empty : state = {graph = G.empty; varmap = VarMap.empty; vmap = VMap.empty}

let is_empty s = compare s empty = 0

(* add an int to all vertex values *)
let shift s : state =
  assert_invariants s;
  if is_empty s then s else begin
    Options.debug ~level:8 "before shift: node_counter=%d@.%a"
      !node_counter Pretty.pp_debug s;
    let max_idx = G.fold_vertex max s.graph 0 in
    let min_idx = G.fold_vertex min s.graph max_idx in
    let offset = !node_counter - min_idx in
    let shift x = x + offset in
    let shift_vmap shift_elem vmap =
      VMap.of_seq @@ Stdlib.Seq.map shift_elem @@ VMap.to_seq vmap
    in
    let {graph; varmap; vmap} = s in
    node_counter := max_idx + offset + 1;
    let result =
      {graph = G.map_vertex shift graph;
       varmap = VarMap.map shift varmap;
       vmap = shift_vmap (fun (key, l) -> shift key, l) vmap}
    in
    Options.debug ~level:8 "after shift: node_counter=%d@.%a"
      !node_counter Pretty.pp_debug result;
    asserting_invariants result
  end

let union_find vmap intersections =
  let module Store : UnionFind.STORE = UnionFind.StoreMap.Make (VMap) in
  let module UF = UnionFind.Make (Store) in
  let uf = UF.new_store () in
  let refs = VMap.mapi (fun i _ -> UF.make uf i) vmap in
  let put_into_uf (v1,v2) =
    let r1 = VMap.find v1 refs in
    let r2 = VMap.find v2 refs in
    ignore @@ UF.union uf r1 r2
  in
  let _vs = Seq.iter put_into_uf intersections in
  let sets_to_be_joined =
    let add_to_map i r sets =
      let repr = UF.find uf r in
      let add_to_set = function
        | None -> Some (VSet.singleton i)
        | Some set -> Some (VSet.add i set)
      in
      VMap.update (UF.get uf repr) add_to_set sets
    in
    VMap.fold add_to_map refs VMap.empty in
  sets_to_be_joined

let union s1 s2 : state =
  assert_invariants s1;
  assert_invariants s2;

  Options.debug ~level:4 "Union: First graph:%a" Pretty.pp_graph s1;
  Options.debug ~level:5 "Union: First graph:%a" Pretty.pp_debug s1;
  Options.debug ~level:4 "Union: Second graph:%a" Pretty.pp_graph s2;
  Options.debug ~level:5 "Union: Second graph:%a" Pretty.pp_debug s2;
  let new_graph =
    G.fold_vertex
      (fun v2 g -> G.add_vertex g v2)
      s2.graph
      s1.graph
  in
  let new_graph =
    G.fold_edges_e (fun e g -> G.add_edge_e g e) s2.graph new_graph
  in
  let new_vmap =
    VMap.union (fun _ lset1 lset2 -> Option.some @@ VarSet.union lset1 lset2)
      s2.vmap
      s1.vmap
  in
  let sets_to_be_joined =
    let intersections = VarMap.to_seq @@ VarMap.intersect s1.varmap s2.varmap in
    union_find new_vmap @@ Seq.map snd intersections
  in
  let new_varmap = VarMap.union (fun _ l _r -> Some l) s1.varmap s2.varmap in
  Options.debug ~level:7 "Union: sets to be joined:@[";
  VMap.iter (fun _ set -> Options.debug ~level:7 "%a" VSet.pretty set) sets_to_be_joined;
  Options.debug ~level:7 "@]";
  let s = {graph = new_graph; varmap = new_varmap; vmap = new_vmap} in
  let merged_nodes, s =
    VMap.fold
      (fun _ set (merged_nodes, s) -> let v0, s = merge_set s set in (v0 :: merged_nodes), s)
      sets_to_be_joined
      ([], s)
  in
  let s = List.fold_left join_succs s merged_nodes in
  Options.debug ~level:4 "Union: Result graph:%a" Pretty.pp_graph s;
  Options.debug ~level:5 "Union: Result graph:%a" Pretty.pp_debug s;
  begin try assert_invariants s
    with Assert_failure _ ->
      Options.debug "union failed";
      Options.debug "Union: First graph:%a" Pretty.pp_graph s1;
      Options.debug "Union: First graph:%a" Pretty.pp_debug s1;
      Options.debug "Union: Second graph:%a" Pretty.pp_graph s2;
      Options.debug "Union: Second graph:%a" Pretty.pp_debug s2;
      Options.debug "Union: Result graph:%a" Pretty.pp_graph s;
      Options.debug "Union: Result graph:%a" Pretty.pp_debug s;
      assert_invariants s
  end;
  s


module Summary = struct
  (* a type for summaries of functions *)
  type t = {state   : state option;
            formals : lval list;
            return  : exp option}

  let make s (kf : kernel_function) =
    let exp_return : exp option =
      if Kernel_function.has_definition kf then
        let return_stmt = Kernel_function.find_return kf in
        match return_stmt.skind with
        | Return (e, _) -> e
        | _ -> Options.fatal "this should not happen"
      else None
    in
    let s =
      match exp_return with
      | None -> s
      | Some e ->
        begin match s, LvalOrRef.from_exp e with
          | _, None -> s
          | s, Some lv ->
            let _, new_s = find_or_create_lval_or_ref_vertex lv s in
            new_s
        end
    in
    {state = Some s;
     formals = List.map (fun v -> (Var v,NoOffset)) (Kernel_function.get_formals kf);
     return = exp_return}

  let pretty ?(debug=false) fmt summary =
    let pp_list_lval s fmt (l: lval list) =
      let is_first = ref true in
      let pp_elem lv =
        if !is_first then is_first := false else Format.fprintf fmt "@  ";
        Format.fprintf fmt "@[%a" Cil_datatype.Lval.pretty lv;
        let pointees = Readout.points_to_vars lv s in
        if not @@ VarSet.is_empty pointees then
          Format.fprintf fmt "→%a" VarSet.pretty pointees;
        Format.fprintf fmt "@]";
      in
      List.iter pp_elem l
    in
    let pp_option pp fmt = function
      | Some x -> pp fmt x
      | None -> Format.fprintf fmt "<none>"
    in
    match summary.state with
    | None -> if debug then Format.fprintf fmt "not found"
    | Some s when is_empty s -> if debug then Format.fprintf fmt "empty"
    | Some s ->
      Format.fprintf fmt "@[formals: @[%a@]@;<4>returns: @[%a@]@;<4>state: @[%a@] "
        (pp_list_lval s) summary.formals
        (pp_option Exp.pretty) summary.return
        (pp_option @@ pretty ~debug) summary.state

end

(* the algorithm:
   - unify the two graphs dropping all the variables from the summary
   - pair arguments with formals assigning the formal's successor as the argument's successor
*)
let call s (res : lval option) (args : exp list) (summary : Summary.t) : state =
  assert_invariants s;
  let formals = summary.Summary.formals in
  assert (List.length args = List.length formals);
  let sum_state = shift @@ Option.get summary.state in

  (* pair up formals and their corresponding arguments,
     as well as the bound result with the returned value *)
  let arg_formal_pairs =
    let res_ret = match res, summary.return with
      | None, None -> []
      | Some res, Some ret ->
        let simplify_ret x = match LvalOrRef.from_exp x with
          | Some (LvalOrRef.Lval lval) -> lval
          | _ -> Options.fatal "unexpected form of return statement"
        in
        [LvalOrRef.Lval (Lval.simplify res), simplify_ret ret]
      | None, Some _ -> []
      | Some _, None -> (* Shouldn't happen: Frama-C adds missing returns *)
        Options.fatal "unexpected case: result without return"
    in
    let simplify_both (arg, formal) =
      try
        match LvalOrRef.from_exp arg with
        | None -> None
        | Some lv -> Some (lv, Lval.simplify formal)
      with Explicit_pointer_address loc ->
        Options.warning ~source:(fst loc) ~wkey:Options.Warn.unsupported_address
          "unsupported feature: explicit pointer address: %a; analysis may be unsound"
          Printer.pp_exp arg;
        None
    in
    res_ret @ List.filter_map simplify_both @@ List.combine args formals
  in

  (* for each pair (lv1,lv2) find (or create) the corresponding vertices *)
  let s, vertex_pairs =
    let s = ref s in
    let find_vertex (lv1, lv2) =
      try
        let v2 = find_lval_vertex lv2 sum_state in
        let v1, new_state = find_or_create_lval_or_ref_vertex lv1 !s in
        s := new_state;
        Some (v1, v2)
      with Not_found -> None
    in
    !s, List.filter_map find_vertex arg_formal_pairs
  in

  (* merge the function graph;
     for every arg/formal vertex pair (v1,v2) and every edge v2→v create edge v1→v. *)
  let g =
    let transfer_succs g (v1,v2) =
      List.fold_left
        (fun g e -> G.add_edge_e g @@ E.create v1 (E.label e) (E.dst e))
        g
        (G.succ_e sum_state.graph v2)
    in
    let g = s.graph in
    let g = G.fold_vertex (fun i g -> G.add_vertex g i) sum_state.graph g in
    let g = G.fold_edges_e (fun e g -> G.add_edge_e g e) sum_state.graph g in
    List.fold_left transfer_succs g vertex_pairs
  in

  (* garbage collect: remove leaf vertices from g that originate from sum_state *)
  let vertices_to_add_to_g, g =
    let g = ref g in
    let remove_if_leaf v _ =
      if G.in_degree !g v = 0
      then let () = g := G.remove_vertex !g v in None
      else Some VarSet.empty
    in
    let remaining_vertices = VMap.filter_map remove_if_leaf sum_state.vmap in
    remaining_vertices, !g
  in

  let s = {
    graph = g;
    varmap = s.varmap;
    vmap =
      let left_bias _ l _ = Some l in
      VMap.union left_bias s.vmap vertices_to_add_to_g}
  in

  asserting_invariants
    (List.fold_left join_succs s @@ List.map fst vertex_pairs)

module Dot = struct
  let find_vars_ref = Extlib.mk_fun "find_vars"

  include Graph.Graphviz.Dot (struct
      include G
      let edge_attributes _ = []
      let default_edge_attributes _ = []
      let get_subgraph _ = None
      let vertex_attributes v =
        let lset = !find_vars_ref v in
        let label =
          VarSet.pretty Format.str_formatter lset;
          Format.flush_str_formatter ()
        in
        [`Label label]

      let vertex_name v = string_of_int v
      let default_vertex_attributes _ = [`Shape `Box]
      let graph_attributes _ = []
    end)
end

module API = struct
  type t = state

  type summary = Summary.t

  let pretty_summary = Summary.pretty

  let make_summary = Summary.make

  let vid v : int = v

  let rec closure_find_lset v s : (V.t * LSet.t) list =
    match G.psucc_opt s.graph v with
    | None -> [v, Readout.get_lval_set v s]
    | Some v_next -> (v, Readout.get_lval_set v s) :: closure_find_lset v_next s

  let find_transitive_closure lv s : (V.t * LSet.t) list =
    let lv = Lval.simplify lv in
    assert_invariants s;
    try closure_find_lset (find_lval_vertex lv s) s with Not_found -> []
  (* TODO : what about offsets ? *)

  let get_lval_set = Readout.get_lval_set
  let find_vars = Readout.find_vars
  let find_synonyms = Readout.find_synonyms
  let find_aliases = Readout.find_synonyms
  let alias_vars = Readout.alias_vars
  let alias_lvals = Readout.alias_lvals
  let find_all_aliases = Readout.alias_lvals (* deprecated *)
  let points_to_vars = Readout.points_to_vars
  let points_to_set = Readout.points_to_lvals
  let points_to_lvals = Readout.points_to_lvals
  let alias_sets_vars = Readout.alias_sets_vars
  let alias_sets_lvals = Readout.alias_sets_lvals

  let get_graph s = s.graph

  let print_dot filename s =
    let file = open_out filename in
    Dot.find_vars_ref := (fun v -> get_vars v s);
    Dot.output_graph file s.graph;
    close_out file
end

include API
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