From 32c527f3c25a85326ca5755577e90123117c3dcf Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 26 Aug 2026 10:19:06 +0200 Subject: [PATCH 1/3] Dataflow: test --- .../codeql/dataflow/internal/DataFlowImpl.qll | 48 +++++++++++++++++-- 1 file changed, 45 insertions(+), 3 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index e467e6caa708..0c94591fa105 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -2497,6 +2497,48 @@ module MakeImpl Lang> { ) } + private module DistancePruning { + private predicate isAnySource(PathNodeImpl n) { n.isArbitrarySource() } + + private predicate isAnySink(PathNodeImpl n) { n.isArbitrarySink() } + + private predicate directStep(PathNodeImpl n1, PathNodeImpl n2) { + n1.getANonHiddenSuccessor(_) = n2 and directReach(n2) + } + + private predicate directStepRev(PathNodeImpl n1, PathNodeImpl n2) { + directStep(n2, n1) + } + + private int srcDist1(PathNodeImpl n) = + shortestDistances(isAnySource/1, directStep/2)(_, n, result) + + private int sinkDist1(PathNodeImpl n) = + shortestDistances(isAnySink/1, directStepRev/2)(_, n, result) + + private int srcDist(PathNodeImpl n) { result = srcDist1(n) - 1 } + + private int sinkDist(PathNodeImpl n) { result = sinkDist1(n) - 1 } + + private int pathLength() { + exists(int fwdLen, int revLen | + result = fwdLen.maximum(revLen) and + fwdLen = max(PathNodeImpl n | n.isSink() | srcDist(n)) and + revLen = max(PathNodeImpl n | n.isSource() | sinkDist(n)) + ) + } + + private int slack() { result = 0 } + + predicate nearShortestDirectReach(PathNodeImpl n) { + directReach(n) and + srcDist(n) + sinkDist(n) <= pathLength() + slack() + } + } + + // private predicate directReach_2 = directReach/1; + private predicate directReach_2 = DistancePruning::nearShortestDirectReach/1; + /** * Holds if `n` can reach a return node in a summarized subpath that can reach a sink. */ @@ -2504,7 +2546,7 @@ module MakeImpl Lang> { fwdReach(n) and ( exists(PathNodeImpl out | subpaths2(_, _, n, out) | - directReach(out) or retReach(out) + directReach_2(out) or retReach(out) ) or exists(PathNodeImpl mid | @@ -2516,7 +2558,7 @@ module MakeImpl Lang> { } /** Holds if `n` can reach a sink or is used in a subpath that can reach a sink. */ - private predicate reach(PathNodeImpl n) { directReach(n) or retReach(n) } + private predicate reach(PathNodeImpl n) { directReach_2(n) or retReach(n) } /** * A `Node` augmented with a call context (except for sinks) and an access path. @@ -2568,7 +2610,7 @@ module MakeImpl Lang> { /** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */ private predicate pathSucc(PathNodeImpl n1, PathNodeImpl n2) { - n1.getANonHiddenSuccessor(_) = n2 and directReach(n2) + n1.getANonHiddenSuccessor(_) = n2 and directReach_2(n2) } private predicate tcSrc(PathNodeImpl n) { n.isSource() } From 4fdb8238e63c2f1bd9e18fbd461b02b663bd420d Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 26 Aug 2026 11:47:55 +0200 Subject: [PATCH 2/3] try slack=15 --- shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 0c94591fa105..bf906bdb1041 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -2528,7 +2528,7 @@ module MakeImpl Lang> { ) } - private int slack() { result = 0 } + private int slack() { result = 15 } predicate nearShortestDirectReach(PathNodeImpl n) { directReach(n) and From e23a7e40aba7a3133ea85455cae98a520820ef5c Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 26 Aug 2026 14:24:02 +0200 Subject: [PATCH 3/3] Account for all pairs in cartesian combinations --- .../codeql/dataflow/internal/DataFlowImpl.qll | 42 +++++++++++++------ 1 file changed, 30 insertions(+), 12 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index bf906bdb1041..9b8cd0397330 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -2497,6 +2497,18 @@ module MakeImpl Lang> { ) } + /** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */ + private predicate pathSucc(PathNodeImpl n1, PathNodeImpl n2) { + n1.getANonHiddenSuccessor(_) = n2 and directReach(n2) + } + + private predicate tcSrc(PathNodeImpl n) { n.isSource() } + + private predicate tcSink(PathNodeImpl n) { n.isSink() } + + private predicate pathSuccPlus(PathNodeImpl n1, PathNodeImpl n2) = + doublyBoundedFastTC(pathSucc/2, tcSrc/1, tcSink/1)(n1, n2) + private module DistancePruning { private predicate isAnySource(PathNodeImpl n) { n.isArbitrarySource() } @@ -2520,15 +2532,25 @@ module MakeImpl Lang> { private int sinkDist(PathNodeImpl n) { result = sinkDist1(n) - 1 } + private int srcSinkDiff() { + exists(PathNodeImpl src, PathNodeImpl sink | + pathSuccPlus(src, sink) and + result = sinkDist(src) - srcDist(sink) + ) + } + private int pathLength() { - exists(int fwdLen, int revLen | - result = fwdLen.maximum(revLen) and + exists(int fwdLen, int revLen, int srcSpread, int sinkSpread | + // result = fwdLen.maximum(revLen) and + result = (fwdLen + revLen + srcSpread + sinkSpread) / 2 and fwdLen = max(PathNodeImpl n | n.isSink() | srcDist(n)) and - revLen = max(PathNodeImpl n | n.isSource() | sinkDist(n)) + revLen = max(PathNodeImpl n | n.isSource() | sinkDist(n)) and + srcSpread = max(srcSinkDiff()) and + sinkSpread = max(-srcSinkDiff()) ) } - private int slack() { result = 15 } + private int slack() { result = 0 } predicate nearShortestDirectReach(PathNodeImpl n) { directReach(n) and @@ -2609,16 +2631,12 @@ module MakeImpl Lang> { } /** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */ - private predicate pathSucc(PathNodeImpl n1, PathNodeImpl n2) { + private predicate pathSucc_2(PathNodeImpl n1, PathNodeImpl n2) { n1.getANonHiddenSuccessor(_) = n2 and directReach_2(n2) } - private predicate tcSrc(PathNodeImpl n) { n.isSource() } - - private predicate tcSink(PathNodeImpl n) { n.isSink() } - - private predicate pathSuccPlus(PathNodeImpl n1, PathNodeImpl n2) = - doublyBoundedFastTC(pathSucc/2, tcSrc/1, tcSink/1)(n1, n2) + private predicate pathSuccPlus_2(PathNodeImpl n1, PathNodeImpl n2) = + doublyBoundedFastTC(pathSucc_2/2, tcSrc/1, tcSink/1)(n1, n2) /** * Holds if data can flow from `source` to `sink`. @@ -2642,7 +2660,7 @@ module MakeImpl Lang> { source = flowsource and sink = flowsink | flowsource.isSource() and - (flowsource = flowsink or pathSuccPlus(flowsource, flowsink)) and + (flowsource = flowsink or pathSuccPlus_2(flowsource, flowsink)) and flowsink.isSink() ) }