Ignore:
Timestamp:
Dec 1, 2011, 2:50:27 PM (8 years ago)
Author:
tranquil
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/clight/loopPeeling.ml

    r1569 r1580  
    88
    99(* this function tells when to perform the optimization on a statement. It *)
    10 (* should always return [false] when the optimization cannot be applied *) 
     10(* should always return [false] when the optimization cannot be applied *)
    1111let heuristics
    1212    (_ : heuristics_info)
    13                 : Clight.statement -> bool = function
    14                         | Clight.Swhile (Some _, _, _) | Clight.Sfor (Some _, _, _, _, _)
    15                         | Clight.Sdowhile (Some _, _, _) -> true
    16                         | _ -> false
     13    : Clight.statement -> bool = function
     14      | Clight.Swhile (Some _, _, _) | Clight.Sfor (Some _, _, _, _, _)
     15      | Clight.Sdowhile (Some _, _, _) -> true
     16      | _ -> false
    1717
    1818let zero_sexpr = CostLabel.Sexpr(0,0)
     
    2121
    2222let 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
     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
    2828
    2929(** compose the mapping i |--> s with all labels in a statement *)
    3030let reindex_stmt i s =
    3131  let f_stmt stmt expr_res stmt_res =
    32                 match stmt, stmt_res with
    33                         | Clight.Scost(lbl, _), stmt' :: _ ->
     32    match stmt, stmt_res with
     33      | Clight.Scost(lbl, _), stmt' :: _ ->
    3434        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
     35        Clight.Scost(lbl,stmt')
     36      | _ -> ClightFold.statement_fill_subs stmt expr_res stmt_res in
    3737  ClightFold.statement2 (f_expr_reindex i s) f_stmt
    3838
     
    4242
    4343let 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
     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
    5151
    5252let 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        
     53  let f_lbl lbl = Label.Map.add lbl (fresh ()) in
     54  Label.Set.fold f_lbl lbl_set Label.Map.empty
     55
    5656let 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                
     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
    7272let 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
     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
    136136
    137137let 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
     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
    142142
    143143let 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        
     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
    149149open Languages
    150150
    151151let trans =
    152         (Clight, function (AstClight p) -> AstClight (apply p) | _ -> assert false)
    153                
     152  (Clight, function (AstClight p) -> AstClight (apply p) | _ -> assert false)
Note: See TracChangeset for help on using the changeset viewer.