Changeset 1542 for Deliverables/D2.2/8051/src/clight/clightLabelling.ml
 Timestamp:
 Nov 23, 2011, 5:43:24 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051/src/clight/clightLabelling.ml
r1504 r1542 1 1 2 2 (** This module defines the labelling of a [Clight] program. *) 3 4 module IntListSet = Set.Make(struct type t = int list let compare = compare end) 3 5 4 6 open Clight … … 6 8 7 9 8 (* Add a cost label in front of a statement . *)9 10 let add_starting_cost_label cost_universe stmt =11 Clight.Scost (CostLabel. Gen.freshcost_universe, stmt)10 (* Add a cost label in front of a statement with the current indexing. *) 11 12 let add_starting_cost_label indexing cost_universe stmt = 13 Clight.Scost (CostLabel.fresh indexing cost_universe, stmt) 12 14 13 15 (* Add a cost label at the end of a statement. *) 14 16 15 let add_ending_cost_label cost_universe stmt = 16 Clight.Ssequence (stmt, add_starting_cost_label cost_universe Clight.Sskip) 17 let 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) 17 20 18 21 … … 24 27 25 28 26 let add_cost_label_e cost_universe e =27 Expr (Ecost (CostLabel. Gen.freshcost_universe, e), typeof e)29 let add_cost_label_e indexing cost_universe e = 30 Expr (Ecost (CostLabel.fresh indexing cost_universe, e), typeof e) 28 31 29 32 30 33 (* Add cost labels to an expression. *) 31 34 32 let rec add_cost_labels_e cost_universe = function33  Expr (exp,cty) > Expr (add_cost_labels_expr cost_universe exp,cty)34 35 and add_cost_labels_expr cost_universe exp = match exp with35 let rec add_cost_labels_e ind cost_universe = function 36  Expr (exp,cty) > Expr (add_cost_labels_expr ind cost_universe exp,cty) 37 38 and add_cost_labels_expr ind cost_universe exp = match exp with 36 39  Econst_int _  Econst_float _  Evar _  Esizeof _ > exp 37  Ederef e > Ederef (add_cost_labels_e cost_universe e)38  Eaddrof e > Eaddrof (add_cost_labels_e cost_universe e)39  Eunop (op,e) > Eunop (op,(add_cost_labels_e cost_universe e))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)) 40 43  Ebinop (op,e1,e2) > 41 44 Ebinop (op, 42 add_cost_labels_e cost_universe e1,43 add_cost_labels_e cost_universe e2)44  Ecast (t,e) > Ecast (t, add_cost_labels_e cost_universe e)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) 45 48  Eandbool (e1,e2) > 46 let e1' = add_cost_labels_e cost_universe e1 in47 let e2' = add_cost_labels_e cost_universe e2 in48 let b1 = add_cost_label_e cost_universe (const_int 1) in49 let b2 = add_cost_label_e cost_universe (const_int 0) in49 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 50 53 let e2' = Expr (Econdition (e2', b1, b2), int_type) in 51 let e2' = add_cost_label_e cost_universe e2' in52 let e3' = add_cost_label_e cost_universe (const_int 0) in54 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 53 56 Econdition (e1', e2', e3') 54 57  Eorbool (e1,e2) > 55 let e1' = add_cost_labels_e cost_universe e1 in56 let e2' = add_cost_label_e cost_universe (const_int 1) in57 let e3' = add_cost_labels_e cost_universe e2 in58 let b1 = add_cost_label_e cost_universe (const_int 1) in59 let b2 = add_cost_label_e cost_universe (const_int 0) in58 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 60 63 let e3' = Expr (Econdition (e3', b1, b2), int_type) in 61 let e3' = add_cost_label_e cost_universe e3' in64 let e3' = add_cost_label_e ind cost_universe e3' in 62 65 Econdition (e1', e2', e3') 63  Efield (e,id) > Efield (add_cost_labels_e cost_universe e,id)66  Efield (e,id) > Efield (add_cost_labels_e ind cost_universe e,id) 64 67  Econdition (e1,e2,e3) > 65 let e1' = add_cost_labels_e cost_universe e1 in66 let e2' = add_cost_labels_e cost_universe e2 in67 let e2' = add_cost_label_e cost_universe e2' in68 let e3' = add_cost_labels_e cost_universe e3 in69 let e3' = add_cost_label_e cost_universe e3' in68 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 70 73 Econdition (e1', e2', e3') 71 74  Ecost (_,_)  Ecall _ > assert false (* Should not happen *) 72 75 73 let add_cost_labels_opt cost_universe = function 74  None > None 75  Some e > Some (add_cost_labels_e cost_universe e) 76 77 let add_cost_labels_lst cost_universe l = 78 List.map (add_cost_labels_e cost_universe) l 76 let add_cost_labels_opt ind cost_universe = 77 Option.map (add_cost_labels_e ind cost_universe) 78 79 let add_cost_labels_lst ind cost_universe l = 80 List.map (add_cost_labels_e ind cost_universe) l 79 81 80 82 81 83 (* Add cost labels to a statement. *) 82 84 83 let rec add_cost_labels_st cost_universe = function 85 let update_ind i ind = 86 match i with 87  None > ind 88  Some _ > CostLabel.add_id_indexing ind 89 90 let rec add_cost_labels_st ind cost_universe = function 84 91  Sskip > Sskip 85 92  Sassign (e1,e2) > 86 Sassign (add_cost_labels_ecost_universe e1,87 add_cost_labels_ecost_universe e2)93 Sassign (add_cost_labels_e ind cost_universe e1, 94 add_cost_labels_e ind cost_universe e2) 88 95  Scall (e1,e2,lst) > 89 Scall (add_cost_labels_optcost_universe e1,90 add_cost_labels_ecost_universe e2,91 add_cost_labels_lstcost_universe 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) 92 99  Ssequence (s1,s2) > 93 Ssequence (add_cost_labels_stcost_universe s1,94 add_cost_labels_st cost_universe s2)100 Ssequence (add_cost_labels_st ind cost_universe s1, 101 add_cost_labels_st ind cost_universe s2) 95 102  Sifthenelse (e,s1,s2) > 96 let s1' = add_cost_labels_st cost_universe s1 in 97 let s1' = add_starting_cost_label cost_universe s1' in 98 let s2' = add_cost_labels_st cost_universe s2 in 99 let s2' = add_starting_cost_label cost_universe s2' in 100 Sifthenelse (add_cost_labels_e cost_universe e, s1', s2') 101  Swhile (e,s) > 102 let s' = add_cost_labels_st cost_universe s in 103 let s' = add_starting_cost_label cost_universe s' in 104 add_ending_cost_label cost_universe 105 (Swhile (add_cost_labels_e cost_universe e, s')) 106  Sdowhile (e,s) > 107 let s = add_cost_labels_st cost_universe s in 108 let s' = add_starting_cost_label cost_universe s in 109 add_ending_cost_label cost_universe 110 (Sdowhile (add_cost_labels_e cost_universe e, s')) 111  Sfor (s1,e,s2,s3) > 112 let s1' = add_cost_labels_st cost_universe s1 in 113 let s2' = add_cost_labels_st cost_universe s2 in 114 let s3' = add_cost_labels_st cost_universe s3 in 115 let s3' = add_starting_cost_label cost_universe s3' in 116 add_ending_cost_label cost_universe 117 (Sfor (s1', add_cost_labels_e cost_universe e, s2', s3')) 118  Sreturn e > Sreturn (add_cost_labels_opt cost_universe e) 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) 119 130  Sswitch (e,ls) > 120 Sswitch (add_cost_labels_ecost_universe e,121 add_cost_labels_lscost_universe ls)131 Sswitch (add_cost_labels_e ind cost_universe e, 132 add_cost_labels_ls ind cost_universe ls) 122 133  Slabel (lbl,s) > 123 let s' = add_cost_labels_stcost_universe s in124 let s' = add_starting_cost_labelcost_universe s' in125 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') 126 137  Scost (_,_) > assert false 127 138  _ as stmt > stmt 128 139 129 and add_cost_labels_ls cost_universe = function140 and add_cost_labels_ls ind cost_universe = function 130 141  LSdefault s > 131 let s' = add_cost_labels_st cost_universe s in132 let s' = add_starting_cost_label cost_universe s' in142 let s' = add_cost_labels_st ind cost_universe s in 143 let s' = add_starting_cost_label ind cost_universe s' in 133 144 LSdefault s' 134 145  LScase (i,s,ls) > 135 let s' = add_cost_labels_st cost_universe s in 136 let s' = add_starting_cost_label cost_universe s' in 137 LScase (i, s', add_cost_labels_ls cost_universe ls) 138 139 140 (* Add cost labels to a function. *) 141 142 let add_cost_labels_f cost_universe = function 143  (id,Internal fd) > (id,Internal { 144 fn_return = fd.fn_return ; 145 fn_params = fd.fn_params ; 146 fn_vars = fd.fn_vars ; 147 fn_body = add_starting_cost_label cost_universe 148 (add_cost_labels_st cost_universe fd.fn_body) 149 }) 150  (id,External (a,b,c)) > (id,External (a,b,c)) 151 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. *) 154 let 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 173 and 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 179 let 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 multientry due to a goto in [s]. *) 186 let 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 211 and 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 *) 219 let 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 255 and 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 *) 266 let 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 multientry *) 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 152 285 153 286 (** [add_cost_labels prog] inserts some labels to enable … … 156 289 let add_cost_labels p = 157 290 let labs = ClightAnnotator.all_labels p in 158 let labs = StringTools.Set.fold CostLabel.Set.add labs CostLabel.Set.empty in 159 let cost_prefix = CostLabel.Gen.fresh_prefix labs "_cost" in 160 let cost_universe = CostLabel.Gen.new_universe cost_prefix in 161 { 162 prog_funct = List.map (add_cost_labels_f cost_universe) p.prog_funct; 163 prog_main = p.prog_main; 164 prog_vars = p.prog_vars 165 } 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 TracChangeset
for help on using the changeset viewer.