Commit c07f9fd6 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: forbid reset variables in postconditions

parent a6fb3775
......@@ -43,16 +43,13 @@ WhyML
The type cast can then play the role of the "close" instruction.
Do we need it? What's the good syntax for open types?
- we check the context type invariants around Eany, but not around
Eabstr, which is rather strange. Should Eabstr have preconditions?
If not, why should it post-ensure the invariants that didn't
necessarily hold before its execution? Probably, we shouldn't
add the context invariants to the outer spec of Eany.
- we check the context type invariants around Eany and after Eabstr.
It might be strange that Eabstr post-ensures the invariants that
didn't necessarily hold before its execution. Also, what about
return/raise invariants, should Eany and Eabstr enforce them?
(at the moment, they do)
- and what about return/raise invariants, should Eany and Eabstr
ensure them? (at the moment, they do)
- currently every unhandled exception has postcondition "true".
- currently every unhandled exception has the postcondition "true".
"false" would be a poor choice, as it could introduce inconsistency
in the WPs of the caller. Should we allow unhandled exceptions at all?
......@@ -78,19 +75,6 @@ WhyML
require tedious checks pretty much everywhere in the code,
and they cannot be translated to OCaml.
- the following function is verifiable:
type dref 'a = {| mutable dcontents : ref 'a |}
let fn (dr : dref int) (r : ref int) =
{ !r = 0 } dr.dcontents <- r; dr.dcontents := 1 { !r = 0 }
Strictly speaking, this is benign, since r is reset by the
first assignement, and the corresponding reference cannot be
used anymore during the program execution. However, it would
be nice to forbid the use of reset regions in post-conditions,
unless they are put under "old".
syntax
------
......
module Bad
use import int.Int
use import ref.Ref
type dref 'a = {| mutable dcontents : ref 'a |}
let one (x : dref 'a) (y : ref 'a) =
{ }
x.dcontents <- y;
y
{ !(x.dcontents) = !(old y) }
end
module Bad
use import int.Int
use import ref.Ref
type dref 'a = {| mutable dcontents : ref 'a |}
let one (x : dref 'a) (y : ref 'a) =
{ }
x.dcontents <- y
{ !(x.dcontents) = !y }
end
......@@ -544,6 +544,18 @@ let l_pvset pvs lam =
let pvs = spec_pvset pvs (spec_of_lambda lam 0) in
List.fold_right Spv.remove lam.l_args pvs
let spec_of_abstract e q xq = {
c_pre = t_true;
c_post = q;
c_xpost = xq;
c_effect = e.e_effect;
c_variant = [];
c_letrec = 0; }
let abstr_pvset pvs e q xq =
let pvs = e_pvset pvs e in
spec_pvset pvs (spec_of_abstract e q xq)
(* check admissibility of consecutive events *)
exception StaleRegion of expr * ident
......@@ -953,13 +965,7 @@ let e_any spec vty =
mk_expr (Eany spec) vty spec.c_effect varm
let e_abstract e q xq =
let spec = {
c_pre = t_true;
c_post = q;
c_xpost = xq;
c_effect = e.e_effect;
c_variant = [];
c_letrec = 0 } in
let spec = spec_of_abstract e q xq in
spec_check spec e.e_vty;
let varm = spec_varmap e.e_varm spec in
mk_expr (Eabstr (e,q,xq)) e.e_vty e.e_effect varm
......
......@@ -191,6 +191,7 @@ and lambda = {
val e_pvset : Spv.t -> expr -> Spv.t
val l_pvset : Spv.t -> lambda -> Spv.t
val abstr_pvset : Spv.t -> expr -> post -> xpost -> Spv.t
val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
val e_label_add : label -> expr -> expr
......
......@@ -676,7 +676,20 @@ let env_invariant lenv eff pvs =
in
Spv.fold add_pv pvs (t_true,t_true)
let post_invariant lenv inv ity q =
let rec check_reset rvs t = match t.t_node with
| Tvar vs when Svs.mem vs rvs ->
errorm "The variable %s is reset and can only be used \
under `old' in the postcondition" vs.vs_name.id_string
| Tapp (ls,_) when ls_equal ls fs_at -> false
| Tlet _ | Tcase _ | Teps _ | Tquant _ ->
let rvs = Mvs.set_inter rvs t.t_vars in
if Mvs.is_empty rvs then false else
t_any (check_reset rvs) t
| _ ->
t_any (check_reset rvs) t
let post_invariant lenv rvs inv ity q =
ignore (check_reset rvs q);
let vs, q = open_post q in
let kn = get_known lenv.mod_uc in
let lkn = Theory.get_known (get_theory lenv.mod_uc) in
......@@ -688,27 +701,39 @@ let ity_or_unit = function
| VTvalue v -> v.vtv_ity
| VTarrow _ -> ity_unit
let reset_vars eff pvs =
let add pv s =
if eff_stale_region eff pv.pv_vtv.vtv_ity.ity_vars
then Svs.add pv.pv_vs s else s in
if Mreg.is_empty eff.eff_resets then Svs.empty else
Spv.fold add pvs Svs.empty
let spec_invariant lenv pvs vty spec =
let ity = ity_or_unit vty in
let pvs = spec_pvset pvs spec in
let rvs = reset_vars spec.c_effect pvs in
let pinv,qinv = env_invariant lenv spec.c_effect pvs in
let post_inv = post_invariant lenv qinv in
let post_inv = post_invariant lenv rvs qinv in
let xpost_inv xs q = post_inv xs.xs_ity q in
{ spec with c_pre = t_and_simp spec.c_pre pinv;
c_post = post_inv ity spec.c_post;
c_xpost = Mexn.mapi xpost_inv spec.c_xpost }
let abst_invariant lenv e q xq =
let abstr_invariant lenv e q xq =
let ity = ity_or_unit e.e_vty in
let post_inv = post_invariant lenv t_true in
let pvs = abstr_pvset Spv.empty e q xq in
let rvs = reset_vars e.e_effect pvs in
let _,qinv = env_invariant lenv e.e_effect pvs in
let post_inv = post_invariant lenv rvs qinv in
let xpost_inv xs q = post_inv xs.xs_ity q in
post_inv ity q, Mexn.mapi xpost_inv xq
let lambda_invariant lenv pvs lam =
let ity = ity_or_unit lam.l_expr.e_vty in
let pvs = List.fold_right Spv.add lam.l_args pvs in
let rvs = reset_vars lam.l_expr.e_effect pvs in
let pinv,qinv = env_invariant lenv lam.l_expr.e_effect pvs in
let post_inv = post_invariant lenv qinv in
let post_inv = post_invariant lenv rvs qinv in
let xpost_inv xs q = post_inv xs.xs_ity q in
{ lam with l_pre = t_and_simp lam.l_pre pinv;
l_post = post_inv ity lam.l_post;
......@@ -895,7 +920,10 @@ let rec type_c lenv gh pvs vars dtyc =
let xpost = if Svs.is_empty esvs then spec.c_xpost else
let exn = Invalid_argument "Mlw_typing.type_c" in
let res = create_vsymbol (id_fresh "dummy") ty_unit in
let add vs f = let t = t_var vs in t_and_simp (t_equ t t) f in
let t_old = t_var pv_old.pv_vs in
let add vs f = (* put under 'old' in case of reset *)
let t = fs_app fs_at [t_var vs; t_old] vs.vs_ty in
t_and_simp (t_equ t t) f in
let xq = Mlw_ty.create_post res (Svs.fold add esvs t_true) in
Mexn.add_new exn xs_exit xq spec.c_xpost in
let spec = { spec with c_xpost = xpost } in
......@@ -1030,7 +1058,7 @@ and expr_desc lenv loc de = match de.de_desc with
let e1 = expr lenv de1 in
let q = create_post lenv "result" e1.e_vty q in
let xq = complete_xpost lenv e1.e_effect xq in
let q, xq = abst_invariant lenv e1 q xq in
let q, xq = abstr_invariant lenv e1 q xq in
e_abstract e1 q xq
| DEassert (ak, f) ->
let ak = match ak with
......
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