Skip to content

Shared/Java: Introduce a shared control flow reachability library and replace the Java Nullness implementation. #20367

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 14 commits into from
Sep 16, 2025
Merged

Shared/Java: Introduce a shared control flow reachability library and replace the Java Nullness implementation. #20367

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
db1f399
Java: Preparatory Nullness refactor.
aschackmull Aug 14, 2025
1ebdcdf
Guards: Support integer ranges.
aschackmull Aug 15, 2025
924a8ea
Java: Improve precision of SuccessorType labels in CFG.
aschackmull Sep 2, 2025
452bbf7
Java: Add some more nullness tests.
aschackmull Aug 25, 2025
4a8ffea
Shared: Add control flow reachability lib.
aschackmull Aug 7, 2025
03321ff
Java: Replace nullness implementation.
aschackmull Aug 14, 2025
60d07cf
Java: Clean up IntegerGuards.qll
aschackmull Sep 5, 2025
e8f1ec6
Java: Accept guards test results.
aschackmull Sep 5, 2025
2743fc0
Guards: Include ConditionalExpr in exprHasValue.
aschackmull Sep 10, 2025
f9ffee0
Java: Minor nullness cleanup.
aschackmull Sep 12, 2025
e302616
Java: Accept qltest change.
aschackmull Sep 12, 2025
b308c54
Java: Add a change note, and a minor ql comment.
aschackmull Sep 15, 2025
be39c4c
Shared: Minor precision improvement.
aschackmull Sep 15, 2025
acb4d9f
Shared: Copy some qldoc from Guards.qll
aschackmull Sep 15, 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
40 changes: 25 additions & 15 deletions java/ql/lib/semmle/code/java/dataflow/Nullness.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,13 +45,21 @@ private import semmle.code.java.Collections
private import semmle.code.java.controlflow.internal.Preconditions

/** Gets an expression that may be `null`. */
Expr nullExpr() {
result instanceof NullLiteral or
result.(ChooseExpr).getAResultExpr() = nullExpr() or
result.(AssignExpr).getSource() = nullExpr() or
result.(CastExpr).getExpr() = nullExpr() or
result.(ImplicitCastExpr).getExpr() = nullExpr() or
result instanceof SafeCastExpr
Expr nullExpr() { result = nullExpr(_) }

/** Gets an expression that may be `null`. */
private Expr nullExpr(Expr reason) {
result instanceof NullLiteral and reason = result
or
result.(ChooseExpr).getAResultExpr() = nullExpr(reason)
or
result.(AssignExpr).getSource() = nullExpr(reason)
or
result.(CastExpr).getExpr() = nullExpr(reason)
or
result.(ImplicitCastExpr).getExpr() = nullExpr(reason)
or
result instanceof SafeCastExpr and reason = result
}

/** An expression of a boxed type that is implicitly unboxed. */
Expand Down Expand Up @@ -174,12 +182,13 @@ private predicate firstVarDereferenceInBlock(BasicBlock bb, SsaVariable v, VarAc
}

/** A variable suspected of being `null`. */
private predicate varMaybeNull(SsaVariable v, string msg, Expr reason) {
private predicate varMaybeNull(SsaVariable v, ControlFlowNode node, string msg, Expr reason) {
// A variable compared to null might be null.
exists(Expr e |
reason = e and
msg = "as suggested by $@ null guard" and
guardSuggestsVarMaybeNull(e, v) and
node = v.getCfgNode() and
not v instanceof SsaPhiNode and
not clearlyNotNull(v) and
// Comparisons in finally blocks are excluded since missing exception edges in the CFG could otherwise yield FPs.
Expand All @@ -195,6 +204,7 @@ private predicate varMaybeNull(SsaVariable v, string msg, Expr reason) {
// A parameter might be null if there is a null argument somewhere.
exists(Parameter p, Expr arg |
v.(SsaImplicitInit).isParameterDefinition(p) and
node = v.getCfgNode() and
p.getAnArgument() = arg and
reason = arg and
msg = "because of $@ null argument" and
Expand All @@ -205,7 +215,7 @@ private predicate varMaybeNull(SsaVariable v, string msg, Expr reason) {
// If the source of a variable is null then the variable may be null.
exists(VariableAssign def |
v.(SsaExplicitUpdate).getDefiningExpr() = def and
def.getSource() = nullExpr() and
def.getSource() = nullExpr(node.asExpr()) and
reason = def and
msg = "because of $@ assignment"
)
Expand Down Expand Up @@ -299,7 +309,7 @@ private predicate leavingFinally(BasicBlock bb1, BasicBlock bb2, boolean normale
}

private predicate ssaSourceVarMaybeNull(SsaSourceVariable v) {
varMaybeNull(v.getAnSsaVariable(), _, _)
varMaybeNull(v.getAnSsaVariable(), _, _, _)
}

/**
Expand Down Expand Up @@ -352,7 +362,7 @@ private predicate nullVarStep(
private predicate varMaybeNullInBlock(
SsaVariable ssa, SsaSourceVariable v, BasicBlock bb, boolean storedcompletion
) {
varMaybeNull(ssa, _, _) and
varMaybeNull(ssa, _, _, _) and
bb = ssa.getBasicBlock() and
storedcompletion = false and
v = ssa.getSourceVariable()
Expand All @@ -378,7 +388,7 @@ private predicate varMaybeNullInBlock_origin(
SsaVariable origin, SsaVariable ssa, BasicBlock bb, boolean storedcompletion
) {
nullDerefCandidateVariable(ssa.getSourceVariable()) and
varMaybeNull(ssa, _, _) and
varMaybeNull(ssa, _, _, _) and
bb = ssa.getBasicBlock() and
storedcompletion = false and
origin = ssa
Expand Down Expand Up @@ -546,7 +556,7 @@ private predicate varMaybeNullInBlock_corrCond(
not varConditionallyNull(ssa, cond1, _) and
(branch = true or branch = false)
) and
varMaybeNull(ssa, _, _) and
varMaybeNull(ssa, _, _, _) and
bb = ssa.getBasicBlock() and
storedcompletion = false and
origin = ssa
Expand Down Expand Up @@ -752,7 +762,7 @@ private predicate varMaybeNullInBlock_trackVar(
isReset(trackssa, trackvar, kind, init, _)
)
) and
varMaybeNull(ssa, _, _) and
varMaybeNull(ssa, _, _, _) and
bb = ssa.getBasicBlock() and
storedcompletion = false and
origin = ssa
Expand Down Expand Up @@ -804,7 +814,7 @@ private predicate varMaybeNullInBlock_trackVar(
predicate nullDeref(SsaSourceVariable v, VarAccess va, string msg, Expr reason) {
exists(SsaVariable origin, SsaVariable ssa, BasicBlock bb |
nullDerefCandidate(origin, va) and
varMaybeNull(origin, msg, reason) and
varMaybeNull(origin, _, msg, reason) and
ssa.getSourceVariable() = v and
firstVarDereferenceInBlock(bb, ssa, va) and
forall(ConditionBlock cond | correlatedConditions(v, cond, _, _) |
Expand Down
69 changes: 49 additions & 20 deletions shared/controlflow/codeql/controlflow/Guards.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -208,6 +208,11 @@ module Make<

private newtype TGuardValue =
TValue(TAbstractSingleValue val, Boolean isVal) or
TIntRange(int bound, Boolean upper) {
exists(ConstantExpr c | c.asIntegerValue() + [-1, 0, 1] = bound) and
bound != 2147483647 and
Copy link
Copy Markdown
Contributor

@michaelnebel michaelnebel Sep 15, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

Total cornercase / nit question: If c holds the maximum integer value of 2147483647 shouldn't we then have TIntRange(2147483646, _) and TIntRange(2147483647, _) (the latter is excluded)?

Copy link
Copy Markdown
Contributor Author

@aschackmull aschackmull Sep 15, 2025

Choose a reason for hiding this comment

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

For edge cases like TIntRange(2147483647, upper) we can easily run into trouble: If upper = false then this is likely a singleton value set, and quite unlikely as a useful bound. And with upper = true, the bound becomes trivial assuming that it applies to e.g. a Java int, but worse is that the default computation of its dual lower bound overflows in QL. Simply excluding the edge cases as valid bounds helps avoid that.

Copy link
Copy Markdown
Contributor Author

@aschackmull aschackmull Sep 15, 2025

Choose a reason for hiding this comment

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

I'll add a comment in the code.

bound != -2147483648
} or
Comment on lines +211 to +216
Copy link

Copilot AI Sep 4, 2025

Choose a reason for hiding this comment

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

[nitpick] The integer bounds 2147483647 and -2147483648 appear to be hardcoded limits for 32-bit integers. Consider using named constants or a more explicit representation to make the intent clearer and improve maintainability.

Copilot uses AI. Check for mistakes.
TException(Boolean throws)

private class AbstractSingleValue extends TAbstractSingleValue {
Expand Down Expand Up @@ -238,6 +243,15 @@ module Make<
result = TValue(val, isVal.booleanNot())
)
or
exists(int bound, int d, boolean upper |
upper = true and d = 1
or
upper = false and d = -1
|
this = TIntRange(bound, pragma[only_bind_into](upper)) and
result = TIntRange(bound + d, pragma[only_bind_into](upper.booleanNot()))
)
or
exists(boolean throws |
this = TException(throws) and
result = TException(throws.booleanNot())
Expand All @@ -262,6 +276,14 @@ module Make<
/** Gets the constant that this value represents, if any. */
ConstantValue asConstantValue() { this = TValue(TValueConstant(result), true) }

/**
* Holds if this value represents an integer range.
*
* If `upper = true` the range is `(-infinity, bound]`.
* If `upper = false` the range is `[bound, infinity)`.
*/
predicate isIntRange(int bound, boolean upper) { this = TIntRange(bound, upper) }

/** Holds if this value represents throwing an exception. */
predicate isThrowsException() { this = TException(true) }

Expand All @@ -275,6 +297,12 @@ module Make<
this = TValue(val, false) and result = "not " + val.toString()
)
or
exists(int bound |
this = TIntRange(bound, true) and result = "Upper bound " + bound.toString()
or
this = TIntRange(bound, false) and result = "Lower bound " + bound.toString()
)
or
exists(boolean throws | this = TException(throws) |
throws = true and result = "exception"
or
Expand All @@ -293,6 +321,24 @@ module Make<
b = TValue(b1, true) and
a1 != b1
)
or
exists(int upperbound, int lowerbound |
a = TIntRange(upperbound, true) and b = TIntRange(lowerbound, false)
or
b = TIntRange(upperbound, true) and a = TIntRange(lowerbound, false)
|
upperbound < lowerbound
)
or
exists(int bound, boolean upper, int k |
a = TIntRange(bound, upper) and b.asIntValue() = k
or
b = TIntRange(bound, upper) and a.asIntValue() = k
|
upper = true and bound < k
or
upper = false and bound > k
)
}

private predicate constantHasValue(ConstantExpr c, GuardValue v) {
Expand Down Expand Up @@ -681,18 +727,6 @@ module Make<
)
}

/** Holds if `e` may take the value `k` */
private predicate relevantInt(Expr e, int k) {
e.(ConstantExpr).asIntegerValue() = k
or
relevantInt(any(Expr e1 | valueStep(e1, e)), k)
or
exists(SsaDefinition def |
guardReadsSsaVar(e, def) and
relevantInt(getAnUltimateDefinition(def, _).(SsaWriteDefinition).getDefinition(), k)
)
}

private predicate impliesStep1(Guard g1, GuardValue v1, Guard g2, GuardValue v2) {
baseImpliesStep(g1, v1, g2, v2)
or
Expand All @@ -705,14 +739,9 @@ module Make<
not g2.directlyValueControls(g1.getBasicBlock(), v2)
)
or
exists(int k1, int k2, boolean upper |
rangeGuard(g1, v1, g2, k1, upper) and
relevantInt(g2, k2) and
v2 = TValue(TValueInt(k2), false)
|
upper = true and k1 < k2 // g2 <= k1 < k2 ==> g2 != k2
or
upper = false and k1 > k2 // g2 >= k1 > k2 ==> g2 != k2
exists(int k, boolean upper |
rangeGuard(g1, v1, g2, k, upper) and
v2 = TIntRange(k, upper)
)
or
exists(boolean isNull |
Expand Down