Merge pull request #2514 from hvitved/csharp/code-contracts

C#: Recognize Code Contract assertions

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

@@ -1,6 +1,7 @@
 /** Provides classes for assertions. */
 
 private import semmle.code.csharp.frameworks.system.Diagnostics
+private import semmle.code.csharp.frameworks.system.diagnostics.Contracts
 private import semmle.code.csharp.frameworks.test.VisualStudio
 private import semmle.code.csharp.frameworks.System
 private import ControlFlow
@@ -169,6 +170,29 @@ class SystemDiagnosticsDebugAssertTrueMethod extends AssertTrueMethod {
   }
 }
 
+/**
+ * A `System.Diagnostics.Contracts.Contract` assertion method.
+ */
+class SystemDiagnosticsContractAssertTrueMethod extends AssertTrueMethod {
+  SystemDiagnosticsContractAssertTrueMethod() {
+    exists(SystemDiagnosticsContractsContractClass c |
+      this = c.getAnAssertMethod()
+      or
+      this = c.getAnAssumeMethod()
+      or
+      this = c.getARequiresMethod()
+    )
+  }
+
+  override int getAssertionIndex() { result = 0 }
+
+  override Class getExceptionClass() {
+    // A failing assertion generates a message box, see
+    // https://docs.microsoft.com/en-us/dotnet/api/system.diagnostics.contracts.contract.assert
+    none()
+  }
+}
+
 /** A Visual Studio assertion method. */
 class VSTestAssertTrueMethod extends AssertTrueMethod {
   VSTestAssertTrueMethod() { this = any(VSTestAssertClass c).getIsTrueMethod() }

csharp/ql/src/semmle/code/csharp/frameworks/system/Diagnostics.qll

@@ -23,7 +23,7 @@ class SystemDiagnosticsDebugClass extends SystemDiagnosticsClass {
     this.isStatic()
   }
 
-  /** Gets and `Assert(bool, ...)` method. */
+  /** Gets an `Assert(bool, ...)` method. */
   Method getAssertMethod() {
     result.getDeclaringType() = this and
     result.hasName("Assert") and

csharp/ql/src/semmle/code/csharp/frameworks/system/diagnostics/Contracts.qll

@@ -0,0 +1,51 @@
+/** Provides definitions related to the namespace `System.Diagnostics.Contracts`. */
+
+import semmle.code.csharp.Type
+private import semmle.code.csharp.frameworks.system.Diagnostics
+
+/** The `System.Diagnostics.Contracts` namespace. */
+class SystemDiagnosticsContractsNamespace extends Namespace {
+  SystemDiagnosticsContractsNamespace() {
+    this.getParentNamespace() instanceof SystemDiagnosticsNamespace and
+    this.hasName("Contracts")
+  }
+}
+
+/** A class in the `System.Diagnostics.Contracts` namespace. */
+class SystemDiagnosticsContractsClass extends Class {
+  SystemDiagnosticsContractsClass() {
+    this.getNamespace() instanceof SystemDiagnosticsContractsNamespace
+  }
+}
+
+/** The `System.Diagnostics.Contracts.Contract` class. */
+class SystemDiagnosticsContractsContractClass extends SystemDiagnosticsContractsClass {
+  SystemDiagnosticsContractsContractClass() {
+    this.hasName("Contract") and
+    this.isStatic()
+  }
+
+  /** Gets an `Assert(bool, ...)` method. */
+  Method getAnAssertMethod() {
+    result.getDeclaringType() = this and
+    result.hasName("Assert") and
+    result.getParameter(0).getType() instanceof BoolType and
+    result.getReturnType() instanceof VoidType
+  }
+
+  /** Gets an `Assume(bool, ...)` method. */
+  Method getAnAssumeMethod() {
+    result.getDeclaringType() = this and
+    result.hasName("Assume") and
+    result.getParameter(0).getType() instanceof BoolType and
+    result.getReturnType() instanceof VoidType
+  }
+
+  /** Gets a `Requires(bool, ...)` method. */
+  Method getARequiresMethod() {
+    result.getDeclaringType() = this and
+    result.hasName("Requires") and
+    result.getParameter(0).getType() instanceof BoolType and
+    result.getReturnType() instanceof VoidType
+  }
+}