Unhandled: a static checker for unhandled effects in OCaml 5, and a negative result

Ecosystem
1

OCaml 5’s effect handlers are untyped: the compiler does not check that a
performed effect is handled, so a missing handler compiles cleanly and fails
at run time with Effect.Unhandled. We have been building a static checker
for that, and we would like some criticism of it, particularly of the parts
we think are weakest.

What it does. It reads the compiler’s own .cmt files, infers a
per-function effect set, propagates by call-graph fixpoint, subtracts effects
discharged at handler sites, and reports every perform that can reach a
program entry point unhandled. Findings come with a blame path from entry to
perform, and with a generated witness program: we synthesise it, compile it,
run it, and only report the finding as confirmed if the effect actually
arrives at an outer boundary.

How it is tested. Differential testing against the runtime as oracle: a
generator emits programs, and we compare the checker’s prediction against what
the compiled program actually does when executed. Over 1000 generated
programs, 0 false negatives. Branch-free programs: 600, no false positives.
Branching programs: 400, 5.3% false positives, from joining both arms of a
conditional. The witnesses deliberately do not parse the crash message.
Handy, since 5.4 stopped printing the effect payload for two of our test
programs and nothing broke.

The negative result, which is the reason for this post. We wanted to show
the checker catches crashes that really happened, so we built a corpus of
commits that fixed documented Effect.Unhandled problems and analysed each
parent commit. It caught 0 of 6. The cause turned out to be that the modules
the bugs lived in never compiled in our environment, so the analyser was never
shown the code. The batch runner now reports “out of scope” separately from
“missed” for exactly this reason.

Then we ran it across every opam package depending on eio, eio_main,
picos, domainslib, riot, moonpool or miou, giving 85 repositories
after deduplicating by dev-repo. 38 of them built far enough to analyse,
3,881 modules in total, and the tool reported 31 escapes. Every single one
was our own false positive. Four causes, each found by reading the code we
had accused:

  1. We modelled “calls anything under Eio.” as “requires an Eio runtime”.
    Wrong for constructors and vtable builders: Eio.Flow.Pi.source,
    Eio.Stream.create, Eio.Condition.create,
    Eio.Buf_read.parse_string_exn.

  2. We applied that client-usage model to eio’s own source, which is a
    category error. eio does not need an Eio runtime to define itself.

  3. We did not see through application operators. let@ env = Eio_main.run in body is ( let@ ) Eio_main.run (fun env -> body), and with the operator
    opaque the head of that application is not Eio_main.run, so the scheduler
    boundary vanished and an entire program looked like it ran with no runtime.
    The fix is to read %apply and %revapply out of the value description,
    which would also cover @@, |>, and operators a project defines for
    itself.

  4. We only recognised an Effect.Unhandled guard when it named the exception.
    picos writes it as a catch-all and says why:

    | exception _exn ->
    (* This should only happen when not running under a scheduler.
       However, we don't match on a specific exception, because it
       depends on the OCaml version. *)

    We had recorded the same observation independently, and then watched 5.4
    stop printing the effect payload, which is the same problem from the other
    side.

Causes 1 and 2 are fixed and regression-tested in both directions. Causes 3
and 4 are diagnosed but not yet fixed: the attempt broke the test suite and we
reverted it rather than ship a red one, so they are written up in
docs/LIMITATIONS.md with the forester and picos source that produced them.
Twenty-five escapes fixed, six remaining and explained.

Every escape this tool has ever reported on third-party code has turned out
to be our own false positive. We have not found a real bug in anyone’s
code. We would rather say that plainly than imply otherwise.

If there is a transferable lesson it is probably that one: a checker pointed
at real code for the first time is mostly measuring itself, and the only way
to tell the difference is to read the source you just accused.

What we would like criticism of.

  • Is the library-contract output useful to you? On picos it produces:
module Picos
  Picos.Trigger.await                may perform {Picos.Trigger.Await}
  Picos.Fiber.current                may perform {Picos.Fiber.Current}
  Picos.Fiber.spawn                  may perform {Picos.Fiber.Spawn}
  Picos.Fiber.yield                  may perform {Picos.Fiber.Yield}
  Picos.Fiber.Maybe.to_fiber_or_current may perform {Picos.Fiber.Current}
  Picos.Fiber.Maybe.or_current       may perform {Picos.Fiber.Current}
  Picos.Fiber.Maybe.current_if       may perform {Picos.Fiber.Current}
  Picos.Fiber.Maybe.current_and_check_if may perform {Picos.Fiber.Current, ...unknown}

module Picos_std_event__Event
  Picos_std_event__Event.sync        may perform {Picos.Trigger.Await, ...unknown}
  Picos_std_event__Event.select      may perform {Picos.Trigger.Await, ...unknown}

module Picos_std_structured__Run
  Picos_std_structured__Run.spawn    may perform {Picos.Fiber.Spawn, ...unknown}

...unknown in a set means the contract is incomplete at that function
because it calls something we have no .cmt for; we would rather show that
than round it down to a clean-looking set.

Is a machine-checked statement of “what this library asks its callers to
handle” worth having in a README or in CI?

  • What shapes do we miss? We know about effects performed inside effc
    branch bodies, dynamically built handler records, and closures that reach a
    call site through a data structure (no 0-CFA yet). We would like to hear
    about the ones we do not know about.

  • The scheduler model, meaning which entry point installs handlers for which
    family of effects, is data rather than analysis, and lives in
    models/schedulers.conf. The eio entries are cited to specific lines. The riot, moonpool and miou entries are
    guesses and labelled as such. Corrections very welcome.

  • Has anyone actually hit an Effect.Unhandled crash in production? We are
    short of real examples and would take any pointer, including “we hit it and
    the cause was something your design cannot see”.

Requires OCaml 5.3 or later, since Texp_match only grows its effect-case
list in 5.3. CI runs 5.3 and 5.4.

Repository: GitHub - manishpaulish/unhandled: A static effect-safety checker for OCaml 5: the analyzer that proves its own warnings. SegFault 2026. · GitHub

Happy to be told the approach is wrong.

2

Being able to analyse OCaml code like this seems pretty cool, even if this particular use didn’t find anything. Maybe it would help with Why Ocsigen is staying on Lwt (for now) for example?

I don’t think I have. I have had the opposite problem though: when running Eio and Lwt code together, I’d like to be sure that the Lwt code doesn’t perform an Eio effect, even though it will be handled. This can result in deadlock because Lwt assumes that all code returns immediately (if the code needs to wait, it will immediately return a promise).

Lwt_eio has Lwt_eio.with_event_loop ~debug:true, which catches all effects from Lwt code and reports an error, but a static analysis might be better.

The main case I worry about is callbacks from C to OCaml, since effects don’t work over a C call (C functions can’t be suspended).

The most common case of unhandled effects in Eio is in unit-tests, since you don’t need to start an event loop to get access to mock resources for testing, so it’s easy to forget. But a runtime error is reported immediately, so there’s no benefit to static analysis here.

3

This is more useful than the entire sweep was, thank you.

Taking the unit-test point first, because I think you are right and it is worth
saying so plainly. A missing handler in a test crashes immediately with the
effect named in the message. A static checker that tells you what the next
dune test would have told you anyway is not worth installing. That is most of
the crash-finding case, and it explains my negative result better than my own
post did: I built a detector for a failure mode that is already loud.

The Lwt case is the opposite and I had not seen it. Let me restate it so you can
tell me if I have it wrong. The effect is performed, a handler catches it, the
program does not crash, and it is still wrong, because Lwt’s engine assumed the
callback returned immediately when in fact it suspended. So the property is not
“this perform has no handler”. It is “this perform is inside a region where
suspending is forbidden, even though a handler exists”. Handled, and still
broken, and with no crash to observe.

That is a different question over machinery I already have. The tool computes a
per-function effect set by call-graph fixpoint and subtracts effects discharged
at handler sites. There is also a table of contexts where performing anything is
fatal, currently:

{ path = "Stdlib.Gc.finalise";     callback_arg = 0; why = "a finaliser, ..." }
{ path = "Stdlib.Sys.set_signal";  callback_arg = 1; why = "a signal handler, ..." }
{ path = "Stdlib.Callback.register"; callback_arg = 1;
  why = "a callback invoked from C, which an effect cannot cross" }
{ path = "Stdlib.Thread.create";   callback_arg = 0;
  why = "a new systhread, where the spawn site's handlers do not apply" }

Each entry names a function, says which argument is the callback, and the
analysis reports anything reachable from that callback that can perform. What
you are describing is the same shape with one field added: instead of “every
effect is fatal here”, it is “effects in the Eio family are forbidden here,
everything else is fine”. My existing entries become the degenerate case where
the forbidden set is everything. Then Lwt_eio.run_eio is an escape hatch that
reopens the region, structurally the same as a handler discharging an effect.

Two reasons I would rather build this than speculate about it.

First, with_event_loop ~debug:true gives me a runtime oracle, and that is
exactly how the rest of the tool is tested. My whole methodology is differential
against execution: generate a program, ask the checker, run it, see who was
right. For unhandled effects the oracle is the crash. Here the oracle is your
debug mode, which is a better one, because a deadlock gives you nothing to
observe on its own.

Second, the boundary is data rather than analysis, which is where I have been
careful to be honest about what I know. The scheduler model is a config file,
the eio entries are cited to specific lines in your source, and the riot,
moonpool and miou entries are labelled as guesses because they are.

So the one thing I would like from you rather than guess at: which functions
open and close the region? My reading is that Lwt_eio.run_lwt and
Lwt_eio.Promise.await_eio are the two ways you end up executing Lwt code, and
Lwt_eio.run_eio and Lwt_eio.Promise.await_lwt are the sanctioned ways back
across. Is that the whole boundary? In particular, does a callback passed to
Lwt.bind inside an Lwt_eio program count as Lwt code for this purpose, or
only the bodies passed to those entry points? I would rather have that from you
in one line than infer it and mislabel it as confirmed.

On C callbacks: that one is already in, as Callback.register in the table
above, on the manual’s line that an effect cannot cross caml_callback. It
reports the callback body, not the registration site. I have no real-world test
case for it though, so if you know of a library that registers an OCaml callback
which transitively touches Eio, I would like to point it at that and find out
whether it works or whether I have only tested it against my own examples.

The Ocsigen thread is a good pointer, thank you. Vincent’s second obstacle is
the same class: a DOM event handler is invoked by the browser with no Eio
handler on the stack, so any perform is unconditionally fatal rather than racy.
That is the finaliser case with a different registrar, and it is the kind of
thing this can already answer for a whole codebase at once rather than one call
site at a time. I will look at whether js_of_ocaml’s event registration is
recognisable in the typed tree the way Sys.set_signal is.

4

Yes, here’s an example of a typical Lwt_eio bug:

open Eio.Std
open Lwt.Syntax

let sleep n =
  Eio_unix.sleep n;     (* Error: using Eio from Lwt context *)
  Lwt.return_unit

let lwt_code () =
  let timeout = sleep 3.0 in
  let* () = Lwt_io.print "Lwt job starts...\n" in
  let* () = timeout in
  Lwt_io.print "Lwt job finished\n"

let () =
  Eio_main.run @@ fun env ->
  Lwt_eio.with_event_loop ~clock:env#clock ~debug:false @@ fun () ->
  Fiber.both
    (fun () -> Lwt_eio.run_lwt lwt_code)
    (fun () ->
       traceln "Eio job starts...";
       Eio_unix.sleep 1.0;
       traceln "Eio job finished"

The Lwt code is expecting sleep 3.0 to immediately return a promise, but instead it waits and then returns a resolved promise. It’s an easy mistake to make while porting code, and it’s confusing to debug because the Eio parts continue to run while the Lwt parts stop.

The output is:

+Eio job starts...                 
+Eio job finished
Lwt job starts...
Lwt job finished

With ~debug:true you get:

Fatal error: exception Invalid_argument("Attempt to perform effect in Lwt context")

When fixed with let sleep = Lwt_unix.sleep you get the correct output:

+Eio job starts...                 
Lwt job starts...
+Eio job finished
Lwt job finished

Yes, although in this case debug mode catches all effects (since existing code typically doesn’t use any and getting the full set is hard).

One the run ones matter. For await, the code is already running. And yes, Lwt.bind should only be used from Lwt context.

I don’t have a good example for the C callbacks. The cases where I’ve seen it, it happened every time and so didn’t get missed (it was also more of a problem with the old Eio luv bindings, since they ran the mainloop itself as C code, but that’s been replaced now).

5

That example is exactly what I needed, thank you. It goes into the corpus as
the first real test case for this, with your three outputs as the expected
results: the silent wrong ordering under ~debug:false, the Invalid_argument
under ~debug:true, and the correct interleaving once sleep is
Lwt_unix.sleep. Having a case where the bug is a reordering rather than a
crash is worth more to me than a dozen synthetic ones, because it is the
failure mode I cannot generate convincingly by hand.

Two things in your answer change the design, and both make it smaller.

Only the run functions matter, so the table is two entries rather than four.
And since debug mode catches all effects rather than the Eio family, the
forbidden set is everything, which means the extra field I was proposing is not
needed. My existing table already says “performing anything inside this
callback is an error”. The one thing it cannot express is the escape hatch:
Lwt_eio.run_lwt opens the region and Lwt_eio.run_eio closes it again. That
is a smaller change than the one I described, which is usually a good sign.

On “getting the full set is hard”: that is the one place where reading .cmt
files has an advantage over the dynamic check. I do not have to enumerate the
Eio family in advance, because the effect name comes out of the typed tree at
the perform site. So where debug mode reports that an effect happened, this
should be able to say which effect, at which line, and through which chain of
calls from run_lwt. Whether that is worth much over an immediate
Invalid_argument is a fair question, and the honest answer is probably “only
when the path is rare enough that the test suite never takes it”, which is the
same argument I just conceded about unit tests, pointed the other way.

Dropping the C callback question, given it fails every time and gets noticed.

I will report back when it runs on your example, or when I find out why it does
not.

6

Reporting back, as promised.

The short answer is that it fires on two reduced forms of your example and stays silent on the one you actually wrote. Against the real lwt_eio, Eio.Fiber and Eio_unix rather than a mock:

probe1_direct   E005 reported   Lwt_eio.run_lwt at the top level
probe2_fiber    E005 reported   the same call inside Eio.Fiber.both
probe3_loop     silent          the same call inside Lwt_eio.with_event_loop

Probe 3 is your program, so the honest headline is that the feature does not yet work on the case that motivated it. bench/lwt_demo.sh runs all three.

What is established rather than assumed: the effect is seen, and contract reports Lwt_ctx.sleep may perform {Eio__core.Suspend.Suspend} and propagates it to lwt_code; the rule matches the real Lwt_eio.run_lwt path, per probe 1; and the runtime agrees with you exactly, the buggy program serialising the two jobs and the fixed one interleaving them.

This is the term the analysis has built at the point it goes wrong:

call Lwt_eio.with_event_loop @8
join
  join []

The callee is correctly unresolved, the lambda handed to it is correctly applied, and the applied body still evaluates to empty. Fiber.both is not the cause, since probe 2 differs from probe 3 only by that wrapper and does report the finding. So the analysis knows the effect, knows the region, and loses the connection between them at depth.

Both of your corrections made the design smaller. Only the run functions matter, so it is one table entry rather than four, and since debug mode forbids all effects rather than the Eio family, the extra field I was proposing was not needed. What the table could not express was the escape hatch, so entries now carry a permits list: Lwt_eio.run_lwt opens the region and Lwt_eio.run_eio closes it. models/schedulers.conf cites this thread rather than guessing.

The part actually worth reporting is what the hunt turned up. Four of my five attempts guessed at a path name or an argument position without looking at anything. The one that worked printed the term the analysis had already computed, and found a real defect in a single run: a lambda passed to a callee we have no .cmt for was assumed never to be called. That is unsound, and it had been quietly swallowing effects in every with_resource (fun r -> ...) in the corpus, a pattern with nothing to do with Lwt. That fix is worth more than the feature that prompted it, and I would not have gone looking without your example.

One correction to my first post while I am here. The sweep has since been re-run over a larger corpus: 96 repositories, 48 of them analysed, 4,735 modules, rather than the 85, 38 and 3,881 I quoted. The conclusion is unchanged. Every escape I have triaged is still my own false positive.

7

I find this thread difficult to read because the style of the text is off, as if it was not written by a human, and the posts are fairly long, and usually towards the end of the post there is a remark that says that what you are doing does not work at all. My impression is that one of the following is true:

  1. The effect checking work you are doing is very useful, but production software on opam does not have this sort of mistakes so it is reasonable that only false alarms are found, or
  2. Despite the impressive description, the project is implemented without enough human expertise, will lead nowhere, and reading copious amount of AI-generated text about it is a waste of my time, I should run away.

This issue of style set aside, and before I run away, I have a few questions:

  • Is there a set of tests that have been written by a human, testing both bugs and non-bugs scenarios, on which the tool is known to perform well?
  • Why are the handlers assumed/axiomatized rather than analyzed? (maybe the logic you have implemented to add and substract effects could be used to analyze the effect itself?)
  • I don’t understand why you are posting to explain, in details, what does not work within your tools. (In both messages this takes most of the space.) Presumably this information is useful for people working on the tool directly and not much for other people? I would naively expect someone advertising for such a tool to focus first on the part that works correctly, that users could be curious about. Or: if the point is to ask experts for advanced use-cases they would like to see supported, as @talex5’ excellent feedback is doing, then maybe it is possible to say so without going in details about internal tool failures.