Ignore:
Timestamp:
Nov 15, 2011, 5:11:19 PM (8 years ago)
Author:
tranquil
Message:
  • added an option to not use ternary expressions in costs, to accomodate frama-c explosion of such expressions
  • corrected some typos in comments
  • added a check for well behaved for loops in loop unrolling, but intelligent unrolling is not done yet
  • TODO: peeling and unrolling can contradict preciseness (with difference between introduced branches around 2 cycles). I guess it can be corrected easily
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml

    r1433 r1507  
    2727
    2828let empty_triple =
    29         (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
     29  (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
    3030
    3131let name_singleton id =
     
    7272  let def_idents = function
    7373    | Clight.Internal def ->
    74         let vars =
    75           string_set_of_list
    76             (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
    77         let (names, cost_labels, user_labels) =
    78           body_idents def.Clight.fn_body in
    79         (StringTools.Set.union vars names, cost_labels, user_labels)
     74      let vars =
     75        string_set_of_list
     76          (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
     77      let (names, cost_labels, user_labels) =
     78        body_idents def.Clight.fn_body in
     79      (StringTools.Set.union vars names, cost_labels, user_labels)
    8080    | Clight.External (id, _, _) ->
    81         (StringTools.Set.singleton id, CostLabel.Set.empty,
    82         Label.Set.empty) in
     81      (StringTools.Set.singleton id, CostLabel.Set.empty,
     82      Label.Set.empty) in
    8383  let fun_idents (id, f_def) =
    8484    let (names, cost_labels, user_labels) = def_idents f_def in
     
    9696let all_labels p =
    9797  let (_, cost_labels, user_labels) = prog_idents p in
    98         let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     98  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
    9999  let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
    100100  Label.Set.fold StringTools.Set.add user_labels all
     
    102102let all_idents p =
    103103  let (names, cost_labels, user_labels) = prog_idents p in
    104         let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     104  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
    105105  let cost_labels = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
    106106  let to_string_set fold set =
     
    140140    let modulus =
    141141      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
    142         let modulus_eq =
    143              Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ) in
    144         let greater =
    145             Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) in
     142    let modulus_eq =
     143      Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ) in
     144    let greater =
     145      Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) in
    146146    Clight.Expr(Clight.Eandbool(modulus_eq, greater),int_typ)
    147  
     147
     148let rec expr_of_cost_gen_cond var gc =
     149  assert (not (CostExpr.CondSet.is_empty gc));
     150  let c = CostExpr.CondSet.min_elt gc in
     151  let c_expr = expr_of_cost_cond var c in
     152  let rest = CostExpr.CondSet.remove c gc in
     153  if CostExpr.CondSet.is_empty rest then c_expr else
     154    let rest_expr = expr_of_cost_gen_cond var rest in
     155    Clight.Expr(Clight.Eandbool(c_expr, rest_expr), int_typ)
     156
    148157let rec expr_of_cost_expr prefix = function
    149     | CostExpr.Exact k -> const_int k
    150     | CostExpr.Ternary(index, cond, if_true, if_false) ->
     158  | CostExpr.Exact k -> const_int k
     159  | CostExpr.Ternary(index, cond, if_true, if_false) ->
    151160    let id = CostLabel.make_id prefix index in
    152161    let var = Clight.Expr(Clight.Evar id, int_typ) in
    153     let cond_e = expr_of_cost_cond var cond in
     162    let cond_e = expr_of_cost_gen_cond var cond in
    154163    let if_true_e = expr_of_cost_expr prefix if_true in
    155164    let if_false_e = expr_of_cost_expr prefix if_false in
    156     Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)   
     165    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
     166
     167(* as long as Clight parser will be called at the end, this hack works *)
     168(* this will be called in case -no-cost-tern is active. *)
     169let rec side_effect_expr_of_cost_expr prefix cost_incr cont e_type = function
     170  | CostExpr.Exact k ->
     171    Clight.Expr(Clight.Ecall (cost_incr, const_int k, cont), e_type)
     172  | CostExpr.Ternary(index, cond, if_true, if_false) ->
     173    let id = CostLabel.make_id prefix index in
     174    let var = Clight.Expr(Clight.Evar id, int_typ) in
     175    let cond_e = expr_of_cost_gen_cond var cond in
     176    let rec_call = side_effect_expr_of_cost_expr prefix cost_incr cont e_type in
     177    let if_true_e = rec_call if_true in
     178    let if_false_e = rec_call if_false in
     179    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
     180
     181let rec stmt_of_cost_expr prefix cost_incr = function
     182  | CostExpr.Exact k -> Clight.Scall (None, cost_incr, [const_int k])
     183  | CostExpr.Ternary(index, cond, if_true, if_false) ->
     184    let id = CostLabel.make_id prefix index in
     185    let var = Clight.Expr(Clight.Evar id, int_typ) in
     186    let cond_e = expr_of_cost_gen_cond var cond in
     187    let if_true_s = stmt_of_cost_expr prefix cost_incr if_true in
     188    let if_false_s = stmt_of_cost_expr prefix cost_incr if_false in
     189    Clight.Sifthenelse (cond_e, if_true_s, if_false_s)
    157190
    158191(* Instrument an expression. *)
    159192
    160 let rec instrument_expr l_ind cost_mapping cost_incr e =
    161   let Clight.Expr (e, t) = e in
    162         let e' = instrument_expr_descr l_ind cost_mapping cost_incr e in
    163         Clight.Expr (e', t)
    164 and instrument_expr_descr l_ind cost_mapping cost_incr e = match e with
    165   | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
    166   | Clight.Esizeof _ -> e
    167   | Clight.Ederef e ->
    168       let e' = instrument_expr l_ind cost_mapping cost_incr e in
    169       Clight.Ederef e'
    170   | Clight.Eaddrof e ->
    171       let e' = instrument_expr l_ind cost_mapping cost_incr e in
    172       Clight.Eaddrof e'
    173   | Clight.Eunop (op, e) ->
    174       let e' = instrument_expr l_ind cost_mapping cost_incr e in
    175       Clight.Eunop (op, e')
    176   | Clight.Ebinop (op, e1, e2) ->
    177       let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
    178       let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
    179       Clight.Ebinop (op, e1', e2')
    180   | Clight.Ecast (t, e) ->
    181       let e' = instrument_expr l_ind cost_mapping cost_incr e in
    182       Clight.Ecast (t, e')
    183   | Clight.Econdition (e1, e2, e3) ->
    184       let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
    185       let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
    186       let e3' = instrument_expr l_ind cost_mapping cost_incr e3 in
    187       Clight.Econdition (e1', e2', e3')
    188   | Clight.Eandbool (e1, e2) ->
    189       let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
    190       let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
    191       Clight.Eandbool (e1', e2')
    192   | Clight.Eorbool (e1, e2) ->
    193       let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
    194       let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
    195       Clight.Eorbool (e1', e2')
    196   | Clight.Efield (e, x) ->
    197       let e' = instrument_expr l_ind cost_mapping cost_incr e in
    198       Clight.Efield (e', x)
    199   | Clight.Ecost (lbl, e) ->
    200       let e' = instrument_expr l_ind cost_mapping cost_incr e in
    201             let atom = lbl.CostLabel.name in
    202             let cost =
    203                 try
    204                     CostLabel.Atom.Map.find atom cost_mapping
    205                 with (* if atom is not present, then map to 0 *)
    206                     | Not_found -> CostExpr.Exact 0 in
    207       if cost = CostExpr.Exact 0 then let Clight.Expr (e'', _) = e' in e''
    208       else let cost = expr_of_cost_expr l_ind cost in
    209                   Clight.Ecall (cost_incr, cost, e')
    210   | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *)
     193(* FIXME: follow cost_tern option *)
     194let instrument_expr cost_tern l_ind cost_mapping cost_incr =
     195  let f_expr (Clight.Expr(ed, et) as e) sub_res = match ed, sub_res with
     196  | Clight.Ecost (lbl, _), e' :: _ ->
     197    let atom = lbl.CostLabel.name in
     198    let cost =
     199      try
     200        CostLabel.Atom.Map.find atom cost_mapping
     201      with (* if atom is not present, then map to 0 *)
     202        | Not_found -> CostExpr.Exact 0 in
     203    if cost = CostExpr.Exact 0 then e' else
     204      if cost_tern then
     205        let cost = expr_of_cost_expr l_ind cost in
     206        Clight.Expr(Clight.Ecall (cost_incr, cost, e'), et)
     207      else
     208        side_effect_expr_of_cost_expr l_ind cost_incr e' et cost
     209  | Clight.Ecall (_, _, _), _ -> assert false (* Should not happen. *)
     210  | _ -> ClightFold.expr_fill_exprs e sub_res in
     211  ClightFold.expr2 f_expr
    211212
    212213let loop_increment prefix depth body = match depth  with
    213         | None -> body
    214         | Some d ->
    215                 let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
    216                 let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in
    217                 Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1)))
    218                
     214  | None -> body
     215  | Some d ->
     216    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
     217    let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in
     218    Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1)))
     219     
    219220let loop_reset_index prefix depth loop = match depth with
    220         | None -> loop
    221         | Some d ->
     221  | None -> loop
     222  | Some d ->
    222223    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
    223224    Clight.Ssequence(Clight.Sassign(id, const_int 0), loop)
     
    226227(* Instrument a statement. *)
    227228
    228 let rec instrument_body l_ind cost_mapping cost_incr stmt = match stmt with
    229   | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
    230   | Clight.Sgoto _ ->
    231     stmt
    232   | Clight.Sassign (e1, e2) ->
    233     let e1' = instrument_expr l_ind cost_mapping cost_incr e1 in
    234     let e2' = instrument_expr l_ind cost_mapping cost_incr e2 in
    235     Clight.Sassign (e1', e2')
    236   | Clight.Scall (eopt, f, args) ->
    237     let eopt' = match eopt with
    238       | None -> None
    239       | Some e -> Some (instrument_expr l_ind cost_mapping cost_incr e) in
    240     let f' = instrument_expr l_ind cost_mapping cost_incr f in
    241     let args' = List.map (instrument_expr l_ind cost_mapping cost_incr) args in
    242     Clight.Scall (eopt', f', args')
    243   | Clight.Ssequence (s1, s2) ->
    244     Clight.Ssequence (instrument_body l_ind cost_mapping cost_incr s1,
    245                       instrument_body l_ind cost_mapping cost_incr s2)
    246   | Clight.Sifthenelse (e, s1, s2) ->
    247     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    248     let s1' = instrument_body l_ind cost_mapping cost_incr s1 in
    249     let s2' = instrument_body l_ind cost_mapping cost_incr s2 in
    250     Clight.Sifthenelse (e', s1', s2')
    251   | Clight.Swhile (i, e, s) ->
    252     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    253     let s' = instrument_body l_ind cost_mapping cost_incr s in
    254                 let s' = loop_increment l_ind i s' in
    255     loop_reset_index l_ind i (Clight.Swhile (None, e', s'))
    256   | Clight.Sdowhile (i, e, s) ->
    257     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    258     let s' = instrument_body l_ind cost_mapping cost_incr s in
    259     let s' = loop_increment l_ind i s' in
    260     loop_reset_index l_ind i (Clight.Sdowhile (None, e', s'))
    261   | Clight.Sfor (i, s1, e, s2, s3) ->
    262     let s1' = instrument_body l_ind cost_mapping cost_incr s1 in
    263     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    264     let s2' = instrument_body l_ind cost_mapping cost_incr s2 in
    265     let s3' = instrument_body l_ind cost_mapping cost_incr s3 in
    266     let s3' = loop_increment l_ind i s3' in
    267                 loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3'))
    268   | Clight.Sreturn (Some e) ->
    269     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    270     Clight.Sreturn (Some e')
    271   | Clight.Sswitch (e, ls) ->
    272     let e' = instrument_expr l_ind cost_mapping cost_incr e in
    273     let ls' = instrument_ls l_ind cost_mapping cost_incr ls in
    274     Clight.Sswitch (e', ls')
    275   | Clight.Slabel (lbl, s) ->
    276     let s' = instrument_body l_ind cost_mapping cost_incr s in
    277     Clight.Slabel (lbl, s')
    278   | Clight.Scost (lbl, s) ->
     229(* not using ClightFold as l_ind changes through loops *)
     230let rec instrument_body cost_tern l_ind cost_mapping cost_incr stmt =
     231  let instr_expr = instrument_expr cost_tern l_ind cost_mapping cost_incr in
     232  let instr_body = instrument_body cost_tern l_ind cost_mapping cost_incr in
     233  match stmt with
     234    | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
     235    | Clight.Sgoto _ ->
     236      stmt
     237    | Clight.Sassign (e1, e2) ->
     238      let e1' = instr_expr e1 in
     239      let e2' = instr_expr e2 in
     240      Clight.Sassign (e1', e2')
     241    | Clight.Scall (eopt, f, args) ->
     242      let eopt' = Option.map instr_expr eopt in
     243      let f' = instr_expr f in
     244      let args = List.map (instr_expr) args in
     245      Clight.Scall (eopt', f', args)
     246    | Clight.Ssequence (s1, s2) ->
     247      Clight.Ssequence (
     248        instr_body s1,
     249        instr_body s2)
     250    | Clight.Sifthenelse (e, s1, s2) ->
     251      let e' = instr_expr e in
     252      let s1' = instr_body s1 in
     253      let s2' = instr_body s2 in
     254      Clight.Sifthenelse (e', s1', s2')
     255    | Clight.Swhile (i, e, s) ->
     256      let e' = instr_expr e in
     257      let s' = instr_body s in
     258      let s' = loop_increment l_ind i s' in
     259      loop_reset_index l_ind i (Clight.Swhile (None, e', s'))
     260    | Clight.Sdowhile (i, e, s) ->
     261      let e' = instr_expr e in
     262      let s' = instr_body s in
     263      let s' = loop_increment l_ind i s' in
     264      loop_reset_index l_ind i (Clight.Sdowhile (None, e', s'))
     265    | Clight.Sfor (i, s1, e, s2, s3) ->
     266      let s1' = instr_body s1 in
     267      let e' = instr_expr e in
     268      let s2' = instr_body s2 in
     269      let s3' = instr_body s3 in
     270      let s3' = loop_increment l_ind i s3' in
     271      loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3'))
     272    | Clight.Sreturn (Some e) ->
     273      let e' = instr_expr e in
     274      Clight.Sreturn (Some e')
     275    | Clight.Sswitch (e, ls) ->
     276      let e' = instr_expr e in
     277      let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
     278      Clight.Sswitch (e', ls')
     279    | Clight.Slabel (lbl, s) ->
     280      let s' = instr_body s in
     281      Clight.Slabel (lbl, s')
     282    | Clight.Scost (lbl, s) ->
    279283    (* Keep the cost label in the code. *)
    280     let s' = instrument_body l_ind cost_mapping cost_incr s in
    281                 let atom = lbl.CostLabel.name in
    282                 let cost =
    283                         try
    284                                 CostLabel.Atom.Map.find atom cost_mapping
    285                         with (* if atom is not present, then map to 0 *)
    286                                 | Not_found -> CostExpr.Exact 0 in
    287                 let cost = expr_of_cost_expr l_ind cost in
    288     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    289     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    290     Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, [cost]), s'))
    291   (*
    292     let s' = instrument_body l_ind cost_mapping cost_incr s in
    293     let incr = CostLabel.Map.find lbl cost_mapping in
    294     if incr = 0 then s'
    295     else
    296     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    297     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    298     let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
    299     Clight.Ssequence (Clight.Scall (None, f, args), s')
    300   *)
    301   (*
    302     instrument_body l_ind cost_mapping cost_incr s
    303   *)
    304 and instrument_ls l_ind cost_mapping cost_incr = function
     284      let s' = instr_body s in
     285      let atom = lbl.CostLabel.name in
     286      let cost =
     287        try
     288          CostLabel.Atom.Map.find atom cost_mapping
     289        with (* if atom is not present, then map to 0 *)
     290          | Not_found -> CostExpr.Exact 0 in
     291      let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
     292      let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
     293      let cost_stmt =
     294        if not cost_tern then stmt_of_cost_expr l_ind f cost else
     295        let cost = expr_of_cost_expr l_ind cost in
     296        Clight.Scall(None, f, [cost]) in
     297      Clight.Scost (lbl, Clight.Ssequence (cost_stmt, s'))
     298(*
     299  let s' = instrument_body l_ind cost_mapping cost_incr s in
     300  let incr = CostLabel.Map.find lbl cost_mapping in
     301  if incr = 0 then s'
     302  else
     303  let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
     304  let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
     305  let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
     306  Clight.Ssequence (Clight.Scall (None, f, args), s')
     307*)
     308(*
     309  instrument_body l_ind cost_mapping cost_incr s
     310*)
     311and instrument_ls cost_tern l_ind cost_mapping cost_incr = function
    305312  | Clight.LSdefault s ->
    306     let s' = instrument_body l_ind cost_mapping cost_incr s in
     313    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
    307314    Clight.LSdefault s'
    308315  | Clight.LScase (i, s, ls) ->
    309     let s' = instrument_body l_ind cost_mapping cost_incr s in
    310     let ls' = instrument_ls l_ind cost_mapping cost_incr ls in
     316    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
     317    let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
    311318    Clight.LScase (i, s', ls')
    312                
     319     
    313320let rec loop_indexes_defs prefix max_depth =
    314         if max_depth = 0 then [] else
    315         let max_depth = max_depth - 1 in
    316         let id = CostLabel.make_id prefix max_depth in
    317         (id, int_typ) :: loop_indexes_defs prefix max_depth
     321  if max_depth = 0 then [] else
     322    let max_depth = max_depth - 1 in
     323    let id = CostLabel.make_id prefix max_depth in
     324    (id, int_typ) :: loop_indexes_defs prefix max_depth
    318325
    319326let max_depth =
    320         let f_expr _ _ = () in
    321         let f_stmt stmt _ res_stmts =
    322                 let curr_max = List.fold_left max 0 res_stmts in
    323                 if curr_max > 0 then curr_max else     
    324                 match stmt with
    325                 | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_)
    326                 | Clight.Sfor(Some x,_,_,_,_) -> x + 1
    327                 | _ -> 0 in
    328         ClightFold.statement2 f_expr f_stmt
     327  let f_expr _ _ = () in
     328  let f_stmt stmt _ res_stmts =
     329    let curr_max = List.fold_left max 0 res_stmts in
     330    if curr_max > 0 then curr_max else 
     331      match stmt with
     332        | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_)
     333        | Clight.Sfor(Some x,_,_,_,_) -> x + 1
     334        | _ -> 0 in
     335  ClightFold.statement2 f_expr f_stmt
    329336
    330337(* Instrument a function. *)
    331338
    332 let instrument_funct l_ind cost_mapping cost_incr (id, def) =
     339let instrument_funct cost_tern  l_ind cost_mapping cost_incr (id, def) =
    333340  let def = match def with
    334341    | Clight.Internal def ->
    335         let max_depth = max_depth def.Clight.fn_body in
    336         let vars = loop_indexes_defs l_ind max_depth in
    337         let vars = List.rev_append vars def.Clight.fn_vars in
    338         let body = instrument_body l_ind cost_mapping cost_incr def.Clight.fn_body in
    339         Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
     342      let max_depth = max_depth def.Clight.fn_body in
     343      let vars = loop_indexes_defs l_ind max_depth in
     344      let vars = List.rev_append vars def.Clight.fn_vars in
     345      let body = def.Clight.fn_body in
     346      let body =
     347        instrument_body cost_tern l_ind cost_mapping cost_incr body in
     348      Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
    340349    | Clight.External _ -> def
    341350  in
     
    370379  flush cout ;
    371380  close_out cout
    372        
    373        
     381   
     382   
    374383(** [instrument prog cost_map] instruments the program [prog]. First a fresh
    375384    global variable --- the so-called cost variable --- is added to the program.
     
    378387    name of the cost variable and the name of the cost increment function. *)
    379388
    380 let instrument p cost_mapping =
     389let instrument cost_tern p cost_mapping =
    381390
    382391  (* Create a fresh 'cost' variable. *)
     
    384393  let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
    385394  let cost_decl = cost_decl cost_id in
    386        
    387         (* Create a fresh loop index prefix *)
    388         let names = StringTools.Set.add cost_id names in
     395
     396  (* Create a fresh loop index prefix *)
     397  let names = StringTools.Set.add cost_id names in
    389398  let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in
    390399
     
    396405
    397406  (* Turn the mapping from indexed cost labels to integers into one from *)
    398         (* cost atoms to cost expresisons *)
    399         let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in
     407  (* cost atoms to cost expresisons *)
     408  let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in
    400409
    401410  (* Instrument each function *)
    402411  let prog_funct = p.Clight.prog_funct in
    403         let prog_funct =
    404     List.map (instrument_funct l_ind cost_mapping cost_incr) prog_funct in
     412  let prog_funct =
     413    let f = instrument_funct cost_tern l_ind cost_mapping cost_incr in
     414    List.map f prog_funct in
    405415
    406416  (* Glue all this together. *)
     
    416426  let tmp_file = Filename.temp_file "clight_instrument" ".c" in
    417427  save_tmp tmp_file (ClightPrinter.print_program p') ;
    418   let res = ClightParser.process tmp_file in
     428  let p' = ClightParser.process tmp_file in
    419429  Misc.SysExt.safe_remove tmp_file ;
    420   (res, cost_id, cost_incr)
     430  (p', cost_id, cost_incr)
Note: See TracChangeset for help on using the changeset viewer.