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

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

32 and 16 bits operations support in D2.2/8051

File size: 13.1 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    (names1, cost_labels1, user_labels1)
22    (names2, cost_labels2, user_labels2) =
23  (StringTools.Set.union names1 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 name_singleton id =
30  (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty)
31
32let cost_label_singleton cost_lbl =
33  (StringTools.Set.empty, CostLabel.Set.singleton cost_lbl, Label.Set.empty)
34
35let label_singleton lbl =
36  (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.singleton lbl)
37
38let list_union l = List.fold_left triple_union empty_triple l
39
40let f_ctype ctype sub_ctypes_res =
41  let res = match ctype with
42    | Clight.Tstruct (id, fields) | Clight.Tunion (id, fields) ->
43      (string_set_of_list (id :: (List.map fst fields)),
44       CostLabel.Set.empty, Label.Set.empty)
45    | Clight.Tcomp_ptr id -> name_singleton id
46    | _ -> empty_triple in
47  list_union (res :: sub_ctypes_res)
48
49let f_expr _ sub_ctypes_res sub_expr_descrs_res =
50  list_union (sub_ctypes_res @ sub_expr_descrs_res)
51
52let f_expr_descr ed sub_ctypes_res sub_exprs_res =
53  let res = match ed with
54    | Clight.Evar id | Clight.Efield (_, id) | Clight.Ecall (id, _, _) ->
55      name_singleton id
56    | Clight.Ecost (cost_lbl, _) -> cost_label_singleton cost_lbl
57    | _ -> empty_triple in
58  list_union (res :: (sub_ctypes_res @ sub_exprs_res))
59
60let f_stmt stmt sub_exprs_res sub_stmts_res =
61  let stmt_res = match stmt with
62    | Clight.Slabel (lbl, _) | Clight.Sgoto lbl -> label_singleton lbl
63    | Clight.Scost (cost_lbl, _) -> cost_label_singleton cost_lbl
64    | _ -> empty_triple in
65  list_union (stmt_res :: (sub_exprs_res @ sub_stmts_res))
66
67let body_idents = ClightFold.statement f_ctype f_expr f_expr_descr f_stmt
68
69let prog_idents p =
70  let def_idents = function
71    | Clight.Internal def ->
72        let vars =
73          string_set_of_list
74            (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
75        let (names, cost_labels, user_labels) =
76          body_idents def.Clight.fn_body in
77        (StringTools.Set.union vars names, cost_labels, user_labels)
78    | Clight.External (id, _, _) ->
79        (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
80  let fun_idents (id, f_def) =
81    let (names, cost_labels, user_labels) = def_idents f_def in
82    (StringTools.Set.add id names, cost_labels, user_labels) in
83  let f idents def = triple_union idents (fun_idents def) in
84  List.fold_left f empty_triple p.Clight.prog_funct
85
86let names p =
87  let (names, _, _) = prog_idents p in names
88let cost_labels p =
89  let (_, cost_labels, _) = prog_idents p in cost_labels
90let user_labels p =
91  let (_, _, user_labels) = prog_idents p in user_labels
92
93let all_labels p =
94  let (_, cost_labels, user_labels) = prog_idents p in
95  let all =
96    CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls)
97      cost_labels StringTools.Set.empty in
98  Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all
99
100let all_idents p =
101  let (names, cost_labels, user_labels) = prog_idents p in
102  let to_string_set fold set =
103    fold (fun lbl idents -> StringTools.Set.add lbl idents) set
104      StringTools.Set.empty in
105  let cost_labels = to_string_set CostLabel.Set.fold cost_labels in
106  let user_labels = to_string_set Label.Set.fold user_labels in
107  StringTools.Set.union names (StringTools.Set.union cost_labels user_labels)
108
109let fresh_ident base p =
110  StringTools.Gen.fresh_prefix (all_idents p) base
111
112let fresh_universe base p =
113  let universe = fresh_ident base p in
114  StringTools.Gen.new_universe universe
115
116let make_fresh base p =
117  let universe = fresh_universe base p in
118  (fun () -> StringTools.Gen.fresh universe)
119
120
121(* Instrumentation *)
122
123let int_typ = Clight.Tint (Clight.I32, AST.Signed)
124
125let const_int i = Clight.Expr (Clight.Econst_int i, int_typ)
126
127(* Instrument an expression. *)
128
129let rec instrument_expr cost_mapping cost_incr e =
130  let Clight.Expr (e, t) = e in
131  match e with
132    | Clight.Ecost (lbl, e) when CostLabel.Map.find lbl cost_mapping = 0 ->
133        e
134    | _ ->
135        let e' = instrument_expr_descr cost_mapping cost_incr e in
136        Clight.Expr (e', t)
137and instrument_expr_descr cost_mapping cost_incr e = match e with
138  | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
139  | Clight.Esizeof _ -> e
140  | Clight.Ederef e ->
141      let e' = instrument_expr cost_mapping cost_incr e in
142      Clight.Ederef e'
143  | Clight.Eaddrof e ->
144      let e' = instrument_expr cost_mapping cost_incr e in
145      Clight.Eaddrof e'
146  | Clight.Eunop (op, e) ->
147      let e' = instrument_expr cost_mapping cost_incr e in
148      Clight.Eunop (op, e')
149  | Clight.Ebinop (op, e1, e2) ->
150      let e1' = instrument_expr cost_mapping cost_incr e1 in
151      let e2' = instrument_expr cost_mapping cost_incr e2 in
152      Clight.Ebinop (op, e1', e2')
153  | Clight.Ecast (t, e) ->
154      let e' = instrument_expr cost_mapping cost_incr e in
155      Clight.Ecast (t, e')
156  | Clight.Econdition (e1, e2, e3) ->
157      let e1' = instrument_expr cost_mapping cost_incr e1 in
158      let e2' = instrument_expr cost_mapping cost_incr e2 in
159      let e3' = instrument_expr cost_mapping cost_incr e3 in
160      Clight.Econdition (e1', e2', e3')
161  | Clight.Eandbool (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.Eandbool (e1', e2')
165  | Clight.Eorbool (e1, e2) ->
166      let e1' = instrument_expr cost_mapping cost_incr e1 in
167      let e2' = instrument_expr cost_mapping cost_incr e2 in
168      Clight.Eorbool (e1', e2')
169  | Clight.Efield (e, x) ->
170      let e' = instrument_expr cost_mapping cost_incr e in
171      Clight.Efield (e', x)
172  | Clight.Ecost (lbl, e) when CostLabel.Map.mem lbl cost_mapping ->
173      let e' = instrument_expr cost_mapping cost_incr e in
174      let incr = CostLabel.Map.find lbl cost_mapping in
175      if incr = 0 then let Clight.Expr (e'', _) = e' in e''
176      else Clight.Ecall (cost_incr, const_int incr, e')
177  | Clight.Ecost (_, e) ->
178    let Clight.Expr (e', _) = instrument_expr cost_mapping cost_incr e in
179    e'
180  | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *)
181
182(* Instrument a statement. *)
183
184let rec instrument_body cost_mapping cost_incr stmt = match stmt with
185  | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
186  | Clight.Sgoto _ ->
187    stmt
188  | Clight.Sassign (e1, e2) ->
189    let e1' = instrument_expr cost_mapping cost_incr e1 in
190    let e2' = instrument_expr cost_mapping cost_incr e2 in
191    Clight.Sassign (e1', e2')
192  | Clight.Scall (eopt, f, args) ->
193    let eopt' = match eopt with
194      | None -> None
195      | Some e -> Some (instrument_expr cost_mapping cost_incr e) in
196    let f' = instrument_expr cost_mapping cost_incr f in
197    let args' = List.map (instrument_expr cost_mapping cost_incr) args in
198    Clight.Scall (eopt', f', args')
199  | Clight.Ssequence (s1, s2) ->
200    Clight.Ssequence (instrument_body cost_mapping cost_incr s1,
201                      instrument_body cost_mapping cost_incr s2)
202  | Clight.Sifthenelse (e, s1, s2) ->
203    let e' = instrument_expr cost_mapping cost_incr e in
204    let s1' = instrument_body cost_mapping cost_incr s1 in
205    let s2' = instrument_body cost_mapping cost_incr s2 in
206    Clight.Sifthenelse (e', s1', s2')
207  | Clight.Swhile (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.Swhile (e', s')
211  | Clight.Sdowhile (e, s) ->
212    let e' = instrument_expr cost_mapping cost_incr e in
213    let s' = instrument_body cost_mapping cost_incr s in
214    Clight.Sdowhile (e', s')
215  | Clight.Sfor (s1, e, s2, s3) ->
216    let s1' = instrument_body cost_mapping cost_incr s1 in
217    let e' = instrument_expr cost_mapping cost_incr e in
218    let s2' = instrument_body cost_mapping cost_incr s2 in
219    let s3' = instrument_body cost_mapping cost_incr s3 in
220    Clight.Sfor (s1', e', s2', s3')
221  | Clight.Sreturn (Some e) ->
222    let e' = instrument_expr cost_mapping cost_incr e in
223    Clight.Sreturn (Some e')
224  | Clight.Sswitch (e, ls) ->
225    let e' = instrument_expr cost_mapping cost_incr e in
226    let ls' = instrument_ls cost_mapping cost_incr ls in
227    Clight.Sswitch (e', ls')
228  | Clight.Slabel (lbl, s) ->
229    let s' = instrument_body cost_mapping cost_incr s in
230    Clight.Slabel (lbl, s')
231  | Clight.Scost (lbl, s) when CostLabel.Map.mem lbl cost_mapping ->
232    (* Keep the cost label in the code. *)
233    let s' = instrument_body cost_mapping cost_incr s in
234    let incr = CostLabel.Map.find lbl cost_mapping in
235    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
236    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
237    let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
238    Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
239  (*
240    let s' = instrument_body cost_mapping cost_incr s in
241    let incr = CostLabel.Map.find lbl cost_mapping in
242    if incr = 0 then s'
243    else
244    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
245    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
246    let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
247    Clight.Ssequence (Clight.Scall (None, f, args), s')
248  *)
249  | Clight.Scost (lbl, s) ->
250    (* Keep the cost label in the code and show the increment of 0. *)
251    let s' = instrument_body cost_mapping cost_incr s in
252    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
253    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
254    let args = [Clight.Expr (Clight.Econst_int 0, int_typ)] in
255    Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
256  (*
257    instrument_body cost_mapping cost_incr s
258  *)
259and instrument_ls cost_mapping cost_incr = function
260  | Clight.LSdefault s ->
261    let s' = instrument_body cost_mapping cost_incr s in
262    Clight.LSdefault s'
263  | Clight.LScase (i, s, ls) ->
264    let s' = instrument_body cost_mapping cost_incr s in
265    let ls' = instrument_ls cost_mapping cost_incr ls in
266    Clight.LScase (i, s', ls')
267
268(* Instrument a function. *)
269
270let instrument_funct cost_mapping cost_incr (id, def) =
271  let def = match def with
272    | Clight.Internal def ->
273        let body = instrument_body cost_mapping cost_incr def.Clight.fn_body in
274        Clight.Internal { def with Clight.fn_body = body }
275    | Clight.External _ -> def
276  in
277  (id, def)
278
279(* This is the declaration of the cost variable. *)
280
281let cost_decl cost_id =
282  let init = [Clight.Init_int32 0] in
283  ((cost_id, init), int_typ)
284
285(* This is the definition of the increment cost function. *)
286
287let cost_incr_def cost_id cost_incr =
288  let int_var x = Clight.Expr (Clight.Evar x, int_typ) in
289  let param = "incr" in
290  let cost = int_var cost_id in
291  let increment = int_var param in
292  let cost_increment =
293    Clight.Expr (Clight.Ebinop (Clight.Oadd, cost, increment), int_typ) in
294  let stmt = Clight.Sassign (cost, cost_increment) in
295  let cfun =
296    { Clight.fn_return = Clight.Tvoid ;
297      Clight.fn_params = [(param, int_typ)] ;
298      Clight.fn_vars   = [] ;
299      Clight.fn_body =   stmt } in
300  (cost_incr, Clight.Internal cfun)
301
302let save_tmp tmp_file s =
303  let cout = open_out tmp_file in
304  output_string cout s ;
305  flush cout ;
306  close_out cout
307
308(** [instrument prog cost_map] instruments the program [prog]. First a fresh
309    global variable --- the so-called cost variable --- is added to the program.
310    Then, each cost label in the program is replaced by an increment of the cost
311    variable, following the mapping [cost_map]. The function also returns the
312    name of the cost variable and the name of the cost increment function. *)
313
314let instrument p cost_mapping =
315
316  (* Create a fresh 'cost' variable. *)
317  let names = names p in
318  let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
319  let cost_decl = cost_decl cost_id in
320
321  (* Define an increment function for the cost variable. *)
322  let cost_incr =
323    StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id names)
324      cost_incr_prefix in
325  let cost_incr_def = cost_incr_def cost_id cost_incr in
326
327  (* Instrument each function *)
328  let prog_funct =
329    List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in
330
331  (* Glue all this together. *)
332  let prog_vars = cost_decl :: p.Clight.prog_vars in
333  let prog_funct = cost_incr_def :: prog_funct in
334  let p' =
335    { p with Clight.prog_vars = prog_vars ; Clight.prog_funct = prog_funct } in
336
337  (* Save the resulted program. Then re-parse it.
338     Indeed, the instrumentation may add side-effects in expressions, which is
339     not Clight compliant. Re-parsing the result with CIL will remove these
340     side-effects in expressions to obtain a Clight program. *)
341  let tmp_file = Filename.temp_file "clight_instrument" ".c" in
342  save_tmp tmp_file (ClightPrinter.print_program p') ;
343  let res = ClightParser.process tmp_file in
344  Misc.SysExt.safe_remove tmp_file ;
345  (res, cost_id, cost_incr)
Note: See TracBrowser for help on using the repository browser.