Guards: Improve join-order for wrapper guards

[aschackmull]

Improves the asymptotic performance of wrapper guards by applying the usual rank-iteration tranformation to a recursive universal quantification.

An observed example of the form

int foo(string x) {
  switch(x) {
     case "1" : return 1;
     case "2" : return 2;
     ...
     case "1000" : return 1000;
     default: return 0;
  }
}

goes from O(n^3) to O(n^2) to evaluate the O(n) result (the set of implications from return value to parameter value seeded with return being zero or not-zero).

[Copilot]

Pull Request Overview

This PR improves the asymptotic performance of wrapper guards by applying a rank-iteration transformation to a recursive universal quantification. The optimization changes the complexity from O(n³) to O(n²) when evaluating O(n) results for methods with many return expressions (e.g., a switch statement with 1000 cases).

Key Changes

• Introduces dense ranking for return expressions based on their location to enable incremental processing
• Replaces a universal quantification (forex) with a rank-based recursion that iterates through return expressions in order
• Adds helper predicates to track relevance of return expressions and their values

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[hvitved]

LGTM, two comments.

[hvitved]

Is this line needed?

[aschackmull]

Yes. The condition for iterating to the next rank is otherwise vacuously true, and then we'll get "infinite" tuples.

[hvitved]

It's the validReturnInCustomGuard(_, _, m, ppos, retval, val) that ensures that this becomes a forex and not a forall, right? If so, that might deserve a comment.

[aschackmull]

Yes. And the fact that we've pushed the constraint

          not exists(GuardValue notRetval |
            exprHasValue(ret, notRetval) and
            disjointValues(notRetval, retval)
          )

into it.

[aschackmull]

I've added a commit with an elaborating comment.