Skip to content

Commit f53a05b

Browse files
authored
Merge pull request github#12475 from aschackmull/dataflow/mergepathgraph
Dataflow: Add MergePathGraph module.
2 parents a0fca20 + c380ecb commit f53a05b

File tree

24 files changed

+1005
-9
lines changed

24 files changed

+1005
-9
lines changed
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
---
2+
category: feature
3+
---
4+
* Added support for merging two `PathGraph`s via disjoint union to allow results from multiple data flow computations in a single `path-problem` query.

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlow.qll

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -243,3 +243,111 @@ module MakeWithState<StateConfigSig Config> implements DataFlowSig {
243243

244244
import Impl<C>
245245
}
246+
247+
signature class PathNodeSig {
248+
/** Gets a textual representation of this element. */
249+
string toString();
250+
251+
/**
252+
* Holds if this element is at the specified location.
253+
* The location spans column `startcolumn` of line `startline` to
254+
* column `endcolumn` of line `endline` in file `filepath`.
255+
* For more information, see
256+
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
257+
*/
258+
predicate hasLocationInfo(
259+
string filepath, int startline, int startcolumn, int endline, int endcolumn
260+
);
261+
262+
/** Gets the underlying `Node`. */
263+
Node getNode();
264+
}
265+
266+
signature module PathGraphSig<PathNodeSig PathNode> {
267+
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
268+
predicate edges(PathNode a, PathNode b);
269+
270+
/** Holds if `n` is a node in the graph of data flow path explanations. */
271+
predicate nodes(PathNode n, string key, string val);
272+
273+
/**
274+
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
275+
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
276+
* `ret -> out` is summarized as the edge `arg -> out`.
277+
*/
278+
predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out);
279+
}
280+
281+
/**
282+
* Constructs a `PathGraph` from two `PathGraph`s by disjoint union.
283+
*/
284+
module MergePathGraph<
285+
PathNodeSig PathNode1, PathNodeSig PathNode2, PathGraphSig<PathNode1> Graph1,
286+
PathGraphSig<PathNode2> Graph2>
287+
{
288+
private newtype TPathNode =
289+
TPathNode1(PathNode1 p) or
290+
TPathNode2(PathNode2 p)
291+
292+
/** A node in a graph of path explanations that is formed by disjoint union of the two given graphs. */
293+
class PathNode extends TPathNode {
294+
/** Gets this as a projection on the first given `PathGraph`. */
295+
PathNode1 asPathNode1() { this = TPathNode1(result) }
296+
297+
/** Gets this as a projection on the second given `PathGraph`. */
298+
PathNode2 asPathNode2() { this = TPathNode2(result) }
299+
300+
/** Gets a textual representation of this element. */
301+
string toString() {
302+
result = this.asPathNode1().toString() or
303+
result = this.asPathNode2().toString()
304+
}
305+
306+
/**
307+
* Holds if this element is at the specified location.
308+
* The location spans column `startcolumn` of line `startline` to
309+
* column `endcolumn` of line `endline` in file `filepath`.
310+
* For more information, see
311+
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
312+
*/
313+
predicate hasLocationInfo(
314+
string filepath, int startline, int startcolumn, int endline, int endcolumn
315+
) {
316+
this.asPathNode1().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) or
317+
this.asPathNode2().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
318+
}
319+
320+
/** Gets the underlying `Node`. */
321+
Node getNode() {
322+
result = this.asPathNode1().getNode() or
323+
result = this.asPathNode2().getNode()
324+
}
325+
}
326+
327+
/**
328+
* Provides the query predicates needed to include a graph in a path-problem query.
329+
*/
330+
module PathGraph implements PathGraphSig<PathNode> {
331+
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
332+
query predicate edges(PathNode a, PathNode b) {
333+
Graph1::edges(a.asPathNode1(), b.asPathNode1()) or
334+
Graph2::edges(a.asPathNode2(), b.asPathNode2())
335+
}
336+
337+
/** Holds if `n` is a node in the graph of data flow path explanations. */
338+
query predicate nodes(PathNode n, string key, string val) {
339+
Graph1::nodes(n.asPathNode1(), key, val) or
340+
Graph2::nodes(n.asPathNode2(), key, val)
341+
}
342+
343+
/**
344+
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
345+
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
346+
* `ret -> out` is summarized as the edge `arg -> out`.
347+
*/
348+
query predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out) {
349+
Graph1::subpaths(arg.asPathNode1(), par.asPathNode1(), ret.asPathNode1(), out.asPathNode1()) or
350+
Graph2::subpaths(arg.asPathNode2(), par.asPathNode2(), ret.asPathNode2(), out.asPathNode2())
351+
}
352+
}
353+
}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3157,7 +3157,7 @@ module Impl<FullStateConfigSig Config> {
31573157
/**
31583158
* Provides the query predicates needed to include a graph in a path-problem query.
31593159
*/
3160-
module PathGraph {
3160+
module PathGraph implements PathGraphSig<PathNode> {
31613161
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
31623162
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b }
31633163

cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlow.qll

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -243,3 +243,111 @@ module MakeWithState<StateConfigSig Config> implements DataFlowSig {
243243

244244
import Impl<C>
245245
}
246+
247+
signature class PathNodeSig {
248+
/** Gets a textual representation of this element. */
249+
string toString();
250+
251+
/**
252+
* Holds if this element is at the specified location.
253+
* The location spans column `startcolumn` of line `startline` to
254+
* column `endcolumn` of line `endline` in file `filepath`.
255+
* For more information, see
256+
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
257+
*/
258+
predicate hasLocationInfo(
259+
string filepath, int startline, int startcolumn, int endline, int endcolumn
260+
);
261+
262+
/** Gets the underlying `Node`. */
263+
Node getNode();
264+
}
265+
266+
signature module PathGraphSig<PathNodeSig PathNode> {
267+
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
268+
predicate edges(PathNode a, PathNode b);
269+
270+
/** Holds if `n` is a node in the graph of data flow path explanations. */
271+
predicate nodes(PathNode n, string key, string val);
272+
273+
/**
274+
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
275+
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
276+
* `ret -> out` is summarized as the edge `arg -> out`.
277+
*/
278+
predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out);
279+
}
280+
281+
/**
282+
* Constructs a `PathGraph` from two `PathGraph`s by disjoint union.
283+
*/
284+
module MergePathGraph<
285+
PathNodeSig PathNode1, PathNodeSig PathNode2, PathGraphSig<PathNode1> Graph1,
286+
PathGraphSig<PathNode2> Graph2>
287+
{
288+
private newtype TPathNode =
289+
TPathNode1(PathNode1 p) or
290+
TPathNode2(PathNode2 p)
291+
292+
/** A node in a graph of path explanations that is formed by disjoint union of the two given graphs. */
293+
class PathNode extends TPathNode {
294+
/** Gets this as a projection on the first given `PathGraph`. */
295+
PathNode1 asPathNode1() { this = TPathNode1(result) }
296+
297+
/** Gets this as a projection on the second given `PathGraph`. */
298+
PathNode2 asPathNode2() { this = TPathNode2(result) }
299+
300+
/** Gets a textual representation of this element. */
301+
string toString() {
302+
result = this.asPathNode1().toString() or
303+
result = this.asPathNode2().toString()
304+
}
305+
306+
/**
307+
* Holds if this element is at the specified location.
308+
* The location spans column `startcolumn` of line `startline` to
309+
* column `endcolumn` of line `endline` in file `filepath`.
310+
* For more information, see
311+
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
312+
*/
313+
predicate hasLocationInfo(
314+
string filepath, int startline, int startcolumn, int endline, int endcolumn
315+
) {
316+
this.asPathNode1().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) or
317+
this.asPathNode2().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
318+
}
319+
320+
/** Gets the underlying `Node`. */
321+
Node getNode() {
322+
result = this.asPathNode1().getNode() or
323+
result = this.asPathNode2().getNode()
324+
}
325+
}
326+
327+
/**
328+
* Provides the query predicates needed to include a graph in a path-problem query.
329+
*/
330+
module PathGraph implements PathGraphSig<PathNode> {
331+
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
332+
query predicate edges(PathNode a, PathNode b) {
333+
Graph1::edges(a.asPathNode1(), b.asPathNode1()) or
334+
Graph2::edges(a.asPathNode2(), b.asPathNode2())
335+
}
336+
337+
/** Holds if `n` is a node in the graph of data flow path explanations. */
338+
query predicate nodes(PathNode n, string key, string val) {
339+
Graph1::nodes(n.asPathNode1(), key, val) or
340+
Graph2::nodes(n.asPathNode2(), key, val)
341+
}
342+
343+
/**
344+
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
345+
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
346+
* `ret -> out` is summarized as the edge `arg -> out`.
347+
*/
348+
query predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out) {
349+
Graph1::subpaths(arg.asPathNode1(), par.asPathNode1(), ret.asPathNode1(), out.asPathNode1()) or
350+
Graph2::subpaths(arg.asPathNode2(), par.asPathNode2(), ret.asPathNode2(), out.asPathNode2())
351+
}
352+
}
353+
}

cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3157,7 +3157,7 @@ module Impl<FullStateConfigSig Config> {
31573157
/**
31583158
* Provides the query predicates needed to include a graph in a path-problem query.
31593159
*/
3160-
module PathGraph {
3160+
module PathGraph implements PathGraphSig<PathNode> {
31613161
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
31623162
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b }
31633163

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlow.qll

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -243,3 +243,111 @@ module MakeWithState<StateConfigSig Config> implements DataFlowSig {
243243

244244
import Impl<C>
245245
}
246+
247+
signature class PathNodeSig {
248+
/** Gets a textual representation of this element. */
249+
string toString();
250+
251+
/**
252+
* Holds if this element is at the specified location.
253+
* The location spans column `startcolumn` of line `startline` to
254+
* column `endcolumn` of line `endline` in file `filepath`.
255+
* For more information, see
256+
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
257+
*/
258+
predicate hasLocationInfo(
259+
string filepath, int startline, int startcolumn, int endline, int endcolumn
260+
);
261+
262+
/** Gets the underlying `Node`. */
263+
Node getNode();
264+
}
265+
266+
signature module PathGraphSig<PathNodeSig PathNode> {
267+
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
268+
predicate edges(PathNode a, PathNode b);
269+
270+
/** Holds if `n` is a node in the graph of data flow path explanations. */
271+
predicate nodes(PathNode n, string key, string val);
272+
273+
/**
274+
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
275+
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
276+
* `ret -> out` is summarized as the edge `arg -> out`.
277+
*/
278+
predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out);
279+
}
280+
281+
/**
282+
* Constructs a `PathGraph` from two `PathGraph`s by disjoint union.
283+
*/
284+
module MergePathGraph<
285+
PathNodeSig PathNode1, PathNodeSig PathNode2, PathGraphSig<PathNode1> Graph1,
286+
PathGraphSig<PathNode2> Graph2>
287+
{
288+
private newtype TPathNode =
289+
TPathNode1(PathNode1 p) or
290+
TPathNode2(PathNode2 p)
291+
292+
/** A node in a graph of path explanations that is formed by disjoint union of the two given graphs. */
293+
class PathNode extends TPathNode {
294+
/** Gets this as a projection on the first given `PathGraph`. */
295+
PathNode1 asPathNode1() { this = TPathNode1(result) }
296+
297+
/** Gets this as a projection on the second given `PathGraph`. */
298+
PathNode2 asPathNode2() { this = TPathNode2(result) }
299+
300+
/** Gets a textual representation of this element. */
301+
string toString() {
302+
result = this.asPathNode1().toString() or
303+
result = this.asPathNode2().toString()
304+
}
305+
306+
/**
307+
* Holds if this element is at the specified location.
308+
* The location spans column `startcolumn` of line `startline` to
309+
* column `endcolumn` of line `endline` in file `filepath`.
310+
* For more information, see
311+
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
312+
*/
313+
predicate hasLocationInfo(
314+
string filepath, int startline, int startcolumn, int endline, int endcolumn
315+
) {
316+
this.asPathNode1().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) or
317+
this.asPathNode2().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
318+
}
319+
320+
/** Gets the underlying `Node`. */
321+
Node getNode() {
322+
result = this.asPathNode1().getNode() or
323+
result = this.asPathNode2().getNode()
324+
}
325+
}
326+
327+
/**
328+
* Provides the query predicates needed to include a graph in a path-problem query.
329+
*/
330+
module PathGraph implements PathGraphSig<PathNode> {
331+
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
332+
query predicate edges(PathNode a, PathNode b) {
333+
Graph1::edges(a.asPathNode1(), b.asPathNode1()) or
334+
Graph2::edges(a.asPathNode2(), b.asPathNode2())
335+
}
336+
337+
/** Holds if `n` is a node in the graph of data flow path explanations. */
338+
query predicate nodes(PathNode n, string key, string val) {
339+
Graph1::nodes(n.asPathNode1(), key, val) or
340+
Graph2::nodes(n.asPathNode2(), key, val)
341+
}
342+
343+
/**
344+
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
345+
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
346+
* `ret -> out` is summarized as the edge `arg -> out`.
347+
*/
348+
query predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out) {
349+
Graph1::subpaths(arg.asPathNode1(), par.asPathNode1(), ret.asPathNode1(), out.asPathNode1()) or
350+
Graph2::subpaths(arg.asPathNode2(), par.asPathNode2(), ret.asPathNode2(), out.asPathNode2())
351+
}
352+
}
353+
}

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3157,7 +3157,7 @@ module Impl<FullStateConfigSig Config> {
31573157
/**
31583158
* Provides the query predicates needed to include a graph in a path-problem query.
31593159
*/
3160-
module PathGraph {
3160+
module PathGraph implements PathGraphSig<PathNode> {
31613161
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
31623162
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b }
31633163

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
---
2+
category: feature
3+
---
4+
* Added support for merging two `PathGraph`s via disjoint union to allow results from multiple data flow computations in a single `path-problem` query.

0 commit comments

Comments
 (0)