Changeset 1483 for Deliverables/D2.2
- Timestamp:
- Nov 2, 2011, 2:40:33 PM (9 years ago)
- 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 235 235 236 236 module Fexprid = Fix.Make (Label.ImpMap) (Lexprid) 237 237 238 (* printing tools to debug *) 238 239 … … 409 410 let redundant g late isol lbl = 410 411 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) -> 412 413 false 413 414 | Some _ -> true … … 461 462 | BinOp (op, s, t) -> St_op2 (op, r, s, t, l) 462 463 464 let 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 474 let 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 463 487 let store_optimal_computation (def, redundants) optimal = 464 488 (* first add the temporaries' declarations *) … … 470 494 let freshl () = Label.Gen.fresh def.f_luniverse in 471 495 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 491 503 { def with f_locals = f_locals; f_graph = Label.Map.fold f g g } 492 504 -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/loopPeeling.ml
r1433 r1483 126 126 let e_next = reindex_expr i succ_sexpr e in 127 127 (* rebuild the loop *) 128 let loop = Clight.Sfor(Some i, Clight.Sskip, e_next, s2_next, s3_next) in128 let loop = Clight.Sfor(Some i, s2_first, e_next, s2_next, s3_next) in 129 129 (* 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 132 131 (* add the guard at the start *) 133 132 Clight.Ssequence(s1,Clight.Sifthenelse(e_first, peeled, Clight.Sskip)) -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costExpr.ml
r1468 r1483 14 14 15 15 let cond_of_sexpr = function 16 17 18 16 | Sexpr(0, b) -> Ceq(b) 17 | Sexpr(1, b) -> Cgeq(b) 18 | Sexpr(a, b) when b < a -> Cmod(a, b) 19 19 | Sexpr(a, b) -> Cgeqmod(b, a, b mod a) 20 20 … … 76 76 (* while true is given by Cgeq 0. We will call sets general conditions *) 77 77 78 let 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 84 let print_gen_cond gc = 85 let f c = Printf.sprintf "%s || %s" (print_cond c) in 86 CondSet.fold f gc "F" 87 78 88 (* cond_and_single c1 c2 gives c1 && c2 as a generalized condition. Recursion*) 79 89 (* is only to re-use match cases *) … … 91 101 | Cgeq h, Cmod (a,b) | Cmod (a,b), Cgeq h -> 92 102 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)) 94 104 | Cgeq h, Cgeqmod (k, a, b) | Cgeqmod(k, a, b), Cgeq h -> 95 105 cond_and_single' (Cgeq (max h k)) (Cmod(a, b)) … … 101 111 let lcm = a_gcd * c in 102 112 let res = (b + a_gcd * x * (d - b)) mod lcm in 103 Some (Cmod( res, lcm))113 Some (Cmod(lcm, res)) 104 114 | Cmod (a, b), Cgeqmod(k, c, d) | Cgeqmod(k, c, d), Cmod(a, b) -> 105 115 opt_bind (cond_and_single' (Cmod(a, b)) (Cmod(c,d))) -
Deliverables/D2.2/8051-indexed-labels-branch/src/options.ml
r1477 r1483 100 100 "-pre", Arg.Unit (add_transformation RedundancyElimination.trans), 101 101 " 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)."; 102 106 103 107 (*
Note: See TracChangeset
for help on using the changeset viewer.