java: inline range test #17997

yoff · 2024-11-15T11:32:59Z

This adds inline expectation test for the java range analysis.
Feel free to suggest better tests or better syntax.

Pull Request checklist

All query authors

A change note is added if necessary. See the documentation in this repository.
All new queries have appropriate .qhelp. See the documentation in this repository.
QL tests are added if necessary. See Testing custom queries in the GitHub documentation.
New and changed queries have correct query metadata. See the documentation in this repository.

Internal query authors only

Autofixes generated based on these changes are valid, only needed if this PR makes significant changes to .ql, .qll, or .qhelp files. See the documentation (internal access required).
Changes are validated at scale (internal access required).
Adding a new query? Consider also adding the query to autofix.

java/ql/test/library-tests/dataflow/range-analysis-inline/range.ql

java/ql/test/library-tests/dataflow/range-analysis-inline/B.java

aschackmull · 2024-11-18T10:25:00Z

java/ql/test/library-tests/dataflow/range-analysis-inline/B.java

+
+    public int forloopexitupd() {
+        int result = 0;
+        for (; result < 10; result++) { // $ bound="result in [0..9]" bound="result in [0..10]"


Yes, I will get that done.

aschackmull · 2024-11-18T10:25:23Z

java/ql/test/library-tests/dataflow/range-analysis-inline/B.java

+
+    public int emptyforloop() {
+        int result = 0;
+        for (int i = 0; i < 0; i++) { // $ bound="i = 0" bound="i in [0..-1]"


aschackmull · 2024-11-18T10:35:24Z

One of the key features of the range analysis library is the ability to report bounds in terms of SSA variables or interesting expressions such as arr.length. I think it would be nice to add some cases of inline expectations for those bounds as well. Given that they're plentiful, they should only be reported relative to indicated bound expression positions. E.g.

static void bound(int b) { }

static void tst(int[] arr) {
  bound(arr.length);
  for (int i = 0; i < arr.length; i++) {
    arr[i]++; // $ bound="i <= arr.length - 1"
  }
}

But feel free to take or leave this suggestion, depending on how much effort you want to put in, as it's also fine to just merge what's already here in the PR.

Co-authored-by: Anders Schack-Mulligen <[email protected]>

yoff · 2024-11-19T12:40:24Z

One of the key features of the range analysis library is the ability to report bounds in terms of SSA variables or interesting expressions such as arr.length. I think it would be nice to add some cases of inline expectations for those bounds as well. Given that they're plentiful, they should only be reported relative to indicated bound expression positions. E.g.

I think that is a nice idea. The current set of tests is based on my hunt for opportunities to improve range analysis results by rewriting the CFG. But the current PR should rather just present a useful set of tests for range analysis, so I will give this a go :-)

yoff · 2024-11-25T13:49:42Z

But the current PR should rather just present a useful set of tests for range analysis

This can probably still be improved quite a bit. But now there is at least support for annotating non-integer bounds.

java/ql/test/library-tests/dataflow/range-analysis-inline/range.ql

aschackmull · 2024-11-25T13:57:03Z

java/ql/test/library-tests/dataflow/range-analysis-inline/B.java

+            i++) { // $ bound="i <= b - 1"
+            result = i; // $ bound="i <= b - 1"
+        }
+        return result; // $ MISSING: bound="result <= b - 1"


That's not MISSING - such a bound would be wrong if b is negative or zero, and thus the range analysis won't infer it.

Ah, nice. So if I add a guard for b being positive, it might appear. Having both versions would be a good illustration of this.

I could not get the bound to appear, so now there are just a bunch of negative tests..

aschackmull · 2024-11-25T14:03:20Z

java/ql/test/library-tests/dataflow/range-analysis-inline/range.ql

+    boundExpr = b.getExpr() and
+    exists(Call c | c.getCallee().getName() = "bound" and c.getArgument(0) = boundExpr) and
+    // non-trivial bound
+    (DataFlow::localFlow(DataFlow::exprNode(boundExpr), DataFlow::exprNode(e)) implies delta != 0)


This constraint looks very weird. Perhaps something like this would suffice?

Suggested change

(DataFlow::localFlow(DataFlow::exprNode(boundExpr), DataFlow::exprNode(e)) implies delta != 0)

not e = b.getExpr()

I tried that first, but it let through some trivial things. However, it works now...I think I am not used to ensuring the test file compiles all the time... 😅

aschackmull · 2024-11-25T14:05:16Z

java/ql/test/library-tests/dataflow/range-analysis-inline/range.ql

+      exists(
+        Expr e, int delta, string deltaStr, boolean upper, string cmp, Bound b, Expr boundExpr
+      |
+        annotatedBound(e, b, boundExpr, delta, upper) and


Suggested change

annotatedBound(e, b, boundExpr, delta, upper) and

annotatedBound(e, _, boundExpr, delta, upper) and

aschackmull · 2024-11-25T14:05:59Z

java/ql/test/library-tests/dataflow/range-analysis-inline/range.ql

+import java
+import semmle.code.java.dataflow.RangeAnalysis
+private import TestUtilities.InlineExpectationsTest as IET
+private import semmle.code.java.dataflow.DataFlow


We should not add data flow to the mix.

Suggested change

private import semmle.code.java.dataflow.DataFlow

aschackmull · 2024-11-26T13:37:23Z

java/ql/test/library-tests/dataflow/range-analysis-inline/B.java

+                i++) { // $ bound="i <= b - 1"
+                result = i; // $ bound="i <= b - 1"
+            }
+            return result; // $ MISSING: bound="result <= b - 1"


Btw. this is actually a case that potentially could be improved by some sort of "loop executes at least once" analysis.

aschackmull

LGTM now.

java: inline range test

15953bf

yoff added the no-change-note-required This PR does not need a change note label Nov 15, 2024

yoff requested a review from a team as a code owner November 15, 2024 11:33

github-actions bot added the Java label Nov 15, 2024

aschackmull reviewed Nov 18, 2024

View reviewed changes

java/ql/test/library-tests/dataflow/range-analysis-inline/range.ql Outdated Show resolved Hide resolved

aschackmull reviewed Nov 18, 2024

View reviewed changes

java/ql/test/library-tests/dataflow/range-analysis-inline/range.ql Outdated Show resolved Hide resolved

aschackmull reviewed Nov 18, 2024

View reviewed changes

java/ql/test/library-tests/dataflow/range-analysis-inline/B.java Outdated Show resolved Hide resolved

aschackmull reviewed Nov 18, 2024

View reviewed changes

Apply suggestions from code review

6ed8950

Co-authored-by: Anders Schack-Mulligen <[email protected]>

yoff added 2 commits November 25, 2024 12:32

java: separate bounds onto different lines

37935ee

Java: Add support for non-integer bounds in inline expectations

25664d0

yoff requested a review from aschackmull November 25, 2024 13:49

github-advanced-security bot found potential problems Nov 25, 2024

View reviewed changes

java/ql/test/library-tests/dataflow/range-analysis-inline/range.ql Fixed Show fixed Hide fixed

aschackmull reviewed Nov 25, 2024

View reviewed changes

Java: address review comments

f508f8e

yoff requested a review from aschackmull November 26, 2024 10:48

aschackmull reviewed Nov 26, 2024

View reviewed changes

aschackmull approved these changes Nov 26, 2024

View reviewed changes

yoff merged commit 6d6f269 into github:main Nov 26, 2024
10 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

java: inline range test #17997

java: inline range test #17997

yoff commented Nov 15, 2024

aschackmull Nov 18, 2024

yoff Nov 19, 2024

aschackmull Nov 18, 2024

yoff Nov 19, 2024

aschackmull commented Nov 18, 2024

yoff commented Nov 19, 2024

yoff commented Nov 25, 2024

aschackmull Nov 25, 2024 •

edited

Loading

yoff Nov 25, 2024

yoff Nov 26, 2024

aschackmull Nov 25, 2024

yoff Nov 26, 2024

aschackmull Nov 25, 2024

aschackmull Nov 25, 2024

aschackmull Nov 26, 2024

aschackmull left a comment

	(DataFlow::localFlow(DataFlow::exprNode(boundExpr), DataFlow::exprNode(e)) implies delta != 0)
	not e = b.getExpr()

	annotatedBound(e, b, boundExpr, delta, upper) and
	annotatedBound(e, _, boundExpr, delta, upper) and

java: inline range test #17997

java: inline range test #17997

Conversation

yoff commented Nov 15, 2024

Pull Request checklist

All query authors

Internal query authors only

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

aschackmull commented Nov 18, 2024

yoff commented Nov 19, 2024

yoff commented Nov 25, 2024

aschackmull Nov 25, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

aschackmull left a comment

Choose a reason for hiding this comment

aschackmull Nov 25, 2024 •

edited

Loading