diff options
| -rw-r--r-- | src/c_backend.ml | 9 | ||||
| -rw-r--r-- | src/interpreter.ml | 11 | ||||
| -rw-r--r-- | src/type_check.mli | 2 | ||||
| -rw-r--r-- | test/c/fallthrough_exception.expect | 1 | ||||
| -rw-r--r-- | test/c/fallthrough_exception.sail | 20 |
5 files changed, 38 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 *) diff --git a/test/c/fallthrough_exception.expect b/test/c/fallthrough_exception.expect new file mode 100644 index 00000000..6d9de85e --- /dev/null +++ b/test/c/fallthrough_exception.expect @@ -0,0 +1 @@ +E2 diff --git a/test/c/fallthrough_exception.sail b/test/c/fallthrough_exception.sail new file mode 100644 index 00000000..6260a603 --- /dev/null +++ b/test/c/fallthrough_exception.sail @@ -0,0 +1,20 @@ +default Order dec + +$include <prelude.sail> + +val print = "print_endline" : string -> unit + +union exception = { + E1 : unit, + E2 : unit +} + +function main((): unit) -> unit = { + try { + try throw(E2()) catch { + E1() => print("E1") + } + } catch { + E2() => print("E2") + } +}
\ No newline at end of file |