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
open Cil_types
open Cil_datatype
open Pdg_types
let rec pp_stmt fmt s = match s.skind with
| Instr _ | Return _ | Goto _ | Break _ | Continue _ | TryFinally _
| TryExcept _ | Throw _ | TryCatch _ ->
Printer.without_annot Printer.pp_stmt fmt s
| If (e, _, _, _) ->
Format.fprintf fmt "if(%a) <..>" Printer.pp_exp e
| Switch (e, _, _, _) ->
Format.fprintf fmt "switch(%a)<..>" Printer.pp_exp e
| Loop _ -> Format.fprintf fmt "while (...)"
| Block b ->
begin match b.bstmts with
| [] -> Format.fprintf fmt "<Block {}>"
| s :: _ -> Format.fprintf fmt "<Block { %a }>" pp_stmt s
end
| UnspecifiedSequence _ -> Format.fprintf fmt "TODO"
let print_results fmt a =
Pretty_utils.pp_list
(fun fmt s ->
Format.fprintf fmt "@[<hov 2>%a (sid %d): %a@]"
Printer.pp_location (Stmt.loc s) s.sid pp_stmt s
) fmt a
let compute_from_stmt stmt =
let kf = Kernel_function.find_englobing_kf stmt in
let skip = Compute_impact.skip () in
let reason = Options.Reason.get () in
Compute_impact.stmts_impacted ~skip ~reason kf [stmt]
let compute_from_nodes kf nodes =
let skip = Compute_impact.skip () in
let reason = Options.Reason.get () in
let r = Compute_impact.nodes_impacted ~skip ~reason kf nodes in
Pdg_aux.NS.fold
(fun (n, _z) acc -> PdgTypes.NodeSet.add n acc)
r PdgTypes.NodeSet.empty
let compute_multiple_stmts skip kf ls =
Options.debug "computing impact of statement(s) %a"
(Pretty_utils.pp_list ~sep:",@ " Stmt.pretty_sid) ls;
let reason = Options.Reason.get () in
let res, _, _ = Compute_impact.nodes_impacted_by_stmts ~skip ~reason kf ls in
let res_nodes = Compute_impact.result_to_nodes res in
let res_stmts = Compute_impact.nodes_to_stmts res_nodes in
if Options.Print.get () then begin
Options.result "@[<v 2>@[impacted statements of stmt(s) %a are:@]@ %a@]"
(Pretty_utils.pp_list ~sep:",@ " Stmt.pretty_sid) ls
print_results res_stmts
end;
res_nodes
let slice (stmts:stmt list) =
Options.feedback ~level:2 "beginning slicing";
let name = "impact slicing" in
Slicing.Api.Project.reset_slicing ();
let select sel ({ sid = id } as stmt) =
let kf = Kernel_function.find_englobing_kf stmt in
Options.debug ~level:3 "selecting sid %d (of %s)"
id
(Kernel_function.get_name kf);
Slicing.Api.Select.select_stmt sel ~spare:false stmt kf
in
let sel = List.fold_left select Slicing.Api.Select.empty_selects stmts in
Options.debug ~level:2 "applying slicing request";
Slicing.Api.Request.add_persistent_selection sel;
Slicing.Api.Request.apply_all_internal ();
Slicing.Api.Slice.remove_uncalled ();
let = Slicing.Api.Project.extract name in
Options.feedback ~level:2 "slicing done";
extracted_prj
let () =
let typer typing_context loc args =
match args with
| [] -> Ext_terms []
| _ -> typing_context.Logic_typing.error loc "Invalid impact directive"
in
Acsl_extension.register_code_annot_next_both
~plugin:"impact" "impact_stmt" typer false
let is_impact_annot code_annot =
match code_annot.annot_content with
| AExtended (_, _, { ext_name = "impact_stmt"; }) -> true
| _ -> false
let compute_annots () =
Ast.compute ();
let compute_impact_stmts kf acc =
let fundec = Kernel_function.get_definition kf in
let has_impact_annot stmt =
let impact_annots = Annotations.code_annot ~filter:is_impact_annot stmt in
not (impact_annots = [])
in
let impact_stmts = List.filter has_impact_annot fundec.sallstmts in
if impact_stmts = [] then acc
else (kf, impact_stmts) :: acc
in
let impact_stmts = Options.Annot.fold compute_impact_stmts [] in
let skip = Compute_impact.skip () in
let nodes = List.fold_left
(fun nodes (kf, stmts) ->
Pdg_aux.NS.union nodes (compute_multiple_stmts skip kf stmts))
Pdg_aux.NS.empty impact_stmts
in
let stmts = Compute_impact.nodes_to_stmts nodes in
if Options.Slicing.get () then ignore (slice stmts);
stmts;
;;
let from_stmt = compute_from_stmt
let from_nodes = compute_from_nodes
let main () =
if Options.is_on () then begin
Options.feedback "beginning analysis";
assert (not (Options.Annot.is_empty ()));
ignore (compute_annots ());
Options.feedback "analysis done"
end
let () = Boot.Main.extend main