[Eva] multidim: reorganize files

- split Abstract_memory into multiple file
- move from kernel_services to value/domains/multidim

Makefile

@@ -605,9 +605,6 @@ KERNEL_CMO=\
 	src/kernel_services/abstract_interp/locations.cmo               \
 	src/kernel_services/abstract_interp/lmap.cmo                    \
 	src/kernel_services/abstract_interp/lmap_bitwise.cmo            \
-	src/kernel_services/abstract_interp/multidim.cmo                \
-	src/kernel_services/abstract_interp/abstract_offset.cmo         \
-	src/kernel_services/abstract_interp/abstract_memory.cmo         \
 	src/kernel_services/visitors/visitor.cmo                        \
 	src/kernel_services/ast_data/statuses_by_call.cmo               \
 	src/kernel_services/ast_printing/printer_tag.cmo                \
@@ -822,7 +819,7 @@ PLUGIN_NAME:=Eva
 PLUGIN_DIR:=src/plugins/value
 PLUGIN_EXTRA_DIRS:=engine values domains api domains/cvalue domains/apron \
 	domains/gauges domains/equality legacy partitioning utils gui_files \
-	api values/numerors domains/numerors
+	api values/numerors domains/numerors domains/multidim
 PLUGIN_TESTS_DIRS+=value/traces
 PLUGIN_GENERATED:=$(PLUGIN_DIR)/Eva.mli
 PLUGIN_DISTRIB_EXTERNAL+=gen-api.sh
@@ -905,7 +902,15 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
 	engine/transfer_logic engine/transfer_stmt engine/transfer_specification \
 	engine/mem_exec engine/iterator engine/initialization \
 	engine/compute_functions engine/analysis register \
-	domains/multidim_domain \
+	domains/multidim/lattice_extrema \
+	domains/multidim/multidim \
+	domains/multidim/abstract_offset \
+	domains/multidim/abstract_memory \
+	domains/multidim/pretty_memory \
+	domains/multidim/abstract_structure \
+	domains/multidim/segmentation \
+	domains/multidim/typed_memory \
+	domains/multidim/multidim_domain \
 	domains/taint_domain \
 	$(APRON_CMO) $(NUMERORS_CMO) \
 	utils/eva_results \

headers/header_spec.txt

@@ -474,10 +474,6 @@ src/kernel_services/README.md: .ignore
 src/kernel_services/abstract_interp/README.md: .ignore
 src/kernel_services/abstract_interp/abstract_interp.ml: CEA_LGPL
 src/kernel_services/abstract_interp/abstract_interp.mli: CEA_LGPL
-src/kernel_services/abstract_interp/abstract_memory.ml: CEA_LGPL
-src/kernel_services/abstract_interp/abstract_memory.mli: CEA_LGPL
-src/kernel_services/abstract_interp/abstract_offset.ml: CEA_LGPL
-src/kernel_services/abstract_interp/abstract_offset.mli: CEA_LGPL
 src/kernel_services/abstract_interp/base.ml: CEA_LGPL
 src/kernel_services/abstract_interp/base.mli: CEA_LGPL
 src/kernel_services/abstract_interp/eva_lattice_type.mli: CEA_LGPL
@@ -516,8 +512,6 @@ src/kernel_services/abstract_interp/locations.ml: CEA_LGPL
 src/kernel_services/abstract_interp/locations.mli: CEA_LGPL
 src/kernel_services/abstract_interp/map_lattice.ml: CEA_LGPL
 src/kernel_services/abstract_interp/map_lattice.mli: CEA_LGPL
-src/kernel_services/abstract_interp/multidim.ml: CEA_LGPL
-src/kernel_services/abstract_interp/multidim.mli: CEA_LGPL
 src/kernel_services/abstract_interp/offsetmap.ml: CEA_LGPL
 src/kernel_services/abstract_interp/offsetmap.mli: CEA_LGPL
 src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli: CEA_LGPL
@@ -1416,8 +1410,23 @@ src/plugins/value/domains/hcexprs.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/hcexprs.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/inout_domain.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/inout_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/multidim_domain.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/abstract_memory.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/abstract_memory.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/abstract_offset.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/abstract_offset.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/abstract_structure.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/abstract_structure.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/lattice_extrema.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/multidim.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/multidim.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/multidim_domain.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/multidim_domain.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/pretty_memory.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/pretty_memory.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/segmentation.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/segmentation.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/typed_memory.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/multidim/typed_memory.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/octagons.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/octagons.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/offsm_domain.ml: CEA_LGPL_OR_PROPRIETARY

src/plugins/value/domains/multidim/abstract_memory.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Lattice_extrema
+
+
+(* Composition operator for compare function *)
+
+let (<?>) c lcmp =
+  if c = 0 then 0 else Lazy.force lcmp
+
+
+(* Imprecise bits abstraction *)
+
+type initialization =
+  | SurelyInitialized
+  | MaybeUninitialized
+
+type bit =
+  | Uninitialized
+  | Zero of initialization
+  | Any of Base.SetLattice.t * initialization
+
+module Initialization =
+struct
+  let pretty fmt = function
+    | SurelyInitialized -> ()
+    | MaybeUninitialized ->
+      Format.fprintf fmt "or UNINITIALIZED"
+
+  let hash = function
+    | SurelyInitialized -> 3
+    | MaybeUninitialized -> 7
+
+  let equal i1 i2 =
+    match i1, i2 with
+    | SurelyInitialized, SurelyInitialized
+    | MaybeUninitialized, MaybeUninitialized -> true
+    | _, _ -> false
+
+  let compare i1 i2 =
+    match i1, i2 with
+    | SurelyInitialized, SurelyInitialized
+    | MaybeUninitialized, MaybeUninitialized -> 0
+    | SurelyInitialized, MaybeUninitialized -> -1
+    | MaybeUninitialized, SurelyInitialized -> 1
+
+  let is_included i1 i2 =
+    match i1, i2 with
+    | SurelyInitialized, _
+    | _, MaybeUninitialized -> true
+    | MaybeUninitialized, SurelyInitialized -> false
+
+  let join i1 i2 =
+    match i1, i2 with
+    | SurelyInitialized, SurelyInitialized -> SurelyInitialized
+    | MaybeUninitialized, _
+    | _, MaybeUninitialized -> MaybeUninitialized
+end
+
+module Bit =
+struct
+  module Bases = Base.SetLattice
+
+  type t = bit
+
+  let uninitialized = Uninitialized
+  let zero = Zero SurelyInitialized
+  let numerical = Any (Bases.empty, SurelyInitialized)
+  let top = Any (Bases.top, MaybeUninitialized)
+
+
+  let pretty fmt = function
+    | Uninitialized ->
+      Format.fprintf fmt "UNINITIALIZED"
+    | Zero i ->
+      Format.fprintf fmt "0%a" Initialization.pretty i
+    | Any (Set set, i) when Base.SetLattice.O.is_empty set ->
+      Format.fprintf fmt "[--..--]%a" Initialization.pretty i
+    | Any _ -> Format.fprintf fmt "T"
+
+  let is_any = function Any _ -> true | _ -> false
+
+  let hash = function
+    | Uninitialized -> 7
+    | Zero i -> Hashtbl.hash (3, Initialization.hash i)
+    | Any (set, i)-> Hashtbl.hash (53, Bases.hash set, Initialization.hash i)
+
+  let equal d1 d2 =
+    match d1,d2 with
+    | Uninitialized, Uninitialized -> true
+    | Zero i1, Zero i2 -> Initialization.equal i1 i2
+    | Any (set1,i1), Any (set2,i2) ->
+      Bases.equal set1 set2 && Initialization.equal i1 i2
+    | _, _ -> false
+
+  let compare d1 d2 =
+    match d1,d2 with
+    | Uninitialized, Uninitialized -> 0
+    | Zero i1, Zero i2 -> Initialization.compare i1 i2
+    | Any (set1,i1), Any (set2,i2) ->
+      Bases.compare set1 set2 <?> lazy (Initialization.compare i1 i2)
+    | Uninitialized, _ -> 1
+    | _, Uninitialized -> -1
+    | Zero _, _ -> 1
+    | _, Zero _-> -1
+
+  let initialization = function
+    | Uninitialized -> MaybeUninitialized
+    | Zero i -> i
+    | Any (_,i) -> i
+
+  let is_included d1 d2 =
+    Initialization.is_included (initialization d1) (initialization d2) &&
+    match d1, d2 with
+    | Uninitialized, _ -> true
+    | _, Uninitialized -> false
+    | Zero _, _ -> true
+    | _, Zero _ -> false
+    | Any (set1,_), Any (set2,_) -> Bases.is_included set1 set2
+
+  let join d1 d2 =
+    match d1, d2 with
+    | Uninitialized, Uninitialized -> Uninitialized
+    | Zero i1, Zero i2 ->
+      Zero (Initialization.join i1 i2)
+    | Any (set1,i1), Any (set2,i2) ->
+      Any (Bases.join set1 set2, Initialization.join i1 i2)
+    | Zero _, Uninitialized
+    | Uninitialized, Zero _ -> Zero MaybeUninitialized
+    | Any (set,i), (Zero _ | Uninitialized as b)
+    | (Zero _ | Uninitialized as b), Any (set,i) ->
+      Any (set, Initialization.join i (initialization b))
+end
+
+
+(* Early stage of memory abstraction building *)
+
+type size = Integer.t
+type side = Left | Right
+type oracle = Cil_types.exp -> Int_val.t
+type bioracle = side -> oracle
+
+module type ProtoMemory =
+sig
+  type t
+  type value
+
+  val pretty : Format.formatter -> t -> unit
+  val pretty_root : Format.formatter -> t -> unit
+  val hash : t -> int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+
+  val of_raw : bit -> t
+  val raw : t -> bit
+  val of_value : Cil_types.typ -> value -> t
+  val to_value : Cil_types.typ -> t -> value
+  val to_singleton_int : t -> Integer.t option
+  val weak_erase : bit -> t -> t
+  val is_included : t -> t -> bool
+  val unify : oracle:bioracle ->
+    (size:size -> value -> value -> value) -> t -> t -> t
+  val join : oracle:bioracle -> t -> t -> t
+  val smash : oracle:oracle -> t -> t -> t
+  val read : oracle:oracle -> (Cil_types.typ -> t -> 'a) -> ('a -> 'a -> 'a) ->
+    Abstract_offset.t -> t -> 'a
+  val update : oracle:oracle ->
+    (weak:bool -> Cil_types.typ -> t -> t or_bottom) ->
+    weak:bool -> Abstract_offset.t -> t -> t or_bottom
+  val incr_bound : oracle:oracle -> Cil_types.varinfo -> Integer.t option ->
+    t -> t
+  val add_segmentation_bounds : oracle:oracle -> typ:Cil_types.typ ->
+    Cil_types.exp list -> t -> t
+end

src/plugins/value/domains/multidim/abstract_memory.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Lattice_extrema
+
+(* Memory initialization *)
+type initialization =
+  | SurelyInitialized
+  | MaybeUninitialized
+
+(* Abstraction of an unstructured bit in the memory *)
+type bit =
+  | Uninitialized (* Uninitialized everywhere *)
+  | Zero of initialization (* Zero or uninitialized everywhere *)
+  | Any of Base.SetLattice.t * initialization
+  (* Undetermined anywhere, and can contain bits
+     of pointers. If the base set is empty,
+     the bit can only come from numerical values. *)
+
+module Bit :
+sig
+  type t = bit
+
+  val uninitialized : t
+  val zero : t
+  val numerical : t
+  val top : t
+
+  val is_any : t -> bool
+  val initialization : t -> initialization
+
+  val pretty : Format.formatter -> t -> unit
+  val hash : t -> int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+
+  val is_included : t -> t -> bool
+  val join : t -> t -> t
+end
+
+(* Size type for memory abstraction *)
+type size = Integer.t
+
+(* Oracles for memory abstraction *)
+type side = Left | Right
+type oracle = Cil_types.exp -> Int_val.t
+type bioracle = side -> oracle
+
+(* Early stage of memory abstraction building *)
+module type ProtoMemory =
+sig
+  type t
+  type value
+
+  val pretty : Format.formatter -> t -> unit
+  val pretty_root : Format.formatter -> t -> unit
+  val hash : t -> int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+
+  val of_raw : bit -> t
+  val raw : t -> bit
+  val of_value : Cil_types.typ -> value -> t
+  val to_value : Cil_types.typ -> t -> value
+  val to_singleton_int : t -> Integer.t option
+  val weak_erase : bit -> t -> t
+  val is_included : t -> t -> bool
+  val unify : oracle:bioracle ->
+    (size:size -> value -> value -> value) -> t -> t -> t
+  val join : oracle:bioracle -> t -> t -> t
+  val smash : oracle:oracle -> t -> t -> t
+  val read : oracle:oracle -> (Cil_types.typ -> t -> 'a) -> ('a -> 'a -> 'a) ->
+    Abstract_offset.t -> t -> 'a
+  val update : oracle:oracle ->
+    (weak:bool -> Cil_types.typ -> t -> t or_bottom) ->
+    weak:bool -> Abstract_offset.t -> t -> t or_bottom
+  val incr_bound : oracle:oracle -> Cil_types.varinfo -> Integer.t option ->
+    t -> t
+  val add_segmentation_bounds : oracle:oracle -> typ:Cil_types.typ ->
+    Cil_types.exp list -> t -> t
+end

src/kernel_services/abstract_interp/abstract_offset.ml → src/plugins/value/domains/multidim/abstract_offset.ml

@@ -20,34 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Top =
-struct
-  [@@@warning "-32"]
-
-  let zip x y =
-    match x, y with
-    | `Top, _ | _, `Top -> `Top
-    | `Value x, `Value y -> `Value (x,y)
-
-  let (>>-) t f = match t with
-    | `Top  -> `Top
-    | `Value t -> f t
-
-  let (>>-:) t f = match t with
-    | `Top  -> `Top
-    | `Value t -> `Value (f t)
-
-  let (let+) = (>>-:)
-  let (and+) = zip
-  let (let*) = (>>-)
-
-  let of_option = function
-    | None -> `Top
-    | Some x -> `Value x
-end
-
-type 'a or_top = [`Value of 'a | `Top]
-
+open Lattice_extrema
 open Top
 
 type t =

src/kernel_services/abstract_interp/abstract_offset.mli → src/plugins/value/domains/multidim/abstract_offset.mli

@@ -20,13 +20,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Lattice_extrema
+
 type t =
   | NoOffset of Cil_types.typ
   | Index of Cil_types.exp option * Int_val.t * Cil_types.typ * t
   | Field of Cil_types.fieldinfo * t
 
-type 'a or_top = [`Value of 'a | `Top]
-
 val pretty : Format.formatter -> t -> unit
 
 val of_var_address : Cil_types.varinfo -> t

src/plugins/value/domains/multidim/abstract_structure.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Lattice_extrema
+open Abstract_memory
+open Pretty_memory
+
+let no_oracle = fun _exp -> Int_val.top
+
+(* Composition operator for compare function *)
+
+let (<?>) c lcmp =
+  if c = 0 then 0 else Lazy.force lcmp
+
+
+(* ------------------------------------------------------------------------ *)
+(* --- C struct abstraction                                             --- *)
+(* ------------------------------------------------------------------------ *)
+
+module type Config =
+sig
+  val deps : State.t list
+end
+
+module type Structure =
+sig
+  type t
+  type submemory
+  val pretty : Format.formatter -> t -> unit
+  val hash : t -> int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+  val raw : t -> Bit.t
+  val of_raw : Bit.t -> t
+  val weak_erase : Bit.t -> t -> t
+  val is_included : t -> t -> bool
+  val unify : (submemory -> submemory -> submemory) -> t -> t -> t
+  val read : t -> Cil_types.fieldinfo -> submemory
+  val update : (submemory -> submemory or_bottom) -> t -> Cil_types.fieldinfo ->
+    t or_bottom
+  val map : (submemory -> submemory) -> t -> t
+end
+
+module Make (Config : Config) (M : ProtoMemory) =
+struct
+  module Field =
+  struct
+    include Cil_datatype.Fieldinfo
+    let id f = f.Cil_types.forder (* At each node, all fields come from the same comp *)
+  end
+  module Values =
+  struct
+    include Datatype.Make (
+      struct
+        include Datatype.Serializable_undefined
+        include M
+        let name = "Abstract_Memory.Structure.Values"
+        let reprs = [ of_raw Bit.zero ]
+      end)
+    let pretty_debug = pretty
+  end
+  module Initial_Values = struct let v = [[]] end
+  module Deps = struct let l = Config.deps end
+
+  module FieldMap =
+    Hptmap.Make (Field) (Values) (Hptmap.Comp_unused) (Initial_Values) (Deps)
+
+  type t = {
+    padding: Bit.t;
+    fields: FieldMap.t;
+  }
+
+  type submemory = M.t
+
+  let pretty fmt m =
+    pp_iter2 ~format:"@[<hv>.%a%a@]"
+      FieldMap.iter Field.pretty M.pretty fmt m.fields
+
+  let hash m =
+    Hashtbl.hash (m.padding, FieldMap.hash m.fields)
+
+  let equal m1 m2 =
+    FieldMap.equal m1.fields m2.fields &&
+    Bit.equal m1.padding m2.padding
+
+  let compare m1 m2 =
+    FieldMap.compare m1.fields m2.fields <?>
+    lazy (Bit.compare m1.padding m2.padding)
+
+  let raw m =
+    FieldMap.fold (fun _ x acc -> Bit.join acc (M.raw x)) m.fields m.padding
+
+  let of_raw m =
+    { padding = m ; fields = FieldMap.empty }
+
+  let weak_erase b m =
+    {
+      padding = Bit.join b m.padding ;
+      fields = FieldMap.map (M.weak_erase b) m.fields ;
+    }
+
+  let is_included m1 m2 =
+    Bit.is_included m1.padding m2.padding &&
+    let decide_fast s t = if s == t then FieldMap.PTrue else PUnknown in
+    let decide_fst _fi m1 = M.is_included m1 (M.of_raw m2.padding) in
+    let decide_snd _fi m2 = M.is_included (M.of_raw m1.padding) m2 in
+    let decide_both _fi m1 m2 = M.is_included m1 m2 in
+    FieldMap.binary_predicate Hptmap_sig.NoCache UniversalPredicate
+      ~decide_fast ~decide_fst ~decide_snd ~decide_both
+      m1.fields m2.fields
+
+  let unify f m1 m2 = (* f is not symmetric *)
+    let decide_both _fi = fun m1 m2 -> Some (f m1 m2)
+    and decide_left = FieldMap.Traversing (fun _fi m1 ->
+        Some (f m1 (M.of_raw m2.padding)))
+    and decide_right = FieldMap.Traversing (fun _fi m2 ->
+        Some (f (M.of_raw m1.padding) m2))
+    in
+    let fields = FieldMap.merge
+        ~cache:Hptmap_sig.NoCache ~symmetric:false ~idempotent:true
+        ~decide_both ~decide_left ~decide_right
+        m1.fields m2.fields
+    in { padding = Bit.join m1.padding m2.padding ; fields }
+
+  let read m fi =
+    try
+      FieldMap.find fi m.fields
+    with Not_found -> (* field undefined *)
+      M.of_raw m.padding
+
+  let update f m fi =
+    try
+      let update' opt =
+        let x = Option.value ~default:(M.of_raw m.padding) opt in
+        match f x with
+        | `Value v -> Some v
+        | `Bottom -> raise Exit
+      in
+      `Value { m with fields = FieldMap.replace update' fi m.fields }
+    with Exit ->
+      `Bottom
+
+  let map f m =
+    { m with fields = FieldMap.map f m.fields }
+end
+
+
+(* ------------------------------------------------------------------------ *)
+(* --- Disjunctions of structures                                       --- *)
+(* ------------------------------------------------------------------------ *)
+
+(* This abstraction focus on catching structures invariants of the form
+
+   x.f = c₁ ⇒ ϕ₁(x)  ⋁  x.f = c₂ ⇒ ϕ₂(x)  ⋁  ...
+
+   where f is a field, c₁, c₂, ... are constants and ϕ₁, ϕ₂, ... properties
+   about the structure x.
+
+   During the analysis, we track fields f, called keys which are assigned
+   constant values. As the analysis  progresses, the set of keys is reduced each
+   time we discover one of the field is actually not a key because it is
+   assigned with non-singleton values. *)
+
+module type Disjunction =
+sig
+  type t
+  type submemory
+  type structure
+  val pretty : Format.formatter -> t -> unit
+  val hash : t -> int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+  val raw : t -> Bit.t
+  val of_raw : Cil_types.compinfo -> Bit.t -> t
+  val of_struct : Cil_types.compinfo -> structure -> t
+  val to_struct : oracle:oracle -> t -> structure
+  val weak_erase : Cil_types.compinfo -> Bit.t -> t -> t
+  val is_included : t -> t -> bool
+  val unify : oracle:bioracle -> (submemory -> submemory -> submemory) ->
+    t -> t -> t
+  val read : (submemory -> 'a) -> ('a -> 'a -> 'a)  ->
+    t -> Cil_types.fieldinfo -> 'a
+  val update : oracle:oracle -> (submemory -> submemory or_bottom) ->
+    t -> Cil_types.fieldinfo -> t or_bottom
+  val map : (submemory -> submemory) -> t -> t
+end
+
+module Disjunction (Config : Config) (M : ProtoMemory)
+    (S : Structure with type submemory = M.t) =
+struct
+  module Valuation =
+  struct
+    module FMap = Cil_datatype.Fieldinfo.Map
+    module FSet = Cil_datatype.Fieldinfo.Set
+
+    include FMap
+    include FMap.Make (Datatype.Integer)
+    let keys map = fold (fun k _ set -> FSet.add k set) map FSet.empty
+  end
+
+  module Map = (* 'a Map.t : (fi -> int) -> 'a *)
+  struct
+    module Info = struct let module_name = "Abstract_memory.Disjunction.Map" end
+    include Datatype.Map (Map.Make (Valuation)) (Valuation) (Info)
+
+    (* Defined only for Ocaml >= 4.11 *)
+    let filter_map f m =
+      fold (fun k x m -> match f k x with None -> m | Some y -> add k y m) m empty
+  end
+
+  module S = (* Structures in the disjunction *)
+  struct
+    include Datatype.Serializable_undefined
+    include S
+
+    let name = "Abstract_Memory.Disjunction.S"
+    let reprs = [ of_raw Bit.zero ]
+    let eval_key key m = M.to_singleton_int (read m key)
+    let suitable_key key m = Option.is_some (eval_key key m)
+    let keys_candidates ci m =
+      let fields = Option.value ~default:[] ci.Cil_types.cfields in
+      List.filter (fun fi -> suitable_key fi m) fields |>
+      Valuation.FSet.of_list
+    let evaluate keys m : Valuation.t =
+      let update_key fi map =
+        eval_key fi m |> (* should be Some *)
+        Option.fold ~none:map ~some:(fun v -> Valuation.add fi v map)
+      in
+      Valuation.FSet.fold update_key keys Valuation.empty
+  end
+
+  include Map.Make (Datatype.Make (S))
+
+  type submemory = M.t
+  type structure = S.t
+
+  let keys (m : t) = Valuation.keys (fst (Map.choose m))
+
+  let pick (m : t) =
+    match Map.choose_opt m with
+    | None -> Kernel.fatal "The disjunction should never be empty"
+    | Some (k,s) -> k,s,Map.remove k m
+
+  let pretty fmt (m : t) =
+    match Map.bindings m with
+    | [] -> assert false
+    | [(_,s)] -> S.pretty fmt s
+    | bindings ->
+      let l = List.map snd bindings in
+      pp_iter ~format:"@[<hv>%a@]" ~sep:" or @;<1 2>" List.iter S.pretty fmt l
+
+  let hash (m : t) =
+    Hashtbl.hash (Map.fold (fun _ s acc -> s :: acc) m [])
+
+  let reevaluate ~oracle keys (m : t) : t =
+    let update _k s acc =
+      let merge prev =
+        Extlib.merge_opt (fun () -> S.unify (M.smash ~oracle)) () (Some s) prev
+      in
+      Map.update (S.evaluate keys s) merge acc
+    in
+    Map.fold update m Map.empty
+
+  let smash ?(oracle=no_oracle) (m : t) =
+    let _k,s,m = pick m in
+    Map.fold (fun _k -> S.unify (M.smash ~oracle)) m s
+
+  let of_struct (ci : Cil_types.compinfo) (s : S.t) =
+    let keys = S.keys_candidates ci s in
+    Map.singleton (S.evaluate keys s) s
+
+  let to_struct ~oracle (m : t) =
+    smash ~oracle m
+
+  let raw (m : t) : bit =
+    let f _ x acc =
+      Bottom.join Bit.join acc (`Value (S.raw x))
+    in
+    Bottom.non_bottom (Map.fold f m `Bottom) (* The map should not be empty *)
+
+  let of_raw (ci : Cil_types.compinfo) (b : bit) : t =
+    let s = S.of_raw b in
+    of_struct ci s
+
+  let weak_erase (ci : Cil_types.compinfo) (b : bit) (m : t) : t =
+    (* if b is Zero, more could be done as all scalar fields might be a key *)
+    (* weak_erase is probably linear in the number of join operators, so we
+       weak_erase befoire joining as the join on erased memory is faster. *)
+    let m = Map.map (fun m -> S.weak_erase b m) m in
+    let s = smash m in
+    of_struct ci s
+
+  let is_included (m1 : t) (m2 : t) : bool  =
+    (* Imprecise inclusion: we only consider inclusion of disjunctions where
+       the set of field keys is the same *)
+    let aux k s1 =
+      match Map.find_opt k m2 with
+      | None -> false
+      | Some s2 -> S.is_included s1 s2
+    in
+    Map.for_all aux m1
+
+  let unify ~oracle f (m1 : t) (m2 : t) =
+    let keys = Valuation.FSet.inter (keys m1) (keys m2) in
+    let m1 = reevaluate ~oracle:(oracle Left) keys m1
+    and m2 = reevaluate ~oracle:(oracle Right) keys m2 in
+    Map.union (fun _k m1 m2 -> Some (S.unify f m1 m2)) m1 m2
+
+  let read map reduce (m : t) (fi : Cil_types.fieldinfo) =
+    let aux _k s acc =
+      map (S.read s fi) |>
+      Option.fold ~none:Fun.id ~some:reduce acc |>
+      Option.some
+    in
+    Option.get (Map.fold aux m None) (* If the map is not empty, result is Some *)
+
+  let update ~oracle f (m : t) (fi : Cil_types.fieldinfo) =
+    let m = Map.filter_map (fun _k s -> Bottom.to_option (S.update f s fi)) m in
+    if Map.is_empty m then
+      `Bottom
+    else
+      let is_key = Map.for_all (fun _k s -> S.suitable_key fi s) m in
+      let old_keys = keys m in
+      if is_key || Valuation.FSet.mem fi old_keys then
+        let new_keys =
+          if is_key
+          then Valuation.FSet.add fi old_keys
+          else Valuation.FSet.remove fi old_keys
+        in
+        `Value (reevaluate ~oracle new_keys m)
+      else
+        `Value (m)
+
+  let map f m =
+    Map.map (S.map f) m
+end

src/plugins/value/domains/multidim/abstract_structure.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Lattice_extrema
+open Abstract_memory
+
+module type Config =
+sig
+  (* Dependencies of the hash-consing table. The table will be cleared
+     whenever one of those dependencies is cleared. *)
+  val deps : State.t list
+end
+
+module type Structure =
+sig
+  type t
+  type submemory
+  val pretty : Format.formatter -> t -> unit
+  val hash : t -> int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+  val raw : t -> Bit.t
+  val of_raw : Bit.t -> t
+  val weak_erase : Bit.t -> t -> t
+  val is_included : t -> t -> bool
+  val unify : (submemory -> submemory -> submemory) -> t -> t -> t
+  val read : t -> Cil_types.fieldinfo -> submemory
+  val update : (submemory -> submemory or_bottom) -> t -> Cil_types.fieldinfo ->
+    t or_bottom
+  val map : (submemory -> submemory) -> t -> t
+end
+
+module Make (Config : Config) (M : ProtoMemory) :
+  Structure with type submemory = M.t
+
+module type Disjunction =
+sig
+  type t
+  type submemory
+  type structure
+  val pretty : Format.formatter -> t -> unit
+  val hash : t -> int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+  val raw : t -> Bit.t
+  val of_raw : Cil_types.compinfo -> Bit.t -> t
+  val of_struct : Cil_types.compinfo -> structure -> t
+  val to_struct : oracle:oracle -> t -> structure
+  val weak_erase : Cil_types.compinfo -> Bit.t -> t -> t
+  val is_included : t -> t -> bool
+  val unify : oracle:bioracle -> (submemory -> submemory -> submemory) ->
+    t -> t -> t
+  val read : (submemory -> 'a) -> ('a -> 'a -> 'a)  ->
+    t -> Cil_types.fieldinfo -> 'a
+  val update : oracle:oracle -> (submemory -> submemory or_bottom) ->
+    t -> Cil_types.fieldinfo -> t or_bottom
+  val map : (submemory -> submemory) -> t -> t
+end
+
+module Disjunction (Config : Config) (M : ProtoMemory)
+    (S : Structure with type submemory = M.t) :
+  Disjunction with type submemory = M.t and type structure = S.t

src/plugins/value/domains/multidim/lattice_extrema.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+type 'a or_bottom = [`Bottom | `Value of 'a]
+type 'a or_top = [`Top | `Value of 'a]
+type 'a or_top_bottom = [`Top | `Bottom | `Value of 'a]
+
+module Bot =
+struct
+  include Bottom.Type
+  let zip x y =
+    match x, y with
+    | `Bottom, _ | _, `Bottom -> `Bottom
+    | `Value x, `Value y -> `Value (x,y)
+
+  (* Applicative syntax *)
+  let ( let+ ) = (>>-:)
+  let ( and+ ) = zip
+  (* Monad syntax *)
+  let ( let* ) = (>>-)
+  let ( and* ) = zip
+end
+
+module Top =
+struct
+  let zip x y =
+    match x, y with
+    | `Top, _ | _, `Top -> `Top
+    | `Value x, `Value y -> `Value (x,y)
+
+  let (>>-) t f = match t with
+    | `Top  -> `Top
+    | `Value t -> f t
+
+  let (>>-:) t f = match t with
+    | `Top  -> `Top
+    | `Value t -> `Value (f t)
+
+  let (let+) = (>>-:)
+  let (and+) = zip
+  let (let*) = (>>-)
+  let (and*) = zip
+  let of_option = function
+    | None -> `Top
+    | Some v -> `Value v
+end
+
+module TopBot =
+struct
+  let (>>-) t f = match t with
+    | `Top  -> `Top
+    | `Bottom -> `Bottom
+    | `Value t -> f t
+
+  let (>>-:) t f = match t with
+    | `Top  -> `Top
+    | `Bottom -> `Bottom
+    | `Value t -> `Value (f t)
+
+  let (let+) = (>>-:)
+  let (let*) = (>>-)
+end

src/plugins/value/domains/multidim_domain.ml → src/plugins/value/domains/multidim/multidim_domain.ml

@@ -280,7 +280,7 @@ struct
     let disjunctive_invariants =
       Parameters.MultidimDisjunctiveInvariants.get
   end
-  module Memory = Abstract_memory.TypedMemory (Config) (Value_or_Uninitialized)
+  module Memory = Typed_memory.Make (Config) (Value_or_Uninitialized)
 
   module Prototype =
   (* Datatype *)

src/plugins/value/domains/multidim/pretty_memory.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+type 'a sformat = ('a,Format.formatter,unit) format
+type 'a formatter = Format.formatter -> 'a -> unit
+
+(* inspired by Pretty_utils.pp_iter *)
+
+let pp_iter
+    ?(pre=format_of_string "{@;<1 2>")
+    ?(sep=format_of_string ",@;<1 2>")
+    ?(suf=format_of_string "@ }")
+    ?(format=format_of_string "@[<hv>%a@]")
+    iter pp fmt v =
+  let need_sep = ref false in
+  Format.fprintf fmt pre;
+  iter (fun v ->
+      if !need_sep then Format.fprintf fmt sep else need_sep := true;
+      Format.fprintf fmt format pp v;
+    ) v;
+  Format.fprintf fmt suf
+
+let pp_iter2 ?pre ?sep ?suf ?(format=format_of_string "@[<hv>%a%a@]")
+    iter2 pp_key pp_val fmt v =
+  let iter f = iter2 (fun k v -> f (k,v)) in
+  let pp fmt (k,v) = Format.fprintf fmt format pp_key k pp_val v in
+  pp_iter ?pre ?sep ?suf ~format:"%a" iter pp fmt v

src/plugins/value/domains/multidim/pretty_memory.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+type 'a sformat = ('a,Format.formatter,unit) format
+type 'a formatter = Format.formatter -> 'a -> unit
+
+(* Pretty printing for iterators *)
+
+val pp_iter :
+  ?pre:unit sformat ->
+  ?sep:unit sformat ->
+  ?suf:unit sformat ->
+  ?format:('a formatter -> 'a -> unit) sformat ->
+  (('a -> unit) -> 'b -> unit) ->
+  'a formatter -> 'b formatter
+
+val pp_iter2 :
+  ?pre:(unit sformat) ->
+  ?sep:(unit sformat) ->
+  ?suf:(unit sformat) ->
+  ?format:('a formatter -> 'a -> 'b formatter -> 'b -> unit) sformat ->
+  (('a -> 'b -> unit) -> 'c -> unit) ->
+  'a formatter -> 'b formatter -> 'c formatter

src/plugins/value/domains/multidim/segmentation.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Lattice_extrema
+open Abstract_memory
+
+module type Config =
+sig
+  (* Limit on the number of slice after a write for array segmentations.
+     Makes sense above or equal to 1, though below 3 is counter-productive. *)
+  val slice_limit : unit -> int
+end
+
+module Bound :
+sig
+  type t
+  exception UnsupportedBoundExpression
+  val of_exp : Cil_types.exp -> t
+  val of_integer : Integer.t -> t
+  val succ : t -> t
+end
+
+module type Segmentation =
+sig
+  type bound = Bound.t
+  type submemory
+  type t
+  val pretty : Format.formatter -> t -> unit
+  val hash : t -> int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+  val hull : oracle:oracle -> t -> (bound * bound) or_top
+  val raw : t -> Bit.t
+  val weak_erase : Bit.t -> t -> t
+  val is_included : t -> t -> bool
+  val unify : oracle:bioracle -> (submemory -> submemory -> submemory) ->
+    t -> t -> t or_top
+  val single : bit -> bound -> bound -> submemory -> t
+  val read : oracle:oracle ->
+    (submemory -> 'a) -> ('a -> 'a -> 'a) -> t -> bound -> bound -> 'a
+  val update : oracle:oracle -> (submemory -> submemory or_bottom) ->
+    t -> bound -> bound -> t or_top_bottom
+  val incr_bound :
+    oracle:oracle -> Cil_types.varinfo -> Integer.t option -> t -> t or_top
+  val map : (submemory -> submemory) -> t -> t
+  val fold : (submemory -> 'a -> 'a) -> (bit -> 'b -> 'a) -> t -> 'b -> 'a
+  val add_segmentation_bounds : oracle:oracle -> bound list -> t -> t
+end
+
+module Make (Config : Config) (M : ProtoMemory) :
+  Segmentation with type submemory = M.t

src/kernel_services/abstract_interp/abstract_memory.mli → src/plugins/value/domains/multidim/typed_memory.mli

@@ -20,29 +20,23 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type size = Integer.t
+open Lattice_extrema
+open Abstract_memory
 
-type initialization =
-  | SurelyInitialized
-  | MaybeUninitialized
-
-type bit =
-  | Uninitialized (* Uninitialized everywhere *)
-  | Zero of initialization (* Zero or uninitialized everywhere *)
-  | Any of Base.SetLattice.t * initialization
-  (* Undetermined anywhere, and can contain bits
-     of pointers. If the base set is empty,
-     the bit can only come from numerical values. *)
-
-
-module Bit :
+(* Configuration of the Abstract Memory model *)
+module type Config =
 sig
-  type t = bit
+  (* Dependencies of the hash-consing table. The table will be cleared
+     whenever one of those dependencies is cleared. *)
+  val deps : State.t list
 
-  val uninitialized : t
-  val zero : t
-  val numerical : t
-  val top : t
+  (* Limit on the number of slice after a write for array segmentations.
+     Makes sense above or equal to 1, though below 3 is counter-productive. *)
+  val slice_limit : unit -> int
+
+  (* Whether the memory model try to infer some structure disjunctive
+     invariants. *)
+  val disjunctive_invariants : unit -> bool
 end
 
 (* Values the memory is mapped to *)
@@ -64,28 +58,7 @@ sig
   val join : t -> t -> t
 end
 
-module type Config =
-sig
-  (* Dependencies of the hash-consing table. The table will be cleared
-     whenever one of those dependencies is cleared. *)
-  val deps : State.t list
-
-  (* Limit on the number of slice after a write for array segmentations.
-     Makes sense above or equal to 1, though below 3 is counter-productive. *)
-  val slice_limit : unit -> int
-
-  (* Whether the memory model try to infer some structure disjunctive
-     invariants. *)
-  val disjunctive_invariants : unit -> bool
-end
-
-
-type side = Left | Right
-type oracle = Cil_types.exp -> Int_val.t
-type bioracle = side -> oracle
-type strength = Strong | Weak | Reinforce (* update strength *)
-
-module TypedMemory (Config : Config) (Value : Value) :
+module Make (Config : Config) (Value : Value) :
 sig
   type location = Abstract_offset.t
   type value = Value.t
@@ -123,7 +96,7 @@ sig
   (* Reinforce values on a set of locations when the locations match the
      memory structure ; does nothing on locations that cannot be matched *)
   val reinforce : oracle:oracle ->
-    (value -> value Bottom.or_bottom) ->  t -> location -> t Bottom.or_bottom
+    (value -> value or_bottom) ->  t -> location -> t or_bottom
 
   (* Test inclusion of one memory map into another *)
   val is_included : t -> t -> bool