source: Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml @ 1305

Last change on this file since 1305 was 1305, checked in by tranquil, 9 years ago

added indexes to loop constructors. Branch does not compile atm

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