[wp] fixed init-range lemmas

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

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 *)

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