Commit e1c01e09 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: check for ghost effects in toplevel symbols

parent 8cb787a3
......@@ -320,7 +320,24 @@ let known_add_decl lkn0 kn0 d =
if Sid.is_empty unk then kn
else raise (UnknownIdent (Sid.choose unk))
let check_match lkn d =
let rec find_td its1 = function
| (its2,csl,inv) :: _ when its_equal its1 its2 -> csl,inv
| _ :: tdl -> find_td its1 tdl
| [] -> raise Not_found
let find_constructors kn its =
match (Mid.find its.its_pure.ts_name kn).pd_node with
| PDtype _ -> []
| PDdata tdl -> fst (find_td its tdl)
| PDval _ | PDlet _ | PDrec _ | PDexn _ -> assert false
let find_invariant kn its =
match (Mid.find its.its_pure.ts_name kn).pd_node with
| PDtype _ -> null_invariant its
| PDdata tdl -> snd (find_td its tdl)
| PDval _ | PDlet _ | PDrec _ | PDexn _ -> assert false
let check_match lkn _kn d =
let rec checkE () e = match e.e_node with
| Ecase (e1,bl) ->
let typ = ty_of_ity (vtv_of_expr e1).vtv_ity in
......@@ -340,24 +357,70 @@ let check_match lkn d =
| PDlet { let_expr = e } -> checkE () e
| PDval _ | PDtype _ | PDdata _ | PDexn _ -> ()
exception NonupdatableType of ity
let inst_constructors lkn kn ity = match ity.ity_node with
| Itypur (ts,_) ->
let csl = Decl.find_constructors lkn ts in
let d = Mid.find ts.ts_name lkn in
let is_rec = Mid.mem ts.ts_name d.Decl.d_syms in
if csl = [] || is_rec then raise (NonupdatableType ity);
let base = ity_pur ts (List.map ity_var ts.ts_args) in
let sbs = ity_match ity_subst_empty base ity in
let subst ty = vty_value (ity_full_inst sbs (ity_of_ty ty)) in
List.map (fun (cs,_) -> cs, List.map subst cs.ls_args) csl
| Ityapp (its,_,_) ->
let csl = find_constructors kn its in
let d = Mid.find its.its_pure.ts_name lkn in
let is_rec = Mid.mem its.its_pure.ts_name d.Decl.d_syms in
if csl = [] || is_rec then raise (NonupdatableType ity);
let base = ity_app its (List.map ity_var its.its_args) its.its_regs in
let sbs = ity_match ity_subst_empty base ity in
let subst vtv =
let ghost = vtv.vtv_ghost in
let mut = Util.option_map (reg_full_inst sbs) vtv.vtv_mut in
vty_value ~ghost ?mut (ity_full_inst sbs vtv.vtv_ity) in
List.map (fun (cs,_) -> cs.pl_ls, List.map subst cs.pl_args) csl
| Ityvar _ ->
invalid_arg "Mlw_decl.inst_constructors"
let check_ghost lkn kn d =
let rec access regs ity =
let check vtv = match vtv.vtv_mut with
| _ when vtv.vtv_ghost -> ()
| Some r when Sreg.mem r regs -> raise (GhostWrite (e_void, r))
| _ -> access regs vtv.vtv_ity in
let check (_cs,vtvl) = List.iter check vtvl in
let occurs r = reg_occurs r ity.ity_vars in
if not (Sreg.exists occurs regs) then () else
List.iter check (inst_constructors lkn kn ity)
in
let rec check pvs vta =
let eff = vta.vta_spec.c_effect in
if not (Sexn.is_empty eff.eff_ghostx) then
raise (GhostRaise (e_void, Sexn.choose eff.eff_ghostx));
let pvs = List.fold_right Spv.add vta.vta_args pvs in
let test pv =
if pv.pv_vtv.vtv_ghost then () else
access eff.eff_ghostw pv.pv_vtv.vtv_ity
in
Spv.iter test pvs;
match vta.vta_result with
| VTarrow vta -> check pvs vta
| VTvalue _ -> ()
in
let check ps =
if ps.ps_vta.vta_ghost then () else
check (ps_pvset Spv.empty ps) ps.ps_vta
in
match d.pd_node with
| PDrec rd -> List.iter (fun fd -> check fd.fun_ps) rd.rec_defn
| PDval (LetA ps) | PDlet { let_sym = LetA ps } -> check ps
| PDval _ | PDlet _ | PDtype _ | PDdata _ | PDexn _ -> ()
let known_add_decl lkn kn d =
let kn = known_add_decl lkn kn d in
check_match lkn d;
check_ghost lkn kn d;
check_match lkn kn d;
kn
let rec find_td its1 = function
| (its2,csl,inv) :: _ when its_equal its1 its2 -> csl,inv
| _ :: tdl -> find_td its1 tdl
| [] -> raise Not_found
let find_constructors kn its =
match (Mid.find its.its_pure.ts_name kn).pd_node with
| PDtype _ -> []
| PDdata tdl -> fst (find_td its tdl)
| PDval _ | PDlet _ | PDrec _ | PDexn _ -> assert false
let find_invariant kn its =
match (Mid.find its.its_pure.ts_name kn).pd_node with
| PDtype _ -> null_invariant its
| PDdata tdl -> snd (find_td its tdl)
| PDval _ | PDlet _ | PDrec _ | PDexn _ -> assert false
......@@ -86,3 +86,8 @@ val merge_known : known_map -> known_map -> known_map
val find_constructors : known_map -> itysymbol -> constructor list
val find_invariant : known_map -> itysymbol -> post
exception NonupdatableType of ity
val inst_constructors :
Decl.known_map -> known_map -> ity -> (lsymbol * vty_value list) list
......@@ -524,11 +524,15 @@ let pv_effect pv = match pv.pv_vtv.vtv_mut with
let add_e_vars e m = varmap_union e.e_varm m
let e_pvset pvs e =
let varmap_pvset pvs varm =
let add_id id _ s =
try Spv.add (restore_pv_by_id id) s
with Not_found -> s in
Mid.fold add_id e.e_varm pvs
Mid.fold add_id varm pvs
let ps_pvset pvs ps = varmap_pvset pvs ps.ps_varm
let e_pvset pvs e = varmap_pvset pvs e.e_varm
let spec_of_lambda lam letrec = {
c_pre = lam.l_pre;
......
......@@ -121,6 +121,7 @@ val create_psymbol : preid -> vty_arrow -> psymbol
val create_psymbol_extra : preid -> vty_arrow -> Spv.t -> Sps.t -> psymbol
val spec_pvset : Spv.t -> spec -> Spv.t
val ps_pvset : Spv.t -> psymbol -> Spv.t
(** program expressions *)
......
......@@ -465,8 +465,8 @@ let () = Exn_printer.register
| Mlw_expr.GhostWrite (_e, _reg) ->
fprintf fmt "This expression stores a ghost value in a non-ghost location"
| Mlw_expr.GhostRaise (_e, xs) ->
fprintf fmt "This expression raises a ghost exception %a \
catched by a non-ghost code" print_xs xs
fprintf fmt "This expression raises an escaping ghost exception %a"
print_xs xs
| Mlw_expr.StaleRegion (_e, id) ->
fprintf fmt "This expression prohibits further \
usage of variable %s" id.id_string
......@@ -476,5 +476,7 @@ let () = Exn_printer.register
fprintf fmt "This expression is not a function and cannot be applied"
| Mlw_expr.Immutable _e ->
fprintf fmt "Mutable expression expected"
| Mlw_decl.NonupdatableType ity ->
fprintf fmt "Cannot update values of type @[%a@]" print_ity ity
| _ -> raise exn
end
......@@ -270,52 +270,26 @@ let decrease ?loc env olds varl =
(** Reconstruct pure values after writes *)
let find_constructors lkm km sts ity = match ity.ity_node with
| Itypur (ts,_) ->
let base = ity_pur ts (List.map ity_var ts.ts_args) in
let sbs = ity_match ity_subst_empty base ity in
let csl = Decl.find_constructors lkm ts in
if csl = [] || Sts.mem ts sts then Loc.errorm
"Cannot update values of type %a" Mlw_pretty.print_ity base;
let subst ty = ity_full_inst sbs (ity_of_ty ty), None in
let cnstr (cs,_) = cs, List.map subst cs.ls_args in
Sts.add ts sts, List.map cnstr csl
| Ityapp (its,_,_) ->
let base = ity_app its (List.map ity_var its.its_args) its.its_regs in
let sbs = ity_match ity_subst_empty base ity in
let csl = Mlw_decl.find_constructors km its in
if csl = [] || Sts.mem its.its_pure sts then Loc.errorm
"Cannot update values of type %a" Mlw_pretty.print_ity base;
let subst vtv =
ity_full_inst sbs vtv.vtv_ity,
Util.option_map (reg_full_inst sbs) vtv.vtv_mut in
let cnstr (cs,_) = cs.pl_ls, List.map subst cs.pl_args in
Sts.add its.its_pure sts, List.map cnstr csl
| Ityvar _ -> assert false
let analyze_var fn_down fn_join lkm km sts vs ity =
let sts, csl = find_constructors lkm km sts ity in
let branch (cs,ityl) =
let mk_var (ity,_) = create_vsymbol (id_fresh "y") (ty_of_ity ity) in
let vars = List.map mk_var ityl in
let mk_arg vs (ity, mut) = fn_down sts vs ity mut in
let t = fn_join cs (List.map2 mk_arg vars ityl) vs.vs_ty in
let analyze_var fn_down fn_join lkm km vs ity =
let branch (cs,vtvl) =
let mk_var vtv = create_vsymbol (id_fresh "y") (ty_of_ity vtv.vtv_ity) in
let vars = List.map mk_var vtvl in
let t = fn_join cs (List.map2 fn_down vars vtvl) vs.vs_ty in
let pat = pat_app cs (List.map pat_var vars) vs.vs_ty in
t_close_branch pat t in
t_case (t_var vs) (List.map branch csl)
t_case (t_var vs) (List.map branch (Mlw_decl.inst_constructors lkm km ity))
let update_var env mreg vs =
let rec update sts vs ity mut =
let rec update vs { vtv_ity = ity; vtv_mut = mut } =
(* are we a mutable variable? *)
let get_vs r = Mreg.find_def vs r mreg in
let vs = Util.option_apply vs get_vs mut in
(* should we update our value further? *)
let check_reg r _ = reg_occurs r ity.ity_vars in
if ity_pure ity || not (Mreg.exists check_reg mreg) then t_var vs
else analyze_var update fs_app env.pure_known env.prog_known sts vs ity
else analyze_var update fs_app env.pure_known env.prog_known vs ity
in
let vtv = vtv_of_vs vs in
update Sts.empty vs vtv.vtv_ity vtv.vtv_mut
update vs (vtv_of_vs vs)
(* substitute the updated values in the "contemporary" variables *)
let rec subst_at_now now m t = match t.t_node with
......@@ -404,7 +378,7 @@ let ps_inv = Term.create_psymbol (id_fresh "inv")
[ty_var (create_tvsymbol (id_fresh "a"))]
let full_invariant lkm km vs ity =
let rec update sts vs ity _ =
let rec update vs { vtv_ity = ity } =
if not (ity_inv ity) then t_true else
(* what is our current invariant? *)
let f = match ity.ity_node with
......@@ -415,11 +389,11 @@ let full_invariant lkm km vs ity =
| _ -> t_true in
(* what are our sub-invariants? *)
let join _ fl _ = wp_ands ~sym:true fl in
let g = analyze_var update join lkm km sts vs ity in
let g = analyze_var update join lkm km vs ity in
(* put everything together *)
wp_and ~sym:true f g
in
update Sts.empty vs ity None
update vs (vty_value ity)
(** Value tracking *)
......
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