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,49 @@
+/** 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
+  }
+}

csharp/ql/test/library-tests/commons/Assertions/Assertions.expected

@@ -14,6 +14,14 @@ assertTrue
 | Assertions.cs:37:9:37:33 | call to method MyAssert | Assertions.cs:37:29:37:32 | true |
 | Assertions.cs:38:9:38:35 | call to method MyAssert2 | Assertions.cs:38:30:38:34 | false |
 | Assertions.cs:39:9:39:34 | call to method MyAssert2 | Assertions.cs:39:30:39:33 | true |
+| Assertions.cs:44:9:44:36 | call to method Requires | Assertions.cs:44:27:44:35 | ... != ... |
+| Assertions.cs:45:9:45:58 | call to method Requires | Assertions.cs:45:27:45:35 | ... != ... |
+| Assertions.cs:46:9:46:47 | call to method Requires | Assertions.cs:46:38:46:46 | ... != ... |
+| Assertions.cs:47:9:47:69 | call to method Requires | Assertions.cs:47:38:47:46 | ... != ... |
+| Assertions.cs:48:9:48:34 | call to method Assert | Assertions.cs:48:25:48:33 | ... != ... |
+| Assertions.cs:49:9:49:51 | call to method Assert | Assertions.cs:49:25:49:33 | ... != ... |
+| Assertions.cs:50:9:50:34 | call to method Assume | Assertions.cs:50:25:50:33 | ... != ... |
+| Assertions.cs:51:9:51:51 | call to method Assume | Assertions.cs:51:25:51:33 | ... != ... |
 assertFalse
 | Assertions.cs:22:9:22:33 | call to method IsFalse | Assertions.cs:22:24:22:32 | ... != ... |
 | Assertions.cs:23:9:23:33 | call to method IsFalse | Assertions.cs:23:24:23:32 | ... == ... |