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

Last change on this file since 1664 was 1664, checked in by tranquil, 8 years ago

corrected a bug in loop peeling where continue and breaks were not handled right

File size: 8.5 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 remove_cnt_brk cnt_lbl brk_lbl =
73  let f_stmt stmt exprs stmts =
74    match stmt with
75      | Clight.Sbreak -> Clight.Sgoto brk_lbl
76      | Clight.Scontinue -> Clight.Sgoto cnt_lbl
77      | _ ->ClightFold. statement_fill_subs stmt exprs stmts in
78  ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
79
80let peel fresh info =
81  let process_cnt_brk peeled_body has_brk has_cnt =
82    let (brk_lbl, add_tail) = if has_brk then
83        let new_lbl = fresh () in
84        (new_lbl, fun stmt ->
85          Clight.Ssequence (stmt, Clight.Slabel (new_lbl, Clight.Sskip)))
86      else
87        (Label.dummy, fun stmt -> stmt) in
88    let (cnt_lbl, add_head) = if has_cnt then
89        let new_lbl = fresh () in
90        (new_lbl, fun stmt -> Clight.Slabel(new_lbl, stmt))
91      else
92        (Label.dummy, fun stmt -> stmt) in
93          (* we could avoid making a further pass, but sacrificing the use
94             of the fold machinery *)
95    let peeled_body = if has_brk || has_cnt then
96        remove_cnt_brk cnt_lbl brk_lbl peeled_body
97      else peeled_body in
98    (add_head, peeled_body, add_tail) in
99
100  let f_stmt stmt exprs stmts_w_flags =
101    if heuristics info stmt then
102      match stmt, exprs, stmts_w_flags with
103        | Clight.Swhile (Some i, _, _), e :: _, (s, (has_brk, has_cnt)) :: _  ->
104      (* we can suppose no label in stmt is target of a goto outside of stmt, *)
105      (* as loop is indexed and thus single entry. So we can freely rename *)
106      (* labels in stmt. Notice outgoing gotos are not changed *)
107          let label_map = create_fresh_labels fresh (labels_of s) in
108          let s_first = apply_label_map label_map s in
109          (* reindex to zero the copies of s and e *)
110          let s_first = reindex_stmt i zero_sexpr s_first in
111          let e_first = reindex_expr i zero_sexpr e in
112          (* reindex to successor the other copies of s and e *)
113          let s_next = reindex_stmt i succ_sexpr s in
114          let e_next = reindex_expr i succ_sexpr e in
115          (* rebuild the loop *)
116          let loop = Clight.Swhile(Some i, e_next, s_next) in
117          (* all break and continue statements, if any, must be replaced by
118             gotos in the peeled body *)
119          let (head, s_first, tail) = process_cnt_brk s_first has_brk has_cnt in
120          (* build the peeled loop *)
121          let peeled = Clight.Ssequence(s_first, head loop) in
122          (tail (Clight.Sifthenelse(e_first, peeled, Clight.Sskip)),
123           (false, false))
124        | Clight.Sdowhile (Some i, _, _), e :: _,
125           (s, (has_brk, has_cnt)) :: _  ->
126        (* we can suppose no label in stmt is target of a goto outside, *)
127        (* as loop is indexed and thus single entry. So we can freely rename *)
128        (* labels in stmt. *)
129          let label_map = create_fresh_labels fresh (labels_of s) in
130          let s_first = apply_label_map label_map s in
131          (* reindex to zero the copies of s and e *)
132          let s_first = reindex_stmt i zero_sexpr s_first in
133          let e_first = reindex_expr i zero_sexpr e in
134          (* reindex to successor the other copies of s and e *)
135          let s_next = reindex_stmt i succ_sexpr s in
136          let e_next = reindex_expr i succ_sexpr e in
137          (* rebuild the loop *)
138          let loop = Clight.Sdowhile(Some i, e_next, s_next) in
139          let (head, s_first, tail) = process_cnt_brk s_first has_brk has_cnt in
140          (* put a guard before the following iterations of the loop *)
141          let guarded_loop =
142            Clight.Sifthenelse(e_first, head loop, Clight.Sskip) in
143          (* build the peeled loop *)
144          (tail (Clight.Ssequence(s_first, guarded_loop)), (false, false))
145        | Clight.Sfor (Some i, _, _, _, _), e :: _,
146           (s1, _) :: (s2, _) :: (s3, (has_brk, has_cnt)) ::_ ->
147        (* we can suppose no label in s3 is target of a goto outside of stmt, *)
148        (* as loop is indexed and thus single entry. So we can freely rename *)
149        (* labels in stmt. *)
150        (* IMPORTANT: I am supposing no labels are in s1 and s2 *)
151          let label_map = create_fresh_labels fresh (labels_of s3) in
152          let s3_first = apply_label_map label_map s3 in
153          (* reindex to zero the copies of s2, s3 and e *)
154          let s2_first = reindex_stmt i zero_sexpr s2 in
155          let s3_first = reindex_stmt i zero_sexpr s3_first in
156          let e_first = reindex_expr i zero_sexpr e in
157          (* reindex to successor the other copies of s2, s3 and e *)
158          let s2_next = reindex_stmt i succ_sexpr s2 in
159          let s3_next = reindex_stmt i succ_sexpr s3 in
160          let e_next = reindex_expr i succ_sexpr e in
161          (* rebuild the loop *)
162          let loop = Clight.Sfor(Some i, s2_first, e_next, s2_next, s3_next) in
163          let (head, s3_first, tail) =
164            process_cnt_brk s3_first has_brk has_cnt in
165          (* build the peeled loop *)
166          let peeled = Clight.Ssequence(s3_first, head loop) in
167          let guarded = Clight.Sifthenelse(e_first, peeled, Clight.Sskip) in
168          (* add the guard at the start *)
169          (tail (Clight.Ssequence(s1, guarded)), (false, false))
170        | _ -> assert false (* heuristics should have crossed out other cases *)
171    else match stmt with
172      | Clight.Sbreak -> (Clight.Sbreak, (true, false))
173      | Clight.Scontinue -> (Clight.Scontinue, (false, true))
174      | _ ->
175        let stmts, flags = List.split stmts_w_flags in
176        let f (b1, b2) (c1, c2) = (b1 || c1, b2 || c2) in
177        (ClightFold.statement_fill_subs stmt exprs stmts,
178         List.fold_left f (false, false) flags) in
179  ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
180
181let peel_funct fresh info = function
182  | (id, Clight.Internal def) ->
183    let body, _ = peel fresh info def.Clight.fn_body in
184    (id, Clight.Internal {def with Clight.fn_body = body})
185  | _ as p -> p
186
187let apply p =
188  let fresh = ClightAnnotator.make_fresh "_l" p in
189  let info = mk_heuristics_info p in
190  let functs = List.map (peel_funct fresh info) p.Clight.prog_funct in
191  {p with Clight.prog_funct = functs}
192
193open Languages
194
195let trans =
196  (Clight, function (AstClight p) -> AstClight (apply p) | _ -> assert false)
Note: See TracBrowser for help on using the repository browser.