Merge pull request #8435 from jketema/all-the-barriers · Sam-at-git/codeql@7a9a9d8 · GitHub
Skip to content

Commit 7a9a9d8

Browse files
jketemajketema
authored
Merge pull request github#8435 from jketema/all-the-barriers
Add flow state versions of isBarrierIn, isBarrierOut, and isBarrierGuard
2 parents 68f24cd + 157a36b commit 7a9a9d8

50 files changed

Lines changed: 2266 additions & 336 deletions

File tree

Some content is hidden

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

‎cpp/ql/lib/change-notes/2022-03-14-flow-state-barriers.md‎

Lines changed: 4 additions & 0 deletions

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

Lines changed: 62 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -87,12 +87,30 @@ abstract class Configuration extends string {
8787
/** Holds if data flow into `node` is prohibited. */
8888
predicate isBarrierIn(Node node) { none() }
8989

90+
/**
91+
* Holds if data flow into `node` is prohibited when the flow state is
92+
* `state`
93+
*/
94+
predicate isBarrierIn(Node node, FlowState state) { none() }
95+
9096
/** Holds if data flow out of `node` is prohibited. */
9197
predicate isBarrierOut(Node node) { none() }
9298

99+
/**
100+
* Holds if data flow out of `node` is prohibited when the flow state is
101+
* `state`
102+
*/
103+
predicate isBarrierOut(Node node, FlowState state) { none() }
104+
93105
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
94106
predicate isBarrierGuard(BarrierGuard guard) { none() }
95107

108+
/**
109+
* Holds if data flow through nodes guarded by `guard` is prohibited when
110+
* the flow state is `state`
111+
*/
112+
predicate isBarrierGuard(BarrierGuard guard, FlowState state) { none() }
113+
96114
/**
97115
* Holds if the additional flow step from `node1` to `node2` must be taken
98116
* into account in the analysis.
@@ -305,7 +323,7 @@ private class RetNodeEx extends NodeEx {
305323
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
306324
}
307325

308-
private predicate inBarrier(NodeEx node, Configuration config) {
326+
private predicate fullInBarrier(NodeEx node, Configuration config) {
309327
exists(Node n |
310328
node.asNode() = n and
311329
config.isBarrierIn(n)
@@ -314,7 +332,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
314332
)
315333
}
316334

317-
private predicate outBarrier(NodeEx node, Configuration config) {
335+
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
336+
exists(Node n |
337+
node.asNode() = n and
338+
config.isBarrierIn(n, state)
339+
|
340+
config.isSource(n, state)
341+
)
342+
}
343+
344+
private predicate fullOutBarrier(NodeEx node, Configuration config) {
318345
exists(Node n |
319346
node.asNode() = n and
320347
config.isBarrierOut(n)
@@ -323,6 +350,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
323350
)
324351
}
325352

353+
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
354+
exists(Node n |
355+
node.asNode() = n and
356+
config.isBarrierOut(n, state)
357+
|
358+
config.isSink(n, state)
359+
)
360+
}
361+
326362
pragma[nomagic]
327363
private predicate fullBarrier(NodeEx node, Configuration config) {
328364
exists(Node n | node.asNode() = n |
@@ -345,9 +381,19 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
345381

346382
pragma[nomagic]
347383
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
348-
exists(Node n |
349-
node.asNode() = n and
384+
exists(Node n | node.asNode() = n |
350385
config.isBarrier(n, state)
386+
or
387+
config.isBarrierIn(n, state) and
388+
not config.isSource(n, state)
389+
or
390+
config.isBarrierOut(n, state) and
391+
not config.isSink(n, state)
392+
or
393+
exists(BarrierGuard g |
394+
config.isBarrierGuard(g, state) and
395+
n = g.getAGuardedNode()
396+
)
351397
)
352398
}
353399

@@ -376,8 +422,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
376422
/** Provides the relevant barriers for a step from `node1` to `node2`. */
377423
pragma[inline]
378424
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
379-
not outBarrier(node1, config) and
380-
not inBarrier(node2, config) and
425+
not fullOutBarrier(node1, config) and
426+
not fullInBarrier(node2, config) and
381427
not fullBarrier(node1, config) and
382428
not fullBarrier(node2, config)
383429
}
@@ -430,6 +476,8 @@ private predicate additionalLocalStateStep(
430476
config.isAdditionalFlowStep(n1, s1, n2, s2) and
431477
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
432478
stepFilter(node1, node2, config) and
479+
not stateOutBarrier(node1, s1, config) and
480+
not stateInBarrier(node2, s2, config) and
433481
not stateBarrier(node1, s1, config) and
434482
not stateBarrier(node2, s2, config)
435483
)
@@ -471,6 +519,8 @@ private predicate additionalJumpStateStep(
471519
config.isAdditionalFlowStep(n1, s1, n2, s2) and
472520
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
473521
stepFilter(node1, node2, config) and
522+
not stateOutBarrier(node1, s1, config) and
523+
not stateInBarrier(node2, s2, config) and
474524
not stateBarrier(node1, s1, config) and
475525
not stateBarrier(node2, s2, config) and
476526
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -870,8 +920,8 @@ private module Stage1 {
870920
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
871921
revFlow(node, true, config) and
872922
fwdFlow(node, true, config) and
873-
not inBarrier(node, config) and
874-
not outBarrier(node, config)
923+
not fullInBarrier(node, config) and
924+
not fullOutBarrier(node, config)
875925
}
876926

877927
/** Holds if flow may return from `callable`. */
@@ -966,8 +1016,8 @@ private predicate flowOutOfCallNodeCand1(
9661016
) {
9671017
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
9681018
Stage1::revFlow(ret, config) and
969-
not outBarrier(ret, config) and
970-
not inBarrier(out, config)
1019+
not fullOutBarrier(ret, config) and
1020+
not fullInBarrier(out, config)
9711021
}
9721022

9731023
pragma[nomagic]
@@ -988,8 +1038,8 @@ private predicate flowIntoCallNodeCand1(
9881038
) {
9891039
viableParamArgNodeCand1(call, p, arg, config) and
9901040
Stage1::revFlow(p, config) and
991-
not outBarrier(arg, config) and
992-
not inBarrier(p, config)
1041+
not fullOutBarrier(arg, config) and
1042+
not fullInBarrier(p, config)
9931043
}
9941044

9951045
/**

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

Lines changed: 62 additions & 12 deletions

0 commit comments

Comments
 (0)