(**************************************************************************)
(*                                                                        *)
(*  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).                     *)
(*                                                                        *)
(**************************************************************************)

(**
* This is the main entry for the Concurrency plugin gui.
*)

(*GUIs*)
open Gtk_helper
open Pretty_source 

(*Plugin modules*)
open Concurrency_main
open Cil_datatype 
open Cil_types
open Visitor

(*open Option - was not been able to link this library ExtLib*)
open Concurguiglobs
open Vappgui
open Accessesgui 
open Epsgui


let show_column = ref (fun _ -> ());;	(*the 'Concurrency' column in filetree*)

(** Computes an intersection of the variable sets used by the main thread
 *  and the selected thread*)
let update_var_overlap () =
  if (List.length (SelectedThreads.get ())) > 0  && ((SelectedMain.get) () != init_fundec)
  then
    (
      let main_vars = variables_used (get_option !cg) (SelectedMain.get ()) in
 
      let intersect_vars st f2 =
	if f2 != (SelectedMain.get ()) then
	  Varinfo.Set.inter st (variables_used (get_option !cg) f2)
	else
	  st
      in
 
      let out_set = List.fold_left intersect_vars main_vars (SelectedThreads.get ()) in
	
      VarOverlapSet_ref.set out_set;
    )
  else
    () ;;
 
(** Updates the R/W access locations for a particular variable and thread 
 * and converts this data to the local data holder type*)
let update_acc() =
  if (List.length (SelectedThreads.get ())) > 0  
    && (SelectedMain.get ()) != init_fundec 
      && (LockedVar.get ()) != init_varinfo
  then
    begin
      (*obtains the locs for the current entry point*)
      let get_locs_for_v_from_ep v ep = 
	let vis = new varAccess v in
	let visfun _ f = 
	  let _ = visitFramacFunction (vis:>frama_c_visitor) f in ()
	in
	cg_dfs_fundecs (get_option !cg) visfun ep;
	vis#locs
      in
      
      (*converts locs to the AccessForList type*)
      let to_access_for ep (a, b, c) =
	(ep, a, b, c) 
      in
      
      let main_locs = get_locs_for_v_from_ep (LockedVar.get ()) (SelectedMain.get ()) in
      
      AccessForList.set [];
      AccessForList.set (List.append (AccessForList.get ()) (List.map (to_access_for (SelectedMain.get ())) main_locs));
      
      
      let apply_to_all_eps ep =
	let ep_locs = get_locs_for_v_from_ep (LockedVar.get ()) ep in
	AccessForList.set (List.append (AccessForList.get ()) (List.map (to_access_for ep) ep_locs))
      in
      List.iter apply_to_all_eps (SelectedThreads.get ())
    end ;;

(** Updates the pretty source viewer part of the Frama-C GUI
* to highlight the critical regions in the code.
*)
let concur_highlighter buffer loc ~start ~stop =
  if (List.length (AccessForList.get ())) > 0 then
    begin
      let highlight clr =
	(*make_tag apply_tag are frama-c functions*)
	let tag = make_tag buffer "concurrency" [`BACKGROUND clr ] in
        apply_tag buffer tag start stop
      in 
      
      match loc with
        | PLval (_, ki, (lh,_)) ->     
	  let same_lval ki lh (_,k,_,_) = 
	    (Kinstr.equal ki k) && 
	      match lh with 
		| Var(vi) -> (Varinfo.equal vi (LockedVar.get ()))  
		| _ ->  false 
	  in
	  if List.exists (same_lval ki lh) (AccessForList.get ()) then
 	    highlight "yellow";
	| PTermLval (_,ki,(lh,_)) ->	  
	  let same_tlval ki lh (_,k,_,_) = 
	    (Kinstr.equal ki k) && 
	      match lh with 
		| TVar(tv) ->
		  begin
		    match tv.lv_origin with
		      | Some(vi) -> (Varinfo.equal vi (LockedVar.get ()))  
		      | None ->  false
		  end
		| _ -> false
	  in 
	  if List.exists (same_tlval ki lh) (AccessForList.get ()) then 
	    highlight "yellow"
		
	| PVDecl(_, vi') when Varinfo.equal (LockedVar.get ()) vi' ->
	  highlight "yellow"
	    
        | PVDecl _ | PStmt _ | PGlobal _ | PIP _ -> ()
    end;;

(** Configures the concurrency plugin side panel and loads the additional forms. 
*)
let concurrency_panel main_ui =  
  let eps_display = new vEpsWindow in 			(*entry points form*)
  let var_overlap_display = new vAppWindow in		(*intersected variables form*)
  let access_display = new vAccWindow main_ui in	(*access form*) 

  (*setup the side panel*)
  let v_box = GPack.vbox () in 
  let h0_box = GPack.hbox ~packing: v_box#pack () in
  let _ = GMisc.label 
    ~xalign:0.0 
    ~text:"Filter:" 
    ~width:100
    ~packing:(h0_box#pack ~expand:false) () 
  in
  let open_ep_filter = GButton.button ~label:"Entry Points" ~packing:h0_box#pack () in
 
  ignore (open_ep_filter#connect#pressed (fun () -> eps_display#show_eps ()));

  (*Create Main combo and label*)
  let h2_box = GPack.hbox ~packing: v_box#pack () in

  let _ = GMisc.label 
    ~xalign:0.0 
    ~text:"Current main: "
    ~width:100
    ~packing:(h2_box#pack ~expand:false) () 
  in

  let main_combo = GEdit.combo_box_text ~strings:[] 
    ~has_frame:true ~packing:h2_box#pack () 
  in
  
  (*Populates the main entry point combo box with 
    selection of available entry points*)
  let populate_main () =
    let add_eps_to_combo ep = 
      let ep_name = (Kernel_function.get_name ep) in
      GEdit.text_combo_add main_combo ep_name
    in
    let (_,(a,_)) = main_combo in
    a#clear ();
    List.iter add_eps_to_combo (FilteredEntryPoints.get ()) 
  in

  let (a,_) = main_combo in
  ignore(a#connect#changed (fun () -> 
    let mn = match GEdit.text_combo_get_active main_combo with
      | Some(a) -> Globals.Functions.find_by_name a
      | None ->   init_fundec
    in
    if mn != init_fundec then
      begin
	SelectedMain.set mn; 
	LockedVar.set  init_varinfo; 
	AccessForList.set []; 
	SelectedThreads.set [];
	VarOverlapSet_ref.set Varinfo.Set.empty;
	refresh := (false,true,true,true,false)	(*update gui*)
      end));
 
  (*Create E.P. combo and label*)
  let h3_box = GPack.hbox ~packing: v_box#pack () in

  let _ = GMisc.label 
    ~xalign:0.0 
    ~text:"Current E.P.: " 
    ~width:100
    ~packing:(h3_box#pack ~expand:false) () 
  in

  let eps_combo = GEdit.combo_box_text ~strings:[] ~has_frame:true ~packing:h3_box#pack () in

  (* Populates the Entry Points combo with the 
  available entry points except what was selected as a main entry point*)
  let populate_eps () =
    let current_main = match GEdit.text_combo_get_active main_combo with
      | Some(a) -> a
      | None -> ""
    in
    let add_eps_to_combo ep = 
      let ep_name = (Kernel_function.get_name ep) in
      if not (ep_name = current_main) then
	GEdit.text_combo_add eps_combo ep_name
    in
    let (_,(a,_)) = eps_combo in
    a#clear ();
    List.iter add_eps_to_combo (FilteredEntryPoints.get ()) 
  in
  let (a,_) = eps_combo in
  ignore(a#connect#changed (
    fun () -> 
      let ep = match GEdit.text_combo_get_active eps_combo with
	| Some(a) -> Globals.Functions.find_by_name a
	| None ->  init_fundec
      in
      if ep != init_fundec then
	begin
	  SelectedThreads.set [ep];
	  LockedVar.set  init_varinfo; 
	  VarOverlapSet_ref.set Varinfo.Set.empty;
	  AccessForList.set [];
	  refresh := (false,false,true,true,false) (*update gui*)
	end));

  (*Create the currently selected variable combo box*)
  let h1_box = GPack.hbox ~packing: v_box#pack () in
  
  let _ = GMisc.label 
    ~xalign:0.0 
    ~text:"Current variable:" 
    ~width:100
    ~packing:(h1_box#pack ~expand:false) () 
  in
 
  let var_combo = GEdit.combo_box_text ~strings:[] ~has_frame:true ~packing:h1_box#pack () in

  (*Populates the combo box with the current 
  variables shared between main and EP thread.*)
  let populate_var () = 
    let (a,(b,_)) = var_combo in
    let add_vars_to_combo vi c =
      if not (Cil.isFunctionType vi.vtype) then begin
        GEdit.text_combo_add var_combo vi.vname;
      
        (*the purpose of this is to activate the currently selected variable*)
        if vi.vname == (LockedVar.get ()).vname then
	  a#set_active c; (*how to get the number of elements added*)
        c+1
      end
      else c
    in
    b#clear (); 
    ignore(Varinfo.Set.fold  add_vars_to_combo (VarOverlapSet_ref.get ()) 0);
  in

  let (a,_) = var_combo in
  ignore(a#connect#changed (fun () ->  
    let vi = match GEdit.text_combo_get_active var_combo with
      | Some(a) ->
        (try Globals.Vars.find_from_astinfo a VGlobal
         with Not_found -> init_varinfo)
      | None ->  init_varinfo
    in
    if vi != init_varinfo then
      LockedVar.set vi;
    AccessForList.set [];
    refresh := (false, false, false, true, false) (*update gui*)
  ));

  (*create buttons*)
  let show_vapp = GButton.button ~label:"Details" ~packing:h1_box#pack () in
 
  ignore (show_vapp#connect#pressed (fun () -> var_overlap_display#show_vapp ()));
  
  let h4_box = GPack.hbox ~packing: v_box#pack () in 
  let _ = GMisc.label 
    ~xalign:0.0 
    ~text:"Compute:" 
    ~width:100
    ~packing:(h4_box#pack ~expand:false) () 
  in

  let button_access_details = GButton.button ~label:"Show Details" ~packing:h4_box#pack () in
  ignore (button_access_details#connect#pressed(fun () -> update_acc (); access_display#show_acc ()));

  (* Drives the GUI statemachine updating the Concurrency section of the GUI*)
  let refresh = fun () -> 
    begin 
      (*We could replace this by some sort of signal*)
      let (m,e,v,g,_) = !refresh in
      if m then
	populate_main ();

      (*main has changed*)
      if e then
	populate_eps ();
      
      (*main or eps have changed*)
      if v then 
	begin
	  update_var_overlap (); 
	  populate_var ();
	  !show_column `Visibility
	end;

      (*main or eps or var have changed*)
      if g then
	begin
	  populate_var (); 
	  update_acc ();
	  !show_column `Visibility
	end;

     if m || e || v || g then
       (
	 var_overlap_display#refresh ();
	 access_display#refresh (); 
	 main_ui#rehighlight ();
       );

     
      refresh := (false,false, false, false, false)
    end	
  in
  "Concurrency", v_box#coerce, Some refresh 
;;     

(** Decorates the file tree Concurrency colum to show the 
 * functions where a particular variable is used.
*)
let file_tree_decorate (file_tree:Filetree.t) =
  show_column := 
    file_tree#append_pixbuf_column 
    ~title:"Concurrency"
    (fun globs ->
      if  List.length (AccessForList.get ()) > 0 then
	begin
          let in_globals (_,ki,_,_) =
            match ki with
              | Kglobal -> false
              | Kstmt stmt ->
		let kf = Kernel_function.find_englobing_kf stmt in
		let {vid=v0} = Kernel_function.get_vi kf in
		List.exists
                  (fun glob -> match glob with
                    | GFun ({svar ={vid=v1}},_ ) -> v1=v0
                    |  _ -> false)
                  globs
          in
          if (List.exists in_globals (AccessForList.get ())) then [`STOCK_ID "gtk-apply"]
          else [`STOCK_ID ""]
	end
      else
        [`STOCK_ID ""])
    (fun () -> not (Varinfo.equal (LockedVar.get ()) init_varinfo));
  !show_column `Visibility ;;


let concur_gui_f main_ui= 
  (*init*)
  start_concurrency ();
  Self.result "Starting concur plugin";
  (*menu accessible from right clicking on the source viewer*)
  (*main_ui#register_source_selector concur_menu_item;*)
  (*highlights in main code display when necessary parameters of the plugin 
  are set*)
  main_ui#register_source_highlighter concur_highlighter;
  main_ui#register_panel concurrency_panel;
  file_tree_decorate main_ui#file_tree;
;;

(*Register the main_gui function as enty point for Concur GUI*)
let () = Design.register_extension concur_gui_f ;;