Merge pull request #10238 from michaelnebel/csharp/theoremsforfree

C#: Theorems for Free - Model generation

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

@@ -6,9 +6,9 @@
  * @tags model-generator
  */
 
-private import internal.CaptureModels
-private import internal.CaptureSummaryFlow
+import internal.CaptureModels
+import internal.CaptureSummaryFlow
 
-from TargetApi api, string noflow
+from DataFlowTargetApi api, string noflow
 where noflow = captureNoFlow(api)
 select noflow order by noflow

java/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

java/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

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

@@ -6,9 +6,9 @@
  * @tags model-generator
  */
 
-private import internal.CaptureModels
-private import internal.CaptureSummaryFlow
+import internal.CaptureModels
+import internal.CaptureSummaryFlow
 
-from TargetApi api, string flow
+from DataFlowTargetApi api, string flow
 where flow = captureFlow(api)
 select flow order by flow

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

@@ -5,7 +5,9 @@
 
 private import CaptureModelsSpecific
 
-class TargetApi = TargetApiSpecific;
+class DataFlowTargetApi extends TargetApiSpecific {
+  DataFlowTargetApi() { isRelevantForDataFlowModels(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) {
+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) {
+private 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

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

@@ -59,6 +59,11 @@ private predicate isRelevantForModels(J::Callable api) {
   not api instanceof J::StaticInitializer
 }
 
+/**
+ * Holds if it is relevant to generate models for `api` based on data flow analysis.
+ */
+predicate isRelevantForDataFlowModels = isRelevantForModels/1;
+
 /**
  * A class of Callables that are relevant for generating summary, source and sinks models for.
  *

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

@@ -67,7 +67,7 @@ private import CaptureModels
  * Captured Model:
  * ```p;Foo;true;addToList;;Argument[0];Argument[1];taint```
  */
-string captureFlow(TargetApi api) {
+string captureFlow(DataFlowTargetApi api) {
   result = captureQualifierFlow(api) or
   result = captureThroughFlow(api)
 }
@@ -76,7 +76,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)
 }