Ignore:
Timestamp:
Nov 15, 2011, 5:12:58 PM (8 years ago)
Author:
tranquil
Message:

branched a version of the plug-in that is compatible with the indexed labels
branch of the compiler, taking into account dependent costs. It is not
backward compatible as it extracts loop indexes, and fails if it does not
find them.

Further modifications:

  • Some more reductions of cost_value terms to further simplify expressions
Location:
Deliverables/D5.1/cost-plug-in-indexed-labels-branch
Files:
1 edited
1 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D5.1/cost-plug-in-indexed-labels-branch/plugin/compute.ml

    r1462 r1508  
    203203    [env]. *)
    204204
    205 let are_parameters env fun_name set =
    206   let f x res = res && (is_parameter env fun_name x) in
    207   StringTools.Set.fold f set true
     205let are_parameters env fun_name =
     206        StringTools.Set.for_all (is_parameter env fun_name)
    208207
    209208let prototypes env =
     
    348347    represents. *)
    349348
    350 let cost_incr_cost = function
    351   | e :: _ ->
    352     (match e.Cil_types.enode with
    353       | Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
    354         Cost_value.Int (Int64.to_int i)
    355       | _ -> raise Cost_incr_arg_not_constant)
    356   | _ -> raise Cost_incr_arg_not_constant
     349let cost_incr_cost e =
     350  match e.Cil_types.enode with
     351    | Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
     352      Cost_value.Int (Int64.to_int i)
     353    | _ -> raise Cost_incr_arg_not_constant
    357354
    358355(** [call cost cost_incr f args] returns the cost of calling the function [f] on
     
    363360
    364361let call_cost cost_incr f args = match f.Cil_types.enode with
    365   | Cil_types.Lval (Cil_types.Var var, _)
     362  | Cil_types.Lval (Cil_types.Var var, Cil_types.NoOffset)
    366363      when var.Cil_types.vname = cost_incr ->
    367     cost_incr_cost args
    368   | Cil_types.Lval (Cil_types.Var var, _) ->
     364    cost_incr_cost (List.hd args)
     365  | Cil_types.Lval (Cil_types.Var var, Cil_types.NoOffset) ->
    369366    (try
    370367       let args = List.map Cost_value.of_cil_exp args in
     
    402399    the case of a loop initialization instruction. *)
    403400
    404 let extract_counter_and_init stmt_opt =
     401let extract_counter_and_init stmt2_opt stmt1_opt =
    405402  let error () = raise (Unsupported_loop "no initialization found") in
    406   match stmt_opt with
    407     | None -> error ()
    408     | Some stmt -> match stmt.Cil_types.skind with
    409         | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) ->
    410           (v.Cil_types.vname, Cost_value.of_cil_exp e)
     403  match stmt2_opt, stmt1_opt with
     404    | None, _ | _, None -> error ()
     405    | Some stmt2, Some stmt1 ->
     406      match stmt2.Cil_types.skind, stmt1.Cil_types.skind with
     407        | Cil_types.Instr (Cil_types.Set ((Cil_types.Var i, _), z, _)),
     408          Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) ->
     409          (match Cost_value.of_cil_exp z with
     410            | Cost_value.Int 0 ->
     411              (v.Cil_types.vname, i.Cil_types.vname, Cost_value.of_cil_exp e)
     412            | _ -> error())
    411413        | _ -> error ()
    412414
     
    422424
    423425let exp_is_var name e = match e.Cil_types.enode with
    424   | Cil_types.Lval (Cil_types.Var v, _) -> v.Cil_types.vname = name
     426  | Cil_types.Lval (Cil_types.Var v, Cil_types.NoOffset) ->
     427    v.Cil_types.vname = name
    425428  | _ -> false
     429
     430let var_of_exp e = match e.Cil_types.enode with
     431  | Cil_types.Lval (Cil_types.Var v, Cil_types.NoOffset) ->
     432    v.Cil_types.vname
     433  | _ -> invalid_arg "var_of_exp"
     434
     435let const_of_exp e =
     436  match e.Cil_types.enode with
     437    | Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
     438      Int64.to_int i
     439    | _ -> invalid_arg "const_of_exp"
    426440
    427441(** [starts_with_break block] returns true iff the block [block] starts with a
     
    453467  | _ :: l -> last l
    454468
    455 (** [last_stmt block] returns the last statement of the block [block], if
     469let rec last_2 = function
     470  | [] | [_] -> raise (Failure "Compute.last_2")
     471  | [e1 ; e2] -> (e1, e2)
     472  | _ :: l -> last_2 l
     473
     474let rec last_stmt stmt = match stmt.Cil_types.skind with
     475  | Cil_types.Block block ->
     476    last_stmt (last block.Cil_types.bstmts)
     477  | _ -> stmt
     478
     479(** [last_2_stmt block] returns the last two statement of the block [block], if
    456480    any. *)
    457481
    458 let last_stmt block = match block.Cil_types.bstmts with
    459   | [] -> raise (Unsupported_loop "no increment instruction")
    460   | stmts -> last stmts
     482let last_2_stmt block = match block.Cil_types.bstmts with
     483  | [] | [_] -> raise (Unsupported_loop "no increment instruction")
     484  | stmts ->
     485    let (snd_last, last) = last_2 stmts in
     486    (last_stmt snd_last, last)
     487
    461488
    462489(** [extract_added_value counter e] supposes that the expression [e] is either
     
    477504    used to extract the increment in a loop body. *)
    478505
    479 let extract_increment counter block =
    480   match (last_stmt block).Cil_types.skind with
    481     | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _))
    482         when v.Cil_types.vname = counter ->
    483       extract_added_value counter e
     506let extract_increment counter index block =
     507  let (snd_last, last) = last_2_stmt block in
     508  match snd_last.Cil_types.skind, last.Cil_types.skind with
     509    | Cil_types.Instr (Cil_types.Set ((Cil_types.Var i, _), o, _)),
     510      Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _))
     511      when v.Cil_types.vname = counter && i.Cil_types.vname = index ->
     512      (match extract_added_value index o with
     513        | Cost_value.Int 1 -> extract_added_value counter e
     514        | _ -> raise (Unsupported_loop "loop index malformation"))
    484515    | _ -> raise (Unsupported_loop "no increment instruction found")
    485516
     
    531562    "the value of a parameter in a loop expression may be modified"
    532563
     564let rec mk_loop_cost_index index k v inc cost =
     565  let round_up h a b =
     566    let h_mod_a = h mod a in
     567    let b_mod_a = b mod a in
     568    h - h_mod_a + b_mod_a + if h_mod_a <= b_mod_a then 0 else a in
     569  match cost with
     570  | Cost_value.CostCond (i, cond, tif, telse) when i <> index ->
     571    let tif = mk_loop_cost_index index k v inc tif in
     572    let telse = mk_loop_cost_index index k v inc telse in
     573    Cost_value.CostCond (i, cond, tif, telse)
     574  | Cost_value.CostCond (_, Cost_value.Ceq h, _, telse) when k > h ->
     575    mk_loop_cost_index index k v inc telse
     576  | Cost_value.CostCond (_, Cost_value.Ceq h, tif, telse) when k = h ->
     577    (* let sum = *)
     578      Cost_value.add tif (mk_loop_cost_index index (k+inc) v inc telse) (* in *)
     579    (* Cost_value.Cond(v, Cost_value.Le, Cost_value.Int k, Cost_value.Int 0, sum) *)
     580  | Cost_value.CostCond (_, Cost_value.Ceq h, tif, telse)
     581    when (h - k) mod inc = 0 ->
     582    let tif' = mk_loop_cost_index index k v inc telse in
     583    let h_val = Cost_value.Int h in
     584    let sum =
     585      Cost_value.add tif (mk_loop_cost_index index (h + inc) v inc telse) in
     586    let telse' =
     587      Cost_value.add (mk_loop_cost_index index k h_val inc telse) sum in
     588    Cost_value.Cond(v, Cost_value.Lt, Cost_value.Int h, tif', telse')
     589  | Cost_value.CostCond (_, Cost_value.Ceq _, _, telse) ->
     590    mk_loop_cost_index index k v inc telse
     591  | Cost_value.CostCond (_, Cost_value.Cgeq h, tif, _) when k >= h ->
     592    mk_loop_cost_index index k v inc tif
     593  | Cost_value.CostCond (_, Cost_value.Cgeq h, tif, telse) ->
     594    let tif' = mk_loop_cost_index index k v inc telse in
     595    let h_val = Cost_value.Int h in
     596    let telse' =
     597      Cost_value.add
     598        (mk_loop_cost_index index k h_val inc telse)
     599        (mk_loop_cost_index index (round_up h inc k) v inc tif) in
     600    Cost_value.Cond(v, Cost_value.Lt, Cost_value.Int h, tif', telse')
     601  (* I'm supposing unrolling is never repeated *)
     602  | Cost_value.CostCond (_, Cost_value.Cmod (a, b), tif, telse) when inc = 1 ->
     603    let k' = round_up k a b in
     604    let sub = Cost_value.sub
     605      (mk_loop_cost_index index k' v a tif)
     606      (mk_loop_cost_index index k' v a telse) in
     607    Cost_value.add (mk_loop_cost_index index k v 1 telse) sub
     608  | Cost_value.CostCond (_, Cost_value.Cmod (a, b), tif, telse)
     609    when inc = a ->
     610    let next = if k mod inc = b then tif else telse in
     611    mk_loop_cost_index index k v inc next
     612  | Cost_value.CostCond (_, Cost_value.Cmod _, _, _) ->
     613    raise (Unsupported_loop "possible repeated unrolling")
     614  | Cost_value.CostCond (_, Cost_value.Cgeqmod (h, a, b), tif, telse)
     615    when k >= h ->
     616    let next =
     617      Cost_value.CostCond (index, Cost_value.Cmod (a, b), tif, telse) in
     618    mk_loop_cost_index index k v inc next
     619  | Cost_value.CostCond (_, Cost_value.Cgeqmod (h, a, b), tif, telse) ->
     620    let tif' = mk_loop_cost_index index k v inc telse in
     621    let h_val = Cost_value.Int h in
     622    let next =
     623      Cost_value.CostCond (index, Cost_value.Cmod (a, b), tif, telse) in
     624    let telse' =
     625      Cost_value.add
     626        (mk_loop_cost_index index k h_val inc telse)
     627        (mk_loop_cost_index index (round_up h inc k) v inc next) in
     628    Cost_value.Cond(v, Cost_value.Lt, Cost_value.Int h, tif', telse')
     629  | Cost_value.CostCond _ ->
     630    raise (Unsupported_loop "unsupported cost condition")
     631  | _ ->
     632    let k_val = Cost_value.Int k in
     633    let inc_val = Cost_value.Int inc in
     634    let inc_val_m_1 = Cost_value.sub inc_val (Cost_value.Int 1) in
     635    let n = Cost_value.add (Cost_value.sub v k_val) inc_val_m_1 in
     636    let n = Cost_value.div n inc_val in
     637    Cost_value.mul n cost
     638    (* let zero = Cost_value.Int 0 in *)
     639    (* Cost_value.Cond (v, Cost_value.Gt, k_val, Cost_value.mul n cost, zero) *)
     640
    533641(** [mk_loop_cost init_value increment body_cost] returns a function that, when
    534642    providing a current value of the loop counter, returns the current cost of a
     
    538646    cost of the loop. *)
    539647
    540 let mk_loop_cost init_value increment body_cost =
     648let mk_loop_cost init_value increment index body_cost =
    541649  fun i ->
    542650    let v = Cost_value.BinOp (Cost_value.Sub, i, init_value) in
    543651    let v = Cost_value.BinOp (Cost_value.Div, v, increment) in
    544     Cost_value.BinOp (Cost_value.Mul, v, body_cost)
     652    (* this will in general reduce the steps and the size of amalgamation *)
     653    let e = StringTools.Map.empty in
     654    let body_cost = Cost_value.reduce e e e body_cost in
     655    let body_cost = Cost_value.amalgamation body_cost in
     656    mk_loop_cost_index index 0 v 1 body_cost
     657
     658
    545659
    546660(** [last_value rel init_value exit_value increment] returns the last value
     
    563677  Cost_value.BinOp (Cost_value.Add, res, v3)
    564678
    565 (** [stmt_cost fun_name cost_incr env previous_stmt stmt] returns the
     679(** [stmt_cost fun_name cost_incr ind_set env prev2 prev1 stmt] returns the
    566680    requirements and the cost of the statement [stmt] of the function [fun_name]
    567681    in the environment [env] when [cost_incr] is the name of the cost update
    568     function and [previous_stmt] is the (optional) previous statement. *)
    569 
    570 let rec stmt_cost fun_name cost_incr env previous_stmt stmt
     682    function, [ind_set] is the set of loop indices encountered at this point
     683    (which will be at most a singleton until nested loops are not supported)
     684    and [prev2] and [prev1] are the (optional) previous statements. *)
     685
     686let rec stmt_cost fun_name cost_incr ind_set env prev2 prev1 stmt
    571687    : require list * Cost_value.t =
    572   let block_cost block = block_cost fun_name cost_incr env block in
     688  let block_cost block = block_cost fun_name cost_incr ind_set env block in
    573689
    574690  let rec aux stmt = match stmt.Cil_types.skind with
    575 
    576691    | Cil_types.Instr instr -> ([], instr_cost cost_incr instr)
    577692
    578693    | Cil_types.Goto (stmt_ref, _) -> goto_cost !stmt_ref
    579694
    580     | Cil_types.If (_, block1, block2, _) ->
     695    | Cil_types.If (e, block1, block2, _) ->
    581696      let (requires1, cost1) = block_cost block1 in
    582697      let (requires2, cost2) = block_cost block2 in
    583       (requires1 @ requires2, Cost_value.BinOp (Cost_value.Max, cost1, cost2))
     698      let cost =
     699        match Cost_value.mk_cost_cond e with
     700          | Some (ind, cost_cond) when List.mem ind ind_set ->
     701            Cost_value.CostCond (ind, cost_cond, cost1, cost2)
     702          | _ -> Cost_value.max cost1 cost2 in
     703      (requires1 @ requires2, cost)
    584704
    585705    | Cil_types.Loop (_, block, _, _, _) ->
    586706      (* if has_loop block then raise Nested_loops
    587       else *) loop_cost fun_name cost_incr env previous_stmt block
     707      else *) loop_cost fun_name cost_incr ind_set env prev2 prev1 block
    588708
    589709    | Cil_types.Block block -> block_cost block
     
    594714    | Cil_types.Switch _ -> raise (Unsupported "switch")
    595715
    596     | Cil_types.UnspecifiedSequence _ ->
    597       raise (Unsupported "unspecified sequence")
     716    | Cil_types.UnspecifiedSequence l ->
     717      (* not interested in execution order, costs should reflect the
     718         particular order chosen by the compiler *)
     719      block_cost (Cil.block_from_unspecified_sequence l)
    598720
    599721    | Cil_types.TryFinally _ -> raise (Unsupported "try finally")
     
    603725  aux stmt
    604726
    605 (** [block_cost fun_name cost_incr env block] returns the requirements and the
    606     cost of the block [block] of the function [fun_name] in the environment
    607     [env] when [cost_incr] is the name of the cost update function. *)
    608 
    609 and block_cost fun_name cost_incr env block : require list * Cost_value.t =
    610   let f (previous_stmt, requires, cost) stmt =
     727(** [block_cost fun_name cost_incr ind_set env block] returns the requirements
     728    and the cost of the block [block] of the function [fun_name] in the
     729    environment [env] when [cost_incr] is the name of the cost update function
     730    and [ind_set] is the set of loop indices whose scope we are in. *)
     731
     732and block_cost fun_name cost_incr ind_set env block
     733    : require list * Cost_value.t =
     734  let f (prev2, prev1, requires, cost) stmt =
    611735    let (added_requires, added_cost) =
    612       stmt_cost fun_name cost_incr env previous_stmt stmt in
    613     (Some stmt,
     736      stmt_cost fun_name cost_incr ind_set env prev2 prev1 stmt in
     737    (prev1, Some stmt,
    614738     requires @ added_requires,
    615      Cost_value.BinOp (Cost_value.Add, cost, added_cost)) in
    616   let (_, requires, cost) =
    617     List.fold_left f (None, [], Cost_value.Int 0) block.Cil_types.bstmts in
     739     Cost_value.add cost added_cost) in
     740  let (_, _, requires, cost) =
     741    List.fold_left f (None,None,[],Cost_value.Int 0) block.Cil_types.bstmts in
    618742  (requires, cost)
    619743
    620 (** [loop_infos fun_name cost_incr env previous_stmt block] returns all the
    621     extracted cost information of a loop in function [fun_name], in environment
    622     [env], with [cost_incr] for the name of the cost update function, with
    623     (optional) previous statement [previous_stmt] and of body [block]. The
     744(** [loop_infos fun_name cost_incr ind_set env prev2 prev1 block] returns all
     745    the extracted cost information of a loop in function [fun_name], in
     746    environment [env], with [cost_incr] for the name of the cost update
     747    function and [ind_set] for the loop indexes whose scope we are in, with
     748    (optional) previous statements [prev2], [prev1] and of body [block]. The
    624749    returned information are: the requirements for the loop termination, the
    625     loop counter, its first value, the comparison relation of the guard, the
    626     compared value in the guard, the increment and a function that, provided a
    627     current value for the loop counter, returns the current cost of the loop. *)
    628 
    629 and loop_infos fun_name cost_incr env previous_stmt block
    630     : require list * string * Cost_value.t * Cost_value.relation *
     750    loop counter, the loop index, its first value, the comparison relation of
     751    the guard, the compared value in the guard, the increment and a function
     752    that, provided a current value for the loop counter, returns the current
     753    cost of the loop. *)
     754
     755and loop_infos fun_name cost_incr ind_set env prev2 prev1 block
     756    : require list * string * string * Cost_value.t * Cost_value.relation *
    631757      Cost_value.t * Cost_value.t * (Cost_value.t -> Cost_value.t) =
    632   let (counter, init_value) = extract_counter_and_init previous_stmt in
     758  let (counter, index, init_value) = extract_counter_and_init prev2 prev1 in
     759  let ind_set = index :: ind_set in
    633760  let (rel, exit_value) = extract_guard counter block in
    634   let increment = extract_increment counter block in
     761  let increment = extract_increment counter index block in
    635762  check_supported_loop
    636763    fun_name env counter init_value exit_value increment block ;
    637   let (requires, body_cost) = block_cost fun_name cost_incr env block in
    638   let requires = [(rel, init_value, exit_value, increment)] @ requires in
    639   let cost = mk_loop_cost init_value increment body_cost in
    640   (requires, counter, init_value, rel, exit_value, increment, cost)
    641 
    642 (** [loop_cost fun_name cost_incr env previous_stmt block] returns the
     764  let (requires, body_cost) = block_cost fun_name cost_incr ind_set env block in
     765  let requires = (rel, init_value, exit_value, increment) :: requires in
     766  let cost = mk_loop_cost init_value increment index body_cost in
     767  (requires, counter, index, init_value, rel, exit_value, increment, cost)
     768
     769(** [loop_cost fun_name cost_incr ind_set env prev2 prev1 block] returns the
    643770    requirements and the cost of the loop of body [block] in the function
    644771    [fun_name] in the environment [env] when [cost_incr] is the name of the cost
    645     update function and [previous_stmt] is the (optional) previous statement. *)
    646 
    647 and loop_cost fun_name cost_incr env previous_stmt block
     772    update function, [ind_set] is the set of loop indexes whose scope we are in
     773    and [prev2] and [prev1] are the (optional) previous statements. *)
     774
     775and loop_cost fun_name cost_incr ind_set env prev2 prev1 block
    648776    : require list * Cost_value.t =
    649   let (requires, _, init_value, rel, exit_value, increment, cost) =
    650     loop_infos fun_name cost_incr env previous_stmt block in
     777  let (requires, _, _,  init_value, rel, exit_value, increment, cost) =
     778    loop_infos fun_name cost_incr ind_set env prev2 prev1 block in
    651779  let cost = cost (last_value rel init_value exit_value increment) in
    652780  let cost =
     
    707835    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
    708836    let block = fundec.Cil_types.sbody in
    709     let cost = block_cost fun_name cost_incr env block in
     837    let cost = block_cost fun_name cost_incr [] env block in
    710838    costs := StringTools.Map.add fun_name cost !costs ;
    711839    Cil.SkipChildren
     
    735863(*** Add annotations ***)
    736864
    737 let add_tmp_cost_init env tmp_cost stmt =
     865let add_tmp_cost_init env tmp_cost obj stmt =
    738866  let lval = Cil.var tmp_cost in
    739867  let e =
     
    743871    Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in
    744872  let new_stmt = Cil.mkStmt new_stmt in
     873  obj#chop_index ;
    745874  Cil.mkStmt (Cil_types.Block (Cil.mkBlock [new_stmt ; stmt]))
    746875
     876(* will transform requirements (rel, init_value, exit_value, increment) *)
     877(* into (init_value rel exit_value) ⇒ (increment rel' 0) where rel' is  *)
     878(* the strict version of rel. If this requirement is trivially satisfied *)
     879(* it is suppressed *)
    747880let make_requires requires =
    748   let f (rel, init_value, exit_value, increment) =
    749     let init_value = Cost_value.to_cil_term init_value in
    750     let exit_value = Cost_value.to_cil_term exit_value in
    751     let increment = Cost_value.to_cil_term increment in
     881  let f (rel, init_value, exit_value, increment) reqs =
    752882    let rel' = Cost_value.mk_strict rel in
    753     let rel = Cost_value.cil_rel_of_rel rel in
    754     let rel' = Cost_value.cil_rel_of_rel rel' in
    755     let t1 = Logic_const.prel (rel, init_value, exit_value) in
    756     let t2 = Logic_const.prel (rel', Cost_value.tinteger 0, increment) in
    757     Logic_const.pimplies (t1, t2) in
    758   List.map f requires
     883    match init_value, exit_value, increment with
     884      | _, _, Cost_value.Int i
     885        when Cost_value.bool_fun_of_relation rel' 0 i ->
     886        reqs
     887      | Cost_value.Int i, Cost_value.Int e, _
     888        when not (Cost_value.bool_fun_of_relation rel i e) ->
     889        reqs
     890      | _ ->
     891        let rel = Cost_value.cil_rel_of_rel rel in
     892        let rel' = Cost_value.cil_rel_of_rel rel' in
     893        let init_value = Cost_value.to_cil_term init_value in
     894        let exit_value = Cost_value.to_cil_term exit_value in
     895        let increment = Cost_value.to_cil_term increment in
     896        let t1 = Logic_const.prel (rel, init_value, exit_value) in
     897        let t2 = Logic_const.prel (rel', Cost_value.tinteger 0, increment) in
     898        Logic_const.pimplies (t1, t2) :: reqs in
     899  List.fold_right f requires []
    759900
    760901let add_spec pres post spec =
     
    846987let annot_loop
    847988    extern_costs tmp_cost cost_id cost_incr env costs obj stmt
    848     previous_stmt block =
     989    prev2 prev1 block =
    849990  let (_, costs) = StringTools.Map.split_couple costs in
    850991  let prots = prototypes env in
    851992  let fun_name = current_fun_name obj in
    852   let (_, counter, init_value, rel, exit_value, increment, cost) =
    853     loop_infos fun_name cost_incr env previous_stmt block in
     993  let (_, counter, index, init_value, rel, exit_value, increment, cost) =
     994    loop_infos fun_name cost_incr obj#get_ind_set env prev2 prev1 block in
    854995  let invariant_counter_init_value =
    855996    mk_loop_invariant_counter_init_value
     
    8661007    mk_loop_variant extern_costs costs prots counter init_value rel exit_value
    8671008      increment in
     1009  obj#push_index index;
    8681010  add_loop_annot obj stmt invariant_counter_init_value ;
    8691011  add_loop_annot obj stmt invariant_counter_last_value ;
     
    8761018
    8771019  val mutable tmp_costs : Cil_types.varinfo list = []
    878   val mutable previous_stmt = None
     1020  val mutable prev2 = None
     1021  val mutable prev1 = None
     1022  val mutable ind_set : string list = []
     1023
     1024  method get_ind_set = ind_set
     1025  method push_index index = ind_set <- index :: ind_set
     1026  method chop_index = ind_set <- List.tl ind_set
    8791027
    8801028  method vstmt_aux stmt =
    881     let old_stmt = previous_stmt in
    882     previous_stmt <- Some stmt ;
     1029    let snd_last_stmt = prev2 in
     1030    let last_stmt = prev1 in
     1031    prev2 <- last_stmt ;
     1032    prev1 <- Some stmt ;
    8831033    match stmt.Cil_types.skind with
    8841034      | Cil_types.Loop (_, block, _, _, _) ->
     
    8891039        annot_loop
    8901040          extern_costs tmp_cost_id cost_id cost_incr env costs self stmt
    891           old_stmt block ;
    892         Cil.ChangeDoChildrenPost (stmt, add_tmp_cost_init env tmp_cost)
     1041          snd_last_stmt last_stmt block ;
     1042        Cil.ChangeDoChildrenPost (stmt, add_tmp_cost_init env tmp_cost self)
    8931043      | _ -> Cil.DoChildren
    8941044
     
    9101060    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
    9111061    tmp_costs <- make_freshes fundec (get_nb_loops env fun_name) cost_id ;
    912     previous_stmt <- None ;
     1062    prev2 <- None ;
     1063    prev1 <- None ;
    9131064    Cil.DoChildren
    9141065
     
    9161067
    9171068let add_annotations extern_costs fname cost_id cost_incr env costs =
    918   let add_annotations_prj =     
    919     File.create_project_from_visitor
    920       "cerco_add_annotations"
    921       (new add_annotations extern_costs cost_id cost_incr env costs) in
     1069  let add_annotations_prj =
     1070    let visitor =
     1071      new add_annotations extern_costs cost_id cost_incr env costs in
     1072    File.create_project_from_visitor "cerco_add_annotations"
     1073      (visitor :> Project.t -> Visitor.frama_c_visitor) in
    9221074  let f () =
    9231075    Parameters.CodeOutput.set fname ;
Note: See TracChangeset for help on using the changeset viewer.