whyml: any expr raising a ghost exception is ghost

This makes unnecessary all checks for ghost exceptions
escaping into the non-ghost code.

bench/programs/bad-typing/ghost2.mlw

+module TestGhost
+  use import int.Int
+  use import list.List
+  use import ref.Ref
+
+  type t = { f1 : int; ghost f2 : int }
+
+  exception Found int
+
+  let test1 (x: int) (y: t)
+    ensures { result = y.f1 }
+  =
+    try raise (Found y.f2) with
+      Found _ -> y.f1
+    end
+end

src/whyml/mlw_decl.ml

@@ -393,8 +393,6 @@ let check_ghost lkn kn d =
   in
   let rec check pvs aty =
     let eff = aty.aty_spec.c_effect in
-    if not (Sexn.is_empty eff.eff_ghostx) then
-      raise (GhostRaise (e_void, Sexn.choose eff.eff_ghostx));
     let pvs = List.fold_right Spv.add aty.aty_args pvs in
     let test pv =
       if pv.pv_ghost then () else

src/whyml/mlw_expr.ml

@@ -473,7 +473,6 @@ let e_find pr e =
 
 exception StaleRegion of expr * ident
 exception GhostWrite of expr * region
-exception GhostRaise of expr * xsymbol
 
 let check_reset e varm =
   (* If we reset a region, then it may only occur in the later code
@@ -499,15 +498,16 @@ let check_postexpr e eff varm =
 
 (* smart constructors *)
 
-let mk_expr node vty ghost eff varm = {
-  e_node   = node;
-  e_vty    = vty;
-  e_ghost  = ghost;
-  e_effect = eff_ghostify ghost eff;
-  e_varm   = varm;
-  e_label  = Slab.empty;
-  e_loc    = None;
-}
+let mk_expr node vty ghost eff varm =
+  let ghost = ghost || not (Sexn.is_empty eff.eff_ghostx) in
+  let eff = eff_ghostify ghost eff in
+  { e_node   = node;
+    e_vty    = vty;
+    e_ghost  = ghost;
+    e_effect = eff;
+    e_varm   = varm;
+    e_label  = Slab.empty;
+    e_loc    = None; }
 
 (* program variables and program symbols *)
 
@@ -853,11 +853,7 @@ let e_try e0 bl =
         let eff = eff_ghostify ghost eff in
         check_postexpr e0 eff varm; (* cumulated varmap *)
         (* remove from e0.e_effect the catched exceptions *)
-        let remove eff0 (xs,_,_) =
-          (* we catch in a ghost exception in a non-ghost code *)
-          if not ghost && Sexn.mem xs eff0.eff_ghostx then
-            Loc.error ?loc:e0.e_loc (GhostRaise (e0,xs));
-          eff_remove_raise eff0 xs in
+        let remove eff0 (xs,_,_) = eff_remove_raise eff0 xs in
         let eff0 = List.fold_left remove e0.e_effect bl in
         (* total effect and varmap *)
         let eff = eff_union eff0 eff in

src/whyml/mlw_expr.mli

@@ -198,8 +198,7 @@ val ity_of_expr : expr -> ity
 val aty_of_expr : expr -> aty
 
 exception GhostWrite of expr * region
-exception GhostRaise of expr * xsymbol
-(* a ghost expression writes in a non-ghost region or raises an exception *)
+(* a ghost expression writes in a non-ghost region *)
 
 val e_app : expr -> expr list -> expr
 (** [e_app e el] builds the application of [e] to arguments [el].

src/whyml/mlw_pretty.ml

@@ -470,9 +470,6 @@ let () = Exn_printer.register
   | Mlw_expr.GhostWrite (_e, _reg) ->
       fprintf fmt
         "This expression performs a ghost write in a non-ghost location"
-  | Mlw_expr.GhostRaise (_e, xs) ->
-      fprintf fmt "This expression raises an escaping ghost exception %a"
-        print_xs xs
   | Mlw_expr.StaleRegion (_e, id) ->
       fprintf fmt "This expression prohibits further \
         usage of variable %s" id.id_string

src/whyml/mlw_ty.ml

@@ -817,6 +817,8 @@ let spec_filter ghost varm vars c =
   let check { vs_name = id } _ = if not (Mid.mem id varm) then
     Loc.errorm "Local variable %s escapes from its scope" id.id_string in
   Mvs.iter check vss;
+  if not ghost && not (Sexn.is_empty c.c_effect.eff_ghostx) then
+    Loc.errorm "Only ghost functions may raise ghost exceptions";
   { c with c_effect = eff_ghostify ghost (eff_filter vars c.c_effect) }
 
 exception UnboundException of xsymbol

src/whyml/mlw_typing.ml

@@ -1371,7 +1371,7 @@ and expr_desc lenv loc de = match de.de_desc with
         | _ -> mk_expr e1 in
       begin match e1.e_vty with
         | VTarrow _ when e1.e_ghost && not gh ->
-            errorm ~loc "%s must be a ghost function" x.id
+            Loc.errorm ~loc "%s must be a ghost function" x.id
         | VTarrow _ -> flatten e1
         | VTvalue _ -> mk_expr e1
       end;
@@ -1466,11 +1466,6 @@ and expr_desc lenv loc de = match de.de_desc with
             xs, pv, e_case (e_value pv) (List.rev bl)
       in
       e_try e1 (List.rev_map mk_branch xsl)
-  (* We push ghost down in order to safely capture even non-ghost
-     raises of the inner expression in "ghost try e1 with ..." *)
-  | DEghost ({ de_desc = DEtry (de2, bl) } as de1) ->
-      let de2 = { de1 with de_desc = DEghost de2 } in
-      expr lenv { de1 with de_desc = DEtry (de2, bl) }
   | DEmark (x, de1) ->
       let ld = create_let_defn (Denv.create_user_id x) e_now in
       let lenv = add_local x.id ld.let_sym lenv in
@@ -1543,7 +1538,7 @@ and expr_lam lenv gh pvl (de, dsp) =
   let lenv = add_binders lenv pvl in
   let e = e_ghostify gh (expr lenv de) in
   if not gh && e.e_ghost then
-    errorm ~loc:de.de_loc "ghost body in a non-ghost function";
+    Loc.errorm ~loc:de.de_loc "ghost body in a non-ghost function";
   let spec = spec_of_dspec lenv e.e_effect e.e_vty dsp in
   { l_args = pvl; l_expr = e; l_spec = spec }