[wp/region] complete refactor

src/plugins/region/Region.ml

@@ -49,4 +49,3 @@ let exp m e = Option.map (Memory.node m) @@ Memory.exp m e
 let cvar = Memory.cvar
 let field = Memory.field
 let index = Memory.index
-let shift m r ~size = Memory.sindex m r size

src/plugins/region/Region.mli

@@ -125,7 +125,3 @@ val field : map -> node -> fieldinfo -> node
 
 (** Unormalized. @raises Not_found *)
 val index : map -> node -> typ -> node
-
-(** The size if the size of elements of the array, in bits.
-    Unormalized. @raises Not_found *)
-val shift : map -> node -> size:int -> node

src/plugins/region/memory.ml

@@ -567,9 +567,6 @@ let field (m: map) (r: node) (fd: fieldinfo) : node =
 let index (m : map) (r: node) (ty:typ) : node =
   move m r 0 (Cil.bitsSizeOf ty)
 
-let sindex (m: map) (r: node) (size:int) : node =
-  move m r 0 size
-
 let rec lval (m: map) (h,ofs) : node =
   offset m (lhost m h) (Cil.typeOfLhost h) ofs
 

src/plugins/region/memory.mli

@@ -96,7 +96,6 @@ val merge_copy : map -> l:node -> r:node -> unit
 val cvar : map -> varinfo -> node
 val field : map -> node -> fieldinfo -> node
 val index : map -> node -> typ -> node
-val sindex : map -> node -> int -> node
 val lval : map -> lval -> node
 val exp : map -> exp -> node option
 

src/plugins/wp/MemRegion.ml

@@ -56,28 +56,16 @@ module type RegionProxy =
 sig
   type region
   module Type : Sigs.Type with type t = region
-  val null : unit -> region
-
+  val id : region -> int
+  val of_id : int -> region option
   val kind : region -> kind
-
-  val tau_of_region : region -> tau
-  val points_to : region -> region option
-
-  val separated : region -> region -> bool
-  val included : region -> region -> bool
-
   val cvar : varinfo -> region option
   val field : region -> fieldinfo -> region option
   val shift : region -> c_object -> region option
-  val base_addr : region -> region
-
+  val points_to : region -> region option
   val literal : eid:int -> Cstring.cst -> region option
-  val pointer_loc : unit -> region option
-  val loc_of_int : unit -> region option
-
-  val id : region -> int
-  val of_id : int -> region option
-
+  val separated : region -> region -> bool
+  val included : region -> region -> bool
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -86,10 +74,10 @@ end
 
 module type ModelWithLoader = sig
   include Sigs.Model
-
+  include Sigs.Model
   val sizeof : c_object -> term
-  val last : sigma -> c_object -> loc -> term
 
+  val last : sigma -> c_object -> loc -> term
   val frames : c_object -> loc -> chunk -> frame list
 
   val havoc : c_object -> loc -> length:term -> chunk -> fresh:term -> current:term -> term
@@ -100,18 +88,17 @@ module type ModelWithLoader = sig
   val load_float : sigma -> c_float -> loc -> term
   val load_pointer : sigma -> typ -> loc -> loc
 
-  val store_int : sigma -> c_int -> loc -> term -> Chunk.t * term
-  val store_float : sigma -> c_float -> loc -> term -> Chunk.t * term
-  val store_pointer : sigma -> typ -> loc -> term -> Chunk.t * term
+  val store_int : sigma -> c_int -> loc -> term -> chunk * term
+  val store_float : sigma -> c_float -> loc -> term -> chunk * term
+  val store_pointer : sigma -> typ -> loc -> term -> chunk * term
 
   val set_init_atom : sigma -> c_object -> loc -> term -> chunk * term
   val set_init : c_object -> loc -> length:term -> chunk -> current:term -> term
   val is_init_atom : sigma -> c_object -> loc -> term
   val is_init_range : sigma -> c_object -> loc -> term -> pred
 
-  val value_footprint : c_object -> loc -> Sigma.domain
-  val init_footprint : c_object -> loc -> Sigma.domain
-
+  val value_footprint : c_object -> loc -> domain
+  val init_footprint : c_object -> loc -> domain
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -183,14 +170,14 @@ struct
   let cmap f g (m,r) = (f m, g r)
   let cmap2 f g (m1,r1) (m2,r2) = (f m1 m2, g r1 r2)
   let capply f g (m,r) = function M c -> f m c, r | R c -> m, g r c
-  let cmerge f g c (m,r) = match c with M c -> f m c | R c -> g r c
+  let cmerge f g (m,r) = function M c -> f m c | R c -> g r c
+  let mseq { pre ; post } = { pre = fst pre ; post = fst post }
+  let rseq { pre ; post } = { pre = snd pre ; post = snd post }
 
-  module Chunk =
+  module Chunk : Sigs.Chunk with type t = chunk =
   struct
-    let self = "MemRegion.Make.Chunk"
-
     type t = chunk
-
+    let self = "Wp.MemRegion.Self"
     let hash = function
       | M c -> 3 * MChunk.hash c
       | R c -> 5 * RChunk.hash c
@@ -226,31 +213,35 @@ struct
   end
 
   module Heap = Qed.Collection.Make(Chunk)
+  module Domain = Heap.Set
 
   type sigma = MSigma.t * RSigma.t
-  type domain = Heap.Set.t
+  type domain = Domain.t
 
   module Sigma =
   struct
 
     type t = sigma
     type chunk = Chunk.t
-    module Chunk = Chunk
+    module Chunk = Heap
 
-    let create () : sigma = (MSigma.create (), RSigma.create ())
+    type domain = Domain.t
+
+    let create () : t = (MSigma.create (), RSigma.create ())
 
     let pretty fmt (m,r) =
       Format.fprintf fmt "@[<hv 0>{@[<hv 2>@ %a;@ %a;@]@ }@]"
         MSigma.pretty m
         RSigma.pretty r
 
-    let empty : domain = Heap.Set.empty
+    let empty : domain = Domain.empty
+    let union = Domain.union
     let mem = cmerge MSigma.mem RSigma.mem
     let get = cmerge MSigma.get RSigma.get
     let value = cmerge MSigma.value RSigma.value
     let copy = cmap MSigma.copy RSigma.copy
     let choose = cmap2 MSigma.choose RSigma.choose
-    let havoc_chunk = cmap MSigma.havoc_chunk RSigma.havoc_chunk
+    let havoc_chunk = capply MSigma.havoc_chunk RSigma.havoc_chunk
     let havoc_any ~call = cmap (MSigma.havoc_any ~call) (RSigma.havoc_any ~call)
 
     let merge (m1,r1) (m2,r2) =
@@ -279,14 +270,14 @@ struct
       end
 
     let mdomain d =
-      MHeap.Set.fold (fun c s -> Heap.Set.add (M c) s) d Heap.Set.empty
+      MHeap.Set.fold (fun c s -> Domain.add (M c) s) d Domain.empty
     let rdomain d =
-      RHeap.Set.fold (fun c s -> Heap.Set.add (R c) s) d Heap.Set.empty
+      RHeap.Set.fold (fun c s -> Domain.add (R c) s) d Domain.empty
 
     let dsplit d =
       let m = ref MHeap.Set.empty in
       let r = ref RHeap.Set.empty in
-      Heap.Set.iter
+      Domain.iter
         (function
           | M c -> m := MHeap.Set.add c !m
           | R c -> r := RHeap.Set.add c !r
@@ -308,23 +299,25 @@ struct
       MSigma.remove_chunks m dm, RSigma.remove_chunks r dr
 
     let domain (m,r) =
-      Heap.Set.union (mdomain @@ MSigma.domain m) (rdomain @@ RSigma.domain r)
+      union (mdomain @@ MSigma.domain m) (rdomain @@ RSigma.domain r)
 
-    let writes { pre = (m1,r1) ; post = (m2,r2) } =
-      let m = { pre = m1 ; post = m2 } in
-      let r = { pre = r1 ; post = r2 } in
-      Heap.Set.union (mdomain @@ MSigma.writes m) (rdomain @@ RSigma.writes r)
+    let writes (s : sigma sequence) =
+      union
+        (mdomain @@ MSigma.writes @@ mseq s)
+        (rdomain @@ RSigma.writes @@ rseq s)
 
   end
 
-  (***************************************************************************)
-  (* module Region : MemLoader.Module                                       **)
-  (***************************************************************************)
+  (* -------------------------------------------------------------------------- *)
+  (* --- Region Loader                                                         --- *)
+  (* -------------------------------------------------------------------------- *)
+
+  module Loader =
+  struct
+    let name = "MemRegion.Loader"
 
-  module Region = struct
     module Chunk = Chunk
     module Sigma = Sigma
-    let name = "RegionModel"
 
     type loc =
       | Null
@@ -335,16 +328,15 @@ struct
     let loc = function Null -> M.null | Raw a | Loc(a,_) -> a
     let reg = function Null | Raw _ -> None | Loc(_,r) -> Some r
     let kind = function Null | Raw _ -> Garbled | Loc(_,r) -> R.kind r
-    let rid = function Null | Raw _ -> 0 | Loc(_,r) -> R.id r
     let rfold f = function Null | Raw _ -> None | Loc(_,r) -> f r
-    let rmap f = function Null | Raw _ -> None | Loc(_,r) -> Some (f r)
 
     (* ---------------------------------------------------------------------- *)
     (* --- Utilities on locations                                         --- *)
     (* ---------------------------------------------------------------------- *)
 
     let last sigma ty l = M.last (fst sigma) ty (loc l)
-    let pointer_val l = M.pointer_val (loc l)
+
+    let to_addr l = M.pointer_val (loc l)
 
     let sizeof ty = M.sizeof ty
 
@@ -361,7 +353,7 @@ struct
         let sizeof = Lang.F.e_one in
         let tau = Chunk.tau_of_chunk c in
         let basename = Chunk.basename_of_chunk c in
-        MemMemory.frames ~addr:(pointer_val l) ~offset ~sizeof ~basename tau
+        MemMemory.frames ~addr:(to_addr l) ~offset ~sizeof ~basename tau
       | _ -> []
 
     let havoc ty l ~length chunk ~fresh ~current =
@@ -370,7 +362,7 @@ struct
       | R c ->
         match c.mu with
         | Value _ | ValInit -> fresh
-        | Array _ | ArrInit -> e_fun f_havoc [fresh;current;pointer_val l;length]
+        | Array _ | ArrInit -> e_fun f_havoc [fresh;current;to_addr l;length]
 
     let eqmem_forall ty l chunk m1 m2 =
       match chunk with
@@ -383,7 +375,7 @@ struct
           let p = e_var xp in
           let n = M.sizeof ty in
           let separated =
-            p_call MemAddr.p_separated [p;e_one;pointer_val l;n] in
+            p_call MemAddr.p_separated [p;e_one;to_addr l;n] in
           let equal = p_equal (e_get m1 p) (e_get m2 p) in
           [xp],separated,equal
 
@@ -400,7 +392,13 @@ struct
           "Attempt to %s without region (%a)" action M.pretty a
       | Loc(l,r) -> l,r
 
-    let check action (p:primitive) (q:primitive) =
+    let to_region_pointer l =
+      let l,r = localized "loader" l in R.id r, M.pointer_val l
+
+    let of_region_pointer r _ t =
+      make (M.pointer_loc t) (R.of_id r)
+
+    let check_access action (p:primitive) (q:primitive) =
       if Stdlib.(<>) p q then
         Warning.error ~source:"MemRegion"
           "Inconsistent %s (%a <> %a)"
@@ -411,10 +409,10 @@ struct
       match R.kind r with
       | Garbled -> M.load_int (fst sigma) iota l
       | Single p ->
-        check "load" p (Int iota) ;
+        check_access "load" p (Int iota) ;
         RSigma.value (snd sigma) { mu = Value p ; region = r }
       | Many p ->
-        check "load" p (Int iota) ;
+        check_access "load" p (Int iota) ;
         e_get
           (RSigma.value (snd sigma) { mu = Array p ; region = r})
           (M.pointer_val l)
@@ -424,16 +422,16 @@ struct
       match R.kind r with
       | Garbled -> M.load_float (fst sigma) flt l
       | Single p ->
-        check "load" p (Float flt) ;
+        check_access "load" p (Float flt) ;
         RSigma.value (snd sigma) { mu = Value p ; region = r }
       | Many p ->
-        check "load" p (Float flt) ;
+        check_access "load" p (Float flt) ;
         e_get
           (RSigma.value (snd sigma) { mu = Array p ; region = r})
           (M.pointer_val l)
 
     let load_pointer sigma ty loc : loc =
-      let l,r = localized "load float" loc in
+      let l,r = localized "load pointer" loc in
       match R.points_to r with
       | None ->
         Warning.error ~source:"MemRegion"
@@ -445,11 +443,11 @@ struct
           match R.kind r with
           | Garbled -> M.load_pointer (fst sigma) ty l
           | Single p ->
-            check "load" p Ptr ;
+            check_access "load" p Ptr ;
             M.pointer_loc @@
             RSigma.value (snd sigma) { mu = Value p ; region = r }
           | Many p ->
-            check "load" p Ptr ;
+            check_access "load" p Ptr ;
             M.pointer_loc @@
             e_get
               (RSigma.value (snd sigma) { mu = Array p ; region = r})
@@ -460,343 +458,137 @@ struct
     (* --- Store                                                          --- *)
     (* ---------------------------------------------------------------------- *)
 
-    let store_int sigma c_int loc v : Chunk.t * term = match loc with
-      | Null ->
-        let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.store_int"
-            ~effect:"Loc is Null" "Attempt to store_int inside Null"
-        in let c, t = M.store_int sigma.Tuple.model c_int M.null v in
-        M c, t
-      | Raw { repr } ->
-        let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.store_int"
-            ~effect:"Loc is Raw" "store_int(Raw %a)" M.pretty repr
-        in let c, t = M.store_int sigma.Tuple.model c_int repr v in
-        M c, t
-      | Loc { repr ; region } ->
-        let c = R (B.CVal region) in
-        match R.kind region with
-        | Many (Int c_int') as k ->
-          if compare_c_int c_int c_int' = 0
-          then (c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v)
-          else
-            let _ = Warning.emit ~severe:false
-                ~source:"MemRegion.Region.store_int"
-                ~effect:"Int types are not the same"
-                "(%a in %a : %a != %a)"
-                M.pretty repr R.pretty region pp_kind k Ctypes.pp_int c_int
-            in (c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v)
-        | Single (Int c_int') as k ->
-          if compare_c_int c_int c_int' = 0
-          then (c, v)
-          else
-            let _ = Warning.emit ~severe:false
-                ~source:"MemRegion.Region.store_int"
-                ~effect:"Int types are not the same"
-                "(%a in %a : %a != %a)"
-                M.pretty repr R.pretty region pp_kind k Ctypes.pp_int c_int
-            in (c, v)
-        | Garbled ->
-          let (c', v) = M.store_int sigma.model c_int repr v in
-          (M c', v)
-        | k ->
-          let _ = Warning.emit ~severe:false
-              ~source:"MemRegion.Region.store_int"
-              ~effect:"Int types are not the same"
-              "(%a in %a : %a != %a)"
-              M.pretty repr R.pretty region pp_kind k Ctypes.pp_int c_int
-          in assert false
-
-    let store_float sigma c_float loc v : Chunk.t * term = match loc with
-      | Null ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.store_float"
-            ~effect:"Loc is Null" "Attempt to store_float inside Null"
-        in let c, t = M.store_float sigma.Tuple.model c_float M.null v in
-        M c, t
-      | Raw { repr } ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.store_float"
-            ~effect:"Loc is Raw" "store_float(Raw %a)" M.pretty repr
-        in let c, t = M.store_float sigma.Tuple.model c_float repr v in
-        M c, t
-      | Loc { repr ; region } ->
-        let c = R (B.CVal region) in
-        match R.kind region with
-        | Many (Float c_float') as k ->
-          if compare_c_float c_float c_float' = 0
-          then (c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v)
-          else
-            let _ = Warning.emit ~severe:false
-                ~source:"MemRegion.Region.store_float"
-                ~effect:"Float types are not the same"
-                "(%a in %a : %a != %a)"
-                M.pretty repr R.pretty region pp_kind k Ctypes.pp_float c_float
-            in (c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v)
-        | Single (Float c_float') as k ->
-          if compare_c_float c_float c_float' = 0
-          then (c, v)
-          else
-            let _ = Warning.emit ~severe:false
-                ~source:"MemRegion.Region.store_float"
-                ~effect:"Float types are not the same"
-                "(%a in %a : %a != %a)"
-                M.pretty repr R.pretty region pp_kind k Ctypes.pp_float c_float
-            in (c, v)
-        | Garbled ->
-          let (c, t) = M.store_float sigma.Tuple.model c_float repr v in
-          (M c, t)
-        | k ->
-          let _ = Warning.emit ~severe:false
-              ~source:"MemRegion.Region.store_float"
-              ~effect:"Float types are not the same"
-              "(%a in %a : %a != %a)"
-              M.pretty repr R.pretty region pp_kind k Ctypes.pp_float c_float
-          in assert false
-
-    let store_pointer sigma ty loc v : Chunk.t * term = match loc with
-      | Null ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.store_pointer"
-            ~effect:"Loc is Null" "Attempt to store_pointer inside Null"
-        in let c, t = M.store_pointer sigma.Tuple.model ty M.null v in
-        M c, t
-      | Raw { repr } ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.store_pointer"
-            ~effect:"Loc is Raw" "store_pointer(Raw %a : *%a)"
-            M.pretty repr Printer.pp_typ ty
-        in let c, t = M.store_pointer sigma.Tuple.model ty repr v in
-        M c, t
-      | Loc { repr ; region } ->
-        let c = R (B.CVal region) in
-        match R.kind region with
-        | Many (Ptr) ->
-          c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v
-        | Single (Ptr) -> c,v
-        | Garbled ->
-          let (c, repr) = M.store_pointer sigma.Tuple.model ty repr v in
-          (M c, repr)
-        | k ->
-          let _ = Warning.emit ~severe:false
-              ~source:"MemRegion.Region.store_pointer"
-              ~effect:"This is not a region with pointer type"
-              "(%a in %a : %a != *%a)"
-              M.pretty repr R.pretty region pp_kind k Printer.pp_typ ty
-          in assert false
+    let store_int sigma iota loc v : Chunk.t * term =
+      let l,r = localized "store int" loc in
+      match R.kind r with
+      | Garbled ->
+        let c, m = M.store_int (fst sigma) iota l v in M c, m
+      | Single p ->
+        check_access "store" p (Int iota) ;
+        R { mu = Value p ; region = r }, v
+      | Many p ->
+        check_access "store" p (Int iota) ;
+        let rc = RChunk.{ mu = Array p ; region = r } in
+        R rc, e_set (RSigma.value (snd sigma) rc) (M.pointer_val l) v
+
+    let store_float sigma flt loc v : Chunk.t * term =
+      let l,r = localized "store float" loc in
+      match R.kind r with
+      | Garbled ->
+        let c,m = M.store_float (fst sigma) flt l v in M c, m
+      | Single p ->
+        check_access "store" p (Float flt) ;
+        R { mu = Value p ; region = r }, v
+      | Many p ->
+        check_access "store" p (Float flt) ;
+        let rc = RChunk.{ mu = Array p ; region = r } in
+        R rc, e_set (RSigma.value (snd sigma) rc) (M.pointer_val l) v
+
+    let store_pointer sigma ty loc v : Chunk.t * term =
+      let l,r = localized "store pointer" loc in
+      match R.kind r with
+      | Garbled ->
+        let c,m = M.store_pointer (fst sigma) ty l v in M c, m
+      | Single p ->
+        check_access "store" p Ptr ;
+        R { mu = Value p ; region = r }, v
+      | Many p ->
+        check_access "store" p Ptr ;
+        let rc = RChunk.{ mu = Array p ; region = r } in
+        R rc, e_set (RSigma.value (snd sigma) rc) (M.pointer_val l) v
 
     (* ---------------------------------------------------------------------- *)
     (* --- Init                                                           --- *)
     (* ---------------------------------------------------------------------- *)
 
-    let set_init_atom sigma ty loc v = match loc with
-      | Null ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.set_init_atom"
-            ~effect:"Loc is Null" "Attempt to set_init_atom with Null"
-        in let (c, t) = M.set_init_atom sigma.Tuple.model ty M.null v in
-        (M c, t)
-      | Raw { repr } ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.set_init_atom"
-            ~effect:"Loc is Raw" "set_init_atom(Raw %a <- %a)"
-            M.pretty repr QED.pretty v
-        in let (c, t) = M.set_init_atom sigma.Tuple.model ty repr v in
-        (M c, t)
-      | Loc { repr ; region }->
-        match R.kind region with
-        | Garbled ->
-          let (c, t) = M.set_init_atom sigma.Tuple.model ty repr v in
-          (M c, t)
-        | Single _-> R (B.CInit region), v
-        | Many _ ->
-          let c = R (B.CInit region) in
-          c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v
-
-    let is_init_atom sigma ty loc : term = match loc with
-      | Null ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.is_init_atom"
-            ~effect:"Loc is Null" "is_init_atom(Null)"
-        in M.is_init_atom sigma.Tuple.model ty M.null
-      | Raw { repr } ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.is_init_atom"
-            ~effect:"Loc is Raw" "is_init_atom(Raw %a)"
-            M.pretty repr
-        in M.is_init_atom sigma.Tuple.model ty repr
-      | Loc { repr ; region } ->
-        let c = R (B.CInit region) in
-        match R.kind region with
-        | Garbled -> M.is_init_atom sigma.Tuple.model ty repr
-        | Many _ -> F.e_get (Sigma.value sigma c) @@ M.pointer_val repr
-        | Single _ -> Sigma.value sigma c
-
-    let is_init_range sigma ty loc length : pred = match loc with
-      | Null ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.is_init_range"
-            ~effect:"Loc is Null" "is_init_range(Null)"
-        in M.is_init_range sigma.Tuple.model ty M.null length
-      | Raw { repr } ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.is_init_range"
-            ~effect:"Loc is Raw" "is_init_range(%a, ty=%a, length=%a)"
-            M.pretty repr Ctypes.pp_object ty QED.pretty length
-        in M.is_init_range sigma.Tuple.model ty repr length
-      | Loc { repr ; region } ->
-        match R.kind region with
-        | Garbled -> M.is_init_range sigma.Tuple.model ty repr length
-        | Many _ ->
-          let c = R (B.CInit region) in
-          let n = F.e_mul (M.sizeof ty) length in
-          F.p_call p_is_init_r [Sigma.value sigma c;M.pointer_val repr;n]
-        | Single _ as k ->
-          let _ = Warning.emit ~severe:false
-              ~source:"MemRegion.Region.is_init_range"
-              ~effect:"Region is Single kind" "is_init_range(%a in %a : %a, ty=%a, length=%a)"
-              M.pretty repr R.pretty region pp_kind k
-              Ctypes.pp_object ty QED.pretty length
-          in (* TODO *) assert false
-
-
-    let set_init ty loc ~length chunk ~current : term = match loc, chunk with
-      | Null, M c ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.set_init"
-            ~effect:"Loc is Null" "set_init(Null)"
-        in M.set_init ty M.null ~length c ~current
-      | Null, Chunk.CRegion _ ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.set_init"
-            ~effect:"Loc is Null" "set_init(Null) and Chunk is Region"
-        in assert false
-      | Raw { repr }, M c ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.set_init"
-            ~effect:"Loc is Null" "set_init(Raw %a)"
-            M.pretty repr
-        in M.set_init ty repr ~length c ~current
-      | Raw { repr }, Chunk.CRegion _ ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.set_init"
-            ~effect:"Loc is Null" "set_init(Raw %a) and Chunk is Region"
-            M.pretty repr
-        in assert false
-      | Loc { repr }, M c -> M.set_init ty repr ~length c ~current
-      | Loc { repr ; region }, Chunk.CRegion c ->
-        match R.kind region, c with
-        | Garbled, ( B.CVal _ | B.CInit _| B.CGhost _) ->
-          let _ = Warning.emit ~severe:false
-              ~source:"MemRegion.Region.set_init"
-              ~effect:"Garbled is not associated to low memory model"
-              "set_init(%a in %a : Garbled)"
-              M.pretty repr R.pretty region
-          in assert false
-        | Many _, _ ->
-          let n = F.e_mul (M.sizeof ty) length in
-          F.e_fun f_set_init [current;M.pointer_val repr;n]
-        | Single _, _ ->
-          let _ = Warning.emit ~severe:false
-              ~source:"MemRegion.Region.set_init"
-              ~effect:"Single is not supported"
-              "set_init(%a in %a : Single)"
-              M.pretty repr R.pretty region
-          in (* TODO *) assert false
+    let is_init_atom sigma ty loc : term =
+      let l,r = localized "init atom" loc in
+      match R.kind r with
+      | Garbled -> M.is_init_atom (fst sigma) ty l
+      | Single _-> RSigma.value (snd sigma) { mu = ValInit ; region = r }
+      | Many _ ->
+        e_get
+          (RSigma.value (snd sigma) { mu = ArrInit ; region = r })
+          (M.pointer_val l)
 
+    let set_init_atom sigma ty loc v : Chunk.t * term =
+      let l,r = localized "init atom" loc in
+      match R.kind r with
+      | Garbled ->
+        let c,m = M.set_init_atom (fst sigma) ty l v in M c, m
+      | Single _-> R { mu = ValInit ; region = r }, v
+      | Many _ ->
+        let rc = RChunk.{ mu = ArrInit ; region = r } in
+        R rc, e_set (RSigma.value (snd sigma) rc) (M.pointer_val l) v
+
+    let is_init_range sigma ty loc length : pred =
+      let l,r = localized "init atom" loc in
+      match R.kind r with
+      | Garbled -> M.is_init_range (fst sigma) ty l length
+      | Single _ ->
+        Lang.F.p_bool @@ RSigma.value (snd sigma) { mu = ValInit ; region = r }
+      | Many _ ->
+        let map = RSigma.value (snd sigma) { mu = ArrInit ; region = r } in
+        let size = e_mul (M.sizeof ty) length in
+        p_call p_is_init_r [map;M.pointer_val l;size]
+
+
+    let set_init ty loc ~length chunk ~current : term =
+      let l,r = localized "init atom" loc in
+      match R.kind r, chunk with
+      | Garbled, M c -> M.set_init ty l ~length c ~current
+      | Garbled, R _ -> assert false
+      | Single _, _ -> e_true
+      | Many _ , _ ->
+        let size = e_mul (M.sizeof ty) length in
+        e_fun f_set_init [current;M.pointer_val l;size]
 
     (* ---------------------------------------------------------------------- *)
     (* --- Footprints                                                     --- *)
     (* ---------------------------------------------------------------------- *)
 
-    let rec value_footprint ty loc = match loc with
-      | Null -> Sigma.empty
-      | Raw { repr } ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.value_footprint"
-            ~effect:"Loc is Raw"
-            "value_footprint(Raw %a : %a)"
-            M.pretty repr Ctypes.pp_object ty
-        in
-        let model = M.value_footprint ty repr in
-        Sigma.to_domain Tuple.{ model ; region = RegionSigma.empty }
-      | Loc { repr ; region } ->
-        match R.kind region, ty with
-        | Garbled, (C_int _ | C_float _ | C_pointer _) ->
-          let model = M.value_footprint ty repr in
-          Sigma.to_domain Tuple.{ model ; region = RegionSigma.empty }
-        | (Many (Int   _) | Single (Int   _)), C_int _
-        | (Many (Float _) | Single (Float _)), C_float _
-        | (Many (Ptr    ) | Single (Ptr    )), C_pointer _->
-          Heap.Set.singleton (R (B.CVal region))
-        | (Many _ | Single _) as k, (C_int _ | C_float _ | C_pointer _) ->
-          let _ = Warning.emit ~severe:false
-              ~source:"MemRegion.Region.value_footprint"
-              ~effect:"Type is not the same in chunk and in argument"
-              "value_footprint(%a : %a in %a : %a)"
-              M.pretty repr Ctypes.pp_object ty R.pretty region pp_kind k
-          in Heap.Set.singleton @@ R (B.CVal region)
-        | _, C_comp { cfields } ->
-          let none = Heap.Set.empty in
-          let f_fold acc fd =
-            Heap.Set.union acc
-            @@ value_footprint (Ctypes.object_of fd.ftype)
-            @@ field loc fd
-          in let some l_fields =
-               List.fold_left f_fold Heap.Set.empty l_fields
-          in Option.fold ~none ~some cfields
-        | _, C_array { arr_element } ->
-          let ty = object_of arr_element in
-          value_footprint ty (shift loc ty e_zero)
-
-    let rec init_footprint ty loc = match loc with
-      | Null -> Sigma.empty
-      | Raw { repr } ->
-        let _ = Warning.emit ~severe:false
-            ~source:"MemRegion.Region.init_footprint"
-            ~effect:"Loc is Raw"
-            "init_footprint(Raw %a : %a)"
-            M.pretty repr Ctypes.pp_object ty
-        in let model = M.init_footprint ty repr in
-        Sigma.to_domain Tuple.{ model ; region = RegionSigma.empty }
-      | Loc { repr ; region } ->
-        match R.kind region, ty with
-        | Garbled, (C_int _ | C_float _ | C_pointer _) ->
-          let model =  M.init_footprint ty repr in
-          Sigma.to_domain Tuple.{ model ; region = RegionSigma.empty }
-        | (Many (Int   _) | Single (Int   _)), C_int _
-        | (Many (Float _) | Single (Float _)), C_float _
-        | (Many (Ptr    ) | Single (Ptr    )), C_pointer _->
-          Heap.Set.singleton @@ R (B.CInit region)
-        | (Many _ | Single _) as k, (C_int _ | C_float _ | C_pointer _) ->
-          let _ = Warning.emit ~severe:false
-              ~source:"MemRegion.Region.init_footprint"
-              ~effect:"Type is not the same in chunk and in argument"
-              "init_footprint(%a : %a in %a : %a)"
-              M.pretty repr Ctypes.pp_object ty R.pretty region pp_kind k
-          in Heap.Set.singleton @@ R (B.CInit region)
-        | _, C_comp { cfields } ->
-          let none = Heap.Set.empty in
-          let f_fold acc fd =
-            Heap.Set.union acc
-            @@ init_footprint (Ctypes.object_of fd.ftype)
-            @@ field loc fd
-          in let some l_fields = List.fold_left f_fold Heap.Set.empty l_fields
-          in Option.fold ~none ~some cfields
-        | _, C_array { arr_element } ->
-          let ty = object_of arr_element in
-          init_footprint ty (shift loc ty e_zero)
+    let mfootprint ~value obj l =
+      if value
+      then M.value_footprint obj l
+      else M.init_footprint obj l
+
+    let rec footprint ~value obj loc = match loc with
+      | Null  -> Sigma.mdomain @@ mfootprint ~value obj M.null
+      | Raw l -> Sigma.mdomain @@ mfootprint ~value obj l
+      | Loc(l,r) ->
+        match obj with
+        | C_comp { cfields = None} -> Domain.empty
+        | C_comp { cfields = Some fds } ->
+          List.fold_left
+            (fun dom fd ->
+               let obj = Ctypes.object_of fd.ftype in
+               let loc = field loc fd in
+               Domain.union dom (footprint ~value obj loc)
+            ) Domain.empty fds
+        | C_array { arr_element = elt } ->
+          let obj = object_of elt in
+          footprint ~value obj (shift loc obj e_zero)
+        | C_int _ | C_float _ | C_pointer _ ->
+          match R.kind r with
+          | Garbled ->
+            Sigma.mdomain @@ mfootprint ~value obj l
+          | Single p ->
+            let mu = if value then RChunk.Value p else ValInit in
+            Sigma.rdomain @@ RHeap.Set.singleton { mu ; region = r }
+          | Many p ->
+            let mu = if value then RChunk.Array p else ArrInit in
+            Sigma.rdomain @@ RHeap.Set.singleton { mu ; region = r }
+
+    let value_footprint = footprint ~value:true
+    let init_footprint = footprint ~value:false
 
   end
 
-  type loc = Region.loc
-  type domain = Sigma.domain
-  type chunk = Chunk.t
+  type loc = Loader.loc
   type segment = loc rloc
 
-
-
-  (***************************************************************************)
-  module LOADER = MemLoader.Make(Region)
-  (*****************************************************************************)
+  open Loader
+  module LOADER = MemLoader.Make(Loader)
 
   let load = LOADER.load
   let load_init = LOADER.load_init
@@ -806,34 +598,13 @@ struct
   let copied_init = LOADER.copied_init
   let initialized = LOADER.initialized
   let domain = LOADER.domain
-
-  let assigned seq ty sloc = match sloc with
-    | Sloc (Region.Null) | Sarray (Region.Null,_,_)
-    | Srange (Region.Null,_,_,_) | Sdescr (_,Region.Null,_) ->
-      LOADER.assigned seq ty sloc
-    | Sloc (Region.Raw _) | Sarray (Region.Raw _,_,_)
-    | Srange (Region.Raw _,_,_,_) | Sdescr (_,Region.Raw _,_) ->
-      LOADER.assigned seq ty sloc
-    | _ ->
-      (* Maintain always initialized values initialized *)
-      let region = match sloc with
-        | Sloc (Region.Loc loc) | Sarray (Region.Loc loc, _, _)
-        | Srange (Region.Loc loc, _, _, _)
-        | Sdescr (_, Region.Loc loc, _) -> loc.region
-        | Sloc (Region.Null|Region.Raw _)
-        | Sarray ((Region.Null|Region.Raw _),_,_)
-        | Srange ((Region.Null|Region.Raw _),_,_,_)
-        | Sdescr (_,(Region.Null|Region.Raw _),_) -> assert false
-      in
-      Assert (MemMemory.cinits
-              @@ Sigma.value seq.post @@ R (B.CInit region)) ::
-      LOADER.assigned seq ty sloc
+  let assigned = LOADER.assigned
 
   (* {2 Reversing the Model} *)
 
   type state = M.state
 
-  let state sigma = M.state sigma.Tuple.model
+  let state sigma = M.state (fst sigma)
 
   let lookup s e = M.lookup s e
 
@@ -843,300 +614,104 @@ struct
 
   let iter = M.iter
 
-  let pretty fmt = function
-    | Region.Null -> Format.fprintf fmt "NULL"
-    | Region.Raw { repr } -> Format.fprintf fmt "{ Raw %a }" M.pretty repr
-    | Region.Loc { repr ; region } ->
-      Format.fprintf fmt "{ %a in %a }"
-        M.pretty repr R.pretty region
-
+  let pretty fmt (l: loc) =
+    match l with
+    | Null -> M.pretty fmt M.null
+    | Raw l -> M.pretty fmt l
+    | Loc (l,r) -> Format.fprintf fmt "%a@%a" M.pretty l R.Type.pretty r
 
   (* {2 Memory Model API} *)
 
-  let vars = function
-    | Region.Null -> Vars.empty
-    | Region.Raw { repr } | Region.Loc { repr } -> M.vars repr
-  (* Return the logic variables from which the given location depend on. *)
-
-  let occurs var = function
-    | Region.Null -> false
-    | Region.Raw {repr } | Region.Loc { repr } -> M.occurs var repr
-  (* Test if a location depend on a given logic variable *)
-
-  let null = Region.Null
-  (* Return the location of the null pointer *)
-
-  let literal ~eid:eid name =
-    let repr = M.literal ~eid name in
-    match R.literal ~eid name with
-    | None -> Region.Raw { repr }
-    | Some region -> Region.Loc { repr ; region }
-  (* Return the memory location of a constant string,
-      the id is a unique identifier. *)
-
-  let cvar var =
-    match R.cvar var with
-    | None ->
-      let _ = Warning.emit ~severe:false ~source:"MemRegion.cvar"
-          ~effect:"No region for this var" "%a"
-          Printer.pp_varinfo var
-      in Region.Raw { repr = M.cvar var }
-    | Some region -> Region.Loc { repr = M.cvar var ; region }
-  (* Return the location of a C variable. *)
-
-  let pointer_loc term =
-    if QED.equal term @@ M.pointer_val M.null
-    then Region.Null
-    else let repr = M.pointer_loc term in
-      match R.pointer_loc () with
-      | None -> Region.Raw { repr }
-      | Some region -> Region.Loc { repr ; region }
-  (* Interpret an address value (a pointer) as an abstract location.
-      Might fail on memory models not supporting pointers. *)
-
-  let pointer_val = function
-    | Region.Null -> M.pointer_val M.null
-    | Region.Raw { repr } ->
-      let _ = Warning.emit ~severe:false ~source:"MemRegion.pointer_val"
-          ~effect:"No region for this loc" "%a" M.pretty repr
-      in M.pointer_val repr
-    | Region.Loc { repr } -> M.pointer_val repr
-  (* Return the adress value (a pointer) of an abstract location.
-      Might fail on memory models not capable of representing pointers. *)
-
-  let field loc fieldinfo = match loc with
-    | Region.Null ->
-      let _ = Warning.emit ~severe:false ~source:"MemRegion.field"
-          ~effect:"Loc is NULL"
-          "NULL.(%a)" Printer.pp_field fieldinfo
-      in Region.Null
-    | Region.Raw { repr } ->
-      let _ = Warning.emit ~severe:false ~source:"MemRegion.field"
-          ~effect:"Loc is Raw"
-          "(%a).(%a)" M.pretty repr Printer.pp_field fieldinfo
-      in Region.Raw { repr = M.field repr fieldinfo }
-    | Region.Loc { repr ; region } ->
-      match R.field region fieldinfo with
-      | None ->
-        let _ = Warning.emit ~severe:false ~source:"MemRegion.field"
-            ~effect:"No region for this field"
-            "(%a in %a).(%a in no region)"
-            M.pretty repr R.pretty region Printer.pp_field fieldinfo
-        in Region.Raw { repr = M.field repr fieldinfo }
-      | Some region -> Region.Loc { repr = M.field repr fieldinfo ; region }
-  (* Return the memory location obtained by field access from a given
-      memory location. *)
-
-  let shift loc ty term = match loc with
-    | Region.Null ->
-      let _ = Warning.emit ~severe:false ~source:"MemRegion.shift"
-          ~effect:"Loc is NULL"
-          "NULL.[%a : %a]" QED.pretty term Ctypes.pp_object ty
-      in Region.Null
-    | Region.Raw { repr } ->
-      let _ = Warning.emit ~severe:false ~source:"MemRegion.shift"
-          ~effect:"Loc is Raw"
-          "(%a).[%a : %a]"
-          M.pretty repr QED.pretty term Ctypes.pp_object ty
-      in Region.Raw { repr = M.shift repr ty term }
-    | Region.Loc { repr ; region } ->
-      match R.shift region ty term with
-      | None ->
-        let _ = Warning.emit ~severe:false ~source:"MemRegion.shift"
-            ~effect:"Loc is Raw"
-            "(%a in %a).[%a : %a] in no region"
-            M.pretty repr R.pretty region QED.pretty term Ctypes.pp_object ty
-        in Region.Raw { repr = M.shift repr ty term }
-      | Some region -> Region.Loc { repr = M.shift repr ty term ; region }
-  (* Return the memory location obtained by array access at an index
-      represented by the given {!term}. The element of the array are of
-      the given {!c_object} type. *)
-
-  let base_addr  = function
-    | Region.Null -> Region.Null
-    | Region.Raw { repr } ->
-      let _ = Warning.emit ~severe:false ~source:"MemRegion.base_addr"
-          ~effect:"Loc is Raw" "base_addr(%a)" M.pretty repr
-      in Region.Raw { repr = M.base_addr repr }
-    | Region.Loc { repr ; region } ->
-      Region.Loc { repr = M.base_addr repr ; region = R.base_addr region }
-  (* Return the memory location of the base address of a given memory
-      location. *)
-
-  let base_offset = function
-    | Region.Null -> M.base_offset M.null
-    | Region.Raw { repr } ->
-      let _ = Warning.emit ~severe:false ~source:"MemRegion.base_offset"
-          ~effect:"Loc is Raw" "base_offset(%a)" M.pretty repr
-      in M.base_offset repr
-    | Region.Loc { repr } -> M.base_offset repr
-  (* Return the offset of the location, in bytes, from its base_addr. *)
-
-  let block_length sigma ty  = function
-    | Region.Null -> M.block_length sigma.Tuple.model ty M.null
-    | Region.Raw { repr } ->
-      let _ = Warning.emit ~severe:false ~source:"MemRegion.block_length"
-          ~effect:"Loc is Raw" "block_length(%a)" M.pretty repr
-      in M.block_length sigma.Tuple.model ty repr
-    | Region.Loc { repr } -> M.block_length sigma.Tuple.model ty repr
-  (*  Returns the length (in bytes) of the allocated block containing
-       the given location. *)
-
-  let cast objs = function
-    | Region.Null -> Region.Null
-    | Region.Raw { repr } ->
-      let _ = Warning.emit ~severe:false ~source:"MemRegion.cast"
-          ~effect:"Loc is NULL" "NULL=%a" M.pretty repr
-      in Region.Raw { repr = M.cast objs repr }
-    | Region.Loc loc -> Region.Loc { loc with repr = M.cast objs loc.repr }
-  (* Cast a memory location into another memory location.
-      For [cast ty loc] the cast is done from [ty.pre] to [ty.post].
-      Might fail on memory models not supporting pointer casts. *)
-
-  let loc_of_int ty term =
-    if QED.equal term @@ M.pointer_val M.null
-    then Region.Null
-    else match R.loc_of_int () with
-      | None -> Region.Raw { repr = M.loc_of_int ty term }
-      | Some region -> Region.Loc { repr = M.loc_of_int ty term ; region }
-
-  let int_of_loc c_int = function
-    | Region.Null -> M.int_of_loc c_int M.null
-    | Region.Raw { repr } ->
-      let _ = Warning.emit ~severe:false ~source:"MemRegion.int_of_loc"
-          ~effect:"Loc is Raw" "NULL=%a" M.pretty repr
-      in M.int_of_loc c_int repr
-    | Region.Loc { repr } -> M.int_of_loc c_int repr
-  (* Cast a memory location into its absolute memory address,
-      given as an integer with the given C-type. *)
-
-  let is_null = function
-    | Region.Null -> p_true
-    | Region.Raw { repr } | Region.Loc { repr } -> M.is_null repr
-  (* Return the formula that check if a given location is null *)
-
-  let get_repr = function
-    | Region.Null -> M.null
-    | Region.Raw { repr } -> repr
-    | Region.Loc { repr } -> repr
-
-  let loc_eq loc_a loc_b = M.loc_eq (get_repr loc_a) (get_repr loc_b)
-  let loc_lt loc_a loc_b = M.loc_lt (get_repr loc_a) (get_repr loc_b)
-  let loc_neq loc_a loc_b =  M.loc_neq (get_repr loc_a) (get_repr loc_b)
-  let loc_leq loc_a loc_b =  M.loc_leq (get_repr loc_a) (get_repr loc_b)
-  (* Memory location comparisons *)
-
-  let loc_diff ty loc_a loc_b =  M.loc_diff ty (get_repr loc_a) (get_repr loc_b)
-  (* Compute the length in bytes between two memory locations *)
-
-  let get_rloc = function
-    | Rloc (ty, Region.Null) -> Rloc (ty, M.null)
-    | Rloc (ty, Region.Raw { repr }) -> Rloc (ty, repr)
-    | Rloc (ty, Region.Loc loc) ->
-      Rloc (ty, loc.repr)
-    | Rrange (Region.Null, ty, inf, sup) ->
-      Rrange (M.null, ty, inf, sup)
-    | Rrange (Region.Raw { repr }, ty, inf, sup) ->
-      Rrange (repr, ty, inf, sup)
-    | Rrange (Region.Loc loc, ty, inf, sup) ->
-      Rrange (loc.repr, ty, inf, sup)
-
-
-  let get_rloc_region = function
-    | Rloc (ty, loc) ->
-      Rloc (ty, (match loc with Region.Null -> M.null
-                              | Region.Raw { repr } | Region.Loc { repr } -> repr)),
-      (match loc with Region.Null | Region.Raw _ -> None
-                    | Region.Loc { region } -> Some region)
-    | Rrange (loc, ty, inf, sup) ->
-      Rrange ((match loc with Region.Null -> M.null
-                            | Region.Raw { repr } | Region.Loc { repr } -> repr), ty, inf, sup),
-      (match loc with Region.Null | Region.Raw _ -> None
-                    | Region.Loc { region } -> Some region)
-
-
-  let valid sigma acs (rloc : loc rloc) =
-    M.valid sigma.Tuple.model acs @@ get_rloc rloc
-  (* Return the formula that tests if a memory state is valid
-      (according to {!acs}) in the given memory state at the given
-      segment.
-  *)
+  let vars l = M.vars @@ loc l
+  let occurs x l = M.occurs x @@ loc l
+  let null = Null
+
+  let literal ~eid:eid str = make (M.literal ~eid str) (R.literal ~eid str)
+
+  let cvar v = make (M.cvar v) (R.cvar v)
+  let field = field
+  let shift = shift
+
+  let pointer_loc t = Raw (M.pointer_loc t)
+  let pointer_val l = M.pointer_val @@ loc l
+  let base_addr l = Raw (M.base_addr @@ loc l)
+  let base_offset l = M.base_offset @@ loc l
+  let block_length sigma obj l = M.block_length (fst sigma) obj @@ loc l
+  let is_null = function Null -> p_true | Raw l | Loc(l,_) -> M.is_null l
+  let loc_of_int obj t = Raw (M.loc_of_int obj t)
+  let int_of_loc iota l = M.int_of_loc iota @@ loc l
+
+  let cast conv l =
+    let l0 = loc l in
+    let r0 = reg l in
+    make (M.cast conv l0) r0
+
+  let loc_eq  a b = M.loc_eq  (loc a) (loc b)
+  let loc_lt  a b = M.loc_lt  (loc a) (loc b)
+  let loc_neq a b = M.loc_neq (loc a) (loc b)
+  let loc_leq a b = M.loc_leq (loc a) (loc b)
+  let loc_diff obj a b = M.loc_diff obj (loc a) (loc b)
+
+  let rloc = function
+    | Rloc(obj, l) -> Rloc (obj, loc l)
+    | Rrange(l, obj, inf, sup) -> Rrange(loc l, obj, inf, sup)
+
+  let rloc_region = function Rloc(_,l) | Rrange(l,_,_,_) -> reg l
+
+  let valid sigma acs r = M.valid (fst sigma) acs @@ rloc r
+  let invalid sigma r = M.invalid (fst sigma) (rloc r)
+
+  let included (a : segment) (b : segment) =
+    let sa = rloc a in
+    let sb = rloc b in
+    match rloc_region a, rloc_region b with
+    | Some ra, Some rb when R.separated ra rb -> p_false
+    | _ -> M.included sa sb
+
+  let separated (a : segment) (b : segment) =
+    let sa = rloc a in
+    let sb = rloc b in
+    match rloc_region a, rloc_region b with
+    | Some ra, Some rb when R.separated ra rb -> p_true
+    | _ -> M.separated sa sb
+
+  let alloc sigma vars =
+    if vars = [] then sigma else
+      let m,r = sigma in M.alloc m vars, r
+
+  let scope seq scope vars = M.scope (mseq seq) scope vars
+
+  let global sigma p = M.global (fst sigma) p
 
   let frame sigma =
-    let region_frame sigma = function
-      | B.CInit region ->
-        MemMemory.cinits @@ Sigma.value sigma @@ Chunk.CRegion (B.CInit region)
-      | B.CVal region | B.CGhost region ->  match R.kind region with
-        | Many Ptr | Single Ptr ->
-          MemMemory.framed @@ Sigma.value sigma @@ Chunk.CRegion (B.CVal region)
-        | Garbled | Many (Int _ | Float _)
-        | Single (Int _ | Float _) -> p_true
-    in
-    RegionSigma.Chunk.Set.fold
-      (fun c l -> region_frame sigma c :: l)
-      (RegionSigma.domain sigma.region)
-    @@ M.frame sigma.model
-  (* Assert the memory is a proper heap state preceeding the function
-      entry point. *)
-
-  let alloc (sigma:sigma) vars =
-    if vars = [] then sigma
-    else { sigma with model = M.alloc sigma.model vars }
-  (* Allocates new chunk for the validity of variables. *)
-
-  let invalid (sigma:sigma) rloc = M.invalid sigma.model (get_rloc rloc)
-  (* Returns the formula that tests if the entire memory is invalid
-      for write access. *)
-
-  let scope (s:sigma sequence) scope vars =
-    let m_sigma = { pre = s.pre.model ; post = s.post.model } in
-    M.scope m_sigma scope vars
-  (* Manage the scope of variables.  Returns the updated memory model
-      and hypotheses modeling the new validity-scope of the variables. *)
-
-  let global (sigma:sigma) p = M.global sigma.model p
-  (* Given a pointer value [p], assumes this pointer [p] (when valid)
-      is allocated outside the function frame under analysis. This means
-      separated from the formals and locals of the function. *)
-
-  let included (rloc1 : segment) (rloc2 : segment) =
-    let (rl1, region1) = get_rloc_region rloc1 in
-    let (rl2, region2) = get_rloc_region rloc2 in
-    match region1, region2 with
-    | None, _ -> M.included rl1 rl2
-    | _, None -> p_false
-    | Some region1, Some region2 ->
-      if R.separated region1 region2 then p_false
-      else M.included rl1 rl2
-
-  let separated (rloc1 : segment) (rloc2 : segment) =
-    let (rl1, region1) = get_rloc_region rloc1 in
-    let (rl2, region2) = get_rloc_region rloc2 in
-    match region1, region2 with
-    | None, _ | _, None -> M.separated rl1 rl2
-    | Some region1, Some region2 ->
-      if R.separated region1 region2 then p_true
-      else M.separated rl1 rl2
-
-  let is_well_formed_chunk sigma chunk = match chunk with
-    | M _ | Chunk.CRegion (B.CInit _)
-    | Chunk.CRegion (B.CGhost _) -> p_true
-    | Chunk.CRegion (B.CVal region) -> match R.kind region with
-      | Garbled -> p_true
-      | Many (Float _ | Ptr )
-      | Single (Float _ | Ptr ) -> p_true
-      | Many (Int cint) ->
-        let l = Lang.freshvar ~basename:"l" (Lang.t_addr()) in
-        let m = Sigma.value sigma chunk in
-        p_forall [l] (Cint.range cint (F.e_get m (e_var l)))
-      | Single (Int cint) ->
-        Cint.range cint @@ Sigma.value sigma chunk
+    let pool = ref @@ M.frame (fst sigma) in
+    let assume p = pool := p :: !pool in
+    RSigma.iter
+      (fun c m ->
+         let open RChunk in
+         match c.mu with
+         | ValInit -> ()
+         | ArrInit -> assume @@ MemMemory.cinits (e_var m)
+         | Value Ptr -> assume @@ global sigma (e_var m)
+         | Array Ptr -> assume @@ MemMemory.framed (e_var m)
+         | Value (Int _ | Float _) | Array (Int _ | Float _) -> ()
+      ) (snd sigma) ;
+    !pool
 
   let is_well_formed sigma =
-    p_conj @@
-    Sigma.Chunk.Set.fold
-      (fun c l -> is_well_formed_chunk sigma c :: l)
-      (Sigma.domain sigma)
-      [M.is_well_formed sigma.model]
+    let pool = ref @@ [M.is_well_formed (fst sigma)] in
+    let assume p = pool := p :: !pool in
+    RSigma.iter
+      (fun c m ->
+         let open RChunk in
+         match c.mu with
+         | ValInit | ArrInit -> ()
+         | Value (Int iota) -> assume @@ Cint.range iota (e_var m)
+         | Array (Int iota) ->
+
+           assume @@ Cint.range iota (e_var m)
+         | Value (Float _ | Ptr) | Array (Float _ | Ptr) -> ()
+      ) (snd sigma) ;
+    p_conj !pool
 
 end

src/plugins/wp/MemRegion.mli

@@ -37,38 +37,24 @@ module type RegionProxy =
 sig
   type region
   module Type : Sigs.Type with type t = region
-
+  val id : region -> int
+  val of_id : int -> region option
   val kind : region -> kind
-
-  val null : unit -> region
-
-  val tau_of_region : region -> tau
-  val points_to : region -> region option
-
-  val separated : region -> region -> bool
-  val included : region -> region -> bool
-
   val cvar : varinfo -> region option
   val field : region -> fieldinfo -> region option
-  val shift : region -> c_object -> term -> region option
-  val base_addr : region -> region
-
+  val shift : region -> c_object -> region option
+  val points_to : region -> region option
   val literal : eid:int -> Cstring.cst -> region option
-  val pointer_loc : unit -> region option
-  val loc_of_int : unit -> region option
-
-  val id : region -> int
-  val region_of_id : int -> region option
-
+  val separated : region -> region -> bool
+  val included : region -> region -> bool
 end
 
 module type ModelWithLoader =
 sig
   include Sigs.Model
-
   val sizeof : c_object -> term
-  val last : sigma -> c_object -> loc -> term
 
+  val last : sigma -> c_object -> loc -> term
   val frames : c_object -> loc -> chunk -> frame list
 
   val havoc : c_object -> loc -> length:term -> chunk -> fresh:term -> current:term -> term

src/plugins/wp/RegionAnalysis.ml

@@ -20,24 +20,20 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Cil_types
-open Ctypes
-open Lang.F
+(* -------------------------------------------------------------------------- *)
+(* --- Proxy to Region Analysis for Region Model                          --- *)
+(* -------------------------------------------------------------------------- *)
 
 type region = Region.node
 
-let get_map () = match WpContext.get_scope () with
-  | WpContext.Kf f   -> Region.map f
-  | WpContext.Global -> Wp_parameters.not_yet_implemented "[WP/RegionAnalysis.ml] get_map: No global region analysis yet"
-
-let null () : region =
-  Warning.emit ~severe:false ~source:"Region Memory Model"
-    ~effect:"Create null pointer value" "NULL" ;
-  Wp_parameters.not_yet_implemented "[WP/RegionAnalysis.ml] null: cannot create null region"
+let get_map () =
+  match WpContext.get_scope () with
+  | Kf kf -> Region.map kf
+  | Global -> Wp_parameters.not_yet_implemented "[region] logic context"
 
 let id region = Region.uid (get_map ()) region
 
-let region_of_id id =
+let of_id id =
   try Some (Region.find (get_map ()) id)
   with Not_found -> None
 
@@ -82,50 +78,20 @@ module Kind = WpContext.Generator(Type)
     end)
 
 let kind = Kind.get
-
-let tau_of_region region : tau =
-  match types region with
-  | [ ty ] -> Lang.tau_of_ctype ty
-  | _ -> (*TODO*) assert false
-
 let points_to region = Region.points_to (get_map ()) region
-
 let separated r1 r2 = Region.separated (get_map ()) r1 r2
-
 let included r1 r2 = Region.included (get_map ()) r1 r2
 
 let cvar var =
   try Some (Region.cvar (get_map ()) var)
-  with Not_found ->
-    Warning.emit ~severe:false ~source:"RegionAnalysis.cvar"
-      ~effect:"No region found for C variable" "%a" Printer.pp_varinfo var ;
-    None
+  with Not_found -> None
 
-let field (region: region) (fd: fieldinfo) : region option =
-  try Some (Region.field (get_map ()) region fd)
-  with Not_found ->
-    Warning.emit ~severe:false
-      ~source:"RegionAnalysis.field"
-      ~effect:"No region found for field"
-      "No region for field %a from region %a"
-      Printer.pp_field fd Type.pretty region;
-    None
+let field r fd =
+  try Some (Region.field (get_map ()) r fd)
+  with Not_found -> None
 
-let shift region ty offset =
-  let rec aux = function
-    | [] ->
-      Warning.emit ~severe:false
-        ~source:"RegionAnalysis.shift"
-        ~effect:"No region found"
-        "No region for shift %a from region %a"
-        QED.pretty offset Type.pretty region;
-      None
-    | typ :: rest ->
-      try Some (Region.index (get_map ()) region typ)
-      with Not_found -> aux rest
-  in aux @@ Ctypes.object_to ty
+let shift r obj =
+  try Some (Region.index (get_map ()) r (Ctypes.object_to obj))
+  with Not_found -> None
 
-let base_addr _ = assert false
-let literal ~eid _ = ignore eid ; assert false
-let pointer_loc () = assert false
-let loc_of_int () = assert false
+let literal ~eid _ = ignore eid ; None

src/plugins/wp/ctypes.ml

@@ -389,26 +389,30 @@ let () =
 (* --- Revert c_object to typ                                             --- *)
 (* -------------------------------------------------------------------------- *)
 
-let ikinds_of cint =
-  let all_ikind = [IBool;IChar;ISChar;IUChar;IInt;IUInt;IShort;IUShort;ILong;IULong;ILongLong;IULongLong] in
-  List.filter (fun ikind -> 0 == compare_c_int cint @@ c_int ikind) all_ikind
-
-let fkinds_of cfloat =
-  let all_fkind = [FFloat;FDouble;FLongDouble] in
-  List.filter (fun fkind -> 0 == compare_c_float cfloat @@ c_float fkind) all_fkind
+let ikinds = [
+  IBool;IChar;
+  ISChar;IUChar;
+  IInt;IUInt;
+  IShort;IUShort;
+  ILong;IULong;
+  ILongLong;IULongLong
+]
+let fkinds = [FFloat;FDouble;FLongDouble]
+
+let to_ikind iota =
+  List.find (fun ik -> c_int ik = iota) ikinds
+
+let to_fkind flt =
+  List.find (fun fk -> c_float fk = flt) fkinds
 
 let object_to = function
-  | C_int cint as ty when equal ty (object_of (TVoid [])) -> (TVoid []) :: (List.map (fun ik -> TInt (ik,[])) @@ ikinds_of cint)
-  | C_int cint -> List.map (fun ik -> TInt (ik,[])) @@ ikinds_of cint
-  | C_float cfloat -> List.map (fun fk -> TFloat (fk,[])) @@ fkinds_of cfloat
-  | C_pointer (TVoid [] as typ) -> [ TBuiltin_va_list [] ; TPtr (typ,[]) ]
-  | C_pointer typ -> [ TPtr (typ,[]) ]
-  | C_comp comp -> [ TComp (comp,[]) ]
-  | C_array arr ->
-    match arr.arr_flat with
-    | None -> [ TArray (arr.arr_element, None, []) ]
-    | Some _e -> [ TArray (arr.arr_element, None (* Some (Cil.integer ~loc:Cil_builder.loc @@ Int64.of_int e) *), [])]
-
+  | C_int i -> TInt(to_ikind i,[])
+  | C_float f -> TFloat(to_fkind f,[])
+  | C_pointer typ -> TPtr(typ,[])
+  | C_comp comp -> TComp(comp,[])
+  | C_array { arr_element = elt ; arr_flat = None } -> TArray(elt,None,[])
+  | C_array { arr_element = elt ; arr_flat = Some { arr_size = size } } ->
+    TArray(elt,Some (Cil.integer ~loc:Location.unknown size),[])
 
 (* -------------------------------------------------------------------------- *)
 (* --- Accessor Utilities                                                 --- *)

src/plugins/wp/ctypes.mli

@@ -97,8 +97,14 @@ val c_int    : ikind -> c_int
 val c_float  : fkind -> c_float
 (** Conforms to {!Machine.theMachine} *)
 
+val to_ikind : c_int -> ikind
+(** @raises Not_found *)
+
+val to_fkind : c_float -> fkind
+(** @raises Not_found *)
+
 val object_of : typ -> c_object
-val object_to : c_object -> typ list
+val object_to : c_object -> typ
 
 val is_pointer : c_object -> bool
 

src/plugins/wp/tests/wp_region/oracle/swap.res.oracle

@@ -11,15 +11,15 @@
 ------------------------------------------------------------
 
 Goal Post-condition (file swap.i, line 20) in 'swap_aliased':
-Let a = ValueChunk_2[global(P_b_33)].
-Let a_1 = ValueChunk_1[global(P_a_32)].
-Let x = ValueChunk_0[a_1].
-Let x_1 = ValueChunk_0[a].
-Let x_2 = ValueChunk_0[a_1 <- x_1][a <- x][a_1].
+Let a = Mptr_1[global(P_b_33)].
+Let a_1 = Mptr_0[global(P_a_32)].
+Let x = Msint32_0[a_1].
+Let x_1 = Msint32_0[a].
+Let x_2 = Msint32_0[a_1 <- x_1][a <- x][a_1].
 Assume {
   Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2).
   (* Heap *)
-  Type: linked(alloc_0) /\ framed(ValueChunk_1) /\ framed(ValueChunk_2).
+  Type: linked(alloc_0) /\ framed(Mptr_0) /\ framed(Mptr_1).
   (* Pre-condition *)
   Have: valid_rw(alloc_0, a_1, 4).
   (* Pre-condition *)