From 0a4406dec97496c5cf59bd3be89ea7af0e8de9a4 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 11 Nov 2025 12:45:46 +0100 Subject: [PATCH 1/5] Guards: Push forex-range constraint in. --- .../controlflow/codeql/controlflow/Guards.qll | 30 +++++++++++++++---- 1 file changed, 24 insertions(+), 6 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 17aee2a7caee..a9998c0e65e4 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -1024,16 +1024,34 @@ module Make< ReturnImplies::guardControls(call, val, _, _) } - predicate relevantReturnValue(NonOverridableMethod m, GuardValue val) { + /** + * Holds if a call to `m` having a return value of `retval` is reachable + * by a chain of implications. + */ + predicate relevantReturnValue(NonOverridableMethod m, GuardValue retval) { exists(NonOverridableMethodCall call | - relevantCallValue(call, val) and + relevantCallValue(call, retval) and call.getMethod() = m and - not val instanceof TException + not retval instanceof TException + ) + } + + /** + * Holds if a call to `m` having a return value of `retval` is reachable + * by a chain of implications, and `ret` is a return expression in `m` + * that could possibly have the value `retval`. + */ + predicate relevantReturnExprValue(NonOverridableMethod m, ReturnExpr ret, GuardValue retval) { + relevantReturnValue(m, retval) and + ret = m.getAReturnExpr() and + not exists(GuardValue notRetval | + exprHasValue(ret, notRetval) and + disjointValues(notRetval, retval) ) } private predicate returnGuard(Guard guard, GuardValue val) { - relevantReturnValue(guard.(ReturnExpr).getMethod(), val) + relevantReturnExprValue(_, guard, val) } module ReturnImplies = ImpliesTC; @@ -1058,7 +1076,7 @@ module Make< exists(Guard g0, GuardValue v0 | directlyControlsReturn(g0, v0, ret) and BranchImplies::ssaControls(param, val, g0, v0) and - relevantReturnValue(m, retval) + relevantReturnExprValue(m, ret, retval) ) or ReturnImplies::ssaControls(param, val, ret, retval) @@ -1166,7 +1184,7 @@ module Make< guardChecksDef(guard, param, val, state) | guard.valueControls(ret.getBasicBlock(), val) and - relevantReturnValue(m, retval) + relevantReturnExprValue(m, ret, retval) or ReturnImplies::guardControls(guard, val, ret, retval) ) From a5279ec420c5aacb8d827d71dc09b5bd600fe784 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 11 Nov 2025 12:52:07 +0100 Subject: [PATCH 2/5] Guards: Rank return expressions. --- .../controlflow/codeql/controlflow/Guards.qll | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index a9998c0e65e4..4729878d9287 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -1008,6 +1008,8 @@ module Make< * wrappers. */ private module WrapperGuard { + private import codeql.util.DenseRank + final private class FinalExpr = Expr; class ReturnExpr extends FinalExpr { @@ -1019,6 +1021,25 @@ module Make< BasicBlock getBasicBlock() { result = super.getBasicBlock() } } + private module DenseRankInput implements DenseRankInputSig1 { + class C = NonOverridableMethod; + + class Ranked = ReturnExpr; + + int getRank(NonOverridableMethod m, ReturnExpr ret) { + m.getAReturnExpr() = ret and + result = ret.getLocation().getStartLine() + } + } + + private module ReturnExprRank = DenseRank1; + + private predicate rankedReturnExpr = ReturnExprRank::denseRank/2; + + private int maxRank(NonOverridableMethod m) { + result = max(int rnk | exists(rankedReturnExpr(m, rnk))) + } + private predicate relevantCallValue(NonOverridableMethodCall call, GuardValue val) { BranchImplies::guardControls(call, val, _, _) or ReturnImplies::guardControls(call, val, _, _) From 3c7522ca7d6cbc09f53d2fdbbb2cdac5a1efc3cc Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 11 Nov 2025 13:03:05 +0100 Subject: [PATCH 3/5] Guards: Replace recursion through universal quantification with rank-iteration. --- .../controlflow/codeql/controlflow/Guards.qll | 35 ++++++++++++------- 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 4729878d9287..2f964258b416 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -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 From 62e28d2dcfec0d49360182da8d8a9de508088290 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 11 Nov 2025 13:34:47 +0100 Subject: [PATCH 4/5] Guards: Simplify non-linear join. --- shared/controlflow/codeql/controlflow/Guards.qll | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index 2f964258b416..db81aa8443ad 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -1082,6 +1082,15 @@ module Make< guard.directlyValueControls(ret.getBasicBlock(), val) } + private predicate parameterControlsReturnExpr( + SsaParameterInit param, GuardValue val, ReturnExpr ret + ) { + exists(Guard g0, GuardValue v0 | + directlyControlsReturn(g0, v0, ret) and + BranchImplies::ssaControls(param, val, g0, v0) + ) + } + /** * Holds if `ret` is a return expression in a non-overridable method that * on a return value of `retval` allows the conclusion that the `ppos`th @@ -1095,11 +1104,8 @@ module Make< ret = rankedReturnExpr(m, rnk) and param.getParameter() = m.getParameter(ppos) | - exists(Guard g0, GuardValue v0 | - directlyControlsReturn(g0, v0, ret) and - BranchImplies::ssaControls(param, val, g0, v0) and - relevantReturnExprValue(m, ret, retval) - ) + parameterControlsReturnExpr(param, val, ret) and + relevantReturnExprValue(m, ret, retval) or ReturnImplies::ssaControls(param, val, ret, retval) ) From b31dfdd5f4d30bd0c163c7955a6b7a9d9d024aaf Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 13 Nov 2025 13:09:44 +0100 Subject: [PATCH 5/5] Guards: Add elaborating comment. --- shared/controlflow/codeql/controlflow/Guards.qll | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/shared/controlflow/codeql/controlflow/Guards.qll b/shared/controlflow/codeql/controlflow/Guards.qll index db81aa8443ad..8fd39279ff65 100644 --- a/shared/controlflow/codeql/controlflow/Guards.qll +++ b/shared/controlflow/codeql/controlflow/Guards.qll @@ -1114,6 +1114,11 @@ module Make< private predicate validReturnInCustomGuardToRank( int rnk, NonOverridableMethod m, ParameterPosition ppos, GuardValue retval, GuardValue val ) { + // The forall-range has been pushed all the way into + // `relevantReturnExprValue` and `validReturnInCustomGuard`. This means + // that this base case ensures that at least one return expression + // non-vacuously satisfies that it's a valid implication from return + // value to parameter value. validReturnInCustomGuard(_, _, m, ppos, retval, val) and rnk = 0 or validReturnInCustomGuardToRank(rnk - 1, m, ppos, retval, val) and