# Changeset 1444

Ignore:
Timestamp:
Oct 21, 2011, 6:12:15 PM (8 years ago)
Message:
• expression simplification finished
Location:
Deliverables/D2.2/8051-indexed-labels-branch/src/common
Files:
2 edited

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

 r1433 Map.fold f m Atom.Map.empty let rec extended_gcd a = function | 0 -> (1, 0, a) | b -> let (x, y, r) = extended_gcd b (a mod b) in (y, x - (a / b) * y, r) let opt_bind (t : 'a option) (f : 'a -> 'b option) : 'b option = match t with | None -> None | Some x -> f x let rec cond_and_single c1 c2 = match c1, c2 with | Ceq h as c, Ceq k when h = k -> Some c | (Ceq h as c), Cgeq k | Cgeq k, (Ceq h as c) when h >= k -> Some c | (Ceq h as c), Cmod(a, b) | Cmod (a, b), (Ceq h as c) when h mod a = b -> Some c | (Ceq h as c), Cgeqmod(k, a, b) | Cgeqmod (k, a, b), (Ceq h as c) when h mod a = b && h >= k -> Some c | Ceq _, _ | _, Ceq _ -> None | Cgeq h, Cgeq k -> Some (Cgeq (max h k)) | 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)) | Cgeq h, Cgeqmod (k, a, b) | Cgeqmod(k, a, b), Cgeq h -> cond_and_single (Cgeq (max h k)) (Cmod(a, b)) (* special case of Chinese remainder theorem *) | Cmod (a, b), Cmod(c, d) -> let (x, y, gcd) = extended_gcd a c in if b mod gcd <> d mod gcd then None else let a_gcd = a / gcd in let lcm = a_gcd * c in let res = (b + a_gcd * x * (d - b)) mod lcm in Some (Cmod(res, lcm)) | 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))) (fun x -> cond_and_single (Cgeq k) x) | Cgeqmod (h, a, b), Cgeqmod(k, c, d) -> opt_bind (cond_and_single (Cmod(a, b)) (Cmod(c,d))) (fun x -> cond_and_single (Cgeq (max h k)) x) let cond_and s1 c2 = let f c1 s = match cond_and_single c1 c2 with | None -> s | Some c -> CondSet.add c s in CondSet.fold f s1 CondSet.empty let rec init_set f  n = if n <= 0 then CondSet.empty else CondSet.add (f (n-1)) (init_set f (n-1)) let rec cond_and_not_single c1 c2 = match c1, c2 with | Ceq h, Ceq k when h = k -> CondSet.empty | Ceq h, Cgeq k when h >= k -> CondSet.empty | Ceq h, Cmod (a, b) when h mod a = b -> CondSet.empty | Ceq h, Cgeqmod (k, a, b) when h >= k && h mod a = b -> CondSet.empty | Ceq _, _ -> CondSet.singleton c1 | Cgeq h, Ceq k when k < h -> CondSet.singleton c1 | Cgeq h, Ceq k -> (* Ceq h, Ceq (h+1), ... , Ceq (k-1), Cgeq (k+1) *) let s' = init_set (fun x -> Ceq(h + x)) (k - h) in CondSet.add (Cgeq(k+1)) s' | Cgeq h, Cgeq k -> (* if k < h init_set will correctly give an empty set, otherwise *) (* Ceq h, ... , Ceq (k - 1) *) init_set (fun x -> Ceq(h + x)) (k - h) | Cmod (a, b), Ceq k when k mod a <> b -> CondSet.singleton c1 | Cmod (a, b), Ceq k -> let s' = init_set (fun x -> Ceq(a * x + b)) (k / a) in CondSet.add (Cgeqmod(k + a, a, b)) s' | Cmod (a, b), Cgeq k -> init_set (fun x -> Ceq(a * x + b)) (k / a) | Cgeqmod(h, a, b), Ceq k when k < h || k mod a <> b -> CondSet.singleton c1 | Cgeqmod(h, a, b), Ceq k -> let h' = h - h mod a + b in let s' = init_set (fun x -> Ceq(a * x + h')) (k / a - h / a) in CondSet.add (Cgeqmod(k + a, a, b)) s' | Cgeqmod(h, a, b), Cgeq k -> let h' = h - h mod a + b in init_set (fun x -> Ceq(a * x + h')) (k / a - h / a) (* when we do not use cleverer ways, we just use cond_and_single *) | c1, (Cmod (a, b) as c2) -> let s' = CondSet.remove c2 (init_set (fun x -> Cmod(a, x)) a) in let f x s'' = match cond_and_single c1 x with | None -> s'' | Some y -> CondSet.add y s'' in CondSet.fold f s' CondSet.empty | c1, Cgeqmod (k, a, b) -> let c2 = Cmod (a, b) in let s' = CondSet.remove c2 (init_set (fun x -> Cmod(a, x)) a) in let f x s'' = match cond_and_single c1 x with | None -> s'' | Some y -> CondSet.add y s'' in let s'' = cond_and_not_single c1 (Cgeq k) in CondSet.fold f s' s'' let cond_and_not s1 c2 = let add_and_not x = CondSet.union (cond_and_not_single x c2) in CondSet.fold add_and_not s1 CondSet.empty let cond_implied_by_single c2 c1 = match c1, c2 with | c1, c2 when c1 = c2 -> true (* shortcut *) | Ceq h, Ceq k -> h = k | Ceq h, Cgeq k | Cgeq h, Cgeq k -> h >= k | Ceq h, Cmod (a, b) -> h mod a = b | Ceq h, Cgeqmod (k, a, b) -> h >= k && h mod a = b | Cmod (a, b), Cmod(c, d) | Cgeqmod(_, a, b), Cmod(c, d) -> a mod c = 0 && b mod c = d mod c | Cmod (a, b), Cgeqmod(k, c, d) -> let k' = k - k mod c + d in b >= k' && a mod c = 0 && b mod c = d mod c | Cgeqmod (h, a, b), Cgeqmod(k, c, d) -> let h' = h - h mod a + b in let k' = k - k mod c + d in h' >= k' && a mod c = 0 && b mod c = d mod c | _ -> false let cond_implies s1 c2 = CondSet.for_all (cond_implied_by_single c2) s1 let cond_neg_implied_by_single c2 c1 = match c1, c2 with | Ceq h, Ceq k -> h <> k | Ceq h, Cgeq k | Cgeq k, Ceq h -> h < k | Ceq h, Cmod (a, b) | Cmod (a, b), Ceq h -> h mod a <> b | Ceq h, Cgeqmod (k, a, b) | Cgeqmod(k, a, b), Ceq h -> h < k || h mod a <> b | Cmod (a, b), Cmod (c, d) | Cmod (a, b), Cgeqmod(_, c, d) | Cgeqmod(_, a, b), Cmod (c, d) | Cgeqmod(_, a, b), Cgeqmod(_, c, d) -> let (_, _, gcd) = extended_gcd a c in b mod gcd <> d mod gcd | _ -> false let cond_implies_neg s1 c2 = CondSet.for_all (cond_neg_implied_by_single c2) s1 (** Simplify the cost expression, removing useless conditions in it *) let remove_useless_branches = let rec simplify' conds = function | Exact k -> Exact k | Ternary (i, cond, if_true, if_false) -> ExtArray.ensure conds i; let conds_i = ExtArray.get conds i in if cond_implies conds_i cond then (simplify' conds if_true) else if cond_implies_neg conds_i cond then (simplify' conds if_false) else begin ExtArray.set conds i (cond_and conds_i cond); let if_true' = simplify' conds if_true in ExtArray.set conds i (cond_and_not conds_i cond); let if_false' = simplify' conds if_false in Ternary (i, cond, if_true', if_false') end in let conds = ExtArray.make ~buff:4 0 (CondSet.singleton (Cgeq 0)) in simplify' conds let rec remove_useless_branchings = function | Exact k -> Exact k | Ternary (i, cond, if_true, if_false) -> let if_true' = remove_useless_branchings if_true in let if_false' = remove_useless_branchings if_false in if if_true = if_false then if_true else Ternary (i, cond, if_true', if_false') let cost_expr_mapping_of_cost_mapping m = let sets = indexing_sets_from_cost_mapping m in let f at s = Atom.Map.add at (cost_mapping_ind at [] m s) in let e = cost_mapping_ind at [] m s in let e = remove_useless_branches e in let e = remove_useless_branchings e in Atom.Map.add at e in Atom.Map.fold f sets Atom.Map.empty let rec init_set f = function | 0 -> CondSet.empty | n -> CondSet.add (f (n-1)) (init_set f (n-1)) let fill_ceq = init_set (fun x -> Ceq x) let fill_mod a = init_set (fun x -> Cmod (a, x)) let fill_ceq_mod a b = init_set (fun x -> Ceq (a * x + b)) let cond_not = function | Ceq k -> CondSet.add (Cgeq (k+1)) (fill_ceq k) | Cgeq k -> fill_ceq k | Cmod (a, b) -> CondSet.remove (Cmod (a, b)) (fill_mod a a) | Cgeqmod (k, a, b) -> let non_mod = CondSet.remove (Cmod (a, b)) (fill_mod a a) in CondSet.union (fill_ceq_mod a b (k / a)) non_mod
• ## Deliverables/D2.2/8051-indexed-labels-branch/src/common/costExpr.mli

 r1433 labels into a mapping from cost atoms to cost expressions *) val cost_expr_mapping_of_cost_mapping : int Map.t -> cost_expr Atom.Map.t (** Simplify the cost expression, removing useless conditions in it *) val remove_useless_branches : cost_expr -> cost_expr
Note: See TracChangeset for help on using the changeset viewer.