C#: Initial implementation of Type based summarymodel generation.

csharp/ql/src/utils/model-generator/CaptureDiscardedSummaryModels.ql

@@ -4,10 +4,10 @@
  * @id csharp/utils/model-generator/discarded-summary-models
  */
 
-private import semmle.code.csharp.dataflow.ExternalFlow
+import semmle.code.csharp.dataflow.ExternalFlow
-private import internal.CaptureModels
+import internal.CaptureModels
-private import internal.CaptureSummaryFlow
+import internal.CaptureSummaryFlow
 
-from TargetApi api, string flow
+from DataFlowTargetApi api, string flow
 where flow = captureFlow(api) and hasSummary(api, false)
 select flow order by flow

csharp/ql/src/utils/model-generator/CaptureNegativeSummaryModels.ql

@@ -6,10 +6,12 @@
  * @tags model-generator
  */
 
-private import semmle.code.csharp.dataflow.ExternalFlow
+import semmle.code.csharp.dataflow.ExternalFlow
-private import internal.CaptureModels
+import internal.CaptureModels
-private import internal.CaptureSummaryFlow
+import internal.CaptureSummaryFlow
 
-from TargetApi api, string noflow
+from DataFlowTargetApi api, string noflow
-where noflow = captureNoFlow(api) and not hasSummary(api, false)
+where
+  noflow = captureNoFlow(api) and
+  not hasSummary(api, false)
 select noflow order by noflow

csharp/ql/src/utils/model-generator/CaptureSinkModels.ql

@@ -6,8 +6,8 @@
  * @tags model-generator
  */
 
-private import internal.CaptureModels
+import internal.CaptureModels
 
-from TargetApi api, string sink
+from DataFlowTargetApi api, string sink
 where sink = captureSink(api)
 select sink order by sink

csharp/ql/src/utils/model-generator/CaptureSourceModels.ql

@@ -6,8 +6,8 @@
  * @tags model-generator
  */
 
-private import internal.CaptureModels
+import internal.CaptureModels
 
-from TargetApi api, string source
+from DataFlowTargetApi api, string source
 where source = captureSource(api)
 select source order by source

csharp/ql/src/utils/model-generator/CaptureSummaryModels.ql

@@ -6,10 +6,10 @@
  * @tags model-generator
  */
 
-private import semmle.code.csharp.dataflow.ExternalFlow
+import semmle.code.csharp.dataflow.ExternalFlow
-private import internal.CaptureModels
+import internal.CaptureModels
-private import internal.CaptureSummaryFlow
+import internal.CaptureSummaryFlow
 
-from TargetApi api, string flow
+from DataFlowTargetApi api, string flow
 where flow = captureFlow(api) and not hasSummary(api, false)
 select flow order by flow

csharp/ql/src/utils/model-generator/CaptureTheoremsForFreeSummaryModels.ql

@@ -0,0 +1,14 @@
+/**
+ * @name Capture Theorems for Free summary models.
+ * @description Finds applicable summary models to be used by other queries.
+ * @kind diagnostic
+ * @id cs/utils/model-generator/summary-models-theorems-for-free
+ * @tags model-generator
+ */
+
+import semmle.code.csharp.dataflow.ExternalFlow
+import internal.CaptureTheoremsForFreeSummaryModels
+
+from TheoremTargetApi api, string flow
+where flow = captureFlow(api)
+select flow order by flow

csharp/ql/src/utils/model-generator/internal/CaptureModels.qll

@@ -5,7 +5,9 @@
 
 private import CaptureModelsSpecific
 
-class TargetApi = TargetApiSpecific;
+class DataFlowTargetApi extends TargetApiSpecific {
+  DataFlowTargetApi() { isRelevantForFlowModels(this) }
+}
 
 /**
  * Holds if data can flow from `node1` to `node2` either via a read or a write of an intermediate field `f`.
@@ -40,7 +42,7 @@ private predicate isRelevantContent(DataFlow::Content c) {
  * Gets the summary model for `api` with `input`, `output` and `kind`.
  */
 bindingset[input, output, kind]
-private string asSummaryModel(TargetApi api, string input, string output, string kind) {
+private string asSummaryModel(TargetApiSpecific api, string input, string output, string kind) {
   result =
     asPartialModel(api) + input + ";" //
       + output + ";" //
@@ -48,13 +50,15 @@ private string asSummaryModel(TargetApi api, string input, string output, string
       + "generated"
 }
 
-string asNegativeSummaryModel(TargetApi api) { result = asPartialNegativeModel(api) + "generated" }
+string asNegativeSummaryModel(TargetApiSpecific api) {
+  result = asPartialNegativeModel(api) + "generated"
+}
 
 /**
  * Gets the value summary model for `api` with `input` and `output`.
  */
 bindingset[input, output]
-private string asValueModel(TargetApi api, string input, string output) {
+private string asValueModel(TargetApiSpecific api, string input, string output) {
   result = asSummaryModel(api, input, output, "value")
 }
 
@@ -62,7 +66,7 @@ private string asValueModel(TargetApi api, string input, string output) {
  * Gets the taint summary model for `api` with `input` and `output`.
  */
 bindingset[input, output]
-private string asTaintModel(TargetApi api, string input, string output) {
+string asTaintModel(TargetApiSpecific api, string input, string output) {
   result = asSummaryModel(api, input, output, "taint")
 }
 
@@ -70,7 +74,7 @@ private string asTaintModel(TargetApi api, string input, string output) {
  * Gets the sink model for `api` with `input` and `kind`.
  */
 bindingset[input, kind]
-private string asSinkModel(TargetApi api, string input, string kind) {
+private string asSinkModel(TargetApiSpecific api, string input, string kind) {
   result =
     asPartialModel(api) + input + ";" //
       + kind + ";" //
@@ -81,7 +85,7 @@ private string asSinkModel(TargetApi api, string input, string kind) {
  * Gets the source model for `api` with `output` and `kind`.
  */
 bindingset[output, kind]
-private string asSourceModel(TargetApi api, string output, string kind) {
+private string asSourceModel(TargetApiSpecific api, string output, string kind) {
   result =
     asPartialModel(api) + output + ";" //
       + kind + ";" //
@@ -91,7 +95,7 @@ private string asSourceModel(TargetApi api, string output, string kind) {
 /**
  * Gets the summary model of `api`, if it follows the `fluent` programming pattern (returns `this`).
  */
-string captureQualifierFlow(TargetApi api) {
+string captureQualifierFlow(TargetApiSpecific api) {
   exists(DataFlowImplCommon::ReturnNodeExt ret |
     api = returnNodeEnclosingCallable(ret) and
     isOwnInstanceAccessNode(ret)
@@ -140,7 +144,7 @@ private class ThroughFlowConfig extends TaintTracking::Configuration {
 
   override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) {
     source instanceof DataFlow::ParameterNode and
-    source.getEnclosingCallable() instanceof TargetApi and
+    source.getEnclosingCallable() instanceof DataFlowTargetApi and
     state.(TaintRead).getStep() = 0
   }
 
@@ -184,7 +188,7 @@ private class ThroughFlowConfig extends TaintTracking::Configuration {
 /**
  * Gets the summary model(s) of `api`, if there is flow from parameters to return value or parameter.
  */
-string captureThroughFlow(TargetApi api) {
+string captureThroughFlow(DataFlowTargetApi api) {
   exists(
     ThroughFlowConfig config, DataFlow::ParameterNode p,
     DataFlowImplCommon::ReturnNodeExt returnNodeExt, string input, string output
@@ -211,7 +215,7 @@ private class FromSourceConfiguration extends TaintTracking::Configuration {
   override predicate isSource(DataFlow::Node source) { ExternalFlow::sourceNode(source, _) }
 
   override predicate isSink(DataFlow::Node sink) {
-    exists(TargetApi c |
+    exists(DataFlowTargetApi c |
       sink instanceof DataFlowImplCommon::ReturnNodeExt and
       sink.getEnclosingCallable() = c
     )
@@ -229,7 +233,7 @@ private class FromSourceConfiguration extends TaintTracking::Configuration {
 /**
  * Gets the source model(s) of `api`, if there is flow from an existing known source to the return of `api`.
  */
-string captureSource(TargetApi api) {
+string captureSource(DataFlowTargetApi api) {
   exists(DataFlow::Node source, DataFlow::Node sink, FromSourceConfiguration config, string kind |
     config.hasFlow(source, sink) and
     ExternalFlow::sourceNode(source, kind) and
@@ -259,7 +263,7 @@ private class PropagateToSinkConfiguration extends PropagateToSinkConfigurationS
 /**
  * Gets the sink model(s) of `api`, if there is flow from a parameter to an existing known sink.
  */
-string captureSink(TargetApi api) {
+string captureSink(DataFlowTargetApi api) {
   exists(DataFlow::Node src, DataFlow::Node sink, PropagateToSinkConfiguration config, string kind |
     config.hasFlow(src, sink) and
     ExternalFlow::sinkNode(sink, kind) and

csharp/ql/src/utils/model-generator/internal/CaptureModelsSpecific.qll

@@ -36,10 +36,21 @@ private predicate isRelevantForModels(CS::Callable api) {
   api.getDeclaringType().getNamespace().getQualifiedName() != "" and
   not api instanceof CS::ConversionOperator and
   not api instanceof Util::MainMethod and
-  not isHigherOrder(api) and
   not api instanceof CS::Destructor
 }
 
+/**
+ * Holds if it is relevant to generate models for `api` based on data flow analysis.
+ */
+predicate isRelevantForFlowModels(CS::Callable api) {
+  isRelevantForModels(api) and not isHigherOrder(api)
+}
+
+/**
+ * Holds if it is relevant to generate models for `api` based on Theorems for Free.
+ */
+predicate isRelevantForTheoremModels = isRelevantForModels/1;
+
 /**
  * A class of callables that are relevant generating summary, source and sinks models for.
  *
@@ -49,8 +60,7 @@ private predicate isRelevantForModels(CS::Callable api) {
 class TargetApiSpecific extends DotNet::Callable {
   TargetApiSpecific() {
     this.fromSource() and
-    this.isUnboundDeclaration() and
+    this.isUnboundDeclaration()
-    isRelevantForModels(this)
   }
 }
 
@@ -100,7 +110,7 @@ predicate isRelevantType(CS::Type t) {
  */
 string qualifierString() { result = "Argument[this]" }
 
-private string parameterAccess(CS::Parameter p) {
+string parameterAccess(CS::Parameter p) {
   if Collections::isCollectionType(p.getType())
   then result = "Argument[" + p.getPosition() + "].Element"
   else result = "Argument[" + p.getPosition() + "]"

csharp/ql/src/utils/model-generator/internal/CaptureSummaryFlow.qll

@@ -75,7 +75,7 @@ private import CaptureModels
  * Captured Model:
  * ```Summaries;BasicFlow;false;AssignToArray;(System.Int32,System.Int32[]);Argument[0];Argument[1].Element;taint```
  */
-string captureFlow(TargetApi api) {
+string captureFlow(DataFlowTargetApi api) {
   result = captureQualifierFlow(api) or
   result = captureThroughFlow(api)
 }
@@ -84,7 +84,7 @@ string captureFlow(TargetApi api) {
  * Gets the negative summary for `api`, if any.
  * A negative summary is generated, if there does not exist any positive flow.
  */
-string captureNoFlow(TargetApi api) {
+string captureNoFlow(DataFlowTargetApi api) {
   not exists(captureFlow(api)) and
   result = asNegativeSummaryModel(api)
 }

csharp/ql/src/utils/model-generator/internal/CaptureTheoremsForFreeSummaryModels.qll

@@ -0,0 +1,118 @@
+private import csharp
+private import semmle.code.csharp.commons.Collections as Collections
+private import semmle.code.csharp.dataflow.internal.DataFlowPrivate
+private import semmle.code.csharp.frameworks.system.linq.Expressions
+private import CaptureModelsSpecific as Specific
+private import CaptureModels
+
+/**
+ * A class of callables that are relevant generating summaries for based
+ * on the Theorems for Free approach.
+ */
+class TheoremTargetApi extends Specific::TargetApiSpecific {
+  TheoremTargetApi() { Specific::isRelevantForTheoremModels(this) }
+
+  private predicate isClassTypeParameter(TypeParameter t) {
+    t = this.getDeclaringType().(UnboundGeneric).getATypeParameter()
+  }
+
+  private predicate isMethodTypeParameter(TypeParameter t) {
+    t = this.(UnboundGeneric).getATypeParameter()
+  }
+
+  bindingset[t]
+  private string getAccess(TypeParameter t) {
+    exists(string access |
+      if Collections::isCollectionType(this.getDeclaringType())
+      then access = ".Element"
+      else access = ""
+    |
+      result = Specific::qualifierString() + ".SyntheticField[Arg" + t.getName() + "]" + access
+    )
+  }
+
+  private predicate returns(TypeParameter t) { this.getReturnType() = t }
+
+  private predicate parameter(TypeParameter t, Parameter p) {
+    p = this.getAParameter() and
+    p.getType() = t
+  }
+
+  /**
+   * Gets the string representation of a summary for `this`, where this has a signature like
+   * this : T -> unit
+   * where T is type parameter for the class declaring `this`.
+   */
+  private string getSetterSummary() {
+    exists(TypeParameter t, Parameter p |
+      this.isClassTypeParameter(t) and
+      this.getReturnType() instanceof VoidType and
+      this.parameter(t, p)
+    |
+      result = asTaintModel(this, Specific::parameterAccess(p), this.getAccess(t))
+    )
+  }
+
+  /**
+   * Gets the string representation of a summary for `this`, where this has a signature like
+   * this : unit -> T
+   * where T is type parameter for the class declaring `this`.
+   */
+  private string getGetterSummary() {
+    exists(TypeParameter t |
+      this.isClassTypeParameter(t) and
+      this.returns(t) and
+      not this.parameter(t, _)
+    |
+      result = asTaintModel(this, this.getAccess(t), "ReturnValue")
+    )
+  }
+
+  /**
+   * Gets the string representation of a summary for `this`, where this has a signature like
+   * this : T -> T
+   */
+  private string getTransformSummary() {
+    exists(TypeParameter t, Parameter p |
+      (this.isClassTypeParameter(t) or this.isMethodTypeParameter(t)) and
+      this.returns(t) and
+      this.parameter(t, p)
+    |
+      result = asTaintModel(this, Specific::parameterAccess(p), "ReturnValue")
+    )
+  }
+
+  /**
+   * Gets the string representation of a summary for `this`, where this has a signature like
+   * this : (T -> V1) -> V2
+   * where T is type parameter for the class declaring `this`.
+   */
+  private string getApplySummary() {
+    exists(TypeParameter t, Parameter p1, Parameter p2 |
+      this.isClassTypeParameter(t) and
+      p1 = this.getAParameter() and
+      p2 = p1.getType().(SystemLinqExpressions::DelegateExtType).getDelegateType().getAParameter() and
+      p2.getType() = t
+    |
+      result =
+        asTaintModel(this, this.getAccess(t),
+          Specific::parameterAccess(p1) + ".Parameter[" + p2.getPosition() + "]")
+    )
+  }
+
+  /**
+   * Gets the string representation of all summaries based on the Theorems for Free approach.
+   */
+  string getSummaries() {
+    result =
+      [
+        this.getSetterSummary(), this.getGetterSummary(), this.getTransformSummary(),
+        this.getApplySummary()
+      ]
+  }
+}
+
+/**
+ * Returns the Theorems for Free summaries for `api`.
+ */
+string captureFlow(TheoremTargetApi api) { result = api.getSummaries() }