From f38cca53c28f7b615db93f72fc837d249f62b1dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 15 Oct 2020 13:50:50 +0200
Subject: [PATCH] [wp] fixed init-range lemmas
---
src/plugins/wp/Matrix.ml | 13 +++++---
src/plugins/wp/Matrix.mli | 2 +-
src/plugins/wp/MemLoader.ml | 61 +++++++++++++++++++++----------------
3 files changed, 43 insertions(+), 33 deletions(-)
diff --git a/src/plugins/wp/Matrix.ml b/src/plugins/wp/Matrix.ml
index e3774cc9949..4c4cdad80fc 100644
--- a/src/plugins/wp/Matrix.ml
+++ b/src/plugins/wp/Matrix.ml
@@ -66,7 +66,7 @@ type env = {
index_val : term list ; (* index values *)
index_range : pred list ; (* indices are in range of size variables *)
index_offset : term list ; (* polynomial of indices multiplied by previous sizes *)
- monotonic : bool ; (* all dimensions are fixed *)
+ length : term option ; (* number of array cells ; None is infinite *)
}
let rec collect rank = function
@@ -78,7 +78,7 @@ let rec collect rank = function
index_val = [] ;
index_range = [] ;
index_offset = [] ;
- monotonic = true ;
+ length = Some e_one ;
}
| d::ds ->
let denv = collect (succ rank) ds in
@@ -92,7 +92,7 @@ let rec collect rank = function
index_var = k_var :: denv.index_var ;
index_val = k_val :: denv.index_val ;
index_offset = k_ofs :: denv.index_offset ;
- monotonic = false ;
+ length = None ;
}
| `Fix ->
let n_base = match rank with 0 -> "n" | 1 -> "m" | _ -> "d" in
@@ -100,14 +100,17 @@ let rec collect rank = function
let n_val = e_var n_var in
let k_inf = p_leq e_zero k_val in
let k_sup = p_lt k_val n_val in
- {
+ let length = match denv.length with
+ | None -> None
+ | Some len -> Some (e_mul n_val len)
+ in {
size_var = n_var :: denv.size_var ;
size_val = n_val :: denv.size_val ;
index_var = k_var :: denv.index_var ;
index_val = k_val :: denv.index_val ;
index_offset = k_ofs :: denv.index_offset ;
index_range = k_inf :: k_sup :: denv.index_range ;
- monotonic = denv.monotonic ;
+ length ;
}
let cc_env = collect 0
diff --git a/src/plugins/wp/Matrix.mli b/src/plugins/wp/Matrix.mli
index d138d00ddc3..7ee7ac37f55 100644
--- a/src/plugins/wp/Matrix.mli
+++ b/src/plugins/wp/Matrix.mli
@@ -43,7 +43,7 @@ type env = {
index_val : term list ; (** index values *)
index_range : pred list ; (** indices are in range of size variables *)
index_offset : term list ; (** polynomial of indices *)
- monotonic : bool ; (** all dimensions are defined *)
+ length : term option ; (** number of cells (None is infinite) *)
}
val cc_tau : tau -> t -> tau (** Type of matrix *)
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 31a1bf4b891..62ef4a7efcc 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -294,7 +294,7 @@ struct
l_lemma = lemma ;
l_cluster = cluster ;
} ;
- if env.monotonic then
+ if env.length <> None then
begin
let ns = List.map F.e_var env.size_var in
frame_lemmas lfun obj loc (v::ns) chunks
@@ -345,19 +345,6 @@ struct
let isinitrec = ref (fun _ _ _ -> assert false)
- let initialization_lemma cluster name (sigma, obj, loc) (lfun, params) =
- let high = p_call lfun (List.map F.e_var params) in
- let low = M.is_init_range sigma obj loc e_one in
- let lemma = p_equiv high low in
- {
- l_kind = `Axiom ;
- l_name = name ^ "_low" ; l_types = 0 ;
- l_forall = F.p_vars lemma ;
- l_triggers = [] ;
- l_lemma = lemma ;
- l_cluster = cluster ;
- }
-
module IS_INIT_COMP = WpContext.Generator(COMP_KEY)
(struct
let name = M.name ^ ".IS_INIT_COMP"
@@ -366,30 +353,39 @@ struct
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 loc = M.of_region_pointer r obj (e_var x) in
let domain = M.init_footprint obj loc in
let cluster = cluster () in
- (* Function Is_init *)
+ (* Is_init: structural definition *)
let name =
Format.asprintf "Is%s%a" (Lang.comp_init_id c) pp_rid r
in
let lfun = Lang.generated_p name in
let xms,chunks,sigma = signature domain in
+ let params = x :: xms in
let def = p_all
(fun f -> !isinitrec sigma (object_of f.ftype) (M.field loc f))
c.cfields
in
Definitions.define_symbol {
d_lfun = lfun ; d_types = 0 ;
- d_params = x :: xms ;
+ d_params = params ;
d_definition = Predicate(Def , def) ;
d_cluster = cluster ;
} ;
- (* Lemma for low-level view of the memory *)
- Definitions.define_lemma
- (initialization_lemma cluster name (sigma,obj,loc) (lfun,x::xms)) ;
+ (* Is_init: full-range definition *)
+ let is_init_p = p_call lfun (List.map e_var (x :: xms)) in
+ let is_init_r = M.is_init_range sigma obj loc e_one in
+ let lemma = p_equiv is_init_p is_init_r in
+ Definitions.define_lemma {
+ l_kind = `Axiom ;
+ l_name = name ^ "_range" ; l_types = 0 ;
+ l_forall = params ;
+ l_triggers = [] ;
+ l_lemma = lemma ;
+ l_cluster = cluster ;
+ } ;
lfun , chunks
let compile = Lang.local generate
@@ -413,21 +409,32 @@ struct
let lfun = Lang.generated_p name in
let xmem,chunks,sigma = signature domain in
let env = Matrix.cc_env ds in
+ let params = x :: env.size_var @ xmem in
let ofs = e_sum env.index_offset in
let vm = !isinitrec sigma obj (M.shift loc obj ofs) in
let def = p_forall env.index_var (p_hyps env.index_range vm) in
let cluster = cluster () in
+ (* Is_init: structural definition *)
Definitions.define_symbol {
d_lfun = lfun ; d_types = 0 ;
- d_params = x :: env.size_var @ xmem ;
+ d_params = params ;
d_definition = Predicate (Def, def) ;
d_cluster = cluster ;
} ;
- (* Lemma for low-level view of the memory *)
- Definitions.define_lemma
- (initialization_lemma cluster name
- (sigma, obj, loc)
- (lfun, x :: env.size_var @ xmem)) ;
+ (* Is_init: range definition *)
+ begin match env.length with None -> () | Some len ->
+ let is_init_p = p_call lfun (List.map e_var params) in
+ let is_init_r = M.is_init_range sigma obj loc len in
+ let lemma = p_equiv is_init_p is_init_r in
+ Definitions.define_lemma {
+ l_kind = `Axiom ;
+ l_name = name ^ "_range" ; l_types = 0 ;
+ l_forall = params ;
+ l_triggers = [] ;
+ l_lemma = lemma ;
+ l_cluster = cluster ;
+ }
+ end ;
lfun , chunks
let compile = Lang.local generate
--
GitLab