mirror of
https://github.com/github/codeql.git
synced 2025-12-20 10:46:30 +01:00
Merge pull request #1718 from aschackmull/java/barrierguard
Java/C++/C#: Add support for BarrierGuards.
This commit is contained in:
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
/**
|
||||
* Holds if the additional flow step from `node1` to `node2` must be taken
|
||||
* into account in the analysis.
|
||||
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
|
||||
or
|
||||
config.isBarrierOut(node) and
|
||||
not config.isSink(node)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g) and
|
||||
node = g.getAGuardedNode()
|
||||
)
|
||||
}
|
||||
|
||||
private class AdditionalFlowStepSource extends Node {
|
||||
|
||||
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
/**
|
||||
* Holds if the additional flow step from `node1` to `node2` must be taken
|
||||
* into account in the analysis.
|
||||
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
|
||||
or
|
||||
config.isBarrierOut(node) and
|
||||
not config.isSink(node)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g) and
|
||||
node = g.getAGuardedNode()
|
||||
)
|
||||
}
|
||||
|
||||
private class AdditionalFlowStepSource extends Node {
|
||||
|
||||
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
/**
|
||||
* Holds if the additional flow step from `node1` to `node2` must be taken
|
||||
* into account in the analysis.
|
||||
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
|
||||
or
|
||||
config.isBarrierOut(node) and
|
||||
not config.isSink(node)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g) and
|
||||
node = g.getAGuardedNode()
|
||||
)
|
||||
}
|
||||
|
||||
private class AdditionalFlowStepSource extends Node {
|
||||
|
||||
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
/**
|
||||
* Holds if the additional flow step from `node1` to `node2` must be taken
|
||||
* into account in the analysis.
|
||||
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
|
||||
or
|
||||
config.isBarrierOut(node) and
|
||||
not config.isSink(node)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g) and
|
||||
node = g.getAGuardedNode()
|
||||
)
|
||||
}
|
||||
|
||||
private class AdditionalFlowStepSource extends Node {
|
||||
|
||||
@@ -331,3 +331,22 @@ VariableAccess getAnAccessToAssignedVariable(Expr assign) {
|
||||
result = var.getAnAccess()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* A guard that validates some expression.
|
||||
*
|
||||
* To use this in a configuration, extend the class and provide a
|
||||
* characteristic predicate precisely specifying the guard, and override
|
||||
* `checks` to specify what is being validated and in which branch.
|
||||
*
|
||||
* It is important that all extending classes in scope are disjoint.
|
||||
*/
|
||||
class BarrierGuard extends Expr {
|
||||
/** NOT YET SUPPORTED. Holds if this guard validates `e` upon evaluating to `branch`. */
|
||||
abstract deprecated predicate checks(Expr e, boolean branch);
|
||||
|
||||
/** Gets a node guarded by this guard. */
|
||||
final Node getAGuardedNode() {
|
||||
none() // stub
|
||||
}
|
||||
}
|
||||
|
||||
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
/**
|
||||
* Holds if the additional flow step from `node1` to `node2` must be taken
|
||||
* into account in the analysis.
|
||||
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
|
||||
or
|
||||
config.isBarrierOut(node) and
|
||||
not config.isSink(node)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g) and
|
||||
node = g.getAGuardedNode()
|
||||
)
|
||||
}
|
||||
|
||||
private class AdditionalFlowStepSource extends Node {
|
||||
|
||||
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
/**
|
||||
* Holds if the additional flow step from `node1` to `node2` must be taken
|
||||
* into account in the analysis.
|
||||
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
|
||||
or
|
||||
config.isBarrierOut(node) and
|
||||
not config.isSink(node)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g) and
|
||||
node = g.getAGuardedNode()
|
||||
)
|
||||
}
|
||||
|
||||
private class AdditionalFlowStepSource extends Node {
|
||||
|
||||
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
/**
|
||||
* Holds if the additional flow step from `node1` to `node2` must be taken
|
||||
* into account in the analysis.
|
||||
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
|
||||
or
|
||||
config.isBarrierOut(node) and
|
||||
not config.isSink(node)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g) and
|
||||
node = g.getAGuardedNode()
|
||||
)
|
||||
}
|
||||
|
||||
private class AdditionalFlowStepSource extends Node {
|
||||
|
||||
@@ -75,6 +75,9 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
/**
|
||||
* Holds if the additional flow step from `node1` to `node2` must be taken
|
||||
* into account in the analysis.
|
||||
@@ -136,6 +139,11 @@ private predicate fullBarrier(Node node, Configuration config) {
|
||||
or
|
||||
config.isBarrierOut(node) and
|
||||
not config.isSink(node)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g) and
|
||||
node = g.getAGuardedNode()
|
||||
)
|
||||
}
|
||||
|
||||
private class AdditionalFlowStepSource extends Node {
|
||||
|
||||
@@ -4,6 +4,7 @@
|
||||
|
||||
private import cpp
|
||||
private import semmle.code.cpp.ir.IR
|
||||
private import semmle.code.cpp.controlflow.IRGuards
|
||||
|
||||
/**
|
||||
* A node in a data flow graph.
|
||||
@@ -166,3 +167,22 @@ predicate localFlowStep(Node nodeFrom, Node nodeTo) {
|
||||
* (intra-procedural) steps.
|
||||
*/
|
||||
predicate localFlow(Node source, Node sink) { localFlowStep*(source, sink) }
|
||||
|
||||
/**
|
||||
* A guard that validates some expression.
|
||||
*
|
||||
* To use this in a configuration, extend the class and provide a
|
||||
* characteristic predicate precisely specifying the guard, and override
|
||||
* `checks` to specify what is being validated and in which branch.
|
||||
*
|
||||
* It is important that all extending classes in scope are disjoint.
|
||||
*/
|
||||
class BarrierGuard extends IRGuardCondition {
|
||||
/** NOT YET SUPPORTED. Holds if this guard validates `e` upon evaluating to `b`. */
|
||||
abstract deprecated predicate checks(Instruction e, boolean b);
|
||||
|
||||
/** Gets a node guarded by this guard. */
|
||||
final Node getAGuardedNode() {
|
||||
none() // stub
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user