whyml: accept missing exception postconditions for "abstract"

In this case, we break the encapsulation and prove the global
exception postcondition directly from the code under "abstract".

src/whyml/mlw_expr.ml

@@ -877,9 +877,10 @@ let e_any spec vty =
   aty_check (vars_merge varm vars_empty) aty;
   mk_expr (Eany spec) vty false spec.c_effect varm
 
-let e_abstract e spec =
+let e_abstract ({ e_effect = eff } as e) spec =
   if spec.c_letrec <> 0 then invalid_arg "Mlw_expr.e_abstract";
-  spec_check { spec with c_effect = e.e_effect } e.e_vty;
+  let spec = { spec with c_effect = eff } in
+  spec_check ~full_xpost:false spec e.e_vty;
   let varm = spec_varmap e.e_varm spec in
   mk_expr (Eabstr (e,spec)) e.e_vty e.e_ghost e.e_effect varm
 
@@ -896,6 +897,7 @@ let create_fun_defn id ({l_expr = e; l_spec = c} as lam) recsyms =
   let eff = if c.c_letrec <> 0 && c.c_variant = []
     then eff_diverge e.e_effect else e.e_effect in
   let spec = { c with c_effect = eff } in
+  let lam = { lam with l_spec = spec } in
   let varm = spec_varmap e.e_varm spec in
   let del_pv m pv = Mid.remove pv.pv_vs.vs_name m in
   let varm = List.fold_left del_pv varm lam.l_args in

src/whyml/mlw_ty.ml

@@ -812,7 +812,7 @@ let spec_filter ghost varm vars c =
 
 exception UnboundException of xsymbol
 
-let spec_check c ty =
+let spec_check ~full_xpost c ty =
   if c.c_pre.t_ty <> None then
     Loc.error ?loc:c.c_pre.t_loc (Term.FmlaExpected c.c_pre);
   check_post ty c.c_post;
@@ -821,10 +821,10 @@ let spec_check c ty =
     | Some ps -> ignore (ps_app ps [t;t])
     | None -> ignore (t_type t) in
   List.iter check_variant c.c_variant;
-  let sexn = Sexn.union c.c_effect.eff_raises c.c_effect.eff_ghostx in
-  let sexn = Mexn.set_diff sexn c.c_xpost in
-  if not (Sexn.is_empty sexn) then
-    raise (UnboundException (Sexn.choose sexn))
+  if full_xpost then
+    let sexn = Sexn.union c.c_effect.eff_raises c.c_effect.eff_ghostx in
+    if not (Sexn.is_empty (Mexn.set_diff sexn c.c_xpost)) then
+      raise (UnboundException (Sexn.choose sexn))
 
 (** program variables *)
 
@@ -889,7 +889,8 @@ let ty_of_vty = function
   | VTvalue ity -> ty_of_ity ity
   | VTarrow _   -> ty_unit
 
-let spec_check spec vty = spec_check spec (ty_of_vty vty)
+let spec_check ?(full_xpost=true) spec vty =
+  spec_check ~full_xpost spec (ty_of_vty vty)
 
 let vty_arrow_unsafe argl spec vty = {
   aty_args   = argl;

src/whyml/mlw_ty.mli

@@ -317,7 +317,7 @@ val aty_filter : ?ghost:bool -> varmap -> aty -> aty
 val aty_app : aty -> pvsymbol -> spec * bool * vty
 
 (* verify that the spec corresponds to the result type *)
-val spec_check : spec -> vty -> unit
+val spec_check : ?full_xpost:bool -> spec -> vty -> unit
 
 (* convert arrows to the unit type *)
 val ity_of_vty : vty -> ity

src/whyml/mlw_typing.ml

@@ -978,26 +978,22 @@ let reset_vars eff pvs =
 
 (* add dummy postconditions for uncovered exceptions *)
 let complete_xpost eff xq =
-  let xe = Sexn.union eff.eff_raises eff.eff_ghostx in
-  let check xs _ = Loc.errorm
-    "this expression does not raise exception %a" print_xs xs in
-  Mexn.iter check (Mexn.set_diff xq xe);
   let dummy { xs_ity = ity } () =
     let v = create_vsymbol (id_fresh "dummy") (ty_of_ity ity) in
     Mlw_ty.create_post v t_true in
+  let xe = Sexn.union eff.eff_raises eff.eff_ghostx in
   Mexn.set_union xq (Mexn.mapi dummy (Mexn.set_diff xe xq))
 
 let spec_invariant lenv pvs vty spec =
   let ity = ity_of_vty vty in
   let pvs = spec_pvset pvs spec in
   let rvs = reset_vars spec.c_effect pvs in
-  let xpost = complete_xpost spec.c_effect spec.c_xpost in
   let pinv,qinv = env_invariant lenv spec.c_effect pvs in
   let post_inv = post_invariant lenv rvs qinv in
   let xpost_inv xs q = post_inv xs.xs_ity q in
   { spec with c_pre   = t_and_asym_simp pinv spec.c_pre;
               c_post  = post_inv ity spec.c_post;
-              c_xpost = Mexn.mapi xpost_inv xpost }
+              c_xpost = Mexn.mapi xpost_inv spec.c_xpost }
 
 let abstr_invariant lenv e spec0 =
   let pvs = e_pvset Spv.empty e in
@@ -1010,6 +1006,12 @@ let lambda_invariant lenv pvs eff lam =
   let pvs = List.fold_right Spv.add lam.l_args pvs in
   let spec = { lam.l_spec with c_effect = eff } in
   let spec = spec_invariant lenv pvs lam.l_expr.e_vty spec in
+  (* we add dummy xposts for uncovered exceptions to silence
+     Mlw_ty.spec_check, but we do another proper check later
+     in check_user_effect, which will give us a precise
+     location of the exception-raising sub-expression *)
+  let xpost = complete_xpost eff spec.c_xpost in
+  let spec = { spec with c_xpost = xpost } in
   { lam with l_spec = spec }
 
 (* specification handling *)
@@ -1165,7 +1167,11 @@ let eff_of_deff lenv dsp =
   let add_raise xs _ eff = eff_raise eff xs in
   Mexn.fold add_raise dsp.ds_xpost eff, svs
 
-let check_user_effect lenv e eeff otv dsp =
+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 lenv e eeff full_xpost dsp =
   let has_read reg eff =
     Sreg.mem reg eff.eff_reads || Sreg.mem reg eff.eff_ghostr in
   let has_write reg eff =
@@ -1194,32 +1200,31 @@ let check_user_effect lenv e eeff otv dsp =
       "this expression does not raise exception %a" print_xs xs in
   let ueff = Mexn.fold add_raise dsp.ds_xpost ueff in
   (* check that every computed effect is listed *)
-  let read reg = if not (has_read reg ueff) then
-    let loc = (e_find (fun e ->
-      e.e_loc <> None && has_read reg e.e_effect) e).e_loc in
-    Loc.errorm ?loc "this expression produces an unlisted read effect" in
-  if ueff_ro then Sreg.iter read eeff.eff_reads;
-  if ueff_ro then Sreg.iter read eeff.eff_ghostr;
-  let write reg = if not (has_write reg ueff) then
-    let loc = (e_find (fun e ->
-      e.e_loc <> None && has_write reg e.e_effect) e).e_loc in
-    Loc.errorm ?loc "this expression produces an unlisted write effect" in
-  if ueff_rw then Sreg.iter write eeff.eff_writes;
-  if ueff_rw then Sreg.iter write eeff.eff_ghostw;
-  let raize xs = if not (has_raise xs ueff) then
-    let loc = (e_find (fun e ->
-      e.e_loc <> None && has_raise xs e.e_effect) e).e_loc in
-    Loc.errorm ?loc "this expression raises unlisted exception %a" print_xs xs
-  in
-  Sexn.iter raize eeff.eff_raises;
-  Sexn.iter raize eeff.eff_ghostx;
+  let check_read reg = if not (has_read reg ueff) then
+    Loc.errorm ?loc:(e_find_loc (fun e -> has_read reg e.e_effect) e)
+      "this expression produces an unlisted read effect" in
+  if ueff_ro then Sreg.iter check_read eeff.eff_reads;
+  if ueff_ro then Sreg.iter check_read eeff.eff_ghostr;
+  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 ueff_rw then Sreg.iter check_write eeff.eff_writes;
+  if ueff_rw then Sreg.iter check_write eeff.eff_ghostw;
+  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" 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
+
+let check_lambda_effect lenv ({fun_lambda = lam} as fd) bl dsp =
+  let lenv = add_binders lenv lam.l_args in
+  let eeff = fd.fun_ps.ps_aty.aty_spec.c_effect in
+  check_user_effect lenv lam.l_expr eeff true dsp;
   (* check that we don't look inside opaque type variables *)
-  let bad_comp tv _ _ =
-    let loc = (e_find (fun e ->
-      e.e_loc <> None && Stv.mem tv e.e_effect.eff_compar) e).e_loc in
-    Loc.errorm ?loc "type parameter %a is not opaque in this expression"
-      Pretty.print_tv tv in
-  ignore (Mtv.inter bad_comp otv eeff.eff_compar)
+  let bad_comp tv _ _ = Loc.errorm
+    ?loc:(e_find_loc (fun e -> Stv.mem tv e.e_effect.eff_compar) lam.l_expr)
+    "type parameter %a is not opaque in this expression" Pretty.print_tv tv in
+  ignore (Mtv.inter bad_comp (opaque_binders Stv.empty bl) eeff.eff_compar)
 
 let spec_of_dspec lenv eff vty dsp = {
   c_pre     = create_pre lenv dsp.ds_pre;
@@ -1407,7 +1412,7 @@ and expr_desc lenv loc de = match de.de_desc with
       let spec = spec_of_dspec lenv e1.e_effect e1.e_vty dsp in
       if spec.c_variant <> [] then Loc.errorm
         "variants are not allowed in `abstract'";
-      check_user_effect lenv e1 e1.e_effect Stv.empty dsp;
+      check_user_effect lenv e1 e1.e_effect false dsp;
       let spec = abstr_invariant lenv e1 spec in
       e_abstract e1 spec
   | DEassert (ak, f) ->
@@ -1499,11 +1504,12 @@ and expr_rec lenv dfdl =
   let eff = List.fold_left rd_effect eff_empty fdl in
   let step3 (ps, lam) = ps, lambda_invariant lenv pvs eff lam in
   let fdl = create_rec_defn (List.map step3 fdl) in
-  let step4 fd (_,_,_,bl,tr) = check_effects lenv fd bl tr in
+  let step4 fd (_,_,_,bl,(de,dsp)) =
+    Loc.try4 de.de_loc check_lambda_effect lenv fd bl dsp in
   List.iter2 step4 fdl dfdl;
   fdl
 
-and expr_fun lenv x gh bl (_, dsp as tr) =
+and expr_fun lenv x gh bl (de, dsp as tr) =
   let lam = expr_lam lenv gh (binders bl) tr in
   if lam.l_spec.c_variant <> [] then Loc.errorm
     "variants are not allowed in a non-recursive definition";
@@ -1522,7 +1528,7 @@ and expr_fun lenv x gh bl (_, dsp as tr) =
   let pvs = l_pvset Spv.empty lam in
   let lam = lambda_invariant lenv pvs lam.l_expr.e_effect lam in
   let fd = create_fun_defn (Denv.create_user_id x) lam in
-  check_effects lenv fd bl tr;
+  Loc.try4 de.de_loc check_lambda_effect lenv fd bl dsp;
   fd
 
 and expr_lam lenv gh pvl (de, dsp) =
@@ -1533,13 +1539,6 @@ and expr_lam lenv gh pvl (de, dsp) =
   let spec = spec_of_dspec lenv e.e_effect e.e_vty dsp in
   { l_args = pvl; l_expr = e; l_spec = spec }
 
-and check_effects lenv fd bl (de, dsp) =
-  let lam = fd.fun_lambda in
-  let otv = opaque_binders Stv.empty bl in
-  let lenv = add_binders lenv lam.l_args in
-  let eff = fd.fun_ps.ps_aty.aty_spec.c_effect in
-  Loc.try5 de.de_loc check_user_effect lenv lam.l_expr eff otv dsp
-
 (** Type declaration *)
 
 let add_type_invariant loc uc id params inv =

src/whyml/mlw_wp.ml

@@ -716,8 +716,13 @@ and wp_desc env e q xq = match e.e_node with
       wp_expr env e1 q xq (* FIXME? should (wp_label e) rather be here? *)
   | Eabstr (e1, spec) ->
       let p = wp_label e (wp_expl expl_pre spec.c_pre) in
-      let w1 = backstep (wp_expr env e1) spec.c_post spec.c_xpost in
-      let w2 = wp_abstract env e1.e_effect spec.c_post spec.c_xpost q xq in
+      (* every exception uncovered in spec is passed to xq *)
+      let c_xq = Mexn.set_union spec.c_xpost xq in
+      let w1 = backstep (wp_expr env e1) spec.c_post c_xq in
+      (* so that now we don't need to prove these exceptions again *)
+      let lost = Mexn.set_diff (exns_of_raises e1.e_effect) spec.c_xpost in
+      let c_eff = Sexn.fold_left eff_remove_raise e1.e_effect lost in
+      let w2 = wp_abstract env c_eff spec.c_post spec.c_xpost q xq in
       wp_and ~sym:false p (wp_and ~sym:true (wp_label e w1) w2)
   | Eassign (pl, e1, reg, pv) ->
       (* if we create an intermediate variable npv to represent e1

tests/test-pgm-jcf.mlw

-module M1 
+module TestAbstr
+  use import int.Int
+  use import ref.Ref
+
+  exception E1 int
+  exception E2 int
+
+  let test (r : ref int) (z : int)
+    ensures { !r = 3 /\ result > 0 }
+    raises  { E1 x -> !r = 1 /\ x < 0 }
+    raises  { E2 x -> !r = 3 /\ x = 0 }
+  =
+    r := 1;
+    abstract begin
+      if z < 0 then raise (E1 z);
+      r := !r + 2;
+      if z = 0 then raise (E2 z)
+    end
+    ensures { !r = 3 }
+    raises { E1 x -> x = 5 };
+    if z = 42 then 41 else z
+
+end
+
+module M1
   predicate eq (x y : 'a)
 end
 
@@ -13,7 +37,7 @@ module M2
   with my_eq7 (x : 'a) (y : 'a) = my_eq8 x y
   with my_eq8 (x : 'a) (y : 'a) = my_eq9 x y
   with my_eq9 (x : 'a) (y : 'a) = x = y
-  
+
   clone M1 with predicate eq = my_eq
 end
 
@@ -30,7 +54,6 @@ module TestGhost
     assert { x > 0 };
     let r1 = ref x in
     peq r1 r1
-
 end