src/clight/clightAnnotator.ml

   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
   6 let error_prefix = "Clight Annotator"
   7 let error = Error.global_error error_prefix
   8
   9
  10 let cost_id_prefix = "__cost"
  11 let cost_incr_prefix = "__cost_incr"
  12
  13
  14 (* Program var and fun names, cost labels and labels *)
  15
  16 let string_set_of_list l =
  17   List.fold_left (fun res s -> StringTools.Set.add s res)
  18     StringTools.Set.empty l
  19
  20 let 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
  27 let empty_triple = (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
  28
  29 let name_singleton id =
  30   (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty)
  31
  32 let cost_label_singleton cost_lbl =
  33   (StringTools.Set.empty, CostLabel.Set.singleton cost_lbl, Label.Set.empty)
  34
  35 let label_singleton lbl =
  36   (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.singleton lbl)
  37
  38 let list_union l = List.fold_left triple_union empty_triple l
  39
  40 let f_ctype ctype sub_ctypes_res =
  41   let res = match ctype with
  42     | Clight.Tstruct (id, fields) | Clight.Tunion (id, fields) ->
  43       (string_set_of_list (id :: (List.map fst fields)),
  44        CostLabel.Set.empty, Label.Set.empty)
  45     | Clight.Tcomp_ptr id -> name_singleton id
  46     | _ -> empty_triple in
  47   list_union (res :: sub_ctypes_res)
  48
  49 let f_expr _ sub_ctypes_res sub_expr_descrs_res =
  50   list_union (sub_ctypes_res @ sub_expr_descrs_res)
  51
  52 let f_expr_descr ed sub_ctypes_res sub_exprs_res =
  53   let res = match ed with
  54     | Clight.Evar id | Clight.Efield (_, id) | Clight.Ecall (id, _, _) ->
  55       name_singleton id
  56     | Clight.Ecost (cost_lbl, _) -> cost_label_singleton cost_lbl
  57     | _ -> empty_triple in
  58   list_union (res :: (sub_ctypes_res @ sub_exprs_res))
  59
  60 let f_stmt stmt sub_exprs_res sub_stmts_res =
  61   let stmt_res = match stmt with
  62     | Clight.Slabel (lbl, _) | Clight.Sgoto lbl -> label_singleton lbl
  63     | Clight.Scost (cost_lbl, _) -> cost_label_singleton cost_lbl
  64     | _ -> empty_triple in
  65   list_union (stmt_res :: (sub_exprs_res @ sub_stmts_res))
  66
  67 let body_idents = ClightFold.statement f_ctype f_expr f_expr_descr f_stmt
  68
  69 let prog_idents p =
  70   let def_idents = function
  71     | Clight.Internal def ->
  72         let vars =
  73           string_set_of_list
  74             (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
  75         let (names, cost_labels, user_labels) =
  76           body_idents def.Clight.fn_body in
  77         (StringTools.Set.union vars names, cost_labels, user_labels)
  78     | Clight.External (id, _, _) ->
  79         (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
  80   let fun_idents (id, f_def) =
  81     let (names, cost_labels, user_labels) = def_idents f_def in
  82     (StringTools.Set.add id names, cost_labels, user_labels) in
  83   let f idents def = triple_union idents (fun_idents def) in
  84   List.fold_left f empty_triple p.Clight.prog_funct
  85
  86 let names p =
  87   let (names, _, _) = prog_idents p in names
  88 let cost_labels p =
  89   let (_, cost_labels, _) = prog_idents p in cost_labels
  90 let user_labels p =
  91   let (_, _, user_labels) = prog_idents p in user_labels
  92
  93 let all_labels p =
  94   let (_, cost_labels, user_labels) = prog_idents p in
  95   let all =
  96     CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls)
  97       cost_labels StringTools.Set.empty in
  98   Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all
  99
 100 let all_idents p =
 101   let (names, cost_labels, user_labels) = prog_idents p in
 102   let to_string_set fold set =
 103     fold (fun lbl idents -> StringTools.Set.add lbl idents) set
 104       StringTools.Set.empty in
 105   let cost_labels = to_string_set CostLabel.Set.fold cost_labels in
 106   let user_labels = to_string_set Label.Set.fold user_labels in
 107   StringTools.Set.union names (StringTools.Set.union cost_labels user_labels)
 108
 109 let fresh_ident base p =
 110   StringTools.Gen.fresh_prefix (all_idents p) base
 111
 112 let fresh_universe base p =
 113   let universe = fresh_ident base p in
 114   StringTools.Gen.new_universe universe
 115
 116 let make_fresh base p =
 117   let universe = fresh_universe base p in
 118   (fun () -> StringTools.Gen.fresh universe)
 119
 120
 121 (* Instrumentation *)
 122
 123 let int_typ = Clight.Tint (Clight.I32, AST.Signed)
 124
 125 let const_int i = Clight.Expr (Clight.Econst_int i, int_typ)
 126
 127 (* Instrument an expression. *)
 128
 129 let rec instrument_expr cost_mapping cost_incr e =
 130   let Clight.Expr (e, t) = e in
 131   match e with
 132     | Clight.Ecost (lbl, e)
 133         when CostLabel.Map.mem lbl cost_mapping &&
 134              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)
 139 and 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
 184 (* Instrument a statement. *)
 185
 186 let rec instrument_body cost_mapping cost_incr stmt = match stmt with
 187   | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
 188   | Clight.Sgoto _ ->
 189     stmt
 190   | Clight.Sassign (e1, e2) ->
 191     let e1' = instrument_expr cost_mapping cost_incr e1 in
 192     let e2' = instrument_expr cost_mapping cost_incr e2 in
 193     Clight.Sassign (e1', e2')
 194   | Clight.Scall (eopt, f, args) ->
 195     let eopt' = match eopt with
 196       | None -> None
 197       | Some e -> Some (instrument_expr cost_mapping cost_incr e) in
 198     let f' = instrument_expr cost_mapping cost_incr f in
 199     let args' = List.map (instrument_expr cost_mapping cost_incr) args in
 200     Clight.Scall (eopt', f', args')
 201   | Clight.Ssequence (s1, s2) ->
 202     Clight.Ssequence (instrument_body cost_mapping cost_incr s1,
 203                       instrument_body cost_mapping cost_incr s2)
 204   | Clight.Sifthenelse (e, s1, s2) ->
 205     let e' = instrument_expr cost_mapping cost_incr e in
 206     let s1' = instrument_body cost_mapping cost_incr s1 in
 207     let s2' = instrument_body cost_mapping cost_incr s2 in
 208     Clight.Sifthenelse (e', s1', s2')
 209   | Clight.Swhile (e, s) ->
 210     let e' = instrument_expr cost_mapping cost_incr e in
 211     let s' = instrument_body cost_mapping cost_incr s in
 212     Clight.Swhile (e', s')
 213   | Clight.Sdowhile (e, s) ->
 214     let e' = instrument_expr cost_mapping cost_incr e in
 215     let s' = instrument_body cost_mapping cost_incr s in
 216     Clight.Sdowhile (e', s')
 217   | Clight.Sfor (s1, e, s2, s3) ->
 218     let s1' = instrument_body cost_mapping cost_incr s1 in
 219     let e' = instrument_expr cost_mapping cost_incr e in
 220     let s2' = instrument_body cost_mapping cost_incr s2 in
 221     let s3' = instrument_body cost_mapping cost_incr s3 in
 222     Clight.Sfor (s1', e', s2', s3')
 223   | Clight.Sreturn (Some e) ->
 224     let e' = instrument_expr cost_mapping cost_incr e in
 225     Clight.Sreturn (Some e')
 226   | Clight.Sswitch (e, ls) ->
 227     let e' = instrument_expr cost_mapping cost_incr e in
 228     let ls' = instrument_ls cost_mapping cost_incr ls in
 229     Clight.Sswitch (e', ls')
 230   | Clight.Slabel (lbl, s) ->
 231     let s' = instrument_body cost_mapping cost_incr s in
 232     Clight.Slabel (lbl, s')
 233   | Clight.Scost (lbl, s) when CostLabel.Map.mem lbl cost_mapping ->
 234     (* Keep the cost label in the code. *)
 235     let s' = instrument_body cost_mapping cost_incr s in
 236     let incr = CostLabel.Map.find lbl cost_mapping in
 237     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
 238     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
 239     let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
 240     Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
 241   (*
 242     let s' = instrument_body cost_mapping cost_incr s in
 243     let incr = CostLabel.Map.find lbl cost_mapping in
 244     if incr = 0 then s'
 245     else
 246     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
 247     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
 248     let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
 249     Clight.Ssequence (Clight.Scall (None, f, args), s')
 250   *)
 251   | Clight.Scost (lbl, s) ->
 252     (* Keep the cost label in the code and show the increment of 0. *)
 253     let s' = instrument_body cost_mapping cost_incr s in
 254     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
 255     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
 256     let args = [Clight.Expr (Clight.Econst_int 0, int_typ)] in
 257     Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
 258   (*
 259     instrument_body cost_mapping cost_incr s
 260   *)
 261 and instrument_ls cost_mapping cost_incr = function
 262   | Clight.LSdefault s ->
 263     let s' = instrument_body cost_mapping cost_incr s in
 264     Clight.LSdefault s'
 265   | Clight.LScase (i, s, ls) ->
 266     let s' = instrument_body cost_mapping cost_incr s in
 267     let ls' = instrument_ls cost_mapping cost_incr ls in
 268     Clight.LScase (i, s', ls')
 269
 270 (* Instrument a function. *)
 271
 272 let instrument_funct cost_mapping cost_incr (id, def) =
 273   let def = match def with
 274     | Clight.Internal def ->
 275         let body = instrument_body cost_mapping cost_incr def.Clight.fn_body in
 276         Clight.Internal { def with Clight.fn_body = body }
 277     | Clight.External _ -> def
 278   in
 279   (id, def)
 280
 281 (* This is the declaration of the cost variable. *)
 282
 283 let cost_decl cost_id =
 284   let init = [Clight.Init_int32 0] in
 285   ((cost_id, init), int_typ)
 286
 287 (* This is the definition of the increment cost function. *)
 288
 289 let cost_incr_def cost_id cost_incr =
 290   let int_var x = Clight.Expr (Clight.Evar x, int_typ) in
 291   let param = "incr" in
 292   let cost = int_var cost_id in
 293   let increment = int_var param in
 294   let cost_increment =
 295     Clight.Expr (Clight.Ebinop (Clight.Oadd, cost, increment), int_typ) in
 296   let stmt = Clight.Sassign (cost, cost_increment) in
 297   let cfun =
 298     { Clight.fn_return = Clight.Tvoid ;
 299       Clight.fn_params = [(param, int_typ)] ;
 300       Clight.fn_vars   = [] ;
 301       Clight.fn_body =   stmt } in
 302   (cost_incr, Clight.Internal cfun)
 303
 304 (* Create a fresh uninitialized cost variable for each external function. This
 305    will be used by the Cost plug-in of the Frama-C platform. *)
 306
 307 let extern_cost_variables make_unique functs =
 308   let prefix = "_cost_of_" in
 309   let f (decls, map) (_, def) = match def with
 310     | Clight.Internal _ -> (decls, map)
 311     | Clight.External (id, _, _) ->
 312       let new_var = make_unique (prefix ^ id) in
 313       (decls @ [cost_decl new_var], StringTools.Map.add id new_var map) in
 314   List.fold_left f ([], StringTools.Map.empty) functs
 315
 316 let save_tmp tmp_file s =
 317   let cout = open_out tmp_file in
 318   output_string cout s ;
 319   flush cout ;
 320   close_out cout
 321
 322 (** [instrument prog cost_map] instruments the program [prog]. First a fresh
 323     global variable --- the so-called cost variable --- is added to the program.
 324     Then, each cost label in the program is replaced by an increment of the cost
 325     variable, following the mapping [cost_map]. The function also returns the
 326     name of the cost variable and the name of the cost increment function. *)
 327
 328 let instrument p cost_mapping =
 329
 330   (* Create a fresh 'cost' variable. *)
 331   let names = names p in
 332   let make_unique = StringTools.make_unique names in
 333   let cost_id = make_unique cost_id_prefix in
 334   let cost_decl = cost_decl cost_id in
 335
 336   (* Create a fresh uninitialized global variable for each extern function. *)
 337   let (extern_cost_decls, extern_cost_variables) =
 338     extern_cost_variables make_unique p.Clight.prog_funct in
 339
 340   (* Define an increment function for the cost variable. *)
 341   let cost_incr =
 342     StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id names)
 343       cost_incr_prefix in
 344   let cost_incr_def = cost_incr_def cost_id cost_incr in
 345
 346   (* Instrument each function *)
 347   let prog_funct =
 348     List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in
 349
 350   (* Glue all this together. *)
 351   let prog_vars = cost_decl :: extern_cost_decls @ p.Clight.prog_vars in
 352   let prog_funct = cost_incr_def :: prog_funct in
 353   let p' =
 354     { p with Clight.prog_vars = prog_vars ; Clight.prog_funct = prog_funct } in
 355
 356   (* Save the resulted program. Then re-parse it.
 357      Indeed, the instrumentation may add side-effects in expressions, which is
 358      not Clight compliant. Re-parsing the result with CIL will remove these
 359      side-effects in expressions to obtain a Clight program. *)
 360   let output = ClightPrinter.print_program p' in
 361   let res = ClightParser.process (`Source ("annotated", output)) in
 362   (res, cost_id, cost_incr, extern_cost_variables)