Expand nested predicates

[ionathanch]

Fixes #20.

At first I had merged getting the predicate ids with expanding the predicates because it's really tricky getting all those nested names without doing the actual expansion, but since we only don't expand (mutually) recursive predicates, we don't need to return those names anyway.

Also, instead of passing in a set of predicate names that are or aren't expanded, I've abstracted that into a condition that's passed along (a Scala predicate for the Viper predicate names, so to speak) so that we can adjust the condition in InlinePredicatePlugin if ever needed.

Meanwhile, in beforeVerify, I've added getting all predicate ids in advance, filtered by whether those have bodies, since it's not really expandPredicate's business to find out anyway; all it should do is check cond, check current scope, eat hot chip, and lie.

I've also commented out the stuff to do with the inline keyword. Once that's implemented, we can switch over, but I imagine we might also want to provide a global flag of some sort to say "please inline all predicates by default", then inline only those with the keyword in its absence? Then whether the cond uses nonrecursivePredIds or nonrecursiveInlinePredIds depends on the state of the flag. I suppose I should open a new stretch goal issue for that (but it could be as simple as adding a parser for a new type of declaration!).

Also it turns out I was working on the wrong branch so I've committed on top of a (fork of) yoo/fix-fold-unfold-bug oops, which I guess means this would also fix #10 if merged?

[jyoo980]

eat hot chip, and lie.

??

[ionathanch]

This has been tested with the following:

Nested predicates

Before

field left: Int
field right: Int
field middle: Int

predicate p1(this: Ref) {
  acc(this.left) && p2(this)
}

predicate p2(this: Ref) {
  acc(this.middle) && p3(this)
}

predicate p3(this: Ref) {
  acc(this.right)
}

method sumTriple(this: Ref)
  returns  (sum: Int)
  requires p1(this)
  ensures  p1(this)
{
  unfold p1(this)
  unfold p2(this)
  unfold p3(this)
  sum := this.left + this.middle + this.right
  fold p3(this)
  fold p2(this)
  fold p1(this)
}

After

field left: Int
field right: Int
field middle: Int

predicate p1(this: Ref) {
  acc(this.left, write) && acc(p2(this), write)
}

predicate p2(this: Ref) {
  acc(this.middle, write) && acc(p3(this), write)
}

predicate p3(this: Ref) {
  acc(this.right, write)
}

method sumTriple(this: Ref) returns (sum: Int)
  requires acc(this.left, write) && (acc(this.middle, write) && acc(this.right, write))
  ensures acc(this.left, write) && (acc(this.middle, write) && acc(this.right, write))
{
  sum := this.left + this.middle + this.right
}

Redundant folds/unfolds

Before

field content: Int

predicate boxed(box: Ref) {
  acc(box.content)
}

predicate bottom(box: Ref) { true }

method setBox(box: Ref, i: Int)
  requires boxed(box) && bottom(box)
  ensures  boxed(box)
  ensures  unfolding boxed(box) in box.content == i
{
  unfold boxed(box)
  unfold bottom(box)
  box.content := i
  fold boxed(box)
  unfold boxed(box)
  fold boxed(box)
}

After

field left: Int

field right: Int

field middle: Int

field content: Int

predicate boxed(box: Ref) {
  acc(box.content, write)
}

predicate bottom(box: Ref) { true }

method setBox(box: Ref, i: Int)
  requires acc(box.content, write) && true
  ensures acc(box.content, write)
  ensures box.content == i
{
  box.content := i
}

Bonus

Before

method makeBox(i: Int)
  returns (box: Ref)
  // Note the missing `ensures boxed(box)`
{
  box := new(content)
  box.content := i
  fold boxed(box)
}

After

method makeBox(i: Int)
  returns (box: Ref)
{
  box := new(content)
  box.content := i
}

[jyoo980]

Oh I get it: https://knowyourmeme.com/memes/eat-hot-chip-and-lie

👍