Skip to content

Data flow: Make PathGraph::edges/2 and PathNode::getASuccessor/1 consistent #9316

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.

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
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
50 changes: 29 additions & 21 deletions cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -3854,24 +3854,30 @@ class PathNode extends TPathNode {
/** Gets the associated configuration. */
Configuration getConfiguration() { none() }

private PathNode getASuccessorIfHidden() {
this.(PathNodeImpl).isHidden() and
result = this.(PathNodeImpl).getASuccessorImpl()
}

/** Gets a successor of this node, if any. */
final PathNode getASuccessor() {
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
not this.(PathNodeImpl).isHidden() and
not result.(PathNodeImpl).isHidden()
result = this.(PathNodeImpl).getANonHiddenSuccessor() and
reach(this) and
reach(result)
}

/** Holds if this node is a source. */
predicate isSource() { none() }
}

abstract private class PathNodeImpl extends PathNode {
abstract PathNode getASuccessorImpl();
abstract PathNodeImpl getASuccessorImpl();

private PathNodeImpl getASuccessorIfHidden() {
this.isHidden() and
result = this.getASuccessorImpl()
}

final PathNodeImpl getANonHiddenSuccessor() {
result = this.getASuccessorImpl().getASuccessorIfHidden*() and
not this.isHidden() and
not result.isHidden()
}

abstract NodeEx getNodeEx();

Expand Down Expand Up @@ -3914,15 +3920,17 @@ abstract private class PathNodeImpl extends PathNode {
}

/** Holds if `n` can reach a sink. */
private predicate directReach(PathNode n) {
n instanceof PathNodeSink or directReach(n.getASuccessor())
private predicate directReach(PathNodeImpl n) {
n instanceof PathNodeSink or directReach(n.getANonHiddenSuccessor())
}

/** Holds if `n` can reach a sink or is used in a subpath that can reach a sink. */
private predicate reach(PathNode n) { directReach(n) or Subpaths::retReach(n) }

/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
private predicate pathSucc(PathNode n1, PathNode n2) { n1.getASuccessor() = n2 and directReach(n2) }
private predicate pathSucc(PathNodeImpl n1, PathNode n2) {
n1.getANonHiddenSuccessor() = n2 and directReach(n2)
}

private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1, n2)

Expand All @@ -3931,7 +3939,7 @@ private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1
*/
module PathGraph {
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(a) and reach(b) }
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b }

/** Holds if `n` is a node in the graph of data flow path explanations. */
query predicate nodes(PathNode n, string key, string val) {
Expand Down Expand Up @@ -4049,7 +4057,7 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {

override Configuration getConfiguration() { result = config }

override PathNode getASuccessorImpl() { none() }
override PathNodeImpl getASuccessorImpl() { none() }

override predicate isSource() { sourceNode(node, state, config) }
}
Expand Down Expand Up @@ -4365,8 +4373,8 @@ private module Subpaths {
}

pragma[nomagic]
private predicate hasSuccessor(PathNode pred, PathNodeMid succ, NodeEx succNode) {
succ = pred.getASuccessor() and
private predicate hasSuccessor(PathNodeImpl pred, PathNodeMid succ, NodeEx succNode) {
succ = pred.getANonHiddenSuccessor() and
succNode = succ.getNodeEx()
}

Expand All @@ -4375,9 +4383,9 @@ private module Subpaths {
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
* `ret -> out` is summarized as the edge `arg -> out`.
*/
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
predicate subpaths(PathNodeImpl arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
pragma[only_bind_into](arg).getASuccessor() = pragma[only_bind_into](out0) and
pragma[only_bind_into](arg).getANonHiddenSuccessor() = pragma[only_bind_into](out0) and
subpaths03(pragma[only_bind_into](arg), p, localStepToHidden*(ret), o, sout, apout) and
hasSuccessor(pragma[only_bind_into](arg), par, p) and
not ret.isHidden() and
Expand All @@ -4390,12 +4398,12 @@ private module Subpaths {
/**
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
*/
predicate retReach(PathNode n) {
predicate retReach(PathNodeImpl n) {
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
or
exists(PathNode mid |
exists(PathNodeImpl mid |
retReach(mid) and
n.getASuccessor() = mid and
n.getANonHiddenSuccessor() = mid and
not subpaths(_, mid, _, _)
)
}
Expand Down
50 changes: 29 additions & 21 deletions cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll
Original file line number Diff line number Diff line change
Expand Up @@ -3854,24 +3854,30 @@ class PathNode extends TPathNode {
/** Gets the associated configuration. */
Configuration getConfiguration() { none() }

private PathNode getASuccessorIfHidden() {
this.(PathNodeImpl).isHidden() and
result = this.(PathNodeImpl).getASuccessorImpl()
}

/** Gets a successor of this node, if any. */
final PathNode getASuccessor() {
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
not this.(PathNodeImpl).isHidden() and
not result.(PathNodeImpl).isHidden()
result = this.(PathNodeImpl).getANonHiddenSuccessor() and
reach(this) and
reach(result)
}

/** Holds if this node is a source. */
predicate isSource() { none() }
}

abstract private class PathNodeImpl extends PathNode {
abstract PathNode getASuccessorImpl();
abstract PathNodeImpl getASuccessorImpl();

private PathNodeImpl getASuccessorIfHidden() {
this.isHidden() and
result = this.getASuccessorImpl()
}

final PathNodeImpl getANonHiddenSuccessor() {
result = this.getASuccessorImpl().getASuccessorIfHidden*() and
not this.isHidden() and
not result.isHidden()
}

abstract NodeEx getNodeEx();

Expand Down Expand Up @@ -3914,15 +3920,17 @@ abstract private class PathNodeImpl extends PathNode {
}

/** Holds if `n` can reach a sink. */
private predicate directReach(PathNode n) {
n instanceof PathNodeSink or directReach(n.getASuccessor())
private predicate directReach(PathNodeImpl n) {
n instanceof PathNodeSink or directReach(n.getANonHiddenSuccessor())
}

/** Holds if `n` can reach a sink or is used in a subpath that can reach a sink. */
private predicate reach(PathNode n) { directReach(n) or Subpaths::retReach(n) }

/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
private predicate pathSucc(PathNode n1, PathNode n2) { n1.getASuccessor() = n2 and directReach(n2) }
private predicate pathSucc(PathNodeImpl n1, PathNode n2) {
n1.getANonHiddenSuccessor() = n2 and directReach(n2)
}

private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1, n2)

Expand All @@ -3931,7 +3939,7 @@ private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1
*/
module PathGraph {
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(a) and reach(b) }
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b }

/** Holds if `n` is a node in the graph of data flow path explanations. */
query predicate nodes(PathNode n, string key, string val) {
Expand Down Expand Up @@ -4049,7 +4057,7 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {

override Configuration getConfiguration() { result = config }

override PathNode getASuccessorImpl() { none() }
override PathNodeImpl getASuccessorImpl() { none() }

override predicate isSource() { sourceNode(node, state, config) }
}
Expand Down Expand Up @@ -4365,8 +4373,8 @@ private module Subpaths {
}

pragma[nomagic]
private predicate hasSuccessor(PathNode pred, PathNodeMid succ, NodeEx succNode) {
succ = pred.getASuccessor() and
private predicate hasSuccessor(PathNodeImpl pred, PathNodeMid succ, NodeEx succNode) {
succ = pred.getANonHiddenSuccessor() and
succNode = succ.getNodeEx()
}

Expand All @@ -4375,9 +4383,9 @@ private module Subpaths {
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
* `ret -> out` is summarized as the edge `arg -> out`.
*/
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
predicate subpaths(PathNodeImpl arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
pragma[only_bind_into](arg).getASuccessor() = pragma[only_bind_into](out0) and
pragma[only_bind_into](arg).getANonHiddenSuccessor() = pragma[only_bind_into](out0) and
subpaths03(pragma[only_bind_into](arg), p, localStepToHidden*(ret), o, sout, apout) and
hasSuccessor(pragma[only_bind_into](arg), par, p) and
not ret.isHidden() and
Expand All @@ -4390,12 +4398,12 @@ private module Subpaths {
/**
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
*/
predicate retReach(PathNode n) {
predicate retReach(PathNodeImpl n) {
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
or
exists(PathNode mid |
exists(PathNodeImpl mid |
retReach(mid) and
n.getASuccessor() = mid and
n.getANonHiddenSuccessor() = mid and
not subpaths(_, mid, _, _)
)
}
Expand Down
50 changes: 29 additions & 21 deletions cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll
Original file line number Diff line number Diff line change
Expand Up @@ -3854,24 +3854,30 @@ class PathNode extends TPathNode {
/** Gets the associated configuration. */
Configuration getConfiguration() { none() }

private PathNode getASuccessorIfHidden() {
this.(PathNodeImpl).isHidden() and
result = this.(PathNodeImpl).getASuccessorImpl()
}

/** Gets a successor of this node, if any. */
final PathNode getASuccessor() {
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
not this.(PathNodeImpl).isHidden() and
not result.(PathNodeImpl).isHidden()
result = this.(PathNodeImpl).getANonHiddenSuccessor() and
reach(this) and
reach(result)
}

/** Holds if this node is a source. */
predicate isSource() { none() }
}

abstract private class PathNodeImpl extends PathNode {
abstract PathNode getASuccessorImpl();
abstract PathNodeImpl getASuccessorImpl();

private PathNodeImpl getASuccessorIfHidden() {
this.isHidden() and
result = this.getASuccessorImpl()
}

final PathNodeImpl getANonHiddenSuccessor() {
result = this.getASuccessorImpl().getASuccessorIfHidden*() and
not this.isHidden() and
not result.isHidden()
}

abstract NodeEx getNodeEx();

Expand Down Expand Up @@ -3914,15 +3920,17 @@ abstract private class PathNodeImpl extends PathNode {
}

/** Holds if `n` can reach a sink. */
private predicate directReach(PathNode n) {
n instanceof PathNodeSink or directReach(n.getASuccessor())
private predicate directReach(PathNodeImpl n) {
n instanceof PathNodeSink or directReach(n.getANonHiddenSuccessor())
}

/** Holds if `n` can reach a sink or is used in a subpath that can reach a sink. */
private predicate reach(PathNode n) { directReach(n) or Subpaths::retReach(n) }

/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
private predicate pathSucc(PathNode n1, PathNode n2) { n1.getASuccessor() = n2 and directReach(n2) }
private predicate pathSucc(PathNodeImpl n1, PathNode n2) {
n1.getANonHiddenSuccessor() = n2 and directReach(n2)
}

private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1, n2)

Expand All @@ -3931,7 +3939,7 @@ private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1
*/
module PathGraph {
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(a) and reach(b) }
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b }

/** Holds if `n` is a node in the graph of data flow path explanations. */
query predicate nodes(PathNode n, string key, string val) {
Expand Down Expand Up @@ -4049,7 +4057,7 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {

override Configuration getConfiguration() { result = config }

override PathNode getASuccessorImpl() { none() }
override PathNodeImpl getASuccessorImpl() { none() }

override predicate isSource() { sourceNode(node, state, config) }
}
Expand Down Expand Up @@ -4365,8 +4373,8 @@ private module Subpaths {
}

pragma[nomagic]
private predicate hasSuccessor(PathNode pred, PathNodeMid succ, NodeEx succNode) {
succ = pred.getASuccessor() and
private predicate hasSuccessor(PathNodeImpl pred, PathNodeMid succ, NodeEx succNode) {
succ = pred.getANonHiddenSuccessor() and
succNode = succ.getNodeEx()
}

Expand All @@ -4375,9 +4383,9 @@ private module Subpaths {
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
* `ret -> out` is summarized as the edge `arg -> out`.
*/
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
predicate subpaths(PathNodeImpl arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
pragma[only_bind_into](arg).getASuccessor() = pragma[only_bind_into](out0) and
pragma[only_bind_into](arg).getANonHiddenSuccessor() = pragma[only_bind_into](out0) and
subpaths03(pragma[only_bind_into](arg), p, localStepToHidden*(ret), o, sout, apout) and
hasSuccessor(pragma[only_bind_into](arg), par, p) and
not ret.isHidden() and
Expand All @@ -4390,12 +4398,12 @@ private module Subpaths {
/**
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
*/
predicate retReach(PathNode n) {
predicate retReach(PathNodeImpl n) {
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
or
exists(PathNode mid |
exists(PathNodeImpl mid |
retReach(mid) and
n.getASuccessor() = mid and
n.getANonHiddenSuccessor() = mid and
not subpaths(_, mid, _, _)
)
}
Expand Down
Loading