From 3b8234ecec1cd0d40e0ed2e19efc82b70e10be7c Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 28 Jul 2025 10:25:31 +0200 Subject: [PATCH] SSA: Update data flow integration and BarrierGuard interface to use GuardValue. --- .../ir/dataflow/internal/DataFlowPrivate.qll | 12 ++-- .../cpp/ir/dataflow/internal/SsaInternals.qll | 19 ++++-- .../code/csharp/dataflow/internal/SsaImpl.qll | 14 ++-- .../code/java/dataflow/internal/SsaImpl.qll | 18 ++--- .../dataflow/internal/BarrierGuards.qll | 4 +- .../internal/TaintTrackingPrivate.qll | 3 +- .../dataflow/internal/sharedlib/Ssa.qll | 12 ++-- .../codeql/ruby/dataflow/internal/SsaImpl.qll | 18 +++-- .../codeql/rust/dataflow/internal/SsaImpl.qll | 18 +++-- .../codeql/dataflow/VariableCapture.qll | 8 ++- shared/ssa/codeql/ssa/Ssa.qll | 66 ++++++++++--------- 11 files changed, 121 insertions(+), 71 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll index d7f26dd00513..192d00b5942e 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll @@ -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() } diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll index fd9ba967a13d..cfaa625f9f5a 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll @@ -961,6 +961,8 @@ class GlobalDef extends Definition { private module SsaImpl = SsaImplCommon::Make; 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 { } 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 diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll index 6d59c0579860..d1490c849163 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll @@ -975,7 +975,8 @@ private module Cached { cached // nothing is actually cached module BarrierGuard { 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 diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll index 45ad9d0a73b7..5a6c5ff6339b 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll @@ -563,9 +563,9 @@ private module Cached { cached // nothing is actually cached module BarrierGuard { 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() } diff --git a/javascript/ql/lib/semmle/javascript/dataflow/internal/BarrierGuards.qll b/javascript/ql/lib/semmle/javascript/dataflow/internal/BarrierGuards.qll index d02728ef551c..0af57ec01869 100644 --- a/javascript/ql/lib/semmle/javascript/dataflow/internal/BarrierGuards.qll +++ b/javascript/ql/lib/semmle/javascript/dataflow/internal/BarrierGuards.qll @@ -193,6 +193,8 @@ private module ConditionGuardDominators { module MakeStateBarrierGuard< FlowStateSig FlowState, WithFlowState::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 | diff --git a/javascript/ql/lib/semmle/javascript/dataflow/internal/TaintTrackingPrivate.qll b/javascript/ql/lib/semmle/javascript/dataflow/internal/TaintTrackingPrivate.qll index 4bb07df9a875..548d06ef64f5 100644 --- a/javascript/ql/lib/semmle/javascript/dataflow/internal/TaintTrackingPrivate.qll +++ b/javascript/ql/lib/semmle/javascript/dataflow/internal/TaintTrackingPrivate.qll @@ -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 diff --git a/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll b/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll index bea32b384371..eef4dc08318a 100644 --- a/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll +++ b/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll @@ -50,6 +50,8 @@ module SsaConfig implements InputSig { import Make 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 diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll index 3e1d27a17ba0..fd1619b1c634 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll @@ -400,7 +400,8 @@ private module Cached { cached // nothing is actually cached module BarrierGuard { 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) } } diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll index aef8391b66ff..9b6d254dec13 100644 --- a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll +++ b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll @@ -301,7 +301,8 @@ private module Cached { cached // nothing is actually cached module BarrierGuard { 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 diff --git a/shared/dataflow/codeql/dataflow/VariableCapture.qll b/shared/dataflow/codeql/dataflow/VariableCapture.qll index 4df415f90ad9..922391221a40 100644 --- a/shared/dataflow/codeql/dataflow/VariableCapture.qll +++ b/shared/dataflow/codeql/dataflow/VariableCapture.qll @@ -733,13 +733,15 @@ module Flow Input> implements OutputSig predicate hasCfgNode(BasicBlock bb, int i) { bb.getNode(i) = this } } + class GuardValue = Void; + class Guard extends Void { - predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { none() } + predicate hasValueBranchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue val) { none() } - predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { 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() } diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index d9a017920171..2aa136ff7197 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -1566,23 +1566,29 @@ module Make 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 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 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 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 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 Input> { private module WithState { /** - * 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 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 Input> { */ module BarrierGuard { 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; @@ -2188,9 +2194,9 @@ module Make Input> { module BarrierGuardWithState::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; @@ -2210,14 +2216,14 @@ module Make 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 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) ) ) }