liquid runs out of memory

UnkindPartition commented 10 years ago

When I run liquid on this file https://gist.github.com/22ff7db5341036478a8f, it runs for about a minute and runs out of memory:

% liquid mark1.hs 
LiquidHaskell © Copyright 2009-14 Regents of the University of California. All Rights Reserved.

**** DONE:  Extracted Core using GHC *******************************************

liquid: out of memory (requested 1048576 bytes)

(This is the version from master)

ranjitjhala commented 10 years ago

Hmm, thats surprising. Thanks for letting us know!

ranjitjhala commented 10 years ago

@nikivazou I think I've seen this before -- I think it has to do with the auto-generated SYB instances?

gridaphobe commented 10 years ago

@ranjitjhala as I suspected, this seems to be caused by our expansion of the pattern matches to fill in the default case. If I run liquid with --no-case-expand it makes it to the fixpoint stage, but the story doesn't end there..

Somehow the following line ends up in the .fq file

bind 9048 VV#62967 : {VV#62967 : int | [(VV#62967 = 10686306464474265204)]}

which causes fixpoint to crash with what looks like an exceeded-max-bound error

safe_int_of_string crashes on: 10686306464474265204 (error = Failure("int_of_string"))Fatal error: exception Failure("int_of_string")

That exact number doesn't appear in the Core anywhere, but there is this snippet..

       lq_anf__d3Jx =
         Data.Typeable.Internal.mkTyCon
           (__word 3419515456169262827)
           (__word 5927002282174334353)
           lq_anf__d3Ju
           lq_anf__d3Jv
           lq_anf__d3Jw } in

ranjitjhala commented 10 years ago

Ah yes, can you add this to tests/todo ? We should use the support for literals in fix point to solve this for one and for all...

On Sep 3, 2014, at 1:13 AM, Eric Seidel notifications@github.com wrote:

@ranjitjhala as I suspected, this seems to be caused by our expansion of the pattern matches to fill in the default case. If I run liquid with --no-case-expand it makes it to the fixpoint stage, but the story doesn't end there..

Somehow the following line ends up in the .fq file

bind 9048 VV#62967 : {VV#62967 : int | [(VV#62967 = 10686306464474265204)]} which causes fixpoint to crash with what looks like an exceeded-max-bound error

safe_int_of_string crashes on: 10686306464474265204 (error = Failure("int_of_string"))Fatal error: exception Failure("int_of_string") That exact number doesn't appear in the Core anywhere, but there is this snippet..
   lq_anf__d3Jx =
     Data.Typeable.Internal.mkTyCon
       (__word 3419515456169262827)
       (__word 5927002282174334353)
       lq_anf__d3Ju
       lq_anf__d3Jv
       lq_anf__d3Jw } in
— Reply to this email directly or view it on GitHub.

nikivazou commented 10 years ago

Thanks for the report @feuerbach! If you want to give it another try you can use two liquid flags that suppress the bug (we will provide a proper solution soon...).

I added some basic annotations and the flags at your file here: tests/todo/Machine.hs

Now it only proves that your recursive call at line 95 actually decreases the termination metric elen e.

About the flags

flag no-case-expand LH automatically expands the case expressions to all the possible cases to get more precise info for your code. It seems that this expansion lead to huge code that made liquid run out of memory. I wouldn't expect that because there are not so many data constructors, so we should take a closer look at the code generated by case expansion...
flag trust-internals With this flag LH gives true types to the binders automatically generated by ghc (like dictionaries and class methods) without looking at the code that generates them.

We need this flag for two reasons First, as @ranjitjhala and @gridaphobe said the auto-generated SYB instances use introduces a very big number that cannot be handled by ocaml.

Another reason is that LH decides that the Typeable dictionary created inside subst has type false, so it trivially verifies subst but without really checking anything. This is a serious issue that we need to address, presumably by giving true type to all dictionaries...

ranjitjhala commented 10 years ago

By "true type" you mean "non refined" or "trivially refined" type, correct?

On Sep 5, 2014, at 6:10 AM, Niki Vazou notifications@github.com wrote:

Thanks for the report @feuerbach! If you want to give it another try you can use two liquid flags that suppress the bug (we will provide a proper solution soon...).

I added some basic annotations and the flags at your file here: tests/todo/Machine.hs

Now it only proves that your recursive call at line 95 actually decreases the termination metric elen e.

About the flags

flag no-case-expand LH automatically expands the case expressions to all the possible cases to get more precise info for your code. It seems that this expansion lead to huge code that made liquid run out of memory. I wouldn't expect that because there are not so many data constructors, so we should take a closer look at the code generated by case expansion...

flag trust-internals With this flag LH gives true types to the binders automatically generated by ghc (like dictionaries and class methods) without looking at the code that generates them.

We need this flag for two reasons First, as @ranjitjhala and @gridaphobe said the auto-generated SYB instances use introduces a very big number that cannot be handled by ocaml.

Another reason is that LH decides that the Typeable dictionary created inside subst has type false, so it trivially verifies subst but without really checking anything. This is a serious issue that we need to address, presumably by giving true type to all dictionaries...

— Reply to this email directly or view it on GitHub.

gridaphobe commented 10 years ago

Furthermore, do you mean the dictionary DataCons or the dictionaries themselves?

We can't give the DataCons a non-refined type because that's how we verify the class instances.

On Friday, September 5, 2014, Ranjit Jhala notifications@github.com wrote:

By "true type" you mean "non refined" or "trivially refined" type, correct?

On Sep 5, 2014, at 6:10 AM, Niki Vazou <notifications@github.com javascript:_e(%7B%7D,'cvml','notifications@github.com');> wrote:

Thanks for the report @feuerbach! If you want to give it another try you can use two liquid flags that suppress the bug (we will provide a proper solution soon...).

I added some basic annotations and the flags at your file here: tests/todo/Machine.hs

Now it only proves that your recursive call at line 95 actually decreases the termination metric elen e.

About the flags

flag no-case-expand LH automatically expands the case expressions to all the possible cases to get more precise info for your code. It seems that this expansion lead to huge code that made liquid run out of memory. I wouldn't expect that because there are not so many data constructors, so we should take a closer look at the code generated by case expansion...

flag trust-internals With this flag LH gives true types to the binders automatically generated by ghc (like dictionaries and class methods) without looking at the code that generates them.

We need this flag for two reasons First, as @ranjitjhala and @gridaphobe said the auto-generated SYB instances use introduces a very big number that cannot be handled by ocaml.

Another reason is that LH decides that the Typeable dictionary created inside subst has type false, so it trivially verifies subst but without really checking anything. This is a serious issue that we need to address, presumably by giving true type to all dictionaries...

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/237#issuecomment-54609624 .

Sent from Gmail Mobile

nikivazou commented 10 years ago

Correct @ranjitjhala !

@gridaphobe I mean the dictionary variables that ghc builds, eg, let $dData :: Data.Data.Data a ) = ... But giving them trivial or non-refined types we indeed cannot verify type classes. This is why I added a flag instead of making it the default behavior. We need to find a solution that addresses both these issues...

ranjitjhala commented 10 years ago

Well, this is not so bad for now, because this is only for derived instances right? Or is it all dictionary instances? (If the latter, then its more severe of course...)

On Fri, Sep 5, 2014 at 8:07 AM, Niki Vazou notifications@github.com wrote:

Correct @ranjitjhala https://github.com/ranjitjhala !

@gridaphobe https://github.com/gridaphobe I mean the dictionary variables that ghc builds, eg, let $dData :: Data.Data.Data a ) = ... But giving them trivial or non-refined types we indeed cannot verify type classes. This is why I added a flag instead of making it the default behavior. We need to find a solution that addresses both these issues...

Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/237#issuecomment-54616903 .

Ranjit.

nikivazou commented 10 years ago

The latter... In Roman's example there is this function subst that inside the body creates a dictionary that does not get any constraints.... So, without the flag subst's body is unsoundly decided SAFE.

gridaphobe commented 10 years ago

Is the dictionary not used anywhere?

On Friday, September 5, 2014, Niki Vazou notifications@github.com wrote:

The latter... In Roman's example there is this function subst that inside the body creates a dictionary that does not get any constraints.... So, without the flag subst's body is unsoundly decided SAFE.

— Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/237#issuecomment-54617659 .

Sent from Gmail Mobile

ucsd-progsys / liquidhaskell

liquid runs out of memory #237