source: Deliverables/D2.2/8051/src/clight/clightLabelling.ml @ 1664

Last change on this file since 1664 was 1542, checked in by tranquil, 8 years ago

merge of indexed labels branch

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 update_ind i ind =
86  match i with
87    | None -> ind
88    | Some _ -> CostLabel.add_id_indexing ind
89
90let rec add_cost_labels_st ind cost_universe = function
91  | Sskip -> Sskip
92  | Sassign (e1,e2) ->
93    Sassign (add_cost_labels_e ind cost_universe e1,
94             add_cost_labels_e ind cost_universe e2)
95  | Scall (e1,e2,lst) ->
96    Scall (add_cost_labels_opt ind cost_universe e1,
97           add_cost_labels_e ind cost_universe e2,
98           add_cost_labels_lst ind cost_universe lst)
99  | Ssequence (s1,s2) ->
100    Ssequence (add_cost_labels_st ind cost_universe s1,
101               add_cost_labels_st ind cost_universe s2)
102  | Sifthenelse (e,s1,s2) ->
103    let s1' = add_cost_labels_st ind cost_universe s1 in
104    let s1' = add_starting_cost_label ind cost_universe s1' in
105    let s2' = add_cost_labels_st ind cost_universe s2 in
106    let s2' = add_starting_cost_label ind cost_universe s2' in
107    Sifthenelse (add_cost_labels_e ind cost_universe e, s1', s2')
108  | Swhile (i,e,s) ->
109    let ind' = update_ind i ind in
110    let s' = add_cost_labels_st ind' cost_universe s in
111    let s' = add_starting_cost_label ind' cost_universe s' in
112      (* exit label indexed with outside indexing *) 
113    add_ending_cost_label ind cost_universe
114      (Swhile (i,add_cost_labels_e ind cost_universe e, s'))
115  | Sdowhile (i,e,s) ->
116    let ind' = update_ind i ind in
117    let s' = add_cost_labels_st ind' cost_universe s in
118    let s' = add_starting_cost_label ind' cost_universe s' in
119    add_ending_cost_label ind cost_universe
120      (Sdowhile (i,add_cost_labels_e ind cost_universe e, s'))
121  | Sfor (i,s1,e,s2,s3) ->
122    let s1' = add_cost_labels_st ind cost_universe s1 in
123    let ind' = update_ind i ind in
124    let s2' = add_cost_labels_st ind' cost_universe s2 in
125    let s3' = add_cost_labels_st ind' cost_universe s3 in
126    let s3' = add_starting_cost_label ind' cost_universe s3' in
127    add_ending_cost_label ind cost_universe
128      (Sfor (i, s1', add_cost_labels_e ind cost_universe e, s2', s3'))
129  | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e)
130  | Sswitch (e,ls) ->
131    Sswitch (add_cost_labels_e ind cost_universe e,
132             add_cost_labels_ls ind cost_universe ls)
133  | Slabel (lbl,s) ->
134    let s' = add_cost_labels_st ind cost_universe s in
135    let s' = add_starting_cost_label ind cost_universe s' in
136    Slabel (lbl,s')
137  | Scost (_,_) -> assert false
138  | _ as stmt -> stmt
139
140and add_cost_labels_ls ind cost_universe = function
141  | LSdefault s ->
142      let s' = add_cost_labels_st ind cost_universe s in
143      let s' = add_starting_cost_label ind cost_universe s' in
144      LSdefault s'
145  | LScase (i,s,ls) ->
146      let s' = add_cost_labels_st ind cost_universe s in
147      let s' = add_starting_cost_label ind cost_universe s' in
148      LScase (i, s', add_cost_labels_ls ind cost_universe ls)
149
150
151(* traversal of code assigning to every label the "loop address" of it. *)
152(* A loop address like [2, 0, 1] means the corresponding label is in the *)
153(* third loop inside the first loop inside the second loop of the body. *)
154let rec assign_loop_addrs_s
155    (current : int list)
156    (offset  : int)
157    (m       : int list Label.Map.t)
158    : Clight.statement -> int*int list Label.Map.t =
159  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 =
191  function
192      (* I am supposing you cannot jump to the update statement of for loops... *)
193    | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
194      let current' = offset :: current in
195      let (_, set) = find_multi_entry_loops_s m current' 0 s in
196      (offset + 1, set)
197    | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
198      let (offset, set1) = find_multi_entry_loops_s m current offset s1 in
199      let (offset, set2) = find_multi_entry_loops_s m current offset s2 in
200      (offset, IntListSet.union set1 set2)
201    | Slabel(_,s) -> find_multi_entry_loops_s m current offset s
202    | Sgoto l ->
203        (* all labels should have a binding in m *)
204      let addr = Label.Map.find l m in
205      let cond = is_prefix addr current in
206      let set = if cond then IntListSet.empty else IntListSet.singleton addr in
207      (offset, set)   
208    | Sswitch(_,ls) -> find_multi_entry_loops_ls m current offset ls
209    | _ -> (offset, IntListSet.empty)
210
211and find_multi_entry_loops_ls m current offset = function
212  | LSdefault s -> find_multi_entry_loops_s m current offset s
213  | LScase(_,s,ls) ->
214    let (offset, set1) = find_multi_entry_loops_s m current offset s in
215    let (offset, set2) = find_multi_entry_loops_ls m current offset ls in
216    (offset, IntListSet.union set1 set2)
217     
218(* final pass where loops are indexed *)
219let rec index_loops_s multi_entry current offset depth = function
220  (* I am supposing you cannot jump to the update statement of for loops... *)
221  | Swhile(_,b,s) ->
222    let current' = offset :: current in
223    let is_bad = IntListSet.mem current' multi_entry in 
224    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
225    let (_, s) = index_loops_s multi_entry current' 0 depth s in 
226    (offset + 1, Swhile(i,b,s))
227  | Sdowhile(_,b,s) ->
228    let current' = offset :: current in
229    let is_bad = IntListSet.mem current' multi_entry in 
230    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
231    let (_, s) = index_loops_s multi_entry current' 0 depth s in 
232    (offset + 1, Sdowhile(i,b,s))
233  | Sfor(_,a1,a2,a3,s) ->
234    let current' = offset :: current in
235    let is_bad = IntListSet.mem current' multi_entry in 
236    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
237    let (_, s) = index_loops_s multi_entry current' 0 depth s in 
238    (offset + 1, Sfor(i,a1,a2,a3,s))
239  | Ssequence(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, Ssequence(s1,s2))
243  | Sifthenelse(b,s1,s2) ->
244    let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
245    let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
246    (offset, Sifthenelse(b,s1,s2))
247  | Slabel(l,s) ->
248    let (offset, s) = index_loops_s multi_entry current offset depth s in
249    (offset, Slabel(l, s))
250  | Sswitch(v,ls) ->
251    let (offset, s) = index_loops_ls multi_entry current offset depth ls in
252    (offset, Sswitch(v, ls))
253  | _ as s -> (offset, s)
254
255and index_loops_ls multi_entry current offset depth = function
256  | LSdefault s ->
257    let (offset, s) =
258      index_loops_s multi_entry current offset depth s in
259    (offset, LSdefault s)
260  | LScase(v,s,ls) ->
261    let (offset, s) = index_loops_s multi_entry current offset depth s in
262    let (offset, ls) = index_loops_ls multi_entry current offset depth ls in
263    (offset, LScase(v,s,ls))
264
265(* Index loops and introduce cost labels in functions *)
266let process_f cost_universe = function
267  | (id,Internal fd) ->
268    let body = fd.fn_body in
269    (* assign loop addresses to labels *)
270    let (_, m) = assign_loop_addrs_s [] 0 Label.Map.empty body in
271    (* find which loops are potentially multi-entry *)
272    let (_, multi_entry) = find_multi_entry_loops_s m [] 0 body in
273    (* index loops accordingly *)
274    let (_, body) = index_loops_s multi_entry [] 0 0 body in
275    (* initialize indexing *)
276    let ind = CostLabel.empty_indexing in
277    (* add cost labels inside *)
278    let body = add_cost_labels_st ind cost_universe body in
279    (* add cost label in front *)
280    let body = add_starting_cost_label ind cost_universe body in 
281    (id,Internal {fd with fn_body = body})
282  | _ as x -> x
283       
284         
285
286(** [add_cost_labels prog] inserts some labels to enable
287    cost annotation. *)
288
289let add_cost_labels p =
290  let labs = ClightAnnotator.all_labels p in
291  let add = CostLabel.Atom.Set.add in
292  let empty = CostLabel.Atom.Set.empty in
293  let labs = StringTools.Set.fold add labs empty in
294  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
295  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
296  {p with prog_funct = List.map (process_f cost_universe) p.prog_funct}
Note: See TracBrowser for help on using the repository browser.