Module GraphPathSearch
A module that implements an efficient search for a path within a custom directional graph from a set of start nodes to a set of end nodes.
To show discovered paths to users, see the module CustomPathProblem which uses this module as
its underlying search implementation.
This module uses a pattern called “forward reverse pruning” for efficiency. This pattern is useful for reducing the search space when looking for paths in a directional graph. In a first pass, it finds nodes reachable from the starting point. In the second pass, it finds the subset of those nodes that can be reached from the end point. Together, these create a path from start points to end points.
To use this module, provide an implementation of the GraphPathSearchSig signature as follows:
module Config implements GraphPathSearchSig<Person> {
predicate start(Person p) { p.checkSomething() }
predicate edge(Person p1, Person p2) { p2 = p1.getAParent() }
predicate end(Person p) { p.checkSomethingElse() }
}
The design of these predicate has a great effect in how well this performance pattern will ultimately perform.
The resulting predicate hasPath should be a much more efficient search of connected start nodes
to end nodes than a naive search (which in CodeQL could easily be evaluated as either a full
graph search, or a search over the cross product of all nodes).
from Person p1, Person p2
// Fast graph path detection thanks to forward-reverse pruning.
where GraphPathSearch<Person, Config>::hasPath(p1, p2)
select p1, p2
The resulting module also exposes two classes:
ForwardNode: All nodes reachable from the start nodes.ReverseNode: All forward nodes that reach end nodes.
These classes may be useful in addition to the hasPath predicate.
Import path
import qtil.graph.GraphPathSearchPredicates
| hasConnection | A start node, end node pair that are connected in the graph. |
| hasPath | A performant path search within a custom directed graph from a set of start nodes to a set of end nodes. |
| pathEdge | All relevant edges in the graph which participate in a connection from a start to an end node. |
Classes
| ForwardNode | The set of all nodes reachable from the start nodes (inclusive). |
| ReverseNode | The set of all forward nodes that reach end nodes (inclusive). |