Changeset 1468 for Deliverables/D2.2
- Timestamp:
- Oct 26, 2011, 7:45:42 PM (9 years ago)
- 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 84 84 end 85 85 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) 86 module F = Fix.Make (Label.ImpMap) (L) 112 87 113 88 (* 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 Languages2 3 1 (** The loop peeling transformation *) 4 val trans : transformation2 val trans : Languages.transformation -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costExpr.ml
r1444 r1468 60 60 Map.fold f m Atom.Map.empty 61 61 62 (* extended_gcd a b = (x, y, gcd(a, b)) where x*a + y*b = gcd(a, b) *) 62 63 let rec extended_gcd a = function 63 64 | 0 -> (1, 0, a) … … 71 72 | Some x -> f x 72 73 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 *) 80 let cond_and_single c1 c2 = 81 let rec cond_and_single' c1 c2 = match c1, c2 with 74 82 | Ceq h as c, Ceq k when h = k -> Some c 75 83 | (Ceq h as c), Cgeq k | Cgeq k, (Ceq h as c) when h >= k -> … … 85 93 Some (Cgeqmod(h - h mod a + b, a, b)) 86 94 | 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)) 88 96 (* special case of Chinese remainder theorem *) 89 97 | Cmod (a, b), Cmod(c, d) -> … … 95 103 Some (Cmod(res, lcm)) 96 104 | 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) 99 107 | 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) *) 103 116 let 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) } *) 110 121 let rec init_set f n = 111 122 if n <= 0 then CondSet.empty else 112 123 CondSet.add (f (n-1)) (init_set f (n-1)) 113 124 125 (* cond_and_not_single c1 c2 is equivalent to c1 && !c2 as a generalized *) 126 (* condition *) 114 127 let rec cond_and_not_single c1 c2 = 115 128 match c1, c2 with … … 126 139 | Cgeq h, Cgeq k -> 127 140 (* if k < h init_set will correctly give an empty set, otherwise *) 128 (* Ceq h, ... , Ceq (k - 1)*)141 (* {Ceq h, ... , Ceq (k - 1)} *) 129 142 init_set (fun x -> Ceq(h + x)) (k - h) 130 143 | Cmod (a, b), Ceq k when k mod a <> b -> CondSet.singleton c1 … … 146 159 | c1, (Cmod (a, b) as c2) -> 147 160 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 152 162 CondSet.fold f s' CondSet.empty 153 163 | c1, Cgeqmod (k, a, b) -> 154 164 let c2 = Cmod (a, b) in 155 165 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 160 167 let s'' = cond_and_not_single c1 (Cgeq k) in 161 168 CondSet.fold f s' s'' 162 169 170 (* generalization *) 163 171 let cond_and_not s1 c2 = 164 172 let add_and_not x = CondSet.union (cond_and_not_single x c2) in 165 173 CondSet.fold add_and_not s1 CondSet.empty 166 174 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. *) 167 177 let cond_implied_by_single c2 c1 = match c1, c2 with 168 178 | c1, c2 when c1 = c2 -> true (* shortcut *) … … 183 193 | _ -> false 184 194 195 (* cond_implies s1 c2 iff s1 => c2. Based on fact that (c1 || ... || ck) => c *) 196 (* iff c1 => c && ... && ck => c *) 185 197 let cond_implies s1 c2 = CondSet.for_all (cond_implied_by_single c2) s1 186 198 199 (* cond_neg_implied_by_single c2 c1 iff c1 => !c2 iff !(c1 && c2), which is *) 200 (* symmetric. *) 187 201 let cond_neg_implied_by_single c2 c1 = match c1, c2 with 188 202 | Ceq h, Ceq k -> h <> k … … 197 211 b mod gcd <> d mod gcd 198 212 | _ -> false 199 213 214 (* cond_implies_neg s1 c2 iff s1 => !c2 *) 200 215 let 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. *) 219 let cond_simpl s = function 220 | Cgeqmod(k, a, b) when cond_implies s (Cgeq k) -> Cmod(a, b) 221 | c -> c 201 222 202 223 (** Simplify the cost expression, removing useless conditions in it *) 203 224 let remove_useless_branches = 225 (* conds represents the info known while descending the branches *) 204 226 let rec simplify' conds = function 205 227 | Exact k -> Exact k 206 228 | 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 }) *) 207 232 ExtArray.ensure conds i; 208 233 let conds_i = ExtArray.get conds i in 234 (* if conds => cond, then we can erase the if_false branch *) 209 235 if cond_implies conds_i cond then (simplify' conds if_true) else 236 (* if conds => !cond, then we can erase if_true *) 210 237 if cond_implies_neg conds_i cond then (simplify' conds if_false) else 211 238 begin 239 let cond' = cond_simpl conds_i cond in 240 (* simplify the if_true branch knowing that cond *) 212 241 ExtArray.set conds i (cond_and conds_i cond); 213 242 let if_true' = simplify' conds if_true in 243 (* simplify the if_false branch knowing that !cond *) 214 244 ExtArray.set conds i (cond_and_not conds_i cond); 215 245 let if_false' = simplify' conds if_false in 216 Ternary (i, cond , if_true', if_false')246 Ternary (i, cond', if_true', if_false') 217 247 end in 218 248 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 15 15 val cost_expr_mapping_of_cost_mapping : int Map.t -> cost_expr Atom.Map.t 16 16 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 1 1 2 2 include StringTools 3 4 module 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 27 end 28 -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/label.mli
r486 r1468 4 4 5 5 include StringSig.S 6 7 (** Imperative label maps for use with Fix *) 8 module ImpMap : (Fix.IMPERATIVE_MAPS with type key = t) 9 -
Deliverables/D2.2/8051-indexed-labels-branch/src/options.ml
r1433 r1468 49 49 50 50 let transformations = ref [] 51 let add_transformation t () = transformations := t :: !transformations 51 let add_transformation t () = transformations := !transformations @ [t] 52 let add_transformations ts () = transformations := !transformations @ ts 52 53 let get_transformations () = !transformations 53 54 … … 88 89 " Prefix of the output files."; 89 90 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."; 92 99 93 100 (* -
Deliverables/D2.2/8051-indexed-labels-branch/src/utilities/extArray.ml
r1357 r1468 14 14 (if n < 0 || n >= v.t_length then invalid_arg "out of bounds"); 15 15 v.t_cont.(n) 16 17 16 18 17 let length v = v.t_length
Note: See TracChangeset
for help on using the changeset viewer.