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

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

Pretty output in D2.2.

File size: 13.5 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 and fun 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) when CostLabel.Map.mem lbl cost_mapping ->
169      let e' = instrument_expr cost_mapping cost_incr e in
170      let incr = CostLabel.Map.find lbl cost_mapping in
171      if incr = 0 then let Clight.Expr (e'', _) = e' in e''
172      else Clight.Ecall (cost_incr, const_int incr, e')
173  | Clight.Ecost (_, e) ->
174    let Clight.Expr (e', _) = instrument_expr cost_mapping cost_incr e in
175    e'
176  | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *)
177
178(* Instrument a statement. *)
179
180let rec instrument_body cost_mapping cost_incr stmt = match stmt with
181  | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
182  | Clight.Sgoto _ ->
183    stmt
184  | Clight.Sassign (e1, e2) ->
185    let e1' = instrument_expr cost_mapping cost_incr e1 in
186    let e2' = instrument_expr cost_mapping cost_incr e2 in
187    Clight.Sassign (e1', e2')
188  | Clight.Scall (eopt, f, args) ->
189    let eopt' = match eopt with
190      | None -> None
191      | Some e -> Some (instrument_expr cost_mapping cost_incr e) in
192    let f' = instrument_expr cost_mapping cost_incr f in
193    let args' = List.map (instrument_expr cost_mapping cost_incr) args in
194    Clight.Scall (eopt', f', args')
195  | Clight.Ssequence (s1, s2) ->
196    Clight.Ssequence (instrument_body cost_mapping cost_incr s1,
197                      instrument_body cost_mapping cost_incr s2)
198  | Clight.Sifthenelse (e, s1, s2) ->
199    let e' = instrument_expr cost_mapping cost_incr e in
200    let s1' = instrument_body cost_mapping cost_incr s1 in
201    let s2' = instrument_body cost_mapping cost_incr s2 in
202    Clight.Sifthenelse (e', s1', s2')
203  | Clight.Swhile (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.Swhile (e', s')
207  | Clight.Sdowhile (e, s) ->
208    let e' = instrument_expr cost_mapping cost_incr e in
209    let s' = instrument_body cost_mapping cost_incr s in
210    Clight.Sdowhile (e', s')
211  | Clight.Sfor (s1, e, s2, s3) ->
212    let s1' = instrument_body cost_mapping cost_incr s1 in
213    let e' = instrument_expr cost_mapping cost_incr e in
214    let s2' = instrument_body cost_mapping cost_incr s2 in
215    let s3' = instrument_body cost_mapping cost_incr s3 in
216    Clight.Sfor (s1', e', s2', s3')
217  | Clight.Sreturn (Some e) ->
218    let e' = instrument_expr cost_mapping cost_incr e in
219    Clight.Sreturn (Some e')
220  | Clight.Sswitch (e, ls) ->
221    let e' = instrument_expr cost_mapping cost_incr e in
222    let ls' = instrument_ls cost_mapping cost_incr ls in
223    Clight.Sswitch (e', ls')
224  | Clight.Slabel (lbl, s) ->
225    let s' = instrument_body cost_mapping cost_incr s in
226    Clight.Slabel (lbl, s')
227  | Clight.Scost (lbl, s) when CostLabel.Map.mem lbl cost_mapping ->
228    (* Keep the cost label in the code. *)
229    let s' = instrument_body cost_mapping cost_incr s in
230    let incr = CostLabel.Map.find lbl cost_mapping in
231    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
232    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
233    let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
234    Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
235  (*
236    let s' = instrument_body cost_mapping cost_incr s in
237    let incr = CostLabel.Map.find lbl cost_mapping in
238    if incr = 0 then s'
239    else
240    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
241    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
242    let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
243    Clight.Ssequence (Clight.Scall (None, f, args), s')
244  *)
245  | Clight.Scost (lbl, s) ->
246    (* Keep the cost label in the code and show the increment of 0. *)
247    let s' = instrument_body cost_mapping cost_incr s in
248    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
249    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
250    let args = [Clight.Expr (Clight.Econst_int 0, int_typ)] in
251    Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
252  (*
253    instrument_body cost_mapping cost_incr s
254  *)
255and instrument_ls cost_mapping cost_incr = function
256  | Clight.LSdefault s ->
257    let s' = instrument_body cost_mapping cost_incr s in
258    Clight.LSdefault s'
259  | Clight.LScase (i, s, ls) ->
260    let s' = instrument_body cost_mapping cost_incr s in
261    let ls' = instrument_ls cost_mapping cost_incr ls in
262    Clight.LScase (i, s', ls')
263
264(* Instrument a function. *)
265
266let instrument_funct cost_mapping cost_incr (id, def) =
267  let def = match def with
268    | Clight.Internal def ->
269        let body = instrument_body cost_mapping cost_incr def.Clight.fn_body in
270        Clight.Internal { def with Clight.fn_body = body }
271    | Clight.External _ -> def
272  in
273  (id, def)
274
275(* This is the declaration of the cost variable. *)
276
277let cost_decl cost_id =
278  let init = [Clight.Init_int32 0] in
279  ((cost_id, init), int_typ)
280
281(* This is the definition of the increment cost function. *)
282
283let cost_incr_def cost_id cost_incr =
284  let int_var x = Clight.Expr (Clight.Evar x, int_typ) in
285  let param = "incr" in
286  let cost = int_var cost_id in
287  let increment = int_var param in
288  let cost_increment =
289    Clight.Expr (Clight.Ebinop (Clight.Oadd, cost, increment), int_typ) in
290  let stmt = Clight.Sassign (cost, cost_increment) in
291  let cfun =
292    { Clight.fn_return = Clight.Tvoid ;
293      Clight.fn_params = [(param, int_typ)] ;
294      Clight.fn_vars   = [] ;
295      Clight.fn_body =   stmt } in
296  (cost_incr, Clight.Internal cfun)
297
298let save_tmp tmp_file s =
299  let cout = open_out tmp_file in
300  output_string cout s ;
301  flush cout ;
302  close_out cout
303
304(** [instrument prog cost_map] instruments the program [prog]. First a fresh
305    global variable --- the so-called cost variable --- is added to the program.
306    Then, each cost label in the program is replaced by an increment of the cost
307    variable, following the mapping [cost_map]. The function also returns the
308    name of the cost variable and the name of the cost increment function. *)
309
310let instrument p cost_mapping =
311
312  (* Create a fresh 'cost' variable. *)
313  let var_names = var_names p in
314  let cost_id = StringTools.Gen.fresh_prefix var_names cost_id_prefix in
315  let cost_decl = cost_decl cost_id in
316
317  (* Define an increment function for the cost variable. *)
318  let cost_incr =
319    StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id var_names)
320      cost_incr_prefix in
321  let cost_incr_def = cost_incr_def cost_id cost_incr in
322
323  (* Instrument each function *)
324  let prog_funct =
325    List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in
326
327  (* Glue all this together. *)
328  let prog_vars = cost_decl :: p.Clight.prog_vars in
329  let prog_funct = cost_incr_def :: prog_funct in
330  let p' =
331    { p with Clight.prog_vars = prog_vars ; Clight.prog_funct = prog_funct } in
332
333  (* Save the resulted program. Then re-parse it.
334     Indeed, the instrumentation may add side-effects in expressions, which is
335     not Clight compliant. Re-parsing the result with CIL will remove these
336     side-effects in expressions to obtain a Clight program. *)
337  let tmp_file = Filename.temp_file "clight_instrument" ".c" in
338  save_tmp tmp_file (ClightPrinter.print_program p') ;
339  let res = ClightParser.process tmp_file in
340  Misc.SysExt.safe_remove tmp_file ;
341  (res, cost_id, cost_incr)
Note: See TracBrowser for help on using the repository browser.