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

Last change on this file was 1542, checked in by tranquil, 8 years ago

merge of indexed labels branch

File size: 16.9 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 = (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 cost_lbl =
34  (StringTools.Set.empty, CostLabel.Set.singleton cost_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, Label.Set.empty) in
81  let fun_idents (id, f_def) =
82    let (names, cost_labels, user_labels) = def_idents f_def in
83    (StringTools.Set.add id names, cost_labels, user_labels) in
84  let f idents def = triple_union idents (fun_idents def) in
85  List.fold_left f empty_triple p.Clight.prog_funct
86
87let names p =
88  let (names, _, _) = prog_idents p in names
89let cost_labels p =
90  let (_, cost_labels, _) = prog_idents p in cost_labels
91let user_labels p =
92  let (_, _, user_labels) = prog_idents p in user_labels
93
94let all_labels p =
95  let (_, cost_labels, user_labels) = prog_idents p in
96  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in 
97  let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
98  Label.Set.fold StringTools.Set.add user_labels all
99
100let all_idents p =
101  let (names, cost_labels, user_labels) = prog_idents p in
102  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
103  let cost_labels = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
104  let to_string_set fold set =
105    fold (fun lbl idents -> StringTools.Set.add lbl idents) set
106      StringTools.Set.empty in
107  let user_labels = to_string_set Label.Set.fold user_labels in
108  StringTools.Set.union names (StringTools.Set.union cost_labels user_labels)
109
110let fresh_ident base p =
111  StringTools.Gen.fresh_prefix (all_idents p) base
112
113let fresh_universe base p =
114  let universe = fresh_ident base p in
115  StringTools.Gen.new_universe universe
116
117let make_fresh base p =
118  let universe = fresh_universe base p in
119  (fun () -> StringTools.Gen.fresh universe)
120
121
122(* Instrumentation *)
123
124let int_typ = Clight.Tint (Clight.I32, AST.Signed)
125
126let const_int i = Clight.Expr (Clight.Econst_int i, int_typ)
127
128let expr_of_cost_cond var = function
129  | CostExpr.Ceq k ->
130    Clight.Expr(Clight.Ebinop(Clight.Oeq, var, const_int k),int_typ) 
131  | CostExpr.Cgeq k ->
132    Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) 
133  | CostExpr.Cmod (a, b) ->
134    let modulus =
135      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
136    Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ)
137  | CostExpr.Cgeqmod (k, a, b) ->
138    let modulus =
139      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
140    let modulus_eq =
141      Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ) in
142    let greater =
143      Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) in
144    Clight.Expr(Clight.Eandbool(modulus_eq, greater),int_typ)
145
146let rec expr_of_cost_gen_cond var gc =
147  assert (not (CostExpr.CondSet.is_empty gc));
148  let c = CostExpr.CondSet.min_elt gc in
149  let c_expr = expr_of_cost_cond var c in
150  let rest = CostExpr.CondSet.remove c gc in
151  if CostExpr.CondSet.is_empty rest then c_expr else
152    let rest_expr = expr_of_cost_gen_cond var rest in
153    Clight.Expr(Clight.Eandbool(c_expr, rest_expr), int_typ)
154
155let rec expr_of_cost_expr prefix = function
156  | CostExpr.Exact k -> const_int k
157  | CostExpr.Ternary(index, cond, if_true, if_false) ->
158    let id = CostLabel.make_id prefix index in
159    let var = Clight.Expr(Clight.Evar id, int_typ) in 
160    let cond_e = expr_of_cost_gen_cond var cond in
161    let if_true_e = expr_of_cost_expr prefix if_true in
162    let if_false_e = expr_of_cost_expr prefix if_false in
163    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
164
165(* as long as Clight parser will be called at the end, this hack works *)
166(* this will be called in case -no-cost-tern is active. *)
167let rec side_effect_expr_of_cost_expr prefix cost_incr cont e_type = function
168  | CostExpr.Exact k ->
169    Clight.Expr(Clight.Ecall (cost_incr, const_int k, cont), e_type)
170  | CostExpr.Ternary(index, cond, if_true, if_false) ->
171    let id = CostLabel.make_id prefix index in
172    let var = Clight.Expr(Clight.Evar id, int_typ) in
173    let cond_e = expr_of_cost_gen_cond var cond in
174    let rec_call = side_effect_expr_of_cost_expr prefix cost_incr cont e_type in
175    let if_true_e = rec_call if_true in
176    let if_false_e = rec_call if_false in
177    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
178
179let rec stmt_of_cost_expr prefix cost_incr = function
180  | CostExpr.Exact k -> Clight.Scall (None, cost_incr, [const_int k])
181  | CostExpr.Ternary(index, cond, if_true, if_false) ->
182    let id = CostLabel.make_id prefix index in
183    let var = Clight.Expr(Clight.Evar id, int_typ) in 
184    let cond_e = expr_of_cost_gen_cond var cond in
185    let if_true_s = stmt_of_cost_expr prefix cost_incr if_true in
186    let if_false_s = stmt_of_cost_expr prefix cost_incr if_false in
187    Clight.Sifthenelse (cond_e, if_true_s, if_false_s)
188
189(* Instrument an expression. *)
190
191(* FIXME: currently using a hack (reparsing) *)
192let instrument_expr cost_tern l_ind cost_mapping cost_incr =
193  let f_expr (Clight.Expr(ed, et) as e) sub_res = match ed, sub_res with
194  | Clight.Ecost (lbl, _), e' :: _ ->
195    let atom = lbl.CostLabel.name in
196    let cost =
197      try
198        CostLabel.Atom.Map.find atom cost_mapping
199      with (* if atom is not present, then map to 0 *)
200        | Not_found -> CostExpr.Exact 0 in
201    if cost = CostExpr.Exact 0 then e' else
202      if cost_tern then
203        let cost = expr_of_cost_expr l_ind cost in
204        Clight.Expr(Clight.Ecall (cost_incr, cost, e'), et)
205      else
206        side_effect_expr_of_cost_expr l_ind cost_incr e' et cost
207  | Clight.Ecall (_, _, _), _ -> assert false (* Should not happen. *)
208  | _ -> ClightFold.expr_fill_exprs e sub_res in
209  ClightFold.expr2 f_expr
210
211let loop_increment prefix depth body = match depth  with
212  | None -> body
213  | Some d ->
214    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
215    let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in
216    Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1)))
217     
218let loop_reset_index prefix depth loop = match depth with
219  | None -> loop
220  | Some d ->
221    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
222    Clight.Ssequence(Clight.Sassign(id, const_int 0), loop)
223
224
225(* Instrument a statement. *)
226
227(* FIXME: use ClightFold, a much better option *)
228let rec instrument_body cost_tern l_ind cost_mapping cost_incr stmt =
229  let instr_expr = instrument_expr cost_tern l_ind cost_mapping cost_incr in
230  let instr_body = instrument_body cost_tern l_ind cost_mapping cost_incr in
231  match stmt with
232    | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
233    | Clight.Sgoto _ ->
234      stmt
235    | Clight.Sassign (e1, e2) ->
236      let e1' = instr_expr e1 in
237      let e2' = instr_expr e2 in
238      Clight.Sassign (e1', e2')
239    | Clight.Scall (eopt, f, args) ->
240      let eopt' = Option.map instr_expr eopt in
241      let f' = instr_expr f in
242      let args = List.map (instr_expr) args in
243      Clight.Scall (eopt', f', args)
244    | Clight.Ssequence (s1, s2) ->
245      Clight.Ssequence (
246        instr_body s1,
247        instr_body s2)
248    | Clight.Sifthenelse (e, s1, s2) ->
249      let e' = instr_expr e in
250      let s1' = instr_body s1 in
251      let s2' = instr_body s2 in
252      Clight.Sifthenelse (e', s1', s2')
253    | Clight.Swhile (i, e, s) ->
254      let e' = instr_expr e in
255      let s' = instr_body s in
256      let s' = loop_increment l_ind i s' in
257      loop_reset_index l_ind i (Clight.Swhile (None, e', s'))
258    | Clight.Sdowhile (i, e, s) ->
259      let e' = instr_expr e in
260      let s' = instr_body s in
261      let s' = loop_increment l_ind i s' in
262      loop_reset_index l_ind i (Clight.Sdowhile (None, e', s'))
263    | Clight.Sfor (i, s1, e, s2, s3) ->
264      let s1' = instr_body s1 in
265      let e' = instr_expr e in
266      let s2' = instr_body s2 in
267      let s3' = instr_body s3 in
268      let s3' = loop_increment l_ind i s3' in
269      loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3'))
270    | Clight.Sreturn (Some e) ->
271      let e' = instr_expr e in
272      Clight.Sreturn (Some e')
273    | Clight.Sswitch (e, ls) ->
274      let e' = instr_expr e in
275      let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
276      Clight.Sswitch (e', ls')
277    | Clight.Slabel (lbl, s) ->
278      let s' = instr_body s in
279      Clight.Slabel (lbl, s')
280    | Clight.Scost (lbl, s) ->
281    (* Keep the cost label in the code. *)
282      let s' = instr_body s in
283      let atom = lbl.CostLabel.name in
284      let cost =
285        try
286          CostLabel.Atom.Map.find atom cost_mapping
287        with (* if atom is not present, then map to 0 *)
288          | Not_found -> CostExpr.Exact 0 in
289      let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
290      let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
291      let cost_stmt =
292        if not cost_tern then stmt_of_cost_expr l_ind f cost else
293        let cost = expr_of_cost_expr l_ind cost in
294        Clight.Scall(None, f, [cost]) in
295      Clight.Scost (lbl, Clight.Ssequence (cost_stmt, s'))
296(*
297  let s' = instrument_body l_ind cost_mapping cost_incr s in
298  let incr = CostLabel.Map.find lbl cost_mapping in
299  if incr = 0 then s'
300  else
301  let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
302  let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
303  let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
304  Clight.Ssequence (Clight.Scall (None, f, args), s')
305*)
306(*
307  instrument_body l_ind cost_mapping cost_incr s
308*)
309and instrument_ls cost_tern l_ind cost_mapping cost_incr = function
310  | Clight.LSdefault s ->
311    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
312    Clight.LSdefault s'
313  | Clight.LScase (i, s, ls) ->
314    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
315    let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
316    Clight.LScase (i, s', ls')
317     
318let rec loop_indexes_defs prefix max_depth =
319  if max_depth = 0 then [] else
320    let max_depth = max_depth - 1 in
321    let id = CostLabel.make_id prefix max_depth in
322    (id, int_typ) :: loop_indexes_defs prefix max_depth
323
324let max_depth =
325  let f_expr _ _ = () in
326  let f_stmt stmt _ res_stmts =
327    let curr_max = List.fold_left max 0 res_stmts in
328    if curr_max > 0 then curr_max else 
329      match stmt with
330        | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_)
331        | Clight.Sfor(Some x,_,_,_,_) -> x + 1
332        | _ -> 0 in
333  ClightFold.statement2 f_expr f_stmt
334
335(* Instrument a function. *)
336
337let instrument_funct cost_tern  l_ind cost_mapping cost_incr (id, def) =
338  let def = match def with
339    | Clight.Internal def ->
340      let max_depth = max_depth def.Clight.fn_body in
341      let vars = loop_indexes_defs l_ind max_depth in
342      let vars = List.rev_append vars def.Clight.fn_vars in
343      let body = def.Clight.fn_body in
344      let body =
345        instrument_body cost_tern l_ind cost_mapping cost_incr body in
346      Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
347    | Clight.External _ -> def
348  in
349  (id, def)
350
351(* This is the declaration of the cost variable. *)
352
353let cost_decl cost_id =
354  let init = [Clight.Init_int32 0] in
355  ((cost_id, init), int_typ)
356
357(* This is the definition of the increment cost function. *)
358
359let cost_incr_def cost_id cost_incr =
360  let int_var x = Clight.Expr (Clight.Evar x, int_typ) in
361  let param = "incr" in
362  let cost = int_var cost_id in
363  let increment = int_var param in
364  let cost_increment =
365    Clight.Expr (Clight.Ebinop (Clight.Oadd, cost, increment), int_typ) in
366  let stmt = Clight.Sassign (cost, cost_increment) in
367  let cfun =
368    { Clight.fn_return = Clight.Tvoid ;
369      Clight.fn_params = [(param, int_typ)] ;
370      Clight.fn_vars   = [] ;
371      Clight.fn_body =   stmt } in
372  (cost_incr, Clight.Internal cfun)
373
374(* Create a fresh uninitialized cost variable for each external function. This
375   will be used by the Cost plug-in of the Frama-C platform. *)
376
377let extern_cost_variables make_unique functs =
378  let prefix = "_cost_of_" in
379  let f (decls, map) (_, def) = match def with
380    | Clight.Internal _ -> (decls, map)
381    | Clight.External (id, _, _) ->
382      let new_var = make_unique (prefix ^ id) in
383      (decls @ [cost_decl new_var], StringTools.Map.add id new_var map) in
384  List.fold_left f ([], StringTools.Map.empty) functs
385
386let save_tmp tmp_file s =
387  let cout = open_out tmp_file in
388  output_string cout s ;
389  flush cout ;
390  close_out cout
391
392(** [instrument prog cost_map] instruments the program [prog]. First a fresh
393    global variable --- the so-called cost variable --- is added to the program.
394    Then, each cost label in the program is replaced by an increment of the cost
395    variable, following the mapping [cost_map]. The function also returns the
396    name of the cost variable and the name of the cost increment function. *)
397
398let instrument cost_tern p cost_mapping =
399
400  (* Create a fresh 'cost' variable. *)
401  let names = names p in
402  let make_unique = StringTools.make_unique names in
403  let cost_id = make_unique cost_id_prefix in
404  let cost_decl = cost_decl cost_id in
405
406  (* Create a fresh loop index prefix *)
407  let names = StringTools.Set.add cost_id names in
408  let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in
409
410  (* Create a fresh uninitialized global variable for each extern function. *)
411  let (extern_cost_decls, extern_cost_variables) =
412    extern_cost_variables make_unique p.Clight.prog_funct in
413
414  (* Define an increment function for the cost variable. *)
415  let cost_incr =
416    StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id names)
417      cost_incr_prefix in
418  let cost_incr_def = cost_incr_def cost_id cost_incr in
419
420  (* Turn the mapping from indexed cost labels to integers into one from *)
421  (* cost atoms to cost expresisons *)
422  let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in
423
424  (* Instrument each function *)
425  let prog_funct = p.Clight.prog_funct in
426  let prog_funct =
427    let f = instrument_funct cost_tern l_ind cost_mapping cost_incr in
428    List.map f prog_funct in
429
430  (* Glue all this together. *)
431  let prog_vars = cost_decl :: extern_cost_decls @ p.Clight.prog_vars in
432  let prog_funct = cost_incr_def :: prog_funct in
433  let p' =
434    { p with Clight.prog_vars = prog_vars ; Clight.prog_funct = prog_funct } in
435
436  (* Save the resulted program. Then re-parse it.
437     Indeed, the instrumentation may add side-effects in expressions, which is
438     not Clight compliant. Re-parsing the result with CIL will remove these
439     side-effects in expressions to obtain a Clight program. *)
440  let tmp_file = Filename.temp_file "clight_instrument" ".c" in
441  save_tmp tmp_file (ClightPrinter.print_program p') ;
442  let res = ClightParser.process tmp_file in
443  Misc.SysExt.safe_remove tmp_file ;
444  (res, cost_id, cost_incr, extern_cost_variables)
Note: See TracBrowser for help on using the repository browser.