From 85c58cde12be60777172dd848009d793abc87d02 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 17 Sep 2020 11:08:38 +0200
Subject: [PATCH] [Eva] In bases, locations, cvalue and lmap: adds function
[replace_base].
---
src/kernel_services/abstract_interp/base.ml | 12 ++++++++++++
src/kernel_services/abstract_interp/base.mli | 6 ++++++
src/kernel_services/abstract_interp/lmap.ml | 8 ++++++++
src/kernel_services/abstract_interp/lmap_sig.mli | 2 ++
src/kernel_services/abstract_interp/locations.ml | 13 +++++++++++++
src/kernel_services/abstract_interp/locations.mli | 4 ++++
src/plugins/value_types/cvalue.ml | 4 ++++
src/plugins/value_types/cvalue.mli | 2 ++
8 files changed, 51 insertions(+)
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 0bfde596c3a..0c7e3ba7eec 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -452,6 +452,7 @@ module Base = struct
let varname = Datatype.undefined
end)
let id = id
+ let pretty_debug = pretty
end
include Base
@@ -549,6 +550,17 @@ let of_string_exp e =
module SetLattice = Make_Hashconsed_Lattice_Set(Base)(Hptset)
+module BMap =
+ Hptmap.Make (Base) (Base) (Hptmap.Comp_unused)
+ (struct let v = [ [] ] end)
+ (struct let l = [ Ast.self ] end)
+
+type substitution = base Hptmap.Shape(Base).t
+
+let substitution_from_list list =
+ let add map (key, elt) = BMap.add key elt map in
+ let bmap = List.fold_left add BMap.empty list in
+ BMap.shape bmap
(*
Local Variables:
diff --git a/src/kernel_services/abstract_interp/base.mli b/src/kernel_services/abstract_interp/base.mli
index 708c79c5579..ccebf749bbf 100644
--- a/src/kernel_services/abstract_interp/base.mli
+++ b/src/kernel_services/abstract_interp/base.mli
@@ -225,6 +225,12 @@ val register_memory_var : Cil_types.varinfo -> validity -> t
They are created only to fill the contents of another variable.
Their field [vsource] is set to false. *)
+type substitution = base Hptmap.Shape(Base).t
+(** Type used for the substitution between bases. *)
+
+val substitution_from_list: (base * base) list -> substitution
+(** Creates a substitution from an association list. *)
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 46906585f76..b2223cda947 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -638,6 +638,14 @@ struct
| Top -> Top
| Map m -> Map (M.remove b m)
+ let replace_base shape = function
+ | Bottom -> Bottom
+ | Top -> Top
+ | Map map as t ->
+ let decide _key = Offsetmap.join in
+ let modified, map = M.replace_key ~decide shape map in
+ if modified then Map map else t
+
let is_reachable = function
| Bottom -> false
| Top | Map _ -> true
diff --git a/src/kernel_services/abstract_interp/lmap_sig.mli b/src/kernel_services/abstract_interp/lmap_sig.mli
index 9a7ac8d40b9..b9070fa559c 100644
--- a/src/kernel_services/abstract_interp/lmap_sig.mli
+++ b/src/kernel_services/abstract_interp/lmap_sig.mli
@@ -150,6 +150,8 @@ val filter_by_shape: 'a Hptmap.Shape(Base.Base).t -> t -> t
(** Removes the base if it is present. Does nothing otherwise. *)
val remove_base : Base.t -> t -> t
+val replace_base: Base.substitution -> t -> t
+
(** {2 Iterators} *)
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index f5c126c7119..442b8d59bc6 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -358,6 +358,19 @@ module Location_Bytes = struct
| Map _ -> false);
true
+ let replace_base substitution v =
+ let substitute replace make acc =
+ let modified, set' = replace substitution acc in
+ modified, if modified then make set' else v
+ in
+ match v with
+ | Top (Base.SetLattice.Top, _) -> false, v
+ | Top (Base.SetLattice.Set set, origin) ->
+ substitute Base.Hptset.replace (inject_top_origin_internal origin) set
+ | Map map ->
+ let decide _key = Ival.join in
+ substitute (M.replace_key ~decide) (fun m -> Map m) map
+
let overlaps ~partial ~size mm1 mm2 =
match mm1, mm2 with
| Top _, _ | _, Top _ -> intersects mm1 mm2
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index 760e1b93fa6..5157be7d4ed 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -78,6 +78,10 @@ module Location_Bytes : sig
(** [add b i loc] binds [b] to [i] in [loc] when [i] is not {!Ival.bottom},
and returns {!bottom} otherwise. *)
+ val replace_base: Base.substitution -> t -> bool * t
+ (** [replace_base subst loc] changes the location [loc] by substituting the
+ pointed bases according to [subst]. *)
+
val diff : t -> t -> t
(** Over-approximation of difference. [arg2] needs to be exact or an
under_approximation. *)
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index a545314edfe..0fdd5f2fea5 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -909,6 +909,10 @@ module V_Or_Uninitialized = struct
in
removed, t'
+ let replace_base substitution t =
+ let modified, v = V.replace_base substitution (get_v t) in
+ modified, if modified then create (get_flags t) v else t
+
let reduce_by_initializedness pos v =
if pos then
meet v (C_init_esc V.top)
diff --git a/src/plugins/value_types/cvalue.mli b/src/plugins/value_types/cvalue.mli
index a5c93243c0b..717c387372f 100644
--- a/src/plugins/value_types/cvalue.mli
+++ b/src/plugins/value_types/cvalue.mli
@@ -226,6 +226,8 @@ module V_Or_Uninitialized : sig
val unspecify_escaping_locals :
exact:bool -> (V.M.key -> bool) -> t -> bool * t
+ val replace_base: Base.substitution -> t -> bool * t
+
val map: (V.t -> V.t) -> t -> t
val map2: (V.t -> V.t -> V.t) -> t -> t -> t
(** initialized/escaping information is the join of the information
--
GitLab