Simplify wildcard multiplication

[marcoeilers]

Simplifying the product of a wildcard and any positive term to be just the wildcard, similar to what Carbon already does.
In particular, this is intended to avoid non-linear wildcard-wildcard multiplications, which Z3 seems to struggle with.

Also adding some more cases to permission multiplication simplification to enable avoid these products also inside more complex terms.

This may or may not result in a small performance improvement. @jcp19

[mschwerhoff]

Doesn't that result in surprises when using perm? E.g.

inhale acc(x.f, wildcard)
inhale acc(x.g, perm(x.f) * 1/2)

assert perm(x.f) == perm(x.g) // would unexpectedly hold

assume perm(x.g) < 1
assert perm(x.g) < 1/2 // would unexpectedly fail

[marcoeilers]

I think it might, yes. I was trying to get it to do something like that yesterday but didn't immediately succeed. The important case IMO is really wildcard * wildcard, which I hope is not problematic; I only added the wildcard times anything positive cases in the first place because I saw that Carbon uses them, but will remove them again if they lead to issues like this one.

Although I think there are specific cases where the other simplifications are also valid and don't result in perm-problems.

[mschwerhoff]

Regarding wildcard * wildcard:

inhale acc(x.f, wildcard)
inhale acc(x.g, wildcard)
inhale acc(x.h, perm(x.f) * perm(x.g))
assert perm(x.h) == perm(x.f) || perm(x.h) == perm(x.g) // one of the two should hold due to the transformation, but which one might be backend-specific

Or am I misunderstanding this and "only" source-level wildcard multiplications are transformed?

[marcoeilers]

Crap, you're right.
Well, all the simplifications should be sound if the wildcard in question is constrainable or the method does not use permission introspection for the resource.
We'll see if this leads to any relevant performance improvements, and if yes I'll try implementing it for these special cases.

[mschwerhoff]

Happy to help — destroy your plans, that is :-P

[marcoeilers]

The code now tracks for which resources in the method/... that's being verified perm expressions are used, so in Malte's example from above, the simplification no longer happens for produce or consume related to the f or g fields, and thus we're sound.

However, I can still think of at least one scenario where we might not be sound:

predicate P(x: Ref) {
  acc(x.f) && acc(x.g, 1/2)
}

method m(x: Ref) {
  inhale P(x)
  unfold acc(P(x), wildcard) 
  // let's call the wildcard amount k. Now we should have k permission to x.f and k/2 to x.g, but we have k for both
  var p: Perm := perm(x.f)  
  assert acc(x.g, p)  // asserts we have k permission to x.g, which I think will pass after the simplification even though it shouldn't.
}

That means that the simplification is potentially unsafe if we use perm to find out the value of a wildcard and then exhale that amount of a different resource of which we have an amount that is some expression involving the same wildcard.