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

C#: Replace NullMaybe.ql implementation.

Browse Source
This commit is contained in:
Anders Schack-Mulligen
2025-09-26 13:38:25 +02:00
parent 6cfadbfe90
commit 587901bc8a
2 changed files with 14 additions and 306 deletions
Download Patch File Download Diff File Expand all files Collapse all files

309
csharp/ql/lib/semmle/code/csharp/dataflow/Nullness.qll
View File

@@ -20,7 +20,6 @@
import csharp
private import ControlFlow
private import internal.CallableReturns
private import semmle.code.csharp.commons.Assertions
private import semmle.code.csharp.controlflow.Guards as G
private import semmle.code.csharp.controlflow.Guards::AbstractValues
private import semmle.code.csharp.dataflow.internal.SsaImpl as SsaImpl
@@ -119,49 +118,12 @@ private predicate nonNullDef(Ssa::ExplicitDefinition def) {
}
/**
* Holds if the `i`th node of basic block `bb` is a dereference `d` of SSA
* definition `def`.
* Holds if the `node` is a dereference `d` of SSA definition `def`.
*/
private predicate dereferenceAt(BasicBlock bb, int i, Ssa::Definition def, Dereference d) {
d = def.getAReadAtNode(bb.getNode(i))
}
private predicate dereferenceAt(ControlFlow::Node node, Ssa::Definition def, Dereference d) {
d = def.getAReadAtNode(node)
}
/**
* Holds if `e` having abstract value `vExpr` implies that SSA definition `def`
* has abstract value `vDef`.
*/
private predicate exprImpliesSsaDef(
G::Guard e, G::AbstractValue vExpr, Ssa::Definition def, G::AbstractValue vDef
) {
vExpr = e.getAValue() and
vExpr = vDef and
(
e = def.getARead()
or
e = def.(Ssa::ExplicitDefinition).getADefinition().getTargetAccess()
)
or
exists(Expr e0, G::AbstractValue vExpr0 |
exprImpliesSsaDef(e0, vExpr0, def, vDef) and
G::Internal::impliesStep(e, vExpr, e0, vExpr0)
)
}
/**
* Gets an element that tests whether a given SSA definition, `def`, is
* `null` or not.
*
* If the returned element takes the `s` branch, then `def` is guaranteed to be
* `null` if `nv.isNull()` holds, and non-`null` otherwise.
*/
private ControlFlowElement getANullCheck(Ssa::Definition def, ConditionalSuccessor s, NullValue nv) {
exists(Expr e, G::AbstractValue v | v.branch(result, s, e) | exprImpliesSsaDef(e, v, def, nv))
}
private predicate isMaybeNullArgument(Ssa::ImplicitParameterDefinition def, MaybeNullExpr arg) {
exists(AssignableDefinitions::ImplicitParameterDefinition pdef, Parameter p |
p = def.getParameter()
@@ -263,7 +225,7 @@ private predicate defMaybeNull(
)
or
// A variable of nullable type may be null
exists(Dereference d | dereferenceAt(_, _, def, d) |
exists(Dereference d | dereferenceAt(_, def, d) |
node = def.getControlFlowNode() and
d.hasNullableType() and
not def instanceof Ssa::PhiNode and
@@ -273,219 +235,6 @@ private predicate defMaybeNull(
)
}
pragma[noinline]
private predicate sourceVariableMaybeNull(Ssa::SourceVariable v) {
defMaybeNull(v.getAnSsaDefinition(), _, _, _)
}
pragma[noinline]
private predicate defNullImpliesStep0(
Ssa::SourceVariable v, Ssa::Definition def1, BasicBlock bb1, BasicBlock bb2
) {
sourceVariableMaybeNull(v) and
def1.getSourceVariable() = v and
def1.isLiveAtEndOfBlock(bb1) and
bb2 = bb1.getASuccessor()
}
/**
* Holds if `def1` being `null` in basic block `bb1` implies that `def2` might
* be `null` in basic block `bb2`. The SSA definitions share the same source
* variable.
*/
private predicate defNullImpliesStep(
Ssa::Definition def1, BasicBlock bb1, Ssa::Definition def2, BasicBlock bb2
) {
exists(Ssa::SourceVariable v | defNullImpliesStep0(v, def1, bb1, bb2) |
def2.(Ssa::PhiNode).getAnInput() = def1 and
bb2 = def2.getBasicBlock()
or
def2 = def1 and
not exists(Ssa::PhiNode phi |
phi.getSourceVariable() = v and
bb2 = phi.getBasicBlock()
)
) and
not exists(ConditionalSuccessor s, NullValue nv |
bb1.getLastNode() = getANullCheck(def1, s, nv).getAControlFlowNode()
|
bb2 = bb1.getASuccessor(s) and
nv.isNonNull()
)
}
/**
* The transitive closure of `defNullImpliesStep()` originating from `defMaybeNull()`.
* That is, those basic blocks for which the SSA definition is suspected of being `null`.
*/
private predicate defMaybeNullInBlock(Ssa::Definition def, BasicBlock bb) {
defMaybeNull(def, _, _, _) and
bb = def.getBasicBlock()
or
exists(BasicBlock mid, Ssa::Definition midDef | defMaybeNullInBlock(midDef, mid) |
defNullImpliesStep(midDef, mid, def, bb)
)
}
/**
* Holds if `v` is a source variable that might reach a potential `null`
* dereference.
*/
private predicate nullDerefCandidateVariable(Ssa::SourceVariable v) {
exists(Ssa::Definition def, BasicBlock bb | dereferenceAt(bb, _, def, _) |
defMaybeNullInBlock(def, bb) and
v = def.getSourceVariable()
)
}
private predicate succStep(PathNode pred, Ssa::Definition def, BasicBlock bb) {
defNullImpliesStep(pred.getSsaDefinition(), pred.getBasicBlock(), def, bb)
}
private predicate succNullArgument(SourcePathNode pred, Ssa::Definition def, BasicBlock bb) {
pred = TSourcePathNode(def, _, _, true) and
bb = def.getBasicBlock()
}
private predicate succSourceSink(SourcePathNode source, Ssa::Definition def, BasicBlock bb) {
source = TSourcePathNode(def, _, _, false) and
bb = def.getBasicBlock()
}
private newtype TPathNode =
TSourcePathNode(Ssa::Definition def, string msg, Element reason, boolean isNullArgument) {
nullDerefCandidateVariable(def.getSourceVariable()) and
defMaybeNull(def, _, msg, reason) and
if isMaybeNullArgument(def, reason) then isNullArgument = true else isNullArgument = false
} or
TInternalPathNode(Ssa::Definition def, BasicBlock bb) {
succStep(_, def, bb)
or
succNullArgument(_, def, bb)
} or
TSinkPathNode(Ssa::Definition def, BasicBlock bb, int i, Dereference d) {
dereferenceAt(bb, i, def, d) and
(
succStep(_, def, bb)
or
succNullArgument(_, def, bb)
or
succSourceSink(_, def, bb)
)
}
/**
* An SSA definition, which may be `null`, augmented with at basic block which can
* be reached without passing through a `null` check.
*/
abstract class PathNode extends TPathNode {
/** Gets the SSA definition. */
abstract Ssa::Definition getSsaDefinition();
/** Gets the basic block that can be reached without passing through a `null` check. */
abstract BasicBlock getBasicBlock();
/** Gets another node that can be reached from this node. */
abstract PathNode getASuccessor();
/** Gets a textual representation of this node. */
abstract string toString();
/** Gets the location of this node. */
abstract Location getLocation();
}
private class SourcePathNode extends PathNode, TSourcePathNode {
private Ssa::Definition def;
private string msg;
private Element reason;
private boolean isNullArgument;
SourcePathNode() { this = TSourcePathNode(def, msg, reason, isNullArgument) }
override Ssa::Definition getSsaDefinition() { result = def }
override BasicBlock getBasicBlock() {
isNullArgument = false and
result = def.getBasicBlock()
}
string getMessage() { result = msg }
Element getReason() { result = reason }
override PathNode getASuccessor() {
succStep(this, result.getSsaDefinition(), result.getBasicBlock())
or
succNullArgument(this, result.getSsaDefinition(), result.getBasicBlock())
or
result instanceof SinkPathNode and
succSourceSink(this, result.getSsaDefinition(), result.getBasicBlock())
}
override string toString() {
if isNullArgument = true then result = reason.toString() else result = def.toString()
}
override Location getLocation() {
if isNullArgument = true then result = reason.getLocation() else result = def.getLocation()
}
}
private class InternalPathNode extends PathNode, TInternalPathNode {
private Ssa::Definition def;
private BasicBlock bb;
InternalPathNode() { this = TInternalPathNode(def, bb) }
override Ssa::Definition getSsaDefinition() { result = def }
override BasicBlock getBasicBlock() { result = bb }
override PathNode getASuccessor() {
succStep(this, result.getSsaDefinition(), result.getBasicBlock())
}
override string toString() { result = bb.getFirstNode().toString() }
override Location getLocation() { result = bb.getFirstNode().getLocation() }
}
private class SinkPathNode extends PathNode, TSinkPathNode {
private Ssa::Definition def;
private BasicBlock bb;
private int i;
private Dereference d;
SinkPathNode() { this = TSinkPathNode(def, bb, i, d) }
override Ssa::Definition getSsaDefinition() { result = def }
override BasicBlock getBasicBlock() { result = bb }
override PathNode getASuccessor() { none() }
Dereference getDereference() { result = d }
override string toString() { result = d.toString() }
override Location getLocation() { result = d.getLocation() }
}
/**
* Provides the query predicates needed to include a graph in a path-problem query
* for `Dereference::is[First]MaybeNull()`.
*/
module PathGraph {
query predicate nodes(PathNode n) { n.getASuccessor*() instanceof SinkPathNode }
query predicate edges(PathNode pred, PathNode succ) {
nodes(pred) and
nodes(succ) and
succ = pred.getASuccessor()
}
}
private Ssa::Definition getAPseudoInput(Ssa::Definition def) {
result = def.(Ssa::PhiNode).getAnInput()
}
@@ -499,21 +248,15 @@ private Ssa::Definition getAnUltimateDefinition(Ssa::Definition def) {
/**
* Holds if SSA definition `def` can reach a read at `cfn`, without passing
* through an intermediate dereference that always (`always = true`) or
* maybe (`always = false`) throws a null reference exception.
* through an intermediate dereference that always throws a null reference
* exception.
*/
private predicate defReaches(Ssa::Definition def, ControlFlow::Node cfn, boolean always) {
exists(def.getAFirstReadAtNode(cfn)) and
(always = true or always = false)
private predicate defReaches(Ssa::Definition def, ControlFlow::Node cfn) {
exists(def.getAFirstReadAtNode(cfn))
or
exists(ControlFlow::Node mid | defReaches(def, mid, always) |
exists(ControlFlow::Node mid | defReaches(def, mid) |
SsaImpl::adjacentReadPairSameVar(_, mid, cfn) and
not mid =
any(Dereference d |
if always = true
then d.isAlwaysNull(def.getSourceVariable())
else d.isMaybeNull(def, _, _, _, _)
).getAControlFlowNode()
not mid = any(Dereference d | d.isAlwaysNull(def.getSourceVariable())).getAControlFlowNode()
)
}
@@ -534,7 +277,7 @@ private module NullnessConfig implements Cf::ControlFlowReachability::ConfigSig
private module NullnessFlow = Cf::ControlFlowReachability::Flow<NullnessConfig>;
predicate debug_nullness_new(Dereference d, Ssa::SourceVariable v, string msg, Element reason) {
predicate maybeNullDeref(Dereference d, Ssa::SourceVariable v, string msg, Element reason) {
exists(
Ssa::Definition origin, Ssa::Definition ssa, ControlFlow::Node src, ControlFlow::Node sink
|
@@ -546,11 +289,6 @@ predicate debug_nullness_new(Dereference d, Ssa::SourceVariable v, string msg, E
)
}
predicate debug_nullness_orig(Dereference d, Ssa::SourceVariable v, string msg, Element reason) {
d.isFirstMaybeNull(v.getAnSsaDefinition(), _, _, msg, reason) and
not d instanceof NonNullExpr
}
/**
* An expression that dereferences a value. That is, an expression that may
* result in a `NullReferenceException` if the value is `null`.
@@ -645,33 +383,6 @@ class Dereference extends G::DereferenceableExpr {
*/
predicate isFirstAlwaysNull(Ssa::SourceVariable v) {
this.isAlwaysNull(v) and
defReaches(v.getAnSsaDefinition(), this.getAControlFlowNode(), true)
}
/**
* Holds if this expression dereferences SSA definition `def`, which may
* be `null`.
*/
predicate isMaybeNull(
Ssa::Definition def, SourcePathNode source, SinkPathNode sink, string msg, Element reason
) {
source.getASuccessor*() = sink and
msg = source.getMessage() and
reason = source.getReason() and
def = sink.getSsaDefinition() and
this = sink.getDereference() and
not this.isAlwaysNull(def.getSourceVariable())
}
/**
* Holds if this expression dereferences SSA definition `def`, which may
* be `null`, and this expression can be reached from `def` without passing
* through another such dereference.
*/
predicate isFirstMaybeNull(
Ssa::Definition def, SourcePathNode source, SinkPathNode sink, string msg, Element reason
) {
this.isMaybeNull(def, source, sink, msg, reason) and
defReaches(def, this.getAControlFlowNode(), false)
defReaches(v.getAnSsaDefinition(), this.getAControlFlowNode())
}
}

11
csharp/ql/src/CSI/NullMaybe.ql
View File

@@ -2,7 +2,7 @@
* @name Dereferenced variable may be null
* @description Dereferencing a variable whose value may be 'null' may cause a
* 'NullReferenceException'.
* @kind path-problem
* @kind problem
* @problem.severity warning
* @precision high
* @id cs/dereferenced-value-may-be-null
@@ -15,10 +15,7 @@
import csharp
import semmle.code.csharp.dataflow.Nullness
import PathGraph
from
Dereference d, PathNode source, PathNode sink, Ssa::SourceVariable v, string msg, Element reason
where d.isFirstMaybeNull(v.getAnSsaDefinition(), source, sink, msg, reason)
select d, source, sink, "Variable $@ may be null at this access " + msg + ".", v, v.toString(),
reason, "this"
from Dereference d, Ssa::SourceVariable v, string msg, Element reason
where maybeNullDeref(d, v, msg, reason)
select d, "Variable $@ may be null at this access " + msg + ".", v, v.toString(), reason, "this"