Merge branch 'main' into rc/3.7

.bazelrc

@@ -1,3 +1,3 @@
-build --repo_env=CC=clang --repo_env=CXX=clang++ --copt="-std=c++17"
+build --repo_env=CC=clang --repo_env=CXX=clang++ --cxxopt="-std=c++17"
 
 try-import %workspace%/local.bazelrc

.github/workflows/check-qldoc.yml

@@ -27,7 +27,8 @@ jobs:
         run: |
           EXIT_CODE=0
           # TODO: remove the swift exception from the regex when we fix generated QLdoc
-          changed_lib_packs="$(git diff --name-only --diff-filter=ACMRT HEAD^ HEAD | { grep -Po '^(?!swift)[a-z]*/ql/lib' || true; } | sort -u)"
+          # TODO: remove the shared exception from the regex when coverage of qlpacks without dbschemes is supported
+          changed_lib_packs="$(git diff --name-only --diff-filter=ACMRT HEAD^ HEAD | { grep -Po '^(?!(swift|shared))[a-z]*/ql/lib' || true; } | sort -u)"
           for pack_dir in ${changed_lib_packs}; do
             lang="${pack_dir%/ql/lib}"
             codeql generate library-doc-coverage --output="${RUNNER_TEMP}/${lang}-current.txt" --dir="${pack_dir}"

.github/workflows/codeql-analysis.yml

@@ -56,7 +56,7 @@ jobs:
     #    uses a compiled language
 
     - run: |
-       dotnet build csharp /p:UseSharedCompilation=false
+       dotnet build csharp
 
     - name: Perform CodeQL Analysis
       uses: github/codeql-action/analyze@main

.github/workflows/csv-coverage-metrics.yml

@@ -55,7 +55,7 @@ jobs:
           DATABASE="${{ runner.temp }}/csharp-database"
           PROJECT="${{ runner.temp }}/csharp-project"
           dotnet new classlib --language=C# --output="$PROJECT"
-          codeql database create "$DATABASE" --language=csharp --source-root="$PROJECT" --command 'dotnet build /t:rebuild csharp-project.csproj /p:UseSharedCompilation=false'
+          codeql database create "$DATABASE" --language=csharp --source-root="$PROJECT" --command 'dotnet build /t:rebuild csharp-project.csproj'
       - name: Capture coverage information
         run: |
           DATABASE="${{ runner.temp }}/csharp-database"

.github/workflows/ql-for-ql-build.yml

@@ -5,6 +5,13 @@ on:
     branches: [main]
   pull_request:
     branches: [main]
+    paths:
+      - "ql/**"
+      - "**.qll"
+      - "**.ql"
+      - "**.dbscheme"
+      - "**/qlpack.yml"
+      - ".github/workflows/ql-for-ql-build.yml"
 
 env:
   CARGO_TERM_COLOR: always
@@ -108,7 +115,7 @@ jobs:
       ### Run the analysis ###
       - name: Hack codeql-action options
         run: |
-          JSON=$(jq -nc --arg pack "${PACK}" '.database."run-queries"=["--search-path", $pack] | .resolve.queries=["--search-path", $pack] | .resolve.extractor=["--search-path", $pack] | .database.init=["--search-path", $pack]')
+          JSON=$(jq -nc --arg pack "${PACK}" '.database."run-queries"=["--search-path", $pack] | .resolve.queries=["--search-path", $pack] | .resolve.extractor=["--search-path", $pack] | .resolve.languages=["--search-path", $pack] | .database.init=["--search-path", $pack]')
           echo "CODEQL_ACTION_EXTRA_OPTIONS=${JSON}" >> ${GITHUB_ENV}
         env:
           PACK: ${{ runner.temp }}/pack

.github/workflows/ruby-build.yml

@@ -95,6 +95,7 @@ jobs:
         uses: ./.github/actions/fetch-codeql
       - name: Build Query Pack
         run: |
+          codeql pack create ../shared/ssa --output target/packs
           codeql pack create ql/lib --output target/packs
           codeql pack install ql/src
           codeql pack create ql/src --output target/packs

.github/workflows/swift-codegen.yml

@@ -4,6 +4,8 @@ on:
   pull_request:
     paths:
       - "swift/**"
+      - "misc/bazel/**"
+      - "*.bazel*"
       - .github/workflows/swift-codegen.yml
       - .github/actions/fetch-codeql/action.yml
     branches:

.github/workflows/swift-integration-tests.yml

@@ -4,6 +4,8 @@ on:
   pull_request:
     paths:
       - "swift/**"
+      - "misc/bazel/**"
+      - "*.bazel*"
       - .github/workflows/swift-integration-tests.yml
       - .github/actions/fetch-codeql/action.yml
       - codeql-workspace.yml
@@ -30,6 +32,14 @@ jobs:
       - name: Build Swift extractor
         run: |
           bazel run //swift:create-extractor-pack
+      - name: Get Swift version
+        id: get_swift_version
+        run: |
+          VERSION=$(bazel run //swift/extractor -- --version | sed -ne 's/.*version \(\S*\).*/\1/p')
+          echo "::set-output name=version::$VERSION"
+      - uses: swift-actions/setup-swift@v1
+        with:
+          swift-version: "${{steps.get_swift_version.outputs.version}}"
       - name: Run integration tests
         run: |
           python integration-tests/runner.py

.github/workflows/swift-qltest.yml

@@ -4,6 +4,8 @@ on:
   pull_request:
     paths:
       - "swift/**"
+      - "misc/bazel/**"
+      - "*.bazel*"
       - .github/workflows/swift-qltest.yml
       - .github/actions/fetch-codeql/action.yml
       - codeql-workspace.yml

CODEOWNERS

@@ -30,6 +30,8 @@
 
 # Bazel (excluding BUILD.bazel files)
 WORKSPACE.bazel @github/codeql-ci-reviewers
+.bazelversion @github/codeql-ci-reviewers
+.bazelrc @github/codeql-ci-reviewers
 **/*.bzl @github/codeql-ci-reviewers
 
 # Documentation etc

codeql-workspace.yml

@@ -4,6 +4,7 @@ provide:
   - "*/ql/test/qlpack.yml"
   - "*/ql/examples/qlpack.yml"
   - "*/ql/consistency-queries/qlpack.yml"
+  - "shared/*/qlpack.yml"
   - "cpp/ql/test/query-tests/Security/CWE/CWE-190/semmle/tainted/qlpack.yml"
   - "go/ql/config/legacy-support/qlpack.yml"
   - "go/build/codeql-extractor-go/codeql-extractor.yml"

config/identical-files.json

@@ -17,6 +17,10 @@
     "cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll",
+    "cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll",
+    "cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll",
+    "cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll",
+    "cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll",
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll",
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl2.qll",
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl3.qll",
@@ -30,12 +34,14 @@
     "ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll",
     "ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl2.qll",
     "ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForLibraries.qll",
+    "ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForHttpClientLibraries.qll",
     "swift/ql/lib/codeql/swift/dataflow/internal/DataFlowImpl.qll"
   ],
   "DataFlow Java/C++/C#/Python Common": [
     "java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplCommon.qll",
     "cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplCommon.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImplCommon.qll",
+    "cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImplCommon.qll",
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImplCommon.qll",
     "python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImplCommon.qll",
     "ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplCommon.qll",
@@ -47,6 +53,9 @@
     "cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking1/TaintTrackingImpl.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking2/TaintTrackingImpl.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking3/TaintTrackingImpl.qll",
+    "cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/tainttracking1/TaintTrackingImpl.qll",
+    "cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/tainttracking2/TaintTrackingImpl.qll",
+    "cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/tainttracking3/TaintTrackingImpl.qll",
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll",
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll",
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking3/TaintTrackingImpl.qll",
@@ -67,15 +76,17 @@
     "java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplConsistency.qll",
     "cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplConsistency.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImplConsistency.qll",
+    "cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImplConsistency.qll",
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImplConsistency.qll",
     "python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImplConsistency.qll",
     "ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplConsistency.qll",
     "swift/ql/lib/codeql/swift/dataflow/internal/DataFlowImplConsistency.qll"
   ],
-  "DataFlow Java/C# Flow Summaries": [
+  "DataFlow Java/C#/Ruby/Python/Swift Flow Summaries": [
     "java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll",
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll",
     "ruby/ql/lib/codeql/ruby/dataflow/internal/FlowSummaryImpl.qll",
+    "python/ql/lib/semmle/python/dataflow/new/internal/FlowSummaryImpl.qll",
     "swift/ql/lib/codeql/swift/dataflow/internal/FlowSummaryImpl.qll"
   ],
   "SsaReadPosition Java/C#": [
@@ -460,15 +471,6 @@
     "javascript/ql/lib/IDEContextual.qll",
     "python/ql/lib/analysis/IDEContextual.qll"
   ],
-  "SSA C#": [
-    "csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImplCommon.qll",
-    "csharp/ql/lib/semmle/code/csharp/controlflow/internal/pressa/SsaImplCommon.qll",
-    "csharp/ql/lib/semmle/code/csharp/dataflow/internal/basessa/SsaImplCommon.qll",
-    "csharp/ql/lib/semmle/code/cil/internal/SsaImplCommon.qll",
-    "ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImplCommon.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImplCommon.qll",
-    "swift/ql/lib/codeql/swift/dataflow/internal/SsaImplCommon.qll"
-  ],
   "CryptoAlgorithms Python/JS/Ruby": [
     "javascript/ql/lib/semmle/javascript/security/CryptoAlgorithms.qll",
     "python/ql/lib/semmle/python/concepts/CryptoAlgorithms.qll",
@@ -540,7 +542,7 @@
     "java/ql/lib/semmle/code/java/dataflow/internal/AccessPathSyntax.qll",
     "javascript/ql/lib/semmle/javascript/frameworks/data/internal/AccessPathSyntax.qll",
     "ruby/ql/lib/codeql/ruby/dataflow/internal/AccessPathSyntax.qll",
-    "python/ql/lib/semmle/python/frameworks/data/internal/AccessPathSyntax.qll",
+    "python/ql/lib/semmle/python/dataflow/new/internal/AccessPathSyntax.qll",
     "swift/ql/lib/codeql/swift/dataflow/internal/AccessPathSyntax.qll"
   ],
   "IncompleteUrlSubstringSanitization": [
@@ -584,19 +586,19 @@
   ],
   "Swift declarations test file": [
     "swift/ql/test/extractor-tests/declarations/declarations.swift",
-    "swift/ql/test/library-tests/parent/declarations.swift"
+    "swift/ql/test/library-tests/ast/declarations.swift"
   ],
   "Swift statements test file": [
     "swift/ql/test/extractor-tests/statements/statements.swift",
-    "swift/ql/test/library-tests/parent/statements.swift"
+    "swift/ql/test/library-tests/ast/statements.swift"
   ],
   "Swift expressions test file": [
     "swift/ql/test/extractor-tests/expressions/expressions.swift",
-    "swift/ql/test/library-tests/parent/expressions.swift"
+    "swift/ql/test/library-tests/ast/expressions.swift"
   ],
   "Swift patterns test file": [
     "swift/ql/test/extractor-tests/patterns/patterns.swift",
-    "swift/ql/test/library-tests/parent/patterns.swift"
+    "swift/ql/test/library-tests/ast/patterns.swift"
   ],
   "IncompleteMultiCharacterSanitization JS/Ruby": [
     "javascript/ql/lib/semmle/javascript/security/IncompleteMultiCharacterSanitizationQuery.qll",

cpp/autobuilder/Semmle.Autobuild.Cpp.Tests/BuildScripts.cs

@@ -299,7 +299,7 @@ namespace Semmle.Autobuild.Cpp.Tests
         {
             Actions.RunProcess[@"cmd.exe /C nuget restore C:\Project\test.sln -DisableParallelProcessing"] = 1;
             Actions.RunProcess[@"cmd.exe /C C:\Project\.nuget\nuget.exe restore C:\Project\test.sln -DisableParallelProcessing"] = 0;
-            Actions.RunProcess[@"cmd.exe /C CALL ^""C:\Program Files ^(x86^)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat^"" && set Platform=&& type NUL && C:\odasa\tools\odasa index --auto msbuild C:\Project\test.sln /p:UseSharedCompilation=false /t:rebuild /p:Platform=""x86"" /p:Configuration=""Release"" /p:MvcBuildViews=true"] = 0;
+            Actions.RunProcess[@"cmd.exe /C CALL ^""C:\Program Files ^(x86^)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat^"" && set Platform=&& type NUL && C:\odasa\tools\odasa index --auto msbuild C:\Project\test.sln /t:rebuild /p:Platform=""x86"" /p:Configuration=""Release"" /p:MvcBuildViews=true"] = 0;
             Actions.RunProcessOut[@"C:\Program Files (x86)\Microsoft Visual Studio\Installer\vswhere.exe -prerelease -legacy -property installationPath"] = "";
             Actions.RunProcess[@"C:\Program Files (x86)\Microsoft Visual Studio\Installer\vswhere.exe -prerelease -legacy -property installationPath"] = 1;
             Actions.RunProcess[@"C:\Program Files (x86)\Microsoft Visual Studio\Installer\vswhere.exe -prerelease -legacy -property installationVersion"] = 0;

cpp/downgrades/625f706f2a44ae8dc3fc168bfe2637e65c30b012/exprs.ql

@@ -0,0 +1,17 @@
+class Expr extends @expr {
+  string toString() { none() }
+}
+
+class Location extends @location_expr {
+  string toString() { none() }
+}
+
+predicate isExprWithNewBuiltin(Expr expr) {
+  exists(int kind | exprs(expr, kind, _) | 336 <= kind and kind <= 362)
+}
+
+from Expr expr, int kind, int kind_new, Location location
+where
+  exprs(expr, kind, location) and
+  if isExprWithNewBuiltin(expr) then kind_new = 1 else kind_new = kind
+select expr, kind_new, location

cpp/downgrades/625f706f2a44ae8dc3fc168bfe2637e65c30b012/upgrade.properties

@@ -0,0 +1,3 @@
+description: Add new builtin operations
+compatibility: partial
+exprs.rel: run exprs.qlo

cpp/ql/lib/change-notes/2022-09-06-additional-builtin-support.md

@@ -0,0 +1,4 @@
+---
+category: feature
+---
+* Added subclasses of `BuiltInOperations` for `__is_same`, `__is_function`, `__is_layout_compatible`, `__is_pointer_interconvertible_base_of`, `__is_array`, `__array_rank`, `__array_extent`, `__is_arithmetic`, `__is_complete_type`, `__is_compound`, `__is_const`, `__is_floating_point`, `__is_fundamental`, `__is_integral`, `__is_lvalue_reference`, `__is_member_function_pointer`, `__is_member_object_pointer`, `__is_member_pointer`, `__is_object`, `__is_pointer`, `__is_reference`, `__is_rvalue_reference`, `__is_scalar`, `__is_signed`, `__is_unsigned`, `__is_void`, and `__is_volatile`.

cpp/ql/lib/change-notes/2022-09-08-implicit-read-flowstates.md

@@ -0,0 +1,4 @@
+---
+category: fix
+---
+* Fixed an issue in the taint tracking analysis where implicit reads were not allowed by default in sinks or additional taint steps that used flow states.

cpp/ql/lib/change-notes/2022-09-12-uppercase.md

@@ -0,0 +1,5 @@
+---
+category: deprecated
+---
+* Some classes/modules with upper-case acronyms in their name have been renamed to follow our style-guide. 
+  The old name still exists as a deprecated alias.

cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll

@@ -0,0 +1,165 @@
+import experimental.semmle.code.cpp.ir.dataflow.DataFlow
+import experimental.semmle.code.cpp.ir.dataflow.DataFlow2
+
+module ProductFlow {
+  abstract class Configuration extends string {
+    bindingset[this]
+    Configuration() { any() }
+
+    /**
+     * Holds if `(source1, source2)` is a relevant data flow source.
+     *
+     * `source1` and `source2` must belong to the same callable.
+     */
+    predicate isSourcePair(DataFlow::Node source1, DataFlow::Node source2) { none() }
+
+    /**
+     * Holds if `(source1, source2)` is a relevant data flow source with initial states `state1`
+     * and `state2`, respectively.
+     *
+     * `source1` and `source2` must belong to the same callable.
+     */
+    predicate isSourcePair(
+      DataFlow::Node source1, string state1, DataFlow::Node source2, string state2
+    ) {
+      state1 = "" and
+      state2 = "" and
+      this.isSourcePair(source1, source2)
+    }
+
+    /**
+     * Holds if `(sink1, sink2)` is a relevant data flow sink.
+     *
+     * `sink1` and `sink2` must belong to the same callable.
+     */
+    predicate isSinkPair(DataFlow::Node sink1, DataFlow::Node sink2) { none() }
+
+    /**
+     * Holds if `(sink1, sink2)` is a relevant data flow sink with final states `state1`
+     * and `state2`, respectively.
+     *
+     * `sink1` and `sink2` must belong to the same callable.
+     */
+    predicate isSinkPair(
+      DataFlow::Node sink1, DataFlow::FlowState state1, DataFlow::Node sink2,
+      DataFlow::FlowState state2
+    ) {
+      state1 = "" and
+      state2 = "" and
+      this.isSinkPair(sink1, sink2)
+    }
+
+    predicate hasFlowPath(
+      DataFlow::PathNode source1, DataFlow2::PathNode source2, DataFlow::PathNode sink1,
+      DataFlow2::PathNode sink2
+    ) {
+      reachable(this, source1, source2, sink1, sink2)
+    }
+  }
+
+  private import Internal
+
+  module Internal {
+    class Conf1 extends DataFlow::Configuration {
+      Conf1() { this = "Conf1" }
+
+      override predicate isSource(DataFlow::Node source, string state) {
+        exists(Configuration conf | conf.isSourcePair(source, state, _, _))
+      }
+
+      override predicate isSink(DataFlow::Node sink, string state) {
+        exists(Configuration conf | conf.isSinkPair(sink, state, _, _))
+      }
+    }
+
+    class Conf2 extends DataFlow2::Configuration {
+      Conf2() { this = "Conf2" }
+
+      override predicate isSource(DataFlow::Node source, string state) {
+        exists(Configuration conf, DataFlow::Node source1 |
+          conf.isSourcePair(source1, _, source, state) and
+          any(Conf1 c).hasFlow(source1, _)
+        )
+      }
+
+      override predicate isSink(DataFlow::Node sink, string state) {
+        exists(Configuration conf, DataFlow::Node sink1 |
+          conf.isSinkPair(sink1, _, sink, state) and any(Conf1 c).hasFlow(_, sink1)
+        )
+      }
+    }
+  }
+
+  private predicate reachableInterprocEntry(
+    Configuration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2,
+    DataFlow::PathNode node1, DataFlow2::PathNode node2
+  ) {
+    conf.isSourcePair(node1.getNode(), _, node2.getNode(), _) and
+    node1 = source1 and
+    node2 = source2
+    or
+    exists(
+      DataFlow::PathNode midEntry1, DataFlow2::PathNode midEntry2, DataFlow::PathNode midExit1,
+      DataFlow2::PathNode midExit2
+    |
+      reachableInterprocEntry(conf, source1, source2, midEntry1, midEntry2) and
+      interprocEdgePair(midExit1, midExit2, node1, node2) and
+      localPathStep1*(midEntry1, midExit1) and
+      localPathStep2*(midEntry2, midExit2)
+    )
+  }
+
+  private predicate localPathStep1(DataFlow::PathNode pred, DataFlow::PathNode succ) {
+    DataFlow::PathGraph::edges(pred, succ) and
+    pragma[only_bind_out](pred.getNode().getEnclosingCallable()) =
+      pragma[only_bind_out](succ.getNode().getEnclosingCallable())
+  }
+
+  private predicate localPathStep2(DataFlow2::PathNode pred, DataFlow2::PathNode succ) {
+    DataFlow2::PathGraph::edges(pred, succ) and
+    pragma[only_bind_out](pred.getNode().getEnclosingCallable()) =
+      pragma[only_bind_out](succ.getNode().getEnclosingCallable())
+  }
+
+  pragma[nomagic]
+  private predicate interprocEdge1(
+    Declaration predDecl, Declaration succDecl, DataFlow::PathNode pred1, DataFlow::PathNode succ1
+  ) {
+    DataFlow::PathGraph::edges(pred1, succ1) and
+    predDecl != succDecl and
+    pred1.getNode().getEnclosingCallable() = predDecl and
+    succ1.getNode().getEnclosingCallable() = succDecl
+  }
+
+  pragma[nomagic]
+  private predicate interprocEdge2(
+    Declaration predDecl, Declaration succDecl, DataFlow2::PathNode pred2, DataFlow2::PathNode succ2
+  ) {
+    DataFlow2::PathGraph::edges(pred2, succ2) and
+    predDecl != succDecl and
+    pred2.getNode().getEnclosingCallable() = predDecl and
+    succ2.getNode().getEnclosingCallable() = succDecl
+  }
+
+  private predicate interprocEdgePair(
+    DataFlow::PathNode pred1, DataFlow2::PathNode pred2, DataFlow::PathNode succ1,
+    DataFlow2::PathNode succ2
+  ) {
+    exists(Declaration predDecl, Declaration succDecl |
+      interprocEdge1(predDecl, succDecl, pred1, succ1) and
+      interprocEdge2(predDecl, succDecl, pred2, succ2)
+    )
+  }
+
+  private predicate reachable(
+    Configuration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2,
+    DataFlow::PathNode sink1, DataFlow2::PathNode sink2
+  ) {
+    exists(DataFlow::PathNode mid1, DataFlow2::PathNode mid2 |
+      reachableInterprocEntry(conf, source1, source2, mid1, mid2) and
+      conf.isSinkPair(sink1.getNode(), _, sink2.getNode(), _) and
+      localPathStep1*(mid1, sink1) and
+      localPathStep2*(mid2, sink2)
+    )
+  }
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/DataFlow.qll

@@ -0,0 +1,26 @@
+/**
+ * Provides a library for local (intra-procedural) and global (inter-procedural)
+ * data flow analysis: deciding whether data can flow from a _source_ to a
+ * _sink_. This library differs from the one in `semmle.code.cpp.dataflow` in that
+ * this library uses the IR (Intermediate Representation) library, which provides
+ * a more precise semantic representation of the program, whereas the other dataflow
+ * library uses the more syntax-oriented ASTs. This library should provide more accurate
+ * results than the AST-based library in most scenarios.
+ *
+ * Unless configured otherwise, _flow_ means that the exact value of
+ * the source may reach the sink. We do not track flow across pointer
+ * dereferences or array indexing.
+ *
+ * To use global (interprocedural) data flow, extend the class
+ * `DataFlow::Configuration` as documented on that class. To use local
+ * (intraprocedural) data flow between expressions, call
+ * `DataFlow::localExprFlow`. For more general cases of local data flow, call
+ * `DataFlow::localFlow` or `DataFlow::localFlowStep` with arguments of type
+ * `DataFlow::Node`.
+ */
+
+import cpp
+
+module DataFlow {
+  import experimental.semmle.code.cpp.ir.dataflow.internal.DataFlowImpl
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/DataFlow2.qll

@@ -0,0 +1,16 @@
+/**
+ * Provides a `DataFlow2` module, which is a copy of the `DataFlow` module. Use
+ * this class when data-flow configurations must depend on each other. Two
+ * classes extending `DataFlow::Configuration` should never depend on each
+ * other, but one of them should instead depend on a
+ * `DataFlow2::Configuration`, a `DataFlow3::Configuration`, or a
+ * `DataFlow4::Configuration`.
+ *
+ * See `semmle.code.cpp.ir.dataflow.DataFlow` for the full documentation.
+ */
+
+import cpp
+
+module DataFlow2 {
+  import experimental.semmle.code.cpp.ir.dataflow.internal.DataFlowImpl2
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/DataFlow3.qll

@@ -0,0 +1,16 @@
+/**
+ * Provides a `DataFlow3` module, which is a copy of the `DataFlow` module. Use
+ * this class when data-flow configurations must depend on each other. Two
+ * classes extending `DataFlow::Configuration` should never depend on each
+ * other, but one of them should instead depend on a
+ * `DataFlow2::Configuration`, a `DataFlow3::Configuration`, or a
+ * `DataFlow4::Configuration`.
+ *
+ * See `semmle.code.cpp.ir.dataflow.DataFlow` for the full documentation.
+ */
+
+import cpp
+
+module DataFlow3 {
+  import experimental.semmle.code.cpp.ir.dataflow.internal.DataFlowImpl3
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/DataFlow4.qll

@@ -0,0 +1,16 @@
+/**
+ * Provides a `DataFlow4` module, which is a copy of the `DataFlow` module. Use
+ * this class when data-flow configurations must depend on each other. Two
+ * classes extending `DataFlow::Configuration` should never depend on each
+ * other, but one of them should instead depend on a
+ * `DataFlow2::Configuration`, a `DataFlow3::Configuration`, or a
+ * `DataFlow4::Configuration`.
+ *
+ * See `semmle.code.cpp.ir.dataflow.DataFlow` for the full documentation.
+ */
+
+import cpp
+
+module DataFlow4 {
+  import experimental.semmle.code.cpp.ir.dataflow.internal.DataFlowImpl4
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/ResolveCall.qll

@@ -0,0 +1,23 @@
+/**
+ * Provides a predicate for non-contextual virtual dispatch and function
+ * pointer resolution.
+ */
+
+import cpp
+private import semmle.code.cpp.ir.ValueNumbering
+private import internal.DataFlowDispatch
+private import semmle.code.cpp.ir.IR
+
+/**
+ * Resolve potential target function(s) for `call`.
+ *
+ * If `call` is a call through a function pointer (`ExprCall`) or its target is
+ * a virtual member function, simple data flow analysis is performed in order
+ * to identify the possible target(s).
+ */
+Function resolveCall(Call call) {
+  exists(CallInstruction callInstruction |
+    callInstruction.getAst() = call and
+    result = viableCallable(callInstruction)
+  )
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/TaintTracking.qll

@@ -0,0 +1,23 @@
+/**
+ * Provides classes for performing local (intra-procedural) and
+ * global (inter-procedural) taint-tracking analyses.
+ *
+ * We define _taint propagation_ informally to mean that a substantial part of
+ * the information from the source is preserved at the sink. For example, taint
+ * propagates from `x` to `x + 100`, but it does not propagate from `x` to `x >
+ * 100` since we consider a single bit of information to be too little.
+ *
+ * To use global (interprocedural) taint tracking, extend the class
+ * `TaintTracking::Configuration` as documented on that class. To use local
+ * (intraprocedural) taint tracking between expressions, call
+ * `TaintTracking::localExprTaint`. For more general cases of local taint
+ * tracking, call `TaintTracking::localTaint` or
+ * `TaintTracking::localTaintStep` with arguments of type `DataFlow::Node`.
+ */
+
+import semmle.code.cpp.ir.dataflow.DataFlow
+import semmle.code.cpp.ir.dataflow.DataFlow2
+
+module TaintTracking {
+  import experimental.semmle.code.cpp.ir.dataflow.internal.tainttracking1.TaintTrackingImpl
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/TaintTracking2.qll

@@ -0,0 +1,15 @@
+/**
+ * Provides a `TaintTracking2` module, which is a copy of the `TaintTracking`
+ * module. Use this class when data-flow configurations or taint-tracking
+ * configurations must depend on each other. Two classes extending
+ * `DataFlow::Configuration` should never depend on each other, but one of them
+ * should instead depend on a `DataFlow2::Configuration`, a
+ * `DataFlow3::Configuration`, or a `DataFlow4::Configuration`. The
+ * `TaintTracking::Configuration` class extends `DataFlow::Configuration`, and
+ * `TaintTracking2::Configuration` extends `DataFlow2::Configuration`.
+ *
+ * See `semmle.code.cpp.ir.dataflow.TaintTracking` for the full documentation.
+ */
+module TaintTracking2 {
+  import experimental.semmle.code.cpp.ir.dataflow.internal.tainttracking2.TaintTrackingImpl
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/TaintTracking3.qll

@@ -0,0 +1,15 @@
+/**
+ * Provides a `TaintTracking3` module, which is a copy of the `TaintTracking`
+ * module. Use this class when data-flow configurations or taint-tracking
+ * configurations must depend on each other. Two classes extending
+ * `DataFlow::Configuration` should never depend on each other, but one of them
+ * should instead depend on a `DataFlow2::Configuration`, a
+ * `DataFlow3::Configuration`, or a `DataFlow4::Configuration`. The
+ * `TaintTracking::Configuration` class extends `DataFlow::Configuration`, and
+ * `TaintTracking2::Configuration` extends `DataFlow2::Configuration`.
+ *
+ * See `semmle.code.cpp.ir.dataflow.TaintTracking` for the full documentation.
+ */
+module TaintTracking3 {
+  import experimental.semmle.code.cpp.ir.dataflow.internal.tainttracking3.TaintTrackingImpl
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowDispatch.qll

@@ -0,0 +1,273 @@
+private import cpp
+private import semmle.code.cpp.ir.IR
+private import experimental.semmle.code.cpp.ir.dataflow.DataFlow
+private import experimental.semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
+private import experimental.semmle.code.cpp.ir.dataflow.internal.DataFlowUtil
+private import DataFlowImplCommon as DataFlowImplCommon
+
+/**
+ * Gets a function that might be called by `call`.
+ */
+cached
+Function viableCallable(CallInstruction call) {
+  DataFlowImplCommon::forceCachingInSameStage() and
+  result = call.getStaticCallTarget()
+  or
+  // If the target of the call does not have a body in the snapshot, it might
+  // be because the target is just a header declaration, and the real target
+  // will be determined at run time when the caller and callee are linked
+  // together by the operating system's dynamic linker. In case a _unique_
+  // function with the right signature is present in the database, we return
+  // that as a potential callee.
+  exists(string qualifiedName, int nparams |
+    callSignatureWithoutBody(qualifiedName, nparams, call) and
+    functionSignatureWithBody(qualifiedName, nparams, result) and
+    strictcount(Function other | functionSignatureWithBody(qualifiedName, nparams, other)) = 1
+  )
+  or
+  // Virtual dispatch
+  result = call.(VirtualDispatch::DataSensitiveCall).resolve()
+}
+
+/**
+ * Provides virtual dispatch support compatible with the original
+ * implementation of `semmle.code.cpp.security.TaintTracking`.
+ */
+private module VirtualDispatch {
+  /** A call that may dispatch differently depending on the qualifier value. */
+  abstract class DataSensitiveCall extends DataFlowCall {
+    /**
+     * Gets the node whose value determines the target of this call. This node
+     * could be the qualifier of a virtual dispatch or the function-pointer
+     * expression in a call to a function pointer. What they have in common is
+     * that we need to find out which data flows there, and then it's up to the
+     * `resolve` predicate to stitch that information together and resolve the
+     * call.
+     */
+    abstract DataFlow::Node getDispatchValue();
+
+    /** Gets a candidate target for this call. */
+    abstract Function resolve();
+
+    /**
+     * Whether `src` can flow to this call.
+     *
+     * Searches backwards from `getDispatchValue()` to `src`. The `allowFromArg`
+     * parameter is true when the search is allowed to continue backwards into
+     * a parameter; non-recursive callers should pass `_` for `allowFromArg`.
+     */
+    predicate flowsFrom(DataFlow::Node src, boolean allowFromArg) {
+      src = this.getDispatchValue() and allowFromArg = true
+      or
+      exists(DataFlow::Node other, boolean allowOtherFromArg |
+        this.flowsFrom(other, allowOtherFromArg)
+      |
+        // Call argument
+        exists(DataFlowCall call, Position i |
+          other
+              .(DataFlow::ParameterNode)
+              .isParameterOf(pragma[only_bind_into](call).getStaticCallTarget(), i) and
+          src.(ArgumentNode).argumentOf(call, pragma[only_bind_into](pragma[only_bind_out](i)))
+        ) and
+        allowOtherFromArg = true and
+        allowFromArg = true
+        or
+        // Call return
+        exists(DataFlowCall call, ReturnKind returnKind |
+          other = getAnOutNode(call, returnKind) and
+          returnNodeWithKindAndEnclosingCallable(src, returnKind, call.getStaticCallTarget())
+        ) and
+        allowFromArg = false
+        or
+        // Local flow
+        DataFlow::localFlowStep(src, other) and
+        allowFromArg = allowOtherFromArg
+        or
+        // Flow from global variable to load.
+        exists(LoadInstruction load, GlobalOrNamespaceVariable var |
+          var = src.asVariable() and
+          other.asInstruction() = load and
+          addressOfGlobal(load.getSourceAddress(), var) and
+          // The `allowFromArg` concept doesn't play a role when `src` is a
+          // global variable, so we just set it to a single arbitrary value for
+          // performance.
+          allowFromArg = true
+        )
+        or
+        // Flow from store to global variable.
+        exists(StoreInstruction store, GlobalOrNamespaceVariable var |
+          var = other.asVariable() and
+          store = src.asInstruction() and
+          storeIntoGlobal(store, var) and
+          // Setting `allowFromArg` to `true` like in the base case means we
+          // treat a store to a global variable like the dispatch itself: flow
+          // may come from anywhere.
+          allowFromArg = true
+        )
+      )
+    }
+  }
+
+  pragma[noinline]
+  private predicate storeIntoGlobal(StoreInstruction store, GlobalOrNamespaceVariable var) {
+    addressOfGlobal(store.getDestinationAddress(), var)
+  }
+
+  /** Holds if `addressInstr` is an instruction that produces the address of `var`. */
+  private predicate addressOfGlobal(Instruction addressInstr, GlobalOrNamespaceVariable var) {
+    // Access directly to the global variable
+    addressInstr.(VariableAddressInstruction).getAstVariable() = var
+    or
+    // Access to a field on a global union
+    exists(FieldAddressInstruction fa |
+      fa = addressInstr and
+      fa.getObjectAddress().(VariableAddressInstruction).getAstVariable() = var and
+      fa.getField().getDeclaringType() instanceof Union
+    )
+  }
+
+  /**
+   * A ReturnNode with its ReturnKind and its enclosing callable.
+   *
+   * Used to fix a join ordering issue in flowsFrom.
+   */
+  pragma[noinline]
+  private predicate returnNodeWithKindAndEnclosingCallable(
+    ReturnNode node, ReturnKind kind, DataFlowCallable callable
+  ) {
+    node.getKind() = kind and
+    node.getEnclosingCallable() = callable
+  }
+
+  /** Call through a function pointer. */
+  private class DataSensitiveExprCall extends DataSensitiveCall {
+    DataSensitiveExprCall() { not exists(this.getStaticCallTarget()) }
+
+    override DataFlow::Node getDispatchValue() { result.asInstruction() = this.getCallTarget() }
+
+    override Function resolve() {
+      exists(FunctionInstruction fi |
+        this.flowsFrom(DataFlow::instructionNode(fi), _) and
+        result = fi.getFunctionSymbol()
+      ) and
+      (
+        this.getNumberOfArguments() <= result.getEffectiveNumberOfParameters() and
+        this.getNumberOfArguments() >= result.getEffectiveNumberOfParameters()
+        or
+        result.isVarargs()
+      )
+    }
+  }
+
+  /** Call to a virtual function. */
+  private class DataSensitiveOverriddenFunctionCall extends DataSensitiveCall {
+    DataSensitiveOverriddenFunctionCall() {
+      exists(this.getStaticCallTarget().(VirtualFunction).getAnOverridingFunction())
+    }
+
+    override DataFlow::Node getDispatchValue() { result.asInstruction() = this.getThisArgument() }
+
+    override MemberFunction resolve() {
+      exists(Class overridingClass |
+        this.overrideMayAffectCall(overridingClass, result) and
+        this.hasFlowFromCastFrom(overridingClass)
+      )
+    }
+
+    /**
+     * Holds if `this` is a virtual function call whose static target is
+     * overridden by `overridingFunction` in `overridingClass`.
+     */
+    pragma[noinline]
+    private predicate overrideMayAffectCall(Class overridingClass, MemberFunction overridingFunction) {
+      overridingFunction.getAnOverriddenFunction+() = this.getStaticCallTarget().(VirtualFunction) and
+      overridingFunction.getDeclaringType() = overridingClass
+    }
+
+    /**
+     * Holds if the qualifier of `this` has flow from an upcast from
+     * `derivedClass`.
+     */
+    pragma[noinline]
+    private predicate hasFlowFromCastFrom(Class derivedClass) {
+      exists(ConvertToBaseInstruction toBase |
+        this.flowsFrom(DataFlow::instructionNode(toBase), _) and
+        derivedClass = toBase.getDerivedClass()
+      )
+    }
+  }
+}
+
+/**
+ * Holds if `f` is a function with a body that has name `qualifiedName` and
+ * `nparams` parameter count. See `functionSignature`.
+ */
+private predicate functionSignatureWithBody(string qualifiedName, int nparams, Function f) {
+  functionSignature(f, qualifiedName, nparams) and
+  exists(f.getBlock())
+}
+
+/**
+ * Holds if the target of `call` is a function _with no definition_ that has
+ * name `qualifiedName` and `nparams` parameter count. See `functionSignature`.
+ */
+pragma[noinline]
+private predicate callSignatureWithoutBody(string qualifiedName, int nparams, CallInstruction call) {
+  exists(Function target |
+    target = call.getStaticCallTarget() and
+    not exists(target.getBlock()) and
+    functionSignature(target, qualifiedName, nparams)
+  )
+}
+
+/**
+ * Holds if `f` has name `qualifiedName` and `nparams` parameter count. This is
+ * an approximation of its signature for the purpose of matching functions that
+ * might be the same across link targets.
+ */
+private predicate functionSignature(Function f, string qualifiedName, int nparams) {
+  qualifiedName = f.getQualifiedName() and
+  nparams = f.getNumberOfParameters() and
+  not f.isStatic()
+}
+
+/**
+ * Holds if the set of viable implementations that can be called by `call`
+ * might be improved by knowing the call context.
+ */
+predicate mayBenefitFromCallContext(CallInstruction call, Function f) {
+  mayBenefitFromCallContext(call, f, _)
+}
+
+/**
+ * Holds if `call` is a call through a function pointer, and the pointer
+ * value is given as the `arg`'th argument to `f`.
+ */
+private predicate mayBenefitFromCallContext(
+  VirtualDispatch::DataSensitiveCall call, Function f, int arg
+) {
+  f = pragma[only_bind_out](call).getEnclosingCallable() and
+  exists(InitializeParameterInstruction init |
+    not exists(call.getStaticCallTarget()) and
+    init.getEnclosingFunction() = f and
+    call.flowsFrom(DataFlow::instructionNode(init), _) and
+    init.getParameter().getIndex() = arg
+  )
+}
+
+/**
+ * Gets a viable dispatch target of `call` in the context `ctx`. This is
+ * restricted to those `call`s for which a context might make a difference.
+ */
+Function viableImplInCallContext(CallInstruction call, CallInstruction ctx) {
+  result = viableCallable(call) and
+  exists(int i, Function f |
+    mayBenefitFromCallContext(pragma[only_bind_into](call), f, i) and
+    f = ctx.getStaticCallTarget() and
+    result = ctx.getArgument(i).getUnconvertedResultExpression().(FunctionAccess).getTarget()
+  )
+}
+
+/** Holds if arguments at position `apos` match parameters at position `ppos`. */
+pragma[inline]
+predicate parameterMatch(ParameterPosition ppos, ArgumentPosition apos) { ppos = apos }

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImplConsistency.qll

@@ -0,0 +1,212 @@
+/**
+ * Provides consistency queries for checking invariants in the language-specific
+ * data-flow classes and predicates.
+ */
+
+private import DataFlowImplSpecific::Private
+private import DataFlowImplSpecific::Public
+private import tainttracking1.TaintTrackingParameter::Private
+private import tainttracking1.TaintTrackingParameter::Public
+
+module Consistency {
+  private newtype TConsistencyConfiguration = MkConsistencyConfiguration()
+
+  /** A class for configuring the consistency queries. */
+  class ConsistencyConfiguration extends TConsistencyConfiguration {
+    string toString() { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `uniqueEnclosingCallable`. */
+    predicate uniqueEnclosingCallableExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `uniqueNodeLocation`. */
+    predicate uniqueNodeLocationExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `missingLocation`. */
+    predicate missingLocationExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `postWithInFlow`. */
+    predicate postWithInFlowExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `argHasPostUpdate`. */
+    predicate argHasPostUpdateExclude(ArgumentNode n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `reverseRead`. */
+    predicate reverseReadExclude(Node n) { none() }
+  }
+
+  private class RelevantNode extends Node {
+    RelevantNode() {
+      this instanceof ArgumentNode or
+      this instanceof ParameterNode or
+      this instanceof ReturnNode or
+      this = getAnOutNode(_, _) or
+      simpleLocalFlowStep(this, _) or
+      simpleLocalFlowStep(_, this) or
+      jumpStep(this, _) or
+      jumpStep(_, this) or
+      storeStep(this, _, _) or
+      storeStep(_, _, this) or
+      readStep(this, _, _) or
+      readStep(_, _, this) or
+      defaultAdditionalTaintStep(this, _) or
+      defaultAdditionalTaintStep(_, this)
+    }
+  }
+
+  query predicate uniqueEnclosingCallable(Node n, string msg) {
+    exists(int c |
+      n instanceof RelevantNode and
+      c = count(nodeGetEnclosingCallable(n)) and
+      c != 1 and
+      not any(ConsistencyConfiguration conf).uniqueEnclosingCallableExclude(n) and
+      msg = "Node should have one enclosing callable but has " + c + "."
+    )
+  }
+
+  query predicate uniqueType(Node n, string msg) {
+    exists(int c |
+      n instanceof RelevantNode and
+      c = count(getNodeType(n)) and
+      c != 1 and
+      msg = "Node should have one type but has " + c + "."
+    )
+  }
+
+  query predicate uniqueNodeLocation(Node n, string msg) {
+    exists(int c |
+      c =
+        count(string filepath, int startline, int startcolumn, int endline, int endcolumn |
+          n.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
+        ) and
+      c != 1 and
+      not any(ConsistencyConfiguration conf).uniqueNodeLocationExclude(n) and
+      msg = "Node should have one location but has " + c + "."
+    )
+  }
+
+  query predicate missingLocation(string msg) {
+    exists(int c |
+      c =
+        strictcount(Node n |
+          not exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
+            n.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
+          ) and
+          not any(ConsistencyConfiguration conf).missingLocationExclude(n)
+        ) and
+      msg = "Nodes without location: " + c
+    )
+  }
+
+  query predicate uniqueNodeToString(Node n, string msg) {
+    exists(int c |
+      c = count(n.toString()) and
+      c != 1 and
+      msg = "Node should have one toString but has " + c + "."
+    )
+  }
+
+  query predicate missingToString(string msg) {
+    exists(int c |
+      c = strictcount(Node n | not exists(n.toString())) and
+      msg = "Nodes without toString: " + c
+    )
+  }
+
+  query predicate parameterCallable(ParameterNode p, string msg) {
+    exists(DataFlowCallable c | isParameterNode(p, c, _) and c != nodeGetEnclosingCallable(p)) and
+    msg = "Callable mismatch for parameter."
+  }
+
+  query predicate localFlowIsLocal(Node n1, Node n2, string msg) {
+    simpleLocalFlowStep(n1, n2) and
+    nodeGetEnclosingCallable(n1) != nodeGetEnclosingCallable(n2) and
+    msg = "Local flow step does not preserve enclosing callable."
+  }
+
+  private DataFlowType typeRepr() { result = getNodeType(_) }
+
+  query predicate compatibleTypesReflexive(DataFlowType t, string msg) {
+    t = typeRepr() and
+    not compatibleTypes(t, t) and
+    msg = "Type compatibility predicate is not reflexive."
+  }
+
+  query predicate unreachableNodeCCtx(Node n, DataFlowCall call, string msg) {
+    isUnreachableInCall(n, call) and
+    exists(DataFlowCallable c |
+      c = nodeGetEnclosingCallable(n) and
+      not viableCallable(call) = c
+    ) and
+    msg = "Call context for isUnreachableInCall is inconsistent with call graph."
+  }
+
+  query predicate localCallNodes(DataFlowCall call, Node n, string msg) {
+    (
+      n = getAnOutNode(call, _) and
+      msg = "OutNode and call does not share enclosing callable."
+      or
+      n.(ArgumentNode).argumentOf(call, _) and
+      msg = "ArgumentNode and call does not share enclosing callable."
+    ) and
+    nodeGetEnclosingCallable(n) != call.getEnclosingCallable()
+  }
+
+  // This predicate helps the compiler forget that in some languages
+  // it is impossible for a result of `getPreUpdateNode` to be an
+  // instance of `PostUpdateNode`.
+  private Node getPre(PostUpdateNode n) {
+    result = n.getPreUpdateNode()
+    or
+    none()
+  }
+
+  query predicate postIsNotPre(PostUpdateNode n, string msg) {
+    getPre(n) = n and
+    msg = "PostUpdateNode should not equal its pre-update node."
+  }
+
+  query predicate postHasUniquePre(PostUpdateNode n, string msg) {
+    exists(int c |
+      c = count(n.getPreUpdateNode()) and
+      c != 1 and
+      msg = "PostUpdateNode should have one pre-update node but has " + c + "."
+    )
+  }
+
+  query predicate uniquePostUpdate(Node n, string msg) {
+    1 < strictcount(PostUpdateNode post | post.getPreUpdateNode() = n) and
+    msg = "Node has multiple PostUpdateNodes."
+  }
+
+  query predicate postIsInSameCallable(PostUpdateNode n, string msg) {
+    nodeGetEnclosingCallable(n) != nodeGetEnclosingCallable(n.getPreUpdateNode()) and
+    msg = "PostUpdateNode does not share callable with its pre-update node."
+  }
+
+  private predicate hasPost(Node n) { exists(PostUpdateNode post | post.getPreUpdateNode() = n) }
+
+  query predicate reverseRead(Node n, string msg) {
+    exists(Node n2 | readStep(n, _, n2) and hasPost(n2) and not hasPost(n)) and
+    not any(ConsistencyConfiguration conf).reverseReadExclude(n) and
+    msg = "Origin of readStep is missing a PostUpdateNode."
+  }
+
+  query predicate argHasPostUpdate(ArgumentNode n, string msg) {
+    not hasPost(n) and
+    not any(ConsistencyConfiguration c).argHasPostUpdateExclude(n) and
+    msg = "ArgumentNode is missing PostUpdateNode."
+  }
+
+  // This predicate helps the compiler forget that in some languages
+  // it is impossible for a `PostUpdateNode` to be the target of
+  // `simpleLocalFlowStep`.
+  private predicate isPostUpdateNode(Node n) { n instanceof PostUpdateNode or none() }
+
+  query predicate postWithInFlow(Node n, string msg) {
+    isPostUpdateNode(n) and
+    not clearsContent(n, _) and
+    simpleLocalFlowStep(_, n) and
+    not any(ConsistencyConfiguration c).postWithInFlowExclude(n) and
+    msg = "PostUpdateNode should not be the target of local flow."
+  }
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImplSpecific.qll

@@ -0,0 +1,11 @@
+/**
+ * Provides IR-specific definitions for use in the data flow library.
+ */
+module Private {
+  import DataFlowPrivate
+  import DataFlowDispatch
+}
+
+module Public {
+  import DataFlowUtil
+}

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

@@ -0,0 +1,560 @@
+private import cpp as Cpp
+private import DataFlowUtil
+private import semmle.code.cpp.ir.IR
+private import DataFlowDispatch
+private import DataFlowImplConsistency
+private import semmle.code.cpp.ir.internal.IRCppLanguage
+private import SsaInternals as Ssa
+
+/** Gets the callable in which this node occurs. */
+DataFlowCallable nodeGetEnclosingCallable(Node n) { result = n.getEnclosingCallable() }
+
+/** Holds if `p` is a `ParameterNode` of `c` with position `pos`. */
+predicate isParameterNode(ParameterNode p, DataFlowCallable c, ParameterPosition pos) {
+  p.isParameterOf(c, pos)
+}
+
+/** Holds if `arg` is an `ArgumentNode` of `c` with position `pos`. */
+predicate isArgumentNode(ArgumentNode arg, DataFlowCall c, ArgumentPosition pos) {
+  arg.argumentOf(c, pos)
+}
+
+/**
+ * A data flow node that occurs as the argument of a call and is passed as-is
+ * to the callable. Instance arguments (`this` pointer) and read side effects
+ * on parameters are also included.
+ */
+abstract class ArgumentNode extends Node {
+  /**
+   * Holds if this argument occurs at the given position in the given call.
+   * The instance argument is considered to have index `-1`.
+   */
+  abstract predicate argumentOf(DataFlowCall call, ArgumentPosition pos);
+
+  /** Gets the call in which this node is an argument. */
+  DataFlowCall getCall() { this.argumentOf(result, _) }
+}
+
+/**
+ * A data flow node that occurs as the argument to a call, or an
+ * implicit `this` pointer argument.
+ */
+private class PrimaryArgumentNode extends ArgumentNode, OperandNode {
+  override ArgumentOperand op;
+
+  PrimaryArgumentNode() { exists(CallInstruction call | op = call.getAnArgumentOperand()) }
+
+  override predicate argumentOf(DataFlowCall call, ArgumentPosition pos) {
+    op = call.getArgumentOperand(pos.(DirectPosition).getIndex())
+  }
+
+  override string toStringImpl() { result = argumentOperandToString(op) }
+}
+
+private string argumentOperandToString(ArgumentOperand op) {
+  exists(Expr unconverted |
+    unconverted = op.getDef().getUnconvertedResultExpression() and
+    result = unconverted.toString()
+  )
+  or
+  // Certain instructions don't map to an unconverted result expression. For these cases
+  // we fall back to a simpler naming scheme. This can happen in IR-generated constructors.
+  not exists(op.getDef().getUnconvertedResultExpression()) and
+  (
+    result = "Argument " + op.(PositionalArgumentOperand).getIndex()
+    or
+    op instanceof ThisArgumentOperand and result = "Argument this"
+  )
+}
+
+private class SideEffectArgumentNode extends ArgumentNode, SideEffectOperandNode {
+  override predicate argumentOf(DataFlowCall dfCall, ArgumentPosition pos) {
+    this.getCallInstruction() = dfCall and
+    pos.(IndirectionPosition).getArgumentIndex() = this.getArgumentIndex() and
+    pos.(IndirectionPosition).getIndirectionIndex() = super.getIndirectionIndex()
+  }
+
+  override string toStringImpl() {
+    result = argumentOperandToString(this.getAddressOperand()) + " indirection"
+  }
+}
+
+/** A parameter position represented by an integer. */
+class ParameterPosition = Position;
+
+/** An argument position represented by an integer. */
+class ArgumentPosition = Position;
+
+class Position extends TPosition {
+  abstract string toString();
+}
+
+class DirectPosition extends Position, TDirectPosition {
+  int index;
+
+  DirectPosition() { this = TDirectPosition(index) }
+
+  override string toString() { if index = -1 then result = "this" else result = index.toString() }
+
+  int getIndex() { result = index }
+}
+
+class IndirectionPosition extends Position, TIndirectionPosition {
+  int argumentIndex;
+  int indirectionIndex;
+
+  IndirectionPosition() { this = TIndirectionPosition(argumentIndex, indirectionIndex) }
+
+  override string toString() {
+    if argumentIndex = -1
+    then if indirectionIndex > 0 then result = "this indirection" else result = "this"
+    else
+      if indirectionIndex > 0
+      then result = argumentIndex.toString() + " indirection"
+      else result = argumentIndex.toString()
+  }
+
+  int getArgumentIndex() { result = argumentIndex }
+
+  int getIndirectionIndex() { result = indirectionIndex }
+}
+
+newtype TPosition =
+  TDirectPosition(int index) { exists(any(CallInstruction c).getArgument(index)) } or
+  TIndirectionPosition(int argumentIndex, int indirectionIndex) {
+    hasOperandAndIndex(_, any(CallInstruction call).getArgumentOperand(argumentIndex),
+      indirectionIndex)
+  }
+
+private newtype TReturnKind =
+  TNormalReturnKind(int index) {
+    exists(IndirectReturnNode return |
+      return.getAddressOperand() = any(ReturnValueInstruction r).getReturnAddressOperand() and
+      index = return.getIndirectionIndex() - 1 // We subtract one because the return loads the value.
+    )
+  } or
+  TIndirectReturnKind(int argumentIndex, int indirectionIndex) {
+    exists(IndirectReturnNode return, ReturnIndirectionInstruction returnInd |
+      returnInd.hasIndex(argumentIndex) and
+      return.getAddressOperand() = returnInd.getSourceAddressOperand() and
+      indirectionIndex = return.getIndirectionIndex() - 1 // We subtract one because the return loads the value.
+    )
+  }
+
+/**
+ * A return kind. A return kind describes how a value can be returned
+ * from a callable. For C++, this is simply a function return.
+ */
+class ReturnKind extends TReturnKind {
+  /** Gets a textual representation of this return kind. */
+  abstract string toString();
+}
+
+private class NormalReturnKind extends ReturnKind, TNormalReturnKind {
+  int index;
+
+  NormalReturnKind() { this = TNormalReturnKind(index) }
+
+  override string toString() { result = "indirect return" }
+}
+
+private class IndirectReturnKind extends ReturnKind, TIndirectReturnKind {
+  int argumentIndex;
+  int indirectionIndex;
+
+  IndirectReturnKind() { this = TIndirectReturnKind(argumentIndex, indirectionIndex) }
+
+  override string toString() { result = "indirect outparam[" + argumentIndex.toString() + "]" }
+}
+
+/** A data flow node that occurs as the result of a `ReturnStmt`. */
+class ReturnNode extends Node instanceof IndirectReturnNode {
+  /** Gets the kind of this returned value. */
+  abstract ReturnKind getKind();
+}
+
+/**
+ * This predicate represents an annoying hack that we have to do. We use the
+ * `ReturnIndirectionInstruction` to determine which variables need flow back
+ * out of a function. However, the IR will unconditionally create those for a
+ * variable passed to a function even though the variable was never updated by
+ * the function. And if a function has too many `ReturnNode`s the dataflow
+ * library lowers its precision for that function by disabling field flow.
+ *
+ * So we those eliminate `ReturnNode`s that would have otherwise been created
+ * by this unconditional `ReturnIndirectionInstruction` by requiring that there
+ * must exist an SSA definition of the IR variable in the function.
+ */
+private predicate hasNonInitializeParameterDef(IRVariable v) {
+  exists(Ssa::Def def |
+    not def.getDefiningInstruction() instanceof InitializeParameterInstruction and
+    v = def.getSourceVariable().getBaseVariable().(Ssa::BaseIRVariable).getIRVariable()
+  )
+}
+
+class ReturnIndirectionNode extends IndirectReturnNode, ReturnNode {
+  override ReturnKind getKind() {
+    exists(int argumentIndex, ReturnIndirectionInstruction returnInd |
+      returnInd.hasIndex(argumentIndex) and
+      this.getAddressOperand() = returnInd.getSourceAddressOperand() and
+      result = TIndirectReturnKind(argumentIndex, this.getIndirectionIndex() - 1) and
+      hasNonInitializeParameterDef(returnInd.getIRVariable())
+    )
+    or
+    this.getAddressOperand() = any(ReturnValueInstruction r).getReturnAddressOperand() and
+    result = TNormalReturnKind(this.getIndirectionIndex() - 1)
+  }
+}
+
+private Operand fullyConvertedCallStep(Operand op) {
+  not exists(getANonConversionUse(op)) and
+  exists(Instruction instr |
+    conversionFlow(op, instr, _) and
+    result = getAUse(instr)
+  )
+}
+
+/**
+ * Gets the instruction that uses this operand, if the instruction is not
+ * ignored for dataflow purposes.
+ */
+private Instruction getUse(Operand op) {
+  result = op.getUse() and
+  not Ssa::ignoreOperand(op)
+}
+
+/** Gets a use of the instruction `instr` that is not ignored for dataflow purposes. */
+Operand getAUse(Instruction instr) {
+  result = instr.getAUse() and
+  not Ssa::ignoreOperand(result)
+}
+
+/**
+ * Gets a use of `operand` that is:
+ * - not ignored for dataflow purposes, and
+ * - not a conversion-like instruction.
+ */
+private Instruction getANonConversionUse(Operand operand) {
+  result = getUse(operand) and
+  not conversionFlow(_, result, _)
+}
+
+/**
+ * Gets the operand that represents the first use of the value of `call` following
+ * a sequnce of conversion-like instructions.
+ */
+predicate operandForfullyConvertedCall(Operand operand, CallInstruction call) {
+  exists(getANonConversionUse(operand)) and
+  (
+    operand = getAUse(call)
+    or
+    operand = fullyConvertedCallStep*(getAUse(call))
+  )
+}
+
+/**
+ * Gets the instruction that represents the first use of the value of `call` following
+ * a sequnce of conversion-like instructions.
+ *
+ * This predicate only holds if there is no suitable operand (i.e., no operand of a non-
+ * conversion instruction) to use to represent the value of `call` after conversions.
+ */
+predicate instructionForfullyConvertedCall(Instruction instr, CallInstruction call) {
+  not operandForfullyConvertedCall(_, call) and
+  (
+    // If there is no use of the call then we pick the call instruction
+    not exists(getAUse(call)) and
+    instr = call
+    or
+    // Otherwise, flow to the first non-conversion use.
+    exists(Operand operand | operand = fullyConvertedCallStep*(getAUse(call)) |
+      instr = getANonConversionUse(operand)
+    )
+  )
+}
+
+/** Holds if `node` represents the output node for `call`. */
+private predicate simpleOutNode(Node node, CallInstruction call) {
+  operandForfullyConvertedCall(node.asOperand(), call)
+  or
+  instructionForfullyConvertedCall(node.asInstruction(), call)
+}
+
+/** A data flow node that represents the output of a call. */
+class OutNode extends Node {
+  OutNode() {
+    // Return values not hidden behind indirections
+    simpleOutNode(this, _)
+    or
+    // Return values hidden behind indirections
+    this instanceof IndirectReturnOutNode
+    or
+    // Modified arguments hidden behind indirections
+    this instanceof IndirectArgumentOutNode
+  }
+
+  /** Gets the underlying call. */
+  abstract DataFlowCall getCall();
+
+  abstract ReturnKind getReturnKind();
+}
+
+private class DirectCallOutNode extends OutNode {
+  CallInstruction call;
+
+  DirectCallOutNode() { simpleOutNode(this, call) }
+
+  override DataFlowCall getCall() { result = call }
+
+  override ReturnKind getReturnKind() { result = TNormalReturnKind(0) }
+}
+
+private class IndirectCallOutNode extends OutNode, IndirectReturnOutNode {
+  override DataFlowCall getCall() { result = this.getCallInstruction() }
+
+  override ReturnKind getReturnKind() { result = TNormalReturnKind(this.getIndirectionIndex()) }
+}
+
+private class SideEffectOutNode extends OutNode, IndirectArgumentOutNode {
+  override DataFlowCall getCall() { result = this.getCallInstruction() }
+
+  override ReturnKind getReturnKind() {
+    result = TIndirectReturnKind(this.getArgumentIndex(), this.getIndirectionIndex())
+  }
+}
+
+/**
+ * Gets a node that can read the value returned from `call` with return kind
+ * `kind`.
+ */
+OutNode getAnOutNode(DataFlowCall call, ReturnKind kind) {
+  result.getCall() = call and
+  result.getReturnKind() = kind
+}
+
+/**
+ * Holds if data can flow from `node1` to `node2` in a way that loses the
+ * calling context. For example, this would happen with flow through a
+ * global or static variable.
+ */
+predicate jumpStep(Node n1, Node n2) {
+  exists(Cpp::GlobalOrNamespaceVariable v |
+    v =
+      n1.asInstruction()
+          .(StoreInstruction)
+          .getResultAddress()
+          .(VariableAddressInstruction)
+          .getAstVariable() and
+    v = n2.asVariable()
+    or
+    v =
+      n2.asInstruction()
+          .(LoadInstruction)
+          .getSourceAddress()
+          .(VariableAddressInstruction)
+          .getAstVariable() and
+    v = n1.asVariable()
+  )
+}
+
+/**
+ * Holds if data can flow from `node1` to `node2` via an assignment to `f`.
+ * Thus, `node2` references an object with a field `f` that contains the
+ * value of `node1`.
+ */
+predicate storeStep(Node node1, Content c, PostFieldUpdateNode node2) {
+  exists(int indirectionIndex1, int numberOfLoads, StoreInstruction store |
+    nodeHasInstruction(node1, store, pragma[only_bind_into](indirectionIndex1)) and
+    node2.getIndirectionIndex() = 0 and
+    numberOfLoadsFromOperand(node2.getFieldAddress(), store.getDestinationAddressOperand(),
+      numberOfLoads)
+  |
+    exists(FieldContent fc | fc = c |
+      fc.getField() = node2.getUpdatedField() and
+      fc.getIndirectionIndex() = 1 + indirectionIndex1 + numberOfLoads
+    )
+    or
+    exists(UnionContent uc | uc = c |
+      uc.getAField() = node2.getUpdatedField() and
+      uc.getIndirectionIndex() = 1 + indirectionIndex1 + numberOfLoads
+    )
+  )
+}
+
+/**
+ * Holds if `operandFrom` flows to `operandTo` using a sequence of conversion-like
+ * operations and exactly `n` `LoadInstruction` operations.
+ */
+private predicate numberOfLoadsFromOperandRec(Operand operandFrom, Operand operandTo, int ind) {
+  exists(LoadInstruction load | load.getSourceAddressOperand() = operandFrom |
+    operandTo = operandFrom and ind = 0
+    or
+    numberOfLoadsFromOperand(load.getAUse(), operandTo, ind - 1)
+  )
+  or
+  exists(Operand op, Instruction instr |
+    instr = op.getDef() and
+    conversionFlow(operandFrom, instr, _) and
+    numberOfLoadsFromOperand(op, operandTo, ind)
+  )
+}
+
+/**
+ * Holds if `operandFrom` flows to `operandTo` using a sequence of conversion-like
+ * operations and exactly `n` `LoadInstruction` operations.
+ */
+private predicate numberOfLoadsFromOperand(Operand operandFrom, Operand operandTo, int n) {
+  numberOfLoadsFromOperandRec(operandFrom, operandTo, n)
+  or
+  not any(LoadInstruction load).getSourceAddressOperand() = operandFrom and
+  not conversionFlow(operandFrom, _, _) and
+  operandFrom = operandTo and
+  n = 0
+}
+
+// Needed to join on both an operand and an index at the same time.
+pragma[noinline]
+predicate nodeHasOperand(Node node, Operand operand, int indirectionIndex) {
+  node.asOperand() = operand and indirectionIndex = 0
+  or
+  hasOperandAndIndex(node, operand, indirectionIndex)
+}
+
+// Needed to join on both an instruction and an index at the same time.
+pragma[noinline]
+predicate nodeHasInstruction(Node node, Instruction instr, int indirectionIndex) {
+  node.asInstruction() = instr and indirectionIndex = 0
+  or
+  hasInstructionAndIndex(node, instr, indirectionIndex)
+}
+
+/**
+ * Holds if data can flow from `node1` to `node2` via a read of `f`.
+ * Thus, `node1` references an object with a field `f` whose value ends up in
+ * `node2`.
+ */
+predicate readStep(Node node1, Content c, Node node2) {
+  exists(FieldAddress fa1, Operand operand, int numberOfLoads, int indirectionIndex2 |
+    nodeHasOperand(node2, operand, indirectionIndex2) and
+    nodeHasOperand(node1, fa1.getObjectAddressOperand(), _) and
+    numberOfLoadsFromOperand(fa1, operand, numberOfLoads)
+  |
+    exists(FieldContent fc | fc = c |
+      fc.getField() = fa1.getField() and
+      fc.getIndirectionIndex() = indirectionIndex2 + numberOfLoads
+    )
+    or
+    exists(UnionContent uc | uc = c |
+      uc.getAField() = fa1.getField() and
+      uc.getIndirectionIndex() = indirectionIndex2 + numberOfLoads
+    )
+  )
+}
+
+/**
+ * Holds if values stored inside content `c` are cleared at node `n`.
+ */
+predicate clearsContent(Node n, Content c) {
+  none() // stub implementation
+}
+
+/**
+ * Holds if the value that is being tracked is expected to be stored inside content `c`
+ * at node `n`.
+ */
+predicate expectsContent(Node n, ContentSet c) { none() }
+
+/** Gets the type of `n` used for type pruning. */
+IRType getNodeType(Node n) {
+  suppressUnusedNode(n) and
+  result instanceof IRVoidType // stub implementation
+}
+
+/** Gets a string representation of a type returned by `getNodeType`. */
+string ppReprType(IRType t) { none() } // stub implementation
+
+/**
+ * Holds if `t1` and `t2` are compatible, that is, whether data can flow from
+ * a node of type `t1` to a node of type `t2`.
+ */
+pragma[inline]
+predicate compatibleTypes(IRType t1, IRType t2) {
+  any() // stub implementation
+}
+
+private predicate suppressUnusedNode(Node n) { any() }
+
+//////////////////////////////////////////////////////////////////////////////
+// Java QL library compatibility wrappers
+//////////////////////////////////////////////////////////////////////////////
+/** A node that performs a type cast. */
+class CastNode extends Node {
+  CastNode() { none() } // stub implementation
+}
+
+/**
+ * A function that may contain code or a variable that may contain itself. When
+ * flow crosses from one _enclosing callable_ to another, the interprocedural
+ * data-flow library discards call contexts and inserts a node in the big-step
+ * relation used for human-readable path explanations.
+ */
+class DataFlowCallable = Cpp::Declaration;
+
+class DataFlowExpr = Expr;
+
+class DataFlowType = IRType;
+
+/** A function call relevant for data flow. */
+class DataFlowCall extends CallInstruction {
+  Function getEnclosingCallable() { result = this.getEnclosingFunction() }
+}
+
+predicate isUnreachableInCall(Node n, DataFlowCall call) { none() } // stub implementation
+
+int accessPathLimit() { result = 5 }
+
+/**
+ * Holds if access paths with `c` at their head always should be tracked at high
+ * precision. This disables adaptive access path precision for such access paths.
+ */
+predicate forceHighPrecision(Content c) { none() }
+
+/** The unit type. */
+private newtype TUnit = TMkUnit()
+
+/** The trivial type with a single element. */
+class Unit extends TUnit {
+  /** Gets a textual representation of this element. */
+  string toString() { result = "unit" }
+}
+
+/** Holds if `n` should be hidden from path explanations. */
+predicate nodeIsHidden(Node n) { n instanceof OperandNode and not n instanceof ArgumentNode }
+
+class LambdaCallKind = Unit;
+
+/** Holds if `creation` is an expression that creates a lambda of kind `kind` for `c`. */
+predicate lambdaCreation(Node creation, LambdaCallKind kind, DataFlowCallable c) { none() }
+
+/** Holds if `call` is a lambda call of kind `kind` where `receiver` is the lambda expression. */
+predicate lambdaCall(DataFlowCall call, LambdaCallKind kind, Node receiver) { none() }
+
+/** Extra data-flow steps needed for lambda flow analysis. */
+predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preservesValue) { none() }
+
+/**
+ * Holds if flow is allowed to pass from parameter `p` and back to itself as a
+ * side-effect, resulting in a summary from `p` to itself.
+ *
+ * One example would be to allow flow like `p.foo = p.bar;`, which is disallowed
+ * by default as a heuristic.
+ */
+predicate allowParameterReturnInSelf(ParameterNode p) { none() }
+
+private class MyConsistencyConfiguration extends Consistency::ConsistencyConfiguration {
+  override predicate argHasPostUpdateExclude(ArgumentNode n) {
+    // The rules for whether an IR argument gets a post-update node are too
+    // complex to model here.
+    any()
+  }
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/ModelUtil.qll

@@ -0,0 +1,93 @@
+/**
+ * Provides predicates for mapping the `FunctionInput` and `FunctionOutput`
+ * classes used in function models to the corresponding instructions.
+ */
+
+private import semmle.code.cpp.ir.IR
+private import experimental.semmle.code.cpp.ir.dataflow.DataFlow
+private import experimental.semmle.code.cpp.ir.dataflow.internal.DataFlowUtil
+private import SsaInternals as Ssa
+
+/**
+ * Gets the instruction that goes into `input` for `call`.
+ */
+DataFlow::Node callInput(CallInstruction call, FunctionInput input) {
+  // An argument or qualifier
+  exists(int index |
+    result.asOperand() = call.getArgumentOperand(index) and
+    input.isParameterOrQualifierAddress(index)
+  )
+  or
+  // A value pointed to by an argument or qualifier
+  exists(int index, int indirectionIndex |
+    hasOperandAndIndex(result, call.getArgumentOperand(index), indirectionIndex) and
+    input.isParameterDerefOrQualifierObject(index, indirectionIndex)
+  )
+  or
+  exists(int ind |
+    result = getIndirectReturnOutNode(call, ind) and
+    input.isReturnValueDeref(ind)
+  )
+}
+
+/**
+ * Gets the instruction that holds the `output` for `call`.
+ */
+Node callOutput(CallInstruction call, FunctionOutput output) {
+  // The return value
+  result.asInstruction() = call and
+  output.isReturnValue()
+  or
+  // The side effect of a call on the value pointed to by an argument or qualifier
+  exists(int index, int indirectionIndex |
+    result.(IndirectArgumentOutNode).getArgumentIndex() = index and
+    result.(IndirectArgumentOutNode).getIndirectionIndex() + 1 = indirectionIndex and
+    result.(IndirectArgumentOutNode).getCallInstruction() = call and
+    output.isParameterDerefOrQualifierObject(index, indirectionIndex)
+  )
+  or
+  exists(int ind |
+    result = getIndirectReturnOutNode(call, ind) and
+    output.isReturnValueDeref(ind)
+  )
+}
+
+DataFlow::Node callInput(CallInstruction call, FunctionInput input, int d) {
+  exists(DataFlow::Node n | n = callInput(call, input) and d > 0 |
+    // An argument or qualifier
+    hasOperandAndIndex(result, n.asOperand(), d)
+    or
+    exists(Operand operand, int indirectionIndex |
+      // A value pointed to by an argument or qualifier
+      hasOperandAndIndex(n, operand, indirectionIndex) and
+      hasOperandAndIndex(result, operand, indirectionIndex + d)
+    )
+  )
+}
+
+private IndirectReturnOutNode getIndirectReturnOutNode(CallInstruction call, int d) {
+  result.getCallInstruction() = call and
+  result.getIndirectionIndex() = d
+}
+
+/**
+ * Gets the instruction that holds the `output` for `call`.
+ */
+bindingset[d]
+Node callOutput(CallInstruction call, FunctionOutput output, int d) {
+  exists(DataFlow::Node n | n = callOutput(call, output) and d > 0 |
+    // The return value
+    result = getIndirectReturnOutNode(n.asInstruction(), d)
+    or
+    // If there isn't an indirect out node for the call with indirection `d` then
+    // we conflate this with the underlying `CallInstruction`.
+    not exists(getIndirectReturnOutNode(call, d)) and
+    n.asInstruction() = result.asInstruction()
+    or
+    // The side effect of a call on the value pointed to by an argument or qualifier
+    exists(Operand operand, int indirectionIndex |
+      Ssa::outNodeHasAddressAndIndex(n, operand, indirectionIndex) and
+      Ssa::outNodeHasAddressAndIndex(result, operand, indirectionIndex + d)
+    )
+  )
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/PrintIRLocalFlow.qll

@@ -0,0 +1,136 @@
+private import cpp
+// The `ValueNumbering` library has to be imported right after `cpp` to ensure
+// that the cached IR gets the same checksum here as it does in queries that use
+// `ValueNumbering` without `DataFlow`.
+private import semmle.code.cpp.ir.ValueNumbering
+private import semmle.code.cpp.ir.IR
+private import semmle.code.cpp.ir.dataflow.DataFlow
+private import semmle.code.cpp.ir.dataflow.internal.DataFlowUtil
+private import PrintIRUtilities
+
+/**
+ * Gets the local dataflow from other nodes in the same function to this node.
+ */
+private string getFromFlow(DataFlow::Node useNode, int order1, int order2) {
+  exists(DataFlow::Node defNode, string prefix |
+    (
+      simpleLocalFlowStep(defNode, useNode) and prefix = ""
+      or
+      any(DataFlow::Configuration cfg).isAdditionalFlowStep(defNode, useNode) and
+      defNode.getEnclosingCallable() = useNode.getEnclosingCallable() and
+      prefix = "+"
+    ) and
+    if defNode.asInstruction() = useNode.asOperand().getAnyDef()
+    then
+      // Shorthand for flow from the def of this operand.
+      result = prefix + "def" and
+      order1 = -1 and
+      order2 = 0
+    else
+      if defNode.asOperand().getUse() = useNode.asInstruction()
+      then
+        // Shorthand for flow from an operand of this instruction
+        result = prefix + defNode.asOperand().getDumpId() and
+        order1 = -1 and
+        order2 = defNode.asOperand().getDumpSortOrder()
+      else result = prefix + nodeId(defNode, order1, order2)
+  )
+}
+
+/**
+ * Gets the local dataflow from this node to other nodes in the same function.
+ */
+private string getToFlow(DataFlow::Node defNode, int order1, int order2) {
+  exists(DataFlow::Node useNode, string prefix |
+    (
+      simpleLocalFlowStep(defNode, useNode) and prefix = ""
+      or
+      any(DataFlow::Configuration cfg).isAdditionalFlowStep(defNode, useNode) and
+      defNode.getEnclosingCallable() = useNode.getEnclosingCallable() and
+      prefix = "+"
+    ) and
+    if useNode.asInstruction() = defNode.asOperand().getUse()
+    then
+      // Shorthand for flow to this operand's instruction.
+      result = prefix + "result" and
+      order1 = -1 and
+      order2 = 0
+    else result = prefix + nodeId(useNode, order1, order2)
+  )
+}
+
+/**
+ * Gets the properties of the dataflow node `node`.
+ */
+private string getNodeProperty(DataFlow::Node node, string key) {
+  // List dataflow into and out of this node. Flow into this node is printed as `src->@`, and flow
+  // out of this node is printed as `@->dest`.
+  key = "flow" and
+  result =
+    strictconcat(string flow, boolean to, int order1, int order2 |
+      flow = getFromFlow(node, order1, order2) + "->@" and to = false
+      or
+      flow = "@->" + getToFlow(node, order1, order2) and to = true
+    |
+      flow, ", " order by to, order1, order2, flow
+    )
+  or
+  // Is this node a dataflow sink?
+  key = "sink" and
+  any(DataFlow::Configuration cfg).isSink(node) and
+  result = "true"
+  or
+  // Is this node a dataflow source?
+  key = "source" and
+  any(DataFlow::Configuration cfg).isSource(node) and
+  result = "true"
+  or
+  // Is this node a dataflow barrier, and if so, what kind?
+  key = "barrier" and
+  result =
+    strictconcat(string kind |
+      any(DataFlow::Configuration cfg).isBarrier(node) and kind = "full"
+      or
+      any(DataFlow::Configuration cfg).isBarrierIn(node) and kind = "in"
+      or
+      any(DataFlow::Configuration cfg).isBarrierOut(node) and kind = "out"
+    |
+      kind, ", "
+    )
+  or
+  // Is there partial flow from a source to this node?
+  // This property will only be emitted if partial flow is enabled by overriding
+  // `DataFlow::Configration::explorationLimit()`.
+  key = "pflow" and
+  result =
+    strictconcat(DataFlow::PartialPathNode sourceNode, DataFlow::PartialPathNode destNode, int dist,
+      int order1, int order2 |
+      any(DataFlow::Configuration cfg).hasPartialFlow(sourceNode, destNode, dist) and
+      destNode.getNode() = node and
+      // Only print flow from a source in the same function.
+      sourceNode.getNode().getEnclosingCallable() = node.getEnclosingCallable()
+    |
+      nodeId(sourceNode.getNode(), order1, order2) + "+" + dist.toString(), ", "
+      order by
+        order1, order2, dist desc
+    )
+}
+
+/**
+ * Property provider for local IR dataflow.
+ */
+class LocalFlowPropertyProvider extends IRPropertyProvider {
+  override string getOperandProperty(Operand operand, string key) {
+    exists(DataFlow::Node node |
+      operand = node.asOperand() and
+      result = getNodeProperty(node, key)
+    )
+  }
+
+  override string getInstructionProperty(Instruction instruction, string key) {
+    exists(DataFlow::Node node |
+      instruction = node.asInstruction() and
+      result = getNodeProperty(node, key)
+    )
+  }
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/PrintIRStoreSteps.qll

@@ -0,0 +1,33 @@
+/**
+ * Print the dataflow local store steps in IR dumps.
+ */
+
+private import cpp
+// The `ValueNumbering` library has to be imported right after `cpp` to ensure
+// that the cached IR gets the same checksum here as it does in queries that use
+// `ValueNumbering` without `DataFlow`.
+private import semmle.code.cpp.ir.ValueNumbering
+private import semmle.code.cpp.ir.IR
+private import semmle.code.cpp.ir.dataflow.DataFlow
+private import semmle.code.cpp.ir.dataflow.internal.DataFlowUtil
+private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
+private import PrintIRUtilities
+
+/**
+ * Property provider for local IR dataflow store steps.
+ */
+class LocalFlowPropertyProvider extends IRPropertyProvider {
+  override string getInstructionProperty(Instruction instruction, string key) {
+    exists(DataFlow::Node objectNode, Content content |
+      key = "content[" + content.toString() + "]" and
+      instruction = objectNode.asInstruction() and
+      result =
+        strictconcat(string element, DataFlow::Node fieldNode |
+          storeStep(fieldNode, content, objectNode) and
+          element = nodeId(fieldNode, _, _)
+        |
+          element, ", "
+        )
+    )
+  }
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/PrintIRUtilities.qll

@@ -0,0 +1,39 @@
+/**
+ * Shared utilities used when printing dataflow annotations in IR dumps.
+ */
+
+private import cpp
+// The `ValueNumbering` library has to be imported right after `cpp` to ensure
+// that the cached IR gets the same checksum here as it does in queries that use
+// `ValueNumbering` without `DataFlow`.
+private import semmle.code.cpp.ir.ValueNumbering
+private import semmle.code.cpp.ir.IR
+private import semmle.code.cpp.ir.dataflow.DataFlow
+
+/**
+ * Gets a short ID for an IR dataflow node.
+ * - For `Instruction`s, this is just the result ID of the instruction (e.g. `m128`).
+ * - For `Operand`s, this is the label of the operand, prefixed with the result ID of the
+ *   instruction and a dot (e.g. `m128.left`).
+ * - For `Variable`s, this is the qualified name of the variable.
+ */
+string nodeId(DataFlow::Node node, int order1, int order2) {
+  exists(Instruction instruction | instruction = node.asInstruction() |
+    result = instruction.getResultId() and
+    order1 = instruction.getBlock().getDisplayIndex() and
+    order2 = instruction.getDisplayIndexInBlock()
+  )
+  or
+  exists(Operand operand, Instruction instruction |
+    operand = node.asOperand() and
+    instruction = operand.getUse()
+  |
+    result = instruction.getResultId() + "." + operand.getDumpId() and
+    order1 = instruction.getBlock().getDisplayIndex() and
+    order2 = instruction.getDisplayIndexInBlock()
+  )
+  or
+  result = "var(" + node.asVariable().getQualifiedName() + ")" and
+  order1 = 1000000 and
+  order2 = 0
+}

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

@@ -0,0 +1,547 @@
+private import codeql.ssa.Ssa as SsaImplCommon
+private import semmle.code.cpp.ir.IR
+private import DataFlowUtil
+private import DataFlowImplCommon as DataFlowImplCommon
+private import semmle.code.cpp.models.interfaces.Allocation as Alloc
+private import semmle.code.cpp.models.interfaces.DataFlow as DataFlow
+private import semmle.code.cpp.ir.internal.IRCppLanguage
+private import DataFlowPrivate
+private import ssa0.SsaInternals as SsaInternals0
+import SsaInternalsCommon
+
+private module SourceVariables {
+  int getMaxIndirectionForIRVariable(IRVariable var) {
+    exists(Type type, boolean isGLValue |
+      var.getLanguageType().hasType(type, isGLValue) and
+      if isGLValue = true
+      then result = 1 + getMaxIndirectionsForType(type)
+      else result = getMaxIndirectionsForType(type)
+    )
+  }
+
+  class BaseSourceVariable = SsaInternals0::BaseSourceVariable;
+
+  class BaseIRVariable = SsaInternals0::BaseIRVariable;
+
+  class BaseCallVariable = SsaInternals0::BaseCallVariable;
+
+  cached
+  private newtype TSourceVariable =
+    TSourceIRVariable(BaseIRVariable baseVar, int ind) {
+      ind = [0 .. getMaxIndirectionForIRVariable(baseVar.getIRVariable())]
+    } or
+    TCallVariable(AllocationInstruction call, int ind) {
+      ind = [0 .. countIndirectionsForCppType(getResultLanguageType(call))]
+    }
+
+  abstract class SourceVariable extends TSourceVariable {
+    int ind;
+
+    bindingset[ind]
+    SourceVariable() { any() }
+
+    abstract string toString();
+
+    int getIndirection() { result = ind }
+
+    abstract BaseSourceVariable getBaseVariable();
+  }
+
+  class SourceIRVariable extends SourceVariable, TSourceIRVariable {
+    BaseIRVariable var;
+
+    SourceIRVariable() { this = TSourceIRVariable(var, ind) }
+
+    IRVariable getIRVariable() { result = var.getIRVariable() }
+
+    override BaseIRVariable getBaseVariable() { result.getIRVariable() = this.getIRVariable() }
+
+    override string toString() {
+      ind = 0 and
+      result = this.getIRVariable().toString()
+      or
+      ind > 0 and
+      result = this.getIRVariable().toString() + " indirection"
+    }
+  }
+
+  class CallVariable extends SourceVariable, TCallVariable {
+    AllocationInstruction call;
+
+    CallVariable() { this = TCallVariable(call, ind) }
+
+    AllocationInstruction getCall() { result = call }
+
+    override BaseCallVariable getBaseVariable() { result.getCallInstruction() = call }
+
+    override string toString() {
+      ind = 0 and
+      result = "Call"
+      or
+      ind > 0 and
+      result = "Call indirection"
+    }
+  }
+}
+
+import SourceVariables
+
+predicate hasIndirectOperand(Operand op, int indirectionIndex) {
+  exists(CppType type, int m |
+    not ignoreOperand(op) and
+    type = getLanguageType(op) and
+    m = countIndirectionsForCppType(type) and
+    indirectionIndex = [1 .. m]
+  )
+}
+
+predicate hasIndirectInstruction(Instruction instr, int indirectionIndex) {
+  exists(CppType type, int m |
+    not ignoreInstruction(instr) and
+    type = getResultLanguageType(instr) and
+    m = countIndirectionsForCppType(type) and
+    indirectionIndex = [1 .. m]
+  )
+}
+
+cached
+private newtype TDefOrUseImpl =
+  TDefImpl(Operand address, int indirectionIndex) {
+    isDef(_, _, address, _, _, indirectionIndex) and
+    // We only include the definition if the SSA pruning stage
+    // concluded that the definition is live after the write.
+    any(SsaInternals0::Def def).getAddressOperand() = address
+  } or
+  TUseImpl(Operand operand, int indirectionIndex) {
+    isUse(_, operand, _, _, indirectionIndex) and
+    not isDef(_, _, operand, _, _, _)
+  }
+
+abstract private class DefOrUseImpl extends TDefOrUseImpl {
+  /** Gets a textual representation of this element. */
+  abstract string toString();
+
+  /** Gets the block of this definition or use. */
+  abstract IRBlock getBlock();
+
+  /** Holds if this definition or use has index `index` in block `block`. */
+  abstract predicate hasIndexInBlock(IRBlock block, int index);
+
+  final predicate hasIndexInBlock(IRBlock block, int index, SourceVariable sv) {
+    this.hasIndexInBlock(block, index) and
+    sv = this.getSourceVariable()
+  }
+
+  /** Gets the location of this element. */
+  abstract Cpp::Location getLocation();
+
+  /**
+   * Gets the index (i.e., the number of loads required) of this
+   * definition or use.
+   *
+   * Note that this is _not_ the definition's (or use's) index in
+   * the enclosing basic block. To obtain this index, use
+   * `DefOrUseImpl::hasIndexInBlock/2` or `DefOrUseImpl::hasIndexInBlock/3`.
+   */
+  abstract int getIndirectionIndex();
+
+  /**
+   * Gets the instruction that computes the base of this definition or use.
+   * This is always a `VariableAddressInstruction` or an `AllocationInstruction`.
+   */
+  abstract Instruction getBase();
+
+  final BaseSourceVariable getBaseSourceVariable() {
+    exists(IRVariable var |
+      result.(BaseIRVariable).getIRVariable() = var and
+      instructionHasIRVariable(this.getBase(), var)
+    )
+    or
+    result.(BaseCallVariable).getCallInstruction() = this.getBase()
+  }
+
+  /** Gets the variable that is defined or used. */
+  final SourceVariable getSourceVariable() {
+    exists(BaseSourceVariable v, int ind |
+      sourceVariableHasBaseAndIndex(result, v, ind) and
+      defOrUseHasSourceVariable(this, v, ind)
+    )
+  }
+}
+
+pragma[noinline]
+private predicate instructionHasIRVariable(VariableAddressInstruction vai, IRVariable var) {
+  vai.getIRVariable() = var
+}
+
+private predicate defOrUseHasSourceVariable(DefOrUseImpl defOrUse, BaseSourceVariable bv, int ind) {
+  defHasSourceVariable(defOrUse, bv, ind)
+  or
+  useHasSourceVariable(defOrUse, bv, ind)
+}
+
+pragma[noinline]
+private predicate defHasSourceVariable(DefImpl def, BaseSourceVariable bv, int ind) {
+  bv = def.getBaseSourceVariable() and
+  ind = def.getIndirection()
+}
+
+pragma[noinline]
+private predicate useHasSourceVariable(UseImpl use, BaseSourceVariable bv, int ind) {
+  bv = use.getBaseSourceVariable() and
+  ind = use.getIndirection()
+}
+
+pragma[noinline]
+private predicate sourceVariableHasBaseAndIndex(SourceVariable v, BaseSourceVariable bv, int ind) {
+  v.getBaseVariable() = bv and
+  v.getIndirection() = ind
+}
+
+class DefImpl extends DefOrUseImpl, TDefImpl {
+  Operand address;
+  int ind;
+
+  DefImpl() { this = TDefImpl(address, ind) }
+
+  override Instruction getBase() { isDef(_, _, address, result, _, _) }
+
+  Operand getAddressOperand() { result = address }
+
+  int getIndirection() { isDef(_, _, address, _, result, ind) }
+
+  override int getIndirectionIndex() { result = ind }
+
+  Instruction getDefiningInstruction() { isDef(_, result, address, _, _, _) }
+
+  override string toString() { result = "DefImpl" }
+
+  override IRBlock getBlock() { result = this.getDefiningInstruction().getBlock() }
+
+  override Cpp::Location getLocation() { result = this.getDefiningInstruction().getLocation() }
+
+  final override predicate hasIndexInBlock(IRBlock block, int index) {
+    this.getDefiningInstruction() = block.getInstruction(index)
+  }
+
+  predicate isCertain() { isDef(true, _, address, _, _, ind) }
+}
+
+class UseImpl extends DefOrUseImpl, TUseImpl {
+  Operand operand;
+  int ind;
+
+  UseImpl() { this = TUseImpl(operand, ind) }
+
+  Operand getOperand() { result = operand }
+
+  override string toString() { result = "UseImpl" }
+
+  final override predicate hasIndexInBlock(IRBlock block, int index) {
+    operand.getUse() = block.getInstruction(index)
+  }
+
+  final override IRBlock getBlock() { result = operand.getUse().getBlock() }
+
+  final override Cpp::Location getLocation() { result = operand.getLocation() }
+
+  final int getIndirection() { isUse(_, operand, _, result, ind) }
+
+  override int getIndirectionIndex() { result = ind }
+
+  override Instruction getBase() { isUse(_, operand, result, _, ind) }
+
+  predicate isCertain() { isUse(true, operand, _, _, ind) }
+}
+
+/**
+ * Holds if `defOrUse1` is a definition which is first read by `use`,
+ * or if `defOrUse1` is a use and `use` is a next subsequent use.
+ *
+ * In both cases, `use` can either be an explicit use written in the
+ * source file, or it can be a phi node as computed by the SSA library.
+ */
+predicate adjacentDefRead(DefOrUse defOrUse1, UseOrPhi use) {
+  exists(IRBlock bb1, int i1, SourceVariable v |
+    defOrUse1.asDefOrUse().hasIndexInBlock(bb1, i1, v)
+  |
+    exists(IRBlock bb2, int i2 |
+      adjacentDefRead(_, pragma[only_bind_into](bb1), pragma[only_bind_into](i1),
+        pragma[only_bind_into](bb2), pragma[only_bind_into](i2))
+    |
+      use.asDefOrUse().(UseImpl).hasIndexInBlock(bb2, i2, v)
+    )
+    or
+    exists(PhiNode phi |
+      lastRefRedef(_, bb1, i1, phi) and
+      use.asPhi() = phi and
+      phi.getSourceVariable() = pragma[only_bind_into](v)
+    )
+  )
+}
+
+private predicate useToNode(UseOrPhi use, Node nodeTo) {
+  exists(UseImpl useImpl |
+    useImpl = use.asDefOrUse() and
+    nodeHasOperand(nodeTo, useImpl.getOperand(), useImpl.getIndirectionIndex())
+  )
+  or
+  nodeTo.(SsaPhiNode).getPhiNode() = use.asPhi()
+}
+
+pragma[noinline]
+predicate outNodeHasAddressAndIndex(
+  IndirectArgumentOutNode out, Operand address, int indirectionIndex
+) {
+  out.getAddressOperand() = address and
+  out.getIndirectionIndex() = indirectionIndex
+}
+
+private predicate defToNode(Node nodeFrom, Def def) {
+  nodeHasInstruction(nodeFrom, def.getDefiningInstruction(), def.getIndirectionIndex())
+}
+
+private predicate nodeToDefOrUse(Node nodeFrom, SsaDefOrUse defOrUse) {
+  // Node -> Def
+  defToNode(nodeFrom, defOrUse)
+  or
+  // Node -> Use
+  useToNode(defOrUse, nodeFrom)
+}
+
+/**
+ * Perform a single conversion-like step from `nFrom` to `nTo`. This relation
+ * only holds when there is no use-use relation out of `nTo`.
+ */
+private predicate indirectConversionFlowStep(Node nFrom, Node nTo) {
+  not exists(UseOrPhi defOrUse |
+    nodeToDefOrUse(nTo, defOrUse) and
+    adjacentDefRead(defOrUse, _)
+  ) and
+  exists(Operand op1, Operand op2, int indirectionIndex, Instruction instr |
+    hasOperandAndIndex(nFrom, op1, pragma[only_bind_into](indirectionIndex)) and
+    hasOperandAndIndex(nTo, op2, pragma[only_bind_into](indirectionIndex)) and
+    instr = op2.getDef() and
+    conversionFlow(op1, instr, _)
+  )
+}
+
+/**
+ * The reason for this predicate is a bit annoying:
+ * We cannot mark a `PointerArithmeticInstruction` that computes an offset based on some SSA
+ * variable `x` as a use of `x` since this creates taint-flow in the following example:
+ * ```c
+ * int x = array[source]
+ * sink(*array)
+ * ```
+ * This is because `source` would flow from the operand of `PointerArithmeticInstruction` to the
+ * result of the instruction, and into the `IndirectOperand` that represents the value of `*array`.
+ * Then, via use-use flow, flow will arrive at `*array` in `sink(*array)`.
+ *
+ * So this predicate recurses back along conversions and `PointerArithmeticInstruction`s to find the
+ * first use that has provides use-use flow, and uses that target as the target of the `nodeFrom`.
+ */
+private predicate adjustForPointerArith(Node nodeFrom, UseOrPhi use) {
+  nodeFrom = any(PostUpdateNode pun).getPreUpdateNode() and
+  exists(DefOrUse defOrUse, Node adjusted |
+    indirectConversionFlowStep*(adjusted, nodeFrom) and
+    nodeToDefOrUse(adjusted, defOrUse) and
+    adjacentDefRead(defOrUse, use)
+  )
+}
+
+/** Holds if there is def-use or use-use flow from `nodeFrom` to `nodeTo`. */
+predicate ssaFlow(Node nodeFrom, Node nodeTo) {
+  // `nodeFrom = any(PostUpdateNode pun).getPreUpdateNode()` is implied by adjustedForPointerArith.
+  exists(UseOrPhi use |
+    adjustForPointerArith(nodeFrom, use) and
+    useToNode(use, nodeTo)
+  )
+  or
+  not nodeFrom = any(PostUpdateNode pun).getPreUpdateNode() and
+  exists(DefOrUse defOrUse1, UseOrPhi use |
+    nodeToDefOrUse(nodeFrom, defOrUse1) and
+    adjacentDefRead(defOrUse1, use) and
+    useToNode(use, nodeTo)
+  )
+}
+
+/** Holds if `nodeTo` receives flow from the phi node `nodeFrom`. */
+predicate fromPhiNode(SsaPhiNode nodeFrom, Node nodeTo) {
+  exists(PhiNode phi, SourceVariable sv, IRBlock bb1, int i1, UseOrPhi use |
+    phi = nodeFrom.getPhiNode() and
+    phi.definesAt(sv, bb1, i1) and
+    useToNode(use, nodeTo)
+  |
+    exists(IRBlock bb2, int i2 |
+      use.asDefOrUse().hasIndexInBlock(bb2, i2, sv) and
+      adjacentDefRead(phi, bb1, i1, bb2, i2)
+    )
+    or
+    exists(PhiNode phiTo |
+      lastRefRedef(phi, _, _, phiTo) and
+      nodeTo.(SsaPhiNode).getPhiNode() = phiTo
+    )
+  )
+}
+
+private SsaInternals0::SourceVariable getOldSourceVariable(SourceVariable v) {
+  v.getBaseVariable().(BaseIRVariable).getIRVariable() =
+    result.getBaseVariable().(SsaInternals0::BaseIRVariable).getIRVariable()
+  or
+  v.getBaseVariable().(BaseCallVariable).getCallInstruction() =
+    result.getBaseVariable().(SsaInternals0::BaseCallVariable).getCallInstruction()
+}
+
+/**
+ * Holds if there is a write at index `i` in basic block `bb` to variable `v` that's
+ * subsequently read (as determined by the SSA pruning stage).
+ */
+private predicate variableWriteCand(IRBlock bb, int i, SourceVariable v) {
+  exists(SsaInternals0::Def def, SsaInternals0::SourceVariable v0 |
+    def.asDefOrUse().hasIndexInBlock(bb, i, v0) and
+    v0 = getOldSourceVariable(v)
+  )
+}
+
+private module SsaInput implements SsaImplCommon::InputSig {
+  import InputSigCommon
+  import SourceVariables
+
+  /**
+   * Holds if the `i`'th write in block `bb` writes to the variable `v`.
+   * `certain` is `true` if the write is guaranteed to overwrite the entire variable.
+   */
+  predicate variableWrite(IRBlock bb, int i, SourceVariable v, boolean certain) {
+    DataFlowImplCommon::forceCachingInSameStage() and
+    variableWriteCand(bb, i, v) and
+    exists(DefImpl def | def.hasIndexInBlock(bb, i, v) |
+      if def.isCertain() then certain = true else certain = false
+    )
+  }
+
+  /**
+   * Holds if the `i`'th read in block `bb` reads to the variable `v`.
+   * `certain` is `true` if the read is guaranteed. For C++, this is always the case.
+   */
+  predicate variableRead(IRBlock bb, int i, SourceVariable v, boolean certain) {
+    exists(UseImpl use | use.hasIndexInBlock(bb, i, v) |
+      if use.isCertain() then certain = true else certain = false
+    )
+  }
+}
+
+/**
+ * The final SSA predicates used for dataflow purposes.
+ */
+cached
+module SsaCached {
+  /**
+   * Holds if `def` is accessed at index `i1` in basic block `bb1` (either a read
+   * or a write), `def` is read at index `i2` in basic block `bb2`, and there is a
+   * path between them without any read of `def`.
+   */
+  cached
+  predicate adjacentDefRead(Definition def, IRBlock bb1, int i1, IRBlock bb2, int i2) {
+    SsaImpl::adjacentDefRead(def, bb1, i1, bb2, i2)
+  }
+
+  /**
+   * Holds if the node at index `i` in `bb` is a last reference to SSA definition
+   * `def`. The reference is last because it can reach another write `next`,
+   * without passing through another read or write.
+   */
+  cached
+  predicate lastRefRedef(Definition def, IRBlock bb, int i, Definition next) {
+    SsaImpl::lastRefRedef(def, bb, i, next)
+  }
+}
+
+cached
+private newtype TSsaDefOrUse =
+  TDefOrUse(DefOrUseImpl defOrUse) {
+    defOrUse instanceof UseImpl
+    or
+    // Like in the pruning stage, we only include definition that's live after the
+    // write as the final definitions computed by SSA.
+    exists(Definition def, SourceVariable sv, IRBlock bb, int i |
+      def.definesAt(sv, bb, i) and
+      defOrUse.(DefImpl).hasIndexInBlock(bb, i, sv)
+    )
+  } or
+  TPhi(PhiNode phi)
+
+abstract private class SsaDefOrUse extends TSsaDefOrUse {
+  string toString() { none() }
+
+  DefOrUseImpl asDefOrUse() { none() }
+
+  PhiNode asPhi() { none() }
+
+  abstract Location getLocation();
+}
+
+class DefOrUse extends TDefOrUse, SsaDefOrUse {
+  DefOrUseImpl defOrUse;
+
+  DefOrUse() { this = TDefOrUse(defOrUse) }
+
+  final override DefOrUseImpl asDefOrUse() { result = defOrUse }
+
+  final override Location getLocation() { result = defOrUse.getLocation() }
+
+  final SourceVariable getSourceVariable() { result = defOrUse.getSourceVariable() }
+
+  override string toString() { result = defOrUse.toString() }
+}
+
+class Phi extends TPhi, SsaDefOrUse {
+  PhiNode phi;
+
+  Phi() { this = TPhi(phi) }
+
+  final override PhiNode asPhi() { result = phi }
+
+  final override Location getLocation() { result = phi.getBasicBlock().getLocation() }
+
+  override string toString() { result = "Phi" }
+}
+
+class UseOrPhi extends SsaDefOrUse {
+  UseOrPhi() {
+    this.asDefOrUse() instanceof UseImpl
+    or
+    this instanceof Phi
+  }
+
+  final override Location getLocation() {
+    result = this.asDefOrUse().getLocation() or result = this.(Phi).getLocation()
+  }
+}
+
+class Def extends DefOrUse {
+  override DefImpl defOrUse;
+
+  Operand getAddressOperand() { result = defOrUse.getAddressOperand() }
+
+  Instruction getAddress() { result = this.getAddressOperand().getDef() }
+
+  /**
+   * This predicate ensures that joins go from `defOrUse` to the result
+   * instead of the other way around.
+   */
+  pragma[inline]
+  int getIndirectionIndex() {
+    pragma[only_bind_into](result) = pragma[only_bind_out](defOrUse).getIndirectionIndex()
+  }
+
+  Instruction getDefiningInstruction() { result = defOrUse.getDefiningInstruction() }
+}
+
+private module SsaImpl = SsaImplCommon::Make<SsaInput>;
+
+class PhiNode = SsaImpl::PhiNode;
+
+class Definition = SsaImpl::Definition;
+
+import SsaCached

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/SsaInternalsCommon.qll

@@ -0,0 +1,268 @@
+import cpp as Cpp
+import semmle.code.cpp.ir.IR
+import semmle.code.cpp.ir.internal.IRCppLanguage
+private import semmle.code.cpp.ir.implementation.raw.internal.SideEffects as SideEffects
+private import DataFlowImplCommon as DataFlowImplCommon
+private import DataFlowUtil
+
+/**
+ * Holds if `operand` is an operand that is not used by the dataflow library.
+ * Ignored operands are not recognizd as uses by SSA, and they don't have a
+ * corresponding `(Indirect)OperandNode`.
+ */
+predicate ignoreOperand(Operand operand) {
+  operand = any(Instruction instr | ignoreInstruction(instr)).getAnOperand()
+}
+
+/**
+ * Holds if `instr` is an instruction that is not used by the dataflow library.
+ * Ignored instructions are not recognized as reads/writes by SSA, and they
+ * don't have a corresponding `(Indirect)InstructionNode`.
+ */
+predicate ignoreInstruction(Instruction instr) {
+  DataFlowImplCommon::forceCachingInSameStage() and
+  (
+    instr instanceof WriteSideEffectInstruction or
+    instr instanceof PhiInstruction or
+    instr instanceof ReadSideEffectInstruction or
+    instr instanceof ChiInstruction or
+    instr instanceof InitializeIndirectionInstruction
+  )
+}
+
+/**
+ * Gets the C++ type of `this` in the member function `f`.
+ * The result is a glvalue if `isGLValue` is true, and
+ * a prvalue if `isGLValue` is false.
+ */
+bindingset[isGLValue]
+private CppType getThisType(Cpp::MemberFunction f, boolean isGLValue) {
+  result.hasType(f.getTypeOfThis(), isGLValue)
+}
+
+/**
+ * Gets the C++ type of the instruction `i`.
+ *
+ * This is equivalent to `i.getResultLanguageType()` with the exception
+ * of instructions that directly references a `this` IRVariable. In this
+ * case, `i.getResultLanguageType()` gives an unknown type, whereas the
+ * predicate gives the expected type (i.e., a potentially cv-qualified
+ * type `A*` where `A` is the declaring type of the member function that
+ * contains `i`).
+ */
+cached
+CppType getResultLanguageType(Instruction i) {
+  if i.(VariableAddressInstruction).getIRVariable() instanceof IRThisVariable
+  then
+    if i.isGLValue()
+    then result = getThisType(i.getEnclosingFunction(), true)
+    else result = getThisType(i.getEnclosingFunction(), false)
+  else result = i.getResultLanguageType()
+}
+
+/**
+ * Gets the C++ type of the operand `operand`.
+ * This is equivalent to the type of the operand's defining instruction.
+ *
+ * See `getResultLanguageType` for a description of this behavior.
+ */
+CppType getLanguageType(Operand operand) { result = getResultLanguageType(operand.getDef()) }
+
+/**
+ * Gets the maximum number of indirections a glvalue of type `type` can have.
+ * For example:
+ * - If `type = int`, the result is 1
+ * - If `type = MyStruct`, the result is 1
+ * - If `type = char*`, the result is 2
+ */
+int getMaxIndirectionsForType(Type type) {
+  result = countIndirectionsForCppType(getTypeForGLValue(type))
+}
+
+/**
+ * Gets the maximum number of indirections a value of type `type` can have.
+ *
+ * Note that this predicate is intended to be called on unspecified types
+ * (i.e., `countIndirections(e.getUnspecifiedType())`).
+ */
+private int countIndirections(Type t) {
+  result =
+    1 +
+      countIndirections([t.(Cpp::PointerType).getBaseType(), t.(Cpp::ReferenceType).getBaseType()])
+  or
+  not t instanceof Cpp::PointerType and
+  not t instanceof Cpp::ReferenceType and
+  result = 0
+}
+
+/**
+ * Gets the maximum number of indirections a value of C++
+ * type `langType` can have.
+ */
+int countIndirectionsForCppType(LanguageType langType) {
+  exists(Type type | langType.hasType(type, true) |
+    result = 1 + countIndirections(type.getUnspecifiedType())
+  )
+  or
+  exists(Type type | langType.hasType(type, false) |
+    result = countIndirections(type.getUnspecifiedType())
+  )
+}
+
+/**
+ * A `CallInstruction` that calls an allocation function such
+ * as `malloc` or `operator new`.
+ */
+class AllocationInstruction extends CallInstruction {
+  AllocationInstruction() { this.getStaticCallTarget() instanceof Cpp::AllocationFunction }
+}
+
+/**
+ * Holds if `i` is a base instruction that starts a sequence of uses
+ * of some variable that SSA can handle.
+ *
+ * This is either when `i` is a `VariableAddressInstruction` or when
+ * `i` is a fresh allocation produced by an `AllocationInstruction`.
+ */
+private predicate isSourceVariableBase(Instruction i) {
+  i instanceof VariableAddressInstruction or i instanceof AllocationInstruction
+}
+
+/**
+ * Holds if the value pointed to by `operand` can potentially be
+ * modified be the caller.
+ */
+predicate isModifiableByCall(ArgumentOperand operand) {
+  exists(CallInstruction call, int index, CppType type |
+    type = getLanguageType(operand) and
+    call.getArgumentOperand(index) = operand and
+    if index = -1
+    then not call.getStaticCallTarget() instanceof Cpp::ConstMemberFunction
+    else not SideEffects::isConstPointerLike(any(Type t | type.hasType(t, _)))
+  )
+}
+
+cached
+private module Cached {
+  /**
+   * Holds if `op` is a use of an SSA variable rooted at `base` with `ind` number
+   * of indirections.
+   *
+   * `certain` is `true` if the operand is guaranteed to read the variable, and
+   * `indirectionIndex` specifies the number of loads required to read the variable.
+   */
+  cached
+  predicate isUse(boolean certain, Operand op, Instruction base, int ind, int indirectionIndex) {
+    not ignoreOperand(op) and
+    certain = true and
+    exists(LanguageType type, int m, int ind0 |
+      type = getLanguageType(op) and
+      m = countIndirectionsForCppType(type) and
+      isUseImpl(op, base, ind0) and
+      ind = ind0 + [0 .. m] and
+      indirectionIndex = ind - ind0
+    )
+  }
+
+  /**
+   * Holds if `operand` is a use of an SSA variable rooted at `base`, and the
+   * path from `base` to `operand` passes through `ind` load-like instructions.
+   */
+  private predicate isUseImpl(Operand operand, Instruction base, int ind) {
+    DataFlowImplCommon::forceCachingInSameStage() and
+    ind = 0 and
+    operand.getDef() = base and
+    isSourceVariableBase(base)
+    or
+    exists(Operand mid, Instruction instr |
+      isUseImpl(mid, base, ind) and
+      instr = operand.getDef() and
+      conversionFlow(mid, instr, false)
+    )
+    or
+    exists(int ind0 |
+      isUseImpl(operand.getDef().(LoadInstruction).getSourceAddressOperand(), base, ind0)
+      or
+      isUseImpl(operand.getDef().(InitializeParameterInstruction).getAnOperand(), base, ind0)
+    |
+      ind0 = ind - 1
+    )
+  }
+
+  /**
+   * Holds if `address` is an address of an SSA variable rooted at `base`,
+   * and `instr` is a definition of the SSA variable with `ind` number of indirections.
+   *
+   * `certain` is `true` if `instr` is guaranteed to write to the variable, and
+   * `indirectionIndex` specifies the number of loads required to read the variable
+   * after the write operation.
+   */
+  cached
+  predicate isDef(
+    boolean certain, Instruction instr, Operand address, Instruction base, int ind,
+    int indirectionIndex
+  ) {
+    certain = true and
+    exists(int ind0, CppType type, int m |
+      address =
+        [
+          instr.(StoreInstruction).getDestinationAddressOperand(),
+          instr.(InitializeParameterInstruction).getAnOperand(),
+          instr.(InitializeDynamicAllocationInstruction).getAllocationAddressOperand(),
+          instr.(UninitializedInstruction).getAnOperand()
+        ]
+    |
+      isDefImpl(address, base, ind0) and
+      type = getLanguageType(address) and
+      m = countIndirectionsForCppType(type) and
+      ind = ind0 + [1 .. m] and
+      indirectionIndex = ind - (ind0 + 1)
+    )
+  }
+
+  /**
+   * Holds if `address` is a use of an SSA variable rooted at `base`, and the
+   * path from `base` to `address` passes through `ind` load-like instructions.
+   *
+   * Note: Unlike `isUseImpl`, this predicate recurses through pointer-arithmetic
+   * instructions.
+   */
+  private predicate isDefImpl(Operand address, Instruction base, int ind) {
+    DataFlowImplCommon::forceCachingInSameStage() and
+    ind = 0 and
+    address.getDef() = base and
+    isSourceVariableBase(base)
+    or
+    exists(Operand mid, Instruction instr |
+      isDefImpl(mid, base, ind) and
+      instr = address.getDef() and
+      conversionFlow(mid, instr, _)
+    )
+    or
+    exists(int ind0 |
+      isDefImpl(address.getDef().(LoadInstruction).getSourceAddressOperand(), base, ind0)
+      or
+      isDefImpl(address.getDef().(InitializeParameterInstruction).getAnOperand(), base, ind0)
+    |
+      ind0 = ind - 1
+    )
+  }
+}
+
+import Cached
+
+/**
+ * Inputs to the shared SSA library's parameterized module that is shared
+ * between the SSA pruning stage, and the final SSA stage.
+ */
+module InputSigCommon {
+  class BasicBlock = IRBlock;
+
+  BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result.immediatelyDominates(bb) }
+
+  BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
+
+  class ExitBasicBlock extends IRBlock {
+    ExitBasicBlock() { this.getLastInstruction() instanceof ExitFunctionInstruction }
+  }
+}

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

@@ -0,0 +1,208 @@
+private import semmle.code.cpp.ir.IR
+private import experimental.semmle.code.cpp.ir.dataflow.DataFlow
+private import ModelUtil
+private import semmle.code.cpp.models.interfaces.DataFlow
+private import semmle.code.cpp.models.interfaces.SideEffect
+private import DataFlowUtil
+private import DataFlowPrivate
+private import semmle.code.cpp.models.Models
+
+/**
+ * Holds if taint propagates from `nodeFrom` to `nodeTo` in exactly one local
+ * (intra-procedural) step.
+ */
+predicate localTaintStep(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
+  DataFlow::localFlowStep(nodeFrom, nodeTo)
+  or
+  localAdditionalTaintStep(nodeFrom, nodeTo)
+}
+
+/**
+ * Holds if taint can flow in one local step from `nodeFrom` to `nodeTo` excluding
+ * local data flow steps. That is, `nodeFrom` and `nodeTo` are likely to represent
+ * different objects.
+ */
+cached
+predicate localAdditionalTaintStep(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
+  operandToInstructionTaintStep(nodeFrom.asOperand(), nodeTo.asInstruction())
+  or
+  modeledTaintStep(nodeFrom, nodeTo)
+  or
+  // Flow from `op` to `*op`.
+  exists(Operand operand, int indirectionIndex |
+    nodeHasOperand(nodeFrom, operand, indirectionIndex) and
+    nodeHasOperand(nodeTo, operand, indirectionIndex - 1)
+  )
+  or
+  // Flow from `instr` to `*instr`.
+  exists(Instruction instr, int indirectionIndex |
+    nodeHasInstruction(nodeFrom, instr, indirectionIndex) and
+    nodeHasInstruction(nodeTo, instr, indirectionIndex - 1)
+  )
+  or
+  // Flow from (the indirection of) an operand of a pointer arithmetic instruction to the
+  // indirection of the pointer arithmetic instruction. This provides flow from `source`
+  // in `x[source]` to the result of the associated load instruction.
+  exists(PointerArithmeticInstruction pai, int indirectionIndex |
+    nodeHasOperand(nodeFrom, pai.getAnOperand(), pragma[only_bind_into](indirectionIndex)) and
+    hasInstructionAndIndex(nodeTo, pai, indirectionIndex + 1)
+  )
+}
+
+/**
+ * Holds if taint propagates from `nodeFrom` to `nodeTo` in exactly one local
+ * (intra-procedural) step.
+ */
+private predicate operandToInstructionTaintStep(Operand opFrom, Instruction instrTo) {
+  // Taint can flow through expressions that alter the value but preserve
+  // more than one bit of it _or_ expressions that follow data through
+  // pointer indirections.
+  instrTo.getAnOperand() = opFrom and
+  (
+    instrTo instanceof ArithmeticInstruction
+    or
+    instrTo instanceof BitwiseInstruction
+    or
+    instrTo instanceof PointerArithmeticInstruction
+  )
+  or
+  // The `CopyInstruction` case is also present in non-taint data flow, but
+  // that uses `getDef` rather than `getAnyDef`. For taint, we want flow
+  // from a definition of `myStruct` to a `myStruct.myField` expression.
+  instrTo.(LoadInstruction).getSourceAddressOperand() = opFrom
+  or
+  // Unary instructions tend to preserve enough information in practice that we
+  // want taint to flow through.
+  // The exception is `FieldAddressInstruction`. Together with the rules below for
+  // `LoadInstruction`s and `ChiInstruction`s, flow through `FieldAddressInstruction`
+  // could cause flow into one field to come out an unrelated field.
+  // This would happen across function boundaries, where the IR would not be able to
+  // match loads to stores.
+  instrTo.(UnaryInstruction).getUnaryOperand() = opFrom and
+  (
+    not instrTo instanceof FieldAddressInstruction
+    or
+    instrTo.(FieldAddressInstruction).getField().getDeclaringType() instanceof Union
+  )
+}
+
+/**
+ * Holds if taint may propagate from `source` to `sink` in zero or more local
+ * (intra-procedural) steps.
+ */
+pragma[inline]
+predicate localTaint(DataFlow::Node source, DataFlow::Node sink) { localTaintStep*(source, sink) }
+
+/**
+ * Holds if taint can flow from `i1` to `i2` in zero or more
+ * local (intra-procedural) steps.
+ */
+pragma[inline]
+predicate localInstructionTaint(Instruction i1, Instruction i2) {
+  localTaint(DataFlow::instructionNode(i1), DataFlow::instructionNode(i2))
+}
+
+/**
+ * Holds if taint can flow from `e1` to `e2` in zero or more
+ * local (intra-procedural) steps.
+ */
+pragma[inline]
+predicate localExprTaint(Expr e1, Expr e2) {
+  localTaint(DataFlow::exprNode(e1), DataFlow::exprNode(e2))
+}
+
+/**
+ * Holds if the additional step from `src` to `sink` should be included in all
+ * global taint flow configurations.
+ */
+predicate defaultAdditionalTaintStep(DataFlow::Node src, DataFlow::Node sink) {
+  localAdditionalTaintStep(src, sink)
+}
+
+/**
+ * Holds if default `TaintTracking::Configuration`s should allow implicit reads
+ * of `c` at sinks and inputs to additional taint steps.
+ */
+bindingset[node]
+predicate defaultImplicitTaintRead(DataFlow::Node node, DataFlow::Content c) { none() }
+
+/**
+ * Holds if `node` should be a sanitizer in all global taint flow configurations
+ * but not in local taint.
+ */
+predicate defaultTaintSanitizer(DataFlow::Node node) { none() }
+
+/**
+ * Holds if taint can flow from `instrIn` to `instrOut` through a call to a
+ * modeled function.
+ */
+predicate modeledTaintStep(DataFlow::Node nodeIn, DataFlow::Node nodeOut) {
+  // Normal taint steps
+  exists(CallInstruction call, TaintFunction func, FunctionInput modelIn, FunctionOutput modelOut |
+    call.getStaticCallTarget() = func and
+    func.hasTaintFlow(modelIn, modelOut)
+  |
+    (
+      nodeIn = callInput(call, modelIn)
+      or
+      exists(int n |
+        modelIn.isParameterDerefOrQualifierObject(n) and
+        if n = -1
+        then nodeIn = callInput(call, any(InQualifierAddress inQualifier))
+        else nodeIn = callInput(call, any(InParameter inParam | inParam.getIndex() = n))
+      )
+    ) and
+    nodeOut = callOutput(call, modelOut)
+    or
+    exists(int d |
+      nodeIn = callInput(call, modelIn, d)
+      or
+      exists(int n |
+        d = 1 and
+        modelIn.isParameterDerefOrQualifierObject(n) and
+        if n = -1
+        then nodeIn = callInput(call, any(InQualifierAddress inQualifier))
+        else nodeIn = callInput(call, any(InParameter inParam | inParam.getIndex() = n))
+      )
+    |
+      call.getStaticCallTarget() = func and
+      func.hasTaintFlow(modelIn, modelOut) and
+      nodeOut = callOutput(call, modelOut, d)
+    )
+  )
+  or
+  // Taint flow from one argument to another and data flow from an argument to a
+  // return value. This happens in functions like `strcat` and `memcpy`. We
+  // could model this flow in two separate steps, but that would add reverse
+  // flow from the write side-effect to the call instruction, which may not be
+  // desirable.
+  exists(
+    CallInstruction call, Function func, FunctionInput modelIn, OutParameterDeref modelMidOut,
+    int indexMid, InParameter modelMidIn, OutReturnValue modelOut
+  |
+    nodeIn = callInput(call, modelIn) and
+    nodeOut = callOutput(call, modelOut) and
+    call.getStaticCallTarget() = func and
+    func.(TaintFunction).hasTaintFlow(modelIn, modelMidOut) and
+    func.(DataFlowFunction).hasDataFlow(modelMidIn, modelOut) and
+    modelMidOut.isParameterDeref(indexMid) and
+    modelMidIn.isParameter(indexMid)
+  )
+  or
+  // Taint flow from a pointer argument to an output, when the model specifies flow from the deref
+  // to that output, but the deref is not modeled in the IR for the caller.
+  exists(
+    CallInstruction call, DataFlow::SideEffectOperandNode indirectArgument, Function func,
+    FunctionInput modelIn, FunctionOutput modelOut
+  |
+    indirectArgument = callInput(call, modelIn) and
+    indirectArgument.getAddressOperand() = nodeIn.asOperand() and
+    call.getStaticCallTarget() = func and
+    (
+      func.(DataFlowFunction).hasDataFlow(modelIn, modelOut)
+      or
+      func.(TaintFunction).hasTaintFlow(modelIn, modelOut)
+    ) and
+    nodeOut = callOutput(call, modelOut)
+  )
+}

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

@@ -0,0 +1,314 @@
+/**
+ * This module defines an initial SSA pruning stage that doesn't take
+ * indirections into account.
+ */
+
+private import codeql.ssa.Ssa as SsaImplCommon
+private import semmle.code.cpp.ir.IR
+private import experimental.semmle.code.cpp.ir.dataflow.internal.DataFlowImplCommon as DataFlowImplCommon
+private import semmle.code.cpp.models.interfaces.Allocation as Alloc
+private import semmle.code.cpp.models.interfaces.DataFlow as DataFlow
+private import semmle.code.cpp.ir.implementation.raw.internal.SideEffects as SideEffects
+private import semmle.code.cpp.ir.internal.IRCppLanguage
+private import experimental.semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
+private import experimental.semmle.code.cpp.ir.dataflow.internal.DataFlowUtil
+private import experimental.semmle.code.cpp.ir.dataflow.internal.SsaInternalsCommon
+
+private module SourceVariables {
+  newtype TBaseSourceVariable =
+    // Each IR variable gets its own source variable
+    TBaseIRVariable(IRVariable var) or
+    // Each allocation gets its own source variable
+    TBaseCallVariable(AllocationInstruction call)
+
+  abstract class BaseSourceVariable extends TBaseSourceVariable {
+    abstract string toString();
+
+    abstract DataFlowType getType();
+  }
+
+  class BaseIRVariable extends BaseSourceVariable, TBaseIRVariable {
+    IRVariable var;
+
+    IRVariable getIRVariable() { result = var }
+
+    BaseIRVariable() { this = TBaseIRVariable(var) }
+
+    override string toString() { result = var.toString() }
+
+    override DataFlowType getType() { result = var.getIRType() }
+  }
+
+  class BaseCallVariable extends BaseSourceVariable, TBaseCallVariable {
+    AllocationInstruction call;
+
+    BaseCallVariable() { this = TBaseCallVariable(call) }
+
+    AllocationInstruction getCallInstruction() { result = call }
+
+    override string toString() { result = call.toString() }
+
+    override DataFlowType getType() { result = call.getResultIRType() }
+  }
+
+  private newtype TSourceVariable =
+    TSourceIRVariable(BaseIRVariable baseVar) or
+    TCallVariable(AllocationInstruction call)
+
+  abstract class SourceVariable extends TSourceVariable {
+    abstract string toString();
+
+    abstract BaseSourceVariable getBaseVariable();
+  }
+
+  class SourceIRVariable extends SourceVariable, TSourceIRVariable {
+    BaseIRVariable var;
+
+    SourceIRVariable() { this = TSourceIRVariable(var) }
+
+    IRVariable getIRVariable() { result = var.getIRVariable() }
+
+    override BaseIRVariable getBaseVariable() { result.getIRVariable() = this.getIRVariable() }
+
+    override string toString() { result = this.getIRVariable().toString() }
+  }
+
+  class CallVariable extends SourceVariable, TCallVariable {
+    AllocationInstruction call;
+
+    CallVariable() { this = TCallVariable(call) }
+
+    AllocationInstruction getCall() { result = call }
+
+    override BaseCallVariable getBaseVariable() { result.getCallInstruction() = call }
+
+    override string toString() { result = "Call" }
+  }
+}
+
+import SourceVariables
+
+private newtype TDefOrUseImpl =
+  TDefImpl(Operand address) { isDef(_, _, address, _, _, _) } or
+  TUseImpl(Operand operand) {
+    isUse(_, operand, _, _, _) and
+    not isDef(_, _, operand, _, _, _)
+  }
+
+abstract private class DefOrUseImpl extends TDefOrUseImpl {
+  /** Gets a textual representation of this element. */
+  abstract string toString();
+
+  /** Gets the block of this definition or use. */
+  abstract IRBlock getBlock();
+
+  /** Holds if this definition or use has index `index` in block `block`. */
+  abstract predicate hasIndexInBlock(IRBlock block, int index);
+
+  final predicate hasIndexInBlock(IRBlock block, int index, SourceVariable sv) {
+    this.hasIndexInBlock(block, index) and
+    sv = this.getSourceVariable()
+  }
+
+  /** Gets the location of this element. */
+  abstract Cpp::Location getLocation();
+
+  abstract Instruction getBase();
+
+  final BaseSourceVariable getBaseSourceVariable() {
+    exists(IRVariable var |
+      result.(BaseIRVariable).getIRVariable() = var and
+      instructionHasIRVariable(this.getBase(), var)
+    )
+    or
+    result.(BaseCallVariable).getCallInstruction() = this.getBase()
+  }
+
+  /** Gets the variable that is defined or used. */
+  final SourceVariable getSourceVariable() {
+    exists(BaseSourceVariable v |
+      sourceVariableHasBaseAndIndex(result, v) and
+      defOrUseHasSourceVariable(this, v)
+    )
+  }
+}
+
+pragma[noinline]
+private predicate instructionHasIRVariable(VariableAddressInstruction vai, IRVariable var) {
+  vai.getIRVariable() = var
+}
+
+private predicate defOrUseHasSourceVariable(DefOrUseImpl defOrUse, BaseSourceVariable bv) {
+  defHasSourceVariable(defOrUse, bv)
+  or
+  useHasSourceVariable(defOrUse, bv)
+}
+
+pragma[noinline]
+private predicate defHasSourceVariable(DefImpl def, BaseSourceVariable bv) {
+  bv = def.getBaseSourceVariable()
+}
+
+pragma[noinline]
+private predicate useHasSourceVariable(UseImpl use, BaseSourceVariable bv) {
+  bv = use.getBaseSourceVariable()
+}
+
+pragma[noinline]
+private predicate sourceVariableHasBaseAndIndex(SourceVariable v, BaseSourceVariable bv) {
+  v.getBaseVariable() = bv
+}
+
+class DefImpl extends DefOrUseImpl, TDefImpl {
+  Operand address;
+
+  DefImpl() { this = TDefImpl(address) }
+
+  override Instruction getBase() { isDef(_, _, address, result, _, _) }
+
+  Operand getAddressOperand() { result = address }
+
+  Instruction getDefiningInstruction() { isDef(_, result, address, _, _, _) }
+
+  override string toString() { result = address.toString() }
+
+  override IRBlock getBlock() { result = this.getDefiningInstruction().getBlock() }
+
+  override Cpp::Location getLocation() { result = this.getDefiningInstruction().getLocation() }
+
+  final override predicate hasIndexInBlock(IRBlock block, int index) {
+    this.getDefiningInstruction() = block.getInstruction(index)
+  }
+
+  predicate isCertain() { isDef(true, _, address, _, _, _) }
+}
+
+class UseImpl extends DefOrUseImpl, TUseImpl {
+  Operand operand;
+
+  UseImpl() { this = TUseImpl(operand) }
+
+  Operand getOperand() { result = operand }
+
+  override string toString() { result = operand.toString() }
+
+  final override predicate hasIndexInBlock(IRBlock block, int index) {
+    operand.getUse() = block.getInstruction(index)
+  }
+
+  final override IRBlock getBlock() { result = operand.getUse().getBlock() }
+
+  final override Cpp::Location getLocation() { result = operand.getLocation() }
+
+  override Instruction getBase() { isUse(_, operand, result, _, _) }
+
+  predicate isCertain() { isUse(true, operand, _, _, _) }
+}
+
+private module SsaInput implements SsaImplCommon::InputSig {
+  import InputSigCommon
+  import SourceVariables
+
+  /**
+   * Holds if the `i`'th write in block `bb` writes to the variable `v`.
+   * `certain` is `true` if the write is guaranteed to overwrite the entire variable.
+   */
+  predicate variableWrite(IRBlock bb, int i, SourceVariable v, boolean certain) {
+    DataFlowImplCommon::forceCachingInSameStage() and
+    exists(DefImpl def | def.hasIndexInBlock(bb, i, v) |
+      if def.isCertain() then certain = true else certain = false
+    )
+  }
+
+  /**
+   * Holds if the `i`'th read in block `bb` reads to the variable `v`.
+   * `certain` is `true` if the read is guaranteed.
+   */
+  predicate variableRead(IRBlock bb, int i, SourceVariable v, boolean certain) {
+    exists(UseImpl use | use.hasIndexInBlock(bb, i, v) |
+      if use.isCertain() then certain = true else certain = false
+    )
+  }
+}
+
+private newtype TSsaDefOrUse =
+  TDefOrUse(DefOrUseImpl defOrUse) {
+    defOrUse instanceof UseImpl
+    or
+    // If `defOrUse` is a definition we only include it if the
+    // SSA library concludes that it's live after the write.
+    exists(Definition def, SourceVariable sv, IRBlock bb, int i |
+      def.definesAt(sv, bb, i) and
+      defOrUse.(DefImpl).hasIndexInBlock(bb, i, sv)
+    )
+  } or
+  TPhi(PhiNode phi)
+
+abstract private class SsaDefOrUse extends TSsaDefOrUse {
+  string toString() { result = "SsaDefOrUse" }
+
+  DefOrUseImpl asDefOrUse() { none() }
+
+  PhiNode asPhi() { none() }
+
+  abstract Location getLocation();
+}
+
+class DefOrUse extends TDefOrUse, SsaDefOrUse {
+  DefOrUseImpl defOrUse;
+
+  DefOrUse() { this = TDefOrUse(defOrUse) }
+
+  final override DefOrUseImpl asDefOrUse() { result = defOrUse }
+
+  final override Location getLocation() { result = defOrUse.getLocation() }
+
+  final SourceVariable getSourceVariable() { result = defOrUse.getSourceVariable() }
+}
+
+class Phi extends TPhi, SsaDefOrUse {
+  PhiNode phi;
+
+  Phi() { this = TPhi(phi) }
+
+  final override PhiNode asPhi() { result = phi }
+
+  final override Location getLocation() { result = phi.getBasicBlock().getLocation() }
+}
+
+class UseOrPhi extends SsaDefOrUse {
+  UseOrPhi() {
+    this.asDefOrUse() instanceof UseImpl
+    or
+    this instanceof Phi
+  }
+
+  final override Location getLocation() {
+    result = this.asDefOrUse().getLocation() or result = this.(Phi).getLocation()
+  }
+
+  override string toString() {
+    result = this.asDefOrUse().toString()
+    or
+    this instanceof Phi and
+    result = "Phi"
+  }
+}
+
+class Def extends DefOrUse {
+  override DefImpl defOrUse;
+
+  Operand getAddressOperand() { result = defOrUse.getAddressOperand() }
+
+  Instruction getAddress() { result = this.getAddressOperand().getDef() }
+
+  Instruction getDefiningInstruction() { result = defOrUse.getDefiningInstruction() }
+
+  override string toString() { result = this.asDefOrUse().toString() + " (def)" }
+}
+
+private module SsaImpl = SsaImplCommon::Make<SsaInput>;
+
+class PhiNode = SsaImpl::PhiNode;
+
+class Definition = SsaImpl::Definition;

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

@@ -0,0 +1,191 @@
+/**
+ * Provides an implementation of global (interprocedural) taint tracking.
+ * This file re-exports the local (intraprocedural) taint-tracking analysis
+ * from `TaintTrackingParameter::Public` and adds a global analysis, mainly
+ * exposed through the `Configuration` class. For some languages, this file
+ * exists in several identical copies, allowing queries to use multiple
+ * `Configuration` classes that depend on each other without introducing
+ * mutual recursion among those configurations.
+ */
+
+import TaintTrackingParameter::Public
+private import TaintTrackingParameter::Private
+
+/**
+ * A configuration of interprocedural taint tracking analysis. This defines
+ * sources, sinks, and any other configurable aspect of the analysis. Each
+ * use of the taint tracking library must define its own unique extension of
+ * this abstract class.
+ *
+ * A taint-tracking configuration is a special data flow configuration
+ * (`DataFlow::Configuration`) that allows for flow through nodes that do not
+ * necessarily preserve values but are still relevant from a taint tracking
+ * perspective. (For example, string concatenation, where one of the operands
+ * is tainted.)
+ *
+ * To create a configuration, extend this class with a subclass whose
+ * characteristic predicate is a unique singleton string. For example, write
+ *
+ * ```ql
+ * class MyAnalysisConfiguration extends TaintTracking::Configuration {
+ *   MyAnalysisConfiguration() { this = "MyAnalysisConfiguration" }
+ *   // Override `isSource` and `isSink`.
+ *   // Optionally override `isSanitizer`.
+ *   // Optionally override `isSanitizerIn`.
+ *   // Optionally override `isSanitizerOut`.
+ *   // Optionally override `isSanitizerGuard`.
+ *   // Optionally override `isAdditionalTaintStep`.
+ * }
+ * ```
+ *
+ * Then, to query whether there is flow between some `source` and `sink`,
+ * write
+ *
+ * ```ql
+ * exists(MyAnalysisConfiguration cfg | cfg.hasFlow(source, sink))
+ * ```
+ *
+ * Multiple configurations can coexist, but it is unsupported to depend on
+ * another `TaintTracking::Configuration` or a `DataFlow::Configuration` in the
+ * overridden predicates that define sources, sinks, or additional steps.
+ * Instead, the dependency should go to a `TaintTracking2::Configuration` or a
+ * `DataFlow2::Configuration`, `DataFlow3::Configuration`, etc.
+ */
+abstract class Configuration extends DataFlow::Configuration {
+  bindingset[this]
+  Configuration() { any() }
+
+  /**
+   * Holds if `source` is a relevant taint source.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSource(DataFlow::Node source) { none() }
+
+  /**
+   * Holds if `source` is a relevant taint source with the given initial
+   * `state`.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) { none() }
+
+  /**
+   * Holds if `sink` is a relevant taint sink
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSink(DataFlow::Node sink) { none() }
+
+  /**
+   * Holds if `sink` is a relevant taint sink accepting `state`.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) { none() }
+
+  /** Holds if the node `node` is a taint sanitizer. */
+  predicate isSanitizer(DataFlow::Node node) { none() }
+
+  final override predicate isBarrier(DataFlow::Node node) {
+    this.isSanitizer(node) or
+    defaultTaintSanitizer(node)
+  }
+
+  /**
+   * Holds if the node `node` is a taint sanitizer when the flow state is
+   * `state`.
+   */
+  predicate isSanitizer(DataFlow::Node node, DataFlow::FlowState state) { none() }
+
+  final override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) {
+    this.isSanitizer(node, state)
+  }
+
+  /** Holds if taint propagation into `node` is prohibited. */
+  predicate isSanitizerIn(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
+
+  /** Holds if taint propagation out of `node` is prohibited. */
+  predicate isSanitizerOut(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
+
+  /**
+   * DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
+   *
+   * Holds if taint propagation through nodes guarded by `guard` is prohibited.
+   */
+  deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
+
+  deprecated final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
+    this.isSanitizerGuard(guard)
+  }
+
+  /**
+   * DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
+   *
+   * Holds if taint propagation through nodes guarded by `guard` is prohibited
+   * when the flow state is `state`.
+   */
+  deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
+    none()
+  }
+
+  deprecated final override predicate isBarrierGuard(
+    DataFlow::BarrierGuard guard, DataFlow::FlowState state
+  ) {
+    this.isSanitizerGuard(guard, state)
+  }
+
+  /**
+   * Holds if taint may propagate from `node1` to `node2` in addition to the normal data-flow and taint steps.
+   */
+  predicate isAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) { none() }
+
+  final override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+    this.isAdditionalTaintStep(node1, node2) or
+    defaultAdditionalTaintStep(node1, node2)
+  }
+
+  /**
+   * Holds if taint may propagate from `node1` to `node2` in addition to the normal data-flow and taint steps.
+   * This step is only applicable in `state1` and updates the flow state to `state2`.
+   */
+  predicate isAdditionalTaintStep(
+    DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
+    DataFlow::FlowState state2
+  ) {
+    none()
+  }
+
+  final override predicate isAdditionalFlowStep(
+    DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
+    DataFlow::FlowState state2
+  ) {
+    this.isAdditionalTaintStep(node1, state1, node2, state2)
+  }
+
+  override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
+    (
+      this.isSink(node) or
+      this.isSink(node, _) or
+      this.isAdditionalTaintStep(node, _) or
+      this.isAdditionalTaintStep(node, _, _, _)
+    ) and
+    defaultImplicitTaintRead(node, c)
+  }
+
+  /**
+   * Holds if taint may flow from `source` to `sink` for this configuration.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate hasFlow(DataFlow::Node source, DataFlow::Node sink) {
+    super.hasFlow(source, sink)
+  }
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/tainttracking1/TaintTrackingParameter.qll

@@ -0,0 +1,5 @@
+import experimental.semmle.code.cpp.ir.dataflow.internal.TaintTrackingUtil as Public
+
+module Private {
+  import experimental.semmle.code.cpp.ir.dataflow.DataFlow::DataFlow as DataFlow
+}

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

@@ -0,0 +1,191 @@
+/**
+ * Provides an implementation of global (interprocedural) taint tracking.
+ * This file re-exports the local (intraprocedural) taint-tracking analysis
+ * from `TaintTrackingParameter::Public` and adds a global analysis, mainly
+ * exposed through the `Configuration` class. For some languages, this file
+ * exists in several identical copies, allowing queries to use multiple
+ * `Configuration` classes that depend on each other without introducing
+ * mutual recursion among those configurations.
+ */
+
+import TaintTrackingParameter::Public
+private import TaintTrackingParameter::Private
+
+/**
+ * A configuration of interprocedural taint tracking analysis. This defines
+ * sources, sinks, and any other configurable aspect of the analysis. Each
+ * use of the taint tracking library must define its own unique extension of
+ * this abstract class.
+ *
+ * A taint-tracking configuration is a special data flow configuration
+ * (`DataFlow::Configuration`) that allows for flow through nodes that do not
+ * necessarily preserve values but are still relevant from a taint tracking
+ * perspective. (For example, string concatenation, where one of the operands
+ * is tainted.)
+ *
+ * To create a configuration, extend this class with a subclass whose
+ * characteristic predicate is a unique singleton string. For example, write
+ *
+ * ```ql
+ * class MyAnalysisConfiguration extends TaintTracking::Configuration {
+ *   MyAnalysisConfiguration() { this = "MyAnalysisConfiguration" }
+ *   // Override `isSource` and `isSink`.
+ *   // Optionally override `isSanitizer`.
+ *   // Optionally override `isSanitizerIn`.
+ *   // Optionally override `isSanitizerOut`.
+ *   // Optionally override `isSanitizerGuard`.
+ *   // Optionally override `isAdditionalTaintStep`.
+ * }
+ * ```
+ *
+ * Then, to query whether there is flow between some `source` and `sink`,
+ * write
+ *
+ * ```ql
+ * exists(MyAnalysisConfiguration cfg | cfg.hasFlow(source, sink))
+ * ```
+ *
+ * Multiple configurations can coexist, but it is unsupported to depend on
+ * another `TaintTracking::Configuration` or a `DataFlow::Configuration` in the
+ * overridden predicates that define sources, sinks, or additional steps.
+ * Instead, the dependency should go to a `TaintTracking2::Configuration` or a
+ * `DataFlow2::Configuration`, `DataFlow3::Configuration`, etc.
+ */
+abstract class Configuration extends DataFlow::Configuration {
+  bindingset[this]
+  Configuration() { any() }
+
+  /**
+   * Holds if `source` is a relevant taint source.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSource(DataFlow::Node source) { none() }
+
+  /**
+   * Holds if `source` is a relevant taint source with the given initial
+   * `state`.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) { none() }
+
+  /**
+   * Holds if `sink` is a relevant taint sink
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSink(DataFlow::Node sink) { none() }
+
+  /**
+   * Holds if `sink` is a relevant taint sink accepting `state`.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) { none() }
+
+  /** Holds if the node `node` is a taint sanitizer. */
+  predicate isSanitizer(DataFlow::Node node) { none() }
+
+  final override predicate isBarrier(DataFlow::Node node) {
+    this.isSanitizer(node) or
+    defaultTaintSanitizer(node)
+  }
+
+  /**
+   * Holds if the node `node` is a taint sanitizer when the flow state is
+   * `state`.
+   */
+  predicate isSanitizer(DataFlow::Node node, DataFlow::FlowState state) { none() }
+
+  final override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) {
+    this.isSanitizer(node, state)
+  }
+
+  /** Holds if taint propagation into `node` is prohibited. */
+  predicate isSanitizerIn(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
+
+  /** Holds if taint propagation out of `node` is prohibited. */
+  predicate isSanitizerOut(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
+
+  /**
+   * DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
+   *
+   * Holds if taint propagation through nodes guarded by `guard` is prohibited.
+   */
+  deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
+
+  deprecated final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
+    this.isSanitizerGuard(guard)
+  }
+
+  /**
+   * DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
+   *
+   * Holds if taint propagation through nodes guarded by `guard` is prohibited
+   * when the flow state is `state`.
+   */
+  deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
+    none()
+  }
+
+  deprecated final override predicate isBarrierGuard(
+    DataFlow::BarrierGuard guard, DataFlow::FlowState state
+  ) {
+    this.isSanitizerGuard(guard, state)
+  }
+
+  /**
+   * Holds if taint may propagate from `node1` to `node2` in addition to the normal data-flow and taint steps.
+   */
+  predicate isAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) { none() }
+
+  final override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+    this.isAdditionalTaintStep(node1, node2) or
+    defaultAdditionalTaintStep(node1, node2)
+  }
+
+  /**
+   * Holds if taint may propagate from `node1` to `node2` in addition to the normal data-flow and taint steps.
+   * This step is only applicable in `state1` and updates the flow state to `state2`.
+   */
+  predicate isAdditionalTaintStep(
+    DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
+    DataFlow::FlowState state2
+  ) {
+    none()
+  }
+
+  final override predicate isAdditionalFlowStep(
+    DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
+    DataFlow::FlowState state2
+  ) {
+    this.isAdditionalTaintStep(node1, state1, node2, state2)
+  }
+
+  override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
+    (
+      this.isSink(node) or
+      this.isSink(node, _) or
+      this.isAdditionalTaintStep(node, _) or
+      this.isAdditionalTaintStep(node, _, _, _)
+    ) and
+    defaultImplicitTaintRead(node, c)
+  }
+
+  /**
+   * Holds if taint may flow from `source` to `sink` for this configuration.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate hasFlow(DataFlow::Node source, DataFlow::Node sink) {
+    super.hasFlow(source, sink)
+  }
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/tainttracking2/TaintTrackingParameter.qll

@@ -0,0 +1,5 @@
+import experimental.semmle.code.cpp.ir.dataflow.internal.TaintTrackingUtil as Public
+
+module Private {
+  import experimental.semmle.code.cpp.ir.dataflow.DataFlow2::DataFlow2 as DataFlow
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/tainttracking3/TaintTrackingImpl.qll

@@ -0,0 +1,191 @@
+/**
+ * Provides an implementation of global (interprocedural) taint tracking.
+ * This file re-exports the local (intraprocedural) taint-tracking analysis
+ * from `TaintTrackingParameter::Public` and adds a global analysis, mainly
+ * exposed through the `Configuration` class. For some languages, this file
+ * exists in several identical copies, allowing queries to use multiple
+ * `Configuration` classes that depend on each other without introducing
+ * mutual recursion among those configurations.
+ */
+
+import TaintTrackingParameter::Public
+private import TaintTrackingParameter::Private
+
+/**
+ * A configuration of interprocedural taint tracking analysis. This defines
+ * sources, sinks, and any other configurable aspect of the analysis. Each
+ * use of the taint tracking library must define its own unique extension of
+ * this abstract class.
+ *
+ * A taint-tracking configuration is a special data flow configuration
+ * (`DataFlow::Configuration`) that allows for flow through nodes that do not
+ * necessarily preserve values but are still relevant from a taint tracking
+ * perspective. (For example, string concatenation, where one of the operands
+ * is tainted.)
+ *
+ * To create a configuration, extend this class with a subclass whose
+ * characteristic predicate is a unique singleton string. For example, write
+ *
+ * ```ql
+ * class MyAnalysisConfiguration extends TaintTracking::Configuration {
+ *   MyAnalysisConfiguration() { this = "MyAnalysisConfiguration" }
+ *   // Override `isSource` and `isSink`.
+ *   // Optionally override `isSanitizer`.
+ *   // Optionally override `isSanitizerIn`.
+ *   // Optionally override `isSanitizerOut`.
+ *   // Optionally override `isSanitizerGuard`.
+ *   // Optionally override `isAdditionalTaintStep`.
+ * }
+ * ```
+ *
+ * Then, to query whether there is flow between some `source` and `sink`,
+ * write
+ *
+ * ```ql
+ * exists(MyAnalysisConfiguration cfg | cfg.hasFlow(source, sink))
+ * ```
+ *
+ * Multiple configurations can coexist, but it is unsupported to depend on
+ * another `TaintTracking::Configuration` or a `DataFlow::Configuration` in the
+ * overridden predicates that define sources, sinks, or additional steps.
+ * Instead, the dependency should go to a `TaintTracking2::Configuration` or a
+ * `DataFlow2::Configuration`, `DataFlow3::Configuration`, etc.
+ */
+abstract class Configuration extends DataFlow::Configuration {
+  bindingset[this]
+  Configuration() { any() }
+
+  /**
+   * Holds if `source` is a relevant taint source.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSource(DataFlow::Node source) { none() }
+
+  /**
+   * Holds if `source` is a relevant taint source with the given initial
+   * `state`.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) { none() }
+
+  /**
+   * Holds if `sink` is a relevant taint sink
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSink(DataFlow::Node sink) { none() }
+
+  /**
+   * Holds if `sink` is a relevant taint sink accepting `state`.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) { none() }
+
+  /** Holds if the node `node` is a taint sanitizer. */
+  predicate isSanitizer(DataFlow::Node node) { none() }
+
+  final override predicate isBarrier(DataFlow::Node node) {
+    this.isSanitizer(node) or
+    defaultTaintSanitizer(node)
+  }
+
+  /**
+   * Holds if the node `node` is a taint sanitizer when the flow state is
+   * `state`.
+   */
+  predicate isSanitizer(DataFlow::Node node, DataFlow::FlowState state) { none() }
+
+  final override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) {
+    this.isSanitizer(node, state)
+  }
+
+  /** Holds if taint propagation into `node` is prohibited. */
+  predicate isSanitizerIn(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
+
+  /** Holds if taint propagation out of `node` is prohibited. */
+  predicate isSanitizerOut(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
+
+  /**
+   * DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
+   *
+   * Holds if taint propagation through nodes guarded by `guard` is prohibited.
+   */
+  deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
+
+  deprecated final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) {
+    this.isSanitizerGuard(guard)
+  }
+
+  /**
+   * DEPRECATED: Use `isSanitizer` and `BarrierGuard` module instead.
+   *
+   * Holds if taint propagation through nodes guarded by `guard` is prohibited
+   * when the flow state is `state`.
+   */
+  deprecated predicate isSanitizerGuard(DataFlow::BarrierGuard guard, DataFlow::FlowState state) {
+    none()
+  }
+
+  deprecated final override predicate isBarrierGuard(
+    DataFlow::BarrierGuard guard, DataFlow::FlowState state
+  ) {
+    this.isSanitizerGuard(guard, state)
+  }
+
+  /**
+   * Holds if taint may propagate from `node1` to `node2` in addition to the normal data-flow and taint steps.
+   */
+  predicate isAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) { none() }
+
+  final override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+    this.isAdditionalTaintStep(node1, node2) or
+    defaultAdditionalTaintStep(node1, node2)
+  }
+
+  /**
+   * Holds if taint may propagate from `node1` to `node2` in addition to the normal data-flow and taint steps.
+   * This step is only applicable in `state1` and updates the flow state to `state2`.
+   */
+  predicate isAdditionalTaintStep(
+    DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
+    DataFlow::FlowState state2
+  ) {
+    none()
+  }
+
+  final override predicate isAdditionalFlowStep(
+    DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
+    DataFlow::FlowState state2
+  ) {
+    this.isAdditionalTaintStep(node1, state1, node2, state2)
+  }
+
+  override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
+    (
+      this.isSink(node) or
+      this.isSink(node, _) or
+      this.isAdditionalTaintStep(node, _) or
+      this.isAdditionalTaintStep(node, _, _, _)
+    ) and
+    defaultImplicitTaintRead(node, c)
+  }
+
+  /**
+   * Holds if taint may flow from `source` to `sink` for this configuration.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate hasFlow(DataFlow::Node source, DataFlow::Node sink) {
+    super.hasFlow(source, sink)
+  }
+}

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/tainttracking3/TaintTrackingParameter.qll

@@ -0,0 +1,5 @@
+import experimental.semmle.code.cpp.ir.dataflow.internal.TaintTrackingUtil as Public
+
+module Private {
+  import experimental.semmle.code.cpp.ir.dataflow.DataFlow3::DataFlow3 as DataFlow
+}

cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/Bound.qll

@@ -28,6 +28,10 @@ private newtype TBound =
       i.(LoadInstruction).getSourceAddress() instanceof FieldAddressInstruction
       or
       i.getAUse() instanceof ArgumentOperand
+      or
+      i instanceof PointerArithmeticInstruction
+      or
+      i.getAUse() instanceof AddressOperand
     )
   }
 
@@ -73,7 +77,7 @@ class ValueNumberBound extends Bound, TBoundValueNumber {
     this = TBoundValueNumber(valueNumber(result)) and delta = 0
   }
 
-  override string toString() { result = vn.getExampleInstruction().toString() }
+  override string toString() { result = "ValueNumberBound" }
 
   override Location getLocation() { result = vn.getLocation() }
 

cpp/ql/lib/experimental/semmle/code/cpp/semantic/SemanticExpr.qll

@@ -178,11 +178,11 @@ class SemRelationalExpr extends SemBinaryExpr {
 }
 
 class SemAddExpr extends SemBinaryExpr {
-  SemAddExpr() { opcode instanceof Opcode::Add }
+  SemAddExpr() { opcode instanceof Opcode::Add or opcode instanceof Opcode::PointerAdd }
 }
 
 class SemSubExpr extends SemBinaryExpr {
-  SemSubExpr() { opcode instanceof Opcode::Sub }
+  SemSubExpr() { opcode instanceof Opcode::Sub or opcode instanceof Opcode::PointerSub }
 }
 
 class SemMulExpr extends SemBinaryExpr {

cpp/ql/lib/experimental/semmle/code/cpp/semantic/SemanticExprSpecific.qll

@@ -112,12 +112,11 @@ module SemanticExprConfig {
 
   predicate hasDominanceInformation(BasicBlock block) { any() }
 
-  int getBasicBlockUniqueId(BasicBlock block) {
-    // REVIEW: `getDisplayIndex()` is not intended for use in real queries, but for now it's the
-    // best we can do because `equivalentRelation` won't accept a predicate whose parameters are IPA
-    // types.
-    result = block.getDisplayIndex()
-  }
+  private predicate id(Cpp::Locatable x, Cpp::Locatable y) { x = y }
+
+  private predicate idOf(Cpp::Locatable x, int y) = equivalenceRelation(id/2)(x, y)
+
+  int getBasicBlockUniqueId(BasicBlock block) { idOf(block.getFirstInstruction().getAst(), result) }
 
   newtype TSsaVariable =
     TSsaInstruction(IR::Instruction instr) { instr.hasMemoryResult() } or
@@ -162,7 +161,7 @@ module SemanticExprConfig {
   predicate phi(SsaVariable v) { v.asInstruction() instanceof IR::PhiInstruction }
 
   SsaVariable getAPhiInput(SsaVariable v) {
-    exists(IR::PhiInstruction instr |
+    exists(IR::PhiInstruction instr | v.asInstruction() = instr |
       result.asInstruction() = instr.getAnInput()
       or
       result.asOperand() = instr.getAnInputOperand()
@@ -267,17 +266,7 @@ module SemanticExprConfig {
 
     ValueNumberBound() { bound = this }
 
-    override string toString() {
-      result =
-        min(SsaVariable v |
-          v.asInstruction() = bound.getValueNumber().getAnInstruction()
-        |
-          v
-          order by
-            v.asInstruction().getBlock().getDisplayIndex(),
-            v.asInstruction().getDisplayIndexInBlock()
-        ).toString()
-    }
+    override string toString() { result = bound.toString() }
   }
 
   predicate zeroBound(Bound bound) { bound instanceof IRBound::ZeroBound }

cpp/ql/lib/experimental/semmle/code/cpp/semantic/SemanticOpcode.qll

@@ -65,10 +65,18 @@ module Opcode {
     override string toString() { result = "Add" }
   }
 
+  class PointerAdd extends Opcode, TPointerAdd {
+    override string toString() { result = "PointerAdd" }
+  }
+
   class Sub extends Opcode, TSub {
     override string toString() { result = "Sub" }
   }
 
+  class PointerSub extends Opcode, TPointerSub {
+    override string toString() { result = "PointerSub" }
+  }
+
   class Mul extends Opcode, TMul {
     override string toString() { result = "Mul" }
   }

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll

@@ -223,7 +223,9 @@ private SemGuard boundFlowCond(
       else resultIsStrict = testIsTrue.booleanNot()
     ) and
     (
-      if getTrackedTypeForSsaVariable(v) instanceof SemIntegerType
+      if
+        getTrackedTypeForSsaVariable(v) instanceof SemIntegerType or
+        getTrackedTypeForSsaVariable(v) instanceof SemAddressType
       then
         upper = true and strengthen = -1
         or
@@ -542,12 +544,32 @@ private predicate unequalIntegralSsa(
 ) {
   exists(SemExpr e, int d1, int d2 |
     unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
-    bounded(e, b, d2, true, _, _, _) and
-    bounded(e, b, d2, false, _, _, _) and
+    boundedUpper(e, b, d1) and
+    boundedLower(e, b, d2) and
     delta = d2 + d1
   )
 }
 
+/**
+ * Holds if `b + delta` is an upper bound for `e`.
+ *
+ * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
+ */
+pragma[nomagic]
+private predicate boundedUpper(SemExpr e, SemBound b, int delta) {
+  bounded(e, b, delta, true, _, _, _)
+}
+
+/**
+ * Holds if `b + delta` is a lower bound for `e`.
+ *
+ * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
+ */
+pragma[nomagic]
+private predicate boundedLower(SemExpr e, SemBound b, int delta) {
+  bounded(e, b, delta, false, _, _, _)
+}
+
 /** Weakens a delta to lie in the range `[-1..1]`. */
 bindingset[delta, upper]
 private int weakenDelta(boolean upper, int delta) {

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SignAnalysisCommon.qll

@@ -204,6 +204,7 @@ private class BinarySignExpr extends FlowSignExpr {
   }
 }
 
+pragma[nomagic]
 private predicate binaryExprOperands(SemBinaryExpr binary, SemExpr left, SemExpr right) {
   binary.getLeftOperand() = left and binary.getRightOperand() = right
 }

cpp/ql/lib/qlpack.yml

@@ -5,3 +5,5 @@ dbscheme: semmlecode.cpp.dbscheme
 extractor: cpp
 library: true
 upgrades: upgrades
+dependencies:
+  codeql/ssa: 0.0.1

cpp/ql/lib/semmle/code/cpp/Class.qll

@@ -404,7 +404,10 @@ class Class extends UserType {
    * compiled for. For this reason, the `is_pod_class` predicate is
    * generated by the extractor.
    */
-  predicate isPOD() { is_pod_class(underlyingElement(this)) }
+  predicate isPod() { is_pod_class(underlyingElement(this)) }
+
+  /** DEPRECATED: Alias for isPod */
+  deprecated predicate isPOD() { this.isPod() }
 
   /**
    * Holds if this class, struct or union is a standard-layout class

cpp/ql/lib/semmle/code/cpp/PODType03.qll

@@ -79,17 +79,17 @@ predicate isAggregateType03(Type t) {
  *   user-defined copy assignment operator and no user-defined destructor.
  *   A POD class is a class that is either a POD-struct or a POD-union.
  */
-predicate isPODClass03(Class c) {
+predicate isPodClass03(Class c) {
   isAggregateClass03(c) and
   not exists(Variable v |
     v.getDeclaringType() = c and
     not v.isStatic()
   |
-    not isPODType03(v.getType())
+    not isPodType03(v.getType())
     or
     exists(ArrayType at |
       at = v.getType() and
-      not isPODType03(at.getBaseType())
+      not isPodType03(at.getBaseType())
     )
     or
     v.getType() instanceof ReferenceType
@@ -104,6 +104,9 @@ predicate isPODClass03(Class c) {
   )
 }
 
+/** DEPRECATED: Alias for isPodClass03 */
+deprecated predicate isPODClass03 = isPodClass03/1;
+
 /**
  * Holds if `t` is a POD type, according to the rules specified in
  * C++03 3.9(10):
@@ -112,14 +115,17 @@ predicate isPODClass03(Class c) {
  *   such types and cv-qualified versions of these types (3.9.3) are
  *   collectively called POD types.
  */
-predicate isPODType03(Type t) {
+predicate isPodType03(Type t) {
   exists(Type ut | ut = t.getUnderlyingType() |
     isScalarType03(ut)
     or
-    isPODClass03(ut)
+    isPodClass03(ut)
     or
-    exists(ArrayType at | at = ut and isPODType03(at.getBaseType()))
+    exists(ArrayType at | at = ut and isPodType03(at.getBaseType()))
     or
-    isPODType03(ut.(SpecifiedType).getUnspecifiedType())
+    isPodType03(ut.(SpecifiedType).getUnspecifiedType())
   )
 }
+
+/** DEPRECATED: Alias for isPodType03 */
+deprecated predicate isPODType03 = isPodType03/1;

cpp/ql/lib/semmle/code/cpp/commons/Dependency.qll

@@ -238,7 +238,7 @@ predicate dependsOnTransitive(DependsSource src, Element dest) {
 /**
  * A dependency that targets a TypeDeclarationEntry.
  */
-private predicate dependsOnTDE(Element src, Type t, TypeDeclarationEntry dest) {
+private predicate dependsOnTde(Element src, Type t, TypeDeclarationEntry dest) {
   dependsOnTransitive(src, t) and
   getDeclarationEntries(t, dest)
 }
@@ -247,8 +247,8 @@ private predicate dependsOnTDE(Element src, Type t, TypeDeclarationEntry dest) {
  * A dependency that targets a visible TypeDeclarationEntry.
  */
 pragma[noopt]
-private predicate dependsOnVisibleTDE(Element src, Type t, TypeDeclarationEntry dest) {
-  dependsOnTDE(src, t, dest) and
+private predicate dependsOnVisibleTde(Element src, Type t, TypeDeclarationEntry dest) {
+  dependsOnTde(src, t, dest) and
   exists(File g | g = dest.getFile() |
     exists(File f | f = src.getFile() | f.getAnIncludedFile*() = g)
   )
@@ -260,8 +260,8 @@ private predicate dependsOnVisibleTDE(Element src, Type t, TypeDeclarationEntry
 private predicate dependsOnDeclarationEntry(Element src, DeclarationEntry dest) {
   exists(Type t |
     // dependency from a Type use -> unique visible TDE
-    dependsOnVisibleTDE(src, t, dest) and
-    strictcount(TypeDeclarationEntry alt | dependsOnVisibleTDE(src, t, alt)) = 1
+    dependsOnVisibleTde(src, t, dest) and
+    strictcount(TypeDeclarationEntry alt | dependsOnVisibleTde(src, t, alt)) = 1
   )
   or
   exists(TypedefType mid |

cpp/ql/lib/semmle/code/cpp/commons/NULL.qll

@@ -1,11 +1,14 @@
 import semmle.code.cpp.Macro
 
 /** A macro defining NULL. */
-class NULLMacro extends Macro {
-  NULLMacro() { this.getHead() = "NULL" }
+class NullMacro extends Macro {
+  NullMacro() { this.getHead() = "NULL" }
 }
 
+/** DEPRECATED: Alias for NullMacro */
+deprecated class NULLMacro = NullMacro;
+
 /** A use of the NULL macro. */
 class NULL extends Literal {
-  NULL() { exists(NULLMacro nm | this = nm.getAnInvocation().getAnExpandedElement()) }
+  NULL() { exists(NullMacro nm | this = nm.getAnInvocation().getAnExpandedElement()) }
 }

cpp/ql/lib/semmle/code/cpp/commons/Scanf.qll

@@ -143,6 +143,28 @@ class ScanfFunctionCall extends FunctionCall {
    * (rather than a `char*`).
    */
   predicate isWideCharDefault() { this.getScanfFunction().isWideCharDefault() }
+
+  /**
+   * Gets the output argument at position `n` in the vararg list of this call.
+   *
+   * The range of `n` is from `0` to `this.getNumberOfOutputArguments() - 1`.
+   */
+  Expr getOutputArgument(int n) {
+    result = this.getArgument(this.getTarget().getNumberOfParameters() + n) and
+    n >= 0
+  }
+
+  /**
+   * Gets an output argument given to this call in vararg position.
+   */
+  Expr getAnOutputArgument() { result = this.getOutputArgument(_) }
+
+  /**
+   * Gets the number of output arguments present in this call.
+   */
+  int getNumberOfOutputArguments() {
+    result = this.getNumberOfArguments() - this.getTarget().getNumberOfParameters()
+  }
 }
 
 /**

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

@@ -474,7 +474,7 @@ module FlowVar_internal {
   }
 
   /** Type-specialized version of `getEnclosingElement`. */
-  private ControlFlowNode getCFNParent(ControlFlowNode node) { result = node.getEnclosingElement() }
+  private ControlFlowNode getCfnParent(ControlFlowNode node) { result = node.getEnclosingElement() }
 
   /**
    * A for-loop or while-loop whose condition is always true upon entry but not
@@ -526,7 +526,7 @@ module FlowVar_internal {
     }
 
     private predicate bbInLoopCondition(BasicBlock bb) {
-      getCFNParent*(bb.getANode()) = this.(Loop).getCondition()
+      getCfnParent*(bb.getANode()) = this.(Loop).getCondition()
     }
 
     private predicate bbInLoop(BasicBlock bb) {

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

@@ -172,7 +172,12 @@ abstract class Configuration extends DataFlow::Configuration {
   }
 
   override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
-    (this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
+    (
+      this.isSink(node) or
+      this.isSink(node, _) or
+      this.isAdditionalTaintStep(node, _) or
+      this.isAdditionalTaintStep(node, _, _, _)
+    ) and
     defaultImplicitTaintRead(node, c)
   }
 

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

@@ -172,7 +172,12 @@ abstract class Configuration extends DataFlow::Configuration {
   }
 
   override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
-    (this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
+    (
+      this.isSink(node) or
+      this.isSink(node, _) or
+      this.isAdditionalTaintStep(node, _) or
+      this.isAdditionalTaintStep(node, _, _, _)
+    ) and
     defaultImplicitTaintRead(node, c)
   }
 

cpp/ql/lib/semmle/code/cpp/exprs/BuiltInOperations.qll

@@ -1040,6 +1040,494 @@ class BuiltInOperationHasUniqueObjectRepresentations extends BuiltInOperation,
   override string getAPrimaryQlClass() { result = "BuiltInOperationHasUniqueObjectRepresentations" }
 }
 
+/**
+ * A C++ `__is_same` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if two types are the same.
+ * ```
+ * template<typename _Tp, typename _Up>
+ *   struct is_same
+ *   : public integral_constant<bool, __is_same(_Tp, _Up)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsSame extends BuiltInOperation, @issame {
+  override string toString() { result = "__is_same" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsSame" }
+}
+
+/**
+ * A C++ `__is_function` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is a function type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_function
+ *   : public integral_constant<bool, __is_function(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsFunction extends BuiltInOperation, @isfunction {
+  override string toString() { result = "__is_function" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsFunction" }
+}
+
+/**
+ * A C++ `__is_layout_compatible` built-in operation (used by some implementations
+ * of the `<type_traits>` header).
+ *
+ * Returns `true` if two types are layout-compatible.
+ * ```
+ * template<typename _Tp, typename _Up>
+ *   struct is_layout_compatible
+ *   : public integral_constant<bool, __is_layout_compatible(_Tp, _Up)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsLayoutCompatible extends BuiltInOperation, @islayoutcompatible {
+  override string toString() { result = "__is_layout_compatible" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsLayoutCompatible" }
+}
+
+/**
+ * A C++ `__is_pointer_interconvertible_base_of` built-in operation (used
+ * by some implementations of the `<type_traits>` header).
+ *
+ * Returns `true` if the second type is pointer-interconvertible with the first type.
+ * ```
+ * template<typename _Tp, typename _Up>
+ *   struct is_pointer_interconvertible_base_of_v
+ *   : public integral_constant<bool, __is_pointer_interconvertible_base_of(_Tp, _Up)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsPointerInterconvertibleBaseOf extends BuiltInOperation,
+  @ispointerinterconvertiblebaseof {
+  override string toString() { result = "__is_pointer_interconvertible_base_of" }
+
+  override string getAPrimaryQlClass() {
+    result = "BuiltInOperationIsPointerInterconvertibleBaseOf"
+  }
+}
+
+/**
+ * A C++ `__is_array` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is an array type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_array
+ *   : public integral_constant<bool, __is_array(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsArray extends BuiltInOperation, @isarray {
+  override string toString() { result = "__is_array" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsArray" }
+}
+
+/**
+ * A C++ `__array_rank` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * If known, returns the number of dimentsions of an arrary type.
+ * ```
+ * template<typename _Tp>
+ *   struct rank
+ *   : public integral_constant<size_t, __array_rank(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationArrayRank extends BuiltInOperation, @arrayrank {
+  override string toString() { result = "__array_rank" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationArrayRank" }
+}
+
+/**
+ * A C++ `__array_extent` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * If known, returns the number of elements of an arrary type in the specified
+ * dimension.
+ * ```
+ * template<typename _Tp,  unsigned int _Dim>
+ *   struct extent
+ *   : public integral_constant<size_t, __array_extent(_Tp, _Dim)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationArrayExtent extends BuiltInOperation, @arrayextent {
+  override string toString() { result = "__array_extent" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationArrayExtent" }
+}
+
+/**
+ * A C++ `__is_arithmetic` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is an arithmetic type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_arithmetic
+ *   : public integral_constant<bool, __is_arithmetic(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsArithmetic extends BuiltInOperation, @isarithmetic {
+  override string toString() { result = "__is_arithmetic" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsArithmetic" }
+}
+
+/**
+ * A C++ `__is_complete_type` built-in operation.
+ *
+ * Returns `true` if a type is a complete type. Note that this built-in operation
+ * can return different values for the same type at different points in a program.
+ * ```
+ * class S;
+ * bool b = __complete_type(S);
+ * ```
+ */
+class BuiltInOperationIsCompleteType extends BuiltInOperation, @iscompletetype {
+  override string toString() { result = "__is_complete_type" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsCompleteType" }
+}
+
+/**
+ * A C++ `__is_compound` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is a compound type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_compound
+ *   : public integral_constant<bool, __is_compound(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsCompound extends BuiltInOperation, @iscompound {
+  override string toString() { result = "__is_compound" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsCompound" }
+}
+
+/**
+ * A C++ `__is_const` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is a const-qualified type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_const
+ *   : public integral_constant<bool, __is_const(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsConst extends BuiltInOperation, @isconst {
+  override string toString() { result = "__is_const" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsConst" }
+}
+
+/**
+ * A C++ `__is_floating_point` built-in operation (used by some implementations
+ * of the `<type_traits>` header).
+ *
+ * Returns `true` if a type is a floating point type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_floating_point
+ *   : public integral_constant<bool, __is_floating_point(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsFloatingPoint extends BuiltInOperation, @isfloatingpoint {
+  override string toString() { result = "__is_floating_point" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsFloatingPoint" }
+}
+
+/**
+ * A C++ `__is_fundamental` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is a fundamental C++ type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_fundamental
+ *   : public integral_constant<bool, __is_fundamental(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsFundamental extends BuiltInOperation, @isfundamental {
+  override string toString() { result = "__is_fundamental" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsFundamental" }
+}
+
+/**
+ * A C++ `__is_integral` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is an integral type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_integral
+ *   : public integral_constant<bool, __is_integral(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsIntegral extends BuiltInOperation, @isintegral {
+  override string toString() { result = "__is_integral" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsIntegral" }
+}
+
+/**
+ * A C++ `__is_lvalue_reference` built-in operation (used by some implementations
+ * of the `<type_traits>` header).
+ *
+ * Returns `true` if a type is an lvalue reference type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_lvalue_reference
+ *   : public integral_constant<bool, __is_lvalue_reference(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsLvalueReference extends BuiltInOperation, @islvaluereference {
+  override string toString() { result = "__is_lvalue_reference" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsLvalueReference" }
+}
+
+/**
+ * A C++ `__is_member_function_pointer` built-in operation (used by some implementations
+ * of the `<type_traits>` header).
+ *
+ * Returns `true` if a type is an non-static member function pointer type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_member_function_pointer
+ *   : public integral_constant<bool, __is_member_function_pointer(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsMemberFunctionPointer extends BuiltInOperation, @ismemberfunctionpointer {
+  override string toString() { result = "__is_member_function_pointer" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsMemberFunctionPointer" }
+}
+
+/**
+ * A C++ `__is_member_object_pointer` built-in operation (used by some implementations
+ * of the `<type_traits>` header).
+ *
+ * Returns `true` if a type is an non-static member object pointer type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_member_object_pointer
+ *   : public integral_constant<bool, __is_member_object_pointer(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsMemberObjectPointer extends BuiltInOperation, @ismemberobjectpointer {
+  override string toString() { result = "__is_member_object_pointer" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsMemberObjectPointer" }
+}
+
+/**
+ * A C++ `__is_member_pointer` built-in operation (used by some implementations
+ * of the `<type_traits>` header).
+ *
+ * Returns `true` if a type is an non-static member object of function pointer type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_member_pointer
+ *   : public integral_constant<bool, __is_member_pointer(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsMemberPointer extends BuiltInOperation, @ismemberpointer {
+  override string toString() { result = "__is_member_pointer" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsMemberPointer" }
+}
+
+/**
+ * A C++ `__is_object` built-in operation (used by some implementations
+ * of the `<type_traits>` header).
+ *
+ * Returns `true` if a type is an object type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_object
+ *   : public integral_constant<bool, __is_object(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsObject extends BuiltInOperation, @isobject {
+  override string toString() { result = "__is_object" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsObject" }
+}
+
+/**
+ * A C++ `__is_pointer` built-in operation (used by some implementations
+ * of the `<type_traits>` header).
+ *
+ * Returns `true` if a type is a pointer to an object or function type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_pointer
+ *   : public integral_constant<bool, __is_pointer(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsPointer extends BuiltInOperation, @ispointer {
+  override string toString() { result = "__is_pointer" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsPointer" }
+}
+
+/**
+ * A C++ `__is_reference` built-in operation (used by some implementations
+ * of the `<type_traits>` header).
+ *
+ * Returns `true` if a type is an lvalue or rvalue reference type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_reference
+ *   : public integral_constant<bool, __is_reference(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsReference extends BuiltInOperation, @isreference {
+  override string toString() { result = "__is_reference" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsReference" }
+}
+
+/**
+ * A C++ `__is_rvalue_reference` built-in operation (used by some implementations
+ * of the `<type_traits>` header).
+ *
+ * Returns `true` if a type is an rvalue reference type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_rvalue_reference
+ *   : public integral_constant<bool, __is_rvalue_reference(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsRvalueReference extends BuiltInOperation, @isrvaluereference {
+  override string toString() { result = "__is_rvalue_reference" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsRvalueReference" }
+}
+
+/**
+ * A C++ `__is_scalar` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is a scalar type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_scalar
+ *   : public integral_constant<bool, __is_scalar(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsScalar extends BuiltInOperation, @isscalar {
+  override string toString() { result = "__is_scalar" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsScalar" }
+}
+
+/**
+ * A C++ `__is_signed` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is a signed arithmetic type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_signed
+ *   : public integral_constant<bool, __is_signed(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsSigned extends BuiltInOperation, @issigned {
+  override string toString() { result = "__is_signed" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsSigned" }
+}
+
+/**
+ * A C++ `__is_unsigned` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is an unsigned arithmetic type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_unsigned
+ *   : public integral_constant<bool, __is_unsigned(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsUnsigned extends BuiltInOperation, @isunsigned {
+  override string toString() { result = "__is_unsigned" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsUnsigned" }
+}
+
+/**
+ * A C++ `__is_void` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is a void type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_void
+ *   : public integral_constant<bool, __is_void(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsVoid extends BuiltInOperation, @isvoid {
+  override string toString() { result = "__is_void" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsVoid" }
+}
+
+/**
+ * A C++ `__is_volatile` built-in operation (used by some implementations of the
+ * `<type_traits>` header).
+ *
+ * Returns `true` if a type is a volatile-qualified type.
+ * ```
+ * template<typename _Tp>
+ *   struct is_volatile
+ *   : public integral_constant<bool, __is_volatile(_Tp)>
+ *   { };
+ * ```
+ */
+class BuiltInOperationIsVolatile extends BuiltInOperation, @isvolatile {
+  override string toString() { result = "__is_volatile" }
+
+  override string getAPrimaryQlClass() { result = "BuiltInOperationIsVolatile" }
+}
+
 /**
  * A C/C++ `__builtin_bit_cast` built-in operation (used by some implementations
  * of `std::bit_cast`).

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

@@ -1,795 +0,0 @@
-/**
- * Provides a language-independent implementation of static single assignment
- * (SSA) form.
- */
-
-private import SsaImplSpecific
-
-private BasicBlock getABasicBlockPredecessor(BasicBlock bb) { getABasicBlockSuccessor(result) = bb }
-
-/**
- * Liveness analysis (based on source variables) to restrict the size of the
- * SSA representation.
- */
-private module Liveness {
-  /**
-   * A classification of variable references into reads (of a given kind) and
-   * (certain or uncertain) writes.
-   */
-  private newtype TRefKind =
-    Read(boolean certain) { certain in [false, true] } or
-    Write(boolean certain) { certain in [false, true] }
-
-  private class RefKind extends TRefKind {
-    string toString() {
-      exists(boolean certain | this = Read(certain) and result = "read (" + certain + ")")
-      or
-      exists(boolean certain | this = Write(certain) and result = "write (" + certain + ")")
-    }
-
-    int getOrder() {
-      this = Read(_) and
-      result = 0
-      or
-      this = Write(_) and
-      result = 1
-    }
-  }
-
-  /**
-   * Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.
-   */
-  predicate ref(BasicBlock bb, int i, SourceVariable v, RefKind k) {
-    exists(boolean certain | variableRead(bb, i, v, certain) | k = Read(certain))
-    or
-    exists(boolean certain | variableWrite(bb, i, v, certain) | k = Write(certain))
-  }
-
-  private newtype OrderedRefIndex =
-    MkOrderedRefIndex(int i, int tag) {
-      exists(RefKind rk | ref(_, i, _, rk) | tag = rk.getOrder())
-    }
-
-  private OrderedRefIndex refOrd(BasicBlock bb, int i, SourceVariable v, RefKind k, int ord) {
-    ref(bb, i, v, k) and
-    result = MkOrderedRefIndex(i, ord) and
-    ord = k.getOrder()
-  }
-
-  /**
-   * Gets the (1-based) rank of the reference to `v` at the `i`th node of
-   * basic block `bb`, which has the given reference kind `k`.
-   *
-   * Reads are considered before writes when they happen at the same index.
-   */
-  private int refRank(BasicBlock bb, int i, SourceVariable v, RefKind k) {
-    refOrd(bb, i, v, k, _) =
-      rank[result](int j, int ord, OrderedRefIndex res |
-        res = refOrd(bb, j, v, _, ord)
-      |
-        res order by j, ord
-      )
-  }
-
-  private int maxRefRank(BasicBlock bb, SourceVariable v) {
-    result = refRank(bb, _, v, _) and
-    not result + 1 = refRank(bb, _, v, _)
-  }
-
-  predicate lastRefIsRead(BasicBlock bb, SourceVariable v) {
-    maxRefRank(bb, v) = refRank(bb, _, v, Read(_))
-  }
-
-  /**
-   * Gets the (1-based) rank of the first reference to `v` inside basic block `bb`
-   * that is either a read or a certain write.
-   */
-  private int firstReadOrCertainWrite(BasicBlock bb, SourceVariable v) {
-    result =
-      min(int r, RefKind k |
-        r = refRank(bb, _, v, k) and
-        k != Write(false)
-      |
-        r
-      )
-  }
-
-  /**
-   * Holds if source variable `v` is live at the beginning of basic block `bb`.
-   */
-  predicate liveAtEntry(BasicBlock bb, SourceVariable v) {
-    // The first read or certain write to `v` inside `bb` is a read
-    refRank(bb, _, v, Read(_)) = firstReadOrCertainWrite(bb, v)
-    or
-    // There is no certain write to `v` inside `bb`, but `v` is live at entry
-    // to a successor basic block of `bb`
-    not exists(firstReadOrCertainWrite(bb, v)) and
-    liveAtExit(bb, v)
-  }
-
-  /**
-   * Holds if source variable `v` is live at the end of basic block `bb`.
-   */
-  predicate liveAtExit(BasicBlock bb, SourceVariable v) {
-    liveAtEntry(getABasicBlockSuccessor(bb), v)
-  }
-
-  /**
-   * Holds if variable `v` is live in basic block `bb` at index `i`.
-   * The rank of `i` is `rnk` as defined by `refRank()`.
-   */
-  private predicate liveAtRank(BasicBlock bb, int i, SourceVariable v, int rnk) {
-    exists(RefKind kind | rnk = refRank(bb, i, v, kind) |
-      rnk = maxRefRank(bb, v) and
-      liveAtExit(bb, v)
-      or
-      ref(bb, i, v, kind) and
-      kind = Read(_)
-      or
-      exists(RefKind nextKind |
-        liveAtRank(bb, _, v, rnk + 1) and
-        rnk + 1 = refRank(bb, _, v, nextKind) and
-        nextKind != Write(true)
-      )
-    )
-  }
-
-  /**
-   * Holds if variable `v` is live after the (certain or uncertain) write at
-   * index `i` inside basic block `bb`.
-   */
-  predicate liveAfterWrite(BasicBlock bb, int i, SourceVariable v) {
-    exists(int rnk | rnk = refRank(bb, i, v, Write(_)) | liveAtRank(bb, i, v, rnk))
-  }
-}
-
-private import Liveness
-
-/**
- * Holds if `df` is in the dominance frontier of `bb`.
- *
- * This is equivalent to:
- *
- * ```ql
- * bb = getImmediateBasicBlockDominator*(getABasicBlockPredecessor(df)) and
- * not bb = getImmediateBasicBlockDominator+(df)
- * ```
- */
-private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
-  bb = getABasicBlockPredecessor(df) and not bb = getImmediateBasicBlockDominator(df)
-  or
-  exists(BasicBlock prev | inDominanceFrontier(prev, df) |
-    bb = getImmediateBasicBlockDominator(prev) and
-    not bb = getImmediateBasicBlockDominator(df)
-  )
-}
-
-/**
- * Holds if `bb` is in the dominance frontier of a block containing a
- * definition of `v`.
- */
-pragma[noinline]
-private predicate inDefDominanceFrontier(BasicBlock bb, SourceVariable v) {
-  exists(BasicBlock defbb, Definition def |
-    def.definesAt(v, defbb, _) and
-    inDominanceFrontier(defbb, bb)
-  )
-}
-
-cached
-newtype TDefinition =
-  TWriteDef(SourceVariable v, BasicBlock bb, int i) {
-    variableWrite(bb, i, v, _) and
-    liveAfterWrite(bb, i, v)
-  } or
-  TPhiNode(SourceVariable v, BasicBlock bb) {
-    inDefDominanceFrontier(bb, v) and
-    liveAtEntry(bb, v)
-  }
-
-private module SsaDefReaches {
-  newtype TSsaRefKind =
-    SsaActualRead() or
-    SsaPhiRead() or
-    SsaDef()
-
-  class SsaRead = SsaActualRead or SsaPhiRead;
-
-  /**
-   * A classification of SSA variable references into reads and definitions.
-   */
-  class SsaRefKind extends TSsaRefKind {
-    string toString() {
-      this = SsaActualRead() and
-      result = "SsaActualRead"
-      or
-      this = SsaPhiRead() and
-      result = "SsaPhiRead"
-      or
-      this = SsaDef() and
-      result = "SsaDef"
-    }
-
-    int getOrder() {
-      this instanceof SsaRead and
-      result = 0
-      or
-      this = SsaDef() and
-      result = 1
-    }
-  }
-
-  /**
-   * Holds if `bb` is in the dominance frontier of a block containing a
-   * read of `v`.
-   */
-  pragma[nomagic]
-  private predicate inReadDominanceFrontier(BasicBlock bb, SourceVariable v) {
-    exists(BasicBlock readbb | inDominanceFrontier(readbb, bb) |
-      lastRefIsRead(readbb, v)
-      or
-      phiRead(readbb, v)
-    )
-  }
-
-  /**
-   * Holds if a phi-read node should be inserted for variable `v` at the beginning
-   * of basic block `bb`.
-   *
-   * Phi-read nodes are like normal phi nodes, but they are inserted based on reads
-   * instead of writes, and only if the dominance-frontier block does not already
-   * contain a reference (read or write) to `v`. Unlike normal phi nodes, this is
-   * an internal implementation detail that is not exposed.
-   *
-   * The motivation for adding phi-reads is to improve performance of the use-use
-   * calculation in cases where there is a large number of reads that can reach the
-   * same join-point, and from there reach a large number of basic blocks. Example:
-   *
-   * ```cs
-   * if (a)
-   *   use(x);
-   * else if (b)
-   *   use(x);
-   * else if (c)
-   *   use(x);
-   * else if (d)
-   *   use(x);
-   * // many more ifs ...
-   *
-   * // phi-read for `x` inserted here
-   *
-   * // program not mentioning `x`, with large basic block graph
-   *
-   * use(x);
-   * ```
-   *
-   * Without phi-reads, the analysis has to replicate reachability for each of
-   * the guarded uses of `x`. However, with phi-reads, the analysis will limit
-   * each conditional use of `x` to reach the basic block containing the phi-read
-   * node for `x`, and only that basic block will have to compute reachability
-   * through the remainder of the large program.
-   *
-   * Like normal reads, each phi-read node `phi-read` can be reached from exactly
-   * one SSA definition (without passing through another definition): Assume, for
-   * the sake of contradiction, that there are two reaching definitions `def1` and
-   * `def2`. Now, if both `def1` and `def2` dominate `phi-read`, then the nearest
-   * dominating definition will prevent the other from reaching `phi-read`. So, at
-   * least one of `def1` and `def2` cannot dominate `phi-read`; assume it is `def1`.
-   * Then `def1` must go through one of its dominance-frontier blocks in order to
-   * reach `phi-read`. However, such a block will always start with a (normal) phi
-   * node, which contradicts reachability.
-   *
-   * Also, like normal reads, the unique SSA definition `def` that reaches `phi-read`,
-   * will dominate `phi-read`. Assuming it doesn't means that the path from `def`
-   * to `phi-read` goes through a dominance-frontier block, and hence a phi node,
-   * which contradicts reachability.
-   */
-  pragma[nomagic]
-  predicate phiRead(BasicBlock bb, SourceVariable v) {
-    inReadDominanceFrontier(bb, v) and
-    liveAtEntry(bb, v) and
-    // only if there are no other references to `v` inside `bb`
-    not ref(bb, _, v, _) and
-    not exists(Definition def | def.definesAt(v, bb, _))
-  }
-
-  /**
-   * Holds if the `i`th node of basic block `bb` is a reference to `v`,
-   * either a read (when `k` is `SsaRead()`) or an SSA definition (when `k`
-   * is `SsaDef()`).
-   *
-   * Unlike `Liveness::ref`, this includes `phi` nodes.
-   */
-  pragma[nomagic]
-  predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
-    variableRead(bb, i, v, _) and
-    k = SsaActualRead()
-    or
-    phiRead(bb, v) and
-    i = -1 and
-    k = SsaPhiRead()
-    or
-    any(Definition def).definesAt(v, bb, i) and
-    k = SsaDef()
-  }
-
-  private newtype OrderedSsaRefIndex =
-    MkOrderedSsaRefIndex(int i, SsaRefKind k) { ssaRef(_, i, _, k) }
-
-  private OrderedSsaRefIndex ssaRefOrd(BasicBlock bb, int i, SourceVariable v, SsaRefKind k, int ord) {
-    ssaRef(bb, i, v, k) and
-    result = MkOrderedSsaRefIndex(i, k) and
-    ord = k.getOrder()
-  }
-
-  /**
-   * Gets the (1-based) rank of the reference to `v` at the `i`th node of basic
-   * block `bb`, which has the given reference kind `k`.
-   *
-   * For example, if `bb` is a basic block with a phi node for `v` (considered
-   * to be at index -1), reads `v` at node 2, and defines it at node 5, we have:
-   *
-   * ```ql
-   * ssaRefRank(bb, -1, v, SsaDef()) = 1    // phi node
-   * ssaRefRank(bb,  2, v, Read())   = 2    // read at node 2
-   * ssaRefRank(bb,  5, v, SsaDef()) = 3    // definition at node 5
-   * ```
-   *
-   * Reads are considered before writes when they happen at the same index.
-   */
-  int ssaRefRank(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
-    ssaRefOrd(bb, i, v, k, _) =
-      rank[result](int j, int ord, OrderedSsaRefIndex res |
-        res = ssaRefOrd(bb, j, v, _, ord)
-      |
-        res order by j, ord
-      )
-  }
-
-  int maxSsaRefRank(BasicBlock bb, SourceVariable v) {
-    result = ssaRefRank(bb, _, v, _) and
-    not result + 1 = ssaRefRank(bb, _, v, _)
-  }
-
-  /**
-   * Holds if the SSA definition `def` reaches rank index `rnk` in its own
-   * basic block `bb`.
-   */
-  predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rnk, SourceVariable v) {
-    exists(int i |
-      rnk = ssaRefRank(bb, i, v, SsaDef()) and
-      def.definesAt(v, bb, i)
-    )
-    or
-    ssaDefReachesRank(bb, def, rnk - 1, v) and
-    rnk = ssaRefRank(bb, _, v, any(SsaRead k))
-  }
-
-  /**
-   * Holds if the SSA definition of `v` at `def` reaches index `i` in the same
-   * basic block `bb`, without crossing another SSA definition of `v`.
-   */
-  predicate ssaDefReachesReadWithinBlock(SourceVariable v, Definition def, BasicBlock bb, int i) {
-    exists(int rnk |
-      ssaDefReachesRank(bb, def, rnk, v) and
-      rnk = ssaRefRank(bb, i, v, any(SsaRead k))
-    )
-  }
-
-  /**
-   * Same as `ssaRefRank()`, but restricted to a particular SSA definition `def`.
-   */
-  int ssaDefRank(Definition def, SourceVariable v, BasicBlock bb, int i, SsaRefKind k) {
-    v = def.getSourceVariable() and
-    result = ssaRefRank(bb, i, v, k) and
-    (
-      ssaDefReachesRead(_, def, bb, i)
-      or
-      def.definesAt(_, bb, i)
-    )
-  }
-
-  /**
-   * Holds if the reference to `def` at index `i` in basic block `bb` is the
-   * last reference to `v` inside `bb`.
-   */
-  pragma[noinline]
-  predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
-    ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
-  }
-
-  predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v, SsaRefKind k) {
-    exists(ssaDefRank(def, v, bb, _, k))
-  }
-
-  pragma[noinline]
-  private predicate ssaDefReachesThroughBlock(Definition def, BasicBlock bb) {
-    ssaDefReachesEndOfBlock(bb, def, _) and
-    not defOccursInBlock(_, bb, def.getSourceVariable(), _)
-  }
-
-  /**
-   * Holds if `def` is accessed in basic block `bb1` (either a read or a write),
-   * `bb2` is a transitive successor of `bb1`, `def` is live at the end of _some_
-   * predecessor of `bb2`, and the underlying variable for `def` is neither read
-   * nor written in any block on the path between `bb1` and `bb2`.
-   *
-   * Phi reads are considered as normal reads for this predicate.
-   */
-  pragma[nomagic]
-  private predicate varBlockReachesInclPhiRead(Definition def, BasicBlock bb1, BasicBlock bb2) {
-    defOccursInBlock(def, bb1, _, _) and
-    bb2 = getABasicBlockSuccessor(bb1)
-    or
-    exists(BasicBlock mid |
-      varBlockReachesInclPhiRead(def, bb1, mid) and
-      ssaDefReachesThroughBlock(def, mid) and
-      bb2 = getABasicBlockSuccessor(mid)
-    )
-  }
-
-  pragma[nomagic]
-  private predicate phiReadStep(Definition def, SourceVariable v, BasicBlock bb1, BasicBlock bb2) {
-    varBlockReachesInclPhiRead(def, bb1, bb2) and
-    defOccursInBlock(def, bb2, v, SsaPhiRead())
-  }
-
-  pragma[nomagic]
-  private predicate varBlockReachesExclPhiRead(Definition def, BasicBlock bb1, BasicBlock bb2) {
-    varBlockReachesInclPhiRead(pragma[only_bind_into](def), bb1, pragma[only_bind_into](bb2)) and
-    ssaRef(bb2, _, def.getSourceVariable(), [SsaActualRead().(TSsaRefKind), SsaDef()])
-    or
-    exists(BasicBlock mid |
-      varBlockReachesExclPhiRead(def, mid, bb2) and
-      phiReadStep(def, _, bb1, mid)
-    )
-  }
-
-  /**
-   * Holds if `def` is accessed in basic block `bb1` (either a read or a write),
-   * the underlying variable `v` of `def` is accessed in basic block `bb2`
-   * (either a read or a write), `bb2` is a transitive successor of `bb1`, and
-   * `v` is neither read nor written in any block on the path between `bb1`
-   * and `bb2`.
-   */
-  pragma[nomagic]
-  predicate varBlockReaches(Definition def, BasicBlock bb1, BasicBlock bb2) {
-    varBlockReachesExclPhiRead(def, bb1, bb2) and
-    not defOccursInBlock(def, bb1, _, SsaPhiRead())
-  }
-
-  pragma[nomagic]
-  predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
-    varBlockReaches(def, bb1, bb2) and
-    ssaRefRank(bb2, i2, def.getSourceVariable(), SsaActualRead()) = 1
-  }
-
-  /**
-   * Holds if `def` is accessed in basic block `bb` (either a read or a write),
-   * `bb1` can reach a transitive successor `bb2` where `def` is no longer live,
-   * and `v` is neither read nor written in any block on the path between `bb`
-   * and `bb2`.
-   */
-  pragma[nomagic]
-  predicate varBlockReachesExit(Definition def, BasicBlock bb) {
-    exists(BasicBlock bb2 | varBlockReachesInclPhiRead(def, bb, bb2) |
-      not defOccursInBlock(def, bb2, _, _) and
-      not ssaDefReachesEndOfBlock(bb2, def, _)
-    )
-    or
-    exists(BasicBlock mid |
-      varBlockReachesExit(def, mid) and
-      phiReadStep(def, _, bb, mid)
-    )
-  }
-}
-
-predicate phiReadExposedForTesting = phiRead/2;
-
-private import SsaDefReaches
-
-pragma[nomagic]
-predicate liveThrough(BasicBlock bb, SourceVariable v) {
-  liveAtExit(bb, v) and
-  not ssaRef(bb, _, v, SsaDef())
-}
-
-/**
- * NB: If this predicate is exposed, it should be cached.
- *
- * Holds if the SSA definition of `v` at `def` reaches the end of basic
- * block `bb`, at which point it is still live, without crossing another
- * SSA definition of `v`.
- */
-pragma[nomagic]
-predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
-  exists(int last |
-    last = maxSsaRefRank(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and
-    ssaDefReachesRank(bb, def, last, v) and
-    liveAtExit(bb, v)
-  )
-  or
-  // The construction of SSA form ensures that each read of a variable is
-  // dominated by its definition. An SSA definition therefore reaches a
-  // control flow node if it is the _closest_ SSA definition that dominates
-  // the node. If two definitions dominate a node then one must dominate the
-  // other, so therefore the definition of _closest_ is given by the dominator
-  // tree. Thus, reaching definitions can be calculated in terms of dominance.
-  ssaDefReachesEndOfBlock(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and
-  liveThrough(bb, pragma[only_bind_into](v))
-}
-
-/**
- * NB: If this predicate is exposed, it should be cached.
- *
- * Holds if `inp` is an input to the phi node `phi` along the edge originating in `bb`.
- */
-pragma[nomagic]
-predicate phiHasInputFromBlock(PhiNode phi, Definition inp, BasicBlock bb) {
-  exists(SourceVariable v, BasicBlock bbDef |
-    phi.definesAt(v, bbDef, _) and
-    getABasicBlockPredecessor(bbDef) = bb and
-    ssaDefReachesEndOfBlock(bb, inp, v)
-  )
-}
-
-/**
- * NB: If this predicate is exposed, it should be cached.
- *
- * Holds if the SSA definition of `v` at `def` reaches a read at index `i` in
- * basic block `bb`, without crossing another SSA definition of `v`. The read
- * is of kind `rk`.
- */
-pragma[nomagic]
-predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int i) {
-  ssaDefReachesReadWithinBlock(v, def, bb, i)
-  or
-  ssaRef(bb, i, v, any(SsaRead k)) and
-  ssaDefReachesEndOfBlock(getABasicBlockPredecessor(bb), def, v) and
-  not ssaDefReachesReadWithinBlock(v, _, bb, i)
-}
-
-/**
- * NB: If this predicate is exposed, it should be cached.
- *
- * Holds if `def` is accessed at index `i1` in basic block `bb1` (either a read
- * or a write), `def` is read at index `i2` in basic block `bb2`, and there is a
- * path between them without any read of `def`.
- */
-pragma[nomagic]
-predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
-  exists(int rnk |
-    rnk = ssaDefRank(def, _, bb1, i1, _) and
-    rnk + 1 = ssaDefRank(def, _, bb1, i2, SsaActualRead()) and
-    variableRead(bb1, i2, _, _) and
-    bb2 = bb1
-  )
-  or
-  lastSsaRef(def, _, bb1, i1) and
-  defAdjacentRead(def, bb1, bb2, i2)
-}
-
-pragma[noinline]
-private predicate adjacentDefRead(
-  Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
-) {
-  adjacentDefRead(def, bb1, i1, bb2, i2) and
-  v = def.getSourceVariable()
-}
-
-private predicate adjacentDefReachesRead(
-  Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
-) {
-  exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
-    ssaRef(bb1, i1, v, SsaDef())
-    or
-    variableRead(bb1, i1, v, true)
-  )
-  or
-  exists(BasicBlock bb3, int i3 |
-    adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
-    variableRead(bb3, i3, _, false) and
-    adjacentDefRead(def, bb3, i3, bb2, i2)
-  )
-}
-
-/**
- * NB: If this predicate is exposed, it should be cached.
- *
- * Same as `adjacentDefRead`, but ignores uncertain reads.
- */
-pragma[nomagic]
-predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
-  adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
-  variableRead(bb2, i2, _, true)
-}
-
-/**
- * NB: If this predicate is exposed, it should be cached.
- *
- * Holds if the node at index `i` in `bb` is a last reference to SSA definition
- * `def`. The reference is last because it can reach another write `next`,
- * without passing through another read or write.
- */
-pragma[nomagic]
-predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
-  exists(SourceVariable v |
-    // Next reference to `v` inside `bb` is a write
-    exists(int rnk, int j |
-      rnk = ssaDefRank(def, v, bb, i, _) and
-      next.definesAt(v, bb, j) and
-      rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
-    )
-    or
-    // Can reach a write using one or more steps
-    lastSsaRef(def, v, bb, i) and
-    exists(BasicBlock bb2 |
-      varBlockReaches(def, bb, bb2) and
-      1 = ssaDefRank(next, v, bb2, _, SsaDef())
-    )
-  )
-}
-
-/**
- * NB: If this predicate is exposed, it should be cached.
- *
- * Holds if `inp` is an immediately preceding definition of uncertain definition
- * `def`. Since `def` is uncertain, the value from the preceding definition might
- * still be valid.
- */
-pragma[nomagic]
-predicate uncertainWriteDefinitionInput(UncertainWriteDefinition def, Definition inp) {
-  lastRefRedef(inp, _, _, def)
-}
-
-private predicate adjacentDefReachesUncertainRead(
-  Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
-) {
-  adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
-  variableRead(bb2, i2, _, false)
-}
-
-/**
- * NB: If this predicate is exposed, it should be cached.
- *
- * Same as `lastRefRedef`, but ignores uncertain reads.
- */
-pragma[nomagic]
-predicate lastRefRedefNoUncertainReads(Definition def, BasicBlock bb, int i, Definition next) {
-  lastRefRedef(def, bb, i, next) and
-  not variableRead(bb, i, def.getSourceVariable(), false)
-  or
-  exists(BasicBlock bb0, int i0 |
-    lastRefRedef(def, bb0, i0, next) and
-    adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
-  )
-}
-
-/**
- * NB: If this predicate is exposed, it should be cached.
- *
- * Holds if the node at index `i` in `bb` is a last reference to SSA
- * definition `def`.
- *
- * That is, the node can reach the end of the enclosing callable, or another
- * SSA definition for the underlying source variable, without passing through
- * another read.
- */
-pragma[nomagic]
-predicate lastRef(Definition def, BasicBlock bb, int i) {
-  // Can reach another definition
-  lastRefRedef(def, bb, i, _)
-  or
-  exists(SourceVariable v | lastSsaRef(def, v, bb, i) |
-    // Can reach exit directly
-    bb instanceof ExitBasicBlock
-    or
-    // Can reach a block using one or more steps, where `def` is no longer live
-    varBlockReachesExit(def, bb)
-  )
-}
-
-/**
- * NB: If this predicate is exposed, it should be cached.
- *
- * Same as `lastRefRedef`, but ignores uncertain reads.
- */
-pragma[nomagic]
-predicate lastRefNoUncertainReads(Definition def, BasicBlock bb, int i) {
-  lastRef(def, bb, i) and
-  not variableRead(bb, i, def.getSourceVariable(), false)
-  or
-  exists(BasicBlock bb0, int i0 |
-    lastRef(def, bb0, i0) and
-    adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
-  )
-}
-
-/** A static single assignment (SSA) definition. */
-class Definition extends TDefinition {
-  /** Gets the source variable underlying this SSA definition. */
-  SourceVariable getSourceVariable() { this.definesAt(result, _, _) }
-
-  /**
-   * Holds if this SSA definition defines `v` at index `i` in basic block `bb`.
-   * Phi nodes are considered to be at index `-1`, while normal variable writes
-   * are at the index of the control flow node they wrap.
-   */
-  final predicate definesAt(SourceVariable v, BasicBlock bb, int i) {
-    this = TWriteDef(v, bb, i)
-    or
-    this = TPhiNode(v, bb) and i = -1
-  }
-
-  /** Gets the basic block to which this SSA definition belongs. */
-  final BasicBlock getBasicBlock() { this.definesAt(_, result, _) }
-
-  /** Gets a textual representation of this SSA definition. */
-  string toString() { none() }
-}
-
-/** An SSA definition that corresponds to a write. */
-class WriteDefinition extends Definition, TWriteDef {
-  private SourceVariable v;
-  private BasicBlock bb;
-  private int i;
-
-  WriteDefinition() { this = TWriteDef(v, bb, i) }
-
-  override string toString() { result = "WriteDef" }
-}
-
-/** A phi node. */
-class PhiNode extends Definition, TPhiNode {
-  override string toString() { result = "Phi" }
-}
-
-/**
- * An SSA definition that represents an uncertain update of the underlying
- * source variable.
- */
-class UncertainWriteDefinition extends WriteDefinition {
-  UncertainWriteDefinition() {
-    exists(SourceVariable v, BasicBlock bb, int i |
-      this.definesAt(v, bb, i) and
-      variableWrite(bb, i, v, false)
-    )
-  }
-}
-
-/** Provides a set of consistency queries. */
-module Consistency {
-  abstract class RelevantDefinition extends Definition {
-    abstract predicate hasLocationInfo(
-      string filepath, int startline, int startcolumn, int endline, int endcolumn
-    );
-  }
-
-  query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
-    ssaDefReachesRead(v, def, bb, i) and
-    not exists(unique(Definition def0 | ssaDefReachesRead(v, def0, bb, i)))
-  }
-
-  query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
-    variableRead(bb, i, v, _) and
-    not ssaDefReachesRead(v, _, bb, i)
-  }
-
-  query predicate deadDef(RelevantDefinition def, SourceVariable v) {
-    v = def.getSourceVariable() and
-    not ssaDefReachesRead(_, def, _, _) and
-    not phiHasInputFromBlock(_, def, _) and
-    not uncertainWriteDefinitionInput(_, def)
-  }
-
-  query predicate notDominatedByDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
-    exists(BasicBlock bbDef, int iDef | def.definesAt(v, bbDef, iDef) |
-      ssaDefReachesReadWithinBlock(v, def, bb, i) and
-      (bb != bbDef or i < iDef)
-      or
-      ssaDefReachesRead(v, def, bb, i) and
-      not ssaDefReachesReadWithinBlock(v, def, bb, i) and
-      not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _)
-    )
-  }
-}

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

@@ -1,18 +0,0 @@
-private import semmle.code.cpp.ir.IR
-private import SsaInternals as Ssa
-
-class BasicBlock = IRBlock;
-
-class SourceVariable = Ssa::SourceVariable;
-
-BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result.immediatelyDominates(bb) }
-
-BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
-
-class ExitBasicBlock extends IRBlock {
-  ExitBasicBlock() { this.getLastInstruction() instanceof ExitFunctionInstruction }
-}
-
-predicate variableWrite = Ssa::variableWrite/4;
-
-predicate variableRead = Ssa::variableRead/4;

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

@@ -1,10 +1,10 @@
-import SsaImplCommon
 private import cpp as Cpp
 private import semmle.code.cpp.ir.IR
 private import DataFlowUtil
 private import DataFlowImplCommon as DataFlowImplCommon
 private import semmle.code.cpp.models.interfaces.Allocation as Alloc
 private import semmle.code.cpp.models.interfaces.DataFlow as DataFlow
+private import codeql.ssa.Ssa as SsaImplCommon
 
 private module SourceVariables {
   private newtype TSourceVariable =
@@ -38,8 +38,6 @@ private module SourceVariables {
   }
 }
 
-import SourceVariables
-
 cached
 private newtype TDefOrUse =
   TExplicitDef(Instruction store) { explicitWrite(_, store, _) } or
@@ -86,7 +84,7 @@ abstract class Def extends DefOrUse {
   Instruction getInstruction() { result = store }
 
   /** Gets the variable that is defined by this definition. */
-  abstract SourceVariable getSourceVariable();
+  abstract SourceVariables::SourceVariable getSourceVariable();
 
   /** Holds if this definition is guaranteed to happen. */
   abstract predicate isCertain();
@@ -103,10 +101,10 @@ abstract class Def extends DefOrUse {
 private class ExplicitDef extends Def, TExplicitDef {
   ExplicitDef() { this = TExplicitDef(store) }
 
-  override SourceVariable getSourceVariable() {
+  override SourceVariables::SourceVariable getSourceVariable() {
     exists(VariableInstruction var |
       explicitWrite(_, this.getInstruction(), var) and
-      result.(SourceIRVariable).getIRVariable() = var.getIRVariable()
+      result.(SourceVariables::SourceIRVariable).getIRVariable() = var.getIRVariable()
     )
   }
 
@@ -116,11 +114,11 @@ private class ExplicitDef extends Def, TExplicitDef {
 private class ParameterDef extends Def, TInitializeParam {
   ParameterDef() { this = TInitializeParam(store) }
 
-  override SourceVariable getSourceVariable() {
-    result.(SourceIRVariable).getIRVariable() =
+  override SourceVariables::SourceVariable getSourceVariable() {
+    result.(SourceVariables::SourceIRVariable).getIRVariable() =
       store.(InitializeParameterInstruction).getIRVariable()
     or
-    result.(SourceIRVariableIndirection).getUnderlyingIRVariable() =
+    result.(SourceVariables::SourceIRVariableIndirection).getUnderlyingIRVariable() =
       store.(InitializeIndirectionInstruction).getIRVariable()
   }
 
@@ -138,7 +136,7 @@ abstract class Use extends DefOrUse {
   override string toString() { result = "Use" }
 
   /** Gets the variable that is used by this use. */
-  abstract SourceVariable getSourceVariable();
+  abstract SourceVariables::SourceVariable getSourceVariable();
 
   override IRBlock getBlock() { result = use.getUse().getBlock() }
 
@@ -148,12 +146,14 @@ abstract class Use extends DefOrUse {
 private class ExplicitUse extends Use, TExplicitUse {
   ExplicitUse() { this = TExplicitUse(use) }
 
-  override SourceVariable getSourceVariable() {
+  override SourceVariables::SourceVariable getSourceVariable() {
     exists(VariableInstruction var |
       use.getDef() = var and
       if use.getUse() instanceof ReadSideEffectInstruction
-      then result.(SourceIRVariableIndirection).getUnderlyingIRVariable() = var.getIRVariable()
-      else result.(SourceIRVariable).getIRVariable() = var.getIRVariable()
+      then
+        result.(SourceVariables::SourceIRVariableIndirection).getUnderlyingIRVariable() =
+          var.getIRVariable()
+      else result.(SourceVariables::SourceIRVariable).getIRVariable() = var.getIRVariable()
     )
   }
 }
@@ -161,10 +161,11 @@ private class ExplicitUse extends Use, TExplicitUse {
 private class ReturnParameterIndirection extends Use, TReturnParamIndirection {
   ReturnParameterIndirection() { this = TReturnParamIndirection(use) }
 
-  override SourceVariable getSourceVariable() {
+  override SourceVariables::SourceVariable getSourceVariable() {
     exists(ReturnIndirectionInstruction ret |
       returnParameterIndirection(use, ret) and
-      result.(SourceIRVariableIndirection).getUnderlyingIRVariable() = ret.getIRVariable()
+      result.(SourceVariables::SourceIRVariableIndirection).getUnderlyingIRVariable() =
+        ret.getIRVariable()
     )
   }
 }
@@ -610,27 +611,45 @@ private module Cached {
 
 import Cached
 
-/**
- * Holds if the `i`'th write in block `bb` writes to the variable `v`.
- * `certain` is `true` if the write is guaranteed to overwrite the entire variable.
- */
-predicate variableWrite(IRBlock bb, int i, SourceVariable v, boolean certain) {
-  DataFlowImplCommon::forceCachingInSameStage() and
-  exists(Def def |
-    def.hasIndexInBlock(bb, i) and
-    v = def.getSourceVariable() and
-    (if def.isCertain() then certain = true else certain = false)
-  )
+private module SsaInput implements SsaImplCommon::InputSig {
+  private import semmle.code.cpp.ir.IR
+
+  class BasicBlock = IRBlock;
+
+  class SourceVariable = SourceVariables::SourceVariable;
+
+  BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result.immediatelyDominates(bb) }
+
+  BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
+
+  class ExitBasicBlock extends IRBlock {
+    ExitBasicBlock() { this.getLastInstruction() instanceof ExitFunctionInstruction }
+  }
+
+  /**
+   * Holds if the `i`'th write in block `bb` writes to the variable `v`.
+   * `certain` is `true` if the write is guaranteed to overwrite the entire variable.
+   */
+  predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+    DataFlowImplCommon::forceCachingInSameStage() and
+    exists(Def def |
+      def.hasIndexInBlock(bb, i) and
+      v = def.getSourceVariable() and
+      (if def.isCertain() then certain = true else certain = false)
+    )
+  }
+
+  /**
+   * Holds if the `i`'th read in block `bb` reads to the variable `v`.
+   * `certain` is `true` if the read is guaranteed. For C++, this is always the case.
+   */
+  predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+    exists(Use use |
+      use.hasIndexInBlock(bb, i) and
+      v = use.getSourceVariable() and
+      certain = true
+    )
+  }
 }
 
-/**
- * Holds if the `i`'th read in block `bb` reads to the variable `v`.
- * `certain` is `true` if the read is guaranteed. For C++, this is always the case.
- */
-predicate variableRead(IRBlock bb, int i, SourceVariable v, boolean certain) {
-  exists(Use use |
-    use.hasIndexInBlock(bb, i) and
-    v = use.getSourceVariable() and
-    certain = true
-  )
-}
+import SsaImplCommon::Make<SsaInput>

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

@@ -172,7 +172,12 @@ abstract class Configuration extends DataFlow::Configuration {
   }
 
   override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
-    (this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
+    (
+      this.isSink(node) or
+      this.isSink(node, _) or
+      this.isAdditionalTaintStep(node, _) or
+      this.isAdditionalTaintStep(node, _, _, _)
+    ) and
     defaultImplicitTaintRead(node, c)
   }
 

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

@@ -172,7 +172,12 @@ abstract class Configuration extends DataFlow::Configuration {
   }
 
   override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
-    (this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
+    (
+      this.isSink(node) or
+      this.isSink(node, _) or
+      this.isAdditionalTaintStep(node, _) or
+      this.isAdditionalTaintStep(node, _, _, _)
+    ) and
     defaultImplicitTaintRead(node, c)
   }
 

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/tainttracking3/TaintTrackingImpl.qll

@@ -172,7 +172,12 @@ abstract class Configuration extends DataFlow::Configuration {
   }
 
   override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
-    (this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
+    (
+      this.isSink(node) or
+      this.isSink(node, _) or
+      this.isAdditionalTaintStep(node, _) or
+      this.isAdditionalTaintStep(node, _, _, _)
+    ) and
     defaultImplicitTaintRead(node, c)
   }
 

cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConsistency.qll

@@ -1,2 +1,2 @@
-private import SSAConstruction as SSA
-import SSA::SsaConsistency
+private import SSAConstruction as Ssa
+import Ssa::SsaConsistency

cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConstruction.qll

@@ -1135,7 +1135,7 @@ deprecated module SSAConsistency = SsaConsistency;
  * These predicates are all just aliases for predicates defined in the `Cached` module. This ensures
  * that all of SSA construction will be evaluated in the same stage.
  */
-module SSA {
+module Ssa {
   class MemoryLocation = Alias::MemoryLocation;
 
   predicate hasPhiInstruction = Cached::hasPhiInstructionCached/2;
@@ -1144,3 +1144,6 @@ module SSA {
 
   predicate hasUnreachedInstruction = Cached::hasUnreachedInstructionCached/1;
 }
+
+/** DEPRECATED: Alias for Ssa */
+deprecated module SSA = Ssa;

cpp/ql/lib/semmle/code/cpp/ir/implementation/internal/TInstruction.qll

@@ -20,24 +20,24 @@ newtype TInstruction =
     IRConstruction::Raw::hasInstruction(tag1, tag2)
   } or
   TUnaliasedSsaPhiInstruction(
-    TRawInstruction blockStartInstr, UnaliasedSsa::SSA::MemoryLocation memoryLocation
+    TRawInstruction blockStartInstr, UnaliasedSsa::Ssa::MemoryLocation memoryLocation
   ) {
-    UnaliasedSsa::SSA::hasPhiInstruction(blockStartInstr, memoryLocation)
+    UnaliasedSsa::Ssa::hasPhiInstruction(blockStartInstr, memoryLocation)
   } or
   TUnaliasedSsaChiInstruction(TRawInstruction primaryInstruction) { none() } or
   TUnaliasedSsaUnreachedInstruction(IRFunctionBase irFunc) {
-    UnaliasedSsa::SSA::hasUnreachedInstruction(irFunc)
+    UnaliasedSsa::Ssa::hasUnreachedInstruction(irFunc)
   } or
   TAliasedSsaPhiInstruction(
-    TRawInstruction blockStartInstr, AliasedSsa::SSA::MemoryLocation memoryLocation
+    TRawInstruction blockStartInstr, AliasedSsa::Ssa::MemoryLocation memoryLocation
   ) {
-    AliasedSsa::SSA::hasPhiInstruction(blockStartInstr, memoryLocation)
+    AliasedSsa::Ssa::hasPhiInstruction(blockStartInstr, memoryLocation)
   } or
   TAliasedSsaChiInstruction(TRawInstruction primaryInstruction) {
-    AliasedSsa::SSA::hasChiInstruction(primaryInstruction)
+    AliasedSsa::Ssa::hasChiInstruction(primaryInstruction)
   } or
   TAliasedSsaUnreachedInstruction(IRFunctionBase irFunc) {
-    AliasedSsa::SSA::hasUnreachedInstruction(irFunc)
+    AliasedSsa::Ssa::hasUnreachedInstruction(irFunc)
   }
 
 /**
@@ -50,7 +50,7 @@ module UnaliasedSsaInstructions {
   class TPhiInstruction = TUnaliasedSsaPhiInstruction;
 
   TPhiInstruction phiInstruction(
-    TRawInstruction blockStartInstr, UnaliasedSsa::SSA::MemoryLocation memoryLocation
+    TRawInstruction blockStartInstr, UnaliasedSsa::Ssa::MemoryLocation memoryLocation
   ) {
     result = TUnaliasedSsaPhiInstruction(blockStartInstr, memoryLocation)
   }
@@ -83,7 +83,7 @@ module AliasedSsaInstructions {
   class TPhiInstruction = TAliasedSsaPhiInstruction or TUnaliasedSsaPhiInstruction;
 
   TPhiInstruction phiInstruction(
-    TRawInstruction blockStartInstr, AliasedSsa::SSA::MemoryLocation memoryLocation
+    TRawInstruction blockStartInstr, AliasedSsa::Ssa::MemoryLocation memoryLocation
   ) {
     result = TAliasedSsaPhiInstruction(blockStartInstr, memoryLocation)
   }

cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/SideEffects.qll

@@ -55,7 +55,15 @@ private predicate isDeeplyConstBelow(Type t) {
   isDeeplyConstBelow(t.(TypedefType).getBaseType())
 }
 
-private predicate isConstPointerLike(Type t) {
+/**
+ * INTERNAL: Do not use.
+ *
+ * Holds if `t` is a pointer-like type (i.e., a pointer,
+ * an array a reference, or a pointer-wrapper such as
+ * `std::unique_ptr`) that is constant and only contains
+ * constant types, excluding the type itself.
+ */
+predicate isConstPointerLike(Type t) {
   (
     t instanceof PointerWrapper
     or

cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll

@@ -13,8 +13,8 @@ private import TranslatedInitialization
  * Gets the `TranslatedDeclarationEntry` that represents the declaration
  * `entry`.
  */
-TranslatedDeclarationEntry getTranslatedDeclarationEntry(DeclarationEntry entry) {
-  result.getAst() = entry
+TranslatedDeclarationEntry getTranslatedDeclarationEntry(IRDeclarationEntry entry) {
+  result.getIRDeclarationEntry() = entry
 }
 
 /**
@@ -24,20 +24,22 @@ TranslatedDeclarationEntry getTranslatedDeclarationEntry(DeclarationEntry entry)
  * functions do not have a `TranslatedDeclarationEntry`.
  */
 abstract class TranslatedDeclarationEntry extends TranslatedElement, TTranslatedDeclarationEntry {
-  DeclarationEntry entry;
+  IRDeclarationEntry entry;
 
   TranslatedDeclarationEntry() { this = TTranslatedDeclarationEntry(entry) }
 
   final override Function getFunction() {
     exists(DeclStmt stmt |
-      stmt.getADeclarationEntry() = entry and
+      stmt = entry.getStmt() and
       result = stmt.getEnclosingFunction()
     )
   }
 
+  IRDeclarationEntry getIRDeclarationEntry() { result = entry }
+
   final override string toString() { result = entry.toString() }
 
-  final override Locatable getAst() { result = entry }
+  final override Locatable getAst() { result = entry.getAst() }
 
   /** DEPRECATED: Alias for getAst */
   deprecated override Locatable getAST() { result = getAst() }
@@ -216,7 +218,7 @@ class TranslatedStaticLocalVariableDeclarationEntry extends TranslatedDeclaratio
  */
 class TranslatedStaticLocalVariableInitialization extends TranslatedElement,
   TranslatedLocalVariableDeclaration, TTranslatedStaticLocalVariableInitialization {
-  VariableDeclarationEntry entry;
+  IRVariableDeclarationEntry entry;
   StaticLocalVariable var;
 
   TranslatedStaticLocalVariableInitialization() {
@@ -226,7 +228,7 @@ class TranslatedStaticLocalVariableInitialization extends TranslatedElement,
 
   final override string toString() { result = "init: " + entry.toString() }
 
-  final override Locatable getAst() { result = entry }
+  final override Locatable getAst() { result = entry.getAst() }
 
   /** DEPRECATED: Alias for getAst */
   deprecated override Locatable getAST() { result = getAst() }
@@ -236,40 +238,6 @@ class TranslatedStaticLocalVariableInitialization extends TranslatedElement,
   final override Function getFunction() { result = var.getFunction() }
 }
 
-/**
- * Gets the `TranslatedRangeBasedForVariableDeclaration` that represents the declaration of
- * `var`.
- */
-TranslatedRangeBasedForVariableDeclaration getTranslatedRangeBasedForVariableDeclaration(
-  LocalVariable var
-) {
-  result.getVariable() = var
-}
-
-/**
- * Represents the IR translation of a compiler-generated variable in a range-based `for` loop.
- */
-class TranslatedRangeBasedForVariableDeclaration extends TranslatedLocalVariableDeclaration,
-  TTranslatedRangeBasedForVariableDeclaration {
-  RangeBasedForStmt forStmt;
-  LocalVariable var;
-
-  TranslatedRangeBasedForVariableDeclaration() {
-    this = TTranslatedRangeBasedForVariableDeclaration(forStmt, var)
-  }
-
-  override string toString() { result = var.toString() }
-
-  override Locatable getAst() { result = var }
-
-  /** DEPRECATED: Alias for getAst */
-  deprecated override Locatable getAST() { result = getAst() }
-
-  override Function getFunction() { result = forStmt.getEnclosingFunction() }
-
-  override LocalVariable getVariable() { result = var }
-}
-
 TranslatedConditionDecl getTranslatedConditionDecl(ConditionDeclExpr expr) {
   result.getAst() = expr
 }

cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll

@@ -443,10 +443,10 @@ predicate hasTranslatedSyntheticTemporaryObject(Expr expr) {
  * necessary for automatic local variables, or for static local variables with dynamic
  * initialization.
  */
-private predicate translateDeclarationEntry(DeclarationEntry entry) {
+private predicate translateDeclarationEntry(IRDeclarationEntry entry) {
   exists(DeclStmt declStmt, LocalVariable var |
     translateStmt(declStmt) and
-    declStmt.getADeclarationEntry() = entry and
+    declStmt = entry.getStmt() and
     // Only declarations of local variables need to be translated to IR.
     var = entry.getDeclaration() and
     (
@@ -458,6 +458,102 @@ private predicate translateDeclarationEntry(DeclarationEntry entry) {
   )
 }
 
+private module IRDeclarationEntries {
+  private newtype TIRDeclarationEntry =
+    TPresentDeclarationEntry(DeclarationEntry entry) or
+    TMissingDeclarationEntry(DeclStmt stmt, Declaration d, int index) {
+      not exists(stmt.getDeclarationEntry(index)) and
+      stmt.getDeclaration(index) = d
+    }
+
+  /**
+   * An entity that represents a declaration entry in the database.
+   *
+   * This class exists to work around the fact that `DeclStmt`s in some cases
+   * do not have `DeclarationEntry`s. Currently, this is the case for:
+   * - `DeclStmt`s in template instantiations.
+   * - `DeclStmt`s that are generated by the desugaring of range-based for-loops.
+   *
+   * So instead, the IR works with `IRDeclarationEntry`s that synthesize missing
+   * `DeclarationEntry`s when there is no result for `DeclStmt::getDeclarationEntry`.
+   */
+  abstract class IRDeclarationEntry extends TIRDeclarationEntry {
+    /** Gets a string representation of this `IRDeclarationEntry`. */
+    abstract string toString();
+
+    /** Gets the `DeclStmt` that this `IRDeclarationEntry` belongs to. */
+    abstract DeclStmt getStmt();
+
+    /** Gets the `Declaration` declared by this `IRDeclarationEntry`. */
+    abstract Declaration getDeclaration();
+
+    /** Gets the AST represented by this `IRDeclarationEntry`. */
+    abstract Locatable getAst();
+
+    /**
+     * Holds if this `IRDeclarationEntry` is the `index`'th entry
+     * declared by the enclosing `DeclStmt`.
+     */
+    abstract predicate hasIndex(int index);
+  }
+
+  /** A `IRDeclarationEntry` for an existing `DeclarationEntry`. */
+  private class PresentDeclarationEntry extends IRDeclarationEntry, TPresentDeclarationEntry {
+    DeclarationEntry entry;
+
+    PresentDeclarationEntry() { this = TPresentDeclarationEntry(entry) }
+
+    override string toString() { result = entry.toString() }
+
+    override DeclStmt getStmt() { result.getADeclarationEntry() = entry }
+
+    override Declaration getDeclaration() { result = entry.getDeclaration() }
+
+    override Locatable getAst() { result = entry }
+
+    override predicate hasIndex(int index) { this.getStmt().getDeclarationEntry(index) = entry }
+  }
+
+  /**
+   * A synthesized `DeclarationEntry` that is created when a `DeclStmt` is missing a
+   * result for `DeclStmt::getDeclarationEntry`
+   */
+  private class MissingDeclarationEntry extends IRDeclarationEntry, TMissingDeclarationEntry {
+    DeclStmt stmt;
+    Declaration d;
+    int index;
+
+    MissingDeclarationEntry() { this = TMissingDeclarationEntry(stmt, d, index) }
+
+    override string toString() { result = "missing declaration of " + d.getName() }
+
+    override DeclStmt getStmt() { result = stmt }
+
+    override Declaration getDeclaration() { result = d }
+
+    override Locatable getAst() { result = stmt }
+
+    override predicate hasIndex(int idx) { idx = index }
+  }
+
+  /** A `IRDeclarationEntry` that represents an entry for a `Variable`. */
+  class IRVariableDeclarationEntry instanceof IRDeclarationEntry {
+    Variable v;
+
+    IRVariableDeclarationEntry() { super.getDeclaration() = v }
+
+    Variable getDeclaration() { result = v }
+
+    string toString() { result = super.toString() }
+
+    Locatable getAst() { result = super.getAst() }
+
+    DeclStmt getStmt() { result = super.getStmt() }
+  }
+}
+
+import IRDeclarationEntries
+
 newtype TTranslatedElement =
   // An expression that is not being consumed as a condition
   TTranslatedValueExpr(Expr expr) {
@@ -613,23 +709,13 @@ newtype TTranslatedElement =
     )
   } or
   // A local declaration
-  TTranslatedDeclarationEntry(DeclarationEntry entry) { translateDeclarationEntry(entry) } or
+  TTranslatedDeclarationEntry(IRDeclarationEntry entry) { translateDeclarationEntry(entry) } or
   // The dynamic initialization of a static local variable. This is a separate object from the
   // declaration entry.
-  TTranslatedStaticLocalVariableInitialization(DeclarationEntry entry) {
+  TTranslatedStaticLocalVariableInitialization(IRDeclarationEntry entry) {
     translateDeclarationEntry(entry) and
     entry.getDeclaration() instanceof StaticLocalVariable
   } or
-  // A compiler-generated variable to implement a range-based for loop. These don't have a
-  // `DeclarationEntry` in the database, so we have to go by the `Variable` itself.
-  TTranslatedRangeBasedForVariableDeclaration(RangeBasedForStmt forStmt, LocalVariable var) {
-    translateStmt(forStmt) and
-    (
-      var = forStmt.getRangeVariable() or
-      var = forStmt.getBeginEndDeclaration().getADeclaration() or
-      var = forStmt.getVariable()
-    )
-  } or
   // An allocator call in a `new` or `new[]` expression
   TTranslatedAllocatorCall(NewOrNewArrayExpr newExpr) { not ignoreExpr(newExpr) } or
   // An allocation size for a `new` or `new[]` expression

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

@@ -76,6 +76,13 @@ class TranslatedDeclStmt extends TranslatedStmt {
 
   private int getChildCount() { result = count(getDeclarationEntry(_)) }
 
+  IRDeclarationEntry getIRDeclarationEntry(int index) {
+    result.hasIndex(index) and
+    result.getStmt() = stmt
+  }
+
+  IRDeclarationEntry getAnIRDeclarationEntry() { result = this.getIRDeclarationEntry(_) }
+
   /**
    * Gets the `TranslatedDeclarationEntry` child at zero-based index `index`. Since not all
    * `DeclarationEntry` objects have a `TranslatedDeclarationEntry` (e.g. extern functions), we map
@@ -85,7 +92,7 @@ class TranslatedDeclStmt extends TranslatedStmt {
   private TranslatedDeclarationEntry getDeclarationEntry(int index) {
     result =
       rank[index + 1](TranslatedDeclarationEntry entry, int originalIndex |
-        entry = getTranslatedDeclarationEntry(stmt.getDeclarationEntry(originalIndex))
+        entry = getTranslatedDeclarationEntry(this.getIRDeclarationEntry(originalIndex))
       |
         entry order by originalIndex
       )
@@ -597,36 +604,32 @@ class TranslatedRangeBasedForStmt extends TranslatedStmt, ConditionContext {
   override RangeBasedForStmt stmt;
 
   override TranslatedElement getChild(int id) {
-    id = 0 and result = getRangeVariableDeclaration()
+    id = 0 and result = getRangeVariableDeclStmt()
     or
-    id = 1 and result = getBeginVariableDeclaration()
+    // Note: `__begin` and `__end` are declared by the same `DeclStmt`
+    id = 1 and result = getBeginEndVariableDeclStmt()
     or
-    id = 2 and result = getEndVariableDeclaration()
+    id = 2 and result = getCondition()
     or
-    id = 3 and result = getCondition()
+    id = 3 and result = getUpdate()
     or
-    id = 4 and result = getUpdate()
+    id = 4 and result = getVariableDeclStmt()
     or
-    id = 5 and result = getVariableDeclaration()
-    or
-    id = 6 and result = getBody()
+    id = 5 and result = getBody()
   }
 
   override Instruction getFirstInstruction() {
-    result = getRangeVariableDeclaration().getFirstInstruction()
+    result = getRangeVariableDeclStmt().getFirstInstruction()
   }
 
   override Instruction getChildSuccessor(TranslatedElement child) {
-    child = getRangeVariableDeclaration() and
-    result = getBeginVariableDeclaration().getFirstInstruction()
+    child = getRangeVariableDeclStmt() and
+    result = getBeginEndVariableDeclStmt().getFirstInstruction()
     or
-    child = getBeginVariableDeclaration() and
-    result = getEndVariableDeclaration().getFirstInstruction()
-    or
-    child = getEndVariableDeclaration() and
+    child = getBeginEndVariableDeclStmt() and
     result = getCondition().getFirstInstruction()
     or
-    child = getVariableDeclaration() and
+    child = getVariableDeclStmt() and
     result = getBody().getFirstInstruction()
     or
     child = getBody() and
@@ -643,23 +646,25 @@ class TranslatedRangeBasedForStmt extends TranslatedStmt, ConditionContext {
   override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
 
   override Instruction getChildTrueSuccessor(TranslatedCondition child) {
-    child = getCondition() and result = getVariableDeclaration().getFirstInstruction()
+    child = getCondition() and result = getVariableDeclStmt().getFirstInstruction()
   }
 
   override Instruction getChildFalseSuccessor(TranslatedCondition child) {
     child = getCondition() and result = getParent().getChildSuccessor(this)
   }
 
-  private TranslatedRangeBasedForVariableDeclaration getRangeVariableDeclaration() {
-    result = getTranslatedRangeBasedForVariableDeclaration(stmt.getRangeVariable())
+  private TranslatedDeclStmt getRangeVariableDeclStmt() {
+    exists(IRVariableDeclarationEntry entry |
+      entry.getDeclaration() = stmt.getRangeVariable() and
+      result.getAnIRDeclarationEntry() = entry
+    )
   }
 
-  private TranslatedRangeBasedForVariableDeclaration getBeginVariableDeclaration() {
-    result = getTranslatedRangeBasedForVariableDeclaration(stmt.getBeginVariable())
-  }
-
-  private TranslatedRangeBasedForVariableDeclaration getEndVariableDeclaration() {
-    result = getTranslatedRangeBasedForVariableDeclaration(stmt.getEndVariable())
+  private TranslatedDeclStmt getBeginEndVariableDeclStmt() {
+    exists(IRVariableDeclarationEntry entry |
+      entry.getStmt() = stmt.getBeginEndDeclaration() and
+      result.getAnIRDeclarationEntry() = entry
+    )
   }
 
   // Public for getInstructionBackEdgeSuccessor
@@ -672,8 +677,11 @@ class TranslatedRangeBasedForStmt extends TranslatedStmt, ConditionContext {
     result = getTranslatedExpr(stmt.getUpdate().getFullyConverted())
   }
 
-  private TranslatedRangeBasedForVariableDeclaration getVariableDeclaration() {
-    result = getTranslatedRangeBasedForVariableDeclaration(stmt.getVariable())
+  private TranslatedDeclStmt getVariableDeclStmt() {
+    exists(IRVariableDeclarationEntry entry |
+      entry.getDeclaration() = stmt.getVariable() and
+      result.getAnIRDeclarationEntry() = entry
+    )
   }
 
   private TranslatedStmt getBody() { result = getTranslatedStmt(stmt.getStmt()) }

cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/SSAConsistency.qll

@@ -1,2 +1,2 @@
-private import SSAConstruction as SSA
-import SSA::SsaConsistency
+private import SSAConstruction as Ssa
+import Ssa::SsaConsistency

cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/SSAConstruction.qll

@@ -1135,7 +1135,7 @@ deprecated module SSAConsistency = SsaConsistency;
  * These predicates are all just aliases for predicates defined in the `Cached` module. This ensures
  * that all of SSA construction will be evaluated in the same stage.
  */
-module SSA {
+module Ssa {
   class MemoryLocation = Alias::MemoryLocation;
 
   predicate hasPhiInstruction = Cached::hasPhiInstructionCached/2;
@@ -1144,3 +1144,6 @@ module SSA {
 
   predicate hasUnreachedInstruction = Cached::hasUnreachedInstructionCached/1;
 }
+
+/** DEPRECATED: Alias for Ssa */
+deprecated module SSA = Ssa;

cpp/ql/lib/semmle/code/cpp/models/implementations/StdContainer.qll

@@ -176,7 +176,7 @@ private class StdSequenceContainerInsert extends TaintFunction {
     ) and
     (
       output.isQualifierObject() or
-      output.isReturnValueDeref()
+      output.isReturnValue()
     )
   }
 }

cpp/ql/lib/semmle/code/cpp/models/implementations/StdString.qll

@@ -543,11 +543,11 @@ private class StdOStreamOutNonMember extends DataFlowFunction, TaintFunction {
 
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     // flow from second parameter to first parameter
-    input.isParameter(1) and
+    input.isParameterDeref(1) and
     output.isParameterDeref(0)
     or
     // flow from second parameter to return value
-    input.isParameter(1) and
+    input.isParameterDeref(1) and
     output.isReturnValueDeref()
     or
     // reverse flow from returned reference to the first parameter

cpp/ql/lib/semmle/code/cpp/models/implementations/Strcat.qll

@@ -61,7 +61,7 @@ class StrcatFunction extends TaintFunction, DataFlowFunction, ArrayFunction, Sid
     input.isParameterDeref(0) and
     output.isParameterDeref(0)
     or
-    input.isParameter(1) and
+    input.isParameterDeref(1) and
     output.isParameterDeref(0)
   }
 

cpp/ql/lib/semmle/code/cpp/models/interfaces/FunctionInputsAndOutputs.qll

@@ -46,6 +46,26 @@ class FunctionInput extends TFunctionInput {
    */
   deprecated final predicate isInParameter(ParameterIndex index) { this.isParameter(index) }
 
+  /**
+   * Holds if this is the input value pointed to (through `ind` number of indirections) by a
+   * pointer parameter to a function, or the input value referred to by a reference parameter
+   * to a function, where the parameter has index `index`.
+   *
+   * Example:
+   * ```
+   * void func(int n, char* p, float& r);
+   * ```
+   * - `isParameterDeref(1, 1)` holds for the `FunctionInput` that represents the value of `*p` (with
+   *   type `char`) on entry to the function.
+   * - `isParameterDeref(2, 1)` holds for the `FunctionInput` that represents the value of `r` (with type
+   *   `float`) on entry to the function.
+   * - There is no `FunctionInput` for which `isParameterDeref(0, _)` holds, because `n` is neither a
+   *   pointer nor a reference.
+   */
+  predicate isParameterDeref(ParameterIndex index, int ind) {
+    ind = 1 and this.isParameterDeref(index)
+  }
+
   /**
    * Holds if this is the input value pointed to by a pointer parameter to a function, or the input
    * value referred to by a reference parameter to a function, where the parameter has index
@@ -62,7 +82,7 @@ class FunctionInput extends TFunctionInput {
    * - There is no `FunctionInput` for which `isParameterDeref(0)` holds, because `n` is neither a
    *   pointer nor a reference.
    */
-  predicate isParameterDeref(ParameterIndex index) { none() }
+  predicate isParameterDeref(ParameterIndex index) { this.isParameterDeref(index, 1) }
 
   /**
    * Holds if this is the input value pointed to by a pointer parameter to a function, or the input
@@ -87,7 +107,22 @@ class FunctionInput extends TFunctionInput {
    * - `isQualifierObject()` holds for the `FunctionInput` that represents the value of `*this`
    *   (with type `C const`) on entry to the function.
    */
-  predicate isQualifierObject() { none() }
+  predicate isQualifierObject(int ind) { ind = 1 and this.isQualifierObject() }
+
+  /**
+   * Holds if this is the input value pointed to by the `this` pointer of an instance member
+   * function.
+   *
+   * Example:
+   * ```
+   * struct C {
+   *   void mfunc(int n, char* p, float& r) const;
+   * };
+   * ```
+   * - `isQualifierObject()` holds for the `FunctionInput` that represents the value of `*this`
+   *   (with type `C const`) on entry to the function.
+   */
+  predicate isQualifierObject() { this.isQualifierObject(1) }
 
   /**
    * Holds if this is the input value pointed to by the `this` pointer of an instance member
@@ -143,16 +178,49 @@ class FunctionInput extends TFunctionInput {
    * rare, but they do occur when a function returns a reference to itself,
    * part of itself, or one of its other inputs.
    */
-  predicate isReturnValueDeref() { none() }
+  predicate isReturnValueDeref() { this.isReturnValueDeref(1) }
+
+  /**
+   * Holds if this is the input value pointed to by the return value of a
+   * function, if the function returns a pointer, or the input value referred
+   * to by the return value of a function, if the function returns a reference.
+   *
+   * Example:
+   * ```
+   * char* getPointer();
+   * float& getReference();
+   * int getInt();
+   * ```
+   * - `isReturnValueDeref(1)` holds for the `FunctionInput` that represents the
+   *   value of `*getPointer()` (with type `char`).
+   * - `isReturnValueDeref(1)` holds for the `FunctionInput` that represents the
+   *   value of `getReference()` (with type `float`).
+   * - There is no `FunctionInput` of `getInt()` for which
+   *   `isReturnValueDeref(_)` holds because the return type of `getInt()` is
+   *   neither a pointer nor a reference.
+   *
+   * Note that data flows in through function return values are relatively
+   * rare, but they do occur when a function returns a reference to itself,
+   * part of itself, or one of its other inputs.
+   */
+  predicate isReturnValueDeref(int ind) { ind = 1 and this.isReturnValueDeref() }
+
+  /**
+   * Holds if `i >= 0` and `isParameterDeref(i, ind)` holds for this value, or
+   * if `i = -1` and `isQualifierObject(ind)` holds for this value.
+   */
+  final predicate isParameterDerefOrQualifierObject(ParameterIndex i, int ind) {
+    i >= 0 and this.isParameterDeref(i, ind)
+    or
+    i = -1 and this.isQualifierObject(ind)
+  }
 
   /**
    * Holds if `i >= 0` and `isParameterDeref(i)` holds for this value, or
    * if `i = -1` and `isQualifierObject()` holds for this value.
    */
   final predicate isParameterDerefOrQualifierObject(ParameterIndex i) {
-    i >= 0 and this.isParameterDeref(i)
-    or
-    i = -1 and this.isQualifierObject()
+    this.isParameterDerefOrQualifierObject(i, 1)
   }
 }
 
@@ -308,7 +376,25 @@ class FunctionOutput extends TFunctionOutput {
    * - There is no `FunctionOutput` for which `isParameterDeref(0)` holds, because `n` is neither a
    *   pointer nor a reference.
    */
-  predicate isParameterDeref(ParameterIndex i) { none() }
+  predicate isParameterDeref(ParameterIndex i) { this.isParameterDeref(i, 1) }
+
+  /**
+   * Holds if this is the output value pointed to by a pointer parameter (through `ind` number
+   * of indirections) to a function, or the output value referred to by a reference parameter to
+   * a function, where the parameter has index `index`.
+   *
+   * Example:
+   * ```
+   * void func(int n, char* p, float& r);
+   * ```
+   * - `isParameterDeref(1, 1)` holds for the `FunctionOutput` that represents the value of `*p` (with
+   *   type `char`) on return from the function.
+   * - `isParameterDeref(2, 1)` holds for the `FunctionOutput` that represents the value of `r` (with
+   *   type `float`) on return from the function.
+   * - There is no `FunctionOutput` for which `isParameterDeref(0, _)` holds, because `n` is neither a
+   *   pointer nor a reference.
+   */
+  predicate isParameterDeref(ParameterIndex i, int ind) { ind = 1 and this.isParameterDeref(i) }
 
   /**
    * Holds if this is the output value pointed to by a pointer parameter to a function, or the
@@ -333,7 +419,22 @@ class FunctionOutput extends TFunctionOutput {
    * - `isQualifierObject()` holds for the `FunctionOutput` that represents the value of `*this`
    *   (with type `C`) on return from the function.
    */
-  predicate isQualifierObject() { none() }
+  predicate isQualifierObject() { this.isQualifierObject(1) }
+
+  /**
+   * Holds if this is the output value pointed to by the `this` pointer of an instance member
+   *   function.
+   *
+   * Example:
+   * ```
+   * struct C {
+   *   void mfunc(int n, char* p, float& r);
+   * };
+   * ```
+   * - `isQualifierObject()` holds for the `FunctionOutput` that represents the value of `*this`
+   *   (with type `C`) on return from the function.
+   */
+  predicate isQualifierObject(int ind) { ind = 1 and this.isQualifierObject() }
 
   /**
    * Holds if this is the output value pointed to by the `this` pointer of an instance member
@@ -385,7 +486,27 @@ class FunctionOutput extends TFunctionOutput {
    * - There is no `FunctionOutput` of `getInt()` for which `isReturnValueDeref()` holds because the
    *   return type of `getInt()` is neither a pointer nor a reference.
    */
-  predicate isReturnValueDeref() { none() }
+  predicate isReturnValueDeref() { this.isReturnValueDeref(_) }
+
+  /**
+   * Holds if this is the output value pointed to by the return value of a function, if the function
+   * returns a pointer, or the output value referred to by the return value of a function, if the
+   * function returns a reference.
+   *
+   * Example:
+   * ```
+   * char* getPointer();
+   * float& getReference();
+   * int getInt();
+   * ```
+   * - `isReturnValueDeref(1)` holds for the `FunctionOutput` that represents the value of
+   *   `*getPointer()` (with type `char`).
+   * - `isReturnValueDeref(1)` holds for the `FunctionOutput` that represents the value of
+   *   `getReference()` (with type `float`).
+   * - There is no `FunctionOutput` of `getInt()` for which `isReturnValueDeref(_)` holds because the
+   *   return type of `getInt()` is neither a pointer nor a reference.
+   */
+  predicate isReturnValueDeref(int ind) { ind = 1 and this.isReturnValueDeref() }
 
   /**
    * Holds if this is the output value pointed to by the return value of a function, if the function
@@ -395,14 +516,22 @@ class FunctionOutput extends TFunctionOutput {
    */
   deprecated final predicate isOutReturnPointer() { this.isReturnValueDeref() }
 
+  /**
+   * Holds if `i >= 0` and `isParameterDeref(i, ind)` holds for this is the value, or
+   * if `i = -1` and `isQualifierObject(ind)` holds for this value.
+   */
+  final predicate isParameterDerefOrQualifierObject(ParameterIndex i, int ind) {
+    i >= 0 and this.isParameterDeref(i, ind)
+    or
+    i = -1 and this.isQualifierObject(ind)
+  }
+
   /**
    * Holds if `i >= 0` and `isParameterDeref(i)` holds for this is the value, or
    * if `i = -1` and `isQualifierObject()` holds for this value.
    */
   final predicate isParameterDerefOrQualifierObject(ParameterIndex i) {
-    i >= 0 and this.isParameterDeref(i)
-    or
-    i = -1 and this.isQualifierObject()
+    this.isParameterDerefOrQualifierObject(i, 1)
   }
 }
 
@@ -431,6 +560,10 @@ class OutParameterDeref extends FunctionOutput, TOutParameterDeref {
   ParameterIndex getIndex() { result = index }
 
   override predicate isParameterDeref(ParameterIndex i) { i = index }
+
+  override predicate isParameterDeref(ParameterIndex i, int ind) {
+    this.isParameterDeref(i) and ind = 1
+  }
 }
 
 /**

cpp/ql/lib/semmle/code/cpp/pointsto/PointsTo.qll

@@ -19,6 +19,10 @@
  * `pointstoinfo` predicate determines the transitively implied points-to
  * information by collapsing pointers into equivalence classes. These
  * equivalence classes are called "points-to sets".
+ *
+ * WARNING: This library may perform poorly on very large projects.
+ * Consider using another library such as `semmle.code.cpp.dataflow.DataFlow`
+ * instead.
  */
 
 import semmle.code.cpp.commons.File

cpp/ql/lib/semmle/code/cpp/valuenumbering/GlobalValueNumberingImpl.qll

@@ -165,7 +165,7 @@ private ControlFlowNode mostRecentSideEffect(ControlFlowNode node) {
 
 /** Used to represent the "global value number" of an expression. */
 cached
-private newtype GVNBase =
+private newtype GvnBase =
   GVN_IntConst(int val, Type t) { mk_IntConst(val, t, _) } or
   GVN_FloatConst(float val, Type t) { mk_FloatConst(val, t, _) } or
   // If the local variable does not have a defining value, then
@@ -221,8 +221,8 @@ private newtype GVNBase =
  * expression with this `GVN` and using its `toString` and `getLocation`
  * methods.
  */
-class GVN extends GVNBase {
-  GVN() { this instanceof GVNBase }
+class GVN extends GvnBase {
+  GVN() { this instanceof GvnBase }
 
   /** Gets an expression that has this GVN. */
   Expr getAnExpr() { this = globalValueNumber(result) }

cpp/ql/lib/semmlecode.cpp.dbscheme

@@ -746,7 +746,7 @@ type_mentions(
     unique int id: @type_mention,
     int type_id: @type ref,
     int location: @location ref,
-    // a_symbol_reference_kind from the EDG frontend.  See symbol_ref.h there.
+    // a_symbol_reference_kind from the frontend.
     int kind: int ref
 );
 
@@ -1596,7 +1596,7 @@ case @expr.kind of
 | 117 = @ispolyexpr // __is_polymorphic ::= type
 | 118 = @isunionexpr // __is_union ::= type
 | 119 = @typescompexpr // GNU __builtin_types_compatible ::= type type
-| 120 = @intaddrexpr // EDG internal builtin, used to implement offsetof
+| 120 = @intaddrexpr // frontend internal builtin, used to implement offsetof
 // ...
 | 122 = @hastrivialdestructor // __has_trivial_destructor ::= type
 | 123 = @literal
@@ -1666,6 +1666,33 @@ case @expr.kind of
 | 333 = @builtinbitcast
 | 334 = @builtinshuffle
 | 335 = @blockassignexpr
+| 336 = @issame
+| 337 = @isfunction
+| 338 = @islayoutcompatible
+| 339 = @ispointerinterconvertiblebaseof
+| 340 = @isarray
+| 341 = @arrayrank
+| 342 = @arrayextent
+| 343 = @isarithmetic
+| 344 = @iscompletetype
+| 345 = @iscompound
+| 346 = @isconst
+| 347 = @isfloatingpoint
+| 348 = @isfundamental
+| 349 = @isintegral
+| 350 = @islvaluereference
+| 351 = @ismemberfunctionpointer
+| 352 = @ismemberobjectpointer
+| 353 = @ismemberpointer
+| 354 = @isobject
+| 355 = @ispointer
+| 356 = @isreference
+| 357 = @isrvaluereference
+| 358 = @isscalar
+| 359 = @issigned
+| 360 = @isunsigned
+| 361 = @isvoid
+| 362 = @isvolatile
 ;
 
 @var_args_expr = @vastartexpr
@@ -1732,6 +1759,33 @@ case @expr.kind of
             | @hasuniqueobjectrepresentations
             | @builtinbitcast
             | @builtinshuffle
+            | @issame
+            | @isfunction
+            | @islayoutcompatible
+            | @ispointerinterconvertiblebaseof
+            | @isarray
+            | @arrayrank
+            | @arrayextent
+            | @isarithmetic
+            | @iscompletetype
+            | @iscompound
+            | @isconst
+            | @isfloatingpoint
+            | @isfundamental
+            | @isintegral
+            | @islvaluereference
+            | @ismemberfunctionpointer
+            | @ismemberobjectpointer
+            | @ismemberpointer
+            | @isobject
+            | @ispointer
+            | @isreference
+            | @isrvaluereference
+            | @isscalar
+            | @issigned
+            | @isunsigned
+            | @isvoid
+            | @isvolatile
             ;
 
 new_allocated_type(

cpp/ql/lib/upgrades/f96ad9b2da43bbc9e55a72a165febd270ae07981/upgrade.properties

@@ -0,0 +1,2 @@
+description: Add new builtin operations
+compatibility: backwards

cpp/ql/src/Architecture/General Class-Level Information/HubClasses.ql

@@ -12,5 +12,5 @@ import cpp
 
 from Class c
 where c.fromSource()
-select c as Class, c.getMetrics().getAfferentCoupling() as AfferentCoupling,
-  c.getMetrics().getEfferentSourceCoupling() as EfferentCoupling order by AfferentCoupling desc
+select c as class_, c.getMetrics().getAfferentCoupling() as afferentCoupling,
+  c.getMetrics().getEfferentSourceCoupling() as efferentCoupling order by afferentCoupling desc

cpp/ql/src/Architecture/General Class-Level Information/InheritanceDepthDistribution.ql

@@ -16,5 +16,5 @@ predicate hasInheritanceDepth(Class c, int d) {
 
 from int depth
 where hasInheritanceDepth(_, depth)
-select depth as InheritanceDepth, count(Class c | hasInheritanceDepth(c, depth)) as NumberOfClasses
-  order by InheritanceDepth
+select depth as inheritanceDepth, count(Class c | hasInheritanceDepth(c, depth)) as numberOfClasses
+  order by inheritanceDepth

cpp/ql/src/Architecture/General Top-Level Information/GeneralStatistics.ql

@@ -51,4 +51,4 @@ where
         100 * sum(Class c | c.fromSource() | c.getMetrics().getEfferentSourceCoupling()) /
           sum(Class c | c.fromSource() | c.getMetrics().getEfferentCoupling())
       ).toString() + "%"
-select l as Title, n as Value
+select l as title, n as value

cpp/ql/src/Architecture/Refactoring Opportunities/ClassesWithManyDependencies.ql

@@ -16,4 +16,4 @@ where
   t.fromSource() and
   n = t.getMetrics().getEfferentSourceCoupling() and
   n > 10
-select t as Class, "This class has too many dependencies (" + n.toString() + ")"
+select t as class_, "This class has too many dependencies (" + n.toString() + ")"

cpp/ql/src/Architecture/Refactoring Opportunities/ClassesWithManyFields.ql

@@ -63,17 +63,17 @@ class VariableDeclarationLine extends TVariableDeclarationInfo {
   /**
    * Gets a `VariableDeclarationEntry` on this line.
    */
-  VariableDeclarationEntry getAVDE() { vdeInfo(result, c, f, line) }
+  VariableDeclarationEntry getAVde() { vdeInfo(result, c, f, line) }
 
   /**
    * Gets the start column of the first `VariableDeclarationEntry` on this line.
    */
-  int getStartColumn() { result = min(this.getAVDE().getLocation().getStartColumn()) }
+  int getStartColumn() { result = min(this.getAVde().getLocation().getStartColumn()) }
 
   /**
    * Gets the end column of the last `VariableDeclarationEntry` on this line.
    */
-  int getEndColumn() { result = max(this.getAVDE().getLocation().getEndColumn()) }
+  int getEndColumn() { result = max(this.getAVde().getLocation().getEndColumn()) }
 
   /**
    * Gets the rank of this `VariableDeclarationLine` in its file and class
@@ -134,13 +134,13 @@ class VariableDeclarationGroup extends VariableDeclarationLine {
       count(VariableDeclarationLine l |
         l = this.getProximateNext*()
       |
-        l.getAVDE().getVariable().getName()
+        l.getAVde().getVariable().getName()
       )
   }
 
   override string toString() {
     this.getCount() = 1 and
-    result = "declaration of " + this.getAVDE().getVariable().getName()
+    result = "declaration of " + this.getAVde().getVariable().getName()
     or
     this.getCount() > 1 and
     result = "group of " + this.getCount() + " fields here"