Java: Fix range analysis false negative

Author: tamasvajk

java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll

@@ -252,6 +252,15 @@ private Guard boundFlowCond(SsaVariable v, Expr e, int delta, boolean upper, boo
   or
   result = eqFlowCond(v, e, delta, true, testIsTrue) and
   (upper = true or upper = false)
+  or
+  // guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
+  // exists a guard `guardEq` such that `v = v2 - d1 + d2`.
+  exists(SsaVariable v2, Guard guardEq, boolean eqIsTrue, int d1, int d2 |
+    guardEq = eqFlowCond(v, ssaRead(v2, d1), d2, true, eqIsTrue) and
+    result = boundFlowCond(v2, e, delta + d1 - d2, upper, testIsTrue) and
+    // guardEq needs to control guard
+    guardEq.directlyControls(result.getBasicBlock(), eqIsTrue)
+  )
 }
 
 private newtype TReason =

java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected

@@ -27,11 +27,13 @@
 | A.java:8:25:8:25 | y | SSA init(y) | 0 | upper | NoReason |
 | A.java:8:29:8:31 | 300 | 0 | 300 | lower | NoReason |
 | A.java:8:29:8:31 | 300 | 0 | 300 | upper | NoReason |
+| A.java:9:16:9:16 | x | 0 | 299 | lower | ... > ... |
 | A.java:9:16:9:16 | x | 0 | 400 | upper | ... > ... |
 | A.java:9:16:9:16 | x | SSA init(x) | 0 | lower | NoReason |
 | A.java:9:16:9:16 | x | SSA init(x) | 0 | upper | NoReason |
 | A.java:9:16:9:16 | x | SSA init(y) | -2 | lower | ... == ... |
 | A.java:9:16:9:16 | x | SSA init(y) | -2 | upper | ... == ... |
+| A.java:9:16:9:20 | ... + ... | 0 | 300 | lower | ... > ... |
 | A.java:9:16:9:20 | ... + ... | SSA init(x) | 1 | lower | NoReason |
 | A.java:9:16:9:20 | ... + ... | SSA init(y) | -1 | lower | ... == ... |
 | A.java:9:20:9:20 | y | 0 | 301 | lower | ... > ... |
@@ -61,11 +63,13 @@
 | A.java:15:13:15:13 | y | SSA init(y) | 0 | upper | NoReason |
 | A.java:15:17:15:19 | 300 | 0 | 300 | lower | NoReason |
 | A.java:15:17:15:19 | 300 | 0 | 300 | upper | NoReason |
+| A.java:16:21:16:21 | x | 0 | 302 | lower | ... > ... |
 | A.java:16:21:16:21 | x | 0 | 400 | upper | ... > ... |
 | A.java:16:21:16:21 | x | SSA init(x) | 0 | lower | NoReason |
 | A.java:16:21:16:21 | x | SSA init(x) | 0 | upper | NoReason |
 | A.java:16:21:16:21 | x | SSA init(y) | 1 | lower | ... != ... |
 | A.java:16:21:16:21 | x | SSA init(y) | 1 | upper | ... != ... |
+| A.java:16:21:16:25 | ... + ... | 0 | 303 | lower | ... > ... |
 | A.java:16:21:16:25 | ... + ... | SSA init(x) | 1 | lower | NoReason |
 | A.java:16:21:16:25 | ... + ... | SSA init(y) | 2 | lower | ... != ... |
 | A.java:16:25:16:25 | y | 0 | 301 | lower | ... > ... |
@@ -141,17 +145,24 @@
 | A.java:34:50:34:50 | z | SSA init(z) | 0 | upper | NoReason |
 | A.java:34:55:34:57 | 350 | 0 | 350 | lower | NoReason |
 | A.java:34:55:34:57 | 350 | 0 | 350 | upper | NoReason |
-| A.java:35:16:35:16 | x | 0 | 400 | upper | ... > ... |
+| A.java:35:16:35:16 | x | 0 | 349 | lower | ... == ... |
+| A.java:35:16:35:16 | x | 0 | 349 | upper | ... == ... |
 | A.java:35:16:35:16 | x | SSA init(x) | 0 | lower | NoReason |
 | A.java:35:16:35:16 | x | SSA init(x) | 0 | upper | NoReason |
 | A.java:35:16:35:16 | x | SSA init(y) | 1 | lower | ... == ... |
 | A.java:35:16:35:16 | x | SSA init(y) | 1 | upper | ... == ... |
+| A.java:35:16:35:16 | x | SSA init(z) | -1 | lower | ... == ... |
+| A.java:35:16:35:16 | x | SSA init(z) | -1 | upper | ... == ... |
+| A.java:35:16:35:20 | ... + ... | 0 | 350 | lower | ... == ... |
 | A.java:35:16:35:20 | ... + ... | SSA init(x) | 1 | lower | NoReason |
 | A.java:35:16:35:20 | ... + ... | SSA init(y) | 2 | lower | ... == ... |
+| A.java:35:16:35:20 | ... + ... | SSA init(z) | 0 | lower | ... == ... |
+| A.java:35:16:35:24 | ... + ... | 0 | 351 | lower | ... == ... |
 | A.java:35:16:35:24 | ... + ... | SSA init(x) | 2 | lower | NoReason |
 | A.java:35:16:35:24 | ... + ... | SSA init(y) | 3 | lower | ... == ... |
-| A.java:35:20:35:20 | y | 0 | 301 | lower | ... > ... |
-| A.java:35:20:35:20 | y | 0 | 399 | upper | ... == ... |
+| A.java:35:16:35:24 | ... + ... | SSA init(z) | 1 | lower | ... == ... |
+| A.java:35:20:35:20 | y | 0 | 348 | lower | ... == ... |
+| A.java:35:20:35:20 | y | 0 | 348 | upper | ... == ... |
 | A.java:35:20:35:20 | y | SSA init(x) | -1 | lower | ... == ... |
 | A.java:35:20:35:20 | y | SSA init(x) | -1 | upper | ... == ... |
 | A.java:35:20:35:20 | y | SSA init(y) | 0 | lower | NoReason |