Skip to content

Commit 9819752

Browse files
smowtonsmowton
authored
Merge pull request github#7526 from smowton/smowton/fix/restore-nodes-edges-consistency
Don't include arg -> param edges in PathGraph::edges where arg is not reachable
2 parents 7e215a5 + fff3b5c commit 9819752

File tree

42 files changed

+685
-436
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

42 files changed

+685
-436
lines changed

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

Lines changed: 23 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -3729,7 +3729,7 @@ private predicate directReach(PathNode n) {
37293729
n instanceof PathNodeSink or directReach(n.getASuccessor())
37303730
}
37313731

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

37353735
/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
@@ -3742,14 +3742,25 @@ private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1
37423742
*/
37433743
module PathGraph {
37443744
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
3745-
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(b) }
3745+
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(a) and reach(b) }
37463746

37473747
/** Holds if `n` is a node in the graph of data flow path explanations. */
37483748
query predicate nodes(PathNode n, string key, string val) {
37493749
reach(n) and key = "semmle.label" and val = n.toString()
37503750
}
37513751

3752-
query predicate subpaths = Subpaths::subpaths/4;
3752+
/**
3753+
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
3754+
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
3755+
* `ret -> out` is summarized as the edge `arg -> out`.
3756+
*/
3757+
query predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out) {
3758+
Subpaths::subpaths(arg, par, ret, out) and
3759+
reach(arg) and
3760+
reach(par) and
3761+
reach(ret) and
3762+
reach(out)
3763+
}
37533764
}
37543765

37553766
/**
@@ -4169,24 +4180,25 @@ private module Subpaths {
41694180
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41704181
* `ret -> out` is summarized as the edge `arg -> out`.
41714182
*/
4172-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4173-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4183+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4184+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41744185
pragma[only_bind_into](arg).getASuccessor() = par and
4175-
pragma[only_bind_into](arg).getASuccessor() = out and
4186+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41764187
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41774188
not ret.isHidden() and
41784189
par.getNodeEx() = p and
4179-
out.getNodeEx() = o and
4180-
out.getState() = sout and
4181-
out.getAp() = apout
4190+
out0.getNodeEx() = o and
4191+
out0.getState() = sout and
4192+
out0.getAp() = apout and
4193+
(out = out0 or out = out0.projectToSink())
41824194
)
41834195
}
41844196

41854197
/**
4186-
* Holds if `n` can reach a return node in a summarized subpath.
4198+
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41874199
*/
41884200
predicate retReach(PathNode n) {
4189-
subpaths(_, _, n, _)
4201+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41904202
or
41914203
exists(PathNode mid |
41924204
retReach(mid) and

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

Lines changed: 23 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -3729,7 +3729,7 @@ private predicate directReach(PathNode n) {
37293729
n instanceof PathNodeSink or directReach(n.getASuccessor())
37303730
}
37313731

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

37353735
/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
@@ -3742,14 +3742,25 @@ private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1
37423742
*/
37433743
module PathGraph {
37443744
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
3745-
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(b) }
3745+
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(a) and reach(b) }
37463746

37473747
/** Holds if `n` is a node in the graph of data flow path explanations. */
37483748
query predicate nodes(PathNode n, string key, string val) {
37493749
reach(n) and key = "semmle.label" and val = n.toString()
37503750
}
37513751

3752-
query predicate subpaths = Subpaths::subpaths/4;
3752+
/**
3753+
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
3754+
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
3755+
* `ret -> out` is summarized as the edge `arg -> out`.
3756+
*/
3757+
query predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out) {
3758+
Subpaths::subpaths(arg, par, ret, out) and
3759+
reach(arg) and
3760+
reach(par) and
3761+
reach(ret) and
3762+
reach(out)
3763+
}
37533764
}
37543765

37553766
/**
@@ -4169,24 +4180,25 @@ private module Subpaths {
41694180
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41704181
* `ret -> out` is summarized as the edge `arg -> out`.
41714182
*/
4172-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4173-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4183+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4184+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41744185
pragma[only_bind_into](arg).getASuccessor() = par and
4175-
pragma[only_bind_into](arg).getASuccessor() = out and
4186+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41764187
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41774188
not ret.isHidden() and
41784189
par.getNodeEx() = p and
4179-
out.getNodeEx() = o and
4180-
out.getState() = sout and
4181-
out.getAp() = apout
4190+
out0.getNodeEx() = o and
4191+
out0.getState() = sout and
4192+
out0.getAp() = apout and
4193+
(out = out0 or out = out0.projectToSink())
41824194
)
41834195
}
41844196

41854197
/**
4186-
* Holds if `n` can reach a return node in a summarized subpath.
4198+
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41874199
*/
41884200
predicate retReach(PathNode n) {
4189-
subpaths(_, _, n, _)
4201+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41904202
or
41914203
exists(PathNode mid |
41924204
retReach(mid) and

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

Lines changed: 23 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -3729,7 +3729,7 @@ private predicate directReach(PathNode n) {
37293729
n instanceof PathNodeSink or directReach(n.getASuccessor())
37303730
}
37313731

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

37353735
/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
@@ -3742,14 +3742,25 @@ private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1
37423742
*/
37433743
module PathGraph {
37443744
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
3745-
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(b) }
3745+
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(a) and reach(b) }
37463746

37473747
/** Holds if `n` is a node in the graph of data flow path explanations. */
37483748
query predicate nodes(PathNode n, string key, string val) {
37493749
reach(n) and key = "semmle.label" and val = n.toString()
37503750
}
37513751

3752-
query predicate subpaths = Subpaths::subpaths/4;
3752+
/**
3753+
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
3754+
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
3755+
* `ret -> out` is summarized as the edge `arg -> out`.
3756+
*/
3757+
query predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out) {
3758+
Subpaths::subpaths(arg, par, ret, out) and
3759+
reach(arg) and
3760+
reach(par) and
3761+
reach(ret) and
3762+
reach(out)
3763+
}
37533764
}
37543765

37553766
/**
@@ -4169,24 +4180,25 @@ private module Subpaths {
41694180
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41704181
* `ret -> out` is summarized as the edge `arg -> out`.
41714182
*/
4172-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4173-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4183+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4184+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41744185
pragma[only_bind_into](arg).getASuccessor() = par and
4175-
pragma[only_bind_into](arg).getASuccessor() = out and
4186+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41764187
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41774188
not ret.isHidden() and
41784189
par.getNodeEx() = p and
4179-
out.getNodeEx() = o and
4180-
out.getState() = sout and
4181-
out.getAp() = apout
4190+
out0.getNodeEx() = o and
4191+
out0.getState() = sout and
4192+
out0.getAp() = apout and
4193+
(out = out0 or out = out0.projectToSink())
41824194
)
41834195
}
41844196

41854197
/**
4186-
* Holds if `n` can reach a return node in a summarized subpath.
4198+
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41874199
*/
41884200
predicate retReach(PathNode n) {
4189-
subpaths(_, _, n, _)
4201+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41904202
or
41914203
exists(PathNode mid |
41924204
retReach(mid) and

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

Lines changed: 23 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -3729,7 +3729,7 @@ private predicate directReach(PathNode n) {
37293729
n instanceof PathNodeSink or directReach(n.getASuccessor())
37303730
}
37313731

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

37353735
/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
@@ -3742,14 +3742,25 @@ private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1
37423742
*/
37433743
module PathGraph {
37443744
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
3745-
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(b) }
3745+
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(a) and reach(b) }
37463746

37473747
/** Holds if `n` is a node in the graph of data flow path explanations. */
37483748
query predicate nodes(PathNode n, string key, string val) {
37493749
reach(n) and key = "semmle.label" and val = n.toString()
37503750
}
37513751

3752-
query predicate subpaths = Subpaths::subpaths/4;
3752+
/**
3753+
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
3754+
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
3755+
* `ret -> out` is summarized as the edge `arg -> out`.
3756+
*/
3757+
query predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out) {
3758+
Subpaths::subpaths(arg, par, ret, out) and
3759+
reach(arg) and
3760+
reach(par) and
3761+
reach(ret) and
3762+
reach(out)
3763+
}
37533764
}
37543765

37553766
/**
@@ -4169,24 +4180,25 @@ private module Subpaths {
41694180
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41704181
* `ret -> out` is summarized as the edge `arg -> out`.
41714182
*/
4172-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4173-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4183+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4184+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41744185
pragma[only_bind_into](arg).getASuccessor() = par and
4175-
pragma[only_bind_into](arg).getASuccessor() = out and
4186+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41764187
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41774188
not ret.isHidden() and
41784189
par.getNodeEx() = p and
4179-
out.getNodeEx() = o and
4180-
out.getState() = sout and
4181-
out.getAp() = apout
4190+
out0.getNodeEx() = o and
4191+
out0.getState() = sout and
4192+
out0.getAp() = apout and
4193+
(out = out0 or out = out0.projectToSink())
41824194
)
41834195
}
41844196

41854197
/**
4186-
* Holds if `n` can reach a return node in a summarized subpath.
4198+
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41874199
*/
41884200
predicate retReach(PathNode n) {
4189-
subpaths(_, _, n, _)
4201+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41904202
or
41914203
exists(PathNode mid |
41924204
retReach(mid) and

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

Lines changed: 23 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -3729,7 +3729,7 @@ private predicate directReach(PathNode n) {
37293729
n instanceof PathNodeSink or directReach(n.getASuccessor())
37303730
}
37313731

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

37353735
/** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
@@ -3742,14 +3742,25 @@ private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1
37423742
*/
37433743
module PathGraph {
37443744
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
3745-
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(b) }
3745+
query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(a) and reach(b) }
37463746

37473747
/** Holds if `n` is a node in the graph of data flow path explanations. */
37483748
query predicate nodes(PathNode n, string key, string val) {
37493749
reach(n) and key = "semmle.label" and val = n.toString()
37503750
}
37513751

3752-
query predicate subpaths = Subpaths::subpaths/4;
3752+
/**
3753+
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
3754+
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
3755+
* `ret -> out` is summarized as the edge `arg -> out`.
3756+
*/
3757+
query predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out) {
3758+
Subpaths::subpaths(arg, par, ret, out) and
3759+
reach(arg) and
3760+
reach(par) and
3761+
reach(ret) and
3762+
reach(out)
3763+
}
37533764
}
37543765

37553766
/**
@@ -4169,24 +4180,25 @@ private module Subpaths {
41694180
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41704181
* `ret -> out` is summarized as the edge `arg -> out`.
41714182
*/
4172-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4173-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4183+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4184+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41744185
pragma[only_bind_into](arg).getASuccessor() = par and
4175-
pragma[only_bind_into](arg).getASuccessor() = out and
4186+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41764187
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41774188
not ret.isHidden() and
41784189
par.getNodeEx() = p and
4179-
out.getNodeEx() = o and
4180-
out.getState() = sout and
4181-
out.getAp() = apout
4190+
out0.getNodeEx() = o and
4191+
out0.getState() = sout and
4192+
out0.getAp() = apout and
4193+
(out = out0 or out = out0.projectToSink())
41824194
)
41834195
}
41844196

41854197
/**
4186-
* Holds if `n` can reach a return node in a summarized subpath.
4198+
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41874199
*/
41884200
predicate retReach(PathNode n) {
4189-
subpaths(_, _, n, _)
4201+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41904202
or
41914203
exists(PathNode mid |
41924204
retReach(mid) and

0 commit comments

Comments
 (0)