Ignore:
Timestamp:
Nov 23, 2011, 5:43:24 PM (8 years ago)
Author:
tranquil
Message:

merge of indexed labels branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/clight/clightLabelling.ml

    r1504 r1542  
    11
    22(** This module defines the labelling of a [Clight] program. *)
     3
     4module IntListSet = Set.Make(struct type t = int list let compare = compare end)
    35
    46open Clight
     
    68
    79
    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.fresh cost_universe, stmt)
     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)
    1214
    1315(* Add a cost label at the end of a statement. *)
    1416
    15 let add_ending_cost_label cost_universe stmt =
    16   Clight.Ssequence (stmt, add_starting_cost_label cost_universe Clight.Sskip)
     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)
    1720
    1821
     
    2427
    2528
    26 let add_cost_label_e cost_universe e =
    27   Expr (Ecost (CostLabel.Gen.fresh cost_universe, e), typeof e)
     29let add_cost_label_e indexing cost_universe e =
     30  Expr (Ecost (CostLabel.fresh indexing cost_universe, e), typeof e)
    2831
    2932
    3033(* Add cost labels to an expression. *)
    3134
    32 let rec add_cost_labels_e cost_universe = function 
    33   | Expr (exp,cty) -> Expr (add_cost_labels_expr cost_universe exp,cty)
    34 
    35 and add_cost_labels_expr cost_universe exp = match exp with
     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
    3639  | 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))
    4043  | Ebinop (op,e1,e2) ->
    4144      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)
    4548  | Eandbool (e1,e2) ->
    46       let e1' = add_cost_labels_e cost_universe e1 in
    47       let e2' = add_cost_labels_e cost_universe e2 in
    48       let b1 = add_cost_label_e cost_universe (const_int 1) in
    49       let b2 = add_cost_label_e cost_universe (const_int 0) in
     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
    5053      let e2' = Expr (Econdition (e2', b1, b2), int_type) in
    51       let e2' = add_cost_label_e cost_universe e2' in
    52       let e3' = add_cost_label_e cost_universe (const_int 0) 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
    5356      Econdition (e1', e2', e3')
    5457  | Eorbool (e1,e2) ->
    55       let e1' = add_cost_labels_e cost_universe e1 in
    56       let e2' = add_cost_label_e cost_universe (const_int 1) in
    57       let e3' = add_cost_labels_e cost_universe e2 in
    58       let b1 = add_cost_label_e cost_universe (const_int 1) in
    59       let b2 = add_cost_label_e cost_universe (const_int 0) in
     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
    6063      let e3' = Expr (Econdition (e3', b1, b2), int_type) in
    61       let e3' = add_cost_label_e cost_universe e3' in
     64      let e3' = add_cost_label_e ind cost_universe e3' in
    6265      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)
    6467  | Econdition (e1,e2,e3) ->
    65       let e1' = add_cost_labels_e cost_universe e1 in
    66       let e2' = add_cost_labels_e cost_universe e2 in
    67       let e2' = add_cost_label_e cost_universe e2' in
    68       let e3' = add_cost_labels_e cost_universe e3 in
    69       let e3' = add_cost_label_e cost_universe e3' in
     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
    7073      Econdition (e1', e2', e3')
    7174  | Ecost (_,_) | Ecall _ -> assert false (* Should not happen *)
    7275
    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
     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
    7981
    8082
    8183(* Add cost labels to a statement. *)
    8284
    83 let rec add_cost_labels_st cost_universe = function
     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
    8491  | Sskip -> Sskip
    8592  | Sassign (e1,e2) ->
    86       Sassign (add_cost_labels_e cost_universe e1,
    87                add_cost_labels_e cost_universe e2)
     93    Sassign (add_cost_labels_e ind cost_universe e1,
     94             add_cost_labels_e ind cost_universe e2)
    8895  | Scall (e1,e2,lst) ->
    89       Scall (add_cost_labels_opt cost_universe e1,
    90              add_cost_labels_e cost_universe e2,
    91              add_cost_labels_lst cost_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)
    9299  | Ssequence (s1,s2) ->
    93       Ssequence (add_cost_labels_st cost_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)
    95102  | 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)
    119130  | Sswitch (e,ls) ->
    120       Sswitch (add_cost_labels_e cost_universe e,
    121                add_cost_labels_ls cost_universe ls)
     131    Sswitch (add_cost_labels_e ind cost_universe e,
     132             add_cost_labels_ls ind cost_universe ls)
    122133  | Slabel (lbl,s) ->
    123       let s' = add_cost_labels_st cost_universe s in
    124       let s' = add_starting_cost_label cost_universe s' in
    125       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')
    126137  | Scost (_,_) -> assert false
    127138  | _ as stmt -> stmt
    128139
    129 and add_cost_labels_ls cost_universe = function
     140and add_cost_labels_ls ind cost_universe = function
    130141  | LSdefault s ->
    131       let s' = add_cost_labels_st cost_universe s in
    132       let s' = add_starting_cost_label cost_universe s' in
     142      let s' = add_cost_labels_st ind cost_universe s in
     143      let s' = add_starting_cost_label ind cost_universe s' in
    133144      LSdefault s'
    134145  | 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. *)
     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         
    152285
    153286(** [add_cost_labels prog] inserts some labels to enable
     
    156289let add_cost_labels p =
    157290  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.