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 073d7a4bbc9..39cc58d54b0 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 @@ -1903,6 +1903,10 @@ module IteratorFlow { predicate allowFlowIntoUncertainDef(IteratorSsa::UncertainWriteDefinition def) { any() } class Guard extends Void { + predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) { + none() + } + predicate controlsBranchEdge( SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch ) { 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 bea6b68d511..7799081eae3 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 @@ -991,13 +991,17 @@ private module DataFlowIntegrationInput implements SsaImpl::DataFlowIntegrationI class Guard instanceof IRGuards::IRGuardCondition { string toString() { result = super.toString() } - predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) { + predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) { exists(EdgeKind kind | super.getBlock() = bb1 and kind = getConditionalEdge(branch) and bb1.getSuccessor(kind) = bb2 ) } + + predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) { + this.hasBranchEdge(bb1, bb2, branch) + } } predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) { 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 ad7a2aba911..6d59c057986 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll @@ -1044,17 +1044,25 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu class Guard extends Guards::Guard { /** - * Holds if the control flow branching from `bb1` is dependent on this guard, - * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this - * guard to `branch`. + * Holds if the evaluation of this guard to `branch` corresponds to the edge + * from `bb1` to `bb2`. */ - predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { + predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { exists(ControlFlow::SuccessorTypes::ConditionalSuccessor s | this.getAControlFlowNode() = bb1.getLastNode() and bb2 = bb1.getASuccessorByType(s) and s.getValue() = branch ) } + + /** + * Holds if this guard evaluating to `branch` 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`. + */ + predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { + this.hasBranchEdge(bb1, bb2, branch) + } } /** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */ diff --git a/java/ql/lib/semmle/code/java/controlflow/Guards.qll b/java/ql/lib/semmle/code/java/controlflow/Guards.qll index 99a832c08a8..5cedb97ec05 100644 --- a/java/ql/lib/semmle/code/java/controlflow/Guards.qll +++ b/java/ql/lib/semmle/code/java/controlflow/Guards.qll @@ -272,6 +272,15 @@ class Guard extends ExprParent { preconditionControls(this, controlled, branch) } + /** + * Holds if this guard evaluating to `branch` 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`. + */ + predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { + guardControlsBranchEdge_v3(this, bb1, bb2, branch) + } + /** * Holds if this guard evaluating to `branch` directly or indirectly controls * the block `controlled`. That is, the evaluation of `controlled` is @@ -351,6 +360,18 @@ private predicate guardControls_v3(Guard guard, BasicBlock controlled, boolean b ) } +pragma[nomagic] +private predicate guardControlsBranchEdge_v3( + Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch +) { + guard.hasBranchEdge(bb1, bb2, branch) + or + exists(Guard g, boolean b | + guardControlsBranchEdge_v3(g, bb1, bb2, b) and + implies_v3(g, b, guard, branch) + ) +} + private predicate equalityGuard(Guard g, Expr e1, Expr e2, boolean polarity) { exists(EqualityTest eqtest | eqtest = g 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 6054db635bc..2a1ea8b0e06 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll @@ -654,16 +654,7 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu def instanceof SsaUncertainImplicitUpdate } - class Guard extends Guards::Guard { - /** - * Holds if the control flow branching from `bb1` is dependent on this guard, - * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this - * guard to `branch`. - */ - predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { - super.hasBranchEdge(bb1, bb2, branch) - } - } + 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) { 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 adc4a79dd04..bea32b38437 100644 --- a/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll +++ b/javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll @@ -75,11 +75,10 @@ module SsaDataflowInput implements DataFlowIntegrationInputSig { Guard() { this = any(js::ConditionGuardNode g).getTest() } /** - * Holds if the control flow branching from `bb1` is dependent on this guard, - * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this - * guard to `branch`. + * Holds if the evaluation of this guard to `branch` corresponds to the edge + * from `bb1` to `bb2`. */ - predicate controlsBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, boolean branch) { + predicate hasBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, boolean branch) { exists(js::ConditionGuardNode g | g.getTest() = this and bb1 = this.getBasicBlock() and @@ -87,6 +86,15 @@ module SsaDataflowInput implements DataFlowIntegrationInputSig { branch = g.getOutcome() ) } + + /** + * Holds if this guard evaluating to `branch` 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`. + */ + predicate controlsBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, boolean branch) { + this.hasBranchEdge(bb1, bb2, branch) + } } pragma[inline] diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll index b4ba8e3ffad..adbec18be64 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll @@ -484,17 +484,25 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu class Guard extends Cfg::CfgNodes::AstCfgNode { /** - * Holds if the control flow branching from `bb1` is dependent on this guard, - * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this - * guard to `branch`. + * Holds if the evaluation of this guard to `branch` corresponds to the edge + * from `bb1` to `bb2`. */ - predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) { + predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) { exists(Cfg::SuccessorTypes::ConditionalSuccessor s | this.getBasicBlock() = bb1 and bb2 = bb1.getASuccessor(s) and s.getValue() = branch ) } + + /** + * Holds if this guard evaluating to `branch` 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`. + */ + predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) { + this.hasBranchEdge(bb1, bb2, branch) + } } /** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */ diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll index f2500f32ca8..42b1d09f8f9 100644 --- a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll +++ b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll @@ -363,17 +363,25 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu class Guard extends CfgNodes::AstCfgNode { /** - * Holds if the control flow branching from `bb1` is dependent on this guard, - * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this - * guard to `branch`. + * Holds if the evaluation of this guard to `branch` corresponds to the edge + * from `bb1` to `bb2`. */ - predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) { + predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) { exists(Cfg::ConditionalSuccessor s | this = bb1.getANode() and bb2 = bb1.getASuccessor(s) and s.getValue() = branch ) } + + /** + * Holds if this guard evaluating to `branch` 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`. + */ + predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) { + this.hasBranchEdge(bb1, bb2, branch) + } } /** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */ diff --git a/shared/dataflow/codeql/dataflow/VariableCapture.qll b/shared/dataflow/codeql/dataflow/VariableCapture.qll index c76e1320a37..c2c84b7f0f8 100644 --- a/shared/dataflow/codeql/dataflow/VariableCapture.qll +++ b/shared/dataflow/codeql/dataflow/VariableCapture.qll @@ -732,6 +732,8 @@ module Flow Input> implements OutputSig } class Guard extends Void { + predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { none() } + predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { none() } } diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index a0a8a1c864d..a5f9e3f862b 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -1570,9 +1570,15 @@ module Make Input> { string toString(); /** - * Holds if the control flow branching from `bb1` is dependent on this guard, - * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this - * guard to `branch`. + * 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); + + /** + * Holds if this guard evaluating to `branch` 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`. */ predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch); } @@ -1667,7 +1673,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.controlsBranchEdge(input, phi.getBasicBlock(), _)) + exists(DfInput::Guard g | g.hasBranchEdge(input, phi.getBasicBlock(), _)) or // or if the unique predecessor is not an equivalent substitute in // terms of being controlled by the same guards.