Commit 3cd56b05 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: ensure the absence of alias in function types

One exception to this rule is the the result type in a non-recursive
function may contain regions coming the function's arguments (though
not from the context). It is sometimes useful to write a function
around a constructor or a projection: see function [create] in
verifythis_fm2012_LRS.mlw. For recursive functions we impose
the full non-alias discipline.
parent 6d269278
module Bad
use import ref.Ref
function comp ~'a 'a : int
let test () =
let rec f x y =
(* the arguments of [g] share the region, but we don't know it yet,
and specialize [g] as fully region polymorpic. Since we do not
compute the fixed point during type inference, the type of [f]
will be erroneously over-generalized, the types of [x] and [y]
won't be unified, and we will have a region mismatch on [g x y]
when building the expression. This is why recursive functions
must be completely alias-free. *)
g x y
with g u v =
u := comp u v
in
()
end
......@@ -961,17 +961,9 @@ let aty_full_inst sbs aty =
(* remove from the given arrow every inner effect *)
let rec aty_filter ghost svs vars aty =
let add svs { pv_vs = vs } = Svs.add vs svs in
let add svs pv = Svs.add pv.pv_vs svs in
let svs = List.fold_left add svs aty.aty_args in
(* every region in the type must be unique *)
let check_alias vars ity =
(* FIXME? This check is not needed for soundness
and can be made outside of the core WhyML API *)
let check reg = if reg_occurs reg vars then
Loc.errorm "The type of this function contains an alias" in
reg_iter check ity.ity_vars in
let add vars { pv_ity = ity } =
check_alias vars ity; vars_union vars ity.ity_vars in
let add vars pv = vars_union vars pv.pv_ity.ity_vars in
let vars = List.fold_left add vars aty.aty_args in
(* remove the effects that do not affect the context *)
let spec = spec_filter ghost svs vars aty.aty_spec in
......@@ -984,9 +976,7 @@ let rec aty_filter ghost svs vars aty =
(* filter the result type *)
let vty = match aty.aty_result with
| VTarrow a -> VTarrow (aty_filter ghost svs vars a)
(* FIXME? This check is commented out since we do have examples
where a mutable argument is incorporated into the result. *)
| VTvalue _ -> (*check_alias vars v;*) aty.aty_result in
| VTvalue _ -> aty.aty_result in
vty_arrow_unsafe aty.aty_args spec vty
let aty_filter ?(ghost=false) pvs aty =
......
......@@ -1018,6 +1018,41 @@ let check_lambda_effect lenv ({fun_lambda = lam} as fd) bl dsp =
"type parameter %a is not opaque in this expression" Pretty.print_tv tv in
ignore (Mtv.inter bad_comp (opaque_binders Stv.empty bl) eeff.eff_compar)
let check_user_ps recu ps =
let ps_regs = ps.ps_subst.ity_subst_reg in
let report r =
if Mreg.mem r ps_regs then let spv = Spv.filter
(fun pv -> reg_occurs r pv.pv_ity.ity_vars) ps.ps_pvset in
Loc.errorm "The type of this function contains an alias with \
external variable %a" Mlw_pretty.print_pv (Spv.choose spv)
else
Loc.errorm "The type of this function contains an alias"
in
let rec check regs ity = match ity.ity_node with
| Ityapp (_,_,rl) ->
let add regs r =
if Mreg.mem r regs then report r else
check (Mreg.add r r regs) r.reg_ity in
let regs = List.fold_left add regs rl in
ity_fold check regs ity
| _ ->
ity_fold check regs ity
in
let rec down regs a =
let add regs pv = check regs pv.pv_ity in
let regs = List.fold_left add regs a.aty_args in
match a.aty_result with
| VTarrow a -> down regs a
| VTvalue v -> check (if recu then regs else ps_regs) v
(* we allow the value in a non-recursive function to contain
regions coming the function's arguments, but not from the
context. It is sometimes useful to write a function around
a constructor or a projection. For recursive functions, we
impose the full non-alias discipline, to ensure the safety
of region polymorphism (see add_rec_mono). *)
in
ignore (down ps_regs ps.ps_aty)
let spec_of_dspec lenv eff vty dsp = {
c_pre = create_pre lenv dsp.ds_pre;
c_post = create_post lenv vty dsp.ds_post;
......@@ -1283,8 +1318,9 @@ and expr_rec lenv dfdl =
let fdl = create_rec_defn (List.map step2 fdl) in
let step3 fd = fd.fun_ps, lambda_invariant lenv fd.fun_lambda in
let fdl = create_rec_defn (List.map step3 fdl) in
let step4 fd (_,_,_,bl,(de,dsp)) =
Loc.try4 de.de_loc check_lambda_effect lenv fd bl dsp in
let step4 fd (id,_,_,bl,(de,dsp)) =
Loc.try4 de.de_loc check_lambda_effect lenv fd bl dsp;
Loc.try2 id.id_loc check_user_ps true fd.fun_ps in
List.iter2 step4 fdl dfdl;
fdl
......@@ -1307,6 +1343,7 @@ and expr_fun lenv x gh bl (de, dsp as tr) =
let lam = lambda_invariant lenv lam in
let fd = create_fun_defn (Denv.create_user_id x) lam in
Loc.try4 de.de_loc check_lambda_effect lenv fd bl dsp;
Loc.try2 x.id_loc check_user_ps false fd.fun_ps;
fd
and expr_lam lenv gh pvl (de, dsp) =
......
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