source: Deliverables/D2.2/8051-indexed-labels-branch/src/clight/loopUnrolling.ml @ 1483

Last change on this file since 1483 was 1483, checked in by tranquil, 9 years ago
  • implemented a first draft of loop unrolling
  • correced bugs in CostExpr?
File size: 6.0 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
54(* this function tells when to perform the optimization on a statement. It *)
55(* should always return [false] when the optimization cannot be applied *) 
56let heuristics
57    ((max_factor, global_vars) : heuristic_global_info)
58    (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
75
76let sexpr a b = CostLabel.Sexpr(a,b)
77
78(** compose the mapping i |--> s with all labels *)
79let reindex_expr, reindex_stmt =
80  let f_expr i s e expr_res =
81    match e, expr_res with
82      | Clight.Expr (Clight.Ecost (lbl, _), t), e::_ ->
83        let lbl = CostLabel.comp_index i s lbl in
84        Clight.Expr (Clight.Ecost (lbl, e), t)
85      | _ -> ClightFold.expr_fill_exprs e expr_res in
86  let f_stmt i s stmt expr_res stmt_res =
87                match stmt, stmt_res with
88                        | Clight.Scost(lbl, _), stmt' :: _ ->
89        let lbl = CostLabel.comp_index i s lbl in
90                                Clight.Scost(lbl,stmt')
91                        | _ -> ClightFold.statement_fill_subs stmt expr_res stmt_res in
92        (fun i s -> ClightFold.expr2 (f_expr i s)),
93  (fun i s -> ClightFold.statement2 (f_expr i s) (f_stmt i s))
94
95let labels_of =
96        let f_expr _ _ = () in
97        let f_stmt stmt _ res_stmts =
98                let s = match stmt with
99                        | Clight.Slabel(lbl, _) -> Label.Set.singleton lbl
100                        | _ -> Label.Set.empty in
101                List.fold_left Label.Set.union s res_stmts in
102        ClightFold.statement2 f_expr f_stmt
103
104let create_fresh_labels fresh lbl_set =
105        let f_lbl lbl = Label.Map.add lbl (fresh ()) in
106        Label.Set.fold f_lbl lbl_set Label.Map.empty
107       
108let apply_label_map map =
109        let f_stmt stmt exprs stmts =
110                match stmt, stmts with
111                        | Clight.Slabel (lbl, _), s :: _ ->
112                                (* lbl must be in domain of map *)
113                                Clight.Slabel (Label.Map.find lbl map, s)
114                        | Clight.Sgoto lbl, _ ->
115                                Clight.Sgoto (
116                                        try
117                                                Label.Map.find lbl map
118                                  with
119                                          | Not_found -> (* means it is an outgoing goto *)
120                                            lbl)
121                        | _ -> ClightFold.statement_fill_subs stmt exprs stmts in
122        ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
123
124(* unroll the k-th copy over a total of n *)   
125let rec do_the_unrolling fresh k n i e sb st labels_of_sb =
126        if k = 0 then reindex_stmt i (sexpr n 0) sb else
127        let preamble = do_the_unrolling fresh (k-1) n i e sb st labels_of_sb in 
128  let st_pre = reindex_stmt i (sexpr n (k-1)) st in
129  let e_next = reindex_expr i (sexpr n k) e in
130        let sb_next = apply_label_map (create_fresh_labels fresh labels_of_sb) sb in
131  let sb_next = reindex_stmt i (sexpr n k) sb_next in
132        Ssequence(preamble,
133        Ssequence(st_pre,
134        Ssequence(Sifthenelse(e_next, Sskip, Sbreak),
135                  sb_next)))
136
137let 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 (k-1)) st in
148                                let body = do_the_unrolling fresh (k-1) 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
154
155let unroll_funct fresh g_info = function
156        | (id, Clight.Internal def) ->
157                let l_info = mk_heuristic_local_info def in
158                let body = unroll fresh g_info l_info def.Clight.fn_body in
159                (id, Clight.Internal {def with Clight.fn_body = body})
160        | f -> f
161
162open Languages
163
164let trans ?(factor = 2) () = Clight, function
165        | AstClight p ->
166                let g_info = mk_heuristic_global_info factor p in
167                let fresh = ClightAnnotator.make_fresh "_l" p in
168    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               
Note: See TracBrowser for help on using the repository browser.