(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Concurrency Plugin for Frama-C               *)
(*                                                                        *)
(*  Copyright (C) 2013                                                    *)
(*    Adelard LLP                                                         *)
(*    CINIF (Control and Instrumentation Nuclear Industry Forum)          *)
(*                                                                        *)
(*  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 3.                                                *)
(*                                                                        *)
(*  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 v3                  *)
(*  for more details (enclosed in the file ./LGPLv3).                     *)
(*                                                                        *)
(**************************************************************************)
open Cil
open Cil_types
open Cil_datatype
open Callgraph
open Visitor

type u_result = 
    {
      entry: kernel_function;
      globvar: varinfo;
      func: varinfo;
      write: bool
    }


(*registering the plugin with frama c*)
module Self = 
              Plugin.Register
              (struct
                let name = "concurrency"
                let shortname = "concur"
		let help = "Simple concurrency analysis plugin"
              end)


(*registering an option for the frama-c command line*)
module Enabled = 
                 Self.False
                 (struct
		   let option_name = "-concur"
                   let help = "Enable the concurrency analysis plugin"
                 end)

module VarOverlap =
                 Self.False
                 (struct
		   let option_name = "-var-overlap"
                   let help = "List overlapping variables between entrypoints"
                 end)

module AccessesFor =
                 Self.String
                 (struct
		   let option_name = "-accesses-for"
		   let default = ""
                   let help = "Show where the given variable is accessed"
		   let arg_name = ""
                 end)
                 
module Mainthread =
                 Self.String
                 (struct
		   let option_name = "-main-thread"
		   let default = ""
                   let help = "Define the main thread against which interactions are computed"
		   let arg_name = ""
                 end)

module FileOfThreads =
                 Self.String
                 (struct
		   let option_name = "-threads"
		   let default = ""
                   let help = "A list of threads (comma separated)"
		   let arg_name = ""
                 end)


(** Custom printer to provide direct printing of variable declarations *)
class printerClass = object
  inherit Printer.extensible_printer () as super
  method pp_vdecl fmt var = super#vdecl fmt var
end
 

(** Visitor class which reports the set of global-life variables used *)
class allVars = 
  object 
    inherit frama_c_inplace
    val mutable seen : Varinfo.Set.t = Varinfo.Set.empty

    method seen = seen

    method! vvrbl v = 
      match v.vstorage with
	NoStorage when not v.vglob -> SkipChildren; (* we don't care about local-scope local-life *)
      | _ -> if not v.vgenerated then seen <- Varinfo.Set.add v seen; SkipChildren; (* static, global, etc. *)
  end

(** Visitor class which reports a list of variables uses *)
class varAccess(locvar:varinfo) =
object(self)
  inherit frama_c_inplace

  val mutable writing : bool = false; (* are we currently reading or writing? *)
  val mutable locs : (Kinstr.t * Kernel_function.t option * bool) list = []; (* locations of variable uses, and a write flag *)
  method locs = List.rev locs;
    

  method! vvrbl v =
    if locvar.vid = v.vid then 
      locs <- (self#current_kinstr,self#current_kf,writing) :: locs; (* record this variable *)
    SkipChildren;

  method! vinst inst =
    begin
      let write_to_var _ o e =
	(* assignment to locvar: write to locvar, read from offset and expression *)
	locs <- (self#current_kinstr,self#current_kf,true) :: self#locs;
	writing <- false;
	ignore (visitFramacOffset (self:>frama_c_visitor) o);
	ignore (visitFramacExpr (self:>frama_c_visitor) e);
      and write_to_expr p o e =
	(* possible assignment to *locvar: write to locvar, read from offset and expression *)
	writing <- true;
	ignore (visitFramacExpr (self:>frama_c_visitor) p);
	writing <- false;
	ignore (visitFramacOffset (self:>frama_c_visitor) o);
	ignore (visitFramacExpr (self:>frama_c_visitor) e);
      and visit_parameters =
	(* make sure we look at the parameters of any function calls considered *)
	List.iter 
	  (fun e -> ignore (visitFramacExpr (self:>frama_c_visitor) e));
      in
      match inst with
      	Set((Var(v),o),e,_) when locvar.vid = v.vid -> 
	  write_to_var v o e;
	  SkipChildren;
      |	Set((Mem(p),o),e,_) -> 
	  write_to_expr p o e;
	  SkipChildren;
      |	Call(Some(Var(v),o),e,es,_) when locvar.vid = v.vid -> 
	  write_to_var v o e;
	  visit_parameters es;
	  SkipChildren;
      |	Call(Some(Mem(p),o),e,es,_) -> 
	  write_to_expr p o e;
	  visit_parameters es;
	  SkipChildren;
      | _ -> DoChildren;
    end
end

(**
 * This searches though all variable uses and searches whether a particular
 * var placed in set_locvar is being used. The result is obtained through 
 * get_g_result : boolean
*)	
class varVisitor(locvar:varinfo) =
object
  inherit frama_c_inplace

  val mutable read : bool = false
  val mutable written : bool = false

  method is_read = read;
  method is_written = written;

  method! vvrbl vu =
    begin
      if locvar.vid = vu.vid then read <- true;
      SkipChildren;
    end

  method! vinst inst =
    begin
      match inst with
	Set((Var(v),_),_,_) -> (* find instructions that are assignments acting on v *)
	  if locvar.vid = v.vid then written <- true;
	  DoChildren;
      |	 _ -> DoChildren;
    end
end


(** Generic depth-first search over the callgraph 
 *   apply f to each fundec found up to depth d (0/default = infinite),
 *   starting from entrypoint function ep *)
let cg_dfs_fundecs cg fn ?(d=0) ep =
  let rec _dfs seen fn d key cn =
    if not (Datatype.Int.Hashtbl.mem seen key) then
      match cn.cnInfo with
	NIVar(v, _) -> 
	  begin
	    match (Globals.Functions.get v).fundec with
	      Definition(f, _) -> 
		Datatype.Int.Hashtbl.add seen key ();
		fn (d!=1) f;
		if d!=1 then 
		  Datatype.Int.Hashtbl.iter (_dfs seen fn (d-1)) cn.cnCallees 
	    | _ -> ()
	  end
      | _ -> ()
  and cn_ep = Hashtbl.find cg (Globals.Functions.get_vi ep).vname
  in
  _dfs (Datatype.Int.Hashtbl.create 10) fn d cn_ep.cnid cn_ep

(** Return the set of variables used in a particular function *)
let variables_used cg ep =
  let vis = new allVars in
  let visfun _ f = 
    let _ = visitFramacFunction (vis:>frama_c_visitor) f in ()
  in
  cg_dfs_fundecs cg visfun ep;
  vis#seen


let computeEntryPoints cg =
  let traverse_cg _ node eps =
    if (Datatype.Int.Hashtbl.length node.cnCallers) == 0 then
      match node.cnInfo with
      | NIVar(a,_) -> (Globals.Functions.get a) :: eps
      | _ -> eps
    else eps
  in 
  Hashtbl.fold traverse_cg cg []




(*The functions above are shared between gui and command line. The following 
functions are command line only *)




(** Finds whether a particular variable is used in a particular function.*)
let find_in_function var_varinfo func =
  let v_vis = new varVisitor var_varinfo in
  let _ = visitFramacFunction (v_vis:>frama_c_visitor) func in ();
  (v_vis#is_read, v_vis#is_written);;

(** Given a varinfo v, find all entry points and functions where it
  * is being used *)
let is_var_being_used v cg eps =
  let visfun b i v ep _ f =
    let (read,write) = find_in_function v f in
    if read then
      let el = {entry=ep; globvar=v; func=f.svar; write=false} in
      b.(!i) <- (Some(el) :: b.(!i));
    if write then
      let el = {entry=ep; globvar=v; func=f.svar; write=true} in
      b.(!i) <- (Some(el) :: b.(!i));
  in

  let do_all_entry_points b i ep = 
    cg_dfs_fundecs cg (visfun b i v ep) ep;
    i := (!i + 1);
  in
  
  let emty = (None : u_result option) in
  let b = (Array.make (List.length eps) [emty]) in
  let index = ref 0 in
  List.iter (do_all_entry_points b index) eps;
  b;;

let show_eps eps =
  Self.result "---Entry points---";
  List.iter (fun f -> Self.result "%s " (Globals.Functions.get_vi f).vname) eps;;

let show_vars_in_common cg f1 fs =
  let main_vars = variables_used cg f1 
  in
  let show_result f1 f2 vs = 
    Self.result "-----------------";
    Self.result "Variables shared by %s and %s:" 
      (Globals.Functions.get_vi f1).vname 
      (Globals.Functions.get_vi f2).vname;
    Varinfo.Set.iter 
      (fun v -> 
	Self.result "%a %s" 
	  Printer.pp_varinfo v
	  (match v.vstorage with
	    NoStorage -> if v.vglob then "(global)" else "(local)"
	  | Static -> "(static)"
	  | Register -> "(register)"
	  | Extern -> 
	    try 
	      (
		let _ = Globals.Functions.get v in
		"(extern function)"
	      )
	    with Not_found -> "(extern)")
      ) vs
  in
  let show_results f1 f2 =
    if f1 != f2 then
      show_result f1 f2
	(Varinfo.Set.inter main_vars (variables_used cg f2))
  in
  List.iter (show_results f1) fs;;

(* Show where and how v is accessed in the callgraph starting from ep *)
let show_var_accesses_for_fun cg v ep =
  let vis = new varAccess v in
  let visfun _ f = 
    let _ = visitFramacFunction (vis:>frama_c_visitor) f in ()
  in
  
  let showresult (i,f,b) =
    let fname = match f with
      Some(f) -> Kernel_function.get_name f
    | None -> "(global)"
    in
    if b then
      Self.result "write at %a in %s" Printer.pp_location (Kinstr.loc i) fname
    else
      Self.result "read at %a in %s" Printer.pp_location (Kinstr.loc i) fname
  in

  cg_dfs_fundecs cg visfun ep;
  if List.length vis#locs > 0 then
    begin
      Self.result "------------------";
      Self.result "Accesses to %s from %s:" v.vname (Globals.Functions.get_vi ep).vname;
      List.iter showresult vis#locs
    end;;

let show_var_accesses cg eps vname =
  let v = Globals.Vars.find_from_astinfo vname VGlobal
  and printer = new printerClass in
  Self.result "------------------";
  Self.result "Declaration: %a" printer#pp_vdecl v;
  Self.result "Basic size in bytes: %d" (Cil.bytesSizeOf v.vtype);
  Self.result "Basic size in bits: %d" (Cil.bitsSizeOf v.vtype);
  List.iter (show_var_accesses_for_fun cg v) eps;;
    
(*   MAIN   *)
let main () =
  if Enabled.get () then 
    begin
      Self.result "Starting concurrency\n";
      let cg = computeGraph (Ast.get ()) in

      (*Obtaining entry points from file or scanning*)
      let eps =  
	match FileOfThreads.get() with
	    "" -> computeEntryPoints cg
	  | str -> 
	    let eps_list = Str.split (Str.regexp ",") str in
	    let get_epses e =
	      try Globals.Functions.find_by_name e
	      with Not_found -> (Self.result "Interrupt %s not found" e ; exit 1)
	    in
	    List.map get_epses eps_list
      in
      
      (*Setting the main thread from command line or simply main()*)
      let main = 
	match Mainthread.get () with
	  "" -> (fst (Globals.entry_point ())) 
	  | mt ->  (
	      try Globals.Functions.find_by_name mt
	      with Not_found -> (Self.result "The main function was not found"; exit 1)
	  )
      in
      
      (*REPORTING PART*)
      show_eps eps;
      if VarOverlap.get () then
        show_vars_in_common cg main eps;
      
      match AccessesFor.get () with	
	  "" -> ()
     	| v -> show_var_accesses cg (main::eps) v;
	  
    (* show_all cg eps *)
     	  
    end;;


(*FileOfThreads*)
(*Extend the frama-C main stage of initialisation with the method main above *)
let () = Db.Main.extend main