1 | open Clight |
---|
2 | |
---|
3 | module IdentSet = Set.Make(struct type t = AST.ident let compare = compare end) |
---|
4 | |
---|
5 | type heuristic_global_info = int * IdentSet.t |
---|
6 | |
---|
7 | type heuristic_local_info = IdentSet.t |
---|
8 | |
---|
9 | let big_union : IdentSet.t list -> IdentSet.t = |
---|
10 | List.fold_left IdentSet.union IdentSet.empty |
---|
11 | |
---|
12 | let referenced : statement -> IdentSet.t = |
---|
13 | let f_expr e res_list = |
---|
14 | let res = big_union res_list in |
---|
15 | let Expr(ed, _) = e in |
---|
16 | match ed with |
---|
17 | | Eaddrof (Expr(Evar x, _)) -> IdentSet.add x res |
---|
18 | | _ -> res in |
---|
19 | let f_stmt stmt eres sres = |
---|
20 | IdentSet.union (big_union eres) (big_union sres) in |
---|
21 | ClightFold.statement2 f_expr f_stmt |
---|
22 | |
---|
23 | let mk_heuristic_global_info (max_factor : int) (p : program) |
---|
24 | : heuristic_global_info = |
---|
25 | let f set ((id, _), _) = IdentSet.add id set in |
---|
26 | (max_factor, List.fold_left f IdentSet.empty p.prog_vars) |
---|
27 | |
---|
28 | let mk_heuristic_local_info (f : cfunction) = referenced f.fn_body |
---|
29 | |
---|
30 | let vars_of_expr, vars_of_stmt = |
---|
31 | let f_expr e res_list = |
---|
32 | let res = big_union res_list in |
---|
33 | let Expr(ed, _) = e in |
---|
34 | match ed with |
---|
35 | | Evar x -> IdentSet.add x res |
---|
36 | | _ -> res in |
---|
37 | let f_stmt stmt eres sres = |
---|
38 | IdentSet.union (big_union eres) (big_union sres) in |
---|
39 | ClightFold.expr2 f_expr, ClightFold.statement2 f_expr f_stmt |
---|
40 | |
---|
41 | let changed_in = |
---|
42 | let f_expr e _ = () in |
---|
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 |
---|
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 |
---|
85 | |
---|
86 | (* this function tells when to perform the optimization on a statement. It *) |
---|
87 | (* should always return [false] when the optimization cannot be applied *) |
---|
88 | let heuristics |
---|
89 | ((max_factor, global_vars) : heuristic_global_info) |
---|
90 | (rfrncd_vars : heuristic_local_info) |
---|
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 |
---|
115 | |
---|
116 | let sexpr a b = CostLabel.Sexpr(a,b) |
---|
117 | |
---|
118 | (** compose the mapping i |--> s with all labels *) |
---|
119 | let reindex_expr, reindex_stmt = |
---|
120 | let f_expr i s e expr_res = |
---|
121 | match e, expr_res with |
---|
122 | | Clight.Expr (Clight.Ecost (lbl, _), t), e::_ -> |
---|
123 | let lbl = CostLabel.comp_index i s lbl in |
---|
124 | Clight.Expr (Clight.Ecost (lbl, e), t) |
---|
125 | | _ -> ClightFold.expr_fill_exprs e expr_res in |
---|
126 | let f_stmt i s stmt expr_res stmt_res = |
---|
127 | match stmt, stmt_res with |
---|
128 | | Clight.Scost(lbl, _), stmt' :: _ -> |
---|
129 | let lbl = CostLabel.comp_index i s lbl in |
---|
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)), |
---|
133 | (fun i s -> ClightFold.statement2 (f_expr i s) (f_stmt i s)) |
---|
134 | |
---|
135 | let labels_of = |
---|
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 |
---|
143 | |
---|
144 | let create_fresh_labels fresh lbl_set = |
---|
145 | let f_lbl lbl = Label.Map.add lbl (fresh ()) in |
---|
146 | Label.Set.fold f_lbl lbl_set Label.Map.empty |
---|
147 | |
---|
148 | let apply_label_map map = |
---|
149 | let f_stmt stmt exprs stmts = |
---|
150 | match stmt, stmts with |
---|
151 | | Clight.Slabel (lbl, _), s :: _ -> |
---|
152 | (* lbl must be in domain of map *) |
---|
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 k-th copy over a total of n *) |
---|
165 | let rec do_the_unrolling fresh k n i e sb st labels_of_sb = |
---|
166 | if k = 0 then reindex_stmt i (sexpr n 0) sb else |
---|
167 | let preamble = do_the_unrolling fresh (k-1) n i e sb st labels_of_sb in |
---|
168 | let st_pre = reindex_stmt i (sexpr n (k-1)) 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))) |
---|
176 | |
---|
177 | let unroll fresh g_info l_info = |
---|
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 (k-1)) st in |
---|
189 | let body = do_the_unrolling fresh (k-1) 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 |
---|
195 | |
---|
196 | let unroll_funct fresh g_info = function |
---|
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 |
---|
202 | |
---|
203 | open Languages |
---|
204 | |
---|
205 | let trans ?(factor = 2) () = Clight, function |
---|
206 | | AstClight p -> |
---|
207 | let g_info = mk_heuristic_global_info factor p in |
---|
208 | let fresh = ClightAnnotator.make_fresh "_l" p in |
---|
209 | let functs = List.map (unroll_funct fresh g_info) p.Clight.prog_funct in |
---|
210 | AstClight { p with Clight.prog_funct = functs } |
---|
211 | | _ -> assert false |
---|