Commit d7f43b06 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: update modified variables

parent ae3c9526
......@@ -19,6 +19,7 @@
(**************************************************************************)
open Why3
open Stdlib
open Util
open Ident
open Ty
......@@ -35,6 +36,16 @@ type pvsymbol = {
let pv_equal : pvsymbol -> pvsymbol -> bool = (==)
module PVsym = WeakStructMake (struct
type t = pvsymbol
let tag pv = pv.pv_vs.vs_name.id_tag
end)
module Spv = PVsym.S
module Mpv = PVsym.M
module Hpv = PVsym.H
module Wpv = PVsym.W
let create_pvsymbol id vtv = {
pv_vs = create_vsymbol id (ty_of_ity vtv.vtv_ity);
pv_vtv = vtv;
......@@ -107,8 +118,8 @@ exception HiddenPLS of lsymbol
(** specification *)
type pre = term (* precondition *)
type post = term (* postcondition *)
type pre = term (* precondition: pre_fmla *)
type post = term (* postcondition: eps result . post_fmla *)
type xpost = post Mexn.t (* exceptional postconditions *)
type type_c = {
......@@ -142,7 +153,11 @@ let create_post vs f = t_eps_close vs f
let open_post f = match f.t_node with
| Teps bf -> t_open_bound bf
| _ -> assert false
| _ -> Loc.errorm "invalid post-condition"
let check_post f = match f.t_node with
| Teps _ -> ()
| _ -> Loc.errorm "invalid post-condition"
let varmap_join = Mid.fold (fun _ -> vars_union)
let varmap_union = Mid.set_union
......@@ -155,6 +170,7 @@ let fmla_vars f vsset =
Mvs.set_union vsset f.t_vars
let post_vars ity f vsset =
check_post f;
Ty.ty_equal_check (ty_of_ity ity) (t_type f);
Mvs.set_union vsset f.t_vars
......@@ -170,12 +186,17 @@ let variant_vars varl vsset =
Mvs.set_union s t.t_vars in
List.fold_left add_variant vsset varl
(* FIXME? Should we check that every raised exception is in xpost? *)
let spec_vars varm variant pre post xpost _effect result =
exception UnboundException of xsymbol
let spec_vars varm variant pre post xpost eff result =
let vsset = fmla_vars pre Mvs.empty in
let vsset = post_vars result post vsset in
let vsset = xpost_vars xpost vsset in
let vsset = variant_vars variant vsset in
let badex = Sexn.union eff.eff_raises eff.eff_ghostx in
let badex = Mexn.set_diff badex xpost in
if not (Sexn.is_empty badex) then
raise (UnboundException (Sexn.choose badex));
Mvs.fold (fun vs _ m -> add_vs_vars vs m) vsset varm
let spec_arrow pvl effect vty =
......
......@@ -19,6 +19,7 @@
(**************************************************************************)
open Why3
open Stdlib
open Util
open Ident
open Ty
......@@ -35,10 +36,17 @@ type pvsymbol = private {
pv_vtv : vty_value;
}
module Mpv : Map.S with type key = pvsymbol
module Spv : Mpv.Set
module Hpv : Hashtbl.S with type key = pvsymbol
module Wpv : Hashweak.S with type key = pvsymbol
val pv_equal : pvsymbol -> pvsymbol -> bool
val create_pvsymbol : preid -> vty_value -> pvsymbol
val restore_pv : vsymbol -> pvsymbol
(** program symbols *)
(* psymbols represent lambda-abstractions. They are polymorphic and
......@@ -89,8 +97,8 @@ exception HiddenPLS of lsymbol
(** specification *)
type pre = term (* precondition *)
type post = term (* postcondition: a formula with a bound variable *)
type pre = term (* precondition: pre_fmla *)
type post = term (* postcondition: eps result . post_fmla *)
type xpost = post Mexn.t (* exceptional postconditions *)
val create_post : vsymbol -> term -> post
......@@ -120,6 +128,8 @@ type val_decl = private {
val create_val : Ident.preid -> type_v -> val_decl
exception UnboundException of xsymbol
(** patterns *)
type ppattern = private {
......
......@@ -467,5 +467,8 @@ let () = Exn_printer.register
fprintf fmt "This expression is not a function and cannot be applied"
| Mlw_expr.Immutable _e ->
fprintf fmt "Mutable expression expected"
| Mlw_expr.UnboundException xs ->
fprintf fmt "This function raises %a but does not \
specify a post-condition for it" print_xs xs
| _ -> raise exn
end
......@@ -30,7 +30,7 @@ open Mlw_expr
let debug = Debug.register_flag "whyml_wp"
(** WP-only builtins *)
(** Marks *)
let ts_mark = create_tysymbol (id_fresh "'mark") [] None
let ty_mark = ty_app ts_mark []
......@@ -70,7 +70,26 @@ let old_mark lab t = t_subst_single vs_old (t_var lab) t
(* replace [at(t,lab)] with [at(t,'now)] everywhere in formula [f] *)
let erase_mark lab t = t_subst_single lab (t_var vs_now) t
(** Weakest preconditions *)
(* replace [at(t,now)] with [t] modulo variable renaming *)
let rec drop_at now m t = match t.t_node with
| Tvar vs when now ->
begin try t_var (Mvs.find vs m) with Not_found -> t end
| Tapp (ls, _) when ls_equal ls fs_old ->
assert false
| Tapp (ls, [e;{t_node = Tvar lab}]) when ls_equal ls fs_at ->
if vs_equal lab vs_old then assert false else
if vs_equal lab vs_now then drop_at true m e else
(* no longer assume that unmarked variables are at mark 'now *)
t_map (drop_at false m) t
| Tlet _ | Tcase _ | Teps _ | Tquant _ ->
(* do not open unless necessary *)
let m = Mvs.set_inter m t.t_vars in
if Mvs.is_empty m then t else
t_map (drop_at now m) t
| _ ->
t_map (drop_at now m) t
(** WP utilities *)
let ty_of_vty = function
| VTvalue vtv -> ty_of_ity vtv.vtv_ity
......@@ -82,8 +101,7 @@ let default_exn_post xs _ =
let default_post vty ef =
let vs = create_vsymbol (id_fresh "result") (ty_of_vty vty) in
create_post vs t_true,
Mexn.mapi default_exn_post ef.eff_raises
create_post vs t_true, Mexn.mapi default_exn_post ef.eff_raises
let wp_label e f =
let loc = if f.t_loc = None then e.e_loc else f.t_loc in
......@@ -101,28 +119,118 @@ let wp_and ?(sym=false) f1 f2 =
let wp_ands ?(sym=false) fl =
if sym then t_and_simp_l fl else t_and_asym_simp_l fl
let wp_implies f1 f2 = match f2.t_node with
| Tfalse -> t_implies f1 f2
| _ -> t_implies_simp f1 f2
let wp_forall v f =
(* if t_occurs_single v f then t_forall_close_simp [v] [] f else f *)
match f.t_node with
| Tbinop (Timplies, {t_node = Tapp (s,[{t_node = Tvar u};r])},h)
when ls_equal s ps_equ && vs_equal u v && not (Mvs.mem v r.t_vars) ->
t_let_close_simp v r h
| Tbinop (Timplies, {t_node = Tbinop (Tand, g,
{t_node = Tapp (s,[{t_node = Tvar u};r])})},h)
when ls_equal s ps_equ && vs_equal u v && not (Mvs.mem v r.t_vars) ->
t_let_close_simp v r (t_implies_simp g h)
| _ when Mvs.mem v f.t_vars ->
t_forall_close_simp [v] [] f
| _ ->
f
let wp_implies = t_implies_simp
let wp_forall v f = match f.t_node with
| Tbinop (Timplies, {t_node = Tapp (s,[{t_node = Tvar u};r])},h)
when ls_equal s ps_equ && vs_equal u v && not (Mvs.mem v r.t_vars) ->
t_let_close_simp v r h
| Tbinop (Timplies, {t_node = Tbinop (Tand, g,
{t_node = Tapp (s,[{t_node = Tvar u};r])})},h)
when ls_equal s ps_equ && vs_equal u v && not (Mvs.mem v r.t_vars) ->
t_let_close_simp v r (t_implies_simp g h)
| _ when Mvs.mem v f.t_vars ->
t_forall_close_simp [v] [] f
| _ ->
f
let wp_binder x f = wp_forall x.pv_vs f
let wp_binder pv f = wp_forall pv.pv_vs f
let wp_binders = List.fold_right wp_binder
(** Reconstruct pure values after writes *)
let find_constructors km lkm sts ity = match ity.ity_node with
| Itypur (ts,_) ->
let base = ity_pur ts (List.map ity_var ts.ts_args) in
let sbs = ity_match ity_subst_empty base ity in
let csl = Decl.find_constructors lkm ts in
if csl = [] || Sts.mem ts sts then Loc.errorm
"Cannot update values of type %a" Mlw_pretty.print_ity base;
let subst ty = ity_full_inst sbs (ity_of_ty ty), None in
let cnstr (cs,_) = cs, List.map subst cs.ls_args in
Sts.add ts sts, List.map cnstr csl
| Ityapp (its,_,_) ->
let base = ity_app its (List.map ity_var its.its_args) its.its_regs in
let sbs = ity_match ity_subst_empty base ity in
let csl = Mlw_decl.find_constructors km its in
if csl = [] || Sts.mem its.its_pure sts then Loc.errorm
"Cannot update values of type %a" Mlw_pretty.print_ity base;
let subst vtv =
ity_full_inst sbs vtv.vtv_ity,
Util.option_map (reg_full_inst sbs) vtv.vtv_mut in
let cnstr (cs,_) = cs.pl_ls, List.map subst cs.pl_args in
Sts.add its.its_pure sts, List.map cnstr csl
| Ityvar _ -> assert false
let update_var km lkm mreg vs =
let rec update sts vs ity mut =
(* are we a mutable variable? *)
let get_vs r = Mreg.find_def vs r mreg in
let vs = Util.option_apply vs get_vs mut in
(* should we update our value further? *)
let check_reg r _ = reg_occurs r ity.ity_vars in
if ity_pure ity || not (Mreg.exists check_reg mreg) then
t_var vs
else
let sts, csl = find_constructors km lkm sts ity in
let branch (cs,ityl) =
let mk_var (ity,_) = create_vsymbol (id_fresh "y") (ty_of_ity ity) in
let vars = List.map mk_var ityl in
let pat = pat_app cs (List.map pat_var vars) vs.vs_ty in
let mk_arg vs (ity, mut) = update sts vs ity mut in
let t = fs_app cs (List.map2 mk_arg vars ityl) vs.vs_ty in
t_close_branch pat t in
t_case (t_var vs) (List.map branch csl)
in
let vtv = (restore_pv vs).pv_vtv in
update Sts.empty vs vtv.vtv_ity vtv.vtv_mut
(* quantify over all references in eff
eff : effect
f : formula
let eff = { rho1, ..., rhon }
we collect in vars all variables involving these regions
let vars = { v1, ..., vm }
forall r1:ty(rho1). ... forall rn:ty(rhon).
let v'1 = update v1 r1...rn in
...
let v'm = update vm r1...rn in
f[vi <- v'i]
*)
let model1_lab = Slab.singleton (create_label "model:1")
let model2_lab = Slab.singleton (create_label "model:quantify(2)")
let mk_var id label ty = create_vsymbol (id_clone ~label id) ty
let quantify km lkm eff f =
(* mreg : modified rho -> vs *)
let get_var reg () =
let test vs _ id = match (restore_pv vs).pv_vtv with
| { vtv_ity = { ity_node = Ityapp (_,_,[r]) }}
| { vtv_mut = Some r } when reg_equal r reg -> vs.vs_name
| _ -> id in
let id = Mvs.fold test f.t_vars reg.reg_name in
mk_var id model1_lab (ty_of_ity reg.reg_ity)
in
let sreg = Sreg.union eff.eff_writes eff.eff_ghostw in
let mreg = Mreg.mapi get_var sreg in
(* update all program variables involving these regions *)
let update_var vs _ = match update_var km lkm mreg vs with
| { t_node = Tvar nv } when vs_equal vs nv -> None
| t -> Some t in
let vars = Mvs.mapi_filter update_var f.t_vars in
(* vv' : old vs -> new vs *)
let new_var vs _ = mk_var vs.vs_name model2_lab vs.vs_ty in
let vv' = Mvs.mapi new_var vars in
(* quantify *)
let update v t f = t_let_close_simp (Mvs.find v vv') t f in
let f = Mvs.fold update vars (drop_at true vv' f) in
Mreg.fold (Util.const wp_forall) mreg f
(** Weakest preconditions *)
let wp_close_state _km _lkm _ef f =
f (* TODO *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment