Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for exceptional behaviour to printing runnable scenario #206

Merged
merged 2 commits into from
Mar 18, 2024

Conversation

n-osborne
Copy link
Collaborator

This PR proposes to add support for exceptional behaviour when printing a runnable scenariowhen a test is failing.

This PR is based on #204, please consider only the two last commits.

This PR should complete the story to fix #188

Again, if we introduce a bug in plugins/qcheck-stm/test/array.ml (here let get a _ = get a 7), we have now:

λ dune build @launchtests
File "plugins/qcheck-stm/test/dune.inc", line 49, characters 0-75:
49 | (rule
50 |  (alias launchtests)
51 |  (action
52 |   (run %{dep:array_stm_tests.exe} -v)))
random seed: 163835566
generated error fail pass / total     time test name
[✗]    1    0    1    0 / 1000     0.0s Array STM tests (generating)

--- Failure --------------------------------------------------------------------

Test Array STM tests failed (5 shrink steps):

   protect (fun () -> get sut (-952798241484687328))


+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Messages for test Array STM tests:

Gospel specification violation in function get

  File "array.mli", line 11, characters 11-26:
    0 <= i < t.size
  
when executing the following sequence of operations:

  open Array
  let protect f = try Ok (f ()) with e -> Error e
  let sut = make 16 'a'
  let r = protect (fun () -> get sut (-952798241484687328))
  assert (match r with
            | Error (Invalid_argument _) -> true
            | _ -> false)
  (* returned Ok ('a') *)
  

================================================================================
failure (1 tests failed, 0 tests errored, ran 1 tests)
                                     
[1]

So the call to any function that may raise an exception (according to the Gospel psecifications) are protected to return a ('a, exn) result instead of a simple 'a (as it is done today in QCheck-STM).

The value returned by the protected call is then compared to the expected result: here we were expecting an Invalid_argument exception because the clause is a checks, but in the case of a raises clause, the name of the expected exception will be printed.

Note that only the name of the exception is printed, this PR does not propose to handle the arguments of the said exception. I may want to wait to see how gospel#379 evolves.

@n-osborne n-osborne added this to the 0.2 milestone Mar 6, 2024
@n-osborne n-osborne force-pushed the print-exn-result branch 3 times, most recently from cd72dd1 to 5f0d547 Compare March 14, 2024 10:26
Copy link
Contributor

@shym shym left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This reads very nicely (might be a question of momentum, after reviewing a series of such PRs :-), thank you!

I wondered why you chose Either (introduced in 4.12 IIUC) rather than Result (introduced in 4.08), both on the dependency aspect and the fact that Result is a sensible use case to encode exception or not.
I would suggest we raise the dependency where needed if we keep Either.

By the way, I see that our runtime is already requiring 4.12 (do you remember why? the git history suggests that it was fixed thanks to a OPAM-CI complaining when we released 0.1, but it is otherwise short on details :-/ I should have written a better commit message then). If the reason for that 4.12 dependency for the runtime was strong anyway, we might just adopt it all across our packages.

@n-osborne
Copy link
Collaborator Author

n-osborne commented Mar 18, 2024

I went for Either as reporting an exception here is not really an error (or it is in the same way as reporting a value).

I agree on having consistency on on the ocaml version 👍

Collect the name of the exception when checking an exceptional
postcondition (not the arguments as they are not always specified).
@n-osborne n-osborne merged commit 0023018 into ocaml-gospel:main Mar 18, 2024
3 checks passed
@n-osborne n-osborne deleted the print-exn-result branch March 18, 2024 11:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

ortac-qcheck-stm: print which invariant failed and more details about the failure
2 participants