#5426: Clever programs violate GHC assumptions about representation
---------------------------------+------------------------------------------
Reporter: batterseapower | Owner:
Type: bug | Status: new
Priority: high | Milestone: 7.6.1
Component: Compiler | Version: 7.2.1
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: GHC accepts invalid program
---------------------------------+------------------------------------------
Old description:
> Consider this program:
>
> {{{
> $ cat Blargh.hs
> {-# LANGUAGE KindSignatures, RankNTypes, GADTs, MagicHash #-}
> module Main where
>
> import GHC.Exts
> import GHC.IO
>
> {-# NOINLINE foo #-}
> foo :: forall (f :: * -> !). f RealWorld -> Int -> Int
> foo x y = case x of _ -> y + 10
>
> main :: IO ()
> main = IO $ \s -> case print (foo s 10) of IO f -> f s
> }}}
>
> When compiled run it produces this result:
>
> {{{
> $ ./Blargh
> -5116089176676103435
> }}}
>
> It can easily be modified to provoke a segfault instead.
>
> The problem here is that when generating the code for foo,
> Type.typePrimRep assumes that any TyApp has Ptr representation and so
> expects that argument to be a word wide.
>
> Unfortunately, the State# TyCon has kind (* -> #) and is represented by
> VoidRep, so we can make the call site of foo believe that the argument to
> foo is of width 0... havoc ensues.
>
> One way to fix this is to encode representation in the kind hierarchy, so
> we have WordRep, IntRep, VoidRep all subkinds of #. Then we can know the
> representation of types without relying on deconstructing them.
New description:
Consider this program:
{{{
$ cat Blargh.hs
{-# LANGUAGE KindSignatures, RankNTypes, GADTs, MagicHash #-}
module Main where
import GHC.Exts
import GHC.IO
{-# NOINLINE foo #-}
foo :: forall (f :: * -> !). f RealWorld -> Int -> Int
foo x y = case x of _ -> y + 10
main :: IO ()
main = IO $ \s -> case print (foo s 10) of IO f -> f s
}}}
When compiled run it produces this result:
{{{
$ ./Blargh
-5116089176676103435
}}}
It can easily be modified to provoke a segfault instead.
The problem here is that when generating the code for foo,
`Type.typePrimRep` assumes that any `TyApp` has `Ptr` representation and
so expects that argument to be a word wide.
Unfortunately, the `State# TyCon` has kind `(* -> #)` and is represented
by `VoidRep`, so we can make the call site of foo believe that the
argument to foo is of width 0... havoc ensues.
One way to fix this is to encode representation in the kind hierarchy, so
we have `WordRep`, `IntRep`, `VoidRep` all subkinds of #. Then we can know
the representation of types without relying on deconstructing them.
--
Comment(by simonpj):
This is indeed terrible. It arises becaues the comment in
`Type.typePrimRep` doesn't hold:
{{{
-- Types of the form 'f a' must be of kind *, not *#, so
-- we are guaranteed that they are represented by pointers.
-- The reason is that f must have kind *->*, not *->*#, because
-- (we claim) there is no way to constrain f's kind any other
-- way.
}}}
The reason it can go wrong is because used to admit kinds like `* -> !`;
and even used to parse them!
No more. In the upcoming `PolyKinds` stuff, we've simplified kinds a bit
so there are never any of those nasty `!` or `#` things under an arrow.
(Except in the kinds of some primitive type constructors like `State#` or
`MutVar#`, and we insist that they are always saturated.) In short, '''we
can't abstract over kinds involving the wierd constants !, #''', and
that's what you were doing here.
I'll assign this to Pedro to close after doing these things:
* Remove the "!" case from the parser for kinds. Was
{{{
akind :: { Located Kind }
: '*' { L1 liftedTypeKind }
| '!' { L1 unliftedTypeKind }
| CONID {% checkKindName (L1 (getCONID $1)) }
| '(' kind ')' { LL (unLoc $2) }
}}}
It's probably different now anyway.
* When kind-checking types, make sure that in a `TyConApp`, a tycon
returning an `unliftedKind` is always saturated. All these tycons are
`WiredIn` so it should be a cheap and easy test.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5426#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
