Skip to content

Rangeanalysis: Simplify Guards integration. #19571

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
merged 2 commits into from
May 26, 2025
Merged

Rangeanalysis: Simplify Guards integration. #19571

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6200031
Rangeanalysis: Simplify Guards integration.
aschackmull May 23, 2025
5b21188
C#: Sync.
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: 0 additions & 4 deletions cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -264,10 +264,6 @@ module SemanticExprConfig {

Guard comparisonGuard(Expr e) { getSemanticExpr(result) = e }

predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
none() // TODO
}

/** Gets the expression associated with `instr`. */
SemExpr getSemanticExpr(IR::Instruction instr) { result = instr }
}
Expand Down
8 changes: 2 additions & 6 deletions cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticGuard.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,11 @@ class SemGuard instanceof Specific::Guard {
Specific::equalityGuard(this, e1, e2, polarity)
}

Copy link
Preview

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.

[nitpick] Add a brief doc comment explaining controls to match the Java Guard_v2 documentation and improve clarity for future maintainers.

Suggested change
/**
* Determines whether this guard directly controls the specified basic block.
*
* @param controlled The basic block that is potentially controlled by this guard.
* @param branch Indicates the branch direction (e.g., true for the true branch, false for the false branch).
* @return True if this guard directly controls the specified block in the given branch direction; otherwise, false.
*/

Copilot uses AI. Check for mistakes.

final predicate directlyControls(SemBasicBlock controlled, boolean branch) {
final predicate controls(SemBasicBlock controlled, boolean branch) {
Specific::guardDirectlyControlsBlock(this, controlled, branch)
}

final predicate hasBranchEdge(SemBasicBlock bb1, SemBasicBlock bb2, boolean branch) {
final predicate controlsBranchEdge(SemBasicBlock bb1, SemBasicBlock bb2, boolean branch) {
Specific::guardHasBranchEdge(this, bb1, bb2, branch)
}

Expand All @@ -31,8 +31,4 @@ class SemGuard instanceof Specific::Guard {
final SemExpr asExpr() { result = Specific::getGuardAsExpr(this) }
}

predicate semImplies_v2(SemGuard g1, boolean b1, SemGuard g2, boolean b2) {
Specific::implies_v2(g1, b1, g2, b2)
}

SemGuard semGetComparisonGuard(SemRelationalExpr e) { result = Specific::comparisonGuard(e) }
2 changes: 0 additions & 2 deletions ...ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,8 +77,6 @@ module Sem implements Semantic<SemLocation> {

class Guard = SemGuard;

predicate implies_v2 = semImplies_v2/4;

class Type = SemType;

class IntegerType = SemIntegerType;
Expand Down
2 changes: 1 addition & 1 deletion csharp/ql/lib/semmle/code/csharp/dataflow/ModulusAnalysis.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, i
exists(Guard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = eqFlowCond(v, e, delta, true, testIsTrue) and
guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
guardControlsSsaRead(guard, pos, testIsTrue)
)
}

Expand Down
2 changes: 0 additions & 2 deletions csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,6 @@ module Private {

class LeftShiftExpr = RU::ExprNode::LeftShiftExpr;

predicate guardDirectlyControlsSsaRead = RU::guardControlsSsaRead/3;

predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;

predicate valueFlowStep = RU::valueFlowStep/3;
Expand Down
35 changes: 34 additions & 1 deletion 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 @@ -145,7 +145,7 @@ private predicate isNonFallThroughPredecessor(SwitchCase sc, ControlFlowNode pre
* Evaluating a switch case to true corresponds to taking that switch case, and
* evaluating it to false corresponds to taking some other branch.
*/
class Guard extends ExprParent {
final class Guard extends ExprParent {
Guard() {
this.(Expr).getType() instanceof BooleanType and not this instanceof BooleanLiteral
or
Expand Down Expand Up @@ -360,6 +360,18 @@ private predicate guardControls_v3(Guard guard, BasicBlock controlled, boolean b
)
}

pragma[nomagic]
Copy link
Preview

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.

[nitpick] Consider removing the unused guardControlsBranchEdge_v3 definitions if no consumer relies on them, to avoid confusion with the new v2 predicates.

Copilot uses AI. Check for mistakes.

private predicate guardControlsBranchEdge_v2(
Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch
) {
guard.hasBranchEdge(bb1, bb2, branch)
or
exists(Guard g, boolean b |
guardControlsBranchEdge_v2(g, bb1, bb2, b) and
implies_v2(g, b, guard, branch)
)
}

pragma[nomagic]
private predicate guardControlsBranchEdge_v3(
Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch
Expand All @@ -372,6 +384,27 @@ private predicate guardControlsBranchEdge_v3(
)
}

/** INTERNAL: Use `Guard` instead. */
final class Guard_v2 extends Guard {
/**
* 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_v2(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
* dominated by this guard evaluating to `branch`.
*/
predicate controls(BasicBlock controlled, boolean branch) {
guardControls_v2(this, controlled, branch)
}
}

private predicate equalityGuard(Guard g, Expr e1, Expr e2, boolean polarity) {
exists(EqualityTest eqtest |
eqtest = g and
Expand Down
2 changes: 1 addition & 1 deletion java/ql/lib/semmle/code/java/dataflow/ModulusAnalysis.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, i
exists(Guard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = eqFlowCond(v, e, delta, true, testIsTrue) and
guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
guardControlsSsaRead(guard, pos, testIsTrue)
)
}

Expand Down
8 changes: 1 addition & 7 deletions java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -219,16 +219,10 @@ module Sem implements Semantic<Location> {

int getBlockId1(BasicBlock bb) { idOf(bb, result) }

final private class FinalGuard = GL::Guard;

class Guard extends FinalGuard {
class Guard extends GL::Guard_v2 {
Expr asExpr() { result = this }
}

predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
GL::implies_v2(g1, b1, g2, b2)
}

class Type = J::Type;

class IntegerType extends J::IntegralType {
Expand Down
2 changes: 0 additions & 2 deletions java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,6 @@ predicate ssaUpdateStep = U::ssaUpdateStep/3;

predicate valueFlowStep = U::valueFlowStep/3;

predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3;

predicate guardControlsSsaRead = U::guardControlsSsaRead/3;

predicate eqFlowCond = U::eqFlowCond/5;
Expand Down
27 changes: 7 additions & 20 deletions java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ module Private {
private import semmle.code.java.dataflow.RangeUtils as RU
private import semmle.code.java.controlflow.Guards as G
private import semmle.code.java.controlflow.BasicBlocks as BB
private import semmle.code.java.controlflow.internal.GuardsLogic as GL
private import SsaReadPositionCommon

class BasicBlock = BB::BasicBlock;
Expand All @@ -15,7 +14,7 @@ module Private {

class Expr = J::Expr;

class Guard = G::Guard;
class Guard = G::Guard_v2;

class ConstantIntegerExpr = RU::ConstantIntegerExpr;

Expand Down Expand Up @@ -101,29 +100,17 @@ module Private {
}
}

/**
* Holds if `guard` directly controls the position `controlled` with the
* value `testIsTrue`.
*/
pragma[nomagic]
predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
or
exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
)
}

/**
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
*/
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
guard.controls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
or
exists(Guard guard0, boolean testIsTrue0 |
GL::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
guardControlsSsaRead(guard0, controlled, testIsTrue0)
exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
guard.controls(controlledEdge.getOrigBlock(), testIsTrue) or
guard
.controlsBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(),
testIsTrue)
)
}

Expand Down
29 changes: 7 additions & 22 deletions java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,12 @@ module Private {
private import semmle.code.java.dataflow.SSA as Ssa
private import semmle.code.java.controlflow.Guards as G
private import SsaReadPositionCommon
private import semmle.code.java.controlflow.internal.GuardsLogic as GL
private import Sign
import Impl

class ConstantIntegerExpr = RU::ConstantIntegerExpr;

class Guard = G::Guard;
class Guard = G::Guard_v2;

class SsaVariable = Ssa::SsaVariable;

Expand Down Expand Up @@ -170,31 +169,17 @@ module Private {

predicate ssaRead = RU::ssaRead/2;

/**
* Holds if `guard` directly controls the position `controlled` with the
* value `testIsTrue`.
*/
pragma[nomagic]
private predicate guardDirectlyControlsSsaRead(
Guard guard, SsaReadPosition controlled, boolean testIsTrue
) {
guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
or
exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
)
}

/**
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
*/
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
guard.controls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
or
exists(Guard guard0, boolean testIsTrue0 |
GL::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
guardControlsSsaRead(guard0, controlled, testIsTrue0)
exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
guard.controls(controlledEdge.getOrigBlock(), testIsTrue) or
guard
.controlsBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(),
testIsTrue)
)
}
}
Expand Down
2 changes: 1 addition & 1 deletion shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ module ModulusAnalysis<
exists(Sem::Guard guard, boolean testIsTrue |
hasReadOfVarInlineLate(pos, v) and
guard = eqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
guardControlsSsaRead(guard, pos, testIsTrue)
)
}

Expand Down
63 changes: 18 additions & 45 deletions shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -181,21 +181,6 @@ signature module Semantic<LocationSig Location> {
*/
Expr asExpr();

/**
* Holds if the guard directly controls a given basic block. For example in
* the following code, the guard `(x > y)` directly controls the block
* beneath it:
* ```
* if (x > y)
* {
* Console.WriteLine("x is greater than y");
* }
* ```
* `branch` indicates whether the basic block is entered when the guard
* evaluates to `true` or when it evaluates to `false`.
*/
predicate directlyControls(BasicBlock controlled, boolean branch);

/**
* Holds if this guard is an equality test between `e1` and `e2`. If the
* test is negated, that is `!=`, then `polarity` is false, otherwise
Expand All @@ -204,24 +189,19 @@ signature module Semantic<LocationSig Location> {
predicate isEquality(Expr e1, Expr e2, boolean polarity);

/**
* Holds if there is a branch edge between two basic blocks. For example
* in the following C code, there are two branch edges from the basic block
* containing the condition `(x > y)` to the beginnings of the true and
* false blocks that follow:
* ```
* if (x > y) {
* printf("x is greater than y\n");
* } else {
* printf("x is not greater than y\n");
* }
* ```
* `branch` indicates whether the second basic block is the one entered
* when the guard evaluates to `true` or when it evaluates to `false`.
* 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 hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);
}
predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);

predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2);
/**
* Holds if this guard evaluating to `branch` directly or indirectly controls
* the block `controlled`. That is, the evaluation of `controlled` is
* dominated by this guard evaluating to `branch`.
*/
predicate controls(BasicBlock controlled, boolean branch);
}

class Type;

Expand Down Expand Up @@ -670,19 +650,14 @@ module RangeStage<
delta = D::fromFloat(D::toFloat(d1) + d2 + d3)
)
or
exists(boolean testIsTrue0 |
Sem::implies_v2(result, testIsTrue, boundFlowCond(v, e, delta, upper, testIsTrue0),
testIsTrue0)
)
or
result = eqFlowCond(v, e, delta, true, testIsTrue) and
(upper = true or upper = false)
or
// guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
// exists a guard `guardEq` such that `v = v2 - d1 + d2`.
// guard that tests whether `v2` is bounded by `e + delta - d` and
// exists a guard `guardEq` such that `v = v2 + d`.
exists(Sem::SsaVariable v2, D::Delta oldDelta, float d |
// equality needs to control guard
result.getBasicBlock() = eqSsaCondDirectlyControls(v, v2, d) and
result.getBasicBlock() = eqSsaCondControls(v, v2, d) and
result = boundFlowCond(v2, e, oldDelta, upper, testIsTrue) and
delta = D::fromFloat(D::toFloat(oldDelta) + d)
)
Expand All @@ -692,13 +667,11 @@ module RangeStage<
* Gets a basic block in which `v1` equals `v2 + delta`.
*/
pragma[nomagic]
private Sem::BasicBlock eqSsaCondDirectlyControls(
Sem::SsaVariable v1, Sem::SsaVariable v2, float delta
) {
private Sem::BasicBlock eqSsaCondControls(Sem::SsaVariable v1, Sem::SsaVariable v2, float delta) {
exists(Sem::Guard guardEq, D::Delta d1, D::Delta d2, boolean eqIsTrue |
guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
delta = D::toFloat(d2) - D::toFloat(d1) and
guardEq.directlyControls(result, eqIsTrue)
guardEq.controls(result, eqIsTrue)
)
}

Expand Down Expand Up @@ -749,7 +722,7 @@ module RangeStage<
exists(Sem::Guard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
guardControlsSsaRead(guard, pos, testIsTrue) and
reason = TSemCondReason(guard)
)
}
Expand All @@ -762,7 +735,7 @@ module RangeStage<
exists(Sem::Guard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = eqFlowCond(v, e, delta, false, testIsTrue) and
guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
guardControlsSsaRead(guard, pos, testIsTrue) and
reason = TSemCondReason(guard)
)
}
Expand Down
Loading
Loading