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

merge of indexed labels branch

Location:
Deliverables/D2.2/8051/src/clight
Files:
10 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D2.2/8051/src/clight/clight.mli

    r818 r1542  
    117117  (** The following constructors are used by the annotation process only. *)
    118118
    119   | Ecost of CostLabel.t*expr                   (**r cost label. *)
     119  | Ecost of CostLabel.t * expr                 (**r cost label. *)
    120120  | Ecall of ident * expr * expr
    121121
    … …  
    130130type label = Label.t
    131131
     132type loop_index = CostLabel.index option
     133
    132134type statement =
    133135  | Sskip                                       (**r do nothing *)
    … …  
    136138  | Ssequence of statement*statement            (**r sequence *)
    137139  | Sifthenelse of expr*statement*statement     (**r conditional *)
    138   | Swhile of expr*statement                    (**r [while] loop *)
    139   | Sdowhile of expr*statement                  (**r [do] loop *)
    140   | Sfor of statement*expr*statement*statement  (**r [for] loop *)
     140  | Swhile of loop_index*expr*statement         (**r [while] loop *)
     141  | Sdowhile of loop_index*expr*statement       (**r [do] loop *)
     142  | Sfor of loop_index*statement*expr*statement*statement (**r [for] loop *)
    141143  | Sbreak                                      (**r [break] statement *)
    142144  | Scontinue                                   (**r [continue] statement *)

  • 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. *)

  • Deliverables/D2.2/8051/src/clight/clightAnnotator.mli

    r1462 r1542  
    22(** This module defines the instrumentation of a [Clight] program. *)
    33
    4 (** [instrument prog cost_map] instruments the program [prog]. First a fresh
    5     global variable --- the so-called cost variable --- is added to the program.
    6     Then, each cost label in the program is replaced by an increment of the cost
    7     variable, following the mapping [cost_map]. The function also returns the
    8     name of the cost variable, the name of the cost increment function, and a
    9     fresh uninitialized global (cost) variable associated to each extern
    10     function. *)
    11 
    12 val instrument : Clight.program -> int CostLabel.Map.t ->
     4(** [instrument cost_tern prog cost_map] instruments the program [prog]. First a
     5    fresh global variable --- the so-called cost variable --- is added to the
     6    program. Then, each cost label in the program is replaced by an increment of
     7    the cost variable, following the mapping [cost_map]. The function also
     8    returns the name of the cost variable, the name of the cost increment
     9    function, and a fresh uninitialized global (cost) variable associated to each
     10    extern function. [cost_tern] rules whether cost increments are given by
     11    ternary expressions (more readable) or by branch statements (for frama-c
     12    itegration). *)
     13val instrument : bool -> Clight.program -> int CostLabel.Map.t ->
    1314                 Clight.program * string * string * string StringTools.Map.t
    1415

  • Deliverables/D2.2/8051/src/clight/clightFold.ml

    r818 r1542  
    116116  | Clight.Ssequence (stmt1, stmt2) -> ([], [stmt1 ; stmt2])
    117117  | Clight.Sifthenelse (e, stmt1, stmt2) -> ([e], [stmt1 ; stmt2])
    118   | Clight.Swhile (e, stmt) | Clight.Sdowhile (e, stmt) -> ([e], [stmt])
    119   | Clight.Sfor (stmt1, e, stmt2, stmt3) -> ([e], [stmt1 ; stmt2 ; stmt3])
     118  | Clight.Swhile (_, e, stmt) | Clight.Sdowhile (_, e, stmt) -> ([e], [stmt])
     119  | Clight.Sfor (_, stmt1, e, stmt2, stmt3) -> ([e], [stmt1 ; stmt2 ; stmt3])
    120120  | Clight.Sreturn (Some e) -> ([e], [])
    121121  | Clight.Sswitch (e, lbl_stmts) -> ([e], labeled_statements_subs lbl_stmts)
    … …  
    145145    | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
    146146      Clight.Sifthenelse (e, stmt1, stmt2)
    147     | Clight.Swhile _, e :: _, stmt :: _ ->
    148       Clight.Swhile (e, stmt)
    149     | Clight.Sdowhile _, e :: _, stmt :: _ ->
    150       Clight.Sdowhile (e, stmt)
    151     | Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
    152       Clight.Sfor (stmt1, e, stmt2, stmt3)
     147    | Clight.Swhile (i, _, _), e :: _, stmt :: _ ->
     148      Clight.Swhile (i, e, stmt)
     149    | Clight.Sdowhile (i, _, _), e :: _, stmt :: _ ->
     150      Clight.Sdowhile (i, e, stmt)
     151    | Clight.Sfor (i, _, _, _, _), e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
     152      Clight.Sfor (i, stmt1, e, stmt2, stmt3)
    153153    | Clight.Sreturn (Some _), e :: _, _ -> Clight.Sreturn (Some e)
    154154    | Clight.Sswitch (_, lbl_stmts), e :: _, _ ->

  • Deliverables/D2.2/8051/src/clight/clightFromC.ml

    r818 r1542  
    490490      Sifthenelse(convertExpr env e, convertStmt env s1, convertStmt env s2)
    491491  | C.Swhile(e, s1) ->
    492       Swhile(convertExpr env e, convertStmt env s1)
     492      Swhile(None, convertExpr env e, convertStmt env s1)
    493493  | C.Sdowhile(s1, e) ->
    494       Sdowhile(convertExpr env e, convertStmt env s1)
     494      Sdowhile(None, convertExpr env e, convertStmt env s1)
    495495  | C.Sfor(s1, e, s2, s3) ->
    496       Sfor(convertStmt env s1, convertExpr env e, convertStmt env s2,
     496      Sfor(None, convertStmt env s1, convertExpr env e, convertStmt env s2,
    497497           convertStmt env s3)
    498498  | C.Sbreak ->

  • Deliverables/D2.2/8051/src/clight/clightInterpret.ml

    r818 r1542  
    44type localEnv = Value.address LocalEnv.t
    55type memory = Clight.fundef Mem.memory
     6type indexing = CostLabel.const_indexing
    67
    78open Clight
    … …  
    2627  | Kstop
    2728  | Kseq of statement*continuation
    28   | Kwhile of expr*statement*continuation
    29   | Kdowhile of expr*statement*continuation
    30   | Kfor2 of expr*statement*statement*continuation
    31   | Kfor3 of expr*statement*statement*continuation
     29  | Kwhile of int option*expr*statement*continuation
     30  | Kdowhile of int option*expr*statement*continuation
     31  | Kfor2 of int option*expr*statement*statement*continuation
     32  | Kfor3 of int option*expr*statement*statement*continuation
    3233  | Kswitch of continuation
    3334  | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
    3435
    3536type state =
    36   | State of cfunction*statement*continuation*localEnv*memory
    37   | Callstate of fundef*Value.t list*continuation*memory
    38   | Returnstate of Value.t*continuation*memory
     37  | State of cfunction*statement*continuation*localEnv*memory*indexing list
     38  | Callstate of fundef*Value.t list*continuation*memory*indexing list
     39  | Returnstate of Value.t*continuation*memory*indexing list
    3940
    4041let string_of_unop = function
    … …  
    104105  | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")"
    105106  | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
    106   | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
     107  | Ecost (cost_lbl, e) ->
     108    let cost_lbl = CostLabel.string_of_cost_label cost_lbl in
     109    "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
    107110  | Ecall (f, arg, e) ->
    108111    "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
    … …  
    110113let string_of_args args =
    111114  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
     115
     116let string_of_loop_depth = function
     117        | None -> ""
     118        | Some d -> " at " ^ string_of_int d
    112119
    113120let rec string_of_statement = function
    … …  
    119126  | Ssequence _ -> "sequence"
    120127  | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
    121   | Swhile (e, _) -> "while (" ^ (string_of_expr e) ^ ")"
    122   | Sdowhile _ -> "dowhile"
    123   | Sfor (s, _, _, _) -> "for (" ^ (string_of_statement s) ^ "; ...)"
     128  | Swhile (i, e, _) ->
     129                let d = string_of_loop_depth i in
     130                "while" ^ d ^ " (" ^ (string_of_expr e) ^ ")"
     131  | Sdowhile (i, _, _) ->
     132    let d = string_of_loop_depth i in
     133    "dowhile" ^ d
     134  | Sfor (i, s, _, _, _) ->
     135                let d = string_of_loop_depth i in
     136                "for" ^ d ^ " (" ^ (string_of_statement s) ^ "; ...)"
    124137  | Sbreak -> "break"
    125138  | Scontinue -> "continue"
    … …  
    129142  | Slabel (lbl, _) -> "label " ^ lbl
    130143  | Sgoto lbl -> "goto " ^ lbl
    131   | Scost (lbl, _) -> "cost " ^ lbl
     144  | Scost (lbl, _) ->
     145    let lbl = CostLabel.string_of_cost_label lbl in
     146                "cost " ^ lbl
    132147
    133148let string_of_local_env lenv =
    … …  
    136151  LocalEnv.fold f lenv ""
    137152
    138 let print_state = function
    139   | State (_, stmt, _, lenv, mem) ->
    140     Printf.printf "Local environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
     153let print_state state = match state with
     154  | State (_, stmt, _, lenv, mem, c) ->
     155    Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing: "
    141156      (string_of_local_env lenv)
    142       (Mem.to_string mem)
     157      (Mem.to_string mem);
     158    let i = CostLabel.curr_const_ind c in
     159    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
     160    Printf.printf "\nRegular state: %s\n\n%!"
    143161      (string_of_statement stmt)
    144   | Callstate (_, args, _, mem) ->
     162  | Callstate (_, args, _, mem, _) ->
    145163    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
    146164      (Mem.to_string mem)
    147165      (MiscPottier.string_of_list " " Value.to_string args)
    148   | Returnstate (v, _, mem) ->
     166  | Returnstate (v, _, mem, _) ->
    149167    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    150168      (Mem.to_string mem)
    … …  
    155173
    156174let rec call_cont = function
    157   | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k)
    158   | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k
     175  | Kseq (_,k) | Kwhile (_, _,_,k) | Kdowhile (_, _,_,k)
     176  | Kfor2 (_, _,_,_,k) | Kfor3 (_, _,_,_,k) | Kswitch k -> call_cont k
    159177  | k -> k
    160178
    … …  
    174192      | None -> find_label1 lbl s2 k
    175193      )
    176   | Swhile (a,s1) -> find_label1 lbl s1 (Kwhile(a,s1,k))
    177   | Sdowhile (a,s1) -> find_label1 lbl s1 (Kdowhile(a,s1,k))
    178   | Sfor (a1,a2,a3,s1) ->
    179       (match find_label1 lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
     194  | Swhile (i,a,s1) -> find_label1 lbl s1 (Kwhile(i,a,s1,k))
     195  | Sdowhile (i,a,s1) -> find_label1 lbl s1 (Kdowhile(i,a,s1,k))
     196  | Sfor (i,a1,a2,a3,s1) ->
     197                (* doubt: should we search for labels in a1? *)
     198      (match find_label1 lbl a1 (Kseq ((Sfor(i,Sskip,a2,a3,s1)),k)) with
    180199      | Some sk -> Some sk
    181200      | None ->
    182           (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with
     201          (match find_label1 lbl s1 (Kfor2(i,a2,a3,s1,k)) with
    183202          | Some sk -> Some sk
    184           | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k))
     203          | None -> find_label1 lbl a3 (Kfor3(i,a2,a3,s1,k))
    185204          ))
    186205  | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
    … …  
    355374let is_false (v, _) = Value.is_false v
    356375
    357 let rec eval_expr localenv m (Expr (ee, tt)) =
     376let rec eval_expr localenv m c (Expr (ee, tt)) =
    358377  match ee with
    359378    | Econst_int i ->
    … …  
    369388      ((v, tt), [])
    370389    | Ederef e when is_function_type tt || is_big_type tt ->
    371       let ((v1,_),l1) = eval_expr localenv m e in
     390      let ((v1,_),l1) = eval_expr localenv m c e in
    372391      ((v1,tt),l1)
    373392    | Ederef e ->
    374       let ((v1,_),l1) = eval_expr localenv m e in
     393      let ((v1,_),l1) = eval_expr localenv m c e in
    375394      let addr = address_of_value v1 in
    376395      let v = Mem.load m (size_of_ctype tt) addr in
    377396      ((v,tt),l1)
    378397    | Eaddrof exp ->
    379       let ((addr,_),l) = eval_lvalue localenv m exp in
     398      let ((addr,_),l) = eval_lvalue localenv m c exp in
    380399      ((value_of_address addr,tt),l)
    381400    | Ebinop (op,exp1,exp2) -> 
    382       let (v1,l1) = eval_expr localenv m exp1 in
    383       let (v2,l2) = eval_expr localenv m exp2 in
     401      let (v1,l1) = eval_expr localenv m c exp1 in
     402      let (v2,l2) = eval_expr localenv m c exp2 in
    384403      ((eval_binop tt v1 v2 op,tt),l1@l2)
    385404    | Eunop (op,exp) ->
    386       let (e1,l1) = eval_expr localenv m exp in
     405      let (e1,l1) = eval_expr localenv m c exp in
    387406      ((eval_unop tt e1 op,tt),l1)
    388407    | Econdition (e1,e2,e3) ->
    389       let (v1,l1) = eval_expr localenv m e1 in
    390       if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
     408      let (v1,l1) = eval_expr localenv m c e1 in
     409      if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
    391410      else
    392         if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3)
     411        if is_false v1 then let (v3,l3) = eval_expr localenv m c e3 in (v3,l1@l3)
    393412      else (v1,l1)
    394413    | Eandbool (e1,e2) ->
    395       let (v1,l1) = eval_expr localenv m e1 in
    396       if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
     414      let (v1,l1) = eval_expr localenv m c e1 in
     415      if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
    397416      else (v1,l1)
    398417    | Eorbool (e1,e2) ->
    399       let (v1,l1) = eval_expr localenv m e1 in
    400       if is_false v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
     418      let (v1,l1) = eval_expr localenv m c e1 in
     419      if is_false v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
    401420      else (v1,l1)
    402421    | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
    403422    | Efield (e1,id) ->
    404       let ((v1,t1),l1) = eval_expr localenv m e1 in
     423      let ((v1,t1),l1) = eval_expr localenv m c e1 in
    405424      let addr = address_of_value (get_offset v1 id t1) in
    406425      ((Mem.load m (size_of_ctype tt) addr, tt), l1)
    407426    | Ecost (lbl,e1) ->
    408       let (v1,l1) = eval_expr localenv m e1 in
     427      (* applying current indexing on label *)
     428      let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
     429      let (v1,l1) = eval_expr localenv m c e1 in
    409430      (v1,lbl::l1)
    410431    | Ecall _ -> assert false (* only used by the annotation process *)
    411432    | Ecast (cty,exp) ->
    412       let ((v,ty),l1) = eval_expr localenv m exp in
     433      let ((v,ty),l1) = eval_expr localenv m c exp in
    413434      ((eval_cast (v,ty,cty),tt),l1)
    414435
    415 and eval_lvalue localenv m (Expr (e,t)) = match e with
     436and eval_lvalue localenv m c (Expr (e,t)) = match e with
    416437  | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
    417438  | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_)
    … …  
    419440  | Evar id -> ((find_symbol localenv m id,t),[])
    420441  | Ederef ee ->
    421     let ((v,_),l1) = eval_expr localenv m ee in
     442    let ((v,_),l1) = eval_expr localenv m c ee in
    422443    ((address_of_value v,t),l1)
    423444  | Efield (ee,id) ->
    424     let ((v,tt),l1) = eval_expr localenv m ee in
     445    let ((v,tt),l1) = eval_expr localenv m c ee in
    425446    let v' = get_offset v id tt in
    426447    ((address_of_value v', t), l1)
    427448  | Ecost (lbl,ee) ->
    428     let (v,l) = eval_lvalue localenv m ee in
     449    let (v,l) = eval_lvalue localenv m c ee in
    429450    (v,lbl::l)
    430451  | Ecall _ -> assert false (* only used in the annotation process *)
    431452
    432 let eval_exprlist lenv mem es =
     453let eval_exprlist lenv mem c es =
    433454  let f (vs, cost_lbls) e =
    434     let ((v, _), cost_lbls') = eval_expr lenv mem e in
     455    let ((v, _), cost_lbls') = eval_expr lenv mem c e in
    435456    (vs @ [v], cost_lbls @ cost_lbls') in
    436457  List.fold_left f ([], []) es
    … …  
    464485  else error "undefined condition guard value."
    465486
    466 let eval_stmt f k e m s = match s, k with
    467   | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[])
    468   | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
    469   | Sskip, Kdowhile(a,s,k) ->
    470     let ((v1, _),l1) = eval_expr e m a in
    471     let a_false = (State(f,Sskip,k,e,m),l1) in
    472     let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
     487let eval_stmt f k e m s c = match s, k with
     488  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m,c),[])
     489  | Sskip, Kwhile(i,a,s,k') | Scontinue, Kwhile(i,a,s,k')
     490  | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') ->
     491    (* possibly continuing a loop *)
     492    CostLabel.continue_loop_opt c i; (* if loop is not continued, this change
     493                                        will have no effect in the following. *)
     494    let ((v1,_),l1) = eval_expr e m c a in
     495    let a_false = (State(f,Sskip,k',e,m,c),l1) in
     496    let a_true = (State(f,s,k,e,m,c),l1) in
    473497    condition v1 a_true a_false
    474   | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
    475   | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
    476   | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[])
     498  | Sskip, Kfor3(i,a2,a3,s,k) | Scontinue, Kfor3(i,a2,a3,s,k) ->
     499    CostLabel.continue_loop_opt c i;
     500    let ((v1,_),l1) = eval_expr e m c a2 in
     501    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     502    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
     503    condition v1 a_true a_false
     504  | Sskip, Kfor2(i,a2,a3,s,k) ->
     505    (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[])
     506  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
    477507  | Sskip, Kcall _ ->
    478508    let m' = free_local_env m e in
    479     (Returnstate(Value.undef,k,m'),[])
     509    (Returnstate(Value.undef,k,m',c),[])
    480510  | Sassign(a1, a2), _ ->
    481     let ((v1,t1),l1) = (eval_lvalue e m a1) in
    482     let ((v2,t2),l2) = eval_expr e m a2 in
    483     (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
     511    let ((v1,t1),l1) = (eval_lvalue e m c a1) in
     512    let ((v2,t2),l2) = eval_expr e m c a2 in
     513    (State(f,Sskip,k,e,assign m v2 t1 v1,c),l1@l2)
    484514  | Scall(None,a,al), _ ->
    485     let ((v1,_),l1) = eval_expr e m a in
     515    let ((v1,_),l1) = eval_expr e m c a in
    486516    let fd = Mem.find_fun_def m (address_of_value v1) in
    487     let (vargs,l2) = eval_exprlist e m al in
    488     (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
     517    let (vargs,l2) = eval_exprlist e m c al in
     518    (Callstate(fd,vargs,Kcall(None,f,e,k),m,c),l1@l2)
    489519  | Scall(Some lhs,a,al), _ ->
    490     let ((v1,_),l1) = eval_expr e m a in
     520    let ((v1,_),l1) = eval_expr e m c a in
    491521    let fd = Mem.find_fun_def m (address_of_value v1) in
    492     let (vargs,l2) = eval_exprlist e m al in
    493     let (vt3,l3) = eval_lvalue e m lhs in
    494     (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m),l1@l2@l3)
    495   | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m),[])
     522    let (vargs,l2) = eval_exprlist e m c al in
     523    let (vt3,l3) = eval_lvalue e m c lhs in
     524    (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m,c),l1@l2@l3)
     525  | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m,c),[])
    496526  | Sifthenelse(a,s1,s2), _ ->
    497     let ((v1,_),l1) = eval_expr e m a in
    498     let a_true = (State(f,s1,k,e,m),l1) in
    499     let a_false = (State(f,s2,k,e,m),l1) in
     527    let ((v1,_),l1) = eval_expr e m c a in
     528    let a_true = (State(f,s1,k,e,m,c),l1) in
     529    let a_false = (State(f,s2,k,e,m,c),l1) in
    500530    condition v1 a_true a_false
    501   | Swhile(a,s), _ ->
    502     let ((v1,_),l1) = eval_expr e m a in
    503     let a_false = (State(f,Sskip,k,e,m),l1) in
    504     let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in
     531  | Swhile(i,a,s), _ ->
     532    CostLabel.enter_loop_opt c i;
     533    let ((v1,_),l1) = eval_expr e m c a in
     534    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     535    let a_true = (State(f,s,Kwhile(i,a,s,k),e,m,c),l1) in
    505536    condition v1 a_true a_false
    506   | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[])
    507   | Sfor(Sskip,a2,a3,s), _ ->
    508     let ((v1,_),l1) = eval_expr e m a2 in
    509     let a_false = (State(f,Sskip,k,e,m),l1) in
    510     let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in
     537  | Sdowhile(i,a,s), _ ->
     538    CostLabel.enter_loop_opt c i;
     539    (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
     540  | Sfor(i,Sskip,a2,a3,s), _ ->
     541    CostLabel.enter_loop_opt c i;
     542    let ((v1,_),l1) = eval_expr e m c a2 in
     543    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     544    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
    511545    condition v1 a_true a_false
    512   | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
    513   | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m),[])
    514   | Sbreak, Kwhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
    515   | Sbreak, Kdowhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
    516   | Sbreak, Kfor2(_,_,_,k) -> (State(f,Sskip,k,e,m),[])
    517   | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m),[])
    518   | Scontinue, Kseq(_,k) -> (State(f,Scontinue,k,e,m),[])
    519   | Scontinue, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
    520   | Scontinue, Kdowhile(a,s,k) ->
    521     let ((v1,_),l1) = eval_expr e m a in
    522     let a_false = (State(f,Sskip,k,e,m),l1) in
    523     let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
    524     condition v1 a_true a_false
    525   | Scontinue, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
    526   | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m),[])
     546  | Sfor(i,a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(i,Sskip,a2,a3,s),k),e,m,c),[])
     547  | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m,c),[])
     548  | Sbreak, Kwhile(_,_,_,k) | Sbreak, Kdowhile(_,_,_,k)
     549  | Sbreak, Kfor2(_,_,_,_,k) | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
     550  | Scontinue, Kseq(_,k)
     551  | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m,c),[])
    527552  | Sreturn None, _ ->
    528553    let m' = free_local_env m e in
    529     (Returnstate(Value.undef,(call_cont k),m'),[])
     554    (Returnstate(Value.undef,(call_cont k),m',c),[])
    530555  | Sreturn (Some a), _ ->
    531     let ((v1,_),l1) = eval_expr e m a  in
     556    let ((v1,_),l1) = eval_expr e m c a  in
    532557    let m' = free_local_env m e in
    533     (Returnstate(v1,call_cont k,m'),l1)
     558    (Returnstate(v1,call_cont k,m',c),l1)
    534559  | Sswitch(a,sl), _ ->
    535     let ((v,_),l) = eval_expr e m a in
     560    let ((v,_),l) = eval_expr e m c a in
    536561    let n = Value.to_int v in
    537     (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
    538   | Slabel(lbl,s), _ -> (State(f,s,k,e,m),[])
    539   | Scost(lbl,s), _ -> (State(f,s,k,e,m),[lbl])
     562  (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l)
     563  | Slabel(lbl,s), _ -> (State(f,s,k,e,m,c),[])
     564  | Scost(lbl,s), _ ->
     565    (* applying current indexing on label *)
     566    let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
     567    (State(f,s,k,e,m,c),[lbl])
    540568  | Sgoto lbl, _ ->
     569    (* if we exit an indexed loop, we don't care. It should not be possible to *)
     570    (* enter an indexed loop that is not the current one, so we do nothing *)
     571    (* to loop indexes *)
    541572    let (s', k') = find_label lbl f.fn_body (call_cont k) in
    542     (State(f,s',k',e,m),[])
     573    (State(f,s',k',e,m,c),[])
    543574  | _ -> assert false (* should be impossible *)
    544575
    … …  
    546577module InterpretExternal = Primitive.Interpret (Mem)
    547578
    548 let interpret_external k mem f args =
     579let interpret_external k mem c f args =
    549580  let (mem', v) = match InterpretExternal.t mem f args with
    550581    | (mem', InterpretExternal.V vs) ->
    … …  
    552583      (mem', v)
    553584    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
    554   Returnstate (v, k, mem')
    555 
    556 let step_call args cont mem = function
     585  Returnstate (v, k, mem',c)
     586
     587let step_call args cont mem c = function
    557588  | Internal f ->
    558589    let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
    559     State (f, f.fn_body, cont, e, mem')
     590    (* initializing loop indices *)
     591    let c = CostLabel.new_const_ind c in
     592    State (f, f.fn_body, cont, e, mem', c)
    560593  | External(id,targs,tres) when List.length targs = List.length args ->
    561     interpret_external cont mem id args
     594    interpret_external cont mem c id args
    562595  | External(id,_,_) ->
    563596    error ("wrong size of arguments when calling external " ^ id ^ ".")
    564597
    565598let step = function
    566   | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt
    567   | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    568   | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[])
    569   | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) ->
     599  | State(f,stmt,k,e,m,c) -> eval_stmt f k e m stmt c
     600  | Callstate(fun_def,vargs,k,m,c) -> (step_call vargs k m c fun_def,[])
     601  | Returnstate(v,Kcall(None,f,e,k),m,c) ->
     602    let c = CostLabel.forget_const_ind c in
     603    (State(f,Sskip,k,e,m,c),[])
     604  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) ->
     605    let c = CostLabel.forget_const_ind c in
    570606    let m' = assign m v ty vv in
    571     (State(f,Sskip,k,e,m'),[])
     607    (State(f,Sskip,k,e,m',c),[])
    572608  | _ -> error "state malformation."
    573609
    … …  
    603639    if debug then Printf.printf "Result = %s\n%!"
    604640      (IntValue.Int32.to_string res) ;
    605     (res, cost_labels) in
     641    (res, List.rev cost_labels) in
    606642  if debug then print_state state ;
    607643  match state with
    608     | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
     644    | Returnstate(v,Kstop,_,_) -> (* Explicit return in main *)
    609645      print_and_return_result (compute_result v)
    610     | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
     646    | State(_,Sskip,Kstop,_,_,_) -> (* Implicit return in main *)
    611647      print_and_return_result IntValue.Int32.zero
    612648    | state -> exec debug cost_labels (step state)
    … …  
    618654    | Some main ->
    619655      let mem = init_mem prog in
    620       let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
     656      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem,[]),[]) in
    621657      exec debug [] first_state

  • 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}

  • Deliverables/D2.2/8051/src/clight/clightParser.mli

    r1462 r1542  
    1 
    21(** This module implements a parser for [C] based on [gcc] and
    32    [CIL]. *)

  • Deliverables/D2.2/8051/src/clight/clightPrinter.ml

    r818 r1542  
    196196  | Efield(e1, id) ->
    197197      fprintf p "%a.%s" print_expr_prec (level, e1) id
    198   | Ecost (lbl,e1) ->
    199       fprintf p "(/* %s */ %a)" lbl print_expr e1
    200   | Ecall (f, arg, e) ->
     198  | Ecost(lbl, e1) ->
     199    (* printing label uglily even if in comment for consistence *)
     200    let lbl = CostLabel.string_of_cost_label lbl in
     201    fprintf p "(/* %s */ %a)" lbl print_expr e1
     202  | Ecall(f, arg, e) ->
    201203      fprintf p "(%s(%a), %a)" f print_expr arg print_expr e
    202204
    … …  
    214216      print_expr p e1;
    215217      print_expr_list p (false, et)
     218
     219let print_loop_depth p = function
     220  | None -> fprintf p ""
     221  | Some x -> fprintf p "/* single entry loop depth: %d */@," x
    216222
    217223let rec print_stmt p s =
    … …  
    241247              print_stmt s1
    242248              print_stmt s2
    243   | Swhile(e, s) ->
    244       fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]"
    245               print_expr e
    246               print_stmt s
    247   | Sdowhile(e, s) ->
    248       fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]"
    249               print_stmt s
    250               print_expr e
    251   | Sfor(s_init, e, s_iter, s_body) ->
    252       fprintf p "@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]"
    253               print_stmt_for s_init
    254               print_expr e
    255               print_stmt_for s_iter
    256               print_stmt s_body
     249  | Swhile(i, e, s) ->
     250    fprintf p "@[<v 0>%a@[<v 2>while (%a) {@ %a@;<0 -2>}@]@]"
     251      print_loop_depth i
     252      print_expr e
     253      print_stmt s
     254  | Sdowhile(i, e, s) ->
     255    fprintf p "@[<v 0>%a@[<v 2>do {@ %a@;<0 -2>} while(%a);@]@]"
     256      print_loop_depth i
     257      print_stmt s
     258      print_expr e
     259  | Sfor(i, s_init, e, s_iter, s_body) ->
     260    fprintf p "@[<v 0>%a@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]@]"
     261      print_loop_depth i
     262      print_stmt_for s_init
     263      print_expr e
     264      print_stmt_for s_iter
     265      print_stmt s_body
    257266  | Sbreak ->
    258       fprintf p "break;"
     267    fprintf p "break;"
    259268  | Scontinue ->
    260       fprintf p "continue;"
     269    fprintf p "continue;"
    261270  | Sswitch(e, cases) ->
    262       fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
    263               print_expr e
    264               print_cases cases
     271    fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
     272      print_expr e
     273      print_cases cases
    265274  | Sreturn None ->
    266       fprintf p "return;"
     275    fprintf p "return;"
    267276  | Sreturn (Some e) ->
    268       fprintf p "return %a;" print_expr e
     277    fprintf p "return %a;" print_expr e
    269278  | Slabel(lbl, s1) ->
    270       fprintf p "%s:@ %a" lbl print_stmt s1
     279    fprintf p "%s:@ %a" lbl print_stmt s1
    271280  | Sgoto lbl ->
    272       fprintf p "goto %s;" lbl
    273  | Scost (lbl,s1) ->
     281    fprintf p "goto %s;" lbl
     282  | Scost (lbl,s1) ->
     283    let lbl = CostLabel.string_of_cost_label lbl in
    274284     fprintf p "%s:@ %a" lbl print_stmt s1
    275285
    … …  
    468478  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
    469479  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
    470   | Swhile(e, s) -> collect_expr e; collect_stmt s
    471   | Sdowhile(e, s) -> collect_stmt s; collect_expr e
    472   | Sfor(s_init, e, s_iter, s_body) ->
    473       collect_stmt s_init; collect_expr e;
    474       collect_stmt s_iter; collect_stmt s_body
     480  | Swhile(_, e, s) -> collect_expr e; collect_stmt s
     481  | Sdowhile(_, e, s) -> collect_stmt s; collect_expr e
     482  | Sfor(_, s_init, e, s_iter, s_body) ->
     483    collect_stmt s_init; collect_expr e;
     484    collect_stmt s_iter; collect_stmt s_body
    475485  | Sbreak -> ()
    476486  | Scontinue -> ()

  • Deliverables/D2.2/8051/src/clight/clightToCminor.ml

    r1462 r1542  
    495495    AST.res = ret_type }
    496496
    497 let f_stmt fresh var_locs stmt sub_exprs_res sub_stmts_res =
    498   let (tmps, sub_stmts_res) = List.split sub_stmts_res in
    499   let tmps = List.flatten tmps in
    500 
    501   let (added_tmps, stmt) = match stmt, sub_exprs_res, sub_stmts_res with
    502 
    503     | Clight.Sskip, _, _ -> ([], Cminor.St_skip)
    504 
    505     | Clight.Sassign (e1, _), _ :: e2 :: _, _ ->
     497let ind_0 i stmt = match i with
     498  | None -> stmt
     499  | Some x -> Cminor.St_ind_0(x, stmt)
     500
     501let ind_inc i stmt = match i with
     502  | None -> stmt
     503  | Some x -> Cminor.St_ind_inc(x, stmt)
     504
     505let trans_for =
     506  let f_expr e _ = e in
     507  let f_stmt stmt expr_res stmt_res = match expr_res, stmt_res, stmt with
     508    | e::_, s1::s2::s3::_, Clight.Sfor(i,_,_,_,_) ->
     509      Clight.Ssequence(s1,Clight.Swhile(i,e,
     510                                        Clight.Ssequence(s3, s2)))
     511    | exprs, sub_sts, stm ->
     512      ClightFold.statement_fill_subs stm exprs sub_sts in
     513  ClightFold.statement2 f_expr f_stmt
     514
     515let cmp_complement = function
     516  | AST.Cmp_eq -> AST.Cmp_ne
     517  | AST.Cmp_ne -> AST.Cmp_eq
     518  | AST.Cmp_gt -> AST.Cmp_le
     519  | AST.Cmp_ge -> AST.Cmp_lt
     520  | AST.Cmp_lt -> AST.Cmp_ge
     521  | AST.Cmp_le -> AST.Cmp_gt
     522
     523let negate_expr (Cminor.Expr (_, et) as e) =
     524  let ed' = Cminor.Op1 (AST.Op_notbool, e) in
     525  Cminor.Expr(ed', et)
     526
     527let rec translate_stmt fresh var_locs cnt_lbl br_lbl = function
     528
     529    | Clight.Sskip -> ([], Cminor.St_skip)
     530
     531    | Clight.Sassign (e1, e2) ->
     532      let e2 = translate_expr var_locs e2 in
    506533      ([], assign var_locs e1 e2)
    507534
    508     | Clight.Scall (None, _, _), f :: args, _ ->
     535    | Clight.Scall (None, f, args) ->
     536      let f = translate_expr var_locs f in
     537      let args = List.map (translate_expr var_locs) args in
    509538      ([], Cminor.St_call (None, f, args, call_sig AST.Type_void args))
    510539
    511     | Clight.Scall (Some e, _, _), _ :: f :: args, _ ->
     540    | Clight.Scall (Some e, f, args) ->
     541      let f = translate_expr var_locs f in
     542      let args = List.map (translate_expr var_locs) args in
    512543      let t = sig_type_of_ctype (clight_type_of e) in
    513544      let tmp = fresh () in
    … …  
    518549      ([(tmp, t)], Cminor.St_seq (stmt_call, stmt_assign))
    519550
    520     | Clight.Swhile _, e :: _, stmt :: _ ->
    521       let econd =
    522         Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
     551    | Clight.Swhile (i,e,stmt) ->
     552      let loop_lbl = fresh () in
     553      let llbl_opt = Some loop_lbl in
     554      let exit_lbl = fresh () in
     555      let elbl_opt = Some exit_lbl in
     556      let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in
     557      let e = translate_expr var_locs e in
     558      let jmp lbl = Cminor.St_goto lbl in
     559      (* let econd = negate_expr e in *)
    523560      let scond =
    524         Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
    525       ([],
    526        Cminor.St_block (Cminor.St_loop (Cminor.St_seq (scond,
    527                                                        Cminor.St_block stmt))))
    528 
    529     | Clight.Sdowhile _, e :: _, stmt :: _ ->
    530       let econd =
    531         Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
     561        Cminor.St_ifthenelse (e, Cminor.St_skip, jmp exit_lbl) in
     562      let loop =
     563        Cminor.St_seq(scond,Cminor.St_seq (stmt, ind_inc i (jmp loop_lbl))) in
     564      let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in
     565      (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip)))
     566       
     567    | Clight.Sdowhile (i,e,stmt) ->
     568      let loop_lbl = fresh () in
     569      let llbl_opt = Some loop_lbl in
     570      let exit_lbl = fresh () in
     571      let elbl_opt = Some exit_lbl in
     572      let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in
     573      let e = translate_expr var_locs e in
     574      let jmp lbl = Cminor.St_goto lbl in
    532575      let scond =
    533         Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
    534       ([],
    535        Cminor.St_block (Cminor.St_loop (Cminor.St_seq (Cminor.St_block stmt,
    536                                                        scond))))
    537 
    538     | Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
    539       let econd =
    540         Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
    541       let scond =
    542         Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
    543       let body = Cminor.St_seq (Cminor.St_block stmt3, stmt2) in
    544       ([],
    545        Cminor.St_seq (stmt1,
    546                       Cminor.St_block
    547                         (Cminor.St_loop (Cminor.St_seq (scond, body)))))
    548 
    549     | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
    550       ([], Cminor.St_ifthenelse (e, stmt1, stmt2))
    551 
    552     | Clight.Ssequence _, _, stmt1 :: stmt2 :: _ ->
    553       ([], Cminor.St_seq (stmt1, stmt2))
    554 
    555     | Clight.Sbreak, _, _ -> ([], Cminor.St_exit 1)
    556 
    557     | Clight.Scontinue, _, _ -> ([], Cminor.St_exit 0)
    558 
    559     | Clight.Sswitch _, _, _ ->
     576        Cminor.St_ifthenelse (e, ind_inc i (jmp loop_lbl), Cminor.St_skip) in
     577      let loop =
     578        Cminor.St_seq (stmt, scond) in
     579      let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in
     580      (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip)))
     581       
     582    | Clight.Sfor _ -> assert false (* transformed *)
     583
     584    | Clight.Sifthenelse (e, stmt1, stmt2) ->
     585      let (tmps1, stmt1) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt1 in
     586      let (tmps2, stmt2) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt2 in
     587      let e = translate_expr var_locs e in
     588      (tmps1 @ tmps2, Cminor.St_ifthenelse (e, stmt1, stmt2))
     589
     590    | Clight.Ssequence(stmt1,stmt2) ->
     591      let (tmps1, stmt1) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt1 in
     592      let (tmps2, stmt2) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt2 in
     593      (tmps1 @ tmps2, Cminor.St_seq (stmt1, stmt2))
     594
     595    | Clight.Sbreak ->
     596      let br_lbl = match br_lbl with
     597        | Some x -> x
     598        | None -> invalid_arg("break without enclosing scope") in
     599      ([], Cminor.St_goto br_lbl)
     600
     601    | Clight.Scontinue ->
     602      let cnt_lbl = match cnt_lbl with
     603        | Some x -> x
     604        | None -> invalid_arg("continue without enclosing scope") in
     605      ([], Cminor.St_goto cnt_lbl)
     606    | Clight.Sswitch _ ->
    560607      (* Should not appear because of switch transformation performed
    561608         beforehand. *)
    562609      assert false
    563610
    564     | Clight.Sreturn None, _, _ -> ([], Cminor.St_return None)
    565 
    566     | Clight.Sreturn (Some _), e :: _, _ -> ([], Cminor.St_return (Some e))
    567 
    568     | Clight.Slabel (lbl, _), _, stmt :: _ -> ([], Cminor.St_label (lbl, stmt))
    569 
    570     | Clight.Sgoto lbl, _, _ -> ([], Cminor.St_goto lbl)
    571 
    572     | Clight.Scost (lbl, _), _, stmt :: _ -> ([], Cminor.St_cost (lbl, stmt))
    573 
    574     | _ -> assert false (* type error *) in
    575 
    576   (tmps @ added_tmps, stmt)
    577 
    578 let translate_statement fresh var_locs =
    579   ClightFold.statement2 (f_expr var_locs) (f_stmt fresh var_locs)
     611    | Clight.Sreturn None -> ([], Cminor.St_return None)
     612
     613    | Clight.Sreturn (Some e) ->
     614      let e = translate_expr var_locs e in
     615      ([], Cminor.St_return (Some e))
     616
     617    | Clight.Slabel (lbl, stmt) ->
     618      let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
     619      (tmps, Cminor.St_label (lbl, stmt))
     620
     621    | Clight.Sgoto lbl -> ([], Cminor.St_goto lbl)
     622
     623    | Clight.Scost (lbl, stmt) ->
     624      let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
     625      (tmps, Cminor.St_cost (lbl, stmt))
     626
     627(*    | _ -> assert false (* type error *) *)
    580628
    581629
    … …  
    598646  let params =
    599647    List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in
    600   let (tmps, body) = translate_statement fresh var_locs cfun.Clight.fn_body in
     648  let body = cfun.Clight.fn_body in
     649  let body = trans_for body in
     650  let (tmps, body) = translate_stmt fresh var_locs None None body in
    601651  let body = add_stack_parameters_initialization var_locs body in
    602652  { Cminor.f_return = type_return_of_ctype cfun.Clight.fn_return ;
Note: See TracChangeset for help on using the changeset viewer.