From 6c182564e75c1d8aa8a4b7811fd4910db313b661 Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Fri, 22 Mar 2019 14:45:51 +0100 Subject: [PATCH] C#: Adjustments to CIL/nullness analyses - Cache predicates in the same stage using a cached module. - Introduce `DefUse::defUseVariableUpdate()` and use in `CallableReturns.qll`. The updated file `csharp/ql/test/library-tests/cil/dataflow/Nullness.expected` demonstrates why this is needed. - Utilize CIL analysis in `Guards::nonNullValue()`. - Analyze SSA definitions in `AlwaysNullExpr`, similar to `NonNullExpr`. --- .../src/semmle/code/cil/CallableReturns.qll | 50 +++++++++++-------- csharp/ql/src/semmle/code/cil/DataFlow.qll | 31 ++++++------ .../semmle/code/csharp/controlflow/Guards.qll | 24 ++++++--- .../semmle/code/csharp/dataflow/DataFlow.qll | 2 +- .../semmle/code/csharp/dataflow/Nullness.qll | 19 +++++-- .../library-tests/cil/dataflow/DataFlow.ql | 3 +- .../cil/dataflow/Nullness.expected | 2 + .../controlflow/guards/ExtractorOptions.cs | 1 + .../Nullness/Implications.expected | 2 + 9 files changed, 84 insertions(+), 50 deletions(-) create mode 100644 csharp/ql/test/library-tests/controlflow/guards/ExtractorOptions.cs diff --git a/csharp/ql/src/semmle/code/cil/CallableReturns.qll b/csharp/ql/src/semmle/code/cil/CallableReturns.qll index 0bbc93a0c70..212f2706619 100644 --- a/csharp/ql/src/semmle/code/cil/CallableReturns.qll +++ b/csharp/ql/src/semmle/code/cil/CallableReturns.qll @@ -4,13 +4,31 @@ private import CIL -/** Holds if method `m` always returns null. */ cached -predicate alwaysNullMethod(Method m) { forex(Expr e | m.canReturn(e) | alwaysNullExpr(e)) } +private module Cached { + /** Holds if method `m` always returns null. */ + cached + predicate alwaysNullMethod(Method m) { forex(Expr e | m.canReturn(e) | alwaysNullExpr(e)) } -/** Holds if method `m` always returns non-null. */ -cached -predicate alwaysNotNullMethod(Method m) { forex(Expr e | m.canReturn(e) | alwaysNotNullExpr(e)) } + /** Holds if method `m` always returns non-null. */ + cached + predicate alwaysNotNullMethod(Method m) { forex(Expr e | m.canReturn(e) | alwaysNotNullExpr(e)) } + + /** Holds if method `m` always throws an exception. */ + cached + predicate alwaysThrowsMethod(Method m) { + m.hasBody() and + not exists(m.getImplementation().getAnInstruction().(Return)) + } + + /** Holds if method `m` always throws an exception of type `t`. */ + cached + predicate alwaysThrowsException(Method m, Type t) { + alwaysThrowsMethod(m) and + forex(Throw ex | ex = m.getImplementation().getAnInstruction() | t = ex.getExpr().getType()) + } +} +import Cached /** Holds if expression `expr` always evaluates to `null`. */ private predicate alwaysNullExpr(Expr expr) { @@ -18,7 +36,9 @@ private predicate alwaysNullExpr(Expr expr) { or alwaysNullMethod(expr.(StaticCall).getTarget()) or - forex(VariableUpdate vu | defUse(_, vu, expr) | alwaysNullExpr(vu.getSource())) + forex(VariableUpdate vu | DefUse::variableUpdateUse(_, vu, expr) | + alwaysNullExpr(vu.getSource()) + ) } /** Holds if expression `expr` always evaluates to non-null. */ @@ -29,19 +49,7 @@ private predicate alwaysNotNullExpr(Expr expr) { or alwaysNotNullMethod(expr.(StaticCall).getTarget()) or - forex(VariableUpdate vu | defUse(_, vu, expr) | alwaysNotNullExpr(vu.getSource())) -} - -/** Holds if method `m` always throws an exception. */ -cached -predicate alwaysThrowsMethod(Method m) { - m.hasBody() and - not exists(m.getImplementation().getAnInstruction().(Return)) -} - -/** Holds if method `m` always throws an exception of type `t`. */ -cached -predicate alwaysThrowsException(Method m, Type t) { - alwaysThrowsMethod(m) and - forex(Throw ex | ex = m.getImplementation().getAnInstruction() | t = ex.getExpr().getType()) + forex(VariableUpdate vu | DefUse::variableUpdateUse(_, vu, expr) | + alwaysNotNullExpr(vu.getSource()) + ) } diff --git a/csharp/ql/src/semmle/code/cil/DataFlow.qll b/csharp/ql/src/semmle/code/cil/DataFlow.qll index 96e1485b205..d5e7f6139e0 100644 --- a/csharp/ql/src/semmle/code/cil/DataFlow.qll +++ b/csharp/ql/src/semmle/code/cil/DataFlow.qll @@ -88,7 +88,7 @@ private predicate localTaintStep(DataFlowNode src, DataFlowNode sink) { } cached -private module DefUse { +module DefUse { /** * A classification of variable references into reads and writes. */ @@ -185,21 +185,26 @@ private module DefUse { ) } - /** Holds if the update `def` can be used at the read `use`. */ + /** Holds if the variable update `vu` can be used at the read `use`. */ cached - predicate defUseImpl(StackVariable target, DataFlowNode def, ReadAccess use) { - exists(VariableUpdate vu | def = vu.getSource() | - defReachesReadWithinBlock(target, vu, use) - or - exists(BasicBlock bb, int i | - exists(refRank(bb, i, target, Read())) and - use = bb.getNode(i) and - defReachesEndOfBlock(bb.getAPredecessor(), vu, target) and - not defReachesReadWithinBlock(target, _, use) - ) + predicate variableUpdateUse(StackVariable target, VariableUpdate vu, ReadAccess use) { + defReachesReadWithinBlock(target, vu, use) + or + exists(BasicBlock bb, int i | + exists(refRank(bb, i, target, Read())) and + use = bb.getNode(i) and + defReachesEndOfBlock(bb.getAPredecessor(), vu, target) and + not defReachesReadWithinBlock(target, _, use) ) } + + /** Holds if the update `def` can be used at the read `use`. */ + cached + predicate defUse(StackVariable target, Expr def, ReadAccess use) { + exists(VariableUpdate vu | def = vu.getSource() | variableUpdateUse(target, vu, use)) + } } +private import DefUse abstract library class VariableUpdate extends Instruction { abstract Expr getSource(); @@ -224,5 +229,3 @@ private class MethodOutOrRefTarget extends VariableUpdate, Call { override Expr getSource() { result = this } } - -predicate defUse = DefUse::defUseImpl/3; diff --git a/csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll b/csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll index 0fbd94b9819..765e45ed08f 100644 --- a/csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll +++ b/csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll @@ -3,6 +3,8 @@ */ import csharp +private import cil +private import dotnet private import ControlFlow::SuccessorTypes private import semmle.code.csharp.commons.Assertions private import semmle.code.csharp.commons.ComparisonTest @@ -11,6 +13,7 @@ private import semmle.code.csharp.controlflow.BasicBlocks private import semmle.code.csharp.controlflow.internal.Completion private import semmle.code.csharp.dataflow.Nullness private import semmle.code.csharp.frameworks.System +private import semmle.code.cil.CallableReturns /** An abstract value. */ abstract class AbstractValue extends TAbstractValue { @@ -637,6 +640,15 @@ module Internal { TMatchValue(CaseStmt cs, boolean b) { b = true or b = false } or TEmptyCollectionValue(boolean b) { b = true or b = false } + /** A callable that always returns a non-`null` value. */ + private class NonNullCallable extends DotNet::Callable { + NonNullCallable() { + exists(CIL::Method m | m.matchesHandle(this) | alwaysNotNullMethod(m) and not m.isVirtual()) + or + this = any(SystemObjectClass c).getGetTypeMethod() + } + } + /** Holds if expression `e` is a non-`null` value. */ predicate nonNullValue(Expr e) { e instanceof ObjectCreation @@ -652,12 +664,10 @@ module Internal { e instanceof AddExpr and e.getType() instanceof StringType or - e = any(MethodCall mc | - mc.getTarget() = any(SystemObjectClass c).getGetTypeMethod() and - not mc.isConditional() - ) - or e.(DefaultValueExpr).getType().isValueType() + or + e.(Call).getTarget().getSourceDeclaration() instanceof NonNullCallable and + not e.(QualifiableExpr).isConditional() } /** Holds if expression `e2` is a non-`null` value whenever `e1` is. */ @@ -1288,9 +1298,7 @@ module Internal { ) { isGuardedByNode1(guarded, g, sub, v) and sub = g.getAChildExpr*() and - forall(Ssa::Definition def | def = sub.getAnSsaQualifier(_) | - isGuardedByNode2(guarded, def) - ) + forall(Ssa::Definition def | def = sub.getAnSsaQualifier(_) | isGuardedByNode2(guarded, def)) } /** diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/DataFlow.qll b/csharp/ql/src/semmle/code/csharp/dataflow/DataFlow.qll index 7796cca4e2b..07766786b34 100755 --- a/csharp/ql/src/semmle/code/csharp/dataflow/DataFlow.qll +++ b/csharp/ql/src/semmle/code/csharp/dataflow/DataFlow.qll @@ -1188,7 +1188,7 @@ module DataFlow { * nodes that may potentially be reached in flow from some source to some * sink. */ - module Pruning { + private module Pruning { /** * Holds if `node` is reachable from a source in the configuration `config`, * ignoring call contexts. diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/Nullness.qll b/csharp/ql/src/semmle/code/csharp/dataflow/Nullness.qll index ff10d5ae154..5a07845e71b 100644 --- a/csharp/ql/src/semmle/code/csharp/dataflow/Nullness.qll +++ b/csharp/ql/src/semmle/code/csharp/dataflow/Nullness.qll @@ -61,6 +61,10 @@ class AlwaysNullExpr extends Expr { or this instanceof DefaultValueExpr and this.getType().isRefType() or + this = any(Ssa::Definition def | + forex(Ssa::Definition u | u = def.getAnUltimateDefinition() | nullDef(u)) + ).getARead() + or exists(Callable target | this.(Call).getTarget() = target and not target.(Virtualizable).isVirtual() and @@ -69,6 +73,11 @@ class AlwaysNullExpr extends Expr { } } +/** Holds if SSA definition `def` is always `null`. */ +private predicate nullDef(Ssa::ExplicitDefinition def) { + def.getADefinition().getSource() instanceof AlwaysNullExpr +} + /** An expression that is never `null`. */ class NonNullExpr extends Expr { NonNullExpr() { @@ -78,7 +87,9 @@ class NonNullExpr extends Expr { or this instanceof G::NullGuardedExpr or - exists(Ssa::Definition def | nonNullDef(def) | this = def.getARead()) + this = any(Ssa::Definition def | + forex(Ssa::Definition u | u = def.getAnUltimateDefinition() | nonNullDef(u)) + ).getARead() or exists(Callable target | this.(Call).getTarget() = target and @@ -90,10 +101,10 @@ class NonNullExpr extends Expr { } /** Holds if SSA definition `def` is never `null`. */ -private predicate nonNullDef(Ssa::Definition v) { - v.(Ssa::ExplicitDefinition).getADefinition().getSource() instanceof NonNullExpr +private predicate nonNullDef(Ssa::ExplicitDefinition def) { + def.getADefinition().getSource() instanceof NonNullExpr or - exists(AssignableDefinition ad | ad = v.(Ssa::ExplicitDefinition).getADefinition() | + exists(AssignableDefinition ad | ad = def.getADefinition() | ad instanceof AssignableDefinitions::IsPatternDefinition or ad instanceof AssignableDefinitions::TypeCasePatternDefinition diff --git a/csharp/ql/test/library-tests/cil/dataflow/DataFlow.ql b/csharp/ql/test/library-tests/cil/dataflow/DataFlow.ql index 1db6aa37dee..c80e9ed683e 100644 --- a/csharp/ql/test/library-tests/cil/dataflow/DataFlow.ql +++ b/csharp/ql/test/library-tests/cil/dataflow/DataFlow.ql @@ -1,7 +1,6 @@ import csharp import semmle.code.csharp.dataflow.DataFlow::DataFlow -// import DataFlow::PathGraph - + class FlowConfig extends Configuration { FlowConfig() { this = "FlowConfig" } diff --git a/csharp/ql/test/library-tests/cil/dataflow/Nullness.expected b/csharp/ql/test/library-tests/cil/dataflow/Nullness.expected index 9afaa675dce..8d840cd1e48 100644 --- a/csharp/ql/test/library-tests/cil/dataflow/Nullness.expected +++ b/csharp/ql/test/library-tests/cil/dataflow/Nullness.expected @@ -1,9 +1,11 @@ alwaysNull | dataflow.cs:70:21:70:35 | default(...) | +| dataflow.cs:74:21:74:34 | call to method NullFunction | | dataflow.cs:74:39:74:52 | call to method IndirectNull | | dataflow.cs:78:21:78:45 | call to method ReturnsNull | | dataflow.cs:79:21:79:46 | call to method ReturnsNull2 | | dataflow.cs:80:21:80:44 | access to property NullProperty | +| dataflow.cs:89:31:89:44 | call to method NullFunction | alwaysNotNull | dataflow.cs:71:24:71:35 | default(...) | | dataflow.cs:72:27:72:30 | this access | diff --git a/csharp/ql/test/library-tests/controlflow/guards/ExtractorOptions.cs b/csharp/ql/test/library-tests/controlflow/guards/ExtractorOptions.cs new file mode 100644 index 00000000000..5960523e227 --- /dev/null +++ b/csharp/ql/test/library-tests/controlflow/guards/ExtractorOptions.cs @@ -0,0 +1 @@ +// semmle-extractor-options: --cil diff --git a/csharp/ql/test/query-tests/Nullness/Implications.expected b/csharp/ql/test/query-tests/Nullness/Implications.expected index 2436ab3af33..dbb8657aa27 100644 --- a/csharp/ql/test/query-tests/Nullness/Implications.expected +++ b/csharp/ql/test/query-tests/Nullness/Implications.expected @@ -952,6 +952,8 @@ | D.cs:212:18:212:18 | access to local variable n | null | D.cs:211:20:211:23 | null | null | | D.cs:212:18:212:26 | ... == ... | false | D.cs:212:18:212:18 | access to local variable n | non-null | | D.cs:212:18:212:26 | ... == ... | true | D.cs:212:18:212:18 | access to local variable n | null | +| D.cs:212:18:212:45 | ... ? ... : ... | non-null | D.cs:212:18:212:26 | ... == ... | true | +| D.cs:212:18:212:45 | ... ? ... : ... | non-null | D.cs:212:30:212:41 | object creation of type Object | non-null | | D.cs:212:18:212:45 | ... ? ... : ... | null | D.cs:212:18:212:26 | ... == ... | false | | D.cs:212:18:212:45 | ... ? ... : ... | null | D.cs:212:45:212:45 | access to local variable n | null | | D.cs:212:45:212:45 | access to local variable n | non-null | D.cs:211:20:211:23 | null | non-null |