Skip to content

Commit e23a7e4

Browse files
committed
Account for all pairs in cartesian combinations
1 parent 4fdb823 commit e23a7e4

1 file changed

Lines changed: 30 additions & 12 deletions

File tree

shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll

Lines changed: 30 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -2497,6 +2497,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
24972497
)
24982498
}
24992499

2500+
/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
2501+
private predicate pathSucc(PathNodeImpl n1, PathNodeImpl n2) {
2502+
n1.getANonHiddenSuccessor(_) = n2 and directReach(n2)
2503+
}
2504+
2505+
private predicate tcSrc(PathNodeImpl n) { n.isSource() }
2506+
2507+
private predicate tcSink(PathNodeImpl n) { n.isSink() }
2508+
2509+
private predicate pathSuccPlus(PathNodeImpl n1, PathNodeImpl n2) =
2510+
doublyBoundedFastTC(pathSucc/2, tcSrc/1, tcSink/1)(n1, n2)
2511+
25002512
private module DistancePruning {
25012513
private predicate isAnySource(PathNodeImpl n) { n.isArbitrarySource() }
25022514

@@ -2520,15 +2532,25 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
25202532

25212533
private int sinkDist(PathNodeImpl n) { result = sinkDist1(n) - 1 }
25222534

2535+
private int srcSinkDiff() {
2536+
exists(PathNodeImpl src, PathNodeImpl sink |
2537+
pathSuccPlus(src, sink) and
2538+
result = sinkDist(src) - srcDist(sink)
2539+
)
2540+
}
2541+
25232542
private int pathLength() {
2524-
exists(int fwdLen, int revLen |
2525-
result = fwdLen.maximum(revLen) and
2543+
exists(int fwdLen, int revLen, int srcSpread, int sinkSpread |
2544+
// result = fwdLen.maximum(revLen) and
2545+
result = (fwdLen + revLen + srcSpread + sinkSpread) / 2 and
25262546
fwdLen = max(PathNodeImpl n | n.isSink() | srcDist(n)) and
2527-
revLen = max(PathNodeImpl n | n.isSource() | sinkDist(n))
2547+
revLen = max(PathNodeImpl n | n.isSource() | sinkDist(n)) and
2548+
srcSpread = max(srcSinkDiff()) and
2549+
sinkSpread = max(-srcSinkDiff())
25282550
)
25292551
}
25302552

2531-
private int slack() { result = 15 }
2553+
private int slack() { result = 0 }
25322554

25332555
predicate nearShortestDirectReach(PathNodeImpl n) {
25342556
directReach(n) and
@@ -2609,16 +2631,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26092631
}
26102632

26112633
/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
2612-
private predicate pathSucc(PathNodeImpl n1, PathNodeImpl n2) {
2634+
private predicate pathSucc_2(PathNodeImpl n1, PathNodeImpl n2) {
26132635
n1.getANonHiddenSuccessor(_) = n2 and directReach_2(n2)
26142636
}
26152637

2616-
private predicate tcSrc(PathNodeImpl n) { n.isSource() }
2617-
2618-
private predicate tcSink(PathNodeImpl n) { n.isSink() }
2619-
2620-
private predicate pathSuccPlus(PathNodeImpl n1, PathNodeImpl n2) =
2621-
doublyBoundedFastTC(pathSucc/2, tcSrc/1, tcSink/1)(n1, n2)
2638+
private predicate pathSuccPlus_2(PathNodeImpl n1, PathNodeImpl n2) =
2639+
doublyBoundedFastTC(pathSucc_2/2, tcSrc/1, tcSink/1)(n1, n2)
26222640

26232641
/**
26242642
* Holds if data can flow from `source` to `sink`.
@@ -2642,7 +2660,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26422660
source = flowsource and sink = flowsink
26432661
|
26442662
flowsource.isSource() and
2645-
(flowsource = flowsink or pathSuccPlus(flowsource, flowsink)) and
2663+
(flowsource = flowsink or pathSuccPlus_2(flowsource, flowsink)) and
26462664
flowsink.isSink()
26472665
)
26482666
}

0 commit comments

Comments
 (0)