Changeset 1444 for Deliverables/D2.2
 Timestamp:
 Oct 21, 2011, 6:12:15 PM (8 years ago)
 Location:
 Deliverables/D2.2/8051indexedlabelsbranch/src/common
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051indexedlabelsbranch/src/common/costExpr.ml
r1433 r1444 60 60 Map.fold f m Atom.Map.empty 61 61 62 let rec extended_gcd a = function 63  0 > (1, 0, a) 64  b > 65 let (x, y, r) = extended_gcd b (a mod b) in 66 (y, x  (a / b) * y, r) 67 68 let opt_bind (t : 'a option) (f : 'a > 'b option) : 'b option = 69 match t with 70  None > None 71  Some x > f x 72 73 let rec cond_and_single c1 c2 = match c1, c2 with 74  Ceq h as c, Ceq k when h = k > Some c 75  (Ceq h as c), Cgeq k  Cgeq k, (Ceq h as c) when h >= k > 76 Some c 77  (Ceq h as c), Cmod(a, b)  Cmod (a, b), (Ceq h as c) when h mod a = b > 78 Some c 79  (Ceq h as c), Cgeqmod(k, a, b)  Cgeqmod (k, a, b), (Ceq h as c) 80 when h mod a = b && h >= k > Some c 81  Ceq _, _  _, Ceq _ > None 82  Cgeq h, Cgeq k > Some (Cgeq (max h k)) 83  Cgeq h, Cmod (a,b)  Cmod (a,b), Cgeq h > 84 if h <= b then Some (Cmod (a, b)) else 85 Some (Cgeqmod(h  h mod a + b, a, b)) 86  Cgeq h, Cgeqmod (k, a, b)  Cgeqmod(k, a, b), Cgeq h > 87 cond_and_single (Cgeq (max h k)) (Cmod(a, b)) 88 (* special case of Chinese remainder theorem *) 89  Cmod (a, b), Cmod(c, d) > 90 let (x, y, gcd) = extended_gcd a c in 91 if b mod gcd <> d mod gcd then None else 92 let a_gcd = a / gcd in 93 let lcm = a_gcd * c in 94 let res = (b + a_gcd * x * (d  b)) mod lcm in 95 Some (Cmod(res, lcm)) 96  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) 99  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 103 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 110 let rec init_set f n = 111 if n <= 0 then CondSet.empty else 112 CondSet.add (f (n1)) (init_set f (n1)) 113 114 let rec cond_and_not_single c1 c2 = 115 match c1, c2 with 116  Ceq h, Ceq k when h = k > CondSet.empty 117  Ceq h, Cgeq k when h >= k > CondSet.empty 118  Ceq h, Cmod (a, b) when h mod a = b > CondSet.empty 119  Ceq h, Cgeqmod (k, a, b) when h >= k && h mod a = b > CondSet.empty 120  Ceq _, _ > CondSet.singleton c1 121  Cgeq h, Ceq k when k < h > CondSet.singleton c1 122  Cgeq h, Ceq k > 123 (* Ceq h, Ceq (h+1), ... , Ceq (k1), Cgeq (k+1) *) 124 let s' = init_set (fun x > Ceq(h + x)) (k  h) in 125 CondSet.add (Cgeq(k+1)) s' 126  Cgeq h, Cgeq k > 127 (* if k < h init_set will correctly give an empty set, otherwise *) 128 (* Ceq h, ... , Ceq (k  1) *) 129 init_set (fun x > Ceq(h + x)) (k  h) 130  Cmod (a, b), Ceq k when k mod a <> b > CondSet.singleton c1 131  Cmod (a, b), Ceq k > 132 let s' = init_set (fun x > Ceq(a * x + b)) (k / a) in 133 CondSet.add (Cgeqmod(k + a, a, b)) s' 134  Cmod (a, b), Cgeq k > 135 init_set (fun x > Ceq(a * x + b)) (k / a) 136  Cgeqmod(h, a, b), Ceq k when k < h  k mod a <> b > 137 CondSet.singleton c1 138  Cgeqmod(h, a, b), Ceq k > 139 let h' = h  h mod a + b in 140 let s' = init_set (fun x > Ceq(a * x + h')) (k / a  h / a) in 141 CondSet.add (Cgeqmod(k + a, a, b)) s' 142  Cgeqmod(h, a, b), Cgeq k > 143 let h' = h  h mod a + b in 144 init_set (fun x > Ceq(a * x + h')) (k / a  h / a) 145 (* when we do not use cleverer ways, we just use cond_and_single *) 146  c1, (Cmod (a, b) as c2) > 147 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 152 CondSet.fold f s' CondSet.empty 153  c1, Cgeqmod (k, a, b) > 154 let c2 = Cmod (a, b) in 155 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 160 let s'' = cond_and_not_single c1 (Cgeq k) in 161 CondSet.fold f s' s'' 162 163 let cond_and_not s1 c2 = 164 let add_and_not x = CondSet.union (cond_and_not_single x c2) in 165 CondSet.fold add_and_not s1 CondSet.empty 166 167 let cond_implied_by_single c2 c1 = match c1, c2 with 168  c1, c2 when c1 = c2 > true (* shortcut *) 169  Ceq h, Ceq k > h = k 170  Ceq h, Cgeq k 171  Cgeq h, Cgeq k > h >= k 172  Ceq h, Cmod (a, b) > h mod a = b 173  Ceq h, Cgeqmod (k, a, b) > h >= k && h mod a = b 174  Cmod (a, b), Cmod(c, d) 175  Cgeqmod(_, a, b), Cmod(c, d) > a mod c = 0 && b mod c = d mod c 176  Cmod (a, b), Cgeqmod(k, c, d) > 177 let k' = k  k mod c + d in 178 b >= k' && a mod c = 0 && b mod c = d mod c 179  Cgeqmod (h, a, b), Cgeqmod(k, c, d) > 180 let h' = h  h mod a + b in 181 let k' = k  k mod c + d in 182 h' >= k' && a mod c = 0 && b mod c = d mod c 183  _ > false 184 185 let cond_implies s1 c2 = CondSet.for_all (cond_implied_by_single c2) s1 186 187 let cond_neg_implied_by_single c2 c1 = match c1, c2 with 188  Ceq h, Ceq k > h <> k 189  Ceq h, Cgeq k  Cgeq k, Ceq h > h < k 190  Ceq h, Cmod (a, b)  Cmod (a, b), Ceq h > h mod a <> b 191  Ceq h, Cgeqmod (k, a, b)  Cgeqmod(k, a, b), Ceq h > h < k  h mod a <> b 192  Cmod (a, b), Cmod (c, d) 193  Cmod (a, b), Cgeqmod(_, c, d) 194  Cgeqmod(_, a, b), Cmod (c, d) 195  Cgeqmod(_, a, b), Cgeqmod(_, c, d) > 196 let (_, _, gcd) = extended_gcd a c in 197 b mod gcd <> d mod gcd 198  _ > false 199 200 let cond_implies_neg s1 c2 = CondSet.for_all (cond_neg_implied_by_single c2) s1 201 202 (** Simplify the cost expression, removing useless conditions in it *) 203 let remove_useless_branches = 204 let rec simplify' conds = function 205  Exact k > Exact k 206  Ternary (i, cond, if_true, if_false) > 207 ExtArray.ensure conds i; 208 let conds_i = ExtArray.get conds i in 209 if cond_implies conds_i cond then (simplify' conds if_true) else 210 if cond_implies_neg conds_i cond then (simplify' conds if_false) else 211 begin 212 ExtArray.set conds i (cond_and conds_i cond); 213 let if_true' = simplify' conds if_true in 214 ExtArray.set conds i (cond_and_not conds_i cond); 215 let if_false' = simplify' conds if_false in 216 Ternary (i, cond, if_true', if_false') 217 end in 218 let conds = ExtArray.make ~buff:4 0 (CondSet.singleton (Cgeq 0)) in 219 simplify' conds 220 221 let rec remove_useless_branchings = function 222  Exact k > Exact k 223  Ternary (i, cond, if_true, if_false) > 224 let if_true' = remove_useless_branchings if_true in 225 let if_false' = remove_useless_branchings if_false in 226 if if_true = if_false then if_true else 227 Ternary (i, cond, if_true', if_false') 228 62 229 let cost_expr_mapping_of_cost_mapping m = 63 230 let sets = indexing_sets_from_cost_mapping m in 64 231 let f at s = 65 Atom.Map.add at (cost_mapping_ind at [] m s) in 232 let e = cost_mapping_ind at [] m s in 233 let e = remove_useless_branches e in 234 let e = remove_useless_branchings e in 235 Atom.Map.add at e in 66 236 Atom.Map.fold f sets Atom.Map.empty 67 68 69 let rec init_set f = function 70  0 > CondSet.empty 71  n > CondSet.add (f (n1)) (init_set f (n1)) 72 73 let fill_ceq = init_set (fun x > Ceq x) 74 75 let fill_mod a = init_set (fun x > Cmod (a, x)) 76 77 let fill_ceq_mod a b = init_set (fun x > Ceq (a * x + b)) 78 79 let cond_not = function 80  Ceq k > 81 CondSet.add (Cgeq (k+1)) (fill_ceq k) 82  Cgeq k > fill_ceq k 83  Cmod (a, b) > CondSet.remove (Cmod (a, b)) (fill_mod a a) 84  Cgeqmod (k, a, b) > 85 let non_mod = CondSet.remove (Cmod (a, b)) (fill_mod a a) in 86 CondSet.union (fill_ceq_mod a b (k / a)) non_mod 237 
Deliverables/D2.2/8051indexedlabelsbranch/src/common/costExpr.mli
r1433 r1444 14 14 labels into a mapping from cost atoms to cost expressions *) 15 15 val cost_expr_mapping_of_cost_mapping : int Map.t > cost_expr Atom.Map.t 16 17 (** Simplify the cost expression, removing useless conditions in it *) 18 val remove_useless_branches : cost_expr > cost_expr
Note: See TracChangeset
for help on using the changeset viewer.