Skip to content

Guards: Improve join-order for wrapper guards #20814

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
aschackmull merged 5 commits into from
Nov 13, 2025
Merged

Guards: Improve join-order for wrapper guards #20814

Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
0a4406d
Guards: Push forex-range constraint in.
aschackmull Nov 11, 2025
a5279ec
Guards: Rank return expressions.
aschackmull Nov 11, 2025
3c7522c
Guards: Replace recursion through universal quantification with rank-…
aschackmull Nov 11, 2025
62e28d2
Guards: Simplify non-linear join.
aschackmull Nov 11, 2025
b31dfdd
Guards: Add elaborating comment.
aschackmull Nov 13, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 23 additions & 12 deletions shared/controlflow/codeql/controlflow/Guards.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1088,10 +1088,11 @@ module Make<
* parameter has the value `val`.
*/
private predicate validReturnInCustomGuard(
ReturnExpr ret, ParameterPosition ppos, GuardValue retval, GuardValue val
ReturnExpr ret, int rnk, NonOverridableMethod m, ParameterPosition ppos, GuardValue retval,
GuardValue val
) {
exists(NonOverridableMethod m, SsaParameterInit param |
m.getAReturnExpr() = ret and
exists(SsaParameterInit param |
ret = rankedReturnExpr(m, rnk) and
param.getParameter() = m.getParameter(ppos)
|
exists(Guard g0, GuardValue v0 |
Expand All @@ -1104,6 +1105,24 @@ module Make<
)
}

private predicate validReturnInCustomGuardToRank(
int rnk, NonOverridableMethod m, ParameterPosition ppos, GuardValue retval, GuardValue val
) {
validReturnInCustomGuard(_, _, m, ppos, retval, val) and rnk = 0
Copy link
Contributor

@hvitved hvitved Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

@aschackmull aschackmull Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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

into it.

Copy link
Contributor Author

@aschackmull aschackmull Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've added a commit with an elaborating comment.

or
validReturnInCustomGuardToRank(rnk - 1, m, ppos, retval, val) and
rnk <= maxRank(m) and
Copy link
Contributor

@hvitved hvitved Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this line needed?

Copy link
Contributor Author

@aschackmull aschackmull Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

forall(ReturnExpr ret |
ret = rankedReturnExpr(m, rnk) and
not exists(GuardValue notRetval |
exprHasValue(ret, notRetval) and
disjointValues(notRetval, retval)
)
|
validReturnInCustomGuard(ret, rnk, m, ppos, retval, val)
)
}

private predicate guardDirectlyControlsExit(Guard guard, GuardValue val) {
exists(BasicBlock bb |
guard.directlyValueControls(bb, val) and
Expand All @@ -1119,15 +1138,7 @@ module Make<
private NonOverridableMethod wrapperGuard(
ParameterPosition ppos, GuardValue retval, GuardValue val
) {
forex(ReturnExpr ret |
result.getAReturnExpr() = ret and
not exists(GuardValue notRetval |
exprHasValue(ret, notRetval) and
disjointValues(notRetval, retval)
)
|
validReturnInCustomGuard(ret, ppos, retval, val)
)
validReturnInCustomGuardToRank(maxRank(result), result, ppos, retval, val)
or
exists(SsaParameterInit param, Guard g0, GuardValue v0 |
param.getParameter() = result.getParameter(ppos) and
Expand Down