Nested predicates aren't expanded

[ionathanch]

Description

Original program:

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

predicate mid(this: Ref) {
  acc(this.middle, write)
}

predicate triple(this: Ref) {
  acc(this.left) && acc(this.right) && mid(this)
}

method tripleSum(this: Ref) returns (sum: Int)
  requires triple(this)
  ensures triple(this)
{
  unfold triple(this)
  unfold mid(this)
  sum := this.left + this.middle + this.right
  fold mid(this)
  fold triple(this)
}

Expected:

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

Actual:

method tripleSum(this: Ref) returns (sum: Int)
  requires acc(this.left) && acc(this.right) && mid(this)
  ensures acc(this.left) && acc(this.right) && mid(this)
{
  unfold mid(this)
  sum := this.left + this.middle + this.right
  fold mid(this)
}

Preliminary Investigation

This would be solved in InlineRewrite.expandPredicates by changing the traversal from TopDown to BottomUp, but we can't do that since the variable name context accumulates names from QuantifiedExps outside-in, and changing it to bottom-up could break things.

[jyoo980]

Is there a way to separate the traversals for the variable name context from this? Or am I just being dumb and that's something that has to be done together in the same traversal.

[ionathanch]

I suppose you could traverse first for the name context top-down then expand bottom-up, but the name contexts would have to be stored in a tree structure the same shape as the exp, and during expansion you'd have to traverse the context tree and the exp simultaneously I was hoping the codebase would already have some sort of "get current bound variable names" method handy somewhere, but I haven't found one yet Another option is to iteratively traverse until no more can be expanded, but that could get wildly inefficient

[ionathanch]

On a separate note, this also affects expandablePredicates, since now we also need to look inside the bodies of predicates to see if there's any more to expand.

[jyoo980]

I wonder if this is something that could be put into future work; we could support one level of expansion for now

[jyoo980]

The fix for expandablePredicates should be relatively straightforward, in any case

[jyoo980]

Resolved to make this future work + introduce code to alert the developer that nested predicates will not be inlined

[ionathanch]

Sorry for just thinking of this when you've done all the work for erroring out but I did some digging and if you look at where the scope variables are actually used, ultimately get they passed to the replaceFreeVariablesInExpression function, and the doc comment for it says:

/** This method replaces free variables in the expression by corresponding subexpressions.
  * If bound variables exist and their identifiers clash with the new free variables or scope,
  * then the bound variables are renamed, preventing the new free variables from being 'captured'.
  * ...
  * @param scope        A set of names representing the scope where the expression is located.
  * @return             An expression with all expected replacements, properly sanitized.
  */

So the variables are essentially just being used to make sure that variables don't clash (is this capture-avoiding substitution?), which means we could traverse the entire expression, get all the bound variables, and pass all of them into predicateBody just to be safe Which means we can traverse bottom-up rather than top-down Which means we can expand nested predicates! I'm gonna look into this a bit more... tomorrow

[jyoo980]

Ahh fuck.

I should've looked harder as well, looks like it might be something possible. If not we can still fall back on the warning work.

[ionathanch]

I'm a fool :clown_face: The reason nested predicates aren't being expanded has nothing to do with the traversal order... It's just because expandablePredicates doesn't collect the name so it's not listed as one of the ones that need to be expanded :facepalm:

[jyoo980]

I need a drink.

So it should be a matter of adding another case for expandablePredicates right?

[ionathanch]

Shoulda asked for alcohol from your secret santa too lol For expandablePredicates you've got to traverse the body of the predicate as well, I'm working on adding it rn