Skip to content

Commit 4f3751d

Browse files
aschackmullaschackmull
authored
Merge pull request #9316 from hvitved/dataflow/edges-get-a-successor-consistency
Data flow: Make `PathGraph::edges/2` and `PathNode::getASuccessor/1` consistent
2 parents 9cc10e4 + 4f95abc commit 4f3751d

File tree

32 files changed

+899
-654
lines changed

32 files changed

+899
-654
lines changed

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

Lines changed: 29 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -3854,24 +3854,30 @@ class PathNode extends TPathNode {
38543854
/** Gets the associated configuration. */
38553855
Configuration getConfiguration() { none() }
38563856

3857-
private PathNode getASuccessorIfHidden() {
3858-
this.(PathNodeImpl).isHidden() and
3859-
result = this.(PathNodeImpl).getASuccessorImpl()
3860-
}
3861-
38623857
/** Gets a successor of this node, if any. */
38633858
final PathNode getASuccessor() {
3864-
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
3865-
not this.(PathNodeImpl).isHidden() and
3866-
not result.(PathNodeImpl).isHidden()
3859+
result = this.(PathNodeImpl).getANonHiddenSuccessor() and
3860+
reach(this) and
3861+
reach(result)
38673862
}
38683863

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

38733868
abstract private class PathNodeImpl extends PathNode {
3874-
abstract PathNode getASuccessorImpl();
3869+
abstract PathNodeImpl getASuccessorImpl();
3870+
3871+
private PathNodeImpl getASuccessorIfHidden() {
3872+
this.isHidden() and
3873+
result = this.getASuccessorImpl()
3874+
}
3875+
3876+
final PathNodeImpl getANonHiddenSuccessor() {
3877+
result = this.getASuccessorImpl().getASuccessorIfHidden*() and
3878+
not this.isHidden() and
3879+
not result.isHidden()
3880+
}
38753881

38763882
abstract NodeEx getNodeEx();
38773883

@@ -3914,15 +3920,17 @@ abstract private class PathNodeImpl extends PathNode {
39143920
}
39153921

39163922
/** Holds if `n` can reach a sink. */
3917-
private predicate directReach(PathNode n) {
3918-
n instanceof PathNodeSink or directReach(n.getASuccessor())
3923+
private predicate directReach(PathNodeImpl n) {
3924+
n instanceof PathNodeSink or directReach(n.getANonHiddenSuccessor())
39193925
}
39203926

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

39243930
/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
3925-
private predicate pathSucc(PathNode n1, PathNode n2) { n1.getASuccessor() = n2 and directReach(n2) }
3931+
private predicate pathSucc(PathNodeImpl n1, PathNode n2) {
3932+
n1.getANonHiddenSuccessor() = n2 and directReach(n2)
3933+
}
39263934

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

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

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

40504058
override Configuration getConfiguration() { result = config }
40514059

4052-
override PathNode getASuccessorImpl() { none() }
4060+
override PathNodeImpl getASuccessorImpl() { none() }
40534061

40544062
override predicate isSource() { sourceNode(node, state, config) }
40554063
}
@@ -4365,8 +4373,8 @@ private module Subpaths {
43654373
}
43664374

43674375
pragma[nomagic]
4368-
private predicate hasSuccessor(PathNode pred, PathNodeMid succ, NodeEx succNode) {
4369-
succ = pred.getASuccessor() and
4376+
private predicate hasSuccessor(PathNodeImpl pred, PathNodeMid succ, NodeEx succNode) {
4377+
succ = pred.getANonHiddenSuccessor() and
43704378
succNode = succ.getNodeEx()
43714379
}
43724380

@@ -4375,9 +4383,9 @@ private module Subpaths {
43754383
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
43764384
* `ret -> out` is summarized as the edge `arg -> out`.
43774385
*/
4378-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4386+
predicate subpaths(PathNodeImpl arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
43794387
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
4380-
pragma[only_bind_into](arg).getASuccessor() = pragma[only_bind_into](out0) and
4388+
pragma[only_bind_into](arg).getANonHiddenSuccessor() = pragma[only_bind_into](out0) and
43814389
subpaths03(pragma[only_bind_into](arg), p, localStepToHidden*(ret), o, sout, apout) and
43824390
hasSuccessor(pragma[only_bind_into](arg), par, p) and
43834391
not ret.isHidden() and
@@ -4390,12 +4398,12 @@ private module Subpaths {
43904398
/**
43914399
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
43924400
*/
4393-
predicate retReach(PathNode n) {
4401+
predicate retReach(PathNodeImpl n) {
43944402
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
43954403
or
4396-
exists(PathNode mid |
4404+
exists(PathNodeImpl mid |
43974405
retReach(mid) and
4398-
n.getASuccessor() = mid and
4406+
n.getANonHiddenSuccessor() = mid and
43994407
not subpaths(_, mid, _, _)
44004408
)
44014409
}

‎cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll

Lines changed: 29 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -3854,24 +3854,30 @@ class PathNode extends TPathNode {
38543854
/** Gets the associated configuration. */
38553855
Configuration getConfiguration() { none() }
38563856

3857-
private PathNode getASuccessorIfHidden() {
3858-
this.(PathNodeImpl).isHidden() and
3859-
result = this.(PathNodeImpl).getASuccessorImpl()
3860-
}
3861-
38623857
/** Gets a successor of this node, if any. */
38633858
final PathNode getASuccessor() {
3864-
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
3865-
not this.(PathNodeImpl).isHidden() and
3866-
not result.(PathNodeImpl).isHidden()
3859+
result = this.(PathNodeImpl).getANonHiddenSuccessor() and
3860+
reach(this) and
3861+
reach(result)
38673862
}
38683863

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

38733868
abstract private class PathNodeImpl extends PathNode {
3874-
abstract PathNode getASuccessorImpl();
3869+
abstract PathNodeImpl getASuccessorImpl();
3870+
3871+
private PathNodeImpl getASuccessorIfHidden() {
3872+
this.isHidden() and
3873+
result = this.getASuccessorImpl()
3874+
}
3875+
3876+
final PathNodeImpl getANonHiddenSuccessor() {
3877+
result = this.getASuccessorImpl().getASuccessorIfHidden*() and
3878+
not this.isHidden() and
3879+
not result.isHidden()
3880+
}
38753881

38763882
abstract NodeEx getNodeEx();
38773883

@@ -3914,15 +3920,17 @@ abstract private class PathNodeImpl extends PathNode {
39143920
}
39153921

39163922
/** Holds if `n` can reach a sink. */
3917-
private predicate directReach(PathNode n) {
3918-
n instanceof PathNodeSink or directReach(n.getASuccessor())
3923+
private predicate directReach(PathNodeImpl n) {
3924+
n instanceof PathNodeSink or directReach(n.getANonHiddenSuccessor())
39193925
}
39203926

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

39243930
/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
3925-
private predicate pathSucc(PathNode n1, PathNode n2) { n1.getASuccessor() = n2 and directReach(n2) }
3931+
private predicate pathSucc(PathNodeImpl n1, PathNode n2) {
3932+
n1.getANonHiddenSuccessor() = n2 and directReach(n2)
3933+
}
39263934

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

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

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

40504058
override Configuration getConfiguration() { result = config }
40514059

4052-
override PathNode getASuccessorImpl() { none() }
4060+
override PathNodeImpl getASuccessorImpl() { none() }
40534061

40544062
override predicate isSource() { sourceNode(node, state, config) }
40554063
}
@@ -4365,8 +4373,8 @@ private module Subpaths {
43654373
}
43664374

43674375
pragma[nomagic]
4368-
private predicate hasSuccessor(PathNode pred, PathNodeMid succ, NodeEx succNode) {
4369-
succ = pred.getASuccessor() and
4376+
private predicate hasSuccessor(PathNodeImpl pred, PathNodeMid succ, NodeEx succNode) {
4377+
succ = pred.getANonHiddenSuccessor() and
43704378
succNode = succ.getNodeEx()
43714379
}
43724380

@@ -4375,9 +4383,9 @@ private module Subpaths {
43754383
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
43764384
* `ret -> out` is summarized as the edge `arg -> out`.
43774385
*/
4378-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4386+
predicate subpaths(PathNodeImpl arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
43794387
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
4380-
pragma[only_bind_into](arg).getASuccessor() = pragma[only_bind_into](out0) and
4388+
pragma[only_bind_into](arg).getANonHiddenSuccessor() = pragma[only_bind_into](out0) and
43814389
subpaths03(pragma[only_bind_into](arg), p, localStepToHidden*(ret), o, sout, apout) and
43824390
hasSuccessor(pragma[only_bind_into](arg), par, p) and
43834391
not ret.isHidden() and
@@ -4390,12 +4398,12 @@ private module Subpaths {
43904398
/**
43914399
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
43924400
*/
4393-
predicate retReach(PathNode n) {
4401+
predicate retReach(PathNodeImpl n) {
43944402
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
43954403
or
4396-
exists(PathNode mid |
4404+
exists(PathNodeImpl mid |
43974405
retReach(mid) and
4398-
n.getASuccessor() = mid and
4406+
n.getANonHiddenSuccessor() = mid and
43994407
not subpaths(_, mid, _, _)
44004408
)
44014409
}

‎cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll

Lines changed: 29 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -3854,24 +3854,30 @@ class PathNode extends TPathNode {
38543854
/** Gets the associated configuration. */
38553855
Configuration getConfiguration() { none() }
38563856

3857-
private PathNode getASuccessorIfHidden() {
3858-
this.(PathNodeImpl).isHidden() and
3859-
result = this.(PathNodeImpl).getASuccessorImpl()
3860-
}
3861-
38623857
/** Gets a successor of this node, if any. */
38633858
final PathNode getASuccessor() {
3864-
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
3865-
not this.(PathNodeImpl).isHidden() and
3866-
not result.(PathNodeImpl).isHidden()
3859+
result = this.(PathNodeImpl).getANonHiddenSuccessor() and
3860+
reach(this) and
3861+
reach(result)
38673862
}
38683863

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

38733868
abstract private class PathNodeImpl extends PathNode {
3874-
abstract PathNode getASuccessorImpl();
3869+
abstract PathNodeImpl getASuccessorImpl();
3870+
3871+
private PathNodeImpl getASuccessorIfHidden() {
3872+
this.isHidden() and
3873+
result = this.getASuccessorImpl()
3874+
}
3875+
3876+
final PathNodeImpl getANonHiddenSuccessor() {
3877+
result = this.getASuccessorImpl().getASuccessorIfHidden*() and
3878+
not this.isHidden() and
3879+
not result.isHidden()
3880+
}
38753881

38763882
abstract NodeEx getNodeEx();
38773883

@@ -3914,15 +3920,17 @@ abstract private class PathNodeImpl extends PathNode {
39143920
}
39153921

39163922
/** Holds if `n` can reach a sink. */
3917-
private predicate directReach(PathNode n) {
3918-
n instanceof PathNodeSink or directReach(n.getASuccessor())
3923+
private predicate directReach(PathNodeImpl n) {
3924+
n instanceof PathNodeSink or directReach(n.getANonHiddenSuccessor())
39193925
}
39203926

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

39243930
/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
3925-
private predicate pathSucc(PathNode n1, PathNode n2) { n1.getASuccessor() = n2 and directReach(n2) }
3931+
private predicate pathSucc(PathNodeImpl n1, PathNode n2) {
3932+
n1.getANonHiddenSuccessor() = n2 and directReach(n2)
3933+
}
39263934

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

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

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

40504058
override Configuration getConfiguration() { result = config }
40514059

4052-
override PathNode getASuccessorImpl() { none() }
4060+
override PathNodeImpl getASuccessorImpl() { none() }
40534061

40544062
override predicate isSource() { sourceNode(node, state, config) }
40554063
}
@@ -4365,8 +4373,8 @@ private module Subpaths {
43654373
}
43664374

43674375
pragma[nomagic]
4368-
private predicate hasSuccessor(PathNode pred, PathNodeMid succ, NodeEx succNode) {
4369-
succ = pred.getASuccessor() and
4376+
private predicate hasSuccessor(PathNodeImpl pred, PathNodeMid succ, NodeEx succNode) {
4377+
succ = pred.getANonHiddenSuccessor() and
43704378
succNode = succ.getNodeEx()
43714379
}
43724380

@@ -4375,9 +4383,9 @@ private module Subpaths {
43754383
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
43764384
* `ret -> out` is summarized as the edge `arg -> out`.
43774385
*/
4378-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4386+
predicate subpaths(PathNodeImpl arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
43794387
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
4380-
pragma[only_bind_into](arg).getASuccessor() = pragma[only_bind_into](out0) and
4388+
pragma[only_bind_into](arg).getANonHiddenSuccessor() = pragma[only_bind_into](out0) and
43814389
subpaths03(pragma[only_bind_into](arg), p, localStepToHidden*(ret), o, sout, apout) and
43824390
hasSuccessor(pragma[only_bind_into](arg), par, p) and
43834391
not ret.isHidden() and
@@ -4390,12 +4398,12 @@ private module Subpaths {
43904398
/**
43914399
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
43924400
*/
4393-
predicate retReach(PathNode n) {
4401+
predicate retReach(PathNodeImpl n) {
43944402
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
43954403
or
4396-
exists(PathNode mid |
4404+
exists(PathNodeImpl mid |
43974405
retReach(mid) and
4398-
n.getASuccessor() = mid and
4406+
n.getANonHiddenSuccessor() = mid and
43994407
not subpaths(_, mid, _, _)
44004408
)
44014409
}

0 commit comments

Comments
 (0)