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