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

Expr: check for illegal ghost writes

parent 03640fbb
......@@ -197,6 +197,8 @@ type invariant = term
type variant = term * lsymbol option (** tau * (tau -> tau -> prop) *)
type assign = pvsymbol * pvsymbol * pvsymbol (* region * field * value *)
type vty =
| VtyI of ity
| VtyC of cty
......@@ -226,7 +228,7 @@ and expr_node =
| Elazy of lazy_op * expr * expr
| Eif of expr * expr * expr
| Ecase of expr * (prog_pattern * expr) list
| Eassign of expr * pvsymbol (*field*) * pvsymbol
| Eassign of assign list
| Ewhile of expr * invariant * variant list * expr
| Efor of pvsymbol * for_bounds * invariant * expr
| Etry of expr * (xsymbol * pvsymbol * expr) list
......@@ -297,14 +299,15 @@ let e_const c =
let e_nat_const n =
e_const (Number.ConstInt (Number.int_const_dec (string_of_int n)))
let create_let_defn id e =
let ghost = e.e_ghost in
let create_let_defn id ?(ghost=false) e =
let ghost = ghost || e.e_ghost in
let lv = match e.e_vty with
| VtyC c -> ValS (create_psymbol id ~ghost ~kind:PKnone c)
| VtyI i -> ValV (create_pvsymbol id ~ghost i) in
{ let_sym = lv; let_expr = e }
let create_let_defn_pv id e =
let create_let_defn_pv id ?(ghost=false) e =
let ghost = ghost || e.e_ghost in
let ity = match e.e_vty with
| VtyC ({ cty_args = args; cty_result = res } as c) ->
let error s = Loc.errorm
......@@ -318,10 +321,11 @@ let create_let_defn_pv id e =
if c.cty_pre <> [] then error "is partial";
List.fold_right (fun a i -> ity_func a.pv_ity i) args res
| VtyI i -> i in
let pv = create_pvsymbol id ~ghost:e.e_ghost ity in
let pv = create_pvsymbol id ~ghost ity in
{ let_sym = ValV pv; let_expr = e }, pv
let create_let_defn_ps id ?(kind=PKnone) e =
let create_let_defn_ps id ?(ghost=false) ?(kind=PKnone) e =
let ghost = ghost || e.e_ghost in
let cty = match e.e_vty, kind with
| _, PKfunc n when n > 0 -> invalid_arg "Expr.create_let_defn_ps"
| VtyI _, (PKnone|PKlocal|PKlemma) -> Loc.errorm
......@@ -332,68 +336,125 @@ let create_let_defn_ps id ?(kind=PKnone) e =
| VtyI _, (PKfunc _|PKpred) -> Loc.errorm
"this expression is non-pure, it cannot be used as a pure function"
| VtyC c, _ -> c in
let ps = create_psymbol id ~ghost:e.e_ghost ~kind cty in
let ps = create_psymbol id ~ghost ~kind cty in
{ let_sym = ValS ps; let_expr = e }, ps
let rec get_reads pvs pss acc e =
let add_v acc v =
if Spv.mem v pvs then acc else Spv.add v acc in
let add_c acc c =
let pvs = List.fold_right Spv.add c.cty_args pvs in
Spv.union (Spv.diff c.cty_reads pvs) acc in
let add_s acc s =
if Sps.mem s pss then acc else add_c acc s.ps_cty in
let add_r acc r = Spv.union (Spv.diff r pvs) acc in
let add_c acc c = add_r acc c.cty_reads in
let add_v acc v = if Spv.mem v pvs then acc else Spv.add v acc in
let add_s acc s = if Sps.mem s pss then acc else add_c acc s.ps_cty in
match e.e_node with
| Evar v -> add_v acc v
| Esym s -> add_s acc s
| Efun _ | Eany -> add_c acc (cty_of_expr e)
| Eapp (e,l,_) ->
get_reads pvs pss (List.fold_left add_v acc l) e
| Eapp (e,l,_) -> get_reads pvs pss (List.fold_left add_v acc l) e
| Elet ({let_sym = ValV v; let_expr = d},e) ->
get_reads (Spv.add v pvs) pss (get_reads pvs pss acc d) e
| Elet ({let_sym = ValS s; let_expr = d},e) ->
get_reads pvs (Sps.add s pss) (get_reads pvs pss acc d) e
| Erec ({rec_defn = fdl},e) ->
let add_ps pss fd = Sps.add fd.fun_sym pss in
let pss = List.fold_left add_ps pss fdl in
let add_rs pss fd = Sps.add fd.fun_sym pss in
let pss = List.fold_left add_rs pss fdl in
(* we ignore variants as they will appear in the bodies *)
let add_fd acc fd = get_reads pvs pss acc fd.fun_expr in
get_reads pvs pss (List.fold_left add_fd acc fdl) e
| Enot e | Eraise (_,e) | Eghost e ->
get_reads pvs pss acc e
| Elazy (_,d,e) ->
get_reads pvs pss (get_reads pvs pss acc d) e
| Enot e | Eraise (_,e) | Eghost e -> get_reads pvs pss acc e
| Elazy (_,d,e) -> get_reads pvs pss (get_reads pvs pss acc d) e
| Eif (c,d,e) ->
let acc = get_reads pvs pss acc c in
get_reads pvs pss (get_reads pvs pss acc d) e
| Eassign (e,_,v) ->
get_reads pvs pss (add_v acc v) e
| Etry (e,xl) ->
let add acc (_,v,e) =
get_reads (Spv.add v pvs) pss acc e in
List.fold_left add (get_reads pvs pss acc e) xl
| Eassign al ->
let add acc (r,_,v) = add_v (add_v acc r) v in
List.fold_left add acc al
| Etry (d,xl) ->
let add acc (_,v,e) = get_reads (Spv.add v pvs) pss acc e in
List.fold_left add (get_reads pvs pss acc d) xl
| Ecase (d,bl) ->
let add acc (pp,e) =
let pvs = pvs_of_vss pvs pp.pp_pat.pat_vars in
get_reads pvs pss acc e in
get_reads (pvs_of_vss pvs pp.pp_pat.pat_vars) pss acc e in
List.fold_left add (get_reads pvs pss acc d) bl
| Ewhile (d,inv,vl,e) ->
let acc = get_reads pvs pss acc d in
let spc = t_freepvs Spv.empty inv in
let add spc (t,_) = t_freepvs spc t in
let spc = List.fold_left add spc vl in
let acc = Spv.union (Spv.diff spc pvs) acc in
get_reads pvs pss acc e
let spc = List.fold_left add (t_freepvs Spv.empty inv) vl in
get_reads pvs pss (get_reads pvs pss (add_r acc spc) d) e
| Efor (v,(f,_,t),inv,e) ->
let pvs = Spv.add v pvs in
let spc = t_freepvs Spv.empty inv in
let acc = Spv.union (Spv.diff spc pvs) acc in
get_reads pvs pss (add_v (add_v acc f) t) e
| Eassert (_,t) | Epure t ->
Spv.union (Spv.diff (t_freepvs Spv.empty t) pvs) acc
let acc = add_r acc (Spv.remove v (t_freepvs Spv.empty inv)) in
get_reads (Spv.add v pvs) pss (add_v (add_v acc f) t) e
| Eassert (_,t) | Epure t -> add_r acc (t_freepvs Spv.empty t)
| Econst _ | Eabsurd -> acc
let e_fun args p q xq e =
let pv_r_visible v vis =
if v.pv_ghost then vis else ity_r_visible vis v.pv_ity
let cty_r_visible c =
List.fold_right pv_r_visible c.cty_args
(Spv.fold pv_r_visible c.cty_reads Sreg.empty)
(* A non-ghost application can perform ghost writes into ghost fields
or into ghost arguments. The former is always safe, but the latter
is illegal, if we submit a visible region inside a ghost argument.
A write effect of a computation is ghost whenever the modified region
is not visible in any non-ghost argument or read dependency. Indeed,
if there is at least one non-ghost dependency of a computation where
the modified region is visible, then the write can not be ghost, or
the computation itself would have been rejected. For this check to
be correct, Ity.cty_apply does not accept non-ghost pvsymbols for
ghost arguments. Otherwise, we would put a non-ghost pvsymbol in
cty_reads and would mistakenly consider the write effect non-ghost. *)
let cty_ghost_writes gh c =
let wr = c.cty_effect.eff_writes in
(* If we only write into ghost fields, we do not care.
However, if the type is private, we do not know all
modified fields, and thus cannot exclude the region. *)
let wr = Mreg.filter (fun r fs -> r.reg_its.its_private
|| Spv.exists (fun f -> not f.pv_ghost) fs) wr in
if gh || Mreg.is_empty wr then wr
else Mreg.set_diff wr (cty_r_visible c)
let rec check_ghost_writes vis gh e =
let gh = gh || e.e_ghost in
let add_v v vis = if gh then vis else pv_r_visible v vis in
let add_s s vis = if gh || s.ps_ghost then vis else
Spv.fold pv_r_visible s.ps_cty.cty_reads vis in
let error () = Loc.errorm ?loc:e.e_loc
"this expression makes a ghost write in a non-ghost location" in
match e.e_node with
| Evar _ | Esym _ | Efun _ | Eany
| Eassert _ | Epure _ | Econst _ | Eabsurd -> ()
| Enot e | Eraise (_,e) | Eghost e
| Erec (_,e) | Efor (_,_,_,e) ->
check_ghost_writes vis gh e
| Elazy (_,d,e) | Ewhile (d,_,_,e) ->
check_ghost_writes vis gh d; check_ghost_writes vis gh e
| Eif (c,d,e) -> check_ghost_writes vis gh c;
check_ghost_writes vis gh d; check_ghost_writes vis gh e
| Elet ({let_sym = ValV v; let_expr = d},e) ->
check_ghost_writes vis gh d;
check_ghost_writes (add_v v vis) gh e;
| Elet ({let_sym = ValS s; let_expr = d},e) ->
check_ghost_writes vis gh d;
check_ghost_writes (add_s s vis) gh e
| Etry (d,xl) ->
check_ghost_writes vis gh d;
List.iter (fun (_,_,e) -> check_ghost_writes vis gh e) xl
| Ecase (d,bl) ->
check_ghost_writes vis gh d;
List.iter (fun (pp,e) ->
let pvs = pvs_of_vss Spv.empty pp.pp_pat.pat_vars in
check_ghost_writes (Spv.fold add_v pvs vis) gh e) bl
| Eassign al ->
List.iter (fun (r,f,v) -> (* ghost writes in visible fields *)
if not f.pv_ghost && (gh || r.pv_ghost || v.pv_ghost) then
match r.pv_ity.ity_node with
| Ityreg r when Sreg.mem r vis -> error () | _ -> ()) al
| Eapp (e,vl,c) ->
if c.cty_args <> [] (* partial application *) ||
Mreg.set_disjoint vis (cty_ghost_writes gh c)
then check_ghost_writes vis gh e else error ()
let e_fun args p q xq ({e_effect = eff} as e) =
let pvs = get_reads Spv.empty Sps.empty Spv.empty e in
let c = create_cty args p q xq pvs e.e_effect (ity_of_expr e) in
let c = create_cty args p q xq pvs eff (ity_of_expr e) in
check_ghost_writes (cty_r_visible c) false e;
mk_expr (Efun e) (VtyC c) e.e_ghost eff_empty
......@@ -90,6 +90,8 @@ type invariant = term
type variant = term * lsymbol option (** tau * (tau -> tau -> prop) *)
type assign = pvsymbol * pvsymbol * pvsymbol (* region * field * value *)
type vty =
| VtyI of ity
| VtyC of cty
......@@ -119,7 +121,7 @@ and expr_node = private
| Elazy of lazy_op * expr * expr
| Eif of expr * expr * expr
| Ecase of expr * (prog_pattern * expr) list
| Eassign of expr * pvsymbol (*field*) * pvsymbol
| Eassign of assign list
| Ewhile of expr * invariant * variant list * expr
| Efor of pvsymbol * for_bounds * invariant * expr
| Etry of expr * (xsymbol * pvsymbol * expr) list
......@@ -163,9 +165,12 @@ val e_sym : psymbol -> expr
val e_const : Number.constant -> expr
val e_nat_const : int -> expr
val create_let_defn : preid -> expr -> let_defn
val create_let_defn_pv : preid -> expr -> let_defn * pvsymbol
val create_let_defn_ps : preid -> ?kind:ps_kind -> expr -> let_defn * psymbol
val create_let_defn : preid -> ?ghost:bool -> expr -> let_defn
val create_let_defn_pv : preid -> ?ghost:bool -> expr -> let_defn * pvsymbol
val create_let_defn_ps :
preid -> ?ghost:bool -> ?kind:ps_kind -> expr -> let_defn * psymbol
val e_fun :
pvsymbol list -> pre list -> post list -> post list Mexn.t -> expr -> expr
......@@ -815,12 +815,14 @@ let spec_t_fold fn_t acc pre post xpost =
let acc = fn_l (fn_l acc pre) post in
Mexn.fold (fun _ l a -> fn_l a l) xpost acc
let check_tvs reads result pre post xpost =
let check_tvs reads args result pre post xpost =
(* every type variable in spec comes either from a known vsymbol
or from the result type. We need this to ensure that we always
can do a full instantiation. TODO: do we really need this? *)
let add_pv v s = ity_freevars s v.pv_ity in
let tvs = Spv.fold add_pv reads (ity_freevars Stv.empty result) in
let tvs = ity_freevars Stv.empty result in
let tvs = List.fold_right add_pv args tvs in
let tvs = Spv.fold add_pv reads tvs in
let check_tvs () t =
let ttv = t_ty_freevars Stv.empty t in
if not (Stv.subset ttv tvs) then Loc.error ?loc:t.t_loc
......@@ -843,11 +845,11 @@ let create_cty args pre post xpost reads effect result =
Mexn.iter (fun xs xq -> check_post exn xs.xs_ity xq) xpost;
(* the arguments must be pairwise distinct *)
let sarg = List.fold_right (Spv.add_new exn) args Spv.empty in
(* complete reads and freeze the external context *)
(* remove args from reads and freeze the external context *)
let reads = spec_t_fold t_freepvs reads pre post xpost in
let freeze = Spv.fold freeze_pv (Spv.diff reads sarg) isb_empty in
let reads = Spv.union reads sarg in
check_tvs reads result pre post xpost;
let reads = Spv.diff reads sarg in
let freeze = Spv.fold freeze_pv reads isb_empty in
check_tvs reads args result pre post xpost;
(* remove exceptions whose postcondition is False *)
let is_false _ xq = List.exists (t_equal t_false) xq in
let nothrow = Mexn.filter is_false xpost in
......@@ -873,7 +875,7 @@ let t_subst_l vsb l = List.map (fun t -> t_subst vsb t) l
let cty_apply c pvl args res =
let rec apply isb same gh vsb al vl = match al, vl with
| a::al, v::vl ->
| a::al, v::vl when v.pv_ghost || not a.pv_ghost ->
let isb = ity_match isb a.pv_ity v.pv_ity in
let same = same && ity_equal a.pv_ity v.pv_ity in
let gh = gh || (v.pv_ghost && not a.pv_ghost) in
......@@ -884,7 +886,7 @@ let cty_apply c pvl args res =
List.fold_right freeze_pv pvl c.cty_freeze in
let same = same && ity_equal c.cty_result res &&
List.for_all2 (fun a t -> ity_equal a.pv_ity t) al args in
if same && pvl = [] then gh, c (*what was the point?*) else
if same && pvl = [] then gh, c else
let eff, subst_l =
if same then c.cty_effect, t_subst_l else
let isb = List.fold_left2 (fun s a ity ->
......@@ -901,9 +903,7 @@ let cty_apply c pvl args res =
Mvs.add a.pv_vs (t_var v.pv_vs) m) vsb al args in
let p = subst_l vsb c.cty_pre and q = subst_l vsb c.cty_post in
let xq = Mexn.map (fun xqfl -> subst_l vsb xqfl) c.cty_xpost in
let rds = List.fold_right Spv.remove c.cty_args c.cty_reads in
let rds = List.fold_right Spv.add args rds in
let rds = List.fold_right Spv.add pvl rds in
let rds = List.fold_right Spv.add pvl c.cty_reads in
gh, cty_unsafe args p q xq rds eff res freeze
| _ ->
invalid_arg "Ity.cty_apply" in
......@@ -913,21 +913,20 @@ let cty_add_reads c pvs =
(* the external reads are already frozen and
the arguments should stay instantiable *)
let pvs = Spv.diff pvs c.cty_reads in
let pvs = List.fold_right Spv.remove c.cty_args pvs in
{ c with cty_reads = Spv.union c.cty_reads pvs;
cty_freeze = Spv.fold freeze_pv pvs c.cty_freeze }
let cty_add_pre c pre =
check_pre pre;
let pvs = List.fold_left t_freepvs Spv.empty pre in
let c = cty_add_reads c pvs in
check_tvs c.cty_reads c.cty_result pre [] Mexn.empty;
let c = cty_add_reads c (List.fold_left t_freepvs Spv.empty pre) in
check_tvs c.cty_reads c.cty_args c.cty_result pre [] Mexn.empty;
{ c with cty_pre = pre @ c.cty_pre }
let cty_add_post c post =
check_post (Invalid_argument "Ity.cty_add_post") c.cty_result post;
let pvs = List.fold_left t_freepvs Spv.empty post in
let c = cty_add_reads c pvs in
check_tvs c.cty_reads c.cty_result [] post Mexn.empty;
let c = cty_add_reads c (List.fold_left t_freepvs Spv.empty post) in
check_tvs c.cty_reads c.cty_args c.cty_result [] post Mexn.empty;
{ c with cty_post = post @ c.cty_post }
let cty_pop_post c = match c.cty_post with
......
......@@ -310,11 +310,11 @@ val create_cty : pvsymbol list ->
pre list -> post list -> post list Mexn.t -> Spv.t -> effect -> ity -> cty
(** [create_cty args pre post xpost reads effect result] creates a cty.
The [cty_xpost] field does not have to cover all raised exceptions.
The [cty_reads] field is the union of free variables in all arguments.
The [cty_freeze] field freezes every pvsymbol in [cty_reads \ args].
The [cty_effect] field is filtered with respect to [cty_reads], and
fresh regions in [result] are reset. Every type variable in [pre],
[post], and [xpost] must come from [cty_reads] or from [result]. *)
The [cty_reads] field contains all unbound variables from the spec.
The [cty_freeze] field freezes every pvsymbol in [cty_reads].
The [cty_effect] field is filtered wrt [cty_reads] and [args].
Fresh regions in [result] are reset. Every type variable in [pre],
[post], and [xpost] must come from [cty_reads], [args] or [result]. *)
val cty_apply : cty -> pvsymbol list -> ity list -> ity -> bool * cty
(** [cty_apply cty pvl rest res] instantiates [cty] up to the types in
......@@ -323,13 +323,14 @@ val cty_apply : cty -> pvsymbol list -> ity list -> ity -> bool * cty
This is essentially [rest -> res], with every type variable and
region in [pvl] freezed. The combined length of [pvl] and [rest]
must be equal to the length of [cty.cty_args]. The instantiation
must be compatible with [cty.cty_freeze]. *)
must be compatible with [cty.cty_freeze]. Ghost formal parameters
can only be instantiated with ghost arguments. *)
val cty_add_reads : cty -> Spv.t -> cty
(** [cty_add_reads cty pvs] adds variables in [pvs] to [cty.cty_reads].
This function performs capture: if some variables in [pvs] occur
in [cty.cty_args], no renaming is made, and the corresponding type
variables and regions are not frozen. *)
This function performs capture: if some variables in [pvs] occur in
[cty.cty_args], they are removed from [pvs], and the corresponding
type variables and regions are not frozen. *)
val cty_add_pre : cty -> pre list -> cty
(** [cty_add_pre cty fl] appends pre-conditions in [fl] to [cty.cty_pre].
......
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