From 016f6b1679ee1835f4d809b505465cbe773b33fe Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 16 Nov 2021 11:06:18 +0100
Subject: [PATCH] [Eva] api: Add dependencies calculus
---
src/plugins/value/Eva.mli | 4 ++++
src/plugins/value/register.mli | 8 ++++++--
src/plugins/value/utils/results.ml | 29 ++++++++++++++++++++++++++++-
src/plugins/value/utils/results.mli | 4 ++++
4 files changed, 42 insertions(+), 3 deletions(-)
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 2109d348982..7ee24149cc1 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -68,6 +68,10 @@ module Results: sig
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
+
(* Evaluation *)
val eval_var : Cil_types.varinfo -> request -> value evaluation
val eval_lval : Cil_types.lval -> request -> value evaluation
diff --git a/src/plugins/value/register.mli b/src/plugins/value/register.mli
index c27dd17263f..c0758d9b6fc 100644
--- a/src/plugins/value/register.mli
+++ b/src/plugins/value/register.mli
@@ -20,6 +20,10 @@
(* *)
(**************************************************************************)
-(** Functions of the Value plugin registered in {!Db}.
+(** Functions of the Value plugin registered in {!Db}. Only two functions
+ are exported. *)
- Nothing is 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
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index 9cb35d245f0..cd0ecab0cfd 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -357,7 +357,7 @@ struct
(* Evaluation *)
- let eval_lval lval req=
+ let eval_lval lval req =
let eval state = A.Eval.copy_lvalue state lval in
LValue (Response.map eval (get req))
@@ -486,6 +486,22 @@ struct
match r with
| `Bottom -> true
| `Top | `Value () -> false
+
+ (* Dependencies *)
+
+ let lval_deps lval req =
+ let compute_deps cvalue =
+ Register.eval_deps_lval (cvalue, Locals_scoping.bottom ()) lval
+ in
+ req |> as_cvalue_model |>
+ Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps
+
+ let expr_deps exp req =
+ let compute_deps cvalue =
+ Register.eval_deps (cvalue, Locals_scoping.bottom ()) exp
+ in
+ req |> as_cvalue_model |>
+ Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps
end
@@ -519,6 +535,17 @@ let as_cvalue_model req =
E.as_cvalue_model req
+(* Depedencies *)
+
+let expr_deps exp req =
+ let module E = Make () in
+ E.expr_deps exp req
+
+let lval_deps lval req =
+ let module E = Make () in
+ E.lval_deps lval req
+
+
(* Evaluation *)
module type Lvaluation =
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index 3d13c3c74d0..3720534eb91 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -71,6 +71,10 @@ val fold_callstacks : (callstack -> request -> 'a -> 'a) -> 'a -> request -> 'a
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
+
(* Evaluation *)
val eval_var : Cil_types.varinfo -> request -> value evaluation
val eval_lval : Cil_types.lval -> request -> value evaluation
--
GitLab