source: Deliverables/D2.2/8051/src/clight/loopUnrolling.ml @ 3673

Last change on this file since 3673 was 1569, checked in by tranquil, 8 years ago
  • added in repository some missing files...
File size: 7.2 KB
Line 
1open Clight
2
3module IdentSet = Set.Make(struct type t = AST.ident let compare = compare end)
4
5type heuristic_global_info = int * IdentSet.t
6
7type heuristic_local_info = IdentSet.t
8
9let big_union : IdentSet.t list -> IdentSet.t =
10  List.fold_left IdentSet.union IdentSet.empty
11
12let 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
23let 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
28let mk_heuristic_local_info (f : cfunction) =   referenced f.fn_body
29
30let 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
41let 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
54type sign =
55  | Plus
56  | Minus
57
58let 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
73let 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 *)
88let 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
116let sexpr a b = CostLabel.Sexpr(a,b)
117
118(** compose the mapping i |--> s with all labels *)
119let 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
135let 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
144let 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
148let 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 *)
165let 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
177let 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
196let 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
203open Languages
204
205let 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
Note: See TracBrowser for help on using the repository browser.