Changeset 1444 for Deliverables/D2.2


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

Legend:

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

    r1433 r1444  
    6060    Map.fold f m Atom.Map.empty
    6161   
     62let 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
     68let opt_bind (t : 'a option) (f : 'a -> 'b option) : 'b option =
     69        match t with
     70                | None -> None
     71                | Some x -> f x
     72
     73let 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
     103let 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       
     110let rec init_set f  n =
     111        if n <= 0 then CondSet.empty else
     112  CondSet.add (f (n-1)) (init_set f (n-1))
     113
     114let 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 (k-1), 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
     163let 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
     167let 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
     185let cond_implies s1 c2 = CondSet.for_all (cond_implied_by_single c2) s1
     186
     187let 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 
     200let 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 *)
     203let 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
     221let 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
    62229let cost_expr_mapping_of_cost_mapping m =
    63230    let sets = indexing_sets_from_cost_mapping m in
    64231    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
    66236    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 (n-1)) (init_set f (n-1))
    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/8051-indexed-labels-branch/src/common/costExpr.mli

    r1433 r1444  
    1414    labels into a mapping from cost atoms to cost expressions *)
    1515val 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 *)
     18val remove_useless_branches : cost_expr -> cost_expr
Note: See TracChangeset for help on using the changeset viewer.