Opened 3 years ago

Closed 2 years ago

#5426 closed bug (fixed)

Clever programs violate GHC assumptions about representation

Reported by: batterseapower Owned by: dreixel
Priority: high Milestone: 7.4.1
Component: Compiler Version: 7.2.1
Keywords: Cc: jpm@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description (last modified by simonpj)

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.

Change History (9)

comment:1 Changed 2 years ago by igloo

  • Milestone set to 7.6.1
  • Priority changed from normal to high

comment:2 follow-up: Changed 2 years ago by simonpj

  • Description modified (diff)

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.

comment:3 Changed 2 years ago by simonpj

  • Owner set to dreixel

comment:4 Changed 2 years ago by simonpj

  • Milestone changed from 7.6.1 to 7.4.1

comment:5 in reply to: ↑ 2 Changed 2 years ago by dreixel

  • Cc jpm@… added

Replying to simonpj:

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

The parser doesn't accept ! as a kind anymore, so this part is already done.

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

In core lint?

comment:6 Changed 2 years ago by simonpj@…

commit 0f34f30839c9f382bdeab0335675ce8491361d67

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Tue Dec 13 12:30:40 2011 +0000

    Document the "kind invariant", and check it
    
    See Note [The kind invariant] in TypeRep
    Checked in CoreLint
    All this arises from Trac #5426

 compiler/coreSyn/CoreLint.lhs  |   43 ++-----------------------
 compiler/typecheck/TcMType.lhs |    4 ++
 compiler/types/Type.lhs        |   14 +++++---
 compiler/types/TypeRep.lhs     |   67 ++++++++++++++--------------------------
 4 files changed, 39 insertions(+), 89 deletions(-)

comment:7 Changed 2 years ago by simonpj

  • Difficulty set to Unknown
  • Resolution set to fixed
  • Status changed from new to closed

OK I think that patch does it.

Simon

comment:8 Changed 2 years ago by simonpj

  • Status changed from closed to merge

comment:9 Changed 2 years ago by igloo

  • Status changed from merge to closed
Note: See TracTickets for help on using tickets.