 Timestamp:
 Nov 15, 2011, 5:11:19 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051indexedlabelsbranch/src/clight/clightAnnotator.ml
r1433 r1507 27 27 28 28 let empty_triple = 29 29 (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty) 30 30 31 31 let name_singleton id = … … 72 72 let def_idents = function 73 73  Clight.Internal def > 74 75 76 77 78 79 74 let vars = 75 string_set_of_list 76 (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in 77 let (names, cost_labels, user_labels) = 78 body_idents def.Clight.fn_body in 79 (StringTools.Set.union vars names, cost_labels, user_labels) 80 80  Clight.External (id, _, _) > 81 82 81 (StringTools.Set.singleton id, CostLabel.Set.empty, 82 Label.Set.empty) in 83 83 let fun_idents (id, f_def) = 84 84 let (names, cost_labels, user_labels) = def_idents f_def in … … 96 96 let all_labels p = 97 97 let (_, cost_labels, user_labels) = prog_idents p in 98 98 let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in 99 99 let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in 100 100 Label.Set.fold StringTools.Set.add user_labels all … … 102 102 let all_idents p = 103 103 let (names, cost_labels, user_labels) = prog_idents p in 104 104 let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in 105 105 let cost_labels = CostLabel.Set.fold f cost_labels StringTools.Set.empty in 106 106 let to_string_set fold set = … … 140 140 let modulus = 141 141 Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in 142 143 144 145 142 let modulus_eq = 143 Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ) in 144 let greater = 145 Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) in 146 146 Clight.Expr(Clight.Eandbool(modulus_eq, greater),int_typ) 147 147 148 let rec expr_of_cost_gen_cond var gc = 149 assert (not (CostExpr.CondSet.is_empty gc)); 150 let c = CostExpr.CondSet.min_elt gc in 151 let c_expr = expr_of_cost_cond var c in 152 let rest = CostExpr.CondSet.remove c gc in 153 if CostExpr.CondSet.is_empty rest then c_expr else 154 let rest_expr = expr_of_cost_gen_cond var rest in 155 Clight.Expr(Clight.Eandbool(c_expr, rest_expr), int_typ) 156 148 157 let rec expr_of_cost_expr prefix = function 149 150 158  CostExpr.Exact k > const_int k 159  CostExpr.Ternary(index, cond, if_true, if_false) > 151 160 let id = CostLabel.make_id prefix index in 152 161 let var = Clight.Expr(Clight.Evar id, int_typ) in 153 let cond_e = expr_of_cost_ cond var cond in162 let cond_e = expr_of_cost_gen_cond var cond in 154 163 let if_true_e = expr_of_cost_expr prefix if_true in 155 164 let if_false_e = expr_of_cost_expr prefix if_false in 156 Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ) 165 Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ) 166 167 (* as long as Clight parser will be called at the end, this hack works *) 168 (* this will be called in case nocosttern is active. *) 169 let rec side_effect_expr_of_cost_expr prefix cost_incr cont e_type = function 170  CostExpr.Exact k > 171 Clight.Expr(Clight.Ecall (cost_incr, const_int k, cont), e_type) 172  CostExpr.Ternary(index, cond, if_true, if_false) > 173 let id = CostLabel.make_id prefix index in 174 let var = Clight.Expr(Clight.Evar id, int_typ) in 175 let cond_e = expr_of_cost_gen_cond var cond in 176 let rec_call = side_effect_expr_of_cost_expr prefix cost_incr cont e_type in 177 let if_true_e = rec_call if_true in 178 let if_false_e = rec_call if_false in 179 Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ) 180 181 let rec stmt_of_cost_expr prefix cost_incr = function 182  CostExpr.Exact k > Clight.Scall (None, cost_incr, [const_int k]) 183  CostExpr.Ternary(index, cond, if_true, if_false) > 184 let id = CostLabel.make_id prefix index in 185 let var = Clight.Expr(Clight.Evar id, int_typ) in 186 let cond_e = expr_of_cost_gen_cond var cond in 187 let if_true_s = stmt_of_cost_expr prefix cost_incr if_true in 188 let if_false_s = stmt_of_cost_expr prefix cost_incr if_false in 189 Clight.Sifthenelse (cond_e, if_true_s, if_false_s) 157 190 158 191 (* Instrument an expression. *) 159 192 160 let rec instrument_expr l_ind cost_mapping cost_incr e = 161 let Clight.Expr (e, t) = e in 162 let e' = instrument_expr_descr l_ind cost_mapping cost_incr e in 163 Clight.Expr (e', t) 164 and instrument_expr_descr l_ind cost_mapping cost_incr e = match e with 165  Clight.Econst_int _  Clight.Econst_float _  Clight.Evar _ 166  Clight.Esizeof _ > e 167  Clight.Ederef e > 168 let e' = instrument_expr l_ind cost_mapping cost_incr e in 169 Clight.Ederef e' 170  Clight.Eaddrof e > 171 let e' = instrument_expr l_ind cost_mapping cost_incr e in 172 Clight.Eaddrof e' 173  Clight.Eunop (op, e) > 174 let e' = instrument_expr l_ind cost_mapping cost_incr e in 175 Clight.Eunop (op, e') 176  Clight.Ebinop (op, e1, e2) > 177 let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in 178 let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in 179 Clight.Ebinop (op, e1', e2') 180  Clight.Ecast (t, e) > 181 let e' = instrument_expr l_ind cost_mapping cost_incr e in 182 Clight.Ecast (t, e') 183  Clight.Econdition (e1, e2, e3) > 184 let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in 185 let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in 186 let e3' = instrument_expr l_ind cost_mapping cost_incr e3 in 187 Clight.Econdition (e1', e2', e3') 188  Clight.Eandbool (e1, e2) > 189 let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in 190 let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in 191 Clight.Eandbool (e1', e2') 192  Clight.Eorbool (e1, e2) > 193 let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in 194 let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in 195 Clight.Eorbool (e1', e2') 196  Clight.Efield (e, x) > 197 let e' = instrument_expr l_ind cost_mapping cost_incr e in 198 Clight.Efield (e', x) 199  Clight.Ecost (lbl, e) > 200 let e' = instrument_expr l_ind cost_mapping cost_incr e in 201 let atom = lbl.CostLabel.name in 202 let cost = 203 try 204 CostLabel.Atom.Map.find atom cost_mapping 205 with (* if atom is not present, then map to 0 *) 206  Not_found > CostExpr.Exact 0 in 207 if cost = CostExpr.Exact 0 then let Clight.Expr (e'', _) = e' in e'' 208 else let cost = expr_of_cost_expr l_ind cost in 209 Clight.Ecall (cost_incr, cost, e') 210  Clight.Ecall (x, e1, e2) > assert false (* Should not happen. *) 193 (* FIXME: follow cost_tern option *) 194 let instrument_expr cost_tern l_ind cost_mapping cost_incr = 195 let f_expr (Clight.Expr(ed, et) as e) sub_res = match ed, sub_res with 196  Clight.Ecost (lbl, _), e' :: _ > 197 let atom = lbl.CostLabel.name in 198 let cost = 199 try 200 CostLabel.Atom.Map.find atom cost_mapping 201 with (* if atom is not present, then map to 0 *) 202  Not_found > CostExpr.Exact 0 in 203 if cost = CostExpr.Exact 0 then e' else 204 if cost_tern then 205 let cost = expr_of_cost_expr l_ind cost in 206 Clight.Expr(Clight.Ecall (cost_incr, cost, e'), et) 207 else 208 side_effect_expr_of_cost_expr l_ind cost_incr e' et cost 209  Clight.Ecall (_, _, _), _ > assert false (* Should not happen. *) 210  _ > ClightFold.expr_fill_exprs e sub_res in 211 ClightFold.expr2 f_expr 211 212 212 213 let loop_increment prefix depth body = match depth with 213 214 215 216 217 218 214  None > body 215  Some d > 216 let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in 217 let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in 218 Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1))) 219 219 220 let loop_reset_index prefix depth loop = match depth with 220 221 221  None > loop 222  Some d > 222 223 let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in 223 224 Clight.Ssequence(Clight.Sassign(id, const_int 0), loop) … … 226 227 (* Instrument a statement. *) 227 228 228 let rec instrument_body l_ind cost_mapping cost_incr stmt = match stmt with 229  Clight.Sskip  Clight.Sbreak  Clight.Scontinue  Clight.Sreturn None 230  Clight.Sgoto _ > 231 stmt 232  Clight.Sassign (e1, e2) > 233 let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in 234 let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in 235 Clight.Sassign (e1', e2') 236  Clight.Scall (eopt, f, args) > 237 let eopt' = match eopt with 238  None > None 239  Some e > Some (instrument_expr l_ind cost_mapping cost_incr e) in 240 let f' = instrument_expr l_ind cost_mapping cost_incr f in 241 let args' = List.map (instrument_expr l_ind cost_mapping cost_incr) args in 242 Clight.Scall (eopt', f', args') 243  Clight.Ssequence (s1, s2) > 244 Clight.Ssequence (instrument_body l_ind cost_mapping cost_incr s1, 245 instrument_body l_ind cost_mapping cost_incr s2) 246  Clight.Sifthenelse (e, s1, s2) > 247 let e' = instrument_expr l_ind cost_mapping cost_incr e in 248 let s1' = instrument_body l_ind cost_mapping cost_incr s1 in 249 let s2' = instrument_body l_ind cost_mapping cost_incr s2 in 250 Clight.Sifthenelse (e', s1', s2') 251  Clight.Swhile (i, e, s) > 252 let e' = instrument_expr l_ind cost_mapping cost_incr e in 253 let s' = instrument_body l_ind cost_mapping cost_incr s in 254 let s' = loop_increment l_ind i s' in 255 loop_reset_index l_ind i (Clight.Swhile (None, e', s')) 256  Clight.Sdowhile (i, e, s) > 257 let e' = instrument_expr l_ind cost_mapping cost_incr e in 258 let s' = instrument_body l_ind cost_mapping cost_incr s in 259 let s' = loop_increment l_ind i s' in 260 loop_reset_index l_ind i (Clight.Sdowhile (None, e', s')) 261  Clight.Sfor (i, s1, e, s2, s3) > 262 let s1' = instrument_body l_ind cost_mapping cost_incr s1 in 263 let e' = instrument_expr l_ind cost_mapping cost_incr e in 264 let s2' = instrument_body l_ind cost_mapping cost_incr s2 in 265 let s3' = instrument_body l_ind cost_mapping cost_incr s3 in 266 let s3' = loop_increment l_ind i s3' in 267 loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3')) 268  Clight.Sreturn (Some e) > 269 let e' = instrument_expr l_ind cost_mapping cost_incr e in 270 Clight.Sreturn (Some e') 271  Clight.Sswitch (e, ls) > 272 let e' = instrument_expr l_ind cost_mapping cost_incr e in 273 let ls' = instrument_ls l_ind cost_mapping cost_incr ls in 274 Clight.Sswitch (e', ls') 275  Clight.Slabel (lbl, s) > 276 let s' = instrument_body l_ind cost_mapping cost_incr s in 277 Clight.Slabel (lbl, s') 278  Clight.Scost (lbl, s) > 229 (* not using ClightFold as l_ind changes through loops *) 230 let rec instrument_body cost_tern l_ind cost_mapping cost_incr stmt = 231 let instr_expr = instrument_expr cost_tern l_ind cost_mapping cost_incr in 232 let instr_body = instrument_body cost_tern l_ind cost_mapping cost_incr in 233 match stmt with 234  Clight.Sskip  Clight.Sbreak  Clight.Scontinue  Clight.Sreturn None 235  Clight.Sgoto _ > 236 stmt 237  Clight.Sassign (e1, e2) > 238 let e1' = instr_expr e1 in 239 let e2' = instr_expr e2 in 240 Clight.Sassign (e1', e2') 241  Clight.Scall (eopt, f, args) > 242 let eopt' = Option.map instr_expr eopt in 243 let f' = instr_expr f in 244 let args = List.map (instr_expr) args in 245 Clight.Scall (eopt', f', args) 246  Clight.Ssequence (s1, s2) > 247 Clight.Ssequence ( 248 instr_body s1, 249 instr_body s2) 250  Clight.Sifthenelse (e, s1, s2) > 251 let e' = instr_expr e in 252 let s1' = instr_body s1 in 253 let s2' = instr_body s2 in 254 Clight.Sifthenelse (e', s1', s2') 255  Clight.Swhile (i, e, s) > 256 let e' = instr_expr e in 257 let s' = instr_body s in 258 let s' = loop_increment l_ind i s' in 259 loop_reset_index l_ind i (Clight.Swhile (None, e', s')) 260  Clight.Sdowhile (i, e, s) > 261 let e' = instr_expr e in 262 let s' = instr_body s in 263 let s' = loop_increment l_ind i s' in 264 loop_reset_index l_ind i (Clight.Sdowhile (None, e', s')) 265  Clight.Sfor (i, s1, e, s2, s3) > 266 let s1' = instr_body s1 in 267 let e' = instr_expr e in 268 let s2' = instr_body s2 in 269 let s3' = instr_body s3 in 270 let s3' = loop_increment l_ind i s3' in 271 loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3')) 272  Clight.Sreturn (Some e) > 273 let e' = instr_expr e in 274 Clight.Sreturn (Some e') 275  Clight.Sswitch (e, ls) > 276 let e' = instr_expr e in 277 let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in 278 Clight.Sswitch (e', ls') 279  Clight.Slabel (lbl, s) > 280 let s' = instr_body s in 281 Clight.Slabel (lbl, s') 282  Clight.Scost (lbl, s) > 279 283 (* Keep the cost label in the code. *) 280 let s' = instrument_body l_ind cost_mapping cost_incr s in 281 let atom = lbl.CostLabel.name in 282 let cost = 283 try 284 CostLabel.Atom.Map.find atom cost_mapping 285 with (* if atom is not present, then map to 0 *) 286  Not_found > CostExpr.Exact 0 in 287 let cost = expr_of_cost_expr l_ind cost in 288 let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in 289 let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in 290 Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, [cost]), s')) 291 (* 292 let s' = instrument_body l_ind cost_mapping cost_incr s in 293 let incr = CostLabel.Map.find lbl cost_mapping in 294 if incr = 0 then s' 295 else 296 let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in 297 let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in 298 let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in 299 Clight.Ssequence (Clight.Scall (None, f, args), s') 300 *) 301 (* 302 instrument_body l_ind cost_mapping cost_incr s 303 *) 304 and instrument_ls l_ind cost_mapping cost_incr = function 284 let s' = instr_body s in 285 let atom = lbl.CostLabel.name in 286 let cost = 287 try 288 CostLabel.Atom.Map.find atom cost_mapping 289 with (* if atom is not present, then map to 0 *) 290  Not_found > CostExpr.Exact 0 in 291 let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in 292 let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in 293 let cost_stmt = 294 if not cost_tern then stmt_of_cost_expr l_ind f cost else 295 let cost = expr_of_cost_expr l_ind cost in 296 Clight.Scall(None, f, [cost]) in 297 Clight.Scost (lbl, Clight.Ssequence (cost_stmt, s')) 298 (* 299 let s' = instrument_body l_ind cost_mapping cost_incr s in 300 let incr = CostLabel.Map.find lbl cost_mapping in 301 if incr = 0 then s' 302 else 303 let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in 304 let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in 305 let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in 306 Clight.Ssequence (Clight.Scall (None, f, args), s') 307 *) 308 (* 309 instrument_body l_ind cost_mapping cost_incr s 310 *) 311 and instrument_ls cost_tern l_ind cost_mapping cost_incr = function 305 312  Clight.LSdefault s > 306 let s' = instrument_body l_ind cost_mapping cost_incr s in313 let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in 307 314 Clight.LSdefault s' 308 315  Clight.LScase (i, s, ls) > 309 let s' = instrument_body l_ind cost_mapping cost_incr s in310 let ls' = instrument_ls l_ind cost_mapping cost_incr ls in316 let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in 317 let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in 311 318 Clight.LScase (i, s', ls') 312 319 313 320 let rec loop_indexes_defs prefix max_depth = 314 315 316 317 321 if max_depth = 0 then [] else 322 let max_depth = max_depth  1 in 323 let id = CostLabel.make_id prefix max_depth in 324 (id, int_typ) :: loop_indexes_defs prefix max_depth 318 325 319 326 let max_depth = 320 321 322 323 324 325 326 327 328 327 let f_expr _ _ = () in 328 let f_stmt stmt _ res_stmts = 329 let curr_max = List.fold_left max 0 res_stmts in 330 if curr_max > 0 then curr_max else 331 match stmt with 332  Clight.Swhile(Some x,_,_)  Clight.Sdowhile(Some x,_,_) 333  Clight.Sfor(Some x,_,_,_,_) > x + 1 334  _ > 0 in 335 ClightFold.statement2 f_expr f_stmt 329 336 330 337 (* Instrument a function. *) 331 338 332 let instrument_funct l_ind cost_mapping cost_incr (id, def) =339 let instrument_funct cost_tern l_ind cost_mapping cost_incr (id, def) = 333 340 let def = match def with 334 341  Clight.Internal def > 335 let max_depth = max_depth def.Clight.fn_body in 336 let vars = loop_indexes_defs l_ind max_depth in 337 let vars = List.rev_append vars def.Clight.fn_vars in 338 let body = instrument_body l_ind cost_mapping cost_incr def.Clight.fn_body in 339 Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars} 342 let max_depth = max_depth def.Clight.fn_body in 343 let vars = loop_indexes_defs l_ind max_depth in 344 let vars = List.rev_append vars def.Clight.fn_vars in 345 let body = def.Clight.fn_body in 346 let body = 347 instrument_body cost_tern l_ind cost_mapping cost_incr body in 348 Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars} 340 349  Clight.External _ > def 341 350 in … … 370 379 flush cout ; 371 380 close_out cout 372 373 381 382 374 383 (** [instrument prog cost_map] instruments the program [prog]. First a fresh 375 384 global variable  the socalled cost variable  is added to the program. … … 378 387 name of the cost variable and the name of the cost increment function. *) 379 388 380 let instrument p cost_mapping =389 let instrument cost_tern p cost_mapping = 381 390 382 391 (* Create a fresh 'cost' variable. *) … … 384 393 let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in 385 394 let cost_decl = cost_decl cost_id in 386 387 388 395 396 (* Create a fresh loop index prefix *) 397 let names = StringTools.Set.add cost_id names in 389 398 let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in 390 399 … … 396 405 397 406 (* Turn the mapping from indexed cost labels to integers into one from *) 398 399 407 (* cost atoms to cost expresisons *) 408 let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in 400 409 401 410 (* Instrument each function *) 402 411 let prog_funct = p.Clight.prog_funct in 403 let prog_funct = 404 List.map (instrument_funct l_ind cost_mapping cost_incr) prog_funct in 412 let prog_funct = 413 let f = instrument_funct cost_tern l_ind cost_mapping cost_incr in 414 List.map f prog_funct in 405 415 406 416 (* Glue all this together. *) … … 416 426 let tmp_file = Filename.temp_file "clight_instrument" ".c" in 417 427 save_tmp tmp_file (ClightPrinter.print_program p') ; 418 let res= ClightParser.process tmp_file in428 let p' = ClightParser.process tmp_file in 419 429 Misc.SysExt.safe_remove tmp_file ; 420 ( res, cost_id, cost_incr)430 (p', cost_id, cost_incr)
Note: See TracChangeset
for help on using the changeset viewer.