diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll index 1d17ad8346c4..ff17f9b5405a 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll @@ -923,17 +923,18 @@ module RangeStage< } /** - * Holds if `b + delta` is a valid bound for `inp` when used as an input to - * `phi` along `edge`. + * Holds if `b + delta` is a valid bound for the input `inp` to `phi` along + * the edge with rank `rix`. * - `upper = true` : `inp <= b + delta` * - `upper = false` : `inp >= b + delta` */ private predicate boundedPhiInp( - Sem::SsaPhiNode phi, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge, SemBound b, - D::Delta delta, boolean upper, boolean fromBackEdge, D::Delta origdelta, SemReason reason + Sem::SsaPhiNode phi, int rix, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge, + D::Delta origdelta, SemReason reason ) { - edge.phiInput(phi, inp) and - exists(D::Delta d, boolean fromBackEdge0 | + exists( + D::Delta d, boolean fromBackEdge0, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge + | boundedSsa(inp, b, d, edge, upper, fromBackEdge0, origdelta, reason) or boundedPhi(inp, b, d, upper, fromBackEdge0, origdelta, reason) @@ -945,6 +946,7 @@ module RangeStage< origdelta = D::fromFloat(0) and reason = TSemNoReason() | + rankedPhiInput(phi, inp, edge, rix) and if backEdge(phi, inp, edge) then fromBackEdge = true and @@ -963,33 +965,30 @@ module RangeStage< } /** - * Holds if `b + delta` is a valid bound for `inp` when used as an input to - * `phi` along `edge`. + * Holds if `b + delta` is a valid bound for the input `inp` to `phi` along + * the edge with rank `rix`. * - `upper = true` : `inp <= b + delta` * - `upper = false` : `inp >= b + delta` * - * Equivalent to `boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)`. + * Equivalent to `boundedPhiInp(phi, rix, b, delta, upper, _, _, _)`. */ pragma[noinline] private predicate boundedPhiInp1( - Sem::SsaPhiNode phi, SemBound b, boolean upper, Sem::SsaVariable inp, - SsaReadPositionPhiInputEdge edge, D::Delta delta + Sem::SsaPhiNode phi, SemBound b, boolean upper, int rix, D::Delta delta ) { - boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _) + boundedPhiInp(phi, rix, b, delta, upper, _, _, _) } /** - * Holds if `phi` is a valid bound for `inp` when used as an input to `phi` - * along `edge`. + * Holds if `phi` is a valid bound for the input `inp` to `phi` along the + * edge with rank `rix`. * - `upper = true` : `inp <= phi` * - `upper = false` : `inp >= phi` */ - private predicate selfBoundedPhiInp( - Sem::SsaPhiNode phi, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge, boolean upper - ) { + private predicate selfBoundedPhiInp(Sem::SsaPhiNode phi, int rix, boolean upper) { exists(D::Delta d, SemSsaBound phibound | phibound.getVariable() = phi and - boundedPhiInp(phi, inp, edge, phibound, d, upper, _, _, _) and + boundedPhiInp(phi, rix, phibound, d, upper, _, _, _) and ( upper = true and D::toFloat(d) <= 0 or @@ -1009,33 +1008,34 @@ module RangeStage< Sem::SsaPhiNode phi, boolean upper, SemBound b, D::Delta delta, boolean fromBackEdge, D::Delta origdelta, SemReason reason ) { - boundedPhiInp(phi, _, _, b, delta, upper, fromBackEdge, origdelta, reason) + boundedPhiInp(phi, _, b, delta, upper, fromBackEdge, origdelta, reason) } /** * Holds if the candidate bound `b + delta` for `phi` is valid for the phi input - * `inp` along `edge`. + * along the edge with rank `rix`. */ private predicate boundedPhiCandValidForEdge( Sem::SsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge, - D::Delta origdelta, SemReason reason, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge + D::Delta origdelta, SemReason reason, int rix ) { boundedPhiCand(phi, upper, b, delta, fromBackEdge, origdelta, reason) and ( - exists(D::Delta d | boundedPhiInp1(phi, b, upper, inp, edge, d) | + exists(D::Delta d | boundedPhiInp1(phi, b, upper, rix, d) | upper = true and D::toFloat(d) <= D::toFloat(delta) ) or - exists(D::Delta d | boundedPhiInp1(phi, b, upper, inp, edge, d) | + exists(D::Delta d | boundedPhiInp1(phi, b, upper, rix, d) | upper = false and D::toFloat(d) >= D::toFloat(delta) ) or - selfBoundedPhiInp(phi, inp, edge, upper) + selfBoundedPhiInp(phi, rix, upper) ) } /** - * Holds if `b + delta` is a valid bound for `phi`'s `rix`th input edge. + * Holds if `b + delta` is a valid bound for `phi` when accounting for the + * input edges ranked 1 through `rix`. * - `upper = true` : `phi <= b + delta` * - `upper = false` : `phi >= b + delta` */ @@ -1044,10 +1044,8 @@ module RangeStage< Sem::SsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge, D::Delta origdelta, SemReason reason, int rix ) { - exists(Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge | - rankedPhiInput(phi, inp, edge, rix) and - boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge) - | + boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix) and + ( rix = 1 or boundedPhiRankStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix - 1)