Ignore:
Timestamp:
Nov 15, 2011, 5:12:58 PM (9 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:
4 edited
1 copied

Legend:

Unmodified
Added
Removed

  • Deliverables/D5.1/cost-plug-in-indexed-labels-branch/plugin/cerco.ml

    r1462 r1508  
    4545    | Some i -> i
    4646
    47 let acc_option lustre_option lustre_verify_option lustre_test_option =
    48   if lustre_verify_option || lustre_test_option then "-remove-lustre-externals "
    49   else
    50     if lustre_option then "-lustre "
    51     else ""
     47let acc_option
     48    noopt_option lustre_option lustre_verify_option lustre_test_option =
     49  Printf.sprintf "%s%s%s"
     50    (if noopt_option then "" else "-O ")
     51    (if lustre_verify_option || lustre_test_option then
     52      "-remove-lustre-externals "
     53    else if lustre_option then "-lustre " else "")
     54    "-no-cost-tern "
    5255
    5356(** [apply (filename, _)] apply CerCo's compiler on the file [filename]. The
    … …  
    5558    variable, and the name of the cost update function. *)
    5659
    57 let apply lustre_option lustre_verify_option lustre_test_option (filename, _)
     60let apply noopt_option lustre_option lustre_verify_option lustre_test_option
     61    (filename, _)
    5862    : Cabs.file * string * string * string * string StringTools.Map.t =
    5963  let annotated_ext = "-annotated.c" in
    … …  
    6569  let tmp_filename = fresh_multifile exts tmp_filename in
    6670  let acc_option =
    67     acc_option lustre_option lustre_verify_option lustre_test_option in
     71    acc_option noopt_option lustre_option
     72      lustre_verify_option lustre_test_option in
    6873  let com_acc =
    6974    "acc -a " ^ acc_option ^ "-o " ^ tmp_filename ^ " " ^ filename in

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

  • Deliverables/D5.1/cost-plug-in-indexed-labels-branch/plugin/cost.ml

    r1462 r1508  
    4343    let kind = `Tuning
    4444   end)
     45
     46module NoOpt = Self.False
     47  (struct
     48    let option_name = "-cost-no-opt"
     49    let help = "do not perform optimizations"
     50    let kind = `Tuning
     51   end)
    4552 
    4653module Lustre = Self.False
    … …  
    7279
    7380let run () =
     81  let noopt_option = NoOpt.get () in
    7482  let lustre_option = Lustre.get () in
    7583  let lustre_verify_option = Lustre_verify.get () in
    … …  
    8088        (Cabs.file * string * string * string * string StringTools.Map.t) list =
    8189      List.map
    82         (Cerco.apply lustre_option lustre_verify_option lustre_test_option)
     90        (Cerco.apply noopt_option lustre_option lustre_verify_option
     91           lustre_test_option)
    8392        files in
    8493    List.iter Compute.cost files

  • Deliverables/D5.1/cost-plug-in-indexed-labels-branch/plugin/cost_value.ml

    r1462 r1508  
    5757  | Max -> max
    5858
     59type cost_cond =
     60  | Ceq of int
     61  | Cgeq of int
     62  | Cmod of int * int
     63  | Cgeqmod of int * int * int
     64  | Cor of cost_cond * cost_cond
     65
    5966(** Cost values *)
    6067
    … …  
    6572  | BinOp of binop * t * t
    6673  | Cond of t * relation * t * t * t (* ternary expressions *)
     74  | CostCond of string * cost_cond * t * t (* ternary cost expressions *)
    6775  | CostOf of string * t list (* cost of a function: function name * args *)
    6876  | Any (* any other C expression *)
     77
     78let add t1 t2 = BinOp(Add, t1, t2)
     79let sub t1 t2 = BinOp(Sub, t1, t2)
     80let div t1 t2 = BinOp(Div, t1, t2)
     81let mul t1 t2 = BinOp(Mul, t1, t2)
     82let max t1 t2 = BinOp(Max, t1, t2)
    6983
    7084(** [abs v] return a cost value that represents the absolute value of [v].  *)
    … …  
    8094  | BinOp (_, v1, v2) -> [v1 ; v2]
    8195  | Cond (t1, _, t2, tif, telse) -> [t1 ; t2 ; tif ; telse]
     96  | CostCond (_, _, tif, telse) -> [tif ; telse]
    8297  | CostOf (_, args) -> args
    8398
    … …  
    91106  | Cond (_, rel, _, _, _), t1 :: t2 :: tif :: telse :: _ ->
    92107    Cond (t1, rel, t2, tif, telse)
     108  | CostCond (i, cond, _, _), tif :: telse :: _ -> CostCond(i, cond, tif, telse)
    93109  | CostOf (fun_name, _), _ -> CostOf (fun_name, subs)
    94110  | _ -> raise (Failure "Cost_value.fill_subs") (* wrong number of arguments *)
    … …  
    103119  f v subs_res
    104120
     121let rec string_of_cost_cond i = function
     122  | Ceq k -> Printf.sprintf "%s == %d" i k
     123  | Cgeq k -> Printf.sprintf "%s >= %d" i k
     124  | Cmod (a, b) -> Printf.sprintf "%s %% %d == %d" i a b
     125  | Cgeqmod (k, a, b) -> Printf.sprintf "%s >= %d && %s %% %d == %d" i k i a b
     126  | Cor (c1, c2) ->
     127    Printf.sprintf "(%s) || (%s)"
     128      (string_of_cost_cond i c1)
     129      (string_of_cost_cond i c2)
    105130
    106131let rec f_to_string v subs_res = match v, subs_res with
    … …  
    113138    Printf.sprintf "(%s %s %s)? (%s) : (%s)"
    114139      t1 (string_of_relation rel) t2 tif telse
     140  | CostCond (i, cond, _, _), tif :: telse :: _ ->
     141    Printf.sprintf "(%s)? (%s) : (%s)" (string_of_cost_cond i cond) tif telse
    115142  | CostOf (fun_name, _), args ->
    116143    let f res v = res ^ v ^ ", " in
    117144    fun_name ^ "(" ^ (List.fold_left f "" args) ^ ")"
    118145  | Any, _ -> "any"
    119   | UnOp _, _ | BinOp _, _ | Cond _, _ ->
     146  | UnOp _, _ | BinOp _, _ | Cond _, _ | CostCond _, _ ->
    120147    assert false (* wrong number of arguments *)
    121148
    122149and to_string v = fold f_to_string v
     150
     151(* amalgamation of cost conditions *)
     152
     153let opt_pair (f : 'a -> 'a option) ((x, y) : 'a * 'a) : ('a * 'a) option =
     154  match f x, f y with
     155    | Some x', Some y' -> Some (x', y')
     156    | Some x', _ -> Some (x', y)
     157    | _, Some y' -> Some (x, y')
     158    | _ -> None
     159
     160let process_pair (f : 'a -> 'a option) (x : 'a) (y : 'a) : 'a * 'a =
     161  match opt_pair f (x, y) with
     162    | Some (x', y') -> (x', y')
     163    | _ -> (x, y)
     164
     165let rec amalgamation_step = function
     166  | CostCond (i, cond, tif, telse) ->
     167    (match opt_pair amalgamation_step (tif, telse) with
     168      | Some (tif', telse') -> Some (CostCond (i, cond, tif', telse'))
     169      | None -> None)
     170  | UnOp (unop, CostCond(i, cond, tif, telse)) ->
     171    let tif, telse = process_pair amalgamation_step tif telse in
     172    let tif, telse = UnOp(unop, tif), UnOp(unop, telse) in
     173    Some (CostCond (i, cond, tif, telse))
     174  | UnOp (unop, t) ->
     175    (match amalgamation_step t with
     176      | Some t' -> Some (UnOp (unop, t'))
     177      | None -> None)
     178  | BinOp(binop, CostCond(i1, c1, t11, t12), CostCond(i2, c2, t21, t22)) ->
     179    let t11, t12 = process_pair amalgamation_step t11 t12 in
     180    let t21, t22 = process_pair amalgamation_step t21 t22 in
     181    if (i1, c1) < (i2, c2) then
     182      let t2 = CostCond(i2, c2, t21, t22) in
     183      let tif = BinOp(binop, t11, t2) in
     184      let telse = BinOp(binop, t12, t2) in
     185      Some (CostCond(i1, c1, tif, telse)) else
     186      if (i1, c1) > (i2, c2) then
     187        let t1 = CostCond(i1, c1, t11, t12) in
     188        let tif = BinOp(binop, t1, t21) in
     189        let telse = BinOp(binop, t1, t22) in
     190        Some (CostCond(i2, c2, tif, telse)) else
     191        let tif = BinOp(binop, t11, t21) in
     192        let telse = BinOp(binop, t12, t22) in
     193        Some (CostCond(i1, c1, tif, telse))
     194  | BinOp(binop, CostCond(i1, c1, t11, t12), t2) ->
     195    let t11, t12 = process_pair amalgamation_step t11 t12 in
     196    let tif = BinOp(binop, t11, t2) in
     197    let telse = BinOp(binop, t12, t2) in
     198    Some (CostCond(i1, c1, tif, telse))
     199  | BinOp(binop, t1, CostCond(i2, c2, t21, t22)) ->
     200    let t21, t22 = process_pair amalgamation_step t21 t22 in
     201    let tif = BinOp(binop, t1, t21) in
     202    let telse = BinOp(binop, t1, t22) in
     203    Some (CostCond(i2, c2, tif, telse))
     204  | BinOp(binop, t1, t2) ->
     205    (match opt_pair amalgamation_step (t1, t2) with
     206      | Some (t1', t2') -> Some (BinOp(binop, t1', t2'))
     207      | None -> None)
     208  | Cond(t1, rel, t2, tif, telse) ->
     209    (match opt_pair (opt_pair amalgamation_step) ((t1, t2), (tif, telse)) with
     210      | Some ((t1', t2'), (tif', telse')) ->
     211        Some (Cond(t1', rel, t2', tif', telse'))
     212      | None -> None)
     213  | CostOf(f, args) ->
     214    let amalg_steps arg (l, b) = match amalgamation_step arg with
     215      | Some arg' -> (arg' :: l, true)
     216      | None -> (arg :: l, b) in
     217    (match List.fold_right amalg_steps args ([], false) with
     218      | (_, false) -> None
     219      | (args', true) ->  Some (CostOf(f, args')))
     220  | Var _ | Int _ | Any -> None
     221
     222(* reduce to normal form. It terminates because the sum of heights of
     223   CostCond nodes in the syntactic tree decreases strictly at each step *)
     224let rec amalgamation v =
     225  match amalgamation_step v with
     226    | None -> v
     227    | Some u -> amalgamation u
    123228
    124229
    … …  
    199304    else raise (Unknown_prototype fun_name)
    200305
     306
    201307(* Reduction in the general case. When some specific patterns are found that
    202308   allow to perform a computation (for instance when applying an operation to
    … …  
    208314  | BinOp (binop, _, _), (Int i1) :: (Int i2) :: _ ->
    209315    Int (int_fun_of_binop binop i1 i2)
    210   | BinOp (Add, _, _), (BinOp (Add, v, Int i1)) :: (Int i2) :: _
    211   | BinOp (Add, _, _), (BinOp (Add, Int i1, v)) :: (Int i2) :: _ ->
    212     BinOp (Add, Int (i1 + i2), v)
     316  | BinOp (Sub, _, _), v :: UnOp(Neg, u) :: _ ->
     317    BinOp (Add, v, u)
     318  | BinOp (Sub, _, _), v :: Int i :: _ when i < 0 ->
     319    BinOp (Add, v, Int (- i))
     320  | BinOp (Add, _, _), (Int i1) :: (BinOp (Sub, v, Int i2)) :: _
     321  | BinOp (Add, _, _), (BinOp (Sub, v, Int i2)) :: (Int i1) :: _
     322  | BinOp (Sub, _, _), (BinOp (Add, v, Int i1)) :: (Int i2) :: _ ->
     323    if i1 < i2 then
     324      BinOp (Sub, v, Int (i2 - i1))
     325    else if i1 > i2 then
     326      BinOp (Add, v, Int (i1 - i2))
     327    else
     328      v
     329  | BinOp (Add, _, _), (Int i1) :: (BinOp (Sub, Int i2, v)) :: _
     330  | BinOp (Add, _, _), (BinOp (Sub, Int i2, v)) :: (Int i1) :: _ ->
     331    BinOp (Sub, Int (i1 + i2), v)
     332  | BinOp (Add, _, _), (Int i1) :: (BinOp (Add, Int i2, v)) :: _
     333  | BinOp (Add, _, _), (Int i1) :: (BinOp (Add, v, Int i2)) :: _
     334  | BinOp (Add, _, _), (BinOp (Add, Int i1, v)) :: (Int i2) :: _
     335  | BinOp (Add, _, _), (BinOp (Add, v, Int i1)) :: (Int i2) :: _ ->
     336    BinOp (Add, v, Int (i1 + i2))
    213337  | BinOp (Add, _, _), v :: (Int 0) :: _
    214338  | BinOp (Sub, _, _), v :: (Int 0) :: _
    … …  
    270394  | _ -> raise Unsupported_rel
    271395
     396let cost_cond_of_cil_rel k rel =
     397  let k = Int64.to_int k in
     398  match rel with
     399    | Cil_types.Eq -> Ceq k
     400    | Cil_types.Ge -> Cgeq k
     401    | _ -> invalid_arg "cost_cond_of_cil_rel"
     402
    272403let cil_rel_of_rel = function
    273404  | Lt -> Cil_types.Rlt
    … …  
    294425  | Cil_types.Mod -> Mod
    295426  | _ -> raise (Failure "binop_of_cil_binop")
     427
     428 let rec mk_cost_cond e =
     429   match e.Cil_types.enode with
     430     | Cil_types.BinOp (rel, e1, e2, _) ->
     431       (match rel, e1.Cil_types.enode, e2.Cil_types.enode with
     432         | (Cil_types.Eq | Cil_types.Ge),
     433           Cil_types.Lval (Cil_types.Var v, _),
     434           Cil_types.Const (Cil_types.CInt64 (k, _, _)) ->
     435           Some (v.Cil_types.vname, cost_cond_of_cil_rel k rel)
     436         | Cil_types.Eq,
     437           Cil_types.BinOp (Cil_types.Mod, e11, e12, _),
     438           Cil_types.Const (Cil_types.CInt64 (b, _, _)) ->
     439           (match e11.Cil_types.enode, e12.Cil_types.enode with
     440             | Cil_types.Lval (Cil_types.Var v, _),
     441               Cil_types.Const (Cil_types.CInt64 (a, _, _)) ->
     442               let a = Int64.to_int a in
     443               let b = Int64.to_int b in
     444               Some (v.Cil_types.vname, Cmod (a, b))
     445             | _ -> None)
     446         | Cil_types.LAnd, _, _ ->
     447           (match mk_cost_cond e1, mk_cost_cond e2 with
     448             | Some (v1, Cgeq k), Some (v2, Cmod (a, b)) when v1 = v2 ->
     449               Some (v1, Cgeqmod (k, a, b))
     450             | _ -> None)
     451         | Cil_types.LOr, _, _ ->
     452           (match mk_cost_cond e1, mk_cost_cond e2 with
     453             | Some (v1, c1), Some (v2, c2) when v1 = v2 ->
     454               Some (v1, Cor (c1, c2))
     455             | _ -> None)
     456         | _ -> None)
     457     | _ -> None
     458
    296459
    297460(** [of_cil_exp e] returns a cost value equivalent to the CIL expression [e]. *)
    … …  
    345508    integer_term (Cil_types.Tif (test, tif, telse))
    346509  | Cond _, _ -> assert false (* wrong number of arguments *)
    347   | CostOf _, _ -> assert false (* should never be used on these arguments *)
     510  | CostOf _, _ | CostCond _, _ ->
     511    Printf.printf "%s\n" (to_string v);
     512    assert false (* should never be used on these arguments *)
    348513  | Any, _ -> raise Unsupported_exp
    349514
Note: See TracChangeset for help on using the changeset viewer.