Changeset 1542 for Deliverables/D2.2/8051/src/clight/clightAnnotator.ml
 Timestamp:
 Nov 23, 2011, 5:43:24 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051/src/clight/clightAnnotator.ml
r1462 r1542 10 10 let cost_id_prefix = "_cost" 11 11 let cost_incr_prefix = "_cost_incr" 12 let loop_id_prefix = "_i" 12 13 13 14 … … 70 71 let def_idents = function 71 72  Clight.Internal def > 72 73 74 75 76 77 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) 78 79  Clight.External (id, _, _) > 79 80 (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in 80 81 let fun_idents (id, f_def) = 81 82 let (names, cost_labels, user_labels) = def_idents f_def in … … 93 94 let all_labels p = 94 95 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 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 99 100 100 let all_idents p = 101 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 102 104 let to_string_set fold set = 103 105 fold (fun lbl idents > StringTools.Set.add lbl idents) set 104 106 StringTools.Set.empty in 105 let cost_labels = to_string_set CostLabel.Set.fold cost_labels in106 107 let user_labels = to_string_set Label.Set.fold user_labels in 107 108 StringTools.Set.union names (StringTools.Set.union cost_labels user_labels) … … 125 126 let const_int i = Clight.Expr (Clight.Econst_int i, int_typ) 126 127 128 let 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 146 let 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 155 let 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 nocosttern is active. *) 167 let 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 179 let 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 127 189 (* Instrument an expression. *) 128 190 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. *) 191 (* FIXME: currently using a hack (reparsing) *) 192 let 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 211 let 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 218 let 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 183 224 184 225 (* Instrument a statement. *) 185 226 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 > 227 (* FIXME: use ClightFold, a much better option *) 228 let 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) > 234 281 (* 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 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 *) 309 and instrument_ls cost_tern l_ind cost_mapping cost_incr = function 262 310  Clight.LSdefault s > 263 let s' = instrument_body cost_ mapping cost_incr s in311 let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in 264 312 Clight.LSdefault s' 265 313  Clight.LScase (i, s, ls) > 266 let s' = instrument_body cost_ mapping cost_incr s in267 let ls' = instrument_ls cost_ mapping cost_incr ls in314 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 268 316 Clight.LScase (i, s', ls') 317 318 let 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 324 let 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 269 334 270 335 (* Instrument a function. *) 271 336 272 let instrument_funct cost_ mapping cost_incr (id, def) =337 let instrument_funct cost_tern l_ind cost_mapping cost_incr (id, def) = 273 338 let def = match def with 274 339  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 } 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} 277 347  Clight.External _ > def 278 348 in … … 326 396 name of the cost variable and the name of the cost increment function. *) 327 397 328 let instrument p cost_mapping =398 let instrument cost_tern p cost_mapping = 329 399 330 400 (* Create a fresh 'cost' variable. *) … … 334 404 let cost_decl = cost_decl cost_id in 335 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 336 410 (* Create a fresh uninitialized global variable for each extern function. *) 337 411 let (extern_cost_decls, extern_cost_variables) = … … 344 418 let cost_incr_def = cost_incr_def cost_id cost_incr in 345 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 346 424 (* Instrument each function *) 425 let prog_funct = p.Clight.prog_funct in 347 426 let prog_funct = 348 List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in 427 let f = instrument_funct cost_tern l_ind cost_mapping cost_incr in 428 List.map f prog_funct in 349 429 350 430 (* Glue all this together. *)
Note: See TracChangeset
for help on using the changeset viewer.