source: Deliverables/D2.2/8051/src/clight/loopPeeling.ml @ 1569

Last change on this file since 1569 was 1569, checked in by tranquil, 8 years ago
  • added in repository some missing files...
File size: 6.2 KB
Line 
1
2(* this type should hold global information used by the heuristics to take a *)
3(* decision. As for now we employ a trivial heuristics, no information *)
4(* is actually needed. *)
5type heuristics_info = unit
6
7let mk_heuristics_info (p : Clight.program) = ()
8
9(* this function tells when to perform the optimization on a statement. It *)
10(* should always return [false] when the optimization cannot be applied *) 
11let heuristics
12    (_ : heuristics_info)
13                : Clight.statement -> bool = function
14                        | Clight.Swhile (Some _, _, _) | Clight.Sfor (Some _, _, _, _, _)
15                        | Clight.Sdowhile (Some _, _, _) -> true
16                        | _ -> false
17
18let zero_sexpr = CostLabel.Sexpr(0,0)
19let succ_sexpr = CostLabel.Sexpr(1,1)
20
21
22let f_expr_reindex i s e expr_res =
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
29(** compose the mapping i |--> s with all labels in a statement *)
30let reindex_stmt i s =
31  let f_stmt stmt expr_res stmt_res =
32                match stmt, stmt_res with
33                        | Clight.Scost(lbl, _), stmt' :: _ ->
34        let lbl = CostLabel.comp_index i s lbl in
35                                Clight.Scost(lbl,stmt')
36                        | _ -> ClightFold.statement_fill_subs stmt expr_res stmt_res in
37  ClightFold.statement2 (f_expr_reindex i s) f_stmt
38
39(** compose the mapping i |--> s with all labels in an expression *)
40let reindex_expr i s =
41  ClightFold.expr2 (f_expr_reindex i s)
42
43let labels_of =
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
52let create_fresh_labels fresh lbl_set =
53        let f_lbl lbl = Label.Map.add lbl (fresh ()) in
54        Label.Set.fold f_lbl lbl_set Label.Map.empty
55       
56let apply_label_map map =
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               
72let peel fresh info =
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 (second and onwards) iteration 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
137let peel_funct fresh info = function
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
143let apply p =
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       
149open Languages
150
151let trans =
152        (Clight, function (AstClight p) -> AstClight (apply p) | _ -> assert false) 
153               
Note: See TracBrowser for help on using the repository browser.