[Civl] fixed pack rule when linear types are involved

[shazqadeer]

No description provided.

[bkragl]

What is the pack rule?

[shazqadeer]

After datatypes were added to Boogie and linear types were added to Civl, I had to deal with the problem of safely nesting linear types inside datatypes. So I decided to add two operations pack and unpack. Both use the assignment syntax on the surface and look as follows:

x := Foo(a, b); // pack a Foo value
Foo(a, b) := x; // unpack a Foo value

Pack piggybacks on Boogie AssignCmd but unpack has a new UnpackCmd.

Typing machinery needs to be added so that duplicates of linear values do not get packed or unpacked.

This particular PR appears to be some adjustment to the type checking for pack.

[bkragl]

In your example Foo(a, b), let's assume the type of a is linear. (It's based on the type, right? Meaning it's not possible to declare the field as linear.) I can see two approaches for the type checking. 1) Require that the input for a is available in a pack, and only allow a single unpack on any path that'll make the output for a available. 2) Mark the result of a pack as available if a is available and otherwise the result is just not available (but it is not an error), and only mark the output for a as available if the packed value is available (making the packed value unavailable). Is either of these approaches what happens?

I guess Foo could itself be linear, but there is a priori no semantic connection between its permissions and the permissions of its fields.

[shazqadeer]

Both approaches are possible. Based on the error messages on lines 72 and 78 on this test, it seems the implementation is taking (1).

I guess Foo could itself be linear, but there is a priori no semantic connection between its permissions and the permissions of its fields.

It is not possible to declare a type to be linear currently. We have four primitive linear types---Lval, Lset, Lmap, Lheap. If another type packs one of these types (transitively) in a field, then that is detected and appropriate precautions about duplication are taken.

Ankush Das suggested that it should be possible to allow any type to be declared linear. I don't have enough experience to judge what benefit might derive from that.