From e224af9fcbadaac4b2ee0b2c3e4dab1fbe23ad33 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 7 Oct 2024 16:44:50 +0200
Subject: [PATCH] [wp/region] complete refactor
---
src/plugins/region/Region.ml | 1 -
src/plugins/region/Region.mli | 4 -
src/plugins/region/memory.ml | 3 -
src/plugins/region/memory.mli | 1 -
src/plugins/wp/MemRegion.ml | 963 +++++-------------
src/plugins/wp/MemRegion.mli | 28 +-
src/plugins/wp/RegionAnalysis.ml | 66 +-
src/plugins/wp/ctypes.ml | 40 +-
src/plugins/wp/ctypes.mli | 8 +-
.../wp/tests/wp_region/oracle/swap.res.oracle | 12 +-
10 files changed, 327 insertions(+), 799 deletions(-)
diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index c2b4a6113cf..4c912d7a61b 100644
--- a/src/plugins/region/Region.ml
+++ b/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
diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli
index 57ddcabf05e..baedc6b4030 100644
--- a/src/plugins/region/Region.mli
+++ b/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
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index abd0a00c3e1..048e7ed6ee1 100644
--- a/src/plugins/region/memory.ml
+++ b/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
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index 6fa835ff50c..4e8f5c4da4b 100644
--- a/src/plugins/region/memory.mli
+++ b/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
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index b6d2a88e828..025333ff770 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/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
diff --git a/src/plugins/wp/MemRegion.mli b/src/plugins/wp/MemRegion.mli
index 248a6f45090..8bffdeab36c 100644
--- a/src/plugins/wp/MemRegion.mli
+++ b/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
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index acfa3d87b8a..53cbfdca051 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/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
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 1ea4a065fff..cbae54d6457 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/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 --- *)
diff --git a/src/plugins/wp/ctypes.mli b/src/plugins/wp/ctypes.mli
index 96664cfbe06..060c3e9ffa0 100644
--- a/src/plugins/wp/ctypes.mli
+++ b/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
diff --git a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
index e17459e0f2a..2a9c0dd0929 100644
--- a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
+++ b/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 *)
--
GitLab