Guards: Replace recursion through universal quantification with rank-iteration.

This commit is contained in:
Anders Schack-Mulligen
2025-11-11 13:03:05 +01:00
parent a5279ec420
commit 3c7522ca7d

View File

@@ -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 |
@@ -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
or
validReturnInCustomGuardToRank(rnk - 1, m, ppos, retval, val) and
rnk <= maxRank(m) and
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
@@ -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