Fix behavior for fallthrough cases in catch blocks

Make all backends behave the same when a catch block does not catch a
specific exception.

3 files changed, 17 insertions, 5 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 41970184..ee900569 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1121,6 +1121,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let aexp_setup, aexp_call, aexp_cleanup = compile_aexp ctx aexp in
      let try_return_id = gensym () in
      let handled_exception_label = label "handled_exception_" in
+     let fallthrough_label = label "fallthrough_exception_" in
      let compile_case (apat, guard, body) =
        let trivial_guard = match guard with
          | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _)
@@ -1146,14 +1147,14 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        [iblock case_instrs; ilabel try_label]
      in
      assert (ctyp_equal ctyp (ctyp_of_typ ctx typ));
-     [icomment "begin try catch";
-      idecl ctyp try_return_id;
+     [idecl ctyp try_return_id;
       itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup);
       ijump (F_unary ("!", F_have_exception), CT_bool) handled_exception_label]
      @ List.concat (List.map compile_case cases)
-     @ [imatch_failure ();
+     @ [igoto fallthrough_label;
         ilabel handled_exception_label;
-        icopy l CL_have_exception (F_lit (V_bool false), CT_bool)],
+        icopy l CL_have_exception (F_lit (V_bool false), CT_bool);
+        ilabel fallthrough_label],
      (fun clexp -> icopy l clexp (F_id try_return_id, ctyp)),
      []
 
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 40ee251d..1e1bb816 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -110,6 +110,15 @@ let value_of_exp = function
   | (E_aux (E_internal_value v, _)) -> v
   | _ -> failwith "value_of_exp coerction failed"
 
+let fallthrough =
+  let open Type_check in
+  try
+    let env = initial_env |> Env.add_scattered_variant (mk_id "exception") (mk_typquant []) in
+    check_case env exc_typ (mk_pexp (Pat_exp (mk_pat (P_id (mk_id "exn")), mk_exp (E_throw (mk_exp (E_id (mk_id "exn"))))))) unit_typ
+  with
+  | Type_error (_, l, err) ->
+     Reporting.unreachable l __POS__ (Type_error.string_of_type_error err);
+
 (**************************************************************************)
 (* 1. Interpreter Monad                                                   *)
 (**************************************************************************)
@@ -491,7 +500,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
      begin
        catch (step exp) >>= fun exp' ->
        match exp' with
-       | Left exn -> wrap (E_case (exp_of_value exn, pexps))
+       | Left exn -> wrap (E_case (exp_of_value exn, pexps @ [fallthrough]))
        | Right exp' -> wrap (E_try (exp', pexps))
      end
 
diff --git a/src/type_check.mli b/src/type_check.mli
index 82e9ebc1..801a07ec 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -120,6 +120,8 @@ module Env : sig
 
   val add_local : id -> mut * typ -> t -> t
 
+  val add_scattered_variant : id -> typquant -> t -> t
+
   (** Check if a local variable is mutable. Throws Type_error if it
      isn't a local variable. Probably best to use Env.lookup_id
      instead *)