See the root page for precise exceptions.
Fixing precise exceptions in strictness analysis
Precise exception semantics are really sensitive to transformations changing evaluation order. The prime example of a transformation that changes evaluation order is the worker/wrapper transformation, which feeds on information from strictness analysis to turn call-by-need into call-by-value.
#13380 (closed) shows that we can't treat precise exceptions as just any kind of divergence wrt. strictness analysis. It turns out that we were eagerly evaluating a variable (
y) that we shouldn't actually be strict in as per precise exception semantics.
raiseIO# lazy to preserve precise exceptions, hackily (Step 1)
This was implemented in !2956 (closed).
raiseIO# used to have a
botDiv. This means that it is strict in any free variable (such as
y) and easily fixed by giving it
But that leads to a lot of dead code when a
raiseIO# appliction occurs as a case scrutinee, as the Simplifier fails to eliminate
raiseIO#'s continuation (e.g. its alts) as it could before. There's a simple solution: Treat
raiseIO# specially in the simplifier, so that we drop its continuation although it has
topDiv. That's the hack.
- Give it special treatment in
mkArgInfo, treating it as if it had
Replacing hacks by principled program analyses (Step 2)
Dead code elimination for
ExnOrDiv (Step 2.1)
Special casing on
raiseIO# in the Simplifier is gross, and only needed because it now has
topDiv for its lazy default free variable demand (
defaultFvDmd). We can fix that by introducing
Divergence, denoting that evaluation will diverge(, throw an imprecise exception) or throw a precise exception, but surely never converge. The
exnDiv then is as lazy as for
topDiv. But entering an expression for which we infer such a
Divergence will never return, thus is a dead end. Thus we rename
isDeadEndDiv, similarly all functions that use it and can delete the special case for
The only analysis that I recognise plays a little fast and loose with
botDiv probably is
CoreArity (which will turn
exprBotStrictness_maybe), but I guess we'll fix that when it has bitten us.
Turn the "IO hack" into the proper analysis it should have been, introducing
ConOrDiv (Step 2.2)
We implemented this in !3014 (closed), but it had difficult to predict implications on performance, bugs and was very complicated. So this didn't make it into master.
The "IO hack" (which should rather be called
scrutineeMayThrowPreciseException) is incredibly imprecise (as a program analysis) because it's so syntactic and just assumes that any composite
IO action throws a precise exception. At the same time, it is unsound: For example, it will only recognise
IO happening when the
case matches on
(# State# RealWorld, a #), not
State# RealWorld (an action ultimately calling
(# State# RealWorld, Int#, Int#, Int# #) (an action ending in
threadStatus#). I imagine that when we have nested CPR, there will be a lot more variants of these unboxed tuples returning a
State# RealWorld token.
We can easily be more precise by extending the
Divergence lattice with
ConOrDiv, signifying that an expression may diverge(, throw an imprecise exception) or converge, but not throw a precise exception. Every converging primop except
raiseIO# would have this new
conDiv. Thus we can see whether an expression may throw a precise exception by checking its inferred demand type.
As for soundness: It turns out that such an analysis, while sound, is too imprecise and would give
topDiv, ironically inferring that it might throw a precise exception (see !2525 (comment 260430)). Thus, to be useful, we have to make the assumption that only
IO code can throw a precise exception (so we disregard
realWorld#). Or, more specifically, any code that constructs a
State RealWorld# token. This analysis is now done by
forcesRealWorld, which is consulted in the new
mayThrowPreciseException check. And whenever we annotate a strictness signature, we try to clear the exception flag, so that the precise exception "taint" is contained as much as possible. Why is that? Consider
let err = error "boom" -- has topDiv in case writeMutVar# var err of s -> x
Is this strict in
x? I'd Yes, very much! But considering that we fail to prove (for the above reasons) that the
err can't throw a precise exception, without our measures to limit taint based on type (which clears
conDiv), the answer produced by the analysis will be No: Although
writeMutVar# in itself doesn't throw a precise exception, it might evaluate its argument, which has
topDiv. This taints the whole IO computation and we come out lazy in