diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/Nullness.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/Nullness.qll index 8d19f9720d8..1b527623db5 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/Nullness.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/Nullness.qll @@ -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; -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()) } } diff --git a/csharp/ql/src/CSI/NullMaybe.ql b/csharp/ql/src/CSI/NullMaybe.ql index 67873ebb291..f78a8d89bcf 100644 --- a/csharp/ql/src/CSI/NullMaybe.ql +++ b/csharp/ql/src/CSI/NullMaybe.ql @@ -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"