Commit faf9a2be authored by Léon Gondelman's avatar Léon Gondelman
Browse files

Ity: resets are protected by a common set of covers

The effects now must satisfy the following invariants:

1. Every region in eff_writes, eff_taints, and eff_covers
   must occur in the type of some variable in eff_reads.

2. Both eff_taints and eff_covers are subsets of eff_writes.

3. eff_covers and eff_resets are disjoint.

4. Every region in eff_writes is either in eff_covers or
   is stale (according to Ity.reg_r_stale) and forbidden
   for the later use.

Also, this commit rewrites Ity.eff_assign and Ity.eff_strong
(renamed now to eff_reset_overwritten) to handle correctly
parallel assignments.
parent d3f483bc
......@@ -916,7 +916,7 @@ let cty_of_spec env bl dsp dity =
let env, old = add_label env "0" in
let dsp = get_later env dsp ity in
let _, eff = effect_of_dspec dsp in
let eff = eff_strong eff in
let eff = eff_reset_overwritten eff 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
......
......@@ -383,13 +383,14 @@ let localize_ghost_write v r el =
Loc.error ?loc (BadGhostWrite (v,r))) el;
raise (BadGhostWrite (v,r))
(* localize a cover effect *)
let localize_cover_stale v r el =
let covers eff = match Mreg.find_opt r eff.eff_covers with
| Some cvr -> ity_r_stale r cvr v.pv_ity
| None -> false in
List.iter (fun e -> if covers e.e_effect then
let loc = e_locate_effect covers e in
(* localize a reset effect *)
let localize_reset_stale v r el =
let resets eff =
if Sreg.mem r eff.eff_resets then
ity_r_stale (Sreg.singleton r) eff.eff_covers v.pv_ity
else false in
List.iter (fun e -> if resets e.e_effect then
let loc = e_locate_effect resets e in
Loc.error ?loc (StaleVariable (v,r))) el;
raise (StaleVariable (v,r))
......@@ -403,7 +404,7 @@ let localize_divergence el =
let try_effect el fn x y = try fn x y with
| BadGhostWrite (v,r) -> localize_ghost_write v r el
| StaleVariable (v,r) -> localize_cover_stale v r el
| StaleVariable (v,r) -> localize_reset_stale v r el
| GhostDivergence -> localize_divergence el
(* smart constructors *)
......@@ -658,7 +659,7 @@ let c_fun args p q xq old ({e_effect = eff} as e) =
(* reset variables are forbidden in post-conditions *)
let c = try create_cty args p q xq old eff e.e_ity with
| BadGhostWrite (v,r) -> localize_ghost_write v r [e]
| StaleVariable (v,r) -> localize_cover_stale v r [e] in
| StaleVariable (v,r) -> localize_reset_stale v r [e] in
mk_cexp (Cfun e) c
let c_app s vl ityl ity =
......
This diff is collapsed.
......@@ -190,8 +190,8 @@ val reg_v_occurs : tvsymbol -> region -> bool
val ity_r_occurs : region -> ity -> bool
val reg_r_occurs : region -> region -> bool
val ity_r_stale : region -> Sreg.t -> ity -> bool
val reg_r_stale : region -> Sreg.t -> region -> bool
val ity_r_stale : Sreg.t -> 'a Mreg.t -> ity -> bool
val reg_r_stale : Sreg.t -> 'a Mreg.t -> region -> bool
val ity_closed : ity -> bool
......@@ -281,13 +281,15 @@ exception AssignPrivate of region
exception StaleVariable of pvsymbol * region
exception BadGhostWrite of pvsymbol * region
exception DuplicateField of region * pvsymbol
exception IllegalAssign of region * region * region
exception GhostDivergence
type effect = private {
eff_reads : Spv.t; (* known variables *)
eff_writes : Spv.t Mreg.t; (* modifications to specific fields *)
eff_covers : Sreg.t Mreg.t; (* confinement of regions to covers *)
eff_taints : Sreg.t; (* ghost modifications *)
eff_covers : Sreg.t; (* surviving writes *)
eff_resets : Sreg.t; (* locked by covers *)
eff_raises : Sexn.t; (* raised exceptions *)
eff_oneway : bool; (* non-termination *)
eff_ghost : bool; (* ghost status *)
......@@ -311,8 +313,8 @@ val eff_read_single_pre : pvsymbol -> effect -> effect
val eff_read_single_post : effect -> pvsymbol -> effect
val eff_bind_single : pvsymbol -> effect -> effect
val eff_reset : effect -> region -> effect (* confine to an empty cover *)
val eff_strong : effect -> effect (* confine all subregions under writes *)
(* val eff_reset : effect -> region -> effect (* confine to an empty cover *) *)
val eff_reset_overwritten : effect -> effect (* confine all subregions under writes *)
val eff_raise : effect -> xsymbol -> effect
val eff_catch : effect -> xsymbol -> effect
......
Supports Markdown
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