Skip to content

Dataflow: Restrict partial flow to either forward or reverse flow. #14599

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

Merged
MathiasVP merged 3 commits into from
Oct 26, 2023
Merged

Dataflow: Restrict partial flow to either forward or reverse flow. #14599

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4dca4a7
Dataflow: Restrict partial flow to either forward or reverse flow.
aschackmull Oct 26, 2023
a2e3b37
Dataflow: Fix accidental visibility.
aschackmull Oct 26, 2023
bbc3cfb
Dataflow: Fix documentation.
aschackmull Oct 26, 2023
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
12 changes: 5 additions & 7 deletions ...odeql/writing-codeql-queries/debugging-data-flow-queries-using-partial-flow.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ Partial flow

A naive next step could be to change the sink definition to ``any()``. This would mean that we would get a lot of flow to all the places that are reachable from the sources. While this approach may work in some cases, you might find that it produces so many results that it's very hard to explore the findings. It can also dramatically affect query performance. More importantly, you might not even see all the partial flow paths. This is because the data-flow library tries very hard to prune impossible paths and, since field stores and reads must be evenly matched along a path, we will never see paths going through a store that fail to reach a corresponding read. This can make it hard to see where flow actually stops.

To avoid these problems, the data-flow library comes with a mechanism for exploring partial flow that tries to deal with these caveats. This is the ``MyFlow::FlowExploration<explorationLimit/0>::partialFlow`` predicate:
To avoid these problems, the data-flow library comes with a mechanism for exploring partial flow that tries to deal with these caveats. This is the ``MyFlow::FlowExplorationFwd<explorationLimit/0>::partialFlow`` predicate:

.. code-block:: ql

Expand All @@ -77,21 +77,19 @@ To avoid these problems, the data-flow library comes with a mechanism for explor
*/
predicate partialFlow(PartialPathNode source, PartialPathNode node, int dist) {

There is also a ``partialFlowRev`` for exploring flow backwards from a sink.
There is also a ``MyFlow::FlowExplorationRev<explorationLimit/0>::partialFlow`` for exploring flow backwards from a sink.

To get access to these predicates you must instantiate the ``MyFlow::FlowExploration<>`` module with an exploration limit. For example:
To get access to these predicates you must instantiate the ``MyFlow::FlowExplorationFwd<>`` module with an exploration limit (or the ``MyFlow::FlowExplorationRev<>`` module for reverse flow). For example:

.. code-block:: ql

int explorationLimit() { result = 5 }

module MyPartialFlow = MyFlow::FlowExploration<explorationLimit/0>;
module MyPartialFlow = MyFlow::FlowExplorationFwd<explorationLimit/0>;

This defines the exploration radius within which ``partialFlow`` returns results.

To get good performance when using ``partialFlow`` it is important to ensure the ``isSink`` predicate of the configuration has no results. Likewise, when using ``partialFlowRev`` the ``isSource`` predicate of the configuration should have no results.

It is also useful to focus on a single source at a time as the starting point for the flow exploration. This is most easily done by adding a temporary restriction in the ``isSource`` predicate.
It is useful to focus on a single source at a time as the starting point for the flow exploration. This is most easily done by adding a temporary restriction in the ``isSource`` predicate.

To do quick evaluations of partial flow it is often easiest to add a predicate to the query that is solely intended for quick evaluation (right-click the predicate name and choose "CodeQL: Quick Evaluation"). A good starting point is something like:

Expand Down
182 changes: 105 additions & 77 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 @@ -4357,7 +4357,29 @@ module MakeImpl<InputSig Lang> {
tftuples = -1
}

module FlowExploration<explorationLimitSig/0 explorationLimit> {
private signature predicate flag();

private predicate flagEnable() { any() }

private predicate flagDisable() { none() }

module FlowExplorationFwd<explorationLimitSig/0 explorationLimit> {
private import FlowExploration<explorationLimit/0, flagEnable/0, flagDisable/0>
import Public

predicate partialFlow = partialFlowFwd/3;
}

module FlowExplorationRev<explorationLimitSig/0 explorationLimit> {
private import FlowExploration<explorationLimit/0, flagDisable/0, flagEnable/0>
import Public

predicate partialFlow = partialFlowRev/3;
}

private module FlowExploration<
explorationLimitSig/0 explorationLimit, flag/0 flagFwd, flag/0 flagRev>
{
private predicate callableStep(DataFlowCallable c1, DataFlowCallable c2) {
exists(NodeEx node1, NodeEx node2 |
jumpStepEx(node1, node2)
Expand Down Expand Up @@ -4526,6 +4548,7 @@ module MakeImpl<InputSig Lang> {
NodeEx node, FlowState state, CallContext cc, TSummaryCtx1 sc1, TSummaryCtx2 sc2,
TSummaryCtx3 sc3, TSummaryCtx4 sc4, DataFlowType t, PartialAccessPath ap
) {
flagFwd() and
sourceNode(node, state) and
cc instanceof CallContextAny and
sc1 = TSummaryCtx1None() and
Expand All @@ -4543,6 +4566,7 @@ module MakeImpl<InputSig Lang> {
NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
TRevSummaryCtx3 sc3, PartialAccessPath ap
) {
flagRev() and
revSinkNode(node, state) and
sc1 = TRevSummaryCtx1None() and
sc2 = TRevSummaryCtx2None() and
Expand Down Expand Up @@ -4595,96 +4619,100 @@ module MakeImpl<InputSig Lang> {
partialPathStep1(_, _, _, _, _, _, _, _, t0, t, ap) and t0 != t
}

/**
* A `Node` augmented with a call context, an access path, and a configuration.
*/
class PartialPathNode extends TPartialPathNode {
/** Gets a textual representation of this element. */
string toString() { result = this.getNodeEx().toString() + this.ppType() + this.ppAp() }

module Public {
/**
* Gets a textual representation of this element, including a textual
* representation of the call context.
* A `Node` augmented with a call context, an access path, and a configuration.
*/
string toStringWithContext() {
result = this.getNodeEx().toString() + this.ppType() + this.ppAp() + this.ppCtx()
}
class PartialPathNode extends TPartialPathNode {
/** Gets a textual representation of this element. */
string toString() { result = this.getNodeEx().toString() + this.ppType() + this.ppAp() }

/**
* Gets a textual representation of this element, including a textual
* representation of the call context.
*/
string toStringWithContext() {
result = this.getNodeEx().toString() + this.ppType() + this.ppAp() + this.ppCtx()
}

/**
* Holds if this element is at the specified location.
* The location spans column `startcolumn` of line `startline` to
* column `endcolumn` of line `endline` in file `filepath`.
* For more information, see
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
*/
predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
this.getNodeEx().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
}
/**
* Holds if this element is at the specified location.
* The location spans column `startcolumn` of line `startline` to
* column `endcolumn` of line `endline` in file `filepath`.
* For more information, see
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
*/
predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
this.getNodeEx().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
}

/** Gets the underlying `Node`. */
final Node getNode() { this.getNodeEx().projectToNode() = result }
/** Gets the underlying `Node`. */
final Node getNode() { this.getNodeEx().projectToNode() = result }

FlowState getState() { none() }
FlowState getState() { none() }

private NodeEx getNodeEx() {
result = this.(PartialPathNodeFwd).getNodeEx() or
result = this.(PartialPathNodeRev).getNodeEx()
}
private NodeEx getNodeEx() {
result = this.(PartialPathNodeFwd).getNodeEx() or
result = this.(PartialPathNodeRev).getNodeEx()
}

/** Gets a successor of this node, if any. */
PartialPathNode getASuccessor() { none() }
/** Gets a successor of this node, if any. */
PartialPathNode getASuccessor() { none() }

/**
* Gets the approximate distance to the nearest source measured in number
* of interprocedural steps.
*/
int getSourceDistance() { result = distSrc(this.getNodeEx().getEnclosingCallable()) }
/**
* Gets the approximate distance to the nearest source measured in number
* of interprocedural steps.
*/
int getSourceDistance() { result = distSrc(this.getNodeEx().getEnclosingCallable()) }

/**
* Gets the approximate distance to the nearest sink measured in number
* of interprocedural steps.
*/
int getSinkDistance() { result = distSink(this.getNodeEx().getEnclosingCallable()) }
/**
* Gets the approximate distance to the nearest sink measured in number
* of interprocedural steps.
*/
int getSinkDistance() { result = distSink(this.getNodeEx().getEnclosingCallable()) }

private string ppType() {
this instanceof PartialPathNodeRev and result = ""
or
exists(DataFlowType t | t = this.(PartialPathNodeFwd).getType() |
// The `concat` becomes "" if `ppReprType` has no result.
result = concat(" : " + ppReprType(t))
)
}
private string ppType() {
this instanceof PartialPathNodeRev and result = ""
or
exists(DataFlowType t | t = this.(PartialPathNodeFwd).getType() |
// The `concat` becomes "" if `ppReprType` has no result.
result = concat(" : " + ppReprType(t))
)
}

private string ppAp() {
exists(string s |
s = this.(PartialPathNodeFwd).getAp().toString() or
s = this.(PartialPathNodeRev).getAp().toString()
|
if s = "" then result = "" else result = " " + s
)
}
private string ppAp() {
exists(string s |
s = this.(PartialPathNodeFwd).getAp().toString() or
s = this.(PartialPathNodeRev).getAp().toString()
|
if s = "" then result = "" else result = " " + s
)
}

private string ppCtx() {
result = " <" + this.(PartialPathNodeFwd).getCallContext().toString() + ">"
}
private string ppCtx() {
result = " <" + this.(PartialPathNodeFwd).getCallContext().toString() + ">"
}

/** Holds if this is a source in a forward-flow path. */
predicate isFwdSource() { this.(PartialPathNodeFwd).isSource() }
/** Holds if this is a source in a forward-flow path. */
predicate isFwdSource() { this.(PartialPathNodeFwd).isSource() }

/** Holds if this is a sink in a reverse-flow path. */
predicate isRevSink() { this.(PartialPathNodeRev).isSink() }
}
/** Holds if this is a sink in a reverse-flow path. */
predicate isRevSink() { this.(PartialPathNodeRev).isSink() }
}

/**
* Provides the query predicates needed to include a graph in a path-problem query.
*/
module PartialPathGraph {
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
query predicate edges(PartialPathNode a, PartialPathNode b) { a.getASuccessor() = b }
/**
* Provides the query predicates needed to include a graph in a path-problem query.
*/
module PartialPathGraph {
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
query predicate edges(PartialPathNode a, PartialPathNode b) { a.getASuccessor() = b }
}
}

import Public

private class PartialPathNodeFwd extends PartialPathNode, TPartialPathNodeFwd {
NodeEx node;
FlowState state;
Expand Down Expand Up @@ -5223,7 +5251,7 @@ module MakeImpl<InputSig Lang> {
)
}

private predicate partialFlow(PartialPathNode source, PartialPathNode node) {
private predicate fwdPartialFlow(PartialPathNode source, PartialPathNode node) {
source.isFwdSource() and
node = source.getASuccessor+()
}
Expand All @@ -5245,8 +5273,8 @@ module MakeImpl<InputSig Lang> {
*
* To use this in a `path-problem` query, import the module `PartialPathGraph`.
*/
predicate partialFlow(PartialPathNode source, PartialPathNode node, int dist) {
partialFlow(source, node) and
predicate partialFlowFwd(PartialPathNode source, PartialPathNode node, int dist) {
fwdPartialFlow(source, node) and
dist = node.getSourceDistance()
}

Expand Down