From 8c44e2163970acb46d95ac51e8c43974f3036954 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 10 Feb 2022 14:41:13 +0100
Subject: [PATCH] [Slicing] Minor simplifications in the use of Eva results.
---
src/plugins/slicing/fct_slice.ml | 7 ++-----
src/plugins/slicing/slicingCmds.ml | 23 +++++++++--------------
2 files changed, 11 insertions(+), 19 deletions(-)
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index 8668de2d327..22285f900b9 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -54,9 +54,7 @@ let exists_fun_callers fpred kf =
then false (* no way to call the initial [kf]. *)
else begin
table := Kernel_function.Set.add kf !table ;
- List.exists
- (fun kf -> exists_fun_callers kf)
- (Eva.Results.callers kf)
+ List.exists exists_fun_callers (Eva.Results.callers kf)
end
in
exists_fun_callers kf
@@ -1454,12 +1452,11 @@ 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 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 (Eva.Results.callers kf)
+ List.iter merge_fun_callers (Eva.Results.callers kf)
end
(* else no way to add something, the [kf] contribution is already
accumulated. *)
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index dfd6377fa2e..cdfb8be1be9 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -55,6 +55,11 @@ let apply_all ~propagate_to_callers =
let get_select_kf (fvar, _select) = Globals.Functions.get fvar
+let get_lval_zone ?(access=Locations.Read) stmt lval =
+ let open Eva.Results in
+ before stmt |> eval_address lval |> as_zone ~access
+ |> default Locations.Zone.bottom
+
(** Utilities for [kinstr]. *)
module Kinstr: sig
val iter_from_func : (stmt -> unit) -> kernel_function -> unit
@@ -76,12 +81,8 @@ struct
(* 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 zloc, deps =
- Eva.Results.(
- before stmt |> eval_address lv |> as_zone ~access:Locations.Write |>
- default Locations.Zone.bottom,
- before stmt |> address_deps lv)
- in
+ let zloc = get_lval_zone ~access:Locations.Write stmt lv in
+ let deps = Eva.Results.(before stmt |> address_deps lv) in
Locations.Zone.join read_zone deps, zloc
in
let call_process lv f args _loc =
@@ -320,10 +321,7 @@ 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 zone =
- Eva.Results.(before eval |> eval_address lval |> as_zone) |>
- Result.value ~default:Locations.Zone.bottom
- in
+ let zone = get_lval_zone eval lval in
Locations.Zone.join zone acc)
lval_str
Locations.Zone.bottom
@@ -353,10 +351,7 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
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 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
+ let zone = get_lval_zone ~access eval lval in
Locations.Zone.join zone acc)
lval_str Locations.Zone.bottom
in SlicingParameters.debug ~level:3
--
GitLab