Skip to content

Commit 71e3935

Browse files
aschackmullaschackmull
committed
Dataflow: Sync.
1 parent b22c4e3 commit 71e3935

File tree

26 files changed

+208
-182
lines changed

26 files changed

+208
-182
lines changed

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4175,24 +4175,25 @@ private module Subpaths {
41754175
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41764176
* `ret -> out` is summarized as the edge `arg -> out`.
41774177
*/
4178-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4179-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4178+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4179+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41804180
pragma[only_bind_into](arg).getASuccessor() = par and
4181-
pragma[only_bind_into](arg).getASuccessor() = out and
4181+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41824182
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41834183
not ret.isHidden() and
41844184
par.getNodeEx() = p and
4185-
out.getNodeEx() = o and
4186-
out.getState() = sout and
4187-
out.getAp() = apout
4185+
out0.getNodeEx() = o and
4186+
out0.getState() = sout and
4187+
out0.getAp() = apout and
4188+
(out = out0 or out = out0.projectToSink())
41884189
)
41894190
}
41904191

41914192
/**
41924193
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41934194
*/
41944195
predicate retReach(PathNode n) {
4195-
exists(PathNodeMid out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
4196+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41964197
or
41974198
exists(PathNode mid |
41984199
retReach(mid) and

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4175,24 +4175,25 @@ private module Subpaths {
41754175
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41764176
* `ret -> out` is summarized as the edge `arg -> out`.
41774177
*/
4178-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4179-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4178+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4179+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41804180
pragma[only_bind_into](arg).getASuccessor() = par and
4181-
pragma[only_bind_into](arg).getASuccessor() = out and
4181+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41824182
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41834183
not ret.isHidden() and
41844184
par.getNodeEx() = p and
4185-
out.getNodeEx() = o and
4186-
out.getState() = sout and
4187-
out.getAp() = apout
4185+
out0.getNodeEx() = o and
4186+
out0.getState() = sout and
4187+
out0.getAp() = apout and
4188+
(out = out0 or out = out0.projectToSink())
41884189
)
41894190
}
41904191

41914192
/**
41924193
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41934194
*/
41944195
predicate retReach(PathNode n) {
4195-
exists(PathNodeMid out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
4196+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41964197
or
41974198
exists(PathNode mid |
41984199
retReach(mid) and

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4175,24 +4175,25 @@ private module Subpaths {
41754175
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41764176
* `ret -> out` is summarized as the edge `arg -> out`.
41774177
*/
4178-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4179-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4178+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4179+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41804180
pragma[only_bind_into](arg).getASuccessor() = par and
4181-
pragma[only_bind_into](arg).getASuccessor() = out and
4181+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41824182
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41834183
not ret.isHidden() and
41844184
par.getNodeEx() = p and
4185-
out.getNodeEx() = o and
4186-
out.getState() = sout and
4187-
out.getAp() = apout
4185+
out0.getNodeEx() = o and
4186+
out0.getState() = sout and
4187+
out0.getAp() = apout and
4188+
(out = out0 or out = out0.projectToSink())
41884189
)
41894190
}
41904191

41914192
/**
41924193
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41934194
*/
41944195
predicate retReach(PathNode n) {
4195-
exists(PathNodeMid out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
4196+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41964197
or
41974198
exists(PathNode mid |
41984199
retReach(mid) and

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4175,24 +4175,25 @@ private module Subpaths {
41754175
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41764176
* `ret -> out` is summarized as the edge `arg -> out`.
41774177
*/
4178-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4179-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4178+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4179+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41804180
pragma[only_bind_into](arg).getASuccessor() = par and
4181-
pragma[only_bind_into](arg).getASuccessor() = out and
4181+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41824182
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41834183
not ret.isHidden() and
41844184
par.getNodeEx() = p and
4185-
out.getNodeEx() = o and
4186-
out.getState() = sout and
4187-
out.getAp() = apout
4185+
out0.getNodeEx() = o and
4186+
out0.getState() = sout and
4187+
out0.getAp() = apout and
4188+
(out = out0 or out = out0.projectToSink())
41884189
)
41894190
}
41904191

41914192
/**
41924193
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41934194
*/
41944195
predicate retReach(PathNode n) {
4195-
exists(PathNodeMid out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
4196+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41964197
or
41974198
exists(PathNode mid |
41984199
retReach(mid) and

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4175,24 +4175,25 @@ private module Subpaths {
41754175
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41764176
* `ret -> out` is summarized as the edge `arg -> out`.
41774177
*/
4178-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4179-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4178+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4179+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41804180
pragma[only_bind_into](arg).getASuccessor() = par and
4181-
pragma[only_bind_into](arg).getASuccessor() = out and
4181+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41824182
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41834183
not ret.isHidden() and
41844184
par.getNodeEx() = p and
4185-
out.getNodeEx() = o and
4186-
out.getState() = sout and
4187-
out.getAp() = apout
4185+
out0.getNodeEx() = o and
4186+
out0.getState() = sout and
4187+
out0.getAp() = apout and
4188+
(out = out0 or out = out0.projectToSink())
41884189
)
41894190
}
41904191

41914192
/**
41924193
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41934194
*/
41944195
predicate retReach(PathNode n) {
4195-
exists(PathNodeMid out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
4196+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41964197
or
41974198
exists(PathNode mid |
41984199
retReach(mid) and

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4175,24 +4175,25 @@ private module Subpaths {
41754175
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41764176
* `ret -> out` is summarized as the edge `arg -> out`.
41774177
*/
4178-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4179-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4178+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4179+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41804180
pragma[only_bind_into](arg).getASuccessor() = par and
4181-
pragma[only_bind_into](arg).getASuccessor() = out and
4181+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41824182
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41834183
not ret.isHidden() and
41844184
par.getNodeEx() = p and
4185-
out.getNodeEx() = o and
4186-
out.getState() = sout and
4187-
out.getAp() = apout
4185+
out0.getNodeEx() = o and
4186+
out0.getState() = sout and
4187+
out0.getAp() = apout and
4188+
(out = out0 or out = out0.projectToSink())
41884189
)
41894190
}
41904191

41914192
/**
41924193
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41934194
*/
41944195
predicate retReach(PathNode n) {
4195-
exists(PathNodeMid out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
4196+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41964197
or
41974198
exists(PathNode mid |
41984199
retReach(mid) and

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4175,24 +4175,25 @@ private module Subpaths {
41754175
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41764176
* `ret -> out` is summarized as the edge `arg -> out`.
41774177
*/
4178-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4179-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4178+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4179+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41804180
pragma[only_bind_into](arg).getASuccessor() = par and
4181-
pragma[only_bind_into](arg).getASuccessor() = out and
4181+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41824182
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41834183
not ret.isHidden() and
41844184
par.getNodeEx() = p and
4185-
out.getNodeEx() = o and
4186-
out.getState() = sout and
4187-
out.getAp() = apout
4185+
out0.getNodeEx() = o and
4186+
out0.getState() = sout and
4187+
out0.getAp() = apout and
4188+
(out = out0 or out = out0.projectToSink())
41884189
)
41894190
}
41904191

41914192
/**
41924193
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41934194
*/
41944195
predicate retReach(PathNode n) {
4195-
exists(PathNodeMid out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
4196+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41964197
or
41974198
exists(PathNode mid |
41984199
retReach(mid) and

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4175,24 +4175,25 @@ private module Subpaths {
41754175
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41764176
* `ret -> out` is summarized as the edge `arg -> out`.
41774177
*/
4178-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4179-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4178+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4179+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41804180
pragma[only_bind_into](arg).getASuccessor() = par and
4181-
pragma[only_bind_into](arg).getASuccessor() = out and
4181+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41824182
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41834183
not ret.isHidden() and
41844184
par.getNodeEx() = p and
4185-
out.getNodeEx() = o and
4186-
out.getState() = sout and
4187-
out.getAp() = apout
4185+
out0.getNodeEx() = o and
4186+
out0.getState() = sout and
4187+
out0.getAp() = apout and
4188+
(out = out0 or out = out0.projectToSink())
41884189
)
41894190
}
41904191

41914192
/**
41924193
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41934194
*/
41944195
predicate retReach(PathNode n) {
4195-
exists(PathNodeMid out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
4196+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41964197
or
41974198
exists(PathNode mid |
41984199
retReach(mid) and

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4175,24 +4175,25 @@ private module Subpaths {
41754175
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41764176
* `ret -> out` is summarized as the edge `arg -> out`.
41774177
*/
4178-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4179-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4178+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4179+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41804180
pragma[only_bind_into](arg).getASuccessor() = par and
4181-
pragma[only_bind_into](arg).getASuccessor() = out and
4181+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41824182
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41834183
not ret.isHidden() and
41844184
par.getNodeEx() = p and
4185-
out.getNodeEx() = o and
4186-
out.getState() = sout and
4187-
out.getAp() = apout
4185+
out0.getNodeEx() = o and
4186+
out0.getState() = sout and
4187+
out0.getAp() = apout and
4188+
(out = out0 or out = out0.projectToSink())
41884189
)
41894190
}
41904191

41914192
/**
41924193
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41934194
*/
41944195
predicate retReach(PathNode n) {
4195-
exists(PathNodeMid out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
4196+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41964197
or
41974198
exists(PathNode mid |
41984199
retReach(mid) and

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4175,24 +4175,25 @@ private module Subpaths {
41754175
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
41764176
* `ret -> out` is summarized as the edge `arg -> out`.
41774177
*/
4178-
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNodeMid out) {
4179-
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout |
4178+
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
4179+
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
41804180
pragma[only_bind_into](arg).getASuccessor() = par and
4181-
pragma[only_bind_into](arg).getASuccessor() = out and
4181+
pragma[only_bind_into](arg).getASuccessor() = out0 and
41824182
subpaths03(arg, p, localStepToHidden*(ret), o, sout, apout) and
41834183
not ret.isHidden() and
41844184
par.getNodeEx() = p and
4185-
out.getNodeEx() = o and
4186-
out.getState() = sout and
4187-
out.getAp() = apout
4185+
out0.getNodeEx() = o and
4186+
out0.getState() = sout and
4187+
out0.getAp() = apout and
4188+
(out = out0 or out = out0.projectToSink())
41884189
)
41894190
}
41904191

41914192
/**
41924193
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
41934194
*/
41944195
predicate retReach(PathNode n) {
4195-
exists(PathNodeMid out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
4196+
exists(PathNode out | subpaths(_, _, n, out) | directReach(out) or retReach(out))
41964197
or
41974198
exists(PathNode mid |
41984199
retReach(mid) and

0 commit comments

Comments
 (0)