source: Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml @ 1349

Last change on this file since 1349 was 1349, checked in by tranquil, 9 years ago
  • work on LIN completed
  • small implementation of extensible arrays
File size: 12.2 KB
Line 
1
2(** This module defines the labelling of a [Clight] program. *)
3
4module IntListSet = Set.Make(struct type t = int list let compare = compare end)
5
6open Clight
7open CostLabel
8
9
10(* Add a cost label in front of a statement with the current indexing. *)
11
12let add_starting_cost_label indexing cost_universe stmt =
13  Clight.Scost (CostLabel.fresh indexing cost_universe, stmt)
14
15(* Add a cost label at the end of a statement. *)
16
17let add_ending_cost_label indexing cost_universe stmt =
18        let lbld_skip = add_starting_cost_label indexing cost_universe Clight.Sskip in
19  Clight.Ssequence (stmt, lbld_skip)
20
21
22let int_type = Tint (I32, AST.Signed)
23let const_int i = Expr (Econst_int i, int_type)
24
25
26let typeof e = let Expr (_,t) = e in t
27
28
29let add_cost_label_e indexing cost_universe e =
30  Expr (Ecost (CostLabel.fresh indexing cost_universe, e), typeof e)
31
32
33(* Add cost labels to an expression. *)
34
35let rec add_cost_labels_e ind cost_universe = function 
36  | Expr (exp,cty) -> Expr (add_cost_labels_expr ind cost_universe exp,cty)
37
38and add_cost_labels_expr ind cost_universe exp = match exp with
39  | Econst_int _ | Econst_float _ | Evar _ | Esizeof _ -> exp
40  | Ederef e -> Ederef (add_cost_labels_e ind cost_universe e)
41  | Eaddrof e -> Eaddrof (add_cost_labels_e ind cost_universe e)
42  | Eunop (op,e) -> Eunop (op,(add_cost_labels_e ind cost_universe e))
43  | Ebinop (op,e1,e2) ->
44      Ebinop (op,
45              add_cost_labels_e ind cost_universe e1,
46              add_cost_labels_e ind cost_universe e2)
47  | Ecast (t,e) -> Ecast (t, add_cost_labels_e ind cost_universe e)
48  | Eandbool (e1,e2) ->
49      let e1' = add_cost_labels_e ind cost_universe e1 in
50      let e2' = add_cost_labels_e ind cost_universe e2 in
51      let b1 = add_cost_label_e ind cost_universe (const_int 1) in
52      let b2 = add_cost_label_e ind cost_universe (const_int 0) in
53      let e2' = Expr (Econdition (e2', b1, b2), int_type) in
54      let e2' = add_cost_label_e ind cost_universe e2' in
55      let e3' = add_cost_label_e ind cost_universe (const_int 0) in
56      Econdition (e1', e2', e3')
57  | Eorbool (e1,e2) ->
58      let e1' = add_cost_labels_e ind cost_universe e1 in
59      let e2' = add_cost_label_e ind cost_universe (const_int 1) in
60      let e3' = add_cost_labels_e ind cost_universe e2 in
61      let b1 = add_cost_label_e ind cost_universe (const_int 1) in
62      let b2 = add_cost_label_e ind cost_universe (const_int 0) in
63      let e3' = Expr (Econdition (e3', b1, b2), int_type) in
64      let e3' = add_cost_label_e ind cost_universe e3' in
65      Econdition (e1', e2', e3')
66  | Efield (e,id) -> Efield (add_cost_labels_e ind cost_universe e,id)
67  | Econdition (e1,e2,e3) ->
68      let e1' = add_cost_labels_e ind cost_universe e1 in
69      let e2' = add_cost_labels_e ind cost_universe e2 in
70      let e2' = add_cost_label_e ind cost_universe e2' in
71      let e3' = add_cost_labels_e ind cost_universe e3 in
72      let e3' = add_cost_label_e ind cost_universe e3' in
73      Econdition (e1', e2', e3')
74  | Ecost (_,_) | Ecall _ -> assert false (* Should not happen *)
75
76let add_cost_labels_opt ind cost_universe =
77        Option.map (add_cost_labels_e ind cost_universe) 
78
79let add_cost_labels_lst ind cost_universe l =
80  List.map (add_cost_labels_e ind cost_universe) l
81
82
83(* Add cost labels to a statement. *)
84
85let rec add_cost_labels_st ind cost_universe = function
86  | Sskip -> Sskip
87  | Sassign (e1,e2) ->
88      Sassign (add_cost_labels_e ind cost_universe e1,
89               add_cost_labels_e ind cost_universe e2)
90  | Scall (e1,e2,lst) ->
91      Scall (add_cost_labels_opt ind cost_universe e1,
92             add_cost_labels_e ind cost_universe e2,
93             add_cost_labels_lst ind cost_universe lst)
94  | Ssequence (s1,s2) ->
95      Ssequence (add_cost_labels_st ind cost_universe s1,
96                 add_cost_labels_st ind cost_universe s2) 
97  | Sifthenelse (e,s1,s2) ->
98      let s1' = add_cost_labels_st ind cost_universe s1 in
99      let s1' = add_starting_cost_label ind cost_universe s1' in
100      let s2' = add_cost_labels_st ind cost_universe s2 in
101      let s2' = add_starting_cost_label ind cost_universe s2' in
102      Sifthenelse (add_cost_labels_e ind cost_universe e, s1', s2')
103  | Swhile (i,e,s) ->
104                  let ind' = match i with
105                                | None -> ind
106                                | Some _ -> CostLabel.add_id_indexing ind in
107      let s' = add_cost_labels_st ind' cost_universe s in
108      let s' = add_starting_cost_label ind' cost_universe s' in
109                        (* exit label indexed with outside indexing *) 
110      add_ending_cost_label ind cost_universe
111        (Swhile (i,add_cost_labels_e ind cost_universe e, s'))
112  | Sdowhile (i,e,s) ->
113      let ind' = match i with
114        | None -> ind
115        | Some _ -> CostLabel.add_id_indexing ind in
116      let s' = add_cost_labels_st ind' cost_universe s in
117      let s' = add_starting_cost_label ind' cost_universe s' in
118      add_ending_cost_label ind cost_universe
119        (Sdowhile (i,add_cost_labels_e ind cost_universe e, s'))
120  | Sfor (i,s1,e,s2,s3) ->
121      let s1' = add_cost_labels_st ind cost_universe s1 in
122      let ind' = match i with
123        | None -> ind
124        | Some _ -> CostLabel.add_id_indexing ind in
125      let s2' = add_cost_labels_st ind' cost_universe s2 in
126      let s3' = add_cost_labels_st ind' cost_universe s3 in
127      let s3' = add_starting_cost_label ind' cost_universe s3' in
128      add_ending_cost_label ind cost_universe
129        (Sfor (i, s1', add_cost_labels_e ind cost_universe e, s2', s3'))
130  | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e)
131  | Sswitch (e,ls) ->
132      Sswitch (add_cost_labels_e ind cost_universe e,
133               add_cost_labels_ls ind cost_universe ls)
134  | Slabel (lbl,s) ->
135      let s' = add_cost_labels_st ind cost_universe s in
136      let s' = add_starting_cost_label ind cost_universe s' in
137      Slabel (lbl,s')
138  | Scost (_,_) -> assert false
139  | _ as stmt -> stmt
140
141and add_cost_labels_ls ind cost_universe = function
142  | LSdefault s ->
143      let s' = add_cost_labels_st ind cost_universe s in
144      let s' = add_starting_cost_label ind cost_universe s' in
145      LSdefault s'
146  | LScase (i,s,ls) ->
147      let s' = add_cost_labels_st ind cost_universe s in
148      let s' = add_starting_cost_label ind cost_universe s' in
149      LScase (i, s', add_cost_labels_ls ind cost_universe ls)
150
151
152(* traversal of code assigning to every label the "loop address" of it. *)
153(* A loop address like [2, 0, 1] means the corresponding label is in the *)
154(* third loop inside the first loop inside the second loop of the body. The *)
155let rec assign_loop_addrs_s
156    (current : int list)
157                (offset  : int)
158                (m       : int list Label.Map.t)
159                : Clight.statement -> int*int list Label.Map.t = function
160        (* I am supposing you cannot jump to the update statement of for loops... *)
161        | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
162                let (_, m) = assign_loop_addrs_s (offset :: current) 0 m s in
163                (offset + 1, m)
164        | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
165                let (offset, m) = assign_loop_addrs_s current offset m s1 in
166                assign_loop_addrs_s current offset m s2
167        | Slabel(l,s) ->
168                let (offset, m) = assign_loop_addrs_s current offset m s in
169                (offset, Label.Map.add l current m)
170        | Sswitch(_,ls) -> assign_loop_addrs_ls current offset m ls
171        | _ -> (offset, m)
172
173and assign_loop_addrs_ls current offset m = function
174  | LSdefault s -> assign_loop_addrs_s current offset m s
175  | LScase(_,s,ls) ->
176                let (offset, m) = assign_loop_addrs_s current offset m s in
177                assign_loop_addrs_ls current offset m ls
178
179let rec is_prefix l1 l2 = match l1, l2 with
180        | [], _ -> true
181        | hd1 :: tl1, hd2 :: tl2 when hd1 = hd2 -> is_prefix tl1 tl2
182        | _ -> false
183
184(* traversal of code which for every statement [s] returns the set of loop*)
185(* addresses which are multi-entry due to a goto in [s]. *)
186let rec find_multi_entry_loops_s
187    (m       : int list Label.Map.t)
188                (current : int list)
189                (offset  : int)
190                : Clight.statement -> int*IntListSet.t = function
191        (* I am supposing you cannot jump to the update statement of for loops... *)
192        | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
193                        let current' = offset :: current in
194                        let (_, set) = find_multi_entry_loops_s m current' 0 s in
195                        (offset + 1, set)
196        | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
197          let (offset, set1) = find_multi_entry_loops_s m current offset s1 in
198          let (offset, set2) = find_multi_entry_loops_s m current offset s2 in
199          (offset, IntListSet.union set1 set2)
200        | Slabel(_,s) -> find_multi_entry_loops_s m current offset s
201                | Sgoto l ->
202                        (* all labels should have a binding in m *)
203                        let addr = Label.Map.find l m in
204                        let cond = is_prefix addr current in
205                        let set = if cond then IntListSet.empty else IntListSet.singleton addr in
206                        (offset, set)   
207        | Sswitch(_,ls) -> find_multi_entry_loops_ls m current offset ls
208        | _ -> (offset, IntListSet.empty)
209
210and find_multi_entry_loops_ls m current offset = function
211  | LSdefault s -> find_multi_entry_loops_s m current offset s
212  | LScase(_,s,ls) ->
213    let (offset, set1) = find_multi_entry_loops_s m current offset s in
214    let (offset, set2) = find_multi_entry_loops_ls m current offset ls in
215    (offset, IntListSet.union set1 set2)
216                               
217(* final pass where loops are indexed *)
218let rec index_loops_s multi_entry current offset depth = function
219        (* I am supposing you cannot jump to the update statement of for loops... *)
220        | Swhile(_,b,s) ->
221    let current' = offset :: current in
222                let is_bad = IntListSet.mem current' multi_entry in 
223                let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
224          let (_, s) = index_loops_s multi_entry current' 0 depth s in 
225          (offset + 1, Swhile(i,b,s))
226        | Sdowhile(_,b,s) ->
227    let current' = offset :: current in
228    let is_bad = IntListSet.mem current' multi_entry in 
229    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
230          let (_, s) = index_loops_s multi_entry current' 0 depth s in 
231          (offset + 1, Sdowhile(i,b,s))
232        | Sfor(_,a1,a2,a3,s) ->
233    let current' = offset :: current in
234    let is_bad = IntListSet.mem current' multi_entry in 
235    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
236          let (_, s) = index_loops_s multi_entry current' 0 depth s in 
237          (offset + 1, Sfor(i,a1,a2,a3,s))
238        | Ssequence(s1,s2) ->
239          let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
240          let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
241          (offset, Ssequence(s1,s2))
242        | Sifthenelse(b,s1,s2) ->
243          let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
244          let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
245          (offset, Sifthenelse(b,s1,s2))
246        | Slabel(l,s) ->
247                let (offset, s) = index_loops_s multi_entry current offset depth s in
248                (offset, Slabel(l, s))
249        | Sswitch(v,ls) ->
250    let (offset, s) = index_loops_ls multi_entry current offset depth ls in
251                (offset, Sswitch(v, ls))
252        | _ as s -> (offset, s)
253
254and index_loops_ls multi_entry current offset depth = function
255  | LSdefault s ->
256                let (offset, s) =       index_loops_s multi_entry current offset depth s in
257                (offset, LSdefault s)
258  | LScase(v,s,ls) ->
259    let (offset, s) = index_loops_s multi_entry current offset depth s in
260    let (offset, ls) = index_loops_ls multi_entry current offset depth ls in
261                (offset, LScase(v,s,ls))
262
263(* Index loops and introduce cost labels in functions *)
264let process_f cost_universe = function
265  | (id,Internal fd) ->
266    let body = fd.fn_body in
267    (* assign loop addresses to labels *)
268    let (_, m) = assign_loop_addrs_s [] 0 Label.Map.empty body in
269    (* find which loops are potentially multi-entry *)
270    let (_, multi_entry) = find_multi_entry_loops_s m [] 0 body in
271    (* index loops accordingly *)
272    let (_, body) = index_loops_s multi_entry [] 0 0 body in
273                (* initialize indexing *)
274                let ind = CostLabel.empty_indexing in
275                (* add cost labels inside *)
276                let body = add_cost_labels_st ind cost_universe body in
277                (* add cost label in front *)
278                let body = add_starting_cost_label ind cost_universe body in 
279                (id,Internal {fd with fn_body = body})
280  | _ as x -> x
281       
282         
283
284(** [add_cost_labels prog] inserts some labels to enable
285    cost annotation. *)
286
287let add_cost_labels p =
288  let labs = ClightAnnotator.all_labels p in
289        let add = CostLabel.Atom.Set.add in
290        let empty = CostLabel.Atom.Set.empty in
291  let labs = StringTools.Set.fold add labs empty in
292  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
293  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
294  {p with prog_funct = List.map (process_f cost_universe) p.prog_funct}
Note: See TracBrowser for help on using the repository browser.