Skip to content

WIP: DmdAnal: Reflect precise exceptions in demand types

Sebastian Graf requested to merge wip/dmdanal-precise-exn into master

This is part two of the "fixing precise exception" plan in https://gitlab.haskell.org/ghc/ghc/wikis/fixing-precise-exceptions and, in combination with !2956 (closed), supercedes !2525 (closed).

In #13380 (closed) and #17676 (closed) we saw that we didn't preserve precise exception semantics in demand analysis. We fixed that with minimal changes in !2956 (closed), but that is terribly unprincipled.

That unprincipledness results in a loss of precision, which is tracked by these new test cases:

  • T13380b: Regression in dead code elimination, because !2956 (closed) was too syntactic about raiseIO#
  • T13380c: No need to apply the "IO hack" when the IO action may not throw a precise exception
  • T13380d: Demonstrating unsoundness of the "IO hack" when resorting to manual state token threading and direct use of primops. More details below.

The "IO hack" (which is a fallback to preserve precise exceptions semantics and thus soundness, rather than some smart thing that increases precision) is quite a misnomer and is called mayThrowPreciseException now.

Also there is a slight chance that the IO hack was unsound before, because it assumes that precise exceptions can only be thrown from a case scrutinee of type (# State# RealWorld, _ #). I couldn't come up with a program using the IO abstraction that violates this assumption. But it's easy to do so via manual state token threading and direct use of primops, see T13380d. Also similar code might be generated by Nested CPR in the (hopefully not too) distant future.

Hence, we now have a more careful test in forcesRealWorld that passes T13380d.

As for how we fixed these wrinkles: We augmented the Divergence lattice to a diamond with two new elements forming the middle layer:

  • ExnOrDiv: Means either Diverges (, throws an imprecise exception) or throws a precise exception.
  • ConOrDiv: Means either Diverges (, throws an imprecise exception) or converges.

See the wiki page for more implementational details: https://gitlab.haskell.org/ghc/ghc/wikis/fixing-precise-exceptions#replacing-hacks-by-principled-program-analyses

Merge request reports