From 2ff2492ac382cdbab2e684f073836c2be7a66eb0 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 7 Feb 2022 16:58:31 +0100
Subject: [PATCH] [Slicing] Use the new Eva API
---
src/plugins/slicing/api.ml | 5 ++-
src/plugins/slicing/fct_slice.ml | 19 +++-------
src/plugins/slicing/printSlice.ml | 4 +--
src/plugins/slicing/register.ml | 2 +-
src/plugins/slicing/register_gui.ml | 18 +++++-----
src/plugins/slicing/slicingCmds.ml | 46 ++++++++++++-------------
src/plugins/slicing/slicingMacros.ml | 9 ++---
src/plugins/slicing/slicingProject.ml | 4 +--
src/plugins/slicing/slicingSelect.ml | 4 +--
src/plugins/slicing/slicingState.ml | 2 +-
src/plugins/slicing/slicingTransform.ml | 2 +-
11 files changed, 51 insertions(+), 64 deletions(-)
diff --git a/src/plugins/slicing/api.ml b/src/plugins/slicing/api.ml
index 3ece47ef723..13b39597d7d 100644
--- a/src/plugins/slicing/api.ml
+++ b/src/plugins/slicing/api.ml
@@ -413,10 +413,9 @@ module Slice = struct
let get_called_funcs ff stmt =
match stmt.skind with
- | Instr (Call (_,expr_f,_,_)) ->
+ | Instr (Call _) ->
if snd (Fct_slice.get_called_slice ff stmt) then
- Kernel_function.Hptset.elements
- (snd (!Db.Value.expr_to_kernel_function (Kstmt stmt) ~deps:None expr_f))
+ Eva.Results.callee stmt
else
[]
| Instr (Local_init (_, ConsInit (f, _, _), _)) -> [ Globals.Functions.get f ]
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index 47d922e5bb0..8668de2d327 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -55,8 +55,8 @@ let exists_fun_callers fpred kf =
else begin
table := Kernel_function.Set.add kf !table ;
List.exists
- (fun (kf,_) -> exists_fun_callers kf)
- (!Db.Value.callers kf)
+ (fun kf -> exists_fun_callers kf)
+ (Eva.Results.callers kf)
end
in
exists_fun_callers kf
@@ -146,16 +146,7 @@ end = struct
let indirectly_called_src_functions call_id =
let _, stmt = call_id in
- let funcexp = match stmt.skind with
- | Instr (Call (_,funcexp,_,_)) -> funcexp
- | Instr (Local_init (_, ConsInit (f, _, _), _)) -> Cil.evar f
- | _ -> assert false
- in
- let _, called_functions =
- !Db.Value.expr_to_kernel_function
- (Kstmt stmt) ~deps:(Some Locations.Zone.bottom) funcexp
- in
- Kernel_function.Hptset.elements called_functions
+ Eva.Results.callee stmt
(** [call_id] is a call to [g] in [f].
* we don't want [f] to call [g] anymore, so we have to update [g] [called_by]
@@ -1463,12 +1454,12 @@ let merge_fun_callers get_list get_value merge is_top acc kf =
raise StopMerging (* acceleration when top is reached *)
in
let rec merge_fun_callers kf =
- let merge_fun_caller (kf,_) = merge_fun_callers kf in
+ let merge_fun_caller kf = merge_fun_callers kf in
let vf = Kernel_function.get_vi kf in
if not (Cil_datatype.Varinfo.Set.mem vf !table) then begin
table := Cil_datatype.Varinfo.Set.add vf !table ;
List.iter (fun x -> merge (get_value x)) (get_list kf) ;
- List.iter merge_fun_caller (!Db.Value.callers kf)
+ List.iter merge_fun_caller (Eva.Results.callers kf)
end
(* else no way to add something, the [kf] contribution is already
accumulated. *)
diff --git a/src/plugins/slicing/printSlice.ml b/src/plugins/slicing/printSlice.ml
index 63986e183eb..9c5bd9baed6 100644
--- a/src/plugins/slicing/printSlice.ml
+++ b/src/plugins/slicing/printSlice.ml
@@ -204,10 +204,10 @@ module PrintProject = struct
let iter_edges_src_fun f =
let do_kf_calls kf =
let fi = SlicingMacros.get_kf_fi kf in
- let doit (kf_caller,_) =
+ let doit kf_caller =
let fi_caller = SlicingMacros.get_kf_fi kf_caller in
f ((Src fi_caller, Src fi), None)
- in List.iter doit (!Db.Value.callers kf)
+ in List.iter doit (Eva.Results.callers kf)
in
Globals.Functions.iter do_kf_calls
diff --git a/src/plugins/slicing/register.ml b/src/plugins/slicing/register.ml
index 3f32606a217..4166762d3cc 100644
--- a/src/plugins/slicing/register.ml
+++ b/src/plugins/slicing/register.ml
@@ -27,7 +27,7 @@ let main () =
(* have to do the value analysis before the selections
* because some functions use its results,
* and the value analysis is not launched automatically. *)
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
let project_name = SlicingParameters.ProjectName.get () in
Api.Project.reset_slicing ();
diff --git a/src/plugins/slicing/register_gui.ml b/src/plugins/slicing/register_gui.ml
index 0650a8a5d7d..92251b205bb 100644
--- a/src/plugins/slicing/register_gui.ml
+++ b/src/plugins/slicing/register_gui.ml
@@ -92,7 +92,7 @@ let msg_help_libraries =
undefined functions."
let check_value_computed (main_ui:Design.main_window_extension_points) =
- if Db.Value.is_computed () then true
+ if Eva.Analysis.is_computed () then true
else
let answer = GToolbox.question_box
~title:("Eva Needed")
@@ -102,7 +102,7 @@ let check_value_computed (main_ui:Design.main_window_extension_points) =
^"Do you want to run Eva with its current settings now?")
in
if answer = 1 then
- match main_ui#full_protect ~cancelable:true !Db.Value.compute with
+ match main_ui#full_protect ~cancelable:true Eva.Analysis.compute with
| Some _ ->
main_ui#redisplay (); (* New alarms *)
true
@@ -116,7 +116,7 @@ let gui_apply_action (main_ui:Design.main_window_extension_points) f x ~info =
let slicing_selector (popup_factory:GMenu.menu GMenu.factory)
(main_ui:Design.main_window_extension_points) ~button localizable =
- if (not (Db.Value.is_computed ()))
+ if (not (Eva.Analysis.is_computed ()))
then
ignore
(popup_factory#add_item "Enable _slicing"
@@ -126,7 +126,7 @@ let slicing_selector (popup_factory:GMenu.menu GMenu.factory)
Enabled.set true;
!update_column `Visibility
in
- if (not (Db.Value.is_computed ())) then begin
+ if (not (Eva.Analysis.is_computed ())) then begin
if check_value_computed main_ui then enable ()
end
else enable ()
@@ -344,7 +344,7 @@ let slicing_selector (popup_factory:GMenu.menu GMenu.factory)
in
let some_kf_from_vi vi =
try let kf = Globals.Functions.get vi in
- if !Db.Value.is_called kf then Some kf else None
+ if Eva.Results.is_called kf then Some kf else None
with Not_found -> None in
let some_kf_from_lv lv =
match lv with
@@ -352,7 +352,7 @@ let slicing_selector (popup_factory:GMenu.menu GMenu.factory)
| _ -> None
in
let some_kf_ki_lv kf stmt lvopt =
- if !Db.Value.is_called kf && Db.Value.is_reachable_stmt stmt
+ if Eva.Results.is_called kf && Eva.Results.is_reachable stmt
then Some (kf, stmt, lvopt) else None
in
begin (* add menu for slicing and scope plug-in *)
@@ -386,7 +386,7 @@ let slicing_highlighter(buffer:Design.reactive_buffer) localizable ~start ~stop=
let highlight () =
let buffer = buffer#buffer in
let ki = Pretty_source.ki_of_localizable localizable in
- if Db.Value.is_accessible ki then
+ if Eva.Results.is_reachable_kinstr ki then
let unused_code_area =
Gtk_helper.make_tag buffer
~name:"slicing_unused" [`STRIKETHROUGH true ]
@@ -443,7 +443,7 @@ let slicing_highlighter(buffer:Design.reactive_buffer) localizable ~start ~stop=
end
in
let tag_stmt kf stmt pb pe =
- assert (Db.Value.is_reachable_stmt stmt) ;
+ assert (Eva.Results.is_reachable stmt) ;
apply_on_one_project_and_merge_slices
kf
pb
@@ -554,7 +554,7 @@ let slicing_panel (main_ui:Design.main_window_extension_points) =
(gui_set_slicing_level main_ui)
in
let refresh () =
- let value_is_computed = Db.Value.is_computed () in
+ let value_is_computed = Eva.Analysis.is_computed () in
let enabled = Enabled.get () in
enabled_button#misc#set_sensitive value_is_computed ;
slice_undef_button#misc#set_sensitive enabled ;
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index 79b59cc0fd5..dfd6377fa2e 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -71,17 +71,18 @@ struct
* i.e. directly means when [ki] is a call,
it doesn't don't look at the assigns clause of the called function. *)
let get_rw_zone stmt = (* returns [Zone.t read],[Zone.t written] *)
- assert (Db.Value.is_computed ());
+ assert (Eva.Analysis.is_computed ());
let lval_process read_zone stmt lv =
(* returns [read_zone] joined to [Zone.t read] by [lv], [Zone.t written] by [lv] *)
(* The modified locations are [looking_for], those address are
function of [deps]. *)
- let state = Db.Value.get_stmt_state stmt in
- let deps, zloc, _exact =
- !Db.Value.lval_to_zone_with_deps_state
- state ~deps:(Some read_zone) ~for_writing:true lv
+ let zloc, deps =
+ Eva.Results.(
+ before stmt |> eval_address lv |> as_zone ~access:Locations.Write |>
+ default Locations.Zone.bottom,
+ before stmt |> address_deps lv)
in
- deps, zloc
+ Locations.Zone.join read_zone deps, zloc
in
let call_process lv f args _loc =
(* returns [Zone.t read] by [lv, f, args], [Zone.t written] by [lv] *)
@@ -184,8 +185,8 @@ let select_entry_point_and_some_inputs_outputs set ~mark kf ~return ~outputs ~in
add_to_selection set selection
in if ((Locations.Zone.equal Locations.Zone.bottom outputs) && not return) ||
(try
- let ki = Kernel_function.find_return kf
- in if Db.Value.is_reachable_stmt ki then
+ let stmt = Kernel_function.find_return kf
+ in if Eva.Results.is_reachable stmt then
false
else
begin
@@ -210,8 +211,8 @@ let select_entry_point_and_some_inputs_outputs set ~mark kf ~return ~outputs ~in
(* apply [select ~spare] on each callsite of [kf] and add the returned selection
to [set]. *)
let generic_select_func_calls select_stmt set ~spare kf =
- assert (Db.Value.is_computed ());
- let callers = !Db.Value.callers kf in
+ assert (Eva.Analysis.is_computed ());
+ let callers = Eva.Results.callsites kf in
let select_calls acc (caller, stmts) =
List.fold_left (fun acc s -> select_stmt acc ~spare s caller) acc stmts
in
@@ -245,7 +246,7 @@ let select_func_calls_to set ~spare kf =
let nspare = not spare in
SlicingMarks.mk_user_mark ~data:nspare ~addr:nspare ~ctrl:nspare
in
- assert (Db.Value.is_computed ());
+ assert (Eva.Analysis.is_computed ());
let outputs = !Db.Outputs.get_external kf in
select_entry_point_and_some_inputs_outputs set ~mark kf
~return:true
@@ -308,7 +309,7 @@ let select_stmt_zone set mark zone ~before ki kf =
or after (c.f. boolean [~before]) the statement [ki].
Note: add also a transparent selection on the whole statement. *)
let select_stmt_lval set mark lval_str ~before ki ~eval kf =
- assert (Db.Value.is_computed ());
+ assert (Eva.Analysis.is_computed ());
if Datatype.String.Set.is_empty lval_str
then set
else
@@ -319,10 +320,9 @@ let select_stmt_lval set mark lval_str ~before ki ~eval kf =
let lval =
!Db.Properties.Interp.term_lval_to_lval ~result:None lval_term
in
- let state = Db.Value.get_stmt_state eval in
- let _deps, zone, _exact =
- !Db.Value.lval_to_zone_with_deps_state
- ~deps:None ~for_writing:false state lval
+ let zone =
+ Eva.Results.(before eval |> eval_address lval |> as_zone) |>
+ Result.value ~default:Locations.Zone.bottom
in
Locations.Zone.join zone acc)
lval_str
@@ -342,7 +342,7 @@ let select_stmt_lval set mark lval_str ~before ki ~eval kf =
i.e. when [ki_opt] is a call, the selection doesn't look at the assigns clause
of a call. *)
let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
- assert (Db.Value.is_computed ());
+ assert (Eva.Analysis.is_computed ());
let zone_option ~for_writing lval_str =
if Datatype.String.Set.is_empty lval_str
then None
@@ -352,10 +352,10 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
(fun lval_str acc ->
let lval_term = !Db.Properties.Interp.term_lval kf lval_str in
let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
- let state = Db.Value.get_stmt_state eval in
- let _deps, zone, _exact =
- !Db.Value.lval_to_zone_with_deps_state
- state ~for_writing ~deps:None lval
+ let access = if for_writing then Locations.Write else Locations.Read in
+ let zone =
+ Eva.Results.(before eval |> eval_address lval |> as_zone ~access) |>
+ Result.value ~default:Locations.Zone.bottom
in
Locations.Zone.join zone acc)
lval_str Locations.Zone.bottom
@@ -389,7 +389,7 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
| None ->
Globals.Functions.iter
(fun kf ->
- if !Db.Value.is_called kf then
+ if Eva.Results.is_called kf then
if not (!Db.Value.use_spec_instead_of_definition kf)
then (* Called function with source code: just looks at its stmt *)
Kinstr.iter_from_func (select_rw_from_stmt kf) kf
@@ -413,7 +413,7 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
~return:false ~inputs ~outputs:Locations.Zone.bottom
in
- assert (!Db.Value.is_called kf) ; (* otherwise [!Db.Outputs.get_external kf] gives weird results *)
+ assert (Eva.Results.is_called kf) ; (* otherwise [!Db.Outputs.get_external kf] gives weird results *)
select_inter_zone select_wr zone_wr_opt (!Db.Outputs.get_external kf) ;
select_inter_zone select_rd zone_rd_opt (!Db.Inputs.get_external kf)
end
diff --git a/src/plugins/slicing/slicingMacros.ml b/src/plugins/slicing/slicingMacros.ml
index d49a3f596c1..ebb985bc198 100644
--- a/src/plugins/slicing/slicingMacros.ml
+++ b/src/plugins/slicing/slicingMacros.ml
@@ -173,12 +173,9 @@ let is_call_stmt stmt =
| Instr (Call _ | Local_init(_, ConsInit _,_)) -> true | _ -> false
let get_called_kf call_stmt = match call_stmt.skind with
- | Instr (Call (_, funcexp,_,_)) ->
- let _funcexp_dpds, called_functions =
- !Db.Value.expr_to_kernel_function ~deps:None (Kstmt call_stmt) funcexp
- in
- (match Kernel_function.Hptset.contains_single_elt called_functions with
- | Some kf -> kf
+ | Instr (Call _) ->
+ (match Eva.Results.callee call_stmt with
+ | [kf] -> kf
| _ -> raise SlicingTypes.PtrCallExpr)
| Instr (Local_init(_, ConsInit (f, _, _), _)) -> Globals.Functions.get f
| _ -> invalid_arg "Not a call statement !"
diff --git a/src/plugins/slicing/slicingProject.ml b/src/plugins/slicing/slicingProject.ml
index 73532548cc6..010cbdd86d4 100644
--- a/src/plugins/slicing/slicingProject.ml
+++ b/src/plugins/slicing/slicingProject.ml
@@ -222,13 +222,13 @@ let apply_appli_crit appli_crit =
match appli_crit with
| T.CaCall fi_to_call ->
let kf_to_call = M.get_fi_kf fi_to_call in
- let add_actions actions (kf_caller,_) =
+ let add_actions actions kf_caller =
let fi_caller = M.get_kf_fi kf_caller in
let mark = SlicingMarks.mk_user_spare in
let action =
SlicingActions.mk_crit_mark_calls fi_caller kf_to_call mark in
action :: actions
- in List.fold_left add_actions [] (!Db.Value.callers kf_to_call)
+ in List.fold_left add_actions [] (Eva.Results.callers kf_to_call)
| _ ->
SlicingParameters.not_yet_implemented
"This slicing criterion on application"
diff --git a/src/plugins/slicing/slicingSelect.ml b/src/plugins/slicing/slicingSelect.ml
index 5775c6ecbe4..b4b331aabe2 100644
--- a/src/plugins/slicing/slicingSelect.ml
+++ b/src/plugins/slicing/slicingSelect.ml
@@ -105,7 +105,7 @@ let select_stmt_zone kf ?(select=empty_db_select kf) stmt ~before loc mark =
Locations.Zone.pretty loc
(if before then "before" else "after") stmt.sid
SlicingMarks.pretty_mark mark;
- if not (Db.Value.is_reachable_stmt stmt) then
+ if not (Eva.Results.is_reachable stmt) then
begin
SlicingParameters.feedback
"@[Nothing to select for @[%a@]@ %s unreachable stmt of %a@]"
@@ -194,7 +194,7 @@ let stmt_nodes_to_select pdg stmt =
let select_stmt_computation kf ?(select=empty_db_select kf) stmt mark =
SlicingParameters.debug ~level:1 "[Register.select_stmt_computation] on stmt %d" stmt.sid;
- if not (Db.Value.is_reachable_stmt stmt) then
+ if not (Eva.Results.is_reachable stmt) then
begin
SlicingParameters.feedback
"@[Nothing to select for an unreachable stmt of %a@]"
diff --git a/src/plugins/slicing/slicingState.ml b/src/plugins/slicing/slicingState.ml
index 93a4ad676a1..4b9a224a475 100644
--- a/src/plugins/slicing/slicingState.ml
+++ b/src/plugins/slicing/slicingState.ml
@@ -49,7 +49,7 @@ let may_map ~none f = match P.get_option () with
| Some _ -> f ()
let reset_slicing () =
- !Db.Value.compute () ;
+ Eva.Analysis.compute () ;
let initialized = match P.get_option () with | None -> false | Some _ -> true in
if not initialized then
SlicingParameters.feedback ~level:1 "initializing slicing ..."
diff --git a/src/plugins/slicing/slicingTransform.ml b/src/plugins/slicing/slicingTransform.ml
index c27b8a15e3b..9a4723f9723 100644
--- a/src/plugins/slicing/slicingTransform.ml
+++ b/src/plugins/slicing/slicingTransform.ml
@@ -234,7 +234,7 @@ module Visibility (SliceName : sig
let annotation_visible ff_opt stmt annot =
SlicingParameters.debug ~current:true ~level:2
"[SlicingTransform.Visibility.annotation_visible] ?";
- Db.Value.is_reachable_stmt stmt &&
+ Eva.Results.is_reachable stmt &&
Alarms.find annot = None && (* Always drop alarms: the alarms table
in the new project is not synchronized *)
match ff_opt with
--
GitLab