Segfault in a CoreLinted program (and a GHC-generated Core question)

[Richard Eisenberg]

Phew. This was an alarming email! If a core-linted program segfaults, there's either a bug in CoreLint or a bug in the theory behind GHC. If it's the latter, someone will have an interesting paper to write... :)

Richard

On Oct 26, 2015, at 7:57 PM, Ömer Sinan Ağacan <omeragacan at gmail.com> wrote:

> OK, thanks to people at IRC channel(especially @rwbarton) I realized
> that my lint calls were not actually running, simply because I wasn't
> using -dcore-lint.. I didn't know such a flag exists, and even with
> the absence of the flag I'd expect a core lint would work, because I'm
> explicitly calling the lint function without checking any flags!
> 
> CoreLint is now giving me really awesome diagnostics! Sorry for the noise..
> 
> (I'll try to document linter functions or CoreLint module to let the
> user know he/she needs this flag!)
> 
> 2015-10-26 13:43 GMT-04:00 Simon Peyton Jones <simonpj at microsoft.com>:
>> |  So my questions are: Am I right in assuming that CoreLint accepted programs
>> |  should not segfault?
>> 
>> Yes.  Modulo unsafeCoerce, and FFI calls.
>> 
>> | What about internal invariants? Should CoreLint check
>> |  for those? Is there any pass that checks for invariants and prints helpful
>> |  messages in case of a invariant invalidation?
>> 
>> Yes; they are documented in CoreSyn, which the data type, and Lint checks them.
>> 
>> |  As an attempt at debugging the code generated by my plugin, I wrote the
>> |  function that is supposed to be generated by my Core pass in Haskell and
>> |  compiled with GHC. Generated Core is mostly the same, except at one point it
>> |  has an extra lambda directly applied to a void#, something like ((\_ -> ...)
>> |  void#). Where can I learn more about why GHC is doing that?
>> 
>> Show me the code!
>> 
>> Instead of generating
>> 
>>    x :: Int# = <some expression that might fail>
>> 
>> GHC sometimes generates
>> 
>>    x :: Void# -> Int# = \_ - <some expression that might fail>
>> 
>> and then calls (x void#), to make any div-zero failures happen at the right place.
>> 
>> I'm not sure if that is what you are seeing, but we can work it out when you give more detail.
>> 
>> Simon
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs