(* TODO: transform precondition into assertions, transform added code into ghost
   code. *)

(** This module defines the main analysis of the plug-in. Its actions are:
    - build the CFG of the program;
    - initialize the static environment of analysis (parameters of the
    functions, number of loops, etc);
    - compute the cost of each function depending on the costs of the others;
    - try to solve the inequations formed from the previous step so as to obtain
      an independent cost for each function;
    - save the results;
    - add the annotations on the program. *)


(*** Exceptions ***)

exception ASM_unsupported
exception Try_unsupported

let string_of_exception = function
  | ASM_unsupported -> "ASM instructions not supported"
  | Try_unsupported -> "Try instructions not supported"
  | Cost_value.Unknown_cost fun_name ->
    "Cost for function " ^ fun_name ^ " not found."
  | Cost_value.Unknown_prototype fun_name ->
    "Prototype for function " ^ fun_name ^ " not found."
  | e -> raise e


(*** Debug flag ***)

let debug = ref false


(*** 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 Cil_types.Linteger

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

let cil_logic_int_var x =
  Logic_const.tvar (Cil_const.make_logic_var x Cil_types.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 = Cil_types.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 (Cil_types.AInvariant ([], true, pred))

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

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

(** Casts may get in the way when looking for a loop counter, just remove
    them. *)

let rec remove_casts e = match e.Cil_types.enode with
  | Cil_types.Lval lval ->
    { e with Cil_types.enode = Cil_types.Lval (remove_casts_lval lval) }
  | Cil_types.SizeOfE e ->
    { e with Cil_types.enode = Cil_types.SizeOfE (remove_casts e) }
  | Cil_types.AlignOfE e ->
    { e with Cil_types.enode = Cil_types.AlignOfE (remove_casts e) }
  | Cil_types.UnOp (unop, e, typ) ->
    { e with Cil_types.enode = Cil_types.UnOp (unop, remove_casts e, typ) }
  | Cil_types.BinOp (binop, e1, e2, typ) ->
    let enode =
      Cil_types.BinOp (binop, remove_casts e1, remove_casts e2, typ) in
    { e with Cil_types.enode }
  | Cil_types.CastE (_, e) -> remove_casts e
  | Cil_types.AddrOf lval ->
    { e with Cil_types.enode = Cil_types.AddrOf (remove_casts_lval lval) }
  | Cil_types.StartOf lval ->
    { e with Cil_types.enode = Cil_types.StartOf (remove_casts_lval lval) }
  | Cil_types.Info (e, info) ->
    { e with Cil_types.enode = Cil_types.Info (remove_casts e, info) }
  | _ -> e

and remove_casts_lval (lhost, offset) =
  (remove_casts_lhost lhost, remove_casts_offset offset)

and remove_casts_lhost = function
  | Cil_types.Mem e -> Cil_types.Mem (remove_casts e)
  | lhost -> lhost

and remove_casts_offset = function
  | Cil_types.Field (fieldinfo, offset) ->
    Cil_types.Field (fieldinfo, remove_casts_offset offset)
  | Cil_types.Index (e, offset) ->
    Cil_types.Index (remove_casts e, remove_casts_offset offset)
  | offset -> offset

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

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

let formals_of_varinfo varinfo = match varinfo.Cil_types.vtype with
  | Cil_types.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 "" (Cil_types.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.Cil_types.skind with
    | Cil_types.If (_, block1, block2, _)
    | Cil_types.TryFinally (block1, block2, _)
    | Cil_types.TryExcept (block1, _, block2, _) ->
      (block_subs block1) @ (block_subs block2)
    | Cil_types.Switch (_, block, _, _)
    | Cil_types.Loop (_, block, _, _, _)
    | Cil_types.Block block -> block_subs block
    | Cil_types.UnspecifiedSequence l ->
      List.map (fun (stmt, _, _, _, _) -> stmt) l
    | _ -> [] in
  stmt :: added

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

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

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

let starts_with_break block = match first_stmt block with
  | Some stmt ->
    (match stmt.Cil_types.skind with
      | Cil_types.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.Cil_types.bstmts with
  | None -> None
  | Some stmt -> match stmt.Cil_types.skind with
      | Cil_types. Block block -> last_stmt block
      | _ -> Some stmt

module IntSet = Misc.Int.Set
module IntMap = Misc.Int.Map
module IntCMap = Misc.Int.CMap


(*** Temporary variable name generator ***)

module GenName = struct

  let prefix = ref ""
  let index = ref 0

  let set_prefix prf = prefix := prf
  let reset () = index := 0

  let concat suffix = !prefix ^ "_" ^ suffix

  let fresh () =
    let s = !prefix ^ (string_of_int !index) in
    index := !index + 1 ;
    s

  let rec freshes n = if n = 0 then [] else (freshes (n-1)) @ [fresh ()]

  let fresh_varinfo fundec =
    Cil.makeTempVar fundec ~name:(fresh ()) Cil.intType

  let freshes_varinfo fundec n =
    let vars = freshes n in
    List.map (fun name -> Cil.makeTempVar fundec ~name Cil.intType) vars

end


(*** Debug helpers ***)

let string_of_intset set =
  IntSet.fold (fun i s -> s ^ (string_of_int i) ^ " ") set ""
let string_of_intset_intmap map =
  let f i set s = Printf.sprintf "%s%d: %s\n" s i (string_of_intset set) in
  IntMap.fold f map ""

class print_CFG prj = object inherit Visitor.frama_c_copy prj as super

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

end

let print_CFG () =
  let print_CFG_prj =
    File.create_project_from_visitor "print_CFG" (new print_CFG) in
  let f () = () in
  Project.on print_CFG_prj f ()

class loop_exit prj = object inherit Visitor.frama_c_copy prj as super

  method vstmt_aux stmt =
    let _ = match stmt.Cil_types.skind with
      | Cil_types.Loop (_, block, _, _, _) ->
	(match first_stmt block with
	  | Some stmt ->
	    (match stmt.Cil_types.skind with
	      | Cil_types.If (_, _, block, _) ->
		(match first_stmt block with
		  | Some stmt ->
		    (match stmt.Cil_types.skind with
		      | Cil_types.Break _ ->
			Format.printf "Loop exit: %!" ;
			List.iter
			  (fun stmt -> Format.printf "%d %!" stmt.Cil_types.sid)
			  stmt.Cil_types.succs ;
			Format.printf "\n%!"
		      | _ -> Format.printf "If but no break\n%!")
		  | _ -> Format.printf "If but no child\n%!")
	      | _ -> Format.printf "Loop but no if\n%!")
	  | _ -> Format.printf "Loop but no child\n%!")
      | _ -> () in
    Cil.DoChildren

end

let loop_exit () =
  let loop_exit_prj =
    File.create_project_from_visitor "loop_exit" (new loop_exit) in
  let f () = () in
  Format.printf "\n%!" ;
  Project.on loop_exit_prj f ()


(*** Make CFG ***)

class make_CFG prj = object inherit Visitor.frama_c_copy prj as super

  method vfile file =
    Cfg.clearFileCFG file ;
    Cfg.computeFileCFG file ;
    Cil.SkipChildren

end

let make_CFG () =
  let make_CFG_prj =
    File.create_project_from_visitor "make_CFG" (new make_CFG) in
  let f () = () in
  Project.on make_CFG_prj f ()


(*** Control points that are gotoed to, control points of a loop. Those will
     help checking that a loop has a supported form. ***)

module PointsInfo = struct

  type t = { gotoed : IntSet.t IntMap.t ; loop_points : IntSet.t IntMap.t }

  let empty = { gotoed = IntMap.empty ; loop_points = IntMap.empty }

  let gotoed points_info = points_info.gotoed

  let loop_points points_info = points_info.loop_points

  let mem_gotoed to_id points_info = IntMap.mem to_id (gotoed points_info)

  let find_gotoed to_id points_info = IntMap.find to_id (gotoed points_info)

  let add_gotoed to_id to_from_ids points_info =
    let gotoed = IntMap.add to_id to_from_ids (gotoed points_info) in
    { points_info with gotoed }

  let mem_loop_points loop_id points_info =
    IntMap.mem loop_id (loop_points points_info)

  let find_loop_points loop_id points_info =
    IntMap.find loop_id (loop_points points_info)

  let add_loop_points loop_id ids points_info =
    let loop_points = IntMap.add loop_id ids (loop_points points_info) in
    { points_info with loop_points }

end

(*** PointsInfo for each function ***)

module PointsInfos = struct

  type t = PointsInfo.t Misc.String.Map.t

  let empty = Misc.String.Map.empty

  let mem = Misc.String.Map.mem

  let add = Misc.String.Map.add

  let find = Misc.String.Map.find

  let add_gotoed fun_name to_id to_from_ids points_infos =
    let points_info =
      if mem fun_name points_infos then find fun_name points_infos
      else PointsInfo.empty in
    let points_info = PointsInfo.add_gotoed to_id to_from_ids points_info in
    add fun_name points_info points_infos    

  let add_loop_points fun_name loop_id ids points_infos =
    let points_info =
      if mem fun_name points_infos then find fun_name points_infos
      else PointsInfo.empty in
    let points_info = PointsInfo.add_loop_points loop_id ids points_info in
    add fun_name points_info points_infos    

end

class points_infos points_infos prj =
object inherit Visitor.frama_c_copy prj as super

  val mutable current_fun_name = ""

  method vstmt_aux stmt =
    (* because it is initialized in vfunc *)
    assert (PointsInfos.mem current_fun_name !points_infos) ;
    let points_info = PointsInfos.find current_fun_name !points_infos in
    let _ = match stmt.Cil_types.skind with
      | Cil_types.Goto (stmt_ref, _) ->
	let from_id = stmt.Cil_types.sid in
	let to_id = !stmt_ref.Cil_types.sid in
	let to_from_ids =
	  if PointsInfo.mem_gotoed to_id points_info then
	    PointsInfo.find_gotoed to_id points_info
	  else IntSet.empty in
	let to_from_ids = IntSet.add from_id to_from_ids in
	points_infos :=
	  PointsInfos.add_gotoed current_fun_name to_id to_from_ids
	  !points_infos
      | Cil_types.Loop (_, block, _, _, _) ->
	let loop_id = stmt.Cil_types.sid in
	let ids =
	  if PointsInfo.mem_loop_points loop_id points_info then
	    PointsInfo.find_loop_points loop_id points_info
	  else IntSet.empty in
	let ids = IntSet.add loop_id ids in
	let f_stmts stmt = stmt :: (stmt_subs stmt) in
	let stmts = List.flatten (List.map f_stmts block.Cil_types.bstmts) in
	let f ids stmt = IntSet.add stmt.Cil_types.sid ids in
	let ids = List.fold_left f ids stmts in
	points_infos :=
	  PointsInfos.add_loop_points current_fun_name loop_id ids !points_infos
      | _ -> () in
    Cil.DoChildren

  method vfunc fundec =
    current_fun_name <- fundec.Cil_types.svar.Cil_types.vname ;
    points_infos :=
      PointsInfos.add current_fun_name PointsInfo.empty !points_infos ;
    Cil.DoChildren

end

(** [points_infos ()] returns a mapping that associates to each function of the
    current program in the currently opened project the control points that are
    gotoed to and the control points of loops. *)

let points_infos () : PointsInfos.t =
  let map = ref PointsInfos.empty in
  let points_infos_prj =
    File.create_project_from_visitor "points_infos" (new points_infos map) in
  let f () = !map in
  Project.on points_infos_prj f ()


(*** Value (flat) domain extremes ***)

module BotAndTop = struct

  type t = Bot | Top

  let compare = Pervasives.compare

  let to_string = function
    | Bot -> "bot"
    | Top -> "top"

  let to_cil_term _ = assert false (* should not be used *)

  let top = ArithSig.A Top
  let bot = ArithSig.A Bot

  let neg = function
    | Top -> top
    | Bot -> bot

  let addl a v = match a, v with
    | Bot, _ | _, ArithSig.A Bot -> bot
    | Top, _ -> top

  let addr v a = addl a v

  let minusl a v = match a, v with
    | Bot, _ | _, ArithSig.A Bot -> bot
    | Top, _ -> top

  let minusr v a = match v, a with
    | _, Bot | ArithSig.A Bot, _ -> bot
    | _, Top -> top

  let mull a v = match a, v with
    | Bot, _ | _, ArithSig.A Bot -> bot
    | _, ArithSig.Int 0 -> ArithSig.Int 0
    | Top, _ -> top

  let mulr v a = mull a v

  let divl a v = match a, v with
    | Bot, _ | _, ArithSig.A Bot | _, ArithSig.Int 0 -> bot
    | Top, _ -> top

  let divr v a = match v, a with
    | _, Bot | ArithSig.A Bot, _ -> bot
    | _, Top -> top

  let modl a v = match a, v with
    | Bot, _ | _, ArithSig.A Bot | _, ArithSig.Int 0 -> bot
    | Top, _ -> top

  let modr v a = match v, a with
    | _, Bot | ArithSig.A Bot, _ -> bot
    | _, Top -> top

  let maxl a v = match a, v with
    | Bot, _ | _, ArithSig.A Bot -> bot
    | Top, _ -> top

  let maxr v a = maxl a v

  let lel a v = match a, v with
    | Bot, _ -> true
    | Top, ArithSig.A Top -> true
    | Top, _ -> false

  let ler v a = match v, a with
    | _, Top -> true
    | ArithSig.A Bot, Bot -> true
    | _, Bot -> false

  let ltl a v = match a, v with
    | Bot, ArithSig.A Bot -> false
    | Bot, _ -> true
    | Top, _ -> false

  let ltr v a = match v, a with
    | ArithSig.A Top, Top -> false
    | _, Top -> true
    | _, Bot -> false

  let gel a v = ler v a

  let ger v a = lel a v

  let gtl a v = ltr v a

  let gtr v a = ltl a v

  let compute v = v

end


(*** Arithmetic expressions flat domain ***)

module ArithValDom = struct

  include Arith.Make (BotAndTop)

  let top = A BotAndTop.Top

  let bot = A BotAndTop.Bot

  let join v1 v2 = match v1, v2 with
    | A BotAndTop.Bot, v | v, A BotAndTop.Bot -> v
    | _ when v1 = v2 -> v1
    | _ -> A BotAndTop.Top

  let widen = join

  let narrow v1 v2 = match v1, v2 with
    | A BotAndTop.Top, A _ -> v1
    | A BotAndTop.Top, _ -> v2
    | _ -> v1

  let f_is_concrete v subs_res =
    let b = match v with
      | A _ -> false
      | _ -> true in
    List.fold_left (&&) true (b :: subs_res)

  let is_concrete v = fold f_is_concrete v

  let add_list l = List.fold_left add (Int 0) l

  let last_value rel _ exit_value increment =
    let rel_added = of_int (if is_large rel then 0 else 1) in
    let rel_op = if has_lower_type rel then minus else add in
    add (rel_op exit_value rel_added) increment

  let iteration_nb init_value counter increment =
    div (minus (of_var counter) init_value) increment

end

module Domain = ArithValDom


(*** Abstract cost ***)

module AbsCost = struct

  include (Cost_value.Make (ArithValDom))

end


(*** Requirements for loop termination ***)

module Require = struct

  type t =
      { relation : Domain.relation ;
	init_value : Domain.t ;
	exit_value : Domain.t ;
	increment : Domain.t }

  let compare = Pervasives.compare

  let relation require = require.relation
  let init_value require = require.init_value
  let exit_value require = require.exit_value
  let increment require = require.increment

  let merge f require1 require2 =
    (* each loop has a single condition relation *)
    assert (relation require1 = relation require2) ;
    { relation = relation require1 ;
      init_value = f (init_value require1) (init_value require2) ;
      exit_value = f (exit_value require1) (exit_value require2) ;
      increment = f (increment require1) (increment require2) }

  let join = merge Domain.join
  let widen = merge Domain.widen
  let narrow = merge Domain.narrow

  let le require1 require2 =
    (* each loop has a single condition relation *)
    (relation require1 = relation require2) &&
    (Domain.le (init_value require1) (init_value require2)) &&
    (Domain.le (exit_value require1) (exit_value require2)) &&
    (Domain.le (increment require1) (increment require2))

  let make relation init_value exit_value increment =
    { relation ; init_value ; exit_value ; increment }

  let replace_vars replacements require =
    let init_value = Domain.replace_vars replacements (init_value require) in
    let exit_value = Domain.replace_vars replacements (exit_value require) in
    let increment = Domain.replace_vars replacements (increment require) in
    { require with init_value ; exit_value ; increment }

  let to_string require =
    Printf.sprintf "%s %s %s %s"
      (Domain.string_of_relation (relation require))
      (Domain.to_string (init_value require))
      (Domain.to_string (exit_value require))
      (Domain.to_string (increment require))

end

(*** Associates Require to control points ***)

module Requires = struct

  module M = Misc.Int.Map

  type t = Require.t M.t

  let empty = M.empty

  let mem = M.mem

  let find = M.find

  let merge f =
    let f_merge _ require1 require2 = match require1, require2 with
      | None, None -> None
      | Some require, None | None, Some require -> Some require
      | Some require1, Some require2 -> Some (f require1 require2) in
    M.merge f_merge

  let join = merge Require.join
  let widen = merge Require.widen
  let narrow = merge Require.narrow

  let le requires1 requires2 =
    let f id require1 res =
      res && (mem id requires2) && (Require.le require1 (find id requires2)) in
    M.fold f requires1 true

  let cardinal = M.cardinal

  let fold f requires a =
    let f' _ require a = f require a in
    M.fold f' requires a

  let add = M.add

  let replace_vars replacements = M.map (Require.replace_vars replacements)

  let to_string requires =
    let f id require res =
      Printf.sprintf "%s%d: %s\n%!" res id (Require.to_string require) in
    M.fold f requires ""

end


(*** Point kind ***)

module LoopInfo = struct

  type t =
      { tmp_loop : Cil_types.varinfo ;
	counter : string ;
	relation : Domain.relation ;
	exit_exp : Cil_types.exp ;
	increment : Cil_types.exp ;
	prev_stmts : (Cil_types.stmt * int (* position *)) list ;
	last_stmts : Cil_types.stmt list }

  let tmp_loop loop_info = loop_info.tmp_loop

  let counter loop_info = loop_info.counter

  let relation loop_info = loop_info.relation

  let exit_exp loop_info = loop_info.exit_exp

  let increment loop_info = loop_info.increment

  let prev_stmts loop_info = loop_info.prev_stmts

  let last_stmts loop_info = loop_info.last_stmts

  let make tmp_loop counter relation exit_exp increment prev_stmts last_stmts =
    { tmp_loop ; counter ; relation ; exit_exp ; increment ;
      prev_stmts ; last_stmts }


end

module PointKind = struct

  type t =
    | LoopStart of LoopInfo.t
    | LoopExit of LoopInfo.t
    | ULoopStart (* start of an unrecognized loop *)
    | ULoopExit (* exit of an unrecognized loop *)
    | RegularPoint

  let is_recognized_loop_start = function
    | LoopStart _ -> true
    | _ -> false

  let tmp_loop = function
    | LoopStart loop_info -> LoopInfo.tmp_loop loop_info
    | _ -> raise (Invalid_argument "PointKind.tmp_loop")

end

module PointKinds = struct

  type t = PointKind.t IntMap.t

  let empty = IntMap.empty
  let add = IntMap.add
  let mem = IntMap.mem
  let find = IntMap.find
  let fold = IntMap.fold
  let dom point_kinds = List.map fst (IntMap.bindings point_kinds)

  let mem_loop_start point point_kinds =
    mem point point_kinds &&
    (PointKind.is_recognized_loop_start (find point point_kinds))

  let find_tmp_loop point point_kinds =
    let error = Invalid_argument "PointKinds.find_tmp_loop" in
    PointKind.tmp_loop (IntMap.error_find point point_kinds error)

end


(*** Fun infos ***)

module FunInfo = struct

  type local_vars = (Cil_types.varinfo * string) list * Cil_types.varinfo list

  type t =
      { prototype : local_vars ;
	(* exactly one start and one end points in Frama-C's CFG *)
	start_and_end_points : (int * int) option ;
	nb_loops : int ;
	point_kinds : PointKinds.t }

  let empty =
    { prototype = ([], []) ; start_and_end_points = None ; nb_loops = 0 ;
      point_kinds = PointKinds.empty }

  let make formals locals nb_loops start_and_end_points point_kinds =
    { prototype = (formals, locals) ;
      nb_loops ; start_and_end_points ; point_kinds }

  let prototype fun_info =
    List.map (fun (x, _) -> x.Cil_types.vname) (fst fun_info.prototype)

  let start_and_end_points fun_info = fun_info.start_and_end_points

  let formals_and_locals fun_info = fun_info.prototype

  let point_kinds fun_info = fun_info.point_kinds

  let mem_point point fun_info = PointKinds.mem point fun_info.point_kinds

  let find_point point fun_info = PointKinds.find point fun_info.point_kinds

  let points fun_info = PointKinds.dom fun_info.point_kinds

  let nb_loops fun_info = fun_info.nb_loops

  let add_nb_loops fun_info =
    let nb_loops = fun_info.nb_loops + 1 in
    { fun_info with nb_loops }

  let mem_loop_start point fun_info =
    PointKinds.mem_loop_start point fun_info.point_kinds

  let find_tmp_loop point fun_info =
    PointKinds.find_tmp_loop point fun_info.point_kinds

end

module FunInfos = struct

  type t = FunInfo.t Misc.String.Map.t

  let empty = Misc.String.Map.empty

  let prototypes = Misc.String.Map.map FunInfo.prototype

  let mem = Misc.String.Map.mem

  let add
      fun_name formals locals nb_loops start_and_end_points point_kinds
      fun_infos =
    let fun_info =
      FunInfo.make formals locals nb_loops start_and_end_points point_kinds in
    Misc.String.Map.add fun_name fun_info fun_infos

  let start_and_end_points fun_name fun_infos =
    let error = Invalid_argument "FunInfos.start_and_end_points" in
    let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
    FunInfo.start_and_end_points fun_info

  let formals_and_locals fun_name fun_infos =
    let error = Invalid_argument "FunInfos.formals_and_locals" in
    let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
    FunInfo.formals_and_locals fun_info

  let mem_point fun_name point fun_infos =
    Misc.String.Map.mem fun_name fun_infos &&
    FunInfo.mem_point point (Misc.String.Map.find fun_name fun_infos)

  let find_point fun_name point fun_infos =
    FunInfo.find_point point (Misc.String.Map.find fun_name fun_infos)

  let points fun_name fun_infos =
    let error = Invalid_argument "FunInfos.points" in
    FunInfo.points (Misc.String.Map.error_find fun_name fun_infos error)

  let nb_loops fun_name fun_infos =
    let error = Invalid_argument "FunInfos.nb_loops" in
    FunInfo.nb_loops (Misc.String.Map.error_find fun_name fun_infos error)

  let add_nb_loops fun_name fun_infos =
    let error = Invalid_argument "FunInfos.add_nb_loops" in
    let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
    let fun_info = FunInfo.add_nb_loops fun_info in
    Misc.String.Map.add fun_name fun_info fun_infos

  let mem_loop_start fun_name point fun_infos =
    Misc.String.Map.mem fun_name fun_infos &&
    FunInfo.mem_loop_start point (Misc.String.Map.find fun_name fun_infos)

  let find_tmp_loop fun_name point fun_infos =
    let error = Invalid_argument "FunInfos.find_tmp_loop" in
    let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
    FunInfo.find_tmp_loop point fun_info

  let point_kinds fun_name fun_infos =
    let error = Invalid_argument "FunInfos.point_kinds" in
    let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
    FunInfo.point_kinds fun_info

end


(*** Static environment ***)

module StaticEnv = struct

  type t =
      { fname : string ;
	f_old_name : string ;
	cost_id : string ;
	cost_incr : string ;
	cost_varinfo : Cil_types.varinfo ;
	fun_infos : FunInfos.t ;
	globals : Misc.String.Set.t ;
	extern_costs : string Misc.String.Map.t }

  let init fname f_old_name cost_id cost_incr extern_costs =
    { fname ; f_old_name ; cost_id ; cost_incr ; cost_varinfo = dummy_varinfo ;
      fun_infos = FunInfos.empty ;
      globals = Misc.String.Set.empty ; extern_costs }

  let fname static_env = static_env.fname

  let f_old_name static_env = static_env.f_old_name

  let prototypes static_env = FunInfos.prototypes static_env.fun_infos

  let add_fun_infos
      fun_name formals locals nb_loops start_and_end_points point_kinds
      static_env =
    let fun_infos =
      FunInfos.add fun_name formals locals nb_loops start_and_end_points
	point_kinds static_env.fun_infos in
    { static_env with fun_infos }

  let globals static_env = static_env.globals

  let add_globals x static_env =
    let globals = Misc.String.Set.add x (globals static_env) in
    { static_env with globals }

  let formals_and_locals fun_name static_env =
    FunInfos.formals_and_locals fun_name static_env.fun_infos

  let locals fun_name static_env = snd (formals_and_locals fun_name static_env)
  let formals fun_name static_env = fst (formals_and_locals fun_name static_env)

  let is_local fun_name x static_env =
    let f varinfo = varinfo.Cil_types.vname = x in
    List.exists f (locals fun_name static_env)

  let is_formal fun_name x static_env =
    let (formals, locals) = formals_and_locals fun_name static_env in
    let f_local varinfo = varinfo.Cil_types.vname <> x in
    let f_formal (varinfo, _) = varinfo.Cil_types.vname = x in
    (List.for_all f_local locals) && (List.exists f_formal formals)

  let is_global fun_name x static_env =
    let (formals, locals) = formals_and_locals fun_name static_env in
    let f_local varinfo = varinfo.Cil_types.vname <> x in
    let f_formal (varinfo, _) = varinfo.Cil_types.vname <> x in
    (List.for_all f_local locals) && (List.for_all f_formal formals) &&
    (Misc.String.Set.mem x (globals static_env))

  let cost_id static_env = static_env.cost_id

  let cost_varinfo static_env = static_env.cost_varinfo

  let cost_incr static_env = static_env.cost_incr

  let set_cost_varinfo cost_varinfo static_env =
    { static_env with cost_varinfo }

  let mem_point fun_name point static_env =
    FunInfos.mem_point fun_name point static_env.fun_infos

  let find_point fun_name point static_env =
    FunInfos.find_point fun_name point static_env.fun_infos

  let extern_costs static_env = static_env.extern_costs

  let start_and_end_points fun_name static_env =
    FunInfos.start_and_end_points fun_name static_env.fun_infos

  let mem_fun_name fun_name static_env =
    FunInfos.mem fun_name static_env.fun_infos

  let points fun_name static_env =
    FunInfos.points fun_name static_env.fun_infos

  let nb_loops fun_name static_env =
    FunInfos.nb_loops fun_name static_env.fun_infos

  let add_nb_loops fun_name static_env =
    let fun_infos = FunInfos.add_nb_loops fun_name static_env.fun_infos in
    { static_env with fun_infos }

  let mem_loop_start fun_name point static_env =
    FunInfos.mem_loop_start fun_name point static_env.fun_infos

  let find_tmp_loop fun_name point static_env =
    FunInfos.find_tmp_loop fun_name point static_env.fun_infos

  let point_kinds fun_name static_env =
    FunInfos.point_kinds fun_name static_env.fun_infos

end


(*** Initializations ***)

let special_point f body = match f body with
  | None -> None
  | Some stmt -> Some stmt.Cil_types.sid

let start_point = special_point first_stmt

let end_point = special_point last_stmt

let make_start_and_end_points start_point end_point =
  match start_point, end_point with
    | None, _ | _, None -> None
    | Some start_point, Some end_point -> Some (start_point, end_point)

let make_tmp_names formals =
  let f varinfo = (varinfo, GenName.concat varinfo.Cil_types.vname) in
  List.map f formals

let rec extract_added_value counter e = match e.Cil_types.enode with
  | Cil_types.BinOp (Cil_types.PlusA, e1, e2, _) when exp_is_var counter e1 ->
    Some (counter, e2)
  | Cil_types.BinOp (Cil_types.MinusA, e1, e2, typ)
      when exp_is_var counter e1 ->
    let enode = Cil_types.UnOp (Cil_types.Neg, e2, typ) in
    let e2 = { e2 with Cil_types.enode = enode } in
    Some (counter, e2)
  | Cil_types.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.Cil_types.skind with
    | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) ->
      extract_added_value v.Cil_types.vname e
    | _ ->
      if !debug then
	Format.printf
	  "Could not find increment instruction; found %a instead.\n%!"
	  Cil.d_stmt stmt ;
      None)

let extract_guard block (counter, increment) =
  let open Misc.Option in
  first_stmt block >>=
  (fun stmt -> match stmt.Cil_types.skind with
    | Cil_types.If (e, _, block, _) when starts_with_break block ->
      (match e.Cil_types.enode with
	| Cil_types.BinOp (rel, e1, e2, _)
	    when exp_is_var counter e1 && Domain.is_supported_rel rel ->
	  Some (counter, Domain.rel_of_cil_binop rel, e2, increment)
	| Cil_types.BinOp (rel, e1, e2, _)
	    when exp_is_var counter e2 && Domain.is_supported_rel rel ->
	  let rel = Domain.rel_of_cil_binop rel in
	  let rel = Domain.opposite rel in
	  Some (counter, rel, e1, increment)
	| _ ->
	  if !debug then
	    Format.printf "Unsupported guard condition %a on counter %s.\n%!"
	      Cil.d_exp e counter ;
	  None)
    | Cil_types.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 add_point_kinds
    start_id loop_start_info last_stmts loop_exit_info point_kinds =
  let point_kinds = PointKinds.add start_id loop_start_info point_kinds in
  let f_last_stmts point_kinds stmt =
    PointKinds.add stmt.Cil_types.sid loop_exit_info point_kinds in
  List.fold_left f_last_stmts point_kinds last_stmts

let add_loop_point_kinds id tmp_loop exps prev_stmts last_stmts point_kinds =
  match exps with
    | None ->
      let loop_start_info = PointKind.ULoopStart in
      let loop_exit_info = PointKind.ULoopExit in
      add_point_kinds id loop_start_info last_stmts loop_exit_info point_kinds
    | Some (counter, relation, exit_exp, increment) ->
      let loop_info =
	LoopInfo.make
	  tmp_loop counter relation exit_exp increment prev_stmts last_stmts in
      let loop_start_info = PointKind.LoopStart loop_info in
      let loop_exit_info = PointKind.LoopExit loop_info in
      add_point_kinds id loop_start_info last_stmts loop_exit_info point_kinds

let loop_exits loop_points body =
  let f_exists stmt = not (IntSet.mem stmt.Cil_types.sid loop_points) in
  let f stmt = List.exists f_exists stmt.Cil_types.succs in
  List.filter f (block_subs body)

let stmt_point_kinds fundec points_info point_kinds stmt =
  let id = stmt.Cil_types.sid in
  match stmt.Cil_types.skind with
    | Cil_types.Loop (_, body, _, _, _) ->
      let open Misc.Option in
      assert (PointsInfo.mem_loop_points id points_info) ;
      let loop_points = PointsInfo.find_loop_points id points_info in
      let tmp_loop = GenName.fresh_varinfo fundec in
      let exps = extract_increment body >>= extract_guard body in
      let f_preds res pred =
	let pred_id = pred.Cil_types.sid in
	if IntSet.mem pred_id loop_points then res
	else
	  let succs_id =
	    List.map (fun stmt -> stmt.Cil_types.sid) pred.Cil_types.succs in
	  let opt_pos = Misc.List.pos id succs_id in
	  (* otherwise pred would not be a predecessor of the loop *)
	  assert (opt_pos <> None) ;
	  (pred, Misc.Option.extract opt_pos) :: res in
      let prev_stmts =
	List.fold_left f_preds [] stmt.Cil_types.preds in
      let last_stmts = loop_exits loop_points body in
      let last_stmts = match last_stmt body with
	| None -> last_stmts
	| Some last_stmt -> last_stmt :: last_stmts in
      add_loop_point_kinds id tmp_loop exps prev_stmts last_stmts point_kinds
    | _ when PointKinds.mem id point_kinds -> point_kinds
    | _ -> PointKinds.add id PointKind.RegularPoint point_kinds

class initialize points_infos static_env prj =
object inherit Visitor.frama_c_copy prj as super

  method vglob_aux glob =
    let _ = match glob with
      | Cil_types.GVarDecl (_, varinfo, _) when has_fun_type varinfo ->
	GenName.reset () ;
	GenName.set_prefix "__tmp" ;
	let fun_name = varinfo.Cil_types.vname in
	let formals = formals_of_varinfo varinfo in
	let formals = make_tmp_names formals in
	let locals = [] in
	let nb_loops = 0 in
	let start_and_end_points = None in
	let point_kinds = PointKinds.empty in
	static_env :=
	  StaticEnv.add_fun_infos
	  fun_name formals locals nb_loops start_and_end_points point_kinds
	  !static_env
      | Cil_types.GFun (fundec, _) ->
	GenName.reset () ;
	GenName.set_prefix "__tmp" ;
	let fun_name = fundec.Cil_types.svar.Cil_types.vname in
	(* supposes a good initialization of [points_infos] *)
	assert (PointsInfos.mem fun_name points_infos) ;
	let points_info = PointsInfos.find fun_name points_infos in
	let formals = fundec.Cil_types.sformals in
	let formals = make_tmp_names formals in
	let locals = fundec.Cil_types.slocals in
	let nb_loops = 0 in
	let start_point = start_point fundec.Cil_types.sbody in
	let end_point = end_point fundec.Cil_types.sbody in
	let start_and_end_points =
	  make_start_and_end_points start_point end_point in
	GenName.set_prefix "__tmp_loop" ;
	let point_kinds =
	  List.fold_left (stmt_point_kinds fundec points_info) PointKinds.empty
	    fundec.Cil_types.sallstmts in
	static_env :=
	  StaticEnv.add_fun_infos
	  fun_name formals locals nb_loops start_and_end_points point_kinds
	  !static_env
      | Cil_types.GVar (varinfo, _, _)
	  when varinfo.Cil_types.vname = StaticEnv.cost_id !static_env ->
	static_env := StaticEnv.set_cost_varinfo varinfo !static_env ;
	static_env := StaticEnv.add_globals varinfo.Cil_types.vname !static_env
      | Cil_types.GVar (varinfo, _, _) | Cil_types.GVarDecl (_, varinfo, _) ->
	static_env := StaticEnv.add_globals varinfo.Cil_types.vname !static_env
      | _ -> () in
    Cil.DoChildren

end

let initialize tmp_prefix fname f_old_name cost_id cost_incr extern_costs =
  let points_infos = points_infos () in
  GenName.set_prefix tmp_prefix ;
  let static_env_ref =
    ref (StaticEnv.init fname f_old_name cost_id cost_incr extern_costs) in
  let initialize_prj =
    File.create_project_from_visitor "initialize"
      (new initialize points_infos static_env_ref) in
  let f () = !static_env_ref in
  Project.on initialize_prj f ()


(*** Abstract domains and environments ***)

module type DOMAIN = sig
  type t
  val of_int : int -> t
  val of_var : string -> t
  val top : t
  val bot : t
  val join : t -> t -> t
  val widen : t -> t -> t
  val narrow : t -> t -> t
  val le : t -> t -> bool
  val to_string : t -> string
  val neg : t -> t
  val add : t -> t -> t
  val minus : t -> t -> t
  val mul : t -> t -> t
  val div : t -> t -> t
  val modulo : t -> t -> t
end

module type VARABSENV = sig
  module Domain : DOMAIN
  type t
  val bot       : t
  val top       : t
  val upd       : string -> Domain.t -> t -> t
  val find      : string -> t -> Domain.t
  val init      : Misc.String.Set.t -> (string * string) list -> t
  val join      : t -> t -> t
  val widen     : t -> t -> t
  val narrow    : t -> t -> t
  val le        : t -> t -> bool
  val to_string : t -> string
end

module type ABSENV = sig
  module VarAbsEnv : VARABSENV
  module Domain : DOMAIN
  type t
  type addressed = Misc.String.Set.t
  val cost : t -> AbsCost.t
  val requires : t -> Requires.t
  val set_cost : t -> AbsCost.t -> t
  val add_cost : t -> AbsCost.t -> t
  val add_addressed : t -> addressed -> t
  val set_lval : t -> Cil_types.lval -> Domain.t -> t
  val top_vars : t -> Misc.String.Set.t -> t
  val find : string -> t -> Domain.t
  val bot : t
  val init : Misc.String.Set.t -> (string * string) list -> t
  val join : t -> t -> t
  val widen : t -> t -> t
  val narrow : t -> t -> t
  val le : t -> t -> bool
  val add_require : t -> int -> Require.t -> t
  val to_string : t -> string
end

module MakeVarAbsEnv (D : DOMAIN) : VARABSENV with module Domain = D = struct

  module Domain = D

  type t = Domain.t Misc.String.CMap.t

  let bot = Misc.String.CMap.empty D.bot
  let upd = Misc.String.CMap.upd
  let find = Misc.String.CMap.find

  let init globals formals =
    let f x env = Misc.String.CMap.upd x D.top env in
    let env = Misc.String.Set.fold f globals bot in
    let f env (x, tmp) =
      let env = Misc.String.CMap.upd x (D.of_var tmp) env in
      Misc.String.CMap.upd tmp (D.of_var tmp) env in
    List.fold_left f env formals

  let join = Misc.String.CMap.merge D.join
  let widen = Misc.String.CMap.merge D.widen
  let narrow = Misc.String.CMap.merge D.narrow

  let top = Misc.String.CMap.empty D.top

  let le env1 env2 =
    let f v1 v2 res = res && (Domain.le v1 v2) in
    Misc.String.CMap.cmp f env1 env2 true

  let to_string =
    Misc.String.CMap.to_string (fun x -> x) (fun v -> (D.to_string v) ^ "\n")

end

module MakeAbsEnv (VAE : VARABSENV)
  : ABSENV with module VarAbsEnv = VAE
	   and  module Domain = VAE.Domain = struct

  module VarAbsEnv = VAE
  module Domain = VarAbsEnv.Domain

  type addressed = Misc.String.Set.t

  type t =
      { cost : AbsCost.t ; var_abs_env : VarAbsEnv.t ; addressed : addressed ;
	requires : Requires.t }

  let init globals formals =
    let cost = AbsCost.bot in
    let var_abs_env = VarAbsEnv.init globals formals in
    let addressed = Misc.String.Set.empty in
    let requires = Requires.empty in
    { cost ; var_abs_env ; addressed ; requires }

  let cost env = env.cost

  let requires env = env.requires

  let var_abs_env env = env.var_abs_env

  let find x env = VarAbsEnv.find x (var_abs_env env)

  let set_cost env cost = { env with cost }

  let add_cost env cost = { env with cost = AbsCost.add env.cost cost }

  let addressed env = env.addressed

  let add_addressed env addressed =
    { env with addressed = Misc.String.Set.union env.addressed addressed }

  let set_lval env lval v = match fst lval with
    | Cil_types.Var x ->
      let var_abs_env = VarAbsEnv.upd x.Cil_types.vname v env.var_abs_env in
      { env with var_abs_env }
    | _ -> env

  let top_vars env vars =
    let f x var_abs_env = VarAbsEnv.upd x Domain.top var_abs_env in
    let var_abs_env = Misc.String.Set.fold f vars env.var_abs_env in
    { env with var_abs_env }

  let bot =
    { cost = AbsCost.bot ; var_abs_env = VarAbsEnv.bot ;
      addressed = Misc.String.Set.empty ; requires = Requires.empty }

  let join env1 env2 =
    { cost = AbsCost.join (cost env1) (cost env2) ;
      var_abs_env = VarAbsEnv.join (var_abs_env env1) (var_abs_env env2) ;
      addressed = Misc.String.Set.union (addressed env1) (addressed env2) ;
      requires = Requires.join (requires env1) (requires env2) }

  let widen env1 env2 =
    { cost = AbsCost.widen (cost env1) (cost env2) ;
      var_abs_env = VarAbsEnv.widen (var_abs_env env1) (var_abs_env env2) ;
      addressed = Misc.String.Set.union (addressed env1) (addressed env2) ;
      requires = Requires.widen (requires env1) (requires env2) }

  let narrow env1 env2 =
    { cost = AbsCost.narrow (cost env1) (cost env2) ;
      var_abs_env = VarAbsEnv.narrow (var_abs_env env1) (var_abs_env env2) ;
      addressed = addressed env1 ;
      requires = Requires.narrow (requires env1) (requires env2) }

  let le env1 env2 =
    (AbsCost.le (cost env1) (cost env2)) &&
    (VarAbsEnv.le (var_abs_env env1) (var_abs_env env2)) &&
    (Misc.String.Set.is_subset (addressed env1) (addressed env2)) &&
    (Requires.le (requires env1) (requires env2))

  let add_require env id require =
    { env with requires = Requires.add id require (requires env) }

  let to_string env =
    let f_addressed x res = res ^ x ^ " " in
    "Cost: " ^ (AbsCost.to_string (cost env)) ^ "\n" ^
    "Var env:\n" ^ (VarAbsEnv.to_string (var_abs_env env)) ^
    "Addressed: " ^ (Misc.String.Set.fold f_addressed (addressed env) "") ^
    "\n" ^
    "Requires:\n" ^ (Requires.to_string (requires env)) ^ "\n"

end

module MakePointsAbsEnv (AE : ABSENV) = struct

  module AbsEnv = AE
  module Domain = AbsEnv.Domain

  type t =
      { abs_env : AbsEnv.t IntCMap.t }

  let empty = { abs_env = IntCMap.empty AbsEnv.bot }
  let bot = empty

  let abs_env env = env.abs_env

  let find point env = IntCMap.find point env.abs_env

  let add point abs_env env =
    let abs_env = IntCMap.upd point abs_env env.abs_env in
    { abs_env }

  let le env1 env2 =
    let cmp abs_env1 abs_env2 res = res && (AbsEnv.le abs_env1 abs_env2) in
    IntCMap.cmp cmp (abs_env env1) (abs_env env2) true

  let cost point env = AbsEnv.cost (find point env)

  let requires point env = AbsEnv.requires (find point env)

  let init start_point globals formals =
    add start_point (AbsEnv.init globals formals) empty

  let to_string env =
    IntCMap.to_string string_of_int AbsEnv.to_string (abs_env env)

  let widen env1 env2 =
    let abs_env = IntCMap.merge AbsEnv.widen (abs_env env1) (abs_env env2) in
    { abs_env }

  let narrow env1 env2 =
    let abs_env = IntCMap.merge AbsEnv.narrow (abs_env env1) (abs_env env2) in
    { abs_env }

  let set_cost id cost env = add id (AbsEnv.set_cost (find id env) cost) env

end


module PointsAbsEnv = struct

  module D = Domain

  module VAE = MakeVarAbsEnv (D)

  module AE = MakeAbsEnv (VAE)

  include MakePointsAbsEnv (AE)

end

module AbsEnv  = PointsAbsEnv.AbsEnv


(*** Dependent cost results ***)

module LoopAnnotInfo = struct

  type t =
      { counter : string ;
	relation : Domain.relation ;
	init_value : Domain.t ;
	exit_value : Domain.t ;
	increment : Domain.t ;
	last_value : Domain.t ;
	cost_id : string ;
	tmp_loop : string ;
	iteration_nb : Domain.t ;
	body_cost : AbsCost.t }

  let counter loop_annot_info = loop_annot_info.counter

  let relation loop_annot_info = loop_annot_info.relation

  let init_value loop_annot_info = loop_annot_info.init_value

  let exit_value loop_annot_info = loop_annot_info.exit_value

  let increment loop_annot_info = loop_annot_info.increment

  let last_value loop_annot_info = loop_annot_info.last_value

  let cost_id loop_annot_info = loop_annot_info.cost_id

  let tmp_loop loop_annot_info = loop_annot_info.tmp_loop

  let iteration_nb loop_annot_info = loop_annot_info.iteration_nb

  let body_cost loop_annot_info = loop_annot_info.body_cost

  let make
      counter relation init_value exit_value increment last_value cost_id
      tmp_loop iteration_nb body_cost =
    { counter ; relation ; init_value ; exit_value ; increment ; last_value ;
      cost_id ; tmp_loop ; iteration_nb ; body_cost }

end

module LoopAnnot = struct

  type t =
    | Variant of Domain.t
    | CounterMod of Domain.t * Domain.t
    | CounterLastValue of
	string * Domain.relation * Domain.t * Domain.t * Domain.t
    | NoIteration of string * Domain.relation * Domain.t * Domain.t
    | Cost of string * string * Domain.t * AbsCost.t

  let reduce prototypes costs = function
    | Cost (cost_id, tmp_loop, iteration_nb, body_cost) ->
      let body_cost = AbsCost.reduce prototypes costs body_cost in
      Cost (cost_id, tmp_loop, iteration_nb, body_cost)
    | v -> v

  let compare = Pervasives.compare

  let variant_to_cil v =
    if Domain.is_concrete v then Some (mk_variant (Domain.to_cil_term v))
    else None

  let counter_mod_to_cil v1 v2 =
    if Domain.is_concrete v1 && Domain.is_concrete v2 then
      if v1 = v2 then None
      else
	let v1 = Domain.to_cil_term v1 in
	let v2 = Domain.to_cil_term v2 in
	let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in
	Some (mk_invariant invariant)
    else None

  let counter_last_value_to_cil counter rel init_value exit_value last_value =
    if Domain.is_concrete init_value &&
       Domain.is_concrete exit_value &&
       Domain.is_concrete last_value then
      let init_value = Domain.to_cil_term init_value in
      let exit_value = Domain.to_cil_term exit_value in
      let last_value = Domain.to_cil_term last_value in
      let rel' = Domain.cil_rel_of_rel rel in
      let require = Logic_const.prel (rel', init_value, exit_value) in
      let rel' = Domain.cil_rel_of_rel (Domain.mk_large rel) in
      let counter = cil_logic_int_var counter in
      let prop = Logic_const.prel (rel', counter, last_value) in
      let invariant = Logic_const.pimplies (require, prop) in
      Some (mk_invariant invariant)
    else None

  let no_iteration_to_cil counter rel init_value exit_value =
    if Domain.is_concrete init_value && Domain.is_concrete exit_value then
      let rel = Domain.opposite rel in
      let rel' = Domain.cil_rel_of_rel rel in
      let init_value = Domain.to_cil_term init_value in
      let exit_value = Domain.to_cil_term exit_value in
      let require = Logic_const.prel (rel', init_value, exit_value) in
      let counter = cil_logic_int_var counter in
      let prop = Logic_const.prel (Cil_types.Req, counter, init_value) in
      let invariant = Logic_const.pimplies (require, prop) in
      Some (mk_invariant invariant)
    else None

  let cost_to_cil cost_id tmp_loop iteration_nb body_cost =
    if Domain.is_concrete iteration_nb && AbsCost.is_concrete body_cost then
      let cost_var = cil_logic_int_var cost_id in
      let body_cost = AbsCost.to_ext body_cost in
      let loop_cost = Domain.mul iteration_nb body_cost in
      let cost = Domain.add (Domain.of_var tmp_loop) loop_cost in
      if Domain.is_concrete cost then
	let cost = Domain.to_cil_term cost in
	let invariant = Logic_const.prel (Cil_types.Rle, cost_var, cost) in
	Some (mk_invariant invariant)
      else None
    else None

  let to_cil = function
    | Variant v -> variant_to_cil v
    | CounterMod (v1, v2) -> counter_mod_to_cil v1 v2
    | CounterLastValue(counter, rel, init_value, exit_value, last_value) ->
      counter_last_value_to_cil	counter rel init_value exit_value last_value
    | NoIteration (counter, rel, init_value, exit_value) ->
      no_iteration_to_cil counter rel init_value exit_value
    | Cost (cost_id, tmp_loop, iteration_nb, body_cost) ->
      cost_to_cil cost_id tmp_loop iteration_nb body_cost

  let make_variant loop_annot_info =
    let rel = LoopAnnotInfo.relation loop_annot_info in
    let counter = LoopAnnotInfo.counter loop_annot_info in
    let last_value = LoopAnnotInfo.last_value loop_annot_info in
    let counter_var = Domain.of_var counter in
    let (v1, v2) = match rel with
      | Domain.Lt | Domain.Le -> (last_value, counter_var)
      | Domain.Gt | Domain.Ge -> (counter_var, last_value) in
    Variant (Domain.minus v1 v2)

  let make_counter_mod loop_annot_info =
    let counter = LoopAnnotInfo.counter loop_annot_info in
    let init_value = LoopAnnotInfo.init_value loop_annot_info in
    let increment = LoopAnnotInfo.increment loop_annot_info in
    let mk_value value = Domain.modulo value (Domain.abs increment) in
    let v1 = mk_value (Domain.of_var counter) in
    let v2 = mk_value init_value in
    CounterMod (v1, v2)

  let make_counter_last_value loop_annot_info =
    let counter = LoopAnnotInfo.counter loop_annot_info in
    let rel = LoopAnnotInfo.relation loop_annot_info in
    let init_value = LoopAnnotInfo.init_value loop_annot_info in
    let exit_value = LoopAnnotInfo.exit_value loop_annot_info in
    let last_value = LoopAnnotInfo.last_value loop_annot_info in
    CounterLastValue (counter, rel, init_value, exit_value, last_value)

  let make_no_iteration loop_annot_info =
    let counter = LoopAnnotInfo.counter loop_annot_info in
    let rel = LoopAnnotInfo.relation loop_annot_info in
    let init_value = LoopAnnotInfo.init_value loop_annot_info in
    let exit_value = LoopAnnotInfo.exit_value loop_annot_info in
    NoIteration (counter, rel, init_value, exit_value)

  let make_cost loop_annot_info =
    let cost_id = LoopAnnotInfo.cost_id loop_annot_info in
    let tmp_loop = LoopAnnotInfo.tmp_loop loop_annot_info in
    let iteration_nb = LoopAnnotInfo.iteration_nb loop_annot_info in
    let body_cost = LoopAnnotInfo.body_cost loop_annot_info in
    Cost (cost_id, tmp_loop, iteration_nb, body_cost)

end

module LoopAnnots = struct

  include Eset.Make (LoopAnnot)

  let make loop_annot_info =
    let variant = LoopAnnot.make_variant loop_annot_info in
    (* let counter_mod = LoopAnnot.make_counter_mod loop_annot_info in *)
    let counter_last_value =
      LoopAnnot.make_counter_last_value loop_annot_info in
    let no_iteration = LoopAnnot.make_no_iteration loop_annot_info in
    let cost = LoopAnnot.make_cost loop_annot_info in
    of_list [variant ; (* counter_mod ; *)
	     counter_last_value ; no_iteration ; cost]

  let to_cil loop_annots =
    let f loop_annot res = match LoopAnnot.to_cil loop_annot with
      | Some loop_annot -> loop_annot :: res
      | None -> res in
    fold f loop_annots []

  let reduce prototypes costs loop_annots =
    let f loop_annot res =
      add (LoopAnnot.reduce prototypes costs loop_annot) res in
    fold f loop_annots empty

end

module LoopsAnnots = struct

  type t = LoopAnnots.t IntMap.t

  let empty = IntMap.empty

  let mem = IntMap.mem

  let find = IntMap.find

  let add = IntMap.add

  let to_cil loops_annots =
    IntMap.map LoopAnnots.to_cil loops_annots

  let reduce prototypes costs loops_annots =
    IntMap.map (LoopAnnots.reduce prototypes costs) loops_annots

end

module CostInfo = struct

  type t = { cost : AbsCost.t ; requires : Requires.t ;
	     loops_annots : LoopsAnnots.t }

  let cost cost_info = cost_info.cost

  let requires cost_info = cost_info.requires

  let make cost requires loops_annots = { cost ; requires ; loops_annots }

  let set_cost cost_info cost = { cost_info with cost }

  let init cost =
    { cost ; requires = Requires.empty ; loops_annots = LoopsAnnots.empty }

  let loops_annots cost = cost.loops_annots

  let mem_loop_annots id cost = LoopsAnnots.mem id (loops_annots cost)

  let find_loop_annots id cost = LoopsAnnots.find id (loops_annots cost)

  let to_string cost_info = AbsCost.to_string (cost cost_info)

  let reduce_loops_annots prototypes costs cost_info =
    let loops_annots =
      LoopsAnnots.reduce prototypes costs cost_info.loops_annots in
    { cost_info with loops_annots }

  let replace_vars replacements cost_info =
    let cost = AbsCost.replace_vars replacements (cost cost_info) in
    let requires = Requires.replace_vars replacements (requires cost_info) in
    { cost_info with cost ; requires }

end

module Costs = struct

  type t = CostInfo.t Misc.String.Map.t

  let empty = Misc.String.Map.empty

  let init extern_costs =
    let f fun_name cost costs =
      let cost_info = CostInfo.init (AbsCost.of_extern cost) in
      Misc.String.Map.add fun_name cost_info costs in
    Misc.String.Map.fold f extern_costs empty

  let mem = Misc.String.Map.mem

  let add fun_name cost requires loops_annots costs =
    Misc.String.Map.add fun_name
      (CostInfo.make cost requires loops_annots) costs

  let find_cost fun_name costs =
    CostInfo.cost (Misc.String.Map.find fun_name costs)

  let find_requires fun_name costs =
    CostInfo.requires (Misc.String.Map.find fun_name costs)

  let fun_costs = Misc.String.Map.map CostInfo.cost

  let set_fun_costs costs fun_costs =
    let f fun_name cost_info =
      let cost =
	if Misc.String.Map.mem fun_name fun_costs then
	  Misc.String.Map.find fun_name fun_costs
	else CostInfo.cost cost_info in
      CostInfo.set_cost cost_info cost in
    Misc.String.Map.mapi f costs

  let fold = Misc.String.Map.fold

  let to_string costs =
    let f fun_name cost_info res =
      res ^ "\n" ^ fun_name ^ ": " ^ (CostInfo.to_string cost_info) in
    fold f costs ""

  let mem_loop_point fun_name id costs =
    (Misc.String.Map.mem fun_name costs) &&
    (CostInfo.mem_loop_annots id (Misc.String.Map.find fun_name costs))

  let find_loop_annots fun_name id costs =
    let error = Invalid_argument "Costs.find_loop_annotations" in
    let fun_info = Misc.String.Map.error_find fun_name costs error in
    CostInfo.find_loop_annots id fun_info

  let reduce_loops_annots prototypes costs =
    let fun_costs = fun_costs costs in
    Misc.String.Map.map
      (CostInfo.reduce_loops_annots prototypes fun_costs) costs

  let restore_formals static_env costs =
    let f fun_name cost_info =
      if StaticEnv.mem_fun_name fun_name static_env then
	let formals = StaticEnv.formals fun_name static_env in
	let f (formal, tmp) = (tmp, Domain.of_var formal.Cil_types.vname) in
	let replacements = Misc.String.Map.of_list (List.map f formals) in
	CostInfo.replace_vars replacements cost_info
      else cost_info in
    Misc.String.Map.mapi f costs

end


(*** Abstract interpretation ***)

module MakeAI (M : sig val static_env : StaticEnv.t end) = struct

  let rec addressed e = match e.Cil_types.enode with
    | Cil_types.Const _ | Cil_types.SizeOf _ | Cil_types.SizeOfStr _
    | Cil_types.AlignOf _ ->
      Misc.String.Set.empty
    | Cil_types.Lval lval | Cil_types.AddrOf lval | Cil_types.StartOf lval ->
      lval_addressed lval
    | Cil_types.SizeOfE e | Cil_types.AlignOfE e | Cil_types.UnOp (_, e, _)
    | Cil_types.CastE (_, e) | Cil_types.Info (e, _) -> addressed e
    | Cil_types.BinOp (_, e1, e2, _) ->
      Misc.String.Set.union (addressed e1) (addressed e2)

  and lhost_addressed = function
    | Cil_types.Var _ -> Misc.String.Set.empty
    | Cil_types.Mem e -> addressed e

  and offset_addressed = function
    | Cil_types.Index (e, offset) ->
      Misc.String.Set.union (addressed e) (offset_addressed offset)
    | _ -> Misc.String.Set.empty

  and lval_addressed (lhost, offset) =
    Misc.String.Set.union (lhost_addressed lhost) (offset_addressed offset)

  let branch abs_env _ = [abs_env ; abs_env]

  let abs_fun_of_unop = function
    | Cil_types.Neg -> Domain.neg
    | _ -> (fun _ -> Domain.top)

  let abs_fun_of_binop = function
    | Cil_types.PlusA -> Domain.add
    | Cil_types.MinusA -> Domain.minus
    | Cil_types.Mult -> Domain.mul
    | Cil_types.Div -> Domain.div
    | Cil_types.Mod -> Domain.modulo
    | _ -> (fun _ _ -> Domain.top)

  let rec exp abs_env e = match e.Cil_types.enode with
    | Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
      Domain.of_int (My_bigint.to_int i)
    | Cil_types.Lval (Cil_types.Var varinfo, _) ->
      AbsEnv.find varinfo.Cil_types.vname abs_env
    | Cil_types.Info (e, _) -> exp abs_env e
    | Cil_types.UnOp (unop, e, _) ->
      abs_fun_of_unop unop (exp abs_env e)
    | Cil_types.BinOp (binop, e1, e2, _) ->
      abs_fun_of_binop binop (exp abs_env e1) (exp abs_env e2)
    | Cil_types.CastE (_, e) -> exp abs_env e (* TODO: may be incorrect *)
    | _ -> Domain.top

  let cost_incr_cost = function
    | e :: _ ->
      (match e.Cil_types.enode with
	| Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
	  AbsCost.of_int (My_bigint.to_int i)
	| _ -> AbsCost.top)
    | _ -> AbsCost.top

  let call_proc_cost fun_name abs_env sid f args =
    let f_add_addrd addrd e = Misc.String.Set.union addrd (addressed e) in
    let addrd = List.fold_left f_add_addrd Misc.String.Set.empty (f :: args) in
    let abs_env = AbsEnv.add_addressed abs_env addrd in
    let cost = match f.Cil_types.enode with
      | Cil_types.Lval (Cil_types.Var var, _)
	  when var.Cil_types.vname = StaticEnv.cost_incr M.static_env ->
	cost_incr_cost args
      | Cil_types.Lval (Cil_types.Var var, _) ->
	AbsCost.of_fun_call
	  fun_name sid var.Cil_types.vname (List.map (exp abs_env) args)
      | _ -> AbsCost.top in
    let vars_to_top =
      Misc.String.Set.union (StaticEnv.globals M.static_env) addrd in
    AbsEnv.add_cost (AbsEnv.top_vars abs_env vars_to_top) cost

  (* Executing a goto may create a loop. We over-approximate its cost with a
     Top. There is one exception though: Frama-C transforms programs so that
     there is exactly one return statement that previous return statements in
     the code point to with a goto. So if a goto leads to a return, the cost
     remains the same; in other cases, it is Top. *)

  let stmt_goto abs_env stmt = match stmt.Cil_types.skind with
    | Cil_types.Return _ -> [abs_env]
    | _ -> [AbsEnv.set_cost abs_env AbsCost.top]

  let stmt fun_name abs_env stmt = match stmt.Cil_types.skind with
    | Cil_types.Return _ -> []
    | Cil_types.Break _ | Cil_types.Continue _
    | Cil_types.Loop _ | Cil_types.Block _ | Cil_types.Switch _
    | Cil_types.Instr (Cil_types.Skip _ | Cil_types.Code_annot _) -> [abs_env]
    | Cil_types.Goto (stmt_ref, _) -> stmt_goto abs_env !stmt_ref
    | Cil_types.UnspecifiedSequence l -> make_list (List.length l) abs_env
    | Cil_types.If (e, _, _, _) -> branch abs_env e
    | Cil_types.Instr (Cil_types.Set (lval, e, _)) ->
      let addressed =
	Misc.String.Set.union (lval_addressed lval) (addressed e) in
      let v = exp abs_env e in
      let abs_env = AbsEnv.add_addressed abs_env addressed in
      [AbsEnv.set_lval abs_env lval v]
    | Cil_types.Instr (Cil_types.Call (None, f, args, _)) ->
      [call_proc_cost fun_name abs_env stmt.Cil_types.sid f args]
    | Cil_types.Instr (Cil_types.Call (Some lval, f, args, _)) ->
      let addressed = lval_addressed lval in
      let abs_env = AbsEnv.add_addressed abs_env addressed in
      let abs_env = call_proc_cost fun_name abs_env stmt.Cil_types.sid f args in
      [AbsEnv.set_lval abs_env lval Domain.top]
    | Cil_types.Instr (Cil_types.Asm _) -> raise ASM_unsupported
    | Cil_types.TryFinally _ | Cil_types.TryExcept _ -> raise Try_unsupported

  let merge_succ_regular points_abs_env abs_env stmt =
    let id = stmt.Cil_types.sid in
    let abs_env' = PointsAbsEnv.find id points_abs_env in
    let abs_env' = AbsEnv.join abs_env abs_env' in
    PointsAbsEnv.add id abs_env' points_abs_env

  let merge_succ_uloop_start src_id points_abs_env abs_env =
    let points_abs_env =
      PointsAbsEnv.set_cost src_id AbsCost.top points_abs_env in
    let abs_env = AbsEnv.set_cost abs_env (AbsCost.of_int 0) in
    merge_succ_regular points_abs_env abs_env

  let prev_init_and_cost fun_name counter points_abs_env prev_stmts =
    let f (init_value, before_cost) (stmt_, pos) =
      let abs_env = PointsAbsEnv.find (stmt_.Cil_types.sid) points_abs_env in
      let abs_env = List.nth (stmt fun_name abs_env stmt_) pos in
      let init_value = Domain.join init_value (AbsEnv.find counter abs_env) in
      let before_cost = AbsCost.join before_cost (AbsEnv.cost abs_env) in
      (init_value, before_cost) in
    List.fold_left f (Domain.bot, AbsCost.bot) prev_stmts

  let body_cost points_abs_env last_stmts =
    (* Exiting a loop can only be done through a break or a goto or whatever,
       but certainly not with a cost increment instruction. Thus, executing the
       last statements of a loop should not change the cost information, so its
       unnecessary when this is all we care about. *)
    let f res stmt =
      let id = stmt.Cil_types.sid in
      AbsCost.join res (AbsEnv.cost (PointsAbsEnv.find id points_abs_env)) in
    List.fold_left f AbsCost.bot last_stmts

  let loop_cost fun_name id loop_info points_abs_env abs_env =
    let cost_id = StaticEnv.cost_id M.static_env in
    let tmp_loop = LoopInfo.tmp_loop loop_info in
    let counter = LoopInfo.counter loop_info in
    let relation = LoopInfo.relation loop_info in
    let prev_stmts = LoopInfo.prev_stmts loop_info in
    let last_stmts = LoopInfo.last_stmts loop_info in
    let (init_value, before_cost) =
      prev_init_and_cost fun_name counter points_abs_env prev_stmts in
    let exit_value = exp abs_env (LoopInfo.exit_exp loop_info) in
    let increment = exp abs_env (LoopInfo.increment loop_info) in
    let last_value =
      Domain.last_value relation init_value exit_value increment in
    let iteration_nb = Domain.iteration_nb init_value counter increment in
    let body_cost = body_cost points_abs_env last_stmts in
    let loop_cost =
      if AbsCost.is_top body_cost then AbsCost.top
      else
	AbsCost.of_loop_cost
	  fun_name id relation init_value exit_value increment
	  (AbsCost.extract body_cost) in
    let succ_loop_cost = AbsCost.add before_cost loop_cost in
    (counter, relation, init_value, exit_value, increment, last_value, cost_id,
     tmp_loop, iteration_nb, body_cost, succ_loop_cost)

  let merge_succ_loop_start
      fun_name src_id loop_info points_abs_env points_abs_env' abs_env =
    let src_abs_env = PointsAbsEnv.find src_id points_abs_env in
    let (_, rel, init_value, exit_value, increment, _, _, _, _, _, _) =
      loop_cost fun_name src_id loop_info points_abs_env src_abs_env in
    let require = Require.make rel init_value exit_value increment in
    let abs_env = AbsEnv.add_require abs_env src_id require in
    merge_succ_uloop_start src_id points_abs_env' abs_env

  let merge_succ_loop_exit
      fun_name loop_start_id loop_info points_abs_env points_abs_env'
      abs_env stmt =
    let start_abs_env = PointsAbsEnv.find loop_start_id points_abs_env in
    let (_, _, _, _, _, _, _, _, _, _, succ_loop_cost) =
      loop_cost fun_name loop_start_id loop_info points_abs_env start_abs_env
    in
    let abs_env = AbsEnv.set_cost abs_env succ_loop_cost in
    merge_succ_regular points_abs_env' abs_env stmt

  let merge_succ_uloop_exit points_abs_env abs_env =
    let abs_env = AbsEnv.set_cost abs_env AbsCost.top in
    merge_succ_regular points_abs_env abs_env

  let merge_succ fun_name src_id points_abs_env =
    if StaticEnv.mem_point fun_name src_id M.static_env then
      match StaticEnv.find_point fun_name src_id M.static_env with
	| PointKind.RegularPoint -> merge_succ_regular
	| PointKind.LoopStart loop_info ->
	  merge_succ_loop_start fun_name src_id loop_info points_abs_env
	| PointKind.LoopExit loop_info ->
	  merge_succ_loop_exit fun_name src_id loop_info points_abs_env
	| PointKind.ULoopStart -> merge_succ_uloop_start src_id
	| PointKind.ULoopExit -> merge_succ_uloop_exit
    else raise (Invalid_argument "AI.merge_succ")

  let fundec_stmt fun_name points_abs_env points_abs_env' stmt_ =
    let id = stmt_.Cil_types.sid in
    let abs_env = PointsAbsEnv.find id points_abs_env in
    let abs_envs = stmt fun_name abs_env stmt_ in
    (* Otherwise the [stmt] function is not correct. *)
    assert (List.length abs_envs = List.length stmt_.Cil_types.succs) ;
    let f = merge_succ fun_name id points_abs_env in
    List.fold_left2 f points_abs_env' abs_envs stmt_.Cil_types.succs

  let rec fundec_stmts fun_name points_abs_env cmp merge stmts =
    if !debug then
      Printf.printf "%s\n%!" (PointsAbsEnv.to_string points_abs_env) ;
    let f = fundec_stmt fun_name points_abs_env in
    let points_abs_env' = List.fold_left f PointsAbsEnv.bot stmts in
    let points_abs_env' = merge points_abs_env points_abs_env' in
    if cmp points_abs_env' points_abs_env then
      (if !debug then
	  Printf.printf "%s\n%!" (PointsAbsEnv.to_string points_abs_env') ;
       points_abs_env')
    else fundec_stmts fun_name points_abs_env' cmp merge stmts

  let fundec_stmts_widen fun_name points_abs_env =
    fundec_stmts fun_name points_abs_env PointsAbsEnv.le PointsAbsEnv.widen

  let fundec_stmts_narrow fun_name points_abs_env =
    let cmp env1 env2 = PointsAbsEnv.le env2 env1 in
    fundec_stmts fun_name points_abs_env cmp PointsAbsEnv.narrow

  let loop_annot_info fun_name id points_abs_env loop_info =
    let abs_env = PointsAbsEnv.find id points_abs_env in
    let (counter, relation, init_value, exit_value, last_value, increment,
	 cost_id, tmp_loop, iteration_nb, body_cost, _) =
      loop_cost fun_name id loop_info points_abs_env abs_env in
    LoopAnnotInfo.make
      counter relation init_value exit_value last_value increment cost_id
      tmp_loop.Cil_types.vname iteration_nb body_cost

  let loop_annots fun_name points_abs_env id point_kind loops_annots =
    match point_kind with
      | PointKind.LoopStart loop_info ->
	let loop_annot_info =
	  loop_annot_info fun_name id points_abs_env loop_info in
	let loop_annots = LoopAnnots.make loop_annot_info in
	LoopsAnnots.add id loop_annots loops_annots
      | PointKind.ULoopStart ->
	let loop_annots = LoopAnnots.empty in
	LoopsAnnots.add id loop_annots loops_annots
      | _ -> loops_annots

  let loops_annots fun_name points_abs_env =
    PointKinds.fold (loop_annots fun_name points_abs_env)
      (StaticEnv.point_kinds fun_name M.static_env) LoopsAnnots.empty

end


(*** Dependent costs computation ***)

class compute_costs widen narrow loops_annots static_env costs prj =
object inherit Visitor.frama_c_copy prj as super

  method vfunc fundec =
    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
    if fun_name = StaticEnv.cost_incr static_env then begin
      costs := Costs.add fun_name AbsCost.top Requires.empty
	LoopsAnnots.empty !costs ;
      Cil.SkipChildren end
    else begin
      (* The function should be in the static environment because of the
	 initializations. *)
      assert (StaticEnv.mem_fun_name fun_name static_env) ;
      let _ = match StaticEnv.start_and_end_points fun_name static_env with
	| None ->
	  costs := Costs.add fun_name AbsCost.top Requires.empty
	    LoopsAnnots.empty !costs
	| Some (start_point, end_point) ->
	  if !debug then Printf.printf "Interpreting %s\n%!" fun_name ;
	  let formals = StaticEnv.formals fun_name static_env in
	  let f_formals (varinfo, tmp) = (varinfo.Cil_types.vname, tmp) in
	  let globals = StaticEnv.globals static_env in
	  let formals = List.map f_formals formals in
	  let env = PointsAbsEnv.init start_point globals formals in
	  if !debug then Printf.printf "WIDEN\n%!" ;
	  let env = widen fun_name env fundec.Cil_types.sallstmts in
	  if !debug then Printf.printf "NARROW\n%!" ;
	  let env = narrow fun_name env fundec.Cil_types.sallstmts in
	  let cost = PointsAbsEnv.cost end_point env in
	  let requires = PointsAbsEnv.requires end_point env in
	  let loops_annots = loops_annots fun_name env in
	  (* The last instruction should be a return. Executing it shouldn't
	     change the environment. *)
	  costs := Costs.add fun_name cost requires loops_annots !costs in
      Cil.SkipChildren end

end

let compute_costs static_env =
  let module AI = MakeAI (struct let static_env = static_env end) in
  let costs = ref (Costs.init (StaticEnv.extern_costs static_env)) in
  let compute_costs_prj =	
    File.create_project_from_visitor
      "compute_costs"
      (new compute_costs AI.fundec_stmts_widen AI.fundec_stmts_narrow
	 AI.loops_annots static_env costs) in
  let f () = !costs in
  Project.on compute_costs_prj f ()


(*** Costs solver ***)

let solve_end costs1 costs2 =
  let f fun_name cost res =
    res && (Misc.String.Map.mem fun_name costs1) &&
      (cost = Misc.String.Map.find fun_name costs1) in
  Misc.String.Map.fold f costs2 true

let string_of_fun_costs fun_costs =
  let f fun_name cost res =
    Printf.sprintf "%s%s: %s\n%!" res fun_name (AbsCost.to_string cost) in
  Misc.String.Map.fold f fun_costs ""

let solve_costs static_env costs =
  let costs = Costs.restore_formals static_env costs in
  let fun_costs = Costs.fun_costs costs in
  let prototypes = StaticEnv.prototypes static_env in
  let rec aux fun_costs =
    if !debug then Printf.printf "%s\n%!" (string_of_fun_costs fun_costs) ;
    let fun_costs' = AbsCost.reduces prototypes fun_costs in
    if solve_end fun_costs fun_costs' then fun_costs
    else aux fun_costs' in
  let fun_costs = aux fun_costs in
  let costs = Costs.set_fun_costs costs fun_costs in
  Costs.reduce_loops_annots prototypes costs


(*** Add annotations ***)

let add_tmp_loop_init cost_varinfo tmp_loop stmt =
  let lval = Cil.var tmp_loop in
  let e =
    Cil.new_exp dummy_location (Cil_types.Lval (Cil.var cost_varinfo)) in
  let new_stmt =
    Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in
  let new_stmt = Cil.mkStmt new_stmt in
  Cil.mkStmt (Cil_types.Block (Cil.mkBlock [new_stmt ; stmt]))

let make_tmp_formal_init fundec varinfo tmp_var =
  let tmp_var = Cil.makeTempVar fundec ~name:tmp_var varinfo.Cil_types.vtype in
  let lval = Cil.var tmp_var in
  let e = Cil.new_exp dummy_location (Cil_types.Lval (Cil.var varinfo)) in
  let new_stmt = Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in
  Cil.mkStmt new_stmt

let make_tmp_formals_init fundec l =
  let f (varinfo, tmp_var) = make_tmp_formal_init fundec varinfo tmp_var in
  List.map f l

let add_tmp_formals_init formals fundec =
  let tmp_formals_init = make_tmp_formals_init fundec formals in
  let block = tmp_formals_init @ fundec.Cil_types.sbody.Cil_types.bstmts in
  let body = { fundec.Cil_types.sbody with Cil_types.bstmts = block } in
  { fundec with Cil_types.sbody = body }

let make_require require =
  let rel = Require.relation require in
  let init_value = Require.init_value require in
  let exit_value = Require.exit_value require in
  let increment = Require.increment require in
  if Domain.is_concrete init_value &&
     Domain.is_concrete exit_value &&
     Domain.is_concrete increment then
    let zero = Domain.of_int 0 in
    let rel' = Domain.mk_strict rel in
    let cil_init_value = Domain.to_cil_term init_value in
    let cil_exit_value = Domain.to_cil_term exit_value in
    let cil_zero = Domain.to_cil_term zero in
    let cil_increment = Domain.to_cil_term increment in
    let cil_rel = Domain.cil_rel_of_rel rel in
    let cil_rel' = Domain.cil_rel_of_rel rel' in
    let t1 = Logic_const.prel (cil_rel, cil_init_value, cil_exit_value) in
    let t2 = Logic_const.prel (cil_rel', cil_zero, cil_increment) in
    let t3 = Logic_const.pimplies (t1, t2) in
    Some t3
(*
    if Domain.bool_of_cond rel' zero increment then None
    else
      if Domain.bool_of_cond (Domain.opposite rel) init_value exit_value then
	None
      else
	if Domain.bool_of_cond rel init_value exit_value then Some t2
	else Some t3
*)
  else None

let make_requires requires =
  let f require res =
    let added_require = match make_require require with
    | None -> []
    | Some require -> [require] in
    added_require @ res in
  Requires.fold f requires []

let add_spec pres post spec =
  let requires = List.map Logic_const.new_predicate pres in
  let post_cond = [(Cil_types.Normal, Logic_const.new_predicate post)] in
  let new_behavior = Cil.mk_behavior ~requires ~post_cond () in
  spec.Cil_types.spec_behavior <- new_behavior :: spec.Cil_types.spec_behavior

let add_cost_annotation requires rel cost_id cost spec =
  let post = mk_fun_cost_pred rel cost_id cost in 
  add_spec (make_requires requires) post spec ;
  Cil.ChangeDoChildrenPost (spec, identity)

let add_cost_incr_annotation cost_id fundec =
  let rel = Cil_types.Req in
  let cost =
    Logic_const.tvar (Cil_const.make_logic_var "incr" Cil_types.Linteger)  in
  add_cost_annotation Requires.empty rel cost_id cost fundec 

let add_regular_fun_annotation cost_id requires cost spec =
  if AbsCost.is_concrete cost then
    let cost = AbsCost.to_ext cost in
    let rel = Cil_types.Rle in
    if Domain.is_concrete cost then
      add_cost_annotation requires rel cost_id (Domain.to_cil_term cost) spec
    else Cil.DoChildren
  else Cil.DoChildren

let add_fundec_annotation static_env costs fun_name spec =
  assert (Costs.mem fun_name costs) ;
  let cost = Costs.find_cost fun_name costs in
  let requires = Costs.find_requires fun_name costs in
  let cost_id = StaticEnv.cost_id static_env in
  let cost_incr = StaticEnv.cost_incr static_env in
  if fun_name = cost_incr then add_cost_incr_annotation cost_id spec
  else add_regular_fun_annotation cost_id requires cost spec

class add_annotations static_env costs prj =
object (self) inherit Visitor.frama_c_copy prj as super

  val mutable current_fun_name : string = ""

  method vstmt_aux stmt = match stmt.Cil_types.skind with
    | Cil_types.Loop _
	when StaticEnv.mem_loop_start current_fun_name stmt.Cil_types.sid
	  static_env ->
      let cost_varinfo = StaticEnv.cost_varinfo static_env in
      (* only use with costs correctly set and initialized *)
      assert (Costs.mem_loop_point current_fun_name stmt.Cil_types.sid costs) ;
      let tmp_loop =
	StaticEnv.find_tmp_loop current_fun_name stmt.Cil_types.sid
	  static_env in
      let annots =
	Costs.find_loop_annots current_fun_name stmt.Cil_types.sid costs in
      add_loop_annots self stmt (LoopAnnots.to_cil annots) ;
      let change = add_tmp_loop_init cost_varinfo tmp_loop in
      Cil.ChangeDoChildrenPost (stmt, change)
    | _ -> Cil.DoChildren

  method vfunc fundec =
    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
    current_fun_name <- fun_name ;
    if fun_name = StaticEnv.cost_incr static_env then Cil.DoChildren
    else
      let formals = StaticEnv.formals fun_name static_env in
      Cil.ChangeDoChildrenPost (fundec, add_tmp_formals_init formals)

  method vspec spec = match self#current_kf with
    | None -> Cil.JustCopy 
    | Some kf ->
      match kf.Cil_types.fundec with
	| Cil_types.Definition (fundec, _) ->
	  let fun_name = fundec.Cil_types.svar.Cil_types.vname in
	  add_fundec_annotation static_env costs fun_name spec
	| Cil_types.Declaration (_, f, _, _) ->
	  let fun_name = f.Cil_types.vname in
	  add_fundec_annotation static_env costs fun_name spec

end

let add_annotations static_env costs =
  let add_annotations_prj =	
    File.create_project_from_visitor
      "add_annotations" (new add_annotations static_env costs) in
  let f () =
    Kernel.CodeOutput.set (StaticEnv.fname static_env) ;
    File.pretty_ast () in
  Project.on add_annotations_prj f ()


(*** Save results ***)

let save_results static_env costs =
  let fname = StaticEnv.f_old_name static_env in
  let f fun_name cost_info res =
    let cost = CostInfo.cost cost_info in
    res ^
      (if AbsCost.is_concrete cost then
	  fun_name ^ " " ^ (Domain.to_string (AbsCost.to_ext cost)) ^ "\n"
       else "") in
  let s = Costs.fold f costs "" in
  let save_file =
    try Filename.chop_extension fname
    with Invalid_argument "Filename.chop_extension" -> fname in
  let save_file = save_file ^ ".cost_results" in
  try
    let oc = open_out save_file in
    output_string oc s ;
    close_out oc
  with Sys_error _ ->
    Printf.eprintf "Could not save plug-in results in file %s.\n%!" save_file


(*** Main ***)

let cost ((fname, _), f_old_name, {Cerco.cost_id = cost_id;
                                   cost_incr = cost_incr;
                                   extern_costs = extern_costs} , _) =
  try
    Kernel.Files.set [fname] ;
    File.init_from_cmdline () ;
    if !debug then Printf.printf "Make CFG\n%!" ;
    make_CFG () ;
    if !debug then print_CFG () ;
    if !debug then Printf.printf "Initialize\n%!" ;
    let static_env =
      initialize "__tmp" fname f_old_name cost_id cost_incr extern_costs in
    if !debug then Printf.printf "Compute costs\n%!" ;
    let costs = compute_costs static_env in
    if !debug then Printf.printf "%s\n%!" (Costs.to_string costs) ;
    if !debug then Printf.printf "Solve costs\n%!" ;
    let costs = solve_costs static_env costs in
    if !debug then Printf.printf "Costs:\n%s\n%!" (Costs.to_string costs) ;
    if !debug then Printf.printf "Save results\n%!" ;
    save_results static_env costs ;
    if !debug then Printf.printf "Add annotations\n%!" ;
    add_annotations static_env costs
  with e -> Printf.eprintf "** ERROR: %s.\n%!" (string_of_exception e)