Merge remote-tracking branch 'upstream/master' into UselessCat

CONTRIBUTING.md

@@ -46,6 +46,12 @@ Follow the steps below to help other users understand what your query does, and
    Query help files explain the purpose of your query to other users. Write your query help in a `.qhelp` file and save it in the same directory as your new query. 
    For more information on writing query help, see the [Query help style guide](https://github.com/Semmle/ql/blob/master/docs/query-help-style-guide.md).
 
+7. **Maintain backwards compatibility**
+
+The standard CodeQL libraries must evolve in a backwards compatible manner. If any backwards incompatible changes need to be made, the existing API must first be marked as deprecated. This is done by adding a `deprecated` annotation along with a QLDoc reference to the replacement API. Only after at least one full release cycle has elapsed may the old API be removed.
+
+In addition to contributions to our standard queries and libraries, we also welcome contributions of a more experimental nature, which do not need to fulfill all the requirements listed above. See the guidelines for [experimental queries and libraries](docs/experimental.md) for details.
+
 ## Using your personal data
 
 If you contribute to this project, we will record your name and email

change-notes/1.24/analysis-cpp.md

@@ -46,3 +46,5 @@ The following changes in version 1.24 affect C/C++ analysis in all applications.
   the following improvements:
   * The library now models data flow through `strdup` and similar functions.
   * The library now models data flow through formatting functions such as `sprintf`.
+* The security pack taint tracking library (`semmle.code.cpp.security.TaintTracking`) uses a new intermediate representation. This provides a more precise analysis of pointers to stack variables and flow through parameters, improving the results of many security queries.
+* The global value numbering library (`semmle.code.cpp.valuenumbering.GlobalValueNumbering`) uses a new intermediate representation to provide a more precise analysis of heap allocated memory and pointers to stack variables.

change-notes/1.24/analysis-javascript.md

@@ -2,6 +2,8 @@
 
 ## General improvements
 
+* TypeScript 3.8 is now supported.
+
 * Alert suppression can now be done with single-line block comments (`/* ... */`) as well as line comments (`// ...`).
 
 * Imports with the `.js` extension can now be resolved to a TypeScript file,
@@ -13,6 +15,10 @@
 
 * The analysis of sanitizer guards has improved, leading to fewer false-positive results from the security queries.
 
+* The call graph construction has been improved, leading to more results from the security queries:
+  - Calls can now be resolved to indirectly-defined class members in more cases.
+  - Calls through partial invocations such as `.bind` can now be resolved in more cases.
+
 * Support for the following frameworks and libraries has been improved:
   - [Electron](https://electronjs.org/)
   - [Handlebars](https://www.npmjs.com/package/handlebars)
@@ -37,6 +43,7 @@
 | Cross-site scripting through exception (`js/xss-through-exception`) | security, external/cwe/cwe-079, external/cwe/cwe-116              | Highlights potential XSS vulnerabilities where an exception is written to the DOM. Results are not shown on LGTM by default. |
 | Regular expression always matches (`js/regex/always-matches`) | correctness, regular-expressions | Highlights regular expression checks that trivially succeed by matching an empty substring. Results are shown on LGTM by default. |
 | Missing await (`js/missing-await`) | correctness | Highlights expressions that operate directly on a promise object in a nonsensical way, instead of awaiting its result. Results are shown on LGTM by default. |
+| Polynomial regular expression used on uncontrolled data (`js/polynomial-redos`) | security, external/cwe/cwe-730, external/cwe/cwe-400 | Highlights expensive regular expressions that may be used on malicious input. Results are shown on LGTM by default. | 
 | Prototype pollution in utility function (`js/prototype-pollution-utility`) | security, external/cwe/cwe-400, external/cwe/cwe-471 | Highlights recursive copying operations that are susceptible to prototype pollution. Results are shown on LGTM by default. |
 | Unsafe jQuery plugin (`js/unsafe-jquery-plugin`) | Highlights potential XSS vulnerabilities in unsafely designed jQuery plugins. Results are shown on LGTM by default. |
 | Useless use of cat (`js/useless-use-of-cat`) | correctness, security, maintainability | Highlights command executions of `cat` where the fs API should be used instead. Results are shown on LGTM by default. |

config/identical-files.json

@@ -222,10 +222,12 @@
     "cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/PrintSSA.qll",
     "csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll"
   ],
-  "C++ IR ValueNumberInternal": [
+  "IR ValueNumberInternal": [
     "cpp/ql/src/semmle/code/cpp/ir/implementation/raw/gvn/internal/ValueNumberingInternal.qll",
     "cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingInternal.qll",
-    "cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/internal/ValueNumberingInternal.qll"
+    "cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/internal/ValueNumberingInternal.qll",
+    "csharp/ql/src/semmle/code/csharp/ir/implementation/raw/gvn/internal/ValueNumberingInternal.qll",
+    "csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingInternal.qll"
   ],
   "C++ IR ValueNumber": [
     "cpp/ql/src/semmle/code/cpp/ir/implementation/raw/gvn/ValueNumbering.qll",

cpp/ql/src/experimental/README.md

@@ -0,0 +1 @@
+This directory contains [experimental](../../../../docs/experimental.md) CodeQL queries and libraries.

cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowDispatch.qll

@@ -1,7 +1,5 @@
 private import cpp
 
-Function viableImpl(Call call) { result = viableCallable(call) }
-
 /**
  * Gets a function that might be called by `call`.
  */

cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

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

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

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

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

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

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

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

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

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

@@ -132,16 +132,6 @@ OutNode getAnOutNode(DataFlowCall call, ReturnKind kind) {
  */
 predicate jumpStep(Node n1, Node n2) { none() }
 
-/**
- * Holds if `call` passes an implicit or explicit qualifier, i.e., a
- * `this` parameter.
- */
-predicate callHasQualifier(Call call) {
-  call.hasQualifier()
-  or
-  call.getTarget() instanceof Destructor
-}
-
 private newtype TContent =
   TFieldContent(Field f) or
   TCollectionContent() or

cpp/ql/src/semmle/code/cpp/ir/dataflow/DefaultTaintTracking.qll

@@ -343,6 +343,7 @@ private Element adjustedSink(DataFlow::Node sink) {
   result.(AssignOperation).getAnOperand() = sink.asExpr()
 }
 
+cached
 predicate tainted(Expr source, Element tainted) {
   exists(DefaultTaintTrackingCfg cfg, DataFlow::Node sink |
     cfg.hasFlow(getNodeForSource(source), sink) and
@@ -350,6 +351,7 @@ predicate tainted(Expr source, Element tainted) {
   )
 }
 
+cached
 predicate taintedIncludingGlobalVars(Expr source, Element tainted, string globalVar) {
   tainted(source, tainted) and
   globalVar = ""

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

@@ -3,8 +3,6 @@ private import semmle.code.cpp.ir.IR
 private import semmle.code.cpp.ir.dataflow.DataFlow
 private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
 
-Function viableImpl(CallInstruction call) { result = viableCallable(call) }
-
 /**
  * Gets a function that might be called by `call`.
  */

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

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

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

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

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

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

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

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

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

@@ -67,16 +67,6 @@ OutNode getAnOutNode(DataFlowCall call, ReturnKind kind) {
  */
 predicate jumpStep(Node n1, Node n2) { none() }
 
-/**
- * Holds if `call` passes an implicit or explicit qualifier, i.e., a
- * `this` parameter.
- */
-predicate callHasQualifier(Call call) {
-  call.hasQualifier()
-  or
-  call.getTarget() instanceof Destructor
-}
-
 private newtype TContent =
   TFieldContent(Field f) or
   TCollectionContent() or

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

@@ -303,10 +303,12 @@ ParameterNode parameterNode(Parameter p) { result.getParameter() = p }
 VariableNode variableNode(Variable v) { result.getVariable() = v }
 
 /**
+ * DEPRECATED: See UninitializedNode.
+ *
  * Gets the `Node` corresponding to the value of an uninitialized local
  * variable `v`.
  */
-UninitializedNode uninitializedNode(LocalVariable v) { result.getLocalVariable() = v }
+Node uninitializedNode(LocalVariable v) { none() }
 
 /**
  * Holds if data flows from `nodeFrom` to `nodeTo` in exactly one local

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll

@@ -266,6 +266,16 @@ module InstructionSanity {
       funcText = Language::getIdentityString(func.getFunction())
     )
   }
+
+  query predicate switchInstructionWithoutDefaultEdge(
+    SwitchInstruction switchInstr, string message, IRFunction func, string funcText
+  ) {
+    not exists(switchInstr.getDefaultSuccessor()) and
+    message =
+      "SwitchInstruction " + switchInstr.toString() + " without a DefaultEdge in function '$@'." and
+    func = switchInstr.getEnclosingIRFunction() and
+    funcText = Language::getIdentityString(func.getFunction())
+  }
 }
 
 /**

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/ValueNumbering.qll

@@ -27,19 +27,19 @@ class ValueNumber extends TValueNumber {
   final Language::Location getLocation() {
     if
       exists(Instruction i |
-        i = getAnInstruction() and not i.getLocation() instanceof UnknownLocation
+        i = getAnInstruction() and not i.getLocation() instanceof Language::UnknownLocation
       )
     then
       result =
         min(Language::Location l |
-          l = getAnInstruction().getLocation() and not l instanceof UnknownLocation
+          l = getAnInstruction().getLocation() and not l instanceof Language::UnknownLocation
         |
           l
           order by
             l.getFile().getAbsolutePath(), l.getStartLine(), l.getStartColumn(), l.getEndLine(),
             l.getEndColumn()
         )
-    else result instanceof UnknownDefaultLocation
+    else result instanceof Language::UnknownDefaultLocation
   }
 
   /**

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/internal/ValueNumberingImports.qll

@@ -1,4 +1,3 @@
 import semmle.code.cpp.ir.implementation.aliased_ssa.IR
 import semmle.code.cpp.ir.internal.Overlap
 import semmle.code.cpp.ir.internal.IRCppLanguage as Language
-import semmle.code.cpp.Location

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/internal/ValueNumberingInternal.qll

@@ -1,5 +1,4 @@
 private import ValueNumberingImports
-private import cpp
 
 newtype TValueNumber =
   TVariableAddressValueNumber(IRFunction irFunc, Language::AST ast) {
@@ -15,7 +14,7 @@ newtype TValueNumber =
   TStringConstantValueNumber(IRFunction irFunc, IRType type, string value) {
     stringConstantValueNumber(_, irFunc, type, value)
   } or
-  TFieldAddressValueNumber(IRFunction irFunc, Field field, TValueNumber objectAddress) {
+  TFieldAddressValueNumber(IRFunction irFunc, Language::Field field, TValueNumber objectAddress) {
     fieldAddressValueNumber(_, irFunc, field, objectAddress)
   } or
   TBinaryValueNumber(
@@ -33,7 +32,8 @@ newtype TValueNumber =
     unaryValueNumber(_, irFunc, opcode, operand)
   } or
   TInheritanceConversionValueNumber(
-    IRFunction irFunc, Opcode opcode, Class baseClass, Class derivedClass, TValueNumber operand
+    IRFunction irFunc, Opcode opcode, Language::Class baseClass, Language::Class derivedClass,
+    TValueNumber operand
   ) {
     inheritanceConversionValueNumber(_, irFunc, opcode, baseClass, derivedClass, operand)
   } or
@@ -136,7 +136,7 @@ private predicate initializeThisValueNumber(InitializeThisInstruction instr, IRF
   instr.getEnclosingIRFunction() = irFunc
 }
 
-predicate constantValueNumber(
+private predicate constantValueNumber(
   ConstantInstruction instr, IRFunction irFunc, IRType type, string value
 ) {
   instr.getEnclosingIRFunction() = irFunc and

cpp/ql/src/semmle/code/cpp/ir/implementation/raw/Instruction.qll

@@ -266,6 +266,16 @@ module InstructionSanity {
       funcText = Language::getIdentityString(func.getFunction())
     )
   }
+
+  query predicate switchInstructionWithoutDefaultEdge(
+    SwitchInstruction switchInstr, string message, IRFunction func, string funcText
+  ) {
+    not exists(switchInstr.getDefaultSuccessor()) and
+    message =
+      "SwitchInstruction " + switchInstr.toString() + " without a DefaultEdge in function '$@'." and
+    func = switchInstr.getEnclosingIRFunction() and
+    funcText = Language::getIdentityString(func.getFunction())
+  }
 }
 
 /**

cpp/ql/src/semmle/code/cpp/ir/implementation/raw/gvn/ValueNumbering.qll

@@ -27,19 +27,19 @@ class ValueNumber extends TValueNumber {
   final Language::Location getLocation() {
     if
       exists(Instruction i |
-        i = getAnInstruction() and not i.getLocation() instanceof UnknownLocation
+        i = getAnInstruction() and not i.getLocation() instanceof Language::UnknownLocation
       )
     then
       result =
         min(Language::Location l |
-          l = getAnInstruction().getLocation() and not l instanceof UnknownLocation
+          l = getAnInstruction().getLocation() and not l instanceof Language::UnknownLocation
         |
           l
           order by
             l.getFile().getAbsolutePath(), l.getStartLine(), l.getStartColumn(), l.getEndLine(),
             l.getEndColumn()
         )
-    else result instanceof UnknownDefaultLocation
+    else result instanceof Language::UnknownDefaultLocation
   }
 
   /**

cpp/ql/src/semmle/code/cpp/ir/implementation/raw/gvn/internal/ValueNumberingImports.qll

@@ -1,4 +1,3 @@
 import semmle.code.cpp.ir.implementation.aliased_ssa.IR
 import semmle.code.cpp.ir.internal.Overlap
 import semmle.code.cpp.ir.internal.IRCppLanguage as Language
-import semmle.code.cpp.Location

cpp/ql/src/semmle/code/cpp/ir/implementation/raw/gvn/internal/ValueNumberingInternal.qll

@@ -1,5 +1,4 @@
 private import ValueNumberingImports
-private import cpp
 
 newtype TValueNumber =
   TVariableAddressValueNumber(IRFunction irFunc, Language::AST ast) {
@@ -15,7 +14,7 @@ newtype TValueNumber =
   TStringConstantValueNumber(IRFunction irFunc, IRType type, string value) {
     stringConstantValueNumber(_, irFunc, type, value)
   } or
-  TFieldAddressValueNumber(IRFunction irFunc, Field field, TValueNumber objectAddress) {
+  TFieldAddressValueNumber(IRFunction irFunc, Language::Field field, TValueNumber objectAddress) {
     fieldAddressValueNumber(_, irFunc, field, objectAddress)
   } or
   TBinaryValueNumber(
@@ -33,7 +32,8 @@ newtype TValueNumber =
     unaryValueNumber(_, irFunc, opcode, operand)
   } or
   TInheritanceConversionValueNumber(
-    IRFunction irFunc, Opcode opcode, Class baseClass, Class derivedClass, TValueNumber operand
+    IRFunction irFunc, Opcode opcode, Language::Class baseClass, Language::Class derivedClass,
+    TValueNumber operand
   ) {
     inheritanceConversionValueNumber(_, irFunc, opcode, baseClass, derivedClass, operand)
   } or
@@ -136,7 +136,7 @@ private predicate initializeThisValueNumber(InitializeThisInstruction instr, IRF
   instr.getEnclosingIRFunction() = irFunc
 }
 
-predicate constantValueNumber(
+private predicate constantValueNumber(
   ConstantInstruction instr, IRFunction irFunc, IRType type, string value
 ) {
   instr.getEnclosingIRFunction() = irFunc and

cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/IRConstruction.qll

@@ -102,6 +102,19 @@ private module Cached {
     result = getMemoryOperandDefinition(instr, _, _)
   }
 
+  /**
+   * Gets a non-phi instruction that defines an operand of `instr` but only if
+   * both `instr` and the result have neighbor on the other side of the edge
+   * between them. This is a necessary condition for being in a cycle, and it
+   * removes about two thirds of the tuples that would otherwise be in this
+   * predicate.
+   */
+  private Instruction getNonPhiOperandDefOfIntermediate(Instruction instr) {
+    result = getNonPhiOperandDef(instr) and
+    exists(getNonPhiOperandDef(result)) and
+    instr = getNonPhiOperandDef(_)
+  }
+
   /**
    * Holds if `instr` is part of a cycle in the operand graph that doesn't go
    * through a phi instruction and therefore should be impossible.
@@ -115,7 +128,7 @@ private module Cached {
   cached
   predicate isInCycle(Instruction instr) {
     instr instanceof Instruction and
-    getNonPhiOperandDef+(instr) = instr
+    getNonPhiOperandDefOfIntermediate+(instr) = instr
   }
 
   cached

cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll

@@ -655,6 +655,11 @@ class TranslatedSwitchStmt extends TranslatedStmt {
       kind = getCaseEdge(switchCase) and
       result = getTranslatedStmt(switchCase).getFirstInstruction()
     )
+    or
+    not stmt.hasDefaultCase() and
+    tag = SwitchBranchTag() and
+    kind instanceof DefaultEdge and
+    result = getParent().getChildSuccessor(this)
   }
 
   override Instruction getChildSuccessor(TranslatedElement child) {

cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll

@@ -266,6 +266,16 @@ module InstructionSanity {
       funcText = Language::getIdentityString(func.getFunction())
     )
   }
+
+  query predicate switchInstructionWithoutDefaultEdge(
+    SwitchInstruction switchInstr, string message, IRFunction func, string funcText
+  ) {
+    not exists(switchInstr.getDefaultSuccessor()) and
+    message =
+      "SwitchInstruction " + switchInstr.toString() + " without a DefaultEdge in function '$@'." and
+    func = switchInstr.getEnclosingIRFunction() and
+    funcText = Language::getIdentityString(func.getFunction())
+  }
 }
 
 /**

cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/gvn/ValueNumbering.qll

@@ -27,19 +27,19 @@ class ValueNumber extends TValueNumber {
   final Language::Location getLocation() {
     if
       exists(Instruction i |
-        i = getAnInstruction() and not i.getLocation() instanceof UnknownLocation
+        i = getAnInstruction() and not i.getLocation() instanceof Language::UnknownLocation
       )
     then
       result =
         min(Language::Location l |
-          l = getAnInstruction().getLocation() and not l instanceof UnknownLocation
+          l = getAnInstruction().getLocation() and not l instanceof Language::UnknownLocation
         |
           l
           order by
             l.getFile().getAbsolutePath(), l.getStartLine(), l.getStartColumn(), l.getEndLine(),
             l.getEndColumn()
         )
-    else result instanceof UnknownDefaultLocation
+    else result instanceof Language::UnknownDefaultLocation
   }
 
   /**

cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingImports.qll

@@ -1,4 +1,3 @@
 import semmle.code.cpp.ir.implementation.aliased_ssa.IR
 import semmle.code.cpp.ir.internal.Overlap
 import semmle.code.cpp.ir.internal.IRCppLanguage as Language
-import semmle.code.cpp.Location

cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingInternal.qll

@@ -1,5 +1,4 @@
 private import ValueNumberingImports
-private import cpp
 
 newtype TValueNumber =
   TVariableAddressValueNumber(IRFunction irFunc, Language::AST ast) {
@@ -15,7 +14,7 @@ newtype TValueNumber =
   TStringConstantValueNumber(IRFunction irFunc, IRType type, string value) {
     stringConstantValueNumber(_, irFunc, type, value)
   } or
-  TFieldAddressValueNumber(IRFunction irFunc, Field field, TValueNumber objectAddress) {
+  TFieldAddressValueNumber(IRFunction irFunc, Language::Field field, TValueNumber objectAddress) {
     fieldAddressValueNumber(_, irFunc, field, objectAddress)
   } or
   TBinaryValueNumber(
@@ -33,7 +32,8 @@ newtype TValueNumber =
     unaryValueNumber(_, irFunc, opcode, operand)
   } or
   TInheritanceConversionValueNumber(
-    IRFunction irFunc, Opcode opcode, Class baseClass, Class derivedClass, TValueNumber operand
+    IRFunction irFunc, Opcode opcode, Language::Class baseClass, Language::Class derivedClass,
+    TValueNumber operand
   ) {
     inheritanceConversionValueNumber(_, irFunc, opcode, baseClass, derivedClass, operand)
   } or
@@ -136,7 +136,7 @@ private predicate initializeThisValueNumber(InitializeThisInstruction instr, IRF
   instr.getEnclosingIRFunction() = irFunc
 }
 
-predicate constantValueNumber(
+private predicate constantValueNumber(
   ConstantInstruction instr, IRFunction irFunc, IRType type, string value
 ) {
   instr.getEnclosingIRFunction() = irFunc and

cpp/ql/src/semmle/code/cpp/ir/internal/IRCppLanguage.qll

@@ -13,6 +13,10 @@ class Function = Cpp::Function;
 
 class Location = Cpp::Location;
 
+class UnknownLocation = Cpp::UnknownLocation;
+
+class UnknownDefaultLocation = Cpp::UnknownDefaultLocation;
+
 class File = Cpp::File;
 
 class AST = Cpp::Locatable;

cpp/ql/src/semmle/code/cpp/models/implementations/Pure.qll

@@ -80,7 +80,7 @@ class PureStrFunction extends AliasFunction, ArrayFunction, TaintFunction, SideE
 
   override predicate parameterIsAlwaysReturned(int i) { none() }
 
-  override predicate hasOnlySpecificReadSideEffects() { none() }
+  override predicate hasOnlySpecificReadSideEffects() { any() }
 
   override predicate hasOnlySpecificWriteSideEffects() { any() }
 

cpp/ql/src/semmle/code/cpp/models/interfaces/SideEffect.qll

@@ -18,14 +18,18 @@ abstract class SideEffectFunction extends Function {
   /**
    * Holds if the function never reads from memory that was defined before entry to the function.
    * This memory could be from global variables, or from other memory that was reachable from a
-   * pointer that was passed into the function.
+   * pointer that was passed into the function. Input side-effects, and reads from memory that
+   * cannot be visible to the caller (for example a buffer inside an I/O library) are not modeled
+   * here.
    */
   abstract predicate hasOnlySpecificReadSideEffects();
 
   /**
    * Holds if the function never writes to memory that remains allocated after the function
    * returns. This memory could be from global variables, or from other memory that was reachable
-   * from a pointer that was passed into the function.
+   * from a pointer that was passed into the function. Output side-effects, and writes to memory
+   * that cannot be visible to the caller (for example a buffer inside an I/O library) are not
+   * modeled here.
    */
   abstract predicate hasOnlySpecificWriteSideEffects();
 
@@ -43,7 +47,6 @@ abstract class SideEffectFunction extends Function {
    */
   predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) { none() }
 
-  // TODO: name?
   /**
    * Gets the index of the parameter that indicates the size of the buffer pointed to by the
    * parameter at index `i`.

cpp/ql/src/semmle/code/cpp/security/TaintTracking.qll

@@ -2,4 +2,4 @@
  * Support for tracking tainted data through the program.
  */
 
-import TaintTrackingImpl
+import semmle.code.cpp.ir.dataflow.DefaultTaintTracking

cpp/ql/src/semmle/code/cpp/valuenumbering/GlobalValueNumbering.qll

@@ -1 +1 @@
-import GlobalValueNumberingImpl
+import semmle.code.cpp.ir.internal.ASTValueNumbering

cpp/ql/test/experimental/README.md

@@ -0,0 +1 @@
+This directory contains tests for [experimental](../../../../docs/experimental.md) CodeQL queries and libraries.

cpp/ql/test/library-tests/dataflow/security-taint/tainted.ql

@@ -1,4 +1,4 @@
-import semmle.code.cpp.security.TaintTracking
+import semmle.code.cpp.security.TaintTrackingImpl
 
 from Expr source, Element tainted, string globalVar
 where

cpp/ql/test/library-tests/dataflow/security-taint/tainted_diff.ql

@@ -1,4 +1,4 @@
-import semmle.code.cpp.security.TaintTracking as AST
+import semmle.code.cpp.security.TaintTrackingImpl as AST
 import semmle.code.cpp.ir.dataflow.DefaultTaintTracking as IR
 import cpp
 

cpp/ql/test/library-tests/ir/ir/PrintAST.expected

@@ -8070,6 +8070,239 @@ ir.cpp:
 # 1170|               Type = [ArrayType] const char[4]
 # 1170|               Value = [StringLiteral] "foo"
 # 1170|               ValueCategory = lvalue
+# 1173| [TopLevelFunction] void switch1Case(int)
+# 1173|   params: 
+# 1173|     0: [Parameter] x
+# 1173|         Type = [IntType] int
+# 1173|   body: [Block] { ... }
+# 1174|     0: [DeclStmt] declaration
+# 1174|       0: [VariableDeclarationEntry] definition of y
+# 1174|           Type = [IntType] int
+# 1174|         init: [Initializer] initializer for y
+# 1174|           expr: [Literal] 0
+# 1174|               Type = [IntType] int
+# 1174|               Value = [Literal] 0
+# 1174|               ValueCategory = prvalue
+# 1175|     1: [SwitchStmt] switch (...) ... 
+# 1175|       0: [VariableAccess] x
+# 1175|           Type = [IntType] int
+# 1175|           ValueCategory = prvalue(load)
+# 1175|       1: [Block] { ... }
+# 1176|         0: [SwitchCase] case ...:
+# 1176|           0: [Literal] 1
+# 1176|               Type = [IntType] int
+# 1176|               Value = [Literal] 1
+# 1176|               ValueCategory = prvalue
+# 1177|         1: [ExprStmt] ExprStmt
+# 1177|           0: [AssignExpr] ... = ...
+# 1177|               Type = [IntType] int
+# 1177|               ValueCategory = lvalue
+# 1177|             0: [VariableAccess] y
+# 1177|                 Type = [IntType] int
+# 1177|                 ValueCategory = lvalue
+# 1177|             1: [Literal] 2
+# 1177|                 Type = [IntType] int
+# 1177|                 Value = [Literal] 2
+# 1177|                 ValueCategory = prvalue
+# 1179|     2: [DeclStmt] declaration
+# 1179|       0: [VariableDeclarationEntry] definition of z
+# 1179|           Type = [IntType] int
+# 1179|         init: [Initializer] initializer for z
+# 1179|           expr: [VariableAccess] y
+# 1179|               Type = [IntType] int
+# 1179|               ValueCategory = prvalue(load)
+# 1180|     3: [ReturnStmt] return ...
+# 1182| [TopLevelFunction] void switch2Case_fallthrough(int)
+# 1182|   params: 
+# 1182|     0: [Parameter] x
+# 1182|         Type = [IntType] int
+# 1182|   body: [Block] { ... }
+# 1183|     0: [DeclStmt] declaration
+# 1183|       0: [VariableDeclarationEntry] definition of y
+# 1183|           Type = [IntType] int
+# 1183|         init: [Initializer] initializer for y
+# 1183|           expr: [Literal] 0
+# 1183|               Type = [IntType] int
+# 1183|               Value = [Literal] 0
+# 1183|               ValueCategory = prvalue
+# 1184|     1: [SwitchStmt] switch (...) ... 
+# 1184|       0: [VariableAccess] x
+# 1184|           Type = [IntType] int
+# 1184|           ValueCategory = prvalue(load)
+# 1184|       1: [Block] { ... }
+# 1185|         0: [SwitchCase] case ...:
+# 1185|           0: [Literal] 1
+# 1185|               Type = [IntType] int
+# 1185|               Value = [Literal] 1
+# 1185|               ValueCategory = prvalue
+# 1186|         1: [ExprStmt] ExprStmt
+# 1186|           0: [AssignExpr] ... = ...
+# 1186|               Type = [IntType] int
+# 1186|               ValueCategory = lvalue
+# 1186|             0: [VariableAccess] y
+# 1186|                 Type = [IntType] int
+# 1186|                 ValueCategory = lvalue
+# 1186|             1: [Literal] 2
+# 1186|                 Type = [IntType] int
+# 1186|                 Value = [Literal] 2
+# 1186|                 ValueCategory = prvalue
+# 1187|         2: [SwitchCase] case ...:
+# 1187|           0: [Literal] 2
+# 1187|               Type = [IntType] int
+# 1187|               Value = [Literal] 2
+# 1187|               ValueCategory = prvalue
+# 1188|         3: [ExprStmt] ExprStmt
+# 1188|           0: [AssignExpr] ... = ...
+# 1188|               Type = [IntType] int
+# 1188|               ValueCategory = lvalue
+# 1188|             0: [VariableAccess] y
+# 1188|                 Type = [IntType] int
+# 1188|                 ValueCategory = lvalue
+# 1188|             1: [Literal] 3
+# 1188|                 Type = [IntType] int
+# 1188|                 Value = [Literal] 3
+# 1188|                 ValueCategory = prvalue
+# 1190|     2: [DeclStmt] declaration
+# 1190|       0: [VariableDeclarationEntry] definition of z
+# 1190|           Type = [IntType] int
+# 1190|         init: [Initializer] initializer for z
+# 1190|           expr: [VariableAccess] y
+# 1190|               Type = [IntType] int
+# 1190|               ValueCategory = prvalue(load)
+# 1191|     3: [ReturnStmt] return ...
+# 1193| [TopLevelFunction] void switch2Case(int)
+# 1193|   params: 
+# 1193|     0: [Parameter] x
+# 1193|         Type = [IntType] int
+# 1193|   body: [Block] { ... }
+# 1194|     0: [DeclStmt] declaration
+# 1194|       0: [VariableDeclarationEntry] definition of y
+# 1194|           Type = [IntType] int
+# 1194|         init: [Initializer] initializer for y
+# 1194|           expr: [Literal] 0
+# 1194|               Type = [IntType] int
+# 1194|               Value = [Literal] 0
+# 1194|               ValueCategory = prvalue
+# 1195|     1: [SwitchStmt] switch (...) ... 
+# 1195|       0: [VariableAccess] x
+# 1195|           Type = [IntType] int
+# 1195|           ValueCategory = prvalue(load)
+# 1195|       1: [Block] { ... }
+# 1196|         0: [SwitchCase] case ...:
+# 1196|           0: [Literal] 1
+# 1196|               Type = [IntType] int
+# 1196|               Value = [Literal] 1
+# 1196|               ValueCategory = prvalue
+# 1197|         1: [ExprStmt] ExprStmt
+# 1197|           0: [AssignExpr] ... = ...
+# 1197|               Type = [IntType] int
+# 1197|               ValueCategory = lvalue
+# 1197|             0: [VariableAccess] y
+# 1197|                 Type = [IntType] int
+# 1197|                 ValueCategory = lvalue
+# 1197|             1: [Literal] 2
+# 1197|                 Type = [IntType] int
+# 1197|                 Value = [Literal] 2
+# 1197|                 ValueCategory = prvalue
+# 1198|         2: [BreakStmt] break;
+# 1199|         3: [SwitchCase] case ...:
+# 1199|           0: [Literal] 2
+# 1199|               Type = [IntType] int
+# 1199|               Value = [Literal] 2
+# 1199|               ValueCategory = prvalue
+# 1200|         4: [ExprStmt] ExprStmt
+# 1200|           0: [AssignExpr] ... = ...
+# 1200|               Type = [IntType] int
+# 1200|               ValueCategory = lvalue
+# 1200|             0: [VariableAccess] y
+# 1200|                 Type = [IntType] int
+# 1200|                 ValueCategory = lvalue
+# 1200|             1: [Literal] 3
+# 1200|                 Type = [IntType] int
+# 1200|                 Value = [Literal] 3
+# 1200|                 ValueCategory = prvalue
+# 1201|     2: [LabelStmt] label ...:
+# 1202|     3: [DeclStmt] declaration
+# 1202|       0: [VariableDeclarationEntry] definition of z
+# 1202|           Type = [IntType] int
+# 1202|         init: [Initializer] initializer for z
+# 1202|           expr: [VariableAccess] y
+# 1202|               Type = [IntType] int
+# 1202|               ValueCategory = prvalue(load)
+# 1203|     4: [ReturnStmt] return ...
+# 1205| [TopLevelFunction] void switch2Case_default(int)
+# 1205|   params: 
+# 1205|     0: [Parameter] x
+# 1205|         Type = [IntType] int
+# 1205|   body: [Block] { ... }
+# 1206|     0: [DeclStmt] declaration
+# 1206|       0: [VariableDeclarationEntry] definition of y
+# 1206|           Type = [IntType] int
+# 1206|         init: [Initializer] initializer for y
+# 1206|           expr: [Literal] 0
+# 1206|               Type = [IntType] int
+# 1206|               Value = [Literal] 0
+# 1206|               ValueCategory = prvalue
+# 1207|     1: [SwitchStmt] switch (...) ... 
+# 1207|       0: [VariableAccess] x
+# 1207|           Type = [IntType] int
+# 1207|           ValueCategory = prvalue(load)
+# 1207|       1: [Block] { ... }
+# 1208|         0: [SwitchCase] case ...:
+# 1208|           0: [Literal] 1
+# 1208|               Type = [IntType] int
+# 1208|               Value = [Literal] 1
+# 1208|               ValueCategory = prvalue
+# 1209|         1: [ExprStmt] ExprStmt
+# 1209|           0: [AssignExpr] ... = ...
+# 1209|               Type = [IntType] int
+# 1209|               ValueCategory = lvalue
+# 1209|             0: [VariableAccess] y
+# 1209|                 Type = [IntType] int
+# 1209|                 ValueCategory = lvalue
+# 1209|             1: [Literal] 2
+# 1209|                 Type = [IntType] int
+# 1209|                 Value = [Literal] 2
+# 1209|                 ValueCategory = prvalue
+# 1210|         2: [BreakStmt] break;
+# 1212|         3: [SwitchCase] case ...:
+# 1212|           0: [Literal] 2
+# 1212|               Type = [IntType] int
+# 1212|               Value = [Literal] 2
+# 1212|               ValueCategory = prvalue
+# 1213|         4: [ExprStmt] ExprStmt
+# 1213|           0: [AssignExpr] ... = ...
+# 1213|               Type = [IntType] int
+# 1213|               ValueCategory = lvalue
+# 1213|             0: [VariableAccess] y
+# 1213|                 Type = [IntType] int
+# 1213|                 ValueCategory = lvalue
+# 1213|             1: [Literal] 3
+# 1213|                 Type = [IntType] int
+# 1213|                 Value = [Literal] 3
+# 1213|                 ValueCategory = prvalue
+# 1214|         5: [BreakStmt] break;
+# 1216|         6: [SwitchCase] default: 
+# 1217|         7: [ExprStmt] ExprStmt
+# 1217|           0: [AssignExpr] ... = ...
+# 1217|               Type = [IntType] int
+# 1217|               ValueCategory = lvalue
+# 1217|             0: [VariableAccess] y
+# 1217|                 Type = [IntType] int
+# 1217|                 ValueCategory = lvalue
+# 1217|             1: [Literal] 4
+# 1217|                 Type = [IntType] int
+# 1217|                 Value = [Literal] 4
+# 1217|                 ValueCategory = prvalue
+# 1218|     2: [LabelStmt] label ...:
+# 1219|     3: [DeclStmt] declaration
+# 1219|       0: [VariableDeclarationEntry] definition of z
+# 1219|           Type = [IntType] int
+# 1219|         init: [Initializer] initializer for z
+# 1219|           expr: [VariableAccess] y
+# 1219|               Type = [IntType] int
+# 1219|               ValueCategory = prvalue(load)
+# 1220|     4: [ReturnStmt] return ...
 perf-regression.cpp:
 #    4| [CopyAssignmentOperator] Big& Big::operator=(Big const&)
 #    4|   params: 

cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity.expected

@@ -19,6 +19,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity_unsound.expected

@@ -19,6 +19,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/ir/ir/ir.cpp

@@ -1170,4 +1170,53 @@ String ReturnObjectImpl() {
   return String("foo");
 }
 
+void switch1Case(int x) {
+    int y = 0;
+    switch(x) {
+        case 1:
+        y = 2;
+    }
+    int z = y;
+}
+
+void switch2Case_fallthrough(int x) {
+    int y = 0;
+    switch(x) {
+        case 1:
+        y = 2;
+        case 2:
+        y = 3;
+    }
+    int z = y;
+}
+
+void switch2Case(int x) {
+    int y = 0;
+    switch(x) {
+        case 1:
+        y = 2;
+        break;
+        case 2:
+        y = 3;
+    }
+    int z = y;
+}
+
+void switch2Case_default(int x) {
+    int y = 0;
+    switch(x) {
+        case 1:
+            y = 2;
+            break;
+
+        case 2:
+            y = 3;
+            break;
+
+        default:
+            y = 4;
+    }
+    int z = y;
+}
+
 // semmle-extractor-options: -std=c++17 --clang

cpp/ql/test/library-tests/ir/ir/raw_ir.expected

@@ -6052,6 +6052,182 @@ ir.cpp:
 # 1169|     v1169_8(void)           = AliasedUse                      : ~mu1169_4
 # 1169|     v1169_9(void)           = ExitFunction                    : 
 
+# 1173| void switch1Case(int)
+# 1173|   Block 0
+# 1173|     v1173_1(void)       = EnterFunction          : 
+# 1173|     mu1173_2(unknown)   = AliasedDefinition      : 
+# 1173|     mu1173_3(unknown)   = InitializeNonLocal     : 
+# 1173|     mu1173_4(unknown)   = UnmodeledDefinition    : 
+# 1173|     r1173_5(glval<int>) = VariableAddress[x]     : 
+# 1173|     mu1173_6(int)       = InitializeParameter[x] : &:r1173_5
+# 1174|     r1174_1(glval<int>) = VariableAddress[y]     : 
+# 1174|     r1174_2(int)        = Constant[0]            : 
+# 1174|     mu1174_3(int)       = Store                  : &:r1174_1, r1174_2
+# 1175|     r1175_1(glval<int>) = VariableAddress[x]     : 
+# 1175|     r1175_2(int)        = Load                   : &:r1175_1, ~mu1173_4
+# 1175|     v1175_3(void)       = Switch                 : r1175_2
+#-----|   Case[1] -> Block 1
+#-----|   Default -> Block 2
+
+# 1176|   Block 1
+# 1176|     v1176_1(void)       = NoOp               : 
+# 1177|     r1177_1(int)        = Constant[2]        : 
+# 1177|     r1177_2(glval<int>) = VariableAddress[y] : 
+# 1177|     mu1177_3(int)       = Store              : &:r1177_2, r1177_1
+#-----|   Goto -> Block 2
+
+# 1179|   Block 2
+# 1179|     r1179_1(glval<int>) = VariableAddress[z] : 
+# 1179|     r1179_2(glval<int>) = VariableAddress[y] : 
+# 1179|     r1179_3(int)        = Load               : &:r1179_2, ~mu1173_4
+# 1179|     mu1179_4(int)       = Store              : &:r1179_1, r1179_3
+# 1180|     v1180_1(void)       = NoOp               : 
+# 1173|     v1173_7(void)       = ReturnVoid         : 
+# 1173|     v1173_8(void)       = UnmodeledUse       : mu*
+# 1173|     v1173_9(void)       = AliasedUse         : ~mu1173_4
+# 1173|     v1173_10(void)      = ExitFunction       : 
+
+# 1182| void switch2Case_fallthrough(int)
+# 1182|   Block 0
+# 1182|     v1182_1(void)       = EnterFunction          : 
+# 1182|     mu1182_2(unknown)   = AliasedDefinition      : 
+# 1182|     mu1182_3(unknown)   = InitializeNonLocal     : 
+# 1182|     mu1182_4(unknown)   = UnmodeledDefinition    : 
+# 1182|     r1182_5(glval<int>) = VariableAddress[x]     : 
+# 1182|     mu1182_6(int)       = InitializeParameter[x] : &:r1182_5
+# 1183|     r1183_1(glval<int>) = VariableAddress[y]     : 
+# 1183|     r1183_2(int)        = Constant[0]            : 
+# 1183|     mu1183_3(int)       = Store                  : &:r1183_1, r1183_2
+# 1184|     r1184_1(glval<int>) = VariableAddress[x]     : 
+# 1184|     r1184_2(int)        = Load                   : &:r1184_1, ~mu1182_4
+# 1184|     v1184_3(void)       = Switch                 : r1184_2
+#-----|   Case[1] -> Block 1
+#-----|   Case[2] -> Block 2
+#-----|   Default -> Block 3
+
+# 1185|   Block 1
+# 1185|     v1185_1(void)       = NoOp               : 
+# 1186|     r1186_1(int)        = Constant[2]        : 
+# 1186|     r1186_2(glval<int>) = VariableAddress[y] : 
+# 1186|     mu1186_3(int)       = Store              : &:r1186_2, r1186_1
+#-----|   Goto -> Block 2
+
+# 1187|   Block 2
+# 1187|     v1187_1(void)       = NoOp               : 
+# 1188|     r1188_1(int)        = Constant[3]        : 
+# 1188|     r1188_2(glval<int>) = VariableAddress[y] : 
+# 1188|     mu1188_3(int)       = Store              : &:r1188_2, r1188_1
+#-----|   Goto -> Block 3
+
+# 1190|   Block 3
+# 1190|     r1190_1(glval<int>) = VariableAddress[z] : 
+# 1190|     r1190_2(glval<int>) = VariableAddress[y] : 
+# 1190|     r1190_3(int)        = Load               : &:r1190_2, ~mu1182_4
+# 1190|     mu1190_4(int)       = Store              : &:r1190_1, r1190_3
+# 1191|     v1191_1(void)       = NoOp               : 
+# 1182|     v1182_7(void)       = ReturnVoid         : 
+# 1182|     v1182_8(void)       = UnmodeledUse       : mu*
+# 1182|     v1182_9(void)       = AliasedUse         : ~mu1182_4
+# 1182|     v1182_10(void)      = ExitFunction       : 
+
+# 1193| void switch2Case(int)
+# 1193|   Block 0
+# 1193|     v1193_1(void)       = EnterFunction          : 
+# 1193|     mu1193_2(unknown)   = AliasedDefinition      : 
+# 1193|     mu1193_3(unknown)   = InitializeNonLocal     : 
+# 1193|     mu1193_4(unknown)   = UnmodeledDefinition    : 
+# 1193|     r1193_5(glval<int>) = VariableAddress[x]     : 
+# 1193|     mu1193_6(int)       = InitializeParameter[x] : &:r1193_5
+# 1194|     r1194_1(glval<int>) = VariableAddress[y]     : 
+# 1194|     r1194_2(int)        = Constant[0]            : 
+# 1194|     mu1194_3(int)       = Store                  : &:r1194_1, r1194_2
+# 1195|     r1195_1(glval<int>) = VariableAddress[x]     : 
+# 1195|     r1195_2(int)        = Load                   : &:r1195_1, ~mu1193_4
+# 1195|     v1195_3(void)       = Switch                 : r1195_2
+#-----|   Case[1] -> Block 1
+#-----|   Case[2] -> Block 2
+#-----|   Default -> Block 3
+
+# 1196|   Block 1
+# 1196|     v1196_1(void)       = NoOp               : 
+# 1197|     r1197_1(int)        = Constant[2]        : 
+# 1197|     r1197_2(glval<int>) = VariableAddress[y] : 
+# 1197|     mu1197_3(int)       = Store              : &:r1197_2, r1197_1
+# 1198|     v1198_1(void)       = NoOp               : 
+#-----|   Goto -> Block 3
+
+# 1199|   Block 2
+# 1199|     v1199_1(void)       = NoOp               : 
+# 1200|     r1200_1(int)        = Constant[3]        : 
+# 1200|     r1200_2(glval<int>) = VariableAddress[y] : 
+# 1200|     mu1200_3(int)       = Store              : &:r1200_2, r1200_1
+#-----|   Goto -> Block 3
+
+# 1201|   Block 3
+# 1201|     v1201_1(void)       = NoOp               : 
+# 1202|     r1202_1(glval<int>) = VariableAddress[z] : 
+# 1202|     r1202_2(glval<int>) = VariableAddress[y] : 
+# 1202|     r1202_3(int)        = Load               : &:r1202_2, ~mu1193_4
+# 1202|     mu1202_4(int)       = Store              : &:r1202_1, r1202_3
+# 1203|     v1203_1(void)       = NoOp               : 
+# 1193|     v1193_7(void)       = ReturnVoid         : 
+# 1193|     v1193_8(void)       = UnmodeledUse       : mu*
+# 1193|     v1193_9(void)       = AliasedUse         : ~mu1193_4
+# 1193|     v1193_10(void)      = ExitFunction       : 
+
+# 1205| void switch2Case_default(int)
+# 1205|   Block 0
+# 1205|     v1205_1(void)       = EnterFunction          : 
+# 1205|     mu1205_2(unknown)   = AliasedDefinition      : 
+# 1205|     mu1205_3(unknown)   = InitializeNonLocal     : 
+# 1205|     mu1205_4(unknown)   = UnmodeledDefinition    : 
+# 1205|     r1205_5(glval<int>) = VariableAddress[x]     : 
+# 1205|     mu1205_6(int)       = InitializeParameter[x] : &:r1205_5
+# 1206|     r1206_1(glval<int>) = VariableAddress[y]     : 
+# 1206|     r1206_2(int)        = Constant[0]            : 
+# 1206|     mu1206_3(int)       = Store                  : &:r1206_1, r1206_2
+# 1207|     r1207_1(glval<int>) = VariableAddress[x]     : 
+# 1207|     r1207_2(int)        = Load                   : &:r1207_1, ~mu1205_4
+# 1207|     v1207_3(void)       = Switch                 : r1207_2
+#-----|   Case[1] -> Block 1
+#-----|   Case[2] -> Block 2
+#-----|   Default -> Block 3
+
+# 1208|   Block 1
+# 1208|     v1208_1(void)       = NoOp               : 
+# 1209|     r1209_1(int)        = Constant[2]        : 
+# 1209|     r1209_2(glval<int>) = VariableAddress[y] : 
+# 1209|     mu1209_3(int)       = Store              : &:r1209_2, r1209_1
+# 1210|     v1210_1(void)       = NoOp               : 
+#-----|   Goto -> Block 4
+
+# 1212|   Block 2
+# 1212|     v1212_1(void)       = NoOp               : 
+# 1213|     r1213_1(int)        = Constant[3]        : 
+# 1213|     r1213_2(glval<int>) = VariableAddress[y] : 
+# 1213|     mu1213_3(int)       = Store              : &:r1213_2, r1213_1
+# 1214|     v1214_1(void)       = NoOp               : 
+#-----|   Goto -> Block 4
+
+# 1216|   Block 3
+# 1216|     v1216_1(void)       = NoOp               : 
+# 1217|     r1217_1(int)        = Constant[4]        : 
+# 1217|     r1217_2(glval<int>) = VariableAddress[y] : 
+# 1217|     mu1217_3(int)       = Store              : &:r1217_2, r1217_1
+#-----|   Goto -> Block 4
+
+# 1218|   Block 4
+# 1218|     v1218_1(void)       = NoOp               : 
+# 1219|     r1219_1(glval<int>) = VariableAddress[z] : 
+# 1219|     r1219_2(glval<int>) = VariableAddress[y] : 
+# 1219|     r1219_3(int)        = Load               : &:r1219_2, ~mu1205_4
+# 1219|     mu1219_4(int)       = Store              : &:r1219_1, r1219_3
+# 1220|     v1220_1(void)       = NoOp               : 
+# 1205|     v1205_7(void)       = ReturnVoid         : 
+# 1205|     v1205_8(void)       = UnmodeledUse       : mu*
+# 1205|     v1205_9(void)       = AliasedUse         : ~mu1205_4
+# 1205|     v1205_10(void)      = ExitFunction       : 
+
 perf-regression.cpp:
 #    6| void Big::Big()
 #    6|   Block 0

cpp/ql/test/library-tests/ir/ir/raw_sanity.expected

@@ -19,6 +19,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected

@@ -19,6 +19,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity_unsound.expected

@@ -19,6 +19,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir.expected

@@ -886,27 +886,25 @@ ssa.cpp:
 #  199|     r199_7(char *)         = Load                        : &:r199_6, m198_11
 #  199|     r199_8(char *)         = Convert                     : r199_7
 #  199|     r199_9(int)            = Call                        : func:r199_2, 0:r199_5, 1:r199_8
-#  199|     v199_10(void)          = ^CallReadSideEffect         : ~m198_4
+#  199|     v199_10(void)          = ^BufferReadSideEffect[0]    : &:r199_5, ~m198_9
-#  199|     v199_11(void)          = ^BufferReadSideEffect[0]    : &:r199_5, ~m198_9
+#  199|     v199_11(void)          = ^BufferReadSideEffect[1]    : &:r199_8, ~m198_13
-#  199|     v199_12(void)          = ^BufferReadSideEffect[1]    : &:r199_8, ~m198_13
+#  199|     m199_12(int)           = Store                       : &:r199_1, r199_9
-#  199|     m199_13(int)           = Store                       : &:r199_1, r199_9
 #  200|     r200_1(glval<unknown>) = FunctionAddress[strlen]     : 
 #  200|     r200_2(glval<char *>)  = VariableAddress[str1]       : 
 #  200|     r200_3(char *)         = Load                        : &:r200_2, m198_7
 #  200|     r200_4(char *)         = Convert                     : r200_3
 #  200|     r200_5(int)            = Call                        : func:r200_1, 0:r200_4
-#  200|     v200_6(void)           = ^CallReadSideEffect         : ~m198_4
+#  200|     v200_6(void)           = ^BufferReadSideEffect[0]    : &:r200_4, ~m198_9
-#  200|     v200_7(void)           = ^BufferReadSideEffect[0]    : &:r200_4, ~m198_9
+#  200|     r200_7(glval<int>)     = VariableAddress[ret]        : 
-#  200|     r200_8(glval<int>)     = VariableAddress[ret]        : 
+#  200|     r200_8(int)            = Load                        : &:r200_7, m199_12
-#  200|     r200_9(int)            = Load                        : &:r200_8, m199_13
+#  200|     r200_9(int)            = Add                         : r200_8, r200_5
-#  200|     r200_10(int)           = Add                         : r200_9, r200_5
+#  200|     m200_10(int)           = Store                       : &:r200_7, r200_9
-#  200|     m200_11(int)           = Store                       : &:r200_8, r200_10
 #  201|     r201_1(glval<unknown>) = FunctionAddress[abs]        : 
 #  201|     r201_2(glval<int>)     = VariableAddress[x]          : 
 #  201|     r201_3(int)            = Load                        : &:r201_2, m198_15
 #  201|     r201_4(int)            = Call                        : func:r201_1, 0:r201_3
 #  201|     r201_5(glval<int>)     = VariableAddress[ret]        : 
-#  201|     r201_6(int)            = Load                        : &:r201_5, m200_11
+#  201|     r201_6(int)            = Load                        : &:r201_5, m200_10
 #  201|     r201_7(int)            = Add                         : r201_6, r201_4
 #  201|     m201_8(int)            = Store                       : &:r201_5, r201_7
 #  202|     r202_1(glval<int>)     = VariableAddress[#return]    : 

cpp/ql/test/library-tests/ir/ssa/aliased_ssa_ir_unsound.expected

@@ -883,27 +883,25 @@ ssa.cpp:
 #  199|     r199_7(char *)         = Load                        : &:r199_6, m198_11
 #  199|     r199_8(char *)         = Convert                     : r199_7
 #  199|     r199_9(int)            = Call                        : func:r199_2, 0:r199_5, 1:r199_8
-#  199|     v199_10(void)          = ^CallReadSideEffect         : ~m198_4
+#  199|     v199_10(void)          = ^BufferReadSideEffect[0]    : &:r199_5, ~m198_9
-#  199|     v199_11(void)          = ^BufferReadSideEffect[0]    : &:r199_5, ~m198_9
+#  199|     v199_11(void)          = ^BufferReadSideEffect[1]    : &:r199_8, ~m198_13
-#  199|     v199_12(void)          = ^BufferReadSideEffect[1]    : &:r199_8, ~m198_13
+#  199|     m199_12(int)           = Store                       : &:r199_1, r199_9
-#  199|     m199_13(int)           = Store                       : &:r199_1, r199_9
 #  200|     r200_1(glval<unknown>) = FunctionAddress[strlen]     : 
 #  200|     r200_2(glval<char *>)  = VariableAddress[str1]       : 
 #  200|     r200_3(char *)         = Load                        : &:r200_2, m198_7
 #  200|     r200_4(char *)         = Convert                     : r200_3
 #  200|     r200_5(int)            = Call                        : func:r200_1, 0:r200_4
-#  200|     v200_6(void)           = ^CallReadSideEffect         : ~m198_4
+#  200|     v200_6(void)           = ^BufferReadSideEffect[0]    : &:r200_4, ~m198_9
-#  200|     v200_7(void)           = ^BufferReadSideEffect[0]    : &:r200_4, ~m198_9
+#  200|     r200_7(glval<int>)     = VariableAddress[ret]        : 
-#  200|     r200_8(glval<int>)     = VariableAddress[ret]        : 
+#  200|     r200_8(int)            = Load                        : &:r200_7, m199_12
-#  200|     r200_9(int)            = Load                        : &:r200_8, m199_13
+#  200|     r200_9(int)            = Add                         : r200_8, r200_5
-#  200|     r200_10(int)           = Add                         : r200_9, r200_5
+#  200|     m200_10(int)           = Store                       : &:r200_7, r200_9
-#  200|     m200_11(int)           = Store                       : &:r200_8, r200_10
 #  201|     r201_1(glval<unknown>) = FunctionAddress[abs]        : 
 #  201|     r201_2(glval<int>)     = VariableAddress[x]          : 
 #  201|     r201_3(int)            = Load                        : &:r201_2, m198_15
 #  201|     r201_4(int)            = Call                        : func:r201_1, 0:r201_3
 #  201|     r201_5(glval<int>)     = VariableAddress[ret]        : 
-#  201|     r201_6(int)            = Load                        : &:r201_5, m200_11
+#  201|     r201_6(int)            = Load                        : &:r201_5, m200_10
 #  201|     r201_7(int)            = Add                         : r201_6, r201_4
 #  201|     m201_8(int)            = Store                       : &:r201_5, r201_7
 #  202|     r202_1(glval<int>)     = VariableAddress[#return]    : 

cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity.expected

@@ -15,6 +15,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity_unsound.expected

@@ -15,6 +15,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir.expected

@@ -829,27 +829,25 @@ ssa.cpp:
 #  199|     r199_7(char *)         = Load                        : &:r199_6, m198_10
 #  199|     r199_8(char *)         = Convert                     : r199_7
 #  199|     r199_9(int)            = Call                        : func:r199_2, 0:r199_5, 1:r199_8
-#  199|     v199_10(void)          = ^CallReadSideEffect         : ~mu198_4
+#  199|     v199_10(void)          = ^BufferReadSideEffect[0]    : &:r199_5, ~mu198_4
-#  199|     v199_11(void)          = ^BufferReadSideEffect[0]    : &:r199_5, ~mu198_4
+#  199|     v199_11(void)          = ^BufferReadSideEffect[1]    : &:r199_8, ~mu198_4
-#  199|     v199_12(void)          = ^BufferReadSideEffect[1]    : &:r199_8, ~mu198_4
+#  199|     m199_12(int)           = Store                       : &:r199_1, r199_9
-#  199|     m199_13(int)           = Store                       : &:r199_1, r199_9
 #  200|     r200_1(glval<unknown>) = FunctionAddress[strlen]     : 
 #  200|     r200_2(glval<char *>)  = VariableAddress[str1]       : 
 #  200|     r200_3(char *)         = Load                        : &:r200_2, m198_6
 #  200|     r200_4(char *)         = Convert                     : r200_3
 #  200|     r200_5(int)            = Call                        : func:r200_1, 0:r200_4
-#  200|     v200_6(void)           = ^CallReadSideEffect         : ~mu198_4
+#  200|     v200_6(void)           = ^BufferReadSideEffect[0]    : &:r200_4, ~mu198_4
-#  200|     v200_7(void)           = ^BufferReadSideEffect[0]    : &:r200_4, ~mu198_4
+#  200|     r200_7(glval<int>)     = VariableAddress[ret]        : 
-#  200|     r200_8(glval<int>)     = VariableAddress[ret]        : 
+#  200|     r200_8(int)            = Load                        : &:r200_7, m199_12
-#  200|     r200_9(int)            = Load                        : &:r200_8, m199_13
+#  200|     r200_9(int)            = Add                         : r200_8, r200_5
-#  200|     r200_10(int)           = Add                         : r200_9, r200_5
+#  200|     m200_10(int)           = Store                       : &:r200_7, r200_9
-#  200|     m200_11(int)           = Store                       : &:r200_8, r200_10
 #  201|     r201_1(glval<unknown>) = FunctionAddress[abs]        : 
 #  201|     r201_2(glval<int>)     = VariableAddress[x]          : 
 #  201|     r201_3(int)            = Load                        : &:r201_2, m198_14
 #  201|     r201_4(int)            = Call                        : func:r201_1, 0:r201_3
 #  201|     r201_5(glval<int>)     = VariableAddress[ret]        : 
-#  201|     r201_6(int)            = Load                        : &:r201_5, m200_11
+#  201|     r201_6(int)            = Load                        : &:r201_5, m200_10
 #  201|     r201_7(int)            = Add                         : r201_6, r201_4
 #  201|     m201_8(int)            = Store                       : &:r201_5, r201_7
 #  202|     r202_1(glval<int>)     = VariableAddress[#return]    : 

cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_ir_unsound.expected

@@ -829,27 +829,25 @@ ssa.cpp:
 #  199|     r199_7(char *)         = Load                        : &:r199_6, m198_10
 #  199|     r199_8(char *)         = Convert                     : r199_7
 #  199|     r199_9(int)            = Call                        : func:r199_2, 0:r199_5, 1:r199_8
-#  199|     v199_10(void)          = ^CallReadSideEffect         : ~mu198_4
+#  199|     v199_10(void)          = ^BufferReadSideEffect[0]    : &:r199_5, ~mu198_4
-#  199|     v199_11(void)          = ^BufferReadSideEffect[0]    : &:r199_5, ~mu198_4
+#  199|     v199_11(void)          = ^BufferReadSideEffect[1]    : &:r199_8, ~mu198_4
-#  199|     v199_12(void)          = ^BufferReadSideEffect[1]    : &:r199_8, ~mu198_4
+#  199|     m199_12(int)           = Store                       : &:r199_1, r199_9
-#  199|     m199_13(int)           = Store                       : &:r199_1, r199_9
 #  200|     r200_1(glval<unknown>) = FunctionAddress[strlen]     : 
 #  200|     r200_2(glval<char *>)  = VariableAddress[str1]       : 
 #  200|     r200_3(char *)         = Load                        : &:r200_2, m198_6
 #  200|     r200_4(char *)         = Convert                     : r200_3
 #  200|     r200_5(int)            = Call                        : func:r200_1, 0:r200_4
-#  200|     v200_6(void)           = ^CallReadSideEffect         : ~mu198_4
+#  200|     v200_6(void)           = ^BufferReadSideEffect[0]    : &:r200_4, ~mu198_4
-#  200|     v200_7(void)           = ^BufferReadSideEffect[0]    : &:r200_4, ~mu198_4
+#  200|     r200_7(glval<int>)     = VariableAddress[ret]        : 
-#  200|     r200_8(glval<int>)     = VariableAddress[ret]        : 
+#  200|     r200_8(int)            = Load                        : &:r200_7, m199_12
-#  200|     r200_9(int)            = Load                        : &:r200_8, m199_13
+#  200|     r200_9(int)            = Add                         : r200_8, r200_5
-#  200|     r200_10(int)           = Add                         : r200_9, r200_5
+#  200|     m200_10(int)           = Store                       : &:r200_7, r200_9
-#  200|     m200_11(int)           = Store                       : &:r200_8, r200_10
 #  201|     r201_1(glval<unknown>) = FunctionAddress[abs]        : 
 #  201|     r201_2(glval<int>)     = VariableAddress[x]          : 
 #  201|     r201_3(int)            = Load                        : &:r201_2, m198_14
 #  201|     r201_4(int)            = Call                        : func:r201_1, 0:r201_3
 #  201|     r201_5(glval<int>)     = VariableAddress[ret]        : 
-#  201|     r201_6(int)            = Load                        : &:r201_5, m200_11
+#  201|     r201_6(int)            = Load                        : &:r201_5, m200_10
 #  201|     r201_7(int)            = Add                         : r201_6, r201_4
 #  201|     m201_8(int)            = Store                       : &:r201_5, r201_7
 #  202|     r202_1(glval<int>)     = VariableAddress[#return]    : 

cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity.expected

@@ -15,6 +15,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity_unsound.expected

@@ -15,6 +15,7 @@ containsLoopOfForwardEdges
 lostReachability
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/range_based_for/range_based_for.expected

@@ -0,0 +1,32 @@
+bodies
+| test.cpp:8:3:10:3 | for(...:...) ... | test.cpp:8:28:10:3 | { ... } |
+| test.cpp:28:3:30:3 | for(...:...) ... | test.cpp:28:28:30:3 | { ... } |
+| test.cpp:44:3:46:3 | for(...:...) ... | test.cpp:44:27:46:3 | { ... } |
+variables
+| test.cpp:8:3:10:3 | for(...:...) ... | test.cpp:8:13:8:17 | value | file://:0:0:0:0 | short |
+| test.cpp:28:3:30:3 | for(...:...) ... | test.cpp:28:12:28:16 | value | file://:0:0:0:0 | int |
+| test.cpp:44:3:46:3 | for(...:...) ... | test.cpp:44:13:44:17 | value | file://:0:0:0:0 | long |
+ranges
+| test.cpp:8:3:10:3 | for(...:...) ... | test.cpp:8:21:8:25 | array | file://:0:0:0:0 | short[100] |
+| test.cpp:28:3:30:3 | for(...:...) ... | test.cpp:28:20:28:25 | vector | test.cpp:16:8:16:13 | Vector<int> |
+| test.cpp:44:3:46:3 | for(...:...) ... | test.cpp:44:21:44:24 | list | file://:0:0:0:0 | const List<long> & |
+rangeVariables
+| test.cpp:8:3:10:3 | for(...:...) ... | test.cpp:8:3:8:3 | (__range) | file://:0:0:0:0 | short(&)[100] |
+| test.cpp:28:3:30:3 | for(...:...) ... | test.cpp:28:3:28:3 | (__range) | file://:0:0:0:0 | Vector<int> & |
+| test.cpp:44:3:46:3 | for(...:...) ... | test.cpp:44:3:44:3 | (__range) | file://:0:0:0:0 | const List<long> & |
+conditions
+| test.cpp:8:3:10:3 | for(...:...) ... | file://:0:0:0:0 | ... != ... | file://:0:0:0:0 | (__begin) | file://:0:0:0:0 | (__end) |
+| test.cpp:28:3:30:3 | for(...:...) ... | test.cpp:28:20:28:20 | call to operator!= | file://:0:0:0:0 | (__begin) | file://:0:0:0:0 | (__end) |
+| test.cpp:44:3:46:3 | for(...:...) ... | file://:0:0:0:0 | ... != ... | file://:0:0:0:0 | (__begin) | file://:0:0:0:0 | (__end) |
+beginVariables
+| test.cpp:8:3:10:3 | for(...:...) ... | test.cpp:8:3:8:3 | (__begin) | file://:0:0:0:0 | short * |
+| test.cpp:28:3:30:3 | for(...:...) ... | test.cpp:28:3:28:3 | (__begin) | test.cpp:17:10:17:17 | Iterator |
+| test.cpp:44:3:46:3 | for(...:...) ... | test.cpp:44:3:44:3 | (__begin) | file://:0:0:0:0 | long * |
+endVariables
+| test.cpp:8:3:10:3 | for(...:...) ... | test.cpp:8:3:8:3 | (__end) | file://:0:0:0:0 | short * |
+| test.cpp:28:3:30:3 | for(...:...) ... | test.cpp:28:3:28:3 | (__end) | test.cpp:17:10:17:17 | Iterator |
+| test.cpp:44:3:46:3 | for(...:...) ... | test.cpp:44:3:44:3 | (__end) | file://:0:0:0:0 | long * |
+updates
+| test.cpp:8:3:10:3 | for(...:...) ... | file://:0:0:0:0 | ++ ... | file://:0:0:0:0 | (__begin) |
+| test.cpp:28:3:30:3 | for(...:...) ... | test.cpp:28:20:28:20 | call to operator++ | file://:0:0:0:0 | (__begin) |
+| test.cpp:44:3:46:3 | for(...:...) ... | file://:0:0:0:0 | ++ ... | file://:0:0:0:0 | (__begin) |

cpp/ql/test/library-tests/range_based_for/range_based_for.ql

@@ -0,0 +1,52 @@
+import cpp
+
+query predicate bodies(RangeBasedForStmt rbf, Stmt body) { body = rbf.getStmt() }
+
+query predicate variables(RangeBasedForStmt rbf, LocalVariable v, Type t) {
+  v = rbf.getVariable() and
+  t = v.getType()
+}
+
+query predicate ranges(RangeBasedForStmt rbf, Expr range, Type t) {
+  range = rbf.getRange() and
+  t = range.getType()
+}
+
+query predicate rangeVariables(RangeBasedForStmt rbf, LocalVariable rangeVar, Type t) {
+  rangeVar = rbf.getRangeVariable() and
+  t = rangeVar.getType()
+}
+
+query predicate conditions(RangeBasedForStmt rbf, Expr condition, Expr left, Expr right) {
+  condition = rbf.getCondition() and
+  (
+    condition instanceof BinaryOperation and
+    left = condition.(BinaryOperation).getLeftOperand() and
+    right = condition.(BinaryOperation).getRightOperand()
+    or
+    condition instanceof FunctionCall and
+    left = condition.(FunctionCall).getQualifier() and
+    right = condition.(FunctionCall).getArgument(0)
+  )
+}
+
+query predicate beginVariables(RangeBasedForStmt rbf, LocalVariable beginVar, Type t) {
+  beginVar = rbf.getBeginVariable() and
+  t = beginVar.getType()
+}
+
+query predicate endVariables(RangeBasedForStmt rbf, LocalVariable endVar, Type t) {
+  endVar = rbf.getEndVariable() and
+  t = endVar.getType()
+}
+
+query predicate updates(RangeBasedForStmt rbf, Expr update, Expr operand) {
+  update = rbf.getUpdate() and
+  (
+    update instanceof UnaryOperation and
+    operand = update.(UnaryOperation).getOperand()
+    or
+    update instanceof FunctionCall and
+    operand = update.(FunctionCall).getQualifier()
+  )
+}

cpp/ql/test/library-tests/range_based_for/test.cpp

@@ -0,0 +1,47 @@
+
+void print_short(short);
+void print_int(int);
+void print_long(long);
+
+short array[100];
+void loop_over_c_array() {
+  for (auto value : array) {
+    print_short(value);
+  }
+}
+
+// A class that can be used with range-based-for, because it has the member
+// functions `begin` and `end`.
+template<typename T>
+struct Vector {
+  struct Iterator {
+    const T& operator*() const;
+    bool operator!=(const Iterator &rhs) const;
+    Iterator operator++();
+  };
+  Iterator begin();
+  Iterator end();
+};
+
+Vector<int> vector;
+void loop_over_vector_object() {
+  for (int value : vector) {
+    print_int(value);
+  }
+}
+
+// A class that can be used with range-based-for, because there are `begin` and
+// `end` functions that take a `List` as their argument.
+template<typename T>
+struct List {};
+
+template<typename T>
+T* begin(const List<T> &list);
+template<typename T>
+T* end(const List<T> &list);
+
+void loop_over_list_object(const List<long> &list) {
+  for (auto value : list) {
+    print_long(value);
+  }
+}

cpp/ql/test/library-tests/syntax-zoo/aliased_ssa_sanity.expected

@@ -568,6 +568,7 @@ lostReachability
 | range_analysis.c:371:37:371:39 | Constant: 500 |
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/syntax-zoo/raw_sanity.expected

@@ -645,6 +645,7 @@ useNotDominatedByDefinition
 | pointer_to_member.cpp:36:22:36:28 | Address | Operand 'Address' is not dominated by its definition in function '$@'. | pointer_to_member.cpp:32:6:32:14 | IR: pmIsConst | void pmIsConst() |
 | try_catch.cpp:21:13:21:24 | Address | Operand 'Address' is not dominated by its definition in function '$@'. | try_catch.cpp:19:6:19:23 | IR: throw_from_nonstmt | void throw_from_nonstmt(int) |
 | vla.c:3:27:3:30 | Address | Operand 'Address' is not dominated by its definition in function '$@'. | vla.c:3:5:3:8 | IR: main | int main(int, char**) |
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/syntax-zoo/unaliased_ssa_sanity.expected

@@ -577,6 +577,7 @@ lostReachability
 | range_analysis.c:371:37:371:39 | Constant: 500 |
 backEdgeCountMismatch
 useNotDominatedByDefinition
+switchInstructionWithoutDefaultEdge
 missingCanonicalLanguageType
 multipleCanonicalLanguageTypes
 missingIRType

cpp/ql/test/library-tests/valuenumbering/GlobalValueNumbering/ast_gvn.ql

@@ -1,5 +1,5 @@
 import cpp
-import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+import semmle.code.cpp.valuenumbering.GlobalValueNumberingImpl
 
 from GVN g
 where strictcount(g.getAnExpr()) > 1

cpp/ql/test/library-tests/valuenumbering/GlobalValueNumbering/ast_uniqueness.ql

@@ -1,5 +1,5 @@
 import cpp
-import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+import semmle.code.cpp.valuenumbering.GlobalValueNumberingImpl
 
 // Every expression should have exactly one GVN.
 // So this query should have zero results.

cpp/ql/test/library-tests/valuenumbering/GlobalValueNumbering/diff_ir_expr.ql

@@ -1,5 +1,5 @@
 import cpp
-import semmle.code.cpp.valuenumbering.GlobalValueNumbering as AST
+import semmle.code.cpp.valuenumbering.GlobalValueNumberingImpl as AST
 import semmle.code.cpp.ir.internal.ASTValueNumbering as IR
 import semmle.code.cpp.ir.IR
 

cpp/ql/test/query-tests/Likely Bugs/Memory Management/StrncpyFlippedArgs/StrncpyFlippedArgs.expected

@@ -12,6 +12,5 @@
 | test.cpp:46:2:46:9 | call to strcpy_s | Potentially unsafe call to strcpy_s; second argument should be size of destination. |
 | test.cpp:47:2:47:9 | call to strcpy_s | Potentially unsafe call to strcpy_s; second argument should be size of destination. |
 | test.cpp:60:3:60:9 | call to strncpy | Potentially unsafe call to strncpy; third argument should be size of destination. |
-| test.cpp:63:3:63:9 | call to strncpy | Potentially unsafe call to strncpy; third argument should be size of destination. |
+| test.cpp:68:2:68:8 | call to strncpy | Potentially unsafe call to strncpy; third argument should be size of destination. |
 | test.cpp:79:3:79:9 | call to strncpy | Potentially unsafe call to strncpy; third argument should be size of destination. |
-| test.cpp:82:3:82:9 | call to strncpy | Potentially unsafe call to strncpy; third argument should be size of destination. |

cpp/ql/test/query-tests/Security/CWE/CWE-120/semmle/tests/UnboundedWrite.expected

@@ -1,5 +1,10 @@
 | tests.c:28:3:28:9 | call to sprintf | This 'call to sprintf' with input from $@ may overflow the destination. | tests.c:28:22:28:25 | argv | argv |
 | tests.c:29:3:29:9 | call to sprintf | This 'call to sprintf' with input from $@ may overflow the destination. | tests.c:29:28:29:31 | argv | argv |
+| tests.c:31:15:31:23 | buffer100 | This 'scanf string argument' with input from $@ may overflow the destination. | tests.c:28:22:28:25 | argv | argv |
+| tests.c:31:15:31:23 | buffer100 | This 'scanf string argument' with input from $@ may overflow the destination. | tests.c:29:28:29:31 | argv | argv |
 | tests.c:31:15:31:23 | buffer100 | This 'scanf string argument' with input from $@ may overflow the destination. | tests.c:31:15:31:23 | buffer100 | buffer100 |
+| tests.c:33:21:33:29 | buffer100 | This 'scanf string argument' with input from $@ may overflow the destination. | tests.c:28:22:28:25 | argv | argv |
+| tests.c:33:21:33:29 | buffer100 | This 'scanf string argument' with input from $@ may overflow the destination. | tests.c:29:28:29:31 | argv | argv |
+| tests.c:33:21:33:29 | buffer100 | This 'scanf string argument' with input from $@ may overflow the destination. | tests.c:31:15:31:23 | buffer100 | buffer100 |
 | tests.c:33:21:33:29 | buffer100 | This 'scanf string argument' with input from $@ may overflow the destination. | tests.c:33:21:33:29 | buffer100 | buffer100 |
 | tests.c:34:25:34:33 | buffer100 | This 'sscanf string argument' with input from $@ may overflow the destination. | tests.c:34:10:34:13 | argv | argv |

cpp/ql/test/query-tests/Security/CWE/CWE-129/semmle/ImproperArrayIndexValidation/ImproperArrayIndexValidation.expected

@@ -1,4 +1,3 @@
 | test1.c:18:16:18:16 | i | $@ flows to here and is used in an array indexing expression, potentially causing an invalid access. | test1.c:8:16:8:19 | argv | User-provided value |
 | test1.c:33:11:33:11 | i | $@ flows to here and is used in an array indexing expression, potentially causing an invalid access. | test1.c:8:16:8:19 | argv | User-provided value |
-| test1.c:37:11:37:11 | i | $@ flows to here and is used in an array indexing expression, potentially causing an invalid access. | test1.c:8:16:8:19 | argv | User-provided value |
 | test1.c:53:15:53:15 | j | $@ flows to here and is used in an array indexing expression, potentially causing an invalid access. | test1.c:8:16:8:19 | argv | User-provided value |

cpp/ql/test/query-tests/Security/CWE/CWE-134/semmle/argv/argvLocal.c

@@ -146,19 +146,21 @@ int main(int argc, char **argv) {
 
 	// BAD: i8 value comes from argv
 	char *i8;
-	*(&i8 + 1) = argv[1];
+	*(&i8) = argv[1];
 	printf(i8);
 	printWrapper(i8);
 
 	// BAD: i9 value comes from argv
-	char *i9;
+	char i9buf[32];
-	memcpy(1 ? i9++ : 0, argv[1], 1);
+	char *i9 = i9buf;
+	memcpy(1 ? ++i9 : 0, argv[1], 1);
 	printf(i9);
 	printWrapper(i9);
 
 	// BAD: i91 value comes from argv
-	char *i91;
+	char i91buf[64];
-	memcpy(0 ? 0 : (char *)((int) i91 * 2), argv[1], 1);
+	char *i91 = &i91buf[0];
+	memcpy(0 ? 0 : i91, argv[1] + 1, 1);
 	printf(i91);
 	printWrapper(i91);
 

cpp/ql/test/query-tests/Security/CWE/CWE-134/semmle/argv/argvLocal.expected

@@ -16,15 +16,13 @@
 | argvLocal.c:132:15:132:20 | ... + ... | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:126:10:126:13 | argv | argv |
 | argvLocal.c:135:9:135:12 | ... ++ | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | argvLocal.c:115:13:115:16 | argv | argv |
 | argvLocal.c:136:15:136:18 | -- ... | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:115:13:115:16 | argv | argv |
-| argvLocal.c:139:9:139:26 | ... ? ... : ... | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | argvLocal.c:126:10:126:13 | argv | argv |
-| argvLocal.c:140:15:140:32 | ... ? ... : ... | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:126:10:126:13 | argv | argv |
 | argvLocal.c:144:9:144:10 | i7 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | argvLocal.c:100:7:100:10 | argv | argv |
 | argvLocal.c:145:15:145:16 | i7 | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:100:7:100:10 | argv | argv |
-| argvLocal.c:150:9:150:10 | i8 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | argvLocal.c:149:15:149:18 | argv | argv |
+| argvLocal.c:150:9:150:10 | i8 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | argvLocal.c:149:11:149:14 | argv | argv |
-| argvLocal.c:151:15:151:16 | i8 | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:149:15:149:18 | argv | argv |
+| argvLocal.c:151:15:151:16 | i8 | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:149:11:149:14 | argv | argv |
-| argvLocal.c:156:9:156:10 | i9 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | argvLocal.c:155:23:155:26 | argv | argv |
+| argvLocal.c:157:9:157:10 | i9 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | argvLocal.c:156:23:156:26 | argv | argv |
-| argvLocal.c:157:15:157:16 | i9 | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:155:23:155:26 | argv | argv |
+| argvLocal.c:158:15:158:16 | i9 | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:156:23:156:26 | argv | argv |
-| argvLocal.c:162:9:162:11 | i91 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | argvLocal.c:161:42:161:45 | argv | argv |
+| argvLocal.c:164:9:164:11 | i91 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | argvLocal.c:163:22:163:25 | argv | argv |
-| argvLocal.c:163:15:163:17 | i91 | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:161:42:161:45 | argv | argv |
+| argvLocal.c:165:15:165:17 | i91 | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:163:22:163:25 | argv | argv |
-| argvLocal.c:167:18:167:20 | i10 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | argvLocal.c:166:18:166:21 | argv | argv |
+| argvLocal.c:169:18:169:20 | i10 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | argvLocal.c:168:18:168:21 | argv | argv |
-| argvLocal.c:168:24:168:26 | i10 | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:166:18:166:21 | argv | argv |
+| argvLocal.c:170:24:170:26 | i10 | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format) | argvLocal.c:168:18:168:21 | argv | argv |

cpp/ql/test/query-tests/Security/CWE/CWE-134/semmle/funcs/funcsLocal.expected

@@ -3,6 +3,3 @@
 | funcsLocal.c:32:9:32:10 | i4 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | funcsLocal.c:31:13:31:17 | call to fgets | fgets |
 | funcsLocal.c:37:9:37:10 | i5 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | funcsLocal.c:36:7:36:8 | i5 | gets |
 | funcsLocal.c:42:9:42:10 | i6 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | funcsLocal.c:41:13:41:16 | call to gets | gets |
-| funcsLocal.c:47:9:47:11 | * ... | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | funcsLocal.c:46:7:46:9 | * ... | gets |
-| funcsLocal.c:53:9:53:11 | * ... | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | funcsLocal.c:52:8:52:11 | call to gets | gets |
-| funcsLocal.c:58:9:58:10 | e1 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | funcsLocal.c:16:8:16:9 | i1 | fread |

cpp/ql/test/query-tests/Security/CWE/CWE-134/semmle/ifs/ifs.expected

@@ -1,3 +1,4 @@
+| ifs.c:62:9:62:10 | c7 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | ifs.c:61:8:61:11 | argv | argv |
 | ifs.c:69:9:69:10 | c8 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | ifs.c:68:8:68:11 | argv | argv |
 | ifs.c:75:9:75:10 | i1 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | ifs.c:74:8:74:11 | argv | argv |
 | ifs.c:81:9:81:10 | i2 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format) | ifs.c:80:8:80:11 | argv | argv |

cpp/ql/test/query-tests/Security/CWE/CWE-190/semmle/TaintedAllocationSize/TaintedAllocationSize.expected

@@ -1,6 +1,8 @@
 | test.cpp:42:31:42:36 | call to malloc | This allocation size is derived from $@ and might overflow | test.cpp:39:21:39:24 | argv | user input (argv) |
+| test.cpp:43:31:43:36 | call to malloc | This allocation size is derived from $@ and might overflow | test.cpp:39:21:39:24 | argv | user input (argv) |
 | test.cpp:43:38:43:63 | ... * ... | This allocation size is derived from $@ and might overflow | test.cpp:39:21:39:24 | argv | user input (argv) |
+| test.cpp:45:31:45:36 | call to malloc | This allocation size is derived from $@ and might overflow | test.cpp:39:21:39:24 | argv | user input (argv) |
 | test.cpp:48:25:48:30 | call to malloc | This allocation size is derived from $@ and might overflow | test.cpp:39:21:39:24 | argv | user input (argv) |
 | test.cpp:49:17:49:30 | new[] | This allocation size is derived from $@ and might overflow | test.cpp:39:21:39:24 | argv | user input (argv) |
+| test.cpp:52:21:52:27 | call to realloc | This allocation size is derived from $@ and might overflow | test.cpp:39:21:39:24 | argv | user input (argv) |
 | test.cpp:52:35:52:60 | ... * ... | This allocation size is derived from $@ and might overflow | test.cpp:39:21:39:24 | argv | user input (argv) |
-| test.cpp:55:11:55:24 | new[] | This allocation size is derived from $@ and might overflow | test.cpp:39:21:39:24 | argv | user input (argv) |

cpp/ql/test/query-tests/Security/CWE/CWE-190/semmle/extreme/ArithmeticWithExtremeValues.expected

@@ -1,7 +1,6 @@
 | test.c:17:10:17:12 | min | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:8:9:8:15 | 2147483647 | Extreme value |
 | test.c:48:3:48:5 | sc2 | $@ flows to here and is used in arithmetic, potentially causing an underflow. | test.c:47:9:47:16 | - ... | Extreme value |
 | test.c:50:3:50:5 | sc3 | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:49:9:49:16 | 127 | Extreme value |
-| test.c:56:3:56:5 | sc5 | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:54:9:54:16 | 127 | Extreme value |
 | test.c:59:3:59:5 | sc6 | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:58:9:58:16 | 127 | Extreme value |
 | test.c:63:3:63:5 | sc8 | $@ flows to here and is used in arithmetic, potentially causing an underflow. | test.c:62:9:62:16 | - ... | Extreme value |
 | test.c:75:3:75:5 | sc1 | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.c:74:9:74:16 | 127 | Extreme value |

cpp/ql/test/query-tests/Security/CWE/CWE-190/semmle/uncontrolled/ArithmeticUncontrolled.expected

@@ -8,4 +8,3 @@
 | test.c:77:9:77:9 | r | $@ flows to here and is used in arithmetic, potentially causing an underflow. | test.c:75:13:75:19 | ... ^ ... | Uncontrolled value |
 | test.c:100:5:100:5 | r | $@ flows to here and is used in arithmetic, potentially causing an underflow. | test.c:99:14:99:19 | call to rand | Uncontrolled value |
 | test.cpp:25:7:25:7 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:8:9:8:12 | call to rand | Uncontrolled value |
-| test.cpp:37:7:37:7 | r | $@ flows to here and is used in arithmetic, potentially causing an overflow. | test.cpp:18:9:18:12 | call to rand | Uncontrolled value |

cpp/ql/test/query-tests/Security/CWE/CWE-807/semmle/TaintedCondition/TaintedCondition.expected

@@ -1 +1,2 @@
 | test.cpp:24:10:24:35 | ! ... | Reliance on untrusted input $@ to raise privilege at $@ | test.cpp:20:29:20:34 | call to getenv | call to getenv | test.cpp:25:9:25:27 | ... = ... | ... = ... |
+| test.cpp:41:10:41:38 | ! ... | Reliance on untrusted input $@ to raise privilege at $@ | test.cpp:20:29:20:34 | call to getenv | call to getenv | test.cpp:42:8:42:26 | ... = ... | ... = ... |

csharp/autobuilder/Semmle.Autobuild.Tests/Semmle.Autobuild.Tests.csproj

@@ -4,6 +4,7 @@
     <OutputType>Exe</OutputType>
     <TargetFramework>netcoreapp3.0</TargetFramework>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
+    <RuntimeIdentifiers>win-x64;linux-x64;osx-x64</RuntimeIdentifiers>
   </PropertyGroup>
 
   <ItemGroup>

csharp/autobuilder/Semmle.Autobuild/Semmle.Autobuild.csproj

@@ -8,6 +8,7 @@
     <OutputType>Exe</OutputType>
     <StartupObject />
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
+    <RuntimeIdentifiers>win-x64;linux-x64;osx-x64</RuntimeIdentifiers>
   </PropertyGroup>
 
   <ItemGroup>

csharp/extractor/Semmle.Extraction.CIL.Driver/Semmle.Extraction.CIL.Driver.csproj

@@ -6,6 +6,7 @@
     <AssemblyName>Semmle.Extraction.CIL.Driver</AssemblyName>
     <RootNamespace>Semmle.Extraction.CIL.Driver</RootNamespace>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
+    <RuntimeIdentifiers>win-x64;linux-x64;osx-x64</RuntimeIdentifiers>
   </PropertyGroup>
 
   <ItemGroup>

csharp/extractor/Semmle.Extraction.CIL/Semmle.Extraction.CIL.csproj

@@ -6,6 +6,7 @@
     <RootNamespace>Semmle.Extraction.CIL</RootNamespace>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
     <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+    <RuntimeIdentifiers>win-x64;linux-x64;osx-x64</RuntimeIdentifiers>
   </PropertyGroup>
 
   <PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|AnyCPU'">

csharp/extractor/Semmle.Extraction.CSharp.Driver/Semmle.Extraction.CSharp.Driver.csproj

@@ -6,6 +6,7 @@
     <AssemblyName>Semmle.Extraction.CSharp.Driver</AssemblyName>
     <RootNamespace>Semmle.Extraction.CSharp.Driver</RootNamespace>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
+    <RuntimeIdentifiers>win-x64;linux-x64;osx-x64</RuntimeIdentifiers>
   </PropertyGroup>
 
   <ItemGroup>

csharp/extractor/Semmle.Extraction.CSharp.Standalone/Semmle.Extraction.CSharp.Standalone.csproj

@@ -9,6 +9,7 @@
     <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
     <TreatWarningsAsErrors>false</TreatWarningsAsErrors>
     <WarningsAsErrors />
+    <RuntimeIdentifiers>win-x64;linux-x64;osx-x64</RuntimeIdentifiers>
   </PropertyGroup>
 
   <ItemGroup>

csharp/extractor/Semmle.Extraction.CSharp/Semmle.Extraction.CSharp.csproj

@@ -6,6 +6,7 @@
     <RootNamespace>Semmle.Extraction.CSharp</RootNamespace>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
     <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+    <RuntimeIdentifiers>win-x64;linux-x64;osx-x64</RuntimeIdentifiers>
   </PropertyGroup>
 
   <ItemGroup>

csharp/extractor/Semmle.Extraction.Tests/Semmle.Extraction.Tests.csproj

@@ -4,6 +4,7 @@
     <OutputType>Exe</OutputType>
     <TargetFramework>netcoreapp3.0</TargetFramework>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
+    <RuntimeIdentifiers>win-x64;linux-x64;osx-x64</RuntimeIdentifiers>
   </PropertyGroup>
 
   <ItemGroup>

csharp/extractor/Semmle.Extraction/Semmle.Extraction.csproj

@@ -6,6 +6,7 @@
     <RootNamespace>Semmle.Extraction</RootNamespace>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
     <CodeAnalysisRuleSet>Semmle.Extraction.ruleset</CodeAnalysisRuleSet>
+    <RuntimeIdentifiers>win-x64;linux-x64;osx-x64</RuntimeIdentifiers>
   </PropertyGroup>
 
   <PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|AnyCPU'">

csharp/extractor/Semmle.Util.Tests/Semmle.Util.Tests.csproj

@@ -4,6 +4,7 @@
     <OutputType>Exe</OutputType>
     <TargetFramework>netcoreapp3.0</TargetFramework>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
+    <RuntimeIdentifiers>win-x64;linux-x64;osx-x64</RuntimeIdentifiers>
   </PropertyGroup>
 
   <ItemGroup>

csharp/extractor/Semmle.Util/Semmle.Util.csproj

@@ -5,6 +5,7 @@
     <AssemblyName>Semmle.Util</AssemblyName>
     <RootNamespace>Semmle.Util</RootNamespace>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
+    <RuntimeIdentifiers>win-x64;linux-x64;osx-x64</RuntimeIdentifiers>
   </PropertyGroup>
 
   <ItemGroup>

csharp/ql/src/experimental/README.md

@@ -0,0 +1 @@
+This directory contains [experimental](../../../../docs/experimental.md) CodeQL queries and libraries.

csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImpl2.qll

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImpl3.qll

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImpl4.qll

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImpl5.qll

@@ -259,44 +259,47 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
 
 /**
  * Holds if `node` is reachable from a source in the given configuration
- * ignoring call contexts.
+ * taking simple call contexts into consideration.
  */
-private predicate nodeCandFwd1(Node node, Configuration config) {
+private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config) {
   not fullBarrier(node, config) and
   (
-    config.isSource(node)
+    config.isSource(node) and
+    fromArg = false
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       localFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       additionalLocalFlowStep(mid, node, config)
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      jumpStep(mid, node, config)
+      jumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     exists(Node mid |
       nodeCandFwd1(mid, config) and
-      additionalJumpStep(mid, node, config)
+      additionalJumpStep(mid, node, config) and
+      fromArg = false
     )
     or
     // store
     exists(Node mid |
       useFieldFlow(config) and
-      nodeCandFwd1(mid, config) and
+      nodeCandFwd1(mid, fromArg, config) and
       storeDirect(mid, _, node) and
       not outBarrier(mid, config)
     )
     or
     // read
     exists(Content f |
-      nodeCandFwd1Read(f, node, config) and
+      nodeCandFwd1Read(f, node, fromArg, config) and
       storeCandFwd1(f, config) and
       not inBarrier(node, config)
     )
@@ -304,30 +307,37 @@ private predicate nodeCandFwd1(Node node, Configuration config) {
     // flow into a callable
     exists(Node arg |
       nodeCandFwd1(arg, config) and
-      viableParamArg(_, node, arg)
+      viableParamArg(_, node, arg) and
+      fromArg = true
     )
     or
     // flow out of a callable
-    exists(DataFlowCall call, ReturnPosition pos, ReturnKindExt kind |
+    exists(DataFlowCall call |
-      nodeCandFwd1ReturnPosition(pos, config) and
+      nodeCandFwd1Out(call, node, false, config) and
-      pos = viableReturnPos(call, kind) and
+      fromArg = false
-      node = kind.getAnOutNode(call)
+      or
+      nodeCandFwd1OutFromArg(call, node, config) and
+      flowOutCandFwd1(call, fromArg, config)
     )
   )
 }
 
-pragma[noinline]
+private predicate nodeCandFwd1(Node node, Configuration config) { nodeCandFwd1(node, _, config) }
-private predicate nodeCandFwd1ReturnPosition(ReturnPosition pos, Configuration config) {
+
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnPosition(
+  ReturnPosition pos, boolean fromArg, Configuration config
+) {
   exists(ReturnNodeExt ret |
-    nodeCandFwd1(ret, config) and
+    nodeCandFwd1(ret, fromArg, config) and
     getReturnPosition(ret) = pos
   )
 }
 
 pragma[nomagic]
-private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
+private predicate nodeCandFwd1Read(Content f, Node node, boolean fromArg, Configuration config) {
   exists(Node mid |
-    nodeCandFwd1(mid, config) and
+    nodeCandFwd1(mid, fromArg, config) and
     readDirect(mid, f, node)
   )
 }
@@ -335,7 +345,7 @@ private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
 /**
  * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate storeCandFwd1(Content f, Configuration config) {
   exists(Node mid, Node node |
     not fullBarrier(node, config) and
@@ -345,71 +355,120 @@ private predicate storeCandFwd1(Content f, Configuration config) {
   )
 }
 
+pragma[nomagic]
+private predicate nodeCandFwd1ReturnKind(
+  DataFlowCall call, ReturnKindExt kind, boolean fromArg, Configuration config
+) {
+  exists(ReturnPosition pos |
+    nodeCandFwd1ReturnPosition(pos, fromArg, config) and
+    pos = viableReturnPos(call, kind)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1Out(
+  DataFlowCall call, Node node, boolean fromArg, Configuration config
+) {
+  exists(ReturnKindExt kind |
+    nodeCandFwd1ReturnKind(call, kind, fromArg, config) and
+    node = kind.getAnOutNode(call)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCandFwd1OutFromArg(DataFlowCall call, Node node, Configuration config) {
+  nodeCandFwd1Out(call, node, true, config)
+}
+
+/**
+ * Holds if an argument to `call` is reached in the flow covered by `nodeCandFwd1`.
+ */
+pragma[nomagic]
+private predicate flowOutCandFwd1(DataFlowCall call, boolean fromArg, Configuration config) {
+  exists(ArgumentNode arg |
+    nodeCandFwd1(arg, fromArg, config) and
+    viableParamArg(call, _, arg)
+  )
+}
+
 bindingset[result, b]
 private boolean unbindBool(boolean b) { result != b.booleanNot() }
 
 /**
  * Holds if `node` is part of a path from a source to a sink in the given
- * configuration ignoring call contexts.
+ * configuration taking simple call contexts into consideration.
  */
 pragma[nomagic]
-private predicate nodeCand1(Node node, Configuration config) {
+private predicate nodeCand1(Node node, boolean toReturn, Configuration config) {
+  nodeCand1_0(node, toReturn, config) and
+  nodeCandFwd1(node, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config) {
   nodeCandFwd1(node, config) and
-  config.isSink(node)
+  config.isSink(node) and
+  toReturn = false
   or
-  nodeCandFwd1(node, unbind(config)) and
+  exists(Node mid |
-  (
+    localFlowStep(node, mid, config) and
-    exists(Node mid |
+    nodeCand1(mid, toReturn, config)
-      localFlowStep(node, mid, config) and
+  )
-      nodeCand1(mid, config)
+  or
-    )
+  exists(Node mid |
+    additionalLocalFlowStep(node, mid, config) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  exists(Node mid |
+    jumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  exists(Node mid |
+    additionalJumpStep(node, mid, config) and
+    nodeCand1(mid, _, config) and
+    toReturn = false
+  )
+  or
+  // store
+  exists(Content f |
+    nodeCand1Store(f, node, toReturn, config) and
+    readCand1(f, config)
+  )
+  or
+  // read
+  exists(Node mid, Content f |
+    readDirect(node, f, mid) and
+    storeCandFwd1(f, unbind(config)) and
+    nodeCand1(mid, toReturn, config)
+  )
+  or
+  // flow into a callable
+  exists(DataFlowCall call |
+    nodeCand1Arg(call, node, false, config) and
+    toReturn = false
     or
-    exists(Node mid |
+    nodeCand1ArgToReturn(call, node, config) and
-      additionalLocalFlowStep(node, mid, config) and
+    flowInCand1(call, toReturn, config)
-      nodeCand1(mid, config)
+  )
-    )
+  or
-    or
+  // flow out of a callable
-    exists(Node mid |
+  exists(ReturnPosition pos |
-      jumpStep(node, mid, config) and
+    nodeCand1ReturnPosition(pos, config) and
-      nodeCand1(mid, config)
+    getReturnPosition(node) = pos and
-    )
+    toReturn = true
-    or
-    exists(Node mid |
-      additionalJumpStep(node, mid, config) and
-      nodeCand1(mid, config)
-    )
-    or
-    // store
-    exists(Content f |
-      nodeCand1Store(f, node, config) and
-      readCand1(f, config)
-    )
-    or
-    // read
-    exists(Node mid, Content f |
-      readDirect(node, f, mid) and
-      storeCandFwd1(f, unbind(config)) and
-      nodeCand1(mid, config)
-    )
-    or
-    // flow into a callable
-    exists(Node param |
-      viableParamArg(_, param, node) and
-      nodeCand1(param, config)
-    )
-    or
-    // flow out of a callable
-    exists(ReturnPosition pos |
-      nodeCand1ReturnPosition(pos, config) and
-      getReturnPosition(node) = pos
-    )
   )
 }
 
-pragma[noinline]
+pragma[nomagic]
+private predicate nodeCand1(Node node, Configuration config) { nodeCand1(node, _, config) }
+
+pragma[nomagic]
 private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration config) {
   exists(DataFlowCall call, ReturnKindExt kind, Node out |
-    nodeCand1(out, config) and
+    nodeCand1(out, _, config) and
     pos = viableReturnPos(call, kind) and
     out = kind.getAnOutNode(call)
   )
@@ -418,21 +477,21 @@ private predicate nodeCand1ReturnPosition(ReturnPosition pos, Configuration conf
 /**
  * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
  */
-pragma[noinline]
+pragma[nomagic]
 private predicate readCand1(Content f, Configuration config) {
   exists(Node mid, Node node |
     useFieldFlow(config) and
     nodeCandFwd1(node, unbind(config)) and
     readDirect(node, f, mid) and
     storeCandFwd1(f, unbind(config)) and
-    nodeCand1(mid, config)
+    nodeCand1(mid, _, config)
   )
 }
 
 pragma[nomagic]
-private predicate nodeCand1Store(Content f, Node node, Configuration config) {
+private predicate nodeCand1Store(Content f, Node node, boolean toReturn, Configuration config) {
   exists(Node mid |
-    nodeCand1(mid, config) and
+    nodeCand1(mid, toReturn, config) and
     storeCandFwd1(f, unbind(config)) and
     storeDirect(node, f, mid)
   )
@@ -444,11 +503,45 @@ private predicate nodeCand1Store(Content f, Node node, Configuration config) {
  */
 private predicate readStoreCand1(Content f, Configuration conf) {
   readCand1(f, conf) and
-  nodeCand1Store(f, _, conf)
+  nodeCand1Store(f, _, _, conf)
+}
+
+pragma[nomagic]
+private predicate viableParamArgCandFwd1(
+  DataFlowCall call, ParameterNode p, ArgumentNode arg, Configuration config
+) {
+  viableParamArg(call, p, arg) and
+  nodeCandFwd1(arg, config)
+}
+
+pragma[nomagic]
+private predicate nodeCand1Arg(
+  DataFlowCall call, ArgumentNode arg, boolean toReturn, Configuration config
+) {
+  exists(ParameterNode p |
+    nodeCand1(p, toReturn, config) and
+    viableParamArgCandFwd1(call, p, arg, config)
+  )
+}
+
+pragma[nomagic]
+private predicate nodeCand1ArgToReturn(DataFlowCall call, ArgumentNode arg, Configuration config) {
+  nodeCand1Arg(call, arg, true, config)
+}
+
+/**
+ * Holds if an output from `call` is reached in the flow covered by `nodeCand1`.
+ */
+pragma[nomagic]
+private predicate flowInCand1(DataFlowCall call, boolean toReturn, Configuration config) {
+  exists(Node out |
+    nodeCand1(out, toReturn, config) and
+    nodeCandFwd1OutFromArg(call, out, config)
+  )
 }
 
 private predicate throughFlowNodeCand(Node node, Configuration config) {
-  nodeCand1(node, config) and
+  nodeCand1(node, true, config) and
   not fullBarrier(node, config) and
   not inBarrier(node, config) and
   not outBarrier(node, config)
@@ -2257,13 +2350,12 @@ private class PathNodeSink extends PathNodeImpl, TPathNodeSink {
  * a callable is recorded by `cc`.
  */
 private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCtx sc, AccessPath ap) {
-  exists(LocalCallContext localCC, AccessPath ap0, Node midnode, Configuration conf |
+  exists(
-    midnode = mid.getNode() and
+    AccessPath ap0, Node midnode, Configuration conf, DataFlowCallable enclosing,
-    conf = mid.getConfiguration() and
+    LocalCallContext localCC
-    cc = mid.getCallContext() and
+  |
-    sc = mid.getSummaryCtx() and
+    pathIntoLocalStep(mid, midnode, cc, enclosing, sc, ap0, conf) and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(cc, enclosing)
-    ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, conf, localCC) and
     ap = ap0
@@ -2297,6 +2389,20 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
   pathThroughCallable(mid, node, cc, ap) and sc = mid.getSummaryCtx()
 }
 
+pragma[nomagic]
+private predicate pathIntoLocalStep(
+  PathNodeMid mid, Node midnode, CallContext cc, DataFlowCallable enclosing, SummaryCtx sc,
+  AccessPath ap0, Configuration conf
+) {
+  midnode = mid.getNode() and
+  cc = mid.getCallContext() and
+  conf = mid.getConfiguration() and
+  localFlowBigStep(midnode, _, _, conf, _) and
+  enclosing = midnode.getEnclosingCallable() and
+  sc = mid.getSummaryCtx() and
+  ap0 = mid.getAp()
+}
+
 pragma[nomagic]
 private predicate readCand(Node node1, Content f, Node node2, Configuration config) {
   readDirect(node1, f, node2) and

csharp/ql/src/semmle/code/csharp/ir/implementation/raw/Instruction.qll

@@ -266,6 +266,16 @@ module InstructionSanity {
       funcText = Language::getIdentityString(func.getFunction())
     )
   }
+
+  query predicate switchInstructionWithoutDefaultEdge(
+    SwitchInstruction switchInstr, string message, IRFunction func, string funcText
+  ) {
+    not exists(switchInstr.getDefaultSuccessor()) and
+    message =
+      "SwitchInstruction " + switchInstr.toString() + " without a DefaultEdge in function '$@'." and
+    func = switchInstr.getEnclosingIRFunction() and
+    funcText = Language::getIdentityString(func.getFunction())
+  }
 }
 
 /**

csharp/ql/src/semmle/code/csharp/ir/implementation/raw/gvn/ValueNumbering.qll

@@ -27,19 +27,19 @@ class ValueNumber extends TValueNumber {
   final Language::Location getLocation() {
     if
       exists(Instruction i |
-        i = getAnInstruction() and not i.getLocation() instanceof UnknownLocation
+        i = getAnInstruction() and not i.getLocation() instanceof Language::UnknownLocation
       )
     then
       result =
         min(Language::Location l |
-          l = getAnInstruction().getLocation() and not l instanceof UnknownLocation
+          l = getAnInstruction().getLocation() and not l instanceof Language::UnknownLocation
         |
           l
           order by
             l.getFile().getAbsolutePath(), l.getStartLine(), l.getStartColumn(), l.getEndLine(),
             l.getEndColumn()
         )
-    else result instanceof UnknownDefaultLocation
+    else result instanceof Language::UnknownDefaultLocation
   }
 
   /**

csharp/ql/src/semmle/code/csharp/ir/implementation/raw/gvn/internal/ValueNumberingImports.qll

@@ -1 +1,3 @@
 import semmle.code.csharp.ir.internal.Overlap
+import semmle.code.csharp.ir.internal.IRCSharpLanguage as Language
+import semmle.code.csharp.ir.implementation.unaliased_ssa.IR