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

Last change on this file since 1507 was 1507, checked in by tranquil, 9 years ago
  • added an option to not use ternary expressions in costs, to accomodate frama-c explosion of such expressions
  • corrected some typos in comments
  • added a check for well behaved for loops in loop unrolling, but intelligent unrolling is not done yet
  • TODO: peeling and unrolling can contradict preciseness (with difference between introduced branches around 2 cycles). I guess it can be corrected easily
File size: 16.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"
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_gen_cond var gc =
149  assert (not (CostExpr.CondSet.is_empty gc));
150  let c = CostExpr.CondSet.min_elt gc in
151  let c_expr = expr_of_cost_cond var c in
152  let rest = CostExpr.CondSet.remove c gc in
153  if CostExpr.CondSet.is_empty rest then c_expr else
154    let rest_expr = expr_of_cost_gen_cond var rest in
155    Clight.Expr(Clight.Eandbool(c_expr, rest_expr), int_typ)
156
157let rec expr_of_cost_expr prefix = function
158  | CostExpr.Exact k -> const_int k
159  | CostExpr.Ternary(index, cond, if_true, if_false) ->
160    let id = CostLabel.make_id prefix index in
161    let var = Clight.Expr(Clight.Evar id, int_typ) in 
162    let cond_e = expr_of_cost_gen_cond var cond in
163    let if_true_e = expr_of_cost_expr prefix if_true in
164    let if_false_e = expr_of_cost_expr prefix if_false in
165    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
166
167(* as long as Clight parser will be called at the end, this hack works *)
168(* this will be called in case -no-cost-tern is active. *)
169let rec side_effect_expr_of_cost_expr prefix cost_incr cont e_type = function
170  | CostExpr.Exact k ->
171    Clight.Expr(Clight.Ecall (cost_incr, const_int k, cont), e_type)
172  | CostExpr.Ternary(index, cond, if_true, if_false) ->
173    let id = CostLabel.make_id prefix index in
174    let var = Clight.Expr(Clight.Evar id, int_typ) in
175    let cond_e = expr_of_cost_gen_cond var cond in
176    let rec_call = side_effect_expr_of_cost_expr prefix cost_incr cont e_type in
177    let if_true_e = rec_call if_true in
178    let if_false_e = rec_call if_false in
179    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
180
181let rec stmt_of_cost_expr prefix cost_incr = function
182  | CostExpr.Exact k -> Clight.Scall (None, cost_incr, [const_int k])
183  | CostExpr.Ternary(index, cond, if_true, if_false) ->
184    let id = CostLabel.make_id prefix index in
185    let var = Clight.Expr(Clight.Evar id, int_typ) in 
186    let cond_e = expr_of_cost_gen_cond var cond in
187    let if_true_s = stmt_of_cost_expr prefix cost_incr if_true in
188    let if_false_s = stmt_of_cost_expr prefix cost_incr if_false in
189    Clight.Sifthenelse (cond_e, if_true_s, if_false_s)
190
191(* Instrument an expression. *)
192
193(* FIXME: follow cost_tern option *)
194let instrument_expr cost_tern l_ind cost_mapping cost_incr =
195  let f_expr (Clight.Expr(ed, et) as e) sub_res = match ed, sub_res with
196  | Clight.Ecost (lbl, _), e' :: _ ->
197    let atom = lbl.CostLabel.name in
198    let cost =
199      try
200        CostLabel.Atom.Map.find atom cost_mapping
201      with (* if atom is not present, then map to 0 *)
202        | Not_found -> CostExpr.Exact 0 in
203    if cost = CostExpr.Exact 0 then e' else
204      if cost_tern then
205        let cost = expr_of_cost_expr l_ind cost in
206        Clight.Expr(Clight.Ecall (cost_incr, cost, e'), et)
207      else
208        side_effect_expr_of_cost_expr l_ind cost_incr e' et cost
209  | Clight.Ecall (_, _, _), _ -> assert false (* Should not happen. *)
210  | _ -> ClightFold.expr_fill_exprs e sub_res in
211  ClightFold.expr2 f_expr
212
213let loop_increment prefix depth body = match depth  with
214  | None -> body
215  | Some d ->
216    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
217    let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in
218    Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1)))
219     
220let loop_reset_index prefix depth loop = match depth with
221  | None -> loop
222  | Some d ->
223    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
224    Clight.Ssequence(Clight.Sassign(id, const_int 0), loop)
225
226
227(* Instrument a statement. *)
228
229(* not using ClightFold as l_ind changes through loops *)
230let rec instrument_body cost_tern l_ind cost_mapping cost_incr stmt =
231  let instr_expr = instrument_expr cost_tern l_ind cost_mapping cost_incr in
232  let instr_body = instrument_body cost_tern l_ind cost_mapping cost_incr in
233  match stmt with
234    | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
235    | Clight.Sgoto _ ->
236      stmt
237    | Clight.Sassign (e1, e2) ->
238      let e1' = instr_expr e1 in
239      let e2' = instr_expr e2 in
240      Clight.Sassign (e1', e2')
241    | Clight.Scall (eopt, f, args) ->
242      let eopt' = Option.map instr_expr eopt in
243      let f' = instr_expr f in
244      let args = List.map (instr_expr) args in
245      Clight.Scall (eopt', f', args)
246    | Clight.Ssequence (s1, s2) ->
247      Clight.Ssequence (
248        instr_body s1,
249        instr_body s2)
250    | Clight.Sifthenelse (e, s1, s2) ->
251      let e' = instr_expr e in
252      let s1' = instr_body s1 in
253      let s2' = instr_body s2 in
254      Clight.Sifthenelse (e', s1', s2')
255    | Clight.Swhile (i, e, s) ->
256      let e' = instr_expr e in
257      let s' = instr_body s in
258      let s' = loop_increment l_ind i s' in
259      loop_reset_index l_ind i (Clight.Swhile (None, e', s'))
260    | Clight.Sdowhile (i, e, s) ->
261      let e' = instr_expr e in
262      let s' = instr_body s in
263      let s' = loop_increment l_ind i s' in
264      loop_reset_index l_ind i (Clight.Sdowhile (None, e', s'))
265    | Clight.Sfor (i, s1, e, s2, s3) ->
266      let s1' = instr_body s1 in
267      let e' = instr_expr e in
268      let s2' = instr_body s2 in
269      let s3' = instr_body s3 in
270      let s3' = loop_increment l_ind i s3' in
271      loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3'))
272    | Clight.Sreturn (Some e) ->
273      let e' = instr_expr e in
274      Clight.Sreturn (Some e')
275    | Clight.Sswitch (e, ls) ->
276      let e' = instr_expr e in
277      let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
278      Clight.Sswitch (e', ls')
279    | Clight.Slabel (lbl, s) ->
280      let s' = instr_body s in
281      Clight.Slabel (lbl, s')
282    | Clight.Scost (lbl, s) ->
283    (* Keep the cost label in the code. *)
284      let s' = instr_body s in
285      let atom = lbl.CostLabel.name in
286      let cost =
287        try
288          CostLabel.Atom.Map.find atom cost_mapping
289        with (* if atom is not present, then map to 0 *)
290          | Not_found -> CostExpr.Exact 0 in
291      let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
292      let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
293      let cost_stmt =
294        if not cost_tern then stmt_of_cost_expr l_ind f cost else
295        let cost = expr_of_cost_expr l_ind cost in
296        Clight.Scall(None, f, [cost]) in
297      Clight.Scost (lbl, Clight.Ssequence (cost_stmt, s'))
298(*
299  let s' = instrument_body l_ind cost_mapping cost_incr s in
300  let incr = CostLabel.Map.find lbl cost_mapping in
301  if incr = 0 then s'
302  else
303  let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
304  let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
305  let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
306  Clight.Ssequence (Clight.Scall (None, f, args), s')
307*)
308(*
309  instrument_body l_ind cost_mapping cost_incr s
310*)
311and instrument_ls cost_tern l_ind cost_mapping cost_incr = function
312  | Clight.LSdefault s ->
313    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
314    Clight.LSdefault s'
315  | Clight.LScase (i, s, ls) ->
316    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
317    let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
318    Clight.LScase (i, s', ls')
319     
320let rec loop_indexes_defs prefix max_depth =
321  if max_depth = 0 then [] else
322    let max_depth = max_depth - 1 in
323    let id = CostLabel.make_id prefix max_depth in
324    (id, int_typ) :: loop_indexes_defs prefix max_depth
325
326let max_depth =
327  let f_expr _ _ = () in
328  let f_stmt stmt _ res_stmts =
329    let curr_max = List.fold_left max 0 res_stmts in
330    if curr_max > 0 then curr_max else 
331      match stmt with
332        | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_)
333        | Clight.Sfor(Some x,_,_,_,_) -> x + 1
334        | _ -> 0 in
335  ClightFold.statement2 f_expr f_stmt
336
337(* Instrument a function. *)
338
339let instrument_funct cost_tern  l_ind cost_mapping cost_incr (id, def) =
340  let def = match def with
341    | Clight.Internal def ->
342      let max_depth = max_depth def.Clight.fn_body in
343      let vars = loop_indexes_defs l_ind max_depth in
344      let vars = List.rev_append vars def.Clight.fn_vars in
345      let body = def.Clight.fn_body in
346      let body =
347        instrument_body cost_tern l_ind cost_mapping cost_incr body in
348      Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
349    | Clight.External _ -> def
350  in
351  (id, def)
352
353(* This is the declaration of the cost variable. *)
354
355let cost_decl cost_id =
356  let init = [Clight.Init_int32 0] in
357  ((cost_id, init), int_typ)
358
359(* This is the definition of the increment cost function. *)
360
361let cost_incr_def cost_id cost_incr =
362  let int_var x = Clight.Expr (Clight.Evar x, int_typ) in
363  let param = "incr" in
364  let cost = int_var cost_id in
365  let increment = int_var param in
366  let cost_increment =
367    Clight.Expr (Clight.Ebinop (Clight.Oadd, cost, increment), int_typ) in
368  let stmt = Clight.Sassign (cost, cost_increment) in
369  let cfun =
370    { Clight.fn_return = Clight.Tvoid ;
371      Clight.fn_params = [(param, int_typ)] ;
372      Clight.fn_vars   = [] ;
373      Clight.fn_body =   stmt } in
374  (cost_incr, Clight.Internal cfun)
375
376let save_tmp tmp_file s =
377  let cout = open_out tmp_file in
378  output_string cout s ;
379  flush cout ;
380  close_out cout
381   
382   
383(** [instrument prog cost_map] instruments the program [prog]. First a fresh
384    global variable --- the so-called cost variable --- is added to the program.
385    Then, each cost label in the program is replaced by an increment of the cost
386    variable, following the mapping [cost_map]. The function also returns the
387    name of the cost variable and the name of the cost increment function. *)
388
389let instrument cost_tern p cost_mapping =
390
391  (* Create a fresh 'cost' variable. *)
392  let names = names p in
393  let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
394  let cost_decl = cost_decl cost_id in
395
396  (* Create a fresh loop index prefix *)
397  let names = StringTools.Set.add cost_id names in
398  let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in
399
400  (* Define an increment function for the cost variable. *)
401  let cost_incr =
402    StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id names)
403      cost_incr_prefix in
404  let cost_incr_def = cost_incr_def cost_id cost_incr in
405
406  (* Turn the mapping from indexed cost labels to integers into one from *)
407  (* cost atoms to cost expresisons *)
408  let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in
409
410  (* Instrument each function *)
411  let prog_funct = p.Clight.prog_funct in
412  let prog_funct =
413    let f = instrument_funct cost_tern l_ind cost_mapping cost_incr in
414    List.map f prog_funct in
415
416  (* Glue all this together. *)
417  let prog_vars = cost_decl :: p.Clight.prog_vars in
418  let prog_funct = cost_incr_def :: prog_funct in
419  let p' =
420    { p with Clight.prog_vars = prog_vars ; Clight.prog_funct = prog_funct } in
421
422  (* Save the resulted program. Then re-parse it.
423     Indeed, the instrumentation may add side-effects in expressions, which is
424     not Clight compliant. Re-parsing the result with CIL will remove these
425     side-effects in expressions to obtain a Clight program. *)
426  let tmp_file = Filename.temp_file "clight_instrument" ".c" in
427  save_tmp tmp_file (ClightPrinter.print_program p') ;
428  let p' = ClightParser.process tmp_file in
429  Misc.SysExt.safe_remove tmp_file ;
430  (p', cost_id, cost_incr)
Note: See TracBrowser for help on using the repository browser.