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

merge of indexed labels branch

File:
1 edited

Legend:

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

    r1462 r1542  
    1010let cost_id_prefix = "_cost"
    1111let cost_incr_prefix = "_cost_incr"
     12let loop_id_prefix = "_i"
    1213
    1314
     
    7071  let def_idents = function
    7172    | Clight.Internal def ->
    72         let vars =
    73           string_set_of_list
    74             (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
    75         let (names, cost_labels, user_labels) =
    76           body_idents def.Clight.fn_body in
    77         (StringTools.Set.union vars names, cost_labels, user_labels)
     73      let vars =
     74        string_set_of_list
     75          (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
     76      let (names, cost_labels, user_labels) =
     77        body_idents def.Clight.fn_body in
     78      (StringTools.Set.union vars names, cost_labels, user_labels)
    7879    | Clight.External (id, _, _) ->
    79         (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
     80      (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
    8081  let fun_idents (id, f_def) =
    8182    let (names, cost_labels, user_labels) = def_idents f_def in
     
    9394let all_labels p =
    9495  let (_, cost_labels, user_labels) = prog_idents p in
    95   let all =
    96     CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls)
    97       cost_labels StringTools.Set.empty in
    98   Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all
     96  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     97  let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
     98  Label.Set.fold StringTools.Set.add user_labels all
    9999
    100100let all_idents p =
    101101  let (names, cost_labels, user_labels) = prog_idents p in
     102  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     103  let cost_labels = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
    102104  let to_string_set fold set =
    103105    fold (fun lbl idents -> StringTools.Set.add lbl idents) set
    104106      StringTools.Set.empty in
    105   let cost_labels = to_string_set CostLabel.Set.fold cost_labels in
    106107  let user_labels = to_string_set Label.Set.fold user_labels in
    107108  StringTools.Set.union names (StringTools.Set.union cost_labels user_labels)
     
    125126let const_int i = Clight.Expr (Clight.Econst_int i, int_typ)
    126127
     128let expr_of_cost_cond var = function
     129  | CostExpr.Ceq k ->
     130    Clight.Expr(Clight.Ebinop(Clight.Oeq, var, const_int k),int_typ)
     131  | CostExpr.Cgeq k ->
     132    Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ)
     133  | CostExpr.Cmod (a, b) ->
     134    let modulus =
     135      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
     136    Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ)
     137  | CostExpr.Cgeqmod (k, a, b) ->
     138    let modulus =
     139      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
     140    let modulus_eq =
     141      Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ) in
     142    let greater =
     143      Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) in
     144    Clight.Expr(Clight.Eandbool(modulus_eq, greater),int_typ)
     145
     146let rec expr_of_cost_gen_cond var gc =
     147  assert (not (CostExpr.CondSet.is_empty gc));
     148  let c = CostExpr.CondSet.min_elt gc in
     149  let c_expr = expr_of_cost_cond var c in
     150  let rest = CostExpr.CondSet.remove c gc in
     151  if CostExpr.CondSet.is_empty rest then c_expr else
     152    let rest_expr = expr_of_cost_gen_cond var rest in
     153    Clight.Expr(Clight.Eandbool(c_expr, rest_expr), int_typ)
     154
     155let rec expr_of_cost_expr prefix = function
     156  | CostExpr.Exact k -> const_int k
     157  | CostExpr.Ternary(index, cond, if_true, if_false) ->
     158    let id = CostLabel.make_id prefix index in
     159    let var = Clight.Expr(Clight.Evar id, int_typ) in
     160    let cond_e = expr_of_cost_gen_cond var cond in
     161    let if_true_e = expr_of_cost_expr prefix if_true in
     162    let if_false_e = expr_of_cost_expr prefix if_false in
     163    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
     164
     165(* as long as Clight parser will be called at the end, this hack works *)
     166(* this will be called in case -no-cost-tern is active. *)
     167let rec side_effect_expr_of_cost_expr prefix cost_incr cont e_type = function
     168  | CostExpr.Exact k ->
     169    Clight.Expr(Clight.Ecall (cost_incr, const_int k, cont), e_type)
     170  | CostExpr.Ternary(index, cond, if_true, if_false) ->
     171    let id = CostLabel.make_id prefix index in
     172    let var = Clight.Expr(Clight.Evar id, int_typ) in
     173    let cond_e = expr_of_cost_gen_cond var cond in
     174    let rec_call = side_effect_expr_of_cost_expr prefix cost_incr cont e_type in
     175    let if_true_e = rec_call if_true in
     176    let if_false_e = rec_call if_false in
     177    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
     178
     179let rec stmt_of_cost_expr prefix cost_incr = function
     180  | CostExpr.Exact k -> Clight.Scall (None, cost_incr, [const_int k])
     181  | CostExpr.Ternary(index, cond, if_true, if_false) ->
     182    let id = CostLabel.make_id prefix index in
     183    let var = Clight.Expr(Clight.Evar id, int_typ) in
     184    let cond_e = expr_of_cost_gen_cond var cond in
     185    let if_true_s = stmt_of_cost_expr prefix cost_incr if_true in
     186    let if_false_s = stmt_of_cost_expr prefix cost_incr if_false in
     187    Clight.Sifthenelse (cond_e, if_true_s, if_false_s)
     188
    127189(* Instrument an expression. *)
    128190
    129 let rec instrument_expr cost_mapping cost_incr e =
    130   let Clight.Expr (e, t) = e in
    131   match e with
    132     | Clight.Ecost (lbl, e)
    133         when CostLabel.Map.mem lbl cost_mapping &&
    134              CostLabel.Map.find lbl cost_mapping = 0 ->
    135         e
    136     | _ ->
    137         let e' = instrument_expr_descr cost_mapping cost_incr e in
    138         Clight.Expr (e', t)
    139 and instrument_expr_descr cost_mapping cost_incr e = match e with
    140   | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
    141   | Clight.Esizeof _ -> e
    142   | Clight.Ederef e ->
    143       let e' = instrument_expr cost_mapping cost_incr e in
    144       Clight.Ederef e'
    145   | Clight.Eaddrof e ->
    146       let e' = instrument_expr cost_mapping cost_incr e in
    147       Clight.Eaddrof e'
    148   | Clight.Eunop (op, e) ->
    149       let e' = instrument_expr cost_mapping cost_incr e in
    150       Clight.Eunop (op, e')
    151   | Clight.Ebinop (op, e1, e2) ->
    152       let e1' = instrument_expr cost_mapping cost_incr e1 in
    153       let e2' = instrument_expr cost_mapping cost_incr e2 in
    154       Clight.Ebinop (op, e1', e2')
    155   | Clight.Ecast (t, e) ->
    156       let e' = instrument_expr cost_mapping cost_incr e in
    157       Clight.Ecast (t, e')
    158   | Clight.Econdition (e1, e2, e3) ->
    159       let e1' = instrument_expr cost_mapping cost_incr e1 in
    160       let e2' = instrument_expr cost_mapping cost_incr e2 in
    161       let e3' = instrument_expr cost_mapping cost_incr e3 in
    162       Clight.Econdition (e1', e2', e3')
    163   | Clight.Eandbool (e1, e2) ->
    164       let e1' = instrument_expr cost_mapping cost_incr e1 in
    165       let e2' = instrument_expr cost_mapping cost_incr e2 in
    166       Clight.Eandbool (e1', e2')
    167   | Clight.Eorbool (e1, e2) ->
    168       let e1' = instrument_expr cost_mapping cost_incr e1 in
    169       let e2' = instrument_expr cost_mapping cost_incr e2 in
    170       Clight.Eorbool (e1', e2')
    171   | Clight.Efield (e, x) ->
    172       let e' = instrument_expr cost_mapping cost_incr e in
    173       Clight.Efield (e', x)
    174   | Clight.Ecost (lbl, e) when CostLabel.Map.mem lbl cost_mapping ->
    175       let e' = instrument_expr cost_mapping cost_incr e in
    176       let incr = CostLabel.Map.find lbl cost_mapping in
    177       if incr = 0 then let Clight.Expr (e'', _) = e' in e''
    178       else Clight.Ecall (cost_incr, const_int incr, e')
    179   | Clight.Ecost (_, e) ->
    180     let Clight.Expr (e', _) = instrument_expr cost_mapping cost_incr e in
    181     e'
    182   | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *)
     191(* FIXME: currently using a hack (reparsing) *)
     192let instrument_expr cost_tern l_ind cost_mapping cost_incr =
     193  let f_expr (Clight.Expr(ed, et) as e) sub_res = match ed, sub_res with
     194  | Clight.Ecost (lbl, _), e' :: _ ->
     195    let atom = lbl.CostLabel.name in
     196    let cost =
     197      try
     198        CostLabel.Atom.Map.find atom cost_mapping
     199      with (* if atom is not present, then map to 0 *)
     200        | Not_found -> CostExpr.Exact 0 in
     201    if cost = CostExpr.Exact 0 then e' else
     202      if cost_tern then
     203        let cost = expr_of_cost_expr l_ind cost in
     204        Clight.Expr(Clight.Ecall (cost_incr, cost, e'), et)
     205      else
     206        side_effect_expr_of_cost_expr l_ind cost_incr e' et cost
     207  | Clight.Ecall (_, _, _), _ -> assert false (* Should not happen. *)
     208  | _ -> ClightFold.expr_fill_exprs e sub_res in
     209  ClightFold.expr2 f_expr
     210
     211let loop_increment prefix depth body = match depth  with
     212  | None -> body
     213  | Some d ->
     214    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
     215    let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in
     216    Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1)))
     217     
     218let loop_reset_index prefix depth loop = match depth with
     219  | None -> loop
     220  | Some d ->
     221    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
     222    Clight.Ssequence(Clight.Sassign(id, const_int 0), loop)
     223
    183224
    184225(* Instrument a statement. *)
    185226
    186 let rec instrument_body cost_mapping cost_incr stmt = match stmt with
    187   | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
    188   | Clight.Sgoto _ ->
    189     stmt
    190   | Clight.Sassign (e1, e2) ->
    191     let e1' = instrument_expr cost_mapping cost_incr e1 in
    192     let e2' = instrument_expr cost_mapping cost_incr e2 in
    193     Clight.Sassign (e1', e2')
    194   | Clight.Scall (eopt, f, args) ->
    195     let eopt' = match eopt with
    196       | None -> None
    197       | Some e -> Some (instrument_expr cost_mapping cost_incr e) in
    198     let f' = instrument_expr cost_mapping cost_incr f in
    199     let args' = List.map (instrument_expr cost_mapping cost_incr) args in
    200     Clight.Scall (eopt', f', args')
    201   | Clight.Ssequence (s1, s2) ->
    202     Clight.Ssequence (instrument_body cost_mapping cost_incr s1,
    203                       instrument_body cost_mapping cost_incr s2)
    204   | Clight.Sifthenelse (e, s1, s2) ->
    205     let e' = instrument_expr cost_mapping cost_incr e in
    206     let s1' = instrument_body cost_mapping cost_incr s1 in
    207     let s2' = instrument_body cost_mapping cost_incr s2 in
    208     Clight.Sifthenelse (e', s1', s2')
    209   | Clight.Swhile (e, s) ->
    210     let e' = instrument_expr cost_mapping cost_incr e in
    211     let s' = instrument_body cost_mapping cost_incr s in
    212     Clight.Swhile (e', s')
    213   | Clight.Sdowhile (e, s) ->
    214     let e' = instrument_expr cost_mapping cost_incr e in
    215     let s' = instrument_body cost_mapping cost_incr s in
    216     Clight.Sdowhile (e', s')
    217   | Clight.Sfor (s1, e, s2, s3) ->
    218     let s1' = instrument_body cost_mapping cost_incr s1 in
    219     let e' = instrument_expr cost_mapping cost_incr e in
    220     let s2' = instrument_body cost_mapping cost_incr s2 in
    221     let s3' = instrument_body cost_mapping cost_incr s3 in
    222     Clight.Sfor (s1', e', s2', s3')
    223   | Clight.Sreturn (Some e) ->
    224     let e' = instrument_expr cost_mapping cost_incr e in
    225     Clight.Sreturn (Some e')
    226   | Clight.Sswitch (e, ls) ->
    227     let e' = instrument_expr cost_mapping cost_incr e in
    228     let ls' = instrument_ls cost_mapping cost_incr ls in
    229     Clight.Sswitch (e', ls')
    230   | Clight.Slabel (lbl, s) ->
    231     let s' = instrument_body cost_mapping cost_incr s in
    232     Clight.Slabel (lbl, s')
    233   | Clight.Scost (lbl, s) when CostLabel.Map.mem lbl cost_mapping ->
     227(* FIXME: use ClightFold, a much better option *)
     228let rec instrument_body cost_tern l_ind cost_mapping cost_incr stmt =
     229  let instr_expr = instrument_expr cost_tern l_ind cost_mapping cost_incr in
     230  let instr_body = instrument_body cost_tern l_ind cost_mapping cost_incr in
     231  match stmt with
     232    | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
     233    | Clight.Sgoto _ ->
     234      stmt
     235    | Clight.Sassign (e1, e2) ->
     236      let e1' = instr_expr e1 in
     237      let e2' = instr_expr e2 in
     238      Clight.Sassign (e1', e2')
     239    | Clight.Scall (eopt, f, args) ->
     240      let eopt' = Option.map instr_expr eopt in
     241      let f' = instr_expr f in
     242      let args = List.map (instr_expr) args in
     243      Clight.Scall (eopt', f', args)
     244    | Clight.Ssequence (s1, s2) ->
     245      Clight.Ssequence (
     246        instr_body s1,
     247        instr_body s2)
     248    | Clight.Sifthenelse (e, s1, s2) ->
     249      let e' = instr_expr e in
     250      let s1' = instr_body s1 in
     251      let s2' = instr_body s2 in
     252      Clight.Sifthenelse (e', s1', s2')
     253    | Clight.Swhile (i, e, s) ->
     254      let e' = instr_expr e in
     255      let s' = instr_body s in
     256      let s' = loop_increment l_ind i s' in
     257      loop_reset_index l_ind i (Clight.Swhile (None, e', s'))
     258    | Clight.Sdowhile (i, e, s) ->
     259      let e' = instr_expr e in
     260      let s' = instr_body s in
     261      let s' = loop_increment l_ind i s' in
     262      loop_reset_index l_ind i (Clight.Sdowhile (None, e', s'))
     263    | Clight.Sfor (i, s1, e, s2, s3) ->
     264      let s1' = instr_body s1 in
     265      let e' = instr_expr e in
     266      let s2' = instr_body s2 in
     267      let s3' = instr_body s3 in
     268      let s3' = loop_increment l_ind i s3' in
     269      loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3'))
     270    | Clight.Sreturn (Some e) ->
     271      let e' = instr_expr e in
     272      Clight.Sreturn (Some e')
     273    | Clight.Sswitch (e, ls) ->
     274      let e' = instr_expr e in
     275      let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
     276      Clight.Sswitch (e', ls')
     277    | Clight.Slabel (lbl, s) ->
     278      let s' = instr_body s in
     279      Clight.Slabel (lbl, s')
     280    | Clight.Scost (lbl, s) ->
    234281    (* Keep the cost label in the code. *)
    235     let s' = instrument_body cost_mapping cost_incr s in
    236     let incr = CostLabel.Map.find lbl cost_mapping in
    237     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    238     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    239     let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
    240     Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
    241   (*
    242     let s' = instrument_body cost_mapping cost_incr s in
    243     let incr = CostLabel.Map.find lbl cost_mapping in
    244     if incr = 0 then s'
    245     else
    246     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    247     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    248     let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
    249     Clight.Ssequence (Clight.Scall (None, f, args), s')
    250   *)
    251   | Clight.Scost (lbl, s) ->
    252     (* Keep the cost label in the code and show the increment of 0. *)
    253     let s' = instrument_body cost_mapping cost_incr s in
    254     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    255     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    256     let args = [Clight.Expr (Clight.Econst_int 0, int_typ)] in
    257     Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
    258   (*
    259     instrument_body cost_mapping cost_incr s
    260   *)
    261 and instrument_ls cost_mapping cost_incr = function
     282      let s' = instr_body s in
     283      let atom = lbl.CostLabel.name in
     284      let cost =
     285        try
     286          CostLabel.Atom.Map.find atom cost_mapping
     287        with (* if atom is not present, then map to 0 *)
     288          | Not_found -> CostExpr.Exact 0 in
     289      let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
     290      let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
     291      let cost_stmt =
     292        if not cost_tern then stmt_of_cost_expr l_ind f cost else
     293        let cost = expr_of_cost_expr l_ind cost in
     294        Clight.Scall(None, f, [cost]) in
     295      Clight.Scost (lbl, Clight.Ssequence (cost_stmt, s'))
     296(*
     297  let s' = instrument_body l_ind cost_mapping cost_incr s in
     298  let incr = CostLabel.Map.find lbl cost_mapping in
     299  if incr = 0 then s'
     300  else
     301  let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
     302  let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
     303  let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
     304  Clight.Ssequence (Clight.Scall (None, f, args), s')
     305*)
     306(*
     307  instrument_body l_ind cost_mapping cost_incr s
     308*)
     309and instrument_ls cost_tern l_ind cost_mapping cost_incr = function
    262310  | Clight.LSdefault s ->
    263     let s' = instrument_body cost_mapping cost_incr s in
     311    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
    264312    Clight.LSdefault s'
    265313  | Clight.LScase (i, s, ls) ->
    266     let s' = instrument_body cost_mapping cost_incr s in
    267     let ls' = instrument_ls cost_mapping cost_incr ls in
     314    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
     315    let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
    268316    Clight.LScase (i, s', ls')
     317     
     318let rec loop_indexes_defs prefix max_depth =
     319  if max_depth = 0 then [] else
     320    let max_depth = max_depth - 1 in
     321    let id = CostLabel.make_id prefix max_depth in
     322    (id, int_typ) :: loop_indexes_defs prefix max_depth
     323
     324let max_depth =
     325  let f_expr _ _ = () in
     326  let f_stmt stmt _ res_stmts =
     327    let curr_max = List.fold_left max 0 res_stmts in
     328    if curr_max > 0 then curr_max else 
     329      match stmt with
     330        | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_)
     331        | Clight.Sfor(Some x,_,_,_,_) -> x + 1
     332        | _ -> 0 in
     333  ClightFold.statement2 f_expr f_stmt
    269334
    270335(* Instrument a function. *)
    271336
    272 let instrument_funct cost_mapping cost_incr (id, def) =
     337let instrument_funct cost_tern  l_ind cost_mapping cost_incr (id, def) =
    273338  let def = match def with
    274339    | Clight.Internal def ->
    275         let body = instrument_body cost_mapping cost_incr def.Clight.fn_body in
    276         Clight.Internal { def with Clight.fn_body = body }
     340      let max_depth = max_depth def.Clight.fn_body in
     341      let vars = loop_indexes_defs l_ind max_depth in
     342      let vars = List.rev_append vars def.Clight.fn_vars in
     343      let body = def.Clight.fn_body in
     344      let body =
     345        instrument_body cost_tern l_ind cost_mapping cost_incr body in
     346      Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
    277347    | Clight.External _ -> def
    278348  in
     
    326396    name of the cost variable and the name of the cost increment function. *)
    327397
    328 let instrument p cost_mapping =
     398let instrument cost_tern p cost_mapping =
    329399
    330400  (* Create a fresh 'cost' variable. *)
     
    334404  let cost_decl = cost_decl cost_id in
    335405
     406  (* Create a fresh loop index prefix *)
     407  let names = StringTools.Set.add cost_id names in
     408  let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in
     409
    336410  (* Create a fresh uninitialized global variable for each extern function. *)
    337411  let (extern_cost_decls, extern_cost_variables) =
     
    344418  let cost_incr_def = cost_incr_def cost_id cost_incr in
    345419
     420  (* Turn the mapping from indexed cost labels to integers into one from *)
     421  (* cost atoms to cost expresisons *)
     422  let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in
     423
    346424  (* Instrument each function *)
     425  let prog_funct = p.Clight.prog_funct in
    347426  let prog_funct =
    348     List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in
     427    let f = instrument_funct cost_tern l_ind cost_mapping cost_incr in
     428    List.map f prog_funct in
    349429
    350430  (* Glue all this together. *)
Note: See TracChangeset for help on using the changeset viewer.