[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 | |
---|
| 14 | (* Program var 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 | (var_names1, cost_labels1, user_labels1) |
---|
| 22 | (var_names2, cost_labels2, user_labels2) = |
---|
| 23 | (StringTools.Set.union var_names1 var_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 list_union l = List.fold_left triple_union empty_triple l |
---|
| 30 | |
---|
| 31 | let rec exp_idents e = |
---|
| 32 | let Clight.Expr (e, _) = e in |
---|
| 33 | match e with |
---|
| 34 | | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Esizeof _ -> |
---|
| 35 | empty_triple |
---|
| 36 | | Clight.Evar x -> |
---|
| 37 | (StringTools.Set.singleton x, CostLabel.Set.empty, Label.Set.empty) |
---|
| 38 | | Clight.Ederef e | Clight.Eaddrof e | Clight.Eunop (_, e) |
---|
| 39 | | Clight.Ecast (_, e) -> exp_idents e |
---|
| 40 | | Clight.Efield (e, x) -> |
---|
| 41 | let (var_names, cost_labels, user_labels) = exp_idents e in |
---|
| 42 | (StringTools.Set.add x var_names, cost_labels, user_labels) |
---|
| 43 | | Clight.Ebinop (_, e1, e2) | Clight.Eandbool (e1, e2) |
---|
| 44 | | Clight.Eorbool (e1, e2) -> list_union [exp_idents e1 ; exp_idents e2] |
---|
| 45 | | Clight.Econdition (e1, e2, e3) -> |
---|
| 46 | list_union [exp_idents e1 ; exp_idents e2 ; exp_idents e3] |
---|
| 47 | | Clight.Ecost (lbl, e) -> |
---|
| 48 | let (var_names, cost_labels, user_labels) = exp_idents e in |
---|
| 49 | (var_names, CostLabel.Set.add lbl cost_labels, user_labels) |
---|
| 50 | | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen *) |
---|
| 51 | |
---|
| 52 | let exp_idents_opt = function |
---|
| 53 | | None -> empty_triple |
---|
| 54 | | Some e -> exp_idents e |
---|
| 55 | |
---|
| 56 | let exp_idents_list l = list_union (List.map exp_idents l) |
---|
| 57 | |
---|
| 58 | let rec body_idents = function |
---|
| 59 | | Clight.Sskip | Clight.Sbreak | Clight.Scontinue -> empty_triple |
---|
| 60 | | Clight.Sassign (e1, e2) -> list_union [exp_idents e1 ; exp_idents e2] |
---|
| 61 | | Clight.Scall (eopt, f, args) -> |
---|
| 62 | list_union [exp_idents_opt eopt ; exp_idents f ; exp_idents_list args] |
---|
| 63 | | Clight.Ssequence (s1, s2) -> list_union [body_idents s1 ; body_idents s2] |
---|
| 64 | | Clight.Sifthenelse (e, s1, s2) -> |
---|
| 65 | list_union [exp_idents e ; body_idents s1 ; body_idents s2] |
---|
| 66 | | Clight.Swhile (e, s) | Clight.Sdowhile (e, s) -> |
---|
| 67 | list_union [exp_idents e ; body_idents s] |
---|
| 68 | | Clight.Sfor (s1, e, s2, s3) -> |
---|
| 69 | list_union [body_idents s1 ; exp_idents e ; |
---|
| 70 | body_idents s2 ; body_idents s3] |
---|
| 71 | | Clight.Sreturn eopt -> exp_idents_opt eopt |
---|
| 72 | | Clight.Sswitch (e, ls) -> list_union [exp_idents e ; ls_idents ls] |
---|
| 73 | | Clight.Slabel (lbl, stmt) -> |
---|
| 74 | let (var_names, cost_labels, user_labels) = body_idents stmt in |
---|
| 75 | (var_names, cost_labels, Label.Set.add lbl user_labels) |
---|
| 76 | | Clight.Sgoto lbl -> |
---|
| 77 | (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.singleton lbl) |
---|
| 78 | | Clight.Scost (lbl, stmt) -> |
---|
| 79 | let (var_names, cost_labels, user_labels) = body_idents stmt in |
---|
| 80 | (var_names, CostLabel.Set.add lbl cost_labels, user_labels) |
---|
| 81 | and ls_idents = function |
---|
| 82 | | Clight.LSdefault stmt -> body_idents stmt |
---|
| 83 | | Clight.LScase (_, stmt, ls) -> list_union [body_idents stmt ; ls_idents ls] |
---|
| 84 | |
---|
| 85 | let prog_idents p = |
---|
| 86 | let def_idents = function |
---|
| 87 | | Clight.Internal def -> |
---|
| 88 | let vars = |
---|
| 89 | string_set_of_list |
---|
| 90 | (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in |
---|
| 91 | let (var_names, cost_labels, user_labels) = |
---|
| 92 | body_idents def.Clight.fn_body in |
---|
| 93 | (StringTools.Set.union vars var_names, cost_labels, user_labels) |
---|
| 94 | | Clight.External (id, _, _) -> |
---|
| 95 | (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in |
---|
| 96 | let fun_idents (id, f_def) = |
---|
| 97 | let (var_names, cost_labels, user_labels) = def_idents f_def in |
---|
| 98 | (StringTools.Set.add id var_names, cost_labels, user_labels) in |
---|
| 99 | let f idents def = triple_union idents (fun_idents def) in |
---|
| 100 | List.fold_left f empty_triple p.Clight.prog_funct |
---|
| 101 | |
---|
| 102 | let var_names p = |
---|
| 103 | let (var_names, _, _) = prog_idents p in var_names |
---|
| 104 | let cost_labels p = |
---|
| 105 | let (_, cost_labels, _) = prog_idents p in cost_labels |
---|
| 106 | let user_labels p = |
---|
| 107 | let (_, _, user_labels) = prog_idents p in user_labels |
---|
| 108 | |
---|
| 109 | let all_labels p = |
---|
| 110 | let (_, cost_labels, user_labels) = prog_idents p in |
---|
| 111 | let all = |
---|
| 112 | CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) |
---|
| 113 | cost_labels StringTools.Set.empty in |
---|
| 114 | Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all |
---|
| 115 | |
---|
| 116 | |
---|
| 117 | (* Instrumentation *) |
---|
| 118 | |
---|
| 119 | let int_typ = Clight.Tint (Clight.I32, Clight.Signed) |
---|
| 120 | |
---|
| 121 | let const_int i = Clight.Expr (Clight.Econst_int i, int_typ) |
---|
| 122 | |
---|
| 123 | (* Instrument an expression. *) |
---|
| 124 | |
---|
| 125 | let rec instrument_expr cost_mapping cost_incr e = |
---|
| 126 | let Clight.Expr (e, t) = e in |
---|
| 127 | match e with |
---|
| 128 | | Clight.Ecost (lbl, e) when CostLabel.Map.find lbl cost_mapping = 0 -> |
---|
| 129 | e |
---|
| 130 | | _ -> |
---|
| 131 | let e' = instrument_expr_descr cost_mapping cost_incr e in |
---|
| 132 | Clight.Expr (e', t) |
---|
| 133 | and instrument_expr_descr cost_mapping cost_incr e = match e with |
---|
| 134 | | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _ |
---|
| 135 | | Clight.Esizeof _ -> e |
---|
| 136 | | Clight.Ederef e -> |
---|
| 137 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 138 | Clight.Ederef e' |
---|
| 139 | | Clight.Eaddrof e -> |
---|
| 140 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 141 | Clight.Eaddrof e' |
---|
| 142 | | Clight.Eunop (op, e) -> |
---|
| 143 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 144 | Clight.Eunop (op, e') |
---|
| 145 | | Clight.Ebinop (op, e1, e2) -> |
---|
| 146 | let e1' = instrument_expr cost_mapping cost_incr e1 in |
---|
| 147 | let e2' = instrument_expr cost_mapping cost_incr e2 in |
---|
| 148 | Clight.Ebinop (op, e1', e2') |
---|
| 149 | | Clight.Ecast (t, e) -> |
---|
| 150 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 151 | Clight.Ecast (t, e') |
---|
| 152 | | Clight.Econdition (e1, e2, e3) -> |
---|
| 153 | let e1' = instrument_expr cost_mapping cost_incr e1 in |
---|
| 154 | let e2' = instrument_expr cost_mapping cost_incr e2 in |
---|
| 155 | let e3' = instrument_expr cost_mapping cost_incr e3 in |
---|
| 156 | Clight.Econdition (e1', e2', e3') |
---|
| 157 | | Clight.Eandbool (e1, e2) -> |
---|
| 158 | let e1' = instrument_expr cost_mapping cost_incr e1 in |
---|
| 159 | let e2' = instrument_expr cost_mapping cost_incr e2 in |
---|
| 160 | Clight.Eandbool (e1', e2') |
---|
| 161 | | Clight.Eorbool (e1, e2) -> |
---|
| 162 | let e1' = instrument_expr cost_mapping cost_incr e1 in |
---|
| 163 | let e2' = instrument_expr cost_mapping cost_incr e2 in |
---|
| 164 | Clight.Eorbool (e1', e2') |
---|
| 165 | | Clight.Efield (e, x) -> |
---|
| 166 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 167 | Clight.Efield (e', x) |
---|
| 168 | | Clight.Ecost (lbl, e) -> |
---|
| 169 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 170 | let incr = CostLabel.Map.find lbl cost_mapping in |
---|
| 171 | Clight.Ecall (cost_incr, const_int incr, e') |
---|
| 172 | | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *) |
---|
| 173 | |
---|
| 174 | (* Instrument a statement. *) |
---|
| 175 | |
---|
| 176 | let rec instrument_body cost_mapping cost_incr stmt = match stmt with |
---|
| 177 | | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None |
---|
| 178 | | Clight.Sgoto _ -> |
---|
| 179 | stmt |
---|
| 180 | | Clight.Sassign (e1, e2) -> |
---|
| 181 | let e1' = instrument_expr cost_mapping cost_incr e1 in |
---|
| 182 | let e2' = instrument_expr cost_mapping cost_incr e2 in |
---|
| 183 | Clight.Sassign (e1', e2') |
---|
| 184 | | Clight.Scall (eopt, f, args) -> |
---|
| 185 | let eopt' = match eopt with |
---|
| 186 | | None -> None |
---|
| 187 | | Some e -> Some (instrument_expr cost_mapping cost_incr e) in |
---|
| 188 | let f' = instrument_expr cost_mapping cost_incr f in |
---|
| 189 | let args' = List.map (instrument_expr cost_mapping cost_incr) args in |
---|
| 190 | Clight.Scall (eopt', f', args') |
---|
| 191 | | Clight.Ssequence (s1, s2) -> |
---|
| 192 | Clight.Ssequence (instrument_body cost_mapping cost_incr s1, |
---|
| 193 | instrument_body cost_mapping cost_incr s2) |
---|
| 194 | | Clight.Sifthenelse (e, s1, s2) -> |
---|
| 195 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 196 | let s1' = instrument_body cost_mapping cost_incr s1 in |
---|
| 197 | let s2' = instrument_body cost_mapping cost_incr s2 in |
---|
| 198 | Clight.Sifthenelse (e', s1', s2') |
---|
| 199 | | Clight.Swhile (e, s) -> |
---|
| 200 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 201 | let s' = instrument_body cost_mapping cost_incr s in |
---|
| 202 | Clight.Swhile (e', s') |
---|
| 203 | | Clight.Sdowhile (e, s) -> |
---|
| 204 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 205 | let s' = instrument_body cost_mapping cost_incr s in |
---|
| 206 | Clight.Sdowhile (e', s') |
---|
| 207 | | Clight.Sfor (s1, e, s2, s3) -> |
---|
| 208 | let s1' = instrument_body cost_mapping cost_incr s1 in |
---|
| 209 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 210 | let s2' = instrument_body cost_mapping cost_incr s2 in |
---|
| 211 | let s3' = instrument_body cost_mapping cost_incr s3 in |
---|
| 212 | Clight.Sfor (s1', e', s2', s3') |
---|
| 213 | | Clight.Sreturn (Some e) -> |
---|
| 214 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 215 | Clight.Sreturn (Some e') |
---|
| 216 | | Clight.Sswitch (e, ls) -> |
---|
| 217 | let e' = instrument_expr cost_mapping cost_incr e in |
---|
| 218 | let ls' = instrument_ls cost_mapping cost_incr ls in |
---|
| 219 | Clight.Sswitch (e', ls') |
---|
| 220 | | Clight.Slabel (lbl, s) -> |
---|
| 221 | let s' = instrument_body cost_mapping cost_incr s in |
---|
| 222 | Clight.Slabel (lbl, s') |
---|
| 223 | | Clight.Scost (lbl, s) -> |
---|
| 224 | let s' = instrument_body cost_mapping cost_incr s in |
---|
| 225 | let incr = CostLabel.Map.find lbl cost_mapping in |
---|
| 226 | if incr = 0 then s' |
---|
| 227 | else |
---|
| 228 | let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in |
---|
| 229 | let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in |
---|
| 230 | let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in |
---|
| 231 | Clight.Ssequence (Clight.Scall (None, f, args), s') |
---|
| 232 | and instrument_ls cost_mapping cost_incr = function |
---|
| 233 | | Clight.LSdefault s -> |
---|
| 234 | let s' = instrument_body cost_mapping cost_incr s in |
---|
| 235 | Clight.LSdefault s' |
---|
| 236 | | Clight.LScase (i, s, ls) -> |
---|
| 237 | let s' = instrument_body cost_mapping cost_incr s in |
---|
| 238 | let ls' = instrument_ls cost_mapping cost_incr ls in |
---|
| 239 | Clight.LScase (i, s', ls') |
---|
| 240 | |
---|
| 241 | (* Instrument a function. *) |
---|
| 242 | |
---|
| 243 | let instrument_funct cost_mapping cost_incr (id, def) = |
---|
| 244 | let def = match def with |
---|
| 245 | | Clight.Internal def -> |
---|
| 246 | let body = instrument_body cost_mapping cost_incr def.Clight.fn_body in |
---|
| 247 | Clight.Internal { def with Clight.fn_body = body } |
---|
| 248 | | Clight.External _ -> def |
---|
| 249 | in |
---|
| 250 | (id, def) |
---|
| 251 | |
---|
| 252 | (* This is the declaration of the cost variable. *) |
---|
| 253 | |
---|
| 254 | let cost_decl cost_id = |
---|
| 255 | let init = [Clight.Init_int32 0] in |
---|
| 256 | ((cost_id, init), int_typ) |
---|
| 257 | |
---|
| 258 | (* This is the definition of the increment cost function. *) |
---|
| 259 | |
---|
| 260 | let cost_incr_def cost_id cost_incr = |
---|
| 261 | let int_var x = Clight.Expr (Clight.Evar x, int_typ) in |
---|
| 262 | let param = "incr" in |
---|
| 263 | let cost = int_var cost_id in |
---|
| 264 | let increment = int_var param in |
---|
| 265 | let cost_increment = |
---|
| 266 | Clight.Expr (Clight.Ebinop (Clight.Oadd, cost, increment), int_typ) in |
---|
| 267 | let stmt = Clight.Sassign (cost, cost_increment) in |
---|
| 268 | let cfun = |
---|
| 269 | { Clight.fn_return = Clight.Tvoid ; |
---|
| 270 | Clight.fn_params = [(param, int_typ)] ; |
---|
| 271 | Clight.fn_vars = [] ; |
---|
| 272 | Clight.fn_body = stmt } in |
---|
| 273 | (cost_incr, Clight.Internal cfun) |
---|
| 274 | |
---|
| 275 | let save_tmp tmp_file s = |
---|
| 276 | let cout = open_out tmp_file in |
---|
| 277 | output_string cout s ; |
---|
| 278 | flush cout ; |
---|
| 279 | close_out cout |
---|
| 280 | |
---|
| 281 | (** [instrument prog cost_map] instruments the program [prog]. *) |
---|
| 282 | |
---|
| 283 | let instrument p cost_mapping = |
---|
| 284 | |
---|
| 285 | (* Create a fresh 'cost' variable. *) |
---|
| 286 | let var_names = var_names p in |
---|
| 287 | let cost_id = StringTools.Gen.fresh_prefix var_names cost_id_prefix in |
---|
| 288 | let cost_decl = cost_decl cost_id in |
---|
| 289 | |
---|
| 290 | (* Define an increment function for the cost variable. *) |
---|
| 291 | let cost_incr = |
---|
| 292 | StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id var_names) |
---|
| 293 | cost_incr_prefix in |
---|
| 294 | let cost_incr_def = cost_incr_def cost_id cost_incr in |
---|
| 295 | |
---|
| 296 | (* Instrument each function *) |
---|
| 297 | let prog_funct = |
---|
| 298 | List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in |
---|
| 299 | |
---|
| 300 | (* Glue all this together. *) |
---|
| 301 | let prog_vars = cost_decl :: p.Clight.prog_vars in |
---|
| 302 | let prog_funct = cost_incr_def :: prog_funct in |
---|
| 303 | let p' = |
---|
| 304 | { p with Clight.prog_vars = prog_vars ; Clight.prog_funct = prog_funct } in |
---|
| 305 | |
---|
| 306 | (* Save the resulted program. Then re-parse it. |
---|
| 307 | Indeed, the instrumentation may add side-effects in expressions, which is |
---|
| 308 | not Clight compliant. Re-parsing the result with CIL will remove these |
---|
| 309 | side-effects in expressions to obtain a Clight program. *) |
---|
| 310 | let tmp_file = Filename.temp_file "clight_instrument" ".c" in |
---|
| 311 | save_tmp tmp_file (ClightPrinter.print_program p') ; |
---|
| 312 | let res = ClightParser.process tmp_file in |
---|
| 313 | Misc.SysExt.safe_remove tmp_file ; |
---|
| 314 | res |
---|
| 315 | |
---|
| 316 | |
---|