Merge pull request #2213 from jbj/BarrierGuard

C++: Implement DataFlow::BarrierGuard for AST+IR
This commit is contained in:
Geoffrey White
2019-11-04 11:08:36 +00:00
committed by GitHub
10 changed files with 147 additions and 9 deletions

View File

@@ -5,6 +5,8 @@
private import cpp
private import semmle.code.cpp.dataflow.internal.FlowVar
private import semmle.code.cpp.models.interfaces.DataFlow
private import semmle.code.cpp.controlflow.Guards
private import semmle.code.cpp.valuenumbering.GlobalValueNumbering
cached
private newtype TNode =
@@ -680,12 +682,16 @@ VariableAccess getAnAccessToAssignedVariable(Expr assign) {
*
* 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);
class BarrierGuard extends GuardCondition {
/** Override this predicate to hold if this guard validates `e` upon evaluating to `b`. */
abstract predicate checks(Expr e, boolean b);
/** Gets a node guarded by this guard. */
final Node getAGuardedNode() {
none() // stub
final ExprNode getAGuardedNode() {
exists(GVN value, boolean branch |
result.getExpr() = value.getAnExpr() and
this.checks(value.getAnExpr(), branch) and
this.controls(result.getExpr().getBasicBlock(), branch)
)
}
}

View File

@@ -5,6 +5,7 @@
private import cpp
private import semmle.code.cpp.ir.IR
private import semmle.code.cpp.controlflow.IRGuards
private import semmle.code.cpp.ir.ValueNumbering
/**
* A newtype wrapper to prevent accidental casts between `Node` and
@@ -220,7 +221,7 @@ predicate localFlow(Node source, Node sink) { localFlowStep*(source, sink) }
predicate localExprFlow(Expr e1, Expr e2) { localFlow(exprNode(e1), exprNode(e2)) }
/**
* A guard that validates some expression.
* A guard that validates some instruction.
*
* To use this in a configuration, extend the class and provide a
* characteristic predicate precisely specifying the guard, and override
@@ -229,11 +230,15 @@ predicate localExprFlow(Expr e1, Expr e2) { localFlow(exprNode(e1), exprNode(e2)
* 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);
/** Override this predicate to hold if this guard validates `instr` upon evaluating to `b`. */
abstract predicate checks(Instruction instr, boolean b);
/** Gets a node guarded by this guard. */
final Node getAGuardedNode() {
none() // stub
exists(ValueNumber value, boolean edge |
result.asInstruction() = value.getAnInstruction() and
this.checks(value.getAnInstruction(), edge) and
this.controls(result.asInstruction().getBlock(), edge)
)
}
}