Commit cda6d915 authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw: labels can act as local exceptions

Useful to break out of the loops:

  label Break in
  while ... do
    label Continue in
    ... raise Break ...
    ... raise Continue ...
  done

When a label is put over a non-unit expression,
raise acts as return:

  label Return in
  if ... then raise Return 42; 0

Also, "return <expr>" returns from the innermost function.
This includes abstract blocks, too, so if you want to return
across an abstract block, you should rather use a label at
the top of the main function. TODO/FIXME: maybe we should
let "return" pass across abstract blocks by default, to
avoid surprises?

One shortcoming of the labels-as-exceptions is that they cannot
be used to transmit tuples with ghost elements, nor return ghost
values from non-ghost expressions. A local exception with an
explicit mask should be used instead. Similarly, to return
a partially ghost value from a function, it must have have
its mask explicitly written (which is a good practice anyway).
We cannot know the mask of an expr before we construct it,
but in order to construct it, we need to create the local
exceptions first.

Another caveat is that while it is possible to catch an exception
generated by a label, you should avoid to do so. We only declare
the local exception if the expression under the label _raises_
the exception, and thus the following code will not typecheck:

  label X in (try raise X with X -> () end)

Indeed, the expression in the parentheses does not raise X,
and so we do not declare a local exception X for this label,
and so the program contains an undeclared exception symbol.
parent b3a73a61
......@@ -393,6 +393,9 @@ type dspec = ity -> dspec_final
must have this type. All vsymbols in the exceptional postcondition
clauses must have the type of the corresponding exception. *)
let old_mark = "'Old"
let old_mark_id = id_fresh old_mark
(** Expressions *)
type dinvariant = term list
......@@ -413,8 +416,8 @@ and dexpr_node =
| DEls of lsymbol
| DEconst of Number.constant * dity
| DEapp of dexpr * dexpr
| DEfun of dbinder list * mask * dspec later * dexpr
| DEany of dbinder list * mask * dspec later * dity
| DEfun of dbinder list * dity * mask * dspec later * dexpr
| DEany of dbinder list * dity * mask * dspec later
| DElet of dlet_defn * dexpr
| DErec of drec_defn * dexpr
| DEnot of dexpr
......@@ -434,8 +437,8 @@ and dexpr_node =
| DEabsurd
| DEtrue
| DEfalse
| DEmark of preid * dexpr
| DEcast of dexpr * ity
| DEcast of dexpr * dity
| DEmark of preid * dity * dexpr
| DEuloc of dexpr * Loc.position
| DElabel of dexpr * Slab.t
......@@ -443,8 +446,8 @@ and dlet_defn = preid * ghost * rs_kind * dexpr
and drec_defn = { fds : dfun_defn list }
and dfun_defn = preid * ghost * rs_kind *
dbinder list * mask * dspec later * variant list later * dexpr
and dfun_defn = preid * ghost * rs_kind * dbinder list *
dity * mask * dspec later * variant list later * dexpr
(** Environment *)
......@@ -617,9 +620,9 @@ let drec_defn denv0 prel =
let parse (id,gh,pk,bl,res,msk,pre) =
let dsp, dvl, de = pre (denv_add_args denv1 bl) in
dexpr_expected_type de res;
(id,gh,pk,bl,msk,dsp,dvl,de) in
(id,gh,pk,bl,res,msk,dsp,dvl,de) in
let fdl = List.map parse prel in
let add denv (id,_,_,bl,_,_,_,{de_dvty = dvty}) =
let add denv (id,_,_,bl,res,_,_,_,_) =
(* just in case we linked some polymorphic type var to the outer context *)
let check tv = if is_frozen denv0.frozen tv then Loc.errorm ?loc:id.pre_loc
"This function is expected to be polymorphic in type variable %a"
......@@ -629,7 +632,7 @@ let drec_defn denv0 prel =
| Some (None, _) | None -> assert false
end;
let argl = List.map (fun (_,_,t) -> t) bl in
denv_add_poly denv id (argl, dity_of_dvty dvty) in
denv_add_poly denv id (argl, res) in
List.fold_left add denv0 fdl, { fds = fdl }
(** Constructors *)
......@@ -713,9 +716,10 @@ let dexpr ?loc node =
end;
dexpr_expected_type de2 a;
[], r
| DEfun (bl,_,_,de) ->
List.map (fun (_,_,t) -> t) bl, dity_of_dvty de.de_dvty
| DEany (bl,_,_,res) ->
| DEfun (bl,res,_,_,de) ->
dexpr_expected_type de res;
List.map (fun (_,_,t) -> t) bl, res
| DEany (bl,res,_,_) ->
List.map (fun (_,_,t) -> t) bl, res
| DElet (_,de)
| DErec (_,de) ->
......@@ -785,10 +789,10 @@ let dexpr ?loc node =
| DEtrue
| DEfalse ->
dvty_bool
| DEcast (de,ity) ->
dexpr_expected_type de (dity_of_ity ity);
| DEcast (de,dity)
| DEmark (_,dity,de) ->
dexpr_expected_type de dity;
de.de_dvty
| DEmark (_,de)
| DEuloc (de,_)
| DElabel (de,_) ->
de.de_dvty in
......@@ -1017,7 +1021,7 @@ let rebase_old {pvm = pvm} preold old fvs =
if not (Mvs.mem o fvs) then sbs else match preold with
| Some preold ->
Mvs.add o (t_var (find_old pvm preold v).pv_vs) sbs
| None -> raise (UnboundLabel "0") in
| None -> raise (UnboundLabel old_mark) in
Hpv.fold rebase old Mvs.empty
let rebase_pre env preold old pl =
......@@ -1052,14 +1056,17 @@ let add_pv_map ({pvm = pvm} as env) vm =
let add_binders env pvl = List.fold_left add_pvsymbol env pvl
let add_xsymbol ({xsm = xsm} as env) xs =
{ env with xsm = Mstr.add xs.xs_name.id_string xs xsm }
(** Abstract values *)
let cty_of_spec env bl mask dsp dity =
let ity = ity_of_dity dity in
let bl = binders env.ghs bl in
let env = add_binders env bl in
let preold = Mstr.find_opt "0" env.old in
let env, old = add_label env "0" in
let preold = Mstr.find_opt old_mark env.old in
let env, old = add_label env old_mark in
let dsp = get_later env dsp ity in
let _, eff = effect_of_dspec dsp in
let eff = eff_ghostify env.ghs eff in
......@@ -1187,13 +1194,13 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl =
(* if we were not in the ghost context until now, then
we must ghostify the let-definitions down from here *)
cexp uloc {env with ghs = true; cgh = env.cgh || not env.ghs} de lpl
| DEfun (bl,msk,dsp,de) ->
| DEfun (bl,_,msk,dsp,de) ->
let dvl _ _ _ = [] in
let env = {env with ghs = env.ghs || env.lgh} in
let c, dsp, _ = lambda uloc env (binders env.ghs bl) msk dsp dvl de in
check_fun env.inr None dsp c;
proxy c
| DEany (bl,msk,dsp,dity) ->
| DEany (bl,dity,msk,dsp) ->
let env = {env with ghs = env.ghs || env.lgh} in
proxy (c_any (cty_of_spec env bl msk dsp dity))
| DElet ((_,_,_,{de_dvty = ([],_)}) as dldf,de) ->
......@@ -1361,12 +1368,19 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
e_false
| DEexn (id,dity,mask,de) ->
let xs = create_xsymbol id ~mask (ity_of_dity dity) in
let env = { env with xsm = Mstr.add id.pre_name xs env.xsm } in
e_exn xs (expr uloc env de)
| DEmark ({pre_name = l},de) ->
let env, old = add_label env l in
e_exn xs (expr uloc (add_xsymbol env xs) de)
| DEmark (id,dity,de) ->
let xs = create_xsymbol id (ity_of_dity dity) in
let env, old = add_label env id.pre_name in
let e = expr uloc (add_xsymbol env xs) de in
let e = if Sxs.mem xs e.e_effect.eff_raises then
let v = create_pvsymbol (id_fresh "result") xs.xs_ity in
(* FIXME? We assume that the generated exception will not
be catched inside e. Otherwise, it will not appear in
the effect and we will not declare the exception here. *)
e_exn xs (e_try e (Mxs.singleton xs ([v], e_var v))) else e in
let put _ (ld,_) e = e_let ld e in
Hpv.fold put old (expr uloc env de)
Hpv.fold put old e
| DEcast _ | DEuloc _ | DElabel _ ->
assert false (* already stripped *)
......@@ -1386,10 +1400,10 @@ and sym_defn uloc env (id,gh,kind,de) =
ld::ldl, add_rsymbol env s
and rec_defn uloc ({inr = inr} as env) {fds = dfdl} =
let step1 env (id, gh, kind, bl, mask, dsp, dvl, ({de_dvty = dvty} as de)) =
let step1 env (id, gh, kind, bl, res, mask, dsp, dvl, de) =
let ghost = env.ghs || gh || kind = RKlemma in
let pvl = binders ghost bl in
let ity = Loc.try1 ?loc:de.de_loc ity_of_dity (dity_of_dvty dvty) in
let ity = Loc.try1 ?loc:de.de_loc ity_of_dity res in
let cty = create_cty ~mask pvl [] [] Mxs.empty Mpv.empty eff_empty ity in
let rs = create_rsymbol id ~ghost ~kind:RKnone cty in
add_rsymbol env rs, (rs, kind, mask, dsp, dvl, de) in
......@@ -1421,9 +1435,23 @@ and rec_defn uloc ({inr = inr} as env) {fds = dfdl} =
and lambda uloc env pvl mask dsp dvl de =
let env = add_binders env pvl in
let preold = Mstr.find_opt "0" env.old in
let env, old = add_label env "0" in
let e = expr uloc env de in
let preold = Mstr.find_opt old_mark env.old in
let env, old = add_label env old_mark in
let ity = ity_of_dity (dity_of_dvty de.de_dvty) in
let xs = create_xsymbol old_mark_id ~mask ity in
let e = expr uloc (add_xsymbol env xs) de in
let e = if Sxs.mem xs e.e_effect.eff_raises then
let mk_res n m ity =
create_pvsymbol (id_fresh n) ~ghost:(mask_ghost m) ity in
let vl = match mask, xs.xs_ity.ity_node with
| MaskTuple ml, Ityapp (_, tyl, _) ->
List.map2 (mk_res "r") ml tyl
| _ -> [mk_res "result" mask ity] in
let el = match vl with
| [v] -> e_var v | _ -> e_tuple (List.map e_var vl) in
(* exception 'Old cannot be catched in the surface language,
so we only declare the exception when 'Old is raised *)
e_exn xs (e_try e (Mxs.singleton xs (vl, el))) else e in
let dsp = get_later env dsp e.e_ity in
let dvl = get_later env dvl in
let dvl = rebase_variant env preold old dvl in
......@@ -1437,7 +1465,7 @@ let rec_defn ?(keep_loc=true) drdf =
fst (rec_defn uloc env_empty drdf)
let rec mask_of_fun de = match de.de_node with
| DEfun (_,msk,_,_) -> msk
| DEfun (_,_,msk,_,_) -> msk
| DEghost de | DEcast (de,_)
| DEuloc (de,_) | DElabel (de,_) -> mask_of_fun de
| _ -> MaskGhost (* a safe default for checking *)
......
......@@ -58,6 +58,9 @@ type dbinder = preid option * ghost * dity
exception UnboundLabel of string
val old_mark : string
val old_mark_id : preid
type register_old = pvsymbol -> string -> pvsymbol
(** Program variables occurring under [old] or [at] are passed to
a registrar function. The label string must be ["0"] for [old]. *)
......@@ -103,8 +106,8 @@ and dexpr_node =
| DEls of lsymbol
| DEconst of Number.constant * dity
| DEapp of dexpr * dexpr
| DEfun of dbinder list * mask * dspec later * dexpr
| DEany of dbinder list * mask * dspec later * dity
| DEfun of dbinder list * dity * mask * dspec later * dexpr
| DEany of dbinder list * dity * mask * dspec later
| DElet of dlet_defn * dexpr
| DErec of drec_defn * dexpr
| DEnot of dexpr
......@@ -124,8 +127,8 @@ and dexpr_node =
| DEabsurd
| DEtrue
| DEfalse
| DEmark of preid * dexpr
| DEcast of dexpr * ity
| DEcast of dexpr * dity
| DEmark of preid * dity * dexpr
| DEuloc of dexpr * Loc.position
| DElabel of dexpr * Slab.t
......@@ -133,8 +136,8 @@ and dlet_defn = preid * ghost * rs_kind * dexpr
and drec_defn = private { fds : dfun_defn list }
and dfun_defn = preid * ghost * rs_kind *
dbinder list * mask * dspec later * variant list later * dexpr
and dfun_defn = preid * ghost * rs_kind * dbinder list *
dity * mask * dspec later * variant list later * dexpr
(** Environment *)
......
......@@ -984,7 +984,7 @@ let cty_add_variant d varl = let add s (t,_) = t_freepvs s t in
let rec e_rs_subst sm e = e_label_copy e (match e.e_node with
| Evar _ | Econst _ | Eassign _ | Eassert _ | Epure _ | Eabsurd -> e
| Eexn (xs,e) -> e_exn xs e
| Eexn (xs,e) -> e_exn xs (e_rs_subst sm e)
| Eghost e -> e_ghostify true (e_rs_subst sm e)
| Eexec (c,_) -> e_exec (c_rs_subst sm c)
| Elet (LDvar (v,d),e) ->
......
......@@ -89,6 +89,7 @@
"reads", READS;
"rec", REC;
"requires", REQUIRES;
"return", RETURN;
"returns", RETURNS;
"to", TO;
"try", TRY;
......
......@@ -135,8 +135,8 @@
%token ABSTRACT ABSURD ANY ASSERT ASSUME AT BEGIN CHECK
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
%token PRIVATE PURE RAISE RAISES READS REC REQUIRES RETURNS
%token TO TRY VAL VARIANT WHILE WRITES
%token PRIVATE PURE RAISE RAISES READS REC REQUIRES
%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES
(* symbols *)
......@@ -509,7 +509,7 @@ term_:
| NOT term
{ Tnot $2 }
| OLD term
{ Tat ($2, mk_id "0" $startpos($1) $endpos($1)) }
{ Tat ($2, mk_id Dexpr.old_mark $startpos($1) $endpos($1)) }
| term AT uident
{ Tat ($1, $3) }
| prefix_op term %prec prec_prefix_op
......@@ -775,6 +775,8 @@ expr_:
{ Eraise ($2, $3) }
| RAISE LEFTPAR uqualid expr_arg? RIGHTPAR
{ Eraise ($3, $4) }
| RETURN expr_arg?
{ Eraise (Qident (mk_id Dexpr.old_mark $startpos($1) $endpos($1)), $2) }
| TRY seq_expr WITH bar_list1(exn_handler) END
{ Etry ($2, $4) }
| GHOST expr
......
......@@ -665,14 +665,16 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
DErec (rd, dexpr muc denv e1)
| Ptree.Efun (bl, pty, msk, sp, e) ->
let bl = List.map (dbinder muc) bl in
let e = match pty with
| Some pty -> { e with expr_desc = Ecast (e, pty) }
| None -> e in
let ds = match sp.sp_variant with
| ({term_loc = loc},_)::_ ->
Loc.errorm ~loc "unexpected 'variant' clause"
| _ -> dspec muc sp in
DEfun (bl, msk, ds, dexpr muc (denv_add_args denv bl) e)
let denv = denv_add_args denv bl in
let dity = match pty with
| Some pty -> dity_of_ity (ity_of_pty muc pty)
| None -> dity_fresh () in
let denv = denv_add_exn denv old_mark_id dity in
DEfun (bl, dity, msk, ds, dexpr muc denv e)
| Ptree.Eany (pl, kind, pty, msk, sp) ->
let pl = List.map (dparam muc) pl in
let ds = match sp.sp_variant with
......@@ -684,7 +686,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| RKlemma, None -> ity_unit
| RKpred, None -> ity_bool
| _ -> Loc.errorm ~loc "cannot determine the type of the result" in
DEany (pl, msk, ds, dity_of_ity ity)
DEany (pl, dity_of_ity ity, msk, ds)
| Ptree.Ematch (e1, bl) ->
let e1 = dexpr muc denv e1 in
let branch (pp, e) =
......@@ -772,7 +774,10 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| Ptree.Eassert (ak, f) ->
DEassert (ak, dassert muc f)
| Ptree.Emark (id, e1) ->
DEmark (create_user_id id, dexpr muc denv e1)
let dity = dity_fresh () in
let id = create_user_id id in
let denv = denv_add_exn denv id dity in
DEmark (id, dity, dexpr muc denv e1)
| Ptree.Enamed (Lpos uloc, e1) ->
DEuloc (dexpr muc denv e1, uloc)
| Ptree.Enamed (Lstr lab, e1) ->
......@@ -783,7 +788,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| Ptree.Ecast (e1, pty) ->
let d1 = dexpr muc denv e1 in
let ity = ity_of_pty muc pty in
DEcast (d1, ity)
DEcast (d1, dity_of_ity ity)
end
and drec_defn muc denv fdl =
......@@ -793,6 +798,7 @@ and drec_defn muc denv fdl =
| Some pty -> dity_of_ity (ity_of_pty muc pty)
| None -> dity_fresh () in
let pre denv =
let denv = denv_add_exn denv old_mark_id dity in
let dv = dvariant muc sp.sp_variant in
dspec muc sp, dv, dexpr muc denv e in
create_user_id id, gh, kind, bl, dity, msk, pre 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