Skip to content

SSA: Distinguish between has and controls branch edge. #19567

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
aschackmull merged 3 commits into from
May 23, 2025
Merged

SSA: Distinguish between has and controls branch edge. #19567

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1d30103
SSA: Distinguish between has and controls branch edge.
aschackmull May 23, 2025
893cb59
SSA: Elaborate qldoc a bit.
aschackmull May 23, 2025
f4fb717
SSA: Add change note.
aschackmull May 23, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1903,6 +1903,10 @@ module IteratorFlow {
predicate allowFlowIntoUncertainDef(IteratorSsa::UncertainWriteDefinition def) { any() }

class Guard extends Void {
Copy link

Copilot AI May 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Include a descriptive doc comment above this stubbed hasBranchEdge to clarify why it defaults to none() in this context.

Suggested change
class Guard extends Void {
class Guard extends Void {
/**
* Determines whether there is a branch edge between two basic blocks.
*
* This predicate is currently stubbed with `none()` because branch edge
* analysis is not implemented in this context. It serves as a placeholder
* for future extensions where branch edge relationships may need to be
* explicitly modeled.
*/

Copilot uses AI. Check for mistakes.
predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
none()
}

predicate controlsBranchEdge(
SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch
) {
Expand Down
6 changes: 5 additions & 1 deletion cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
)
}

Copy link

Copilot AI May 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add a documentation comment above controlsBranchEdge explaining that it delegates to hasBranchEdge, matching the patterns in other language integrations.

Suggested change
/**
* Delegates to `hasBranchEdge` to determine if this guard controls
* the branch edge between the given basic blocks (`bb1` and `bb2`)
* for the specified branch condition.
*/

Copilot uses AI. Check for mistakes.
predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
this.hasBranchEdge(bb1, bb2, branch)
}
}

predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {
Expand Down
16 changes: 12 additions & 4 deletions csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`. */
Expand Down
21 changes: 21 additions & 0 deletions java/ql/lib/semmle/code/java/controlflow/Guards.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
11 changes: 1 addition & 10 deletions java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down
16 changes: 12 additions & 4 deletions javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,18 +75,26 @@ 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
bb2 = g.getBasicBlock() and
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]
Expand Down
16 changes: 12 additions & 4 deletions ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`. */
Expand Down
16 changes: 12 additions & 4 deletions rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`. */
Expand Down
2 changes: 2 additions & 0 deletions shared/dataflow/codeql/dataflow/VariableCapture.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -732,6 +732,8 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
}

class Guard extends Void {
Copy link

Copilot AI May 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add a doc comment for hasBranchEdge here to explain its intended behavior and why it currently returns none().

Suggested change
class Guard extends Void {
class Guard extends Void {
/**
* Determines whether there is a branch edge between two basic blocks (`bb1` and `bb2`).
* The `branch` parameter indicates the branch direction (e.g., true for "then" branch, false for "else" branch).
*
* Currently, this predicate returns `none()` because branch edge detection is not implemented
* or not applicable in the current context.
*/

Copilot uses AI. Check for mistakes.
predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { none() }

predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { none() }
}

Expand Down
4 changes: 4 additions & 0 deletions shared/ssa/change-notes/2025-05-23-guards-interface.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
---
category: breaking
---
* Adjusted the Guards interface in the SSA data flow integration to distinguish `hasBranchEdge` from `controlsBranchEdge`. Any breakage can be fixed by implementing one with the other as a reasonable fallback solution.
22 changes: 18 additions & 4 deletions shared/ssa/codeql/ssa/Ssa.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1570,9 +1570,23 @@ module Make<LocationSig Location, InputSig<Location> 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`.
Copy link
Contributor

@hvitved hvitved May 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps add an example to illustrate how this can differ from hasBranchEdge.

Copy link
Contributor Author

@aschackmull aschackmull May 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's the general distinction between direct and indirect control. E.g. if (g) .. vs. b = g; .. if (b) ... I can of course elaborate the qldoc here, but I'm thinking perhaps just leaving it as-is, and then focusing on a more comprehensive elaboration in the upcoming shared Guards library - eventually these two predicates will simply be taken directly from that shared library.

Copy link
Contributor

@hvitved hvitved May 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that is what I was thinking; simply add that example to the QL doc.

Copy link
Contributor Author

@aschackmull aschackmull May 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

*
* This predicate differs from `hasBranchEdge` in that it also covers
* indirect guards, such as:
* ```
* b = guard;
* ...
* if (b) { ... }
* ```
*/
predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);
}
Expand Down Expand Up @@ -1667,7 +1681,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.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.
Expand Down
Loading