Merge pull request #1 from hvitved/cs/non-null-functions

C#: Adjustments to CIL/nullness analyses

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())
+  )
 }

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;

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))
     }
 
     /**

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.

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

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" }
 

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 |

csharp/ql/test/library-tests/controlflow/guards/ExtractorOptions.cs

@@ -0,0 +1 @@
+// semmle-extractor-options: --cil

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 |