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
open Cil_types
open Cil_datatype
open Simplified
module VSet = Datatype.Int.Set
module VMap = Datatype.Int.Map
module Lval = Simplified.Lval
module LSet = Cil_datatype.LvalStructEq.Set
module LMap = Cil_datatype.LvalStructEq.Map
module G = Graph.Persistent.Digraph.ConcreteBidirectional(Datatype.Int)
module V = G.V
let vid (v : G.V.t) : int = v
module LLMap =
struct
module OMap = Offset.Map
type t = (V.t OMap.t) LMap.t
let empty : t = LMap.empty
let mem (lv : lval) (m:t) =
let lv, off = Cil.removeOffsetLval lv in
try
OMap.mem off (LMap.find lv m)
with
Not_found -> false
let find (lv : lval) (m:t) : V.t =
let lv, off = Cil.removeOffsetLval lv in
OMap.find off (LMap.find lv m)
let add (lv : lval) (v:V.t) (m:t) :t =
let lv, off = Cil.removeOffsetLval lv in
let mo = try LMap.find lv m with Not_found -> OMap.empty in
LMap.add lv (OMap.add off v mo) m
let iter f = LMap.iter @@ fun lv -> OMap.iter @@ fun o -> f @@ Cil.addOffsetLval o lv
let map f = LMap.map @@ OMap.map f
let pretty fmt =
let is_first = ref true in
LMap.iter (fun lv ->
OMap.iter
(fun o v -> let lv = Cil.addOffsetLval o lv in
if !is_first then is_first := false else Format.fprintf fmt "@;<3>";
Format.fprintf fmt "@ @[%a:%d@]" Lval.pretty lv v))
let union = LMap.union @@ fun _ l r -> Some (OMap.union (fun _ l _r -> Some l) l r)
let intersect =
let intersect_omap l r = match l, r with
| Some l, Some r -> Some (l,r)
| _ -> None
in
let intersect_lmap l r = match l, r with
| Some l, Some r ->
let omap = OMap.merge (fun _ -> intersect_omap) l r in
if OMap.is_empty omap then None else Some omap
| _ -> None
in
LMap.merge @@ fun _ -> intersect_lmap
let to_seq m = LMap.fold (fun lv omap -> OMap.fold (fun o v s -> Seq.cons (lv,o,v) s) omap) m Seq.empty
let rec is_sub_offset o1 o2 =
match (o1,o2) with
NoOffset, _ -> true
| Index (e1,o1), Index (e2,o2) when Cil_datatype.ExpStructEq.equal e1 e2 -> is_sub_offset o1 o2
| Field (f1,o1), Field (f2,o2) when Fieldinfo.equal f1 f2 -> is_sub_offset o1 o2
| _ -> false
let find_upper_offsets (lv : lval) (m:t) : V.t LMap.t =
let lv, off = Cil.removeOffsetLval lv in
let mo = try LMap.find lv m with Not_found -> OMap.empty in
let f_filter o _v = is_sub_offset o off in
let mo = OMap.filter f_filter mo in
OMap.fold
(fun o -> let lv = Cil.addOffsetLval o lv in LMap.add lv)
mo
LMap.empty
end
type t = {
graph : G.t;
lmap : LLMap.t ;
vmap : LSet.t VMap.t ;
}
let node_counter = ref 0
let fresh_node_id () =
let id = !node_counter in
node_counter := !node_counter + 1;
id
let find_lset (v:V.t) (x:t) : LSet.t =
try VMap.find v x.vmap
with Not_found -> LSet.empty
let find_aliases (lv:lval) (x:t) =
let lv = Lval.simplify lv in
try
let v = LLMap.find lv x.lmap in
find_lset v x
with Not_found -> LSet.empty
let rec get_points_to (v:V.t) (x:t) : LSet.t =
assert (G.mem_vertex x.graph v);
let set_predecessors =
List.fold_left
(fun acc v -> LSet.union acc (get_points_to v x))
LSet.empty
(G.pred x.graph v)
in
LSet.union
(find_lset v x)
(LSet.map Lval.points_to set_predecessors)
let aliases_of_vertex (v:V.t) (x:t) : LSet.t =
assert (G.mem_vertex x.graph v);
let list_pred = G.pred x.graph v in
List.fold_left
(fun acc v -> LSet.union acc (get_points_to v x))
LSet.empty
list_pred
let succ_of_lval (lv:lval) (x:t) : int option =
let lv = Lval.simplify lv in
try begin
let v = LLMap.find lv x.lmap in
match G.succ x.graph v with
| [] -> None
| [succ_v] -> Some succ_v
| _ -> Options.fatal "invariant violated (more than 1 successor)"
end with Not_found -> None
let find_all_aliases (lv:lval) (x:t) : LSet.t =
match succ_of_lval lv x with
| None -> LSet.empty
| Some succ_v -> aliases_of_vertex succ_v x
let points_to_set (lv:lval) (x:t) : LSet.t =
match succ_of_lval lv x with
| None -> LSet.empty
| Some succ_v -> find_lset succ_v x
let get_graph (x:t) = x.graph
let get_lval_set = find_lset
let print_debug fmt (x:t) =
Format.fprintf fmt "@[<v>";
Format.fprintf fmt "@[Edges:";
G.iter_edges (fun v1 v2 -> Format.fprintf fmt "@;<3 2>@[%d → %d@]" v1 v2) x.graph;
Format.fprintf fmt "@]@;<6>";
Format.fprintf fmt "@[LMap:@;<3 2>";
LLMap.pretty fmt x.lmap;
Format.fprintf fmt "@]@;<6>";
Format.fprintf fmt "@[VMap:@;<2>";
VMap.iter (fun v ls -> Format.fprintf fmt "@;<2 2>@[%d:%a@]" v LSet.pretty ls) x.vmap;
Format.fprintf fmt "@]";
Format.fprintf fmt "@]"
let print_graph fmt (x:t) =
let is_first = ref true in
let print_edge v1 v2 =
if !is_first then is_first := false else Format.fprintf fmt "@;<3>";
let print_node v fmt lset = Format.fprintf fmt "%d:%a" v LSet.pretty lset in
Format.fprintf fmt "@[%a@] → @[%a@]"
(print_node v1) (VMap.find v1 x.vmap)
(print_node v2) (VMap.find v2 x.vmap)
in
if G.nb_edges x.graph = 0
then Format.fprintf fmt "<empty>"
else G.iter_edges print_edge x.graph
let print_aliases fmt (x:t) =
let is_first = ref true in
let print_alias_set _ set_lv =
if !is_first then is_first := false else Format.fprintf fmt "@;<2>";
LSet.pretty fmt set_lv
in
let alias_set_of_vertex i _ =
let aliases = aliases_of_vertex i x in
if LSet.cardinal aliases >= 2 then Some aliases else None
in
let alias_sets = VMap.filter_map alias_set_of_vertex x.vmap in
if VMap.is_empty alias_sets
then Format.fprintf fmt "<none>"
else VMap.iter print_alias_set alias_sets
(** invariants of type t must be true before and after each functon call *)
let assert_invariants (x:t) : unit =
assert (!node_counter >= 0);
let assert_vertex (v:V.t) =
assert (v >= 0);
assert (v < !node_counter);
assert (VMap.mem v x.vmap);
assert (List.length (G.succ x.graph v) <= 1)
in
G.iter_vertex assert_vertex x.graph;
let assert_edge v1 v2 =
assert (v1 <> v2);
assert (G.mem_vertex x.graph v1);
assert (G.mem_vertex x.graph v2)
in
G.iter_edges assert_edge x.graph;
let assert_lmap (lv : lval) (v:V.t) =
assert (G.mem_vertex x.graph v);
assert (LSet.mem lv (VMap.find v x.vmap))
in
LLMap.iter assert_lmap x.lmap;
let assert_vmap (v:V.t) (ls:LSet.t) =
assert (G.mem_vertex x.graph v);
assert (LSet.fold (fun lv acc -> acc && V.equal (LLMap.find lv x.lmap) v) ls true)
in
VMap.iter assert_vmap x.vmap
let assert_invariants x = assert (assert_invariants x; true)
let pretty ?(debug = false) fmt (x:t) =
if debug then
try
assert_invariants x;
print_graph fmt x
with Assert_failure _ -> print_debug fmt x
else
print_aliases fmt x
(** .dot printing functions*)
let find_vertex_name_ref = Extlib.mk_fun "find_vertex_name"
module Dot = Graph.Graphviz.Dot (struct
include G
let edge_attributes _ = []
let default_edge_attributes _ = []
let get_subgraph _ = None
let vertex_attributes _ = [`Shape `Box]
let vertex_name (v:V.t) =
let lset = !find_vertex_name_ref v in
let fmt = Format.str_formatter in
Format.fprintf fmt "\"%a\"" LSet.pretty lset;
Format.flush_str_formatter ()
let default_vertex_attributes _ = []
let graph_attributes _ = []
end)
let print_dot filename (a:t) =
let file = open_out filename in
find_vertex_name_ref :=
(fun v -> find_lset v a
);
Dot.output_graph file a.graph;
close_out file
let rec closure_find_lset (v:V.t) (x:t) : (V.t * LSet.t) list =
match G.succ x.graph v with
[] -> [v, find_lset v x]
| [v_next] -> (v, find_lset v x)::(closure_find_lset v_next x)
| _ -> Options.fatal ("this shall not happen (invariant broken)")
let find_transitive_closure (lv:lval) (x:t) : (G.V.t * LSet.t) list =
let lv = Lval.simplify lv in
assert_invariants x;
try closure_find_lset (LLMap.find lv x.lmap) x with Not_found -> []
let create_cst_vertex (x:t) : V.t * t =
let new_v = fresh_node_id () in
new_v,
{
graph = G.add_vertex x.graph new_v;
lmap = x.lmap ;
vmap = VMap.add new_v LSet.empty x.vmap
}
let find_all_aliases_of_offset (lv1 : lval) (x: t) : LSet.t =
let lvals_to_be_searched = decompose_lval lv1 in
let f_map (lv,o) =
try VMap.find (LLMap.find lv x.lmap) x.vmap, o
with Not_found -> LSet.empty, o
in
Options.debug ~level:9 "decompose_lval %a : [@[<hov 2>" Lval.pretty lv1;
List.iter (fun (x, o) -> Options.debug ~level:9 " (%a,%a) " Lval.pretty x Offset.pretty o) lvals_to_be_searched;
Options.debug ~level:9 "@]]";
let aliases = List.map f_map lvals_to_be_searched in
let f_fold_left (acc : LSet.t) (ls,o) =
LSet.fold (fun lv -> LSet.add @@ Cil.addOffsetLval o lv) ls acc
in
List.fold_left f_fold_left (LSet.singleton lv1) aliases
let create_vertex_simple (lv:lval) (x:t) : V.t * t =
let new_v = fresh_node_id () in
let new_g = G.add_vertex x.graph new_v in
let set_of_aliases : LSet.t = find_all_aliases_of_offset lv x in
Options.debug ~level:9 "all_aliases of %a : %a " Lval.pretty lv LSet.pretty set_of_aliases;
let new_lmap =
LSet.fold
(fun lv acc -> assert (not (LLMap.mem lv x.lmap)); LLMap.add lv new_v acc)
set_of_aliases
x.lmap
in
let new_vmap = VMap.add new_v set_of_aliases x.vmap in
let new_x =
{
graph = new_g ;
lmap = new_lmap ;
vmap = new_vmap ;
}
in
assert_invariants new_x;
match lv with
| Var v, NoOffset ->
begin
match v.vtype with
TPtr _ ->
let another_v, new_x = create_cst_vertex new_x in
let new_g = G.add_edge new_x.graph new_v another_v in
new_v, {new_x with graph = new_g}
| _ -> new_v, new_x
end
| _ -> new_v , new_x
let diff_offset (lv1 : lval) (lv2 : lval) =
let rec f_diff_offset o1 o2 =
match o1, o2 with
NoOffset, _ -> o2
| Field (_,o1), Field (_,o2) -> f_diff_offset o1 o2
| Index (_,o1), Index (_,o2) -> f_diff_offset o1 o2
| _ -> Options.fatal "%s: unexpected case" __LOC__
in
let _, o1 = Cil.removeOffsetLval lv1
and _, o2 = Cil.removeOffsetLval lv2
in
assert (LLMap.is_sub_offset o1 o2);
f_diff_offset o1 o2
let rec create_vertex lv x =
Options.debug ~level:9 "creating a vertex for %a" Lval.pretty lv;
assert (not (LLMap.mem lv x.lmap));
begin
match lv with
(Mem e, NoOffset) ->
begin
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_vertex (LvalOrRef.Lval lv1) x
| Some (LvalOrRef.Lval lv1) ->
let v1, x = find_or_create_vertex (LvalOrRef.Lval lv1) x in
begin
match G.succ x.graph v1 with
[] ->
let v2, x = create_vertex_simple lv x in
let new_graph = G.add_edge x.graph v1 v2 in
v2, {x with graph = new_graph }
| [succ_v1] ->
let new_lmap = LLMap.add lv succ_v1 x.lmap in
let new_vmap = VMap.add succ_v1 (LSet.add lv (VMap.find succ_v1 x.vmap)) x.vmap in
succ_v1, {x with lmap = new_lmap ; vmap = new_vmap }
| _ -> Options.fatal " Invariant violated : more than 1 successor"
end
end
| _ -> create_vertex_simple lv x
end
and find_or_create_lval_vertex (lv:lval) (x:t) : V.t * t =
try LLMap.find lv x.lmap, x
with Not_found ->
let map_predecessors : V.t LMap.t =
LLMap.find_upper_offsets lv x.lmap
in
let f_fold_lmap lvx vx acc =
let set_aliases = VMap.find vx x.vmap in
Options.debug ~level:9 "looking for aliases of %a in set %a" Lval.pretty lv LSet.pretty set_aliases;
if LSet.cardinal set_aliases <= 1 then acc else
let off = diff_offset lvx lv in
let f_fold_lset lvs acc =
try
let lvs = Cil.addOffsetLval off lvs in
VSet.add (LLMap.find lvs x.lmap) acc
with
Not_found -> acc
in
LSet.fold f_fold_lset set_aliases acc
in
let vset_res = LMap.fold f_fold_lmap map_predecessors VSet.empty in
Options.debug ~level:9 "found aliases of %a : %a" Lval.pretty lv VSet.pretty vset_res;
if VSet.is_empty vset_res
then create_vertex lv x
else
let () = assert (VSet.cardinal vset_res = 1) in
let v_res = VSet.choose vset_res in
let new_lmap = LLMap.add lv v_res x.lmap in
let new_vmap = VMap.add v_res (LSet.add lv (VMap.find v_res x.vmap)) x.vmap in
v_res, {x with lmap = new_lmap; vmap = new_vmap}
and find_or_create_vertex (lv : LvalOrRef.t) (x:t) : V.t * t =
match lv with
| LvalOrRef.Lval lv -> find_or_create_lval_vertex lv x
| LvalOrRef.Ref lv ->
Options.debug ~level:9 "creating a vertex for %a" LvalOrRef.pretty (LvalOrRef.Ref lv);
let v1, x = find_or_create_lval_vertex lv x in
let va, x = create_cst_vertex x in
va, {x with graph = G.add_edge x.graph va v1}
let find_vertex lv x =
let lv = Lval.simplify lv in
let v,x1 = find_or_create_lval_vertex lv x in
if x == x1
then v
else raise Not_found
let merge x v1 v2 =
if (V.equal v1 v2) || not (G.mem_vertex x.graph v1) || not (G.mem_vertex x.graph v2)
then x
else
let set1 = find_lset v1 x in
let set2 = find_lset v2 x in
let new_set = LSet.union set1 set2 in
let new_lmap = LSet.fold (fun lv2 m -> LLMap.add lv2 v1 m) set2 x.lmap in
let new_vmap = VMap.add v1 new_set (VMap.remove v2 x.vmap) in
let f_fold_succ v_succ (g:G.t) : G.t =
G.add_edge g v1 v_succ
and f_fold_pred v_pred (g:G.t) : G.t =
G.add_edge g v_pred v1
in
let g = x.graph in
let g = G.fold_succ f_fold_succ g v2 g in
let g = G.fold_pred f_fold_pred g v2 g in
let g = G.remove_vertex g v2 in
{graph = g; lmap = new_lmap; vmap = new_vmap}
let rec join_without_check (x:t) (v1:V.t) (v2:V.t) : t =
if (V.equal v1 v2) || not (G.mem_vertex x.graph v1 && G.mem_vertex x.graph v2)
then
x
else
let pt1 = G.succ x.graph v1 in
let pt2 = G.succ x.graph v2 in
let x = merge x v1 v2 in
assert (not (G.mem_vertex x.graph v2));
match (pt1, pt2) with
| [], _ -> x
| _, [] -> x
| [succ_v1],[succ_v2] ->
assert (succ_v1 <> v2);
assert (succ_v2 <> v1);
join_without_check x succ_v1 succ_v2
| _, _ ->
Options.fatal "invariant broken"
let join (x:t) (v1:V.t) (v2:V.t) : t =
Options.debug ~level:7 "graph before join(%d,%d):@;<2>@[%a@]" v1 v2 print_debug x;
assert_invariants x;
let res = join_without_check x v1 v2 in
Options.debug ~level:7 "graph after join(%d,%d):@;<2>@[%a@]" v1 v2 print_debug 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 print_debug x;
Options.debug "graph after join(%d,%d):@;<2>@[ %a@]" v1 v2 print_debug res;
assert_invariants res
end;
res
let merge_set (x:t) (vs:VSet.t) : V.t * t =
let v0 = VSet.choose vs in
if VSet.cardinal vs < 2 then v0, x else begin
Options.debug ~level:7 "graph before merge_set %a:@;<2>@[%a@]" VSet.pretty vs print_debug x;
assert (G.mem_vertex x.graph v0);
let result = VSet.fold (fun v acc -> merge acc v0 v) vs x in
Options.debug ~level:7 "graph after merge_set %a:@;<2>@[%a@]" VSet.pretty vs print_debug result;
v0, result
end
let rec join_succs (x:t) v =
Options.debug ~level:8 "joining successors of %d" v;
if not @@ G.mem_vertex x.graph v then x else
match G.succ x.graph v with
| [] | [_] -> x
| succs ->
let v0, x = merge_set x @@ VSet.of_list succs in
join_succs x v0
let set_type (x:t) (v1:V.t) (v2:V.t) : t =
assert_invariants x;
let g, new_vmap =
match G.succ x.graph v1 with
[] -> x.graph, x.vmap
| [v2] ->
if LSet.is_empty (VMap.find v2 x.vmap)
then (G.remove_vertex x.graph v2, VMap.remove v2 x.vmap)
else (G.remove_edge x.graph v1 v2, x.vmap)
| _ -> Options.fatal "too many outgoing edges in set_type"
in
let new_g = G.add_edge g v1 v2 in
let new_x = {x with graph = new_g ; vmap = new_vmap} in
assert_invariants new_x ; new_x
let assignment (a:t) (lv:lval) (e:exp) : t =
assert_invariants a;
if not @@ Cil.isPointerType (Cil.typeOf e) then a else
let x = Lval.simplify lv in
match LvalOrRef.from_exp e with
| None -> a
| Some y ->
let (v1,a) = find_or_create_lval_vertex x a in
let (v2,a) = find_or_create_vertex y a in
if List.mem v2 (G.succ a.graph v1) || List.mem v1 (G.succ a.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 a
else
let a = join a v1 v2 in
let () = assert_invariants a in
a
let assignment_x_allocate_y (a:t) (lv:lval) : t =
assert_invariants a;
let x = Lval.simplify lv in
let (v1,a) = find_or_create_lval_vertex x a in
match G.succ a.graph v1 with
| [] ->
let (v2,a) = create_cst_vertex a in
let new_a : t = set_type a v1 v2 in
let () = assert_invariants new_a in new_a
| [_v2] -> a
| _ -> Options.fatal "this should not hapen (invariant broken)"
let is_included (a1:t) (a2:t) =
assert_invariants a1;
assert_invariants a2;
Options.debug ~level:8 "testing equal %a AND à.%a" (pretty ~debug:true) a1 (pretty ~debug:true) a2;
let exception Not_included in
try
let iter_lmap (lv : lval) (v1:V.t): unit =
let v2 : V.t = try LLMap.find lv a2.lmap with Not_found -> raise Not_included in
match G.succ a1.graph v1, G.succ a2.graph v2 with
[], _ -> ()
| [_], [] -> raise Not_included
| [v1p], [v2p] ->
if LSet.subset (VMap.find v1p a1.vmap) (VMap.find v2p a2.vmap)
then
()
else
raise Not_included
| _ -> Options.fatal "this should not hapen (invariant broken)"
in
LLMap.iter iter_lmap a1.lmap; true
with
Not_included -> false
let empty :t =
{graph = G.empty; lmap = LLMap.empty; vmap = VMap.empty}
let is_empty s =
compare s empty = 0
let shift (a : t) : t =
assert_invariants a;
if is_empty a then a else
let () = Options.debug ~level:8 "before shift: node_counter=%d@.%a" !node_counter print_debug a in
let max_idx = G.fold_vertex max a.graph 0 in
let min_idx = G.fold_vertex min a.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; lmap; vmap} = a in
node_counter := max_idx + offset + 1;
let result =
{graph = G.map_vertex shift graph;
lmap = LLMap.map shift lmap;
vmap = shift_vmap (fun (key, l) -> (shift key, l)) vmap}
in
let () = Options.debug ~level:8 "after shift: node_counter=%d@.%a" !node_counter print_debug result in
assert_invariants result;
result
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 (a1:t) (a2:t) :t =
assert_invariants a1;
assert_invariants a2;
Options.debug ~level:4 "Union: First graph:%a" print_graph a1;
Options.debug ~level:5 "Union: First graph:%a" print_debug a1;
Options.debug ~level:4 "Union: Second graph:%a" print_graph a2;
Options.debug ~level:5 "Union: Second graph:%a" print_debug a2;
let new_graph =
G.fold_vertex
(fun v2 g -> G.add_vertex g v2)
a2.graph
a1.graph
in
let new_graph =
G.fold_edges
(fun v2a v2b g -> G.add_edge g v2a v2b)
a2.graph
new_graph
in
let new_vmap =
VMap.union (fun _ lset1 lset2 -> Option.some @@ LSet.union lset1 lset2)
a2.vmap
a1.vmap
in
let sets_to_be_joined =
let intersections = LLMap.to_seq @@ LLMap.intersect a1.lmap a2.lmap in
union_find new_vmap @@ Seq.map (fun (_,_,x) -> x) intersections
in
let new_lmap = LLMap.union a1.lmap a2.lmap 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 new_a = {graph = new_graph; lmap = new_lmap; vmap = new_vmap} in
let merged_nodes, new_a =
VMap.fold
(fun _ set (merged_nodes, x) -> let v0, x = merge_set x set in (v0 :: merged_nodes), x)
sets_to_be_joined
([], new_a)
in
let new_a = List.fold_left join_succs new_a merged_nodes in
Options.debug ~level:4 "Union: Result graph:%a" print_graph new_a;
Options.debug ~level:5 "Union: Result graph:%a" print_debug new_a;
begin
try assert_invariants new_a
with Assert_failure _ ->
Options.debug "union failed";
Options.debug "Union: First graph:%a" print_graph a1;
Options.debug "Union: First graph:%a" print_debug a1;
Options.debug "Union: Second graph:%a" print_graph a2;
Options.debug "Union: Second graph:%a" print_debug a2;
Options.debug "Union: Result graph:%a" print_graph new_a;
Options.debug "Union: Result graph:%a" print_debug new_a;
assert_invariants new_a
end;
new_a
(** a type for summaries of functions *)
type summary =
{
state : t option;
formals: lval list;
locals: lval list;
return : exp option
}
let make_summary (s : t) (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_vertex lv s in
new_s
end
in
{
state = Some s;
formals = List.map (fun v -> (Var v,NoOffset)) (Kernel_function.get_formals kf);
locals = List.map (fun v -> (Var v,NoOffset)) (Kernel_function.get_locals kf);
return = exp_return
}
let pretty_summary ?(debug=false) fmt s =
let print_list_lval ~state fmt (l: lval list) =
let is_first = ref true in
let print_elem x =
if !is_first then is_first := false else Format.fprintf fmt "@ ";
Format.fprintf fmt "@[%a" Cil_datatype.Lval.pretty x;
let pointees = points_to_set x state in
if not @@ LSet.is_empty pointees then
Format.fprintf fmt "→%a" LSet.pretty pointees;
Format.fprintf fmt "@]";
in
List.iter print_elem l
in
let print_option pp fmt x =
match x with
| Some x -> pp fmt x
| None -> Format.fprintf fmt "<none>"
in
match s.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 state ->
begin
Format.fprintf fmt "@[formals: @[%a@]@;<4>locals: @[%a@]@;<4>returns: @[%a@]@;<4>state: @[%a@] "
(print_list_lval ~state) s.formals
(print_list_lval ~state) s.locals
(print_option Exp.pretty) s.return
(print_option @@ pretty ~debug) s.state;
end
let call (state:t) (res:lval option) (args:exp list) (summary:summary) :t =
assert_invariants state;
let formals = summary.formals in
assert (List.length args = List.length formals);
let sum_state = shift @@ Option.get summary.state in
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 ->
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
let state, vertex_pairs =
let state = ref state in
let find_vertex (lv1, lv2) =
try
let v2 = LLMap.find lv2 sum_state.lmap in
let v1, new_state = find_or_create_vertex lv1 !state in
state := new_state;
Some (v1, v2)
with Not_found -> None
in
!state, List.filter_map find_vertex arg_formal_pairs
in
let g =
let transfer_succs (g : G.t) (v1,v2) =
let v2_succs = G.succ sum_state.graph v2 in
assert (List.length v2_succs < 2);
List.fold_left (fun g succ -> G.add_edge g v1 succ) g v2_succs
in
let g = state.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 (fun i j g -> G.add_edge g i j) sum_state.graph g in
List.fold_left transfer_succs g vertex_pairs
in
let vertices_to_add_to_g, g =
let g = ref g in
let remove_if_leaf v _ =
if G.in_degree sum_state.graph v = 0
then let () = g := G.remove_vertex !g v in None
else Some LSet.empty
in
let remaining_vertices = VMap.filter_map remove_if_leaf sum_state.vmap in
remaining_vertices, !g
in
let state = {
graph = g;
lmap = state.lmap;
vmap =
let left_bias _ l _ = Some l in
VMap.union left_bias state.vmap vertices_to_add_to_g}
in
let state = List.fold_left join_succs state (List.map fst vertex_pairs) in
assert_invariants state;
state