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.
Problem
#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.
Here we describe the measures taken to fix that ticket (along with #148 (closed), #1592 (closed) and #17676 (closed)).
defaultFvDmd
of raiseIO#
lazy to preserve precise exceptions, hackily (Step 1)
Solution: Make This was implemented in !2956 (closed).
raiseIO#
used to have a Divergence
of botDiv
. This means that it is strict in any free variable (such as y
) and easily fixed by giving it topDiv
.
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.
So all that really needs to be done to fix #17676 (closed) and #13380 (closed) is
- Change
raiseIO#
to havetopDiv
- Give it special treatment in
mkArgInfo
, treating it as if it hadbotDiv
.
Replacing hacks by principled program analyses (Step 2)
This was fully implemented in !3014 (closed). But it ended in a complicated mess, so we only implemented Step 2.1 in !3171 (closed).
raiseIO#
with isDeadEndDiv
, introducing ExnOrDiv
(Step 2.1)
Dead code elimination for 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 ExnOrDiv
to Divergence
, denoting that evaluation will diverge(, throw an imprecise exception) or throw a precise exception, but surely never converge. The defaultFvDmd
of 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 isBotDiv
to isDeadEndDiv
, similarly all functions that use it and can delete the special case for raiseIO#
in SimplUtils.mkArgInfo
.
The only analysis that I recognise plays a little fast and loose with exnDiv
vs. botDiv
probably is CoreArity
(which will turn exnDiv
into botDiv
in exprBotStrictness_maybe
), but I guess we'll fix that when it has bitten us.
ConOrDiv
(Step 2.2)
Turn the "IO hack" into the proper analysis it should have been, introducing 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.
(In hindsight, this improvement is quite independent of #17676 (closed) and #13380 (closed), but similarly revolves around precise exceptions)
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 writeMutVar#
) or (# 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 error
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 unsafePerformIO
and 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 err
to 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 x
.