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

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051indexedlabelsbranch/src/clight/loopUnrolling.ml
r1483 r1507 8 8 9 9 let big_union : IdentSet.t list > IdentSet.t = 10 10 List.fold_left IdentSet.union IdentSet.empty 11 11 12 12 let referenced : statement > IdentSet.t = 13 13 let f_expr e res_list = 14 14 let res = big_union res_list in 15 15 let Expr(ed, _) = e in 16 16 match ed with 17 18 17  Eaddrof (Expr(Evar x, _)) > IdentSet.add x res 18  _ > res in 19 19 let f_stmt stmt eres sres = 20 20 IdentSet.union (big_union eres) (big_union sres) in 21 21 ClightFold.statement2 f_expr f_stmt 22 22 23 23 let mk_heuristic_global_info (max_factor : int) (p : program) 24 24 : heuristic_global_info = 25 26 25 let f set ((id, _), _) = IdentSet.add id set in 26 (max_factor, List.fold_left f IdentSet.empty p.prog_vars) 27 27 28 28 let mk_heuristic_local_info (f : cfunction) = referenced f.fn_body 29 29 30 30 let vars_of_expr, vars_of_stmt = 31 32 31 let f_expr e res_list = 32 let res = big_union res_list in 33 33 let Expr(ed, _) = e in 34 34 match ed with 35 36 35  Evar x > IdentSet.add x res 36  _ > res in 37 37 let f_stmt stmt eres sres = 38 38 IdentSet.union (big_union eres) (big_union sres) in … … 40 40 41 41 let changed_in = 42 let f_expr e _ = () in 42 let f_expr e _ = () in 43 43 let f_stmt stmt _ sres = 44 let res = big_union sres in 45 match stmt with 46  Sassign (Expr(Evar x, _), _) 47  Clight.Scall (Some (Expr(Evar x, _)), _, _) > 48 (* a situation like "*&x = ... " is avoided as dereferenced variables*) 49 (* will be excluded a priori *) 50 IdentSet.add x res 51  _ > res in 52 ClightFold.statement2 f_expr f_stmt 44 let res = big_union sres in 45 match stmt with 46  Sassign (Expr(Evar x, _), _) 47  Clight.Scall (Some (Expr(Evar x, _)), _, _) > 48 (* a situation like "*&x = ... " is avoided as dereferenced variables*) 49 (* will be excluded a priori *) 50 IdentSet.add x res 51  _ > res in 52 ClightFold.statement2 f_expr f_stmt 53 54 type sign = 55  Plus 56  Minus 57 58 let find_increment = function 59  Sassign( 60 Expr(Evar x,_), 61 Expr( 62 (Ebinop(Oadd,Expr(Evar y,_),inc)  63 Ebinop(Oadd,inc,Expr(Evar y,_)) ),_)) 64 when x = y > Some (x, Plus, inc) 65  Sassign( 66 Expr(Evar x,_), 67 Expr( 68 (Ebinop(Osub,Expr(Evar y,_),inc)  69 Ebinop(Osub,inc,Expr(Evar y,_)) ),_)) 70 when x = y > Some (x, Minus, inc) 71  _ > None 72 73 let find_bound s x (Expr(ed, _)) = match s, ed with 74  Plus, Ebinop(Olt,Expr(Evar y,_),b) 75  Plus, Ebinop(Ogt,b,Expr(Evar y,_)) 76  Minus, Ebinop(Olt,b,Expr(Evar y,_)) 77  Minus, Ebinop(Ogt,Expr(Evar y,_),b) 78 when y = x > Some (false, b) 79  Plus, Ebinop(Ole,Expr(Evar y,_),b) 80  Plus, Ebinop(Oge,b,Expr(Evar y,_)) 81  Minus, Ebinop(Ole,b,Expr(Evar y,_)) 82  Minus, Ebinop(Oge,Expr(Evar y,_),b) 83 when y = x > Some (true, b) 84  _ > None 53 85 54 86 (* this function tells when to perform the optimization on a statement. It *) 55 (* should always return [false] when the optimization cannot be applied *) 87 (* should always return [false] when the optimization cannot be applied *) 56 88 let heuristics 57 89 ((max_factor, global_vars) : heuristic_global_info) 58 90 (rfrncd_vars : heuristic_local_info) 59 : Clight.statement > int option = 60 let global_referenced = IdentSet.union global_vars rfrncd_vars in 61 function 62  Clight.Sfor (Some _, init, guard, tail, body) > 63 let head_vars = 64 IdentSet.union 65 (vars_of_stmt init) 66 (IdentSet.union (vars_of_expr guard) (vars_of_stmt tail)) in 67 let dangerous = 68 IdentSet.union (changed_in body) global_referenced in 69 if IdentSet.is_empty (IdentSet.inter head_vars dangerous) then 70 Some max_factor 71 else 72 None 73 (* TODO add a check for size *) 74  _ > None 91 : Clight.statement > (int * AST.ident * sign * expr * expr * bool) option = 92 let global_referenced = IdentSet.union global_vars rfrncd_vars in 93 function 94  Clight.Sfor (Some _, init, guard, tail, body) > 95 begin 96 match find_increment tail with 97  Some (x, dir, inc) > 98 begin 99 match find_bound dir x guard with 100  Some (included, bound) > 101 let head_vars = 102 IdentSet.union (vars_of_expr guard) (vars_of_stmt tail) in 103 let dangerous = 104 IdentSet.union (changed_in body) global_referenced in 105 if IdentSet.is_empty (IdentSet.inter head_vars dangerous) then 106 Some (max_factor, x, dir, inc, bound, included) 107 else 108 None 109  None > None 110 end 111  None > None 112 end 113 (* TODO add a check for size *) 114  _ > None 75 115 76 116 let sexpr a b = CostLabel.Sexpr(a,b) … … 85 125  _ > ClightFold.expr_fill_exprs e expr_res in 86 126 let f_stmt i s stmt expr_res stmt_res = 87 88 127 match stmt, stmt_res with 128  Clight.Scost(lbl, _), stmt' :: _ > 89 129 let lbl = CostLabel.comp_index i s lbl in 90 91 92 130 Clight.Scost(lbl,stmt') 131  _ > ClightFold.statement_fill_subs stmt expr_res stmt_res in 132 (fun i s > ClightFold.expr2 (f_expr i s)), 93 133 (fun i s > ClightFold.statement2 (f_expr i s) (f_stmt i s)) 94 134 95 135 let labels_of = 96 97 98 99 100 101 102 136 let f_expr _ _ = () in 137 let f_stmt stmt _ res_stmts = 138 let s = match stmt with 139  Clight.Slabel(lbl, _) > Label.Set.singleton lbl 140  _ > Label.Set.empty in 141 List.fold_left Label.Set.union s res_stmts in 142 ClightFold.statement2 f_expr f_stmt 103 143 104 144 let create_fresh_labels fresh lbl_set = 105 106 107 145 let f_lbl lbl = Label.Map.add lbl (fresh ()) in 146 Label.Set.fold f_lbl lbl_set Label.Map.empty 147 108 148 let apply_label_map map = 109 110 111 149 let f_stmt stmt exprs stmts = 150 match stmt, stmts with 151  Clight.Slabel (lbl, _), s :: _ > 112 152 (* lbl must be in domain of map *) 113 114 115 116 117 118 119 120 121 122 123 124 (* unroll the kth copy over a total of n *) 153 Clight.Slabel (Label.Map.find lbl map, s) 154  Clight.Sgoto lbl, _ > 155 Clight.Sgoto ( 156 try 157 Label.Map.find lbl map 158 with 159  Not_found > (* means it is an outgoing goto *) 160 lbl) 161  _ > ClightFold.statement_fill_subs stmt exprs stmts in 162 ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt 163 164 (* unroll the kth copy over a total of n *) 125 165 let rec do_the_unrolling fresh k n i e sb st labels_of_sb = 126 127 let preamble = do_the_unrolling fresh (k1) n i e sb st labels_of_sb in 128 let st_pre = reindex_stmt i (sexpr n (k1)) st in129 let e_next = reindex_expr i (sexpr n k) e in130 131 let sb_next = reindex_stmt i (sexpr n k) sb_next in132 133 Ssequence(st_pre,134 Ssequence(Sifthenelse(e_next, Sskip, Sbreak),135 166 if k = 0 then reindex_stmt i (sexpr n 0) sb else 167 let preamble = do_the_unrolling fresh (k1) n i e sb st labels_of_sb in 168 let st_pre = reindex_stmt i (sexpr n (k1)) st in 169 let e_next = reindex_expr i (sexpr n k) e in 170 let sb_next = apply_label_map (create_fresh_labels fresh labels_of_sb) sb in 171 let sb_next = reindex_stmt i (sexpr n k) sb_next in 172 Ssequence(preamble, 173 Ssequence(st_pre, 174 Ssequence(Sifthenelse(e_next, Sskip, Sbreak), 175 sb_next))) 136 176 137 177 let unroll fresh g_info l_info = 138 let f_stmt stmt exprs stmts = 139 match heuristics g_info l_info stmt, stmt, exprs, stmts with 140  Some k, Clight.Sfor (Some i, _, _, _, _), e :: _, si :: st :: sb ::_ > 141 (* we can suppose no label in s3 is target of a goto outside of stmt, *) 142 (* as loop is indexed and thus single entry. So we can freely rename *) 143 (* labels in stmt. *) 144 (* IMPORTANT: I am supposing no labels are in s1 and s2 *) 145 let labels_of_sb = labels_of sb in 146 let e_first = reindex_expr i (sexpr k 0) e in 147 let st_last = reindex_stmt i (sexpr k (k1)) st in 148 let body = do_the_unrolling fresh (k1) k i e sb st labels_of_sb in 149 Sfor (Some i, si, e_first, st_last, body) 150  Some _, _, _, _ > 151 assert false (* heuristics should have crossed out other cases *) 152  _ > ClightFold.statement_fill_subs stmt exprs stmts in 153 ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt 178 let f_stmt stmt exprs stmts = 179 match heuristics g_info l_info stmt, stmt, exprs, stmts with 180  Some (k, x, dir, inc, bound, included), 181 Clight.Sfor (Some i, _, _, _, _), e :: _, si :: st :: sb ::_ > 182 (* we can suppose no label in s3 is target of a goto outside of stmt, *) 183 (* as loop is indexed and thus single entry. So we can freely rename *) 184 (* labels in stmt. *) 185 (* IMPORTANT: I am supposing no labels are in s1 and s2 *) 186 let labels_of_sb = labels_of sb in 187 let e_first = reindex_expr i (sexpr k 0) e in 188 let st_last = reindex_stmt i (sexpr k (k1)) st in 189 let body = do_the_unrolling fresh (k1) k i e sb st labels_of_sb in 190 Sfor (Some i, si, e_first, st_last, body) 191  Some _, _, _, _ > 192 assert false (* heuristics should have crossed out other cases *) 193  _ > ClightFold.statement_fill_subs stmt exprs stmts in 194 ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt 154 195 155 196 let unroll_funct fresh g_info = function 156 157 158 159 160 197  (id, Clight.Internal def) > 198 let l_info = mk_heuristic_local_info def in 199 let body = unroll fresh g_info l_info def.Clight.fn_body in 200 (id, Clight.Internal {def with Clight.fn_body = body}) 201  f > f 161 202 162 203 open Languages 163 204 164 205 let trans ?(factor = 2) () = Clight, function 165 166 167 206  AstClight p > 207 let g_info = mk_heuristic_global_info factor p in 208 let fresh = ClightAnnotator.make_fresh "_l" p in 168 209 let functs = List.map (unroll_funct fresh g_info) p.Clight.prog_funct in 169 AstClight { p with Clight.prog_funct = functs } 170  _ > assert false 171 210 AstClight { p with Clight.prog_funct = functs } 211  _ > assert false
Note: See TracChangeset
for help on using the changeset viewer.