Commit 516cfd3a authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: white-box blocks

Just as abstract blocks, "white-box blocks" are program expressions
with an additional contract attached to their execution place.
Contrary to abstract blocks, whiteboxes do not hide their contents
from the outer computation. In most cases, you would not need
whiteboxes at all, as the same effect can be achieved by adding
assertions. Their utility comes from their syntax: the added
contract clauses bind to the expression and do not require
additional semicolons, begin-end's, let-in's or try-with's.

Compare:

    let x = <expr> in assert { P x }; x
to  <expr> ensures { P result }
or  <expr> returns { x -> P x }

    if ... then begin let x = <expr> in assert { P x }; x end; ...
to  if ... then <expr> ensures { P result }; ...

    try <expr> with E x -> assert { P x }; raise E x; end
to  <expr> raises { E x -> P x }

Internally, whiteboxes are just abstract blocks (zero-argument
anonymous functions executed in-place) with the label "vc:white_box"
on top. The user never needs to write this label explicitly though.
parent 8b67dbad
......@@ -55,10 +55,11 @@ let proxy_of_expr =
let sp_label = Ident.create_label "vc:sp"
let wp_label = Ident.create_label "vc:wp"
let wb_label = Ident.create_label "vc:white_box"
let kp_label = Ident.create_label "vc:keep_precondition"
let vc_labels = Slab.add kp_label
(Slab.add sp_label (Slab.add wp_label Slab.empty))
let vc_labels = Slab.add kp_label (Slab.add wb_label
(Slab.add sp_label (Slab.add wp_label Slab.empty)))
(* VCgen environment *)
......@@ -494,6 +495,47 @@ let rec k_expr env lps e res ?case_xmap xmap =
Klet (res, t_lab (t_var v.pv_vs), t_true)
| Econst c ->
Klet (res, t_lab (t_const c (ty_of_ity e.e_ity)), t_true)
| Eexec ({c_node = Cfun e1; c_cty = {cty_args = []} as cty}, _)
when Slab.mem wb_label e.e_label ->
(* white-box blocks do not hide their contents from the external
computation. Instead, their pre and post are simply added as
assertions at the beginning and the end of the expression.
All preconditions are thus preserved (as with kp_label).
White-box blocks do not force type invariants. *)
let k_of_post expl v ql =
let make = let t = t_var v.pv_vs in fun q ->
vc_expl None lab expl (open_post_with t q) in
let sp = t_and_asym_l (List.map make ql) in
let k = match sp.t_node with
| Tfalse -> Kstop sp | _ -> Kcut sp in
inv_of_pure env loc [sp] k in
(* normal pre- and postcondition *)
let pre = wp_of_pre None lab cty.cty_pre in
let pre = inv_of_pure env loc [pre] (Kcut pre) in
let post = k_of_post expl_post res cty.cty_post in
(* handle exceptions that pass through *)
let xs_pass = e.e_effect.eff_raises in
let xq_pass = Mxs.set_inter cty.cty_xpost xs_pass in
let xq_pass = Mxs.inter (fun _ ql (i,v) ->
let xq = k_of_post expl_xpost v ql in
Some ((i,v), Kseq (xq, 0, Kcont i))) xq_pass xmap in
(* each exception raised in e1 but not in e is hidden
due to an exceptional postcondition False in xpost *)
let bot = Kstop (vc_expl loc lab expl_absurd t_false) in
let xs_lost = Sxs.diff e1.e_effect.eff_raises xs_pass in
let xq_lost = Mxs.set_inter cty.cty_xpost xs_lost in
let xq_lost = Mxs.mapi (fun xs ql ->
let v = res_of_post xs.xs_ity ql in
let xq = k_of_post expl_xpost v ql in
(new_exn env, v), Kseq (xq, 0, bot)) xq_lost in
(* complete xmap with new indices, then handle e1 *)
let xmap = Mxs.set_union (Mxs.map fst xq_lost) xmap in
let k = Kseq (k_expr env lps e1 res xmap, 0, post) in
let add_xq _ ((i,_), xq) k = Kseq (k, i, xq) in
let k = Mxs.fold add_xq xq_lost k in
let k = Mxs.fold add_xq xq_pass k in
let k = bind_oldies cty.cty_oldies k in
if cty.cty_pre = [] then k else Kseq (pre, 0, k)
| Eexec (ce, ({cty_pre = pre; cty_oldies = oldies} as cty)) ->
(* [ VC(ce) (if ce is a lambda executed in-place)
| STOP pre
......
......@@ -11,4 +11,9 @@
open Pdecl
val sp_label : Ident.label (* switch to fast WP *)
val wp_label : Ident.label (* switch to classical WP (Cfun only) *)
val kp_label : Ident.label (* preserve preconditions after the call *)
val wb_label : Ident.label (* treat an abstract block as a whitebox *)
val vc : Env.env -> known_map -> Theory.theory_uc -> pdecl -> pdecl list
......@@ -160,6 +160,8 @@
%nonassoc LET VAL EXCEPTION
%nonassoc prec_no_else
%nonassoc DOT ELSE RETURN
%nonassoc prec_no_spec
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES DIVERGES VARIANT
%nonassoc below_LARROW
%nonassoc LARROW
%nonassoc below_COMMA
......@@ -692,11 +694,18 @@ const_defn:
mk_expr(X): d = X { mk_expr d $startpos $endpos }
seq_expr:
| assign_expr %prec below_SEMI { $1 }
| assign_expr SEMICOLON { $1 }
| assign_expr SEMICOLON seq_expr
| contract_expr %prec below_SEMI { $1 }
| contract_expr SEMICOLON { $1 }
| contract_expr SEMICOLON seq_expr
{ mk_expr (Esequence ($1, $3)) $startpos $endpos }
contract_expr:
| assign_expr %prec prec_no_spec { $1 }
| assign_expr single_spec spec
{ let d = Efun ([], None, Ity.MaskVisible, spec_union $2 $3, $1) in
let d = Enamed (Lstr Vc.wb_label, mk_expr d $startpos $endpos) in
mk_expr d $startpos $endpos }
assign_expr:
| expr %prec below_LARROW { $1 }
| expr LARROW expr
......@@ -720,12 +729,12 @@ assign_expr:
expr:
| single_expr %prec below_COMMA { $1 }
| single_expr COMMA expr_
| single_expr COMMA expr_list1
{ mk_expr (Etuple ($1::$3)) $startpos $endpos }
expr_:
expr_list1:
| single_expr %prec below_COMMA { [$1] }
| single_expr COMMA expr_ { $1::$3 }
| single_expr COMMA expr_list1 { $1::$3 }
single_expr: e = mk_expr(single_expr_) { e }
......@@ -752,9 +761,9 @@ single_expr_:
| expr_arg located(expr_arg)+ (* FIXME/TODO: "expr expr_arg" *)
{ let join f (a,_,e) = mk_expr (Eapply (f,a)) $startpos e in
(List.fold_left join $1 $2).expr_desc }
| IF seq_expr THEN assign_expr ELSE assign_expr
| IF seq_expr THEN contract_expr ELSE contract_expr
{ Eif ($2, $4, $6) }
| IF seq_expr THEN assign_expr %prec prec_no_else
| IF seq_expr THEN contract_expr %prec prec_no_else
{ Eif ($2, $4, mk_expr (Etuple []) $startpos $endpos) }
| LET ghost kind let_pattern EQUAL seq_expr IN seq_expr
{ let re_pat pat d = { pat with pat_desc = d } in
......@@ -818,7 +827,7 @@ single_expr_:
{ Eraise ($2, $3) }
| RAISE LEFTPAR uqualid expr_arg? RIGHTPAR
{ Eraise ($3, $4) }
| RETURN ioption(assign_expr)
| RETURN ioption(contract_expr)
{ Eraise (Qident (mk_id Dexpr.old_mark $startpos($1) $endpos($1)), $2) }
| TRY seq_expr WITH bar_list1(exn_handler) END
{ Etry ($2, false, $4) }
......@@ -916,8 +925,8 @@ for_direction:
(* Specification *)
spec:
| (* epsilon *) { empty_spec }
| single_spec spec { spec_union $1 $2 }
| (* epsilon *) %prec prec_no_spec { empty_spec }
| single_spec spec { spec_union $1 $2 }
single_spec:
| REQUIRES LEFTBRC term RIGHTBRC
......
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