Skip to content

GitLab

why3
why3
Commit 72a36bd8 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

modules: huge refactoring of programs types, in preparation for mutable types

parent 2d519b26
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1107 additions and 600 deletions
Makefile.in
View file @ 72a36bd8
......@@ -281,7 +281,7 @@ install_no_local::
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
src/programs/pgm_lexer.ml
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_effect \
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer \
pgm_types pgm_module pgm_wp pgm_env pgm_typing pgm_main
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
......
src/programs/pgm_fastwp.ml
View file @ 72a36bd8
......@@ -29,7 +29,7 @@ open Theory
open Pgm_ttree
open Pgm_typing
module E = Pgm_effect
module E = Pgm_types.E
module State : sig
type t
......
src/programs/pgm_module.ml
View file @ 72a36bd8
......@@ -6,6 +6,7 @@ open Theory
open Term
open Pgm_types
open Pgm_types.T
open Pgm_ttree
module Mnm = Mstr
......@@ -34,11 +35,9 @@ let ns_replace eq chk x vo vn =
let ns_union eq chk =
Mnm.union (fun x vn vo -> Some (ns_replace eq chk x vo vn))
let pr_equal p1 p2 = ls_equal p1.p_ls p2.p_ls
let rec merge_ns chk ns1 ns2 =
let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
{ ns_pr = ns_union pr_equal chk ns1.ns_pr ns2.ns_pr;
{ ns_pr = ns_union p_equal chk ns1.ns_pr ns2.ns_pr;
ns_ex = ns_union ls_equal chk ns1.ns_ex ns2.ns_ex;
ns_mt = ns_union mt_equal chk ns1.ns_mt ns2.ns_mt;
ns_ns = Mnm.union fusion ns1.ns_ns ns2.ns_ns; }
......@@ -51,7 +50,7 @@ let ns_add eq chk x v m = Mnm.change x (function
| None -> Some v
| Some vo -> Some (ns_replace eq chk x vo v)) m
let pr_add = ns_add pr_equal
let pr_add = ns_add p_equal
let ex_add = ns_add ls_equal
let mt_add = ns_add mt_equal
......@@ -131,7 +130,7 @@ let add_symbol add id v uc =
| _ -> assert false
let add_psymbol ps uc =
add_symbol add_pr ps.p_ls.ls_name ps uc
add_symbol add_pr ps.p_name ps uc
let add_esymbol ls uc =
add_symbol add_ex ls.ls_name ls uc
......
src/programs/pgm_module.mli
View file @ 72a36bd8
......@@ -3,6 +3,7 @@ open Why
open Ident
open Term
open Pgm_types
open Pgm_types.T
module Mnm : Map.S with type key = string
......
src/programs/pgm_ttree.ml
View file @ 72a36bd8
......@@ -18,6 +18,8 @@
(**************************************************************************)
open Why
open Pgm_types
open Pgm_types.T
type loc = Loc.position
......@@ -36,20 +38,22 @@ type for_direction = Pgm_ptree.for_direction
type dreference =
| DRlocal of string
| DRglobal of Term.lsymbol
| DRglobal of psymbol
type deffect = {
de_reads : dreference list;
de_writes : dreference list;
de_raises : Term.lsymbol list;
de_raises : esymbol list;
}
type dpre = Denv.dfmla
type dpost = Denv.dfmla * (Term.lsymbol * Denv.dfmla) list
type dpost_fmla = Denv.dty * Denv.dfmla
type dexn_post_fmla = Denv.dty option * Denv.dfmla
type dpost = dpost_fmla * (Term.lsymbol * dexn_post_fmla) list
type dtype_v =
| DTpure of Denv.dty
| DTpure of Denv.dty
| DTarrow of dbinder list * dtype_c
and dtype_c =
......@@ -58,7 +62,7 @@ and dtype_c =
dc_pre : dpre;
dc_post : dpost; }
and dbinder = ident * dtype_v
and dbinder = ident * Denv.dty * dtype_v
type dvariant = Denv.dterm * Term.lsymbol
......@@ -76,8 +80,8 @@ type dexpr = {
and dexpr_desc =
| DEconstant of constant
| DElocal of string * dtype_v
| DEglobal of Term.lsymbol * dtype_v
| DElocal of string * Denv.dty
| DEglobal of psymbol * dtype_v
| DElogic of Term.lsymbol
| DEapply of dexpr * dexpr
| DEfun of dbinder list * dtriple
......@@ -90,8 +94,8 @@ and dexpr_desc =
| DElazy of lazy_op * dexpr * dexpr
| DEmatch of dexpr * (Denv.dpattern * dexpr) list
| DEabsurd
| DEraise of Term.lsymbol * dexpr option
| DEtry of dexpr * (Term.lsymbol * string option * dexpr) list
| DEraise of esymbol * dexpr option
| DEtry of dexpr * (esymbol * string option * dexpr) list
| DEfor of ident * dexpr * for_direction * dexpr * Denv.dfmla option * dexpr
| DEassert of assertion_kind * Denv.dfmla
......@@ -107,19 +111,39 @@ and dtriple = dpre * dexpr * dpost
type variant = Term.term * Term.lsymbol
type rec_variant = Term.vsymbol * Term.term * Term.lsymbol
type reference = R.t
type reference = Pgm_effect.reference
type pre = T.pre
type pre = Pgm_types.pre
type post = T.post
type post = Pgm_types.post
type ivsymbol = {
i_name : Ident.preid;
i_ty : Ty.ty;
i_vs : Term.vsymbol;
}
type ireference =
| IRlocal of ivsymbol
| IRglobal of psymbol
type ieffect = {
ie_reads : ireference list;
ie_writes : ireference list;
ie_raises : esymbol list;
}
type type_v = Pgm_types.type_v
type itype_v =
| ITpure of Ty.ty
| ITarrow of ibinder list * itype_c
type type_c = Pgm_types.type_c
and itype_c =
{ ic_result_type : itype_v;
ic_effect : ieffect;
ic_pre : pre;
ic_post : post; }
type binder = Pgm_types.binder
and ibinder = ivsymbol * itype_v
type loop_annotation = {
loop_invariant : Term.fmla option;
......@@ -128,6 +152,20 @@ type loop_annotation = {
type label = Term.vsymbol
type irec_variant = ivsymbol * Term.term * Term.lsymbol
type ipattern = {
ipat_pat : Term.pattern;
ipat_node : ipat_node;
}
and ipat_node =
| IPwild
| IPvar of ivsymbol
| IPapp of Term.lsymbol * ipattern list
| IPor of ipattern * ipattern
| IPas of ipattern * ivsymbol
type iexpr = {
iexpr_desc : iexpr_desc;
iexpr_type : Ty.ty;
......@@ -136,29 +174,29 @@ type iexpr = {
and iexpr_desc =
| IElogic of Term.term
| IElocal of Term.vsymbol * type_v
| IEglobal of Term.lsymbol * type_v
| IEapply of iexpr * Term.vsymbol
| IEapply_ref of iexpr * reference
| IEfun of binder list * itriple
| IElet of Term.vsymbol * iexpr * iexpr
| IElocal of ivsymbol
| IEglobal of psymbol
| IEapply of iexpr * ivsymbol
(* | IEapply_ref of iexpr * reference *)
| IEfun of ibinder list * itriple
| IElet of ivsymbol * iexpr * iexpr
| IEletrec of irecfun list * iexpr
| IEif of iexpr * iexpr * iexpr
| IEloop of loop_annotation * iexpr
| IElazy of lazy_op * iexpr * iexpr
| IEmatch of Term.vsymbol * (Term.pattern * iexpr) list
| IEmatch of ivsymbol * (ipattern * iexpr) list
| IEabsurd
| IEraise of Term.lsymbol * iexpr option
| IEtry of iexpr * (Term.lsymbol * Term.vsymbol option * iexpr) list
| IEfor of Term.vsymbol * Term.vsymbol * for_direction * Term.vsymbol *
| IEraise of esymbol * iexpr option
| IEtry of iexpr * (esymbol * ivsymbol option * iexpr) list
| IEfor of ivsymbol * ivsymbol * for_direction * ivsymbol *
Term.fmla option * iexpr
| IEassert of assertion_kind * Term.fmla
| IElabel of label * iexpr
| IEany of type_c
| IEany of itype_c
and irecfun = Term.vsymbol * binder list * rec_variant option * itriple
and irecfun = ivsymbol * ibinder list * irec_variant option * itriple
and itriple = pre * iexpr * post
......@@ -166,43 +204,57 @@ and itriple = pre * iexpr * post
(*****************************************************************************)
(* phase 3: effect inference *)
type rec_variant = pvsymbol * Term.term * Term.lsymbol
type pattern = {
ppat_pat : Term.pattern;
ppat_node : ppat_node;
}
and ppat_node =
| Pwild
| Pvar of pvsymbol
| Papp of Term.lsymbol * pattern list
| Por of pattern * pattern
| Pas of pattern * pvsymbol
type expr = {
expr_desc : expr_desc;
expr_type : Ty.ty;
expr_type_v: type_v;
expr_effect: Pgm_effect.t;
expr_effect: E.t;
expr_loc : loc;
}
and expr_desc =
| Elogic of Term.term
| Elocal of Term.vsymbol
| Eglobal of Term.lsymbol
| Efun of binder list * triple
| Elet of Term.vsymbol * expr * expr
| Elocal of pvsymbol
| Eglobal of psymbol
| Efun of pvsymbol list * triple
| Elet of pvsymbol * expr * expr
| Eletrec of recfun list * expr
| Eif of expr * expr * expr
| Eloop of loop_annotation * expr
| Ematch of Term.vsymbol * (Term.pattern * expr) list
| Ematch of pvsymbol * (pattern * expr) list
| Eabsurd
| Eraise of Term.lsymbol * expr option
| Etry of expr * (Term.lsymbol * Term.vsymbol option * expr) list
| Efor of Term.vsymbol * Term.vsymbol * for_direction * Term.vsymbol *
| Eraise of esymbol * expr option
| Etry of expr * (esymbol * pvsymbol option * expr) list
| Efor of pvsymbol * pvsymbol * for_direction * pvsymbol *
Term.fmla option * expr
| Eassert of assertion_kind * Term.fmla
| Elabel of label * expr
| Eany of type_c
and recfun = Term.vsymbol * binder list * rec_variant option * triple
and recfun = pvsymbol * pvsymbol list * rec_variant option * triple
and triple = pre * expr * post
type decl =
| Dlet of Pgm_types.psymbol * expr
| Dletrec of (Pgm_types.psymbol * recfun) list
| Dparam of Pgm_types.psymbol * type_v
| Dlet of T.psymbol * expr
| Dletrec of (T.psymbol * recfun) list
| Dparam of T.psymbol * type_v
type file = decl list
......
src/programs/pgm_types.ml
View file @ 72a36bd8
This diff is collapsed.
src/programs/pgm_types.mli
View file @ 72a36bd8
......@@ -25,72 +25,134 @@ exception NotMutable
val get_mtsymbol : tysymbol -> mtsymbol
(** raises [NotMutable] if [ts] is not a mutable type *)
val ts_arrow : tysymbol
(* program types *)
module rec T : sig
type effect = Pgm_effect.t
type reference = Pgm_effect.reference
type pre = Term.fmla
type pre = Term.fmla
type post_fmla = Term.vsymbol (* result *) * Term.fmla
type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
type esymbol = lsymbol
type post_fmla = Term.vsymbol (* result *) * Term.fmla
type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
type post = post_fmla * (esymbol * exn_post_fmla) list
type type_v = private
| Tpure of ty
| Tarrow of pvsymbol list * type_c
type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
and type_c = {
c_result_type : type_v;
c_effect : E.t;
c_pre : pre;
c_post : post;
}
type type_v = private
| Tpure of Ty.ty
| Tarrow of binder list * type_c
and pvsymbol = private {
pv_name : ident;
pv_tv : type_v;
pv_ty : ty; (* as a logic type, for typing purposes only *)
pv_vs : vsymbol; (* for use in the logic *)
}
and type_c =
{ c_result_type : type_v;
c_effect : effect;
c_pre : pre;
c_post : post; }
val tpure : ty -> type_v
val tarrow : pvsymbol list -> type_c -> type_v
and binder = Term.vsymbol * type_v
val create_pvsymbol : preid -> ?vs:vsymbol -> type_v -> pvsymbol
val tpure : Ty.ty -> type_v
val tarrow : binder list -> type_c -> type_v
(* program symbols *)
(* program symbols *)
type psymbol = private {
p_name : ident;
p_tv : type_v;
p_ty : ty; (* as a logic type, for typing purposes only *)
p_ls : lsymbol; (* for use in the logic *)
}
val create_psymbol : preid -> type_v -> psymbol
type psymbol = private {
p_ls : lsymbol;
p_tv : type_v;
}
val p_equal : psymbol -> psymbol -> bool
val create_psymbol : preid -> type_v -> psymbol
(* program types -> logic types *)
(* exception symbols *)
val purify : ty -> ty
val purify_type_v : ?logic:bool -> type_v -> ty
(** when [logic] is [true], mutable types are turned into their models *)
(* operations on program types *)
val apply_type_v_var : type_v -> pvsymbol -> type_c
val apply_type_v_sym : type_v -> psymbol -> type_c
val occur_type_v : R.t -> type_v -> bool
val v_result : ty -> vsymbol
val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
val post_map : (fmla -> fmla) -> post -> post
val subst1 : vsymbol -> term -> term Mvs.t
val eq_type_v : type_v -> type_v -> bool
type esymbol = lsymbol
(* pretty-printers *)
(* program types -> logic types *)
val print_type_v : Format.formatter -> type_v -> unit
val print_type_c : Format.formatter -> type_c -> unit
val print_post : Format.formatter -> post -> unit
val ts_arrow : tysymbol
end
and Mpv : sig include Map.S with type key = T.pvsymbol end
(* references *)
and R : sig
type t =
| Rlocal of T.pvsymbol
| Rglobal of T.psymbol
val type_of : t -> ty
val name_of : t -> ident
end
and Sref : sig include Set.S with type elt = R.t end
and Mref : sig include Map.S with type key = R.t end
and Sexn : sig include Set.S with type elt = T.esymbol end
(* effects *)
and E : sig
val purify : ?logic:bool -> type_v -> ty
(** when [logic] is [true], mutable types are turned into their models *)
type t = private {
reads : Sref.t;
writes : Sref.t;
raises : Sexn.t;
}
(* operations on program types *)
val empty : t
val apply_type_v : type_v -> vsymbol -> type_c
val apply_type_v_ref : type_v -> reference -> type_c
val add_read : R.t -> t -> t
val add_write : R.t -> t -> t
val add_raise : T.esymbol -> t -> t
val occur_type_v : reference -> type_v -> bool
val remove_reference : R.t -> t -> t
val filter : (R.t -> bool) -> t -> t
val v_result : ty -> vsymbol
val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
val remove_raise : T.esymbol -> t -> t
val post_map : (fmla -> fmla) -> post -> post
val union : t -> t -> t
val subst1 : vsymbol -> term -> term Mvs.t
val equal : t -> t -> bool
val no_side_effect : t -> bool
val subst : R.t Mpv.t -> t -> t
val eq_type_v : type_v -> type_v -> bool
val occur : R.t -> t -> bool
(* pretty-printers *)
end
val print_type_v : Format.formatter -> type_v -> unit
val print_type_c : Format.formatter -> type_c -> unit
val print_post : Format.formatter -> post -> unit
src/programs/pgm_typing.ml
View file @ 72a36bd8
This diff is collapsed.
src/programs/pgm_wp.ml
View file @ 72a36bd8
......@@ -28,10 +28,9 @@ open Theory
open Pretty
open Pgm_ttree
open Pgm_types
open Pgm_types.T
open Pgm_module
module E = Pgm_effect
let debug = Debug.register_flag "program_wp"
(* phase 4: weakest preconditions *******************************************)
......@@ -83,8 +82,8 @@ let fresh_label env =
let ty = ty_app (find_ts env "label") [] in
create_vsymbol (id_fresh "label") ty
let wp_binder (x, tv) f = match tv with
| Tpure _ -> wp_forall x f
let wp_binder x f = match x.pv_tv with
| Tpure _ -> wp_forall x.pv_vs f
| Tarrow _ -> f
let wp_binders = List.fold_right wp_binder
......@@ -120,9 +119,9 @@ let rec unref env r v f =
f_map (unref_term env r v) (unref env r v) f
and unref_term env r v t = match t.t_node with
| Tapp (ls, [u]) when ls_equal ls (find_ls env "prefix !") ->
let rt = E.reference_of_term u in
if E.ref_equal rt r then t_var v else t
(* | Tapp (ls, [u]) when ls_equal ls (find_ls env "prefix !") -> *)
(* let rt = E.reference_of_term u in *)
(* if E.ref_equal rt r then t_var v else t *)
| Tapp (ls, _) when ls_equal ls (find_ls env "old") ->
assert false
| Tapp (ls, _) when ls_equal ls (find_ls env "at") ->
......@@ -135,23 +134,23 @@ and unref_term env r v t = match t.t_node with
let quantify ?(all=false) env ef f =
(* eprintf "quantify: ef=%a f=%a@." E.print ef Pretty.print_fmla f; *)
let quantify1 r f =
let ty = unref_ty env (E.type_of_reference r) in
let v = create_vsymbol (id_clone (E.name_of_reference r)) ty in
let ty = unref_ty env (R.type_of r) in
let v = create_vsymbol (id_clone (R.name_of r)) ty in
let f = unref env r v f in
wp_forall v f
in
let s = ef.E.writes in
let s = if all then E.Sref.union ef.E.reads s else s in
E.Sref.fold quantify1 s f
let s = if all then Sref.union ef.E.reads s else s in
Sref.fold quantify1 s f
let abstract_wp env ef (q',ql') (q,ql) =
assert (List.length ql' = List.length ql);
let quantify_res f' f res =
let f = wp_implies f' f in
let f = match res with
| Some v when is_ref_ty env v.vs_ty ->
let v' = create_vsymbol (id_clone v.vs_name) (unref_ty env v.vs_ty) in
wp_forall v' (unref env (E.Rlocal v) v' f)
(* | Some v when is_ref_ty env v.vs_ty -> *)
(* let v' = create_vsymbol (id_clone v.vs_name) (unref_ty env v.vs_ty) in *)
(* wp_forall v' (unref env (R.Rlocal v) v' f) *)
| Some v ->
wp_forall v f
| None ->
......@@ -185,7 +184,7 @@ let opaque_wp env ef q' q =
appear in effect [ef] *)
let filter_post ef (q, ql) =
let keep (ls, _) = Sls.mem ls ef.E.raises in
let keep (ls, _) = Sexn.mem ls ef.E.raises in
q, List.filter keep ql
let rec ls_assoc ls = function
......@@ -197,7 +196,7 @@ let default_exn_post ls = ls, (exn_v_result ls, f_true)
let default_post ty ef =
(v_result ty, f_true),
List.map default_exn_post (Sls.elements ef.E.raises)
List.map default_exn_post (Sexn.elements ef.E.raises)
let rec assoc_handler x = function
| [] -> raise Not_found
......@@ -209,7 +208,7 @@ let rec assoc_handler x = function
let saturate_post ef q (_, ql) =
let set_post x = try x, ls_assoc x ql with Not_found -> default_exn_post x in
let xs = Sls.elements ef.E.raises in
let xs = Sexn.elements ef.E.raises in
(q, List.map set_post xs)
(* maximum *)
......@@ -227,7 +226,7 @@ let sup ((q, ql) : post) (_, ql') =
(* post-condition for a loop body *)
let default_exns_post ef =
let xs = Sls.elements ef.E.raises in
let xs = Sexn.elements ef.E.raises in
List.map default_exn_post xs
let term_at env lab t =
......@@ -276,7 +275,7 @@ and wp_desc env e q = match e.expr_desc with
f_subst_single v t q
| Elocal v ->
let (res, q), _ = q in
f_subst (subst1 res (t_var v)) q
f_subst (subst1 res (t_var v.pv_vs)) q
| Eglobal _ ->
let (_, q), _ = q in q
| Efun (bl, t) ->
......@@ -287,7 +286,7 @@ and wp_desc env e q = match e.expr_desc with
let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
let v1 = v_result e1.expr_type in
let t1 = t_label_add (label ~loc:e1.expr_loc "let") (t_var v1) in
let q1 = v1, f_subst (subst1 x t1) w2 in
let q1 = v1, f_subst (subst1 x.pv_vs t1) w2 in
let q1 = saturate_post e1.expr_effect q1 q in
wp_expr env e1 q1
| Eletrec (dl, e1) ->
......@@ -324,13 +323,13 @@ and wp_desc env e q = match e.expr_desc with
in
w
(* optimization for the particular case let _ = y in e *)
| Ematch (_, [{pat_node = Pwild}, e]) ->
| Ematch (_, [{ppat_pat = {pat_node = Term.Pwild}}, e]) ->
wp_expr env e (filter_post e.expr_effect q)
| Ematch (x, bl) ->
let branch (p, e) =
f_close_branch p (wp_expr env e (filter_post e.expr_effect q))
f_close_branch p.ppat_pat (wp_expr env e (filter_post e.expr_effect q))
in
let t = t_var x in
let t = t_var x.pv_vs in
f_case t (List.map branch bl)
| Eabsurd ->
f_false
......@@ -353,6 +352,7 @@ and wp_desc env e q = match e.expr_desc with
List.map
(fun (x, v, h) ->
let w = wp_expr env h (filter_post h.expr_effect q) in
let v = option_map (fun v -> v.pv_vs) v in
x, (v, w))
hl
in
......@@ -379,26 +379,27 @@ and wp_desc env e q = match e.expr_desc with
| Pgm_ptree.Downto ->
find_ls env "infix <", find_ls env "infix >=", t_int_const "-1"
in
let v1_gt_v2 = f_app gt [t_var v1; t_var v2] in
let v1_le_v2 = f_app le [t_var v1; t_var v2] in
let v1_gt_v2 = f_app gt [t_var v1.pv_vs; t_var v2.pv_vs] in
let v1_le_v2 = f_app le [t_var v1.pv_vs; t_var v2.pv_vs] in
let inv = match inv with Some inv -> inv | None -> f_true in
let add = find_ls env "infix +" in
let wp1 =
let xp1 = t_app add [t_var x; incr] ty_int in
let post = f_subst (subst1 x xp1) inv in
let xp1 = t_app add [t_var x.pv_vs; incr] ty_int in
let post = f_subst (subst1 x.pv_vs xp1) inv in
let q1 = saturate_post e1.expr_effect (res, post) q in
wp_expr env e1 q1
in
let f = wp_and ~sym:true
(f_subst (subst1 x (t_var v1)) inv)
(f_subst (subst1 x.pv_vs (t_var v1.pv_vs)) inv)
(quantify env e.expr_effect
(wp_and ~sym:true
(wp_forall x
(wp_implies (wp_and (f_app le [t_var v1; t_var x])
(f_app le [t_var x; t_var v2]))
(wp_forall x.pv_vs
(wp_implies
(wp_and (f_app le [t_var v1.pv_vs; t_var x.pv_vs])
(f_app le [t_var x.pv_vs; t_var v2.pv_vs]))
(wp_implies inv wp1)))
(let sv2 = t_app add [t_var v2; incr] ty_int in
wp_implies (f_subst (subst1 x sv2) inv) q1)))
(let <