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

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

implemented constant propagation in LTL
cleaned up translations in optimizations, a new module for translations is available

File size: 6.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 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 following iterations 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)
Note: See TracBrowser for help on using the repository browser.