open Parameters
open Cil_types
open Simplify_terms
module Varinfo = Cil_datatype.Varinfo
module Logic_var = Cil_datatype.Logic_var
module Stmt = Cil_datatype.Stmt
module Term = Cil_datatype.Term
module Logic_label = Cil_datatype.Logic_label

(** This module defines the main analysis of the plug-in. Its actions are:
    - build the CFG of the program;
    - compute the cost of each function depending on the costs of the others
    at the same time add the needed invariant and at the cost of each function
*)


(*** Helpers ***)

let identity x = x

let string_of_list sep f l =
  let rec aux = function
    | [] -> ""
    | [e] -> f e
    | e :: l -> (f e) ^ sep ^ (aux l) in
  aux l

let integer_term term = Logic_const.term term Linteger

let tinteger i =
  let cint64 = CInt64 (My_bigint.of_int i, IInt, None) in
  let iterm = TConst cint64 in
  integer_term iterm

let cil_logic_int_var x =
  Logic_const.tvar (Cil_const.make_logic_var x Linteger)

let current_kf obj = match obj#current_kf with
  | None -> raise (Failure "Compute.current_kf")
  | Some kf -> kf

let add_loop_annot obj stmt annot =
  let annot = User annot in
  let kf =
    Cil.get_original_kernel_function (Cil.copy_visit ()) (current_kf obj) in
  Queue.add (fun () -> Annotations.add kf stmt [Ast.self] annot)
    obj#get_filling_actions

let add_loop_annots obj stmt annots = List.iter (add_loop_annot obj stmt) annots

let mk_invariant pred =
  Logic_const.new_code_annotation (AInvariant ([], true, pred))

let mk_variant term =
  Logic_const.new_code_annotation (AVariant (term, None))

let mk_fun_cost_pred rel cost_id cost = 
  let cost_var = Cil_const.make_logic_var cost_id Linteger in
  let cost_var = Logic_const.tvar cost_var in
  let old_cost = Logic_const.told cost_var in
  let new_cost = TBinOp (PlusA, old_cost, cost) in
  let new_cost = integer_term new_cost in
  Logic_const.prel (rel, cost_var, new_cost)

let rec exp_is_var name e = match (remove_casts e).enode with
  | Lval (Var v, _) -> v.vname = name
  | Info (e, _) -> exp_is_var name e
  | _ -> false

let has_fun_type varinfo = match varinfo.vtype with
  | TFun _ -> true
  | _ -> false

let formals_of_varinfo varinfo = match varinfo.vtype with
  | TFun (_, args, _, _) -> 
    List.map (fun (x, t, _) -> Cil.makeVarinfo false true x t)
      (Cil.argsToList args)
  | _ -> assert false (* do not use on these arguments *)

let dummy_location = (Lexing.dummy_pos, Lexing.dummy_pos)

let dummy_varinfo = Cil.makeVarinfo false false "" (TVoid [])

let make_list n a =
  let rec aux acc i = if i >= n then acc else aux (a :: acc) (i+1) in
  aux [] 0

let rec stmt_subs stmt =
  let added = match stmt.skind with
    | If (_, block1, block2, _)
    | TryFinally (block1, block2, _)
    | TryExcept (block1, _, block2, _) ->
      (block_subs block1) @ (block_subs block2)
    | Switch (_, block, _, _)
    | Loop (_, block, _, _, _)
    | Block block -> block_subs block
    | UnspecifiedSequence l ->
      List.map (fun (stmt, _, _, _, _) -> stmt) l
    | _ -> [] in
  stmt :: added

and block_subs block = List.flatten (List.map stmt_subs block.bstmts)

let rec first_stmt block = match block.bstmts with
  | [] -> None
  | stmt :: _ -> match stmt.skind with
      | Block block -> first_stmt block
      | _ -> Some stmt

let stmt_is_break stmt = match stmt.skind with
  | Break _ -> true
  | _ -> false

let starts_with_break block = match first_stmt block with
  | Some stmt ->
    (match stmt.skind with
      | Goto (stmt_ref, _) -> stmt_is_break !stmt_ref
      | _ -> stmt_is_break stmt)
  | _ -> false

let rec last = function
  | [] -> None
  | [e] -> Some e
  | _ :: l -> last l

let rec last_stmt block = match last block.bstmts with
  | None -> None
  | Some stmt -> match stmt.skind with
      |  Block block -> last_stmt block
      | _ -> Some stmt

class print_CFG = object inherit Visitor.frama_c_inplace as super

  method vfunc func =
    Format.printf "*** %s ***\n\n%!" func.svar.vname ;
    List.iter
      (fun stmt ->
	Format.printf "%d: %a\n--> %!" stmt.sid Cil.d_stmt stmt ;
	List.iter (fun stmt -> Format.printf "%d %!" stmt.sid)
	  stmt.succs ;
	Format.printf "\n\n%!")
      func.sallstmts ;
    Format.printf "\n\n%!" ;
    Cil.SkipChildren

end

let print_CFG () =
  Visitor.visitFramacFile (new print_CFG) (Ast.get ())

(*** Make CFG ***)

class make_CFG = object inherit Visitor.frama_c_inplace as super

  method vfile file =
    Cfg.clearFileCFG ~clear_id:false file ;
    Cfg.computeFileCFG file ;
    Cil.SkipChildren

end

let make_CFG () =
  Visitor.visitFramacFile (new make_CFG) (Ast.get ())

(** Extract variant *)

let rec extract_added_value counter e = match e.enode with
  | BinOp (PlusA, e1, e2, _) when exp_is_var counter e1 ->
    Some (counter, e2)
  | BinOp (MinusA, e1, e2, typ)
      when exp_is_var counter e1 ->
    let enode = UnOp (Neg, e2, typ) in
    let e2 = { e2 with enode = enode } in
    Some (counter, e2)
  | CastE (_, e) -> extract_added_value counter e
  | _ ->
    if !debug then
      Format.printf
	"Could not find added increment value for counter %s in %a.\n%!"
	counter Cil.d_exp e ;
    None

let extract_increment block =
  let open Misc.Option in
  last_stmt block >>=
  (fun stmt -> match stmt.skind with
    | Instr (Set ((Var v, _), e, _)) ->
      extract_added_value v.vname e
    | _ ->
      if !debug then
	Format.printf
	  "Could not find increment instruction; found %a instead.\n%!"
	  Cil.d_stmt stmt ;
      None)

let gen_variant counter rel guard increment =
  let counter = term_of_exp counter in
  let guard   = term_of_exp guard in
  let increment = term_of_exp increment in
  let guard = match rel with
    | Lt | Gt | Ne -> guard
    | Le | Ge | Eq -> make_binop PlusA (Cil.lconstant My_bigint.one) guard
    | _ -> assert false (* not implemented TODO be gentle *) in
  let variant = make_binop MinusA guard counter in
  let variant =
    if no_division_in_generated_variant
    then make_binop Mult variant (make_sign increment)
    else make_binop Div variant increment in
  simplify_term variant

let opposite = function
  | Lt -> Gt
  | Gt -> Lt
  | Le -> Ge
  | Ge -> Le
  | Eq -> Eq
  | Ne -> Ne
  | _ -> assert false (* not implemented TODO be gentle *)


let extract_guard block (counter, increment) =
  let open Misc.Option in
  first_stmt block >>=
  (fun stmt -> match stmt.skind with
    | If (e, _, block, _) when starts_with_break block ->
      (match e.enode with
	| BinOp (rel, e1, e2, _)
	    when exp_is_var counter e1 (* && Domain.is_supported_rel rel *) ->
	  (*Some (counter, rel, e2, increment)*)
          Some (gen_variant e1 rel e2 increment)
	| BinOp (rel, e1, e2, _)
	    when exp_is_var counter e2 (* && Domain.is_supported_rel rel *) ->
	  (* let rel = rel in *)
	  (* let rel = Domain.opposite rel in *)
	  (* Some (counter, rel, e1, increment) *)
          let rel = opposite rel in
          Some (gen_variant e2 rel e1 increment)
	| _ ->
	  if !debug then
	    Format.printf "Unsupported guard condition %a on counter %s.\n%!"
	      Cil.d_exp e counter ;
	  None)
    | If (_, _, block, _) ->
      if !debug then
	Format.printf "Loop not guarded by a break:\n%a\n%!" Cil.d_block block ;
      None
    | _ ->
      if !debug then Format.printf "Loop not guarded:\n%a\n%!" Cil.d_stmt stmt ;
      None)

let extract_variant body =
  let open Misc.Option in
  extract_increment body >>= extract_guard body

let rec find_variant = function
  | [] -> None
  | {annot_content = AVariant (t,_)}::_ -> Some t
  | _::l -> find_variant l


(** Function computing cost of special instruction  *)

type env =
  { env_fun_cost : term Varinfo.Hashtbl.t;
    env_cost_incr_name : string; (* TODO put the varinfo *)
    env_cost_var : logic_var;
    mutable env_loop_name : unit -> string;
  }

let init_loop_name env file =
  let i = ref 0 in
  let f () =
    incr i;
    Format.sprintf "__cost_%s_loop_%i" file !i in
  env.env_loop_name <- f

let dumb_env_loop_name () : string = assert false

let linteger t = Logic_const.term t Linteger

(** Create a function which compute the cost of a loop.
It uses the variant as the strictly decreasing positive argument.
The cost depend of the other arguments \vec x.

\bcost if the cost of the body of the loop (must be always positive!)
\phi compute the modification of \vec x by one turn of the loop

f(v,\vec x) =
  if v < 0 then 0
  else (f(v-1,\phi(\vec x)) + \bcost(\vec x))

It also create some needed lemmas:
 - f is always positive

or simplifying lemmas:
 - simpler (eg. algebraic) formulation of f:
   * \vec x = \empty, \phi = identity, \bcost = c >= 0
     f(v) = c (v + 1)
   * \phi = identity
     f(v,\vec x) = \bcost(\vec x) * (v + 1)
   * \phi(\vec x) = x_1 + 1,x_2,...,x_n
     \bcost(\vec x) = max(c x_1,0) + \phi(x_2,...,x_n)
     \phi(x_2,...,x_n) >= 0, c >= 0
    f(v,\vec x) = \phi(x_2,...,x_n) (v + 1)
      + c * [y(y+1) - (max(y-v-1,0)(y-v)]/2
*)
let create_fun_loop env dep bcost =
  let v  = Cil_const.make_logic_var "v" Linteger in
  let tv = Logic_const.tvar v in
  let xargs = List.map fst dep in   (** \vec x *)
  let mod_dep = List.map snd dep in (** \phi *)
  let args = v::xargs in
  let targs = List.map Logic_const.tvar args in
  (** The function *)
  let signature = Larrow (List.map (fun _ -> Linteger) args, Linteger) in
  let new_loop_name = env.env_loop_name () in
  let li = { l_var_info = Cil_const.make_logic_var new_loop_name signature;
             l_labels = [];
             l_tparams = [];
             l_type = Some Linteger;
             l_profile = args;
             l_body = LBnone (* temporary *) } in
  let lzero = Cil.lzero () in
  let tvminusone =
    linteger (TBinOp(MinusA, tv, Cil.lconstant (My_bigint.one))) in
  (* let body = linteger (Tapp(li,[],tvminusone::mod_dep)) in *)
  let body = linteger (tapp li (tvminusone::mod_dep)) in
  let body = linteger (TBinOp(PlusA, body, bcost)) in
  let body =
    Tif(linteger (TBinOp(Lt, tv, lzero)), lzero, body) in
  li.l_body <- LBterm (linteger body);
  (** Axiom positive *)
  let lemma = Logic_const.unamed
    (Pforall(args,
             Logic_const.unamed
               (Prel (Rge, linteger (Tapp(li, [], targs)), lzero)))) in
  let lemma = Dlemma (new_loop_name ^ "_is_positive", false, [], [], lemma,
                      Cil_datatype.Location.unknown) in
  (** Register them as global (in reverse order) *)
  Globals.Annotations.add_generated lemma;
  Globals.Annotations.add_generated
    (Dfun_or_pred (li, Cil_datatype.Location.unknown));
  li

(** TODO: extend it to some more interesting cases *)
let cost_loop_term_simple env kern_fun stmt lab_before_loop variant cost_body =
  (** The number of iteration is bounded by the variant + 1, because
      the variant must be positive at the *start* of an iteration *)
  let variant = make_binop PlusA variant (Cil.lconstant (My_bigint.one)) in
  (** Simple version, just do the multiplication *)
  let nbr_iteration = make_at lab_before_loop variant in
  (** the nbr_iteration must be positive *)
  let nbr_iteration = make_max nbr_iteration (Cil.lzero ()) in
  let sum = make_binop Mult nbr_iteration cost_body in

  (** make the cost invariant of the loop *)
  let remaining_nbr_iteration = make_max variant (Cil.lzero ()) in
  (** ensures cost <= \old(cost) +
      ([nbr_iteration]-[remaining_nbr_iteration]) * [cost_body] *)
  let cost_var = Logic_const.tvar env.env_cost_var in
  let old_cost = make_at lab_before_loop cost_var in
  let cost_iterations =
    make_binop Mult
      (make_binop MinusA nbr_iteration remaining_nbr_iteration)
      cost_body in
  let new_cost = make_binop PlusA old_cost cost_iterations in
  let new_cost = simplify_term new_cost in
  let invariant = Logic_const.prel (Rle, cost_var, new_cost) in
  let annot =
    Logic_const.new_code_annotation
      (AInvariant ([time_cost_behavior],true,invariant)) in
  Annotations.add kern_fun stmt [Ast.self] (User annot);
  sum

let cost_loop_term_complexe
    env kern_fun stmt lab_before_loop variant deps cost_body =
  (** the nbr_iteration must be positive *)
  let variant = make_max variant (Cil.lzero ()) in
  let args = List.map fst deps in (** \phi *)
  let targs = List.map Logic_const.tvar args in
  let fl = create_fun_loop env deps cost_body in
  let app = linteger (tapp fl (variant::targs)) in
  let sum = make_at lab_before_loop app in

  (** make the cost invariant of the loop *)
  (** ensures cost <= \old(cost) +
      ([nbr_iteration]-[remaining_nbr_iteration]) * [cost_body] *)
  let cost_var = Logic_const.tvar env.env_cost_var in
  let old_cost = make_at lab_before_loop cost_var in
  let cost_iterations = make_binop MinusA sum app in
  let new_cost = make_binop PlusA old_cost cost_iterations in
  let new_cost = simplify_term new_cost in
  let invariant = Logic_const.prel (Rle, cost_var, new_cost) in
  let annot =
    Logic_const.new_code_annotation
      (AInvariant ([time_cost_behavior],true,invariant)) in
  Annotations.add kern_fun stmt [Ast.self] (User annot);
  sum

let cost_loop_term env kern_fun stmt lab_before_loop variant deps cost_body =
(*
  let const_during_loop = List.for_all (fun (_,_) -> (** TODO *) false) deps in
  if const_during_loop
  then cost_loop_term_simple env kern_fun stmt lab_before_loop variant cost_body
  else cost_loop_term_complexe
    env kern_fun stmt lab_before_loop variant deps cost_body
*)
  let cost_body = simplify_term cost_body in
  match cost_body.term_node with
  | TConst _ ->
    cost_loop_term_simple env kern_fun stmt lab_before_loop variant cost_body
  | _ ->
    cost_loop_term_complexe
      env kern_fun stmt lab_before_loop variant deps cost_body


(** computing cost of fundec which contain a call to funvar *)
let cost_of_fun_call env funvar args =
  (** can't fail since we use the callgraph *)
  let cost = Varinfo.Hashtbl.find env.env_fun_cost funvar in
  (* match cost.term_node with *)
  (* | TConst (CInt64 (_,_,_)) -> cost *)
  (* | _ -> *)
  (** arguments of the function *)
  let formals = Cil.getFormalsDecl funvar in
(*  (** The real arguments are binded using a let and the formal argument are
      replaced by fresh variable *)
  let letvars = List.map
    (fun vi -> Cil.make_temp_logic_var (Ctype vi.vtype))
    formals in
  let subst = List.fold_left2 (fun map vi v ->
    Varinfo.Map.add vi v map) Varinfo.Map.empty formals letvars in
  let cost =
    Visitor.visitFramacTerm (new subst_lval subst (Project.current ()))
      cost in
  let cost = List.fold_left2 (fun tlet v arg ->
    let logic_info = { l_var_info = v; l_type = None; l_tparams = [];
                       l_labels = []; l_profile = [];
                       l_body = LBnone; } in
    let arg = term_of_exp arg in
    let tlet =
      Logic_const.term (Tlet (logic_info, arg))
        tlet.term_type in
    tlet)
    cost letvars args in*)
  let subst = List.fold_left2 (fun map vi arg ->
    try
      Varinfo.Map.add vi (term_of_exp arg) map
    with Untranslatable_expr _ -> map (** TODO verify that this formal doesn't
                                          appear in the cost of the function *)
  ) Varinfo.Map.empty formals args in
  let cost = remove_logic_label Logic_const.pre_label cost in
  let cost =
    Visitor.visitFramacTerm (new subst_lval subst (Project.current ()))
      cost in
  cost

(** Compute the "wp" of a stmt, in fact just make some substitution *)
let stmt_wp stmt term =
  (** try to propagate \at(i,Label) *)
  match stmt.skind with
  | Instr (Set ((Var vi,_),e,_)) ->
    begin
      try
        let t = term_of_exp e in
        let subst = Varinfo.Map.singleton vi t in
        let term =
          Visitor.visitFramacTerm
            (new subst_with_label stmt subst (Project.current ()))
            term in
        term
      with exn ->
        if !debug then Format.eprintf "can't convert exp %a to term: %a.@."
          Cil.defaultCilPrinter#pExp e print_exception exn;
        term
    end
  | _ -> term

let rec stmts_wp bad_stmts stop_stmts stmt term =
  if !debug then
    Format.printf "stmts_wp sid: %i,@ bad_stmts: %a,@ stop_stmts: %a,@\n"
      stmt.sid
      Stmt.Set.pretty bad_stmts
      Stmt.Set.pretty stop_stmts;
  (** statement in last statement *)
  if Stmt.Set.mem stmt stop_stmts
  then Some term
  else if Stmt.Set.mem stmt bad_stmts
  then None
  else
  (** successors *)
  let succs_bad_stmts =
    match stmt.skind with
    | Loop (_,_,_,_,_) -> Stmt.Set.add stmt bad_stmts
    | _ -> bad_stmts in
  (** Cost of the successors of the instruction *)
  let cost_succs =
    stmts_wp_succs succs_bad_stmts stop_stmts stmt.succs term in
  match cost_succs with
  | [] -> None (** can't go in a good state so count nothing *)
  | (a::l) -> (** TODO take care of conditions *)
    assert (l = []);
    let a' = stmt_wp stmt a in
    if !debug then
      Format.printf "[WP]stmt:@,%a@.a:@,%a@.a':@,%a@."
        Cil.defaultCilPrinter#pStmt stmt
        Cil.defaultCilPrinter#pTerm a
        Cil.defaultCilPrinter#pTerm a';
    Some a'

and stmts_wp_succs bad_stmts stop_stmts stmts term =
  let fold acc stmt =
    match stmts_wp bad_stmts stop_stmts stmt term with
    | None -> acc
    | Some t -> t::acc in
  List.fold_left fold [] stmts


(** We go through the cfg we assume that:
    - all functions called have a cost already computed
    - no implicit loop (goto), all are explicit Loop
    - all loops have an invariant (given by the user or previously computed for
    for-loops)

    We iterate on the cfg except when arriving on a loop where we compute the
    body alone and after that go to the next statements (the break statement)

   break_statement in which statement to stop the sum (for loop)
 *)


let rec find_variant = function
  | [] -> None
  | {annot_content = AVariant (t,_)}::_ -> Some t
  | _::l -> find_variant l

(** TODO: cache the statement already done after if-then-else
    (otherwise exponential) *)
(** return None if no path arrive to a good_statement or don't go through
    a bad_statetement *)
let rec cfg_sum env kern_fun bad_stmts stop_stmts stmt =
  if !debug then
    Format.printf "sid: %i,@ bad_stmts: %a,@ stop_stmts: %a,@\n"
      stmt.sid
      Stmt.Set.pretty bad_stmts
      Stmt.Set.pretty stop_stmts;
  (** statement in last statement *)
  if Stmt.Set.mem stmt stop_stmts
  then Some (Cil.lzero ())
  else if Stmt.Set.mem stmt bad_stmts
  then None
  else
  (** successors *)
  let succs_bad_stmts =
    match stmt.skind with
    | Loop (_,_,_,_,_) -> Stmt.Set.add stmt bad_stmts
    | _ -> bad_stmts in
  (** Cost of the successors of the instruction *)
  let cost_succs =
    cfg_sum_succs env kern_fun succs_bad_stmts stop_stmts
      stmt.succs in
  match cost_succs with
  | None -> None (** can't go in a good state so count nothing *)
  | Some cost_succs ->
  (** Cost of the instruction *)
  let cost_instr =
    match stmt.skind with
    (* (\** call to cost_incr *\) *) (** cost_incr is an usual function *)
    (* | Instr *)
    (*     (Call (None, *)
    (*                      { enode = *)
    (*                          Lval (Var var, _)} , *)
    (*                      [cost], _)) *)
    (*     when var.vname = env.env_cost_incr_name -> *)
    (*   term_of_cost_expr cost *)
    (** function call *)
    | Instr
        (Call (_, { enode =
            Lval (Var var, _)},
                         args,_)) ->
      cost_of_fun_call env var args
    (** loops *)
    | Loop (_,body,_,_,_) ->
      cost_loop env kern_fun bad_stmts stop_stmts stmt body
    | _ -> Cil.lzero () in
  (** normalize the cost of the instruction regarding the labels *)
  let labels = NormAtLabels.labels_stmt_pre stmt in
  let cost_instr = NormAtLabels.preproc_annot_term labels cost_instr in
  let cost_succs = stmt_wp stmt cost_succs in
  let sum = make_binop PlusA cost_instr cost_succs in
  (** remove the at that point to this statement we don't know the value at
      this point perhaps we will know before ( use Here?? ) *)
  let sum =
    Visitor.visitFramacTerm
      (new remove_stmt_label stmt (Project.current ()))
      sum in
  if !debug then
    Format.printf "Stmt %i sum=%a@."
      stmt.sid Term.pretty sum;
  Some sum

and cfg_sum_succs env kern_fun bad_stmts stop_stmts stmts =
  let fold cost stmt =
    let cost_succ = cfg_sum env kern_fun bad_stmts stop_stmts stmt in
    make_max_opt cost cost_succ in
  List.fold_left fold None stmts

and cost_loop env kern_fun bad_stmts stop_stmts stmt body =
  (** the first one perhaps not needed *)
  let bad_stmts = Stmt.Set.union bad_stmts stop_stmts in
  let stop_stmts = Stmt.Set.singleton stmt in
  let cost_body =
    cfg_sum_succs env kern_fun bad_stmts stop_stmts stmt.succs in
  let cost_body = match cost_body with
    | None -> (* no cycle in fact *) Cil.lzero ()
    | Some cost -> simplify_term cost in
  (** compute free variable and compute their modification by the loop body *)
  let deps = freevar Logic_var.Set.empty cost_body in
  let deps =
    let fold e acc =
      let result =
        stmts_wp_succs bad_stmts stop_stmts stmt.succs (Logic_const.tvar e)  in
      match result with
      | [] -> assert false (** No cycle? impossible it find one before *)
      | t::l ->
        assert (l = []); (* TODO *)
        (e, t)::acc in
    Logic_var.Set.fold fold deps [] in
  (** this stmt is the continue *)
  let annots = Annotations.get_filter Logic_utils.is_variant stmt in
  let variant = match annots with
    | [] -> (** TODO put it somewhere else *)
      begin match extract_variant body with
      | None ->
        Format.printf
          "Can't@ compute@ cost@ without@ variant@ for@ statement:@,%a@."
          Stmt.pretty stmt; exit 1
      | Some variant ->
        let annot =
          Logic_const.new_code_annotation (AVariant (variant,None)) in
        Annotations.add kern_fun stmt [Ast.self] (User annot);
        variant end
    | ( User { annot_content =
        AVariant (v,_) }
          | AI (_, { annot_content =
              AVariant (v,_) }) (** usefule case ? *)
    )
      :: _ ->
      let v = NormAtLabels.preproc_annot_term
        (NormAtLabels.labels_loop_inv stmt) v in
      let v = remove_logic_label Logic_const.here_label v in
      v
    | _ -> assert false (* result of the filter *)
  in
  if stmt.labels = [] then
    stmt.labels <- (** ugly but... *)
      Label("__stmt_"^(string_of_int stmt.sid),Cil.builtinLoc,false)::
      stmt.labels;
  let label_before_loop = StmtLabel (ref stmt) in
  cost_loop_term env kern_fun stmt label_before_loop variant deps cost_body

let make_leq_cost env sum =
    (** ensures cost <= \old(cost) + [sum] *)
    let cost_var = Logic_const.tvar env.env_cost_var in
    let old_cost = Logic_const.told cost_var in
    let new_cost = Logic_const.term
      (Cil_types.TBinOp (Cil_types.PlusA, old_cost, sum)) Linteger in
    let post = Logic_const.prel (Rle, cost_var, new_cost) in
    let post = Logic_const.new_predicate post in
    post

let fun_sum env vi kernel_fun =
  let fst_stmt = Kernel_function.find_first_stmt kernel_fun in
  let last_stmt = Kernel_function.find_return kernel_fun in
  let bad_stmts = Stmt.Set.empty in
  let stop_stmts = Stmt.Set.singleton last_stmt in
  let sum = cfg_sum env kernel_fun bad_stmts stop_stmts fst_stmt in
  let sum = match sum with
    | None -> assert false (* Oups return not achievable?? *)
          (* Infinity!! *)
    | Some sum ->
      let sum = simplify_term sum in
      let sum = Logic_const.told sum in (** add old and push it *)
      let labels = NormAtLabels.labels_fct_post in
      let sum = NormAtLabels.preproc_annot_term labels sum in
      sum in
  if !debug then
    Format.printf "@[<hov 3>sum of %a: %a@]@."
      Cil.defaultCilPrinter#pVar vi
      Cil.defaultCilPrinter#pTerm sum;
(** add postcondition about cost *)
  let mod_funspec funspec =
    let post = make_leq_cost env sum in
    let behavior =
      Cil.mk_behavior ~name:time_cost_behavior ~post_cond:[Normal, post] () in
    {funspec with spec_behavior = behavior::funspec.spec_behavior;}
  in
  Kernel_function.set_spec kernel_fun mod_funspec;
  sum

(** Before computing the sum check that the user doesn't specify the cost.
    In this case use it *)
let fun_sum env vi =
  init_loop_name env "fun_sum";
  let kernel_fun = Globals.Functions.get vi in
  let funspec = Kernel_function.get_spec kernel_fun in
  let rec find_cost = function
    | [] -> None
    | {b_name = name;
       b_requires = [];
       b_assumes = []; (** TODO? allow more general contract? *)
       (** ensores __cost <= \old(__cost) + t; *)
       b_post_cond = [_,{ip_content=Prel
           (Rle,
            {term_node = (TLval(TVar cost_var,TNoOffset))},
            {term_node = TBinOp(PlusA,{term_node = Tat(
              {term_node = (TLval(TVar cost_var2,TNoOffset))}, old_label)},
                                t)})}]
      }::_ when name = time_cost_behavior &&
             Logic_var.equal cost_var  env.env_cost_var &&
             Logic_var.equal cost_var2 env.env_cost_var &&
             Logic_label.equal old_label Logic_const.old_label
           -> Some t
    | _::l -> find_cost l in
  match find_cost funspec.spec_behavior with
  | None -> fun_sum env vi kernel_fun
  | Some sum ->
    if !debug then
      Format.printf "@[<hov 3>User sum of %a: %a@]@."
        Cil.defaultCilPrinter#pVar vi
        Cil.defaultCilPrinter#pTerm sum;
    let labels = NormAtLabels.labels_fct_post in
    let sum = NormAtLabels.preproc_annot_term labels sum in
    sum

let initialize _tmp_prefix _fname cost_var cost_incr _extern_costs =
  (** TODO? use extern_costs for initializing env_fun_cost ? *)
  let callgraph = Callgraph.computeGraph (Ast.get ()) in
  if !debug then
    Printf.printf "callgraph size: %a\n%!" Callgraph.printGraph callgraph;
  let env = { env_fun_cost = Varinfo.Hashtbl.create 10;
              env_cost_incr_name = cost_incr;
              env_cost_var = cost_var;
              env_loop_name = dumb_env_loop_name} in
  let rec iter : 'a. 'a -> Callgraph.callnode -> unit = fun _ callnode ->
    match callnode.Callgraph.cnInfo with
    | Callgraph.NIVar (vi,{contents = true }) ->
      if not (Varinfo.Hashtbl.mem env.env_fun_cost vi) then begin
        Inthash.iter iter callnode.Callgraph.cnCallees;
        let sum = fun_sum env vi in
        Varinfo.Hashtbl.add env.env_fun_cost vi sum
      end
    | _ -> () (** put an undefined constant here for top *)
  in
  (** add the cost of cost_incr *)
  let cost_incr = Hashtbl.find callgraph cost_incr in
  let cost_incr = match cost_incr.Callgraph.cnInfo with
    | Callgraph.NIVar (vi,_) -> vi
    | _ -> assert false (* cost_incr must be at least declared *) in
  let arg_cost_incr = List.hd (Cil.getFormalsDecl cost_incr) in
  let sum_cost_incr = Logic_const.tvar (Cil.cvar_to_lvar arg_cost_incr) in
  let post_cost_incr = make_leq_cost env sum_cost_incr in
  Kernel_function.set_spec (Globals.Functions.get cost_incr) (fun funspec ->
    let assigns =
      Writes [Logic_const.(new_identified_term (tvar cost_var)), FromAny] in
    let behavior =
      Cil.mk_behavior ~name:time_cost_behavior
        ~post_cond:[Normal, post_cost_incr]
        ~assigns () in
    {funspec with spec_behavior = behavior::funspec.spec_behavior;} );
  Varinfo.Hashtbl.add env.env_fun_cost cost_incr sum_cost_incr;
  (** make the other functions *)
  Hashtbl.iter iter callgraph


(*** Main ***)

let cost ((fname, _), _, cost_time, _) =
  try
    if !debug then Printf.printf "Initialize Cost\n%!" ;
    let cost_var =
      Cil.cvar_to_lvar (Globals.Vars.find_from_astinfo
                          cost_time.Cerco.cost_id VGlobal) in
    initialize "__tmp" fname cost_var
      cost_time.Cerco.cost_incr cost_time.Cerco.extern_costs;
  with e -> Format.eprintf "** ERROR: %a.@." print_exception_raise e