From 7747f9bf37e771e72ad4c8eea04eaa5f83def242 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Mon, 5 Jun 2023 16:55:50 +0200 Subject: [PATCH 1/6] Add Util.Uncaught_exception and Util.wrap_uncaught_exn Add the utilitary exception Uncaught_exception and function wrap_uncaught_exn to improve the error reports in cases of uncaught exceptions This will allow STM and Lin to display the command along with the exception when a command raises an exception but its description did not announce it so --- lib/util.ml | 17 +++++++++++++++++ lib/util.mli | 14 ++++++++++++++ 2 files changed, 31 insertions(+) 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 *) From c9bb098bcd62454a69d3cafdafd3818b6df4f539 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Mon, 5 Jun 2023 17:06:32 +0200 Subject: [PATCH 2/6] Lin: Print commands that trigger uncaught exceptions The standard QCheck mechanism to catch exceptions that are raised in tests do not give much clue about the source (ie Lin command) of that exception This packs the unsoundly-specified command with the exception in such a case so that it can be displayed Before: ``` exception Failure("unexpected") ``` After: ``` exception Failure("unexpected") raised but not caught while running always_fail t ``` --- lib/lin.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 From b340e7f99840690241ea914b54ed518a445554a0 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Mon, 5 Jun 2023 17:02:52 +0200 Subject: [PATCH 3/6] Add an internal test for Lin on uncaught exceptions --- test/dune | 14 ++++++++++++++ test/uncaught_lin.expected | 32 ++++++++++++++++++++++++++++++++ test/uncaught_lin.ml | 24 ++++++++++++++++++++++++ 3 files changed, 70 insertions(+) create mode 100644 test/uncaught_lin.expected create mode 100644 test/uncaught_lin.ml diff --git a/test/dune b/test/dune index 3e0e6d205..b19e2083a 100644 --- a/test/dune +++ b/test/dune @@ -54,3 +54,17 @@ (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)//")))) 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"; + ] From 7020dd3e6be8bb79755aa97b17b37350ff72e3d9 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Mon, 5 Jun 2023 17:04:03 +0200 Subject: [PATCH 4/6] STM: Print commands that trigger uncaught exceptions The standard QCheck mechanism to catch exceptions that are raised in tests do not give much clue about the source (ie STM command) of that exception This packs the unsoundly-specified command with the exception in such a case so that it can be displayed Before: ``` exception Failure("unexpected") ``` After: ``` exception Failure("unexpected") raised but not caught while running AlwaysFail () ``` --- lib/STM.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 From 256047eee66d77d79cb3e8152a61fcf0df292b2d Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Mon, 5 Jun 2023 17:03:29 +0200 Subject: [PATCH 5/6] Add an internal test for STM on uncaught exceptions --- test/dune | 13 +++++++++++++ test/uncaught_stm.expected | 24 ++++++++++++++++++++++++ test/uncaught_stm.ml | 32 ++++++++++++++++++++++++++++++++ 3 files changed, 69 insertions(+) create mode 100644 test/uncaught_stm.expected create mode 100644 test/uncaught_stm.ml diff --git a/test/dune b/test/dune index b19e2083a..844c06564 100644 --- a/test/dune +++ b/test/dune @@ -68,3 +68,16 @@ ; 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_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"; + ] From 8c89082abbaf2fc1d3fa224938f47deccc92c08c Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Mon, 5 Jun 2023 17:42:25 +0200 Subject: [PATCH 6/6] Update CHANGES with #324 Print commands with uncaught exceptions --- CHANGES.md | 6 ++++++ 1 file changed, 6 insertions(+) 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`: