Commit 13edc745 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: check for escaping variables

parent 12c85de3
......@@ -81,12 +81,17 @@ module Wps = PSsym.W
let ps_equal : psymbol -> psymbol -> bool = (==)
let create_psymbol id vta vars = {
ps_name = id_register id;
ps_vta = vta_filter vars vta;
ps_vars = vars;
ps_subst = vars_freeze vars;
}
let create_psymbol_real ~poly id vta vars =
let frozen = if poly then vars else vars_union vars vta.vta_vars
in {
ps_name = id_register id;
ps_vta = vta_filter vars vta;
ps_vars = frozen;
ps_subst = vars_freeze frozen; }
let create_psymbol_poly = create_psymbol_real ~poly:true
let create_psymbol_mono = create_psymbol_real ~poly:false
let create_psymbol id vta = create_psymbol_poly id vta vars_empty
(** program/logic symbols *)
......@@ -265,7 +270,7 @@ let create_val id tyv =
let varm = check_v tyv in
let vars = varmap_join varm vars_empty in
let name = match build_v vars tyv with
| VTarrow vta -> LetA (create_psymbol id vta vars)
| VTarrow vta -> LetA (create_psymbol_poly id vta vars)
| VTvalue vtv -> LetV (create_pvsymbol id vtv) in
{ val_name = name; val_spec = tyv; val_vars = varm }
......@@ -553,7 +558,8 @@ let create_let_defn id e =
| VTvalue vtv ->
LetV (create_pvsymbol id (vtv_unmut vtv))
| VTarrow vta ->
LetA (create_psymbol id vta (varmap_join e.e_vars vta.vta_vars))
let vars = varmap_join e.e_vars vars_empty in
LetA (create_psymbol_mono id vta vars)
in
{ let_var = lv ; let_expr = e }
......@@ -623,7 +629,7 @@ let create_fun_defn id lam =
let vars = varmap_join varm vars_empty in
let vta = spec_arrow lam.l_args e.e_effect e.e_vty in
(* construct rec_defn *)
{ rec_ps = create_psymbol id vta vars;
{ rec_ps = create_psymbol_poly id vta vars;
rec_lambda = lam;
rec_vars = varm; }
......
......@@ -72,7 +72,7 @@ module Wps : Hashweak.S with type key = psymbol
val ps_equal : psymbol -> psymbol -> bool
val create_psymbol : preid -> vty_arrow -> varset -> psymbol
val create_psymbol : preid -> vty_arrow -> psymbol
(** program/logic symbols *)
......
......@@ -727,14 +727,16 @@ and vty_full_inst s = function
let rec vta_filter vars a =
let vars = vars_union vars a.vta_arg.vtv_vars in
let vty, vars = match a.vta_result with
(* FIXME? We allow effects on the regions from a VTvalue result,
but only reset is actually meaningful. Should we require that
any new region in the result be reset? *)
| VTvalue v -> a.vta_result, vars_union vars v.vtv_vars
| VTarrow a -> VTarrow (vta_filter vars a), vars in
let effect = eff_filter vars a.vta_effect in
vty_arrow ~ghost:a.vta_ghost ~effect a.vta_arg vty
let vty = match a.vta_result with
| VTarrow a -> VTarrow (vta_filter vars a)
| VTvalue _ -> a.vta_result in
(* reads and writes must come from the context,
resets may affect the regions in the result *)
let eff = eff_filter vars a.vta_effect in
let rst = { eff_empty with eff_resets = a.vta_effect.eff_resets } in
let rst = eff_filter (vty_vars vars a.vta_result) rst in
let eff = { eff with eff_resets = rst.eff_resets } in
vty_arrow ~ghost:a.vta_ghost ~effect:eff a.vta_arg vty
(** THE FOLLOWING CODE MIGHT BE USEFUL LATER FOR WPgen *)
(*
......
......@@ -955,7 +955,7 @@ and expr_rec lenv rdl =
let vta = match vty_ghostify gh (vty_of_dvty dvty) with
| VTarrow vta -> vta
| VTvalue _ -> assert false in
let ps = create_psymbol (Denv.create_user_id id) vta vars_empty in
let ps = create_psymbol (Denv.create_user_id id) vta in
add_local id.id (LetA ps) lenv, (ps, gh, lam) in
let lenv, rdl = Util.map_fold_left step1 lenv rdl in
let step2 (ps, gh, lam) = ps, expr_lam lenv gh lam in
......
......@@ -93,6 +93,49 @@ let rec drop_at now m t = match t.t_node with
let psymbol_spec_t : type_v Wps.t = Wps.create 17
let add_pv_varm pv m = Mid.add pv.pv_vs.vs_name pv.pv_vtv.vtv_vars m
let add_pv_vars pv s = vars_union pv.pv_vtv.vtv_vars s
let check_spec ps tyv =
let rec check vty tyv = match vty, tyv with
| VTvalue _, SpecV _ -> ()
| VTarrow vta, SpecA (_::(_::_ as pvl), tyc) ->
assert (eff_is_empty vta.vta_effect);
check vta.vta_result (SpecA (pvl, tyc))
| VTarrow vta, SpecA ([_], tyc) ->
let eff1 = vta.vta_effect in
let eff2 = tyc.c_effect in
assert (Sreg.equal eff1.eff_reads eff2.eff_reads);
assert (Sreg.equal eff1.eff_writes eff2.eff_writes);
assert (Sexn.equal eff1.eff_raises eff2.eff_raises);
assert (Sreg.equal eff1.eff_ghostr eff2.eff_ghostr);
assert (Sreg.equal eff1.eff_ghostw eff2.eff_ghostw);
assert (Sexn.equal eff1.eff_ghostx eff2.eff_ghostx);
check vta.vta_result tyc.c_result
| _ -> assert false
in
check (VTarrow ps.ps_vta) tyv
let rec filter_v ~strict varm vars = function
| SpecA (pvl, tyc) ->
let varm = List.fold_right add_pv_varm pvl varm in
let vars = List.fold_right add_pv_vars pvl vars in
SpecA (pvl, filter_c ~strict varm vars tyc)
| tyv -> tyv
and filter_c ~strict varm vars tyc =
let result = filter_v ~strict varm vars tyc.c_result in
let effect = eff_filter vars tyc.c_effect in
if strict then begin
let add _ f s = Mvs.set_union f.t_vars s in
let vss = add () tyc.c_pre tyc.c_post.t_vars in
let vss = Mexn.fold add tyc.c_xpost vss in
let check { vs_name = id } _ = if not (Mid.mem id varm) then
Loc.errorm "Local variable %s escapes from its scope" id.id_string in
Mvs.iter check vss
end;
{ tyc with c_effect = effect; c_result = result }
let spec_lambda l tyv =
let tyc = {
c_pre = l.l_pre;
......@@ -104,12 +147,21 @@ let spec_lambda l tyv =
let spec_val { val_name = lv; val_spec = tyv } = match lv with
| LetA ps when not (Wps.mem psymbol_spec_t ps) ->
check_spec ps tyv; (* TODO: remove *)
Wps.set psymbol_spec_t ps tyv
| _ -> ()
let rec spec_let { let_var = lv; let_expr = e } = match lv with
let rec spec_let ~strict { let_var = lv; let_expr = e } = match lv with
| LetA ps when not (Wps.mem psymbol_spec_t ps) ->
Wps.set psymbol_spec_t ps (spec_expr e)
(* FIXME: memoization is broken if one declares the same psymbol
both as a local (non-strict) let and as a global (strict) let.
First global, then local is safe. First local, then global
may lead to an escaping variable, which will or will not
be detected by the core API. *)
let vars = Mid.fold (fun _ -> vars_union) e.e_vars vars_empty in
let tyv = filter_v ~strict e.e_vars vars (spec_expr e) in
check_spec ps tyv; (* TODO: remove *)
Wps.set psymbol_spec_t ps tyv
| _ -> ()
and spec_rec rdl =
......@@ -118,6 +170,7 @@ and spec_rec rdl =
let add_early_spec rd = match rd.rec_lambda.l_expr.e_vty with
| VTvalue vtv ->
let tyv = spec_lambda rd.rec_lambda (SpecV vtv) in
check_spec rd.rec_ps tyv; (* TODO: remove *)
Wps.set psymbol_spec_t rd.rec_ps tyv
| VTarrow _ when Mid.mem rd.rec_ps.ps_name vars ->
Loc.errorm ?loc:rd.rec_lambda.l_expr.e_loc
......@@ -129,6 +182,7 @@ and spec_rec rdl =
match rd.rec_lambda.l_expr.e_vty with
| VTarrow _ ->
let tyv = spec_lambda rd.rec_lambda tyv in
check_spec rd.rec_ps tyv; (* TODO: remove *)
Wps.set psymbol_spec_t rd.rec_ps tyv
| VTvalue _ -> () in
List.iter add_late_spec rdl
......@@ -144,7 +198,7 @@ and spec_expr e = match e.e_node with
and compute it now. *)
| Eapp (_, _) ->
assert false (* TODO *)
| Elet (ld,e1) -> spec_let ld; spec_expr e1
| Elet (ld,e1) -> spec_let ~strict:false ld; spec_expr e1
| Erec (rdl,e1) -> spec_rec rdl; spec_expr e1
| Eghost e1 -> spec_expr e1
| Eany tyc -> tyc.c_result
......@@ -468,7 +522,7 @@ let mk_env env km th = {
}
let wp_let env km th ({ let_var = lv; let_expr = e } as ld) =
spec_let ld;
spec_let ~strict:true ld;
let env = mk_env env km th in
let q, xq = default_post e.e_vty e.e_effect in
let f = wp_expr env e q xq in
......
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