hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-16 16:53:25 +01:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #20367 from aschackmull/shared/controlflow

Browse Source 
Shared/Java: Introduce a shared control flow reachability library and replace the Java Nullness implementation.
This commit is contained in:
Anders Schack-Mulligen
2025-09-16 10:44:44 +02:00
committed by GitHub
parent 6264f46970 acb4d9f681
commit 57e15b9a91
14 changed files with 1234 additions and 655 deletions
Download Patch File Download Diff File Expand all files Collapse all files

23
java/ql/lib/semmle/code/java/ControlFlowGraph.qll
View File

@@ -82,6 +82,7 @@ module;
*/
import java
private import codeql.controlflow.SuccessorType
private import codeql.util.Boolean
private import Completion
private import controlflow.internal.Preconditions
@@ -124,6 +125,28 @@ module ControlFlow {
result = succ(this, NormalCompletion())
}
/** Gets an immediate successor of this node of a given type, if any. */
Node getASuccessor(SuccessorType t) {
result = branchSuccessor(this, t.(BooleanSuccessor).getValue())
or
exists(Completion completion |
result = succ(this, completion) and
not result = branchSuccessor(this, _)
|
completion = NormalCompletion() and t instanceof DirectSuccessor
or
completion = ReturnCompletion() and t instanceof ReturnSuccessor
or
completion = BreakCompletion(_) and t instanceof BreakSuccessor
or
completion = YieldCompletion(_) and t instanceof BreakSuccessor
or
completion = ContinueCompletion(_) and t instanceof ContinueSuccessor
or
completion = ThrowCompletion(_) and t instanceof ExceptionSuccessor
)
}
/** Gets the basic block that contains this node. */
BasicBlock getBasicBlock() { result.getANode() = this }

14
java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll
View File

@@ -22,20 +22,8 @@ private module Input implements BB::InputSig<Location> {
/** Gets the CFG scope in which this node occurs. */
CfgScope nodeGetCfgScope(Node node) { node.getEnclosingCallable() = result }
private Node getASpecificSuccessor(Node node, SuccessorType t) {
node.(ConditionNode).getABranchSuccessor(t.(BooleanSuccessor).getValue()) = result
or
node.getAnExceptionSuccessor() = result and t instanceof ExceptionSuccessor
}
/** Gets an immediate successor of this node. */
Node nodeGetASuccessor(Node node, SuccessorType t) {
result = getASpecificSuccessor(node, t)
or
node.getASuccessor() = result and
t instanceof DirectSuccessor and
not result = getASpecificSuccessor(node, _)
}
Node nodeGetASuccessor(Node node, SuccessorType t) { result = node.getASuccessor(t) }
/**
* Holds if `node` represents an entry node to be used when calculating

60
java/ql/lib/semmle/code/java/controlflow/ControlFlow.qll Normal file
View File

@@ -0,0 +1,60 @@
/**
* Provides an implementation of local (intraprocedural) control flow reachability.
*/
overlay[local?]
module;
import java
private import codeql.controlflow.ControlFlow
private import semmle.code.java.dataflow.SSA as SSA
private import semmle.code.java.controlflow.Guards as Guards
private module ControlFlowInput implements InputSig<Location, ControlFlowNode, BasicBlock> {
private import java as J
AstNode getEnclosingAstNode(ControlFlowNode node) { node.getAstNode() = result }
class AstNode = ExprParent;
AstNode getParent(AstNode node) {
result = node.(Expr).getParent() or
result = node.(Stmt).getParent()
}
class FinallyBlock extends AstNode {
FinallyBlock() { any(TryStmt try).getFinally() = this }
}
class Expr = J::Expr;
class SourceVariable = SSA::SsaSourceVariable;
class SsaDefinition = SSA::SsaVariable;
class SsaWriteDefinition extends SsaDefinition instanceof SSA::SsaExplicitUpdate {
Expr getDefinition() {
super.getDefiningExpr().(VariableAssign).getSource() = result or
super.getDefiningExpr().(AssignOp) = result
}
}
class SsaPhiNode = SSA::SsaPhiNode;
class SsaUncertainDefinition extends SsaDefinition instanceof SSA::SsaUncertainImplicitUpdate {
SsaDefinition getPriorDefinition() { result = super.getPriorDef() }
}
class GuardValue = Guards::GuardValue;
predicate ssaControlsBranchEdge(SsaDefinition def, BasicBlock bb1, BasicBlock bb2, GuardValue v) {
Guards::Guards_v3::ssaControlsBranchEdge(def, bb1, bb2, v)
}
predicate ssaControls(SsaDefinition def, BasicBlock bb, GuardValue v) {
Guards::Guards_v3::ssaControls(def, bb, v)
}
import Guards::Guards_v3::InternalUtil
}
module ControlFlow = Make<Location, Cfg, ControlFlowInput>;

42
java/ql/lib/semmle/code/java/dataflow/IntegerGuards.qll
View File

@@ -10,7 +10,7 @@ private import RangeUtils
private import RangeAnalysis
/** Gets an expression that might have the value `i`. */
private Expr exprWithIntValue(int i) {
deprecated private Expr exprWithIntValue(int i) {
result.(ConstantIntegerExpr).getIntValue() = i or
result.(ChooseExpr).getAResultExpr() = exprWithIntValue(i)
}
@@ -19,11 +19,11 @@ private Expr exprWithIntValue(int i) {
* An expression for which the predicate `integerGuard` is relevant.
* This includes `VarRead` and `MethodCall`.
*/
class IntComparableExpr extends Expr {
deprecated class IntComparableExpr extends Expr {
IntComparableExpr() { this instanceof VarRead or this instanceof MethodCall }
/** Gets an integer that is directly assigned to the expression in case of a variable; or zero. */
int relevantInt() {
deprecated int relevantInt() {
exists(SsaExplicitUpdate ssa, SsaSourceVariable v |
this = v.getAnAccess() and
ssa.getSourceVariable() = v and
@@ -55,6 +55,9 @@ private predicate comparison(ComparisonExpr comp, boolean branch, Expr e1, Expr
* Holds if `guard` evaluating to `branch` ensures that:
* `e <= k` when `upper = true`
* `e >= k` when `upper = false`
*
* Does _not_ include the constant comparison case where the guard directly
* ensures `e == k`.
*/
pragma[nomagic]
predicate rangeGuard(Expr guard, boolean branch, Expr e, int k, boolean upper) {
@@ -62,7 +65,8 @@ predicate rangeGuard(Expr guard, boolean branch, Expr e, int k, boolean upper) {
eqtest = guard and
eqtest.hasOperands(e, c) and
bounded(c, any(ZeroBound zb), k, upper, _) and
branch = eqtest.polarity()
branch = eqtest.polarity() and
not c instanceof ConstantIntegerExpr
)
or
exists(Expr c, int val, boolean strict, int d |
@@ -87,6 +91,30 @@ predicate rangeGuard(Expr guard, boolean branch, Expr e, int k, boolean upper) {
}
/**
* Gets an expression that directly tests whether a given expression, `e`, is
* non-zero.
*/
Expr nonZeroGuard(Expr e, boolean branch) {
exists(EqualityTest eqtest, boolean polarity, int k |
eqtest = result and
eqtest.hasOperands(e, any(ConstantIntegerExpr c | c.getIntValue() = k)) and
polarity = eqtest.polarity()
|
k = 0 and branch = polarity.booleanNot()
or
k != 0 and branch = polarity
)
or
exists(int val, boolean upper | rangeGuard(result, branch, e, val, upper) |
upper = true and val < 0 // e <= val < 0 ==> e != 0
or
upper = false and val > 0 // e >= val > 0 ==> e != 0
)
}
/**
* DEPRECATED.
*
* An expression that directly tests whether a given expression is equal to `k` or not.
* The set of `k`s is restricted to those that are relevant for the expression or
* have a direct comparison with the expression.
@@ -95,7 +123,7 @@ predicate rangeGuard(Expr guard, boolean branch, Expr e, int k, boolean upper) {
* is true, and different from `k` if `is_k` is false.
*/
pragma[nomagic]
Expr integerGuard(IntComparableExpr e, boolean branch, int k, boolean is_k) {
deprecated Expr integerGuard(IntComparableExpr e, boolean branch, int k, boolean is_k) {
exists(EqualityTest eqtest, boolean polarity |
eqtest = result and
eqtest.hasOperands(e, any(ConstantIntegerExpr c | c.getIntValue() = k)) and
@@ -119,13 +147,15 @@ Expr integerGuard(IntComparableExpr e, boolean branch, int k, boolean is_k) {
}
/**
* DEPRECATED: Use `rangeGuard` instead.
*
* A guard that splits the values of a variable into one range with an upper bound of `k-1`
* and one with a lower bound of `k`.
*
* If `branch_with_lower_bound_k` is true then `result` is equivalent to `k <= x`
* and if it is false then `result` is equivalent to `k > x`.
*/
Expr intBoundGuard(VarRead x, boolean branch_with_lower_bound_k, int k) {
deprecated Expr intBoundGuard(VarRead x, boolean branch_with_lower_bound_k, int k) {
exists(ComparisonExpr comp, ConstantIntegerExpr c, int val |
comp = result and
comp.hasOperands(x, c) and

634
java/ql/lib/semmle/code/java/dataflow/Nullness.qll
View File

@@ -9,49 +9,31 @@
overlay[local?]
module;
/*
* Implementation details:
*
* The three exported predicates, `nullDeref`, `alwaysNullDeref`, and
* `superfluousNullGuard`, compute potential null dereferences, definite null
* dereferences, and superfluous null checks, respectively. The bulk of the
* library supports `nullDeref`, while the latter two are fairly simple in
* comparison.
*
* The NPE (NullPointerException) candidates are computed by
* `nullDerefCandidate` and consist of three parts: A variable definition that
* might be null as computed by `varMaybeNull`, a dereference that can cause a
* NPE as computed by `firstVarDereferenceInBlock`, and a control flow path
* between the two points. The path is computed by `varMaybeNullInBlock`,
* which is the transitive closure of the step relation `nullVarStep`
* originating in a definition given by `varMaybeNull`. The step relation
* `nullVarStep` is essentially just the successor relation on basic blocks
* restricted to exclude edges along which the variable cannot be null.
*
* The step relation `nullVarStep` is then reused twice to produce two
* refinements of the path reachability predicate `varMaybeNullInBlock` in
* order to prune impossible paths that would otherwise lead to a potential
* NPE. These two refinements are `varMaybeNullInBlock_corrCond` and
* `varMaybeNullInBlock_trackVar` and are described in further detail below.
*/
import java
private import SSA
private import semmle.code.java.controlflow.Guards
private import RangeUtils
private import IntegerGuards
private import NullGuards
private import semmle.code.java.Collections
private import semmle.code.java.controlflow.internal.Preconditions
private import semmle.code.java.controlflow.ControlFlow as Cf
/** 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. */
@@ -137,49 +119,29 @@ private ControlFlowNode varDereference(SsaVariable v, VarAccess va) {
}
/**
* A `ControlFlowNode` that ensures that the SSA variable is not null in any
* subsequent use, either by dereferencing it or by an assertion.
*/
private ControlFlowNode ensureNotNull(SsaVariable v) { result = varDereference(v, _) }
private predicate assertFail(BasicBlock bb, ControlFlowNode n) {
bb = n.getBasicBlock() and
methodCallUnconditionallyThrows(n.asExpr())
}
/**
* A variable dereference that cannot be reached by a `null` value, because of an earlier
* dereference or assertion in the same `BasicBlock`.
*/
private predicate unreachableVarDereference(BasicBlock bb, SsaVariable v, ControlFlowNode varDeref) {
exists(ControlFlowNode n, int i, int j |
(n = ensureNotNull(v) or assertFail(bb, n)) and
varDeref = varDereference(v, _) and
bb.getNode(i) = n and
bb.getNode(j) = varDeref and
i < j
)
}
/**
* The first dereference of a variable in a given `BasicBlock` excluding those dereferences
* that are preceded by a not-null assertion or a trivially failing assertion.
* The first dereference of a variable in a given `BasicBlock`.
*/
private predicate firstVarDereferenceInBlock(BasicBlock bb, SsaVariable v, VarAccess va) {
exists(ControlFlowNode n |
varDereference(v, va) = n and
n.getBasicBlock() = bb and
not unreachableVarDereference(bb, v, n)
n =
min(ControlFlowNode n0, int i |
varDereference(v, _) = n0 and bb.getNode(i) = n0
|
n0 order by i
)
)
}
/** 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.
@@ -195,6 +157,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
@@ -205,7 +168,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"
)
@@ -227,7 +190,7 @@ private Expr nonEmptyExpr() {
// ...or it is guarded by a condition proving its length to be non-zero.
exists(ConditionBlock cond, boolean branch, FieldAccess length |
cond.controls(result.getBasicBlock(), branch) and
cond.getCondition() = integerGuard(length, branch, 0, false) and
cond.getCondition() = nonZeroGuard(length, branch) and
length.getField().hasName("length") and
length.getQualifier() = v.getAUse()
)
@@ -257,7 +220,7 @@ private Expr nonEmptyExpr() {
or
// ...or a check on its `size`.
exists(MethodCall size |
c = integerGuard(size, branch, 0, false) and
c = nonZeroGuard(size, branch) and
size.getMethod().hasName("size") and
size.getQualifier() = v.getAUse()
)
@@ -285,536 +248,29 @@ private predicate impossibleEdge(BasicBlock bb1, BasicBlock bb2) {
)
}
/** A control flow edge that leaves a finally-block. */
private predicate leavingFinally(BasicBlock bb1, BasicBlock bb2, boolean normaledge) {
exists(TryStmt try, BlockStmt finally |
try.getFinally() = finally and
bb1.getASuccessor() = bb2 and
bb1.getFirstNode().getEnclosingStmt().getEnclosingStmt*() = finally and
not bb2.getFirstNode().getEnclosingStmt().getEnclosingStmt*() = finally and
if bb1.getLastNode().getANormalSuccessor() = bb2.getFirstNode()
then normaledge = true
else normaledge = false
)
private module NullnessConfig implements Cf::ControlFlow::ConfigSig {
predicate source(ControlFlowNode node, SsaVariable def) { varMaybeNull(def, node, _, _) }
predicate sink(ControlFlowNode node, SsaVariable def) { varDereference(def, _) = node }
predicate barrierValue(GuardValue gv) { gv.isNullness(false) }
predicate barrierEdge(BasicBlock bb1, BasicBlock bb2) { impossibleEdge(bb1, bb2) }
predicate uncertainFlow() { none() }
}
private predicate ssaSourceVarMaybeNull(SsaSourceVariable v) {
varMaybeNull(v.getAnSsaVariable(), _, _)
}
private module NullnessFlow = Cf::ControlFlow::Flow<NullnessConfig>;
/**
* The step relation for propagating that a given SSA variable might be `null` in a given `BasicBlock`.
*
* If `midssa` is null in `mid` then `ssa` might be null in `bb`. The SSA variables share the same
* `SsaSourceVariable`.
*
* A boolean flag tracks whether a non-normal completion is waiting to resume upon the exit of a finally-block.
* If the flag is set, then the normal edge out of the finally-block is prohibited, but if it is not set then
* no knowledge is assumed of any potentially waiting completions. `midstoredcompletion` is the flag before
* the step and `storedcompletion` is the flag after the step.
*/
private predicate nullVarStep(
SsaVariable midssa, BasicBlock mid, boolean midstoredcompletion, SsaVariable ssa, BasicBlock bb,
boolean storedcompletion
) {
exists(SsaSourceVariable v |
ssaSourceVarMaybeNull(v) and
midssa.getSourceVariable() = v
|
ssa.(SsaPhiNode).getAPhiInput() = midssa and ssa.getBasicBlock() = bb
or
ssa = midssa and
not exists(SsaPhiNode phi | phi.getSourceVariable() = v and phi.getBasicBlock() = bb)
) and
(midstoredcompletion = true or midstoredcompletion = false) and
midssa.isLiveAtEndOfBlock(mid) and
not ensureNotNull(midssa).getBasicBlock() = mid and
not assertFail(mid, _) and
bb = mid.getASuccessor() and
not impossibleEdge(mid, bb) and
not nullGuardControlsBranchEdge(midssa, false, mid, bb) and
not (leavingFinally(mid, bb, true) and midstoredcompletion = true) and
if bb.getFirstNode().asStmt() = any(TryStmt try | | try.getFinally())
then
if bb.getFirstNode() = mid.getLastNode().getANormalSuccessor()
then storedcompletion = false
else storedcompletion = true
else
if leavingFinally(mid, bb, _)
then storedcompletion = false
else storedcompletion = midstoredcompletion
}
/**
* The transitive closure of `nullVarStep` originating from `varMaybeNull`. That is, those `BasicBlock`s
* for which the SSA variable is suspected of being `null`.
*/
private predicate varMaybeNullInBlock(
SsaVariable ssa, SsaSourceVariable v, BasicBlock bb, boolean storedcompletion
) {
varMaybeNull(ssa, _, _) and
bb = ssa.getBasicBlock() and
storedcompletion = false and
v = ssa.getSourceVariable()
or
exists(BasicBlock mid, SsaVariable midssa, boolean midstoredcompletion |
varMaybeNullInBlock(midssa, v, mid, midstoredcompletion) and
nullVarStep(midssa, mid, midstoredcompletion, ssa, bb, storedcompletion)
)
}
/**
* Holds if `v` is a source variable that might reach a potential `null`
* dereference.
*/
private predicate nullDerefCandidateVariable(SsaSourceVariable v) {
exists(SsaVariable ssa, BasicBlock bb |
firstVarDereferenceInBlock(bb, ssa, _) and
varMaybeNullInBlock(ssa, v, bb, _)
)
}
private predicate varMaybeNullInBlock_origin(
SsaVariable origin, SsaVariable ssa, BasicBlock bb, boolean storedcompletion
) {
nullDerefCandidateVariable(ssa.getSourceVariable()) and
varMaybeNull(ssa, _, _) and
bb = ssa.getBasicBlock() and
storedcompletion = false and
origin = ssa
or
exists(BasicBlock mid, SsaVariable midssa, boolean midstoredcompletion |
varMaybeNullInBlock_origin(origin, midssa, mid, midstoredcompletion) and
nullVarStep(midssa, mid, midstoredcompletion, ssa, bb, storedcompletion)
)
}
/**
* A potential `null` dereference. That is, the first dereference of a variable in a block
* where it is suspected of being `null`.
*/
private predicate nullDerefCandidate(SsaVariable origin, VarAccess va) {
exists(SsaVariable ssa, BasicBlock bb |
firstVarDereferenceInBlock(bb, ssa, va) and
varMaybeNullInBlock_origin(origin, ssa, bb, _)
)
}
/*
* In the following, the potential `null` dereference candidates are pruned by proving that
* a `NullPointerException` (NPE) cannot occur. This is done by pruning the control-flow paths
* that lead to the NPE candidate in two ways:
*
* 1. For each set of correlated conditions that are passed by the path, consistent
* branches must be taken. For example, the following code is safe due to the two tests on
* `flag` begin correlated.
* ```
* x = null;
* if (flag) x = new A();
* if (flag) x.m();
* ```
*
* 2. For each other variable that changes its value alongside the potential NPE candidate,
* the passed conditions must be consistent with its value. For example, the following
* code is safe due to the value of `t`.
* ```
* x = null;
* t = null;
* if (...) { x = new A(); t = new B(); }
* if (t != null) x.m();
* ```
* We call such a variable a _tracking variable_ as it tracks the null-ness of `x`.
*/
/** A variable that is assigned `null` if the given condition takes the given branch. */
private predicate varConditionallyNull(SsaExplicitUpdate v, ConditionBlock cond, boolean branch) {
exists(ConditionalExpr condexpr |
v.getDefiningExpr().(VariableAssign).getSource() = condexpr and
condexpr.getCondition() = cond.getCondition()
|
condexpr.getBranchExpr(branch) = nullExpr() and
not condexpr.getBranchExpr(branch.booleanNot()) = nullExpr()
)
or
v.getDefiningExpr().(VariableAssign).getSource() = nullExpr() and
cond.controls(v.getBasicBlock(), branch)
}
/**
* A condition that might be useful in proving an NPE candidate safe.
*
* This is a condition along the path that found the NPE candidate.
*/
private predicate interestingCond(SsaSourceVariable npecand, ConditionBlock cond) {
nullDerefCandidateVariable(npecand) and
(
varMaybeNullInBlock(_, npecand, cond, _) or
varConditionallyNull(npecand.getAnSsaVariable(), cond, _)
) and
not cond.getCondition().(Expr).getAChildExpr*() = npecand.getAnAccess()
}
pragma[nomagic]
private ConditionBlock ssaIntegerGuard(SsaVariable v, boolean branch, int k, boolean is_k) {
result.getCondition() = integerGuard(v.getAUse(), branch, k, is_k)
}
pragma[nomagic]
private ConditionBlock ssaIntBoundGuard(SsaVariable v, boolean branch_with_lower_bound_k, int k) {
result.getCondition() = intBoundGuard(v.getAUse(), branch_with_lower_bound_k, k)
}
pragma[nomagic]
private ConditionBlock ssaEnumConstEquality(SsaVariable v, boolean polarity, EnumConstant c) {
result.getCondition() = enumConstEquality(v.getAUse(), polarity, c)
}
private predicate conditionChecksNull(ConditionBlock cond, SsaVariable v, boolean branchIsNull) {
nullGuardControlsBranchEdge(v, true, cond, cond.getTestSuccessor(branchIsNull)) and
nullGuardControlsBranchEdge(v, false, cond, cond.getTestSuccessor(branchIsNull.booleanNot()))
}
/** A pair of correlated conditions for a given NPE candidate. */
private predicate correlatedConditions(
SsaSourceVariable npecand, ConditionBlock cond1, ConditionBlock cond2, boolean inverted
) {
interestingCond(npecand, cond1) and
interestingCond(npecand, cond2) and
cond1 != cond2 and
(
exists(SsaVariable v |
cond1.getCondition() = v.getAUse() and
cond2.getCondition() = v.getAUse() and
inverted = false
)
or
exists(SsaVariable v, boolean branch1, boolean branch2 |
conditionChecksNull(cond1, v, branch1) and
conditionChecksNull(cond2, v, branch2) and
inverted = branch1.booleanXor(branch2)
)
or
exists(SsaVariable v, int k, boolean branch1, boolean branch2 |
cond1 = ssaIntegerGuard(v, branch1, k, true) and
cond1 = ssaIntegerGuard(v, branch1.booleanNot(), k, false) and
cond2 = ssaIntegerGuard(v, branch2, k, true) and
cond2 = ssaIntegerGuard(v, branch2.booleanNot(), k, false) and
inverted = branch1.booleanXor(branch2)
)
or
exists(SsaVariable v, int k, boolean branch1, boolean branch2 |
cond1 = ssaIntBoundGuard(v, branch1, k) and
cond2 = ssaIntBoundGuard(v, branch2, k) and
inverted = branch1.booleanXor(branch2)
)
or
exists(SsaVariable v, EnumConstant c, boolean pol1, boolean pol2 |
cond1 = ssaEnumConstEquality(v, pol1, c) and
cond2 = ssaEnumConstEquality(v, pol2, c) and
inverted = pol1.booleanXor(pol2)
)
or
exists(SsaVariable v, RefType type |
cond1.getCondition() = instanceofExpr(v, type) and
cond2.getCondition() = instanceofExpr(v, type) and
inverted = false
)
or
exists(SsaVariable v1, SsaVariable v2, boolean branch1, boolean branch2 |
cond1.getCondition() = varEqualityTestExpr(v1, v2, branch1) and
cond2.getCondition() = varEqualityTestExpr(v1, v2, branch2) and
inverted = branch1.booleanXor(branch2)
)
)
}
/**
* This is again the transitive closure of `nullVarStep` similarly to `varMaybeNullInBlock`, but
* this time restricted based on pairs of correlated conditions consistent with `cond1`
* evaluating to `branch`.
*/
private predicate varMaybeNullInBlock_corrCond(
SsaVariable origin, SsaVariable ssa, BasicBlock bb, boolean storedcompletion,
ConditionBlock cond1, boolean branch
) {
exists(SsaSourceVariable npecand | npecand = ssa.getSourceVariable() |
nullDerefCandidateVariable(npecand) and correlatedConditions(npecand, cond1, _, _)
) and
(
varConditionallyNull(ssa, cond1, branch)
or
not varConditionallyNull(ssa, cond1, _) and
(branch = true or branch = false)
) and
varMaybeNull(ssa, _, _) and
bb = ssa.getBasicBlock() and
storedcompletion = false and
origin = ssa
or
exists(BasicBlock mid, SsaVariable midssa, boolean midstoredcompletion |
varMaybeNullInBlock_corrCond(origin, midssa, mid, midstoredcompletion, cond1, branch) and
(
cond1 = mid and cond1.getTestSuccessor(branch) = bb
or
exists(ConditionBlock cond2, boolean inverted, boolean branch2 |
cond2 = mid and
correlatedConditions(_, cond1, cond2, inverted) and
cond2.getTestSuccessor(branch2) = bb and
branch = branch2.booleanXor(inverted)
)
or
cond1 != mid and
not exists(ConditionBlock cond2 | cond2 = mid and correlatedConditions(_, cond1, cond2, _))
) and
nullVarStep(midssa, mid, midstoredcompletion, ssa, bb, storedcompletion)
)
}
/*
* A tracking variable has its possible values divided into two sets, A and B, for
* which we can attribute at least one direct assignment to be contained in either
* A or B.
* Four kinds are supported:
* - null: A means null and B means non-null.
* - boolean: A means true and B means false.
* - enum: A means a specific enum constant and B means any other value.
* - int: A means a specific integer value and B means any other value.
*/
private newtype TrackVarKind =
TrackVarKindNull() or
TrackVarKindBool() or
TrackVarKindEnum() or
TrackVarKindInt()
/** A variable that might be relevant as a tracking variable for the NPE candidate. */
private predicate trackingVar(
SsaSourceVariable npecand, SsaExplicitUpdate trackssa, SsaSourceVariable trackvar,
TrackVarKind kind, Expr init
) {
exists(ConditionBlock cond |
interestingCond(npecand, cond) and
varMaybeNullInBlock(_, npecand, cond, _) and
cond.getCondition().(Expr).getAChildExpr*() = trackvar.getAnAccess() and
trackssa.getSourceVariable() = trackvar and
trackssa.getDefiningExpr().(VariableAssign).getSource() = init
|
init instanceof NullLiteral and kind = TrackVarKindNull()
or
init = clearlyNotNullExpr() and kind = TrackVarKindNull()
or
init instanceof BooleanLiteral and kind = TrackVarKindBool()
or
init.(VarAccess).getVariable() instanceof EnumConstant and kind = TrackVarKindEnum()
or
exists(init.(ConstantIntegerExpr).getIntValue()) and kind = TrackVarKindInt()
)
}
/** Gets an expression that tests the value of a given tracking variable. */
private Expr trackingVarGuard(
SsaVariable trackssa, SsaSourceVariable trackvar, TrackVarKind kind, boolean branch, boolean isA
) {
exists(Expr init | trackingVar(_, trackssa, trackvar, kind, init) |
result = basicNullGuard(trackvar.getAnAccess(), branch, isA) and
kind = TrackVarKindNull()
or
result = trackvar.getAnAccess() and
kind = TrackVarKindBool() and
(branch = true or branch = false) and
isA = branch
or
exists(boolean polarity, EnumConstant c, EnumConstant initc |
initc.getAnAccess() = init and
kind = TrackVarKindEnum() and
result = enumConstEquality(trackvar.getAnAccess(), polarity, c) and
(
initc = c and branch = polarity.booleanNot() and isA = false
or
initc = c and branch = polarity and isA = true
or
initc != c and branch = polarity and isA = false
)
)
or
exists(int k |
init.(ConstantIntegerExpr).getIntValue() = k and
kind = TrackVarKindInt()
|
result = integerGuard(trackvar.getAnAccess(), branch, k, isA)
or
exists(int k2 |
result = integerGuard(trackvar.getAnAccess(), branch, k2, true) and
isA = false and
k2 != k
)
or
exists(int bound, boolean branch_with_lower_bound |
result = intBoundGuard(trackvar.getAnAccess(), branch_with_lower_bound, bound) and
isA = false
|
branch = branch_with_lower_bound and k < bound
or
branch = branch_with_lower_bound.booleanNot() and bound <= k
)
)
)
or
exists(EqualityTest eqtest, boolean branch0, boolean polarity, BooleanLiteral boollit |
eqtest = result and
eqtest.hasOperands(trackingVarGuard(trackssa, trackvar, kind, branch0, isA), boollit) and
eqtest.polarity() = polarity and
branch = branch0.booleanXor(polarity).booleanXor(boollit.getBooleanValue())
)
}
/** An update to a tracking variable that is contained fully in either A or B. */
private predicate isReset(
SsaVariable trackssa, SsaSourceVariable trackvar, TrackVarKind kind, SsaExplicitUpdate update,
boolean isA
) {
exists(Expr init, Expr e |
trackingVar(_, trackssa, trackvar, kind, init) and
update.getSourceVariable() = trackvar and
e = update.getDefiningExpr().(VariableAssign).getSource()
|
e instanceof NullLiteral and kind = TrackVarKindNull() and isA = true
or
e = clearlyNotNullExpr() and kind = TrackVarKindNull() and isA = false
or
e.(BooleanLiteral).getBooleanValue() = isA and kind = TrackVarKindBool()
or
e.(VarAccess).getVariable().(EnumConstant) = init.(VarAccess).getVariable() and
kind = TrackVarKindEnum() and
isA = true
or
e.(VarAccess).getVariable().(EnumConstant) != init.(VarAccess).getVariable() and
kind = TrackVarKindEnum() and
isA = false
or
e.(ConstantIntegerExpr).getIntValue() = init.(ConstantIntegerExpr).getIntValue() and
kind = TrackVarKindInt() and
isA = true
or
e.(ConstantIntegerExpr).getIntValue() != init.(ConstantIntegerExpr).getIntValue() and
kind = TrackVarKindInt() and
isA = false
)
}
/** The abstract value of the tracked variable. */
private newtype TrackedValue =
TrackedValueA() or
TrackedValueB() or
TrackedValueUnknown()
private TrackedValue trackValAorB(boolean isA) {
isA = true and result = TrackedValueA()
or
isA = false and result = TrackedValueB()
}
/** A control flow edge passing through a condition that implies a specific value for a tracking variable. */
private predicate stepImplies(
BasicBlock bb1, BasicBlock bb2, SsaVariable trackssa, SsaSourceVariable trackvar,
TrackVarKind kind, boolean isA
) {
exists(ConditionBlock cond, boolean branch |
cond = bb1 and
cond.getTestSuccessor(branch) = bb2 and
cond.getCondition() = trackingVarGuard(trackssa, trackvar, kind, branch, isA)
)
}
/**
* This is again the transitive closure of `nullVarStep` similarly to `varMaybeNullInBlock`, but
* this time restricted based on a tracking variable.
*/
private predicate varMaybeNullInBlock_trackVar(
SsaVariable origin, SsaVariable ssa, BasicBlock bb, boolean storedcompletion,
SsaVariable trackssa, SsaSourceVariable trackvar, TrackVarKind kind, TrackedValue trackvalue
) {
exists(SsaSourceVariable npecand | npecand = ssa.getSourceVariable() |
nullDerefCandidateVariable(npecand) and trackingVar(npecand, trackssa, trackvar, kind, _)
) and
(
exists(SsaVariable init, boolean isA |
init.getSourceVariable() = trackvar and
init.isLiveAtEndOfBlock(bb) and
isReset(trackssa, trackvar, kind, init, isA) and
trackvalue = trackValAorB(isA)
)
or
trackvalue = TrackedValueUnknown() and
not exists(SsaVariable init |
init.getSourceVariable() = trackvar and
init.isLiveAtEndOfBlock(bb) and
isReset(trackssa, trackvar, kind, init, _)
)
) and
varMaybeNull(ssa, _, _) and
bb = ssa.getBasicBlock() and
storedcompletion = false and
origin = ssa
or
exists(BasicBlock mid, SsaVariable midssa, boolean midstoredcompletion, TrackedValue trackvalue0 |
varMaybeNullInBlock_trackVar(origin, midssa, mid, midstoredcompletion, trackssa, trackvar, kind,
trackvalue0) and
nullVarStep(midssa, mid, midstoredcompletion, ssa, bb, storedcompletion) and
(
trackvalue0 = TrackedValueUnknown()
or
// A step that implies a value that contradicts the current value is not allowed.
exists(boolean isA | trackvalue0 = trackValAorB(isA) |
not stepImplies(mid, bb, trackssa, trackvar, kind, isA.booleanNot())
)
) and
(
// If no update occurs then the tracked value is unchanged unless the step implies a given value via a condition.
not exists(SsaUpdate update |
update.getSourceVariable() = trackvar and
update.getBasicBlock() = bb
) and
(
exists(boolean isA | stepImplies(mid, bb, trackssa, trackvar, kind, isA) |
trackvalue = trackValAorB(isA)
)
or
not stepImplies(mid, bb, trackssa, trackvar, kind, _) and trackvalue = trackvalue0
)
or
// If an update occurs then the tracked value is set accordingly.
exists(SsaUpdate update |
update.getSourceVariable() = trackvar and
update.getBasicBlock() = bb
|
exists(boolean isA | isReset(trackssa, trackvar, kind, update, isA) |
trackvalue = trackValAorB(isA)
)
or
not isReset(trackssa, trackvar, kind, update, _) and trackvalue = TrackedValueUnknown()
)
)
)
}
/**
* A potential `null` dereference that has not been proven safe.
* Holds if the dereference of `v` at `va` might be `null`.
*/
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
exists(SsaVariable origin, SsaVariable ssa, ControlFlowNode src, ControlFlowNode sink |
varMaybeNull(origin, src, msg, reason) and
NullnessFlow::flow(src, origin, sink, ssa) and
ssa.getSourceVariable() = v and
firstVarDereferenceInBlock(bb, ssa, va) and
forall(ConditionBlock cond | correlatedConditions(v, cond, _, _) |
varMaybeNullInBlock_corrCond(origin, ssa, bb, _, cond, _)
) and
forall(SsaVariable guardssa, SsaSourceVariable guardvar, TrackVarKind kind |
trackingVar(v, guardssa, guardvar, kind, _)
|
varMaybeNullInBlock_trackVar(origin, ssa, bb, _, guardssa, guardvar, kind, _)
)
varDereference(ssa, va) = sink
)
}

4
java/ql/src/change-notes/2025-09-15-nullness-reimp.md Normal file
View File

@@ -0,0 +1,4 @@
---
category: majorAnalysis
---
* The implementation of `java/dereferenced-value-may-be-null` has been completely replaced with a new general control-flow reachability library. This improves precision by reducing false positives. However, since the entire calculation has been reworked, there can be small corner cases where precision regressions might occur and new false positives may occur, but these cases should be rare.

6
java/ql/test/library-tests/guards/Guards.java
View File

@@ -26,7 +26,7 @@ public class Guards {
}
int sz = a != null ? a.length : 0;
for (int i = 0; i < sz; i++) {
chk(); // $ guarded='a != null:true' guarded='i < sz:true' guarded='sz:not 0' guarded='...?...:...:not 0' guarded='a.length:not 0' guarded='a:not null'
chk(); // $ guarded='a != null:true' guarded='i < sz:true' guarded='sz:Lower bound 1' guarded='...?...:...:Lower bound 1' guarded='a.length:Lower bound 1' guarded='a:not null'
int e = a[i];
if (e > 2) break;
}
@@ -136,11 +136,11 @@ public class Guards {
found = true;
}
if (found) {
chk(); // $ guarded=found:true guarded='i < a.length:true'
chk(); // $ guarded=found:true guarded='i < a.length:true' guarded='a.length:Lower bound 1'
}
}
if (found) {
chk(); // $ guarded=found:true guarded='i < a.length:false'
chk(); // $ guarded=found:true guarded='i < a.length:false' guarded='i:Lower bound 0'
}
}

8
java/ql/test/library-tests/guards/GuardsInline.expected
View File

@@ -8,12 +8,12 @@
| Guards.java:25:7:25:11 | chk(...) | b:false |
| Guards.java:25:7:25:11 | chk(...) | g(1):true |
| Guards.java:25:7:25:11 | chk(...) | g(2):false |
| Guards.java:29:7:29:11 | chk(...) | '...?...:...:not 0' |
| Guards.java:29:7:29:11 | chk(...) | '...?...:...:Lower bound 1' |
| Guards.java:29:7:29:11 | chk(...) | 'a != null:true' |
| Guards.java:29:7:29:11 | chk(...) | 'a.length:not 0' |
| Guards.java:29:7:29:11 | chk(...) | 'a.length:Lower bound 1' |
| Guards.java:29:7:29:11 | chk(...) | 'a:not null' |
| Guards.java:29:7:29:11 | chk(...) | 'i < sz:true' |
| Guards.java:29:7:29:11 | chk(...) | 'sz:not 0' |
| Guards.java:29:7:29:11 | chk(...) | 'sz:Lower bound 1' |
| Guards.java:39:9:39:13 | chk(...) | 's:bar' |
| Guards.java:39:9:39:13 | chk(...) | 's:match "bar"' |
| Guards.java:42:9:42:13 | chk(...) | 's:foo' |
@@ -85,9 +85,11 @@
| Guards.java:127:7:127:11 | chk(...) | 'o != null:false' |
| Guards.java:127:7:127:11 | chk(...) | 'o:null' |
| Guards.java:127:7:127:11 | chk(...) | g(1):false |
| Guards.java:139:9:139:13 | chk(...) | 'a.length:Lower bound 1' |
| Guards.java:139:9:139:13 | chk(...) | 'i < a.length:true' |
| Guards.java:139:9:139:13 | chk(...) | found:true |
| Guards.java:143:7:143:11 | chk(...) | 'i < a.length:false' |
| Guards.java:143:7:143:11 | chk(...) | 'i:Lower bound 0' |
| Guards.java:143:7:143:11 | chk(...) | found:true |
| Guards.java:173:7:173:11 | chk(...) | 's:not null' |
| Guards.java:173:7:173:11 | chk(...) | testNotNull1(...):true |

2
java/ql/test/query-tests/Nullness/A.java
View File

@@ -301,7 +301,7 @@ public class A {
public void assertThatTest() {
Object assertThat_ok1 = maybe() ? null : new Object();
assertThat(assertThat_ok1, notNullValue());
assertThat_ok1.toString();
assertThat_ok1.toString(); // OK
}
private boolean m;

60
java/ql/test/query-tests/Nullness/B.java
View File

@@ -276,7 +276,7 @@ public class B {
int[] a = null;
if (iters > 0) a = new int[iters];
for (int i = 0; i < iters; ++i)
a[i] = 0; // NPE - false positive
a[i] = 0; // OK
if (iters > 0) {
String last = null;
@@ -289,7 +289,7 @@ public class B {
throw new RuntimeException();
}
for (int i = 0; i < iters; ++i) {
b[i] = 0; // NPE - false positive
b[i] = 0; // OK
}
}
@@ -331,7 +331,7 @@ public class B {
x = new Object();
}
if(y instanceof String) {
x.hashCode(); // OK
x.hashCode(); // Spurious NPE - false positive
}
}
@@ -341,7 +341,7 @@ public class B {
x = new Object();
}
if(!(y instanceof String)) {
x.hashCode(); // OK
x.hashCode(); // Spurious NPE - false positive
}
}
@@ -351,7 +351,7 @@ public class B {
x = new Object();
}
if(y == z) {
x.hashCode(); // OK
x.hashCode(); // Spurious NPE - false positive
}
Object x2 = null;
@@ -359,7 +359,7 @@ public class B {
x2 = new Object();
}
if(y != z) {
x2.hashCode(); // OK
x2.hashCode(); // Spurious NPE - false positive
}
Object x3 = null;
@@ -367,7 +367,7 @@ public class B {
x3 = new Object();
}
if(!(y == z)) {
x3.hashCode(); // OK
x3.hashCode(); // Spurious NPE - false positive
}
}
@@ -417,7 +417,7 @@ public class B {
x = null;
}
if (!b) {
x.hashCode(); // NPE - false negative
x.hashCode(); // NPE
}
// flow can loop around from one iteration to the next
}
@@ -445,7 +445,7 @@ public class B {
if (!ready) {
x = null;
} else {
x.hashCode(); // Spurious NPE - false positive
x.hashCode(); // OK
}
if ((a[i] & 1) != 0) {
ready = (a[i] & 2) != 0;
@@ -515,4 +515,46 @@ public class B {
if (c == 100) { return; }
o.hashCode(); // NPE
}
public void testFinally(int[] xs, int[] ys) {
if (xs.length == 0) return;
if (ys.length == 0) return;
String s1 = null;
String s2 = null;
for (int x : xs) {
try {
if (x == 0) { break; }
s1 = "1";
for (int y : ys) {
if (y == 0) { break; }
s2 = "2";
}
} finally {
}
s1.hashCode(); // OK
s2.hashCode(); // NPE
}
s1.hashCode(); // NPE - false negative, Java CFG lacks proper edge label
}
public void lenCheck(int[] xs, int n, int t) {
if (n > 42) return;
if (maybe) {}
if (n > 0 && (xs == null || xs.length < n)) {
return;
}
if (maybe) {}
if (n > 21) return;
if (maybe) {}
for (int i = 0; i < n; ++i) {
xs[i]++; // OK
}
}
public void rangetest(int n) {
String s = null;
if (n < 0 || n > 10) s = "A";
if (n > 100) s.hashCode(); // OK
if (n == 42) s.hashCode(); // OK
}
}

8
java/ql/test/query-tests/Nullness/C.java
View File

@@ -97,7 +97,7 @@ public class C {
arr2 = new int[arr1.length];
}
for (int i = 0; i < arr1.length; i++)
arr2[i] = arr1[i]; // NPE - false positive
arr2[i] = arr1[i]; // OK
}
public void ex8(int x, int lim) {
@@ -107,7 +107,7 @@ public class C {
while (!stop) {
int j = 0;
while (!stop && j < lim) {
int step = (j * obj.hashCode()) % 10; // NPE - false positive
int step = (j * obj.hashCode()) % 10; // OK
if (step == 0) {
obj.hashCode();
i += 1;
@@ -134,7 +134,7 @@ public class C {
cond = true;
}
if (cond) {
obj2.hashCode(); // NPE - false positive
obj2.hashCode(); // OK
}
}
@@ -185,7 +185,7 @@ public class C {
b = true;
} else if (a[i] == 2) {
verifyBool(b);
obj.hashCode(); // NPE - false positive
obj.hashCode(); // OK
}
}
}

14
java/ql/test/query-tests/Nullness/NullMaybe.expected
View File

@@ -15,24 +15,24 @@
| B.java:118:5:118:7 | obj | Variable $@ may be null at this access as suggested by $@ null guard. | B.java:117:27:117:36 | obj | obj | B.java:119:13:119:23 | ... != ... | this |
| B.java:133:5:133:7 | obj | Variable $@ may be null at this access because of $@ assignment. | B.java:128:5:128:22 | Object obj | obj | B.java:128:12:128:21 | obj | this |
| B.java:190:7:190:7 | o | Variable $@ may be null at this access because of $@ assignment. | B.java:178:5:178:20 | Object o | o | B.java:186:5:186:12 | ...=... | this |
| B.java:279:7:279:7 | a | Variable $@ may be null at this access because of $@ assignment. | B.java:276:5:276:19 | int[] a | a | B.java:276:11:276:18 | a | this |
| B.java:292:7:292:7 | b | Variable $@ may be null at this access because of $@ assignment. | B.java:287:5:287:44 | int[] b | b | B.java:287:11:287:43 | b | this |
| B.java:334:7:334:7 | x | Variable $@ may be null at this access because of $@ assignment. | B.java:329:5:329:20 | Object x | x | B.java:329:12:329:19 | x | this |
| B.java:344:7:344:7 | x | Variable $@ may be null at this access because of $@ assignment. | B.java:339:5:339:20 | Object x | x | B.java:339:12:339:19 | x | this |
| B.java:354:7:354:7 | x | Variable $@ may be null at this access because of $@ assignment. | B.java:349:5:349:20 | Object x | x | B.java:349:12:349:19 | x | this |
| B.java:362:7:362:8 | x2 | Variable $@ may be null at this access because of $@ assignment. | B.java:357:5:357:21 | Object x2 | x2 | B.java:357:12:357:20 | x2 | this |
| B.java:370:7:370:8 | x3 | Variable $@ may be null at this access because of $@ assignment. | B.java:365:5:365:21 | Object x3 | x3 | B.java:365:12:365:20 | x3 | this |
| B.java:408:7:408:7 | x | Variable $@ may be null at this access as suggested by $@ null guard. | B.java:374:23:374:30 | x | x | B.java:375:23:375:31 | ... != ... | this |
| B.java:448:9:448:9 | x | Variable $@ may be null at this access because of $@ assignment. | B.java:442:5:442:28 | Object x | x | B.java:446:9:446:16 | ...=... | this |
| B.java:420:9:420:9 | x | Variable $@ may be null at this access because of $@ assignment. | B.java:413:5:413:28 | Object x | x | B.java:417:9:417:16 | ...=... | this |
| B.java:465:9:465:9 | x | Variable $@ may be null at this access because of $@ assignment. | B.java:458:5:458:28 | Object x | x | B.java:470:9:470:16 | ...=... | this |
| B.java:487:9:487:9 | x | Variable $@ may be null at this access because of $@ assignment. | B.java:476:5:476:20 | Object x | x | B.java:476:12:476:19 | x | this |
| B.java:516:5:516:5 | o | Variable $@ may be null at this access as suggested by $@ null guard. | B.java:511:25:511:32 | o | o | B.java:512:22:512:30 | ... == ... | this |
| B.java:535:7:535:8 | s2 | Variable $@ may be null at this access because of $@ assignment. | B.java:523:5:523:21 | String s2 | s2 | B.java:523:12:523:20 | s2 | this |
| C.java:9:44:9:45 | a2 | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:6:5:6:23 | long[][] a2 | a2 | C.java:7:34:7:54 | ... != ... | this |
| C.java:9:44:9:45 | a2 | Variable $@ may be null at this access because of $@ assignment. | C.java:6:5:6:23 | long[][] a2 | a2 | C.java:6:14:6:22 | a2 | this |
| C.java:10:17:10:18 | a3 | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:8:5:8:21 | long[] a3 | a3 | C.java:9:38:9:58 | ... != ... | this |
| C.java:10:17:10:18 | a3 | Variable $@ may be null at this access because of $@ assignment. | C.java:8:5:8:21 | long[] a3 | a3 | C.java:8:12:8:20 | a3 | this |
| C.java:21:7:21:8 | s1 | Variable $@ may be null at this access because of $@ assignment. | C.java:14:5:14:30 | String s1 | s1 | C.java:17:7:17:24 | ...=... | this |
| C.java:51:7:51:11 | slice | Variable $@ may be null at this access because of $@ assignment. | C.java:43:5:43:30 | List<String> slice | slice | C.java:43:18:43:29 | slice | this |
| C.java:100:7:100:10 | arr2 | Variable $@ may be null at this access because of $@ assignment. | C.java:95:5:95:22 | int[] arr2 | arr2 | C.java:95:11:95:21 | arr2 | this |
| C.java:110:25:110:27 | obj | Variable $@ may be null at this access because of $@ assignment. | C.java:106:5:106:30 | Object obj | obj | C.java:118:13:118:22 | ...=... | this |
| C.java:137:7:137:10 | obj2 | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:131:5:131:23 | Object obj2 | obj2 | C.java:132:9:132:20 | ... != ... | this |
| C.java:144:15:144:15 | a | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:141:20:141:26 | a | a | C.java:142:13:142:21 | ... == ... | this |
| C.java:188:9:188:11 | obj | Variable $@ may be null at this access because of $@ assignment. | C.java:181:5:181:22 | Object obj | obj | C.java:181:12:181:21 | obj | this |
| C.java:219:9:219:10 | o1 | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:212:20:212:28 | o1 | o1 | C.java:213:9:213:18 | ... == ... | this |
| C.java:233:7:233:8 | xs | Variable $@ may be null at this access because of $@ assignment. | C.java:231:5:231:56 | int[] xs | xs | C.java:231:11:231:55 | xs | this |
| F.java:11:5:11:7 | obj | Variable $@ may be null at this access as suggested by $@ null guard. | F.java:8:18:8:27 | obj | obj | F.java:9:9:9:19 | ... == ... | this |

929
shared/controlflow/codeql/controlflow/ControlFlow.qll Normal file
View File

@@ -0,0 +1,929 @@
/**
* Provides an implementation of local (intraprocedural) control flow reachability.
*/
overlay[local?]
module;
private import codeql.controlflow.BasicBlock as BB
private import codeql.controlflow.SuccessorType
private import codeql.util.Boolean
private import codeql.util.Location
private import codeql.util.Option
private signature class TypSig;
signature module InputSig<LocationSig Location, TypSig ControlFlowNode, TypSig BasicBlock> {
AstNode getEnclosingAstNode(ControlFlowNode node);
class AstNode {
/** Gets a textual representation of this AST node. */
string toString();
/** Gets the location of this AST node. */
Location getLocation();
}
AstNode getParent(AstNode node);
class Expr extends AstNode;
class FinallyBlock extends AstNode;
/** A variable that can be SSA converted. */
class SourceVariable {
/** Gets a textual representation of this variable. */
string toString();
/** Gets the location of this variable. */
Location getLocation();
}
class SsaDefinition {
SourceVariable getSourceVariable();
predicate definesAt(SourceVariable v, BasicBlock bb, int i);
/** Gets the basic block to which this SSA definition belongs. */
BasicBlock getBasicBlock();
/** Gets a textual representation of this SSA definition. */
string toString();
/** Gets the location of this SSA definition. */
Location getLocation();
/** Holds if this SSA variable is live at the end of `b`. */
predicate isLiveAtEndOfBlock(BasicBlock b);
}
class SsaWriteDefinition extends SsaDefinition {
Expr getDefinition();
}
class SsaPhiNode extends SsaDefinition {
/** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb);
SsaDefinition getAPhiInput();
}
class SsaUncertainDefinition extends SsaDefinition {
/**
* Gets the immediately preceding definition. Since this update is uncertain,
* the value from the preceding definition might still be valid.
*/
SsaDefinition getPriorDefinition();
}
/** An abstract value that a `Guard` may evaluate to. */
class GuardValue {
/** Gets a textual representation of this value. */
string toString();
/**
* Gets the dual value. Examples of dual values include:
* - null vs. not null
* - true vs. false
* - evaluating to a specific value vs. evaluating to any other value
* - throwing an exception vs. not throwing an exception
*/
GuardValue getDualValue();
/** Gets the integer that this value represents, if any. */
int asIntValue();
/**
* 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);
}
/**
* Holds if `def` evaluating to `v` controls the control-flow branch
* edge from `bb1` to `bb2`. That is, following the edge from `bb1` to
* `bb2` implies that `def` evaluated to `v`.
*/
predicate ssaControlsBranchEdge(SsaDefinition def, BasicBlock bb1, BasicBlock bb2, GuardValue v);
/**
* Holds if `def` evaluating to `v` controls the basic block `bb`.
* That is, execution of `bb` implies that `def` evaluated to `v`.
*/
predicate ssaControls(SsaDefinition def, BasicBlock bb, GuardValue v);
predicate exprHasValue(Expr e, GuardValue gv);
bindingset[gv1, gv2]
predicate disjointValues(GuardValue gv1, GuardValue gv2);
}
module Make<
LocationSig Location, BB::CfgSig<Location> Cfg,
InputSig<Location, Cfg::ControlFlowNode, Cfg::BasicBlock> Input>
{
private module Cfg_ = Cfg;
private import Cfg_
private import Input
final private class FinalAstNode = Input::AstNode;
class AstNode extends FinalAstNode {
AstNode getParent() { result = getParent(this) }
}
/**
* Holds if `node` is enclosed by `finally`. In case of nested finally
* blocks, this predicate only holds for the innermost block enclosing
* `node`.
*/
private predicate hasEnclosingFinally(AstNode node, FinallyBlock finally) {
node = finally
or
not node instanceof FinallyBlock and
hasEnclosingFinally(node.getParent(), finally)
}
/**
* Holds if `inner` is nested within `outer`.
*/
private predicate nestedFinally(FinallyBlock inner, FinallyBlock outer) {
hasEnclosingFinally(inner.(AstNode).getParent(), outer)
}
/** Gets the nesting depth of `finally` in terms of number of finally blocks. */
private int finallyNestLevel(FinallyBlock finally) {
not nestedFinally(finally, _) and result = 1
or
exists(FinallyBlock outer |
nestedFinally(finally, outer) and result = 1 + finallyNestLevel(outer)
)
}
private int maxFinallyNesting() { result = max(finallyNestLevel(_)) }
private newtype TFinallyStack =
TNil() or
TCons(Boolean abrupt, FinallyStack tail) { tail.length() < maxFinallyNesting() }
/**
* A stack of split values to track whether entered finally blocks have
* waiting completions.
*/
private class FinallyStack extends TFinallyStack {
string toString() {
result = "" and this = TNil()
or
exists(boolean abrupt, FinallyStack tail |
result = abrupt + ";" + tail.toString() and this = TCons(abrupt, tail)
)
}
/** Gets the length of this stack. */
int length() {
result = 0 and this = TNil()
or
exists(FinallyStack tail | result = 1 + tail.length() and this = TCons(_, tail))
}
/**
* Gets the stack resulting from pushing information about entering a
* finally block through a specific edge onto this stack.
*
* The `abrupt` value indicates whether the edge has an `AbruptSuccessor`
* or not.
*/
FinallyStack enter(boolean abrupt) { result = TCons(abrupt, this) }
/**
* Gets the stack resulting from popping a value, if any, consistent with
* leaving a finally block through a specific edge.
*
* The `abrupt` value indicates whether the edge has an `AbruptSuccessor`
* or not.
*/
FinallyStack leave(Boolean abrupt) {
this = TNil() and result = TNil() and exists(abrupt)
or
abrupt = false and this = TCons(false, result)
or
abrupt = true and this = TCons(_, result)
}
}
private ControlFlowNode basicBlockEndPoint() {
result = any(BasicBlock bb).getNode(0) or
result = any(BasicBlock bb).getLastNode()
}
private predicate inFinally(AstNode node, FinallyBlock finally) {
node = getEnclosingAstNode(basicBlockEndPoint()) and
hasEnclosingFinally(node, finally)
or
exists(FinallyBlock inner | nestedFinally(inner, finally) and inFinally(node, inner))
}
private predicate irrelevantFinally(FinallyBlock finally) {
exists(BasicBlock bb, AstNode n1, AstNode n2 |
n1 = getEnclosingAstNode(bb.getNode(0)) and
n2 = getEnclosingAstNode(bb.getLastNode())
|
inFinally(n1, finally) and not inFinally(n2, finally)
or
not inFinally(n1, finally) and inFinally(n2, finally)
)
}
private predicate entersFinally(
BasicBlock bb1, BasicBlock bb2, boolean abrupt, FinallyBlock finally
) {
exists(AstNode n1, AstNode n2, SuccessorType t |
not irrelevantFinally(finally) and
bb1.getASuccessor(t) = bb2 and
n1 = getEnclosingAstNode(bb1.getLastNode()) and
n2 = getEnclosingAstNode(bb2.getNode(0)) and
not inFinally(n1, finally) and
inFinally(n2, finally) and
if t instanceof AbruptSuccessor then abrupt = true else abrupt = false
)
}
private predicate leavesFinally(
BasicBlock bb1, BasicBlock bb2, boolean abrupt, FinallyBlock finally
) {
exists(AstNode n1, AstNode n2, SuccessorType t |
not irrelevantFinally(finally) and
bb1.getASuccessor(t) = bb2 and
n1 = getEnclosingAstNode(bb1.getLastNode()) and
n2 = getEnclosingAstNode(bb2.getNode(0)) and
inFinally(n1, finally) and
not inFinally(n2, finally) and
if t instanceof AbruptSuccessor then abrupt = true else abrupt = false
)
}
/** Holds if `gv1` is a strict subset of `gv2`. */
bindingset[gv1, gv2]
private predicate smaller(GuardValue gv1, GuardValue gv2) {
disjointValues(gv1, gv2.getDualValue()) and
gv1 != gv2
}
/**
* Holds if the value of `def` is `gv`.
*
* If multiple values apply, then we only include the most precise ones.
*/
private predicate ssaHasValue(SsaWriteDefinition def, GuardValue gv) {
exists(Expr e |
def.getDefinition() = e and
exprHasValue(e, gv) and
not exists(GuardValue gv0 | exprHasValue(e, gv0) and smaller(gv0, gv))
)
}
pragma[nomagic]
private predicate ssaLiveAtEndOfBlock(SourceVariable var, SsaDefinition def, BasicBlock bb) {
def.getSourceVariable() = var and
def.isLiveAtEndOfBlock(bb)
}
pragma[nomagic]
private predicate initSsaValue0(SourceVariable var, BasicBlock bb, SsaDefinition t, GuardValue val) {
ssaLiveAtEndOfBlock(var, t, bb) and
(
ssaControls(t, bb, val)
or
ssaHasValue(t, val)
)
}
/**
* Holds if the value of `t` in `bb` is `val` and that `t` is live at the
* end of `bb`.
*
* If multiple values apply, then we only include the most precise ones.
*
* The underlying variable of `t` is `var`.
*/
private predicate initSsaValue(SourceVariable var, BasicBlock bb, SsaDefinition t, GuardValue val) {
initSsaValue0(var, bb, t, val) and
not exists(GuardValue val0 | initSsaValue0(var, bb, t, val0) and smaller(val0, val))
}
private predicate possibleValue(SourceVariable var, GuardValue gv) {
exists(SsaDefinition def | def.getSourceVariable() = var |
ssaHasValue(def, gv)
or
ssaControlsBranchEdge(def, _, _, gv)
)
}
private predicate possibleRangeBound(SourceVariable var, int bound, boolean upper) {
exists(GuardValue gv | possibleValue(var, gv) and gv.isIntRange(bound, upper))
}
private predicate possibleClosedRange(SourceVariable var, int low, int high) {
possibleRangeBound(var, low, false) and
possibleRangeBound(var, high, true) and
low < high
}
private newtype TGuardValueExt =
AnyValue() or
BaseValue(GuardValue gv) { possibleValue(_, gv) } or
IntRange(int low, int high) { possibleClosedRange(_, low, high) }
private class GuardValueExt extends TGuardValueExt {
string toString() {
result = "Any" and this = AnyValue()
or
result = this.asBase().toString()
or
exists(int low, int high |
this = IntRange(low, high) and result = "[" + low + ", " + high + "]"
)
}
GuardValue asBase() { this = BaseValue(result) }
}
private class TGuardValueOrAny = AnyValue or BaseValue;
private class GuardValueOrAny extends GuardValueExt, TGuardValueOrAny { }
private GuardValueExt mkRange(int low, int high) {
result = IntRange(low, high)
or
low = high and
result.asBase().asIntValue() = low
}
private GuardValueExt intersectBase1(GuardValue gv1, GuardValue gv2) {
exists(SourceVariable var |
possibleValue(var, gv1) and
possibleValue(var, gv2)
|
smaller(gv1, gv2) and result.asBase() = gv1
or
exists(int low, int high |
gv1.isIntRange(low, false) and
gv2.isIntRange(high, true) and
result = mkRange(low, high)
)
or
exists(int bound, boolean upper, int d |
gv1.isIntRange(bound, upper) and
gv2.getDualValue().asIntValue() = bound and
result.asBase().isIntRange(bound + d, upper)
|
upper = true and d = -1
or
upper = false and d = 1
)
)
}
private GuardValueExt intersectBase2(GuardValueExt v1, GuardValue v2) {
result = intersectBase1(v1.asBase(), v2)
or
result = intersectBase1(v2, v1.asBase())
}
bindingset[v1, v2]
pragma[inline_late]
private GuardValueExt intersectRange(GuardValueExt v1, GuardValue v2) {
exists(int low, int high | v1 = IntRange(low, high) |
exists(int bound, boolean upper | v2.isIntRange(bound, upper) |
upper = true and result = mkRange(low, high.minimum(bound))
or
upper = false and result = mkRange(low.maximum(bound), high)
)
or
exists(int k |
v2.asIntValue() = k and
result.asBase() = v2 and
low <= k and
k <= high
)
or
not v2.isIntRange(_, _) and not exists(v2.asIntValue()) and result = v1
)
}
bindingset[v1, v2]
pragma[inline_late]
private GuardValueExt intersect(GuardValueExt v1, GuardValue v2) {
v1 = AnyValue() and result.asBase() = v2
or
result = intersectBase2(v1, v2)
or
result = v1 and
v1 instanceof BaseValue and
not exists(intersectBase2(v1, v2))
or
result = intersectRange(v1, v2)
}
bindingset[v1, gv2]
private predicate disjointValuesExt(GuardValueExt v1, GuardValue gv2) {
disjointValues(v1.asBase(), gv2)
or
exists(int low, int high | v1 = IntRange(low, high) |
gv2.asIntValue() < low
or
high < gv2.asIntValue()
or
exists(int bound, boolean upper | gv2.isIntRange(bound, upper) |
upper = true and bound < low
or
upper = false and high < bound
)
)
}
/** An input configuration for control flow reachability. */
signature module ConfigSig {
/**
* Holds if the value of `def` at `node` is a source for the reachability
* computation.
*/
predicate source(ControlFlowNode node, SsaDefinition def);
/**
* Holds if the value of `def` at `node` is a sink for the reachability
* computation.
*/
predicate sink(ControlFlowNode node, SsaDefinition def);
/**
* Holds if the value of `gv` is a barrier for the reachability computation.
* That is, paths where the tracked variable can be inferred to have the
* value of `gv` are excluded from the reachability analysis.
*/
default predicate barrierValue(GuardValue gv) { none() }
/**
* Holds if the edge from `bb1` to `bb2` should be excluded from the
* reachability analysis.
*/
default predicate barrierEdge(BasicBlock bb1, BasicBlock bb2) { none() }
/**
* Holds if flow through uncertain SSA updates should be included.
*/
default predicate uncertainFlow() { any() }
}
/**
* Constructs a control flow reachability computation.
*/
module Flow<ConfigSig Config> {
private predicate ssaRelevantAtEndOfBlock(SsaDefinition def, BasicBlock bb) {
def.isLiveAtEndOfBlock(bb)
or
def.getBasicBlock().strictlyPostDominates(bb)
}
pragma[nomagic]
private predicate isSource(
ControlFlowNode src, SsaDefinition srcDef, SourceVariable var, BasicBlock bb, int i
) {
Config::source(src, srcDef) and
bb.getNode(i) = src and
srcDef.getSourceVariable() = var
}
pragma[nomagic]
private predicate isSink(
ControlFlowNode sink, SsaDefinition sinkDef, SourceVariable var, BasicBlock bb, int i
) {
Config::sink(sink, sinkDef) and
bb.getNode(i) = sink and
sinkDef.getSourceVariable() = var
}
private predicate uncertainStep(SsaDefinition def1, SsaDefinition def2) {
def2.(SsaUncertainDefinition).getPriorDefinition() = def1 and
Config::uncertainFlow()
}
private predicate intraBlockStep(SsaDefinition def1, SsaDefinition def2) {
exists(BasicBlock bb |
uncertainStep(def1, def2) and
bb = def2.getBasicBlock() and
isSource(_, _, _, bb, _) and
isSink(_, _, _, bb, _)
)
}
private predicate intraBlockFlowAll(
ControlFlowNode src, SsaDefinition srcDef, int i, ControlFlowNode sink, SsaDefinition sinkDef,
int j
) {
exists(SourceVariable var, BasicBlock bb |
isSource(src, srcDef, var, bb, i) and
isSink(sink, sinkDef, var, bb, j) and
i <= j and
intraBlockStep*(srcDef, sinkDef)
)
}
private predicate intraBlockFlow(
ControlFlowNode src, SsaDefinition srcDef, ControlFlowNode sink, SsaDefinition sinkDef
) {
exists(int i, int j |
intraBlockFlowAll(src, srcDef, i, sink, sinkDef, j) and
not exists(int k |
intraBlockFlowAll(src, srcDef, i, _, _, k) and
k < j
)
)
}
private predicate sourceBlock(SsaDefinition def, BasicBlock bb, ControlFlowNode src) {
isSource(src, def, _, bb, _) and
not intraBlockFlow(src, def, _, _)
}
private predicate sinkBlock(SsaDefinition def, BasicBlock bb, ControlFlowNode sink) {
sink =
min(ControlFlowNode n, int i | bb.getNode(i) = n and Config::sink(n, def) | n order by i)
}
/**
* Holds if the edge from `bb1` to `bb2` implies that `def` has a value
* that is considered a barrier.
*/
private predicate ssaValueBarrierEdge(SsaDefinition def, BasicBlock bb1, BasicBlock bb2) {
exists(GuardValue v |
ssaControlsBranchEdge(def, bb1, bb2, v) and
Config::barrierValue(v)
)
}
/** Holds if `def1` in `bb1` may step to `def2` in `bb2`. */
private predicate step(SsaDefinition def1, BasicBlock bb1, SsaDefinition def2, BasicBlock bb2) {
not sinkBlock(def1, bb1, _) and
not Config::barrierEdge(bb1, bb2) and
not ssaValueBarrierEdge(def1, bb1, bb2) and
(
def2.(SsaPhiNode).hasInputFromBlock(def1, bb1) and bb2 = def2.getBasicBlock()
or
exists(SourceVariable v |
ssaRelevantAtEndOfBlock(def1, bb1) and
bb1.getASuccessor() = bb2 and
v = def1.getSourceVariable() and
not exists(SsaPhiNode phi | phi.getBasicBlock() = bb2 and phi.getSourceVariable() = v) and
def1 = def2
)
or
uncertainStep(def1, def2) and
bb2 = def2.getBasicBlock() and
bb1 = bb2
)
}
bindingset[bb1, bb2, fs1]
pragma[inline_late]
private predicate stepFinallyStack(
BasicBlock bb1, BasicBlock bb2, FinallyStack fs1, FinallyStack fs2
) {
exists(boolean abrupt | entersFinally(bb1, bb2, abrupt, _) and fs2 = fs1.enter(abrupt)) and
not leavesFinally(bb1, bb2, _, _)
or
exists(boolean abrupt | leavesFinally(bb1, bb2, abrupt, _) and fs2 = fs1.leave(abrupt)) and
not entersFinally(bb1, bb2, _, _)
or
exists(boolean abrupt |
leavesFinally(bb1, bb2, abrupt, _) and
entersFinally(bb1, bb2, abrupt, _) and
fs2 = fs1.leave(abrupt).enter(abrupt)
)
or
not entersFinally(bb1, bb2, _, _) and not leavesFinally(bb1, bb2, _, _) and fs2 = fs1
}
/**
* Holds if the source `srcDef` in `srcBb` may reach `def` in `bb`. If the
* path has entered one or more finally blocks then `fs` tracks the
* `SuccessorType`s of the edges entering those blocks.
*/
private predicate sourceReachesBlock(
SsaDefinition srcDef, BasicBlock srcBb, SsaDefinition def, BasicBlock bb, FinallyStack fs
) {
sourceBlock(srcDef, srcBb, _) and
def = srcDef and
bb = srcBb and
fs = TNil()
or
exists(SsaDefinition middef, BasicBlock midbb, FinallyStack midfs |
sourceReachesBlock(srcDef, srcBb, middef, midbb, midfs) and
step(middef, midbb, def, bb) and
stepFinallyStack(midbb, bb, midfs, fs)
)
}
/**
* Holds if `def` in `bb` is reachable from a source and may reach a sink.
*/
private predicate blockReachesSink(SsaDefinition def, BasicBlock bb) {
sourceReachesBlock(_, _, def, bb, _) and
(
sinkBlock(def, bb, _)
or
exists(SsaDefinition middef, BasicBlock midbb |
step(def, bb, middef, midbb) and
blockReachesSink(middef, midbb)
)
)
}
private predicate escapeCandidate(SsaDefinition def, BasicBlock bb) {
sourceBlock(def, bb, _)
or
exists(SsaDefinition middef, BasicBlock midbb |
blockReachesSink(middef, midbb) and
step(middef, midbb, def, bb)
)
}
/**
* Holds if the source `srcDef` in `srcBb` may reach `escDef` in `escBb` and from
* there cannot reach a sink.
*/
private predicate sourceEscapesSink(
SsaDefinition srcDef, BasicBlock srcBb, SsaDefinition escDef, BasicBlock escBb
) {
sourceReachesBlock(srcDef, srcBb, escDef, escBb, _) and
escapeCandidate(escDef, escBb) and
not blockReachesSink(escDef, escBb)
}
/** Holds if `bb` is a relevant block for computing reachability of `src`. */
private predicate pathBlock(SourceVariable src, BasicBlock bb) {
exists(SsaDefinition def | def.getSourceVariable() = src |
blockReachesSink(def, bb)
or
escapeCandidate(def, bb)
)
}
/**
* Holds if `bb1` to `bb2` is a relevant edge for computing reachability
* of `src`.
*/
private predicate pathEdge(SourceVariable src, BasicBlock bb1, BasicBlock bb2) {
step(_, bb1, _, bb2) and
pathBlock(pragma[only_bind_into](src), bb1) and
pathBlock(pragma[only_bind_into](src), bb2) and
bb1 != bb2
}
/**
* Holds if the edge from `bb1` to `bb2` implies that `def` has the value
* `gv` and that the edge is relevant for computing reachability of `src`.
*
* If multiple values may be implied by this edge, then we only include the
* most precise ones.
*
* The underlying variable of `t` is `var`.
*/
private predicate ssaControlsPathEdge(
SourceVariable src, SsaDefinition t, SourceVariable var, GuardValue gv, BasicBlock bb1,
BasicBlock bb2
) {
ssaControlsBranchEdge(t, bb1, bb2, gv) and
not exists(GuardValue gv0 | ssaControlsBranchEdge(t, bb1, bb2, gv0) and smaller(gv0, gv)) and
pathEdge(src, bb1, bb2) and
t.getSourceVariable() = var
}
/**
* Holds if the reachability path for `src` may go through a loop with
* entry point `entry`.
*/
pragma[nomagic]
private predicate loopEntryBlock(SourceVariable src, BasicBlock entry) {
exists(BasicBlock pred | pathEdge(src, pred, entry) and entry.strictlyDominates(pred))
}
/**
* Holds if precision may be improved by splitting control flow on the
* value of `var` during the reachability computation of `src`.
*/
private predicate relevantSplit(SourceVariable src, SourceVariable var) {
// `var` may be a relevant split if we encounter 2+ conditional edges
// that imply information about `var`.
2 <= strictcount(BasicBlock bb1 | ssaControlsPathEdge(src, _, var, _, bb1, _))
or
// Or if we encounter a conditional edge that imply a value that's
// incompatible with an initial or later assigned value.
exists(GuardValue gv1, GuardValue gv2, BasicBlock bb |
ssaControlsPathEdge(src, _, var, gv1, _, _) and
initSsaValue(var, bb, _, gv2) and
disjointValues(gv1, gv2) and
pathBlock(src, bb)
)
or
// Or if we encounter a conditional edge in a loop that imply a value for
// `var` that may be unchanged from one iteration to the next.
exists(SsaDefinition def, BasicBlock bb1, BasicBlock bb2, BasicBlock loopEntry |
ssaControlsPathEdge(src, def, var, _, bb1, bb2) and
loopEntryBlock(src, loopEntry) and
loopEntry.strictlyDominates(bb1) and
bb2.getASuccessor*() = loopEntry
|
def.getBasicBlock().dominates(loopEntry)
or
exists(SsaPhiNode phi |
phi.definesAt(var, loopEntry, _) and
phi.getAPhiInput+() = def and
def.(SsaPhiNode).getAPhiInput*() = phi
)
)
}
private module SsaDefOption = Option<SsaDefinition>;
private class SsaDefOption = SsaDefOption::Option;
private predicate lastDefInBlock(SourceVariable var, SsaDefinition def, BasicBlock bb) {
def = max(SsaDefinition d, int i | d.definesAt(var, bb, i) | d order by i)
}
/**
* Holds if `bb1` to `bb2` is a relevant edge for computing reachability of
* `src`, and `var` is a relevant splitting variable that gets (re-)defined
* in `bb2` by `t`, which is not a phi node.
*
* `val` is the best known value for `t` in `bb2`.
*/
private predicate stepSsaValueRedef(
SourceVariable src, BasicBlock bb1, BasicBlock bb2, SourceVariable var, SsaDefinition t,
GuardValueOrAny val
) {
pathEdge(src, bb1, bb2) and
relevantSplit(src, var) and
lastDefInBlock(var, t, bb2) and
not t instanceof SsaPhiNode and
(
ssaHasValue(t, val.asBase())
or
not ssaHasValue(t, _) and val = AnyValue()
)
}
/**
* Holds if `bb1` to `bb2` is a relevant edge for computing reachability of
* `src`, and `var` is a relevant splitting variable that has a phi node,
* `t2`, in `bb2` taking input from `t1` along this edge. Furthermore,
* there is no further redefinition of `var` in `bb2`.
*
* `val` is the best value for `t1`/`t2` implied by taking this edge.
*/
private predicate stepSsaValuePhi(
SourceVariable src, BasicBlock bb1, BasicBlock bb2, SourceVariable var, SsaDefinition t1,
SsaDefinition t2, GuardValueOrAny val
) {
pathEdge(src, bb1, bb2) and
relevantSplit(src, var) and
lastDefInBlock(var, t2, bb2) and
t2.(SsaPhiNode).hasInputFromBlock(t1, bb1) and
(
ssaControlsPathEdge(src, t1, _, val.asBase(), bb1, bb2)
or
not ssaControlsPathEdge(src, t1, _, _, bb1, bb2) and
val = AnyValue()
)
}
/**
* Holds if `bb1` to `bb2` is a relevant edge for computing reachability of
* `src`, and `var` is a relevant splitting variable that has no
* redefinition along this edge nor in `bb2`.
*
* Additionally, this edge implies that the SSA definition `t` of `var` has
* value `val`.
*/
private predicate stepSsaValueNoRedef(
SourceVariable src, BasicBlock bb1, BasicBlock bb2, SourceVariable var, SsaDefinition t,
GuardValue val
) {
pathEdge(src, bb1, bb2) and
relevantSplit(src, var) and
not lastDefInBlock(var, _, bb2) and
ssaControlsPathEdge(src, t, var, val, bb1, bb2)
}
/**
* Holds if the source `srcDef` in `srcBb` may reach `def` in `bb`. The
* taken path takes splitting based on the value of `var` into account.
* The pair `(tracked, val)` is the current SSA definition and known value
* for `var` in `bb`.
*/
private predicate sourceReachesBlockWithTrackedVar(
SsaDefinition srcDef, BasicBlock srcBb, SsaDefinition def, BasicBlock bb, FinallyStack fs,
SsaDefOption tracked, GuardValueExt val, SourceVariable var
) {
sourceBlock(srcDef, srcBb, _) and
def = srcDef and
bb = srcBb and
fs = TNil() and
relevantSplit(def.getSourceVariable(), var) and
(
// tracking variable is not yet live
not ssaLiveAtEndOfBlock(var, _, bb) and
tracked.isNone() and
val = AnyValue()
or
// tracking variable is live but without known value
ssaLiveAtEndOfBlock(var, tracked.asSome(), bb) and
not initSsaValue(var, bb, _, _) and
val = AnyValue()
or
// tracking variable has known value
initSsaValue(var, bb, tracked.asSome(), val.asBase())
)
or
exists(
SourceVariable src, SsaDefinition middef, BasicBlock midbb, FinallyStack midfs,
SsaDefOption tracked0, GuardValueExt val0
|
sourceReachesBlockWithTrackedVar(srcDef, srcBb, middef, midbb, midfs, tracked0, val0, var) and
src = srcDef.getSourceVariable() and
step(middef, midbb, def, bb) and
stepFinallyStack(midbb, bb, midfs, fs) and
pathBlock(src, bb) and
not exists(GuardValue gv |
ssaControlsPathEdge(src, tracked0.asSome(), _, gv, midbb, bb) and
disjointValuesExt(val0, gv)
)
|
// tracking variable is redefined
stepSsaValueRedef(src, midbb, bb, var, tracked.asSome(), val)
or
exists(GuardValueOrAny val1 |
// tracking variable has a phi node, and maybe value information from the edge
stepSsaValuePhi(src, midbb, bb, var, tracked0.asSome(), tracked.asSome(), val1)
|
val = val0 and val1 = AnyValue()
or
val = intersect(val0, val1.asBase())
)
or
exists(GuardValue val1 |
// tracking variable is unchanged, and has value information from the edge
stepSsaValueNoRedef(src, midbb, bb, var, tracked0.asSome(), val1) and
tracked = tracked0 and
val = intersect(val0, val1)
)
or
// tracking variable is unchanged, and has no value information from the edge
not lastDefInBlock(var, _, bb) and
not stepSsaValueNoRedef(src, midbb, bb, var, tracked0.asSome(), _) and
tracked = tracked0 and
val = val0
)
}
/**
* Holds if the source `srcDef` at `src` may reach the sink `sinkDef` at `sink`.
*/
predicate flow(
ControlFlowNode src, SsaDefinition srcDef, ControlFlowNode sink, SsaDefinition sinkDef
) {
intraBlockFlow(src, srcDef, sink, sinkDef)
or
exists(BasicBlock srcBb, BasicBlock sinkBb, SourceVariable srcVar |
sourceBlock(srcDef, srcBb, src) and
sourceReachesBlock(srcDef, srcBb, sinkDef, sinkBb, _) and
sinkBlock(sinkDef, sinkBb, sink) and
srcVar = srcDef.getSourceVariable() and
forall(SourceVariable t | relevantSplit(srcVar, t) |
sourceReachesBlockWithTrackedVar(srcDef, srcBb, sinkDef, sinkBb, _, _, _, t)
)
)
}
/**
* Holds if the source `srcDef` at `src` may escape, that is, there exists
* a path from `src` that circumvents all sinks to a point from which no
* sink is reachable.
*/
predicate escapeFlow(ControlFlowNode src, SsaDefinition srcDef) {
not intraBlockFlow(src, srcDef, _, _) and
exists(BasicBlock srcBb, SsaDefinition escDef, BasicBlock escBb, SourceVariable srcVar |
sourceBlock(srcDef, srcBb, src) and
sourceEscapesSink(srcDef, srcBb, escDef, escBb) and
srcVar = srcDef.getSourceVariable() and
forall(SourceVariable t | relevantSplit(srcVar, t) |
sourceReachesBlockWithTrackedVar(srcDef, srcBb, escDef, escBb, _, _, _, t)
)
)
}
}
}

85
shared/controlflow/codeql/controlflow/Guards.qll
View File

@@ -208,6 +208,12 @@ 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
// exclude edge cases to avoid overflow issues when computing duals
bound != 2147483647 and
bound != -2147483648
} or
TException(Boolean throws)
private class AbstractSingleValue extends TAbstractSingleValue {
@@ -238,6 +244,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())
@@ -262,6 +277,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) }
@@ -275,6 +298,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
@@ -293,6 +322,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) {
@@ -681,18 +728,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
@@ -705,14 +740,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 |
@@ -744,6 +774,10 @@ module Make<
or
exprHasValue(e.(IdExpr).getEqualChildExpr(), v)
or
exists(ConditionalExpr cond | cond = e |
exprHasValue(cond.getThen(), v) and exprHasValue(cond.getElse(), v)
)
or
exists(SsaDefinition def, Guard g, GuardValue gv |
e = def.getARead() and
g.directlyValueControls(e.getBasicBlock(), gv) and
@@ -1213,5 +1247,16 @@ module Make<
this.valueControls(bb, any(GuardValue gv | gv.asBooleanValue() = branch))
}
}
private predicate exprHasValueAlias = exprHasValue/2;
private predicate disjointValuesAlias = disjointValues/2;
/** Provides utility predicates for working with `GuardValue`s. */
module InternalUtil {
predicate exprHasValue = exprHasValueAlias/2;
predicate disjointValues = disjointValuesAlias/2;
}
}
}