Re: [GHC] #11475: Lint should check for inexhaustive alternatives

21 Jan 2016


      #11475: Lint should check for inexhaustive alternatives
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by simonpj:

@@ -20,2 +20,6 @@
- Right Thing.  Trac #11172 turned out to be a bug in the pruning, which led
- to something like
+ Right Thing.   Yet, lacking such a check, a program can pass Lint and then
+ seg-fault, which is Very Bad.
+
+
+ Trac #11172 is an example.  It turned out to be a bug in the pruning,
+ which led to something like

New description:

 GHC's simplifier prunes inaccessible alternatives from case expressions.
 E.g.
 {{{
 case x of
   A y -> e1
   _   -> ....(case x of
                 A y -> r1
                 B -> r2
                 C -> r3) ...
 }}}
 It'll prune the `A` alternative from the inner case to get
 {{{
 case x of
   A y -> e1
   _   -> ....(case x of
                 B -> r2
                 C -> r3) ...
 }}}
 BUT, there is no independent check from Lint that this pruning does the
 Right Thing.   Yet, lacking such a check, a program can pass Lint and then
 seg-fault, which is Very Bad.


 Trac #11172 is an example.  It turned out to be a bug in the pruning,
 which led to something like
 {{{
 case x of
   Left y -> e1
 }}}
 but in fact `x` ended up being bound to `(Right v)` for some value `v`.
 But because there is only a single alternative left, GHC does not test the
 tag, but instead goes ahead and accesses it the `Right` value as if it was
 a `Left` value. And because of pointer-tagging, it'll assume the wrong tag
 on the pointer, and very soon you are in seg-fault land.

 So this ticket is to suggest: make Core Lint do it's best to check that
 all cases are in fact exhaustive.  There are two ways in which we prune
 cases:
  * Enclosing pattern matches (as above)
  * GADT pattern matches may be exhaustive even when they don't mention all
 constructors.

 For the latter, it's impossible for Lint to reproduce all the reasoning of
 the type checker, but I bet that in 99.5% of the cases the existing
 function `dataConCantMatch` will do the job.

 So if Lit
  * Maintains an environment saying what each variable can't match (as the
 simplifier does)
  * Does a simple-minded `dataConCantMatch` test based on the typ of the
 scrutinee
 I think we'd be a long way forward.  It's possible that a valid program
 could trigger a Lint report, but let's see.

 Any volunteers?

--

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11475#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

    