Source file build.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
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
(** Build graphs (PDG) for the function
(see module {!module: Build.BuildPdg})
to represent the dependencies between instructions
in order to use it for slicing purposes.
A function is processed using a forward dataflow analysis
(see module {{: ../html/Dataflow2.html}Dataflow2}
which is instantiated with the module
{!module: Build.Computer} below).
*)
open Pdg_types
let dkey = Pdg_parameters.register_category "build"
let debug fmt = Pdg_parameters.debug ~dkey fmt
let debug2 fmt = Pdg_parameters.debug ~dkey fmt ~level:2
open Cil_types
open Cil_datatype
open PdgTypes
open PdgIndex
exception Err_Bot of string
(** set of nodes of the graph *)
module BoolNodeSet =
Stdlib.Set.Make(Datatype.Pair(Datatype.Bool)(PdgTypes.Node))
let pretty_node ?(key=false) fmt n =
PdgTypes.Node.pretty fmt n;
if key then
Format.fprintf fmt ": %a" PdgIndex.Key.pretty (PdgTypes.Node.elem_key n)
let is_variadic kf =
let varf = Kernel_function.get_vi kf in
match varf.vtype with
| TFun (_, _, is_variadic, _) -> is_variadic
| _ -> Pdg_parameters.fatal
"The variable of a kernel_function has to be a function !"
type arg_nodes = Node.t list
(** type of the whole PDG representation during its building process *)
type pdg_build = {
fct : kernel_function;
mutable other_inputs :
(PdgTypes.Node.t * Dpd.td * Locations.Zone.t) list;
graph : G.t;
states : Pdg_state.states;
index : PdgTypes.Pdg.fi;
ctrl_dpds : BoolNodeSet.t Stmt.Hashtbl.t ;
(** The nodes to which each stmt control-depend on.
* The links will be added in the graph at the end. *)
decl_nodes : Node.t Varinfo.Hashtbl.t ;
(** map between declaration nodes and the variables
to build the dependencies. *)
}
(** create an empty build pdg for the function*)
let create_pdg_build kf =
let nb_stmts =
if Eva.Analysis.use_spec_instead_of_definition kf then 17
else List.length (Kernel_function.get_definition kf).sallstmts
in
let index = FctIndex.create nb_stmts in
let states = Stmt.Hashtbl.create nb_stmts in
let graph = G.create () in
{ fct = kf; graph = graph; states = states; index = index;
other_inputs = [];
ctrl_dpds = Stmt.Hashtbl.create nb_stmts ;
decl_nodes = Varinfo.Hashtbl.create 10 ;
}
let _pretty fmt pdg = PdgTypes.Pdg.pretty_graph fmt pdg.graph
(** add a node to the PDG, but if it is associated with a stmt,
check before if it doesn't exist already (useful for loops).
@return the (new or old) node. *)
let add_elem pdg key =
match key with
| Key.CallStmt _ -> assert false
| _ ->
try
FctIndex.find_info pdg.index key
with Not_found ->
let new_node = G.add_elem pdg.graph key in
debug "add_new_node %a@." (pretty_node ~key:true) new_node;
FctIndex.add pdg.index key new_node;
new_node
let decl_var pdg var =
let new_node = add_elem pdg (Key.decl_var_key var) in
Varinfo.Hashtbl.add pdg.decl_nodes var new_node;
new_node
let get_var_base zone =
try
let base, _ = Locations.Zone.find_lonely_key zone in
match base with
| Base.Var (var,_) -> Some var
| _ -> None
with Not_found -> None
(** add a dependency with the given label between the two nodes.
Pre : the nodes have to be already in pdg. *)
let add_dpd_in_g graph v1 dpd_kind part_opt v2 =
debug "add_dpd : %a -%a-> %a@."
PdgTypes.Node.pretty v1 Dpd.pretty_td dpd_kind
PdgTypes.Node.pretty v2;
G.add_dpd graph v1 dpd_kind part_opt v2
let add_z_dpd pdg n1 k z_part n2 =
add_dpd_in_g pdg.graph n1 k z_part n2
let add_ctrl_dpd pdg n1 n2 =
add_dpd_in_g pdg.graph n1 Dpd.Ctrl None n2
let add_decl_dpd pdg n1 k n2 =
add_dpd_in_g pdg.graph n1 k None n2
(** add a dependency on the variable declaration.
The kind of the dependency is address if the variable appears
in a lvalue, data otherwise.
*)
let add_decl_dpds pdg node dpd_kind varset =
let add_dpd var =
try
let var_decl_node = Varinfo.Hashtbl.find pdg.decl_nodes var in
add_decl_dpd pdg node dpd_kind var_decl_node
with Not_found ->
()
in
Varinfo.Set.iter add_dpd varset
(** [add_dpds pdg v dpd_kind state loc]
* add 'dpd_kind' dependencies from node n to each element
* which are stored for loc in state
*)
let add_dpds pdg n dpd_kind state loc =
let add (node,z_part) =
let z_part = match PdgTypes.Node.elem_key node with
| PdgIndex.Key.SigCallKey
(_, PdgIndex.Signature.Out (PdgIndex.Signature.OutLoc _)) ->
z_part
| _ -> None
in add_z_dpd pdg n dpd_kind z_part node in
let nodes, undef_zone = Pdg_state.get_loc_nodes state loc in
List.iter add nodes;
match undef_zone with
| None -> ()
| Some undef_zone ->
pdg.other_inputs <- (n, dpd_kind, undef_zone) :: pdg.other_inputs
(** Process and clear [pdg.ctrl_dpds] which contains a mapping between the
* statements and the control dependencies that have to be added to the
* statement nodes.
* Because some jump nodes can vanish due to optimisations using the value
* analysis, we can not rely on the transitivity of the dependencies.
* So let's compute a transitive closure of the control dependencies.
* The table gives : stmt -> ctrl dependency nodes of the statement.
* So for each stmt, we have to find if some of its ctrl nodes
* also have dependencies that have to be added to the stmt.
* *)
let add_ctrl_dpds pdg =
let add_indirect ctrl_node_set =
let rec add_node (real, n) (acc, seen) =
if BoolNodeSet.mem (real, n) seen then (acc, seen)
else
let seen = BoolNodeSet.add (real, n) seen in
let acc = if real then BoolNodeSet.add (true, n) acc else acc in
add_rec n (acc, seen)
and add_rec ctrl_node acc =
match PdgTypes.Node.elem_key ctrl_node with
| Key.Stmt ctrl_stmt ->
(try
let stmt_dpds = Stmt.Hashtbl.find pdg.ctrl_dpds ctrl_stmt in
BoolNodeSet.fold add_node stmt_dpds acc
with Not_found -> acc)
| _ -> acc
in
let acc = BoolNodeSet.empty, BoolNodeSet.empty in
let acc, _ = BoolNodeSet.fold add_node ctrl_node_set acc in
acc
in
let add_stmt_ctrl_dpd stmt ctrl_node_set =
let stmt_nodes =
try FctIndex.find_all pdg.index (Key.stmt_key stmt)
with Not_found -> []
in
let label_nodes acc label =
try acc @ FctIndex.find_all pdg.index (Key.label_key stmt label)
with Not_found -> acc
in
let stmt_nodes = List.fold_left label_nodes stmt_nodes stmt.labels in
let ctrl_node_set = add_indirect ctrl_node_set in
let add_node_ctrl_dpds stmt_node =
BoolNodeSet.iter
(fun (_, n) -> add_ctrl_dpd pdg stmt_node n) ctrl_node_set
in List.iter add_node_ctrl_dpds stmt_nodes
in
Stmt.Hashtbl.iter add_stmt_ctrl_dpd pdg.ctrl_dpds;
Stmt.Hashtbl.clear pdg.ctrl_dpds
let process_declarations pdg ~formals ~locals =
let do_param (n, state) v =
let decl_node = decl_var pdg v in
let new_node = add_elem pdg (Key.param_key n) in
add_decl_dpd pdg new_node Dpd.Addr decl_node ;
add_decl_dpd pdg decl_node Dpd.Addr new_node ;
let z = Locations.zone_of_varinfo v in
let new_state = Pdg_state.add_loc_node state ~exact:true z new_node in
(n+1, new_state)
in
let _next_in_num, new_state =
List.fold_left do_param (1, Pdg_state.empty) formals in
List.iter (fun v -> ignore (decl_var pdg v)) locals;
new_state
let ctrl_call_node pdg call_stmt =
try FctIndex.find_info pdg.index (Key.call_ctrl_key call_stmt)
with Not_found -> assert false
let process_call_args pdg d_state stmt args_dpds : arg_nodes =
let num = ref 1 in
let process_arg (dpds, decl_dpds) =
let new_node = add_elem pdg (Key.call_input_key stmt !num) in
add_dpds pdg new_node Dpd.Data d_state dpds;
add_decl_dpds pdg new_node Dpd.Data decl_dpds;
incr num; new_node
in List.map process_arg args_dpds
(** Add a PDG node for each formal argument,
* and add its dependencies to the corresponding argument node.
*)
let process_call_params pdg d_state stmt called_kf (arg_nodes:arg_nodes) =
let ctrl_node = ctrl_call_node pdg stmt in
let param_list = Kernel_function.get_formals called_kf in
let process_param state param arg =
let new_node = arg in
add_ctrl_dpd pdg new_node ctrl_node;
let z = Locations.zone_of_varinfo param in
Pdg_state.add_loc_node state z new_node ~exact:true
in
let rec do_param_arg state param_list (arg_nodes: arg_nodes) =
match param_list, arg_nodes with
| [], [] -> state
| p :: param_list, a :: arg_nodes ->
let state = process_param state p a in
do_param_arg state param_list arg_nodes
| [], _ ->
state
| _, [] -> Pdg_parameters.fatal
"call to a function with to few arguments"
in do_param_arg d_state param_list arg_nodes
let create_call_output_node pdg state stmt out_key out_from fct_dpds =
let new_node = add_elem pdg out_key in
add_dpds pdg new_node Dpd.Data state out_from;
add_dpds pdg new_node Dpd.Ctrl state fct_dpds;
let ctrl_node = ctrl_call_node pdg stmt in
add_ctrl_dpd pdg new_node ctrl_node;
new_node
(** creates a node for lval : caller has to add dpds about the right part *)
let create_lval_node pdg state key ~l_loc ~exact ~l_dpds ~l_decl =
let new_node = add_elem pdg key in
add_dpds pdg new_node Dpd.Addr state l_dpds;
add_decl_dpds pdg new_node Dpd.Addr l_decl;
let new_state = Pdg_state.add_loc_node state ~exact l_loc new_node in
(new_node, new_state)
let add_from pdg state_before state lval (default, deps) =
let new_node = add_elem pdg (Key.out_from_key lval) in
let exact = (not default) in
let state = Pdg_state.add_loc_node state ~exact lval new_node in
add_dpds pdg new_node Dpd.Data state_before deps;
state
let process_call_output pdg state_before_call state stmt out default from_out fct_dpds =
let exact = (not default) in
debug "call-%d Out : %a From %a (%sexact)@."
stmt.sid
Locations.Zone.pretty out Locations.Zone.pretty from_out
(if exact then "" else "not ");
let key = Key.call_output_key stmt out in
let new_node = create_call_output_node pdg state_before_call stmt
key from_out fct_dpds in
let state = Pdg_state.add_loc_node state ~exact out new_node
in state
(** mix between process_call_output and process_asgn *)
let process_call_return pdg state_before_call state_with_inputs stmt
~l_loc ~exact ~l_dpds ~l_decl ~r_dpds fct_dpds =
let out_key = Key.call_outret_key stmt in
let new_node =
create_call_output_node pdg state_with_inputs stmt out_key r_dpds fct_dpds
in
add_dpds pdg new_node Dpd.Addr state_before_call l_dpds;
add_decl_dpds pdg new_node Dpd.Addr l_decl;
let new_state =
Pdg_state.add_loc_node state_before_call ~exact l_loc new_node in
new_state
(** for skip statement : we want to add a node in the PDG in order to be able
* to store information (like marks) about this statement later on *)
let process_skip pdg state stmt =
ignore (add_elem pdg (Key.stmt_key stmt)); state
(** for asm: similar to [process_skip], except that we emit a warning *)
let process_asm pdg state stmt =
Pdg_parameters.warning ~once:true ~current:true
"Ignoring inline assembly code";
ignore (add_elem pdg (Key.stmt_key stmt));
state
let add_label pdg label label_stmt =
let key = Key.label_key label_stmt label in
try FctIndex.find_info pdg.index key
with Not_found -> add_elem pdg key
let process_stmt_labels pdg stmt =
let add label = match label with
| Label _ -> ignore (add_label pdg label stmt)
| _ -> ()
in List.iter add stmt.labels
let add_label_and_dpd pdg label label_stmt jump_node =
let label_node = add_label pdg label label_stmt in
add_ctrl_dpd pdg jump_node label_node
let add_dpd_goto_label pdg goto_node dest_goto =
let rec pickLabel = function
| [] -> None
| Label _ as lab :: _ -> Some lab
| _ :: rest -> pickLabel rest
in
let label = match pickLabel dest_goto.labels with
| Some label -> label
| None ->
let lname = Printf.sprintf "fc_stmt_%d" dest_goto.sid in
let label = Label (lname, Cil_datatype.Stmt.loc dest_goto, false) in
dest_goto.labels <- label::dest_goto.labels;
label
in add_label_and_dpd pdg label dest_goto goto_node
let add_dpd_switch_cases pdg switch_node case_stmts =
let add_case stmt =
let rec pickLabel = function
| [] -> None
| Case _ as lab :: _ -> Some lab
| Default _ as lab :: _ -> Some lab
| _ :: rest -> pickLabel rest
in
match pickLabel stmt.labels with
| Some label -> add_label_and_dpd pdg label stmt switch_node
| None -> assert false
in List.iter add_case case_stmts
(** The control dependencies are stored : they will be added at the end
by [finalize_pdg] *)
let store_ctrl_dpds pdg node iterator (real_dpd, controlled_stmt) =
debug2 "store_ctrl_dpds on %a (real = %b)@."
(pretty_node ~key:true) node real_dpd ;
let add_ctrl_dpd stmt =
let new_dpds =
try
let old_dpds = Stmt.Hashtbl.find pdg.ctrl_dpds stmt in
BoolNodeSet.add (real_dpd, node) old_dpds
with Not_found -> BoolNodeSet.singleton (real_dpd, node)
in
Stmt.Hashtbl.replace pdg.ctrl_dpds stmt new_dpds
in iterator add_ctrl_dpd controlled_stmt
let mk_jump_node pdg stmt controlled_stmts =
let new_node = add_elem pdg (Key.stmt_key stmt) in
begin match stmt.skind with
| If _ | Loop _ | Return _ -> ()
| Break _ | Continue _ ->
()
| Goto (sref,_) -> add_dpd_goto_label pdg new_node !sref
| Switch (_,_,stmts,_) -> add_dpd_switch_cases pdg new_node stmts
| _ -> assert false
end;
store_ctrl_dpds pdg new_node Stmt.Hptset.iter controlled_stmts;
new_node
(** Add a node for a stmt that is a jump.
Add control dependencies from this node to the nodes which correspond to
the stmt list.
Also add dependencies for the jump to the label.
Don't use for jumps with data dependencies : use [process_jump_with_exp]
instead !
*)
let process_jump pdg stmt controlled_stmts =
ignore (mk_jump_node pdg stmt controlled_stmts)
(** like [process_jump] but also add data dependencies on the data and their
declarations. Use for conditional jumps and returns.
*)
let process_jump_with_exp pdg stmt controlled_stmts state loc_cond decls_cond =
let jump_node = mk_jump_node pdg stmt controlled_stmts in
add_dpds pdg jump_node Dpd.Data state loc_cond;
add_decl_dpds pdg jump_node Dpd.Data decls_cond
let add_blk_ctrl_dpds pdg key bstmts =
let new_node = add_elem pdg key in
store_ctrl_dpds pdg new_node List.iter (true, bstmts)
let process_block pdg stmt blk =
add_blk_ctrl_dpds pdg (Key.stmt_key stmt) blk.bstmts
let process_entry_point pdg bstmts =
add_blk_ctrl_dpds pdg Key.entry_point bstmts
let create_fun_output_node pdg state dpds =
let new_node = add_elem pdg Key.output_key in
match state with
| Some state -> add_dpds pdg new_node Dpd.Data state dpds
| None -> ()
let find_return_lval kf =
let stmt = Kernel_function.find_return kf in
match stmt with
| { skind = Return (Some {enode = Lval lval}, _) } -> stmt, lval
| _ -> assert false
(** add a node corresponding to the returned value. *)
let add_retres pdg state ret_stmt retres_loc_dpds retres_decls =
let key_return = Key.stmt_key ret_stmt in
let return_node = add_elem pdg key_return in
let retres =
let stmt, lval = find_return_lval pdg.fct in
Eva.Results.(before stmt |> eval_address ~for_writing:false lval |> as_zone)
in
add_dpds pdg return_node Dpd.Data state retres_loc_dpds;
add_decl_dpds pdg return_node Dpd.Data retres_decls;
let new_state = Pdg_state.add_loc_node state ~exact:true retres return_node in
create_fun_output_node pdg (Some new_state) retres;
new_state
(** part of [finalize_pdg] : add missing inputs
* and build a state with the new nodes to find them back when searching for
* undefined zones.
* (notice that now, they can overlap, for example we can have G and G.a)
* And also deals with warning for uninitialized local variables. *)
let process_other_inputs pdg =
debug2 "process_other_inputs@.";
let rec add n dpd_kind (state, zones) z_or_top =
match zones with
| [] ->
let key = Key.implicit_in_key z_or_top in
let nz = add_elem pdg key in
debug "add_implicit_input : %a@."
Locations.Zone.pretty z_or_top ;
let state = Pdg_state.add_init_state_input state z_or_top nz in
add_z_dpd pdg n dpd_kind None nz;
state, [(z_or_top, nz)]
| (zone, nz)::tl_zones ->
match z_or_top, zone with
| (Locations.Zone.Top (_,_), Locations.Zone.Top (_,_)) ->
add_z_dpd pdg n dpd_kind None nz;
(state, zones)
| (z, _) when (Locations.Zone.equal zone z) ->
add_z_dpd pdg n dpd_kind None nz;
(state, zones)
| _ ->
let state, tl_zones =
add n dpd_kind (state, tl_zones) z_or_top in
state, (zone, nz)::tl_zones
in
let add_zone acc (n, dpd_kind, z) =
let do_add = match get_var_base z with
| Some v -> if Kernel_function.is_local v pdg.fct then false else true
| None -> true
in if do_add then
let acc = match z with
| Locations.Zone.Top (_,_) -> add n dpd_kind acc z
| _ ->
let aux b intervs acc =
let z = Locations.Zone.inject b intervs in
add n dpd_kind acc z
in
Locations.Zone.fold_i aux z acc
in acc
else begin
debug2 "might use uninitialized : %a" Locations.Zone.pretty z;
acc
end
in
let (state, _) =
List.fold_left add_zone (Pdg_state.empty, []) pdg.other_inputs
in state
(** to call then the building process is over :
add the control dependencies in the graph.
@return the real PDG that will be used later on.
@param from_opt for undefined functions (declarations) *)
let finalize_pdg pdg from_opt =
debug2 "try to finalize_pdg";
let last_state =
try Some (Pdg_state.get_last_state pdg.states)
with Not_found ->
let ret =
try Kernel_function.find_return pdg.fct
with Kernel_function.No_Statement ->
Pdg_parameters.abort "No return in a declaration"
in
Pdg_parameters.warning ~once:true ~source:(fst (Stmt.loc ret))
"no final state. Probably unreachable...";
None
in
(match from_opt with
| None -> ()
| Some froms ->
let state = match last_state with Some s -> s | None -> assert false in
let process_out out deps s =
let open Eva.Assigns.DepsOrUnassigned in
if (equal Unassigned deps)
then s
else
let from_out = to_zone deps in
let default = may_be_unassigned deps in
add_from pdg state s out (default, from_out)
in
let from_table = froms.Eva.Assigns.memory in
let new_state =
if Eva.Assigns.Memory.is_bottom from_table then
Pdg_state.bottom
else
let new_state =
match from_table with
| Top ->
process_out
Locations.Zone.top Eva.Assigns.DepsOrUnassigned.top state
| Map m ->
Eva.Assigns.Memory.fold_fuse_same process_out m state
| Bottom -> assert false
in
if not (Kernel_function.returns_void pdg.fct) then begin
let deps_ret = froms.Eva.Assigns.return in
let deps_ret = Eva.Deps.to_zone deps_ret in
ignore
(create_fun_output_node pdg (Some new_state) deps_ret)
end;
new_state
in
Pdg_state.store_last_state pdg.states new_state);
let init_state = process_other_inputs pdg in
Pdg_state.store_init_state pdg.states init_state;
add_ctrl_dpds pdg ;
debug2 "finalize_pdg ok";
PdgTypes.Pdg.make pdg.fct pdg.graph pdg.states pdg.index
(** gives needed informations about [lval] :
= location + exact + dependencies + declarations *)
let get_lval_infos lval stmt =
let decl = Cil.extract_varinfos_from_lval lval in
let request = Eva.Results.before stmt in
let address = Eva.Results.eval_address ~for_writing:true lval request in
let z_loc = Eva.Results.as_zone address in
let exact = Eva.Results.is_singleton address in
let dpds = Eva.Results.address_deps lval request in
(z_loc, exact, dpds, decl)
(** process assignment {v lval = exp; v}
Use the state at ki (before assign)
and returns the new state (after assign). *)
let process_asgn pdg state stmt lval exp =
let r_dpds = Eva.Results.(before stmt |> expr_deps exp) in
let r_decl = Cil.extract_varinfos_from_exp exp in
let (l_loc, exact, l_dpds, l_decl) = get_lval_infos lval stmt in
let key = Key.stmt_key stmt in
let new_node, new_state =
create_lval_node pdg state key ~l_loc ~exact ~l_dpds ~l_decl
in
add_dpds pdg new_node Dpd.Data state r_dpds;
add_decl_dpds pdg new_node Dpd.Data r_decl;
new_state
(** Add a PDG node and its dependencies for each explicit call argument. *)
let process_args pdg st stmt argl =
let process_one_arg arg =
let dpds = Eva.Results.(before stmt |> expr_deps arg) in
let decl_dpds = Cil.extract_varinfos_from_exp arg in
(dpds, decl_dpds)
in let arg_dpds = List.map process_one_arg argl in
process_call_args pdg st stmt arg_dpds
(** Add nodes for the call outputs,
and add the dependencies according to from_table.
To avoid mixing inputs and outputs, [in_state] is the input state
and [new_state] the state to modify.
* Process call outputs (including returned value) *)
let call_outputs pdg state_before_call state_with_inputs stmt
lvaloption assigns fct_dpds =
let Eva.Assigns.{ return = return_deps; memory = memory_deps } = assigns in
let print_outputs fmt =
Format.fprintf fmt "call outputs : %a"
Eva.Assigns.Memory.pretty memory_deps;
if not (lvaloption = None) then
Format.fprintf fmt "\t and \\result %a@."
Eva.Deps.pretty return_deps
in
debug "%t" print_outputs;
let process_out out deps state =
if Eva.Assigns.DepsOrUnassigned.(equal Unassigned deps) then
state
else
let from_out = Eva.Assigns.DepsOrUnassigned.to_zone deps in
let default = Eva.Assigns.DepsOrUnassigned.may_be_unassigned deps in
process_call_output
pdg state_with_inputs state stmt out default from_out fct_dpds
in
if Eva.Assigns.Memory.is_bottom memory_deps then
Pdg_state.bottom
else
let state_with_outputs =
match memory_deps with
| Top ->
process_out
Locations.Zone.top Eva.Assigns.DepsOrUnassigned.top state_before_call
| Bottom -> assert false
| Map m ->
Eva.Assigns.Memory.fold_fuse_same process_out m state_before_call
in
match lvaloption with
| None -> state_with_outputs
| Some lval ->
let r_dpds = Eva.Deps.to_zone return_deps in
let (l_loc, exact, l_dpds, l_decl) = get_lval_infos lval stmt in
process_call_return
pdg
state_with_outputs
state_with_inputs stmt
~l_loc ~exact ~l_dpds ~l_decl
~r_dpds fct_dpds
(** process call : {v lvaloption = funcexp (argl); v}
Use the state at ki (before the call)
and returns the new state (after the call).
*)
let process_call pdg state stmt lvaloption funcexp argl _loc =
let state_before_call = state in
ignore (add_elem pdg (Key.call_ctrl_key stmt));
let arg_nodes = process_args pdg state_before_call stmt argl in
let state_with_args = state in
let called_functions = Eva.Results.callee stmt in
let funcexp_dpds =
match funcexp.enode with
| Lval lval -> Eva.Results.(before stmt |> address_deps lval)
| _ -> assert false
in
let mixed_froms =
try let froms = From.Callwise.find (Kstmt stmt) in Some froms
with Not_found -> None
in
let process_simple_call acc called_kf =
let state_with_inputs =
process_call_params pdg state_with_args stmt called_kf arg_nodes
in
let r =
match mixed_froms with
| Some _ -> state_with_inputs
| None ->
let froms = From.get called_kf in
let state_for_this_call =
call_outputs pdg state_before_call state_with_inputs
stmt lvaloption froms funcexp_dpds
in state_for_this_call
in r :: acc
in
let state_for_each_call =
List.fold_left process_simple_call [] called_functions
in
let new_state =
match state_for_each_call with
| [] ->
let stmt_str = Format.asprintf "%a" Printer.pp_stmt stmt in
Pdg_parameters.not_yet_implemented
~source:(fst (Cil_datatype.Stmt.loc stmt))
"pdg with an unknown function call: %s" stmt_str
| st :: [] -> st
| st :: other_states ->
let merge s1 s2 =
let _,s = Pdg_state.test_and_merge ~old:s1 s2 in s
in List.fold_left merge st other_states
in
let new_state = match mixed_froms with
| None -> new_state
| Some froms ->
call_outputs pdg state_before_call new_state
stmt lvaloption froms funcexp_dpds
in
new_state
(** Add a node in the PDG for the conditional statement,
* and register the statements that are control-dependent on it.
*)
let process_condition ctrl_dpds_infos pdg state stmt condition =
let loc_cond = Eva.Results.(before stmt |> expr_deps condition) in
let decls_cond = Cil.extract_varinfos_from_exp condition in
let controlled_stmts = CtrlDpds.get_if_controlled_stmts ctrl_dpds_infos stmt in
let go_then, go_else = Eva.Results.condition_truth_value stmt in
let real = go_then && go_else in
if not real then
debug
"[process_condition] stmt %d is not a real cond (never goes in '%s')@."
stmt.sid (if go_then then "else" else "then");
process_jump_with_exp pdg stmt (real, controlled_stmts)
state loc_cond decls_cond
(** let's add a node for e jump statement (goto, break, continue)
and find the statements which are depending on it.
Returns are not handled here, but in {!Build.process_return}.
*)
let process_jump_stmt pdg ctrl_dpds_infos jump =
let controlled_stmts =
CtrlDpds.get_jump_controlled_stmts ctrl_dpds_infos jump
in
let real = Eva.Results.is_reachable jump in
if not real then
debug "[process_jump_stmt] stmt %d is not a real jump@." jump.sid;
process_jump pdg jump (real, controlled_stmts)
(** Loop are processed like gotos because CIL transforms them into
* {v while(true) body; v} which is equivalent to {v L : body ; goto L; v}
* There is a small difference because we have to detect the case where
* the [goto L;] would be unreachable (no real loop).
* This is important because it might lead to infinite loop (see bst#787)
*)
let process_loop_stmt pdg ctrl_dpds_infos loop =
let _entry, back_edges = Stmts_graph.loop_preds loop in
debug2 "[process_loop_stmt] for loop %d : back edges = {%a}@."
loop.sid (Pretty_utils.pp_list Stmt.pretty_sid) back_edges;
let controlled_stmts =
CtrlDpds.get_loop_controlled_stmts ctrl_dpds_infos loop
in
let real_loop = List.exists Eva.Results.is_reachable back_edges in
if not real_loop then
debug "[process_loop_stmt] stmt %d is not a real loop@." loop.sid;
process_jump pdg loop (real_loop, controlled_stmts)
(** [return ret_exp;] is equivalent to [out0 = ret_exp; goto END;]
* while a simple [return;] is only a [goto END;].
* Here, we assume that the {{:../html/Oneret.html}Oneret} analysis
* was used, ie. that it is the only return of the function
* and that it is the last statement. So, the [goto] is not useful,
* and the final state is stored to be used later on to compute the outputs.
*)
let process_return _current_function pdg state stmt ret_exp =
let last_state =
match ret_exp with
| Some exp ->
let loc_exp = Eva.Results.(before stmt |> expr_deps exp) in
let decls_exp = Cil.extract_varinfos_from_exp exp in
add_retres pdg state stmt loc_exp decls_exp
| None ->
let controlled_stmt = Cil_datatype.Stmt.Hptset.empty in
let real = Eva.Results.is_reachable stmt in
process_jump pdg stmt (real, controlled_stmt);
state
in
if Eva.Results.is_reachable stmt then
Pdg_state.store_last_state pdg.states last_state
module Computer
(Initial:sig val initial: (stmt * PdgTypes.data_state) list end)
(Fenv:Dataflows.FUNCTION_ENV)
(Param:sig val current_pdg : pdg_build
val ctrl_dpds_infos : CtrlDpds.t
end) = struct
let pdg_debug fmt = debug fmt
type t = PdgTypes.data_state
let current_pdg = Param.current_pdg
let current_function = Fenv.kf;;
assert (current_function == current_pdg.fct);;
let ctrl_dpds_infos = Param.ctrl_dpds_infos
let init = Initial.initial;;
let bottom = Pdg_state.bottom
let pretty fmt (v: t) =
Format.fprintf fmt "<STATE>@\n%a@\n<\\STATE>@." Pdg_state.pretty v
let join_and_is_included smaller larger =
pdg_debug "smaller (new): %a larger (old) %a" pretty smaller pretty larger;
let is_new, new_state = Pdg_state.test_and_merge ~old:larger smaller in
pdg_debug "new_state: %a is_new: %b" pretty new_state is_new;
(new_state, not is_new)
;;
let join a b = fst (join_and_is_included a b)
let is_included a b = snd (join_and_is_included a b)
let rec process_init current_pdg state stmt lv = function
| SingleInit e -> process_asgn current_pdg state stmt lv e
| CompoundInit (_,l) ->
List.fold_left
(fun acc (o,i) ->
let lv = Cil.addOffsetLval o lv in
process_init current_pdg acc stmt lv i)
state l
(** Compute the new state after 'instr' starting from state before 'state'.
*)
let doInstr stmt instr state =
Async.yield ();
pdg_debug "doInstr sid:%d : %a" stmt.sid Printer.pp_instr instr;
match instr with
| _ when not (Eva.Results.is_reachable stmt) ->
pdg_debug "stmt sid:%d is unreachable : skip.@." stmt.sid ;
Pdg_state.bottom
| Local_init (v, AssignInit i, _) ->
process_init current_pdg state stmt (Cil.var v) i
| Local_init (v, ConsInit (f, args, kind), loc) ->
Async.yield ();
Cil.treat_constructor_as_func
(process_call current_pdg state stmt) v f args kind loc
| Set (lv, exp, _) -> process_asgn current_pdg state stmt lv exp
| Call (lvaloption,funcexp,argl,loc) ->
Async.yield ();
process_call current_pdg state stmt lvaloption funcexp argl loc
| Code_annot _
| Skip _ -> process_skip current_pdg state stmt
| Asm _ -> process_asm current_pdg state stmt
(** Called before processing the successors of the statements.
*)
let transfer_stmt (stmt: Cil_types.stmt) (state: t) =
pdg_debug "doStmt %d @." stmt.sid ;
let map_on_all_succs newstate =
List.map (fun x -> (x,newstate)) stmt.succs
in
process_stmt_labels current_pdg stmt;
match stmt.skind with
| Instr i
-> map_on_all_succs (doInstr stmt i state)
| Block blk ->
process_block current_pdg stmt blk;
map_on_all_succs state
| UnspecifiedSequence seq ->
process_block current_pdg stmt
(Cil.block_from_unspecified_sequence seq);
map_on_all_succs state
| Switch (exp,_,_,_)
| If (exp,_,_,_) ->
process_condition ctrl_dpds_infos current_pdg state stmt exp;
map_on_all_succs state
| Return (exp,_) ->
process_return current_function current_pdg state stmt exp;
[]
| Continue _
| Break _
| Goto _ ->
process_jump_stmt current_pdg ctrl_dpds_infos stmt;
map_on_all_succs state
| Loop _ ->
process_loop_stmt current_pdg ctrl_dpds_infos stmt;
map_on_all_succs state
| Throw _ | TryCatch _ ->
Pdg_parameters.fatal "Exception node in the AST"
| TryExcept (_, _, _, _)
| TryFinally (_, _, _) ->
map_on_all_succs state
end
exception Value_State_Top
(** Compute and return the PDG for the given function *)
let compute_pdg_for_f kf =
let pdg = create_pdg_build kf in
let f_locals, f_stmts =
if Eva.Analysis.use_spec_instead_of_definition kf then [], []
else if Eva.Analysis.save_results kf
then
let f = Kernel_function.get_definition kf in
f.slocals, f.sbody.bstmts
else raise Value_State_Top
in
let init_state =
process_entry_point pdg f_stmts;
let formals = Kernel_function.get_formals kf in
process_declarations pdg ~formals ~locals:f_locals
in
let froms = match f_stmts with
| [] ->
Pdg_state.store_last_state pdg.states init_state;
let froms = From.get kf in
Some (froms)
| start :: _ ->
let ctrl_dpds_infos = CtrlDpds.compute kf in
let allstmts = (Kernel_function.get_definition kf).sallstmts in
let allstmts_no_start =
List.filter (fun s -> s.sid != start.sid) allstmts
in
let initial_list =
List.map (fun s -> (s, Pdg_state.bottom)) allstmts_no_start
in
let module Initial = struct
let initial = (start, init_state)::initial_list end
in
let module Fenv =
(val Dataflows.function_env kf: Dataflows.FUNCTION_ENV)
in
let module Computer = Computer(Initial)(Fenv)(struct
let current_pdg = pdg
let ctrl_dpds_infos = ctrl_dpds_infos
end)
in
if Eva.Results.is_reachable start then
begin
let module Compute = Dataflows.Simple_forward(Fenv)(Computer) in
Array.iteri (fun ord value ->
let stmt = Fenv.to_stmt ord in
Stmt.Hashtbl.replace pdg.states stmt value) Compute.before;
None
end
else
raise
(Err_Bot
(Printf.sprintf "unreachable entry point (sid:%d, function %s)"
start.sid (Kernel_function.get_name kf)))
in
let pdg = finalize_pdg pdg froms in
pdg
let degenerated top kf =
Pdg_parameters.feedback "%s for function %a" (if top then "Top" else "Bottom")
Kernel_function.pretty kf;
if top then PdgTypes.Pdg.top kf else PdgTypes.Pdg.bottom kf
let compute_pdg kf =
if not (Eva.Analysis.is_computed ()) then Eva.Analysis.compute ();
Pdg_parameters.feedback "computing for function %a" Kernel_function.pretty kf;
try
if is_variadic kf then
Pdg_parameters.not_yet_implemented "variadic function";
let pdg = compute_pdg_for_f kf in
Pdg_parameters.feedback "done for function %a" Kernel_function.pretty kf;
pdg
with
| Err_Bot what ->
Pdg_parameters.warning "%s" what ;
degenerated false kf
| Value_State_Top -> degenerated true kf
| Log.AbortFatal what ->
Pdg_parameters.warning "internal error: %s" what ;
degenerated true kf
| Log.AbortError what ->
Pdg_parameters.warning "user error: %s" what ;
degenerated true kf
| Pdg_state.Cannot_fold ->
Pdg_parameters.warning "too imprecise value analysis : abort" ;
degenerated true kf
| Log.FeatureRequest (source, who, what) ->
Pdg_parameters.warning ?source "not implemented by %s yet: %s" who what;
degenerated true kf