From 4e05326e197b691aed06b8163692c8c8260d7bcb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 3 Oct 2022 13:35:44 +0200
Subject: [PATCH] [Eva] Exports new function [assigns_tlval_to_zones] in
Eva.Logic_inout.
Intented to replace calls to Db.Properties.Interp.loc_to_loc*, used by
the inout and from plugins.
---
src/plugins/eva/Eva.mli | 12 ++++++++++++
src/plugins/eva/legacy/eval_terms.ml | 3 +++
src/plugins/eva/legacy/eval_terms.mli | 6 ++++++
src/plugins/eva/legacy/logic_inout.ml | 18 ++++++++++++++++++
src/plugins/eva/legacy/logic_inout.mli | 12 ++++++++++++
5 files changed, 51 insertions(+)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 9a535134ce6..0adbbd5ebd2 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -685,6 +685,18 @@ module Logic_inout: sig
result: Cil_types.varinfo option ->
Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+ (** Zones of an lvalue term of an assigns clause. *)
+ type tlval_zones = {
+ under: Locations.Zone.t; (** Under-approximation of the memory zone. *)
+ over: Locations.Zone.t; (** Over-approximation of the memory zone. *)
+ deps: Locations.Zone.t; (** Dependencies needed to evaluate the address. *)
+ }
+
+ (** Evaluation of the memory zones and dependencies of an lvalue term from an
+ assigns clause, in the given cvalue state for a read or write access. *)
+ val assigns_tlval_to_zones:
+ Cvalue.Model.t -> Locations.access -> Cil_types.term -> tlval_zones option
+
(** Evaluate the assigns clauses of the given function in its given pre-state,
and compare them with the given froms (computed by the from plugin).
Emits warnings if needed, and sets statuses to the assigns clauses. *)
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 344e7cd9f1a..ce12bb0f254 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -2773,6 +2773,9 @@ let eval_tlval_as_zone ~alarm_mode access env t =
in
over
+let tlval_deps env t = (eval_term_as_lval ~alarm_mode:Ignore env t).ldeps
+
+
let () =
(* TODO: deprecate loc_to_loc, move loc_to_locs into Value *)
Db.Properties.Interp.loc_to_loc :=
diff --git a/src/plugins/eva/legacy/eval_terms.mli b/src/plugins/eva/legacy/eval_terms.mli
index a8b326ffc3d..ff51402c498 100644
--- a/src/plugins/eva/legacy/eval_terms.mli
+++ b/src/plugins/eva/legacy/eval_terms.mli
@@ -116,5 +116,11 @@ val eval_predicate :
Returns None on either an evaluation error or on unsupported construct. *)
val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
+(** [tlval_deps env t] computes the logic dependencies needed to evaluate the
+ address of lvalue term [t] in the given evaluation environment [env].
+ @raises LogicEvalError on evaluation errors, unsupported constructs, or
+ if [t] is not an lvalue term. *)
+val tlval_deps: eval_env -> Cil_types.term -> logic_deps
+
val reduce_by_predicate :
eval_env -> bool -> predicate -> eval_env
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index a505839980c..e4b4c543a70 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -100,6 +100,24 @@ let assigns_outputs_to_zone ~result state assigns =
| WritesAny -> Locations.Zone.top
| Writes l -> List.fold_left treat_asgn Locations.Zone.bottom l
+type tlval_zones = {
+ under: Locations.Zone.t;
+ over: Locations.Zone.t;
+ deps: Locations.Zone.t;
+}
+
+let assigns_tlval_to_zones state access tlval =
+ let env = Eval_terms.env_post_f ~pre:state ~post:state ~result:None () in
+ let alarm_mode = Eval_terms.Ignore in
+ try
+ let under, over =
+ Eval_terms.eval_tlval_as_zone_under_over ~alarm_mode access env tlval
+ in
+ let deps = join_logic_deps (Eval_terms.tlval_deps env tlval) in
+ Some { under; over; deps; }
+ with Eval_terms.LogicEvalError _ -> None
+
+
(* -------------------------------------------------------------------------- *)
(* --- Verify assigns clauses --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index 92d6afd8168..7e478d9b4c5 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -50,6 +50,18 @@ val assigns_outputs_to_zone:
result: Cil_types.varinfo option ->
Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+(** Zones of an lvalue term of an assigns clause. *)
+type tlval_zones = {
+ under: Locations.Zone.t; (** Under-approximation of the memory zone. *)
+ over: Locations.Zone.t; (** Over-approximation of the memory zone. *)
+ deps: Locations.Zone.t; (** Dependencies needed to evaluate the address. *)
+}
+
+(** Evaluation of the memory zones and dependencies of an lvalue term from an
+ assigns clause, in the given cvalue state for a read or write access. *)
+val assigns_tlval_to_zones:
+ Cvalue.Model.t -> Locations.access -> Cil_types.term -> tlval_zones option
+
(** Evaluate the assigns clauses of the given function in its given pre-state,
and compare them with the given froms (computed by the from plugin).
Emits warnings if needed, and sets statuses to the assigns clauses. *)
--
GitLab