Changeset 1580 for Deliverables/D2.2/8051/src/clight/loopPeeling.ml
 Timestamp:
 Dec 1, 2011, 2:50:27 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051/src/clight/loopPeeling.ml
r1569 r1580 8 8 9 9 (* this function tells when to perform the optimization on a statement. It *) 10 (* should always return [false] when the optimization cannot be applied *) 10 (* should always return [false] when the optimization cannot be applied *) 11 11 let heuristics 12 12 (_ : heuristics_info) 13 14 15 16 13 : Clight.statement > bool = function 14  Clight.Swhile (Some _, _, _)  Clight.Sfor (Some _, _, _, _, _) 15  Clight.Sdowhile (Some _, _, _) > true 16  _ > false 17 17 18 18 let zero_sexpr = CostLabel.Sexpr(0,0) … … 21 21 22 22 let f_expr_reindex i s e expr_res = 23 24 25 26 27 23 match e, expr_res with 24  Clight.Expr (Clight.Ecost (lbl, _), t), e::_ > 25 let lbl = CostLabel.comp_index i s lbl in 26 Clight.Expr (Clight.Ecost (lbl, e), t) 27  _ > ClightFold.expr_fill_exprs e expr_res 28 28 29 29 (** compose the mapping i > s with all labels in a statement *) 30 30 let reindex_stmt i s = 31 31 let f_stmt stmt expr_res stmt_res = 32 33 32 match stmt, stmt_res with 33  Clight.Scost(lbl, _), stmt' :: _ > 34 34 let lbl = CostLabel.comp_index i s lbl in 35 36 35 Clight.Scost(lbl,stmt') 36  _ > ClightFold.statement_fill_subs stmt expr_res stmt_res in 37 37 ClightFold.statement2 (f_expr_reindex i s) f_stmt 38 38 … … 42 42 43 43 let labels_of = 44 45 46 47 48 49 50 44 let f_expr _ _ = () in 45 let f_stmt stmt _ res_stmts = 46 let s = match stmt with 47  Clight.Slabel(lbl, _) > Label.Set.singleton lbl 48  _ > Label.Set.empty in 49 List.fold_left Label.Set.union s res_stmts in 50 ClightFold.statement2 f_expr f_stmt 51 51 52 52 let create_fresh_labels fresh lbl_set = 53 54 55 53 let f_lbl lbl = Label.Map.add lbl (fresh ()) in 54 Label.Set.fold f_lbl lbl_set Label.Map.empty 55 56 56 let apply_label_map map = 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 57 let f_stmt stmt exprs stmts = 58 match stmt, stmts with 59  Clight.Slabel (lbl, _), s :: _ > 60 (* lbl must be in domain of map *) 61 Clight.Slabel (Label.Map.find lbl map, s) 62  Clight.Sgoto lbl, _ > 63 Clight.Sgoto ( 64 try 65 Label.Map.find lbl map 66 with 67  Not_found > (* means it is an outgoing goto *) 68 lbl) 69  _ > ClightFold.statement_fill_subs stmt exprs stmts in 70 ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt 71 72 72 let peel fresh info = 73 let f_stmt stmt exprs stmts = 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 (* put a guard before the (second and onwards) iteration of the loop *) 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 73 let f_stmt stmt exprs stmts = 74 if heuristics info stmt then 75 match stmt, exprs, stmts with 76  Clight.Swhile (Some i, _, _), e :: _, s :: _ > 77 (* we can suppose no label in stmt is target of a goto outside of stmt, *) 78 (* as loop is indexed and thus single entry. So we can freely rename *) 79 (* labels in stmt. Notice outgoing gotos are not changed *) 80 let label_map = create_fresh_labels fresh (labels_of s) in 81 let s_first = apply_label_map label_map s in 82 (* reindex to zero the copies of s and e *) 83 let s_first = reindex_stmt i zero_sexpr s_first in 84 let e_first = reindex_expr i zero_sexpr e in 85 (* reindex to successor the other copies of s and e *) 86 let s_next = reindex_stmt i succ_sexpr s in 87 let e_next = reindex_expr i succ_sexpr e in 88 (* rebuild the loop *) 89 let loop = Clight.Swhile(Some i, e_next, s_next) in 90 (* build the peeled loop *) 91 let peeled = Clight.Ssequence(s_first, loop) in 92 (* add the guard at the start *) 93 Clight.Sifthenelse(e_first, peeled, Clight.Sskip) 94  Clight.Sdowhile (Some i, _, _), e :: _, s :: _ > 95 (* we can suppose no label in stmt is target of a goto outside of stmt, *) 96 (* as loop is indexed and thus single entry. So we can freely rename *) 97 (* labels in stmt. *) 98 let label_map = create_fresh_labels fresh (labels_of s) in 99 let s_first = apply_label_map label_map s in 100 (* reindex to zero the copies of s and e *) 101 let s_first = reindex_stmt i zero_sexpr s_first in 102 let e_first = reindex_expr i zero_sexpr e in 103 (* reindex to successor the other copies of s and e *) 104 let s_next = reindex_stmt i succ_sexpr s in 105 let e_next = reindex_expr i succ_sexpr e in 106 (* rebuild the loop *) 107 let loop = Clight.Sdowhile(Some i, e_next, s_next) in 108 (* put a guard before the following iterations of the loop *) 109 let guarded_loop = Clight.Sifthenelse(e_first, loop, Clight.Sskip) in 110 (* build the peeled loop *) 111 Clight.Ssequence(s_first, guarded_loop) 112  Clight.Sfor (Some i, _, _, _, _), e :: _, s1 :: s2 :: s3 ::_ > 113 (* we can suppose no label in s3 is target of a goto outside of stmt, *) 114 (* as loop is indexed and thus single entry. So we can freely rename *) 115 (* labels in stmt. *) 116 (* IMPORTANT: I am supposing no labels are in s1 and s2 *) 117 let label_map = create_fresh_labels fresh (labels_of s3) in 118 let s3_first = apply_label_map label_map s3 in 119 (* reindex to zero the copies of s2, s3 and e *) 120 let s2_first = reindex_stmt i zero_sexpr s2 in 121 let s3_first = reindex_stmt i zero_sexpr s3_first in 122 let e_first = reindex_expr i zero_sexpr e in 123 (* reindex to successor the other copies of s2, s3 and e *) 124 let s2_next = reindex_stmt i succ_sexpr s2 in 125 let s3_next = reindex_stmt i succ_sexpr s3 in 126 let e_next = reindex_expr i succ_sexpr e in 127 (* rebuild the loop *) 128 let loop = Clight.Sfor(Some i, s2_first, e_next, s2_next, s3_next) in 129 (* build the peeled loop *) 130 let peeled = Clight.Ssequence(s3_first, loop) in 131 (* add the guard at the start *) 132 Clight.Ssequence(s1,Clight.Sifthenelse(e_first, peeled, Clight.Sskip)) 133  _ > assert false (* heuristics should have crossed out other cases *) 134 else ClightFold.statement_fill_subs stmt exprs stmts in 135 ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt 136 136 137 137 let peel_funct fresh info = function 138 139 140 141 138  (id, Clight.Internal def) > 139 let body = peel fresh info def.Clight.fn_body in 140 (id, Clight.Internal {def with Clight.fn_body = body}) 141  _ as p > p 142 142 143 143 let apply p = 144 145 146 147 {p with Clight.prog_funct = functs} 148 144 let fresh = ClightAnnotator.make_fresh "_l" p in 145 let info = mk_heuristics_info p in 146 let functs = List.map (peel_funct fresh info) p.Clight.prog_funct in 147 {p with Clight.prog_funct = functs} 148 149 149 open Languages 150 150 151 151 let trans = 152 (Clight, function (AstClight p) > AstClight (apply p)  _ > assert false) 153 152 (Clight, function (AstClight p) > AstClight (apply p)  _ > assert false)
Note: See TracChangeset
for help on using the changeset viewer.