[Git][ghc/ghc][wip/T13380] Preserve precise exceptions in strictness analysis

Sebastian Graf gitlab at gitlab.haskell.org
Thu Mar 26 18:01:30 UTC 2020



Sebastian Graf pushed to branch wip/T13380 at Glasgow Haskell Compiler / GHC


Commits:
ac492646 by Sebastian Graf at 2020-03-26T19:01:17+01:00
Preserve precise exceptions in strictness analysis

Fix #13380 and #17676 by

1. Changing `raiseIO#` to have `topDiv` instead of `botDiv`
2. Give it special treatment in `Simplifier.Util.mkArgInfo`, treating it
   as if it still had `botDiv`, to recover dead code elimination.

This is the first commit of the plan outlined in
https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2525#note_260886.

- - - - -


5 changed files:

- compiler/GHC/Core/Op/Simplify/Utils.hs
- compiler/basicTypes/Demand.hs
- compiler/prelude/primops.txt.pp
- + testsuite/tests/stranal/should_run/T17676.hs
- testsuite/tests/stranal/should_run/all.T


Changes:

=====================================
compiler/GHC/Core/Op/Simplify/Utils.hs
=====================================
@@ -55,6 +55,7 @@ import Name
 import Id
 import IdInfo
 import Var
+import PrimOp
 import Demand
 import GHC.Core.Op.Simplify.Monad
 import GHC.Core.Type     hiding( substTy )
@@ -500,7 +501,9 @@ mkArgInfo env fun rules n_val_args call_cont
                         -- calls to error.  But now we are more careful about
                         -- inlining lone variables, so it's ok
                         -- (see GHC.Core.Op.Simplify.Utils.analyseCont)
-                   if isBotDiv result_info then
+                        -- See Note [Precise exceptions and strictness analysis] in Demand.hs
+                        -- for the special case on raiseIO#
+                   if isBotDiv result_info || isPrimOpId_maybe fun == Just RaiseIOOp then
                         map isStrictDmd demands         -- Finite => result is bottom
                    else
                         map isStrictDmd demands ++ vanilla_stricts


=====================================
compiler/basicTypes/Demand.hs
=====================================
@@ -932,6 +932,53 @@ instance Outputable Divergence where
   ppr Diverges      = char 'b'
   ppr Dunno         = empty
 
+{- Note [Precise vs imprecise exceptions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+An exception is considered to be /precise/ when it is thrown by the 'raiseIO#'
+primop. It follows that all other primops (such as 'raise#' or
+division-by-zero) throw /imprecise/ exceptions. Note that the actual type of
+the exception thrown doesn't have any impact!
+
+GHC undertakes some effort not to apply an optimisation that would mask a
+/precise/ exception with some other source of nontermination, such as genuine
+divergence or an imprecise exception, so that the user can reliably
+intercept the precise exception with a catch handler before and after
+optimisations.
+
+See also the wiki page on precise exceptions:
+https://gitlab.haskell.org/ghc/ghc/-/wikis/exceptions/precise-exceptions
+Section 5 of "Tackling the awkward squad" talks about semantic concerns.
+Imprecise exceptions are actually more interesting than precise ones (which are
+fairly standard) from the perspective of semantics. See the paper "A Semantics
+for Imprecise Exceptions" for more details.
+
+Note [Precise exceptions and strictness analysis]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+raiseIO# raises a *precise* exception, in contrast to raise# which
+raise an *imprecise* exception.  See Note [Precise vs imprecise exceptions]
+in XXXX.
+
+Unlike raise# (which returns botDiv), we want raiseIO# to return topDiv.
+Here's why. Consider this example from #13380 (similarly #17676):
+    f x y | x>0       = raiseIO Exc
+          | y>0       = return 1
+          | otherwise = return 2
+Is 'f' strict in 'y'? One might be tempted to say yes! But that plays fast and
+loose with the precise exception; after optimisation, (f 42 (error "boom"))
+turns from throwing the precise Exc to throwing the imprecise user error
+"boom". So, the defaultDmd of raiseIO# should be lazy (topDmd), which can be
+achieved by giving it divergence topDiv.
+
+But if it returns topDiv, the simplifier will fail to discard raiseIO#'s
+continuation in
+   case raiseIO# x s of { (# s', r #) -> <BIG> }
+which we'd like to optimise to
+   raiseIO# x s
+Temporary hack solution: special treatment for raiseIO# in
+Simplifier.Utils.mkArgInfo.
+-}
+
+
 ------------------------------------------------------------------------
 -- Combined demand result                                             --
 ------------------------------------------------------------------------


=====================================
compiler/prelude/primops.txt.pp
=====================================
@@ -2644,27 +2644,12 @@ primop  RaiseOverflowOp "raiseOverflow#" GenPrimOp
    out_of_line = True
    has_side_effects = True
 
--- raiseIO# needs to be a primop, because exceptions in the IO monad
--- must be *precise* - we don't want the strictness analyser turning
--- one kind of bottom into another, as it is allowed to do in pure code.
---
--- But we *do* want to know that it returns bottom after
--- being applied to two arguments, so that this function is strict in y
---     f x y | x>0       = raiseIO blah
---           | y>0       = return 1
---           | otherwise = return 2
---
--- TODO Check that the above notes on @f@ are valid. The function successfully
--- produces an IO exception when compiled without optimization. If we analyze
--- it as strict in @y@, won't we change that behavior under optimization?
--- I thought the rule was that it was okay to replace one valid imprecise
--- exception with another, but not to replace a precise exception with
--- an imprecise one (dfeuer, 2017-03-05).
-
 primop  RaiseIOOp "raiseIO#" GenPrimOp
    a -> State# RealWorld -> (# State# RealWorld, b #)
    with
-   strictness  = { \ _arity -> mkClosedStrictSig [topDmd, topDmd] botDiv }
+   -- See Note [Precise exceptions and strictness analysis] in Demand.hs
+   -- for why we give it topDiv
+   -- strictness  = { \ _arity -> mkClosedStrictSig [topDmd, topDmd] topDiv }
    out_of_line = True
    has_side_effects = True
 


=====================================
testsuite/tests/stranal/should_run/T17676.hs
=====================================
@@ -0,0 +1,18 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+import Data.IORef
+import Control.Exception
+import Control.Monad
+
+data Exc = Exc deriving Show
+
+instance Exception Exc
+
+-- Recursive instead of NOINLINE because of #17673
+f :: Int -> Int -> IO ()
+f 0 x = do
+  let true = sum [0..4] == 10
+  when true $ throwIO Exc
+  x `seq` return ()
+f n x = f (n-1) (x+1)
+
+main = f 1 (error "expensive computation") `catch` \(_ :: Exc) -> return ()


=====================================
testsuite/tests/stranal/should_run/all.T
=====================================
@@ -19,7 +19,8 @@ test('T11076', normal, multimod_compile_and_run, ['T11076.hs', 'T11076_prim.cmm'
 test('T11555a', normal, compile_and_run, [''])
 test('T12368', exit_code(1), compile_and_run, [''])
 test('T12368a', exit_code(1), compile_and_run, [''])
-test('T13380', [expect_broken(13380), exit_code(1)], compile_and_run, [''])
+test('T13380', exit_code(1), compile_and_run, [''])
 test('T14171', [expect_broken(14171), exit_code(1)], compile_and_run, [''])
 test('T14290', normal, compile_and_run, [''])
 test('T14285', normal, multimod_compile_and_run, ['T14285', ''])
+test('T17676', normal, compile_and_run, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ac492646fe3453a78c3f7e5f5e97d9736f973cda

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ac492646fe3453a78c3f7e5f5e97d9736f973cda
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200326/af045d57/attachment-0001.html>


More information about the ghc-commits mailing list