Commit 4a48a9ee authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw: move defensive resets and spoils from Dexpr to Ity

Since we are going to authorize "any" and "val" to have aliases
between the argument and the results, we should only reset the
unknown regions -- and these are easier to compute inside create_cty.
parent 8063a44e
......@@ -1100,16 +1100,10 @@ let cty_of_spec env bl mask dsp dity =
let _, eff = effect_of_dspec dsp in
let eff = eff_ghostify env.ghs eff in
let eff = eff_reset_overwritten eff in
let out = ity_freeregs Sreg.empty ity in
let add_xs xs s = ity_freeregs s xs.xs_ity in
let out = Sxs.fold add_xs eff.eff_raises out in
let eff = eff_reset eff out in
let esc = eff_escape eff ity in
let eff = Sity.fold_left eff_spoil eff esc in
let p = rebase_pre env preold old dsp.ds_pre in
let q = create_post ity dsp.ds_post in
let xq = create_xpost dsp.ds_xpost in
create_cty ~mask bl p q xq (get_oldies old) eff ity
create_cty ~mask ~defensive:true bl p q xq (get_oldies old) eff ity
(** Expressions *)
......
......@@ -1296,7 +1296,8 @@ let check_post exn ity post =
| Teps _ -> Ty.ty_equal_check ty (t_type q)
| _ -> raise exn) post
let create_cty ?(mask=MaskVisible) args pre post xpost oldies effect result =
let create_cty ?(mask=MaskVisible) ?(defensive=false)
args pre post xpost oldies effect result =
let exn = Invalid_argument "Ity.create_cty" in
(* pre, post, and xpost are well-typed *)
check_pre pre; check_post exn result post;
......@@ -1352,10 +1353,15 @@ let create_cty ?(mask=MaskVisible) args pre post xpost oldies effect result =
eff_covers = Mreg.set_inter effect.eff_covers rknown;
eff_resets = Mreg.set_inter effect.eff_resets vknown} in
(* only spoil the escaping type variables *)
let esc = eff_escape effect result in
let esc = Sity.fold_left ity_rch_vars Stv.empty esc in
let spoils = Stv.inter effect.eff_spoils esc in
let escape = eff_escape effect result in
let escape = Sity.fold_left ity_rch_vars Stv.empty escape in
let spoils = Stv.inter effect.eff_spoils escape in
let effect = { effect with eff_spoils = spoils } in
(* be defensive in abstract function declarations *)
let effect = if not defensive then effect else
let resets = Mreg.set_diff vknown rknown in
let resets = Mreg.set_union effect.eff_resets resets in
{ effect with eff_resets = resets; eff_spoils = escape } in
(* remove the formal parameters from eff_reads *)
let effect = { effect with eff_reads = xreads } in
cty_unsafe args pre post xpost oldies effect result mask freeze
......@@ -1675,10 +1681,12 @@ let print_spec args pre post xpost oldies eff fmt ity =
(Pp.print_list Pp.comma print_pv) (Spv.elements reads);
if not (Mreg.is_empty eff.eff_writes) then fprintf fmt "@\nwrites { @[%a@] }"
(Pp.print_list Pp.comma print_write) (Mreg.bindings eff.eff_writes);
if not (Mreg.is_empty eff.eff_covers) then fprintf fmt "@\ncovers { @[%a@] }"
if not (Sreg.is_empty eff.eff_covers) then fprintf fmt "@\ncovers { @[%a@] }"
(Pp.print_list Pp.comma print_region) (Sreg.elements eff.eff_covers);
if not (Mreg.is_empty eff.eff_resets) then fprintf fmt "@\nresets { @[%a@] }"
if not (Sreg.is_empty eff.eff_resets) then fprintf fmt "@\nresets { @[%a@] }"
(Pp.print_list Pp.comma print_region) (Sreg.elements eff.eff_resets);
if not (Stv.is_empty eff.eff_spoils) then fprintf fmt "@\nspoils { @[%a@] }"
(Pp.print_list Pp.comma Pretty.print_tv) (Stv.elements eff.eff_spoils);
Pp.print_list Pp.nothing print_pre fmt pre;
Pp.print_list Pp.nothing print_old fmt (Mpv.bindings oldies);
Pp.print_list Pp.nothing print_post fmt post;
......
......@@ -413,11 +413,11 @@ type cty = private {
cty_freeze : ity_subst;
}
val create_cty : ?mask:mask -> pvsymbol list ->
pre list -> post list -> post list Mxs.t ->
val create_cty : ?mask:mask -> ?defensive:bool ->
pvsymbol list -> pre list -> post list -> post list Mxs.t ->
pvsymbol Mpv.t -> effect -> ity -> cty
(** [create_cty ?mask args pre post xpost oldies effect result] creates
a computation type. [post] and [mask] must be consistent with [result].
(** [create_cty ?mask ?defensive args pre post xpost oldies effect result]
creates a new cty. [post] and [mask] must be consistent with [result].
The [cty_xpost] field does not have to cover all raised exceptions.
[cty_effect.eff_reads] is completed wrt the specification and [args].
[cty_freeze] freezes every unbound pvsymbol in [cty_effect.eff_reads].
......@@ -426,7 +426,10 @@ val create_cty : ?mask:mask -> pvsymbol list ->
[post], and [xpost] must come from [cty_reads], [args] or [result].
[oldies] maps ghost pure snapshots of the parameters and external
reads to the original pvsymbols: these snapshots are removed from
[cty_effect.eff_reads] and replaced with the originals. *)
[cty_effect.eff_reads] and replaced with the originals. If [defensive]
is [true], then type variables in the result and exceptional results
are spoiled and fresh regions in the result and exceptional results
are reset. *)
val cty_apply : cty -> pvsymbol list -> ity list -> ity -> cty
(** [cty_apply cty pvl rest res] instantiates [cty] up to the types 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