(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
(*                                                                        *)
(*  Copyright (C) 2012                                                    *)
(*    CEA (Commissariat � l'�nergie atomique et aux �nergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Cil_datatype

let init_mpz () =
  let set_mpzt = object
    inherit Cil.nopCilVisitor
    method vglob = function
    | GType({ torig_name = s } as info, _) when s = "mpz_t" ->
      Mpz.set_t info;
      Cil.SkipChildren
    | _ -> 
      Cil.SkipChildren
  end in
  Cil.visitCilFileSameGlobals set_mpzt (Ast.get ())

module Env: sig
  val default_varinfos: Varinfo.Set.t option -> Varinfo.Set.t
  val apply: (kernel_function -> 'a) -> kernel_function -> 'a
  val clear: unit -> unit
  val add: kernel_function -> Varinfo.Set.t option Stmt.Hashtbl.t -> unit
  val find: kernel_function -> Varinfo.Set.t option Stmt.Hashtbl.t 
  module StartData: Dataflow.StmtStartData with type key = stmt
					   and type data = Varinfo.Set.t option
  val is_consolidated: unit -> bool
  val consolidate: Varinfo.Set.t -> unit
  val consolidated_mem: varinfo -> bool
end = struct

  let current_kf = ref (Kernel_function.dummy ())
  let default_varinfos = function None -> Varinfo.Set.empty | Some s -> s 

  let apply f kf =
    let old = !current_kf in
    current_kf := kf;
    let res = f kf in
    current_kf := old;
    res

  let tbl = Kernel_function.Hashtbl.create 7
  let add = Kernel_function.Hashtbl.add tbl
  let find = Kernel_function.Hashtbl.find tbl

  module StartData = struct
    type data = Varinfo.Set.t option
    type key = stmt
    let apply f = 
      try
	let h =  Kernel_function.Hashtbl.find tbl !current_kf in
	f h
      with Not_found -> 
	assert false
    let clear () = apply Stmt.Hashtbl.clear
    let mem k = apply Stmt.Hashtbl.mem k
    let find k = apply Stmt.Hashtbl.find k
    let replace k v = apply Stmt.Hashtbl.replace k v
    let add k v = apply Stmt.Hashtbl.add k v
    let iter f = apply (Stmt.Hashtbl.iter f)
    let length () = apply Stmt.Hashtbl.length
  end

  let consolidated_set = ref Varinfo.Set.empty
  let is_consolidated_ref = ref false

  let consolidate set = 
    let set = Varinfo.Set.fold Varinfo.Set.add set !consolidated_set in
    consolidated_set := set

  let consolidated_mem v = 
    is_consolidated_ref := true;
    Kernel_function.Hashtbl.clear tbl; (* will not be used anymore *)
    Varinfo.Set.mem v !consolidated_set

  let is_consolidated () = !is_consolidated_ref

  let clear () = 
    Kernel_function.Hashtbl.clear tbl;
    consolidated_set := Varinfo.Set.empty;
    is_consolidated_ref := false

end

let reset = Env.clear

module rec Transfer
  : Dataflow.BackwardsTransfer with type t = Varinfo.Set.t option
			       and type StmtStartData.key = stmt
  = struct

  let name = "E_ACSL.Pre_analysis"

  let debug = ref false

  type t = Varinfo.Set.t option

  module StmtStartData = Env.StartData

  let pretty _fmt _state = assert false

  (** The data at function exit. Used for statements with no successors.
      This is usually bottom, since we'll also use doStmt on Return
      statements. *)
  let funcExitData = None

  (** When the analysis reaches the start of a block, combine the old data with
      the one we have just computed. Return None if the combination is the same
      as the old data, otherwise return the combination. In the latter case, the
      predecessors of the statement are put on the working list. *)
  let combineStmtStartData _stmt ~old state = match old, state with
    | _, None -> assert false
    | None, Some _ -> Some state (* [old] already included in [state] *)
    | Some old, Some new_ -> 
      assert (Varinfo.Set.equal old new_);
      None

  (** Take the data from two successors and combine it *)
  let combineSuccessors s1 s2 = 
    Some (Varinfo.Set.union (Env.default_varinfos s1) (Env.default_varinfos s2))

  let rec register_term_lval kf varinfos (thost, _) = match thost with
    | TVar { lv_origin = None } -> Error.not_yet "logic variable"
    | TVar { lv_origin = Some vi } -> 
      Varinfo.Set.add vi varinfos
    | TResult _ -> Varinfo.Set.add (Misc.result_vi kf) varinfos
    | TMem t -> register_term kf varinfos t

  and register_term kf varinfos term = match term.term_node with
    | TConst _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
    | TAlignOfE _ | Tnull | Ttype _ ->
      varinfos
    | TLval tlv | TAddrOf tlv | TStartOf tlv -> 
      register_term_lval kf varinfos tlv
    | TUnOp(_, t) | TCastE(_, t) | Tlambda(_, t) | Tat(t, _) | Tlet(_, t) ->
      register_term kf varinfos t
    | TBinOp(_, t1, t2) | Tif(_, t1, t2) ->
      let s = register_term kf varinfos t1 in
      register_term kf s t2
    | Tapp(_, _, l) -> List.fold_left (register_term kf) varinfos l
    | TDataCons _ -> Error.not_yet "data constructor"
    | Tbase_addr _ -> Error.not_yet "\\base_addr"
    | Toffset _ -> Error.not_yet "\\offset"
    | Tblock_length _ -> Error.not_yet "\\block_length"
    | TCoerce _ -> Error.not_yet "coerce"
    | TCoerceE _ -> Error.not_yet "coerce expression"
    | TUpdate _ -> Error.not_yet "functional update"
    | Ttypeof _ -> Error.not_yet "typeof"
    | Tempty_set -> Error.not_yet "empty set"
    | Tunion _ -> Error.not_yet "set union"
    | Tinter _ -> Error.not_yet "set intersection"
    | Tcomprehension _ -> Error.not_yet "set comprehension"
    | Trange _ -> Error.not_yet "\\range"

  (** The (backwards) transfer function for a branch. The [(Cil.CurrentLoc.get
      ())] is set before calling this. If it returns None, then we have some
      default handling. Otherwise, the returned data is the data before the
      branch (not considering the exception handlers) *)
  let doStmt stmt =
(*    Options.feedback "ANALYSING %a" Cil.d_stmt stmt;*)
    let _, kf = Kernel_function.find_from_sid stmt.sid in
    let is_first =
      try Stmt.equal stmt (Kernel_function.find_first_stmt kf) 
      with Kernel_function.No_Statement -> assert false
    in
    let is_last =
      try Stmt.equal stmt (Kernel_function.find_return kf) 
      with Kernel_function.No_Statement -> assert false
    in
    let register state_ref = object
      inherit Visitor.frama_c_inplace
      method vpredicate = function
      | Pvalid(_, t) | Pvalid_read(_, t) | Pinitialized(_, t)
      | Pallocable(_, t) | Pfreeable(_, t) | Pfresh(_, _, t, _) ->
(*	Options.feedback "REGISTER %a" Cil.d_term t;*)
	state_ref := register_term kf !state_ref t;
	Cil.SkipChildren
      | Pseparated _ -> Error.not_yet "\\separated"
      | Ptrue | Pfalse | Papp _ | Prel _
      | Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _ 
      | Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->
	Cil.DoChildren
      method vterm term = match term.term_node with
      | Tbase_addr(_, t) | Toffset(_, t) | Tblock_length(_, t) ->
	state_ref := register_term kf !state_ref t;
	Cil.SkipChildren
      | TConst _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _  | TLval _ | Tnull
      | Ttype _ | Tempty_set -> 
	(* no sub-term inside: skip for efficiency *)
	Cil.SkipChildren
      | TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TCastE _ | TAddrOf _
      | TStartOf _ | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
      | TCoerce _ | TCoerceE _ | TUpdate _ | Ttypeof _ | Tunion _ | Tinter _
      | Tcomprehension _ | Trange _ | Tlet _ -> 
	(* potential sub-term inside *)
	Cil.DoChildren
      method vlogic_label _ = Cil.SkipChildren
    end in
    let register_predicate pred state = 
      let state_ref = ref state in
      ignore (Visitor.visitFramacIdPredicate (register state_ref) pred);
      !state_ref
    in
    let register_code_annot a state = 
      let state_ref = ref state in
      ignore (Visitor.visitFramacCodeAnnotation (register state_ref) a);
      !state_ref
    in
    Dataflow.Post 
      (fun state -> 
	let state = Env.default_varinfos state in
	let state = 
	  if is_first || is_last then 
	    Annotations.fold_behaviors
	      (fun _ bhv s -> 
		let handle_annot test f s =
		  if test then 
		    f (fun _ p s -> register_predicate p s) kf bhv.b_name s
		  else
		    s
		in
		let s = handle_annot is_first Annotations.fold_requires s in
		handle_annot 
		  is_last 
		  (fun f -> Annotations.fold_ensures (fun e (_, p) -> f e p)) s)
	      kf
	      state
	  else
	    state
	in
	let state = 
	  Annotations.fold_code_annot (fun _ -> register_code_annot) stmt state
	in
	Some state)

  let rec register_exp varinfos e = match e.enode with
    | Lval lv | AddrOf lv | StartOf lv -> 
      (match lv with
      | Var vi, _ -> Varinfo.Set.add vi varinfos
      | Mem e, _ -> register_exp varinfos e)
    | UnOp(_, e, _) | CastE(_, e) | Info(e, _) -> register_exp varinfos e
    | BinOp(_, e1, e2, _) -> 
      let s = register_exp varinfos e1 in
      register_exp s e2
    | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> 
      varinfos

  let base_addr e = 
    let rec aux acc e = match e.enode with
    | Lval lv | AddrOf lv | StartOf lv -> 
      (match lv with
      | Var vi, _ -> [ vi ]
      | Mem e, _ -> aux acc e)
    | BinOp((PlusPI | IndexPI | MinusPI), e1, _, _) -> aux acc e1
    | BinOp(MinusPP, e1, e2, _) -> 
      let acc = aux acc e1  in
      aux acc e2
    | Info(e, _) | CastE(_, e) -> aux acc e
    | BinOp((PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt 
		| Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr),
	    _, _, _)
    | UnOp _ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ 
    | AlignOfE _ -> assert false
    in
    aux [] e

  (** The (backwards) transfer function for an instruction. The
      [(Cil.CurrentLoc.get ())] is set before calling this. If it returns
      None, then we have some default handling. Otherwise, the returned data is
      the data before the branch (not considering the exception handlers) *)
  let doInstr _stmt instr state = 
    let state = Env.default_varinfos state in
    let extend_to_expr state lhost e =
      let add_vi state vi =
	if Varinfo.Set.mem vi state then register_exp state e
	else state
      in
      match lhost with
      | Var vi -> add_vi state vi
      | Mem e -> 
	let l = base_addr e in
	List.fold_left add_vi state l
    in
    match instr with
    | Set((lhost, _), e, _) -> 
      Dataflow.Done (Some (extend_to_expr state lhost e))
    | Call(result, f_exp, l, _) -> 
      (match f_exp.enode with
      | Lval(Var vi, NoOffset) ->
	let kf = Globals.Functions.get vi in
	let state =
	  if Kernel_function.is_definition kf then
	    let state_kf = Compute.get kf in
	    (* keep arguments whenever the corresponding formals must be kept *)
	    try
	      List.fold_left2
		(fun acc p a -> 
		  if Varinfo.Set.mem p state_kf then 
		    extend_to_expr acc (Var p) a 
		  else
		    acc)
		state
		(Globals.Functions.get_params kf)
		l
	    with Invalid_argument _ -> 
	      Error.not_yet "variadic function call"
	  else
	    state
	in
	let state = match result with
	  | None -> state
	  | Some (lhost, _) ->
		(* result of this call must be kept; so keep each argument *)
	    List.fold_left (fun acc e -> extend_to_expr acc lhost e) state l
	in
	Dataflow.Done (Some state)
      | _ ->
	(* imprecise function call: keep each argument *)
	Dataflow.Done 
	  (Some (List.fold_left (fun acc e -> register_exp acc e) state l)))
    | Asm _ -> Error.not_yet "asm"
    | Skip _ | Code_annot _ -> Dataflow.Default

  (** Whether to put this statement in the worklist. This is called when a
      block would normally be put in the worklist. *)
  let filterStmt _predecessor _block = true

  (** Must return [true] if there is a path in the control-flow graph of the
      function from the first statement to the second. Used to choose a "good"
      node in the worklist. Suggested use is [let stmt_can_reach =
      Stmts_graph.stmt_can_reach kf], where [kf] is the kernel_function
      being analyzed; [let stmt_can_reach _ _ = true] is also correct,
      albeit less efficient *)
  let stmt_can_reach stmt = 
    let _, kf = Kernel_function.find_from_sid stmt.sid in
    Stmts_graph.stmt_can_reach kf stmt

end

and Compute: sig val get: kernel_function -> Varinfo.Set.t end = struct

  module D = Dataflow.Backwards(Transfer)

  let compute kf = 
(*    Options.feedback "ANALYSING %a" Kernel_function.pretty kf;*)
    let tbl = Stmt.Hashtbl.create 17 in
    Env.add kf tbl;
    try 
      let init = object
	inherit Visitor.frama_c_inplace
	method vstmt_aux stmt = 
	  Stmt.Hashtbl.add tbl stmt None;
	  Cil.DoChildren
	method vinst _ = Cil.SkipChildren
	method vexpr _ = Cil.SkipChildren
      end
      in
      let fundec = Kernel_function.get_definition kf in
      let stmt = Kernel_function.find_return kf in
      ignore (Visitor.visitFramacFunction init fundec);
      D.compute [ stmt ];
      tbl
    with Kernel_function.No_Definition | Kernel_function.No_Statement -> 
      tbl

  let get kf =
    try
      let stmt = Kernel_function.find_first_stmt kf in
(*      Options.feedback "GETTING %a" Kernel_function.pretty kf;*)
      let tbl = try Env.find kf	with Not_found -> Env.apply compute kf in
      try
	let set = Stmt.Hashtbl.find tbl stmt in
	Env.default_varinfos set
      with Not_found ->
	Options.fatal "stmt never analyzed: %a" Cil.d_stmt stmt
    with Kernel_function.No_Statement -> 
      Varinfo.Set.empty

end

let must_model_vi ?kf vi =
  if Env.is_consolidated () then
    Env.consolidated_mem vi
  else
    match kf with
    | None -> 
      Globals.Functions.iter 
	(fun kf -> 
	  let set = Compute.get kf in
	  Env.consolidate set);
    (*    Options.feedback "MUST MODEL %s? %b (consolidated)" 
	  vi.vname (Env.consolidated_mem vi);*)
      Env.consolidated_mem vi
    | Some kf -> 
      let set = Compute.get kf in
    (*    Options.feedback "MUST MODEL %s? %b" vi.vname (Varinfo.Set.mem vi set);*)
      Varinfo.Set.mem vi set

let rec must_model_lval kf = function
  | Var vi, _ -> must_model_vi ~kf vi
  | Mem e, _ -> must_model_exp kf e

and must_model_exp kf e = match e.enode with
  | Lval lv | AddrOf lv | StartOf lv -> must_model_lval kf lv
  | BinOp((PlusPI | IndexPI | MinusPI), e1, _, _) -> must_model_exp kf e1
  | BinOp(MinusPP, e1, e2, _) -> must_model_exp kf e1 || must_model_exp kf e2
  | Info(e, _) | CastE(_, e) -> must_model_exp kf e
  | BinOp((PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt 
	      | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr),
	  _, _, _)
  | UnOp _ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ 
  | AlignOfE _ -> assert false

(*
Local Variables:
compile-command: "make"
End:
*)