Greedy-like heuristics for consumeSingleLocation

[marcoeilers]

Heuristic that emulates greedy Silicon behavior for consuming single-receiver permissions for quantified resources.
First: Find singleton chunks that have the same receiver syntactically.
If there are any such chunks, consider those first, then all others.
Second: If nothing matches syntactically, try to find a singleton chunk that matches the receiver using the decider (using the check timeout, like in greedy lookup).
If that's the case, consider that chunk first, then all others.
Third: As a fallback, use the existing hint based heuristics.

This massively speeds up examples like the one @vakaras showed today.

[vakaras]

Did you have a chance to try it on some larger code like SCION?

[marcoeilers]

Yes, does not seem to make a difference unfortunately. Though the benchmarking there is kind of difficult sometimes because parallelism can hide a lot of differences.

[vakaras]

Yes, does not seem to make a difference unfortunately. Though the benchmarking there is kind of difficult sometimes because parallelism can hide a lot of differences.

As far as I know, Gobra puts resources on Viper heap only if they can be aliased, so they would be already invisible to QPs.

[vakaras]

LGTM. Thanks!