C++: use models in TaintTrackingUtil

cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/TaintTrackingUtil.qll

@@ -1,5 +1,7 @@
 private import semmle.code.cpp.ir.IR
 private import semmle.code.cpp.ir.dataflow.DataFlow
+private import ModelUtil
+private import semmle.code.cpp.models.interfaces.DataFlow
 
 /**
  * Holds if taint propagates from `nodeFrom` to `nodeTo` in exactly one local
@@ -45,6 +47,8 @@ private predicate localInstructionTaintStep(Instruction nodeFrom, Instruction no
   )
   or
   nodeTo.(LoadInstruction).getSourceAddress() = nodeFrom
+  or
+  modeledInstructionTaintStep(nodeFrom, nodeTo)
 }
 
 /**
@@ -82,3 +86,31 @@ predicate defaultAdditionalTaintStep(DataFlow::Node src, DataFlow::Node sink) {
  * but not in local taint.
  */
 predicate defaultTaintBarrier(DataFlow::Node node) { none() }
+
+/**
+ * Holds if taint can flow from `instrIn` to `instrOut` through a call to a
+ * modeled function.
+ */
+predicate modeledInstructionTaintStep(Instruction instrIn, Instruction instrOut) {
+  exists(CallInstruction call, TaintFunction func, FunctionInput modelIn, FunctionOutput modelOut |
+    instrIn = callInput(call, modelIn) and
+    instrOut = callOutput(call, modelOut) and
+    call.getStaticCallTarget() = func and
+    func.hasTaintFlow(modelIn, modelOut)
+  )
+  or
+  // Taint flow from one argument to another and data flow from an argument to a
+  // return value. This happens in functions like `strcat` and `memcpy`. We
+  // could model this flow in two separate steps, but that would add reverse
+  // flow from the write side-effect to the call instruction, which may not be
+  // desirable.
+  exists(CallInstruction call, Function func, FunctionInput modelIn, OutParameterDeref modelMidOut, int indexMid, InParameter modelMidIn, OutReturnValue modelOut |
+    instrIn = callInput(call, modelIn) and
+    instrOut = callOutput(call, modelOut) and
+    call.getStaticCallTarget() = func and
+    func.(TaintFunction).hasTaintFlow(modelIn, modelMidOut) and
+    func.(DataFlowFunction).hasDataFlow(modelMidIn, modelOut) and
+    modelMidOut.isParameterDeref(indexMid) and
+    modelMidIn.isParameter(indexMid)
+  )
+}