GHC doesn't respect the imprecise exceptions semantics

changed weight to 5

A stand-alone file (1171Material.tar.gz) that illustrates this problem on a PPC Mac OS X 10.4 is attached. It has been produced by reducing the Yhc code involved in the original report. Here is a session that uses this file:

Thorkil-Naurs-Computer:~/tn/GHC/trac/1171 thorkilnaur$ mkdir verify
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171 thorkilnaur$ cd verify
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/verify thorkilnaur$ cp ../1171Material.tar.gz .
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/verify thorkilnaur$ gunzip 1171Material.tar.gz
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/verify thorkilnaur$ tar xvf 1171Material.tar
1171Material/
1171Material/ghc.sh
1171Material/Package.hs
1171Material/T3.hs
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/verify thorkilnaur$ cd 1171Material
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/verify/1171Material thorkilnaur$ ls
Package.hs      T3.hs           ghc.sh
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/verify/1171Material thorkilnaur$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 6.6.20070220
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/verify/1171Material thorkilnaur$ cat ghc.sh
ghc --make T3 -o T3 -O          
./T3
rm *.o
ghc --make T3 -o T3
./T3
rm *.o
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/verify/1171Material thorkilnaur$ sh ghc.sh
[1 of 2] Compiling Package          ( Package.hs, Package.o )
[2 of 2] Compiling Main             ( T3.hs, T3.o )
Linking T3 ...
T3: 2007-Feb-25 01.57
T3: Empty as++bs
[1 of 2] Compiling Package          ( Package.hs, Package.o )
[2 of 2] Compiling Main             ( T3.hs, T3.o )
Linking T3 ...
T3: 2007-Feb-25 01.57
T3: Error: File not found
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/verify/1171Material thorkilnaur$

In this session, T3+Package is compiled and executed twice, first with -O, then without -O. And, as can be observed, the results are different.

In the wrong case - the one where -O is used - the erroneous result apparently comes about by selecting the wrong alternative in the case in Package.hs:

           case (local,res) of
                ([x], _) -> return x
                (_, [x]) -> return x
                ([], []) -> raiseError $ ErrorFileNone
                (as, bs) -> if as++bs == [] then error "Empty as++bs" else raiseError $ ErrorFileMany file

As can be seen from the output produced, in spite of as+bs being == [], the last alternative is selected when the code is compiled with -O.

Attached file 1171Material.tar.gz (download).

Stand-alone material to illustrate the problem reported in ticket #1171

With a recently built ghc HEAD, I cannot reproduce the problem:

Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/work/1171Material thorkilnaur$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 6.7.20070223
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/work/1171Material thorkilnaur$ sh ghc.sh
[1 of 2] Compiling Package          ( Package.hs, Package.o )
[2 of 2] Compiling Main             ( T3.hs, T3.o )
Linking T3 ...
T3: 2007-Feb-25 01.57
T3: Error: File not found
[1 of 2] Compiling Package          ( Package.hs, Package.o )
[2 of 2] Compiling Main             ( T3.hs, T3.o )
Linking T3 ...
T3: 2007-Feb-25 01.57
T3: Error: File not found
Thorkil-Naurs-Computer:~/tn/GHC/trac/1171/work/1171Material thorkilnaur$

As we can observe, the same (correct) output is produced, both in the -O and the non -O case for this ghc.

changed milestone to %6.6.1

changed weight to 7

wrong-code bugs are a high priority.

Trac metadata

Trac field	Value
Priority	normal → high

changed weight to 5

assigned to @trac-igloo

Great testcase, thanks Thorkil.

The bug also happens on Linux/amd64 with 6.6, but the 6.6 branch looks OK.

I'll leave the bug open for now as a reminder to me to put the testcase in the testsuite.

Thanks

Ian

Trac metadata

Trac field	Value
Priority	high → normal

mentioned in commit 168c6b2a

unassigned @trac-igloo

test added as cg059 in HEAD and 6.6 branches. Still leaving the bug report open for now as we may wish to chase down the actual problem so we can confirm it really has been fixed, rather than just no longer being tickled in this case.

Trac metadata

Trac field	Value
Test case	→ cg059

closed

Not a bug!!!!

Let's look at the code:

           case (local,res) of
                ([x], _) -> return ()
                (_, [x]) -> return ()
                ([], []) -> raiseError $ ErrorFileNone
                (as, bs) -> if as++bs == [] then error "Empty as++bs" else raiseError $ ErrorFileMany file

The last two branches are both _|_. If the value of an expression is definitely _|_, then any _|_ will do: in this case you get the "Empty as++bs" error instead of the one you were expecting. To fix the program you need to use ioError instead of error.

The way this works is like this: after the first two alternatives have been eliminated, we're left with

           case (local,res) of
                ([], []) -> raiseError $ ErrorFileNone
                (as, bs) -> if as++bs == [] then error "Empty as++bs" else raiseError $ ErrorFileMany file

which is semantically equivalent to _|_, and GHC can detect that. However, we don't gratuitously replace it with undefined, of course; in fact GHC compiles this expression:

       let z = if as++bs == [] then error "Empty as++bs"
                               else raiseError $ ErrorFileMany file
       in z `seq`
           case (local,res) of
                ([], []) -> raiseError $ ErrorFileNone
                (as, bs) -> z

It's safe to evaluate z eagerly, because the whole expression is known to be _|_. So there you go.

I don't know whether it's possible to modify the simplifier to get a more expected result here; I suspect not without sacrificing some performance.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

reopened

removed milestone

changed weight to 3

Indeed our paper http://research.microsoft.com/~simonpj/Papers/imprecise-exn.htm is good background reading for this.

Consider

  f :: Bool -> Int -> Int
  f True x = error "urk"
  f False x = x

We'd probably agree that f is strict. And hence we can use call-by-value. But look at the consequences:

  g x = f x (error "flop")

Since f is strict, we'll use call-by-value, and hence g will (always) craxh with "error: flop". But is that right? After all, if we simply inline f we get

  g x = case x of
           True -> error "urk"
           False -> error "flop"

which is very similar to your program. (In your case GHC has made the reverse transformation, lifting one of your case branches out as a shared expression.)

So by doing strictness analysis, GHC is increasing the set of exceptions (see the paper) in the denotation of the program. That's a bit confusing, I grant. It's easily stopped, too, by stopping GHC treating error like bottom; but that would make many functions less strict. It'd be interesting to measure the performance impact of this.

So I'm re-opening the bug because I think it's a legitimate and interesting question what the "right" behaviour should be. I'd like to add a flag to GHC to give the more conservative behaviour. It's the first time this has happened; interesting!

Simon

Trac metadata

Trac field	Value
Priority	normal → low
Resolution	ResolvedInvalid → Unresolved

For reference, Yhc has now been patched to do |unsafePerformIO $ putStrLn "msg" >> exit|, which should fix this behaviour.

Perhaps the problem is that there are two different uses of error, one is as an internal assertion - typically introduced by an incomplete pattern. The other is the programmer explicitly stating that the program should stop now and give the user a message. The Safe [1] library provides an "abort" function to handle the latter, partly so automated checkers can tell the difference between good and bad calls to error.

[1] http://www-users.cs.york.ac.uk/~ndm/projects/safe/Safe.html#v%3Aabort

changed title from GHC generates incorrect code with -O for Haskell 98 program to GHC doesn't respect the imprecise exceptions semantics

Yes, I though we were sticking to the imprecise exception semantics, but in fact we're straying outside a bit. I've modified the ticket subject.

In response to Neil: why use unsafePerformIO rather than IO exceptions here? I think you're asking for more trouble...

The below is from e-mail and IRC conversations that happened in parallel with this bug report. I've editted things slightly to make them flow better, but hopefully haven't changed any important meanings.

I said:``

In http://research.microsoft.com/~simonpj/Papers/imprecise-exn.htm I think you claim in section 4.3, in the rationale for the Bad case, that if we have {{{ f x = case x of True -> error "A" False -> error "B" }}} then the call {{{ f (error "X") }}} is allowed to raise B, as this permits transformations like {{{ f' x = let b = error "B" in b seq case x of True -> error "A" False -> b }}} which in turn is justified because the case expression is strict in {{{ error "B" }}} (as well as every other expression).

However, the Ok case tells me that if I call {{{ f True }}} then I can get the errors raised by the {{{ True -> error "A" }}} branch only. Thus it must raise A. But with the above transformation f' raises B.

I also think that this behaviour is very confusing to users; it makes sense that {{{ error "A" + error "B" }}} needs to evaluate both values, so throwing either exception is reasonable, but in {{{ f True }}} it is "obvious" that A is raised and B is not!

Traditionally, we would say that e is strict in x if {{{ x = | => e = | }}} However, with the set-based imprecise exceptions, in which we distinguish between different bottoms, it seems to me that a better definition would be that e is strict in x if {{{ x = Bad xs => e = Bad ys and xs \subseteq ys }}}

Thus, for example, a case can throw an exception if either the scrutinee can or /all/ the branches can, i.e. in the Bad case in 4.3 we take the big intersection rather than big union.

So we wouldn't be allowed to pull {{{ error "B" }}} out of the above case, but we would still be able to translate {{{ case x of True -> y False -> y }}} into {{{ y seq case x of True -> y False -> y }}}

I am also unconvinced by a non-terminating program being allowed to throw anything it likes. It seems much nicer to permit it only to either not terminate or to throw a special exception, here-on written N.

I haven't written a denotational semantics or anything, so perhaps this would all unravel if I tried, but here are some example definitions followed by what exceptions I think various expressions ought to be able to throw; are there any obvious nasty corners I have left unexplored?:

{{{ f x = case x of True -> error "A" False -> error "B"

g x = case x of True -> error "C" False -> error "C"

h () () = ()

i = i

j = error "D" + j

f True A f (error "E") E g True C g (error "F") C or F h (error "G") (error "H") G or H i N or non-termination j D, N or non-termination }}}

I also haven't looked into the performance implications, although personally I'd prefer a semantics that is more intuitive along with a few more bang patterns sprinkled around.

Simon PJ replied:``

I think you are basically right here. Another way to say it is this. In 4.5 we claim that GHC's transformations can reduce the set of possible exceptions from a term, but not increase it. But the (current) strictness analysis transformation increases it. I agree that is undesirable.

As I say on the Trac, we could change this at the cost of making fewer functions strict. I can tell anyone how to do this, if you want. It would be good to measure the performance impact of doing so.

Simon M has a memory that there is some problem, possibly related to monotonicity, with only allowing non-terminating programs to either not terminate or throw a special non-termination error, rather than allowing them to behave like any bottom they wish as the imprecise exceptions paper allows them to. However, he can't remember what the problem actually is; if anyone can then it would be good to have it documented.

Regarding Simon PJ__'s earlier comment {{{ It's easily stopped, too, by stopping GHC treating error like bottom; but that would make many functions less strict. It'd be interesting to measure the performance impact of this. }}} __Simon M replied:

It would be a shame if error wasn't treated as |, because that would lose the opportunity to transform

{{{ Case error "foo" of alts ===> error "foo" }}}

wouldn't it? This is only dead code elimination of course.

and Simon PJ followed up with:``

You are right that the strictness of an Id would have to distinguish:

normal
diverges (bottom)
crashes (calls error) Currently it does not. Changing the strictness analyser to make 'error' look like 'normal' rather than 'diverges' would indeed have the effect of making GHC not realise that (error "x") was a case scrutinee that could be simplified.

So yes, there is a bit more to testing the effect of making 'error' less strict than I was suggesting. Quite doable, but more than a moment's work.

Regarding my strictness test {{{ x = Bad xs => e = Bad ys and xs \subseteq ys }}}

Simon M suggested that an implementation might:

invent a magic exception X only used by the strictness analyser, and treat this as {{{ x = Bad X => e = Bad ys and X elem\ ys }}} All other exceptions (and |) can be mapped to the same thing; all that matters is whether x's exception was raised or not. I imagine you'd need to fiddle around with the strictness analyser's domain.

The sort of case where Simon PJ is worried we will lose performance is

f x [] = error "Can't happen"
f x (y:ys) = ... strict in x ...

where we would no longer be allowed to claim to be strict in x, as

f (error "X") []

should only throw "Can't happen". Debatably it's better to tell the compiler explicitly that you want it to be strict in x with

f !x [] = error "Can't happen"
f !x (y:ys) = ... strict in x ...

anyway, rather than relying on the strictness analyser to figure it out.

Finally, I am not entirely convinced by the semantics of imprecise exceptions as given in the paper; they tend allow too many exceptions to be thrown, possibly under the assumption no compiler would actually transform a program in such a way that the unexpected exceptions actually would be thrown.

For example

(error "A") (error "B")

is permitted to throw B, even though

error "B"

would never be evaluated under non-strict evaluation.

Similarly,

case error "A" of
    True -> error "B"
    False -> 'x'

is allowed to throw B.

Incidentally, I do think it is reasonable for

case error "A" of
    True -> error "B"
    False -> error "B"

to throw B.

Stefan O'Rear happened to write in haskell-cafe a performance reason for allowing non-termination to throw any exception:

"When you see an expression of the form:

f a

you generally want to evaluate a before applying; but if a is |, this will only give the correct result if f a = |. Merely 'guaranteed to evaluate' misses out on some common cases, for instance ifac:

ifac 0 a = a
ifac n a = ifac (n - 1) (a * n)

ifac is guaranteed to either evaluate a, or go into an infinite loop - so it can be found strict, and unboxed. Whereas 'ifac -1 (error "moo")' is an infinite loop, so using a definition based on evaluation misses this case."

Trac metadata

Trac field	Value
Architecture	Multiple → Unknown/Multiple

Trac metadata

Trac field	Value
Operating system	Multiple → Unknown/Multiple

This reads like a misunderstanding of the semantics described in the paper; close as wontfix?

Trac metadata

Trac field	Value
TypeOfFailure	- → OtherFailure

Replying to [ticket:1171#comment:68152 morabbin]:

This reads like a misunderstanding of the semantics described in the paper; close as wontfix?

There really is a mismatch between the semantics in the paper and what GHC implements, so I think it's good to keep the ticket open. Simon knows the full details, but as I understand it we think that the semantics should take into account the reordering that the strictness analyser does (ie. GHC is right, the semantics is wrong).

Here are some more notes about this subject, culled from an exchange betwen Simon M and Simon PJ.

Consider this:

f :: Bool -> (Int,Int) -> Int
f x y = case x of
            True -> error "urk"
	    False -> case y of (a,b) -> a+b

Can we pass y unboxed? Yes, we do so, because we regard bottom (the error branch) as hyperstrict in everything. So we do a w/w split thus

f x y = case y of (a,b) ->
          case a of I# a1 ->
          case b of I# b1 ->
          fw x a1 b1

That means, of course, that (f True (error "a", 3)) would throw (error "a") not (error "urk"). The paper doesn't allow this, but I believe that it's crucial for strictness analysis to work well.

However, if the function unconditionally diverges, it seems stupid to unbox:

f :: (Int,Int) -> a
f x = error "urk"

Here it seems fruitless to do the same w/w/ split as I gave above, even though the semantics justifies it equally. So pragmatically we do NOT do w/w for a hyper-strict demand. Another variant:

f :: (Int,Int) -> a
f (x,y) = error (show x)

main = ...(f (3, error "no no"))...

Similar to the previous example, the (error "no no") is not even used, so it would be very odd indeed to evaluate it before the call to f. See

Note [Unpacking arguments with product and polymorphic demands]

in stranal/WwLib.

Now that there's a testcase verifying that the original YHC code is currently compiled correctly, should I assume that the issue of the compiler not distinguishing different errors in different case branches is fixed? Testing the example given in comment9 shows it still behaves the same way, which seems to imply that it isn't and the YHC code working is a fluke.

added Plow label

mentioned in issue #22179

added demand analysis exceptions labels

marked this issue as related to #19917

GHC doesn't respect the imprecise exceptions semantics

Child items 0

Activity

GHC doesn't respect the imprecise exceptions semantics

Relates to

Activity