From 1dac43ff74ea3de3abeef1d95f9a784d21fb51f3 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 26 Sep 2023 14:22:21 +0200
Subject: [PATCH] [Eva] use the new Deps module
---
.../eva/domains/cvalue/builtins_memory.ml | 8 +++-----
src/plugins/eva/domains/octagons.ml | 12 +++--------
src/plugins/eva/legacy/logic_inout.ml | 4 ++--
src/plugins/eva/utils/eva_utils.ml | 20 +++----------------
src/plugins/eva/utils/eva_utils.mli | 10 ++--------
5 files changed, 13 insertions(+), 41 deletions(-)
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index 073fc79acf0..c9d89b45120 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -148,9 +148,7 @@ let frama_c_memcpy name state actuals =
let (deps_table, sure_zone) =
let zone_dst = enumerate_valid_bits Locations.Write loc_dst in
let zone_src = enumerate_valid_bits Locations.Read loc_src in
- let deps =
- Function_Froms.(Deps.add_data_dep Deps.bottom zone_src)
- in
+ let deps = Deps.data zone_src in
(* Note: actually a part may be written for sure (if the
difference between the offsets in loc_dst is smaller
than size), but keeping it imprecise reflects more the
@@ -192,10 +190,10 @@ let frama_c_memcpy name state actuals =
let loc_src = make_loc (Location_Bits.shift range src) size_char in
let loc_dst = make_loc (Location_Bits.shift range dst) size_char in
let c_from =
- let open Function_Froms in
let zone_src = enumerate_valid_bits Locations.Read loc_src in
let zone_dst = enumerate_valid_bits Locations.Write loc_dst in
- let deps = Deps.add_data_dep Deps.bottom zone_src in
+ let deps = Deps.data zone_src in
+ let open Function_Froms in
let deps_table =
Memory.add_binding ~exact:false precise_deps_table zone_dst deps
in
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 6ba460b8da9..2cbaa286e14 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -56,7 +56,7 @@ let typ_kind typ =
| TFloat _ -> Float
| _ -> assert false
-type dependencies = Eva_utils.deps = {
+type dependencies = Deps.t = {
data: Locations.Zone.t;
indirect: Locations.Zone.t;
}
@@ -836,12 +836,6 @@ end
module VariableToDeps =
struct
- module Deps =
- struct
- include Function_Froms.Deps
- let pretty_debug = pretty_precise
- end
-
let cache_prefix = "Eva.Octagons.VariableToDeps"
include Hptmap.Make (Variable) (Deps) (Hptmap.Comp_unused)
@@ -1040,7 +1034,7 @@ module Deps = struct
BaseToVariables.add_deps var deps i
in
match VariableToDeps.find_opt var m with
- | Some previous_deps when Function_Froms.Deps.equal previous_deps deps ->
+ | Some previous_deps when Deps.equal previous_deps deps ->
m, i
| Some previous_deps when not (are_bases_increasing previous_deps deps) ->
(* If [var] already exists in the state and had bigger dependencies (a
@@ -1053,7 +1047,7 @@ module Deps = struct
contain variables that do not appear in [m]. *)
let add var deps (m, i: t): t =
match VariableToDeps.find_opt var m with
- | Some d when Function_Froms.Deps.equal d deps -> m, i
+ | Some d when Deps.equal d deps -> m, i
| _ ->
VariableToDeps.add var deps m,
BaseToVariables.add_deps var deps i
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index 03c6ee235ba..e1239bd8a79 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -165,8 +165,8 @@ let check_from pre_state asgn assigns_zone from found_froms =
let eval = eval_assigns_from pre_state in
let stated_indirect_deps = link (List.map eval indirect_deps) in
let stated_direct_deps = link (List.map eval direct_deps) in
- let found_direct_deps = found_deps.Function_Froms.Deps.data in
- let found_indirect_deps = found_deps.Function_Froms.Deps.indirect in
+ let found_direct_deps = found_deps.Deps.data in
+ let found_indirect_deps = found_deps.Deps.indirect in
let res_for_unknown txt =
Self.debug "found_direct deps %a stated_direct_deps %a \
found_indirect_deps %a stated_indirect_deps %a"
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index e1a9d043fec..8741fe7ea42 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -285,20 +285,6 @@ let lval_to_exp =
MemoLvalToExp.memo
(fun lv -> Cil.new_exp ~loc:Cil_datatype.Location.unknown (Lval lv))
-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 deps_of_expr find_loc expr =
let rec process expr = match expr.enode with
@@ -310,7 +296,7 @@ let rec deps_of_expr find_loc expr =
process e
| BinOp (_, e1, e2, _) ->
(* Binary operators. *)
- join_deps (process e1) (process e2)
+ Deps.join (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. *)
@@ -318,11 +304,11 @@ let rec deps_of_expr find_loc expr =
indirect = Locations.Zone.bottom; }
| Const _ | SizeOf _ | AlignOf _ | SizeOfStr _ | SizeOfE _ | AlignOfE _ ->
(* static constructs, nothing is read to evaluate them. *)
- bottom_deps
+ Deps.bottom
in
process expr
-and zone_of_expr find_loc expr = deps_to_zone (deps_of_expr find_loc 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 *)
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index b7c7a84512a..2e6380b1ba6 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/src/plugins/eva/utils/eva_utils.mli
@@ -126,18 +126,12 @@ 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
+ (lval -> Precise_locs.precise_location) -> exp -> Deps.t
(** Given a function computing the location of lvalues, computes the memory
dependencies of an expression. *)
-val deps_of_lval: (lval -> Precise_locs.precise_location) -> lval -> deps
+val deps_of_lval: (lval -> Precise_locs.precise_location) -> lval -> Deps.t
(** Given a function computing the location of lvalues, computes the memory
dependencies of an lvalue. *)
--
GitLab