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

Last change on this file since 1328 was 1328, checked in by tranquil, 9 years ago
  • bug in ClightUtilities?.find_max_depth_lbld fixed
  • single-entry loop detection completed
  • work on Clight completed
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 *)
155(* type is *)
156(* int list -> int -> map -> Clight.statement -> int * map *)
157(* where map = int list Label.Map.t *)
158let rec assign_loop_addrs_s current offset m = function
159        (* I am supposing you cannot jump to the update statement of for loops... *)
160        | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
161                let (_, m) = assign_loop_addrs_s (offset :: current) 0 m s in
162                (offset + 1, m)
163        | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
164                let (offset, m) = assign_loop_addrs_s current offset m s1 in
165                assign_loop_addrs_s current offset m s2
166        | Slabel(l,s) ->
167                let (offset, m) = assign_loop_addrs_s current offset m s in
168                (offset, Label.Map.add l current m)
169        | Sswitch(_,ls) -> assign_loop_addrs_ls current offset m ls
170        | _ -> (offset, m)
171
172and assign_loop_addrs_ls current offset m = function
173  | LSdefault s -> assign_loop_addrs_s current offset m s
174  | LScase(_,s,ls) ->
175                let (offset, m) = assign_loop_addrs_s current offset m s in
176                assign_loop_addrs_ls current offset m ls
177
178let rec is_prefix l1 l2 = match l1, l2 with
179        | [], _ -> true
180        | hd1 :: tl1, hd2 :: tl2 when hd1 = hd2 -> is_prefix tl1 tl2
181        | _ -> false
182
183(* traversal of code which for every statement [s] returns the set of loop*)
184(* addresses which are multi-entry due to a goto in [s]. The type is *)
185(* map -> int list -> int -> statement -> int*set *)
186(* where maps is as above, set = InListSet.t *)
187let rec find_multi_entry_loops_s m current offset = function
188        (* I am supposing you cannot jump to the update statement of for loops... *)
189        | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
190                        let current' = offset :: current in
191                        let (_, set) = find_multi_entry_loops_s m current' 0 s in
192                        (offset + 1, set)
193        | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
194          let (offset, set1) = find_multi_entry_loops_s m current offset s1 in
195          let (offset, set2) = find_multi_entry_loops_s m current offset s2 in
196          (offset, IntListSet.union set1 set2)
197        | Slabel(_,s) -> find_multi_entry_loops_s m current offset s
198                | Sgoto l ->
199                        (* all labels should have a binding in m *)
200                        let addr = Label.Map.find l m in
201                        let cond = is_prefix addr current in
202                        let set = if cond then IntListSet.empty else IntListSet.singleton addr in
203                        (offset, set)   
204        | Sswitch(_,ls) -> find_multi_entry_loops_ls m current offset ls
205        | _ -> (offset, IntListSet.empty)
206
207and find_multi_entry_loops_ls m current offset = function
208  | LSdefault s -> find_multi_entry_loops_s m current offset s
209  | LScase(_,s,ls) ->
210    let (offset, set1) = find_multi_entry_loops_s m current offset s in
211    let (offset, set2) = find_multi_entry_loops_ls m current offset ls in
212    (offset, IntListSet.union set1 set2)
213                               
214(* final pass where loops are indexed *)
215let rec index_loops_s multi_entry current offset depth = function
216        (* I am supposing you cannot jump to the update statement of for loops... *)
217        | Swhile(_,b,s) ->
218    let current' = offset :: current in
219                let is_bad = IntListSet.mem current' multi_entry in 
220                let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
221          let (_, s) = index_loops_s multi_entry current' 0 depth s in 
222          (offset + 1, Swhile(i,b,s))
223        | Sdowhile(_,b,s) ->
224    let current' = offset :: current in
225    let is_bad = IntListSet.mem current' multi_entry in 
226    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
227          let (_, s) = index_loops_s multi_entry current' 0 depth s in 
228          (offset + 1, Sdowhile(i,b,s))
229        | Sfor(_,a1,a2,a3,s) ->
230    let current' = offset :: current in
231    let is_bad = IntListSet.mem current' multi_entry in 
232    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
233          let (_, s) = index_loops_s multi_entry current' 0 depth s in 
234          (offset + 1, Sfor(i,a1,a2,a3,s))
235        | Ssequence(s1,s2) ->
236          let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
237          let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
238          (offset, Ssequence(s1,s2))
239        | Sifthenelse(b,s1,s2) ->
240          let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
241          let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
242          (offset, Sifthenelse(b,s1,s2))
243        | Slabel(l,s) ->
244                let (offset, s) = index_loops_s multi_entry current offset depth s in
245                (offset, Slabel(l, s))
246        | Sswitch(v,ls) ->
247    let (offset, s) = index_loops_ls multi_entry current offset depth ls in
248                (offset, Sswitch(v, ls))
249        | _ as s -> (offset, s)
250
251and index_loops_ls multi_entry current offset depth = function
252  | LSdefault s ->
253                let (offset, s) =       index_loops_s multi_entry current offset depth s in
254                (offset, LSdefault s)
255  | LScase(v,s,ls) ->
256    let (offset, s) = index_loops_s multi_entry current offset depth s in
257    let (offset, ls) = index_loops_ls multi_entry current offset depth ls in
258                (offset, LScase(v,s,ls))
259
260(* Index loops and introduce cost labels in functions *)
261let process_f cost_universe = function
262  | (id,Internal fd) ->
263    let body = fd.fn_body in
264    (* assign loop addresses to labels *)
265    let (_, m) = assign_loop_addrs_s [] 0 Label.Map.empty body in
266    (* find which loops are potentially multi-entry *)
267    let (_, multi_entry) = find_multi_entry_loops_s m [] 0 body in
268    (* index loops accordingly *)
269    let (_, body) = index_loops_s multi_entry [] 0 0 body in
270                (* initialize indexing *)
271                let ind = CostLabel.empty_indexing in
272                (* add cost labels inside *)
273                let body = add_cost_labels_st ind cost_universe body in
274                (* add cost label in front *)
275                let body = add_starting_cost_label ind cost_universe body in 
276                (id,Internal {fd with fn_body = body})
277  | _ as x -> x
278       
279         
280
281(** [add_cost_labels prog] inserts some labels to enable
282    cost annotation. *)
283
284let add_cost_labels p =
285  let labs = ClightAnnotator.all_labels p in
286        let add = CostLabel.Atom.Set.add in
287        let empty = CostLabel.Atom.Set.empty in
288  let labs = StringTools.Set.fold add labs empty in
289  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
290  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
291  {p with prog_funct = List.map (process_f cost_universe) p.prog_funct}
Note: See TracBrowser for help on using the repository browser.