C++: Solve non-monotonic issue by unfolding dataflow-related predicates until we get to the SSA implementations of them.

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

@@ -436,22 +436,21 @@ class IndirectionPosition extends Position, TIndirectionPosition {
 newtype TPosition =
   TDirectPosition(int index) { exists(any(CallInstruction c).getArgument(index)) } or
   TIndirectionPosition(int argumentIndex, int indirectionIndex) {
-    hasOperandAndIndex(_, any(CallInstruction call).getArgumentOperand(argumentIndex),
+    Ssa::hasIndirectOperand(any(CallInstruction call).getArgumentOperand(argumentIndex),
       indirectionIndex)
   }
 
 private newtype TReturnKind =
   TNormalReturnKind(int indirectionIndex) {
-    exists(IndirectReturnNode return |
-      return.isNormalReturn() and
-      indirectionIndex = return.getIndirectionIndex() - 1 // We subtract one because the return loads the value.
-    )
-    or indirectionIndex = 0 // TODO: very much a bodge so that it works on the test that has no return statements
+    Ssa::hasIndirectOperand(any(ReturnValueInstruction ret).getReturnAddressOperand(),
+      indirectionIndex + 1) // We subtract one because the return loads the value.
+    or
+    indirectionIndex = 0 // TODO: very much a bodge so that it works on the test that has no return statements
   } or
   TIndirectReturnKind(int argumentIndex, int indirectionIndex) {
-    exists(IndirectReturnNode return |
-      return.isParameterReturn(argumentIndex) and
-      indirectionIndex = return.getIndirectionIndex()
+    exists(Ssa::FinalParameterUse use |
+      hasFinalParameterNode(use, _, indirectionIndex) and
+      use.getArgumentIndex() = argumentIndex
     )
   }
 

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

@@ -53,14 +53,22 @@ private newtype TIRDataFlowNode =
     Ssa::hasRawIndirectInstruction(node.asInstruction(), indirectionIndex)
   } or
   TFinalParameterNode(Parameter p, int indirectionIndex) {
-    exists(Ssa::FinalParameterUse use |
+    hasFinalParameterNode(_, p, indirectionIndex)
+  } or
+  TFinalGlobalValue(Ssa::GlobalUse globalUse) or
+  TInitialGlobalValue(Ssa::GlobalDef globalUse) or
+  FlowSummaryNode(FlowSummaryImpl::Private::SummaryNode sn)
+
+/**
+ * Holds if `(p, indirectionIndex)` should define a `TFinalParameterNode`
+ * entry because `use` represents the final use of a parameter that has been
+ * written to in the enclosing function of `p`.
+ */
+predicate hasFinalParameterNode(Ssa::FinalParameterUse use, Parameter p, int indirectionIndex) {
   use.getParameter() = p and
   use.getIndirectionIndex() = indirectionIndex and
   parameterIsRedefined(p)
-    )
-  } or
-  TFinalGlobalValue(Ssa::GlobalUse globalUse) or
-  TInitialGlobalValue(Ssa::GlobalDef globalUse)
+}
 
 /**
  * Holds if the value of `*p` (or `**p`, `***p`, etc.) is redefined somewhere in the body

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

@@ -70,18 +70,22 @@ private module SourceVariables {
 
 import SourceVariables
 
+predicate hasIndirectOperand(Operand op, int indirectionIndex) {
+  exists(CppType type, int m |
+    not ignoreOperand(op) and
+    type = getLanguageType(op) and
+    m = countIndirectionsForCppType(type) and
+    indirectionIndex = [1 .. m]
+  )
+}
+
 /**
  * Holds if the `(operand, indirectionIndex)` columns should be
  * assigned a `RawIndirectOperand` value.
  */
 predicate hasRawIndirectOperand(Operand op, int indirectionIndex) {
-  exists(CppType type, int m |
-    not ignoreOperand(op) and
-    type = getLanguageType(op) and
-    m = countIndirectionsForCppType(type) and
-    indirectionIndex = [1 .. m] and
+  hasIndirectOperand(op, indirectionIndex) and
   not hasIRRepresentationOfIndirectOperand(op, indirectionIndex, _, _)
-  )
 }
 
 /**
@@ -403,6 +407,8 @@ class FinalParameterUse extends UseImpl, TFinalParameterUse {
 
   Parameter getParameter() { result = p }
 
+  int getArgumentIndex() { result = p.getIndex() }
+
   override Node getNode() { finalParameterNodeHasParameterAndIndex(result, p, ind) }
 
   override int getIndirection() { result = ind + 1 }