Changeset 1483 for Deliverables/D2.2

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:

• RTLabs/redundancyElimination.ml (modified) (4 diffs)
• clight/loopPeeling.ml (modified) (1 diff)
• clight/loopUnrolling.ml (added)
• clight/loopUnrolling.mli (added)
• common/costExpr.ml (modified) (4 diffs)
• options.ml (modified) (1 diff)

Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/redundancyElimination.ml

@@ -235 +235 @@
 
 module Fexprid = Fix.Make (Label.ImpMap) (Lexprid)
+
 (* printing tools to debug *)
 
@@ -409 +410 @@
 let redundant g late isol lbl =
         match expr_of g lbl with
-                | Some e when ExprSet.mem e (late lbl) || ExprSet.mem e (isol lbl) ->
+                | Some e when ExprSet.mem e (isol lbl) ->
                         false
                 | Some _ -> true
@@ -461 +462 @@
                 | BinOp (op, s, t) -> St_op2 (op, r, s, t, l)
 
+let insert_after exprs redundants g freshl lbl next =
+  let f e (next', g') =
+    try 
+      let (tmp, _) = ExprMap.find e redundants in
+      let opt_calc = stmt_of_expr tmp e next' in
+      RTLabsUtilities.insert_in_between freshl g' lbl next' opt_calc
+                with
+                        | Not_found -> (next', g') in
+  snd (ExprSet.fold f exprs (next, g))
+        
+let insert_before exprs redundants g freshl lbl stmt =
+        let f e (stmt', g') =
+    try 
+      let (tmp, _) = ExprMap.find e redundants in
+                        let n_lbl = freshl () in
+      let opt_calc = stmt_of_expr tmp e n_lbl in
+                        let g' = Label.Map.add n_lbl stmt' g' in
+                        let g' = Label.Map.add lbl opt_calc g' in
+                        (opt_calc, g')
+     with
+                        | Not_found -> (stmt', g') in
+  snd (ExprSet.fold f exprs (stmt, g))
+                
 let store_optimal_computation (def, redundants) optimal =
         (* first add the temporaries' declarations *)
@@ -470 +494 @@
   let freshl () = Label.Gen.fresh def.f_luniverse in
         let f lbl stmt g' =
-    match RTLabsUtilities.statement_successors stmt with
-                        | next :: rest ->
-                                (* I am supposing optimal expressions are only at single-successor *)
-                                (* nodes. To be checked. Also to be checked if putting it after the*)
-                                (* node changes things or not. I do that because otherwise a *)
-                                (* computation might find itself before the first cost_label after a*)
-                                (* branching, breaking well labeling *)
-                    let f' e (next', g'') =
-                                        assert (rest = []); (* when I am assured this must go *)
-                                        if not (ExprMap.mem e redundants) then (next', g'') else
-                                        let (tmp, _) = ExprMap.find e redundants in
-          let opt_calc = 
-                                          match modified_at_stmt stmt, expr_of_stmt stmt with
-                                                  | Some r, Some e' when e = e' ->
-                                                                St_op1 (Op_id, tmp, r, next')
-                                                        | _ -> stmt_of_expr tmp e next' in
-                                        RTLabsUtilities.insert_in_between freshl g'' lbl next' opt_calc in
-                                snd (ExprSet.fold f' (optimal lbl) (next, g'))
-                        | _ -> g' in
+                match stmt with
+                        (* in case of cost emittance the optimal calculations are inserted *)
+                        (* after, to preserve preciness *)
+(*                      | St_cost (_, next) ->
+                                insert_after (optimal lbl) redundants g' freshl lbl next *)
+                        | _ ->
+                                insert_before (optimal lbl) redundants g' freshl lbl stmt in
         { def with f_locals = f_locals; f_graph = Label.Map.fold f g g }
 

Deliverables/D2.2/8051-indexed-labels-branch/src/clight/loopPeeling.ml

@@ -126 +126 @@
               let e_next = reindex_expr i succ_sexpr e in
               (* rebuild the loop *)
-              let loop = Clight.Sfor(Some i,Clight.Sskip, e_next, s2_next, s3_next) in
+              let loop = Clight.Sfor(Some i, s2_first, e_next, s2_next, s3_next) in
                     (* build the peeled loop *)
-                                let peeled = Clight.Ssequence(s2_first, loop) in
-                    let peeled = Clight.Ssequence(s3_first, peeled) in
+                    let peeled = Clight.Ssequence(s3_first, loop) in
                     (* add the guard at the start *)
                     Clight.Ssequence(s1,Clight.Sifthenelse(e_first, peeled, Clight.Sskip))

Deliverables/D2.2/8051-indexed-labels-branch/src/common/costExpr.ml

@@ -14 +14 @@
     
 let cond_of_sexpr = function
-    | Sexpr(0, b) -> Ceq(b)
-    | Sexpr(1, b) -> Cgeq(b)
-    | Sexpr(a, b) when b < a -> Cmod(a, b)
+  | Sexpr(0, b) -> Ceq(b)
+  | Sexpr(1, b) -> Cgeq(b)
+  | Sexpr(a, b) when b < a -> Cmod(a, b)
   | Sexpr(a, b) -> Cgeqmod(b, a, b mod a)
 
@@ -76 +76 @@
 (* while true is given by Cgeq 0. We will call sets general conditions *)
 
+let print_cond = function
+        | Ceq i -> Printf.sprintf "== %d" i
+        | Cgeq i -> Printf.sprintf ">= %d" i
+        | Cmod (a, b) -> Printf.sprintf "%% %d == %d" a b
+        | Cgeqmod (i, a, b) -> Printf.sprintf ">= %d & %% %d == %d" i a b
+
+let print_gen_cond gc =
+        let f c = Printf.sprintf "%s || %s" (print_cond c) in
+        CondSet.fold f gc "F"
+
 (* cond_and_single c1 c2 gives c1 && c2 as a generalized condition. Recursion*)
 (* is only to re-use match cases *)
@@ -91 +101 @@
         | Cgeq h, Cmod (a,b) | Cmod (a,b), Cgeq h ->
                 if h <= b then Some (Cmod (a, b)) else
-                Some (Cgeqmod(h - h mod a + b, a, b))
+                Some (Cgeqmod(h - h mod a + a + b, a, b))
         | Cgeq h, Cgeqmod (k, a, b) | Cgeqmod(k, a, b), Cgeq h ->
     cond_and_single' (Cgeq (max h k)) (Cmod(a, b))
@@ -101 +111 @@
                 let lcm = a_gcd * c in
                 let res = (b + a_gcd * x * (d - b)) mod lcm in
-                Some (Cmod(res, lcm))
+                Some (Cmod(lcm, res))
         | Cmod (a, b), Cgeqmod(k, c, d) | Cgeqmod(k, c, d), Cmod(a, b) ->
                 opt_bind (cond_and_single' (Cmod(a, b)) (Cmod(c,d)))

Deliverables/D2.2/8051-indexed-labels-branch/src/options.ml

@@ -100 +100 @@
     "-pre", Arg.Unit (add_transformation RedundancyElimination.trans),
     " Apply partial redundancy elimination.";
+                
+                "-unroll-for",
+    Arg.Int (fun i -> add_transformation (LoopUnrolling.trans ~factor:i ()) ()),
+                " Apply loop unrolling (specifying factor).";
 
 (*