# source:Deliverables/D2.2/8051-indexed-labels-branch/src/common/costExpr.ml@1444

Last change on this file since 1444 was 1444, checked in by tranquil, 9 years ago
• expression simplification finished
File size: 8.7 KB
Line
1type cond =
2        | Ceq of int         (** index is equal to *)
3        | Cgeq of int        (** index is greater or equal to *)
4        | Cmod of int*int      (** index modulo equal to *)
5  | Cgeqmod of int*int*int (** index greater than and modulo equal to *)
6
7module CondSet = Set.Make(struct
8    type t = cond
9    let compare = compare
10end)
11
12open CostLabel
13
14
15let cond_of_sexpr = function
16    | Sexpr(0, b) -> Ceq(b)
17    | Sexpr(1, b) -> Cgeq(b)
18    | Sexpr(a, b) when b < a -> Cmod(a, b)
19  | Sexpr(a, b) -> Cgeqmod(b, a, b mod a)
20
21type cost_expr =
22    | Exact of int
23    | Ternary of index * cond * cost_expr * cost_expr
24
25(* compute from the set [s] a the 3-uple [Some (h, s_h, s_rest)] where *)
26(* [h] is the head of first elements of [s], and [s] is the union of *)
27(* [{h :: tl | tl in s_h}] and [s_rest]. Gives [None] if either [s] is empty *)
28(* or it starts with an empty list. ([s] should contain lists with same length *)
30    if IndexingSet.is_empty s then None else
31    match IndexingSet.min_elt s with
32        | [] -> None
33        | head :: _ ->
34            let filter x = (List.hd x = head) in
35            let (s_head, s_rest) = IndexingSet.partition filter s in
39
40let rec cost_mapping_ind atom ind (m : int Map.t) (s : IndexingSet.t) =
41    let lbl = {name = atom; i = ind} in
43        | None when Map.mem lbl m-> Exact (Map.find lbl m)
44        | None -> Exact 0
45        | Some(h, s_head, s_rest) ->
46            let i = List.length ind in
47            let condition = cond_of_sexpr h in
48            let if_true = cost_mapping_ind atom (h :: ind) m s_head in
49            let if_false = cost_mapping_ind atom ind m s_rest in
50            Ternary(i, condition, if_true, if_false)
51
52let indexing_sets_from_cost_mapping m =
53    let f k _ sets =
54        let s =
55            try
56                IndexingSet.add k.i (Atom.Map.find k.name sets)
57            with
58                | Not_found -> IndexingSet.singleton k.i in
59        Atom.Map.add k.name s sets in
60    Map.fold f m Atom.Map.empty
61
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
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
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
229let cost_expr_mapping_of_cost_mapping m =
230    let sets = indexing_sets_from_cost_mapping m in
231    let f at s =
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