From 0afda68ba100cbf8b7e016031f4c96835e642ab9 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 17 Aug 2023 11:07:24 +0200 Subject: [PATCH 1/2] Java: Join-order fix in RangeAnalysis. --- .../code/java/dataflow/RangeAnalysis.qll | 20 ++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll index 53c0a83a536..4af0145bee3 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -257,11 +257,21 @@ private Guard boundFlowCond(SsaVariable v, Expr e, int delta, boolean upper, boo 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) + exists(SsaVariable v2, int d | + // equality needs to control guard + result.getBasicBlock() = eqSsaCondDirectlyControls(v, v2, d) and + result = boundFlowCond(v2, e, delta - d, upper, testIsTrue) + ) +} + +/** + * Gets a basic block in which `v1` equals `v2 + delta`. + */ +private BasicBlock eqSsaCondDirectlyControls(SsaVariable v1, SsaVariable v2, int delta) { + exists(Guard guardEq, int d1, int d2, boolean eqIsTrue | + guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and + delta = d2 - d1 and + guardEq.directlyControls(result, eqIsTrue) ) } From f8a0b6cd22dd6e05b1da71c1c8bd898a4849d51d Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 17 Aug 2023 11:20:02 +0200 Subject: [PATCH 2/2] Java: Add nomagic --- java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll | 1 + 1 file changed, 1 insertion(+) diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll index 4af0145bee3..8cdef89c6ab 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -267,6 +267,7 @@ private Guard boundFlowCond(SsaVariable v, Expr e, int delta, boolean upper, boo /** * Gets a basic block in which `v1` equals `v2 + delta`. */ +pragma[nomagic] private BasicBlock eqSsaCondDirectlyControls(SsaVariable v1, SsaVariable v2, int delta) { exists(Guard guardEq, int d1, int d2, boolean eqIsTrue | guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and