Changeset 1483 for Deliverables/D2.2


Ignore:
Timestamp:
Nov 2, 2011, 2:40:33 PM (8 years ago)
Author:
tranquil
Message:
  • implemented a first draft of loop unrolling
  • correced bugs in CostExpr?
Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
2 added
4 edited

Legend:

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

    r1477 r1483  
    235235
    236236module Fexprid = Fix.Make (Label.ImpMap) (Lexprid)
     237
    237238(* printing tools to debug *)
    238239
     
    409410let redundant g late isol lbl =
    410411        match expr_of g lbl with
    411                 | Some e when ExprSet.mem e (late lbl) || ExprSet.mem e (isol lbl) ->
     412                | Some e when ExprSet.mem e (isol lbl) ->
    412413                        false
    413414                | Some _ -> true
     
    461462                | BinOp (op, s, t) -> St_op2 (op, r, s, t, l)
    462463
     464let insert_after exprs redundants g freshl lbl next =
     465  let f e (next', g') =
     466    try
     467      let (tmp, _) = ExprMap.find e redundants in
     468      let opt_calc = stmt_of_expr tmp e next' in
     469      RTLabsUtilities.insert_in_between freshl g' lbl next' opt_calc
     470                with
     471                        | Not_found -> (next', g') in
     472  snd (ExprSet.fold f exprs (next, g))
     473       
     474let insert_before exprs redundants g freshl lbl stmt =
     475        let f e (stmt', g') =
     476    try
     477      let (tmp, _) = ExprMap.find e redundants in
     478                        let n_lbl = freshl () in
     479      let opt_calc = stmt_of_expr tmp e n_lbl in
     480                        let g' = Label.Map.add n_lbl stmt' g' in
     481                        let g' = Label.Map.add lbl opt_calc g' in
     482                        (opt_calc, g')
     483     with
     484                        | Not_found -> (stmt', g') in
     485  snd (ExprSet.fold f exprs (stmt, g))
     486               
    463487let store_optimal_computation (def, redundants) optimal =
    464488        (* first add the temporaries' declarations *)
     
    470494  let freshl () = Label.Gen.fresh def.f_luniverse in
    471495        let f lbl stmt g' =
    472     match RTLabsUtilities.statement_successors stmt with
    473                         | next :: rest ->
    474                                 (* I am supposing optimal expressions are only at single-successor *)
    475                                 (* nodes. To be checked. Also to be checked if putting it after the*)
    476                                 (* node changes things or not. I do that because otherwise a *)
    477                                 (* computation might find itself before the first cost_label after a*)
    478                                 (* branching, breaking well labeling *)
    479                     let f' e (next', g'') =
    480                                         assert (rest = []); (* when I am assured this must go *)
    481                                         if not (ExprMap.mem e redundants) then (next', g'') else
    482                                         let (tmp, _) = ExprMap.find e redundants in
    483           let opt_calc =
    484                                           match modified_at_stmt stmt, expr_of_stmt stmt with
    485                                                   | Some r, Some e' when e = e' ->
    486                                                                 St_op1 (Op_id, tmp, r, next')
    487                                                         | _ -> stmt_of_expr tmp e next' in
    488                                         RTLabsUtilities.insert_in_between freshl g'' lbl next' opt_calc in
    489                                 snd (ExprSet.fold f' (optimal lbl) (next, g'))
    490                         | _ -> g' in
     496                match stmt with
     497                        (* in case of cost emittance the optimal calculations are inserted *)
     498                        (* after, to preserve preciness *)
     499(*                      | St_cost (_, next) ->
     500                                insert_after (optimal lbl) redundants g' freshl lbl next *)
     501                        | _ ->
     502                                insert_before (optimal lbl) redundants g' freshl lbl stmt in
    491503        { def with f_locals = f_locals; f_graph = Label.Map.fold f g g }
    492504
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/loopPeeling.ml

    r1433 r1483  
    126126              let e_next = reindex_expr i succ_sexpr e in
    127127              (* rebuild the loop *)
    128               let loop = Clight.Sfor(Some i,Clight.Sskip, e_next, s2_next, s3_next) in
     128              let loop = Clight.Sfor(Some i, s2_first, e_next, s2_next, s3_next) in
    129129                    (* build the peeled loop *)
    130                                 let peeled = Clight.Ssequence(s2_first, loop) in
    131                     let peeled = Clight.Ssequence(s3_first, peeled) in
     130                    let peeled = Clight.Ssequence(s3_first, loop) in
    132131                    (* add the guard at the start *)
    133132                    Clight.Ssequence(s1,Clight.Sifthenelse(e_first, peeled, Clight.Sskip))
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costExpr.ml

    r1468 r1483  
    1414   
    1515let cond_of_sexpr = function
    16     | Sexpr(0, b) -> Ceq(b)
    17     | Sexpr(1, b) -> Cgeq(b)
    18     | Sexpr(a, b) when b < a -> Cmod(a, b)
     16  | Sexpr(0, b) -> Ceq(b)
     17  | Sexpr(1, b) -> Cgeq(b)
     18  | Sexpr(a, b) when b < a -> Cmod(a, b)
    1919  | Sexpr(a, b) -> Cgeqmod(b, a, b mod a)
    2020
     
    7676(* while true is given by Cgeq 0. We will call sets general conditions *)
    7777
     78let print_cond = function
     79        | Ceq i -> Printf.sprintf "== %d" i
     80        | Cgeq i -> Printf.sprintf ">= %d" i
     81        | Cmod (a, b) -> Printf.sprintf "%% %d == %d" a b
     82        | Cgeqmod (i, a, b) -> Printf.sprintf ">= %d & %% %d == %d" i a b
     83
     84let print_gen_cond gc =
     85        let f c = Printf.sprintf "%s || %s" (print_cond c) in
     86        CondSet.fold f gc "F"
     87
    7888(* cond_and_single c1 c2 gives c1 && c2 as a generalized condition. Recursion*)
    7989(* is only to re-use match cases *)
     
    91101        | Cgeq h, Cmod (a,b) | Cmod (a,b), Cgeq h ->
    92102                if h <= b then Some (Cmod (a, b)) else
    93                 Some (Cgeqmod(h - h mod a + b, a, b))
     103                Some (Cgeqmod(h - h mod a + a + b, a, b))
    94104        | Cgeq h, Cgeqmod (k, a, b) | Cgeqmod(k, a, b), Cgeq h ->
    95105    cond_and_single' (Cgeq (max h k)) (Cmod(a, b))
     
    101111                let lcm = a_gcd * c in
    102112                let res = (b + a_gcd * x * (d - b)) mod lcm in
    103                 Some (Cmod(res, lcm))
     113                Some (Cmod(lcm, res))
    104114        | Cmod (a, b), Cgeqmod(k, c, d) | Cgeqmod(k, c, d), Cmod(a, b) ->
    105115                opt_bind (cond_and_single' (Cmod(a, b)) (Cmod(c,d)))
  • Deliverables/D2.2/8051-indexed-labels-branch/src/options.ml

    r1477 r1483  
    100100    "-pre", Arg.Unit (add_transformation RedundancyElimination.trans),
    101101    " Apply partial redundancy elimination.";
     102               
     103                "-unroll-for",
     104    Arg.Int (fun i -> add_transformation (LoopUnrolling.trans ~factor:i ()) ()),
     105                " Apply loop unrolling (specifying factor).";
    102106
    103107(*
Note: See TracChangeset for help on using the changeset viewer.