Changeset 1468 for Deliverables/D2.2


Ignore:
Timestamp:
Oct 26, 2011, 7:45:42 PM (8 years ago)
Author:
tranquil
Message:
  • implemented constant propagation
  • implementing partial redundancy elimination
Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
5 added
8 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/liveness.ml

    r1345 r1468  
    8484end
    8585
    86 module Label_ImperativeMap = struct
    87 
    88   type key =
    89       Label.Map.key
    90  
    91   type 'data t =
    92       'data Label.Map.t ref
    93      
    94   let create () =
    95     ref Label.Map.empty
    96 
    97   let clear t =
    98     t := Label.Map.empty
    99    
    100   let add k d t =
    101     t := Label.Map.add k d !t
    102 
    103   let find k t =
    104     Label.Map.find k !t
    105 
    106   let iter f t =
    107     Label.Map.iter f !t
    108 
    109 end
    110 
    111 module F = Fix.Make (Label_ImperativeMap) (L)
     86module F = Fix.Make (Label.ImpMap) (L)
    11287
    11388(* These are the sets of variables defined at (written by) a statement. *)

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

    r1433 r1468  
    1 open Languages
    2 
    31(** The loop peeling transformation *)
    4 val trans : transformation
     2val trans : Languages.transformation

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

    r1444 r1468  
    6060    Map.fold f m Atom.Map.empty
    6161   
     62(* extended_gcd a b = (x, y, gcd(a, b)) where x*a + y*b = gcd(a, b) *) 
    6263let rec extended_gcd a = function
    6364        | 0 -> (1, 0, a)
    … …  
    7172                | Some x -> f x
    7273
    73 let rec cond_and_single c1 c2 = match c1, c2 with
     74(* in the following a set of conditions is considered as sequents, i.e. *)
     75(* {c1, ..., ck} is considered as c1 || ... || ck. The empty set is for false,*)
     76(* while true is given by Cgeq 0. We will call sets general conditions *)
     77
     78(* cond_and_single c1 c2 gives c1 && c2 as a generalized condition. Recursion*)
     79(* is only to re-use match cases *)
     80let cond_and_single c1 c2 =
     81        let rec cond_and_single' c1 c2 = match c1, c2 with
    7482        | Ceq h as c, Ceq k when h = k -> Some c
    7583        | (Ceq h as c), Cgeq k | Cgeq k, (Ceq h as c) when h >= k ->
    … …  
    8593                Some (Cgeqmod(h - h mod a + b, a, b))
    8694        | Cgeq h, Cgeqmod (k, a, b) | Cgeqmod(k, a, b), Cgeq h ->
    87     cond_and_single (Cgeq (max h k)) (Cmod(a, b))
     95    cond_and_single' (Cgeq (max h k)) (Cmod(a, b))
    8896        (* special case of Chinese remainder theorem *)
    8997        | Cmod (a, b), Cmod(c, d) ->
    … …  
    95103                Some (Cmod(res, lcm))
    96104        | Cmod (a, b), Cgeqmod(k, c, d) | Cgeqmod(k, c, d), Cmod(a, b) ->
    97                 opt_bind (cond_and_single (Cmod(a, b)) (Cmod(c,d)))
    98                 (fun x -> cond_and_single (Cgeq k) x)
     105                opt_bind (cond_and_single' (Cmod(a, b)) (Cmod(c,d)))
     106                (fun x -> cond_and_single' (Cgeq k) x)
    99107        | Cgeqmod (h, a, b), Cgeqmod(k, c, d) ->
    100                 opt_bind (cond_and_single (Cmod(a, b)) (Cmod(c,d)))
    101                 (fun x -> cond_and_single (Cgeq (max h k)) x)
    102 
     108                opt_bind (cond_and_single' (Cmod(a, b)) (Cmod(c,d)))
     109                (fun x -> cond_and_single' (Cgeq (max h k)) x) in
     110        match cond_and_single' c1 c2 with
     111                | None -> CondSet.empty
     112                | Some x -> CondSet.singleton x
     113
     114(* this generalizes to general conditions for first argument, based on*)
     115(* (c1 || ... || ck) && c = (c1 && c || ... || ck && c) *)
    103116let cond_and s1 c2 =
    104         let f c1 s =
    105                 match cond_and_single c1 c2 with
    106                         | None -> s
    107                         | Some c -> CondSet.add c s in
    108         CondSet.fold f s1 CondSet.empty
    109        
     117        let add_and c1 = CondSet.union (cond_and_single c1 c2) in
     118        CondSet.fold add_and s1 CondSet.empty
     119
     120(* this creates the set { f 0, ..., f (n-1) } *)       
    110121let rec init_set f  n =
    111122        if n <= 0 then CondSet.empty else
    112123  CondSet.add (f (n-1)) (init_set f (n-1))
    113124
     125(* cond_and_not_single c1 c2 is equivalent to c1 && !c2 as a generalized *)
     126(* condition *)
    114127let rec cond_and_not_single c1 c2 =
    115128                match c1, c2 with
    … …  
    126139                        | Cgeq h, Cgeq k ->
    127140                                (* if k < h init_set will correctly give an empty set, otherwise *)
    128                                 (* Ceq h, ... , Ceq (k - 1) *)
     141                                (* {Ceq h, ... , Ceq (k - 1)} *)
    129142                                init_set (fun x -> Ceq(h + x)) (k - h)
    130143                        | Cmod (a, b), Ceq k when k mod a <> b -> CondSet.singleton c1
    … …  
    146159            | c1, (Cmod (a, b) as c2) ->
    147160        let s' = CondSet.remove c2 (init_set (fun x -> Cmod(a, x)) a) in
    148         let f x s'' =
    149             match cond_and_single c1 x with
    150                 | None -> s''
    151                 | Some y -> CondSet.add y s'' in
     161        let f x = CondSet.union (cond_and_single c1 x) in
    152162        CondSet.fold f s' CondSet.empty
    153163            | c1, Cgeqmod (k, a, b) ->
    154164                                let c2 = Cmod (a, b) in
    155165              let s' = CondSet.remove c2 (init_set (fun x -> Cmod(a, x)) a) in
    156         let f x s'' =
    157             match cond_and_single c1 x with
    158                 | None -> s''
    159                 | Some y -> CondSet.add y s'' in
     166        let f x = CondSet.union (cond_and_single c1 x) in
    160167                                let s'' = cond_and_not_single c1 (Cgeq k) in
    161168        CondSet.fold f s' s''
    162169
     170(* generalization *)
    163171let cond_and_not s1 c2 =
    164172        let add_and_not x = CondSet.union (cond_and_not_single x c2) in
    165173        CondSet.fold add_and_not s1 CondSet.empty
    166174
     175(* cond_implied_by_single c2 c1 gives true iff c1 => c2, i.e. if the set *)
     176(* of indexes denoted by c1 is contained in the one denoted by c2. *)
    167177let cond_implied_by_single c2 c1 = match c1, c2 with
    168178        | c1, c2 when c1 = c2 -> true (* shortcut *)
    … …  
    183193        | _ -> false
    184194
     195(* cond_implies s1 c2 iff s1 => c2. Based on fact that (c1 || ... || ck) => c *)
     196(* iff c1 => c && ... && ck => c *)
    185197let cond_implies s1 c2 = CondSet.for_all (cond_implied_by_single c2) s1
    186198
     199(* cond_neg_implied_by_single c2 c1 iff c1 => !c2 iff !(c1 && c2), which is *)
     200(* symmetric. *)
    187201let cond_neg_implied_by_single c2 c1 = match c1, c2 with
    188202        | Ceq h, Ceq k -> h <> k
    … …  
    197211                b mod gcd <> d mod gcd
    198212        | _ -> false
    199  
     213
     214(* cond_implies_neg s1 c2 iff s1 => !c2 *)
    200215let cond_implies_neg s1 c2 = CondSet.for_all (cond_neg_implied_by_single c2) s1
     216
     217(* cond_simpl s turns Cgeqmod conditions into Cmod ones, if s implies the geq *)
     218(* part. *)
     219let cond_simpl s = function
     220        | Cgeqmod(k, a, b) when cond_implies s (Cgeq k) -> Cmod(a, b)
     221        | c -> c
    201222
    202223(** Simplify the cost expression, removing useless conditions in it *)
    203224let remove_useless_branches =
     225        (* conds represents the info known while descending the branches *)
    204226        let rec simplify' conds = function
    205227                | Exact k -> Exact k
    206228                | Ternary (i, cond, if_true, if_false) ->
     229                        (* if it is the first time a condition on i is encountered, we ensure *)
     230                        (* that conds holds a default value that will be the "true" of these *)
     231                        (* conditions (i.e. { Cgeq 0 }) *)
    207232                        ExtArray.ensure conds i;
    208233                        let conds_i = ExtArray.get conds i in
     234                        (* if conds => cond, then we can erase the if_false branch *)
    209235                        if cond_implies conds_i cond then (simplify' conds if_true) else
     236                        (* if conds => !cond, then we can erase if_true *)
    210237                        if cond_implies_neg conds_i cond then (simplify' conds if_false) else
    211238                        begin
     239                                let cond' = cond_simpl conds_i cond in
     240                                (* simplify the if_true branch knowing that cond *)
    212241                                ExtArray.set conds i (cond_and conds_i cond);
    213242                                let if_true' = simplify' conds if_true in
     243                                (* simplify the if_false branch knowing that !cond *)
    214244                                ExtArray.set conds i (cond_and_not conds_i cond);
    215245                                let if_false' = simplify' conds if_false in
    216                                 Ternary (i, cond, if_true', if_false')
     246                                Ternary (i, cond', if_true', if_false')
    217247                        end in
    218248        let conds = ExtArray.make ~buff:4 0 (CondSet.singleton (Cgeq 0)) in

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

    r1444 r1468  
    1515val cost_expr_mapping_of_cost_mapping : int Map.t -> cost_expr Atom.Map.t
    1616
    17 (** Simplify the cost expression, removing useless conditions in it *)
    18 val remove_useless_branches : cost_expr -> cost_expr

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

    r486 r1468  
    11
    22include StringTools
     3
     4module ImpMap = struct
     5
     6  type key =
     7      Map.key
     8 
     9  type 'data t =
     10      'data Map.t ref
     11     
     12  let create () =
     13    ref Map.empty
     14
     15  let clear t =
     16    t := Map.empty
     17   
     18  let add k d t =
     19    t := Map.add k d !t
     20
     21  let find k t =
     22    Map.find k !t
     23
     24  let iter f t =
     25    Map.iter f !t
     26
     27end
     28

  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/label.mli

    r486 r1468  
    44
    55include StringSig.S
     6
     7(** Imperative label maps for use with Fix *)
     8module ImpMap : (Fix.IMPERATIVE_MAPS with type key = t)
     9       

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

    r1433 r1468  
    4949
    5050let transformations = ref []
    51 let add_transformation t () = transformations := t :: !transformations
     51let add_transformation t () = transformations := !transformations @ [t]
     52let add_transformations ts () = transformations := !transformations @ ts
    5253let get_transformations () = !transformations
    5354
    … …  
    8889  " Prefix of the output files.";
    8990       
    90         "-peel", Arg.Unit (add_transformation LoopPeeling.trans),
    91         " Apply loop peeling.";
     91    "-peel", Arg.Unit (add_transformation LoopPeeling.trans),
     92    " Apply loop peeling.";
     93               
     94                "-const-prop", Arg.Unit (add_transformation ConstPropagation.trans),
     95    " Apply constant propagation.";
     96
     97    "-red-elim", Arg.Unit (add_transformation RedundancyElimination.trans),
     98    " Apply partial redundancy elimination.";
    9299
    93100(*

  • Deliverables/D2.2/8051-indexed-labels-branch/src/utilities/extArray.ml

    r1357 r1468  
    1414        (if n < 0 || n >= v.t_length then invalid_arg "out of bounds");
    1515        v.t_cont.(n)
    16 
    1716
    1817let length v = v.t_length
Note: See TracChangeset for help on using the changeset viewer.