From f9a139c84b6dfccb73a642d05d43ad61c81e4c8d Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 8 Feb 2022 21:04:57 +0100
Subject: [PATCH] [Eva] api: separate lval_deps and address_deps
---
src/plugins/value/Eva.mli | 5 +++--
src/plugins/value/register.mli | 7 +++----
src/plugins/value/utils/results.ml | 12 ++++++++++++
src/plugins/value/utils/results.mli | 5 +++--
4 files changed, 21 insertions(+), 8 deletions(-)
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index dd7a35736d2..7872eb90937 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -70,8 +70,9 @@ module Results: sig
val as_cvalue_model : request -> Cvalue.Model.t result
(* Dependencies *)
- val expr_deps : Cil_types.exp -> request -> Locations.Zone.t
- val lval_deps : Cil_types.lval -> request -> Locations.Zone.t
+ val expr_deps : Cil_types.exp -> request -> Locations.Zone.t (* The zone of bits read to evaluate the expression, including adresses computation *)
+ val lval_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, including lvalue zone itself *)
+ val address_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, excluding the lvalue zone itself *)
(* Evaluation *)
val eval_var : Cil_types.varinfo -> request -> value evaluation
diff --git a/src/plugins/value/register.mli b/src/plugins/value/register.mli
index c0758d9b6fc..8dd1c29c58b 100644
--- a/src/plugins/value/register.mli
+++ b/src/plugins/value/register.mli
@@ -23,7 +23,6 @@
(** Functions of the Value plugin registered in {!Db}. Only two functions
are exported. *)
-val eval_deps : Cvalue.Model.t * Locals_scoping.clobbered_set ->
- Cil_types.exp -> Locations.Zone.t
-val eval_deps_lval : Cvalue.Model.t * Locals_scoping.clobbered_set ->
- Cil_types.lval -> Locations.Zone.t
+val eval_deps : Cvalue_domain.State.t -> Cil_types.exp -> Locations.Zone.t
+val eval_deps_lval : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t
+val eval_deps_addr : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index 0e045ae21ec..00bdb7712ad 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -511,6 +511,14 @@ struct
in
req |> as_cvalue_model |>
Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps
+
+ let address_deps lval req =
+ let compute_deps cvalue =
+ Register.eval_deps_addr (cvalue, Locals_scoping.bottom ()) lval
+ in
+ req |> as_cvalue_model |>
+ Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps
+
end
@@ -554,6 +562,10 @@ let lval_deps lval req =
let module E = Make () in
E.lval_deps lval req
+let address_deps lval req =
+ let module E = Make () in
+ E.address_deps lval req
+
(* Evaluation *)
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index 6db2025dfb7..d4030ff471d 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -72,8 +72,9 @@ val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
val as_cvalue_model : request -> Cvalue.Model.t result
(* Dependencies *)
-val expr_deps : Cil_types.exp -> request -> Locations.Zone.t
-val lval_deps : Cil_types.lval -> request -> Locations.Zone.t
+val expr_deps : Cil_types.exp -> request -> Locations.Zone.t (* The zone of bits read to evaluate the expression, including adresses computation *)
+val lval_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, including lvalue zone itself *)
+val address_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, excluding the lvalue zone itself *)
(* Evaluation *)
val eval_var : Cil_types.varinfo -> request -> value evaluation
--
GitLab