source: Deliverables/D2.2/8051/src/clight/clightAnnotator.ml @ 486

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 12.0 KB
Line 
1(* This module provides an annotation function for Clight programs
2   when given the cost associated to each cost labels of the
3   program. *)
4
5
6let error_prefix = "Clight Annotator"
7let error = Error.global_error error_prefix
8
9
10let cost_id_prefix = "_cost"
11let cost_incr_prefix = "_cost_incr"
12
13
14(* Program var names, cost labels and labels *)
15
16let string_set_of_list l =
17  List.fold_left (fun res s -> StringTools.Set.add s res)
18    StringTools.Set.empty l
19
20let triple_union
21    (var_names1, cost_labels1, user_labels1)
22    (var_names2, cost_labels2, user_labels2) =
23  (StringTools.Set.union var_names1 var_names2,
24   CostLabel.Set.union cost_labels1 cost_labels2,
25   Label.Set.union user_labels1 user_labels2)
26
27let empty_triple = (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
28
29let list_union l = List.fold_left triple_union empty_triple l
30
31let rec exp_idents e =
32  let Clight.Expr (e, _) = e in
33  match e with
34    | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Esizeof _ ->
35        empty_triple
36    | Clight.Evar x ->
37        (StringTools.Set.singleton x, CostLabel.Set.empty, Label.Set.empty)
38    | Clight.Ederef e | Clight.Eaddrof e | Clight.Eunop (_, e)
39    | Clight.Ecast (_, e) -> exp_idents e
40    | Clight.Efield (e, x) ->
41        let (var_names, cost_labels, user_labels) = exp_idents e in
42        (StringTools.Set.add x var_names, cost_labels, user_labels)
43    | Clight.Ebinop (_, e1, e2) | Clight.Eandbool (e1, e2)
44    | Clight.Eorbool (e1, e2) -> list_union [exp_idents e1 ; exp_idents e2]
45    | Clight.Econdition (e1, e2, e3) ->
46        list_union [exp_idents e1 ; exp_idents e2 ; exp_idents e3]
47    | Clight.Ecost (lbl, e) ->
48        let (var_names, cost_labels, user_labels) = exp_idents e in
49        (var_names, CostLabel.Set.add lbl cost_labels, user_labels)
50    | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen *)
51
52let exp_idents_opt = function
53  | None -> empty_triple
54  | Some e -> exp_idents e
55
56let exp_idents_list l = list_union (List.map exp_idents l)
57
58let rec body_idents = function
59  | Clight.Sskip | Clight.Sbreak | Clight.Scontinue -> empty_triple
60  | Clight.Sassign (e1, e2) -> list_union [exp_idents e1 ; exp_idents e2]
61  | Clight.Scall (eopt, f, args) ->
62      list_union [exp_idents_opt eopt ; exp_idents f ; exp_idents_list args]
63  | Clight.Ssequence (s1, s2) -> list_union [body_idents s1 ; body_idents s2]
64  | Clight.Sifthenelse (e, s1, s2) ->
65      list_union [exp_idents e ; body_idents s1 ; body_idents s2]
66  | Clight.Swhile (e, s) | Clight.Sdowhile (e, s) ->
67      list_union [exp_idents e ; body_idents s]
68  | Clight.Sfor (s1, e, s2, s3) ->
69      list_union [body_idents s1 ; exp_idents e ;
70                  body_idents s2 ; body_idents s3]
71  | Clight.Sreturn eopt -> exp_idents_opt eopt
72  | Clight.Sswitch (e, ls) -> list_union [exp_idents e ; ls_idents ls]
73  | Clight.Slabel (lbl, stmt) ->
74      let (var_names, cost_labels, user_labels) = body_idents stmt in
75      (var_names, cost_labels, Label.Set.add lbl user_labels)
76  | Clight.Sgoto lbl ->
77      (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.singleton lbl)
78  | Clight.Scost (lbl, stmt) ->
79      let (var_names, cost_labels, user_labels) = body_idents stmt in
80      (var_names, CostLabel.Set.add lbl cost_labels, user_labels)
81and ls_idents = function
82  | Clight.LSdefault stmt -> body_idents stmt
83  | Clight.LScase (_, stmt, ls) -> list_union [body_idents stmt ; ls_idents ls]
84
85let prog_idents p =
86  let def_idents = function
87    | Clight.Internal def ->
88        let vars =
89          string_set_of_list
90            (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
91        let (var_names, cost_labels, user_labels) =
92          body_idents def.Clight.fn_body in
93        (StringTools.Set.union vars var_names, cost_labels, user_labels)
94    | Clight.External (id, _, _) ->
95        (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
96  let fun_idents (id, f_def) =
97    let (var_names, cost_labels, user_labels) = def_idents f_def in
98    (StringTools.Set.add id var_names, cost_labels, user_labels) in
99  let f idents def = triple_union idents (fun_idents def) in
100  List.fold_left f empty_triple p.Clight.prog_funct
101
102let var_names p =
103  let (var_names, _, _) = prog_idents p in var_names
104let cost_labels p =
105  let (_, cost_labels, _) = prog_idents p in cost_labels
106let user_labels p =
107  let (_, _, user_labels) = prog_idents p in user_labels
108
109let all_labels p =
110  let (_, cost_labels, user_labels) = prog_idents p in
111  let all =
112    CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls)
113      cost_labels StringTools.Set.empty in
114  Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all
115
116
117(* Instrumentation *)
118
119let int_typ = Clight.Tint (Clight.I32, Clight.Signed)
120
121let const_int i = Clight.Expr (Clight.Econst_int i, int_typ)
122
123(* Instrument an expression. *)
124
125let rec instrument_expr cost_mapping cost_incr e =
126  let Clight.Expr (e, t) = e in
127  match e with
128    | Clight.Ecost (lbl, e) when CostLabel.Map.find lbl cost_mapping = 0 ->
129        e
130    | _ ->
131        let e' = instrument_expr_descr cost_mapping cost_incr e in
132        Clight.Expr (e', t)
133and instrument_expr_descr cost_mapping cost_incr e = match e with
134  | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
135  | Clight.Esizeof _ -> e
136  | Clight.Ederef e ->
137      let e' = instrument_expr cost_mapping cost_incr e in
138      Clight.Ederef e'
139  | Clight.Eaddrof e ->
140      let e' = instrument_expr cost_mapping cost_incr e in
141      Clight.Eaddrof e'
142  | Clight.Eunop (op, e) ->
143      let e' = instrument_expr cost_mapping cost_incr e in
144      Clight.Eunop (op, e')
145  | Clight.Ebinop (op, e1, e2) ->
146      let e1' = instrument_expr cost_mapping cost_incr e1 in
147      let e2' = instrument_expr cost_mapping cost_incr e2 in
148      Clight.Ebinop (op, e1', e2')
149  | Clight.Ecast (t, e) ->
150      let e' = instrument_expr cost_mapping cost_incr e in
151      Clight.Ecast (t, e')
152  | Clight.Econdition (e1, e2, e3) ->
153      let e1' = instrument_expr cost_mapping cost_incr e1 in
154      let e2' = instrument_expr cost_mapping cost_incr e2 in
155      let e3' = instrument_expr cost_mapping cost_incr e3 in
156      Clight.Econdition (e1', e2', e3')
157  | Clight.Eandbool (e1, e2) ->
158      let e1' = instrument_expr cost_mapping cost_incr e1 in
159      let e2' = instrument_expr cost_mapping cost_incr e2 in
160      Clight.Eandbool (e1', e2')
161  | Clight.Eorbool (e1, e2) ->
162      let e1' = instrument_expr cost_mapping cost_incr e1 in
163      let e2' = instrument_expr cost_mapping cost_incr e2 in
164      Clight.Eorbool (e1', e2')
165  | Clight.Efield (e, x) ->
166      let e' = instrument_expr cost_mapping cost_incr e in
167      Clight.Efield (e', x)
168  | Clight.Ecost (lbl, e) ->
169      let e' = instrument_expr cost_mapping cost_incr e in
170      let incr = CostLabel.Map.find lbl cost_mapping in
171      Clight.Ecall (cost_incr, const_int incr, e')
172  | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *)
173
174(* Instrument a statement. *)
175
176let rec instrument_body cost_mapping cost_incr stmt = match stmt with
177  | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
178  | Clight.Sgoto _ ->
179      stmt
180  | Clight.Sassign (e1, e2) ->
181      let e1' = instrument_expr cost_mapping cost_incr e1 in
182      let e2' = instrument_expr cost_mapping cost_incr e2 in
183      Clight.Sassign (e1', e2')
184  | Clight.Scall (eopt, f, args) ->
185      let eopt' = match eopt with
186        | None -> None
187        | Some e -> Some (instrument_expr cost_mapping cost_incr e) in
188      let f' = instrument_expr cost_mapping cost_incr f in
189      let args' = List.map (instrument_expr cost_mapping cost_incr) args in
190      Clight.Scall (eopt', f', args')
191  | Clight.Ssequence (s1, s2) ->
192      Clight.Ssequence (instrument_body cost_mapping cost_incr s1,
193                        instrument_body cost_mapping cost_incr s2)
194  | Clight.Sifthenelse (e, s1, s2) ->
195      let e' = instrument_expr cost_mapping cost_incr e in
196      let s1' = instrument_body cost_mapping cost_incr s1 in
197      let s2' = instrument_body cost_mapping cost_incr s2 in
198      Clight.Sifthenelse (e', s1', s2')
199  | Clight.Swhile (e, s) ->
200      let e' = instrument_expr cost_mapping cost_incr e in
201      let s' = instrument_body cost_mapping cost_incr s in
202      Clight.Swhile (e', s')
203  | Clight.Sdowhile (e, s) ->
204      let e' = instrument_expr cost_mapping cost_incr e in
205      let s' = instrument_body cost_mapping cost_incr s in
206      Clight.Sdowhile (e', s')
207  | Clight.Sfor (s1, e, s2, s3) ->
208      let s1' = instrument_body cost_mapping cost_incr s1 in
209      let e' = instrument_expr cost_mapping cost_incr e in
210      let s2' = instrument_body cost_mapping cost_incr s2 in
211      let s3' = instrument_body cost_mapping cost_incr s3 in
212      Clight.Sfor (s1', e', s2', s3')
213  | Clight.Sreturn (Some e) ->
214      let e' = instrument_expr cost_mapping cost_incr e in
215      Clight.Sreturn (Some e')
216  | Clight.Sswitch (e, ls) ->
217      let e' = instrument_expr cost_mapping cost_incr e in
218      let ls' = instrument_ls cost_mapping cost_incr ls in
219      Clight.Sswitch (e', ls')
220  | Clight.Slabel (lbl, s) ->
221      let s' = instrument_body cost_mapping cost_incr s in
222      Clight.Slabel (lbl, s')
223  | Clight.Scost (lbl, s) ->
224      let s' = instrument_body cost_mapping cost_incr s in
225      let incr = CostLabel.Map.find lbl cost_mapping in
226      if incr = 0 then s'
227      else
228        let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
229        let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
230        let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
231        Clight.Ssequence (Clight.Scall (None, f, args), s')
232and instrument_ls cost_mapping cost_incr = function
233  | Clight.LSdefault s ->
234      let s' = instrument_body cost_mapping cost_incr s in
235      Clight.LSdefault s'
236  | Clight.LScase (i, s, ls) ->
237      let s' = instrument_body cost_mapping cost_incr s in
238      let ls' = instrument_ls cost_mapping cost_incr ls in
239      Clight.LScase (i, s', ls')
240
241(* Instrument a function. *)
242
243let instrument_funct cost_mapping cost_incr (id, def) =
244  let def = match def with
245    | Clight.Internal def ->
246        let body = instrument_body cost_mapping cost_incr def.Clight.fn_body in
247        Clight.Internal { def with Clight.fn_body = body }
248    | Clight.External _ -> def
249  in
250  (id, def)
251
252(* This is the declaration of the cost variable. *)
253
254let cost_decl cost_id =
255  let init = [Clight.Init_int32 0] in
256  ((cost_id, init), int_typ)
257
258(* This is the definition of the increment cost function. *)
259
260let cost_incr_def cost_id cost_incr =
261  let int_var x = Clight.Expr (Clight.Evar x, int_typ) in
262  let param = "incr" in
263  let cost = int_var cost_id in
264  let increment = int_var param in
265  let cost_increment =
266    Clight.Expr (Clight.Ebinop (Clight.Oadd, cost, increment), int_typ) in
267  let stmt = Clight.Sassign (cost, cost_increment) in
268  let cfun =
269    { Clight.fn_return = Clight.Tvoid ;
270      Clight.fn_params = [(param, int_typ)] ;
271      Clight.fn_vars   = [] ;
272      Clight.fn_body =   stmt } in
273  (cost_incr, Clight.Internal cfun)
274
275let save_tmp tmp_file s =
276  let cout = open_out tmp_file in
277  output_string cout s ;
278  flush cout ;
279  close_out cout
280
281(** [instrument prog cost_map] instruments the program [prog]. *)
282
283let instrument p cost_mapping =
284
285  (* Create a fresh 'cost' variable. *)
286  let var_names = var_names p in
287  let cost_id = StringTools.Gen.fresh_prefix var_names cost_id_prefix in
288  let cost_decl = cost_decl cost_id in
289
290  (* Define an increment function for the cost variable. *)
291  let cost_incr =
292    StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id var_names)
293      cost_incr_prefix in
294  let cost_incr_def = cost_incr_def cost_id cost_incr in
295
296  (* Instrument each function *)
297  let prog_funct =
298    List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in
299
300  (* Glue all this together. *)
301  let prog_vars = cost_decl :: p.Clight.prog_vars in
302  let prog_funct = cost_incr_def :: prog_funct in
303  let p' =
304    { p with Clight.prog_vars = prog_vars ; Clight.prog_funct = prog_funct } in
305
306  (* Save the resulted program. Then re-parse it.
307     Indeed, the instrumentation may add side-effects in expressions, which is
308     not Clight compliant. Re-parsing the result with CIL will remove these
309     side-effects in expressions to obtain a Clight program. *)
310  let tmp_file = Filename.temp_file "clight_instrument" ".c" in
311  save_tmp tmp_file (ClightPrinter.print_program p') ;
312  let res = ClightParser.process tmp_file in
313  Misc.SysExt.safe_remove tmp_file ;
314  res
315
316
Note: See TracBrowser for help on using the repository browser.