[Eva] In bases, locations, cvalue and lmap: adds function [replace_base].

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:

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 ../../.."

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

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} *)
 

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

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. *)

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)

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