From e1c474de860e782657786827a01cd68ceafe35ee Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 21 Jul 2020 13:38:15 +0200
Subject: [PATCH] [wp] Changes hypotheses signature
---
src/plugins/wp/MemEmpty.ml | 2 +-
src/plugins/wp/MemRegion.ml | 2 +-
src/plugins/wp/MemTyped.ml | 2 +-
src/plugins/wp/MemVar.ml | 6 +++---
src/plugins/wp/MemZeroAlias.ml | 2 +-
src/plugins/wp/Sigs.ml | 7 ++++---
src/plugins/wp/register.ml | 3 ++-
src/plugins/wp/wpContext.ml | 7 ++++---
src/plugins/wp/wpContext.mli | 4 ++--
9 files changed, 19 insertions(+), 16 deletions(-)
diff --git a/src/plugins/wp/MemEmpty.ml b/src/plugins/wp/MemEmpty.ml
index 5435ab551b6..837d3f28f39 100644
--- a/src/plugins/wp/MemEmpty.ml
+++ b/src/plugins/wp/MemEmpty.ml
@@ -43,7 +43,7 @@ let configure () =
let no_binder = { bind = fun _ f v -> f v }
let configure_ia _ = no_binder
-let hypotheses () = []
+let hypotheses p = p
module Chunk =
struct
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 3723ce42322..def850d503e 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -441,7 +441,7 @@ let configure_ia =
let no_binder = { bind = fun _ f v -> f v } in
fun _vertex -> no_binder
-let hypotheses () = []
+let hypotheses p = p
let error msg = Warning.error ~source:"Region Model" msg
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 6743fc7a086..9ef4f43ed45 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -42,7 +42,7 @@ module L = Qed.Logic
(* -------------------------------------------------------------------------- *)
let datatype = "MemTyped"
-let hypotheses () = []
+let hypotheses p = p
let configure () =
begin
let orig_pointer = Context.push Lang.pointer (fun _ -> t_addr) in
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 7a395b0e59f..7d07665c6be 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -52,11 +52,11 @@ struct
let no_binder = { bind = fun _ f v -> f v }
let configure_ia _ = no_binder
- let hypotheses () =
+ let hypotheses p =
let kf,init = match WpContext.get_scope () with
| WpContext.Global -> None,false
| WpContext.Kf f -> Some f, WpStrategy.is_main_init f in
- let w = ref MemoryContext.empty in
+ let w = ref p in
V.iter ?kf ~init (fun vi -> w := MemoryContext.set vi (V.param vi) !w) ;
let add_assign kf _emitter = function
| WritesAny ->
@@ -72,7 +72,7 @@ struct
| Some kf ->
Annotations.iter_assigns (add_assign kf) kf Cil.default_behavior_name
end ;
- MemoryContext.requires !w @ M.hypotheses ()
+ M.hypotheses !w
(* -------------------------------------------------------------------------- *)
(* --- Chunk --- *)
diff --git a/src/plugins/wp/MemZeroAlias.ml b/src/plugins/wp/MemZeroAlias.ml
index 3300bf555d9..3e185883a6d 100644
--- a/src/plugins/wp/MemZeroAlias.ml
+++ b/src/plugins/wp/MemZeroAlias.ml
@@ -48,7 +48,7 @@ let no_binder = { bind = fun _ f v -> f v }
let configure_ia _ = no_binder
(* TODO: compute actual separation hypotheses *)
-let hypotheses () = []
+let hypotheses p = p
(* -------------------------------------------------------------------------- *)
(* --- Chunks --- *)
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 98754486ae4..bc4f14f098b 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -291,9 +291,10 @@ sig
val datatype : string
(** For projectification. Must be unique among models. *)
- val hypotheses : unit -> MemoryContext.clause list
- (** Computes the memory model hypotheses including separation and validity
- clauses to be verified for this model. *)
+ val hypotheses : MemoryContext.partition -> MemoryContext.partition
+ (** 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). *)
module Chunk : Chunk
(** Memory model chunks. *)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index c350f0f5779..bb54e4da628 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -105,7 +105,8 @@ let wp_warn_memory_context () =
begin
wp_iter_model
begin fun kf m ->
- let hyp = WpContext.compute_hypotheses m kf in
+ let partition = WpContext.compute_hypotheses m kf in
+ let hyp = MemoryContext.requires partition in
if hyp <> [] then
Wp_parameters.warning
~current:false
diff --git a/src/plugins/wp/wpContext.ml b/src/plugins/wp/wpContext.ml
index b37368f1378..acc32631cad 100644
--- a/src/plugins/wp/wpContext.ml
+++ b/src/plugins/wp/wpContext.ml
@@ -34,11 +34,11 @@ type model = {
and rollback = (unit -> unit)
and scope = Global | Kf of Kernel_function.t
-and hypotheses = unit -> MemoryContext.clause list
+and hypotheses = MemoryContext.partition -> MemoryContext.partition
and context = model * scope
and t = context
-let nohyp (_kf) = []
+let nohyp (_kf) = MemoryContext.empty
module MODEL =
struct
@@ -149,7 +149,8 @@ let get_context () = Context.get context |> snd
let get_model () = get_context () |> fst
let get_scope () = get_context () |> snd
-let compute_hypotheses m f = on_context (m,Kf f) m.hypotheses ()
+let compute_hypotheses m f =
+ on_context (m,Kf f) m.hypotheses MemoryContext.empty
let directory () = get_model () |> MODEL.id |> Wp_parameters.get_output_dir
diff --git a/src/plugins/wp/wpContext.mli b/src/plugins/wp/wpContext.mli
index 7693815595f..a52c5af5f7f 100644
--- a/src/plugins/wp/wpContext.mli
+++ b/src/plugins/wp/wpContext.mli
@@ -25,7 +25,7 @@
type model
type scope = Global | Kf of Kernel_function.t
type rollback = unit -> unit
-type hypotheses = unit -> MemoryContext.clause list
+type hypotheses = MemoryContext.partition -> MemoryContext.partition
val register :
id:string ->
@@ -44,7 +44,7 @@ val register :
val get_descr : model -> string
val get_emitter : model -> Emitter.t
-val compute_hypotheses : model -> Kernel_function.t -> MemoryContext.clause list
+val compute_hypotheses : model -> Kernel_function.t -> MemoryContext.partition
type context = model * scope
type t = context
--
GitLab