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

Last change on this file since 1468 was 1468, checked in by tranquil, 9 years ago
  • implemented constant propagation
  • implementing partial redundancy elimination
File size: 10.4 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 *)
29let heads_tails_of s =
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
36            let add_tail l = IndexingSet.add (List.tl l) in
37            let s_head = IndexingSet.fold add_tail s_head IndexingSet.empty in 
38            Some (head, s_head, s_rest) 
39
40let rec cost_mapping_ind atom ind (m : int Map.t) (s : IndexingSet.t) =
41    let lbl = {name = atom; i = ind} in
42    match heads_tails_of s with
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   
62(* extended_gcd a b = (x, y, gcd(a, b)) where x*a + y*b = gcd(a, b) *) 
63let rec extended_gcd a = function
64        | 0 -> (1, 0, a)
65        | b ->
66                let (x, y, r) = extended_gcd b (a mod b) in
67          (y, x - (a / b) * y, r)
68
69let opt_bind (t : 'a option) (f : 'a -> 'b option) : 'b option =
70        match t with
71                | None -> None
72                | Some x -> f x
73
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 *)
80let cond_and_single c1 c2 = 
81        let rec cond_and_single' c1 c2 = match c1, c2 with 
82        | Ceq h as c, Ceq k when h = k -> Some c
83        | (Ceq h as c), Cgeq k | Cgeq k, (Ceq h as c) when h >= k ->
84                Some c
85        | (Ceq h as c), Cmod(a, b) | Cmod (a, b), (Ceq h as c) when h mod a = b ->
86                Some c
87        | (Ceq h as c), Cgeqmod(k, a, b) | Cgeqmod (k, a, b), (Ceq h as c)
88           when h mod a = b && h >= k -> Some c
89  | Ceq _, _ | _, Ceq _ -> None
90  | Cgeq h, Cgeq k -> Some (Cgeq (max h k))
91        | Cgeq h, Cmod (a,b) | Cmod (a,b), Cgeq h ->
92                if h <= b then Some (Cmod (a, b)) else
93                Some (Cgeqmod(h - h mod a + b, a, b))
94        | Cgeq h, Cgeqmod (k, a, b) | Cgeqmod(k, a, b), Cgeq h ->
95    cond_and_single' (Cgeq (max h k)) (Cmod(a, b))
96        (* special case of Chinese remainder theorem *)
97        | Cmod (a, b), Cmod(c, d) ->
98                let (x, y, gcd) = extended_gcd a c in
99                if b mod gcd <> d mod gcd then None else
100                let a_gcd = a / gcd in
101                let lcm = a_gcd * c in
102                let res = (b + a_gcd * x * (d - b)) mod lcm in
103                Some (Cmod(res, lcm))
104        | Cmod (a, b), Cgeqmod(k, c, d) | Cgeqmod(k, c, d), Cmod(a, b) ->
105                opt_bind (cond_and_single' (Cmod(a, b)) (Cmod(c,d)))
106                (fun x -> cond_and_single' (Cgeq k) x)
107        | Cgeqmod (h, a, b), Cgeqmod(k, c, d) ->
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) *)
116let cond_and s1 c2 =
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) } *)       
121let rec init_set f  n =
122        if n <= 0 then CondSet.empty else
123  CondSet.add (f (n-1)) (init_set f (n-1))
124
125(* cond_and_not_single c1 c2 is equivalent to c1 && !c2 as a generalized *)
126(* condition *)
127let rec cond_and_not_single c1 c2 =
128                match c1, c2 with
129                        | Ceq h, Ceq k when h = k -> CondSet.empty
130                        | Ceq h, Cgeq k when h >= k -> CondSet.empty
131                        | Ceq h, Cmod (a, b) when h mod a = b -> CondSet.empty
132                        | Ceq h, Cgeqmod (k, a, b) when h >= k && h mod a = b -> CondSet.empty
133            | Ceq _, _ -> CondSet.singleton c1
134                        | Cgeq h, Ceq k when k < h -> CondSet.singleton c1
135                        | Cgeq h, Ceq k ->
136                                (* Ceq h, Ceq (h+1), ... , Ceq (k-1), Cgeq (k+1) *)
137                                let s' = init_set (fun x -> Ceq(h + x)) (k - h) in
138                                CondSet.add (Cgeq(k+1)) s'
139                        | Cgeq h, Cgeq k ->
140                                (* if k < h init_set will correctly give an empty set, otherwise *)
141                                (* {Ceq h, ... , Ceq (k - 1)} *)
142                                init_set (fun x -> Ceq(h + x)) (k - h)
143                        | Cmod (a, b), Ceq k when k mod a <> b -> CondSet.singleton c1
144                        | Cmod (a, b), Ceq k ->
145                                let s' = init_set (fun x -> Ceq(a * x + b)) (k / a) in
146                                CondSet.add (Cgeqmod(k + a, a, b)) s'
147                        | Cmod (a, b), Cgeq k ->
148                                init_set (fun x -> Ceq(a * x + b)) (k / a)
149                        | Cgeqmod(h, a, b), Ceq k when k < h || k mod a <> b ->
150                                CondSet.singleton c1
151                        | Cgeqmod(h, a, b), Ceq k ->
152                                let h' = h - h mod a + b in
153        let s' = init_set (fun x -> Ceq(a * x + h')) (k / a - h / a) in
154                                CondSet.add (Cgeqmod(k + a, a, b)) s'
155                        | Cgeqmod(h, a, b), Cgeq k ->
156        let h' = h - h mod a + b in
157        init_set (fun x -> Ceq(a * x + h')) (k / a - h / a)
158                        (* when we do not use cleverer ways, we just use cond_and_single *)
159            | c1, (Cmod (a, b) as c2) ->
160        let s' = CondSet.remove c2 (init_set (fun x -> Cmod(a, x)) a) in
161        let f x = CondSet.union (cond_and_single c1 x) in
162        CondSet.fold f s' CondSet.empty
163            | c1, Cgeqmod (k, a, b) ->
164                                let c2 = Cmod (a, b) in
165              let s' = CondSet.remove c2 (init_set (fun x -> Cmod(a, x)) a) in
166        let f x = CondSet.union (cond_and_single c1 x) in
167                                let s'' = cond_and_not_single c1 (Cgeq k) in
168        CondSet.fold f s' s''
169
170(* generalization *)
171let cond_and_not s1 c2 =
172        let add_and_not x = CondSet.union (cond_and_not_single x c2) in
173        CondSet.fold add_and_not s1 CondSet.empty
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. *)
177let cond_implied_by_single c2 c1 = match c1, c2 with
178        | c1, c2 when c1 = c2 -> true (* shortcut *)
179        | Ceq h, Ceq k -> h = k
180        | Ceq h, Cgeq k
181        | Cgeq h, Cgeq k -> h >= k
182        | Ceq h, Cmod (a, b) -> h mod a = b
183        | Ceq h, Cgeqmod (k, a, b) -> h >= k && h mod a = b
184        | Cmod (a, b), Cmod(c, d)
185        | Cgeqmod(_, a, b), Cmod(c, d) -> a mod c = 0 && b mod c = d mod c
186        | Cmod (a, b), Cgeqmod(k, c, d) ->
187                let k' = k - k mod c + d in
188                b >= k' && a mod c = 0 && b mod c = d mod c
189        | Cgeqmod (h, a, b), Cgeqmod(k, c, d) ->
190                let h' = h - h mod a + b in
191                let k' = k - k mod c + d in
192                h' >= k' && a mod c = 0 && b mod c = d mod c
193        | _ -> false
194
195(* cond_implies s1 c2 iff s1 => c2. Based on fact that (c1 || ... || ck) => c *)
196(* iff c1 => c && ... && ck => c *)
197let cond_implies s1 c2 = CondSet.for_all (cond_implied_by_single c2) s1
198
199(* cond_neg_implied_by_single c2 c1 iff c1 => !c2 iff !(c1 && c2), which is *)
200(* symmetric. *)
201let cond_neg_implied_by_single c2 c1 = match c1, c2 with
202        | Ceq h, Ceq k -> h <> k
203        | Ceq h, Cgeq k | Cgeq k, Ceq h -> h < k
204        | Ceq h, Cmod (a, b) | Cmod (a, b), Ceq h -> h mod a <> b
205        | Ceq h, Cgeqmod (k, a, b) | Cgeqmod(k, a, b), Ceq h -> h < k || h mod a <> b
206        | Cmod (a, b), Cmod (c, d)
207        | Cmod (a, b), Cgeqmod(_, c, d)
208        | Cgeqmod(_, a, b), Cmod (c, d)
209        | Cgeqmod(_, a, b), Cgeqmod(_, c, d) ->
210                let (_, _, gcd) = extended_gcd a c in
211                b mod gcd <> d mod gcd
212        | _ -> false
213
214(* cond_implies_neg s1 c2 iff s1 => !c2 *)
215let 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. *) 
219let cond_simpl s = function
220        | Cgeqmod(k, a, b) when cond_implies s (Cgeq k) -> Cmod(a, b)
221        | c -> c
222
223(** Simplify the cost expression, removing useless conditions in it *) 
224let remove_useless_branches =
225        (* conds represents the info known while descending the branches *)
226        let rec simplify' conds = function
227                | Exact k -> Exact k
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 }) *)
232                        ExtArray.ensure conds i;
233                        let conds_i = ExtArray.get conds i in
234                        (* if conds => cond, then we can erase the if_false branch *)
235                        if cond_implies conds_i cond then (simplify' conds if_true) else
236                        (* if conds => !cond, then we can erase if_true *)
237                        if cond_implies_neg conds_i cond then (simplify' conds if_false) else
238                        begin
239                                let cond' = cond_simpl conds_i cond in
240                                (* simplify the if_true branch knowing that cond *)
241                                ExtArray.set conds i (cond_and conds_i cond);
242                                let if_true' = simplify' conds if_true in
243                                (* simplify the if_false branch knowing that !cond *)
244                                ExtArray.set conds i (cond_and_not conds_i cond);
245                                let if_false' = simplify' conds if_false in
246                                Ternary (i, cond', if_true', if_false')
247                        end in
248        let conds = ExtArray.make ~buff:4 0 (CondSet.singleton (Cgeq 0)) in
249        simplify' conds
250
251let rec remove_useless_branchings = function
252        | Exact k -> Exact k
253        | Ternary (i, cond, if_true, if_false) ->
254                let if_true' = remove_useless_branchings if_true in
255    let if_false' = remove_useless_branchings if_false in
256                if if_true = if_false then if_true else
257                Ternary (i, cond, if_true', if_false')
258
259let cost_expr_mapping_of_cost_mapping m =
260    let sets = indexing_sets_from_cost_mapping m in
261    let f at s =
262                        let e = cost_mapping_ind at [] m s in
263                        let e = remove_useless_branches e in
264                        let e = remove_useless_branchings e in
265      Atom.Map.add at e in
266    Atom.Map.fold f sets Atom.Map.empty
267       
Note: See TracBrowser for help on using the repository browser.