Commit 83858597 authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: add "diverges", "reads {}", and "writes {}" effect clauses

- "diverges" states that the computation may not terminate (which
  does not mean that is always diverges: just as any other effect
  annotation, this clause states a possibility of a side effect).

- "reads {}" states that the computation does not access any variable
  except those that are listed elsewhere in the specification (or the
  proper function arguments, if "reads" is in a function spec).

- "writes {}" states that the computation does not modify any mutable
  value.

- If a function definition or an abstract computation may diverge,
  but there is no "diverges" clause in the specification, a warning
  is produced. If a function definition or an abstract computation
  always terminates, but there is a "diverges" clause in the spec,
  an error is produced.

- If there is a "reads" or a "writes" clause in a function definition
  or an abstract computation, then every modified value must be listed
  in "writes" and every accessed external variable not mentioned in
  the spec must be listed in "reads". (Notice that this is a stricter
  requirement than before, when the presence of a "writes" clause
  did not require to specify "reads".) However, one does not have to
  write "reads {}" or "writes {}" if the corresponding lists are empty.
parent 67316b73
......@@ -35,6 +35,7 @@ let test_not_1 ()
let test_not_2 ()
requires { !x <= 0 }
ensures { !x = 0 }
diverges
= while not (!x = 0) do invariant { !x <= 0 } incr x done
let test_all_1 ()
......
......@@ -121,6 +121,8 @@ let d : pdecl =
sp_reads = [];
sp_writes = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
}
in
let body =
......
......@@ -28,7 +28,7 @@
;; Note: comment font-lock is guaranteed by suitable syntax entries
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
; '("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
`(,(why3-regexp-opt '("invariant" "variant" "requires" "ensures" "returns" "raises" "reads" "writes" "assert" "assume" "check")) . font-lock-type-face)
`(,(why3-regexp-opt '("invariant" "variant" "diverges" "requires" "ensures" "returns" "raises" "reads" "writes" "assert" "assume" "check")) . font-lock-type-face)
`(,(why3-regexp-opt '("use" "clone" "namespace" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face)
)
"Minimal highlighting for Why3 mode")
......
......@@ -205,6 +205,7 @@ on linking described in file LICENSE.
<keyword>absurd</keyword>
<keyword>assert</keyword>
<keyword>assume</keyword>
<keyword>diverges</keyword>
<keyword>ensures</keyword>
<keyword>check</keyword>
<keyword>invariant</keyword>
......
......@@ -6,7 +6,7 @@
{
basicstyle=\ttfamily,
morekeywords=[1]{predicate,function,goal,type,use,import,theory,end,in,%
mutable,invariant,model,requires,ensures,raises,returns,reads,writes,%
mutable,invariant,model,requires,ensures,raises,returns,reads,writes,diverges,%
variant,let,val,while,for,loop,abstract,private,any,assert,assume,check,%
rec,clone,if,then,else,result,old,ghost,%
axiom,lemma,export,forall,exists,match,with,not,inductive,coinductive},%
......
......@@ -100,7 +100,7 @@ syn keyword whyBoolean true false
syn keyword whyType bool int list map option real
syn keyword whyType array ref unit
syn keyword whySpec absurd assert assume check ensures invariant
syn keyword whySpec absurd assert assume check diverges ensures invariant
syn keyword whySpec raises reads requires returns variant writes
syn match whyConstructor "(\s*)"
......
......@@ -71,6 +71,7 @@
"assume", ASSUME;
"begin", BEGIN;
"check", CHECK;
"diverges", DIVERGES;
"do", DO;
"done", DONE;
"downto", DOWNTO;
......
......@@ -120,6 +120,8 @@ end
sp_reads = [];
sp_writes = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
}
let spec_union s1 s2 = {
......@@ -129,6 +131,8 @@ end
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;
sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
sp_diverge = s1.sp_diverge || s2.sp_diverge;
}
(* dead code
......@@ -171,7 +175,7 @@ end
/* program keywords */
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DIVERGES DO DONE DOWNTO
%token ENSURES EXCEPTION FOR
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE PRIVATE RAISE
%token RAISES READS REC REQUIRES RETURNS TO TRY VAL VARIANT WHILE WRITES
......@@ -1383,11 +1387,13 @@ single_spec:
| RAISES LEFTBRC BAR raises RIGHTBRC
{ { empty_spec with sp_xpost = [floc_i 4, $4] } }
| READS LEFTBRC reads RIGHTBRC
{ { empty_spec with sp_reads = $3 } }
{ { empty_spec with sp_reads = $3; sp_checkrw = true } }
| WRITES LEFTBRC writes RIGHTBRC
{ { empty_spec with sp_writes = $3 } }
{ { empty_spec with sp_writes = $3; sp_checkrw = true } }
| RAISES LEFTBRC xsymbols RIGHTBRC
{ { empty_spec with sp_xpost = [floc_i 3, $3] } }
| DIVERGES
{ { empty_spec with sp_diverge = true } }
| variant
{ { empty_spec with sp_variant = $1 } }
;
......@@ -1414,13 +1420,23 @@ raises_case:
;
reads:
| lqualid { [$1] }
| lqualid COMMA reads { $1::$3 }
| /* epsilon */ { [] }
| list_reads1 { $1 }
;
list_reads1:
| lqualid { [$1] }
| lqualid COMMA list_reads1 { $1::$3 }
;
writes:
| lexpr { [$1] }
| lexpr COMMA writes { $1::$3 }
| /* epsilon */ { [] }
| list_writes1 { $1 }
;
list_writes1:
| lexpr { [$1] }
| lexpr COMMA list_writes1 { $1::$3 }
;
xsymbols:
......
......@@ -197,6 +197,8 @@ type spec = {
sp_reads : qualid list;
sp_writes : lexpr list;
sp_variant : variant list;
sp_checkrw : bool;
sp_diverge : bool;
}
type type_v =
......
......@@ -362,6 +362,8 @@ type dspec_final = {
ds_reads : vsymbol list;
ds_writes : term list;
ds_variant : variant list;
ds_checkrw : bool;
ds_diverge : bool;
}
type dspec = ty -> dspec_final
......@@ -857,6 +859,7 @@ let rec effect_of_term t = match t.t_node with
let effect_of_dspec dsp =
let add_raise xs _ eff = eff_raise eff xs in
let eff = Mexn.fold add_raise dsp.ds_xpost eff_empty in
let eff = if dsp.ds_diverge then eff_diverge eff else eff in
let svs = List.fold_right Svs.add dsp.ds_reads Svs.empty in
let add_write (svs,mreg,eff) t =
let vs, fd = effect_of_term t in
......@@ -879,7 +882,7 @@ let e_find_loc pr e =
try (e_find (fun e -> e.e_loc <> None && pr e) e).e_loc
with Not_found -> None
let check_user_effect e spec full_xpost dsp =
let check_user_effect e spec args full_xpost dsp =
let has_write reg eff =
Sreg.mem reg eff.eff_writes || Sreg.mem reg eff.eff_ghostw in
let has_raise xs eff =
......@@ -905,29 +908,38 @@ let check_user_effect e spec full_xpost dsp =
Mlw_pretty.print_xs xs in
Mexn.iter check_raise ueff.eff_raises;
Mexn.iter check_raise ueff.eff_ghostx;
if ueff.eff_diverg && not eeff.eff_diverg then
Loc.errorm ?loc:e.e_loc "this expression does not diverge";
(* check that every computed effect is listed *)
let check_read pv = if not (Svs.mem pv.pv_vs usvs) then
Loc.errorm ?loc:(e_find_loc (fun e -> Spv.mem pv e.e_syms.syms_pv) e)
"this expression depends on variable %a left out in specification"
Mlw_pretty.print_pv pv in
if dsp.ds_reads <> [] then Spv.iter check_read
(Spv.remove Mlw_wp.pv_old
(Spv.diff e.e_syms.syms_pv (spec_pvset Spv.empty spec)));
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
if dsp.ds_writes <> [] then Sreg.iter check_write eeff.eff_writes;
if dsp.ds_writes <> [] then Sreg.iter check_write eeff.eff_ghostw;
if dsp.ds_checkrw then begin
let reads = Spv.remove Mlw_wp.pv_old e.e_syms.syms_pv in
let reads = Spv.diff reads (spec_pvset Spv.empty spec) in
let reads = List.fold_right Spv.remove args reads in
Spv.iter check_read reads;
Sreg.iter check_write eeff.eff_writes;
Sreg.iter check_write eeff.eff_ghostw;
end;
let check_raise xs = if not (has_raise xs ueff) then
Loc.errorm ?loc:(e_find_loc (fun e -> has_raise xs e.e_effect) e)
"this expression raises unlisted exception %a"
Mlw_pretty.print_xs xs in
if full_xpost then Sexn.iter check_raise eeff.eff_raises;
if full_xpost then Sexn.iter check_raise eeff.eff_ghostx
if full_xpost then Sexn.iter check_raise eeff.eff_ghostx;
if eeff.eff_diverg && not ueff.eff_diverg then
Warning.emit ?loc:(e_find_loc (fun e -> e.e_effect.eff_diverg) e)
"this expression may diverge, which is not stated in specification"
let check_lambda_effect ({fun_lambda = lam} as fd) bl dsp =
let spec = fd.fun_ps.ps_aty.aty_spec in
check_user_effect lam.l_expr spec true dsp;
let args = fd.fun_ps.ps_aty.aty_args in
check_user_effect lam.l_expr spec args true dsp;
let optv = opaque_binders Stv.empty bl in
let bad_comp tv _ _ = Loc.errorm
?loc:(e_find_loc (fun e -> Stv.mem tv e.e_effect.eff_compar) lam.l_expr)
......@@ -1300,7 +1312,7 @@ and try_expr keep_loc uloc env ({de_dvty = argl,res} as de0) =
if dsp.ds_variant <> [] then Loc.errorm
"variants are not allowed in `abstract'";
let spec = spec_of_dspec e.e_effect tyv dsp in
check_user_effect e spec false dsp;
check_user_effect e spec [] false dsp;
let speci = spec_invariant env e.e_syms.syms_pv e.e_vty spec in
(* we do not require invariants on free variables *)
e_abstract e { speci with c_pre = spec.c_pre }
......
......@@ -70,6 +70,8 @@ type dspec_final = {
ds_reads : vsymbol list;
ds_writes : term list;
ds_variant : variant list;
ds_checkrw : bool;
ds_diverge : bool;
}
type dspec = ty -> dspec_final
......
......@@ -297,6 +297,8 @@ let dspec lenv sp lvm ty = {
ds_reads = dreads lenv sp.sp_reads lvm;
ds_writes = dwrites lenv sp.sp_writes lvm;
ds_variant = dvariant lenv sp.sp_variant lvm;
ds_checkrw = sp.sp_checkrw;
ds_diverge = sp.sp_diverge;
}
let dassert lenv f lvm =
......@@ -563,7 +565,8 @@ let rec dexpr ({uc = uc} as lenv) denv {expr_desc = desc; expr_loc = loc} =
| Ptree.Eany (tyv, sp) ->
let dsp = if
sp.sp_pre = [] && sp.sp_post = [] && sp.sp_xpost = [] &&
sp.sp_reads = [] && sp.sp_writes = [] && sp.sp_variant = []
sp.sp_reads = [] && sp.sp_writes = [] && sp.sp_variant = [] &&
not sp.sp_checkrw && not sp.sp_diverge
then None
else Some (dspec lenv sp) in
DEany (dtype_v lenv tyv, dsp)
......
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