Commit f2752054 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: separate ghost effects from the real-world ones

parent 3c2f3c2a
......@@ -73,6 +73,7 @@ let create_plsymbol id args value =
let ty_of_vtv vtv = ty_of_ity vtv.vtv_ity in
let pure_args = List.map ty_of_vtv args in
let ls = create_fsymbol id pure_args (ty_of_vtv value) in
let eff_read e r = eff_read e ~ghost:value.vtv_ghost r in
let effect = Util.option_fold eff_read eff_empty value.vtv_mut in
let arg_reset acc a = Util.option_fold eff_reset acc a.vtv_mut in
let effect = List.fold_left arg_reset effect args in {
......@@ -113,18 +114,19 @@ let ppat_plapp pls ppl vtv =
let sbs = ity_match ity_subst_empty pls.pl_value.vtv_ity vtv.vtv_ity in
let mtch eff arg pp =
ignore (ity_match sbs arg.vtv_ity pp.ppat_vtv.vtv_ity);
if pp.ppat_vtv.vtv_ghost <> (vtv.vtv_ghost || arg.vtv_ghost) then
let ghost = pp.ppat_vtv.vtv_ghost in
if ghost <> (vtv.vtv_ghost || arg.vtv_ghost) then
Loc.errorm "Ghost pattern in a non-ghost context";
match arg.vtv_mut, pp.ppat_vtv.vtv_mut with
| Some r1, Some r2 ->
ignore (reg_match sbs r1 r2);
eff_read (eff_union eff pp.ppat_effect) (reg_full_inst sbs r1)
| Some r1, None ->
eff_read (eff_union eff pp.ppat_effect) (reg_full_inst sbs r1)
| None, None ->
eff_union eff pp.ppat_effect
| None, Some _ ->
Loc.errorm "Mutable pattern in a non-mutable position"
| Some r1, Some r2 ->
ignore (reg_match sbs r1 r2);
eff_read ~ghost (eff_union eff pp.ppat_effect) (reg_full_inst sbs r1)
| Some r1, None ->
eff_read ~ghost (eff_union eff pp.ppat_effect) (reg_full_inst sbs r1)
| None, None ->
eff_union eff pp.ppat_effect
| None, Some _ ->
Loc.errorm "Mutable pattern in a non-mutable position"
in
let eff = try List.fold_left2 mtch eff_empty pls.pl_args ppl
with Invalid_argument _ -> raise
......@@ -132,7 +134,7 @@ let ppat_plapp pls ppl vtv =
let pl = List.map (fun pp -> pp.ppat_pattern) ppl in
{ ppat_pattern = pat_app pls.pl_ls pl (ty_of_ity vtv.vtv_ity);
ppat_vtv = vtv;
ppat_effect = eff; }
ppat_effect = if vtv.vtv_ghost then eff_ghostify eff else eff; }
let ppat_lapp ls ppl vtv =
let pls = {
......@@ -239,27 +241,14 @@ let e_label_copy { e_label = lab; e_loc = loc } e =
exception GhostWrite of expr * region
exception GhostRaise of expr * xsymbol
let ghost_effect e = e (* FIXME *)
(*
if vty_ghost e.e_vty then
let eff = e.e_effect in
let check r = not r.reg_ghost in
if Sreg.exists check eff.eff_writes then
let s = Sreg.filter check eff.eff_writes in
raise (GhostWrite (e, Sreg.choose s))
else e
else e
*)
let mk_expr node vty eff vars =
ghost_effect {
e_node = node;
e_vty = vty;
e_effect = eff;
e_vars = vars;
e_label = Slab.empty;
e_loc = None;
}
let mk_expr node vty eff vars = {
e_node = node;
e_vty = vty;
e_effect = if vty_ghost vty then eff_ghostify eff else eff;
e_vars = vars;
e_label = Slab.empty;
e_loc = None;
}
let varmap_join = Mid.fold (fun _ -> vars_union)
let varmap_union = Mid.union (fun _ s1 s2 -> Some (vars_union s1 s2))
......@@ -325,15 +314,19 @@ let e_let ({ let_var = lv ; let_expr = d } as ld) e =
Mid.iter check_id vars
in
Mreg.iter check_reset d.e_effect.eff_resets;
(* FIXME: the tests below are too restrictive. If this let is embedded
into a bigger ghost expression, then a ghost exception raised from d
and catched there is benign. A good test is to traverse top-level
definitions from top to bottom and check if exceptions escape from
the outermost ghost subexpressions. The same for ghost writes. *)
(* If we make a ghost write inside d, then the modified region cannot
be read in a later non-ghost code. We ignore eventual resets in e;
a once ghostified region must stay so, even if if reset. *)
let badwr = Sreg.inter d.e_effect.eff_ghostw e.e_effect.eff_reads in
if not (Sreg.is_empty badwr) then raise (GhostWrite (d, Sreg.choose badwr));
(* We should be able to raise and catch exceptions inside ghost expressions.
The problematic case is a ghost exception that escapes into reality. *)
(* FIXME: this test is too restrictive. If this let is embedded into a
bigger ghost expression, then an exception raised from d and catched
there is benign. A good test is to traverse top-level definitions
from top to bottom and check if exceptions escape from the outermost
ghost subexpressions. *)
if vty_ghost d.e_vty && not (vty_ghost e.e_vty) &&
not (Sexn.is_empty d.e_effect.eff_raises) then
if not (vty_ghost e.e_vty) && not (Sexn.is_empty d.e_effect.eff_ghostx) then
raise (GhostRaise (d, Sexn.choose d.e_effect.eff_raises));
(* This should be the only expression constructor that deals with
sequence of effects *)
......@@ -558,9 +551,9 @@ let e_assign_real mpv pv =
| Some r -> r
| None -> raise (Immutable mpv)
in
let eff = eff_assign eff_empty r pv.pv_vtv.vtv_ity in
let vars = add_pv_vars pv (add_pv_vars mpv Mid.empty) in
let ghost = mpv.pv_vtv.vtv_ghost || pv.pv_vtv.vtv_ghost in
let eff = eff_assign eff_empty ~ghost r pv.pv_vtv.vtv_ity in
let vars = add_pv_vars pv (add_pv_vars mpv Mid.empty) in
let vty = VTvalue (vty_value ~ghost ity_unit) in
mk_expr (Eassign (mpv,r,pv)) vty eff vars
......
......@@ -465,37 +465,65 @@ module Mexn = Exn.M
type effect = {
eff_reads : Sreg.t;
eff_writes : Sreg.t;
eff_raises : Sexn.t;
eff_ghostr : Sreg.t; (* ghost reads *)
eff_ghostw : Sreg.t; (* ghost writes *)
eff_ghostx : Sexn.t; (* ghost raises *)
(* if r1 -> Some r2 then r1 appears in ty(r2) *)
eff_resets : region option Mreg.t;
eff_raises : Sexn.t;
}
let eff_empty = {
eff_reads = Sreg.empty;
eff_writes = Sreg.empty;
eff_raises = Sexn.empty;
eff_ghostr = Sreg.empty;
eff_ghostw = Sreg.empty;
eff_ghostx = Sexn.empty;
eff_resets = Mreg.empty;
eff_raises = Sexn.empty
}
let join_reset _key v1 v2 =
Some (if option_eq reg_equal v1 v2 then v1 else None)
let eff_union x y =
{ eff_reads = Sreg.union x.eff_reads y.eff_reads;
eff_writes = Sreg.union x.eff_writes y.eff_writes;
eff_resets = Mreg.union join_reset x.eff_resets y.eff_resets;
eff_raises = Sexn.union x.eff_raises y.eff_raises;
}
let eff_union x y = {
eff_reads = Sreg.union x.eff_reads y.eff_reads;
eff_writes = Sreg.union x.eff_writes y.eff_writes;
eff_raises = Sexn.union x.eff_raises y.eff_raises;
eff_ghostr = Sreg.union x.eff_ghostr y.eff_ghostr;
eff_ghostw = Sreg.union x.eff_ghostw y.eff_ghostw;
eff_ghostx = Sexn.union x.eff_ghostx y.eff_ghostx;
eff_resets = Mreg.union join_reset x.eff_resets y.eff_resets;
}
let eff_ghostify e = {
eff_reads = Sreg.empty;
eff_writes = Sreg.empty;
eff_raises = Sexn.empty;
eff_ghostr = Sreg.union e.eff_reads e.eff_ghostr;
eff_ghostw = Sreg.union e.eff_writes e.eff_ghostw;
eff_ghostx = Sexn.union e.eff_raises e.eff_ghostx;
eff_resets = e.eff_resets;
}
let eff_read e ?(ghost=false) r = if ghost
then { e with eff_ghostr = Sreg.add r e.eff_ghostr }
else { e with eff_reads = Sreg.add r e.eff_reads }
let eff_write e ?(ghost=false) r = if ghost
then { e with eff_ghostw = Sreg.add r e.eff_ghostw }
else { e with eff_writes = Sreg.add r e.eff_writes }
let eff_raise e ?(ghost=false) x = if ghost
then { e with eff_ghostx = Sexn.add x e.eff_ghostx }
else { e with eff_raises = Sexn.add x e.eff_raises }
let eff_read e r = { e with eff_reads = Sreg.add r e.eff_reads }
let eff_write e r = { e with eff_writes = Sreg.add r e.eff_writes }
let eff_raise e x = { e with eff_raises = Sexn.add x e.eff_raises }
let eff_reset e r = { e with eff_resets = Mreg.add r None e.eff_resets }
exception IllegalAlias of region
let eff_assign e r ty =
let e = eff_write e r in
let eff_assign e ?(ghost=false) r ty =
let e = eff_write e ~ghost r in
let sub = ity_match ity_subst_empty r.reg_ity ty in
(* assignment cannot instantiate type variables *)
let check tv ity = match ity.ity_node with
......@@ -514,15 +542,19 @@ let eff_assign e r ty =
let reset = Mreg.fold add_left sub.ity_subst_reg reset in
{ e with eff_resets = Mreg.union join_reset e.eff_resets reset }
let eff_remove_raise e x = { e with eff_raises = Sexn.remove x e.eff_raises }
let eff_remove_raise e x = { e with
eff_raises = Sexn.remove x e.eff_raises;
eff_ghostx = Sexn.remove x e.eff_ghostx;
}
let eff_full_inst s e =
let s = s.ity_subst_reg in
(* modified or reset regions in e *)
let wr = Mreg.map (Util.const ()) e.eff_resets in
let wr = Sreg.union e.eff_writes wr in
let wr = Sreg.union e.eff_ghostw wr in
(* read-only regions in e *)
let ro = Sreg.diff e.eff_reads wr in
let ro = Sreg.diff (Sreg.union e.eff_reads e.eff_ghostr) wr in
(* all modified or reset regions are instantiated into distinct regions *)
let add_affected r acc =
let r = Mreg.find r s in Sreg.add_new (IllegalAlias r) r acc in
......@@ -532,13 +564,16 @@ let eff_full_inst s e =
let r = Mreg.find r s in if Sreg.mem r wr then raise (IllegalAlias r) in
Sreg.iter add_readonly ro;
(* calculate instantiated effect *)
let add_inst r acc = Sreg.add (Mreg.find r s) acc in
let reads = Sreg.fold add_inst e.eff_reads Sreg.empty in
let writes = Sreg.fold add_inst e.eff_writes Sreg.empty in
let add_inst r v acc =
let add_sreg r acc = Sreg.add (Mreg.find r s) acc in
let add_mreg r v acc =
Mreg.add (Mreg.find r s) (option_map (fun v -> Mreg.find v s) v) acc in
let resets = Mreg.fold add_inst e.eff_resets Mreg.empty in
{ e with eff_reads = reads ; eff_writes = writes ; eff_resets = resets }
{ e with
eff_reads = Sreg.fold add_sreg e.eff_reads Sreg.empty;
eff_writes = Sreg.fold add_sreg e.eff_writes Sreg.empty;
eff_ghostr = Sreg.fold add_sreg e.eff_ghostr Sreg.empty;
eff_ghostw = Sreg.fold add_sreg e.eff_ghostw Sreg.empty;
eff_resets = Mreg.fold add_mreg e.eff_resets Mreg.empty;
}
(* program types *)
......@@ -589,7 +624,7 @@ let vty_arrow vtv ?(effect=eff_empty) ?(ghost=false) vty =
(* mutable arguments are rejected outright *)
if vtv.vtv_mut <> None then
Loc.errorm "Mutable arguments are not allowed in vty_arrow";
(* we accept a mutable vty_value for the result to simplify Mlw_expr,
(* we accept a mutable vty_value as a result to simplify Mlw_expr,
but erase it in the signature: only projections return mutables *)
let vty = match vty with
| VTvalue ({ vtv_mut = Some r ; vtv_vars = vars } as vtv) ->
......@@ -619,7 +654,11 @@ let vty_app_arrow vta vtv =
ity_equal_check vta.vta_arg.vtv_ity vtv.vtv_ity;
let ghost = vta.vta_ghost || (vtv.vtv_ghost && not vta.vta_arg.vtv_ghost) in
let result = if ghost then vty_ghostify vta.vta_result else vta.vta_result in
vta.vta_effect, result
let effect =
if vty_ghost result then eff_ghostify vta.vta_effect else vta.vta_effect in
(* we don't really need this, because Mlw_expr will ensure that the effect
of every ghost expression is properly ghostified *)
effect, result
(* vty instantiation *)
......
......@@ -185,20 +185,24 @@ module Sexn: Mexn.Set
type effect = private {
eff_reads : Sreg.t;
eff_writes : Sreg.t;
eff_raises : Sexn.t;
eff_ghostr : Sreg.t; (* ghost reads *)
eff_ghostw : Sreg.t; (* ghost writes *)
eff_ghostx : Sexn.t; (* ghost raises *)
(* if r1 -> Some r2 then r1 appears in ty(r2) *)
eff_resets : region option Mreg.t;
eff_raises : Sexn.t;
}
val eff_empty : effect
val eff_union : effect -> effect -> effect
val eff_ghostify : effect -> effect
val eff_read : effect -> region -> effect
val eff_write : effect -> region -> effect
val eff_read : effect -> ?ghost:bool -> region -> effect
val eff_write : effect -> ?ghost:bool -> region -> effect
val eff_raise : effect -> ?ghost:bool -> xsymbol -> effect
val eff_reset : effect -> region -> effect
val eff_raise : effect -> xsymbol -> effect
val eff_assign : effect -> region -> ity -> effect
val eff_assign : effect -> ?ghost:bool -> region -> ity -> effect
val eff_remove_raise : effect -> xsymbol -> effect
......
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