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

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