diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index ebb94ce0f2ebec61ecac0b5e194eb7a3c887aa5c..2b5fa1ebb620477dc03035afb7fe355a8445ce90 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -244,7 +244,7 @@ module Comp_Region =
MakeCompiler
(MemVar.Make
(MemVar.Static)
- (MemRegion.MemMake(RegionAnalysis.R)(MemBytes)))
+ (MemRegion.Make(RegionAnalysis.R)(MemBytes)))
let compiler mheap mvar : (module Sigs.Compiler) =
diff --git a/src/plugins/wp/MemBytes.ml b/src/plugins/wp/MemBytes.ml
index 5e63f1f5ed5bebdd460ffd8e05f4babd1c2d84da..d1a6abbfdbe41121f655f3a322e9c10f384e0d60 100644
--- a/src/plugins/wp/MemBytes.ml
+++ b/src/plugins/wp/MemBytes.ml
@@ -28,7 +28,8 @@ module Logic = Qed.Logic
(* Why3 symbols *)
-module Why3 = struct
+module Why3 =
+struct
let library = "membytes"
let t_vblock = Qed.Logic.Array (Qed.Logic.Int, Qed.Logic.Int)
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 1304f3efd6b33cb9ebd118eb200541652778a7e4..bf90ba1869515790d5b56fa5271ddd8180dc6481 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -33,7 +33,6 @@ open MemMemory
module L = Qed.Logic
-
module type ModelLoader = sig
include Sigs.Model
@@ -63,9 +62,6 @@ module type ModelLoader = sig
val init_footprint : c_object -> loc -> Sigma.domain
end
-
-
-(*
module Make (R:RegionAnalysis.API) (M:ModelLoader) (* : Sigs.Model *) =
struct
@@ -103,1080 +99,6 @@ struct
============================> TODO <======================================
*)
- module Chunk =
- struct
- type t =
- | CModel of M.chunk
- | CVal of R.region
- | CInit of R.region
-
- let self = "MemRegion.Make.Chunk"
- (* Chunk names, for pretty-printing. *)
-
- let hash = function
- | CModel c -> M.Chunk.hash c
- | CVal r -> 0x1000 * (R.hash r)
- | CInit r -> 0x1000000 * (R.hash r)
-
- let equal ca cb = match ca, cb with
- | CModel c1, CModel c2 -> M.Chunk.equal c1 c2
- | CVal r1, CVal r2 -> R.equal r1 r2
- | CInit r1, CInit r2 -> R.equal r1 r2
- | _, _ -> false
-
- let compare c1 c2 = (hash c1) - (hash c2)
-
- let pretty fmt = function
- | CModel c -> Format.fprintf fmt "RegionModel.%a" M.Chunk.pretty c
- | CVal r -> Format.fprintf fmt "RegionVal.%a" R.pretty r
- | CInit r -> Format.fprintf fmt "RegionInit.%a" R.pretty r
-
-
- let tau_of_primitive = function
- | R.Int _ -> L.Int
- | R.Float c_float -> Cfloat.tau_of_float c_float
- | R.Ptr -> MemAddr.t_addr
-
- let tau_of_chunk = function
- | CModel c -> M.Chunk.tau_of_chunk c
- | CVal r ->
- begin match R.kind r with
- | R.Single p -> tau_of_primitive p
- | R.Many p -> L.Array(MemAddr.t_addr, tau_of_primitive p)
- | R.Garbled -> assert false
- end
- (* | CAlloc r -> t_malloc *)
- | CInit r ->
- begin match R.kind r with
- | R.Single _ -> t_bool
- | R.Many _ -> t_init
- | R.Garbled -> assert false
- end
-
- let basename_of_chunk = function
- | CModel _ -> "ModelChunk"
- | CVal _ -> "ValueChunk"
- | CInit _ -> "InitChunk"
- (* Used when generating fresh variables for a chunk. *)
-
- let is_framed = function
- | CModel c -> M.Chunk.is_framed c
- | CVal _ | CInit _ -> false
- (* Whether the chunk is local to a function call.
-
- Means the chunk is separated from anyother call side-effects.
- If [true], entails that a function assigning everything can not modify
- the chunk. Only used for optimisation, it would be safe to always
- return [false]. *)
- end
- (* Memory Chunks.
-
- The concrete memory is partionned into a vector of abstract data.
- Each component of the partition is called a {i memory chunk} and
- holds an abstract representation of some part of the memory.
-
- Remark: memory chunks are not required to be independant from each other,
- provided the memory model implementation is consistent with the chosen
- representation. Conversely, a given object might be represented by
- several memory chunks.
-
- *)
-
- (* Chunks Sets and Maps. *)
-
- module ValChunk = struct
- include R
- type t = region
- let self = "chunk_val"
- let tau_of_chunk = tau_of_region
- let basename_of_chunk _ = "ChunkVal"
- let is_framed _ = false
- end
- module InitChunk = struct
- include R
- type t = region
- let self = "chunk_init"
- let tau_of_chunk _ = t_init
- let basename_of_chunk _ = "ChunkInit"
- let is_framed _ = false
- end
-
- module ValHeap = Qed.Collection.Make(ValChunk)
- module ValSigma = Sigma.Make(ValChunk)(ValHeap)
-
- module InitHeap = Qed.Collection.Make(InitChunk)
- module InitSigma = Sigma.Make(InitChunk)(InitHeap)
-
- module Heap = Qed.Collection.Make(Chunk)
-
- module Tuple = struct
- type ('a, 'b, 'c) tuple = {
- model : 'a ;
- value : 'b ;
- init : 'c ;
- }
-
- let create f1 f2 f3 input = {
- model = f1 input ;
- value = f2 input ;
- init = f3 input ;
- }
-
- let iter f1 f2 f3 tuple =
- f1 tuple.model ;
- f2 tuple.value ;
- f3 tuple.init ;
- ()
-
- let iter2 f1 f2 f3 t1 t2 =
- f1 t1.model t2.model ;
- f2 t1.value t2.value ;
- f3 t1.init t2.init ;
- ()
-
- let choose_apply f1 f2 f3 tuple = function
- | Chunk.CModel c -> f1 tuple.model c
- | Chunk.CVal r -> f2 tuple.value r
- | Chunk.CInit r -> f3 tuple.init r
-
- let choose_map f1 f2 f3 tuple = function
- | Chunk.CModel c -> { tuple with model = f1 tuple.model c }
- | Chunk.CVal r -> { tuple with value = f2 tuple.value r }
- | Chunk.CInit r -> { tuple with init = f3 tuple.init r }
-
- let map f1 f2 f3 tuple = {
- model = f1 tuple.model ;
- value = f2 tuple.value ;
- init = f3 tuple.init ;
- }
-
- let map2 f1 f2 f3 t1 t2 = {
- model = f1 t1.model t2.model ;
- value = f2 t1.value t2.value ;
- init = f3 t1.init t2.init ;
- }
-
- let sequence_map f1 f2 f3 seq = {
- model = f1 { pre = seq.pre.model ; post = seq.post.model } ;
- value = f2 { pre = seq.pre.value ; post = seq.post.value } ;
- init = f3 { pre = seq.pre.init ; post = seq.post.init } ;
- }
- end
-
- type sigma = (M.sigma, ValSigma.t, InitSigma.t) Tuple.tuple
-
- module Sigma (*: Sigma *) =
- struct
-
- open Tuple
- type t = sigma
- type chunk = Chunk.t
-
- open Chunk
-
- type domain = Heap.set
-
- type dom = (M.Sigma.domain, ValSigma.domain, InitSigma.domain) Tuple.tuple
-
- (* local *)
- let chunk_split_list l =
- let rec aux acc1 acc2 acc3 = function
- | [] -> { model = List.rev acc1 ; value = List.rev acc2 ; init = List.rev acc3 }
- | CModel c :: rest -> aux (c::acc1) acc2 acc3 rest
- | CVal r :: rest -> aux acc1 (r::acc2) acc3 rest
- | CInit r :: rest -> aux acc1 acc2 (r::acc3) rest
- in aux [] [] [] l
-
- let of_domain (domain:domain) : dom =
- Tuple.map
- M.Sigma.Chunk.Set.of_list
- ValSigma.Chunk.Set.of_list
- InitSigma.Chunk.Set.of_list
- @@ chunk_split_list
- @@ Heap.Set.elements domain
-
- let to_domain (dom:dom) : domain =
- let cmodel = M.Heap.Set.elements dom.model in
- let cvalue = ValSigma.Chunk.Set.elements dom.value in
- let cinit = InitSigma.Chunk.Set.elements dom.init in
- let model = Heap.Set.of_list (List.map (fun c -> CModel c) cmodel) in
- let value = Heap.Set.of_list (List.map (fun r -> CVal r) cvalue) in
- let init = Heap.Set.of_list (List.map (fun r -> CInit r) cinit) in
- Heap.Set.union model @@ Heap.Set.union value init
-
- module Chunk = Heap
-
-
- let create = Tuple.create M.Sigma.create ValSigma.create InitSigma.create
-
- let pretty fmt sigma =
- Format.fprintf fmt "@[{@[%a@];@[%a@];@[%a@]}@]"
- M.Sigma.pretty sigma.model
- ValSigma.pretty sigma.value
- InitSigma.pretty sigma.init
-
- let empty : domain = Heap.Set.empty
-
- let mem = Tuple.choose_apply M.Sigma.mem ValSigma.mem InitSigma.mem
-
- let get = Tuple.choose_apply M.Sigma.get ValSigma.get InitSigma.get
-
- let writes sigma = to_domain @@ Tuple.sequence_map M.Sigma.writes ValSigma.writes InitSigma.writes sigma
-
- let value = Tuple.choose_apply M.Sigma.value ValSigma.value InitSigma.value
-
- let copy = Tuple.map M.Sigma.copy ValSigma.copy InitSigma.copy
-
- let join sigma1 sigma2 =
- let r = Tuple.map2 M.Sigma.join ValSigma.join InitSigma.join sigma1 sigma2 in
- Passive.union r.model @@ Passive.union r.value r.init
-
- let assigned ~pre:sigma1 ~post:sigma2 domain =
- let dom = of_domain domain in
- Bag.concat (M.Sigma.assigned ~pre:sigma1.model ~post:sigma2.model dom.model)
- @@ Bag.concat (ValSigma.assigned ~pre:sigma1.value ~post:sigma2.value dom.value)
- @@ InitSigma.assigned ~pre:sigma1.init ~post:sigma2.init dom.init
-
- let choose = Tuple.map2 M.Sigma.choose ValSigma.choose InitSigma.choose
-
- let merge s1 s2 =
- let (sm, pm1, pm2) = M.Sigma.merge s1.model s2.model in
- let (sv, pv1, pv2) = ValSigma.merge s1.value s2.value in
- let (si, pi1, pi2) = InitSigma.merge s1.init s2.init in
- let s = { model = sm ; value = sv ; init = si } in
- let p1 = Passive.union pm1 @@ Passive.union pv1 pi1 in
- let p2 = Passive.union pm2 @@ Passive.union pv2 pi2 in
- (s,p1,p2)
-
- let merge_list ls = (* TOCHECK *)
- let f (s1,lp) s2 =
- let (s,p1,p2) = merge s1 s2 in
- (s, p1::p2::lp)
- in
- match ls with
- | [] -> (create (), [])
- | [ s ] -> (s, [ Passive.empty ])
- | _ -> List.fold_left f (create (), []) ls
-
- let iter f =
- Tuple.iter
- (M.Sigma.iter (fun c -> f (CModel c)))
- (ValSigma.iter (fun r -> f (CVal r)))
- (InitSigma.iter (fun r -> f (CInit r)))
-
- let iter2 f =
- Tuple.iter2
- (M.Sigma.iter2 (fun c -> f (CModel c)))
- (ValSigma.iter2 (fun r -> f (CVal r)))
- (InitSigma.iter2 (fun r -> f (CInit r)))
-
- let havoc_chunk = Tuple.choose_map M.Sigma.havoc_chunk ValSigma.havoc_chunk InitSigma.havoc_chunk
-
- let havoc sigma domain =
- let dom = of_domain domain in
- Tuple.map2 M.Sigma.havoc ValSigma.havoc InitSigma.havoc sigma dom
-
- let havoc_any ~call:call =
- Tuple.map (M.Sigma.havoc_any ~call) (ValSigma.havoc_any ~call) (InitSigma.havoc_any ~call)
-
- let remove_chunks sigma domain =
- let dom = of_domain domain in
- Tuple.map2 M.Sigma.remove_chunks ValSigma.remove_chunks InitSigma.remove_chunks sigma dom
-
- let dom = Tuple.map M.Sigma.domain ValSigma.domain InitSigma.domain
-
- let domain sigma =
- let dom = dom sigma in
- Chunk.Set.of_list
- @@ List.append
- (List.map (fun l -> CModel l) (M.Heap.Set.elements dom.model ))
- @@ List.append
- (List.map (fun r -> CVal r) (ValHeap.Set.elements dom.value))
- (List.map (fun r -> CInit r) (InitHeap.Set.elements dom.init))
-
- let union = Chunk.Set.union
-
- end
-
- (* ************************************************************************ *)
- (* *** MemLoader instanciation from the implementation of MemTyped *** *)
- (* ************************************************************************ *)
-
-
- (***************************************************************************)
- (* module Region : MemLoader.Module **)
- (***************************************************************************)
-
- module Region = struct
- module Chunk = Chunk
- module Sigma = Sigma
- let name = "RegionModel"
-
- type loc =
- | Null of { repr : M.loc }
- | Loc of { repr : M.loc ; region : region }
-
-
- (* ---------------------------------------------------------------------- *)
- (* --- Utilities on locations --- *)
- (* ---------------------------------------------------------------------- *)
-
- let last sigma ty = function
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.last"
- ~effect:"Loc is NULL" "loc=%a" M.pretty repr ;
- M.pointer_val M.null
- | Loc { repr } -> M.last sigma.Tuple.model ty repr
-
- (* Conversion among loc, t_pointer terms and t_addr terms *)
- let to_addr = function
- | Null { repr } -> M.pointer_val repr
- | Loc { repr } -> M.pointer_val repr
-
- let to_region_pointer = function
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.to_region_pointer"
- ~effect:"Pointer NULL shall not be parsed in this function" "%a" M.pretty repr ;
- (0, M.pointer_val M.null)
- | Loc { repr ; region } -> (R.id_of_region region, M.pointer_val repr)
-
- let of_region_pointer id _ty term =
- if id == 0 then
- let _ =
- Warning.emit ~severe:false ~source:"MemRegion.Region.of_region_pointer"
- ~effect:"No region has been found" "Region_id is zero"
- in Null { repr = M.pointer_loc term }
- else match R.region_of_id id with
- | None ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.of_region_pointer"
- ~effect:"No region has been found" "Region_id=%d" id ;
- Null { repr = M.pointer_loc term }
- | Some region -> Loc { repr = M.pointer_loc term ; region }
-
- (* Basic operations *)
- let sizeof ty = M.sizeof ty
-
- let field loc field : loc = (* TODO: reconstruction *) match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.field"
- ~effect:"Loc is NULL" "(%a).(%a)" M.pretty repr Printer.pp_field field ;
- assert false
- | Loc { repr ; region } ->
- match R.field region field with
- | None ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.field"
- ~effect:"No region for field" "field:%a" Printer.pp_field field ;
- Null { repr = M.field repr field }
- | Some region -> Loc { repr = M.field repr field ; region }
-
- let shift loc ty offset = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.shift"
- ~effect:"Loc is NULL" "pointer=%a and ty=%a and offset=%a"
- M.pretty repr Ctypes.pp_object ty QED.pretty offset ;
- assert false
- | Loc { repr ; region } ->
- match R.shift region ty offset with
- | None ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.field"
- ~effect:"No region for field" "offset:%a" QED.pretty offset ;
- Null { repr = M.shift repr ty offset }
- | Some region ->
- Loc { repr = M.shift repr ty offset ; region }
-
- let frames ty loc chunk =
- match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.frames"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- assert false
- | Loc loc ->
- match chunk with
- | Chunk.CModel c -> M.frames ty loc.repr c
- | CVal r | CInit r ->
- match R.kind r with
- | R.Single R.Ptr | R.Many R.Ptr ->
- let offset = M.sizeof ty in
- let sizeof = F.e_one in
- let tau = Chunk.tau_of_chunk chunk in
- let basename = Chunk.basename_of_chunk chunk in
- MemMemory.frames ~addr:(M.pointer_val loc.repr) ~offset ~sizeof ~basename tau
- | _ -> []
- (*
- begin match R.kind r with
- | R.Single R.Ptr | R.Many R.Ptr -> [MemMemory.framed (Sigma.value chunk)]
- | _ -> []
- end *)
- (*
- si chunk = CVal r et R.tau_of_region == ptr then the predicate MemMemory.framed (Sigma.value chunk)
- si chunk = CInit r then MemMemory.cinits (Sigma.value chunk)
- *)
-
- let havoc ty loc ~length chunk ~fresh ~current = match loc with
- | Null _ ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.havoc"
- ~effect:"Loc is NULL" "NULL loc" ;
- assert false
- | Loc loc ->
- (* TO CHECK *) assert (QED.equal length F.e_one) ;
- match chunk with
- | Chunk.CModel c -> M.havoc ty loc.repr ~length c ~fresh ~current
- | Chunk.CVal _ | Chunk.CInit _ ->
- let n = M.sizeof_havoc ty loc.repr in
- F.e_fun f_havoc [fresh;current;M.pointer_val loc.repr;n]
-
- let eqmem ty loc chunk m1 m2 = match loc with
- | Null _ ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.eqmem"
- ~effect:"Loc is NULL" "NULL loc" ;
- p_true
- | Loc loc ->
- match chunk with
- | Chunk.CModel c -> M.eqmem ty loc.repr c m1 m2
- | Chunk.CVal _ | Chunk.CInit _ ->
- F.p_call p_eqmem [m1;m2;M.pointer_val loc.repr;M.sizeof_havoc ty loc.repr]
-
- let eqmem_forall ty loc chunk m1 m2 =match loc with
- | Null _ ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.eqmem_forall"
- ~effect:"Loc is NULL" "NULL loc" ;
- [], p_true, p_true
- | Loc loc ->
- match chunk with
- | Chunk.CModel c -> M.eqmem_forall ty loc.repr c m1 m2
- | Chunk.CVal _ | Chunk.CInit _ ->
- let xp = Lang.freshvar ~basename:"p" MemAddr.t_addr in
- let p = F.e_var xp in
- let n = M.sizeof ty in
- let separated = F.p_call MemAddr.p_separated [p;e_one;M.pointer_val loc.repr;n] in
- let equal = p_equal (e_get m1 p) (e_get m2 p) in
- [xp],separated,equal
-
- (* ---------------------------------------------------------------------- *)
- (* --- Load --- *)
- (* ---------------------------------------------------------------------- *)
-
- let load_int sigma (c_int:c_int) loc : term =match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.load_int"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- assert false
- | Loc loc ->
- match R.kind loc.region with
- | R.Many (R.Int c_int') ->
- if compare_c_int c_int c_int' = 0
- then F.e_get (Sigma.value sigma (CVal loc.region)) (M.pointer_val loc.repr)
- else
- let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.load_int"
- ~effect:"Type is not the same in chunk and in argument" "%a!=%a"
- Ctypes.pp_int c_int Ctypes.pp_int c_int'
- in
- F.e_get (Sigma.value sigma (CVal loc.region)) (M.pointer_val loc.repr)
- | R.Single (R.Int c_int') ->
- if compare_c_int c_int c_int' = 0
- then Sigma.value sigma (CVal loc.region)
- else assert false
- | R.Garbled -> M.load_int sigma.model c_int loc.repr
- | _ -> assert false
-
- let load_float sigma (c_float:c_float) loc : term = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.load_float"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- assert false
- | Loc loc ->
- match R.kind loc.region with
- | R.Many (R.Float c_float') ->
- if compare_c_float c_float c_float' = 0
- then F.e_get (Sigma.value sigma (CVal loc.region)) (M.pointer_val loc.repr)
- else
- let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.load_float"
- ~effect:"Type is not the same in chunk and in argument" "%a!=%a"
- Ctypes.pp_float c_float Ctypes.pp_float c_float'
- in
- F.e_get (Sigma.value sigma (CVal loc.region)) (M.pointer_val loc.repr)
- | R.Single (R.Float c_float') ->
- if compare_c_float c_float c_float' = 0
- then Sigma.value sigma (CVal loc.region)
- else assert false
- | R.Garbled -> M.load_float sigma.model c_float loc.repr
- | _ ->
- let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.load_float"
- ~effect:"Type is not the same in chunk and in argument" "%a"
- Ctypes.pp_float c_float
- in
- F.e_get (Sigma.value sigma (CVal loc.region)) (M.pointer_val loc.repr)
-
- let load_pointer sigma ty loc : loc = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.load_pointer"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- assert false
- | Loc loc ->
- match R.points_to loc.region with
- | None ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.load_pointer"
- ~effect:"No pointed loc" "Region=%a" R.pretty loc.region ;
- assert false
- | Some region ->
- let repr = match R.kind loc.region with
- | R.Many (R.Ptr) ->
- M.pointer_loc @@ F.e_get (Sigma.value sigma (CVal loc.region)) (M.pointer_val loc.repr)
- | R.Single (R.Ptr) ->
- M.pointer_loc @@ Sigma.value sigma (CVal loc.region)
- | R.Garbled -> M.load_pointer sigma.Tuple.model ty loc.repr
- | _ ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.load_pointer"
- ~effect:"Kind of region is not a pointer" "Region=%a" R.pretty loc.region ;
- assert false
- in Loc { repr ; region }
-
- (* ---------------------------------------------------------------------- *)
- (* --- Store --- *)
- (* ---------------------------------------------------------------------- *)
-
- let store_int sigma c_int loc v : Chunk.t * term = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.store_int"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- assert false
- | Loc loc ->
- let c = Chunk.CVal loc.region in
- match R.kind loc.region with
- | R.Many (R.Int c_int') ->
- if compare_c_int c_int c_int' = 0
- then (c, F.e_set (Sigma.value sigma c) (M.pointer_val loc.repr) v)
- else assert false
- | R.Single (R.Int c_int') ->
- if compare_c_int c_int c_int' = 0
- then (c, v)
- else assert false
- | R.Garbled -> let (c', v) = M.store_int sigma.model c_int loc.repr v in
- (Chunk.CModel c', v)
- | _ -> assert false
-
- let store_float sigma c_float loc v : Chunk.t * term = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.store_float"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- assert false
- | Loc loc ->
- let c = Chunk.CVal loc.region in
- match R.kind loc.region with
- | R.Many (R.Float c_float') ->
- if compare_c_float c_float c_float' = 0
- then (c, F.e_set (Sigma.value sigma c) (M.pointer_val loc.repr) v)
- else assert false
- | R.Single (R.Float c_float') ->
- if compare_c_float c_float c_float' = 0
- then (c, v)
- else assert false
- | R.Garbled ->
- let (c, t) = M.store_float sigma.Tuple.model c_float loc.repr v in
- (Chunk.CModel c, t)
- | _ -> assert false
-
- let store_pointer sigma ty loc v : Chunk.t * term = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.store_pointer"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- assert false
- | Loc loc ->
- let c = Chunk.CVal loc.region in
- match R.kind loc.region with
- | R.Many (R.Ptr) ->
- (c, F.e_set (Sigma.value sigma (CVal loc.region)) (M.pointer_val loc.repr) v)
- | R.Single (R.Ptr) ->
- (c, v)
- | R.Garbled ->
- let (c, repr) = M.store_pointer sigma.Tuple.model ty loc.repr v in
- (Chunk.CModel c, repr)
- | _ -> assert false
-
- (* ---------------------------------------------------------------------- *)
- (* --- Init --- *)
- (* ---------------------------------------------------------------------- *)
-
- let set_init_atom sigma loc v = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.set_init_atom"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- assert false
- | Loc loc ->
- match R.kind loc.region with
- | R.Garbled ->
- let (c, t) = M.set_init_atom sigma.Tuple.model loc.repr v in
- (Chunk.CModel c, t)
- | R.Single _-> (Chunk.CInit loc.region, v)
- | R.Many _ ->
- let c = Chunk.CInit loc.region in
- (c, F.e_set (Sigma.value sigma c) (M.pointer_val loc.repr) v)
-
- let is_init_atom sigma loc : term = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.is_init_atom"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- assert false
- | Loc loc ->
- match R.kind loc.region with
- | R.Garbled ->
- M.is_init_atom sigma.Tuple.model loc.repr
- | R.Many _ ->
- F.e_get (Sigma.value sigma (Chunk.CInit loc.region)) @@ M.pointer_val loc.repr
- | R.Single _ ->
- Sigma.value sigma (Chunk.CInit loc.region)
-
- let is_init_range sigma ty loc length : pred = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.is_init_range"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- assert false
- | Loc loc ->
- match R.kind loc.region with
- | R.Garbled -> M.is_init_range sigma.Tuple.model ty loc.repr length
- | R.Many _ ->
- let n = F.e_mul (M.sizeof ty) length in
- F.p_call p_is_init_r [ Sigma.value sigma (Chunk.CInit loc.region) ; M.pointer_val loc.repr ; n ]
- | R.Single _ -> (* TODO *) assert false
-
-
- let set_init ty loc ~length chunk ~current : term = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.set_init"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- assert false
- | Loc loc ->
- match R.kind loc.region, chunk with
- | R.Garbled, Chunk.CModel c ->
- M.set_init ty loc.repr ~length c ~current
- | R.Garbled, ( Chunk.CVal _ | Chunk.CInit _) -> assert false
- | R.Many _, _ ->
- let n = F.e_mul (M.sizeof ty) length in
- F.e_fun f_set_init [current ; M.pointer_val loc.repr ; n]
- | R.Single _, _ -> (* TODO *) assert false
-
-
- (* ---------------------------------------------------------------------- *)
- (* --- Footprints --- *)
- (* ---------------------------------------------------------------------- *)
-
- let rec value_footprint ty loc = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.value_footprint"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- Sigma.empty
- | Loc loc ->
- match R.kind loc.region, ty with
- | R.Garbled, (C_int _ | C_float _ | C_pointer _) ->
- Heap.Set.of_list @@ List.map (fun c -> Chunk.CModel c) @@ M.Heap.Set.elements
- @@ M.value_footprint ty loc.repr
- | (R.Many (R.Int _) | R.Single (R.Int _)), C_int _
- | (R.Many (R.Float _) | R.Single (R.Float _)), C_float _
- | (R.Many (R.Ptr ) | R.Single (R.Ptr )), C_pointer _->
- Heap.Set.singleton (Chunk.CVal loc.region)
- | (R.Many _ | R.Single _), (C_int _ | C_float _ | C_pointer _) ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.value_footprint"
- ~effect:"Type is not the same in chunk and in argument" "%a" Ctypes.pretty ty ;
- Heap.Set.singleton (Chunk.CVal loc.region)
- | _, C_comp { cfields } ->
- let none = Heap.Set.empty in
- let some l_fields =
- List.fold_left (fun acc f -> Heap.Set.union acc (value_footprint (Ctypes.object_of f.ftype) @@ field (Loc loc) f)) 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 loc) ty e_zero)
-
- let rec init_footprint ty loc = match loc with
- | Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.init_footprint"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- Sigma.empty
- | Loc loc ->
- match R.kind loc.region, ty with
- | R.Garbled, (C_int _ | C_float _ | C_pointer _) ->
- Heap.Set.of_list @@ List.map (fun c -> Chunk.CModel c) @@ M.Heap.Set.elements
- @@ M.init_footprint ty loc.repr
- | (R.Many (R.Int _) | R.Single (R.Int _)), C_int _
- | (R.Many (R.Float _) | R.Single (R.Float _)), C_float _
- | (R.Many (R.Ptr ) | R.Single (R.Ptr )), C_pointer _->
- Heap.Set.singleton (Chunk.CInit loc.region)
- | (R.Many _ | R.Single _) as k, (C_int _ | C_float _ | C_pointer _) ->
- Warning.emit ~severe:false ~source:"MemRegion.Region.init_footprint"
- ~effect:"Type is not the same in chunk and in argument" "%a != %a"
- R.pp_kind k Ctypes.pretty ty ;
- Heap.Set.singleton (Chunk.CInit loc.region)
- | _, C_comp { cfields } ->
- let none = Heap.Set.empty in
- let some l_fields =
- List.fold_left (fun acc f -> Heap.Set.union acc (init_footprint (Ctypes.object_of f.ftype) @@ field (Loc loc) f)) 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 loc) ty e_zero)
-
- end
-
- type loc = Region.loc
- type domain = Sigma.domain
- type chunk = Chunk.t
- type segment = loc rloc
-
-
-
- (***************************************************************************)
- module LOADER = MemLoader.Make(Region)
- (*****************************************************************************)
-
- let load = LOADER.load
- let load_init = LOADER.load_init
- let stored = LOADER.stored
- let stored_init = LOADER.stored_init
- let copied = LOADER.copied
- let copied_init = LOADER.copied_init
- let initialized = LOADER.initialized
- let domain = LOADER.domain
-
-(*
- let sloc_oget = function
- | Sloc None -> Sloc M.null, None
- | Sloc (Some { Region.repr = repr }) -> Sloc repr
- | Sarray (None,a,b) ->
- | Srange (None,_,_,_)
- | Sdescr (_,None,_) ->
- |
-*)
-
- 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
- | _ ->
- (* 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 _) | Sarray (Region.Null _,_,_) | Srange (Region.Null _,_,_,_)
- | Sdescr (_,Region.Null _,_) -> assert false
- in
- Assert (MemMemory.cinits (Sigma.value seq.post (Chunk.CInit region))) ::
- LOADER.assigned seq ty sloc
-
- (* {2 Reversing the Model} *)
-
- type state = M.state
-
- let state sigma = M.state sigma.Tuple.model
-
- let lookup s e = M.lookup s e
-
- let updates = M.updates
-
- let apply = M.apply
-
- let iter = M.iter
-
- let pretty fmt = function
- | Region.Null { repr } -> Format.fprintf fmt "{ NULL=%a }" M.pretty repr
- | Region.Loc loc -> Format.fprintf fmt "{ repr=%a ; region=%a }" M.pretty loc.repr R.pretty loc.region
-
-
- (* {2 Memory Model API} *)
-
- let vars = function
- | Region.Null _ -> Vars.empty
- | 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.Loc { repr } -> M.occurs var repr
- (* Test if a location depend on a given logic variable *)
-
- let null = Region.Null { repr = M.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.Null { 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 ->
- Warning.emit ~severe:false ~source:"MemRegion.cvar"
- ~effect:"No region for this var" "%a" Printer.pp_varinfo var ;
- Region.Null { repr = M.cvar var }
- | Some region -> Region.Loc { repr = M.cvar var ; region }
- (* Return the location of a C variable. *)
-
- let pointer_loc term =
- let repr = M.pointer_loc term in
- if QED.equal term @@ M.pointer_val M.null
- then Region.Null { repr }
- else match R.pointer_loc () with
- | None -> Region.Null { 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 { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.pointer_val"
- ~effect:"No region for this loc" "%a" M.pretty repr ;
- 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 { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.field"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- Region.Null { repr = M.field repr fieldinfo }
- | Region.Loc loc ->
- match R.field loc.region fieldinfo with
- | None ->
- Warning.emit ~severe:false ~source:"MemRegion.field"
- ~effect:"No region for this field" "%a.%a" M.pretty loc.repr Printer.pp_field fieldinfo ;
- Region.Null { repr = M.field loc.repr fieldinfo }
- | Some region -> Region.Loc { repr = M.field loc.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 { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.shift"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- Region.Null { repr = M.shift repr ty term }
- | Region.Loc loc ->
- match R.shift loc.region ty term with
- | None ->
- Warning.emit ~severe:false ~source:"MemRegion.shift"
- ~effect:"No region for this shift" "pointer=%a and ty=%a and offset=%a"
- M.pretty loc.repr Ctypes.pp_object ty QED.pretty term;
- Region.Null { repr = M.shift loc.repr ty term }
- | Some region -> Region.Loc { repr = M.shift loc.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 { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.base_addr"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- Region.Null { repr = M.base_addr repr }
- | Region.Loc loc -> Region.Loc {
- repr = M.base_addr loc.repr ;
- region = R.base_addr loc.region ;
- }
- (* Return the memory location of the base address of a given memory
- location. *)
-
- let base_offset = function
- | Region.Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.base_offset"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- 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 { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.block_length"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- 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 { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.cast"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- Region.Null { 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 =
- let repr = M.loc_of_int ty term in
- if QED.equal term @@ M.pointer_val M.null
- then Region.Null { repr }
- else match R.loc_of_int () with
- | None -> Region.Null { repr }
- | Some region -> Region.Loc { repr ; region }
-
- let int_of_loc c_int = function
- | Region.Null { repr } ->
- Warning.emit ~severe:false ~source:"MemRegion.int_of_loc"
- ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- M.pointer_val 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 { repr } -> M.is_null 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 { 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 { repr }) -> Rloc (ty, repr)
- | Rloc (ty, Region.Loc loc) ->
- Rloc (ty, loc.repr)
- | Rrange (Region.Null { 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 { repr } -> repr | Region.Loc { repr } -> repr)),
- (match loc with Region.Null _ -> None | Region.Loc { region } -> Some region)
- | Rrange (loc, ty, inf, sup) ->
- Rrange ((match loc with Region.Null { repr } -> repr | Region.Loc { repr } -> repr), ty, inf, sup),
- (match loc with Region.Null _ -> 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 frame_value sigma region = match R.kind region with
- | R.Many R.Ptr | R.Single R.Ptr -> MemMemory.framed @@ Sigma.value sigma @@ Chunk.CVal region
- | R.Garbled | R.Many (R.Int _ | R.Float _) | R.Single (R.Int _ | R.Float _) -> p_true
-
- let frame_init sigma region = match R.kind region with
- | R.Many R.Ptr | R.Single R.Ptr -> MemMemory.cinits @@ Sigma.value sigma @@ Chunk.CInit region
- | R.Garbled | R.Many (R.Int _ | R.Float _) | R.Single (R.Int _ | R.Float _) -> p_true
-
- let frame sigma =
- ValSigma.Chunk.Set.fold (fun r l -> frame_value sigma r :: l) (ValSigma.domain sigma.Tuple.value)
- @@ InitSigma.Chunk.Set.fold (fun r l -> frame_init sigma r :: l) (InitSigma.domain sigma.Tuple.init)
- @@ M.frame sigma.Tuple.model
- (* Assert the memory is a proper heap state preceeding the function
- entry point. *)
-
- let alloc sigma vars =
- if vars = [] then sigma else { sigma with Tuple.model = M.alloc sigma.Tuple.model vars }
- (* Allocates new chunk for the validity of variables. *)
-
- let invalid sigma rloc = M.invalid sigma.Tuple.model (get_rloc rloc)
- (* Returns the formula that tests if the entire memory is invalid
- for write access. *)
-
- let scope sigma scope vars =
- let m_sigma = { pre = sigma.pre.Tuple.model ; post = sigma.post.Tuple.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 p = M.global sigma.Tuple.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 chunk_is_well_formed sigma chunk = match chunk with
- | Chunk.CModel _ | Chunk.CInit _ -> p_true
- | Chunk.CVal region -> match R.kind region with
- | R.Garbled -> p_true
- | R.Many (R.Float _ | R.Ptr ) | R.Single (R.Float _ | R.Ptr ) -> p_true
- | R.Many (R.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)))
- | R.Single (R.Int cint) ->
- Cint.range cint @@ Sigma.value sigma chunk
-
-
- let is_well_formed sigma =
- p_and (M.is_well_formed sigma.Tuple.model)
- @@ p_conj @@ Sigma.Chunk.Set.fold (fun c l -> chunk_is_well_formed sigma c :: l) (Sigma.domain sigma) []
-
-
-end
-
-*)
-
-
-module MemMake (R:RegionAnalysis.API) (M:ModelLoader) (* : Sigs.Model *) =
-struct
-
- type region = R.region
-
- (***************************************************************************)
- (* *)
- (* Extern API *)
- (* *)
- (***************************************************************************)
- let datatype = "MemRegion.Make"
- (* For projectification. Must be unique among models. *)
-
- let configure () =
- begin
- let rollback () =
- M.configure () () ;
- in
- rollback
- end
- (* Initializers to be run before using the model.
- Typically push {i Context} values and returns a function to rollback.
- *)
-
- let configure_ia ia = (* TODO *) M.configure_ia ia
- (* Given an automaton, return a vertex's binder.
- Currently used by the automata compiler to bind current vertex.
-
- *)
-
- let hypotheses p = M.hypotheses p
- (* Computes the memory model partitionning of the memory locations.
- This function typically adds new elements to the partition received
- in input (that can be empty).
- ============================> TODO <======================================
- *)
-
module BChunk = struct
(* Do not warn on unused constructors, even if they are not used yet. *)
diff --git a/src/plugins/wp/MemRegion.mli b/src/plugins/wp/MemRegion.mli
index 34dcd4a10daa131bb0c6af052da081099751c3ad..9581a8c56759cebef4747cd6990dc98821608976 100644
--- a/src/plugins/wp/MemRegion.mli
+++ b/src/plugins/wp/MemRegion.mli
@@ -59,5 +59,4 @@ module type ModelLoader = sig
end
-(* module Make (_:RegionAnalysis.API) (_:ModelLoader) : Sigs.Model *)
-module MemMake (_:RegionAnalysis.API) (_:ModelLoader) : Sigs.Model
+module Make (_:RegionAnalysis.API) (_:ModelLoader) : Sigs.Model