From 582d21d93419d49bfd3aada2addc2247aafbef41 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Fri, 9 Jan 2026 11:56:03 +0000 Subject: [PATCH 1/3] Java: Add range analysis testcase. --- .../dataflow/range-analysis/A.java | 25 +++++++ .../range-analysis/RangeAnalysis.expected | 75 +++++++++++++++++++ 2 files changed, 100 insertions(+) diff --git a/java/ql/test/library-tests/dataflow/range-analysis/A.java b/java/ql/test/library-tests/dataflow/range-analysis/A.java index 0b2aeaac2a67..20cf99751944 100644 --- a/java/ql/test/library-tests/dataflow/range-analysis/A.java +++ b/java/ql/test/library-tests/dataflow/range-analysis/A.java @@ -38,4 +38,29 @@ int f2(int x, int y, int z) { return 0; } + + + int f3(char size) { + int i = 0; + while (i < size) { + i++; + } + return i; + } + + int f4(int size) { + int i = 0; + while (i < size) { + i++; + } + return i; + } + + int f5(char size) { + int i = 10; + while (i < size) { + i++; + } + return i; + } } diff --git a/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected b/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected index 2648fd926861..aa135d1784bc 100644 --- a/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected +++ b/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected @@ -230,3 +230,78 @@ | A.java:35:24:35:24 | z | SSA param(z) | 0 | upper | NoReason | | A.java:39:12:39:12 | 0 | 0 | 0 | lower | NoReason | | A.java:39:12:39:12 | 0 | 0 | 0 | upper | NoReason | +| A.java:44:9:44:13 | i | 0 | 0 | lower | NoReason | +| A.java:44:9:44:13 | i | 0 | 0 | upper | NoReason | +| A.java:44:13:44:13 | 0 | 0 | 0 | lower | NoReason | +| A.java:44:13:44:13 | 0 | 0 | 0 | upper | NoReason | +| A.java:45:12:45:12 | i | 0 | 0 | lower | NoReason | +| A.java:45:12:45:12 | i | SSA def(i) | 0 | lower | NoReason | +| A.java:45:12:45:12 | i | SSA phi(i) | 0 | lower | NoReason | +| A.java:45:12:45:12 | i | SSA phi(i) | 0 | upper | NoReason | +| A.java:45:16:45:19 | size | SSA param(size) | 0 | lower | NoReason | +| A.java:45:16:45:19 | size | SSA param(size) | 0 | upper | NoReason | +| A.java:46:7:46:7 | i | 0 | 0 | lower | NoReason | +| A.java:46:7:46:7 | i | SSA def(i) | 0 | lower | NoReason | +| A.java:46:7:46:7 | i | SSA param(size) | -1 | upper | ... < ... | +| A.java:46:7:46:7 | i | SSA phi(i) | 0 | lower | NoReason | +| A.java:46:7:46:7 | i | SSA phi(i) | 0 | upper | NoReason | +| A.java:46:7:46:9 | ...++ | 0 | 0 | lower | NoReason | +| A.java:46:7:46:9 | ...++ | SSA def(i) | 0 | lower | NoReason | +| A.java:46:7:46:9 | ...++ | SSA param(size) | -1 | upper | ... < ... | +| A.java:46:7:46:9 | ...++ | SSA phi(i) | 0 | lower | NoReason | +| A.java:46:7:46:9 | ...++ | SSA phi(i) | 0 | upper | NoReason | +| A.java:48:12:48:12 | i | 0 | 0 | lower | NoReason | +| A.java:48:12:48:12 | i | SSA def(i) | 0 | lower | NoReason | +| A.java:48:12:48:12 | i | SSA param(size) | 0 | lower | ... < ... | +| A.java:48:12:48:12 | i | SSA phi(i) | 0 | lower | NoReason | +| A.java:48:12:48:12 | i | SSA phi(i) | 0 | upper | NoReason | +| A.java:52:9:52:13 | i | 0 | 0 | lower | NoReason | +| A.java:52:9:52:13 | i | 0 | 0 | upper | NoReason | +| A.java:52:13:52:13 | 0 | 0 | 0 | lower | NoReason | +| A.java:52:13:52:13 | 0 | 0 | 0 | upper | NoReason | +| A.java:53:12:53:12 | i | 0 | 0 | lower | NoReason | +| A.java:53:12:53:12 | i | SSA def(i) | 0 | lower | NoReason | +| A.java:53:12:53:12 | i | SSA phi(i) | 0 | lower | NoReason | +| A.java:53:12:53:12 | i | SSA phi(i) | 0 | upper | NoReason | +| A.java:53:16:53:19 | size | SSA param(size) | 0 | lower | NoReason | +| A.java:53:16:53:19 | size | SSA param(size) | 0 | upper | NoReason | +| A.java:54:7:54:7 | i | 0 | 0 | lower | NoReason | +| A.java:54:7:54:7 | i | SSA def(i) | 0 | lower | NoReason | +| A.java:54:7:54:7 | i | SSA param(size) | -1 | upper | ... < ... | +| A.java:54:7:54:7 | i | SSA phi(i) | 0 | lower | NoReason | +| A.java:54:7:54:7 | i | SSA phi(i) | 0 | upper | NoReason | +| A.java:54:7:54:9 | ...++ | 0 | 0 | lower | NoReason | +| A.java:54:7:54:9 | ...++ | SSA def(i) | 0 | lower | NoReason | +| A.java:54:7:54:9 | ...++ | SSA param(size) | -1 | upper | ... < ... | +| A.java:54:7:54:9 | ...++ | SSA phi(i) | 0 | lower | NoReason | +| A.java:54:7:54:9 | ...++ | SSA phi(i) | 0 | upper | NoReason | +| A.java:56:12:56:12 | i | 0 | 0 | lower | NoReason | +| A.java:56:12:56:12 | i | SSA def(i) | 0 | lower | NoReason | +| A.java:56:12:56:12 | i | SSA param(size) | 0 | lower | ... < ... | +| A.java:56:12:56:12 | i | SSA phi(i) | 0 | lower | NoReason | +| A.java:56:12:56:12 | i | SSA phi(i) | 0 | upper | NoReason | +| A.java:60:9:60:14 | i | 0 | 10 | lower | NoReason | +| A.java:60:9:60:14 | i | 0 | 10 | upper | NoReason | +| A.java:60:13:60:14 | 10 | 0 | 10 | lower | NoReason | +| A.java:60:13:60:14 | 10 | 0 | 10 | upper | NoReason | +| A.java:61:12:61:12 | i | 0 | 10 | lower | NoReason | +| A.java:61:12:61:12 | i | SSA def(i) | 0 | lower | NoReason | +| A.java:61:12:61:12 | i | SSA phi(i) | 0 | lower | NoReason | +| A.java:61:12:61:12 | i | SSA phi(i) | 0 | upper | NoReason | +| A.java:61:16:61:19 | size | SSA param(size) | 0 | lower | NoReason | +| A.java:61:16:61:19 | size | SSA param(size) | 0 | upper | NoReason | +| A.java:62:7:62:7 | i | 0 | 10 | lower | NoReason | +| A.java:62:7:62:7 | i | SSA def(i) | 0 | lower | NoReason | +| A.java:62:7:62:7 | i | SSA param(size) | -1 | upper | ... < ... | +| A.java:62:7:62:7 | i | SSA phi(i) | 0 | lower | NoReason | +| A.java:62:7:62:7 | i | SSA phi(i) | 0 | upper | NoReason | +| A.java:62:7:62:9 | ...++ | 0 | 10 | lower | NoReason | +| A.java:62:7:62:9 | ...++ | SSA def(i) | 0 | lower | NoReason | +| A.java:62:7:62:9 | ...++ | SSA param(size) | -1 | upper | ... < ... | +| A.java:62:7:62:9 | ...++ | SSA phi(i) | 0 | lower | NoReason | +| A.java:62:7:62:9 | ...++ | SSA phi(i) | 0 | upper | NoReason | +| A.java:64:12:64:12 | i | 0 | 10 | lower | NoReason | +| A.java:64:12:64:12 | i | SSA def(i) | 0 | lower | NoReason | +| A.java:64:12:64:12 | i | SSA param(size) | 0 | lower | ... < ... | +| A.java:64:12:64:12 | i | SSA phi(i) | 0 | lower | NoReason | +| A.java:64:12:64:12 | i | SSA phi(i) | 0 | upper | NoReason | From 915fcf99aad1fbde144d5b1f6f612aa36c118ccb Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Fri, 9 Jan 2026 11:56:33 +0000 Subject: [PATCH 2/3] Shared/Java: Improve range analysis for phi exits out of loops and accept test changes. --- .../range-analysis/RangeAnalysis.expected | 2 ++ .../codeql/rangeanalysis/RangeAnalysis.qll | 27 +++++++++++++++++++ 2 files changed, 29 insertions(+) diff --git a/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected b/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected index aa135d1784bc..df59f6f10494 100644 --- a/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected +++ b/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected @@ -236,6 +236,7 @@ | A.java:44:13:44:13 | 0 | 0 | 0 | upper | NoReason | | A.java:45:12:45:12 | i | 0 | 0 | lower | NoReason | | A.java:45:12:45:12 | i | SSA def(i) | 0 | lower | NoReason | +| A.java:45:12:45:12 | i | SSA param(size) | 0 | upper | ... < ... | | A.java:45:12:45:12 | i | SSA phi(i) | 0 | lower | NoReason | | A.java:45:12:45:12 | i | SSA phi(i) | 0 | upper | NoReason | | A.java:45:16:45:19 | size | SSA param(size) | 0 | lower | NoReason | @@ -253,6 +254,7 @@ | A.java:48:12:48:12 | i | 0 | 0 | lower | NoReason | | A.java:48:12:48:12 | i | SSA def(i) | 0 | lower | NoReason | | A.java:48:12:48:12 | i | SSA param(size) | 0 | lower | ... < ... | +| A.java:48:12:48:12 | i | SSA param(size) | 0 | upper | ... < ... | | A.java:48:12:48:12 | i | SSA phi(i) | 0 | lower | NoReason | | A.java:48:12:48:12 | i | SSA phi(i) | 0 | upper | NoReason | | A.java:52:9:52:13 | i | 0 | 0 | lower | NoReason | diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll index ff17f9b5405a..2d7964f5aa85 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll @@ -1011,6 +1011,27 @@ module RangeStage< boundedPhiInp(phi, _, b, delta, upper, fromBackEdge, origdelta, reason) } + /** + * Holds if `inp <= delta` where `inp` is the input to `phi` along the edge + * with rank `rix`. + * + * Equivalent to `boundedPhiInp(phi, rix, any(SemZeroBound zb), delta, true, _, _, _)`. + */ + private predicate zeroUpperBoundedPhiInp1(Sem::SsaPhiNode phi, int rix, D::Delta delta) { + boundedPhiInp1(phi, any(SemZeroBound zb), true, rix, delta) + } + + /** + * Holds if `inp <= b + delta` for some input, `inp`, to `phi` and `b >= 0`. + */ + private predicate upperBoundedPhiCand( + Sem::SsaPhiNode phi, SemSsaBound b, D::Delta delta, boolean fromBackEdge, D::Delta origdelta, + SemReason reason + ) { + boundedPhiCand(phi, true, b, delta, fromBackEdge, origdelta, reason) and + typeBound(Sem::getSsaType(b.getVariable()), any(float f | f >= 0), _) + } + /** * Holds if the candidate bound `b + delta` for `phi` is valid for the phi input * along the edge with rank `rix`. @@ -1031,6 +1052,12 @@ module RangeStage< or selfBoundedPhiInp(phi, rix, upper) ) + or + upperBoundedPhiCand(phi, b, delta, fromBackEdge, origdelta, reason) and + exists(D::Delta d1 | zeroUpperBoundedPhiInp1(phi, rix, d1) | + upper = true and + D::toFloat(d1) <= D::toFloat(delta) + ) } /** From 0bcfabac2c0e2872983592eb0ab488b458c34ee7 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Fri, 9 Jan 2026 12:47:42 +0000 Subject: [PATCH 3/3] C++: Accept test changes. --- .../ir/range-analysis/SimpleRangeAnalysis_tests.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp b/cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp index 649d99a7575c..870510ac04fd 100644 --- a/cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp +++ b/cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp @@ -175,12 +175,12 @@ int test12() { size_type Start = 0; while (Start <= test12_helper()-1) { - range(Start); // $ MISSING:range=>=0 + range(Start); // $ range="<=Store: ... += ...+0" MISSING:range=>=0 const size_type Length = test12_helper(); Start += Length + 1; // $ overflow=+ range(Start); // $ MISSING:range=>=1 MISSING:range=>=Start+1 MISSING:range=">=call to test12_helper+1" } - range(Start); // $ MISSING:range=>=0 + range(Start); // $ range="<=Store: ... += ...+0" MISSING:range=>=0 return 1; }