Opened 10 years ago

Last modified 3 years ago

#1171 new bug

GHC doesn't respect the imprecise exceptions semantics

Reported by: neil Owned by:
Priority: low Milestone:
Component: Compiler Version: 6.6
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: cg059
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Yhc bug 122 appears to be a GHC bug: http://code.google.com/p/yhc/issues/detail?id=122 , discussed here: http://thread.gmane.org/gmane.comp.lang.haskell.yhc/720

To reproduce: Download and install Yhc two separate times, once doing "scons" to build, once doing "scons type=release". Follow the steps outlined in the above bug report with the standard version, and it gives the correct behaviour. Try again with the release version and it gives the wrong behaviour. GHC 6.4.2 works fine. The difference between the two is that type=release builds with -O, normal doesn't.

Changing the code slightly, by introducing "obvious" assert statements in Package.hs makes the bug go away. Creating reduced tests cases didn't get very far...

This has been replicated on Mac and Windows with GHC 6.6. If you have any further questions about the code then feel free to email me or the Yhc list. Marking as severity=major because silently doing something different is about as bad as they come.

Thanks to Thorkil for doing the detective work to track this down as far as GHC.

Attachments (1)

1171Material.tar.gz (803 bytes) - added by thorkilnaur 10 years ago.
Stand-alone material to illustrate the problem reported in ticket #1171

Download all attachments as: .zip

Change History (20)

comment:1 Changed 10 years ago by thorkilnaur

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.

Changed 10 years ago by thorkilnaur

Attachment: 1171Material.tar.gz added

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

comment:2 Changed 10 years ago by thorkilnaur

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.

comment:3 Changed 10 years ago by simonmar

Milestone: 6.6.1
Priority: normalhigh

wrong-code bugs are a high priority.

comment:4 Changed 10 years ago by igloo

Owner: set to igloo
Priority: highnormal

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

comment:5 Changed 10 years ago by igloo

Owner: igloo deleted
Test Case: cg059

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.

comment:6 Changed 10 years ago by simonmar

Resolution: invalid
Status: newclosed

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.

comment:7 Changed 10 years ago by malcolm.wallace@…

Wow, you really claim that if the program calls 'error' at all, then _any_ call to error will do!? If my program has an ArithmeticOverflow, then it is OK to report DivideByZero instead?

The semantics of H'98 clearly say that pattern-matching is left-to-right, top-to-bottom, so

case [] of

[] -> error "OK" _ -> error "broken"

really _must_ give the error "OK", not the error "broken".

See H'98, Section 3.17.3, Figure 3.1, case (b).

comment:8 Changed 10 years ago by Stefan O'Rear <stefanor@…>

Such behavior would probably be excusable, indeed desirable in a Haskell 98 compiler. But GHC is not just a Haskell 98 compiler - it also claims to follow the document "A Semantics for Imprecise Exceptions". And that document, if I recall correctly, does not specify a single _|_ but rather allows expressions to evaluate to a set of expressions, and changing the set of expressions returned is not a semantically correct compiler. Does yhc use Control.Exception.catch? If so, I would call this behavior Incorrect.

comment:9 Changed 10 years ago by simonpj

Milestone: 6.6.1_|_
Priority: normallow
Resolution: invalid
severity: majornormal
Status: closedreopened

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

comment:10 Changed 10 years ago by neil

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

comment:11 Changed 10 years ago by simonmar

Summary: GHC generates incorrect code with -O for Haskell 98 programGHC 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...

comment:12 Changed 10 years ago by igloo

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.

comment:13 Changed 10 years ago by Isaac Dupree

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."

comment:14 Changed 9 years ago by simonmar

Architecture: MultipleUnknown/Multiple

comment:15 Changed 9 years ago by simonmar

Operating System: MultipleUnknown/Multiple

comment:16 Changed 4 years ago by morabbin

Type of failure: None/Unknown

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

comment:17 in reply to:  16 Changed 4 years ago by simonmar

Replying to 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).

comment:18 Changed 4 years ago by simonpj

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.

comment:19 Changed 3 years ago by Ian Lynagh <igloo@…>

In 168c6b2a6559a30f1500dcbcf4d3b654c4897d7d/ghc:

Add testcase from trac #1171 as cg059
Note: See TracTickets for help on using tickets.