From aff1407cc01158cb648bc0361cd3252a5ac7a32c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 10 Oct 2022 16:50:09 +0200
Subject: [PATCH] [from] Do not export [find_deps_no_transitivity].
In plugins pdg, scope and slicing, directly uses the Eva API instead of this
function.
---
src/plugins/from/from.ml | 3 ---
src/plugins/from/from.mli | 2 --
src/plugins/from/functionwise.ml | 6 ------
src/plugins/from/functionwise.mli | 2 --
src/plugins/pdg/build.ml | 8 ++++----
src/plugins/scope/zones.ml | 2 +-
src/plugins/slicing/slicingCmds.ml | 12 ++++++------
tests/pdg/dyn_dpds.ml | 8 ++------
8 files changed, 13 insertions(+), 30 deletions(-)
diff --git a/src/plugins/from/from.ml b/src/plugins/from/from.ml
index 9be4cb70c18..f1faee921ea 100644
--- a/src/plugins/from/from.ml
+++ b/src/plugins/from/from.ml
@@ -26,9 +26,6 @@ let compute_all = Functionwise.compute_all
let is_computed = Functionwise.is_computed
let get = Functionwise.get
let pretty = Functionwise.pretty
-let find_deps_no_transitivity = Functionwise.find_deps_no_transitivity
-let find_deps_no_transitivity_state =
- Functionwise.find_deps_no_transitivity_state
let access zone mem = Function_Froms.Memory.find mem zone
diff --git a/src/plugins/from/from.mli b/src/plugins/from/from.mli
index 71bee4f32e4..f71b8ed9ebe 100644
--- a/src/plugins/from/from.mli
+++ b/src/plugins/from/from.mli
@@ -31,8 +31,6 @@ val get : Cil_types.kernel_function -> Function_Froms.froms
val access : Locations.Zone.t -> Function_Froms.Memory.t -> Locations.Zone.t
val pretty : Format.formatter -> kernel_function -> unit
val display : Format.formatter -> unit
-val find_deps_no_transitivity : stmt -> exp -> Locations.Zone.t
-val find_deps_no_transitivity_state : Cvalue.Model.t -> exp -> Locations.Zone.t
module Callwise : sig
val iter : (Cil_types.kinstr -> Function_Froms.froms -> unit) -> unit
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index 13413a811f2..ee80d0cc402 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -110,12 +110,6 @@ let get = To_Use.memo
let pretty fmt v =
Function_Froms.pretty_with_type (Kernel_function.get_type v) fmt (get v)
-let find_deps_no_transitivity stmt expr =
- Eva.Results.(before stmt |> expr_deps expr)
-
-let find_deps_no_transitivity_state state expr =
- Eva.Results.(in_cvalue_state state |> expr_deps expr)
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/from/functionwise.mli b/src/plugins/from/functionwise.mli
index ec01c2be2cf..1e6e14f2d3c 100644
--- a/src/plugins/from/functionwise.mli
+++ b/src/plugins/from/functionwise.mli
@@ -31,5 +31,3 @@ val compute_all : unit -> unit
val is_computed : kernel_function -> bool
val get : Cil_types.kernel_function -> Function_Froms.froms
val pretty : Format.formatter -> kernel_function -> unit
-val find_deps_no_transitivity : stmt -> exp -> Locations.Zone.t
-val find_deps_no_transitivity_state : Cvalue.Model.t -> exp -> Locations.Zone.t
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index ca20eff30ec..2a6758a85fd 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -621,7 +621,7 @@ let get_lval_infos lval stmt =
Use the state at ki (before assign)
and returns the new state (after assign). *)
let process_asgn pdg state stmt lval exp =
- let r_dpds = From.find_deps_no_transitivity stmt exp in
+ let r_dpds = Eva.Results.(before stmt |> expr_deps exp) in
let r_decl = Cil.extract_varinfos_from_exp exp in
let (l_loc, exact, l_dpds, l_decl) = get_lval_infos lval stmt in
let key = Key.stmt_key stmt in
@@ -636,7 +636,7 @@ let process_asgn pdg state stmt lval exp =
(** Add a PDG node and its dependencies for each explicit call argument. *)
let process_args pdg st stmt argl =
let process_one_arg arg =
- let dpds = From.find_deps_no_transitivity stmt arg in
+ let dpds = Eva.Results.(before stmt |> expr_deps arg) in
let decl_dpds = Cil.extract_varinfos_from_exp arg in
(dpds, decl_dpds)
in let arg_dpds = List.map process_one_arg argl in
@@ -763,7 +763,7 @@ let process_call pdg state stmt lvaloption funcexp argl _loc =
* and register the statements that are control-dependent on it.
*)
let process_condition ctrl_dpds_infos pdg state stmt condition =
- let loc_cond = From.find_deps_no_transitivity stmt condition in
+ let loc_cond = Eva.Results.(before stmt |> expr_deps condition) in
let decls_cond = Cil.extract_varinfos_from_exp condition in
let controlled_stmts = CtrlDpds.get_if_controlled_stmts ctrl_dpds_infos stmt in
@@ -819,7 +819,7 @@ let process_return _current_function pdg state stmt ret_exp =
let last_state =
match ret_exp with
| Some exp ->
- let loc_exp = From.find_deps_no_transitivity stmt exp in
+ let loc_exp = Eva.Results.(before stmt |> expr_deps exp) in
let decls_exp = Cil.extract_varinfos_from_exp exp in
add_retres pdg state stmt loc_exp decls_exp
| None ->
diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml
index b28bf52e8ec..78134d802f2 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -40,7 +40,7 @@ module Data = struct
let diff = Locations.Zone.diff (* over-approx *)
let pretty fmt z = Format.fprintf fmt "@[<h 1>%a@]" Locations.Zone.pretty z
- let exp_zone stmt exp = From.find_deps_no_transitivity stmt exp
+ let exp_zone stmt exp = Eva.Results.(before stmt |> expr_deps exp)
end
module Ctx = struct
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index 61fb2ef8ebf..7bdf6c01161 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -86,10 +86,10 @@ struct
in
let call_process lv f args _loc =
(* returns [Zone.t read] by [lv, f, args], [Zone.t written] by [lv] *)
- let read_zone = From.find_deps_no_transitivity stmt f in
+ let read_zone = Eva.Results.(before stmt |> expr_deps f) in
let add_args arg inputs =
- Locations.Zone.join inputs
- (From.find_deps_no_transitivity stmt arg) in
+ Locations.Zone.join inputs Eva.Results.(before stmt |> expr_deps arg)
+ in
let read_zone = List.fold_right add_args args read_zone in
let read_zone,write_zone =
match lv with
@@ -101,16 +101,16 @@ struct
| Switch (exp,_,_,_)
| If (exp,_,_,_) ->
(* returns [Zone.t read] by condition [exp], [Zone.bottom] *)
- From.find_deps_no_transitivity stmt exp, Locations.Zone.bottom
+ Eva.Results.(before stmt |> expr_deps exp), Locations.Zone.bottom
| Instr (Set (lv,exp,_)) ->
(* returns [Zone.t read] by [exp, lv], [Zone.t written] by [lv] *)
- let read_zone = From.find_deps_no_transitivity stmt exp in
+ let read_zone = Eva.Results.(before stmt |> expr_deps exp) in
lval_process read_zone stmt lv
| Instr (Local_init (v, AssignInit i, _)) ->
let rec collect zone i =
match i with
| SingleInit e ->
- Locations.Zone.join zone (From.find_deps_no_transitivity stmt e)
+ Locations.Zone.join zone Eva.Results.(before stmt |> expr_deps e)
| CompoundInit (_,l) ->
List.fold_left
(fun acc (_,i) -> collect acc i) zone l
diff --git a/tests/pdg/dyn_dpds.ml b/tests/pdg/dyn_dpds.ml
index 3a99ce4a5fc..402616dac4b 100644
--- a/tests/pdg/dyn_dpds.ml
+++ b/tests/pdg/dyn_dpds.ml
@@ -8,12 +8,8 @@ zgrviewer tests/pdg/dyn_dpds_2.dot ;
let get_zones str_data (stmt, kf) =
let lval_term = !Db.Properties.Interp.term_lval kf str_data in
let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
- let loc =
- From.find_deps_no_transitivity
- stmt
- (Cil.new_exp ~loc:Cil_datatype.Location.unknown (Cil_types.Lval lval))
- in
- loc
+ let exp = Cil.new_exp ~loc:Cil_datatype.Location.unknown (Cil_types.Lval lval) in
+ Eva.Results.(before stmt |> expr_deps exp)
let main _ =
let memo_debug = Kernel.Debug.get () in
--
GitLab