Commit f6ccfe17 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'fix/wp/matrix-name-clash' into 'master'

[wp] fix matrix name clash

See merge request frama-c/frama-c!2900
parents cfee9261 08b3a7ae
......@@ -126,17 +126,14 @@ struct
let array_name te ds =
let dim = List.length ds in
let pp_dim fmt d = if d > 1 then Format.fprintf fmt "_d%d" d in
match te with
| C_int i ->
Format.asprintf "%sArray%d_%a" C.prefix dim model_int i
| C_float _ ->
Format.asprintf "%sArray%d_float" C.prefix dim
| C_pointer _ ->
Format.asprintf "%sArray%d_pointer" C.prefix dim
Format.asprintf "%sArray%a_%a" C.prefix pp_dim dim model_int i
| C_comp c ->
Format.asprintf "%sArray%d%s" C.prefix dim (Lang.comp_id c)
| C_array _ ->
Wp_parameters.fatal "Unflatten array (%s %a)" C.prefix Ctypes.pretty te
Format.asprintf "%sArray%a_%s" C.prefix pp_dim dim (Lang.comp_id c)
| C_float _ | C_pointer _ | C_array _ ->
assert false
let rec is_obj obj t =
match obj with
......@@ -159,7 +156,7 @@ struct
(Lang.generated_p (C.prefix ^ Lang.comp_id c))
(fun lfun ->
let basename = if c.cstruct then "S" else "U" in
let s = Lang.freshvar ~basename (Lang.tau_of_comp c) in
let s = Lang.freshvar ~basename (Lang.t_comp c) in
let def = p_all
(fun f ->
is_typ f.ftype (e_getfield (e_var s) (Lang.Cfield (f, KValue))))
......@@ -171,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]
......@@ -253,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) ;
......@@ -303,8 +341,9 @@ module EQCOMP = WpContext.Generator(Cil_datatype.Compinfo)
Lang.F.set_builtin lfun reduce_eqcomp ;
(* Definition of the symbol *)
let basename = if c.cstruct then "S" else "U" in
let xa = Lang.freshvar ~basename (Lang.tau_of_comp c) in
let xb = Lang.freshvar ~basename (Lang.tau_of_comp c) in
let tc = Lang.t_comp c in
let xa = Lang.freshvar ~basename tc in
let xb = Lang.freshvar ~basename tc in
let ra = e_var xa in
let rb = e_var xb in
let def = p_all
......@@ -326,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
......
......@@ -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} *)
......
......@@ -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 ;
......
......@@ -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
......
......@@ -180,38 +180,37 @@ let sort_of_ltype t = match Logic_utils.unroll_type ~unroll_typedef:false t with
| Linteger -> Logic.Sint
| Lreal -> Logic.Sreal
let tau_of_comp c = Logic.Data(Comp (c, KValue),[])
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.voidType
let t_addr () = Context.get pointer
let t_float f = Context.get floats f
let t_comp c = Logic.Data(Comp (c, KValue),[])
let t_init c = Logic.Data(Comp (c, KInit), [])
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)
let rec t_matrix a n = if n > 0 then t_matrix (t_array a) (pred n) else a
let rec tau_of_object = function
| C_int _ -> Logic.Int
| C_float f -> Context.get floats f
| C_pointer t -> Context.get pointer t
| C_comp c -> tau_of_comp c
| C_float f -> t_float f
| C_pointer _ -> Context.get pointer
| C_comp c -> t_comp c
| C_array { arr_element = typ } -> t_array (tau_of_ctype typ)
and tau_of_ctype typ = tau_of_object (Ctypes.object_of typ)
let init_of_comp c = Logic.Data(Comp (c, KInit), [])
let poly = Context.create "Wp.Lang.poly"
let rec init_of_object = function
| C_int _ | C_float _ | C_pointer _ -> Logic.Bool
| C_comp c -> init_of_comp c
| C_comp c -> t_init c
| C_array { arr_element = typ } -> t_array (init_of_ctype typ)
and init_of_ctype typ = init_of_object (Ctypes.object_of typ)
let rec varpoly k x = function
| [] -> Warning.error "Unbound type parameter <%s>" x
| y::ys -> if x = y then k else varpoly (succ k) x ys
......@@ -370,8 +369,8 @@ let tau_of_field = function
let tau_of_record = function
| Mfield(mdt,fs,_,_) -> Logic.Data(Mrecord(mdt,fs),[])
| Cfield(f, KValue) -> tau_of_comp f.fcomp
| Cfield(f, KInit) -> init_of_comp f.fcomp
| Cfield(f, KValue) -> t_comp f.fcomp
| Cfield(f, KInit) -> t_init f.fcomp
module Field =
struct
......
......@@ -160,7 +160,6 @@ val extern_t:
(** {2 Sorting and Typing} *)
val tau_of_comp : compinfo -> tau
val tau_of_object : c_object -> tau
val tau_of_ctype : typ -> tau
val tau_of_ltype : logic_type -> tau
......@@ -169,7 +168,6 @@ val tau_of_lfun : lfun -> tau option list -> tau
val tau_of_field : field -> tau
val tau_of_record : field -> tau
val init_of_comp : compinfo -> tau
val init_of_object : c_object -> tau
val init_of_ctype : typ -> tau
......@@ -177,12 +175,16 @@ val t_int : tau
val t_real : tau
val t_bool : tau
val t_prop : tau
val t_addr : unit -> tau (** pointer on Void *)
val t_addr : unit -> tau
val t_comp : compinfo -> tau
val t_init : compinfo -> tau
val t_float : c_float -> tau
val t_array : tau -> tau
val t_farray : tau -> tau -> tau
val t_datatype : adt -> tau list -> tau
val t_matrix : tau -> int -> tau
val pointer : (typ -> tau) Context.value (** type of pointers *)
val pointer : tau Context.value (** type of pointers *)
val floats : (c_float -> tau) Context.value (** type of floats *)
val poly : string list Context.value (** polymorphism *)
val builtin_types: (string -> t_builtin) Context.value (* builtin types *)
......
......@@ -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)
......
......@@ -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 *)
length : term option ; (* number of array cells ; None is infinite *)
}
let rec collect rank = function
......@@ -112,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
......@@ -121,43 +87,45 @@ 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 ;
length = None ;
}
| 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
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 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 +140,5 @@ let rec do_merge ds1 ds2 =
let merge ds1 ds2 =
try Some(do_merge ds1 ds2)
with Exit -> None
(* -------------------------------------------------------------------------- *)
......@@ -24,32 +24,30 @@
(* --- 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 *)
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 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 *)