Ignore:
Timestamp:
Nov 15, 2011, 5:11:19 PM (9 years ago)
Author:
tranquil
Message:
  • added an option to not use ternary expressions in costs, to accomodate frama-c explosion of such expressions
  • corrected some typos in comments
  • added a check for well behaved for loops in loop unrolling, but intelligent unrolling is not done yet
  • TODO: peeling and unrolling can contradict preciseness (with difference between introduced branches around 2 cycles). I guess it can be corrected easily
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/loopUnrolling.ml

    r1483 r1507  
    88
    99let big_union : IdentSet.t list -> IdentSet.t =
    10         List.fold_left IdentSet.union IdentSet.empty
     10  List.fold_left IdentSet.union IdentSet.empty
    1111
    1212let referenced : statement -> IdentSet.t =
    1313  let f_expr e res_list =
    14                 let res = big_union res_list in
     14    let res = big_union res_list in
    1515    let Expr(ed, _) = e in
    1616    match ed with
    17         | Eaddrof (Expr(Evar x, _)) -> IdentSet.add x res
    18         | _ -> res in
     17      | Eaddrof (Expr(Evar x, _)) -> IdentSet.add x res
     18      | _ -> res in
    1919  let f_stmt stmt eres sres =
    20                 IdentSet.union (big_union eres) (big_union sres) in
     20    IdentSet.union (big_union eres) (big_union sres) in
    2121  ClightFold.statement2 f_expr f_stmt
    2222
    2323let mk_heuristic_global_info (max_factor : int) (p : program)
    2424    : 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)
     25  let f set ((id, _), _) = IdentSet.add id set in
     26  (max_factor, List.fold_left f IdentSet.empty p.prog_vars)
    2727
    2828let mk_heuristic_local_info (f : cfunction) =   referenced f.fn_body
    2929
    3030let vars_of_expr, vars_of_stmt =
    31         let f_expr e res_list =
    32                 let res = big_union res_list in
     31  let f_expr e res_list =
     32    let res = big_union res_list in
    3333    let Expr(ed, _) = e in
    3434    match ed with
    35             | Evar x -> IdentSet.add x res
    36             | _ -> res in
     35      | Evar x -> IdentSet.add x res
     36      | _ -> res in
    3737  let f_stmt stmt eres sres =
    3838    IdentSet.union (big_union eres) (big_union sres) in
     
    4040
    4141let changed_in =
    42         let f_expr e _ = () in
     42  let f_expr e _ = () in
    4343  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
     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
     54type sign =
     55  | Plus
     56  | Minus
     57
     58let find_increment = function
     59  | Sassign(
     60    Expr(Evar x,_),
     61    Expr(
     62      (Ebinop(Oadd,Expr(Evar y,_),inc) |
     63          Ebinop(Oadd,inc,Expr(Evar y,_)) ),_))
     64      when x = y -> Some (x, Plus, inc)
     65  | Sassign(
     66    Expr(Evar x,_),
     67    Expr(
     68      (Ebinop(Osub,Expr(Evar y,_),inc) |
     69          Ebinop(Osub,inc,Expr(Evar y,_)) ),_))
     70      when x = y -> Some (x, Minus, inc)
     71  | _ -> None
     72
     73let find_bound s x (Expr(ed, _)) = match s, ed with
     74  | Plus, Ebinop(Olt,Expr(Evar y,_),b)
     75  | Plus, Ebinop(Ogt,b,Expr(Evar y,_))
     76  | Minus, Ebinop(Olt,b,Expr(Evar y,_))
     77  | Minus, Ebinop(Ogt,Expr(Evar y,_),b)
     78    when y = x -> Some (false, b)
     79  | Plus, Ebinop(Ole,Expr(Evar y,_),b)
     80  | Plus, Ebinop(Oge,b,Expr(Evar y,_))
     81  | Minus, Ebinop(Ole,b,Expr(Evar y,_))
     82  | Minus, Ebinop(Oge,Expr(Evar y,_),b)
     83    when y = x -> Some (true, b)
     84  | _ -> None
    5385
    5486(* this function tells when to perform the optimization on a statement. It *)
    55 (* should always return [false] when the optimization cannot be applied *) 
     87(* should always return [false] when the optimization cannot be applied *)
    5688let heuristics
    5789    ((max_factor, global_vars) : heuristic_global_info)
    5890    (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
     91    : Clight.statement -> (int * AST.ident * sign * expr * expr * bool) option =
     92  let global_referenced = IdentSet.union global_vars rfrncd_vars in
     93  function
     94    | Clight.Sfor (Some _, init, guard, tail, body) ->
     95      begin
     96        match find_increment tail with
     97          | Some (x, dir, inc) ->
     98            begin
     99              match find_bound dir x guard with
     100                | Some (included, bound) ->
     101                  let head_vars =
     102                    IdentSet.union (vars_of_expr guard) (vars_of_stmt tail) in
     103                  let dangerous =
     104                    IdentSet.union (changed_in body) global_referenced in
     105                  if IdentSet.is_empty (IdentSet.inter head_vars dangerous) then
     106                    Some (max_factor, x, dir, inc, bound, included)
     107                  else
     108                    None
     109                | None -> None
     110            end
     111          | None -> None
     112      end
     113    (* TODO add a check for size *)
     114    | _ -> None
    75115
    76116let sexpr a b = CostLabel.Sexpr(a,b)
     
    85125      | _ -> ClightFold.expr_fill_exprs e expr_res in
    86126  let f_stmt i s stmt expr_res stmt_res =
    87                 match stmt, stmt_res with
    88                         | Clight.Scost(lbl, _), stmt' :: _ ->
     127    match stmt, stmt_res with
     128      | Clight.Scost(lbl, _), stmt' :: _ ->
    89129        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)),
     130        Clight.Scost(lbl,stmt')
     131      | _ -> ClightFold.statement_fill_subs stmt expr_res stmt_res in
     132  (fun i s -> ClightFold.expr2 (f_expr i s)),
    93133  (fun i s -> ClightFold.statement2 (f_expr i s) (f_stmt i s))
    94134
    95135let 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
     136  let f_expr _ _ = () in
     137  let f_stmt stmt _ res_stmts =
     138    let s = match stmt with
     139      | Clight.Slabel(lbl, _) -> Label.Set.singleton lbl
     140      | _ -> Label.Set.empty in
     141    List.fold_left Label.Set.union s res_stmts in
     142  ClightFold.statement2 f_expr f_stmt
    103143
    104144let 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        
     145  let f_lbl lbl = Label.Map.add lbl (fresh ()) in
     146  Label.Set.fold f_lbl lbl_set Label.Map.empty
     147
    108148let apply_label_map map =
    109         let f_stmt stmt exprs stmts =
    110                 match stmt, stmts with
    111                         | Clight.Slabel (lbl, _), s :: _ ->
     149  let f_stmt stmt exprs stmts =
     150    match stmt, stmts with
     151      | Clight.Slabel (lbl, _), s :: _ ->
    112152                                (* 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 *)   
     153        Clight.Slabel (Label.Map.find lbl map, s)
     154      | Clight.Sgoto lbl, _ ->
     155        Clight.Sgoto (
     156          try
     157            Label.Map.find lbl map
     158          with
     159            | Not_found -> (* means it is an outgoing goto *)
     160              lbl)
     161      | _ -> ClightFold.statement_fill_subs stmt exprs stmts in
     162  ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
     163
     164(* unroll the k-th copy over a total of n *)
    125165let 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)))
     166  if k = 0 then reindex_stmt i (sexpr n 0) sb else
     167    let preamble = do_the_unrolling fresh (k-1) n i e sb st labels_of_sb in
     168    let st_pre = reindex_stmt i (sexpr n (k-1)) st in
     169    let e_next = reindex_expr i (sexpr n k) e in
     170    let sb_next = apply_label_map (create_fresh_labels fresh labels_of_sb) sb in
     171    let sb_next = reindex_stmt i (sexpr n k) sb_next in
     172    Ssequence(preamble,
     173              Ssequence(st_pre,
     174                        Ssequence(Sifthenelse(e_next, Sskip, Sbreak),
     175                                  sb_next)))
    136176
    137177let 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
     178  let f_stmt stmt exprs stmts =
     179    match heuristics g_info l_info stmt, stmt, exprs, stmts with
     180      | Some (k, x, dir, inc, bound, included),
     181    Clight.Sfor (Some i, _, _, _, _), e :: _, si :: st :: sb ::_ ->
     182      (* we can suppose no label in s3 is target of a goto outside of stmt, *)
     183      (* as loop is indexed and thus single entry. So we can freely rename *)
     184      (* labels in stmt. *)
     185      (* IMPORTANT: I am supposing no labels are in s1 and s2 *)
     186      let labels_of_sb = labels_of sb in
     187      let e_first = reindex_expr i (sexpr k 0) e in
     188      let st_last = reindex_stmt i (sexpr k (k-1)) st in
     189      let body = do_the_unrolling fresh (k-1) k i e sb st labels_of_sb in
     190      Sfor (Some i, si, e_first, st_last, body)
     191      | Some _, _, _, _ ->
     192        assert false (* heuristics should have crossed out other cases *)
     193      | _ -> ClightFold.statement_fill_subs stmt exprs stmts in
     194  ClightFold.statement2 ClightFold.expr_fill_exprs f_stmt
    154195
    155196let 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
     197  | (id, Clight.Internal def) ->
     198    let l_info = mk_heuristic_local_info def in
     199    let body = unroll fresh g_info l_info def.Clight.fn_body in
     200    (id, Clight.Internal {def with Clight.fn_body = body})
     201  | f -> f
    161202
    162203open Languages
    163204
    164205let 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
     206  | AstClight p ->
     207    let g_info = mk_heuristic_global_info factor p in
     208    let fresh = ClightAnnotator.make_fresh "_l" p in
    168209    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                
     210    AstClight { p with Clight.prog_funct = functs }
     211  | _ -> assert false
Note: See TracChangeset for help on using the changeset viewer.