add special rule for string literals

[gridaphobe]

fixes #414

[ranjitjhala]

We're going to regret this later :)

On Fri, Jul 10, 2015 at 9:36 AM, Eric Seidel [email protected]
wrote:

fixes #414 #414

You can view, comment on, or merge this pull request online at:

#415
Commit Summary

• add special rule for string literals

File Changes

• M src/Language/Haskell/Liquid/Constraint/Generate.hs
  https://github.com/ucsd-progsys/liquidhaskell/pull/415/files#diff-0
  (13)
• A tests/pos/StringLit.hs
  https://github.com/ucsd-progsys/liquidhaskell/pull/415/files#diff-1
  (4)

Patch Links:

• https://github.com/ucsd-progsys/liquidhaskell/pull/415.patch
• https://github.com/ucsd-progsys/liquidhaskell/pull/415.diff

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

Ranjit.

[gridaphobe]

I know, we'll never remember to s/len/length here when that time comes..

[ranjitjhala]

Well, the tests will break (hopefully) ...

On Fri, Jul 10, 2015 at 9:56 AM, Eric Seidel [email protected]
wrote:

I know, we'll never remember to s/len/length here when that time comes..

—
Reply to this email directly or view it on GitHub
#415 (comment)
.

Ranjit.

[nikivazou]

Instead of hardcoding that, can't we find a way to encode this information in our include/ files?

[gridaphobe]

@nikivazou do you mean the name "len", or the entire rule? I don't see how we could (easily) encode the rule in a .spec since it needs to reach into the Core AST.

[nikivazou]

It does not have to be encoded in the .spec file.
I am just suggesting that it is better if it is an information that is imported rather than hard-coded in our typing rules.

Btw, strings are treated as constant literals, maybe we can use this information. For example give the literal a type that knows its strlen and then teach unpackCString# to keep this information.

unpackCString# :: x:_ -> {v:[Char] | len v = strlen x}

[gridaphobe]

Yes, I thought about that approach after I replied. But then we're just hardcoding something else in our typing rules, the "strlen" property of Addr#s. So I don't really have a strong opinion.

[nikivazou]

I was thinking that the strlen will come from the environment, at a preprocessing stage, not from the typing rules.

At any case the strlen would be something that the user is not aware of (and does not have access to) and cannot change it (like the plan to change len to length)

[ranjitjhala]

Agree with @gridaphobe here.
Really we need a way of exposing the literal to
the constraint generation. This is just shuffling things around?

On Fri, Jul 10, 2015 at 10:49 AM, Eric Seidel [email protected]
wrote:

Yes, I thought about that approach after I replied. But then we're just
hardcoding something else in our typing rules, the "strlen" property of
Addr#s. So I don't really have a strong opinion.

—
Reply to this email directly or view it on GitHub
#415 (comment)
.

Ranjit.

[nikivazou]

My objection is that currently liquidHaskell does not know what len is. It is defined externally in the include (and it is sound without it). strlen would be a measure defined in liquidHaskell especially for the string literals.

Also, if you want to ignore the string's length information you can just edit the type unpackCString# in the include/. With the current solution you need to modify the typing rules.

[gridaphobe]

That's a fair point, in fact this might even make fixpoint/z3 crash if you removed include/ since len probably wouldn't be defined as a function.

An alternative would be to just wire-in len itself, which would remove the need for the otherwise useless strlen measure. But again, I don't have a strong opinion.

[gridaphobe]

(Wiring-in len would also solve the minor renaming concern)

[nikivazou]

On the other hand, the intention is to have len as the lifted haskell length, so, wiring in len is not such a good idea.

[gridaphobe]

How would that work? The measure-lifting functionality requires the source code, so you couldn't put it in include/GHC/List.spec. I don't think we want to ship our own copy of GHC/List.hs, that would probably cause all kinds of headaches. Furthermore, the measure-lifting is a convenience for users, why does it matter if we use it internally?

(Also, the Foldable/Traversable changes in 7.10 included replacing the specialized length on lists with the class method from Data.Foldable, so the lifting machinery won't work properly for length on 7.10 anyway)

[ranjitjhala]

​Except that I really don't want 'len' wired-in. I guess Niki's point is

• It is OK to wire-in primitive-measures for primitive types (e.g.
  strlen), but
• It is BAD to wire-in primitive-measures for non-primitive types (e.g. len)

?

Which does make sense, assuming we have to wire something in...

On Fri, Jul 10, 2015 at 11:15 AM, Eric Seidel [email protected]
wrote:

(Wiring-in len would also solve the minor renaming concern)

—
Reply to this email directly or view it on GitHub
#415 (comment)
.

Ranjit.

[ranjitjhala]

Yes, wiring in 'len' is non-option.

On Fri, Jul 10, 2015 at 11:36 AM, Ranjit Jhala [email protected] wrote:

​Except that I really don't want 'len' wired-in. I guess Niki's point is

• It is OK to wire-in primitive-measures for primitive types (e.g.
  strlen), but
• It is BAD to wire-in primitive-measures for non-primitive types (e.g.
  len)

?

Which does make sense, assuming we have to wire something in...

On Fri, Jul 10, 2015 at 11:15 AM, Eric Seidel [email protected]
wrote:

(Wiring-in len would also solve the minor renaming concern)

—
Reply to this email directly or view it on GitHub
#415 (comment)
.

Ranjit.

Ranjit.

[nikivazou]

@ranjitjhala this is indeed my point.

@gridaphobe my understanding is that we wish to go to a point where there will be no .spec files. You raise a good point about the Foldable version of length, but I do not have an answer right now.

[gridaphobe]

@nikivazou (this is starting to get way off topic, but..) can you point me to the discussion of removing the .spec files? I'm all for it in principle, but it seems like a very long-term goal. We'd have to get our annotations merged into base, containers, etc. which would take time (and force LH users to use the newest GHC/libraries).

[gridaphobe]

More on topic, I'm fine with @nikivazou's rule, I'll update the PR.

[ranjitjhala]

re: .spec files -- @spinda has managed to do this:

https://github.com/spinda/liquidhaskell/tree/iface/std/base-4.8.0.0/GHC

On Fri, Jul 10, 2015 at 11:50 AM, Eric Seidel [email protected]
wrote:

More on topic, I'm fine with @nikivazou https://github.com/nikivazou's
rule, I'll update the PR.

—
Reply to this email directly or view it on GitHub
#415 (comment)
.

Ranjit.

[gridaphobe]

I see, so the idea is not really to get rid of the .specs but rather switch them to the new quasiquoters, that makes more sense :)

[ranjitjhala]

The point is the QQ files are "understood" and imported by GHC and cabal
too.

On Fri, Jul 10, 2015 at 12:10 PM, Eric Seidel [email protected]
wrote:

I see, so the idea is not really to get rid of the .specs but rather
switch them to the new quasiquoters, that makes more sense :)

—
Reply to this email directly or view it on GitHub
#415 (comment)
.

Ranjit.

[gridaphobe]

Sure, but I thought @nikivazou was suggesting the much more ambitious task of removing the default specs entirely by convincing people to adopt them :)

[gridaphobe]

@nikivazou I made the edit you suggested, but it doesn't work. The inferred type for

unpackCString# "foo"

is

VV : {VV : [Char] | len VV == strLen "foo" && len VV >= 0}

which is VERY strange, since the type for unpackCString# is

GHC.CString.unpackCString#
  :: x:GHC.Prim.Addr#
  -> {v:String | len v == strLen x}

Why is x being substituted for the string literal?

[nikivazou]

@gridaphobe what is strangle about it? I think this is the expected type. We now just need to teach logic that strLen "foo" == 3

[ranjitjhala]

It is totally not clear how to teach the logic any such thing...

I think we should just adopt Eric's original solution for now, and revisit this with some proper solution for how to deal with literals.

On Jul 10, 2015, at 5:43 PM, Niki Vazou [email protected] wrote:

@gridaphobe what is strangle about it? I think this is the expected type. We now just need to teach logic that strLen "foo" == 3

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

[nikivazou]

We could just put into the fixpoint environment a binder {v:_ | strLen "foo" == 3} (for every string constant). But I am fine with having Eric's solution for now.

[gridaphobe]

@nikivazou I would expect

{v : [Char] | len v = strLen x}

in an environment where x = "foo" :: {v:Addr# | strLen v = 3}, but it turns out our ANF transformation doesn't introduce a new binder for "foo".

[gridaphobe]

Ah, but of course if we did ANF literals, we would be stuck with predicates drawn from the qualifier set...

[gridaphobe]

The only remaining test failures on travis are the usual ExitFailure 137 suspects (which IIRC may have something to do with running out of memory) so I'm gonna merge.

[spinda]

Yes, exit code 137 is when the OS kills the process before it completes, most likely due to running out of memory.