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

Last change on this file since 1433 was 1433, checked in by tranquil, 8 years ago
  • added infrastructure to add same-language transformations along the compilation chain from command line options
  • started work on cost expression semplification
File size: 16.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
130let expr_of_cost_cond var = function
131  | CostExpr.Ceq k ->
132    Clight.Expr(Clight.Ebinop(Clight.Oeq, var, const_int k),int_typ) 
133  | CostExpr.Cgeq k ->
134    Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) 
135  | CostExpr.Cmod (a, b) ->
136    let modulus =
137      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
138    Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ)
139  | CostExpr.Cgeqmod (k, a, b) ->
140    let modulus =
141      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
142        let modulus_eq =
143             Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ) in
144        let greater =
145            Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) in
146    Clight.Expr(Clight.Eandbool(modulus_eq, greater),int_typ)
147 
148let rec expr_of_cost_expr prefix = function
149    | CostExpr.Exact k -> const_int k
150    | CostExpr.Ternary(index, cond, if_true, if_false) ->
151    let id = CostLabel.make_id prefix index in
152    let var = Clight.Expr(Clight.Evar id, int_typ) in 
153    let cond_e = expr_of_cost_cond var cond in
154    let if_true_e = expr_of_cost_expr prefix if_true in
155    let if_false_e = expr_of_cost_expr prefix if_false in
156    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)   
157
158(* Instrument an expression. *)
159
160let rec instrument_expr l_ind cost_mapping cost_incr e =
161  let Clight.Expr (e, t) = e in
162        let e' = instrument_expr_descr l_ind cost_mapping cost_incr e in
163        Clight.Expr (e', t)
164and instrument_expr_descr l_ind cost_mapping cost_incr e = match e with
165  | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
166  | Clight.Esizeof _ -> e
167  | Clight.Ederef e ->
168      let e' = instrument_expr l_ind cost_mapping cost_incr e in
169      Clight.Ederef e'
170  | Clight.Eaddrof e ->
171      let e' = instrument_expr l_ind cost_mapping cost_incr e in
172      Clight.Eaddrof e'
173  | Clight.Eunop (op, e) ->
174      let e' = instrument_expr l_ind cost_mapping cost_incr e in
175      Clight.Eunop (op, e')
176  | Clight.Ebinop (op, e1, e2) ->
177      let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
178      let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
179      Clight.Ebinop (op, e1', e2')
180  | Clight.Ecast (t, e) ->
181      let e' = instrument_expr l_ind cost_mapping cost_incr e in
182      Clight.Ecast (t, e')
183  | Clight.Econdition (e1, e2, e3) ->
184      let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
185      let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
186      let e3' = instrument_expr l_ind cost_mapping cost_incr e3 in
187      Clight.Econdition (e1', e2', e3')
188  | Clight.Eandbool (e1, e2) ->
189      let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
190      let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
191      Clight.Eandbool (e1', e2')
192  | Clight.Eorbool (e1, e2) ->
193      let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
194      let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
195      Clight.Eorbool (e1', e2')
196  | Clight.Efield (e, x) ->
197      let e' = instrument_expr l_ind cost_mapping cost_incr e in
198      Clight.Efield (e', x)
199  | Clight.Ecost (lbl, e) ->
200      let e' = instrument_expr l_ind cost_mapping cost_incr e in
201            let atom = lbl.CostLabel.name in
202            let cost =
203                try
204                    CostLabel.Atom.Map.find atom cost_mapping
205                with (* if atom is not present, then map to 0 *)
206                    | Not_found -> CostExpr.Exact 0 in
207      if cost = CostExpr.Exact 0 then let Clight.Expr (e'', _) = e' in e''
208      else let cost = expr_of_cost_expr l_ind cost in 
209                  Clight.Ecall (cost_incr, cost, e')
210  | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *)
211
212let loop_increment prefix depth body = match depth  with
213        | None -> body
214        | Some d ->
215                let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
216                let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in
217                Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1)))
218               
219let loop_reset_index prefix depth loop = match depth with
220        | None -> loop
221        | Some d ->
222    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
223    Clight.Ssequence(Clight.Sassign(id, const_int 0), loop)
224
225
226(* Instrument a statement. *)
227
228let rec instrument_body l_ind cost_mapping cost_incr stmt = match stmt with
229  | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
230  | Clight.Sgoto _ ->
231    stmt
232  | Clight.Sassign (e1, e2) ->
233    let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
234    let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
235    Clight.Sassign (e1', e2')
236  | Clight.Scall (eopt, f, args) ->
237    let eopt' = match eopt with
238      | None -> None
239      | Some e -> Some (instrument_expr l_ind cost_mapping cost_incr e) in
240    let f' = instrument_expr l_ind cost_mapping cost_incr f in
241    let args' = List.map (instrument_expr l_ind cost_mapping cost_incr) args in
242    Clight.Scall (eopt', f', args')
243  | Clight.Ssequence (s1, s2) ->
244    Clight.Ssequence (instrument_body l_ind cost_mapping cost_incr s1,
245                      instrument_body l_ind cost_mapping cost_incr s2)
246  | Clight.Sifthenelse (e, s1, s2) ->
247    let e' = instrument_expr l_ind cost_mapping cost_incr e in
248    let s1' = instrument_body l_ind cost_mapping cost_incr s1 in
249    let s2' = instrument_body l_ind cost_mapping cost_incr s2 in
250    Clight.Sifthenelse (e', s1', s2')
251  | Clight.Swhile (i, e, s) ->
252    let e' = instrument_expr l_ind cost_mapping cost_incr e in
253    let s' = instrument_body l_ind cost_mapping cost_incr s in
254                let s' = loop_increment l_ind i s' in
255    loop_reset_index l_ind i (Clight.Swhile (None, e', s'))
256  | Clight.Sdowhile (i, e, s) ->
257    let e' = instrument_expr l_ind cost_mapping cost_incr e in
258    let s' = instrument_body l_ind cost_mapping cost_incr s in
259    let s' = loop_increment l_ind i s' in
260    loop_reset_index l_ind i (Clight.Sdowhile (None, e', s'))
261  | Clight.Sfor (i, s1, e, s2, s3) ->
262    let s1' = instrument_body l_ind cost_mapping cost_incr s1 in
263    let e' = instrument_expr l_ind cost_mapping cost_incr e in
264    let s2' = instrument_body l_ind cost_mapping cost_incr s2 in
265    let s3' = instrument_body l_ind cost_mapping cost_incr s3 in
266    let s3' = loop_increment l_ind i s3' in
267                loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3'))
268  | Clight.Sreturn (Some e) ->
269    let e' = instrument_expr l_ind cost_mapping cost_incr e in
270    Clight.Sreturn (Some e')
271  | Clight.Sswitch (e, ls) ->
272    let e' = instrument_expr l_ind cost_mapping cost_incr e in
273    let ls' = instrument_ls l_ind cost_mapping cost_incr ls in
274    Clight.Sswitch (e', ls')
275  | Clight.Slabel (lbl, s) ->
276    let s' = instrument_body l_ind cost_mapping cost_incr s in
277    Clight.Slabel (lbl, s')
278  | Clight.Scost (lbl, s) ->
279    (* Keep the cost label in the code. *)
280    let s' = instrument_body l_ind cost_mapping cost_incr s in
281                let atom = lbl.CostLabel.name in
282                let cost =
283                        try
284                                CostLabel.Atom.Map.find atom cost_mapping
285                        with (* if atom is not present, then map to 0 *)
286                                | Not_found -> CostExpr.Exact 0 in
287                let cost = expr_of_cost_expr l_ind cost in 
288    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
289    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
290    Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, [cost]), s'))
291  (*
292    let s' = instrument_body l_ind cost_mapping cost_incr s in
293    let incr = CostLabel.Map.find lbl cost_mapping in
294    if incr = 0 then s'
295    else
296    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
297    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
298    let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
299    Clight.Ssequence (Clight.Scall (None, f, args), s')
300  *)
301  (*
302    instrument_body l_ind cost_mapping cost_incr s
303  *)
304and instrument_ls l_ind cost_mapping cost_incr = function
305  | Clight.LSdefault s ->
306    let s' = instrument_body l_ind cost_mapping cost_incr s in
307    Clight.LSdefault s'
308  | Clight.LScase (i, s, ls) ->
309    let s' = instrument_body l_ind cost_mapping cost_incr s in
310    let ls' = instrument_ls l_ind cost_mapping cost_incr ls in
311    Clight.LScase (i, s', ls')
312               
313let rec loop_indexes_defs prefix max_depth =
314        if max_depth = 0 then [] else
315        let max_depth = max_depth - 1 in
316        let id = CostLabel.make_id prefix max_depth in
317        (id, int_typ) :: loop_indexes_defs prefix max_depth
318
319let max_depth =
320        let f_expr _ _ = () in
321        let f_stmt stmt _ res_stmts =
322                let curr_max = List.fold_left max 0 res_stmts in
323                if curr_max > 0 then curr_max else     
324                match stmt with
325                | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_)
326                | Clight.Sfor(Some x,_,_,_,_) -> x + 1
327                | _ -> 0 in
328        ClightFold.statement2 f_expr f_stmt
329
330(* Instrument a function. *)
331
332let instrument_funct l_ind cost_mapping cost_incr (id, def) =
333  let def = match def with
334    | Clight.Internal def ->
335        let max_depth = max_depth def.Clight.fn_body in
336        let vars = loop_indexes_defs l_ind max_depth in
337        let vars = List.rev_append vars def.Clight.fn_vars in
338        let body = instrument_body l_ind cost_mapping cost_incr def.Clight.fn_body in
339        Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
340    | Clight.External _ -> def
341  in
342  (id, def)
343
344(* This is the declaration of the cost variable. *)
345
346let cost_decl cost_id =
347  let init = [Clight.Init_int32 0] in
348  ((cost_id, init), int_typ)
349
350(* This is the definition of the increment cost function. *)
351
352let cost_incr_def cost_id cost_incr =
353  let int_var x = Clight.Expr (Clight.Evar x, int_typ) in
354  let param = "incr" in
355  let cost = int_var cost_id in
356  let increment = int_var param in
357  let cost_increment =
358    Clight.Expr (Clight.Ebinop (Clight.Oadd, cost, increment), int_typ) in
359  let stmt = Clight.Sassign (cost, cost_increment) in
360  let cfun =
361    { Clight.fn_return = Clight.Tvoid ;
362      Clight.fn_params = [(param, int_typ)] ;
363      Clight.fn_vars   = [] ;
364      Clight.fn_body =   stmt } in
365  (cost_incr, Clight.Internal cfun)
366
367let save_tmp tmp_file s =
368  let cout = open_out tmp_file in
369  output_string cout s ;
370  flush cout ;
371  close_out cout
372       
373       
374(** [instrument prog cost_map] instruments the program [prog]. First a fresh
375    global variable --- the so-called cost variable --- is added to the program.
376    Then, each cost label in the program is replaced by an increment of the cost
377    variable, following the mapping [cost_map]. The function also returns the
378    name of the cost variable and the name of the cost increment function. *)
379
380let instrument p cost_mapping =
381
382  (* Create a fresh 'cost' variable. *)
383  let names = names p in
384  let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
385  let cost_decl = cost_decl cost_id in
386       
387        (* Create a fresh loop index prefix *)
388        let names = StringTools.Set.add cost_id names in
389  let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in
390
391  (* Define an increment function for the cost variable. *)
392  let cost_incr =
393    StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id names)
394      cost_incr_prefix in
395  let cost_incr_def = cost_incr_def cost_id cost_incr in
396
397  (* Turn the mapping from indexed cost labels to integers into one from *)
398        (* cost atoms to cost expresisons *)
399        let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in
400
401  (* Instrument each function *)
402  let prog_funct = p.Clight.prog_funct in
403        let prog_funct = 
404    List.map (instrument_funct l_ind cost_mapping cost_incr) prog_funct in
405
406  (* Glue all this together. *)
407  let prog_vars = cost_decl :: p.Clight.prog_vars in
408  let prog_funct = cost_incr_def :: prog_funct in
409  let p' =
410    { p with Clight.prog_vars = prog_vars ; Clight.prog_funct = prog_funct } in
411
412  (* Save the resulted program. Then re-parse it.
413     Indeed, the instrumentation may add side-effects in expressions, which is
414     not Clight compliant. Re-parsing the result with CIL will remove these
415     side-effects in expressions to obtain a Clight program. *)
416  let tmp_file = Filename.temp_file "clight_instrument" ".c" in
417  save_tmp tmp_file (ClightPrinter.print_program p') ;
418  let res = ClightParser.process tmp_file in
419  Misc.SysExt.safe_remove tmp_file ;
420  (res, cost_id, cost_incr)
Note: See TracBrowser for help on using the repository browser.