hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-16 16:53:25 +01:00
Code Issues Packages Projects Releases Wiki Activity

SSA: Update data flow integration and BarrierGuard interface to use GuardValue.

Browse Source
This commit is contained in:
Anders Schack-Mulligen
2025-07-28 10:25:31 +02:00
parent 37b508bf43
commit 3b8234ecec
11 changed files with 122 additions and 72 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
View File

@@ -1982,19 +1982,23 @@ module IteratorFlow {
predicate allowFlowIntoUncertainDef(IteratorSsa::UncertainWriteDefinition def) { any() }
class GuardValue = Void;
class Guard extends Void {
predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue val
) {
none()
}
predicate controlsBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch
predicate valueControlsBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue val
) {
none()
}
}
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, GuardValue val) {
none()
}

19
cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll
View File

@@ -961,6 +961,8 @@ class GlobalDef extends Definition {
private module SsaImpl = SsaImplCommon::Make<Location, SsaInput>;
private module DataFlowIntegrationInput implements SsaImpl::DataFlowIntegrationInputSig {
private import codeql.util.Boolean
class Expr extends Instruction {
Expr() {
exists(IRBlock bb, int i |
@@ -992,10 +994,14 @@ private module DataFlowIntegrationInput implements SsaImpl::DataFlowIntegrationI
result instanceof FalseEdge
}
class GuardValue = Boolean;
class Guard instanceof IRGuards::IRGuardCondition {
string toString() { result = super.toString() }
predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
exists(EdgeKind kind |
super.getBlock() = bb1 and
kind = getConditionalEdge(branch) and
@@ -1003,12 +1009,14 @@ private module DataFlowIntegrationInput implements SsaImpl::DataFlowIntegrationI
)
}
predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
this.hasBranchEdge(bb1, bb2, branch)
predicate valueControlsBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
this.hasValueBranchEdge(bb1, bb2, branch)
}
}
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, GuardValue branch) {
guard.(IRGuards::IRGuardCondition).controls(bb, branch)
}
@@ -1037,7 +1045,8 @@ module BarrierGuardWithIntParam<guardChecksNodeSig/4 guardChecksNode> {
}
private predicate guardChecks(
DataFlowIntegrationInput::Guard g, SsaImpl::Definition def, boolean branch, int indirectionIndex
DataFlowIntegrationInput::Guard g, SsaImpl::Definition def,
DataFlowIntegrationInput::GuardValue branch, int indirectionIndex
) {
exists(UseImpl use |
guardChecksNode(g, use.getNode(), branch, indirectionIndex) and

14
csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
View File

@@ -975,7 +975,8 @@ private module Cached {
cached // nothing is actually cached
module BarrierGuard<guardChecksSig/3 guardChecks> {
private predicate guardChecksAdjTypes(
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e,
DataFlowIntegrationInput::GuardValue branch
) {
exists(Guards::AbstractValues::BooleanValue v |
guardChecks(g, e.getAstNode(), v) and
@@ -1016,6 +1017,7 @@ string getToStringPrefix(Definition def) {
private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
private import csharp as Cs
private import semmle.code.csharp.controlflow.BasicBlocks
private import codeql.util.Boolean
class Expr extends ControlFlow::Node {
predicate hasCfgNode(ControlFlow::BasicBlock bb, int i) { this = bb.getNode(i) }
@@ -1042,12 +1044,14 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
)
}
class GuardValue = Boolean;
class Guard extends Guards::Guard {
/**
* Holds if the evaluation of this guard to `branch` corresponds to the edge
* from `bb1` to `bb2`.
*/
predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue branch) {
exists(ControlFlow::SuccessorTypes::ConditionalSuccessor s |
this.getAControlFlowNode() = bb1.getLastNode() and
bb2 = bb1.getASuccessorByType(s) and
@@ -1060,13 +1064,13 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
* branch edge from `bb1` to `bb2`. That is, following the edge from
* `bb1` to `bb2` implies that this guard evaluated to `branch`.
*/
predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
this.hasBranchEdge(bb1, bb2, branch)
predicate valueControlsBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue branch) {
this.hasValueBranchEdge(bb1, bb2, branch)
}
}
/** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
predicate guardDirectlyControlsBlock(Guard guard, ControlFlow::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, ControlFlow::BasicBlock bb, GuardValue branch) {
exists(ConditionBlock conditionBlock, ControlFlow::SuccessorTypes::ConditionalSuccessor s |
guard.getAControlFlowNode() = conditionBlock.getLastNode() and
s.getValue() = branch and

18
java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
View File

@@ -563,9 +563,9 @@ private module Cached {
cached // nothing is actually cached
module BarrierGuard<guardChecksSig/3 guardChecks> {
private predicate guardChecksAdjTypes(
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, Guards::GuardValue val
) {
guardChecks(g, e, branch)
guardChecks(g, e, val.asBooleanValue())
}
private Node getABarrierNodeImpl() {
@@ -657,16 +657,18 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
def instanceof SsaUncertainImplicitUpdate
}
class GuardValue = Guards::GuardValue;
class Guard = Guards::Guard;
/** Holds if the guard `guard` directly controls block `bb` upon evaluating to `branch`. */
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, boolean branch) {
guard.directlyControls(bb, branch)
/** Holds if the guard `guard` directly controls block `bb` upon evaluating to `val`. */
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, GuardValue val) {
guard.directlyValueControls(bb, val)
}
/** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
predicate guardControlsBlock(Guard guard, BasicBlock bb, boolean branch) {
guard.controls(bb, branch)
/** Holds if the guard `guard` controls block `bb` upon evaluating to `val`. */
predicate guardControlsBlock(Guard guard, BasicBlock bb, GuardValue val) {
guard.valueControls(bb, val)
}
predicate includeWriteDefsInFlowStep() { none() }

4
javascript/ql/lib/semmle/javascript/dataflow/internal/BarrierGuards.qll
View File

@@ -193,6 +193,8 @@ private module ConditionGuardDominators {
module MakeStateBarrierGuard<
FlowStateSig FlowState, WithFlowState<FlowState>::BarrierGuardSig BaseGuard>
{
private import codeql.util.Boolean
final private class FinalNode = DataFlow::Node;
abstract private class BarrierGuard extends FinalNode {
@@ -295,7 +297,7 @@ module MakeStateBarrierGuard<
}
private predicate ssa2GuardChecks(
Ssa2::SsaDataflowInput::Guard guard, Ssa2::SsaDataflowInput::Expr test, boolean branch,
Ssa2::SsaDataflowInput::Guard guard, Ssa2::SsaDataflowInput::Expr test, Boolean branch,
FlowState state
) {
exists(BarrierGuard g |

3
javascript/ql/lib/semmle/javascript/dataflow/internal/TaintTrackingPrivate.qll
View File

@@ -6,6 +6,7 @@ private import semmle.javascript.dataflow.internal.sharedlib.FlowSummaryImpl as
private import semmle.javascript.dataflow.internal.FlowSummaryPrivate as FlowSummaryPrivate
private import semmle.javascript.dataflow.internal.BarrierGuards
private import semmle.javascript.dataflow.internal.sharedlib.Ssa as Ssa2
private import codeql.util.Boolean
cached
predicate defaultAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) {
@@ -37,7 +38,7 @@ predicate defaultAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2,
}
private predicate guardChecksFalsy(
Ssa2::SsaDataflowInput::Guard g, Ssa2::SsaDataflowInput::Expr e, boolean outcome
Ssa2::SsaDataflowInput::Guard g, Ssa2::SsaDataflowInput::Expr e, Boolean outcome
) {
exists(ConditionGuardNode guard |
guard.getTest() = g and

12
javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll
View File

@@ -50,6 +50,8 @@ module SsaConfig implements InputSig<js::DbLocation> {
import Make<js::DbLocation, SsaConfig>
module SsaDataflowInput implements DataFlowIntegrationInputSig {
private import codeql.util.Boolean
class Expr extends js::ControlFlowNode {
Expr() { this = any(SsaConfig::SourceVariable v).getAUse() }
@@ -71,6 +73,8 @@ module SsaDataflowInput implements DataFlowIntegrationInputSig {
)
}
class GuardValue = Boolean;
class Guard extends js::ControlFlowNode {
Guard() { this = any(js::ConditionGuardNode g).getTest() }
@@ -78,7 +82,7 @@ module SsaDataflowInput implements DataFlowIntegrationInputSig {
* Holds if the evaluation of this guard to `branch` corresponds to the edge
* from `bb1` to `bb2`.
*/
predicate hasBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, GuardValue branch) {
exists(js::ConditionGuardNode g |
g.getTest() = this and
bb1 = this.getBasicBlock() and
@@ -92,13 +96,13 @@ module SsaDataflowInput implements DataFlowIntegrationInputSig {
* branch edge from `bb1` to `bb2`. That is, following the edge from
* `bb1` to `bb2` implies that this guard evaluated to `branch`.
*/
predicate controlsBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, boolean branch) {
this.hasBranchEdge(bb1, bb2, branch)
predicate valueControlsBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, GuardValue branch) {
this.hasValueBranchEdge(bb1, bb2, branch)
}
}
pragma[inline]
predicate guardDirectlyControlsBlock(Guard guard, js::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, js::BasicBlock bb, GuardValue branch) {
exists(js::ConditionGuardNode g |
g.getTest() = guard and
g.dominates(bb) and

18
ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
View File

@@ -400,7 +400,8 @@ private module Cached {
cached // nothing is actually cached
module BarrierGuard<guardChecksSig/3 guardChecks> {
private predicate guardChecksAdjTypes(
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e,
DataFlowIntegrationInput::GuardValue branch
) {
guardChecks(g, e, branch)
}
@@ -475,6 +476,7 @@ class ParameterExt extends TParameterExt {
private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
private import codeql.ruby.controlflow.internal.Guards as Guards
private import codeql.util.Boolean
class Expr extends Cfg::CfgNodes::ExprCfgNode {
predicate hasCfgNode(SsaInput::BasicBlock bb, int i) { this = bb.getNode(i) }
@@ -486,12 +488,16 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
any(ParameterExt p).isInitializedBy(def) or def.(Ssa::WriteDefinition).assigns(_)
}
class GuardValue = Boolean;
class Guard extends Cfg::CfgNodes::AstCfgNode {
/**
* Holds if the evaluation of this guard to `branch` corresponds to the edge
* from `bb1` to `bb2`.
*/
predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
exists(Cfg::SuccessorTypes::ConditionalSuccessor s |
this.getBasicBlock() = bb1 and
bb2 = bb1.getASuccessor(s) and
@@ -504,13 +510,15 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
* branch edge from `bb1` to `bb2`. That is, following the edge from
* `bb1` to `bb2` implies that this guard evaluated to `branch`.
*/
predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
this.hasBranchEdge(bb1, bb2, branch)
predicate valueControlsBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
this.hasValueBranchEdge(bb1, bb2, branch)
}
}
/** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, GuardValue branch) {
Guards::guardControlsBlock(guard, bb, branch)
}
}

18
rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
View File

@@ -301,7 +301,8 @@ private module Cached {
cached // nothing is actually cached
module BarrierGuard<guardChecksSig/3 guardChecks> {
private predicate guardChecksAdjTypes(
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e,
DataFlowIntegrationInput::GuardValue branch
) {
guardChecks(g, e, branch)
}
@@ -320,6 +321,7 @@ private import codeql.rust.dataflow.Ssa
private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
private import codeql.rust.dataflow.internal.DataFlowImpl as DataFlowImpl
private import codeql.util.Boolean
class Expr extends CfgNodes::AstCfgNode {
predicate hasCfgNode(SsaInput::BasicBlock bb, int i) { this = bb.getNode(i) }
@@ -348,12 +350,16 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
)
}
class GuardValue = Boolean;
class Guard extends CfgNodes::AstCfgNode {
/**
* Holds if the evaluation of this guard to `branch` corresponds to the edge
* from `bb1` to `bb2`.
*/
predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
predicate hasValueBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
exists(Cfg::ConditionalSuccessor s |
this = bb1.getANode() and
bb2 = bb1.getASuccessor(s) and
@@ -366,13 +372,15 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
* branch edge from `bb1` to `bb2`. That is, following the edge from
* `bb1` to `bb2` implies that this guard evaluated to `branch`.
*/
predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
this.hasBranchEdge(bb1, bb2, branch)
predicate valueControlsBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, GuardValue branch
) {
this.hasValueBranchEdge(bb1, bb2, branch)
}
}
/** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {
predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, GuardValue branch) {
exists(ConditionBasicBlock conditionBlock, ConditionalSuccessor s |
guard = conditionBlock.getLastNode() and
s.getValue() = branch and

10
shared/dataflow/codeql/dataflow/VariableCapture.qll
View File

@@ -733,13 +733,15 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
predicate hasCfgNode(BasicBlock bb, int i) { bb.getNode(i) = this }
}
class Guard extends Void {
predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { none() }
class GuardValue = Void;
predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { none() }
class Guard extends Void {
predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue val) { none() }
predicate valueControlsBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue val) { none() }
}
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, boolean branch) { none() }
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, GuardValue val) { none() }
predicate includeWriteDefsInFlowStep() { none() }

66
shared/ssa/codeql/ssa/Ssa.qll
View File

@@ -1566,23 +1566,29 @@ module Make<LocationSig Location, InputSig<Location> Input> {
*/
default predicate allowFlowIntoUncertainDef(UncertainWriteDefinition def) { none() }
/** An abstract value that a `Guard` may evaluate to. */
class GuardValue {
/** Gets a textual representation of this value. */
string toString();
}
/** A (potential) guard. */
class Guard {
/** Gets a textual representation of this guard. */
string toString();
/**
* Holds if the evaluation of this guard to `branch` corresponds to the edge
* Holds if the evaluation of this guard to `val` corresponds to the edge
* from `bb1` to `bb2`.
*/
predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);
predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue val);
/**
* Holds if this guard evaluating to `branch` controls the control-flow
* Holds if this guard evaluating to `val` controls the control-flow
* branch edge from `bb1` to `bb2`. That is, following the edge from
* `bb1` to `bb2` implies that this guard evaluated to `branch`.
* `bb1` to `bb2` implies that this guard evaluated to `val`.
*
* This predicate differs from `hasBranchEdge` in that it also covers
* This predicate differs from `hasValueBranchEdge` in that it also covers
* indirect guards, such as:
* ```
* b = guard;
@@ -1590,15 +1596,15 @@ module Make<LocationSig Location, InputSig<Location> Input> {
* if (b) { ... }
* ```
*/
predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);
predicate valueControlsBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue val);
}
/** Holds if `guard` directly controls block `bb` upon evaluating to `branch`. */
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, boolean branch);
/** Holds if `guard` directly controls block `bb` upon evaluating to `val`. */
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, GuardValue val);
/** Holds if `guard` controls block `bb` upon evaluating to `branch`. */
default predicate guardControlsBlock(Guard guard, BasicBlock bb, boolean branch) {
guardDirectlyControlsBlock(guard, bb, branch)
/** Holds if `guard` controls block `bb` upon evaluating to `val`. */
default predicate guardControlsBlock(Guard guard, BasicBlock bb, GuardValue val) {
guardDirectlyControlsBlock(guard, bb, val)
}
/**
@@ -1683,7 +1689,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
(
// The input node is relevant either if it sits directly on a branch
// edge for a guard,
exists(DfInput::Guard g | g.hasBranchEdge(input, phi.getBasicBlock(), _))
exists(DfInput::Guard g | g.hasValueBranchEdge(input, phi.getBasicBlock(), _))
or
// or if the unique predecessor is not an equivalent substitute in
// terms of being controlled by the same guards.
@@ -1702,9 +1708,9 @@ module Make<LocationSig Location, InputSig<Location> Input> {
AdjacentSsaRefs::adjacentRefPhi(prev, _, input, phi.getBasicBlock(),
phi.getSourceVariable()) and
prev != input and
exists(DfInput::Guard g, boolean branch |
DfInput::guardDirectlyControlsBlock(g, input, branch) and
not DfInput::guardDirectlyControlsBlock(g, prev, branch)
exists(DfInput::Guard g, DfInput::GuardValue val |
DfInput::guardDirectlyControlsBlock(g, input, val) and
not DfInput::guardDirectlyControlsBlock(g, prev, val)
)
)
)
@@ -2118,13 +2124,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
}
/**
* Holds if the guard `g` validates the expression `e` upon evaluating to `branch`.
* Holds if the guard `g` validates the expression `e` upon evaluating to `val`.
*
* The expression `e` is expected to be a syntactic part of the guard `g`.
* For example, the guard `g` might be a call `isSafe(x)` and the expression `e`
* the argument `x`.
*/
signature predicate guardChecksSig(DfInput::Guard g, DfInput::Expr e, boolean branch);
signature predicate guardChecksSig(DfInput::Guard g, DfInput::Expr e, DfInput::GuardValue val);
pragma[nomagic]
private Definition getAPhiInputDef(SsaInputNodeImpl n) {
@@ -2139,7 +2145,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
private module WithState<StateSig State> {
/**
* Holds if the guard `g` validates the expression `e` upon evaluating to `branch`, blocking
* Holds if the guard `g` validates the expression `e` upon evaluating to `val`, blocking
* flow in the given `state`.
*
* The expression `e` is expected to be a syntactic part of the guard `g`.
@@ -2147,15 +2153,15 @@ module Make<LocationSig Location, InputSig<Location> Input> {
* the argument `x`.
*/
signature predicate guardChecksSig(
DfInput::Guard g, DfInput::Expr e, boolean branch, State state
DfInput::Guard g, DfInput::Expr e, DfInput::GuardValue val, State state
);
/**
* Holds if the guard `g` validates the SSA definition `def` upon
* evaluating to `branch`, blocking flow in the given `state`.
* evaluating to `val`, blocking flow in the given `state`.
*/
signature predicate guardChecksDefSig(
DfInput::Guard g, Definition def, boolean branch, State state
DfInput::Guard g, Definition def, DfInput::GuardValue val, State state
);
}
@@ -2167,9 +2173,9 @@ module Make<LocationSig Location, InputSig<Location> Input> {
*/
module BarrierGuard<guardChecksSig/3 guardChecks> {
private predicate guardChecksWithState(
DfInput::Guard g, DfInput::Expr e, boolean branch, Unit state
DfInput::Guard g, DfInput::Expr e, DfInput::GuardValue val, Unit state
) {
guardChecks(g, e, branch) and exists(state)
guardChecks(g, e, val) and exists(state)
}
private module StatefulBarrier = BarrierGuardWithState<Unit, guardChecksWithState/4>;
@@ -2188,9 +2194,9 @@ module Make<LocationSig Location, InputSig<Location> Input> {
module BarrierGuardWithState<StateSig State, WithState<State>::guardChecksSig/4 guardChecks> {
pragma[nomagic]
private predicate guardChecksSsaDef(
DfInput::Guard g, Definition def, boolean branch, State state
DfInput::Guard g, Definition def, DfInput::GuardValue val, State state
) {
guardChecks(g, DfInput::getARead(def), branch, state)
guardChecks(g, DfInput::getARead(def), val, state)
}
private module Barrier = BarrierGuardDefWithState<State, guardChecksSsaDef/4>;
@@ -2210,14 +2216,14 @@ module Make<LocationSig Location, InputSig<Location> Input> {
/** Gets a node that is safely guarded by the given guard check. */
pragma[nomagic]
Node getABarrierNode(State state) {
exists(DfInput::Guard g, boolean branch, Definition def, BasicBlock bb |
guardChecksSsaDef(g, def, branch, state)
exists(DfInput::Guard g, DfInput::GuardValue val, Definition def, BasicBlock bb |
guardChecksSsaDef(g, def, val, state)
|
// guard controls a read
exists(DfInput::Expr e |
e = DfInput::getARead(def) and
e.hasCfgNode(bb, _) and
DfInput::guardControlsBlock(g, bb, branch) and
DfInput::guardControlsBlock(g, bb, val) and
result.(ExprNode).getExpr() = e
)
or
@@ -2226,9 +2232,9 @@ module Make<LocationSig Location, InputSig<Location> Input> {
def = getAPhiInputDef(result) and
result.(SsaInputNodeImpl).isInputInto(phi, bb)
|
DfInput::guardControlsBlock(g, bb, branch)
DfInput::guardControlsBlock(g, bb, val)
or
g.controlsBranchEdge(bb, phi.getBasicBlock(), branch)
g.valueControlsBranchEdge(bb, phi.getBasicBlock(), val)
)
)
}