Commit 9fd9469c authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: drop read effects

Now that ghost writes are checked via e_syms.syms_pv,
there is no use for read effects anymore.
parent 30c225b4
......@@ -6,7 +6,7 @@ use import ref.Ref
val t : ref int
val m (a:int) (b:int) : unit reads {t} raises { Exception }
val m (a:int) (b:int) : unit raises { Exception }
let test () raises { Exception } = (m ( assert { true } ; 0) 0)
......
......@@ -46,14 +46,14 @@ module ARM
(* memory *)
val mem : ref (map int int)
val mem_ldr (a:int) : int reads { mem } ensures { result = !mem[a] }
val mem_ldr (a:int) : int ensures { result = !mem[a] }
val mem_str (a:int) (v:int) : int writes { mem }
ensures { !mem = (old !mem)[a <- v] }
(* data segment *)
(*
val data : ref (t int int)
val data_ldr (a:int) : int reads { data } ensures { result = data[a] }
val data_ldr (a:int) : int ensures { result = data[a] }
val data_str (a:int) (v:int) : int writes { data }
ensures { data = (old data)[a <- v] }
*)
......@@ -67,16 +67,16 @@ module ARM
val fp : ref int
val pc : ref int (* pc *)
val ldr (r : ref int) (a : int) : unit reads {mem} writes {r}
val ldr (r : ref int) (a : int) : unit writes {r}
ensures { !r = !mem[a] }
val str (r : ref int) (a : int) : unit reads {r} writes {mem}
val str (r : ref int) (a : int) : unit writes {mem}
ensures { !mem = (old !mem)[a <- !r] }
(* condition flags *)
val le : ref bool
val cmp (r : ref int) (v : int) : unit reads {r} writes {le}
val cmp (r : ref int) (v : int) : unit writes {le}
ensures { !le=True <-> !r <= v }
end
......
......@@ -48,14 +48,14 @@ module DijkstraShortestPath
val q: ref (S.set vertex)
val q_is_empty () : bool reads {q}
val q_is_empty () : bool
ensures { result = True <-> S.is_empty !q }
predicate min (m: vertex) (q: S.set vertex) (d: M.map vertex int) =
S.mem m q /\
forall x: vertex. S.mem x q -> d[m] <= d[x]
val q_extract_min () : vertex reads {d} writes {q}
val q_extract_min () : vertex writes {q}
requires { not S.is_empty !q }
ensures { min result (old !q) !d }
ensures { !q = S.remove result (old !q) }
......@@ -173,7 +173,7 @@ module DijkstraShortestPath
(* Iteration on a set *)
val set_has_next (s: ref (S.set 'a)) : bool reads {s}
val set_has_next (s: ref (S.set 'a)) : bool
ensures { result = True <-> not (S.is_empty !s) }
val set_next (s: ref (S.set 'a)) : 'a writes {s}
......
......@@ -26,7 +26,7 @@ module M
exception Not_found
val find (x:int) : int reads { table }
val find (x:int) : int
ensures { !table[x] = Some result }
raises { Not_found -> !table[x] = None }
......
......@@ -78,7 +78,7 @@ module M2
function block_size memory pointer : int
val get_ (p : pointer) (ofs : int) : int reads { mem }
val get_ (p : pointer) (ofs : int) : int
requires { 0 <= ofs < block_size !mem p }
ensures { result = get !mem p ofs }
......@@ -135,7 +135,7 @@ module M3
function block_size memory pointer : int
val get_ (p:pointer) (ofs:int32) : int32 reads { mem }
val get_ (p:pointer) (ofs:int32) : int32
requires { 0 <= to_int ofs < block_size !mem p }
ensures { result = get !mem p (to_int ofs) }
......
......@@ -17,7 +17,7 @@ module M
forall k':key, v':value.
mem !m k' v' <-> if k' = k then v' = v else mem (old !m) k' v' }
val lookup (m:ref rbt) (k:key) : value reads {m}
val lookup (m:ref rbt) (k:key) : value
ensures { mem !m k result }
val remove (m:ref rbt) (k:key) : unit writes {m}
......
......@@ -78,7 +78,7 @@ module M
(***
val ghost_find (u:ref uf) (x:int) : int reads {u}
val ghost_find (u:ref uf) (x:int) : int
requires { inv !u /\ 0 <= x < size !u }
ensures { repr !u x result }
......
......@@ -83,7 +83,7 @@ module HashTable
exception Not_found
val find (h: t 'a 'b) (k: 'a) : 'b reads {h}
val find (h: t 'a 'b) (k: 'a) : 'b
ensures { h[k] = Some result } raises { Not_found -> h[k] = None }
end
......
......@@ -60,7 +60,7 @@ module UnionFind_sig
same (old u.state) x a /\ same (old u.state) b y \/
same (old u.state) x b /\ same (old u.state) a y }
val get_num_classes (u:uf) : int reads {u} ensures { result = num u.state }
val get_num_classes (u:uf) : int ensures { result = num u.state }
end
......
......@@ -24,7 +24,7 @@ module Array
function ([]) (a: array 'a) (i: int) : 'a = get a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
val ([]) (a: array 'a) (i: int) : 'a reads {a}
val ([]) (a: array 'a) (i: int) : 'a
requires { 0 <= i < length a }
ensures { result = a[i] }
......
......@@ -26,23 +26,23 @@ module Hashtbl
ensures { h[k] = Cons v (old h)[k] }
ensures { forall k': key. k' <> k -> h[k'] = (old h)[k'] }
val mem (h: t 'a) (k: key) : bool reads {h}
val mem (h: t 'a) (k: key) : bool
ensures { result=True <-> h[k] <> Nil }
val find (h: t 'a) (k: key) : 'a reads {h}
val find (h: t 'a) (k: key) : 'a
requires { h[k] <> Nil }
ensures { match h[k] with Nil -> false | Cons v _ -> result = v end }
val find_all (h: t 'a) (k: key) : list 'a reads {h}
val find_all (h: t 'a) (k: key) : list 'a
ensures { result = h[k] }
exception NotFound
val defensive_find (h: t 'a) (k: key) : 'a reads {h}
val defensive_find (h: t 'a) (k: key) : 'a
ensures { match h[k] with Nil -> false | Cons v _ -> result = v end }
raises { NotFound -> h[k] = Nil }
val copy (h: t 'a) : t 'a reads {h}
val copy (h: t 'a) : t 'a
ensures { forall k: key. result[k] = h[k] }
val remove (h: t 'a) (k: key) : unit writes {h}
......
......@@ -21,7 +21,7 @@ module Matrix
predicate valid_index (a: matrix 'a) (i: index) =
let r,c = i in 0 <= r < a.rows /\ 0 <= c < a.columns
val get (a: matrix 'a) (i: index) : 'a reads {a}
val get (a: matrix 'a) (i: index) : 'a
requires { valid_index a i }
ensures { result = get a i }
......@@ -74,7 +74,7 @@ module Syntax
function ([]) (a: matrix 'a) (i: index) : 'a = get a i
function ([<-]) (a: matrix 'a) (i: index) (v: 'a) : matrix 'a = set a i v
val ([]) (a: matrix 'a) (i: index) : 'a reads {a}
val ([]) (a: matrix 'a) (i: index) : 'a
requires { valid_index a i }
ensures { result = get a i }
......
......@@ -43,7 +43,7 @@ module Pqueue
raises { Empty -> q.elts = (old q.elts) = Nil }
(** returns the minimal element, without modifying the queue *)
val peek (q: t) : elt reads {q}
val peek (q: t) : elt
ensures { minimal_elt result q.elts }
raises { Empty -> q.elts = Nil }
......@@ -51,14 +51,14 @@ module Pqueue
val clear (q: t) : unit writes {q} ensures { q.elts = Nil }
(** returns a fresh copy of the queue *)
val copy (q: t) : t reads {q} ensures { result = q }
val copy (q: t) : t ensures { result = q }
(** checks whether the queue is empty *)
val is_empty (q: t) : bool reads {q}
val is_empty (q: t) : bool
ensures { result = True <-> q.elts = Nil }
(** returns the number of elements in the queue *)
val length (q: t) : int reads {q}
val length (q: t) : int
ensures { result = length q.elts }
end
......@@ -107,7 +107,7 @@ module PqueueNoDup
raises { Empty -> q.elts = (old q.elts) = empty }
(** returns the minimal element, without modifying the queue *)
val peek (q: t) : elt reads {q}
val peek (q: t) : elt
ensures { minimal_elt result q.elts }
raises { Empty -> q.elts = empty }
......@@ -115,14 +115,14 @@ module PqueueNoDup
val clear (q: t) : unit writes {q} ensures {q.elts = empty }
(** returns a fresh copy of the queue *)
val copy (q: t) : t reads {q} ensures { result = q }
val copy (q: t) : t ensures { result = q }
(** checks whether the queue is empty *)
val is_empty (q: t) : bool reads {q}
val is_empty (q: t) : bool
ensures { result=True <-> q.elts = empty }
(** returns the number of elements in the queue *)
val length (q: t) : int reads {q}
val length (q: t) : int
ensures { result = cardinal q.elts }
end
......@@ -21,7 +21,7 @@ module Queue
| Cons x t -> result = x /\ q.elts = t end }
raises { Empty -> q.elts = old q.elts = Nil }
val peek (q: t 'a) : 'a reads {q}
val peek (q: t 'a) : 'a
ensures { match q.elts with Nil -> false
| Cons x _ -> result = x end }
raises { Empty -> q.elts = Nil }
......@@ -31,21 +31,21 @@ module Queue
ensures { match old q.elts with Nil -> false
| Cons x t -> result = x /\ q.elts = t end }
val safe_peek (q: t 'a) : 'a reads {q}
val safe_peek (q: t 'a) : 'a
requires { q.elts <> Nil }
ensures { match q.elts with Nil -> false
| Cons x _ -> result = x end }
val clear (q: t 'a) : unit writes {q} ensures { q.elts = Nil }
val copy (q: t 'a) : t 'a reads {q} ensures { result = q }
val copy (q: t 'a) : t 'a ensures { result = q }
val is_empty (q: t 'a) : bool reads {q}
val is_empty (q: t 'a) : bool
ensures { result = True <-> q.elts = Nil }
function length (q: t 'a) : int = L.length q.elts
val length (q: t 'a) : int reads {q}
val length (q: t 'a) : int
ensures { result = L.length q.elts }
end
......
......@@ -22,7 +22,7 @@ module Stack
| Cons x t -> result = x /\ s.elts = t end }
raises { Empty -> s.elts = old s.elts = Nil }
val top (s: t 'a) : 'a reads {s}
val top (s: t 'a) : 'a
ensures { match s.elts with Nil -> false
| Cons x _ -> result = x end }
raises { Empty -> s.elts = Nil }
......@@ -32,21 +32,21 @@ module Stack
ensures { match old s.elts with Nil -> false
| Cons x t -> result = x /\ s.elts = t end }
val safe_top (s: t 'a) : 'a reads {s}
val safe_top (s: t 'a) : 'a
requires { s.elts <> Nil }
ensures { match s.elts with Nil -> false
| Cons x _ -> result = x end }
val clear (s: t 'a) : unit writes {s} ensures { s.elts = Nil }
val copy (s: t 'a) : t 'a reads {s} ensures { result = s }
val copy (s: t 'a) : t 'a ensures { result = s }
val is_empty (s: t 'a) : bool reads {s}
val is_empty (s: t 'a) : bool
ensures { result = True <-> s.elts = Nil }
function length (s: t 'a) : int = L.length s.elts
val length (s: t 'a) : int reads {s}
val length (s: t 'a) : int
ensures { result = L.length s.elts }
end
......@@ -66,10 +66,10 @@ module String
ensures { length result = len }
ensures { forall i:int. 0 <= i < len -> result[i] = c }
val get (s:string) (i:int) : char reads {s}
val get (s:string) (i:int) : char
requires { 0 <= i < length s } ensures { result = s[i] }
val unsafe_get (s:string) (i:int) : char reads {s}
val unsafe_get (s:string) (i:int) : char
ensures { result = s[i] }
val set (s:string) (i:int) (v:char) : unit writes {s}
......@@ -79,7 +79,7 @@ module String
val unsafe_set (s:string) (i:int) (v:char) : unit writes {s}
ensures { s.chars = (old s.chars)[i <- v] }
val length (s:string) : int reads {s} ensures { result = length s }
val length (s:string) : int ensures { result = length s }
val copy (s:string) : string
ensures { length result = length s }
......@@ -124,7 +124,7 @@ module Buffer
requires { size >= 0 } ensures { result.length = 0 }
(** [size] is only given as a hint for the initial size *)
val contents (b:t) : string reads {b}
val contents (b:t) : string
ensures { S.length result = length b }
val add_char (b:t) (c:char) : unit writes {b}
......@@ -133,7 +133,7 @@ module Buffer
0 <= i < length b -> b.contents[i] = (old b.contents)[i] }
ensures { b.contents[length b - 1] = c }
val add_string (b:t) (s:string) : unit reads {s} writes {b}
val add_string (b:t) (s:string) : unit writes {b}
ensures { length b = old (length b) + S.length s }
ensures { forall i: int.
0 <= i < old (length b) -> b.contents[i] = (old b.contents)[i] }
......
......@@ -143,7 +143,6 @@ end
sp_pre = [];
sp_post = [];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_variant = [];
}
......@@ -152,7 +151,6 @@ end
sp_pre = s1.sp_pre @ s2.sp_pre;
sp_post = s1.sp_post @ s2.sp_post;
sp_xpost = s1.sp_xpost @ s2.sp_xpost;
sp_reads = s1.sp_reads @ s2.sp_reads;
sp_writes = s1.sp_writes @ s2.sp_writes;
sp_variant = variant_union s1.sp_variant s2.sp_variant;
}
......@@ -1385,7 +1383,8 @@ single_spec:
| RAISES LEFTBRC BAR raises RIGHTBRC
{ { empty_spec with sp_xpost = [floc_i 4, $4] } }
| READS LEFTBRC effect RIGHTBRC
{ { empty_spec with sp_reads = $3 } }
{ Warning.emit ~loc:(floc ()) "read effect annotations are deprecated";
empty_spec }
| WRITES LEFTBRC effect RIGHTBRC
{ { empty_spec with sp_writes = $3 } }
| RAISES LEFTBRC xsymbols RIGHTBRC
......
......@@ -193,7 +193,6 @@ type spec = {
sp_pre : pre list;
sp_post : post list;
sp_xpost : xpost list;
sp_reads : lexpr list;
sp_writes : lexpr list;
sp_variant : variant list;
}
......
......@@ -29,7 +29,6 @@ type dspec = {
ds_pre : dpre;
ds_post : dpost;
ds_xpost : dxpost;
ds_reads : deffect;
ds_writes : deffect;
ds_variant : dvariant list;
}
......
......@@ -125,7 +125,6 @@ type ppattern = {
ppat_pattern : pattern;
ppat_ity : ity;
ppat_ghost : bool;
ppat_effect : effect;
}
type pre_ppattern =
......@@ -151,24 +150,20 @@ let make_ppattern pp ?(ghost=false) ity =
Hstr.add hv nm pv; pv
in
let make_app ls ppl ghost ity =
let add_ppat e pp = eff_union e pp.ppat_effect, pp.ppat_pattern in
let effect, patl = Lists.map_fold_left add_ppat eff_empty ppl in
let patl = List.map (fun pp -> pp.ppat_pattern) ppl in
{ ppat_pattern = pat_app ls patl (ty_of_ity ity);
ppat_ity = ity;
ppat_ghost = ghost;
ppat_effect = effect; }
ppat_ghost = ghost; }
in
let rec make ghost ity = function
| PPwild -> {
ppat_pattern = pat_wild (ty_of_ity ity);
ppat_ity = ity;
ppat_ghost = ghost;
ppat_effect = eff_empty; }
ppat_ghost = ghost; }
| PPvar id -> {
ppat_pattern = pat_var (find id ghost ity).pv_vs;
ppat_ity = ity;
ppat_ghost = ghost;
ppat_effect = eff_empty; }
ppat_ghost = ghost; }
| PPpapp (pls,ppl) ->
if pls.pl_hidden then raise (HiddenPLS pls);
if pls.pl_ls.ls_constr = 0 then
......@@ -178,14 +173,7 @@ let make_ppattern pp ?(ghost=false) ity =
let sbs = ity_match ity_subst_empty ityv ity in
let mtch arg pp =
let ghost = ghost || arg.fd_ghost in
let pp = make ghost (ity_full_inst sbs arg.fd_ity) pp in
match pp.ppat_pattern.pat_node, arg.fd_mut with
| Pwild, _ -> pp
| _, Some r ->
let reg = reg_full_inst sbs r in
let eff = eff_read ~ghost pp.ppat_effect reg in
{ pp with ppat_effect = eff }
| _, _ -> pp in
make ghost (ity_full_inst sbs arg.fd_ity) pp in
let ppl = try List.map2 mtch pls.pl_args ppl with
| Not_found -> raise (Term.ConstructorExpected pls.pl_ls)
| Invalid_argument _ -> raise (Term.BadArity
......@@ -209,14 +197,12 @@ let make_ppattern pp ?(ghost=false) ity =
let pp2 = make ghost ity pp2 in
{ ppat_pattern = pat_or pp1.ppat_pattern pp2.ppat_pattern;
ppat_ity = ity;
ppat_ghost = ghost;
ppat_effect = eff_union pp1.ppat_effect pp2.ppat_effect; }
ppat_ghost = ghost; }
| PPas (pp,id) ->
let pp = make ghost ity pp in
{ ppat_pattern = pat_as pp.ppat_pattern (find id ghost ity).pv_vs;
ppat_ity = ity;
ppat_ghost = ghost;
ppat_effect = pp.ppat_effect; }
ppat_ghost = ghost; }
in
let pp = make ghost ity pp in
let gh = pp.ppat_ghost || !gghost in
......@@ -291,9 +277,7 @@ let rec aty_check vars aty =
let ch_tv tv = test_or_raise (Stv.mem tv vars.vars_tv) in
let check reg = test_or_raise (reg_occurs reg vars) in
let eff = aty.aty_spec.c_effect in
Sreg.iter check eff.eff_reads;
Sreg.iter check eff.eff_writes;
Sreg.iter check eff.eff_ghostr;
Sreg.iter check eff.eff_ghostw;
Stv.iter ch_tv eff.eff_compar;
match aty.aty_result with
......@@ -609,9 +593,8 @@ let e_plapp pls el ity =
if pls.pl_rdonly then raise (RdOnlyPLS pls);
let rec app tl syms ghost eff sbs fdl argl = match fdl, argl with
| [],[] ->
let mut_fold fn leff fd = Opt.fold fn leff fd.fd_mut in
let leff = mut_fold (eff_read ~ghost) eff_empty pls.pl_value in
let leff = List.fold_left (mut_fold eff_reset) leff pls.pl_args in
let mut_fold leff fd = Opt.fold eff_reset leff fd.fd_mut in
let leff = List.fold_left mut_fold eff_empty pls.pl_args in
let mtv = Mtv.set_diff sbs.ity_subst_tv pls.pl_ls.ls_opaque in
let leff = Mtv.fold (fun tv _ e -> eff_compare e tv) mtv leff in
let eff = eff_union eff (eff_full_inst sbs leff) in
......@@ -678,9 +661,9 @@ let e_case e0 bl =
Loc.errorm "Non-ghost pattern in a ghost position";
ity_equal_check (ity_of_expr e0) pp.ppat_ity;
ity_equal_check (ity_of_expr e) bity;
let eff = eff_union eff e.e_effect in
let del_vs vs _ syms = del_pv_syms (restore_pv vs) syms in
let bsyms = Mvs.fold del_vs pp.ppat_pattern.pat_vars e.e_syms in
let eff = eff_union (eff_union eff pp.ppat_effect) e.e_effect in
(* one-branch match is not ghost even if its pattern is ghost *)
let ghost = ghost || (multi_br && pp.ppat_ghost) || e.e_ghost in
branch ghost eff (syms_union syms bsyms) bl
......
......@@ -64,7 +64,6 @@ type ppattern = private {
ppat_pattern : pattern;
ppat_ity : ity;
ppat_ghost : bool;
ppat_effect : effect;
}
type pre_ppattern =
......
......@@ -437,9 +437,6 @@ let clone_export uc m inst =
| XS xs -> xs | _ -> assert false with Not_found -> xs in
let conv_eff eff =
let e = eff_empty in
let conv ghost r e = eff_read ~ghost e (conv_reg r) in
let e = Sreg.fold (conv false) eff.eff_reads e in
let e = Sreg.fold (conv true) eff.eff_ghostr e in
let conv ghost r e = eff_write ~ghost e (conv_reg r) in
let e = Sreg.fold (conv false) eff.eff_writes e in
let e = Sreg.fold (conv true) eff.eff_ghostw e in
......
......@@ -116,10 +116,8 @@ let print_effect fmt eff =
| Some u ->
fprintf fmt "{refresh %a@ under %a}@ " print_regty r print_regty u
in
Sreg.iter (print_reg "read") eff.eff_reads;
Sreg.iter (print_reg "write") eff.eff_writes;
Sexn.iter (print_xs "raise") eff.eff_raises;
Sreg.iter (print_reg "ghost read") eff.eff_ghostr;
Sreg.iter (print_reg "ghost write") eff.eff_ghostw;
Sexn.iter (print_xs "ghost raise") eff.eff_ghostx;
Mreg.iter print_reset eff.eff_resets
......
......@@ -572,10 +572,8 @@ module Mexn = Exn.M
(* effects *)
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) *)
......@@ -585,10 +583,8 @@ type effect = {
}
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;
......@@ -597,17 +593,6 @@ let eff_empty = {
}
let eff_is_empty e =
Sreg.is_empty e.eff_reads &&
Sreg.is_empty e.eff_writes &&
Sexn.is_empty e.eff_raises &&
Sreg.is_empty e.eff_ghostr &&
Sreg.is_empty e.eff_ghostw &&
Sexn.is_empty e.eff_ghostx &&
Mreg.is_empty e.eff_resets &&
(* eff_compar is not a side effect *)
not e.eff_diverg
let eff_is_read_only e =
Sreg.is_empty e.eff_writes &&
Sexn.is_empty e.eff_raises &&
Sreg.is_empty e.eff_ghostw &&
......@@ -617,10 +602,8 @@ let eff_is_read_only e =
not e.eff_diverg
let eff_equal e1 e2 =
Sreg.equal e1.eff_reads e2.eff_reads &&
Sreg.equal e1.eff_writes e2.eff_writes &&
Sexn.equal e1.eff_raises e2.eff_raises &&
Sreg.equal e1.eff_ghostr e2.eff_ghostr &&
Sreg.equal e1.eff_ghostw e2.eff_ghostw &&
Sexn.equal e1.eff_ghostx e2.eff_ghostx &&
Mreg.equal (Opt.equal reg_equal) e1.eff_resets e2.eff_resets &&
......@@ -636,10 +619,8 @@ let join_reset _key v1 v2 = match v1, v2 with
| _ -> Some 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_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;
......@@ -650,10 +631,8 @@ let eff_union x y = {
exception GhostDiverg
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;
......@@ -669,10 +648,6 @@ let eff_ghostify e = {
let eff_ghostify gh e = if gh then eff_ghostify e else e
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 }
......@@ -748,9 +723,7 @@ let eff_full_inst sbs e =
ity_s_fold check (fun () _ -> ()) () ity;
Stv.union acc ity.ity_vars.vars_tv in
{ 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;
eff_compar = Stv.fold add_stv e.eff_compar Stv.empty;
......@@ -764,9 +737,7 @@ let eff_filter vars e =
| _ -> Some None
in
{ e with
eff_reads = Sreg.filter check e.eff_reads;
eff_writes = Sreg.filter check e.eff_writes;
eff_ghostr = Sreg.filter check e.eff_ghostr;
eff_ghostw = Sreg.filter check e.eff_ghostw;
eff_resets = Mreg.mapi_filter reset e.eff_resets;
eff_compar = Stv.inter vars.vars_tv e.eff_compar;
......
......@@ -199,10 +199,8 @@ module Sexn: Extset.S with module M = Mexn
(** effects *)
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) *)
......@@ -216,7 +214,6 @@ val eff_equal : effect -> effect -> bool
val eff_union : effect -> effect -> effect
val eff_ghostify : bool -> effect -> 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
......@@ -238,7 +235,6 @@ exception GhostDiverg
val eff_full_inst : ity_subst -> effect -> effect
val eff_is_empty : effect -> bool
val eff_is_read_only: effect -> bool
(** specification *)
......
......@@ -430,7 +430,6 @@ let dspec uc sp = {
ds_pre = sp.sp_pre;
ds_post = dpost sp.sp_post;
ds_xpost = dxpost uc sp.sp_xpost;
ds_reads = sp.sp_reads;
ds_writes = sp.sp_writes;
ds_variant = dvariant uc sp.sp_variant;
}
......@@ -1154,8 +1153,6 @@ let get_eff_regs lenv fn (eff,svs) le =
let eff_of_deff lenv dsp =
let acc = eff_empty, Svs.empty in
let add_read acc e = get_eff_regs lenv eff_read acc e in
let acc = List.fold_left add_read acc dsp.ds_reads in
let add_write acc e = get_eff_regs lenv eff_write acc e in
let eff, svs = List.fold_left add_write acc dsp.ds_writes in
let add_raise xs _ eff = eff_raise eff xs in
......@@ -1166,21 +1163,12 @@ let e_find_loc pr e =
with Not_found -> None
let check_user_effect lenv e eeff full_xpost dsp =
let has_read reg eff =
Sreg.mem reg eff.eff_reads || Sreg.mem reg eff.eff_ghostr in
let has_write reg eff =
Sreg.mem reg eff.eff_writes || Sreg.mem reg eff.eff_ghostw in
let has_raise xs eff =
Sexn.mem xs eff.eff_raises || Sexn.mem xs eff.eff_ghostx in
(* check that every user effect actually happens *)
let acc = eff_empty, Svs.empty in
let read le ueff ?ghost reg =
if has_read reg eeff then eff_read ?ghost ueff reg
else Loc.errorm ~loc:le.pp_loc
"this read effect never happens in the expression" in
let add_read acc e = get_eff_regs lenv (read e) acc e in
let acc = List.fold_left add_read acc dsp.ds_reads in
let ueff_ro = not (eff_is_empty (fst acc)) in
let write le ueff ?ghost reg =
if has_write reg eeff then eff_write ?ghost ueff reg
else Loc.errorm ~loc:le.pp_loc
......@@ -1194,11 +1182,6 @@ let check_user_effect lenv e eeff full_xpost dsp =
"this expression does not raise exception %a" print_xs xs in
let ueff = Mexn.fold add_raise dsp.ds_xpost ueff in
(* check that every computed effect is listed *)
let check_read reg = if not (has_read reg ueff) then
Loc.errorm ?loc:(e_find_loc (fun e -> has_read reg e.e_effect) e)
"this expression produces an unlisted read effect" in
if ueff_ro then Sreg.iter check_read eeff.eff_reads;
if ueff_ro then Sreg.iter check_read eeff.eff_ghostr;
let check_write reg = if not (has_write reg ueff) then
Loc.errorm ?loc:(e_find_loc (fun e -> has_write reg e.e_effect) e)
"this expression produces an unlisted write effect" in
......
......@@ -1684,7 +1684,7 @@ let wp_rec ~wp env kn th fdl =
if Slab.mem lemma_label name.id_label then
let loc = name.id_loc in
let spec = ps.ps_aty.aty_spec in
if not (eff_is_read_only spec.c_effect) then
if not (eff_is_empty spec.c_effect) then
Loc.errorm ?loc "lemma functions can not have effects";
if not (ity_equal (ity_of_expr l.l_expr) ity_unit) then
Loc.errorm ?loc "lemma functions must return unit";
......
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