Merge pull request #339 from hvitved/csharp/cfg/assertions

C#: Detect constantly failing assertions in the CFG

Author: calumgrant

change-notes/1.19/analysis-csharp.md

@@ -2,8 +2,10 @@
 
 ## General improvements
 
-* The control flow graph construction now takes simple Boolean conditions on local scope variables into account. For example, in `if (b) x = 0; if (b) x = 1;`, the control flow graph will reflect that taking the `true` (resp. `false`) branch in the first condition implies taking the same branch in the second condition. In effect, the first assignment to `x` will now be identified as being dead.
-
+* Control flow graph improvements:
+  * The control flow graph construction now takes simple Boolean conditions on local scope variables into account. For example, in `if (b) x = 0; if (b) x = 1;`, the control flow graph will reflect that taking the `true` (resp. `false`) branch in the first condition implies taking the same branch in the second condition. In effect, the first assignment to `x` will now be identified as being dead.
+  * Code that is only reachable from a constant failing assertion, such as `Debug.Assert(false)`, is considered to be unreachable.
+  
 ## New queries
 
 | **Query**                   | **Tags**  | **Purpose**                                                        |

csharp/ql/src/semmle/code/csharp/commons/Assertions.qll

@@ -1,11 +1,20 @@
 /** Provides classes for assertions. */
 private import semmle.code.csharp.frameworks.system.Diagnostics
 private import semmle.code.csharp.frameworks.test.VisualStudio
+private import semmle.code.csharp.frameworks.System
 
 /** An assertion method. */
 abstract class AssertMethod extends Method {
   /** Gets the index of the parameter being asserted. */
   abstract int getAssertionIndex();
+
+  /** Gets the parameter being asserted. */
+  final Parameter getAssertedParameter() {
+    result = this.getParameter(this.getAssertionIndex())
+  }
+
+  /** Gets the exception being thrown if the assertion fails, if any. */
+  abstract ExceptionClass getExceptionClass();
 }
 
 /** A positive assertion method. */
@@ -24,6 +33,36 @@ abstract class AssertNullMethod extends AssertMethod {
 abstract class AssertNonNullMethod extends AssertMethod {
 }
 
+/** An assertion, that is, a call to an assertion method. */
+class Assertion extends MethodCall {
+  private AssertMethod target;
+
+  Assertion() { this.getTarget() = target }
+
+  /** Gets the assertion method targeted by this assertion. */
+  AssertMethod getAssertMethod() { result = target }
+
+  /** Gets the expression that this assertion pertains to. */
+  Expr getExpr() {
+    result = this.getArgumentForParameter(target.getAssertedParameter())
+  }
+}
+
+/** A trivially failing assertion, for example `Debug.Assert(false)`. */
+class FailingAssertion extends Assertion {
+  FailingAssertion() {
+    exists(AssertMethod am, Expr e |
+      am = this.getAssertMethod() and
+      e = this.getExpr() |
+      am instanceof AssertTrueMethod and
+      e.getValue() = "false"
+      or
+      am instanceof AssertFalseMethod and
+      e.getValue() = "true"
+    )
+  }
+}
+
 /**
  * A `System.Diagnostics.Debug` assertion method.
  */
@@ -33,6 +72,12 @@ class SystemDiagnosticsDebugAssertTrueMethod extends AssertTrueMethod {
   }
 
   override int getAssertionIndex() { result = 0 }
+
+  override ExceptionClass getExceptionClass() {
+    // A failing assertion generates a message box, see
+    // https://docs.microsoft.com/en-us/dotnet/api/system.diagnostics.debug.assert
+    none()
+  }
 }
 
 /** A Visual Studio assertion method. */
@@ -42,6 +87,8 @@ class VSTestAssertTrueMethod extends AssertTrueMethod {
   }
 
   override int getAssertionIndex() { result = 0 }
+
+  override AssertFailedExceptionClass getExceptionClass() { any() }
 }
 
 /** A Visual Studio negated assertion method. */
@@ -51,6 +98,8 @@ class VSTestAssertFalseMethod extends AssertFalseMethod {
   }
 
   override int getAssertionIndex() { result = 0 }
+
+  override AssertFailedExceptionClass getExceptionClass() { any() }
 }
 
 /** A Visual Studio `null` assertion method. */
@@ -60,6 +109,8 @@ class VSTestAssertNullMethod extends AssertNullMethod {
   }
 
   override int getAssertionIndex() { result = 0 }
+
+  override AssertFailedExceptionClass getExceptionClass() { any() }
 }
 
 /** A Visual Studio non-`null` assertion method. */
@@ -69,28 +120,50 @@ class VSTestAssertNonNullMethod extends AssertNonNullMethod {
   }
 
   override int getAssertionIndex() { result = 0 }
+
+  override AssertFailedExceptionClass getExceptionClass() { any() }
 }
 
 /** A method that forwards to another assertion method. */
 class ForwarderAssertMethod extends AssertMethod {
   AssertMethod forwardee;
-  int assertionIndex;
+  Parameter p;
 
   ForwarderAssertMethod() {
-    exists(AssignableDefinitions::ImplicitParameterDefinition def, ParameterRead pr |
-      def.getParameter() = this.getParameter(assertionIndex) and
-      pr = def.getAReachableRead() and
-      pr.getAControlFlowNode().postDominates(this.getEntryPoint()) and
-      forwardee.getParameter(forwardee.getAssertionIndex()).getAnAssignedArgument() = pr
+    p = this.getAParameter() and
+    strictcount(AssignableDefinition def | def.getTarget() = p) = 1 and
+    forex(ControlFlowElement body |
+      body = this.getABody() |
+      exists(Assertion a |
+        body = getAnAssertingElement(a) and
+        a.getExpr() = p.getAnAccess() and
+        forwardee = a.getAssertMethod()
+      )
     )
   }
 
-  override int getAssertionIndex() { result = assertionIndex }
+  override int getAssertionIndex() { result = p.getPosition() }
 
+  override ExceptionClass getExceptionClass() {
+    result = forwardee.getExceptionClass()
+  }
+  
   /** Gets the underlying assertion method that is being forwarded to. */
   AssertMethod getUnderlyingAssertMethod() { result = forwardee }
 }
 
+private ControlFlowElement getAnAssertingElement(Assertion a) {
+  result = a
+  or
+  result = getAnAssertingStmt(a)
+}
+
+private Stmt getAnAssertingStmt(Assertion a) {
+  result.(ExprStmt).getExpr() = getAnAssertingElement(a)
+  or
+  result.(BlockStmt).getFirstStmt() = getAnAssertingElement(a)
+}
+
 /** A method that forwards to a positive assertion method. */
 class ForwarderAssertTrueMethod extends ForwarderAssertMethod, AssertTrueMethod {
   ForwarderAssertTrueMethod() {
@@ -121,8 +194,5 @@ class ForwarderAssertNonNullMethod extends ForwarderAssertMethod, AssertNonNullM
 
 /** Holds if expression `e` appears in an assertion. */
 predicate isExprInAssertion(Expr e) {
-  exists(MethodCall call, AssertMethod assertMethod |
-    call.getTarget() = assertMethod |
-    e = call.getArgument(assertMethod.getAssertionIndex()).getAChildExpr*()
-  )
+  e = any(Assertion a).getExpr().getAChildExpr*()
 }

csharp/ql/src/semmle/code/csharp/controlflow/Completion.qll

@@ -59,6 +59,8 @@ private newtype TCompletion =
   TGotoDefaultCompletion()
   or
   TThrowCompletion(ExceptionClass ec)
+  or
+  TExitCompletion()
 
 /**
  * A completion of a statement or an expression.
@@ -642,3 +644,16 @@ class ThrowCompletion extends Completion, TThrowCompletion {
 
   override string toString() { result = "throw(" + getExceptionClass() + ")" }
 }
+
+/**
+ * A completion that represents evaluation of a statement or an
+ * expression resulting in a program exit, for example
+ * `System.Environment.Exit(0)`.
+ *
+ * An exit completion is different from a `return` completion; the former
+ * exits the whole application, and exists inside `try` statements skip
+ * `finally` blocks.
+ */
+class ExitCompletion extends Completion, TExitCompletion {
+  override string toString() { result = "exit" }
+}