Dataflow: Support alert provenance

cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl1.qll

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {

cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {

cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {

cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {

cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplLocal.qll

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {

cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowPrivate.qll

@@ -286,6 +286,10 @@ predicate lambdaCall(DataFlowCall call, LambdaCallKind kind, Node receiver) { no
 /** Extra data-flow steps needed for lambda flow analysis. */
 predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preservesValue) { none() }
 
+predicate knownSourceModel(Node source, string model) { none() }
+
+predicate knownSinkModel(Node sink, string model) { none() }
+
 /**
  * Holds if flow is allowed to pass from parameter `p` and back to itself as a
  * side-effect, resulting in a summary from `p` to itself.

cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowUtil.qll

@@ -516,7 +516,7 @@ private module ThisFlow {
  */
 cached
 predicate localFlowStep(Node nodeFrom, Node nodeTo) {
-  simpleLocalFlowStep(nodeFrom, nodeTo)
+  simpleLocalFlowStep(nodeFrom, nodeTo, _)
   or
   // Field flow is not strictly a "step" but covers the whole function
   // transitively. There's no way to get a step-like relation out of the global
@@ -530,64 +530,67 @@ predicate localFlowStep(Node nodeFrom, Node nodeTo) {
  * This is the local flow predicate that's used as a building block in global
  * data flow. It may have less flow than the `localFlowStep` predicate.
  */
-predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo) {
-  // Expr -> Expr
-  exprToExprStep_nocfg(nodeFrom.asExpr(), nodeTo.asExpr())
-  or
-  // Assignment -> LValue post-update node
-  //
-  // This is used for assignments whose left-hand side is not a variable
-  // assignment or a storeStep but is still modeled by other means. It could be
-  // a call to `operator*` or `operator[]` where taint should flow to the
-  // post-update node of the qualifier.
-  exists(AssignExpr assign |
-    nodeFrom.asExpr() = assign and
-    nodeTo.(PostUpdateNode).getPreUpdateNode().asExpr() = assign.getLValue()
-  )
-  or
-  // Node -> FlowVar -> VariableAccess
-  exists(FlowVar var |
-    (
-      exprToVarStep(nodeFrom.asExpr(), var)
-      or
-      varSourceBaseCase(var, nodeFrom.asParameter())
-      or
-      varSourceBaseCase(var, nodeFrom.asUninitialized())
-      or
-      var.definedPartiallyAt(nodeFrom.asPartialDefinition())
-    ) and
-    varToNodeStep(var, nodeTo)
-  )
-  or
-  // Expr -> DefinitionByReferenceNode
-  exprToDefinitionByReferenceStep(nodeFrom.asExpr(), nodeTo.asDefiningArgument())
-  or
-  // `this` -> adjacent-`this`
-  ThisFlow::adjacentThisRefs(nodeFrom, nodeTo)
-  or
-  // post-update-`this` -> following-`this`-ref
-  ThisFlow::adjacentThisRefs(nodeFrom.(PostUpdateNode).getPreUpdateNode(), nodeTo)
-  or
-  // In `f(&x->a)`, this step provides the flow from post-`&` to post-`x->a`,
-  // from which there is field flow to `x` via reverse read.
-  exists(PartialDefinition def, Expr inner, Expr outer |
-    def.definesExpressions(inner, outer) and
-    inner = nodeTo.(InnerPartialDefinitionNode).getPreUpdateNode().asExpr() and
-    outer = nodeFrom.(PartialDefinitionNode).getPreUpdateNode().asExpr()
-  )
-  or
-  // Reverse flow: data that flows from the post-update node of a reference
-  // returned by a function call, back into the qualifier of that function.
-  // This allows data to flow 'in' through references returned by a modeled
-  // function such as `operator[]`.
-  exists(DataFlowFunction f, Call call, FunctionInput inModel, FunctionOutput outModel |
-    call.getTarget() = f and
-    inModel.isReturnValueDeref() and
-    outModel.isQualifierObject() and
-    f.hasDataFlow(inModel, outModel) and
-    nodeFrom.(PostUpdateNode).getPreUpdateNode().asExpr() = call and
-    nodeTo.asDefiningArgument() = call.getQualifier()
-  )
+predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo, string model) {
+  (
+    // Expr -> Expr
+    exprToExprStep_nocfg(nodeFrom.asExpr(), nodeTo.asExpr())
+    or
+    // Assignment -> LValue post-update node
+    //
+    // This is used for assignments whose left-hand side is not a variable
+    // assignment or a storeStep but is still modeled by other means. It could be
+    // a call to `operator*` or `operator[]` where taint should flow to the
+    // post-update node of the qualifier.
+    exists(AssignExpr assign |
+      nodeFrom.asExpr() = assign and
+      nodeTo.(PostUpdateNode).getPreUpdateNode().asExpr() = assign.getLValue()
+    )
+    or
+    // Node -> FlowVar -> VariableAccess
+    exists(FlowVar var |
+      (
+        exprToVarStep(nodeFrom.asExpr(), var)
+        or
+        varSourceBaseCase(var, nodeFrom.asParameter())
+        or
+        varSourceBaseCase(var, nodeFrom.asUninitialized())
+        or
+        var.definedPartiallyAt(nodeFrom.asPartialDefinition())
+      ) and
+      varToNodeStep(var, nodeTo)
+    )
+    or
+    // Expr -> DefinitionByReferenceNode
+    exprToDefinitionByReferenceStep(nodeFrom.asExpr(), nodeTo.asDefiningArgument())
+    or
+    // `this` -> adjacent-`this`
+    ThisFlow::adjacentThisRefs(nodeFrom, nodeTo)
+    or
+    // post-update-`this` -> following-`this`-ref
+    ThisFlow::adjacentThisRefs(nodeFrom.(PostUpdateNode).getPreUpdateNode(), nodeTo)
+    or
+    // In `f(&x->a)`, this step provides the flow from post-`&` to post-`x->a`,
+    // from which there is field flow to `x` via reverse read.
+    exists(PartialDefinition def, Expr inner, Expr outer |
+      def.definesExpressions(inner, outer) and
+      inner = nodeTo.(InnerPartialDefinitionNode).getPreUpdateNode().asExpr() and
+      outer = nodeFrom.(PartialDefinitionNode).getPreUpdateNode().asExpr()
+    )
+    or
+    // Reverse flow: data that flows from the post-update node of a reference
+    // returned by a function call, back into the qualifier of that function.
+    // This allows data to flow 'in' through references returned by a modeled
+    // function such as `operator[]`.
+    exists(DataFlowFunction f, Call call, FunctionInput inModel, FunctionOutput outModel |
+      call.getTarget() = f and
+      inModel.isReturnValueDeref() and
+      outModel.isQualifierObject() and
+      f.hasDataFlow(inModel, outModel) and
+      nodeFrom.(PostUpdateNode).getPreUpdateNode().asExpr() = call and
+      nodeTo.asDefiningArgument() = call.getQualifier()
+    )
+  ) and
+  model = ""
 }
 
 /**

cpp/ql/lib/semmle/code/cpp/dataflow/internal/TaintTrackingUtil.qll

@@ -32,8 +32,8 @@ predicate localTaintStep(DataFlow::Node src, DataFlow::Node sink) {
  * Holds if the additional step from `src` to `sink` should be included in all
  * global taint flow configurations.
  */
-predicate defaultAdditionalTaintStep(DataFlow::Node src, DataFlow::Node sink) {
-  localAdditionalTaintStep(src, sink)
+predicate defaultAdditionalTaintStep(DataFlow::Node src, DataFlow::Node sink, string model) {
+  localAdditionalTaintStep(src, sink) and model = ""
 }
 
 /**

cpp/ql/lib/semmle/code/cpp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll

@@ -127,7 +127,7 @@ abstract deprecated class Configuration extends DataFlow::Configuration {
 
   final override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
     this.isAdditionalTaintStep(node1, node2) or
-    defaultAdditionalTaintStep(node1, node2)
+    defaultAdditionalTaintStep(node1, node2, _)
   }
 
   /**

cpp/ql/lib/semmle/code/cpp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll

@@ -127,7 +127,7 @@ abstract deprecated class Configuration extends DataFlow::Configuration {
 
   final override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
     this.isAdditionalTaintStep(node1, node2) or
-    defaultAdditionalTaintStep(node1, node2)
+    defaultAdditionalTaintStep(node1, node2, _)
   }
 
   /**

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl1.qll

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll

@@ -1020,6 +1020,10 @@ predicate lambdaCall(DataFlowCall call, LambdaCallKind kind, Node receiver) { no
 /** Extra data-flow steps needed for lambda flow analysis. */
 predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preservesValue) { none() }
 
+predicate knownSourceModel(Node source, string model) { none() }
+
+predicate knownSinkModel(Node sink, string model) { none() }
+
 /**
  * Holds if flow is allowed to pass from parameter `p` and back to itself as a
  * side-effect, resulting in a summary from `p` to itself.
@@ -1096,7 +1100,7 @@ private predicate localFlowStepWithSummaries(Node node1, Node node2) {
   or
   readStep(node1, _, node2)
   or
-  DataFlowImplCommon::argumentValueFlowsThrough(node1, _, node2)
+  DataFlowImplCommon::argumentValueFlowsThrough(node1, _, node2, _)
 }
 
 /** Holds if `node` flows to a node that is used in a `SwitchInstruction`. */