From c1c4a5bfcf6043589027b0b62d637adb60324536 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 18 Oct 2023 14:42:08 +0200 Subject: [PATCH] Rangeanalysis: Copy qldoc and simplification from Java. --- .../codeql/rangeanalysis/RangeAnalysis.qll | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll index a136a6eabb1..b9ac86b3d3b 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll @@ -1047,6 +1047,11 @@ module RangeStage< ) } + /** + * Holds if `b + delta` is a valid bound for `phi`'s `rix`th input edge. + * - `upper = true` : `phi <= b + delta` + * - `upper = false` : `phi >= b + delta` + */ pragma[nomagic] private predicate boundedPhiRankStep( Sem::SsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge, @@ -1056,9 +1061,9 @@ module RangeStage< rankedPhiInput(phi, inp, edge, rix) and boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge) | - if rix = 1 - then any() - else boundedPhiRankStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix - 1) + rix = 1 + or + boundedPhiRankStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix - 1) ) }