diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 536e8d2c9c8ba5d81f399c5acd2ea78861fc6c04..f0c4e42477c13c469e62ed6ef2307b7492ac817c 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1408,6 +1408,8 @@ src/plugins/wp/MemoryContext.ml: CEA_WP
src/plugins/wp/MemoryContext.mli: CEA_WP
src/plugins/wp/MemEmpty.ml: CEA_WP
src/plugins/wp/MemEmpty.mli: CEA_WP
+src/plugins/wp/MemLoader.ml: CEA_WP
+src/plugins/wp/MemLoader.mli: CEA_WP
src/plugins/wp/MemTyped.ml: CEA_WP
src/plugins/wp/MemTyped.mli: CEA_WP
src/plugins/wp/MemVar.ml: CEA_WP
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 2ba8603148d81bef9b2ec9b53360ab91c4c5bf55..97ab4e5e7ccc7b273ca0deb225bb116d48873d88 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -176,7 +176,7 @@ let t_int = Logic.Int
let t_bool = Logic.Bool
let t_real = Logic.Real
let t_prop = Logic.Prop
-let t_addr () = Context.get pointer (Cil_types.TVoid [])
+let t_addr () = Context.get pointer Cil.voidType
let t_array a = Logic.Array(Logic.Int,a)
let t_farray a b = Logic.Array(a,b)
let t_datatype adt ts = Logic.Data(adt,ts)
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index af9ac3bb08b228a2aed5effed33e13389dfdddff..7ef00de80b20a5fd7a7905706a7a05b7666afac2 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -162,7 +162,7 @@ val t_int : tau
val t_real : tau
val t_bool : tau
val t_prop : tau
-val t_addr : unit -> tau
+val t_addr : unit -> tau (** pointer on Void *)
val t_array : tau -> tau
val t_farray : tau -> tau -> tau
val t_datatype : adt -> tau list -> tau
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 4fed7ec6a85f4c349759b0f59b7cefef24b54c4e..b43a9ba9384e19c262b705d4de3bab97ce20ba5b 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -80,7 +80,8 @@ PLUGIN_CMO:= \
CodeSemantics \
LogicCompiler \
LogicSemantics LogicAssigns \
- Sigma MemEmpty MemZeroAlias MemVar MemTyped \
+ Sigma MemLoader \
+ MemEmpty MemZeroAlias MemVar MemTyped \
wpStrategy wpRTE wpAnnot \
CfgCompiler StmtSemantics \
VCS script proof wpo wpReport \
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
new file mode 100644
index 0000000000000000000000000000000000000000..bfe4d75df24c91bf60afe227a14a1cdfc1dc59f3
--- /dev/null
+++ b/src/plugins/wp/MemLoader.ml
@@ -0,0 +1,372 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+open Cil_types
+open Cil_datatype
+open Definitions
+open Ctypes
+open Lang
+open Lang.F
+open Sigs
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compound Loader --- *)
+(* -------------------------------------------------------------------------- *)
+
+let cluster () =
+ Definitions.cluster ~id:"Compound" ~title:"Memory Compound Loader" ()
+
+type frame = string * Definitions.trigger list * pred list * term * term
+
+module type Model =
+sig
+
+ module Chunk : Chunk
+ module Sigma : Sigma with type chunk = Chunk.t
+
+ val name : string
+
+ type loc
+ val sizeof : c_object -> int
+ val field : loc -> fieldinfo -> loc
+ val shift : loc -> c_object -> term -> loc
+
+ val to_addr : loc -> term
+ val to_region_pointer : loc -> int * term
+ val of_region_pointer : int -> c_object -> term -> loc
+
+ val domain : c_object -> loc -> Sigma.domain
+ val frames : c_object -> loc -> Chunk.t -> frame list
+
+ val last : Sigma.t -> c_object -> loc -> term
+
+ val havoc : c_object -> loc -> length:term ->
+ Chunk.t -> fresh:term -> current:term -> term
+
+ val eqmem : c_object -> loc -> Chunk.t -> term -> term -> pred
+
+ val eqmem_forall :
+ c_object -> loc -> Chunk.t -> term -> term -> var list * pred * pred
+
+ val load_int : Sigma.t -> c_int -> loc -> term
+ val load_float : Sigma.t -> c_float -> loc -> term
+ val load_pointer : Sigma.t -> typ -> loc -> loc
+
+ val store_int : Sigma.t -> c_int -> loc -> term -> Chunk.t * term
+ val store_float : Sigma.t -> c_float -> loc -> term -> Chunk.t * term
+ val store_pointer : Sigma.t -> typ -> loc -> term -> Chunk.t * term
+
+end
+
+module Make (M : Model) =
+struct
+
+ type chunk = M.Chunk.t
+
+ module Chunk = M.Chunk
+ module Sigma = M.Sigma
+ module Domain = M.Sigma.Chunk.Set
+
+ let signature ft =
+ let s = Sigma.create () in
+ let xs = ref [] in
+ let cs = ref [] in
+ Domain.iter
+ (fun c ->
+ cs := c :: !cs ;
+ xs := (Sigma.get s c) :: !xs ;
+ ) ft ;
+ List.rev !xs , List.rev !cs , s
+
+ let pp_rid fmt r = if r <> 0 then Format.fprintf fmt "_R%03d" r
+
+ let loadrec = ref (fun _ _ _ -> assert false)
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Frame Lemmas for Compound Access --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ let memories sigma chunks = List.map (Sigma.value sigma) chunks
+ let assigned sigma c m chunks =
+ List.map
+ (fun c0 -> if Chunk.equal c0 c then m else Sigma.value sigma c0)
+ chunks
+
+ let frame_lemmas phi obj loc params chunks =
+ begin
+ let prefix = Fun.debug phi in
+ let sigma = Sigma.create () in
+ List.iter
+ (fun chunk ->
+ List.iter
+ (fun (name,triggers,conditions,m1,m2) ->
+ let mem1 = assigned sigma chunk m1 chunks in
+ let mem2 = assigned sigma chunk m2 chunks in
+ let value1 = e_fun phi (params @ mem1) in
+ let value2 = e_fun phi (params @ mem2) in
+ let vars1 = F.vars value1 in
+ let vars2 = F.vars value2 in
+ let l_triggers =
+ if Vars.subset vars1 vars2 then
+ [ (Trigger.of_term value2 :: triggers ) ]
+ else
+ if Vars.subset vars2 vars1 then
+ [ (Trigger.of_term value1 :: triggers ) ]
+ else
+ [ (Trigger.of_term value1 :: triggers );
+ (Trigger.of_term value2 :: triggers ) ]
+ in
+ let l_name = Pretty_utils.sfprintf "%s_%s_%a"
+ prefix name Chunk.pretty chunk in
+ let l_lemma = F.p_hyps conditions (p_equal value1 value2) in
+ Definitions.define_lemma {
+ l_assumed = true ;
+ l_name ; l_types = 0 ;
+ l_triggers ;
+ l_forall = F.p_vars l_lemma ;
+ l_lemma = l_lemma ;
+ l_cluster = cluster () ;
+ }
+ ) (M.frames obj loc chunk)
+ ) chunks
+ end
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Compound Loader --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ module COMP_KEY =
+ struct
+ type t = int * compinfo
+ let compare (r,c) (r',c') = if r=r' then Compinfo.compare c c' else r-r'
+ let pretty fmt (r,c) = Format.fprintf fmt "%d:%a" r Compinfo.pretty c
+ end
+
+ module COMP = Model.Generator(COMP_KEY)
+ (struct
+ let name = M.name ^ ".COMP"
+ type key = int * compinfo
+ type data = lfun * chunk list
+
+ let generate (r,c) =
+ let x = Lang.freshvar ~basename:"p" (Lang.t_addr()) in
+ let v = e_var x in
+ let obj = C_comp c in
+ let loc = M.of_region_pointer r obj v in (* t_pointer -> loc *)
+ let domain = M.domain obj loc in
+ let result = Lang.tau_of_comp c in
+ let lfun = Lang.generated_f ~result "Load%a_%s" pp_rid r (Lang.comp_id c) in
+ (* Since its a generated it is the unique name given *)
+ let xms,chunks,sigma = signature domain in
+ let def = List.map
+ (fun f ->
+ Cfield f , !loadrec sigma (object_of f.ftype) (M.field loc f)
+ ) c.cfields in
+ let dfun = Definitions.Function( result , Def , e_record def ) in
+ Definitions.define_symbol {
+ d_lfun = lfun ; d_types = 0 ;
+ d_params = x :: xms ;
+ d_definition = dfun ;
+ d_cluster = cluster () ;
+ } ;
+ frame_lemmas lfun obj loc [v] chunks ;
+ lfun , chunks
+
+ let compile = Lang.local generate
+ end)
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Array Loader --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ module ARRAY_KEY =
+ struct
+ type t = int * arrayinfo * Matrix.matrix
+ let pretty fmt (r,_,m) =
+ Format.fprintf fmt "%d:%a" r Matrix.NATURAL.pretty m
+ let compare (r1,_,m1) (r2,_,m2) =
+ if r1 = r2 then Matrix.NATURAL.compare m1 m2 else r1-r2
+ end
+
+ module ARRAY = Model.Generator(ARRAY_KEY)
+ (struct
+ open Matrix
+ let name = M.name ^ ".ARRAY"
+ type key = int * arrayinfo * Matrix.matrix
+ type data = lfun * chunk list
+
+ let generate (r,ainfo,(obj_e,ds)) =
+ let x = Lang.freshvar ~basename:"p" (Lang.t_addr()) in
+ let v = e_var x in
+ let obj_a = C_array ainfo in
+ let loc = M.of_region_pointer r obj_a v in (* t_pointer -> loc *)
+ let domain = M.domain obj_a loc in
+ let result = Matrix.tau obj_e ds in
+ let lfun = Lang.generated_f ~result "Array%a%s_%s" pp_rid r
+ (Matrix.id ds) (Matrix.natural_id obj_e) in
+ let prefix = Lang.Fun.debug lfun in
+ let axiom = prefix ^ "_access" in
+ let xmem,chunks,sigma = signature domain in
+ let denv = Matrix.denv ds in
+ let phi = e_fun lfun (v :: denv.size_val @ List.map e_var xmem) in
+ let va = List.fold_left e_get phi denv.index_val in
+ let ofs = e_sum denv.index_offset in
+ let vm = !loadrec sigma obj_e (M.shift loc obj_e ofs) in
+ let lemma = p_hyps denv.index_range (p_equal va vm) in
+ let cluster = cluster () in
+ Definitions.define_symbol {
+ d_lfun = lfun ; d_types = 0 ;
+ d_params = x :: denv.size_var @ xmem ;
+ d_definition = Logic result ;
+ d_cluster = cluster ;
+ } ;
+ Definitions.define_lemma {
+ l_assumed = true ;
+ l_name = axiom ; l_types = 0 ;
+ l_forall = F.p_vars lemma ;
+ l_triggers = [[Trigger.of_term va]] ;
+ l_lemma = lemma ;
+ l_cluster = cluster ;
+ } ;
+ if denv.monotonic then
+ begin
+ let ns = List.map F.e_var denv.size_var in
+ frame_lemmas lfun obj_a loc (v::ns) chunks
+ end ;
+ lfun , chunks
+
+ let compile = Lang.local generate
+ end)
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Loader --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ let load_comp sigma comp loc =
+ let r , p = M.to_region_pointer loc in
+ let f , m = COMP.get (r,comp) in
+ F.e_fun f (p :: memories sigma m)
+
+ let load_array sigma a loc =
+ let d = Matrix.of_array a in
+ let r , p = M.to_region_pointer loc in
+ let f , m = ARRAY.get (r,a,d) in
+ F.e_fun f (p :: Matrix.size d @ memories sigma m)
+
+ let loadvalue sigma obj loc =
+ match obj with
+ | C_int i -> M.load_int sigma i loc
+ | C_float f -> M.load_float sigma f loc
+ | C_pointer t -> snd @@ M.to_region_pointer @@ M.load_pointer sigma t loc
+ | C_comp c -> load_comp sigma c loc
+ | C_array a -> load_array sigma a loc
+
+ let load sigma obj loc =
+ let open Sigs in
+ match obj with
+ | C_int i -> Val (M.load_int sigma i loc)
+ | C_float f -> Val (M.load_float sigma f loc)
+ | C_pointer t -> Loc (M.load_pointer sigma t loc)
+ | C_comp c -> Val (load_comp sigma c loc)
+ | C_array a -> Val (load_array sigma a loc)
+
+ let () = loadrec := loadvalue
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Havocs --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ let havoc_length s obj loc length =
+ let ps = ref [] in
+ Domain.iter
+ (fun chunk ->
+ let pre = Sigma.value s.pre chunk in
+ let post = Sigma.value s.post chunk in
+ let tau = Chunk.tau_of_chunk chunk in
+ let basename = Chunk.basename_of_chunk chunk ^ "_undef" in
+ let fresh = F.e_var (Lang.freshvar ~basename tau) in
+ let havoc = M.havoc obj loc ~length chunk ~fresh ~current:pre in
+ ps := Set(post,havoc) :: !ps
+ ) (M.domain obj loc) ; !ps
+
+ let havoc seq obj loc = havoc_length seq obj loc F.e_one
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Stored & Copied --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ let updated seq phi alpha loc value =
+ let chunk,mem = phi seq.pre alpha loc value in
+ [Set(Sigma.value seq.post chunk,mem)]
+
+ let stored seq obj loc value =
+ match obj with
+ | C_int i -> updated seq M.store_int i loc value
+ | C_float f -> updated seq M.store_float f loc value
+ | C_pointer ty -> updated seq M.store_pointer ty loc value
+ | C_comp _ | C_array _ ->
+ Set(loadvalue seq.post obj loc, value) :: havoc seq obj loc
+
+ let copied s obj p q = stored s obj p (loadvalue s.pre obj q)
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Assigned --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ let assigned_loc seq obj loc =
+ match obj with
+ | C_int _ | C_float _ | C_pointer _ ->
+ let x = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
+ stored seq obj loc (e_var x)
+ | C_comp _ | C_array _ ->
+ havoc seq obj loc
+
+ let assigned_range s obj l a b =
+ havoc_length s obj (M.shift l obj a) (e_range a b)
+
+ let assigned seq obj = function
+ | Sloc loc -> assigned_loc seq obj loc
+ | Sdescr(xs,loc,condition) ->
+ let ps = ref [] in
+ Domain.iter
+ (fun c ->
+ let m1 = Sigma.value seq.pre c in
+ let m2 = Sigma.value seq.post c in
+ let p,separated,equal = M.eqmem_forall obj loc c m1 m2 in
+ let sep_from_all = F.p_forall xs (F.p_imply condition separated) in
+ let phi = F.p_forall p (F.p_imply sep_from_all equal) in
+ ps := Assert phi :: !ps
+ ) (M.domain obj loc) ; !ps
+ | Sarray(loc,obj,n) ->
+ assigned_range seq obj loc e_zero (e_int (n-1))
+ | Srange(loc,obj,u,v) ->
+ let a = match u with Some a -> a | None -> e_zero in
+ let b = match v with Some b -> b | None -> M.last seq.pre obj loc in
+ assigned_range seq obj loc a b
+
+ (* -------------------------------------------------------------------------- *)
+
+end
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
new file mode 100644
index 0000000000000000000000000000000000000000..6f94c256955700557f6736215d5e40c72eacb6ae
--- /dev/null
+++ b/src/plugins/wp/MemLoader.mli
@@ -0,0 +1,105 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+
+(** Compound Loader *)
+
+open Cil_types
+open Definitions
+open Ctypes
+open Lang.F
+open Sigs
+
+val cluster : unit -> cluster
+
+(** Frame Conditions.
+ Consider a function [phi(m)] over memory [m],
+ we want memories [m1,m2] and condition [p] such that
+ [p(m1,m2) -> phi(m1) = phi(m2)].
+ - [name] used for generating lemma
+ - [triggers] for the lemma
+ - [conditions] for the frame lemma to hold
+ - [mem1,mem2] to two memories for which the lemma holds *)
+type frame = string * Definitions.trigger list * pred list * term * term
+
+(** Loader Model for Atomic Values *)
+module type Model =
+sig
+
+ module Chunk : Chunk
+ module Sigma : Sigma with type chunk = Chunk.t
+
+ val name : string
+
+ type loc
+ val sizeof : c_object -> int
+ val field : loc -> fieldinfo -> loc
+ val shift : loc -> c_object -> term -> loc
+
+ (** Conversion among loc, t_pointer terms and t_addr terms *)
+
+ val to_addr : loc -> term
+ val to_region_pointer : loc -> int * term
+ val of_region_pointer : int -> c_object -> term -> loc
+
+ val domain : c_object -> loc -> Sigma.domain
+ val frames : c_object -> loc -> Chunk.t -> frame list
+
+ val last : Sigma.t -> c_object -> loc -> term
+
+ val havoc : c_object -> loc -> length:term ->
+ Chunk.t -> fresh:term -> current:term -> term
+
+ val eqmem : c_object -> loc -> Chunk.t -> term -> term -> pred
+
+ val eqmem_forall :
+ c_object -> loc -> Chunk.t -> term -> term -> var list * pred * pred
+
+ val load_int : Sigma.t -> c_int -> loc -> term
+ val load_float : Sigma.t -> c_float -> loc -> term
+ val load_pointer : Sigma.t -> typ -> loc -> loc
+
+ val store_int : Sigma.t -> c_int -> loc -> term -> Chunk.t * term
+ val store_float : Sigma.t -> c_float -> loc -> term -> Chunk.t * term
+ val store_pointer : Sigma.t -> typ -> loc -> term -> Chunk.t * term
+
+end
+
+(** Generates Loader for Compound Values *)
+module Make (M : Model) :
+sig
+
+ val load : M.Sigma.t -> c_object -> M.loc -> M.loc Sigs.value
+ val loadvalue : M.Sigma.t -> c_object -> M.loc -> term
+
+ val havoc : M.Sigma.t sequence -> c_object -> M.loc -> equation list
+ val havoc_length : M.Sigma.t sequence -> c_object -> M.loc -> term -> equation list
+
+ val stored : M.Sigma.t sequence -> c_object -> M.loc -> term -> equation list
+ val copied : M.Sigma.t sequence -> c_object -> M.loc -> M.loc -> equation list
+
+ val assigned : M.Sigma.t sequence -> c_object -> M.loc sloc -> equation list
+
+end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index abb143b4dd2872da790be41d66b6c547d067f3bc..414d5f49fcf816bd1527a34e6482704930e20e5b 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -34,7 +34,6 @@ open Definitions
let dkey_layout = Wp_parameters.register_category "layout"
-
module L = Qed.Logic
let datatype = "MemTyped"
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index d451e04f15fcb2003abd1d85c6769e6a4afc1da0..6fc72a241aaea9e0a3f4c1e465d17c476d787977 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -135,6 +135,7 @@ sig
type t
val self : string (** Chunk names, for pretty-printing. *)
val hash : t -> int
+ val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit