From d9dfcb2132515a0d2f54d4cde81f1d7d6a804220 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Mar 2022 15:07:09 +0000 Subject: [PATCH 1/3] Improve join order for RangeAnalysis::boundedPhi --- .../semmle/code/java/dataflow/RangeAnalysis.qll | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll index de7aca884342..d3556c1ff67b 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -725,6 +725,16 @@ private predicate boundedPhiCandValidForEdge( ) } +pragma[noinline] +private predicate boundedPhiCand2( + SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta, + Reason reason +) { + exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) | + boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge) + ) +} + /** * Holds if `b + delta` is a valid bound for `phi`. * - `upper = true` : `phi <= b + delta` @@ -734,7 +744,11 @@ private predicate boundedPhi( SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta, Reason reason ) { - forex(SsaVariable inp, SsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) | + // Forcibly split into an existence and a forall stage instead of using forex because otherwise + // for certain seminaive variants we would try to postpone restricting by `edge.phiInput(phi, inp)` + // until too late in the process. + boundedPhiCand2(phi, b, delta, upper, fromBackEdge, origdelta, reason) and + forall(SsaVariable inp, SsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) | boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge) ) } From c4aabcef6c1e7fa1ffe3c6daa49ed0a4da5cd15f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Mar 2022 20:55:47 +0000 Subject: [PATCH 2/3] Force CI --- 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 d3556c1ff67b..a4e1741d4991 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -894,3 +894,4 @@ private predicate boundedConditionalExpr( ) { bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason) } + From 8fbdfd52b8e5277396e41d1e5e345eb9562fe2cf Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 10 Mar 2022 20:56:26 +0000 Subject: [PATCH 3/3] Force CI --- java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll | 1 - 1 file changed, 1 deletion(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll index a4e1741d4991..d3556c1ff67b 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -894,4 +894,3 @@ private predicate boundedConditionalExpr( ) { bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason) } -