diff --git a/CHANGES.md b/CHANGES.md index 0b76d1e84..a947b2142 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,11 @@ # Changes +## Next version + +- #324: When a command causes an unexpectedly uncaught exception, + display that command along with the exception itself in both + `Lin` and `STM` + ## 0.2 - #342: Add two submodules of combinators in `Util`: diff --git a/lib/STM.ml b/lib/STM.ml index a6dc0b79a..00923f716 100644 --- a/lib/STM.ml +++ b/lib/STM.ml @@ -170,7 +170,7 @@ struct let rec interp_agree s sut cs = match cs with | [] -> true | c::cs -> - let res = Spec.run c sut in + let res = try Spec.run c sut with e -> Util.wrap_uncaught_exn Spec.show_cmd c e in let b = Spec.postcond c s res in let s' = Spec.next_state c s in b && interp_agree s' sut cs @@ -178,7 +178,7 @@ struct let rec check_disagree s sut cs = match cs with | [] -> None | c::cs -> - let res = Spec.run c sut in + let res = try Spec.run c sut with e -> Util.wrap_uncaught_exn Spec.show_cmd c e in let b = Spec.postcond c s res in let s' = Spec.next_state c s in if b diff --git a/lib/lin.ml b/lib/lin.ml index ab7b12873..6e29b5a9e 100644 --- a/lib/lin.ml +++ b/lib/lin.ml @@ -479,6 +479,8 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct apply_f (f arg) rem state let run cmd state = - let Cmd { args ; rty ; f ; _ } = cmd in - Res (rty, apply_f f args state) + try + let (Cmd { args; rty; f; _ }) = cmd in + Res (rty, apply_f f args state) + with e -> Util.wrap_uncaught_exn show_cmd cmd e end diff --git a/lib/util.ml b/lib/util.ml index 71fc4d3e6..37d5c6ce1 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -75,6 +75,23 @@ let protect (f : 'a -> 'b) (a : 'a) : ('b, exn) result = try Result.Ok (f a) with e -> Result.Error e +exception Uncaught_exception of string * exn + +let print_uncaught_exception e = + match e with + | Uncaught_exception (cmd, exc) -> + Some + (Format.sprintf "%s raised but not caught while running %s" + (Printexc.to_string exc) cmd) + | _ -> None + +let _ = + Printexc.register_printer print_uncaught_exception + +let wrap_uncaught_exn show x e = + let bt = Printexc.get_raw_backtrace () in + Printexc.raise_with_backtrace (Uncaught_exception (show x, e)) bt + module Pp = struct open Format diff --git a/lib/util.mli b/lib/util.mli index 128ef66a5..2c16f1a32 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -41,6 +41,20 @@ val print_triple_vertical : val protect : ('a -> 'b) -> 'a -> ('b, exn) result (** [protect f] turns an [exception] throwing function into a [result] returning function. *) +exception Uncaught_exception of string * exn +(** [Uncaught_exception (cmd, exc)] is used to signal that the + exception [exc] was not caught (but should have been) during the + execution of [cmd]. That exception will be printed as: + ["... raised but not caught while running " ^ cmd]. *) + +val wrap_uncaught_exn : ('a -> string) -> 'a -> exn -> 'b +(** [wrap_uncaught_exn show x e] wraps the exception [e] into an + [Uncaught_exception] with the command as pretty-printed by + [show x] and raises that [Uncaught_exception]. + [wrap_uncaught_exn] preserves the current backtrace so it + must be called from the exception handler, like so: + [try ... with e -> wrap_uncaught_exn show x e] *) + module Pp : sig (** Pretty-printing combinators that generate valid OCaml syntax for common types along with combinators for user-defined types *) diff --git a/test/dune b/test/dune index 3e0e6d205..844c06564 100644 --- a/test/dune +++ b/test/dune @@ -54,3 +54,30 @@ (libraries qcheck-stm.sequential threads.posix) (action (with-accepted-exit-codes 1 (run ./%{test} --verbose --seed 229109553)))) + +(test + (name uncaught_lin) + (package qcheck-lin) + (modules uncaught_lin) + (libraries qcheck-lin.domain) + (enabled_if (>= %{ocaml_version} 5)) + (action + (pipe-outputs + (with-accepted-exit-codes 1 + (run %{test} --no-colors --verbose --seed 260395858)) + ; filter out output that is not deterministic enough across + ; versions and platforms + (run sed -e "/^[[]/d" -e "s/ ([0-9]* shrink steps)//")))) + +(test + (name uncaught_stm) + (package qcheck-stm) + (modules uncaught_stm) + (libraries qcheck-stm.sequential) + (action + (pipe-outputs + (with-accepted-exit-codes 1 + (run %{test} --no-colors --verbose --seed 260395858)) + ; filter out output that is not deterministic enough across + ; versions and platforms + (run sed -e "/^[[]/d" -e "s/ ([0-9]* shrink steps)//")))) diff --git a/test/uncaught_lin.expected b/test/uncaught_lin.expected new file mode 100644 index 000000000..55a2ab4b4 --- /dev/null +++ b/test/uncaught_lin.expected @@ -0,0 +1,32 @@ +random seed: 260395858 +generated error fail pass / total time test name + +=== Error ====================================================================== + +Test Lin DSL test of uncaught exceptions errored on: + + | + always_fail t + | + .---------------------. + | | + + +exception Failure("unexpected") raised but not caught while running always_fail t + + +=== Error ====================================================================== + +Test neg Lin DSL test of uncaught exceptions errored on: + + | + always_fail t + | + .---------------------. + | | + + +exception Failure("unexpected") raised but not caught while running always_fail t + +================================================================================ +failure (0 tests failed, 2 tests errored, ran 2 tests) diff --git a/test/uncaught_lin.ml b/test/uncaught_lin.ml new file mode 100644 index 000000000..66e13a61e --- /dev/null +++ b/test/uncaught_lin.ml @@ -0,0 +1,24 @@ +(* Test of the behaviour of Lin tests with uncaught exceptions *) + +let always_fail () = failwith "unexpected" + +module UncaughtExcConf = struct + open Lin + + type t = unit + + let init () = () + let cleanup _ = () + let api = [ val_ "always_fail" always_fail (t @-> returning unit) ] +end + +module UncaughtExc_domain = Lin_domain.Make (UncaughtExcConf) + +let _ = + QCheck_base_runner.run_tests_main + [ + UncaughtExc_domain.lin_test ~count:10 + ~name:"Lin DSL test of uncaught exceptions"; + UncaughtExc_domain.neg_lin_test ~count:10 + ~name:"neg Lin DSL test of uncaught exceptions"; + ] diff --git a/test/uncaught_stm.expected b/test/uncaught_stm.expected new file mode 100644 index 000000000..b5e4a9877 --- /dev/null +++ b/test/uncaught_stm.expected @@ -0,0 +1,24 @@ +random seed: 260395858 +generated error fail pass / total time test name + +=== Error ====================================================================== + +Test STM test of uncaught exceptions errored on: + + AlwaysFail () + + +exception Failure("unexpected") raised but not caught while running AlwaysFail () + + +=== Error ====================================================================== + +Test neg STM test of uncaught exceptions errored on: + + AlwaysFail () + + +exception Failure("unexpected") raised but not caught while running AlwaysFail () + +================================================================================ +failure (0 tests failed, 2 tests errored, ran 2 tests) diff --git a/test/uncaught_stm.ml b/test/uncaught_stm.ml new file mode 100644 index 000000000..5402094d1 --- /dev/null +++ b/test/uncaught_stm.ml @@ -0,0 +1,32 @@ +(* Test of the behaviour of STM tests with uncaught exceptions *) + +let always_fail () = failwith "unexpected" + +module UncaughtExcConf : STM.Spec = struct + open STM + + type sut = unit + type state = unit + type cmd = AlwaysFail of sut + + let show_cmd = function AlwaysFail () -> "AlwaysFail ()" + let arb_cmd _ = QCheck.(make ~print:show_cmd (Gen.pure (AlwaysFail ()))) + let init_state = () + let next_state _ _ = () + let init_sut _ = () + let cleanup _ = () + let precond _ _ = true + let run c s = match c with AlwaysFail () -> Res (unit, always_fail s) + + let postcond c _ r = + match (c, r) with AlwaysFail (), Res ((Unit, _), _) -> true | _ -> false +end + +module UE = STM_sequential.Make (UncaughtExcConf) + +let _ = + QCheck_base_runner.run_tests_main + [ + UE.agree_test ~count:10 ~name:"STM test of uncaught exceptions"; + UE.neg_agree_test ~count:10 ~name:"neg STM test of uncaught exceptions"; + ]