[486] | 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 | |
---|
[619] | 14 | (* Program var and fun names, cost labels and labels *) |
---|
[486] | 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 |
---|
[818] | 21 | (names1, cost_labels1, user_labels1) |
---|
| 22 | (names2, cost_labels2, user_labels2) = |
---|
| 23 | (StringTools.Set.union names1 names2, |
---|
[486] | 24 | CostLabel.Set.union cost_labels1 cost_labels2, |
---|
| 25 | Label.Set.union user_labels1 user_labels2) |
---|
| 26 | |
---|
[1291] | 27 | let empty_triple = |
---|
| 28 | (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty) |
---|
[486] | 29 | |
---|
[818] | 30 | let name_singleton id = |
---|
| 31 | (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) |
---|
| 32 | |
---|
[1291] | 33 | let cost_label_singleton lbl = |
---|
| 34 | (StringTools.Set.empty, CostLabel.Set.singleton lbl, Label.Set.empty) |
---|
[818] | 35 | |
---|
| 36 | let label_singleton lbl = |
---|
| 37 | (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.singleton lbl) |
---|
| 38 | |
---|
[486] | 39 | let list_union l = List.fold_left triple_union empty_triple l |
---|
| 40 | |
---|
[818] | 41 | let 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) |
---|
[486] | 49 | |
---|
[818] | 50 | let f_expr _ sub_ctypes_res sub_expr_descrs_res = |
---|
| 51 | list_union (sub_ctypes_res @ sub_expr_descrs_res) |
---|
[486] | 52 | |
---|
[818] | 53 | let 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)) |
---|
[486] | 60 | |
---|
[818] | 61 | let 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)) |
---|
[486] | 67 | |
---|
[818] | 68 | let body_idents = ClightFold.statement f_ctype f_expr f_expr_descr f_stmt |
---|
| 69 | |
---|
[486] | 70 | let 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 |
---|
[818] | 76 | let (names, cost_labels, user_labels) = |
---|
[486] | 77 | body_idents def.Clight.fn_body in |
---|
[818] | 78 | (StringTools.Set.union vars names, cost_labels, user_labels) |
---|
[486] | 79 | | Clight.External (id, _, _) -> |
---|
[1291] | 80 | (StringTools.Set.singleton id, CostLabel.Set.empty, |
---|
| 81 | Label.Set.empty) in |
---|
[486] | 82 | let fun_idents (id, f_def) = |
---|
[818] | 83 | let (names, cost_labels, user_labels) = def_idents f_def in |
---|
| 84 | (StringTools.Set.add id names, cost_labels, user_labels) in |
---|
[486] | 85 | let f idents def = triple_union idents (fun_idents def) in |
---|
| 86 | List.fold_left f empty_triple p.Clight.prog_funct |
---|
| 87 | |
---|
[818] | 88 | let names p = |
---|
| 89 | let (names, _, _) = prog_idents p in names |
---|
[486] | 90 | let cost_labels p = |
---|
| 91 | let (_, cost_labels, _) = prog_idents p in cost_labels |
---|
| 92 | let user_labels p = |
---|
| 93 | let (_, _, user_labels) = prog_idents p in user_labels |
---|
| 94 | |
---|
| 95 | let all_labels p = |
---|
| 96 | let (_, cost_labels, user_labels) = prog_idents p in |
---|
[1291] | 97 | let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in |
---|
| 98 | let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in |
---|
| 99 | Label.Set.fold StringTools.Set.add user_labels all |
---|
[486] | 100 | |
---|
[818] | 101 | let all_idents p = |
---|
| 102 | let (names, cost_labels, user_labels) = prog_idents p in |
---|
[1291] | 103 | let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in |
---|
| 104 | let cost_labels = CostLabel.Set.fold f cost_labels StringTools.Set.empty in |
---|
[818] | 105 | let to_string_set fold set = |
---|
| 106 | fold (fun lbl idents -> StringTools.Set.add lbl idents) set |
---|
| 107 | StringTools.Set.empty in |
---|
| 108 | let user_labels = to_string_set Label.Set.fold user_labels in |
---|
| 109 | StringTools.Set.union names (StringTools.Set.union cost_labels user_labels) |
---|
[486] | 110 | |
---|
[818] | 111 | let fresh_ident base p = |
---|
| 112 | StringTools.Gen.fresh_prefix (all_idents p) base |
---|
| 113 | |
---|
| 114 | let fresh_universe base p = |
---|
| 115 | let universe = fresh_ident base p in |
---|
| 116 | StringTools.Gen.new_universe universe |
---|
| 117 | |
---|
| 118 | let make_fresh base p = |
---|
| 119 | let universe = fresh_universe base p in |
---|
| 120 | (fun () -> StringTools.Gen.fresh universe) |
---|
| 121 | |
---|
| 122 | |
---|
[486] | 123 | (* Instrumentation *) |
---|
| 124 | |
---|
[818] | 125 | let int_typ = Clight.Tint (Clight.I32, AST.Signed) |
---|
[486] | 126 | |
---|
| 127 | let const_int i = Clight.Expr (Clight.Econst_int i, int_typ) |
---|
| 128 | |
---|
| 129 | (* Instrument an expression. *) |
---|
| 130 | |
---|
| 131 | let rec instrument_expr cost_mapping cost_incr e = |
---|
| 132 | let Clight.Expr (e, t) = e in |
---|
| 133 | match e with |
---|
| 134 | | Clight.Ecost (lbl, e) when 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) |
---|
[624] | 174 | | Clight.Ecost (lbl, e) when CostLabel.Map.mem lbl cost_mapping -> |
---|
[486] | 175 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 176 | let incr = CostLabel.Map.find lbl cost_mapping in |
---|
[624] | 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' |
---|
[486] | 182 | | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *) |
---|
| 183 | |
---|
[1305] | 184 | let loop_increment prefix depth body = match depth with |
---|
| 185 | | None -> body |
---|
| 186 | | Some d -> |
---|
| 187 | let uint = Clight.Tint(Clight.I32, AST.Unsigned) in |
---|
| 188 | let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), uint) in |
---|
| 189 | let one = Clight.Expr(Clight.Econst_int 1, uint) in |
---|
| 190 | let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), uint) in |
---|
| 191 | Clight.Ssequence(body, Clight.Sassign(id, add id one)) |
---|
| 192 | |
---|
| 193 | let loop_reset_index prefix depth loop = match depth with |
---|
| 194 | | None -> loop |
---|
| 195 | | Some d -> |
---|
| 196 | let uint = Clight.Tint(Clight.I32, AST.Unsigned) in |
---|
| 197 | let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), uint) in |
---|
| 198 | let zero = Clight.Expr(Clight.Econst_int 0, uint) in |
---|
| 199 | Clight.Ssequence(Clight.Sassign(id, zero), loop) |
---|
| 200 | |
---|
[486] | 201 | (* Instrument a statement. *) |
---|
| 202 | |
---|
[1305] | 203 | let rec instrument_body l_ind cost_mapping cost_incr stmt = match stmt with |
---|
[486] | 204 | | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None |
---|
| 205 | | Clight.Sgoto _ -> |
---|
[645] | 206 | stmt |
---|
[486] | 207 | | Clight.Sassign (e1, e2) -> |
---|
[645] | 208 | let e1' = instrument_expr cost_mapping cost_incr e1 in |
---|
| 209 | let e2' = instrument_expr cost_mapping cost_incr e2 in |
---|
| 210 | Clight.Sassign (e1', e2') |
---|
[486] | 211 | | Clight.Scall (eopt, f, args) -> |
---|
[645] | 212 | let eopt' = match eopt with |
---|
| 213 | | None -> None |
---|
| 214 | | Some e -> Some (instrument_expr cost_mapping cost_incr e) in |
---|
| 215 | let f' = instrument_expr cost_mapping cost_incr f in |
---|
| 216 | let args' = List.map (instrument_expr cost_mapping cost_incr) args in |
---|
| 217 | Clight.Scall (eopt', f', args') |
---|
[486] | 218 | | Clight.Ssequence (s1, s2) -> |
---|
[1305] | 219 | Clight.Ssequence (instrument_body l_ind cost_mapping cost_incr s1, |
---|
| 220 | instrument_body l_ind cost_mapping cost_incr s2) |
---|
[486] | 221 | | Clight.Sifthenelse (e, s1, s2) -> |
---|
[645] | 222 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
[1305] | 223 | let s1' = instrument_body l_ind cost_mapping cost_incr s1 in |
---|
| 224 | let s2' = instrument_body l_ind cost_mapping cost_incr s2 in |
---|
[645] | 225 | Clight.Sifthenelse (e', s1', s2') |
---|
[1305] | 226 | | Clight.Swhile (i, e, s) -> |
---|
[645] | 227 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
[1305] | 228 | let s' = instrument_body l_ind cost_mapping cost_incr s in |
---|
| 229 | let s' = loop_increment l_ind i s' in |
---|
| 230 | loop_reset_index l_ind i (Clight.Swhile (None, e', s')) |
---|
| 231 | | Clight.Sdowhile (i, e, s) -> |
---|
[645] | 232 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
[1305] | 233 | let s' = instrument_body l_ind cost_mapping cost_incr s in |
---|
| 234 | let s' = loop_increment l_ind i s' in |
---|
| 235 | loop_reset_index l_ind i (Clight.Sdowhile (None, e', s')) |
---|
| 236 | | Clight.Sfor (i, s1, e, s2, s3) -> |
---|
| 237 | let s1' = instrument_body l_ind cost_mapping cost_incr s1 in |
---|
[645] | 238 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
[1305] | 239 | let s2' = instrument_body l_ind cost_mapping cost_incr s2 in |
---|
| 240 | let s3' = instrument_body l_ind cost_mapping cost_incr s3 in |
---|
| 241 | let s3' = loop_increment l_ind i s3' in |
---|
| 242 | loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3')) |
---|
[486] | 243 | | Clight.Sreturn (Some e) -> |
---|
[645] | 244 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 245 | Clight.Sreturn (Some e') |
---|
[486] | 246 | | Clight.Sswitch (e, ls) -> |
---|
[645] | 247 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
[1305] | 248 | let ls' = instrument_ls l_ind cost_mapping cost_incr ls in |
---|
[645] | 249 | Clight.Sswitch (e', ls') |
---|
[486] | 250 | | Clight.Slabel (lbl, s) -> |
---|
[1305] | 251 | let s' = instrument_body l_ind cost_mapping cost_incr s in |
---|
[645] | 252 | Clight.Slabel (lbl, s') |
---|
[624] | 253 | | Clight.Scost (lbl, s) when CostLabel.Map.mem lbl cost_mapping -> |
---|
[645] | 254 | (* Keep the cost label in the code. *) |
---|
[1305] | 255 | let s' = instrument_body l_ind cost_mapping cost_incr s in |
---|
[645] | 256 | let incr = CostLabel.Map.find lbl cost_mapping in |
---|
| 257 | let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in |
---|
| 258 | let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in |
---|
| 259 | let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in |
---|
| 260 | Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s')) |
---|
| 261 | (* |
---|
[1305] | 262 | let s' = instrument_body l_ind cost_mapping cost_incr s in |
---|
[645] | 263 | let incr = CostLabel.Map.find lbl cost_mapping in |
---|
| 264 | if incr = 0 then s' |
---|
| 265 | else |
---|
| 266 | let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in |
---|
| 267 | let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in |
---|
| 268 | let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in |
---|
| 269 | Clight.Ssequence (Clight.Scall (None, f, args), s') |
---|
| 270 | *) |
---|
| 271 | | Clight.Scost (lbl, s) -> |
---|
| 272 | (* Keep the cost label in the code and show the increment of 0. *) |
---|
[1305] | 273 | let s' = instrument_body l_ind cost_mapping cost_incr s in |
---|
[645] | 274 | let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in |
---|
| 275 | let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in |
---|
| 276 | let args = [Clight.Expr (Clight.Econst_int 0, int_typ)] in |
---|
| 277 | Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s')) |
---|
| 278 | (* |
---|
[1305] | 279 | instrument_body l_ind cost_mapping cost_incr s |
---|
[645] | 280 | *) |
---|
[1305] | 281 | and instrument_ls l_ind cost_mapping cost_incr = function |
---|
[486] | 282 | | Clight.LSdefault s -> |
---|
[1305] | 283 | let s' = instrument_body l_ind cost_mapping cost_incr s in |
---|
[645] | 284 | Clight.LSdefault s' |
---|
[486] | 285 | | Clight.LScase (i, s, ls) -> |
---|
[1305] | 286 | let s' = instrument_body l_ind cost_mapping cost_incr s in |
---|
| 287 | let ls' = instrument_ls l_ind cost_mapping cost_incr ls in |
---|
[645] | 288 | Clight.LScase (i, s', ls') |
---|
[1305] | 289 | |
---|
| 290 | (* calculating the maximal depth of single-entry loops *) |
---|
| 291 | (* (as already calculated during the labeling phase) *) |
---|
[486] | 292 | |
---|
[1305] | 293 | let rec max_loop_index = |
---|
| 294 | let f_expr _ _ = () in |
---|
| 295 | let f_stmt stmt _ sub_stmts_res = |
---|
| 296 | let curr_max = List.fold_left max 0 sub_stmts_res in |
---|
| 297 | match stmt with |
---|
| 298 | | Clight.Swhile (Some x, _, _) | Clight.Sdowhile (Some x, _, _) |
---|
| 299 | | Clight.Sfor (Some x, _, _, _, _) -> max x curr_max (* = curr_max+1 ? *) |
---|
| 300 | | _ -> curr_max in |
---|
| 301 | ClightFold.statement2 f_expr f_stmt |
---|
| 302 | |
---|
| 303 | let rec loop_indexes_defs prefix max_depth = |
---|
| 304 | if max_depth = 0 then [] else |
---|
| 305 | let uint = Clight.Tint(Clight.I32, AST.Unsigned) in |
---|
| 306 | let id = CostLabel.make_id prefix max_depth in |
---|
| 307 | (id, uint) :: loop_indexes_defs prefix (max_depth-1) |
---|
| 308 | |
---|
[486] | 309 | (* Instrument a function. *) |
---|
| 310 | |
---|
[1305] | 311 | let instrument_funct l_ind cost_mapping cost_incr (id, def) = |
---|
[486] | 312 | let def = match def with |
---|
| 313 | | Clight.Internal def -> |
---|
[1305] | 314 | let max_depth = max_loop_index def.Clight.fn_body in |
---|
| 315 | let indexes_defs = loop_indexes_defs l_ind max_depth in |
---|
| 316 | let body = instrument_body l_ind cost_mapping cost_incr def.Clight.fn_body in |
---|
[486] | 317 | Clight.Internal { def with Clight.fn_body = body } |
---|
| 318 | | Clight.External _ -> def |
---|
| 319 | in |
---|
| 320 | (id, def) |
---|
| 321 | |
---|
| 322 | (* This is the declaration of the cost variable. *) |
---|
| 323 | |
---|
| 324 | let cost_decl cost_id = |
---|
| 325 | let init = [Clight.Init_int32 0] in |
---|
| 326 | ((cost_id, init), int_typ) |
---|
| 327 | |
---|
| 328 | (* This is the definition of the increment cost function. *) |
---|
| 329 | |
---|
| 330 | let cost_incr_def cost_id cost_incr = |
---|
| 331 | let int_var x = Clight.Expr (Clight.Evar x, int_typ) in |
---|
| 332 | let param = "incr" in |
---|
| 333 | let cost = int_var cost_id in |
---|
| 334 | let increment = int_var param in |
---|
| 335 | let cost_increment = |
---|
| 336 | Clight.Expr (Clight.Ebinop (Clight.Oadd, cost, increment), int_typ) in |
---|
| 337 | let stmt = Clight.Sassign (cost, cost_increment) in |
---|
| 338 | let cfun = |
---|
| 339 | { Clight.fn_return = Clight.Tvoid ; |
---|
| 340 | Clight.fn_params = [(param, int_typ)] ; |
---|
| 341 | Clight.fn_vars = [] ; |
---|
| 342 | Clight.fn_body = stmt } in |
---|
| 343 | (cost_incr, Clight.Internal cfun) |
---|
| 344 | |
---|
| 345 | let save_tmp tmp_file s = |
---|
| 346 | let cout = open_out tmp_file in |
---|
| 347 | output_string cout s ; |
---|
| 348 | flush cout ; |
---|
| 349 | close_out cout |
---|
| 350 | |
---|
[640] | 351 | (** [instrument prog cost_map] instruments the program [prog]. First a fresh |
---|
| 352 | global variable --- the so-called cost variable --- is added to the program. |
---|
| 353 | Then, each cost label in the program is replaced by an increment of the cost |
---|
| 354 | variable, following the mapping [cost_map]. The function also returns the |
---|
| 355 | name of the cost variable and the name of the cost increment function. *) |
---|
[486] | 356 | |
---|
| 357 | let instrument p cost_mapping = |
---|
| 358 | |
---|
| 359 | (* Create a fresh 'cost' variable. *) |
---|
[818] | 360 | let names = names p in |
---|
| 361 | let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in |
---|
[486] | 362 | let cost_decl = cost_decl cost_id in |
---|
| 363 | |
---|
| 364 | (* Define an increment function for the cost variable. *) |
---|
| 365 | let cost_incr = |
---|
[818] | 366 | StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id names) |
---|
[486] | 367 | cost_incr_prefix in |
---|
| 368 | let cost_incr_def = cost_incr_def cost_id cost_incr in |
---|
| 369 | |
---|
| 370 | (* Instrument each function *) |
---|
| 371 | let prog_funct = |
---|
| 372 | List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in |
---|
| 373 | |
---|
| 374 | (* Glue all this together. *) |
---|
| 375 | let prog_vars = cost_decl :: p.Clight.prog_vars in |
---|
| 376 | let prog_funct = cost_incr_def :: prog_funct in |
---|
| 377 | let p' = |
---|
| 378 | { p with Clight.prog_vars = prog_vars ; Clight.prog_funct = prog_funct } in |
---|
| 379 | |
---|
| 380 | (* Save the resulted program. Then re-parse it. |
---|
| 381 | Indeed, the instrumentation may add side-effects in expressions, which is |
---|
| 382 | not Clight compliant. Re-parsing the result with CIL will remove these |
---|
| 383 | side-effects in expressions to obtain a Clight program. *) |
---|
| 384 | let tmp_file = Filename.temp_file "clight_instrument" ".c" in |
---|
| 385 | save_tmp tmp_file (ClightPrinter.print_program p') ; |
---|
| 386 | let res = ClightParser.process tmp_file in |
---|
| 387 | Misc.SysExt.safe_remove tmp_file ; |
---|
[640] | 388 | (res, cost_id, cost_incr) |
---|