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
open Cil_types
open Cil_datatype
module Options = Reduc_options
exception Alarm_reached
let dkey = Options.register_category "collect"
let debug = Options.debug ~dkey
type 'a alarm_component = Emitter.t ->
kernel_function ->
stmt ->
rank:int -> Alarms.alarm -> code_annotation -> 'a -> 'a
type annoth = AnnotAll | AnnotInout
type env = {
rel_annoth: annoth;
rel_stmts: Stmt.Set.t;
rel_vars: LvalStructEq.Set.t Stmt.Map.t;
}
let empty_env annoth = {
rel_annoth = annoth;
rel_stmts = Stmt.Set.empty;
rel_vars = Stmt.Map.empty;
}
let env_with_stmt env stmt =
{ env with rel_stmts = Stmt.Set.add stmt env.rel_stmts }
let env_with_stmt_vars env stmt lvs =
let vars =
try
Stmt.Map.find stmt env.rel_vars
with Not_found -> LvalStructEq.Set.empty in
let new_vars = LvalStructEq.Set.(union vars (of_list lvs)) in
{ env with rel_vars = Stmt.Map.add stmt new_vars env.rel_vars }
(** Alarms to relevant locations *)
class stmts_vis
(alarm_stmt : stmt)
(env: env ref) = object(_)
inherit Cil.nopCilVisitor
method! vstmt stmt =
env := env_with_stmt !env stmt;
if Stmt.equal stmt alarm_stmt then begin
raise Alarm_reached
end;
Cil.DoChildren
end
let rec collect_off typ =
match typ.tnode with
| TInt _ | TFloat _ -> [ NoOffset ]
| TComp {cfields = Some flds} ->
List.fold_left collect_fields [] flds
| TArray (arrtyp, e_opt) ->
debug "Array of length %a" (Pretty_utils.pp_opt Printer.pp_exp) e_opt;
begin try collect_array arrtyp [] (Cil.lenOfArray64 e_opt)
with Cil.LenOfArray _ -> [] end
| TVoid | TFun _ | TPtr _ | TEnum _ | TNamed _ | TBuiltin_va_list
| TComp {cfields = None} -> []
and collect_fields acc fld =
let offs = collect_off fld.ftype in
List.map (fun off -> Field (fld, off)) offs @ acc
and collect_array typ acc = function
| x when Integer.is_zero x -> acc
| x ->
let offs = collect_off typ in
let exp = Cil.kinteger64 ~loc:Location.unknown x in
let acc' = acc @ List.map (fun off -> Index(exp ,off)) offs in
collect_array typ acc' (Integer.add x Integer.minus_one)
let collect_varinfo acc x =
let offs = collect_off x.vtype in
List.map (fun off -> (Var x, off)) offs @ acc
class inout_vis
(alarm_stmt : stmt)
(kf : Kernel_function.t)
(env : env ref) = object(self)
inherit stmts_vis alarm_stmt env as super
val mutable vars = []
method !vfunc _ =
vars <- Kernel_function.((get_locals kf) @ (get_formals kf));
Cil.DoChildren
method private is_first_stmt stmt =
try Stmt.equal stmt (Kernel_function.find_first_stmt kf)
with Kernel_function.No_Statement -> assert false
method !vstmt stmt =
let out = Inout.stmt_outputs stmt in
let filter_out vi =
let open Locations in
let zone = enumerate_bits (loc_of_varinfo vi) in
Zone.intersects out zone
in
let stmt_effect =
if self#is_first_stmt stmt then vars
else List.filter filter_out vars
in
let vars = List.fold_left collect_varinfo [] stmt_effect in
env := env_with_stmt_vars !env stmt vars;
super#vstmt stmt
end
let get_relevant_stmts kf stmt env =
let do_visit ref_env = match !ref_env.rel_annoth with
| AnnotAll -> Cil.visitCilFunction (new stmts_vis stmt ref_env)
| AnnotInout ->
Cil.visitCilFunction (new inout_vis stmt kf ref_env :> Cil.cilVisitor)
in
let renv = ref env in
try
let fundec = Kernel_function.get_definition kf in
ignore (do_visit renv fundec);
!renv
with Alarm_reached ->
!renv
let get_relevant _emit kf stmt ~rank:_ _a _annot env =
get_relevant_stmts kf stmt env
let should_annotate_stmt env stmt =
Stmt.Set.mem stmt env.rel_stmts
(** Relevant locations to relevant variables *)
class relevant_stmt_vars_visitor
(vars: LvalStructEq.Set.t ref) = object(_)
inherit Cil.nopCilVisitor
method! vstmt stmt =
match stmt.skind with
| Goto _ | UnspecifiedSequence _ -> Cil.SkipChildren
| _ -> Cil.DoChildren
method! vblock _ = Cil.SkipChildren
method !vexpr e =
begin match e.enode with
| Lval lv | AddrOf lv | StartOf lv ->
vars := LvalStructEq.Set.add lv !vars
| _ -> ()
end;
Cil.DoChildren
end
let get_relevant_all_vars_stmt kf stmt =
let do_visit ref_vars =
Cil.visitCilStmt (new relevant_stmt_vars_visitor ref_vars)
in
let ref_vars = ref LvalStructEq.Set.empty in
ignore (do_visit ref_vars stmt);
let locals = Kernel_function.get_locals kf in
let formals = Kernel_function.get_formals kf in
let vars = List.map Cil.var (locals @ formals) in
vars @ LvalStructEq.Set.elements !ref_vars
let get_relevant_inout_vars_stmt env stmt =
try
let vars = Stmt.Map.find stmt env.rel_vars in
LvalStructEq.Set.elements vars
with Not_found -> assert false
let get_relevant_vars_stmt env kf stmt = match env.rel_annoth with
| AnnotAll -> get_relevant_all_vars_stmt kf stmt
| AnnotInout -> get_relevant_inout_vars_stmt env stmt