1
(**************************************************************************)
3
(* This file is part of Frama-C. *)
5
(* Copyright (C) 2007-2008 *)
6
(* CEA (Commissariat � l'�nergie Atomique) *)
7
(* INRIA (Institut National de Recherche en Informatique et en *)
10
(* you can redistribute it and/or modify it under the terms of the GNU *)
11
(* Lesser General Public License as published by the Free Software *)
12
(* Foundation, version 2.1. *)
14
(* It is distributed in the hope that it will be useful, *)
15
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
16
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
17
(* GNU Lesser General Public License for more details. *)
19
(* See the GNU Lesser General Public License version v2.1 *)
20
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
22
(**************************************************************************)
24
(*i $Id: register_gui.ml,v 1.35 2008/12/16 10:02:59 uid526 Exp $ i*)
30
(struct include Datatype.Bool
31
let default () = false
34
let name = "Slicing_gui.State"
39
(* for slicing callback *)
40
let mk_selection fselect = fselect (!Db.Slicing.Select.empty_selects ())
42
(* for slicing callback *)
43
let mk_selection_cad fselect =
44
mk_selection fselect (!Db.Slicing.Mark.make ~ctrl:true ~addr:true ~data:true)
46
(* for slicing callback *)
47
let mk_selection_all fselect =
48
mk_selection fselect ~spare:false
50
(* for slicing callback *)
51
let mk_slice selection =
52
let n = string_of_int (1 + List.length (!Db.Slicing.Project.get_all ())) in
53
let project = !Db.Slicing.Project.mk_project ("Slicing "^ n) in
54
!Db.Slicing.Request.add_persistent_selection project selection ;
55
!Db.Slicing.Request.apply_all_internal project;
56
if Cmdline.Slicing.Mode.Callers.get () then
57
!Db.Slicing.Slice.remove_uncalled project;
58
let new_project = !Db.Slicing.Project.extract ((!Db.Slicing.Project.get_name project)^ " export") project in
59
!Db.Slicing.Project.set_project (Some (project)) ;
62
(* To add a sensitive/unsensitive menu item to a [factory] *)
63
let add_item (factory:GMenu.menu GMenu.factory) ~callback name arg_opt =
65
| None -> (* add the menu item, but it isn't sensitive *)
66
let item = factory#add_item name ~callback:(fun () -> ())
67
in item#misc#set_sensitive false
68
| Some arg -> (* add the menu item with its callback *)
69
ignore (factory#add_item name ~callback:(fun () -> callback arg))
71
(* To inform the user about a status. *)
72
let gui_annot_info (main_ui:Design.main_window_extension_points) ~level txt =
73
if (Cmdline.Slicing.Mode.Verbose.get () >= level) then
75
main_ui#annot_window#buffer#insert ((txt ()) ^ ".\n")
78
(* To inform the user about an action. *)
79
let gui_annot_action (main_ui:Design.main_window_extension_points) txt =
80
if (Cmdline.Slicing.Mode.Verbose.get () >= 0) then
82
let tag_style_italic = Gtk_helper.make_tag main_ui#annot_window#buffer ~name:"slicing:style italic" [`STYLE `ITALIC] in
83
main_ui#annot_window#buffer#insert ~tags:[tag_style_italic] ((txt ()) ^ "\n")
86
(* To inform the user about an error. *)
87
let gui_annot_error (main_ui:Design.main_window_extension_points) txt =
88
let tag_style_italic = Gtk_helper.make_tag main_ui#annot_window#buffer ~name:"slicing:style italic" [`STYLE `OBLIQUE ; ] in
89
main_ui#annot_window#buffer#insert ~tags:[tag_style_italic] (txt ^ ".\n")
91
let gui_mk_slice main_ui selection ~info =
93
gui_annot_action main_ui info;
94
main_ui#lock () in (* lock the gui while ... *)
95
let new_project = mk_slice selection in (* ... slicing computation *)
96
main_ui#unlock already_locked ;
97
gui_annot_action main_ui (fun () -> "Slice exported to project: " ^ (Project.name new_project));
98
main_ui#rehighlight ()
100
let gui_compute_values (main_ui:Design.main_window_extension_points) =
101
if not (Db.Value.is_computed ()) then
103
gui_annot_action main_ui (fun () -> "Activating slicing plugin by running value analysis first");
104
let already_locked = main_ui#lock () in
105
(try !Db.Value.compute ();
106
with Globals.No_such_entry_point msg -> gui_annot_error main_ui msg);
107
main_ui#unlock already_locked
110
(* To do an action and inform the user. *)
111
let gui_apply_action (main_ui:Design.main_window_extension_points) f x ~info =
113
gui_annot_action main_ui info
115
let get_setting_option_text txt = "Setting option " ^ txt ^ " for the current project"
117
let gui_toggle_slice_undef (main_ui:Design.main_window_extension_points) =
118
let slice_undef = not (Cmdline.Slicing.Mode.SliceUndef.get ()) in
119
gui_apply_action main_ui Cmdline.Slicing.Mode.SliceUndef.set slice_undef
122
if slice_undef then (get_setting_option_text "-slice-undef-functions" )^
123
". Allow the use of the slicing level for calls to undefined functions"
124
else (get_setting_option_text "-no-slice-undef-functions") ^
125
". Forbid the slicing of prototypes of undefined functions")
127
let gui_set_project (main_ui:Design.main_window_extension_points) proj_opt =
128
gui_apply_action main_ui !Db.Slicing.Project.set_project proj_opt
130
Extlib.may_map ~dft:"Clear slicing highlighting"
131
(fun project -> ("Highlighting for " ^ (!Db.Slicing.Project.get_name project)))
133
main_ui#rehighlight ()
135
let slicing_selector (popup_factory:GMenu.menu GMenu.factory)
136
(main_ui:Design.main_window_extension_points) ~button localizable =
137
if not (Db.Value.is_computed ()) then
138
ignore (popup_factory#add_item "Activate _Slicing"
139
~callback:(fun () -> gui_compute_values main_ui ))
140
else if not (Enable.get ()) then
141
ignore (popup_factory#add_item "Enable _Slicing menu"
142
~callback:(fun () -> Enable.set true))
144
let slicing_project = !Db.Slicing.Project.get_project () in
146
begin let level = 0 in
147
let slicing_view project =
148
gui_annot_info main_ui ~level (fun () -> "Highlighting for " ^ (!Db.Slicing.Project.get_name project))
150
Extlib.may slicing_view slicing_project;
151
if Cmdline.Slicing.Mode.Verbose.get () > level then begin
152
let slicing_mark project =
153
let slicing_mark kf get_mark =
154
(* use -slicing-debug -verbose to get slicing mark information *)
155
let add_mark_info txt = gui_annot_info ~level main_ui (fun () -> "Tag: " ^ (txt ())) in
156
let slices = !Db.Slicing.Slice.get_all project kf in
158
| [] -> (* No slice for this kf *)
159
add_mark_info (fun () ->
160
if !Db.Slicing.Project.is_called project kf
161
then (* but the source function is called *)
162
(Cil.fprintf_to_string "<src>%a"
163
!Db.Slicing.Mark.pretty (!Db.Slicing.Mark.get_from_src_func project kf))
167
if !Db.Slicing.Project.is_called project kf
168
then begin (* The source function is also called *)
169
assert (not (kf == fst (Globals.entry_point ()))) ;
170
add_mark_info (fun () ->
171
Cil.fprintf_to_string "<src>%a"
172
!Db.Slicing.Mark.pretty (!Db.Slicing.Mark.get_from_src_func project kf))
174
let mark_slice slice =
175
add_mark_info (fun () -> Cil.fprintf_to_string "%a" !Db.Slicing.Mark.pretty (get_mark slice))
176
in List.iter mark_slice slices
177
in match localizable with
178
| Pretty_source.PTermLval(Some kf,(Kstmt ki),_) (* as for the statement *)
179
| Pretty_source.PLval (Some kf,(Kstmt ki),_) (* as for the statement *)
180
| Pretty_source.PStmt (kf,ki) -> slicing_mark kf (fun slice -> !Db.Slicing.Slice.get_mark_from_stmt slice ki)
181
| Pretty_source.PVDecl (Some kf,vi) -> slicing_mark kf (fun slice -> !Db.Slicing.Slice.get_mark_from_local_var slice vi)
183
in Extlib.may slicing_mark slicing_project
186
else if button = 3 then begin
187
let submenu = popup_factory#add_submenu "Slicing" in
188
let slicing_factory = new GMenu.factory submenu in
189
(* definitions for slicing plug-in *)
190
let add_slicing_item name = add_item slicing_factory name in
191
let mk_slice = gui_mk_slice main_ui in
192
let add_slice_menu kf_opt kf_ki_opt =
194
add_slicing_item "Slice calls to"
198
~info:(fun () -> Cil.fprintf_to_string "Request for slicing effects of function %a"
199
Kernel_function.pretty_name kf)
200
((mk_selection_all !Db.Slicing.Select.select_func_calls_to) kf));
201
add_slicing_item "Slice calls into"
205
~info:(fun () -> Cil.fprintf_to_string "Request for slicing entrance into function %a"
206
Kernel_function.pretty_name kf)
207
((mk_selection_all !Db.Slicing.Select.select_func_calls_into) kf));
208
add_slicing_item "Slice result"
209
(Extlib.opt_filter (fun kf ->
210
let is_not_void_kf x =
211
match x.Cil_types.vtype with
212
| Cil_types.TFun (Cil_types.TVoid (_),_,_,_) -> false
214
in is_not_void_kf (Kernel_function.get_vi kf))
218
~info:(fun () -> Cil.fprintf_to_string "Request for returned value of function %a"
219
Kernel_function.pretty_name kf)
220
((mk_selection_all !Db.Slicing.Select.select_func_return) kf));
221
add_slicing_item "Slice stmt"
223
~callback:(fun (kf, ki) ->
225
~info:(fun () -> Cil.fprintf_to_string "Request for slicing effects of statement %d"
227
((mk_selection_all !Db.Slicing.Select.select_stmt) ki kf));
228
add_slicing_item "Slice lval"
230
~callback:(fun (kf, ki) ->
231
let do_with_txt txt =
233
let lval_str = Cilutil.StringSet.add txt Cilutil.StringSet.empty in
235
~info:(fun () -> Cil.fprintf_to_string "Request for slicing Lvalue %s before statement %d"
238
((mk_selection_cad !Db.Slicing.Select.select_stmt_lval)
239
lval_str ~before:true ki ~scope:ki ~eval:ki kf)
240
with e -> main_ui#error "Invalid expression: %s" (Printexc.to_string e)
243
GToolbox.input_string
244
~title:"Input a pure Lvalue expression to slice before current statement"
246
in Extlib.may do_with_txt txt);
247
add_slicing_item "Slice rd"
249
~callback:(fun (kf, ki) ->
250
let do_with_txt txt =
252
let lval_str = Cilutil.StringSet.add txt Cilutil.StringSet.empty in
254
~info:(fun () -> Cil.fprintf_to_string "Request for slicing read accesses to Lvalue %s"
256
((mk_selection_cad !Db.Slicing.Select.select_func_lval_rw)
257
~rd:lval_str ~wr:Cilutil.StringSet.empty ~scope:ki ~eval:ki kf)
258
with e -> main_ui#error "Invalid expression: %s" (Printexc.to_string e)
261
GToolbox.input_string
262
~title:"Input a pure Lvalue expression to slice read accesses"
264
in Extlib.may do_with_txt txt);
265
add_slicing_item "Slice wr"
267
~callback:(fun (kf, ki) ->
268
let do_with_txt txt =
270
let lval_str = Cilutil.StringSet.add txt Cilutil.StringSet.empty in
272
~info:(fun () -> Cil.fprintf_to_string "Request for slicing writen accesses to Lvalue %s"
274
((mk_selection_cad !Db.Slicing.Select.select_func_lval_rw)
275
~rd:Cilutil.StringSet.empty ~wr:lval_str ~scope:ki ~eval:ki kf)
276
with e -> main_ui#error "Invalid expression: %s" (Printexc.to_string e)
279
GToolbox.input_string
280
~title:"Input a pure Lvalue expression to slice read accesses"
282
in Extlib.may do_with_txt txt);
283
add_slicing_item "Slice ctrl"
285
~callback:(fun (kf, ki) ->
287
~info:(fun () -> Cil.fprintf_to_string "Request for slicing accessibility to statement %d"
289
((mk_selection_all !Db.Slicing.Select.select_stmt_ctrl) ki kf))
291
let some_kf_from_vi vi =
292
try let kf = Globals.Functions.get vi in
293
if Enable.get () && !Db.Value.is_called kf then Some kf else None
294
with Not_found -> None in
295
let some_kf_from_lv lv =
297
| Var vi,_ -> some_kf_from_vi vi
299
let some_kf_ki kf ki =
301
&& !Db.Value.is_called kf
302
&& Db.Value.is_accessible (Cil_types.Kstmt ki)
303
then Some (kf, ki) else None in
304
begin (* add menu for slicing and scope plug-in *)
305
match localizable with
306
| Pretty_source.PLval (Some kf,(Kstmt stmt),lv) ->
307
add_slice_menu (some_kf_from_lv lv) (some_kf_ki kf stmt)
308
| Pretty_source.PTermLval(Some kf,(Kstmt ki),_) (* as for the statement *)
309
| Pretty_source.PStmt (kf,ki) ->
310
add_slice_menu None (some_kf_ki kf ki)
311
| Pretty_source.PVDecl (_,vi) ->
312
add_slice_menu (some_kf_from_vi vi) None
314
add_slice_menu None None
316
let projects = !Db.Slicing.Project.get_all() in
317
ignore (slicing_factory#add_separator ());
318
add_slicing_item "_Disable"
320
~callback:(fun () -> Enable.set false);
321
add_slicing_item "_Clear"
322
(if slicing_project = None then None else Some ())
323
~callback:(fun () -> gui_set_project main_ui None) ;
326
let add_highlight_menu sensitive =
328
("Highlight " ^ (Pretty_utils.escape_underscores (!Db.Slicing.Project.get_name proj)))
330
~callback:(fun () -> gui_set_project main_ui (Some proj))
331
in match slicing_project with
332
| Some project -> add_highlight_menu (if (proj == project) then None else Some ())
333
| None -> add_highlight_menu (Some()))
337
let slicing_highlighter
338
(buffer:GSourceView.source_buffer) localizable ~start ~stop =
339
if Enable.get () then begin
340
(* Definition for highlight 'Slicing' *)
341
let highlight project =
342
let ki = match localizable with
343
| Pretty_source.PStmt (_,stmt) -> Kstmt stmt
344
| Pretty_source.PLval (_,ki,_) | Pretty_source.PTermLval(_,ki,_) -> ki
345
| Pretty_source.PVDecl _ -> Kglobal
347
if Db.Value.is_accessible ki then
348
let unused_code_area =
349
Gtk_helper.make_tag buffer ~name:"slicing_unused" [`STRIKETHROUGH true ] in
350
let spare_code_area =
351
Gtk_helper.make_tag buffer ~name:"slicing_spare" [`UNDERLINE `LOW] in
352
let necessary_code_area =
353
Gtk_helper.make_tag buffer ~name:"slicing_necessary" [`BACKGROUND "green"] in
354
let apply_on_one_project_and_merge_slices kf pb pe mark_of_slice =
355
let apply_mark mark =
356
if Cmdline.Debug.get () > 0 then
357
Format.printf "Got mark: %a@." !Db.Slicing.Mark.pretty mark;
358
if !Db.Slicing.Mark.is_bottom mark then
359
Gtk_helper.apply_tag buffer unused_code_area pb pe;
360
if !Db.Slicing.Mark.is_spare mark then
361
Gtk_helper.apply_tag buffer spare_code_area pb pe;
362
if (!Db.Slicing.Mark.is_ctrl mark
363
|| !Db.Slicing.Mark.is_data mark
364
|| !Db.Slicing.Mark.is_addr mark)
366
Gtk_helper.apply_tag buffer necessary_code_area pb pe
368
let slices = !Db.Slicing.Slice.get_all project kf in
372
(* No slice for this kf *)
373
if !Db.Slicing.Project.is_called project kf
375
if Cmdline.Debug.get () > 0 then
376
Format.printf "Got source code@." ;
377
apply_mark (!Db.Slicing.Mark.get_from_src_func project kf)
380
Gtk_helper.apply_tag buffer unused_code_area pb pe
382
if !Db.Slicing.Project.is_called project kf
384
assert (not (kf == fst (Globals.entry_point ()))) ;
385
if Cmdline.Debug.get () > 0 then
386
Format.printf "Got source code@." ;
387
apply_mark (!Db.Slicing.Mark.get_from_src_func project kf)
389
if Cmdline.Debug.get () > 0 then begin
390
let l = List.length slices in
392
Format.printf "Got %d slices@."
395
let mark_slice slice =
396
let mark = mark_of_slice project slice in
398
in List.iter mark_slice slices
401
let tag_stmt kf stmt pb pe =
402
assert (Db.Value.is_accessible (Kstmt stmt)) ;
403
apply_on_one_project_and_merge_slices
407
(fun _ slice -> !Db.Slicing.Slice.get_mark_from_stmt slice stmt)
409
let tag_vdecl kf vi pb pe =
411
apply_on_one_project_and_merge_slices
415
(fun _ slice -> !Db.Slicing.Slice.get_mark_from_local_var slice vi)
417
match localizable with
418
| Pretty_source.PStmt (kf,stmt) -> tag_stmt kf stmt start stop
419
| Pretty_source.PVDecl (Some kf,vi) -> tag_vdecl kf vi start stop
420
| Pretty_source.PVDecl (None,_)
421
| Pretty_source.PLval _
422
| Pretty_source.PTermLval _ -> ()
424
let slicing_project = !Db.Slicing.Project.get_project () in
425
(* 2. Highlights the 'Slicing' *)
426
Extlib.may highlight slicing_project
429
let none_text = "<i>None</i>"
431
let rebuild_model ((_, (model, _column)) as combo_box_text) =
433
GEdit.text_combo_add combo_box_text none_text;
435
(fun p -> GEdit.text_combo_add combo_box_text (!Db.Slicing.Project.get_name p))
436
(List.rev (!Db.Slicing.Project.get_all()))
438
let refresh_combo_box ((combo_box, (model, _column)) as combo_box_text)
439
slicing_project sensitive =
440
let nb_combo_elts = model#iter_n_children None in
441
let projects = List.rev (!Db.Slicing.Project.get_all()) in
442
if nb_combo_elts<>(1+(List.length projects))
443
then rebuild_model combo_box_text;
444
(* Reset the active project as active in the combo box *)
445
let nth_proj = ref 0 in
447
List.iter (fun proj ->
448
Extlib.may (fun slicing_proj ->
449
if proj == slicing_proj then nth_proj := !i)
453
combo_box#set_active !nth_proj;
454
combo_box#misc#set_sensitive sensitive
457
let gui_set_slicing_debug (main_ui:Design.main_window_extension_points) v =
458
let old = Cmdline.Slicing.Mode.Verbose.get () in
459
if v != old then (* Otherwise set is done at every refreshing *)
460
gui_apply_action main_ui Cmdline.Slicing.Mode.Verbose.set v
461
~info:(fun () -> get_setting_option_text ("-slicing-debug \"-debug " ^ (string_of_int v) ^ "\""))
463
let gui_set_slicing_level (main_ui:Design.main_window_extension_points) v =
464
let old = Cmdline.Slicing.Mode.Calls.get () in
465
if v != old then (* Otherwise set is done at every refreshing *)
466
gui_apply_action main_ui Cmdline.Slicing.Mode.Calls.set v
467
~info:(fun () -> get_setting_option_text ("-slicing-level " ^ (string_of_int v)))
469
let gui_set_slicing_undef_functions (main_ui:Design.main_window_extension_points) v =
470
let old = Cmdline.Slicing.Mode.SliceUndef.get () in
471
if v != old then (* Otherwise set is done at every refreshing *)
472
gui_apply_action main_ui Cmdline.Slicing.Mode.SliceUndef.set v
473
~info:(fun () -> get_setting_option_text (if v then "-slicing-undef-functions" else "-no-slice-undef-functions"))
475
let slicing_panel main_ui =
476
let w = GPack.vbox () in
477
let hbox1 = GPack.hbox
478
~packing:w#pack () in
479
let activate_button = GButton.button ~label:"Activate"
480
~packing:hbox1#pack () in
481
let ((combo_box, (_model, column)) as combo_box_text) =
482
GEdit.combo_box_text ~strings:[ none_text ] ~wrap_width:3 ~use_markup:true
483
~packing:(hbox1#pack ~expand:true ~fill:true) () in
485
let table = GPack.table ~columns:2 ~rows:2 ~homogeneous:true ~packing:w#pack () in
487
let hbox2 = GPack.hbox ~packing:(table#attach ~left:1 ~top:0) () in
489
(* [enabled_button] to give slicing menu available *)
490
let enable_refresh () =
491
gui_compute_values main_ui ;
492
main_ui#rehighlight ()
497
~active:(Enable.get ())
498
~packing:(table#attach ~left:0 ~top:0) () in
500
ignore (enabled_button#connect#toggled
502
Enable.set enabled_button#active;
505
let verbose_refresh = Gtk_helper.on_int ~lower:0 ~upper:3
508
~sensitive:Enable.get
509
Cmdline.Slicing.Mode.Verbose.get
510
(gui_set_slicing_debug main_ui)
513
let hbox3 = GPack.hbox ~packing:(table#attach ~left:1 ~top:1) () in
514
(* [slice_undef_button] related to -slice-undef option *)
515
let slice_undef_button =
518
~active:(Enable.get ())
519
~packing:(table#attach ~left:0 ~top:1) () in
521
let level_refresh = Gtk_helper.on_int ~lower:0 ~upper:3
524
~sensitive:Enable.get
525
Cmdline.Slicing.Mode.Calls.get
526
(gui_set_slicing_level main_ui)
529
combo_box#set_active 0 ;
530
ignore (combo_box#connect#changed
532
match combo_box#active_iter with
535
let slicing_project_name =
536
(* get the text entry related to the current slicing project *)
537
Extlib.may_map !Db.Slicing.Project.get_name ~dft:none_text (!Db.Slicing.Project.get_project ())
538
and selected_name = combo_box#model#get ~row ~column in
539
if (selected_name != slicing_project_name) then
541
try Some (List.find (fun proj -> selected_name = !Db.Slicing.Project.get_name proj) (!Db.Slicing.Project.get_all ()))
542
with Not_found -> None
544
gui_set_project main_ui proj_opt));
545
ignore (activate_button#connect#pressed
546
(fun () -> gui_compute_values main_ui ));
548
ignore (slice_undef_button#connect#toggled
550
gui_set_slicing_undef_functions main_ui slice_undef_button#active));
552
Project.register_after_set_current_hook
554
(fun () -> rebuild_model combo_box_text);
557
let value_is_computed = Db.Value.is_computed () in
558
let slicing_project = !Db.Slicing.Project.get_project () in
559
let enabled = Enable.get () in
560
activate_button#misc#set_sensitive (not value_is_computed) ;
561
enabled_button#misc#set_sensitive value_is_computed ;
562
slice_undef_button#misc#set_sensitive enabled ;
567
if enabled_button#active <> enabled then
569
enabled_button#set_active enabled ;
573
slice_undef_button#set_active (Cmdline.Slicing.Mode.SliceUndef.get());
575
ignore (refresh_combo_box combo_box_text slicing_project (enabled && value_is_computed))
578
"Slicing",w#coerce,Some refresh
580
let file_tree_decorate (file_tree:Filetree.t) =
581
file_tree#append_pixbuf_column
587
(fun glob -> match glob with
588
| GFun ({svar = vi},_ ) ->
591
let kf = Globals.Functions.get vi
592
in (!Db.Slicing.Project.is_called project kf)
593
|| ( [] != (!Db.Slicing.Slice.get_all project kf))
594
with Not_found -> false
598
[`STOCK_ID "gtk-yes"]
602
(!Db.Slicing.Project.get_project ()))
604
let main (main_ui:Design.main_window_extension_points) =
605
main_ui#register_source_selector slicing_selector;
606
main_ui#register_source_highlighter slicing_highlighter;
607
main_ui#register_panel slicing_panel;
608
file_tree_decorate main_ui#file_tree
610
let () = Design.register_extension main
614
compile-command: "LC_ALL=C make -C ../.. -j"
added
removed
src/slicing/register_gui.ml
