Skip to content

Commit 4550175

Browse files
committed
Java/C++/C#: Add support for BarrierGuards.
1 parent 5e910a4 commit 4550175

File tree

24 files changed

+221
-0
lines changed

24 files changed

+221
-0
lines changed

cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
7575
/** Holds if data flow out of `node` is prohibited. */
7676
predicate isBarrierOut(Node node) { none() }
7777

78+
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
79+
predicate isBarrierGuard(BarrierGuard guard) { none() }
80+
7881
/**
7982
* Holds if the additional flow step from `node1` to `node2` must be taken
8083
* into account in the analysis.
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
136139
or
137140
config.isBarrierOut(node) and
138141
not config.isSink(node)
142+
or
143+
exists(BarrierGuard g |
144+
config.isBarrierGuard(g) and
145+
node = g.getAGuardedNode()
146+
)
139147
}
140148

141149
private class AdditionalFlowStepSource extends Node {

cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
7575
/** Holds if data flow out of `node` is prohibited. */
7676
predicate isBarrierOut(Node node) { none() }
7777

78+
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
79+
predicate isBarrierGuard(BarrierGuard guard) { none() }
80+
7881
/**
7982
* Holds if the additional flow step from `node1` to `node2` must be taken
8083
* into account in the analysis.
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
136139
or
137140
config.isBarrierOut(node) and
138141
not config.isSink(node)
142+
or
143+
exists(BarrierGuard g |
144+
config.isBarrierGuard(g) and
145+
node = g.getAGuardedNode()
146+
)
139147
}
140148

141149
private class AdditionalFlowStepSource extends Node {

cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
7575
/** Holds if data flow out of `node` is prohibited. */
7676
predicate isBarrierOut(Node node) { none() }
7777

78+
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
79+
predicate isBarrierGuard(BarrierGuard guard) { none() }
80+
7881
/**
7982
* Holds if the additional flow step from `node1` to `node2` must be taken
8083
* into account in the analysis.
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
136139
or
137140
config.isBarrierOut(node) and
138141
not config.isSink(node)
142+
or
143+
exists(BarrierGuard g |
144+
config.isBarrierGuard(g) and
145+
node = g.getAGuardedNode()
146+
)
139147
}
140148

141149
private class AdditionalFlowStepSource extends Node {

cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
7575
/** Holds if data flow out of `node` is prohibited. */
7676
predicate isBarrierOut(Node node) { none() }
7777

78+
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
79+
predicate isBarrierGuard(BarrierGuard guard) { none() }
80+
7881
/**
7982
* Holds if the additional flow step from `node1` to `node2` must be taken
8083
* into account in the analysis.
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
136139
or
137140
config.isBarrierOut(node) and
138141
not config.isSink(node)
142+
or
143+
exists(BarrierGuard g |
144+
config.isBarrierGuard(g) and
145+
node = g.getAGuardedNode()
146+
)
139147
}
140148

141149
private class AdditionalFlowStepSource extends Node {

cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowUtil.qll

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -331,3 +331,14 @@ VariableAccess getAnAccessToAssignedVariable(Expr assign) {
331331
result = var.getAnAccess()
332332
)
333333
}
334+
335+
/** A guard that validates some expression. */
336+
class BarrierGuard extends Expr {
337+
/** Holds if this guard validates `e` upon evaluating to `branch`. */
338+
abstract predicate checks(Expr e, boolean branch);
339+
340+
/** Gets a node guarded by this. */
341+
final Node getAGuardedNode() {
342+
none() // stub
343+
}
344+
}

cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
7575
/** Holds if data flow out of `node` is prohibited. */
7676
predicate isBarrierOut(Node node) { none() }
7777

78+
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
79+
predicate isBarrierGuard(BarrierGuard guard) { none() }
80+
7881
/**
7982
* Holds if the additional flow step from `node1` to `node2` must be taken
8083
* into account in the analysis.
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
136139
or
137140
config.isBarrierOut(node) and
138141
not config.isSink(node)
142+
or
143+
exists(BarrierGuard g |
144+
config.isBarrierGuard(g) and
145+
node = g.getAGuardedNode()
146+
)
139147
}
140148

141149
private class AdditionalFlowStepSource extends Node {

cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
7575
/** Holds if data flow out of `node` is prohibited. */
7676
predicate isBarrierOut(Node node) { none() }
7777

78+
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
79+
predicate isBarrierGuard(BarrierGuard guard) { none() }
80+
7881
/**
7982
* Holds if the additional flow step from `node1` to `node2` must be taken
8083
* into account in the analysis.
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
136139
or
137140
config.isBarrierOut(node) and
138141
not config.isSink(node)
142+
or
143+
exists(BarrierGuard g |
144+
config.isBarrierGuard(g) and
145+
node = g.getAGuardedNode()
146+
)
139147
}
140148

141149
private class AdditionalFlowStepSource extends Node {

cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
7575
/** Holds if data flow out of `node` is prohibited. */
7676
predicate isBarrierOut(Node node) { none() }
7777

78+
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
79+
predicate isBarrierGuard(BarrierGuard guard) { none() }
80+
7881
/**
7982
* Holds if the additional flow step from `node1` to `node2` must be taken
8083
* into account in the analysis.
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
136139
or
137140
config.isBarrierOut(node) and
138141
not config.isSink(node)
142+
or
143+
exists(BarrierGuard g |
144+
config.isBarrierGuard(g) and
145+
node = g.getAGuardedNode()
146+
)
139147
}
140148

141149
private class AdditionalFlowStepSource extends Node {

cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
7575
/** Holds if data flow out of `node` is prohibited. */
7676
predicate isBarrierOut(Node node) { none() }
7777

78+
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
79+
predicate isBarrierGuard(BarrierGuard guard) { none() }
80+
7881
/**
7982
* Holds if the additional flow step from `node1` to `node2` must be taken
8083
* into account in the analysis.
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
136139
or
137140
config.isBarrierOut(node) and
138141
not config.isSink(node)
142+
or
143+
exists(BarrierGuard g |
144+
config.isBarrierGuard(g) and
145+
node = g.getAGuardedNode()
146+
)
139147
}
140148

141149
private class AdditionalFlowStepSource extends Node {

cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44

55
private import cpp
66
private import semmle.code.cpp.ir.IR
7+
private import semmle.code.cpp.controlflow.IRGuards
78

89
/**
910
* A node in a data flow graph.
@@ -166,3 +167,14 @@ predicate localFlowStep(Node nodeFrom, Node nodeTo) {
166167
* (intra-procedural) steps.
167168
*/
168169
predicate localFlow(Node source, Node sink) { localFlowStep*(source, sink) }
170+
171+
/** A guard that validates some expression. */
172+
class BarrierGuard extends IRGuardCondition {
173+
/** Holds if this guard validates `e` upon evaluating to `b`. */
174+
abstract predicate checks(Instruction e, boolean b);
175+
176+
/** Gets a node guarded by this. */
177+
final Node getAGuardedNode() {
178+
none() // stub
179+
}
180+
}

0 commit comments

Comments
 (0)