diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 98c8fc246b5b29c385962602ccb0d469896b2020..998cd2b8400d307c3ed4eb496ac48226c1670a08 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -276,6 +276,17 @@ module Results: sig
evaluate the given lvalue, excluding the lvalue zone itself. *)
val address_deps : Cil_types.lval -> request -> Locations.Zone.t
+ (** Memory dependencies of an expression. *)
+ type deps = Function_Froms.Deps.deps = {
+ data: Locations.Zone.t;
+ (** Memory zone directly required to evaluate the given expression. *)
+ indirect: Locations.Zone.t;
+ (** Memory zone read to compute data addresses. *)
+ }
+
+ (** Computes (an overapproximation of) the memory dependencies of an
+ expression. *)
+ val expr_dependencies : Cil_types.exp -> request -> deps
(** Evaluation *)
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index a1ea4f6e298a456a13947760ae0e3c3d7c15f6f8..7717dfaf3dbd739795331c642429f2ac563bf357 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -274,41 +274,58 @@ let dump_garbled_mix () =
(Pretty_utils.pp_list ~pre:"" ~suf:"" ~sep:"@ " pp_one) l
+type deps = Function_Froms.Deps.deps = {
+ data: Locations.Zone.t;
+ indirect: Locations.Zone.t;
+}
+
+let bottom_deps =
+ { data = Locations.Zone.bottom; indirect = Locations.Zone.bottom }
+
+let join_deps a b =
+ { data = Locations.Zone.join a.data b.data;
+ indirect = Locations.Zone.join a.indirect b.indirect; }
+
+let deps_to_zone deps = Locations.Zone.join deps.data deps.indirect
+
(* Computation of the inputs of an expression. *)
-let rec zone_of_expr find_loc expr =
+let rec deps_of_expr find_loc expr =
let rec process expr = match expr.enode with
| Lval lval ->
(* Dereference of an lvalue. *)
- zone_of_lval find_loc lval
+ deps_of_lval find_loc lval
| UnOp (_, e, _) | CastE (_, e) ->
(* Unary operators. *)
process e
| BinOp (_, e1, e2, _) ->
(* Binary operators. *)
- Locations.Zone.join (process e1) (process e2)
+ join_deps (process e1) (process e2)
| StartOf lv | AddrOf lv ->
(* computation of an address: the inputs of the lvalue whose address
is computed are read to compute said address. *)
- indirect_zone_of_lval find_loc lv
+ { data = indirect_zone_of_lval find_loc lv;
+ indirect = Locations.Zone.bottom; }
| Const _ | SizeOf _ | AlignOf _ | SizeOfStr _ | SizeOfE _ | AlignOfE _ ->
(* static constructs, nothing is read to evaluate them. *)
- Locations.Zone.bottom
+ bottom_deps
in
process expr
+and zone_of_expr find_loc expr = deps_to_zone (deps_of_expr find_loc expr)
+
(* dereference of an lvalue: first, its address must be computed,
then its contents themselves are read *)
-and zone_of_lval find_loc lval =
+and deps_of_lval find_loc lval =
let ploc = find_loc lval in
let zone = Precise_locs.enumerate_valid_bits Read ploc in
- Locations.Zone.join zone
- (indirect_zone_of_lval find_loc lval)
+ { data = zone;
+ indirect = indirect_zone_of_lval find_loc lval; }
(* Computations of the inputs of a lvalue : union of the "host" part and
the offset. *)
and indirect_zone_of_lval find_loc (lhost, offset) =
- (Locations.Zone.join
- (zone_of_lhost find_loc lhost) (zone_of_offset find_loc offset))
+ Locations.Zone.join
+ (zone_of_lhost find_loc lhost) (zone_of_offset find_loc offset)
(* Computation of the inputs of a host. Nothing for a variable, and the
inputs of [e] for a dereference [*e]. *)
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index be3385152b007307f1adab510474ed57dcc21d19..7f665f05f267b3873a053b923f5917eb5ee1526f 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/src/plugins/eva/utils/eva_utils.mli
@@ -107,6 +107,17 @@ val indirect_zone_of_lval:
on which the offset and the pointer expression (if any) of an lvalue depend.
*)
+
+type deps = Function_Froms.Deps.deps = {
+ data: Locations.Zone.t;
+ indirect: Locations.Zone.t;
+}
+
+val deps_of_expr:
+ (lval -> Precise_locs.precise_location) -> exp -> deps
+(** Given a function computing the location of lvalues, computes the memory
+ dependencies of an expression. *)
+
(** Computes the height of an expression, that is the maximum number of nested
operations in this expression. *)
val height_expr: exp -> int
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index db4af18ba2c8eb2abd23d5a27d82d390074c524e..40a6ce93b0622096089d9d4d74de7c0815087d45 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -699,6 +699,15 @@ let address_deps lval request =
let lval_to_loc lv = eval_address lv request |> as_precise_loc in
Eva_utils.indirect_zone_of_lval lval_to_loc lval
+type deps = Function_Froms.Deps.deps = {
+ data: Locations.Zone.t;
+ indirect: Locations.Zone.t;
+}
+
+let expr_dependencies expr request =
+ let lval_to_loc lv = eval_address lv request |> as_precise_loc in
+ Eva_utils.deps_of_expr lval_to_loc expr
+
(* Reachability *)
let is_empty rq =
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index e18f41a032527bbde86a2c4b4122423e202afb9d..007a99c63191bd50a8e5208278ec353dcee8df32 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -181,6 +181,17 @@ val lval_deps : Cil_types.lval -> request -> Locations.Zone.t
evaluate the given lvalue, excluding the lvalue zone itself. *)
val address_deps : Cil_types.lval -> request -> Locations.Zone.t
+(** Memory dependencies of an expression. *)
+type deps = Function_Froms.Deps.deps = {
+ data: Locations.Zone.t;
+ (** Memory zone directly required to evaluate the given expression. *)
+ indirect: Locations.Zone.t;
+ (** Memory zone read to compute data addresses. *)
+}
+
+(** Computes (an overapproximation of) the memory dependencies of an
+ expression. *)
+val expr_dependencies : Cil_types.exp -> request -> deps
(** Evaluation *)