From 2689d15e0f1975f7fba4dae7e99a2c30d491212b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Fri, 30 Aug 2024 09:31:33 +0200
Subject: [PATCH] [wp] MemBornat
# squashed from previous dev
---
src/plugins/wp/Dispatcher.ml | 279 --
src/plugins/wp/Factory.ml | 17 +-
src/plugins/wp/Factory.mli | 2 +-
src/plugins/wp/MemBornat.ml | 2449 +++++++++++++++++
.../wp/{Dispatcher.mli => MemBornat.mli} | 53 +-
src/plugins/wp/MemBytes.ml | 14 +
src/plugins/wp/MemDispatch.ml | 715 -----
src/plugins/wp/MemLoader.mli | 2 +
src/plugins/wp/MemTyped.ml | 16 +
src/plugins/wp/MemTyped.mli | 32 +
src/plugins/wp/RegionAnalysis.ml | 224 ++
.../{MemDispatch.mli => RegionAnalysis.mli} | 42 +-
src/plugins/wp/ctypes.ml | 27 +
src/plugins/wp/ctypes.mli | 1 +
src/plugins/wp/gui/GuiPanel.ml | 4 +-
15 files changed, 2849 insertions(+), 1028 deletions(-)
delete mode 100644 src/plugins/wp/Dispatcher.ml
create mode 100644 src/plugins/wp/MemBornat.ml
rename src/plugins/wp/{Dispatcher.mli => MemBornat.mli} (53%)
delete mode 100644 src/plugins/wp/MemDispatch.ml
create mode 100644 src/plugins/wp/RegionAnalysis.ml
rename src/plugins/wp/{MemDispatch.mli => RegionAnalysis.mli} (61%)
diff --git a/src/plugins/wp/Dispatcher.ml b/src/plugins/wp/Dispatcher.ml
deleted file mode 100644
index c52f5d3a46a..00000000000
--- a/src/plugins/wp/Dispatcher.ml
+++ /dev/null
@@ -1,279 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Either
-open Lang.F
-open Ctypes
-open Cil_types
-open Interpreted_automata
-open Sigs
-
-
-let rec partition_terminal_recursive f accl accr = function
- | [] -> (accl, accr)
- | c :: rest -> match f c with
- | Left _ -> partition_terminal_recursive f (c::accl) accr rest
- | Right _ -> partition_terminal_recursive f accl (c::accr) rest
-
-let partition (f: 'c -> ('a,'b) Either.t) (l:'c list) : 'c list * 'c list =
- partition_terminal_recursive f [] [] l
-
-let rec split_terminal_recursive (accl : 'a list) (accr : 'b list) = function
- | [] -> (accl, accr)
- | (Left l) :: rest -> split_terminal_recursive (l::accl) accr rest
- | (Right r) :: rest -> split_terminal_recursive accl (r::accr) rest
-
-let split l = split_terminal_recursive [] [] l
-
-
-module type Dispatcher =
-sig
-
- type loc_left
- type loc_right
-
- module ML : Sigs.Model with type loc = loc_left
- module MR : Sigs.Model with type loc = loc_right
-
- type loc = (loc_left, loc_right) Either.t
-
- val null : loc
- val is_null : loc -> pred
- val cvar : varinfo -> loc
- val pointer_loc : QED.term -> loc
- val loc_of_int : c_object -> QED.term -> loc
-
- val deref_left : loc_left -> loc_left -> loc
- val deref_right : loc_right -> loc_right -> loc
- val literal : eid:int -> Cstring.cst -> loc
-
-
- (* utilities *)
- val hypotheses : MemoryContext.partition -> MemoryContext.partition
- val configure_ia: automaton -> vertex binder
-
-end
-
-
-module CollectionCObject = Qed.Collection.Make(struct
- type t = Ctypes.c_object
- let compare = Ctypes.compare
- let hash = Ctypes.hash
- let equal = Ctypes.equal
- end)
-
-
-module TySet = CollectionCObject.Set
-
-module RegionAssociator = struct
- (* Data : WpContext.Data with type key = Key.t *)
- type model = Typed | Bytes
- type key = Region.node
- type data = model
- let name = "WP.Dispatcher.RegionDispatch"
- let rec compile (region:Region.node) : model =
- let kf =
- match snd @@ WpContext.get_context () with
- | Global -> raise Not_found
- | Kf f -> f
- in
- let map = Region.get_map kf in
- (* a. if access types are different (c_object), then memBytes *)
- let add_type set ty = TySet.add (Ctypes.object_of ty) set in
- let types = TySet.empty in
- let types = List.fold_left add_type types @@ Region.reads map region in
- let types = List.fold_left add_type types @@ Region.writes map region in
- let types = List.fold_left add_type types @@ Region.shifts map region in
- if List.length @@ TySet.elements types > 1 then Bytes else
- (* b. if access type is aggregate with a union inside, then memBytes *)
- let rec is_aggregate_with_union (ty:c_object) : bool =
- match ty with
- | C_int _ | C_float _ | C_pointer _ -> false
- | C_comp compinfo ->
- if compinfo.cstruct then true
- else begin match compinfo.cfields with
- | None -> false
- | Some l -> List.exists (fun field -> is_aggregate_with_union @@ C_comp field.fcomp) l
- end
- | C_array arrayinfo -> is_aggregate_with_union (object_of arrayinfo.arr_element)
- in
- if TySet.exists is_aggregate_with_union types then Bytes else
- (* c. if at least one of the pointed_by regions is memBytes, then memBytes *)
- let pointed_by = Region.pointed_by map region in
- let model_is_memBytes r = Bytes == compile r in
- if List.exists model_is_memBytes pointed_by then Bytes else
- (* d. otherwise if none of the above, then memTyped *)
- Typed
-end
-
-
-module Make (ML: Sigs.Model) (MR: Sigs.Model) : Dispatcher =
-struct
- type loc_left = ML.loc
- type loc_right = MR.loc
-
- module ML = ML (* intended to be MemTyped *)
- module MR = MR (* intended to be MemBytes *)
-
- type loc = (loc_left, loc_right) Either.t
-
- (** Internal handling of regions *)
- (* Keeping track of the decision to apply which memory model to each region *)
- module RegionDispatch = WpContext.Generator
- (struct
- (* Key : WPContext.Key *)
- type t = Region.node
- let compare a b = Int.compare (Region.get_id a) (Region.get_id b)
- let pretty fmt r = Format.fprintf fmt "R%03d" (Region.get_id r)
- end)
- (RegionAssociator)
-
-
- (** Public API of Dispatch *)
-
- let null = Left ML.null
- let is_null = function
- | Left ll -> ML.is_null ll
- | Right lr -> MR.is_null lr
-
- let cvar (var:varinfo) : loc = (* TODO *)
- let f : kernel_function =
- match snd @@ WpContext.get_context () with
- | Global -> raise Not_found
- | Kf f -> f
- in
- let map_regions = Region.get_map f in
- let region = Region.cvar map_regions var in
- match RegionDispatch.get region with
- | RegionAssociator.Typed -> Left (ML.cvar var)
- | RegionAssociator.Bytes -> Right (MR.cvar var)
-
-
- let pointer_loc term =
- let region = assert false in
- match RegionDispatch.get region with
- | RegionAssociator.Typed -> Left (ML.pointer_loc term)
- | RegionAssociator.Bytes -> Right (MR.pointer_loc term)
-
- let loc_of_int _ty _term = (* TODO *) null
-
- let literal ~eid:_eid _const = (* TODO *) null
-
- let deref_left _ll1 ll2 = (* TODO *) Left ll2
- let deref_right _lr1 lr2 = (* TODO *) Right lr2
-
-
- let hypotheses partition = partition
- let configure_ia automata = (* TODO *)
- ML.configure_ia automata
-
-end
-
-
-(*
-module MultiModuleDispatcher = struct
-
- module Models = struct
- (** Encoding indexes as types (not as integers) *)
- type z = Z (** Zero *)
- type 'a s = S of 'a (** Successor function *)
-
- (** Elements from the list,
- a [n multiloc] corresponds to the type [loc] of the module at index [n] *)
- type _ multiloc = ..
-
-
- (** Index aware module type *)
- module type IndexAware_SigsModel = sig
- include Sigs.Model
- type pos
- val to_multiloc : loc -> pos multiloc
- val of_multiloc : pos multiloc -> loc
- end
-
- (** Index aware list type *)
- type 'pos indexAware_list =
- | Nil: z indexAware_list
- | Cons:
- 'pos indexAware_list * (module IndexAware_SigsModel with type pos = 'pos) ->
- 'pos s indexAware_list
-
- (** Wrapper for the list with its size *)
- module type SizeAware_List = sig
- type size
- val model_list : size indexAware_list
- val get : int -> (module Sigs.Model)
- end
-
- (** The list is stored as a mutable reference *)
- let model_list = ref (module struct
- type size = z
- let model_list = Nil
- let get _ = raise Not_found
- end:SizeAware_List)
-
- (** Add a module to the list *)
- let add_model (module Model : Sigs.Model) =
- let module L = (val !model_list) in
- model_list := (module struct
- (* Create a new constructor for model at position size *)
- type _ multiloc += Loc : Model.loc -> L.size multiloc
- type size = L.size s (* New size of list *)
-
- let model_list = Cons(L.model_list,
- (module struct
- include Model
- type pos = L.size
- let to_multiloc x = Loc x
- let of_multiloc = function
- | Loc x -> x
- | _ -> raise (Invalid_argument "Dispatcher.MultiDispatcher.Models: Dynamic typing error")
- end))
- let get = function
- | 0 -> (module Model:Sigs.Model)
- | n when n < 0 -> raise Not_found
- | n -> L.get (n-1)
- end)
-
- type 'a index =
- | Zero of z
- | Succ of 'a index s
-
- (* (* the following is not typing... even though it would be more efficient *)
- let rec get (index: _ index) (models: 'c indexAware_list) : (module Sigs.Model) =
- begin match (index, models) with
- | (Zero Z, Cons ((_rest : _ indexAware_list), model)) -> model
- | (Succ (S index'), Cons ((rest : _ indexAware_list), (module _model : IndexAware_SigsModel))) ->
- get index' rest
- end
- *)
-
- (*
- (* make type elt private here *)
-
- let () = add_model (module Int)
- let () = add_model (module Bool)
- let () = add_model (module Char)
- *)
- end
-end
-*)
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index f173e8b2e0b..6b824e14825 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva | Bytes
+type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva | Bytes | Bornat
type mvar = Raw | Var | Ref | Caveat
type setup = {
@@ -69,6 +69,7 @@ let descr_mheap d = function
| Typed p -> main d "typed" ; descr_mtyped d p
| Eva -> main d "eva"
| Bytes -> main d "bytes"
+ | Bornat -> main d "bornat"
let descr_mvar d = function
| Var -> ()
@@ -202,9 +203,11 @@ end
module Register(V : MemVar.VarUsage)(M : Sigs.Model)
= MemVar.Make(MakeVarUsage(V))(M)
+
module Model_Hoare_Raw = Register(MemVar.Raw)(MemEmpty)
module Model_Hoare_Ref = Register(Ref)(MemEmpty)
-module Model_Typed_Var = Register(Var)(MemTyped)
+
+module Model_Typed_Var = Register(Var)(MemTyped) (* modèle de base, mettre MemBornat *)
module Model_Typed_Ref = Register(Ref)(MemTyped)
module Model_Bytes_Var = Register(Var)(MemBytes)
module Model_Bytes_Ref = Register(Ref)(MemBytes)
@@ -220,6 +223,7 @@ struct
module A = LogicAssigns.Make(M)(L)
end
+
module Comp_MemZeroAlias = MakeCompiler(MemZeroAlias)
module Comp_Hoare_Raw = MakeCompiler(Model_Hoare_Raw)
@@ -236,6 +240,11 @@ module Comp_Bytes_Var = MakeCompiler(Model_Bytes_Var)
module Comp_Bytes_Ref = MakeCompiler(Model_Bytes_Ref)
module Comp_MemVal = MakeCompiler(MemVal)
+module Comp_Bornat =
+ MakeCompiler
+ (MemVar.Make
+ (MemVar.Static)
+ (MemBornat.MemMake(RegionAnalysis.R)(MemBytes)))
let compiler mheap mvar : (module Sigs.Compiler) =
@@ -251,7 +260,7 @@ let compiler mheap mvar : (module Sigs.Compiler) =
| Bytes, Raw -> (module Comp_MemBytes)
| Bytes, Var -> (module Comp_Bytes_Var)
| Bytes, Ref -> (module Comp_Bytes_Ref)
-
+ | Bornat, _ -> (module Comp_Bornat)
(* -------------------------------------------------------------------------- *)
(* --- Tuning --- *)
@@ -270,6 +279,7 @@ let configure_mheap = function
Context.pop MemTyped.pointer orig_memtyped_pointer
in
rollback
+ | Bornat -> MemBytes.configure ()
let configure_driver setup driver () =
let rollback_mheap = configure_mheap setup.mheap in
@@ -345,6 +355,7 @@ let update_config ~warning m s = function
| "TYPED" -> { s with mheap = Typed MemTyped.Fits }
| "CAST" -> { s with mheap = Typed MemTyped.Unsafe }
| "NOCAST" -> { s with mheap = Typed MemTyped.NoCast }
+ | "BORNAT" -> { s with mheap = Bornat }
| "EVA" -> { s with mheap = Eva }
| "BYTES" -> { s with mheap = Bytes }
| "CAVEAT" -> { s with mvar = Caveat }
diff --git a/src/plugins/wp/Factory.mli b/src/plugins/wp/Factory.mli
index 1b9ac3843c2..9dfc8620575 100644
--- a/src/plugins/wp/Factory.mli
+++ b/src/plugins/wp/Factory.mli
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva | Bytes
+type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva | Bytes | Bornat
type mvar = Raw | Var | Ref | Caveat
type setup = {
diff --git a/src/plugins/wp/MemBornat.ml b/src/plugins/wp/MemBornat.ml
new file mode 100644
index 00000000000..641c6d54bb2
--- /dev/null
+++ b/src/plugins/wp/MemBornat.ml
@@ -0,0 +1,2449 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Bornat Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+open Cil_types
+open Ctypes
+open Lang
+open Lang.F
+open Sigs
+open MemMemory
+
+module L = Qed.Logic
+
+
+module type ModelLoader = sig
+ include Sigs.Model
+
+ val sizeof : c_object -> 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
+
+ val eqmem_forall : c_object -> loc -> chunk -> term -> term -> var list * pred * pred
+
+ val load_int : sigma -> c_int -> loc -> term
+ 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 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
+end
+
+
+
+(*
+module Make (R:RegionAnalysis.API) (M:ModelLoader) (* : Sigs.Model *) =
+struct
+
+ type region = R.region
+
+ (****************************************************************************)
+ (* *)
+ (* Extern API *)
+ (* *)
+ (****************************************************************************)
+ let datatype = "MemBornat.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 Chunk =
+ struct
+ type t =
+ | CModel of M.chunk
+ | CVal of R.region
+ | CInit of R.region
+
+ let self = "MemBornat.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 "BornatModel.%a" M.Chunk.pretty c
+ | CVal r -> Format.fprintf fmt "BornatVal.%a" R.pretty r
+ | CInit r -> Format.fprintf fmt "BornatInit.%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 Bornat : MemLoader.Module **)
+ (****************************************************************************)
+
+ module Bornat = struct
+ module Chunk = Chunk
+ module Sigma = Sigma
+ let name = "BornatModel"
+
+ 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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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:"MemBornat.Bornat.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 = Bornat.loc
+ type domain = Sigma.domain
+ type chunk = Chunk.t
+ type segment = loc rloc
+
+
+
+ (****************************************************************************)
+ module LOADER = MemLoader.Make(Bornat)
+ (******************************************************************************)
+
+ 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 { Bornat.repr = repr }) -> Sloc repr
+ | Sarray (None,a,b) ->
+ | Srange (None,_,_,_)
+ | Sdescr (_,None,_) ->
+ |
+*)
+
+ let assigned seq ty sloc = match sloc with
+ | Sloc (Bornat.Null _) | Sarray (Bornat.Null _,_,_)
+ | Srange (Bornat.Null _,_,_,_) | Sdescr (_,Bornat.Null _,_) ->
+ LOADER.assigned seq ty sloc
+ | _ ->
+ (* Maintain always initialized values initialized *)
+ let region = match sloc with
+ | Sloc (Bornat.Loc loc) | Sarray (Bornat.Loc loc, _, _)
+ | Srange (Bornat.Loc loc, _, _, _)
+ | Sdescr (_, Bornat.Loc loc, _) -> loc.region
+ | Sloc (Bornat.Null _) | Sarray (Bornat.Null _,_,_) | Srange (Bornat.Null _,_,_,_)
+ | Sdescr (_,Bornat.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
+ | Bornat.Null { repr } -> Format.fprintf fmt "{ NULL=%a }" M.pretty repr
+ | Bornat.Loc loc -> Format.fprintf fmt "{ repr=%a ; region=%a }" M.pretty loc.repr R.pretty loc.region
+
+
+ (** {2 Memory Model API} *)
+
+ let vars = function
+ | Bornat.Null _ -> Vars.empty
+ | Bornat.Loc { repr } -> M.vars repr
+ (** Return the logic variables from which the given location depend on. *)
+
+ let occurs var = function
+ | Bornat.Null _ -> false
+ | Bornat.Loc { repr } -> M.occurs var repr
+ (** Test if a location depend on a given logic variable *)
+
+ let null = Bornat.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 -> Bornat.Null { repr }
+ | Some region -> Bornat.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:"MemBornat.cvar"
+ ~effect:"No region for this var" "%a" Printer.pp_varinfo var ;
+ Bornat.Null { repr = M.cvar var }
+ | Some region -> Bornat.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 Bornat.Null { repr }
+ else match R.pointer_loc () with
+ | None -> Bornat.Null { repr }
+ | Some region -> Bornat.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
+ | Bornat.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemBornat.pointer_val"
+ ~effect:"No region for this loc" "%a" M.pretty repr ;
+ M.pointer_val repr
+ | Bornat.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
+ | Bornat.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemBornat.field"
+ ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
+ Bornat.Null { repr = M.field repr fieldinfo }
+ | Bornat.Loc loc ->
+ match R.field loc.region fieldinfo with
+ | None ->
+ Warning.emit ~severe:false ~source:"MemBornat.field"
+ ~effect:"No region for this field" "%a.%a" M.pretty loc.repr Printer.pp_field fieldinfo ;
+ Bornat.Null { repr = M.field loc.repr fieldinfo }
+ | Some region -> Bornat.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
+ | Bornat.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemBornat.shift"
+ ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
+ Bornat.Null { repr = M.shift repr ty term }
+ | Bornat.Loc loc ->
+ match R.shift loc.region ty term with
+ | None ->
+ Warning.emit ~severe:false ~source:"MemBornat.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;
+ Bornat.Null { repr = M.shift loc.repr ty term }
+ | Some region -> Bornat.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
+ | Bornat.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemBornat.base_addr"
+ ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
+ Bornat.Null { repr = M.base_addr repr }
+ | Bornat.Loc loc -> Bornat.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
+ | Bornat.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemBornat.base_offset"
+ ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
+ M.base_offset repr
+ | Bornat.Loc { repr } -> M.base_offset repr
+ (** Return the offset of the location, in bytes, from its base_addr. *)
+
+ let block_length sigma ty = function
+ | Bornat.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemBornat.block_length"
+ ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
+ M.block_length sigma.Tuple.model ty repr
+ | Bornat.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
+ | Bornat.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemBornat.cast"
+ ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
+ Bornat.Null { repr = M.cast objs repr }
+ | Bornat.Loc loc -> Bornat.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 Bornat.Null { repr }
+ else match R.loc_of_int () with
+ | None -> Bornat.Null { repr }
+ | Some region -> Bornat.Loc { repr ; region }
+
+ let int_of_loc c_int = function
+ | Bornat.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemBornat.int_of_loc"
+ ~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
+ M.pointer_val repr
+ | Bornat.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
+ | Bornat.Null { repr } -> M.is_null repr
+ | Bornat.Loc { repr } -> M.is_null repr
+ (** Return the formula that check if a given location is null *)
+
+ let get_repr = function
+ | Bornat.Null { repr } -> repr
+ | Bornat.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, Bornat.Null { repr }) -> Rloc (ty, repr)
+ | Rloc (ty, Bornat.Loc loc) ->
+ Rloc (ty, loc.repr)
+ | Rrange (Bornat.Null { repr }, ty, inf, sup) ->
+ Rrange (repr, ty, inf, sup)
+ | Rrange (Bornat.Loc loc, ty, inf, sup) ->
+ Rrange (loc.repr, ty, inf, sup)
+
+
+ let get_rloc_region = function
+ | Rloc (ty, loc) ->
+ Rloc (ty, (match loc with Bornat.Null { repr } -> repr | Bornat.Loc { repr } -> repr)),
+ (match loc with Bornat.Null _ -> None | Bornat.Loc { region } -> Some region)
+ | Rrange (loc, ty, inf, sup) ->
+ Rrange ((match loc with Bornat.Null { repr } -> repr | Bornat.Loc { repr } -> repr), ty, inf, sup),
+ (match loc with Bornat.Null _ -> None | Bornat.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 = "MemBornat.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. *)
+ [@@@ warning "-37" ]
+
+ type t =
+ | CVal of R.region
+ | CInit of R.region
+ | CGhost of R.region
+
+ let self = "MemBornat.Make.BornatChunk"
+
+
+ let hash = function
+ | CVal r -> 0x02 * R.hash r
+ | CInit r -> 0x100 * R.hash r
+ | CGhost r -> 0x10000 * R.hash r
+
+ let equal c1 c2 = match c1, c2 with
+ | CVal r1, CVal r2 | CInit r1, CInit r2 | CGhost r1, CGhost r2 -> R.equal r1 r2
+ | _ -> false
+
+ let compare c1 c2 = hash c1 - hash c2
+
+ let pretty fmt = function
+ | CVal _ -> Format.fprintf fmt "Value"
+ | CInit _ -> Format.fprintf fmt "Init"
+ | CGhost _ -> Format.fprintf fmt "Ghost"
+
+ 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
+ | CVal r | CGhost 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
+ | CGhost _ -> "GhostChunk"
+ | CVal _ -> "ValueChunk"
+ | CInit _ -> "InitChunk"
+ (** Used when generating fresh variables for a chunk. *)
+
+ let is_framed _ = false
+
+ end
+
+ module B = BChunk
+
+ module BHeap = Qed.Collection.Make(B)
+
+ module BSigma = Sigma.Make(BChunk)(BHeap)
+
+ module Chunk =
+ struct
+ type t =
+ | CModel of M.chunk
+ | CBornat of BChunk.t
+
+ let self = "MemBornat.Make.Chunk"
+ (** Chunk names, for pretty-printing. *)
+
+ let hash = function
+ | CModel c -> M.Chunk.hash c
+ | CBornat c -> 0x1000 * (B.hash c)
+
+ let equal ca cb = match ca, cb with
+ | CModel c1, CModel c2 -> M.Chunk.equal c1 c2
+ | CBornat c1, CBornat c2 -> B.equal c1 c2
+ | CModel _, CBornat _ | CBornat _, CModel _ -> false
+
+ let compare c1 c2 = (hash c1) - (hash c2)
+
+ let pretty fmt = function
+ | CModel c -> Format.fprintf fmt "CModel.%a" M.Chunk.pretty c
+ | CBornat c -> Format.fprintf fmt "CBornat.%a" B.pretty c
+
+ let tau_of_chunk = function
+ | CModel c -> M.Chunk.tau_of_chunk c
+ | CBornat c -> B.tau_of_chunk c
+
+ let basename_of_chunk = function
+ | CModel _ -> "Model"
+ | CBornat _ -> "Bornat"
+ (** Used when generating fresh variables for a chunk. *)
+
+ let is_framed = function
+ | CModel c -> M.Chunk.is_framed c
+ | CBornat _ -> 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.
+
+ *)
+
+ module Heap = Qed.Collection.Make(Chunk)
+
+ module Tuple = struct
+ type ('a, 'b) tuple = {
+ model : 'a ;
+ bornat : 'b ;
+ }
+
+ let create f1 f2 input = {
+ model = f1 input ;
+ bornat = f2 input ;
+ }
+
+ let iter f1 f2 tuple =
+ f1 tuple.model ;
+ f2 tuple.bornat ;
+ ()
+
+ let iter2 f1 f2 t1 t2 =
+ f1 t1.model t2.model ;
+ f2 t1.bornat t2.bornat ;
+ ()
+
+ let choose_apply f1 f2 tuple = function
+ | Chunk.CModel c -> f1 tuple.model c
+ | Chunk.CBornat c -> f2 tuple.bornat c
+
+ let choose_map f1 f2 tuple = function
+ | Chunk.CModel c -> { tuple with model = f1 tuple.model c }
+ | Chunk.CBornat c -> { tuple with bornat = f2 tuple.bornat c }
+
+ let map f1 f2 tuple = {
+ model = f1 tuple.model ;
+ bornat = f2 tuple.bornat ;
+ }
+
+ let map2 f1 f2 t1 t2 = {
+ model = f1 t1.model t2.model ;
+ bornat = f2 t1.bornat t2.bornat ;
+ }
+
+ let sequence_map f1 f2 seq = {
+ model = f1 { pre = seq.pre.model ; post = seq.post.model } ;
+ bornat = f2 { pre = seq.pre.bornat ; post = seq.post.bornat } ;
+ }
+ end
+
+ type sigma = (M.sigma, BSigma.t) Tuple.tuple
+
+ module Sigma = (* Sigma.Make(Chunk)(Heap) *) struct
+
+ open Tuple
+ type t = sigma
+ type chunk = Chunk.t
+
+ open Chunk
+
+ type domain = Heap.set
+
+ type dom = (M.Sigma.domain, BSigma.domain) Tuple.tuple
+
+ (* local *)
+ let chunk_split_list l =
+ let rec aux acc1 acc2 = function
+ | [] -> { model = List.rev acc1 ; bornat = List.rev acc2 }
+ | CModel c :: rest -> aux (c::acc1) acc2 rest
+ | CBornat c :: rest -> aux acc1 (c::acc2) rest
+ in aux [] [] l
+
+ let of_domain (domain:domain) : dom =
+ Tuple.map
+ M.Sigma.Chunk.Set.of_list
+ BSigma.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 cbornat = BSigma.Chunk.Set.elements dom.bornat in
+ let model = Heap.Set.of_list (List.map (fun c -> CModel c) cmodel) in
+ let bornat = Heap.Set.of_list (List.map (fun c -> CBornat c) cbornat) in
+ Heap.Set.union model bornat
+
+ module Chunk = Heap
+
+
+ let create = Tuple.create M.Sigma.create BSigma.create
+
+ let pretty fmt sigma =
+ Format.fprintf fmt "@[{@[%a@];@[%a@]}@]"
+ M.Sigma.pretty sigma.model
+ BSigma.pretty sigma.bornat
+
+ let empty : domain = Heap.Set.empty
+
+ let mem = Tuple.choose_apply M.Sigma.mem BSigma.mem
+
+ let get = Tuple.choose_apply M.Sigma.get BSigma.get
+
+ let writes sigma = to_domain @@ Tuple.sequence_map M.Sigma.writes BSigma.writes sigma
+
+ let value = Tuple.choose_apply M.Sigma.value BSigma.value
+
+ let copy = Tuple.map M.Sigma.copy BSigma.copy
+
+ let join sigma1 sigma2 =
+ let r = Tuple.map2 M.Sigma.join BSigma.join sigma1 sigma2 in
+ Passive.union r.model r.bornat
+
+ 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)
+ @@ BSigma.assigned ~pre:sigma1.bornat ~post:sigma2.bornat dom.bornat
+
+ let choose = Tuple.map2 M.Sigma.choose BSigma.choose
+
+ let merge s1 s2 =
+ let (sm, pm1, pm2) = M.Sigma.merge s1.model s2.model in
+ let (sb, pb1, pb2) = BSigma.merge s1.bornat s2.bornat in
+ let s = { model = sm ; bornat = sb } in
+ let p1 = Passive.union pm1 pb1 in
+ let p2 = Passive.union pm2 pb2 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)))
+ (BSigma.iter (fun c -> f (CBornat c)))
+
+ let iter2 f =
+ Tuple.iter2
+ (M.Sigma.iter2 (fun c -> f (CModel c)))
+ (BSigma.iter2 (fun c -> f (CBornat c)))
+
+ let havoc_chunk = Tuple.choose_map M.Sigma.havoc_chunk BSigma.havoc_chunk
+
+ let havoc sigma domain =
+ let dom = of_domain domain in
+ Tuple.map2 M.Sigma.havoc BSigma.havoc sigma dom
+
+ let havoc_any ~call:call =
+ Tuple.map (M.Sigma.havoc_any ~call) (BSigma.havoc_any ~call)
+
+ let remove_chunks sigma domain =
+ let dom = of_domain domain in
+ Tuple.map2 M.Sigma.remove_chunks BSigma.remove_chunks sigma dom
+
+ let dom = Tuple.map M.Sigma.domain BSigma.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.map (fun c -> CBornat c) (BHeap.Set.elements dom.bornat))
+
+ let union = Chunk.Set.union
+
+ end
+
+ (* ************************************************************************ *)
+ (* *** MemLoader instanciation from the implementation of MemTyped *** *)
+ (* ************************************************************************ *)
+
+
+ (****************************************************************************)
+ (** module Bornat : MemLoader.Module **)
+ (****************************************************************************)
+
+ module Bornat = struct
+ module Chunk = Chunk
+ module Sigma = Sigma
+ let name = "BornatModel"
+
+ type loc =
+ | Null
+ | Raw of { repr : M.loc }
+ | Loc of { repr : M.loc ; region : region }
+
+
+ (* ---------------------------------------------------------------------- *)
+ (* --- Utilities on locations --- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let last sigma ty = function
+ | Null ->
+ Warning.emit ~severe:false ~source:"MemBornat.Bornat.last"
+ ~effect:"Loc is NULL" "loc=NULL" ;
+ M.pointer_val M.null
+ | Raw { repr } ->
+ Warning.emit ~severe:false ~source:"MemBornat.Bornat.last"
+ ~effect:"Loc is Raw" "loc=%a" M.pretty repr ;
+ M.last sigma.Tuple.model ty repr
+ | Loc { repr } -> M.last sigma.Tuple.model ty repr
+
+ (** Conversion among loc, t_pointer terms and t_addr terms *)
+ let to_addr = function
+ | Null -> M.pointer_val M.null
+ | Raw { repr } -> M.pointer_val repr
+ | Loc { repr } -> M.pointer_val repr
+
+ let to_region_pointer = function
+ | Null -> (0, M.pointer_val M.null)
+ | Raw { repr } -> (0, M.pointer_val repr)
+ | Loc { repr ; region } -> (R.id_of_region region, M.pointer_val repr)
+
+ let of_region_pointer id _ty term =
+ if id == 0 then
+ if QED.equal term (M.pointer_val M.null) then Null else
+ let _ =
+ Warning.emit ~severe:false ~source:"MemBornat.Bornat.of_region_pointer"
+ ~effect:"No region has been found" "Region_id is zero for loc=%a"
+ QED.pretty term
+ in Raw { repr = M.pointer_loc term }
+ else match R.region_of_id id with
+ | None ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.of_region_pointer"
+ ~effect:"No region has been found" "Region_id=%d for term=%a" id
+ QED.pretty term
+ in Raw { 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 -> Null
+ | Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.field"
+ ~effect:"Loc is Raw" "(%a).(%a)"
+ M.pretty repr Printer.pp_field field
+ in Raw { repr = M.field repr field }
+ | Loc { repr ; region } ->
+ match R.field region field with
+ | None ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.field"
+ ~effect:"No region for field" "(%a in %a).(%a)"
+ M.pretty repr R.pretty region Printer.pp_field field
+ in Raw { repr = M.field repr field }
+ | Some region -> Loc { repr = M.field repr field ; region }
+
+ let shift loc ty offset = match loc with
+ | Null -> Null
+ | Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.shift"
+ ~effect:"Loc is Raw" "No region for (%a).[%a : %a]"
+ M.pretty repr QED.pretty offset Ctypes.pp_object ty
+ in Raw { repr = M.shift repr ty offset }
+ | Loc { repr ; region } ->
+ match R.shift region ty offset with
+ | None ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.field"
+ ~effect:"No region for shift" "No region for (%a in %a).[%a : %a]"
+ M.pretty repr R.pretty region QED.pretty offset Ctypes.pp_object ty
+ in Raw { repr = M.shift repr ty offset }
+ | Some region ->
+ Loc { repr = M.shift repr ty offset ; region }
+
+ let frames_repr_region ty mloc r c =
+ 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 c in
+ let basename = Chunk.basename_of_chunk c in
+ MemMemory.frames ~addr:(M.pointer_val mloc) ~offset ~sizeof ~basename tau
+ | _ -> []
+
+ let frames ty loc chunk =
+ match loc with
+ | Null -> []
+ | Raw { repr } -> begin match chunk with
+ | Chunk.CModel c ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.frames"
+ ~effect:"Loc is Raw" "Frames %a" M.pretty repr
+ in M.frames ty repr c
+ | Chunk.CBornat (B.CVal r | B.CInit r | B.CGhost r) ->
+ frames_repr_region ty repr r chunk
+ end
+ | Loc { repr ; region } -> frames_repr_region ty repr region chunk
+ (*
+ 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 ->
+ F.e_fun f_havoc [fresh;current;M.pointer_val M.null;length]
+ | Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.havoc"
+ ~effect:"Loc is Raw" "havoc of Raw=%a"
+ M.pretty repr
+ in F.e_fun f_havoc [fresh;current;M.pointer_val repr;length]
+ | Loc { repr } ->
+ (* TO CHECK *) assert (QED.equal length F.e_one) ;
+ match chunk with
+ | Chunk.CModel c -> M.havoc ty repr ~length c ~fresh ~current
+ | Chunk.CBornat _ ->
+ F.e_fun f_havoc [fresh;current;M.pointer_val repr;length]
+
+
+ let eqmem_forall ty loc chunk m1 m2 = match loc, chunk with
+ | Null, Chunk.CModel c -> M.eqmem_forall ty M.null c m1 m2
+ | Null, Chunk.CBornat _ ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.eqmem_forall"
+ ~effect:"Loc is NULL" "Los is Null in eqmem_forall"
+ in [], p_true, p_true
+ | (Raw { repr } | Loc { repr }), Chunk.CModel c ->
+ M.eqmem_forall ty repr c m1 m2
+ | (Raw { repr } | Loc { repr }), Chunk.CBornat _ ->
+ let xp = Lang.freshvar ~basename:"b" 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 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 ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ ~effect:"Loc is Null" "Attempt to load_int inside Null"
+ in M.load_int sigma.Tuple.model c_int M.null
+ | Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ ~effect:"Loc is Raw" "load_int(Raw %a)" M.pretty repr
+ in M.load_int sigma.Tuple.model c_int repr
+ | Loc { repr ; region } ->
+ let c = Chunk.CBornat (B.CVal region) in
+ match R.kind region with
+ | R.Many (R.Int c_int') ->
+ if compare_c_int c_int c_int' = 0
+ then F.e_get (Sigma.value sigma c) @@ M.pointer_val repr
+ else
+ let _ =
+ Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ ~effect:"C_int 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 c)
+ @@ M.pointer_val repr
+ | R.Single (R.Int c_int') ->
+ if compare_c_int c_int c_int' = 0
+ then Sigma.value sigma c
+ else
+ let _ =
+ Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ ~effect:"C_int type is not the same in chunk and in argument"
+ "%a!=%a" Ctypes.pp_int c_int Ctypes.pp_int c_int'
+ in Sigma.value sigma c
+ | R.Garbled -> M.load_int sigma.model c_int repr
+ | k ->
+ let _ =
+ Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ ~effect:"Region's kind is not Int" "%a : %a != %a"
+ R.pretty region R.pp_kind k Ctypes.pp_int c_int
+ in assert false
+
+ let load_float sigma (c_float:c_float) loc : term = match loc with
+ | Null ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.load_float"
+ ~effect:"Loc is Null" "Attempt to load_float inside Null"
+ in M.load_float sigma.Tuple.model c_float M.null
+ | Raw { repr } ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.load_float"
+ ~effect:"Loc is Raw" "load_float(Raw %a)" M.pretty repr
+ in M.load_float sigma.Tuple.model c_float repr
+ | Loc { repr ; region } ->
+ let c = Chunk.CBornat (B.CVal region) in
+ match R.kind region with
+ | R.Many (R.Float c_float') ->
+ if compare_c_float c_float c_float' = 0
+ then F.e_get (Sigma.value sigma c) @@ M.pointer_val repr
+ else
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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 c) @@ M.pointer_val repr
+ | R.Single (R.Float c_float') ->
+ if compare_c_float c_float c_float' = 0
+ then Sigma.value sigma c
+ else
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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 Sigma.value sigma c
+ | R.Garbled -> M.load_float sigma.model c_float repr
+ | k ->
+ let _ =
+ Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_float"
+ ~effect:"Region's kind is not Float" "%a : %a != %a"
+ R.pretty region R.pp_kind k Ctypes.pp_float c_float
+ in assert false
+
+ let load_pointer sigma ty loc : loc = match loc with
+ | Null ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.load_float"
+ ~effect:"Loc is Null" "Attempt to load_float inside Null"
+ in let mloc = M.load_pointer sigma.Tuple.model ty M.null in
+ if QED.equal (M.pointer_val mloc) (M.pointer_val M.null)
+ then Null else Raw { repr = mloc }
+ | Raw { repr } ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.load_pointer"
+ ~effect:"Loc is Raw" "load_pointer(Raw %a : *%a)"
+ M.pretty repr Printer.pp_typ ty
+ in Raw { repr = M.load_pointer sigma.Tuple.model ty repr }
+ | Loc { repr ; region } ->
+ let c = Chunk.CBornat (B.CVal region) in
+ match R.points_to region with
+ | None ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.load_pointer"
+ ~effect:"No region pointed" "No region for *(%a in %a)"
+ M.pretty repr R.pretty region
+ in Raw { repr = M.load_pointer sigma.Tuple.model ty repr }
+ | Some r ->
+ let repr = match R.kind region with
+ | R.Many (R.Ptr) ->
+ M.pointer_loc
+ @@ F.e_get (Sigma.value sigma c) @@ M.pointer_val repr
+ | R.Single (R.Ptr) -> M.pointer_loc @@ Sigma.value sigma c
+ | R.Garbled -> M.load_pointer sigma.Tuple.model ty repr
+ | k ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.load_pointer"
+ ~effect:"Kind of region is not a pointer"
+ "Region %a : %a != %a"
+ R.pretty region R.pp_kind k Printer.pp_typ ty
+ in assert false
+ in Loc { repr ; region = r }
+
+
+
+ (* ---------------------------------------------------------------------- *)
+ (* --- Store --- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let store_int sigma c_int loc v : Chunk.t * term = match loc with
+ | Null ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.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
+ Chunk.CModel c, t
+ | Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.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
+ Chunk.CModel c, t
+ | Loc { repr ; region } ->
+ let c = Chunk.CBornat (B.CVal region) in
+ match R.kind region with
+ | R.Many (R.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:"MemBornat.Bornat.store_int"
+ ~effect:"Int types are not the same"
+ "(%a in %a : %a != %a)"
+ M.pretty repr R.pretty region R.pp_kind k Ctypes.pp_int c_int
+ in (c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v)
+ | R.Single (R.Int c_int') as k ->
+ if compare_c_int c_int c_int' = 0
+ then (c, v)
+ else
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.store_int"
+ ~effect:"Int types are not the same"
+ "(%a in %a : %a != %a)"
+ M.pretty repr R.pretty region R.pp_kind k Ctypes.pp_int c_int
+ in (c, v)
+ | R.Garbled ->
+ let (c', v) = M.store_int sigma.model c_int repr v in
+ (Chunk.CModel c', v)
+ | k ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.store_int"
+ ~effect:"Int types are not the same"
+ "(%a in %a : %a != %a)"
+ M.pretty repr R.pretty region R.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:"MemBornat.Bornat.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
+ Chunk.CModel c, t
+ | Raw { repr } ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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
+ Chunk.CModel c, t
+ | Loc { repr ; region } ->
+ let c = Chunk.CBornat (B.CVal region) in
+ match R.kind region with
+ | R.Many (R.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:"MemBornat.Bornat.store_float"
+ ~effect:"Float types are not the same"
+ "(%a in %a : %a != %a)"
+ M.pretty repr R.pretty region R.pp_kind k Ctypes.pp_float c_float
+ in (c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v)
+ | R.Single (R.Float c_float') as k ->
+ if compare_c_float c_float c_float' = 0
+ then (c, v)
+ else
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.store_float"
+ ~effect:"Float types are not the same"
+ "(%a in %a : %a != %a)"
+ M.pretty repr R.pretty region R.pp_kind k Ctypes.pp_float c_float
+ in (c, v)
+ | R.Garbled ->
+ let (c, t) = M.store_float sigma.Tuple.model c_float repr v in
+ (Chunk.CModel c, t)
+ | k ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.store_float"
+ ~effect:"Float types are not the same"
+ "(%a in %a : %a != %a)"
+ M.pretty repr R.pretty region R.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:"MemBornat.Bornat.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
+ Chunk.CModel c, t
+ | Raw { repr } ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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
+ Chunk.CModel c, t
+ | Loc { repr ; region } ->
+ let c = Chunk.CBornat (B.CVal region) in
+ match R.kind region with
+ | R.Many (R.Ptr) ->
+ c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v
+ | R.Single (R.Ptr) -> c,v
+ | R.Garbled ->
+ let (c, repr) = M.store_pointer sigma.Tuple.model ty repr v in
+ (Chunk.CModel c, repr)
+ | k ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.store_pointer"
+ ~effect:"This is not a region with pointer type"
+ "(%a in %a : %a != *%a)"
+ M.pretty repr R.pretty region R.pp_kind k Printer.pp_typ ty
+ in assert false
+
+ (* ---------------------------------------------------------------------- *)
+ (* --- Init --- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let set_init_atom sigma ty loc v = match loc with
+ | Null ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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
+ (Chunk.CModel c, t)
+ | Raw { repr } ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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
+ (Chunk.CModel c, t)
+ | Loc { repr ; region }->
+ match R.kind region with
+ | R.Garbled ->
+ let (c, t) = M.set_init_atom sigma.Tuple.model ty repr v in
+ (Chunk.CModel c, t)
+ | R.Single _-> Chunk.CBornat (B.CInit region), v
+ | R.Many _ ->
+ let c = Chunk.CBornat (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:"MemBornat.Bornat.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:"MemBornat.Bornat.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 = Chunk.CBornat (B.CInit region) in
+ match R.kind region with
+ | R.Garbled -> M.is_init_atom sigma.Tuple.model ty repr
+ | R.Many _ -> F.e_get (Sigma.value sigma c) @@ M.pointer_val repr
+ | R.Single _ -> Sigma.value sigma c
+
+ let is_init_range sigma ty loc length : pred = match loc with
+ | Null ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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:"MemBornat.Bornat.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
+ | R.Garbled -> M.is_init_range sigma.Tuple.model ty repr length
+ | R.Many _ ->
+ let c = Chunk.CBornat (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]
+ | R.Single _ as k ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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 R.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, Chunk.CModel c ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.set_init"
+ ~effect:"Loc is Null" "set_init(Null)"
+ in M.set_init ty M.null ~length c ~current
+ | Null, Chunk.CBornat _ ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.set_init"
+ ~effect:"Loc is Null" "set_init(Null) and Chunk is Bornat"
+ in assert false
+ | Raw { repr }, Chunk.CModel c ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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.CBornat _ ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.set_init"
+ ~effect:"Loc is Null" "set_init(Raw %a) and Chunk is Bornat"
+ M.pretty repr
+ in assert false
+ | Loc { repr }, Chunk.CModel c -> M.set_init ty repr ~length c ~current
+ | Loc { repr ; region }, Chunk.CBornat c ->
+ match R.kind region, c with
+ | R.Garbled, ( B.CVal _ | B.CInit _| B.CGhost _) ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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
+ | R.Many _, _ ->
+ let n = F.e_mul (M.sizeof ty) length in
+ F.e_fun f_set_init [current;M.pointer_val repr;n]
+ | R.Single _, _ ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.set_init"
+ ~effect:"Single is not supported"
+ "set_init(%a in %a : Single)"
+ M.pretty repr R.pretty region
+ in (* TODO *) assert false
+
+
+ (* ---------------------------------------------------------------------- *)
+ (* --- Footprints --- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let rec value_footprint ty loc = match loc with
+ | Null -> Sigma.empty
+ | Raw { repr } ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.value_footprint"
+ ~effect:"Loc is Raw"
+ "value_footprint(Raw %a : %a)"
+ M.pretty repr Ctypes.pp_object ty
+ in let mdom = M.value_footprint ty repr in
+ let bdom = BSigma.empty in
+ Sigma.to_domain { Tuple.model = mdom ; Tuple.bornat = bdom }
+ | Loc { repr ; region } ->
+ match R.kind region, ty with
+ | R.Garbled, (C_int _ | C_float _ | C_pointer _) ->
+ let mdom = M.value_footprint ty repr in
+ Sigma.to_domain { Tuple.model = mdom ; Tuple.bornat = BSigma.empty }
+ | (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.CBornat (B.CVal region))
+ | (R.Many _ | R.Single _) as k, (C_int _ | C_float _ | C_pointer _) ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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 R.pp_kind k
+ in Heap.Set.singleton @@ Chunk.CBornat (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:"MemBornat.Bornat.init_footprint"
+ ~effect:"Loc is Raw"
+ "init_footprint(Raw %a : %a)"
+ M.pretty repr Ctypes.pp_object ty
+ in let mdom = M.init_footprint ty repr in
+ let bdom = BSigma.empty in
+ Sigma.to_domain { Tuple.model = mdom ; Tuple.bornat = bdom }
+ | Loc { repr ; region } ->
+ match R.kind region, ty with
+ | R.Garbled, (C_int _ | C_float _ | C_pointer _) ->
+ let mdom = M.init_footprint ty repr in
+ Sigma.to_domain { Tuple.model = mdom ; Tuple.bornat = BSigma.empty }
+ | (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.CBornat (B.CInit region)
+ | (R.Many _ | R.Single _) as k, (C_int _ | C_float _ | C_pointer _) ->
+ let _ = Warning.emit ~severe:false
+ ~source:"MemBornat.Bornat.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 R.pp_kind k
+ in Heap.Set.singleton @@ Chunk.CBornat (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)
+
+ end
+
+ type loc = Bornat.loc
+ type domain = Sigma.domain
+ type chunk = Chunk.t
+ type segment = loc rloc
+
+
+
+ (****************************************************************************)
+ module LOADER = MemLoader.Make(Bornat)
+ (******************************************************************************)
+
+ 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 { Bornat.repr = repr }) -> Sloc repr
+ | Sarray (None,a,b) ->
+ | Srange (None,_,_,_)
+ | Sdescr (_,None,_) ->
+ |
+*)
+
+ let assigned seq ty sloc = match sloc with
+ | Sloc (Bornat.Null) | Sarray (Bornat.Null,_,_)
+ | Srange (Bornat.Null,_,_,_) | Sdescr (_,Bornat.Null,_) ->
+ LOADER.assigned seq ty sloc
+ | Sloc (Bornat.Raw _) | Sarray (Bornat.Raw _,_,_)
+ | Srange (Bornat.Raw _,_,_,_) | Sdescr (_,Bornat.Raw _,_) ->
+ LOADER.assigned seq ty sloc
+ | _ ->
+ (* Maintain always initialized values initialized *)
+ let region = match sloc with
+ | Sloc (Bornat.Loc loc) | Sarray (Bornat.Loc loc, _, _)
+ | Srange (Bornat.Loc loc, _, _, _)
+ | Sdescr (_, Bornat.Loc loc, _) -> loc.region
+ | Sloc (Bornat.Null|Bornat.Raw _)
+ | Sarray ((Bornat.Null|Bornat.Raw _),_,_)
+ | Srange ((Bornat.Null|Bornat.Raw _),_,_,_)
+ | Sdescr (_,(Bornat.Null|Bornat.Raw _),_) -> assert false
+ in
+ Assert (MemMemory.cinits
+ @@ Sigma.value seq.post @@ Chunk.CBornat (B.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
+ | Bornat.Null -> Format.fprintf fmt "NULL"
+ | Bornat.Raw { repr } -> Format.fprintf fmt "{ Raw %a }" M.pretty repr
+ | Bornat.Loc { repr ; region } ->
+ Format.fprintf fmt "{ %a in %a }"
+ M.pretty repr R.pretty region
+
+
+ (** {2 Memory Model API} *)
+
+ let vars = function
+ | Bornat.Null -> Vars.empty
+ | Bornat.Raw { repr } | Bornat.Loc { repr } -> M.vars repr
+ (** Return the logic variables from which the given location depend on. *)
+
+ let occurs var = function
+ | Bornat.Null -> false
+ | Bornat.Raw {repr } | Bornat.Loc { repr } -> M.occurs var repr
+ (** Test if a location depend on a given logic variable *)
+
+ let null = Bornat.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 -> Bornat.Raw { repr }
+ | Some region -> Bornat.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:"MemBornat.cvar"
+ ~effect:"No region for this var" "%a"
+ Printer.pp_varinfo var
+ in Bornat.Raw { repr = M.cvar var }
+ | Some region -> Bornat.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 Bornat.Null
+ else let repr = M.pointer_loc term in
+ match R.pointer_loc () with
+ | None -> Bornat.Raw { repr }
+ | Some region -> Bornat.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
+ | Bornat.Null -> M.pointer_val M.null
+ | Bornat.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.pointer_val"
+ ~effect:"No region for this loc" "%a" M.pretty repr
+ in M.pointer_val repr
+ | Bornat.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
+ | Bornat.Null ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.field"
+ ~effect:"Loc is NULL"
+ "NULL.(%a)" Printer.pp_field fieldinfo
+ in Bornat.Null
+ | Bornat.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.field"
+ ~effect:"Loc is Raw"
+ "(%a).(%a)" M.pretty repr Printer.pp_field fieldinfo
+ in Bornat.Raw { repr = M.field repr fieldinfo }
+ | Bornat.Loc { repr ; region } ->
+ match R.field region fieldinfo with
+ | None ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.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 Bornat.Raw { repr = M.field repr fieldinfo }
+ | Some region -> Bornat.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
+ | Bornat.Null ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.shift"
+ ~effect:"Loc is NULL"
+ "NULL.[%a : %a]" QED.pretty term Ctypes.pp_object ty
+ in Bornat.Null
+ | Bornat.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.shift"
+ ~effect:"Loc is Raw"
+ "(%a).[%a : %a]"
+ M.pretty repr QED.pretty term Ctypes.pp_object ty
+ in Bornat.Raw { repr = M.shift repr ty term }
+ | Bornat.Loc { repr ; region } ->
+ match R.shift region ty term with
+ | None ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.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 Bornat.Raw { repr = M.shift repr ty term }
+ | Some region -> Bornat.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
+ | Bornat.Null -> Bornat.Null
+ | Bornat.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.base_addr"
+ ~effect:"Loc is Raw" "base_addr(%a)" M.pretty repr
+ in Bornat.Raw { repr = M.base_addr repr }
+ | Bornat.Loc { repr ; region } ->
+ Bornat.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
+ | Bornat.Null -> M.base_offset M.null
+ | Bornat.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.base_offset"
+ ~effect:"Loc is Raw" "base_offset(%a)" M.pretty repr
+ in M.base_offset repr
+ | Bornat.Loc { repr } -> M.base_offset repr
+ (** Return the offset of the location, in bytes, from its base_addr. *)
+
+ let block_length sigma ty = function
+ | Bornat.Null -> M.block_length sigma.Tuple.model ty M.null
+ | Bornat.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.block_length"
+ ~effect:"Loc is Raw" "block_length(%a)" M.pretty repr
+ in M.block_length sigma.Tuple.model ty repr
+ | Bornat.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
+ | Bornat.Null -> Bornat.Null
+ | Bornat.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.cast"
+ ~effect:"Loc is NULL" "NULL=%a" M.pretty repr
+ in Bornat.Raw { repr = M.cast objs repr }
+ | Bornat.Loc loc -> Bornat.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 Bornat.Null
+ else match R.loc_of_int () with
+ | None -> Bornat.Raw { repr = M.loc_of_int ty term }
+ | Some region -> Bornat.Loc { repr = M.loc_of_int ty term ; region }
+
+ let int_of_loc c_int = function
+ | Bornat.Null -> M.int_of_loc c_int M.null
+ | Bornat.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemBornat.int_of_loc"
+ ~effect:"Loc is Raw" "NULL=%a" M.pretty repr
+ in M.int_of_loc c_int repr
+ | Bornat.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
+ | Bornat.Null -> p_true
+ | Bornat.Raw { repr } | Bornat.Loc { repr } -> M.is_null repr
+ (** Return the formula that check if a given location is null *)
+
+ let get_repr = function
+ | Bornat.Null -> M.null
+ | Bornat.Raw { repr } -> repr
+ | Bornat.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, Bornat.Null) -> Rloc (ty, M.null)
+ | Rloc (ty, Bornat.Raw { repr }) -> Rloc (ty, repr)
+ | Rloc (ty, Bornat.Loc loc) ->
+ Rloc (ty, loc.repr)
+ | Rrange (Bornat.Null, ty, inf, sup) ->
+ Rrange (M.null, ty, inf, sup)
+ | Rrange (Bornat.Raw { repr }, ty, inf, sup) ->
+ Rrange (repr, ty, inf, sup)
+ | Rrange (Bornat.Loc loc, ty, inf, sup) ->
+ Rrange (loc.repr, ty, inf, sup)
+
+
+ let get_rloc_region = function
+ | Rloc (ty, loc) ->
+ Rloc (ty, (match loc with Bornat.Null -> M.null
+ | Bornat.Raw { repr } | Bornat.Loc { repr } -> repr)),
+ (match loc with Bornat.Null | Bornat.Raw _ -> None
+ | Bornat.Loc { region } -> Some region)
+ | Rrange (loc, ty, inf, sup) ->
+ Rrange ((match loc with Bornat.Null -> M.null
+ | Bornat.Raw { repr } | Bornat.Loc { repr } -> repr), ty, inf, sup),
+ (match loc with Bornat.Null | Bornat.Raw _ -> None
+ | Bornat.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 sigma =
+ let bornat_frame sigma = function
+ | B.CInit region ->
+ MemMemory.cinits @@ Sigma.value sigma @@ Chunk.CBornat (B.CInit region)
+ | B.CVal region | B.CGhost region -> match R.kind region with
+ | R.Many R.Ptr | R.Single R.Ptr ->
+ MemMemory.framed @@ Sigma.value sigma @@ Chunk.CBornat (B.CVal region)
+ | R.Garbled | R.Many (R.Int _ | R.Float _)
+ | R.Single (R.Int _ | R.Float _) -> p_true
+ in
+ BSigma.Chunk.Set.fold (fun c l -> bornat_frame sigma c :: l)
+ (BSigma.domain sigma.Tuple.bornat)
+ @@ 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.CBornat (B.CInit _)
+ | Chunk.CBornat (B.CGhost _) -> p_true
+ | Chunk.CBornat (B.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
diff --git a/src/plugins/wp/Dispatcher.mli b/src/plugins/wp/MemBornat.mli
similarity index 53%
rename from src/plugins/wp/Dispatcher.mli
rename to src/plugins/wp/MemBornat.mli
index b06af86458c..828341de2e6 100644
--- a/src/plugins/wp/Dispatcher.mli
+++ b/src/plugins/wp/MemBornat.mli
@@ -20,43 +20,44 @@
(* *)
(**************************************************************************)
-open Either
-open Lang.F
-open Ctypes
open Cil_types
-open Interpreted_automata
+open Ctypes
+open Lang.F
open Sigs
+(* -------------------------------------------------------------------------- *)
+(* --- Bornat Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
-val partition: ('a -> ('b, 'c) Either.t) -> 'a list -> 'a list * 'a list
-val split : ('a, 'b) Either.t list -> 'a list * 'b list
-
-module type Dispatcher =
-sig
+module type ModelLoader = sig
+ include Sigs.Model
- type loc_left
- type loc_right
+ val sizeof : c_object -> term
+ val last : sigma -> c_object -> loc -> term
- module ML : Sigs.Model with type loc = loc_left
- module MR : Sigs.Model with type loc = loc_right
+ val frames : c_object -> loc -> chunk -> frame list
- type loc = (loc_left, loc_right) t
+ val havoc : c_object -> loc -> length:term -> chunk -> fresh:term -> current:term -> term
- val null : loc
- val is_null : loc -> pred
- val cvar : varinfo -> loc
- val pointer_loc : QED.term -> loc
- val loc_of_int : c_object -> QED.term -> loc
+ val eqmem_forall : c_object -> loc -> chunk -> term -> term -> var list * pred * pred
- val deref_left : loc_left -> loc_left -> loc
- val deref_right : loc_right -> loc_right -> loc
- val literal : eid:int -> Cstring.cst -> loc
+ val load_int : sigma -> c_int -> loc -> term
+ 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
- (* utilities *)
- val hypotheses : MemoryContext.partition -> MemoryContext.partition
- val configure_ia: automaton -> vertex binder
+ 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
end
-(* module Make (_: Sigs.Model) (_: Sigs.Model) : Dispatcher *)
+
+(* module Make (_:RegionAnalysis.API) (_:ModelLoader) : Sigs.Model *)
+module MemMake (_:RegionAnalysis.API) (_:ModelLoader) : Sigs.Model
diff --git a/src/plugins/wp/MemBytes.ml b/src/plugins/wp/MemBytes.ml
index b3d3dad054f..dc0f62a17c8 100644
--- a/src/plugins/wp/MemBytes.ml
+++ b/src/plugins/wp/MemBytes.ml
@@ -1130,3 +1130,17 @@ let scope seq scope xs =
in e_set m (BASE.get x) size)
(Sigma.value seq.pre Alloc) xs in
[ p_equal (Sigma.value seq.post Alloc) alloc ]
+
+(* ********************************************************************** *)
+(* API with BORNAT *)
+(* ********************************************************************** *)
+
+let sizeof = protected_sizeof_object
+let last = Model.last
+let frames = Model.frames
+let eqmem_forall = Model.eqmem_forall
+let set_init = Model.set_init
+let is_init_range = Model.is_init_range
+let value_footprint = Model.value_footprint
+let init_footprint = Model.init_footprint
+let havoc = Model.havoc
diff --git a/src/plugins/wp/MemDispatch.ml b/src/plugins/wp/MemDispatch.ml
deleted file mode 100644
index 0784fd8ab6e..00000000000
--- a/src/plugins/wp/MemDispatch.ml
+++ /dev/null
@@ -1,715 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Empty Memory Model --- *)
-(* -------------------------------------------------------------------------- *)
-
-open Either
-open Product
-open Lang.F
-open Sigs
-open Vset
-open Dispatcher
-
-
-module Make(D: Dispatcher) : Sigs.Model =
-struct
- module ML = D.ML
- module MR = D.MR
-
- type loc = D.loc
-
- let datatype = "MemDispatch.Make"
- (** For projectification. Must be unique among models. *)
-
- let configure () =
- begin
- let rollback () =
- ML.configure () () ;
- MR.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 =
- D.configure_ia ia
- (** Given an automaton, return a vertex's binder.
- Currently used by the automata compiler to bind current vertex.
-
- *)
-
- let hypotheses p =
- D.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 Chunk : Chunk
- with type t = (ML.chunk, MR.chunk) Either.t =
- struct
- type t = (ML.chunk, MR.chunk) Either.t
-
- let self = "MemDispatcher.Chunk"
- (** Chunk names, for pretty-printing. *)
-
- let hash = function
- | Left cl -> ML.Chunk.hash cl
- | Right cr -> 0x1000 + MR.Chunk.hash cr
-
- let equal ca cb =
- match ca, cb with
- | Left c1, Left c2 -> ML.Chunk.equal c1 c2
- | Right c1, Right c2 -> MR.Chunk.equal c1 c2
- | _, _ -> false
-
- let compare c1 c2 = (hash c1) - (hash c2)
-
- let pretty fmt = function
- | Left cl -> Format.fprintf fmt "ML.%a" ML.Chunk.pretty cl
- | Right cr -> Format.fprintf fmt "MR.%a" MR.Chunk.pretty cr
-
-
- let tau_of_chunk = function
- | Left c1 -> ML.Chunk.tau_of_chunk c1
- | Right c2 -> MR.Chunk.tau_of_chunk c2
-
- let basename_of_chunk = function
- | Left c1 -> String.concat "." [ "ML" ; ML.Chunk.basename_of_chunk c1 ]
- | Right c2 -> String.concat "." [ "MR" ; MR.Chunk.basename_of_chunk c2 ]
- (** Used when generating fresh variables for a chunk. *)
-
- let is_framed = function
- | Left c1 -> ML.Chunk.is_framed c1
- | Right c2 -> MR.Chunk.is_framed c2
- (** 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 Heap : Qed.Collection.S
- with type t = (ML.chunk, MR.chunk) t
- = Qed.Collection.Make(Chunk)
-
- type sigma = (ML.Sigma.t, MR.Sigma.t) product
-
- module Sigma =
- struct
-
- type chunk = (ML.chunk, MR.chunk) Either.t
-
- module Chunk = Heap
-
- type domain = Chunk.set
- type dom = (ML.Sigma.domain, MR.Sigma.domain) product
-
- let of_domain (domain:domain) : dom =
- let ldomain = Heap.Set.elements domain in
- let (left,right) = split ldomain in
- let left = ML.Sigma.Chunk.Set.of_list left in
- let right = MR.Sigma.Chunk.Set.of_list right in
- { left ; right }
-
- let to_domain (dom:dom) : domain =
- let left = ML.Heap.Set.elements dom.left in
- let right = MR.Heap.Set.elements dom.right in
- let left = Heap.Set.of_list (List.map (fun l -> Left l) left) in
- let right = Heap.Set.of_list (List.map (fun r -> Right r) right) in
- Heap.Set.union left right
-
- type t = sigma
-
- let create () = {
- left = ML.Sigma.create () ;
- right = MR.Sigma.create () ;
- }
-
- let pretty fmt sigma =
- Format.fprintf fmt "@[{@[%a@];@[%a@]}@]" ML.Sigma.pretty sigma.left MR.Sigma.pretty sigma.right
-
- let empty : domain = Heap.Set.empty
-
- let mem sigma = function
- | Left cl -> ML.Sigma.mem sigma.left cl
- | Right cr -> MR.Sigma.mem sigma.right cr
-
- let get sigma = function
- | Left cl -> ML.Sigma.get sigma.left cl
- | Right cr -> MR.Sigma.get sigma.right cr
-
- let writes (seq:sigma sequence) =
- to_domain {
- left = ML.Sigma.writes (Product.sequence_left seq) ;
- right = MR.Sigma.writes (Product.sequence_right seq) ;
- }
-
- let value sigma = function
- | Left cl -> ML.Sigma.value sigma.left cl
- | Right cr -> MR.Sigma.value sigma.right cr
-
- let copy = Product.map2 ML.Sigma.copy MR.Sigma.copy
-
- let join sigma1 sigma2 =
- Passive.union
- (ML.Sigma.join sigma1.left sigma2.left )
- (MR.Sigma.join sigma1.right sigma2.right)
-
- let assigned ~pre:s1 ~post:s2 domain =
- let dom = of_domain domain in
- let bag_left = ML.Sigma.assigned ~pre:s1.left ~post:s2.left dom.left in
- let bag_right = MR.Sigma.assigned ~pre:s1.right ~post:s2.right dom.right in
- Bag.concat bag_left bag_right
-
-
- let choose = Product.map22 ML.Sigma.choose MR.Sigma.choose
-
- let merge s1 s2 =
- let (sl, pl1, pl2) = ML.Sigma.merge s1.left s2.left in
- let (sr, pr1, pr2) = MR.Sigma.merge s1.right s2.right in
- let s = { left = sl ; right = sr } in
- (s, Passive.union pl1 pr1, Passive.union pl2 pr2)
-
- 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 sigma =
- ML.Sigma.iter (fun l -> f (Left l)) sigma.left ;
- MR.Sigma.iter (fun r -> f (Right r)) sigma.right ;
- ()
-
- let iter2 f =
- let f_left c v1 v2 = f (Left c) v1 v2 in
- let f_right c v1 v2 = f (Right c) v1 v2 in
- Product.iter2 (ML.Sigma.iter2 f_left) (MR.Sigma.iter2 f_right)
-
- let havoc_chunk = Product.map_either ML.Sigma.havoc_chunk MR.Sigma.havoc_chunk
-
- let havoc sigma domain =
- let dom = of_domain domain in
- Product.map22 ML.Sigma.havoc MR.Sigma.havoc sigma dom
-
- let havoc_any ~call:call = Product.map2 (ML.Sigma.havoc_any ~call) (MR.Sigma.havoc_any ~call)
-
- let remove_chunks sigma domain =
- let dom = of_domain domain in
- Product.map22 ML.Sigma.remove_chunks MR.Sigma.remove_chunks sigma dom
-
- let dom = Product.map2 ML.Sigma.domain MR.Sigma.domain
-
- let domain sigma =
- let dom = dom sigma in
- let domain = List.append
- (List.map (fun l -> Left l) (ML.Heap.Set.elements dom.left ))
- (List.map (fun r -> Right r) (MR.Heap.Set.elements dom.right))
- in
- Chunk.Set.of_list domain
-
- let union = Chunk.Set.union
-
- end
-
- type chunk = Chunk.t
- type domain = Sigma.domain
- type segment = loc rloc
-
- type state = (ML.state, MR.state) product
- (** Internal (private) memory state description for later reversing the model. *)
-
- (** Returns a memory state description from a memory environement. *)
- let state = Product.map2 ML.state MR.state
-
- (** Try to interpret a term as an in-memory operation
- located at this program point. Only best-effort
- shall be performed, otherwise return [Mvalue].
-
- Recognized [Cil] patterns:
- - [Mvar x,[Mindex 0]] is rendered as [*x] when [x] has a pointer type
- - [Mmem p,[Mfield f;...]] is rendered as [p->f...] like in Cil
- - [Mmem p,[Mindex k;...]] is rendered as [p[k]...] to catch Cil [Mem(AddPI(p,k)),...] *)
- let lookup state term =
- try ML.lookup state.left term with
- | Not_found -> MR.lookup state.right term
-
- (** Try to interpret a sequence of states into updates.
-
- The result shall be exhaustive with respect to values that are printed as [Sigs.mval]
- values at [post] label {i via} the [lookup] function.
- Otherwise, those values would not be pretty-printed to the user. *)
- let updates states var =
- let bag_left = ML.updates (Product.sequence_left states) var in
- let bag_right = MR.updates (Product.sequence_right states) var in
- Bag.concat bag_left bag_right
-
-
- (** Propagate a sequent substitution inside the memory state. *)
- let apply f = Product.map2 (ML.apply f) (MR.apply f)
-
-
- (** Debug *)
- let iter f state = Product.iter (ML.iter f) (MR.iter f) state
-
- let pretty fmt loc = match loc with
- | Left ll -> Format.fprintf fmt "ML.%a" ML.pretty ll
- | Right lr -> Format.fprintf fmt "MR.%a" MR.pretty lr
- (** pretty printing of memory location *)
-
-
- (** {2 Memory Model API} *)
-
- let vars = function
- | Left ll -> ML.vars ll
- | Right lr -> MR.vars lr
-
- (** Return the logic variables from which the given location depend on. *)
-
- let occurs var = function
- | Left ll -> ML.occurs var ll
- | Right lr -> MR.occurs var lr
- (** Test if a location depend on a given logic variable *)
-
- let null = D.null
- (** Return the location of the null pointer *)
-
- let literal ~eid:eid name = D.literal ~eid name
- (** Return the memory location of a constant string,
- the id is a unique identifier. *)
-
- let cvar var = D.cvar var
- (** Return the location of a C variable. *)
-
- let pointer_loc term = D.pointer_loc term
- (** Interpret an address value (a pointer) as an abstract location.
- Might fail on memory models not supporting pointers. *)
-
- let pointer_val = function
- | Left ll -> ML.pointer_val ll
- | Right lr -> MR.pointer_val lr
- (** Return the adress value (a pointer) of an abstract location.
- Might fail on memory models not capable of representing pointers. *)
-
- let field loc fieldinfo =
- let left = fun l -> ML.field l fieldinfo in
- let right = fun r -> MR.field r fieldinfo in
- Either.map ~left ~right loc
- (** Return the memory location obtained by field access from a given
- memory location. *)
-
- let shift loc ty term = match loc with
- | Left l -> D.deref_left l (ML.shift l ty term)
- | Right r -> D.deref_right r (MR.shift r ty term)
- (** 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 = Either.map ~left:ML.base_addr ~right:MR.base_addr
- (** Return the memory location of the base address of a given memory
- location. *)
-
- let base_offset = function
- | Left ll -> ML.base_offset ll
- | Right lr -> MR.base_offset lr
- (** Return the offset of the location, in bytes, from its base_addr. *)
-
- let block_length (sigma:sigma) ty = function
- | Left ll -> ML.block_length sigma.left ty ll
- | Right lr -> MR.block_length sigma.right ty lr
- (** Returns the length (in bytes) of the allocated block containing
- the given location. *)
-
- let cast objs = Either.map ~left:(ML.cast objs) ~right:(MR.cast objs)
-
- (** 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 = D.loc_of_int ty term
- (** Cast a term representing an absolute memory address (to some c_object)
- given as an integer, into an abstract memory location. The sigma parameter
- is meant to assure that the cast returns a pointer only if in this given
- sigma, the physical address makes sense.
-
- @before Frama-C+dev there was no sigma parameter
- *)
-
- let int_of_loc c_int = function
- | Left ll -> ML.int_of_loc c_int ll
- | Right lr -> MR.int_of_loc c_int lr
- (** Cast a memory location into its absolute memory address,
- given as an integer with the given C-type. *)
-
- let domain ty = function
- | Left ll -> Heap.Set.of_list (List.map (fun l -> Left l) (ML.Heap.Set.elements (ML.domain ty ll)))
- | Right lr -> Heap.Set.of_list (List.map (fun r -> Right r) (MR.Heap.Set.elements (MR.domain ty lr)))
- (** Compute the set of chunks that hold the value of an object with
- the given C-type. It is safe to retun an over-approximation of the
- chunks involved. *)
-
- let is_well_formed sigma =
- p_and (ML.is_well_formed sigma.left) (MR.is_well_formed sigma.right)
- (** Provides the constraint corresponding to the kind of data stored by all
- chunks in sigma. *)
-
- let load sigma ty = function
- | Left ll1 -> begin match ML.load sigma.left ty ll1 with
- | Val t -> Val t
- | Loc ll2 -> Loc (D.deref_left ll1 ll2)
- end
- | Right lr1 -> begin match MR.load sigma.right ty lr1 with
- | Val t -> Val t
- | Loc lr2 -> Loc (D.deref_right lr1 lr2)
- end
- (** Return the value of the object of the given type at the given location in
- the given memory state. *)
-
- let load_init sigma ty = function
- | Left ll -> ML.load_init sigma.left ty ll
- | Right lr -> MR.load_init sigma.right ty lr
- (** Return the initialization status at the given location in the given
- memory state. *)
-
- let stored sigmas ty loc term = match loc with
- | Left ll -> ML.stored (Product.sequence_left sigmas) ty ll term
- | Right lr -> MR.stored (Product.sequence_right sigmas) ty lr term
- (**
- Return a set of formula that express a modification between two memory
- state.
-
- [stored sigma ty loc t] returns a set of formula expressing that
- [sigma.pre] and [sigma.post] are identical except for an object [ty] at
- location [loc] which is represented by [t] in [sigma.post].
- *)
-
- let stored_init sigmas ty loc term = match loc with
- | Left ll -> ML.stored_init (Product.sequence_left sigmas) ty ll term
- | Right lr -> MR.stored_init (Product.sequence_right sigmas) ty lr term
- (**
- Return a set of formula that express a modification of the initialization
- status between two memory state.
-
- [stored_init sigma ty loc t] returns a set of formula expressing that
- [sigma.pre] and [sigma.post] are identical except for an object [ty] at
- location [loc] which has a new init represented by [t] in [sigma.post].
- *)
-
- let copied sigmas ty loc1 loc2 = (* TOCHECK *) match loc1, loc2 with
- | Left ll1, Left ll2 ->
- ML.copied (Product.sequence_left sigmas) ty ll1 ll2
- | Right lr1, Right lr2 ->
- MR.copied (Product.sequence_right sigmas) ty lr1 lr2
- | _,_ -> begin match load sigmas.pre ty loc1 with
- | Val t -> stored sigmas ty loc2 t
- | Loc loc -> stored sigmas ty loc2 (pointer_val loc)
- end
- (**
- Return a set of equations that express a copy between two memory state.
-
- [copied sigma ty loc1 loc2] returns a set of formula expressing that the
- content for an object [ty] is the same in [sigma.pre] at [loc1] and in
- [sigma.post] at [loc2].
- *)
-
- let copied_init sigmas ty loc1 loc2 = (* TOCHECK *) match loc1, loc2 with
- | Left ll1, Left ll2 ->
- ML.copied_init (Product.sequence_left sigmas) ty ll1 ll2
- | Right lr1, Right lr2 ->
- MR.copied_init (Product.sequence_right sigmas) ty lr1 lr2
- | _,_ ->
- stored_init sigmas ty loc2 (load_init sigmas.pre ty loc1)
- (**
- Return a set of equations that express a copy of an initialized state
- between two memory state.
-
- [copied sigma ty loc1 loc2] returns a set of formula expressing that the
- initialization status for an object [ty] is the same in [sigma.pre] at
- [loc1] and in [sigma.post] at [loc2].
- *)
-
- let assigned sigma ty divergent_locs =
- match divergent_locs with
- (* loc_left *)
- | Sloc (Left ll) -> ML.assigned (Product.sequence_left sigma) ty (Sloc ll)
- | Sarray (Left ll, ty, size) -> ML.assigned (Product.sequence_left sigma) ty (Sarray (ll,ty,size))
- | Srange (Left ll, ty, inf, sup) -> ML.assigned (Product.sequence_left sigma) ty (Srange (ll, ty, inf, sup))
- | Sdescr (vars, Left ll, p) -> ML.assigned (Product.sequence_left sigma) ty (Sdescr (vars, ll, p))
- (* loc_right *)
- | Sloc (Right lr) -> MR.assigned (Product.sequence_right sigma) ty (Sloc lr)
- | Sarray (Right lr, ty, size) -> MR.assigned (Product.sequence_right sigma) ty (Sarray (lr,ty,size))
- | Srange (Right lr, ty, inf, sup) -> MR.assigned (Product.sequence_right sigma) ty (Srange (lr, ty, inf, sup))
- | Sdescr (vars, Right lr, p) -> MR.assigned (Product.sequence_right sigma) ty (Sdescr (vars, lr, p))
- (**
- Return a set of formula that express that two memory state are the same
- except at the given set of memory location.
-
- This function can over-approximate the set of given memory location (e.g
- it can return [true] as if the all set of memory location was given).
- *)
-
- let is_null l = D.is_null l
- (** Return the formula that check if a given location is null *)
-
- let loc_eq loc_a loc_b = (* TODO: déléguer le cas croisé à D ==> plutôt mettre assert false *)
- match loc_a, loc_b with
- | Right _, Left _| Left _, Right _ -> p_and (is_null loc_a) (is_null loc_b)
- | Left la, Left lb -> ML.loc_eq la lb
- | Right la, Right lb -> MR.loc_eq la lb
- let loc_lt loc_a loc_b = match loc_a, loc_b with
- | Right _, Left _| Left _, Right _ -> assert false
- | Left la, Left lb -> ML.loc_lt la lb
- | Right la, Right lb -> MR.loc_lt la lb
- let loc_neq loc_a loc_b = (* TODO: déléguer le cas croisé à D ==> plutôt mettre assert false *)
- match loc_a, loc_b with
- | Right _, Left _| Left _, Right _ -> p_or (p_not (is_null loc_a)) (p_not (is_null loc_b))
- | Left la, Left lb -> ML.loc_neq la lb
- | Right la, Right lb -> MR.loc_neq la lb
- let loc_leq loc_a loc_b = match loc_a, loc_b with
- | Right _, Left _| Left _, Right _ -> assert false
- | Left la, Left lb -> ML.loc_leq la lb
- | Right la, Right lb -> MR.loc_leq la lb
- (** Memory location comparisons *)
-
- let loc_diff ty loc_a loc_b = match loc_a, loc_b with
- | Right _, Left _| Left _, Right _ -> assert false
- | Left la, Left lb -> ML.loc_diff ty la lb
- | Right la, Right lb -> MR.loc_diff ty la lb
- (** Compute the length in bytes between two memory locations *)
-
- let valid sigma acs = function
- (* loc_left *)
- | Rloc (ty, Left ll) -> ML.valid sigma.left acs (Rloc (ty,ll))
- | Rrange (Left ll, ty, inf, sup) -> ML.valid sigma.left acs (Rrange (ll, ty, inf, sup))
- (* loc_right *)
- | Rloc (ty, Right lr) -> MR.valid sigma.right acs (Rloc (ty,lr))
- | Rrange (Right lr, ty, inf, sup) -> MR.valid sigma.right acs (Rrange (lr, ty, inf, sup))
- (** 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 sigma = List.append (ML.frame sigma.left) (MR.frame sigma.right)
- (** Assert the memory is a proper heap state preceeding the function
- entry point. *)
-
- let alloc sigma vars =
- let (varl, varr) = partition D.cvar vars in
- Product.map2 (fun s -> ML.alloc s varl) (fun s -> MR.alloc s varr) sigma
- (** Allocates new chunk for the validity of variables. *)
-
- let initialized sigma segment =
- match segment with
- (* loc_left *)
- | Rloc (ty, Left ll) -> ML.initialized sigma.left (Rloc (ty,ll))
- | Rrange (Left ll, ty, inf, sup) -> ML.initialized sigma.left (Rrange (ll, ty, inf, sup))
- (* loc_right *)
- | Rloc (ty, Right lr) -> MR.initialized sigma.right (Rloc (ty,lr))
- | Rrange (Right lr, ty, inf, sup) -> MR.initialized sigma.right (Rrange (lr, ty, inf, sup))
- (** Return the formula that tests if a memory state is initialized
- (according to {!acs}) in the given memory state at the given
- segment.
- *)
-
- let invalid sigma = function
- (* loc_left *)
- | Rloc (ty, Left l) -> ML.invalid sigma.left (Rloc (ty,l))
- | Rrange (Left l, ty, inf, sup) -> ML.invalid sigma.left (Rrange (l, ty, inf, sup))
- (* loc_right *)
- | Rloc (ty, Right l) -> MR.invalid sigma.right (Rloc (ty,l))
- | Rrange (Right l, ty, inf, sup) -> MR.invalid sigma.right (Rrange (l, ty, inf, sup))
-
- (** Returns the formula that tests if the entire memory is invalid
- for write access. *)
-
- let scope sigma scope vars =
- let (varl, varr) = partition D.cvar vars in
- List.append
- (ML.scope (Product.sequence_left sigma) scope varl)
- (MR.scope (Product.sequence_right sigma) scope varr)
- (** Manage the scope of variables. Returns the updated memory model
- and hypotheses modeling the new validity-scope of the variables. *)
-
- let global sigma p =
- p_and (ML.global sigma.left p) (MR.global sigma.right 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 s1 s2 = (* TODO: dans la construction des range, multiplier la taille de tau1 ou tau2 (ici o1 ou o2) *) match s1, s2 with
- (* loc_left x2 *)
- | Rloc (ty1, Left ll1), Rloc (ty2, Left ll2) ->
- ML.included (Rloc (ty1, ll1)) (Rloc (ty2, ll2))
- | Rloc (ty1, Left ll1), Rrange (Left ll2, ty2, inf, sup) ->
- ML.included (Rloc (ty1,ll1)) (Rrange (ll2,ty2,inf,sup))
- | Rrange (Left ll1, ty1, inf, sup), Rloc (ty2, Left ll2) ->
- ML.included (Rrange (ll1,ty1,inf,sup)) (Rloc (ty2,ll2))
- | Rrange (Left ll1, ty1, inf1, sup1), Rrange (Left ll2, ty2, inf2, sup2) ->
- ML.included (Rrange (ll1,ty1,inf1,sup1)) (Rrange (ll2,ty2,inf2,sup2))
- (* loc_right x2 *)
- | Rloc (ty1, Right lr1), Rloc (ty2, Right lr2) ->
- MR.included (Rloc (ty1, lr1)) (Rloc (ty2, lr2))
- | Rloc (ty1, Right lr1), Rrange (Right lr2, ty2, inf, sup) ->
- MR.included (Rloc (ty1,lr1)) (Rrange (lr2,ty2,inf,sup))
- | Rrange (Right ll1, ty1, inf, sup), Rloc (ty2, Right ll2) ->
- MR.included (Rrange (ll1,ty1,inf,sup)) (Rloc (ty2,ll2))
- | Rrange (Right lr1, ty1, inf1, sup1), Rrange (Right lr2, ty2, inf2, sup2) ->
- MR.included (Rrange (lr1,ty1,inf1,sup1)) (Rrange (lr2,ty2,inf2,sup2))
- (* Cross case: Rloc x Rloc *)
- | Rloc (tyl, Left ll), Rloc (tyr, Right lr) ->
- p_and (ML.is_null ll) (MR.included (Rloc (tyl, MR.null)) (Rloc (tyr, lr)))
- | Rloc (tyr, Right lr), Rloc (tyl, Left ll) ->
- p_and (MR.is_null lr) (ML.included (Rloc (tyr, ML.null)) (Rloc (tyl, ll)))
- (* Cross case: Rloc x Rrange *)
- | Rloc (tyl, Left ll), Rrange (Right lr, tyr, infr, supr) ->
- p_and (ML.is_null ll) (MR.included (Rloc (tyl, MR.null)) (Rrange (lr, tyr, infr, supr)))
- | Rloc (tyr, Right lr), Rrange (Left ll, tyl, infl, supl) ->
- p_and (MR.is_null lr) (ML.included (Rloc (tyr, ML.null)) (Rrange (ll, tyl, infl, supl)))
- (* Cross case: Rrange x Rloc *)
- | Rrange (Right lr, tyr, infr, supr), Rloc (tyl, Left ll) ->
- let r_range : set = [ Range (infr, supr) ] in
- p_or (Vset.is_empty r_range) (
- p_and
- (ML.is_null (ML.base_addr ll))
- (MR.included (Rrange (lr, tyr, infr, supr)) (Rloc (tyl, MR.null)))
- )
- | Rrange (Left ll, tyl, infl, supl), Rloc (tyr, Right lr) ->
- let l_range : set = [ Range (infl, supl) ] in
- p_or (Vset.is_empty l_range) (
- p_and
- (MR.is_null (MR.base_addr lr))
- (ML.included (Rrange (ll, tyl, infl, supl)) (Rloc (tyr, ML.null)))
- )
- (* Cross case: Rrange x Rrange *)
- | Rrange (Right lr, _tyr, infr, supr), Rrange (Left ll, _tyl, infl, supl) ->
- let r_range : set = [ Range (infr, supr) ] in
- let l_range : set = [ Range (infl, supl) ] in
- (* TOCHECK: should we unify tyl and tyr ? *)
- p_or (Vset.is_empty r_range) (
- p_and (ML.is_null (ML.base_addr ll)) (
- p_and (MR.is_null (MR.base_addr lr))
- (subset r_range l_range)
- ))
- | Rrange (Left ll, _tyl, infl, supl), Rrange (Right lr, _tyr, infr, supr) ->
- let r_range : set = [ Range (infr, supr) ] in
- let l_range : set = [ Range (infl, supl) ] in
- (* TOCHECK: should we unify tyl and tyr ? *)
- p_or (Vset.is_empty l_range) (
- p_and (ML.is_null (ML.base_addr ll)) (
- p_and (MR.is_null (MR.base_addr lr))
- (subset l_range r_range)
- ))
- (* Rrange left + la..lb , Rrange right + ra..rb ->
- construire des range avec Vset et faire les tests avec Vset
- (is_empty la lb)
- \/ (ML.is_null (base_addr l)
- /\ MR.is_null (base_addr r)
- /\ la..lb included in ra..rb) *)
- (* Rloc left , Rrange right + ra..rb
- -> ML.is_null left /\ MR.is_null right /\ 0 \in ra..rb *)
- (** Return the formula that tests if two segment are included *)
-
- let separated s1 s2 = match s1, s2 with
- (* loc_left x2 *)
- | Rloc (ty1, Left ll1), Rloc (ty2, Left ll2) ->
- ML.separated (Rloc (ty1, ll1)) (Rloc (ty2, ll2))
- | Rloc (ty1, Left ll1), Rrange (Left ll2, ty2, inf, sup) ->
- ML.separated (Rloc (ty1,ll1)) (Rrange (ll2,ty2,inf,sup))
- | Rrange (Left ll2, ty2, inf, sup), Rloc (ty1, Left ll1) ->
- ML.separated (Rrange (ll2,ty2,inf,sup)) (Rloc (ty1,ll1))
- | Rrange (Left ll1, ty1, inf1, sup1), Rrange (Left ll2, ty2, inf2, sup2) ->
- ML.separated (Rrange (ll1,ty1,inf1,sup1)) (Rrange (ll2,ty2,inf2,sup2))
- (* loc_right x2 *)
- | Rloc (ty1, Right lr1), Rloc (ty2, Right lr2) ->
- MR.separated (Rloc (ty1, lr1)) (Rloc (ty2, lr2))
- | Rloc (ty1, Right lr1), Rrange (Right lr2, ty2, inf, sup) ->
- MR.separated (Rloc (ty1,lr1)) (Rrange (lr2,ty2,inf,sup))
- | Rrange (Right lr2, ty2, inf, sup), Rloc (ty1, Right lr1) ->
- MR.separated (Rrange (lr2,ty2,inf,sup)) (Rloc (ty1,lr1))
- | Rrange (Right lr1, ty1, inf1, sup1), Rrange (Right lr2, ty2, inf2, sup2) ->
- MR.separated (Rrange (lr1,ty1,inf1,sup1)) (Rrange (lr2,ty2,inf2,sup2))
- (* Cross case: Rloc x Rloc *)
- | Rloc (tyl, Left ll), Rloc (tyr, Right lr) ->
- p_imply (ML.is_null ll) (MR.separated (Rloc (tyl, MR.null)) (Rloc (tyr, lr)))
- | Rloc (tyr, Right lr), Rloc (tyl, Left ll) ->
- p_imply (MR.is_null lr) (ML.separated (Rloc (tyr, ML.null)) (Rloc (tyl, ll)))
- (* Cross case: Rloc x Rrange *)
- | Rloc (tyl, Left ll), Rrange (Right lr, tyr, infr, supr) ->
- p_imply (ML.is_null ll) (MR.separated (Rloc (tyl, MR.null)) (Rrange (lr, tyr, infr, supr)))
- | Rloc (tyr, Right lr), Rrange (Left ll, tyl, infl, supl) ->
- p_imply (MR.is_null lr) (ML.separated (Rloc (tyr, ML.null)) (Rrange (ll, tyl, infl, supl)))
- (* Cross case: Rrange x Rloc *)
- | Rrange (Right lr, tyr, infr, supr), Rloc (tyl, Left ll) ->
- let r_range : set = [ Range (infr, supr) ] in
- p_or (Vset.is_empty r_range) (
- p_and (ML.is_null (ML.base_addr ll)) (MR.included (Rrange (lr, tyr, infr, supr)) (Rloc (tyl, MR.null)))
- )
- | Rrange (Left ll, tyl, infl, supl), Rloc (tyr, Right lr) ->
- let l_range : set = [ Range (infl, supl) ] in
- p_or (Vset.is_empty l_range) (
- p_and (MR.is_null (MR.base_addr lr)) (ML.included (Rrange (ll, tyl, infl, supl)) (Rloc (tyr, ML.null)))
- )
- (* Cross case: Rrange x Rrange *)
- | Rrange (Right lr, _tyr, infr, supr), Rrange (Left ll, _tyl, infl, supl) ->
- let r_range : set = [ Range (infr, supr) ] in
- let l_range : set = [ Range (infl, supl) ] in
- (* TOCHECK: should we unify tyl and tyr ? *)
- p_or (Vset.is_empty r_range) (
- p_and (ML.is_null (ML.base_addr ll)) (
- p_and (MR.is_null (MR.base_addr lr)) (subset r_range l_range)
- ))
- | Rrange (Left ll, _tyl, infl, supl), Rrange (Right lr, _tyr, infr, supr) ->
- let r_range : set = [ Range (infr, supr) ] in
- let l_range : set = [ Range (infl, supl) ] in
- (* TOCHECK: should we unify tyl and tyr ? *)
- p_or (Vset.is_empty l_range) (
- p_and (ML.is_null (ML.base_addr ll)) (
- p_and (MR.is_null (MR.base_addr lr)) (subset l_range r_range)
- ))
- (** Return the formula that tests if two segment are separated *)
-
-end
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index 46d62359db3..6c9818e7da5 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -54,8 +54,10 @@ sig
val value_footprint: c_object -> loc -> Sigma.domain
val init_footprint: c_object -> loc -> Sigma.domain
+ (* toutes les fils qui ne sont pas des points_to *)
val frames : c_object -> loc -> Chunk.t -> frame list
+ (* memBytes *)
val last : Sigma.t -> c_object -> loc -> term
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 473a678b004..661422e6d96 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -1265,3 +1265,19 @@ let updates seq domain =
!pool
(* -------------------------------------------------------------------------- *)
+
+let sizeof = MODEL.sizeof
+let last = MODEL.last
+let havoc = MODEL.havoc
+let sizeof_havoc _ _ = F.e_one
+let eqmem_forall = MODEL.eqmem_forall
+let load_int = MODEL.load_int
+let load_float = MODEL.load_float
+let load_pointer = MODEL.load_pointer
+let store_int = MODEL.store_int
+let store_float = MODEL.store_float
+let store_pointer = MODEL.store_pointer
+let set_init_atom = MODEL.set_init_atom
+let set_init = MODEL.set_init
+let is_init_atom = MODEL.is_init_atom
+let is_init_range = MODEL.is_init_range
diff --git a/src/plugins/wp/MemTyped.mli b/src/plugins/wp/MemTyped.mli
index ccdbfbd0b97..fe4a3929d5f 100644
--- a/src/plugins/wp/MemTyped.mli
+++ b/src/plugins/wp/MemTyped.mli
@@ -20,6 +20,11 @@
(* *)
(**************************************************************************)
+open Cil_types
+open Ctypes
+open Lang.F
+open Sigs
+
(* -------------------------------------------------------------------------- *)
(* --- Typed Memory Model --- *)
(* -------------------------------------------------------------------------- *)
@@ -28,3 +33,30 @@ include Sigs.Model
type pointer = NoCast | Fits | Unsafe
val pointer : pointer Context.value
+
+
+val sizeof : c_object -> 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
+val sizeof_havoc : c_object -> loc -> term
+
+val eqmem_forall : c_object -> loc -> chunk -> term -> term -> var list * pred * pred
+
+val load_int : sigma -> c_int -> loc -> term
+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 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
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
new file mode 100644
index 00000000000..7028c992e2b
--- /dev/null
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -0,0 +1,224 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Ctypes
+open Lang.F
+
+
+(* -------------------------------------------------------------------------- *)
+(* --- Region Analysis API for Bornat Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+module type API = sig
+ type region
+ val null : unit -> region
+
+
+ val hash : region -> int
+ val equal : region -> region -> bool
+ val compare : region -> region -> int
+ val pretty : Format.formatter -> region -> unit
+
+ type primitive = | Int of c_int | Float of c_float | Ptr
+ type kind = Single of primitive | Many of primitive | Garbled
+ val kind : region -> kind
+ val pp_kind : Format.formatter -> kind -> unit
+
+ 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 literal : eid:int -> Cstring.cst -> region option
+ val pointer_loc : unit -> region option
+ val loc_of_int : unit -> region option
+
+ val id_of_region : region -> int
+ val region_of_id : int -> region option
+end
+
+
+(* -------------------------------------------------------------------------- *)
+(* --- Region Analysis for Bornat Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+module R (*: API*) =
+struct
+
+ type region = Region.node
+
+ let get_map () = match WpContext.get_scope () with
+ | WpContext.Kf f -> Region.get_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 id_of_region region = Region.get_uid (get_map ()) region
+
+ let region_of_id id =
+ try Some (Region.get_node (get_map ()) id)
+ with Not_found -> None
+
+ let hash = Region.get_id
+
+ let equal r1 r2 = (Region.get_id r1 = Region.get_id r2)
+
+ let compare r1 r2 = Int.compare (Region.get_id r1) (Region.get_id r2)
+
+ let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.get_id r
+
+ type primitive = | Int of c_int | Float of c_float | Ptr
+ type kind = Single of primitive | Many of primitive | Garbled
+
+ let pp_primitive fmt = function
+ | Int i -> Ctypes.pp_int fmt i
+ | Float f -> Ctypes.pp_float fmt f
+ | Ptr -> Format.pp_print_string fmt "void*"
+ let pp_kind fmt = function
+ | Many p -> Format.fprintf fmt "[%a]" pp_primitive p
+ | Single p -> pp_primitive fmt p
+ | Garbled -> Format.pp_print_string fmt "Garbled"
+
+ module CollectionCObject = Qed.Collection.Make(struct
+ type t = Ctypes.c_object
+ let compare = Ctypes.compare
+ let hash = Ctypes.hash
+ let equal = Ctypes.equal
+ end)
+
+ module CObjects = CollectionCObject.Set
+
+ let types r =
+ let map = get_map () in
+ let add_type set ty = CObjects.add (Ctypes.object_of ty) set in
+ let types = CObjects.empty in
+ let types = List.fold_left add_type types @@ Region.reads map r in
+ let types = List.fold_left add_type types @@ Region.writes map r in
+ let types = List.fold_left add_type types @@ Region.shifts map r in
+ types
+
+ (** Internal handling of region kinds *)
+ module KindCompile = struct
+ (* Data : WpContext.Data with type key = Key.t *)
+ type key = region
+ type data = kind
+ let name = "WP.RegionAnalysis.R"
+ let compile region : kind = match CObjects.elements @@ types region with
+ | [] ->
+ Warning.emit ~severe:false ~source:"RegionAnalysis.KindCompile.compile"
+ ~effect:"Access type list is empty" "%a" pretty region ;
+ Garbled
+ | [ Ctypes.C_int cint ] -> Many (Int cint)
+ | [ Ctypes.C_float cfloat ] -> Many (Float cfloat)
+ | [ Ctypes.C_pointer _ ] -> Many Ptr
+ | [ Ctypes.C_comp _ ] -> Garbled
+ | [ Ctypes.C_array _ ] -> Garbled
+ | _ :: _ :: _ -> Garbled
+ end
+
+
+ (* Keeping track of the decision to apply which memory model to each region *)
+ module Kind = WpContext.Generator(struct
+ (* Key : WPContext.Key *)
+ type t = region
+ let compare = compare
+ let pretty = pretty
+ end)(KindCompile)
+
+ let kind = Kind.get
+
+
+ let tau_of_region region : tau = match CObjects.elements @@ types region with
+ | _ :: _ :: _ ->
+ Warning.emit ~severe:false ~source:"RegionAnalysis.tau_of_region"
+ ~effect:"Access type list is more than a singleton" "%a" pretty region ;
+ assert false
+ | [] ->
+ Warning.emit ~severe:false ~source:"RegionAnalysis.tau_of_region"
+ ~effect:"Access type list is empty" "%a" pretty region ;
+ assert false
+ | [ ty ] -> Lang.tau_of_object ty
+
+ let points_to region = Region.points_to (get_map ()) region
+
+ (*
+
+ if not (Layout.fits ~dst:s.post ~src:s.pre) then
+ Warning.emit ~severe:false ~source:"Region Memory Model"
+ ~effect:"Keep pointer value"
+ "%a" pp_mismatch s ; l
+
+
+ *)
+
+ 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
+
+ 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 pretty region;
+ 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 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 base_addr _ = assert false
+ let literal ~eid _ = ignore eid ; assert false
+ let pointer_loc () = assert false
+ let loc_of_int () = assert false
+
+end
diff --git a/src/plugins/wp/MemDispatch.mli b/src/plugins/wp/RegionAnalysis.mli
similarity index 61%
rename from src/plugins/wp/MemDispatch.mli
rename to src/plugins/wp/RegionAnalysis.mli
index d7915d23a39..057c8124af2 100644
--- a/src/plugins/wp/MemDispatch.mli
+++ b/src/plugins/wp/RegionAnalysis.mli
@@ -20,10 +20,46 @@
(* *)
(**************************************************************************)
+open Cil_types
+open Ctypes
+open Lang.F
+
(* -------------------------------------------------------------------------- *)
-(* --- Empty Memory Model --- *)
+(* --- Region Analysis API for Bornat Memory Model --- *)
(* -------------------------------------------------------------------------- *)
-open Dispatcher
+module type API = sig
+ type region
+ val null : unit -> region
+
+
+ val hash : region -> int
+ val equal : region -> region -> bool
+ val compare : region -> region -> int
+ val pretty : Format.formatter -> region -> unit
+
+ type primitive = | Int of c_int | Float of c_float | Ptr
+ type kind = Single of primitive | Many of primitive | Garbled
+ val kind : region -> kind
+ val pp_kind : Format.formatter -> kind -> unit
+
+ 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 literal : eid:int -> Cstring.cst -> region option
+ val pointer_loc : unit -> region option
+ val loc_of_int : unit -> region option
+
+ val id_of_region : region -> int
+ val region_of_id : int -> region option
+end
-module Make(_: Dispatcher) : Sigs.Model
+module R : API
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index eba61ce0010..1ea4a065fff 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -315,6 +315,7 @@ let rec object_of typ =
C_int (c_int IInt)
| TNamed (r,_) -> object_of r.ttype
+
(* ------------------------------------------------------------------------ *)
(* --- Comparable --- *)
(* ------------------------------------------------------------------------ *)
@@ -384,10 +385,36 @@ let () =
cmp := compare ;
end
+(* -------------------------------------------------------------------------- *)
+(* --- 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 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) *), [])]
+
+
(* -------------------------------------------------------------------------- *)
(* --- Accessor Utilities --- *)
(* -------------------------------------------------------------------------- *)
+
let object_of_pointed = function
C_int _ | C_float _ | C_comp _ as o ->
Wp_parameters.fatal
diff --git a/src/plugins/wp/ctypes.mli b/src/plugins/wp/ctypes.mli
index f38d4d05826..96664cfbe06 100644
--- a/src/plugins/wp/ctypes.mli
+++ b/src/plugins/wp/ctypes.mli
@@ -98,6 +98,7 @@ val c_float : fkind -> c_float
(** Conforms to {!Machine.theMachine} *)
val object_of : typ -> c_object
+val object_to : c_object -> typ list
val is_pointer : c_object -> bool
diff --git a/src/plugins/wp/gui/GuiPanel.ml b/src/plugins/wp/gui/GuiPanel.ml
index 4b25d1880a9..50025d407fd 100644
--- a/src/plugins/wp/gui/GuiPanel.ml
+++ b/src/plugins/wp/gui/GuiPanel.ml
@@ -99,7 +99,7 @@ let run_and_prove
(* --- Model Panel --- *)
(* ------------------------------------------------------------------------ *)
-type memory = TREE | HOARE | TYPED | EVA | BYTES
+type memory = TREE | HOARE | TYPED | EVA | BYTES | BORNAT
class model_selector (main : Design.main_window_extension_points) =
let dialog = new Wpane.dialog
@@ -152,6 +152,7 @@ class model_selector (main : Design.main_window_extension_points) =
| Typed m -> memory#set TYPED ; c_casts#set (m = MemTyped.Unsafe)
| Eva -> memory#set EVA
| Bytes -> memory#set BYTES
+ | Bornat -> memory#set BORNAT
) ;
c_byref#set (s.mvar = Ref) ;
c_ctxt#set (s.mvar = Caveat) ;
@@ -167,6 +168,7 @@ class model_selector (main : Design.main_window_extension_points) =
(if c_casts#get then MemTyped.Unsafe else MemTyped.Fits)
| EVA -> Eva
| BYTES -> Bytes
+ | BORNAT -> Bornat
in {
mheap = m ;
mvar = if c_ctxt#get then Caveat else if c_byref#get then Ref else Var ;
--
GitLab