Mlw: API for local exceptions

src/mlw/compile.ml

@@ -93,6 +93,7 @@ module ML = struct
     (* For loop for Why3's type int *)
     | Efor    of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
     | Eraise  of xsymbol * expr option
+    | Eexn    of xsymbol * ty option * expr
     | Etry    of expr * (xsymbol * pvsymbol list * expr) list
     | Eignore of expr
     | Eabsurd
@@ -234,6 +235,11 @@ module ML = struct
     | Eraise (xs, Some e) ->
       f xs.xs_name;
       iter_deps_expr f e
+    | Eexn (_xs, None, e) -> (* FIXME? How come we never do binding here? *)
+      iter_deps_expr f e
+    | Eexn (_xs, Some ty, e) -> (* FIXME? How come we never do binding here? *)
+      iter_deps_ty f ty;
+      iter_deps_expr f e
     | Etry (e, xbranchl) ->
       iter_deps_expr f e;
       List.iter (iter_deps_xbranch f) xbranchl
@@ -687,6 +693,11 @@ module Translate = struct
         | e -> Some e
       in
       ML.mk_expr (ML.Eraise (xs, ex)) (ML.I e.e_ity) eff
+    | Eexn (xs, e1) ->
+      let e1 = expr info e1 in
+      let ty = if ity_equal xs.xs_ity ity_unit
+        then None else Some (ity xs.xs_ity) in
+      ML.mk_expr (ML.Eexn (xs, ty, e1)) (ML.I e.e_ity) eff
     | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _)
     (*   assert false (\*TODO*\) *)
     | Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole
@@ -913,6 +924,9 @@ module Transform = struct
       let e2, s2 = expr info subst e2 in
       let e3, s3 = expr info subst e3 in
       mk (Eif (e1, e2, e3)), Spv.union (Spv.union s1 s2) s3
+    | Eexn (xs, ty, e1) ->
+      let e1, s1 = expr info subst e1 in
+      mk (Eexn (xs, ty, e1)), s1
     | Ematch (e, bl) ->
       let e, spv = expr info subst e in
       let e_bl, spv_bl = mk_list_eb bl (branch info subst) in
@@ -987,9 +1001,3 @@ module Transform = struct
     { m with mod_decl = mod_decl; mod_known = mod_known }
 
 end
-
-(*
- * Local Variables:
- * compile-command: "make -C ../.. -j3 bin/why3extract.opt"
- * End:
- *)

src/mlw/expr.ml

@@ -326,6 +326,7 @@ and expr_node =
   | Efor    of pvsymbol * for_bounds * invariant list * expr
   | Etry    of expr * (pvsymbol list * expr) Mxs.t
   | Eraise  of xsymbol * expr
+  | Eexn    of xsymbol * expr
   | Eassert of assertion_kind * term
   | Eghost  of expr
   | Epure   of term
@@ -385,7 +386,7 @@ let e_fold fn acc e = match e.e_node with
   | Evar _ | Econst _ | Eexec _ | Eassign _
   | Eassert _ | Epure _ | Eabsurd -> acc
   | Eraise (_,e) | Efor (_,_,_,e) | Eghost e
-  | Elet ((LDsym _|LDrec _), e) -> fn acc e
+  | Elet ((LDsym _|LDrec _), e) | Eexn (_,e) -> fn acc e
   | Elet (LDvar (_,d), e) | Ewhile (d,_,_,e) -> fn (fn acc d) e
   | Eif (c,d,e) -> fn (fn (fn acc c) d) e
   | Ecase (d,bl) -> List.fold_left (fun acc (_,e) -> fn acc e) (fn acc d) bl
@@ -564,7 +565,7 @@ let rec raw_of_expr prop e = match e.e_node with
   | Evar v -> t_var v.pv_vs
   | Econst c -> t_const c (ty_of_ity e.e_ity)
   | Epure t -> t
-  | Eghost e -> pure_of_expr prop e
+  | Eghost e | Eexn (_,e) -> pure_of_expr prop e
   | Eexec (_,{cty_post = []}) -> raise Exit
   | Eexec (_,{cty_post = q::_}) ->
       let v, h = open_post q in
@@ -626,7 +627,7 @@ let rec post_of_expr res e = match e.e_node with
   | Econst (Number.ConstReal _ as c)->
       post_of_term res (t_const c ty_real)
   | Epure t -> post_of_term res t
-  | Eghost e -> post_of_expr res e
+  | Eghost e | Eexn (_,e) -> post_of_expr res e
   | Eexec (_,c) ->
       let conv q = open_post_with res q in
       copy_labels e (t_and_l (List.map conv c.cty_post))
@@ -957,6 +958,12 @@ let e_raise xs e ity =
   let eff = try_effect [e] eff_union_seq e.e_effect eff in
   mk_expr (Eraise (xs,e)) ity MaskVisible eff
 
+exception ExceptionLeak of xsymbol
+
+let e_exn xs e =
+  if Sxs.mem xs e.e_effect.eff_raises then raise (ExceptionLeak xs);
+  mk_expr (Eexn (xs,e)) e.e_ity e.e_mask e.e_effect
+
 (* snapshots, assertions, "any" *)
 
 let e_pure t =
@@ -977,6 +984,7 @@ let cty_add_variant d varl = let add s (t,_) = t_freepvs s t in
 
 let rec e_rs_subst sm e = e_label_copy e (match e.e_node with
   | Evar _ | Econst _ | Eassign _ | Eassert _ | Epure _ | Eabsurd -> e
+  | Eexn (xs,e) -> e_exn xs e
   | Eghost e -> e_ghostify true (e_rs_subst sm e)
   | Eexec (c,_) -> e_exec (c_rs_subst sm c)
   | Elet (LDvar (v,d),e) ->
@@ -1333,6 +1341,10 @@ and print_enode pri fmt e = match e.e_node with
         print_pv pv print_pv pvfrom
         (if dir = To then "to" else "downto") print_pv pvto
         print_invariant inv print_expr e
+  | Eexn (xs, e) ->
+      fprintf fmt (protect_on (pri > 0) "exception %a@ in@\n%a")
+        print_xs xs print_expr e;
+      forget_xs xs
   | Eraise (xs,e) when is_e_void e ->
       fprintf fmt "raise %a" print_xs xs
   | Eraise (xs,e) ->
@@ -1409,4 +1421,6 @@ let () = Exn_printer.register (fun fmt e -> match e with
       "Function %a is not a constructor" print_rs s
   | FieldExpected s -> fprintf fmt
       "Function %a is not a mutable field" print_rs s
+  | ExceptionLeak xs -> fprintf fmt
+      "Uncatched local exception %a" print_xs xs
   | _ -> raise e)

src/mlw/expr.mli

@@ -134,6 +134,7 @@ and expr_node =
   | Efor    of pvsymbol * for_bounds * invariant list * expr
   | Etry    of expr * (pvsymbol list * expr) Mxs.t
   | Eraise  of xsymbol * expr
+  | Eexn    of xsymbol * expr
   | Eassert of assertion_kind * term
   | Eghost  of expr
   | Epure   of term
@@ -224,6 +225,10 @@ val e_false : expr
 val is_e_true  : expr -> bool
 val is_e_false : expr -> bool
 
+exception ExceptionLeak of xsymbol
+
+val e_exn : xsymbol -> expr -> expr
+
 val e_raise : xsymbol -> expr -> ity -> expr
 
 val e_try : expr -> (pvsymbol list * expr) Mxs.t -> expr

src/mlw/ity.ml

@@ -1631,6 +1631,8 @@ let forget_pv v = forget_var v.pv_vs
 
 let print_xs fmt xs = pp_print_string fmt (id_unique xprinter xs.xs_name)
 
+let forget_xs xs = forget_id xprinter xs.xs_name
+
 exception FoundPrefix of pvsymbol list
 
 let unknown = create_pvsymbol (id_fresh "?") ity_unit

src/mlw/ity.mli

@@ -491,6 +491,7 @@ val cty_add_post : cty -> post list -> cty
 
 val forget_reg : region -> unit   (* flush id_unique for a region *)
 val forget_pv  : pvsymbol -> unit (* flush for a program variable *)
+val forget_xs  : xsymbol -> unit  (* flush for a local exception *)
 val forget_cty : cty -> unit      (* forget arguments and oldies *)
 
 val print_its : Format.formatter -> itysymbol -> unit (* type symbol *)

src/mlw/ocaml_printer.ml

@@ -447,6 +447,13 @@ module Print = struct
       fprintf fmt
         "@[<hv>@[<hov 2>begin@ try@ %a@] with@]@\n@[<hov>%a@]@\nend"
         (print_expr info) e (print_list newline (print_xbranch info)) bl
+    | Eexn (xs, None, e) ->
+      fprintf fmt "@[<hv>let exception %a in@\n%a@]"
+        (print_uident info) xs.xs_name (print_expr info) e
+    | Eexn (xs, Some t, e) ->
+      fprintf fmt "@[<hv>let exception %a of %a in@\n%a@]"
+        (print_uident info) xs.xs_name (print_ty ~paren:true info) t
+        (print_expr info) e
     | Eignore e -> fprintf fmt "ignore (%a)" (print_expr info) e
     (* | Enot _ -> (\* TODO *\) assert false *)
     (* | Ebinop _ -> (\* TODO *\) assert false *)
@@ -556,9 +563,3 @@ let fg ?fname m =
 
 let () = Pdriver.register_printer "ocaml"
   ~desc:"printer for OCaml code" fg print_decl
-
-(*
- * Local Variables:
- * compile-command: "make -C ../.. -j3 bin/why3extract.opt"
- * End:
- *)

src/mlw/pdecl.ml

@@ -215,6 +215,9 @@ let get_syms node pure =
               let del_rd syms rd = Sid.remove rd.rec_sym.rs_name syms in
               List.fold_left del_rd esms rdl in
         syms_let_defn (Sid.union syms esms) ld
+    | Eexn (xs, e) ->
+        let esms = syms_expr Sid.empty e in
+        Sid.union syms (Sid.remove xs.xs_name esms)
     | Efor (i,_,invl,e) ->
         syms_pv (syms_tl (syms_expr syms e) invl) i
     | Ewhile (d,invl,varl,e) ->

src/mlw/pinterp.ml

@@ -642,6 +642,7 @@ let rec eval_expr env (e : expr) : result =
         | Normal t -> Excep(xs,t)
         | _ -> r
     end
+  | Eexn(_,e1) -> eval_expr env e1
   | Eassert(_,_t) -> Normal Vvoid (* TODO *)
     (* TODO: do not eval t if no assertion check *)
 (*
@@ -816,10 +817,3 @@ let eval_global_symbol env m fmt rs =
   with Not_found ->
     eprintf "Symbol '%s' has no definition.@." rs.rs_name.Ident.id_string;
     exit 1
-
-
-(*
-Local Variables:
-compile-command: "unset LANG; make -C ../.. bin/why3execute.byte"
-End:
-*)

src/mlw/pmodule.ml

@@ -636,24 +636,31 @@ let cl_save_rs cl s s' =
 type smap = {
   sm_vs : vsymbol Mvs.t;
   sm_pv : pvsymbol Mvs.t;
+  sm_xs : xsymbol Mxs.t;
   sm_rs : rsymbol Mrs.t;
 }
 
 let sm_of_cl cl = {
   sm_vs = Mvs.map (fun v -> v.pv_vs) cl.pv_table;
   sm_pv = cl.pv_table;
+  sm_xs = cl.xs_table;
   sm_rs = cl.rs_table }
 
 let sm_save_vs sm v v' = {
   sm_vs = Mvs.add v v'.pv_vs sm.sm_vs;
   sm_pv = Mvs.add v v' sm.sm_pv;
+  sm_xs = sm.sm_xs;
   sm_rs = sm.sm_rs }
 
 let sm_save_pv sm v v' = {
   sm_vs = Mvs.add v.pv_vs v'.pv_vs sm.sm_vs;
   sm_pv = Mvs.add v.pv_vs v' sm.sm_pv;
+  sm_xs = sm.sm_xs;
   sm_rs = sm.sm_rs }
 
+let sm_save_xs sm s s' =
+  { sm with sm_xs = Mxs.add s s' sm.sm_xs }
+
 let sm_save_rs cl sm s s' =
   let sm = { sm with sm_rs = Mrs.add s s' sm.sm_rs } in
   match s.rs_logic, s'.rs_logic with
@@ -664,6 +671,10 @@ let sm_save_rs cl sm s s' =
 let sm_find_pv sm v = Mvs.find_def v v.pv_vs sm.sm_pv
   (* non-instantiated global variables are not in sm *)
 
+let sm_find_xs sm xs = Mxs.find_def xs xs sm.sm_xs
+
+let sm_find_rs sm rs = Mrs.find_def rs rs sm.sm_rs
+
 let clone_pv cl {pv_vs = vs; pv_ity = ity; pv_ghost = ghost} =
   create_pvsymbol (id_clone vs.vs_name) ~ghost (clone_ity cl ity)
 
@@ -824,7 +835,7 @@ let clone_cty cl sm ?(drop_decr=false) cty =
   let pre = clone_invl cl sm_args pre in
   let post = clone_invl cl sm_olds cty.cty_post in
   let xpost = Mxs.fold (fun xs fl q ->
-    let xs = cl_find_xs cl xs in
+    let xs = sm_find_xs sm xs in
     let fl = clone_invl cl sm_olds fl in
     Mxs.add xs fl q) cty.cty_xpost Mxs.empty in
   let add_read v s = Spv.add (sm_find_pv sm_args v) s in
@@ -844,7 +855,7 @@ let clone_cty cl sm ?(drop_decr=false) cty =
   let add_reset reg s = Sreg.add (clone_reg cl reg) s in
   let resets = Sreg.fold add_reset cty.cty_effect.eff_resets Sreg.empty in
   let eff = eff_reset (eff_write reads writes) resets in
-  let add_raise xs eff = eff_raise eff (cl_find_xs cl xs) in
+  let add_raise xs eff = eff_raise eff (sm_find_xs sm xs) in
   let eff = Sxs.fold add_raise cty.cty_effect.eff_raises eff in
   let eff = if cty.cty_effect.eff_oneway then eff_diverge eff else eff in
   let cty = create_cty ~mask:cty.cty_mask args pre post xpost olds eff res in
@@ -904,10 +915,13 @@ let rec clone_expr cl sm e = e_label_copy e (match e.e_node with
       let conv_br xs (vl, e) m =
         let vl' = List.map (clone_pv cl) vl in
         let sm = List.fold_left2 sm_save_pv sm vl vl' in
-        Mxs.add (cl_find_xs cl xs) (vl', clone_expr cl sm e) m in
+        Mxs.add (sm_find_xs sm xs) (vl', clone_expr cl sm e) m in
       e_try (clone_expr cl sm d) (Mxs.fold conv_br xl Mxs.empty)
   | Eraise (xs, e) ->
-      e_raise (cl_find_xs cl xs) (clone_expr cl sm e) (clone_ity cl e.e_ity)
+      e_raise (sm_find_xs sm xs) (clone_expr cl sm e) (clone_ity cl e.e_ity)
+  | Eexn ({xs_name = id; xs_mask = mask; xs_ity = ity} as xs, e) ->
+      let xs' = create_xsymbol (id_clone id) ~mask (clone_ity cl ity) in
+      e_exn xs' (clone_expr cl (sm_save_xs sm xs xs') e)
   | Eassert (k, f) ->
       e_assert k (clone_term cl sm.sm_vs f)
   | Eghost e ->
@@ -921,7 +935,7 @@ and clone_cexp cl sm c = match c.c_node with
       let vl = List.map (fun v -> sm_find_pv sm v) vl in
       let al = List.map (fun v -> clone_ity cl v.pv_ity) c.c_cty.cty_args in
       let res = clone_ity cl c.c_cty.cty_result in
-      c_app (Mrs.find_def s s sm.sm_rs) vl al res
+      c_app (sm_find_rs sm s) vl al res
   | Cpur (s,vl) ->
       let vl = List.map (fun v -> sm_find_pv sm v) vl in
       let al = List.map (fun v -> clone_ity cl v.pv_ity) c.c_cty.cty_args in

src/mlw/vc.ml

@@ -706,7 +706,8 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap =
         let f = vc_expl None lab expl_check f in
         let k = Kpar (Kstop f, k_unit res) in
         inv_of_pure env e.e_loc [f] k
-    | Eghost e0 ->
+    | Eghost e0
+    | Eexn (_,e0) ->
         k_expr env lps e0 res xmap
     | Epure t ->
         let t = if t.t_ty <> None then t_lab t else