Skip to content

Dataflow/prune to shortestpath2 #22428

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
aschackmull wants to merge 3 commits into
base: main
Choose a base branch
from
+71 −11
Draft

Dataflow/prune to shortestpath2 #22428

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
32c527f
Dataflow: test
aschackmull Aug 26, 2026
4fdb823
try slack=15
aschackmull Aug 26, 2026
e23a7e4
Account for all pairs in cartesian combinations
aschackmull Aug 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
82 changes: 71 additions & 11 deletions shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2497,14 +2497,78 @@ module MakeImpl<LocationSig Location, InputSig<Location> 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() }

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 srcSinkDiff() {
exists(PathNodeImpl src, PathNodeImpl sink |
pathSuccPlus(src, sink) and
result = sinkDist(src) - srcDist(sink)
)
}

private int pathLength() {
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)) and
srcSpread = max(srcSinkDiff()) and
sinkSpread = max(-srcSinkDiff())
)
}

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.
*/
private predicate retReach(PathNodeImpl n) {
fwdReach(n) and
(
exists(PathNodeImpl out | subpaths2(_, _, n, out) |
directReach(out) or retReach(out)
directReach_2(out) or retReach(out)
)
or
exists(PathNodeImpl mid |
Expand All @@ -2516,7 +2580,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> 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.
Expand Down Expand Up @@ -2567,16 +2631,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> 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 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`.
Expand All @@ -2600,7 +2660,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> 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()
)
}
Expand Down
Loading