From b4380d74d19f2b9a5ced98c4f7d67911f9284464 Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@lri.fr>
Date: Thu, 21 Jun 2018 13:07:19 +0200
Subject: [PATCH] WhyML: defensive "any"

---
 examples/vstte12_bfs.mlw |  5 ++++-
 src/parser/parser.mly    | 36 +++++++++++++++++++++++++++++++++++-
 stdlib/set.mlw           |  3 +--
 3 files changed, 40 insertions(+), 4 deletions(-)

diff --git a/examples/vstte12_bfs.mlw b/examples/vstte12_bfs.mlw
index aa83d6f95..a977cefc0 100644
--- a/examples/vstte12_bfs.mlw
+++ b/examples/vstte12_bfs.mlw
@@ -83,6 +83,9 @@ module BFS
 
   function (!!) (s: B.t) : set vertex = B.contents s
 
+  val pick_succ (v: vertex) : B.t
+    ensures { !!result = succ v }
+
   (* function fill_next fills set next with the unvisited successors of v *)
   let fill_next (s t v: vertex) (visited current next: B.t) (d:ref int)
     requires { inv s t !!visited !!current !!next !d /\
@@ -91,7 +94,7 @@ module BFS
     ensures { inv s t !!visited !!current !!next !d /\
       subset (succ v) !!visited  /\
       (forall x: vertex. closure !!visited !!current !!next x) }
-  = let acc = any B.t ensures { !!result = succ v } in
+  = let acc = pick_succ v in
     while not (B.is_empty acc) do
       invariant {
         inv s t !!visited !!current !!next !d /\
diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index ad07d4419..b844c1552 100644
--- a/src/parser/parser.mly
+++ b/src/parser/parser.mly
@@ -106,6 +106,28 @@
     | Pwild -> sp
     | _ -> { sp with sp_post = List.map apply sp.sp_post }
 
+  let we_attr = Ident.create_attribute "expl:witness existence"
+
+  let pre_of_any any_loc ty ql =
+    if ql = [] then [] else
+    let ri loc = { id_str = "result"; id_loc = loc; id_ats = [] } in
+    let rt loc = { term_desc = Tident (Qident (ri loc)); term_loc = loc } in
+    let rec case (loc, pfl) = match pfl with
+      | [{ pat_desc = Ptree.Pparen p; pat_loc = loc}, f] -> case (loc, [p,f])
+      | [{ pat_desc = Ptree.Pwild | Ptree.Ptuple [] }, f] -> f
+      | [{ pat_desc = Ptree.Pvar { id_str = "result" } }, f] -> f
+      | [{ pat_desc = Ptree.Pvar id }, f] ->
+              { term_desc = Tlet (id, rt loc, f); term_loc = loc }
+      | _ ->  { term_desc = Tcase (rt loc, pfl); term_loc = loc } in
+    let mk_t desc = { term_desc = desc; term_loc = any_loc } in
+    let rec join ql = match ql with
+      | [] -> assert false (* never *)
+      | [q] -> case q
+      | q::ql -> mk_t (Tbinop (case q, Dterm.DTand_asym, join ql)) in
+    let bl = [any_loc, Some (ri any_loc), false, Some ty] in
+    let p = mk_t (Tquant (Dterm.DTexists, bl, [], join ql)) in
+    [mk_t (Tattr (ATstr we_attr, p))]
+
   let error_param loc =
     Loc.errorm ~loc "cannot determine the type of the parameter"
 
@@ -850,7 +872,19 @@ single_expr_:
       Efun ($2, None, Ity.MaskVisible, spec_union $3 $5, e) }
 | ANY return_named spec
     { let pat, ty, mask = $2 in
-      Eany ([], Expr.RKnone, Some ty, mask, apply_return pat $3) }
+      let loc = floc $startpos $endpos in
+      let spec = apply_return pat $3 in
+      if spec.sp_writes <> [] then Loc.errorm ~loc
+        "this expression should not produce side effects";
+      if spec.sp_xpost <> [] then Loc.errorm ~loc
+        "this expression should not raise exceptions";
+      if spec.sp_alias <> [] then Loc.errorm ~loc
+        "this expression cannot have alias restrictions";
+      if spec.sp_diverge then Loc.errorm ~loc
+        "this expression must terminate";
+      let pre = pre_of_any loc ty spec.sp_post in
+      let spec = { spec with sp_pre = spec.sp_pre @ pre } in
+      Eany ([], Expr.RKnone, Some ty, mask, spec) }
 | VAL ghost kind attrs(lident_rich) mk_expr(val_defn) IN seq_expr
     { Elet ($4, $2, $3, $5, $7) }
 | MATCH seq_expr WITH ext_match_cases END
diff --git a/stdlib/set.mlw b/stdlib/set.mlw
index 18e3ae58b..4691963a5 100644
--- a/stdlib/set.mlw
+++ b/stdlib/set.mlw
@@ -86,9 +86,8 @@ module Set
   = fun x -> not s[x]
 
   (** arbitrary element *)
-  let ghost function choose(s: set 'a): 'a
+  val ghost function choose(s: set 'a): 'a
     ensures { not (is_empty s) -> mem result s }
-  = any 'a ensures { not (is_empty s) -> mem result s }
 
 end
 
-- 
GitLab