[wp] refactor matrix loaders

src/plugins/wp/Cvalues.ml

@@ -168,17 +168,24 @@ struct
          })
       [s]
 
-  and is_array te ds t =
+  and is_array elt ds t =
     Definitions.call_pred
-      (Lang.generated_p (array_name te ds))
+      (Lang.generated_p (array_name elt ds))
       (fun lfun ->
-         let x = Lang.freshvar ~basename:"T" (Matrix.tau te ds) in
-         let ks = List.map (fun _d -> Lang.freshvar ~basename:"k" Logic.Int) ds in
+         let cluster =
+           match elt with
+           | C_comp c -> Definitions.compinfo c
+           | _ -> Definitions.matrix () in
+         let te = Lang.tau_of_object elt in
+         let d = List.length ds in
+         let x = Lang.freshvar ~basename:"T" (Lang.t_matrix te d) in
+         let fk _d = Lang.freshvar ~basename:"k" Logic.Int in
+         let ks = List.map fk ds in
          let e = List.fold_left (fun a k -> e_get a (e_var k)) (e_var x) ks in
-         let def = p_forall ks (is_obj te e) in
+         let def = p_forall ks (is_obj elt e) in
          {
            d_lfun = lfun ; d_types = 0 ; d_params = [x] ;
-           d_cluster = Definitions.matrix te ;
+           d_cluster = cluster ;
            d_definition = Predicate(Def,def) ;
          }
       ) [t]
@@ -250,34 +257,68 @@ let rec reduce_eqcomp = function
 (* --- ACSL Array Equality                                                --- *)
 (* -------------------------------------------------------------------------- *)
 
-module EQARRAY = WpContext.Generator(Matrix.NATURAL)
+module AKEY =
+struct
+  type t = base * Matrix.t
+  and base = I | F of c_float | P | C of compinfo
+  let make elt ds =
+    let base = match elt with
+      | C_int _ -> I
+      | C_float f -> F f
+      | C_pointer _ -> P
+      | C_comp c -> C c
+      | C_array _ -> assert false
+    in base , ds
+  let key = function
+    | I -> "int"
+    | P -> "ptr"
+    | F f -> Ctypes.f_name f
+    | C c -> Lang.comp_id c
+  let cluster = function
+    | I | P | F _ -> Definitions.matrix ()
+    | C c -> Definitions.compinfo c
+  let tau = function
+    | I -> Lang.t_int
+    | F f -> Lang.t_float f
+    | P -> Lang.t_addr ()
+    | C c -> Lang.t_comp c
+  let equal = function
+    | I | F _ | P -> F.p_equal
+    | C c -> !equal_rec (C_comp c)
+  let compare (a,p) (b,q) =
+    let cmp = String.compare (key a) (key b) in
+    if cmp <> 0 then cmp else Matrix.compare p q
+  let pretty fmt (a,ds) =
+    Format.fprintf fmt "%s%a" (key a) Matrix.pp_suffix_id ds
+end
+
+module EQARRAY = WpContext.Generator(AKEY)
     (struct
-      open Matrix
       let name = "Cvalues.EqArray"
-      type key = matrix
+      type key = AKEY.t
       type data = lfun
-      let compile (te,ds) =
+      let compile (a,ds) =
         (* Contextual Symbol *)
         let lfun = Lang.generated_f
             ~context:true
             ~sort:Logic.Sprop
-            "EqArray%s_%s" (Matrix.id ds) (Matrix.natural_id te) in
+            "EqArray_%s%a" (AKEY.key a) Matrix.pp_suffix_id ds in
         (* Simplification of the symbol *)
         Lang.F.set_builtin lfun reduce_eqcomp ;
         (* Definition of the symbol *)
-        let denv = Matrix.denv ds in
-        let tau = Matrix.tau te ds in
+        let denv = Matrix.cc_env ds in
+        let tau = Matrix.cc_tau (AKEY.tau a) ds in
         let xa = Lang.freshvar ~basename:"T" tau in
         let xb = Lang.freshvar ~basename:"T" tau in
         let ta = e_var xa in
         let tb = e_var xb in
         let ta_xs = List.fold_left e_get ta denv.index_val in
         let tb_xs = List.fold_left e_get tb denv.index_val in
-        let property = p_hyps (denv.index_range) (!equal_rec te ta_xs tb_xs) in
+        let property = p_hyps (denv.index_range) (AKEY.equal a ta_xs tb_xs) in
         let definition = p_forall denv.index_var property in
         (* Registration *)
         Definitions.define_symbol {
-          d_cluster = Definitions.matrix te ;
+          d_cluster = AKEY.cluster a ;
           d_lfun = lfun ; d_types = 0 ;
           d_params = denv.size_var @ [xa ; xb ] ;
           d_definition = Predicate(Def,definition) ;
@@ -324,17 +365,20 @@ module EQCOMP = WpContext.Generator(Cil_datatype.Compinfo)
 (* --- ACSL Equality                                                      --- *)
 (* -------------------------------------------------------------------------- *)
 
+type matrixinfo = c_object * int option list
+
 let equal_comp c a b = p_call (EQCOMP.get c) [a;b]
 let equal_array m a b =
-  match m with
-  | _obj , [None] -> p_equal a b
-  | m -> p_call (EQARRAY.get m) (Matrix.size m @ [a;b])
+  let elt,ns = m in
+  let ds = Matrix.of_dims ns in
+  let ms = Matrix.cc_dims ns in
+  p_call (EQARRAY.get @@ AKEY.make elt ds) (ms @ [a;b])
 
 let equal_object obj a b =
   match obj with
   | C_int _ | C_float _ | C_pointer _ -> p_equal a b
   | C_comp c -> equal_comp c a b
-  | C_array t -> equal_array (Matrix.of_array t) a b
+  | C_array m -> equal_array (Ctypes.array_dimensions m) a b
 
 let () = equal_rec := equal_object
 

src/plugins/wp/Cvalues.mli

@@ -83,9 +83,11 @@ val volatile : ?warn:string -> unit -> bool
 
 (** {2 ACSL Equality} *)
 
+type matrixinfo = c_object * int option list
+
 val equal_object : c_object -> term -> term -> pred
 val equal_comp : compinfo -> term -> term -> pred
-val equal_array : Matrix.matrix -> term -> term -> pred
+val equal_array : matrixinfo -> term -> term -> pred
 
 (** {2 C and ACSL Constants} *)
 

src/plugins/wp/Definitions.ml

@@ -27,7 +27,6 @@
 open LogicUsage
 open Cil_types
 open Cil_datatype
-open Ctypes
 open Qed.Logic
 open Lang
 open Lang.F
@@ -255,11 +254,7 @@ let icompinfo c =
        in cluster.c_irecords <- [c] ; cluster)
     (Lang.comp_init_id c)
 
-let matrix = function
-  | C_array _ -> assert false
-  | C_comp c -> compinfo c
-  | C_int _ | C_float _ | C_pointer _ ->
-      cluster ~id:"Matrix" ~title:"Basic Arrays" ()
+let matrix () = cluster ~id:"Matrix" ~title:"Basic Arrays" ()
 
 let call_fun ~result lfun cc es =
   Symbol.compile (Lang.local cc) lfun ;

src/plugins/wp/Definitions.mli

@@ -22,7 +22,6 @@
 
 open LogicUsage
 open Cil_types
-open Ctypes
 open Lang
 open Lang.F
 
@@ -33,7 +32,7 @@ val cluster : id:string -> ?title:string -> ?position:Filepath.position -> unit
 val axiomatic : axiomatic -> cluster
 val section : logic_section -> cluster
 val compinfo : compinfo -> cluster
-val matrix : c_object -> cluster
+val matrix : unit -> cluster
 
 val cluster_id : cluster -> string (** Unique *)
 val cluster_title : cluster -> string

src/plugins/wp/LogicSemantics.ml

@@ -274,10 +274,12 @@ struct
     | EQ_loc
     | EQ_plain
     | EQ_float of c_float
-    | EQ_array of Matrix.matrix
+    | EQ_array of matrixinfo
     | EQ_comp of compinfo
     | EQ_incomparable
 
+  and matrixinfo = c_object * int option list
+
   let eqsort_of_type t =
     match Logic_utils.unroll_type ~unroll_typedef:false t with
     | Ltype({lt_name="set"},[_]) -> EQ_set
@@ -288,7 +290,7 @@ struct
         | C_int _ -> EQ_plain
         | C_float f -> EQ_float f
         | C_comp c -> EQ_comp c
-        | C_array a -> EQ_array (Matrix.of_array a)
+        | C_array a -> EQ_array (Ctypes.array_dimensions a)
 
   let eqsort_of_comparison a b =
     match eqsort_of_type a.term_type , eqsort_of_type b.term_type with
@@ -296,7 +298,7 @@ struct
     | EQ_loc , EQ_loc -> EQ_loc
     | EQ_comp c1 , EQ_comp c2 ->
         if Compinfo.equal c1 c2 then EQ_comp c1 else EQ_incomparable
-    | EQ_array (t1,d1) , EQ_array (t2,d2) ->
+    | EQ_array(t1,d1) , EQ_array(t2,d2) ->
         if Ctypes.equal t1 t2 then
           match Matrix.merge d1 d2 with
           | Some d -> EQ_array(t1,d)

src/plugins/wp/Matrix.ml

@@ -24,83 +24,49 @@
 (* --- Array Dimensions                                                   --- *)
 (* -------------------------------------------------------------------------- *)
 
-open Ctypes
+(* private *)
+type t = [ `Fix | `Ext ] list
+
+let of_dims = List.map (function None -> `Ext | Some _ -> `Fix)
+
+let compare (ps : t) (qs : t) = Stdlib.compare ps qs
+
+let rec pp_hdims fmt = function
+  | [] -> ()
+  | `Fix :: ps -> pp_ndims `Fix 1 fmt ps
+  | `Ext :: ps -> pp_ndims `Ext 1 fmt ps
+
+and pp_ndims p k fmt = function
+  | q :: qs when p = q -> pp_ndims p (succ k) fmt qs
+  | ps -> pp_kdim p k fmt ; pp_hdims fmt ps
+
+and pp_kdim p k fmt =
+  begin
+    if p = `Fix then Format.pp_print_char fmt 'd' ;
+    if p = `Ext then Format.pp_print_char fmt 'w' ;
+    if k > 1 then Format.pp_print_int fmt k ;
+  end
+
+let pp_suffix_id fmt = function
+  | [] | [`Fix] -> ()
+  | ps -> Format.pp_print_char fmt '_' ; pp_hdims fmt ps
+
+let pretty fmt ps = pp_hdims fmt ps
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compilation Environment                                            --- *)
+(* -------------------------------------------------------------------------- *)
+
 open Lang.F
 
-type dim = int option
-type matrix = c_object * dim list
-
-let of_array = Ctypes.array_dimensions
-
-module KEY(E : sig val compare : c_object -> c_object -> int end) =
-struct
-  type t = matrix
-
-  let compare_dim d1 d2 = match d1 , d2 with
-    | None,None -> 0
-    | Some _,None -> (-1)
-    | None,Some _ -> 1
-    | Some _,Some _ -> 0
-
-  let compare (e1,ds1) (e2,ds2) =
-    let cmp = E.compare e1 e2 in
-    if cmp = 0 then Qed.Hcons.compare_list compare_dim ds1 ds2 else cmp
-
-  let pretty fmt (obj,ds) =
-    Ctypes.pretty fmt obj ;
-    List.iter
-      (function
-        | None -> Format.pp_print_string fmt "[]"
-        | Some d -> Format.fprintf fmt "[%d]" d
-      ) ds
-end
-
-module COBJ =
-struct
-  let compare e1 e2 = match e1 , e2 with
-    | C_int _ , C_int _ -> 0
-    | C_int _ , _ -> (-1)
-    | _ , C_int _ -> 1
-    | C_float _ , C_float _ -> 0
-    | C_float _ , _ -> (-1)
-    | _ , C_float _ -> 1
-    | C_pointer _ , C_pointer _ -> 0
-    | C_pointer _ , _ -> (-1)
-    | _ , C_pointer _ -> 1
-    | C_comp a , C_comp b -> Cil_datatype.Compinfo.compare a b
-    | C_comp _ , _ -> (-1)
-    | _ , C_comp _ -> 1
-    | C_array _ , C_array _ -> assert false
-end
-
-module MACHINE = KEY(Ctypes)
-module NATURAL = KEY(COBJ)
-
-let natural_id = function
-  | C_int _ -> "int"
-  | C_float _ -> "float"
-  | C_pointer _ -> "pointer"
-  | C_array _ -> "array"
-  | C_comp c -> Lang.comp_id c
-
-let add_rank buffer k = if k > 0 then Buffer.add_string buffer (string_of_int k)
-let add_dim buffer rank = function
-  | None -> add_rank buffer rank ; Buffer.add_string buffer "w" ; 0
-  | Some _ -> succ rank
-
-let id ds =
-  let buffer = Buffer.create 8 in
-  add_rank buffer (List.fold_left (add_dim buffer) 0 ds) ;
-  Buffer.contents buffer
-
-type denv = {
+type env = {
   size_var : var list ; (* size variables *)
   size_val : term list ; (* size values *)
   index_var : var list ; (* index variables *)
   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 ;
+  index_offset : term list ; (* polynomial of indices multiplied by previous sizes *)
+  monotonic : bool ; (* all dimensions are fixed *)
 }
 
 let rec collect rank = function
@@ -121,14 +87,14 @@ let rec collect rank = function
       let k_val = e_var k_var in
       let k_ofs = e_prod (k_val :: denv.size_val) in
       match d with
-      | None ->
+      | `Ext ->
           { denv with
             index_var = k_var :: denv.index_var ;
             index_val = k_val :: denv.index_val ;
             index_offset = k_ofs :: denv.index_offset ;
             monotonic = false ;
           }
-      | Some _ ->
+      | `Fix ->
           let n_base = match rank with 0 -> "n" | 1 -> "m" | _ -> "d" in
           let n_var = Lang.freshvar ~basename:n_base Qed.Logic.Int in
           let n_val = e_var n_var in
@@ -144,20 +110,19 @@ let rec collect rank = function
             monotonic = denv.monotonic ;
           }
 
-let denv = collect 0
+let cc_env = collect 0
 
-let rec dval = function
+let rec cc_dims ns =
+  match ns with
   | [] -> []
-  | None :: ds -> dval ds
-  | Some n :: ds -> e_int n :: dval ds
-let size (_,ds) = dval ds
+  | Some n :: ns -> e_int n :: cc_dims ns
+  | None :: ns -> cc_dims ns
 
-let rec kind on_leaf obj = function
-  | [] -> on_leaf obj
-  | _ :: ds -> Qed.Logic.Array( Qed.Logic.Int , kind on_leaf obj ds )
+let cc_tau te ds = Lang.t_matrix te (List.length ds)
 
-let tau = kind Lang.tau_of_object
-let init = kind Lang.init_of_object
+(* -------------------------------------------------------------------------- *)
+(* --- Dimension Merging                                                  --- *)
+(* -------------------------------------------------------------------------- *)
 
 let rec do_merge ds1 ds2 =
   match ds1 , ds2 with
@@ -172,3 +137,5 @@ let rec do_merge ds1 ds2 =
 let merge ds1 ds2 =
   try Some(do_merge ds1 ds2)
   with Exit -> None
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/Matrix.mli

@@ -24,22 +24,19 @@
 (* --- Array Dimensions                                                   --- *)
 (* -------------------------------------------------------------------------- *)
 
-open Ctypes
-open Lang.F
-
-type dim = int option
-type matrix = c_object * dim list
+type t (** Matrix dimensions.
+           Encodes the number of dimensions and their kind *)
 
-module MACHINE : WpContext.Key with type t = matrix
-module NATURAL : WpContext.Key with type t = matrix
+val of_dims : int option list -> t
+val compare : t -> t -> int
+val pretty : Format.formatter -> t -> unit
+val pp_suffix_id : Format.formatter -> t -> unit
 
-val of_array : arrayinfo -> matrix
-val id : dim list -> string (** unique w.r.t [equal] *)
-val natural_id : c_object -> string (** name for elements in NATURAL *)
+val merge : int option list -> int option list -> int option list option
 
-val merge : dim list -> dim list -> dim list option
+open Lang.F
 
-type denv = {
+type env = {
   size_var : var list ; (** size variables *)
   size_val : term list ; (** size values *)
   index_var : var list ; (** index variables *)
@@ -49,7 +46,8 @@ type denv = {
   monotonic : bool ; (** all dimensions are defined *)
 }
 
-val denv : dim list -> denv
-val size : matrix -> term list
-val tau : c_object -> dim list -> tau
-val init : c_object -> dim list -> tau
+val cc_tau : tau -> t -> tau (** Type of matrix *)
+val cc_env : t -> env (** Dimension environment *)
+val cc_dims : int option list -> term list (** Value of size variables *)
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/MemLoader.ml

@@ -217,46 +217,72 @@ struct
   (* ---  Array Loader                                                      --- *)
   (* -------------------------------------------------------------------------- *)
 
-  module ARRAY_KEY =
+  module AKEY =
   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
+    type t = int * base * Matrix.t
+    and base = I of c_int | F of c_float | P | C of compinfo
+    let make r elt ds =
+      let base = match elt with
+        | C_int i -> I i
+        | C_float f -> F f
+        | C_pointer _ -> P
+        | C_comp c -> C c
+        | C_array _ -> raise (Invalid_argument "Wp.EqArray")
+      in r, base , ds
+    let key = function
+      | I i -> Ctypes.i_name i
+      | F f -> Ctypes.f_name f
+      | P -> "ptr"
+      | C c -> Lang.comp_id c
+    let obj = function
+      | I i -> C_int i
+      | F f -> C_float f
+      | P -> C_pointer Cil.voidPtrType
+      | C c -> C_comp c
+    let tau = function
+      | I _ -> Lang.t_int
+      | F f -> Lang.t_float f
+      | P -> Lang.t_addr ()
+      | C c -> Lang.t_comp c
+    let compare (r,a,p) (s,b,q) =
+      if r = s then
+        let cmp = String.compare (key a) (key b) in
+        if cmp <> 0 then cmp else Matrix.compare p q
+      else r - s
+    let pretty fmt (r,a,ds) =
+      Format.fprintf fmt "%s%a%a" (key a) pp_rid r Matrix.pp_suffix_id ds
   end
 
-  module ARRAY = WpContext.Generator(ARRAY_KEY)
+  module ARRAY = WpContext.Generator(AKEY)
       (struct
         open Matrix
         let name = M.name ^ ".ARRAY"
-        type key = int * arrayinfo * Matrix.matrix
+        type key = AKEY.t
         type data = lfun * chunk list
 
-        let generate (r,ainfo,(obj_e,ds)) =
+        let generate (r,a,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.value_footprint obj_a loc in
-          let result = Matrix.tau obj_e ds in
+          let obj = AKEY.obj a in
+          let loc = M.of_region_pointer r obj v in (* t_pointer -> loc *)
+          let domain = M.value_footprint obj loc in
+          let result = Matrix.cc_tau (AKEY.tau a) ds in
           let lfun =
-            Lang.generated_f ~result "Array%a%s_%s"
-              pp_rid r (Matrix.id ds) (Matrix.natural_id obj_e)
-          in
+            Lang.generated_f ~result "Array%a_%s%a"
+              pp_rid r (AKEY.key a) Matrix.pp_suffix_id ds in
           let prefix = Lang.Fun.debug lfun in
           let name = 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 env = Matrix.cc_env ds in
+          let phi = e_fun lfun (v :: env.size_val @ List.map e_var xmem) in
+          let va = List.fold_left e_get phi env.index_val in
+          let ofs = e_sum env.index_offset in
+          let vm = !loadrec sigma obj (M.shift loc obj ofs) in
+          let lemma = p_hyps env.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_params = x :: env.size_var @ xmem ;
             d_definition = Logic result ;
             d_cluster = cluster ;
           } ;
@@ -268,10 +294,10 @@ struct
             l_lemma = lemma ;
             l_cluster = cluster ;
           } ;
-          if denv.monotonic then
+          if env.monotonic then
             begin
-              let ns = List.map F.e_var denv.size_var in
-              frame_lemmas lfun obj_a loc (v::ns) chunks
+              let ns = List.map F.e_var env.size_var in
+              frame_lemmas lfun obj loc (v::ns) chunks
             end ;
           lfun , chunks
 
@@ -288,10 +314,11 @@ struct
     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 e , ns = Ctypes.array_dimensions a in
+    let ds = Matrix.of_dims ns in
+    let f , m = ARRAY.get @@ AKEY.make r e ds in
+    F.e_fun f (p :: Matrix.cc_dims ns @ memories sigma m)
 
   let loadvalue sigma obj loc =
     match obj with
@@ -368,40 +395,39 @@ struct
         let compile = Lang.local generate
       end)
 
-  module ARRAYINIT = WpContext.Generator(ARRAY_KEY)
+  module IS_ARRAY_INIT = WpContext.Generator(AKEY)
       (struct
         open Matrix
-        let name = M.name ^ ".ARRAYINIT"
-        type key = int * arrayinfo * Matrix.matrix
+        let name = M.name ^ ".IS_ARRAY_INIT"
+        type key = AKEY.t
         type data = lfun * chunk list
 
-        let generate (r,ainfo,(obj_e,ds)) =
+        let generate (r,a,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.init_footprint obj_a loc in
-          let name = Format.asprintf "IsInitArray%a%s_%s"
-              pp_rid r (Matrix.id ds) (Matrix.natural_id obj_e)
-          in
+          let obj = AKEY.obj a in
+          let loc = M.of_region_pointer r obj v in
+          let domain = M.init_footprint obj loc in
+          let name = Format.asprintf "IsInitArray%a_%s%a"
+              pp_rid r (AKEY.key a) Matrix.pp_suffix_id ds in
           let lfun = Lang.generated_p name in
           let xmem,chunks,sigma = signature domain in
-          let denv = Matrix.denv ds in
-          let ofs = e_sum denv.index_offset in
-          let vm = !isinitrec sigma obj_e (M.shift loc obj_e ofs) in
-          let def = p_forall denv.index_var (