[wp/region] refactor MemRegion

src/plugins/region/Region.ml

@@ -49,3 +49,4 @@ 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,3 +125,7 @@ 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,6 +567,9 @@ 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,6 +96,7 @@ 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.mli

@@ -36,15 +36,12 @@ val pp_kind : Format.formatter -> kind -> unit
 module type RegionProxy =
 sig
   type region
-  val null : unit -> region
-
-  val hash : region -> int
-  val equal : region -> region -> bool
-  val compare : region -> region -> int
-  val pretty : Format.formatter -> region -> unit
+  module Type : Sigs.Type with type t = region
 
   val kind : region -> kind
 
+  val null : unit -> region
+
   val tau_of_region : region -> tau
   val points_to : region -> region option
 
@@ -60,7 +57,7 @@ sig
   val pointer_loc : unit -> region option
   val loc_of_int : unit -> region option
 
-  val id_of_region : region -> int
+  val id : region -> int
   val region_of_id : int -> region option
 
 end

src/plugins/wp/RegionAnalysis.ml

@@ -35,19 +35,20 @@ let null () : region =
     ~effect:"Create null pointer value" "NULL" ;
   Wp_parameters.not_yet_implemented "[WP/RegionAnalysis.ml] null: cannot create null region"
 
-let id_of_region region = Region.uid (get_map ()) region
+let id region = Region.uid (get_map ()) region
 
 let region_of_id id =
   try Some (Region.find (get_map ()) id)
   with Not_found -> None
 
-let hash = Region.id
-
-let equal r1 r2 = (Region.id r1 = Region.id r2)
-
-let compare r1 r2 = Int.compare (Region.id r1) (Region.id r2)
-
-let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.id r
+module Type =
+struct
+  type t = region
+  let hash = Region.id
+  let equal r1 r2 = (Region.id r1 = Region.id r2)
+  let compare r1 r2 = Int.compare (Region.id r1) (Region.id r2)
+  let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.id r
+end
 
 let types r =
   let module Tset = Cil_datatype.Typ.Set in
@@ -60,13 +61,7 @@ let types r =
   Tset.elements !pool
 
 (* Keeping track of the decision to apply which memory model to each region *)
-module Kind = WpContext.Generator
-    (struct
-      (* Key : WPContext.Key *)
-      type t = region
-      let compare = compare
-      let pretty = pretty
-    end)
+module Kind = WpContext.Generator(Type)
     (struct
       (* Data : WpContext.Data with type key = Key.t *)
       type key = region
@@ -113,7 +108,7 @@ let field (region: region) (fd: fieldinfo) : region option =
       ~source:"RegionAnalysis.field"
       ~effect:"No region found for field"
       "No region for field %a from region %a"
-      Printer.pp_field fd pretty region;
+      Printer.pp_field fd Type.pretty region;
     None
 
 let shift region ty offset =
@@ -123,7 +118,7 @@ let shift region ty offset =
         ~source:"RegionAnalysis.shift"
         ~effect:"No region found"
         "No region for shift %a from region %a"
-        QED.pretty offset pretty region;
+        QED.pretty offset Type.pretty region;
       None
     | typ :: rest ->
       try Some (Region.index (get_map ()) region typ)

src/plugins/wp/Sigs.ml

@@ -129,6 +129,15 @@ type update = Mstore of s_lval * term
 (** {1 Memory Models} *)
 (* -------------------------------------------------------------------------- *)
 
+module type Type =
+sig
+  type t
+  val hash : t -> int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+  val pretty : Format.formatter -> t -> unit
+end
+
 (** Memory Chunks.
 
     The concrete memory is partionned into a vector of abstract data.
@@ -148,10 +157,7 @@ sig
   val self : string
   (** Chunk names, for pretty-printing. *)
 
-  val hash : t -> int
-  val equal : t -> t -> bool
-  val compare : t -> t -> int
-  val pretty : Format.formatter -> t -> unit
+  include Type with type t := t
 
   val tau_of_chunk : t -> tau
   (** The type of data hold in a chunk. *)