Merge pull request #16363 from github/release-prep/2.17.2

Release preparation for version 2.17.2

.bazelrc

@@ -14,4 +14,7 @@ build:linux --cxxopt=-std=c++20
 build:macos --cxxopt=-std=c++20 --cpu=darwin_x86_64
 build:windows --cxxopt=/std:c++20 --cxxopt=/Zc:preprocessor
 
+common --registry=file:///%workspace%/misc/bazel/registry
+common --registry=https://bcr.bazel.build
+
 try-import %workspace%/local.bazelrc

.bazelrc.internal

@@ -0,0 +1,4 @@
+# this file should contain bazel settings required to build things from `semmle-code`
+
+common --registry=file:///%workspace%/ql/misc/bazel/registry
+common --registry=https://bcr.bazel.build

.bazelversion

@@ -1 +1 @@
-7.0.2
+7.1.0

.gitattributes

@@ -67,11 +67,6 @@ go/extractor/opencsv/CSVReader.java -text
 # for those testing dbscheme files.
 */ql/lib/upgrades/initial/*.dbscheme -text
 
-# Generated test files - these are synced from the standard JavaScript libraries using
-# `javascript/ql/experimental/adaptivethreatmodeling/test/update_endpoint_test_files.py`.
-javascript/ql/experimental/adaptivethreatmodeling/test/endpoint_large_scale/autogenerated/**/*.js linguist-generated=true -merge
-javascript/ql/experimental/adaptivethreatmodeling/test/endpoint_large_scale/autogenerated/**/*.ts linguist-generated=true -merge
-
 # Auto-generated modeling for Python
 python/ql/lib/semmle/python/frameworks/data/internal/subclass-capture/*.yml linguist-generated=true
 

.github/labeler.yml

@@ -15,7 +15,7 @@ Java:
   - change-notes/**/*java.*
 
 JS:
-  - any: [ 'javascript/**/*', '!javascript/ql/experimental/adaptivethreatmodeling/**/*' ]
+  - any: [ 'javascript/**/*' ]
   - change-notes/**/*javascript*
 
 Kotlin:
@@ -46,6 +46,3 @@ documentation:
 # Since these are all shared files that need to be synced, just pick _one_ copy of each.
 "DataFlow Library":
   - "shared/dataflow/**/*"
-
-"ATM":
-  - javascript/ql/experimental/adaptivethreatmodeling/**/*

.github/workflows/buildifier.yml

@@ -0,0 +1,28 @@
+name: Check bazel formatting
+
+on:
+  pull_request:
+    paths:
+      - "**.bazel"
+      - "**.bzl"
+    branches:
+      - main
+      - "rc/*"
+
+permissions:
+  contents: read
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+      - name: Check bazel formatting
+        uses: pre-commit/action@646c83fcd040023954eafda54b4db0192ce70507
+        with:
+          extra_args: >
+            buildifier --all-files 2>&1 ||
+            (
+              echo -e "In order to format all bazel files, please run:\n  bazel run //:buildifier"; exit 1
+            )

.github/workflows/cpp-swift-analysis.yml

@@ -0,0 +1,55 @@
+name: "Code scanning - C++"
+
+on:
+  push:
+    branches:
+      - main
+      - 'rc/*'
+  pull_request:
+    branches:
+      - main
+      - 'rc/*'
+    paths:
+      - 'swift/**'
+      - '.github/codeql/**'
+      - '.github/workflows/cpp-swift-analysis.yml'
+  schedule:
+    - cron: '0 9 * * 1'
+
+jobs:
+  CodeQL-Build:
+
+    runs-on: ubuntu-latest
+
+    permissions:
+      contents: read
+      security-events: write
+      pull-requests: read
+
+    steps:
+    - name: Checkout repository
+      uses: actions/checkout@v4
+
+    # Initializes the CodeQL tools for scanning.
+    - name: Initialize CodeQL
+      uses: github/codeql-action/init@main
+      # Override language selection by uncommenting this and choosing your languages
+      with:
+        languages: cpp
+        config-file: ./.github/codeql/codeql-config.yml
+  
+    - name: "[Ubuntu] Remove GCC 13 from runner image"
+      shell: bash
+      run: |
+        sudo rm -f /etc/apt/sources.list.d/ubuntu-toolchain-r-ubuntu-test-jammy.list
+        sudo apt-get update
+        sudo apt-get install -y --allow-downgrades libc6=2.35-* libc6-dev=2.35-* libstdc++6=12.3.0-* libgcc-s1=12.3.0-*
+
+    - name: "Build Swift extractor using Bazel"
+      run: |
+        bazel clean --expunge
+        bazel run //swift:create-extractor-pack --nouse_action_cache --noremote_accept_cached --noremote_upload_local_results --spawn_strategy=local --features=-layering_check
+        bazel shutdown
+
+    - name: Perform CodeQL Analysis
+      uses: github/codeql-action/analyze@main

.github/workflows/swift.yml

@@ -6,6 +6,7 @@ on:
       - "swift/**"
       - "misc/bazel/**"
       - "misc/codegen/**"
+      - "shared/**"
       - "*.bazel*"
       - .github/workflows/swift.yml
       - .github/actions/**
@@ -22,10 +23,12 @@ on:
       - "swift/**"
       - "misc/bazel/**"
       - "misc/codegen/**"
+      - "shared/**"
       - "*.bazel*"
       - .github/workflows/swift.yml
       - .github/actions/**
       - codeql-workspace.yml
+      - .pre-commit-config.yaml
       - "!**/*.md"
       - "!**/*.qhelp"
     branches:

.pre-commit-config.yaml

@@ -20,13 +20,15 @@ repos:
       - id: autopep8
         files: ^misc/codegen/.*\.py
 
-  - repo: https://github.com/warchant/pre-commit-buildifier
-    rev: 0.0.2
-    hooks:
-      - id: buildifier
-
   - repo: local
     hooks:
+      - id: buildifier
+        name: Format bazel files
+        files: \.(bazel|bzl)
+        language: system
+        entry: bazel run //:buildifier
+        pass_filenames: false
+
       - id: codeql-format
         name: Fix QL file formatting
         files: \.qll?$

BUILD.bazel

@@ -0,0 +1,9 @@
+load("@buildifier_prebuilt//:rules.bzl", "buildifier")
+
+buildifier(
+    name = "buildifier",
+    exclude_patterns = [
+        "./.git/*",
+    ],
+    lint_mode = "fix",
+)

CODEOWNERS

@@ -1,4 +1,5 @@
 /cpp/ @github/codeql-c-analysis
+/cpp/autobuilder/ @github/codeql-c-extractor
 /csharp/ @github/codeql-csharp
 /go/ @github/codeql-go
 /java/ @github/codeql-java
@@ -11,9 +12,6 @@
 /java/ql/test-kotlin1/ @github/codeql-kotlin
 /java/ql/test-kotlin2/ @github/codeql-kotlin
 
-# ML-powered queries
-/javascript/ql/experimental/adaptivethreatmodeling/ @github/codeql-ml-powered-queries-reviewers
-
 # CodeQL tools and associated docs
 /docs/codeql/codeql-cli/ @github/codeql-cli-reviewers
 /docs/codeql/codeql-for-visual-studio-code/ @github/codeql-vscode-reviewers
@@ -36,9 +34,7 @@ MODULE.bazel @github/codeql-ci-reviewers
 
 # Workflows
 /.github/workflows/ @github/codeql-ci-reviewers
-/.github/workflows/atm-* @github/codeql-ml-powered-queries-reviewers
 /.github/workflows/go-* @github/codeql-go
-/.github/workflows/js-ml-tests.yml @github/codeql-ml-powered-queries-reviewers
 /.github/workflows/ql-for-ql-* @github/codeql-ql-for-ql-reviewers
 /.github/workflows/ruby-* @github/codeql-ruby
 /.github/workflows/swift.yml @github/codeql-swift

MODULE.bazel

@@ -14,7 +14,7 @@ local_path_override(
 # see https://registry.bazel.build/ for a list of available packages
 
 bazel_dep(name = "platforms", version = "0.0.8")
-bazel_dep(name = "rules_pkg", version = "0.9.1")
+bazel_dep(name = "rules_pkg", version = "0.10.1")
 bazel_dep(name = "rules_nodejs", version = "6.0.3")
 bazel_dep(name = "rules_python", version = "0.31.0")
 bazel_dep(name = "bazel_skylib", version = "1.5.0")
@@ -22,6 +22,8 @@ bazel_dep(name = "abseil-cpp", version = "20240116.0", repo_name = "absl")
 bazel_dep(name = "nlohmann_json", version = "3.11.3", repo_name = "json")
 bazel_dep(name = "fmt", version = "10.0.0")
 
+bazel_dep(name = "buildifier_prebuilt", version = "6.4.0", dev_dependency = True)
+
 pip = use_extension("@rules_python//python/extensions:pip.bzl", "pip")
 pip.parse(
     hub_name = "codegen_deps",
@@ -31,6 +33,8 @@ pip.parse(
 use_repo(pip, "codegen_deps")
 
 swift_deps = use_extension("//swift/third_party:load.bzl", "swift_deps")
+
+# following list can be kept in sync with `bazel mod tidy`
 use_repo(
     swift_deps,
     "binlog",

codeql-workspace.yml

@@ -6,20 +6,11 @@ provide:
   - "*/ql/consistency-queries/qlpack.yml"
   - "*/ql/automodel/src/qlpack.yml"
   - "*/ql/automodel/test/qlpack.yml"
+  - "python/extractor/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"
-  - "javascript/ql/experimental/adaptivethreatmodeling/lib/qlpack.yml"
-  # This pack is explicitly excluded from the workspace since most users
-  # will want to use a version of this pack from the package cache. Internal
-  # users can uncomment the following line and place a custom ML model
-  # in the corresponding pack to test a custom ML model within their local
-  # checkout.
-  # - "javascript/ql/experimental/adaptivethreatmodeling/model/qlpack.yml"
-  - "javascript/ql/experimental/adaptivethreatmodeling/modelbuilding/qlpack.yml"
-  - "javascript/ql/experimental/adaptivethreatmodeling/src/qlpack.yml"
-  - "javascript/ql/experimental/adaptivethreatmodeling/test/qlpack.yml"
   - "csharp/ql/campaigns/Solorigate/lib/qlpack.yml"
   - "csharp/ql/campaigns/Solorigate/src/qlpack.yml"
   - "csharp/ql/campaigns/Solorigate/test/qlpack.yml"
@@ -27,7 +18,6 @@ provide:
   - "misc/suite-helpers/qlpack.yml"
   - "ruby/extractor-pack/codeql-extractor.yml"
   - "swift/extractor-pack/codeql-extractor.yml"
-  - "swift/integration-tests/qlpack.yml"
   - "ql/extractor-pack/codeql-extractor.yml"
   - ".github/codeql/extensions/**/codeql-pack.yml"
 

config/identical-files.json

@@ -88,123 +88,46 @@
   "IR Instruction": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/Instruction.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll",
-    "csharp/ql/src/experimental/ir/implementation/raw/Instruction.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/Instruction.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll"
   ],
   "IR IRBlock": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/IRBlock.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/IRBlock.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/IRBlock.qll",
-    "csharp/ql/src/experimental/ir/implementation/raw/IRBlock.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/IRBlock.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/IRBlock.qll"
   ],
   "IR IRVariable": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/IRVariable.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/IRVariable.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/IRVariable.qll",
-    "csharp/ql/src/experimental/ir/implementation/raw/IRVariable.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/IRVariable.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/IRVariable.qll"
   ],
   "IR IRFunction": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/IRFunction.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/IRFunction.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/IRFunction.qll",
-    "csharp/ql/src/experimental/ir/implementation/raw/IRFunction.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/IRFunction.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/IRFunction.qll"
   ],
   "IR Operand": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/Operand.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/Operand.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/Operand.qll",
-    "csharp/ql/src/experimental/ir/implementation/raw/Operand.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/Operand.qll"
-  ],
-  "IR IRType": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/IRType.qll",
-    "csharp/ql/src/experimental/ir/implementation/IRType.qll"
-  ],
-  "IR IRConfiguration": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/IRConfiguration.qll",
-    "csharp/ql/src/experimental/ir/implementation/IRConfiguration.qll"
-  ],
-  "IR UseSoundEscapeAnalysis": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/UseSoundEscapeAnalysis.qll",
-    "csharp/ql/src/experimental/ir/implementation/UseSoundEscapeAnalysis.qll"
-  ],
-  "IR IRFunctionBase": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/internal/IRFunctionBase.qll",
-    "csharp/ql/src/experimental/ir/implementation/internal/IRFunctionBase.qll"
-  ],
-  "IR Operand Tag": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/internal/OperandTag.qll",
-    "csharp/ql/src/experimental/ir/implementation/internal/OperandTag.qll"
-  ],
-  "IR TInstruction": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/internal/TInstruction.qll",
-    "csharp/ql/src/experimental/ir/implementation/internal/TInstruction.qll"
-  ],
-  "IR TIRVariable": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/internal/TIRVariable.qll",
-    "csharp/ql/src/experimental/ir/implementation/internal/TIRVariable.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/Operand.qll"
   ],
   "IR IR": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/IR.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/IR.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/IR.qll",
-    "csharp/ql/src/experimental/ir/implementation/raw/IR.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/IR.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/IR.qll"
   ],
   "IR IRConsistency": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/IRConsistency.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/IRConsistency.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/IRConsistency.qll",
-    "csharp/ql/src/experimental/ir/implementation/raw/IRConsistency.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/IRConsistency.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/IRConsistency.qll"
   ],
   "IR PrintIR": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/PrintIR.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/PrintIR.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/PrintIR.qll",
-    "csharp/ql/src/experimental/ir/implementation/raw/PrintIR.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/PrintIR.qll"
-  ],
-  "IR IntegerConstant": [
-    "cpp/ql/lib/semmle/code/cpp/ir/internal/IntegerConstant.qll",
-    "csharp/ql/src/experimental/ir/internal/IntegerConstant.qll"
-  ],
-  "IR IntegerInteval": [
-    "cpp/ql/lib/semmle/code/cpp/ir/internal/IntegerInterval.qll",
-    "csharp/ql/src/experimental/ir/internal/IntegerInterval.qll"
-  ],
-  "IR IntegerPartial": [
-    "cpp/ql/lib/semmle/code/cpp/ir/internal/IntegerPartial.qll",
-    "csharp/ql/src/experimental/ir/internal/IntegerPartial.qll"
-  ],
-  "IR Overlap": [
-    "cpp/ql/lib/semmle/code/cpp/ir/internal/Overlap.qll",
-    "csharp/ql/src/experimental/ir/internal/Overlap.qll"
-  ],
-  "IR EdgeKind": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll",
-    "csharp/ql/src/experimental/ir/implementation/EdgeKind.qll"
-  ],
-  "IR MemoryAccessKind": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/MemoryAccessKind.qll",
-    "csharp/ql/src/experimental/ir/implementation/MemoryAccessKind.qll"
-  ],
-  "IR TempVariableTag": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/TempVariableTag.qll",
-    "csharp/ql/src/experimental/ir/implementation/TempVariableTag.qll"
-  ],
-  "IR Opcode": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/Opcode.qll",
-    "csharp/ql/src/experimental/ir/implementation/Opcode.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/PrintIR.qll"
   ],
   "IR SSAConsistency": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/SSAConsistency.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConsistency.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/SSAConsistency.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConsistency.qll"
   ],
   "C++ IR InstructionImports": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/InstructionImports.qll",
@@ -252,8 +175,7 @@
   ],
   "SSA AliasAnalysis": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/AliasAnalysis.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/AliasAnalysis.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/AliasAnalysis.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/AliasAnalysis.qll"
   ],
   "SSA PrintAliasAnalysis": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/PrintAliasAnalysis.qll",
@@ -268,44 +190,28 @@
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingImports.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/internal/ValueNumberingImports.qll"
   ],
-  "IR SSA SimpleSSA": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/SimpleSSA.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/SimpleSSA.qll"
-  ],
-  "IR AliasConfiguration (unaliased_ssa)": [
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/AliasConfiguration.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/AliasConfiguration.qll"
-  ],
   "IR SSA SSAConstruction": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/SSAConstruction.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConstruction.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/SSAConstruction.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConstruction.qll"
   ],
   "IR SSA PrintSSA": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/PrintSSA.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/PrintSSA.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/PrintSSA.qll"
   ],
   "IR ValueNumberInternal": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/gvn/internal/ValueNumberingInternal.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingInternal.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/internal/ValueNumberingInternal.qll",
-    "csharp/ql/src/experimental/ir/implementation/raw/gvn/internal/ValueNumberingInternal.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingInternal.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/internal/ValueNumberingInternal.qll"
   ],
   "C++ IR ValueNumber": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/gvn/ValueNumbering.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/gvn/ValueNumbering.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/ValueNumbering.qll",
-    "csharp/ql/src/experimental/ir/implementation/raw/gvn/ValueNumbering.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/gvn/ValueNumbering.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/ValueNumbering.qll"
   ],
   "C++ IR PrintValueNumbering": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/gvn/PrintValueNumbering.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/gvn/PrintValueNumbering.qll",
-    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/PrintValueNumbering.qll",
-    "csharp/ql/src/experimental/ir/implementation/raw/gvn/PrintValueNumbering.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/gvn/PrintValueNumbering.qll"
+    "cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/PrintValueNumbering.qll"
   ],
   "C++ IR ConstantAnalysis": [
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/constant/ConstantAnalysis.qll",
@@ -333,38 +239,6 @@
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/reachability/PrintDominance.qll",
     "cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/reachability/PrintDominance.qll"
   ],
-  "C# IR InstructionImports": [
-    "csharp/ql/src/experimental/ir/implementation/raw/internal/InstructionImports.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/InstructionImports.qll"
-  ],
-  "C# IR IRImports": [
-    "csharp/ql/src/experimental/ir/implementation/raw/internal/IRImports.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/IRImports.qll"
-  ],
-  "C# IR IRBlockImports": [
-    "csharp/ql/src/experimental/ir/implementation/raw/internal/IRBlockImports.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/IRBlockImports.qll"
-  ],
-  "C# IR IRFunctionImports": [
-    "csharp/ql/src/experimental/ir/implementation/raw/internal/IRFunctionImports.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/IRFunctionImports.qll"
-  ],
-  "C# IR IRVariableImports": [
-    "csharp/ql/src/experimental/ir/implementation/raw/internal/IRVariableImports.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/IRVariableImports.qll"
-  ],
-  "C# IR OperandImports": [
-    "csharp/ql/src/experimental/ir/implementation/raw/internal/OperandImports.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/OperandImports.qll"
-  ],
-  "C# IR PrintIRImports": [
-    "csharp/ql/src/experimental/ir/implementation/raw/internal/PrintIRImports.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/internal/PrintIRImports.qll"
-  ],
-  "C# IR ValueNumberingImports": [
-    "csharp/ql/src/experimental/ir/implementation/raw/gvn/internal/ValueNumberingImports.qll",
-    "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingImports.qll"
-  ],
   "C# ControlFlowReachability": [
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/ControlFlowReachability.qll",
     "csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/ControlFlowReachability.qll"
@@ -377,13 +251,6 @@
     "cpp/ql/src/Security/CWE/CWE-020/SafeExternalAPIFunction.qll",
     "cpp/ql/src/Security/CWE/CWE-020/ir/SafeExternalAPIFunction.qll"
   ],
-  "XML": [
-    "cpp/ql/lib/semmle/code/cpp/XML.qll",
-    "csharp/ql/lib/semmle/code/csharp/XML.qll",
-    "java/ql/lib/semmle/code/xml/XML.qll",
-    "javascript/ql/lib/semmle/javascript/XML.qll",
-    "python/ql/lib/semmle/python/xml/XML.qll"
-  ],
   "DuplicationProblems.inc.qhelp": [
     "cpp/ql/src/Metrics/Files/DuplicationProblems.inc.qhelp",
     "javascript/ql/src/Metrics/DuplicationProblems.inc.qhelp",
@@ -495,7 +362,7 @@
     "java/ql/lib/semmle/code/java/security/internal/EncryptionKeySizes.qll"
   ],
   "Python model summaries test extension": [
-    "python/ql/test/experimental/dataflow/model-summaries/InlineTaintTest.ext.yml",
-    "python/ql/test/experimental/dataflow/model-summaries/NormalDataflowTest.ext.yml"
+    "python/ql/test/library-tests/dataflow/model-summaries/InlineTaintTest.ext.yml",
+    "python/ql/test/library-tests/dataflow/model-summaries/NormalDataflowTest.ext.yml"
   ]
-}
+}

cpp/BUILD.bazel

@@ -1,4 +1,4 @@
-load("@rules_pkg//:mappings.bzl", "pkg_filegroup")
+load("@rules_pkg//pkg:mappings.bzl", "pkg_filegroup")
 
 package(default_visibility = ["//visibility:public"])
 

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

@@ -203,6 +203,8 @@ namespace Semmle.Autobuild.Cpp.Tests
         public IList<DiagnosticMessage> Diagnostics { get; } = new List<DiagnosticMessage>();
 
         public void AddEntry(DiagnosticMessage message) => this.Diagnostics.Add(message);
+
+        public void Dispose() { }
     }
 
     /// <summary>
@@ -250,12 +252,7 @@ namespace Semmle.Autobuild.Cpp.Tests
             EndCallbackIn.Add(s);
         }
 
-        CppAutobuilder CreateAutoBuilder(bool isWindows,
-            string? buildless = null, string? solution = null, string? buildCommand = null, string? ignoreErrors = null,
-            string? msBuildArguments = null, string? msBuildPlatform = null, string? msBuildConfiguration = null, string? msBuildTarget = null,
-            string? dotnetArguments = null, string? dotnetVersion = null, string? vsToolsVersion = null,
-            string? nugetRestore = null, string? allSolutions = null,
-            string cwd = @"C:\Project")
+        CppAutobuilder CreateAutoBuilder(bool isWindows, string? dotnetVersion = null, string cwd = @"C:\Project")
         {
             string codeqlUpperLanguage = Language.Cpp.UpperCaseName;
             Actions.GetEnvironmentVariable[$"CODEQL_AUTOBUILDER_{codeqlUpperLanguage}_NO_INDEXING"] = "false";
@@ -265,22 +262,7 @@ namespace Semmle.Autobuild.Cpp.Tests
             Actions.GetEnvironmentVariable[$"CODEQL_EXTRACTOR_{codeqlUpperLanguage}_DIAGNOSTIC_DIR"] = "";
             Actions.GetEnvironmentVariable["CODEQL_JAVA_HOME"] = @"C:\codeql\tools\java";
             Actions.GetEnvironmentVariable["CODEQL_PLATFORM"] = "win64";
-            Actions.GetEnvironmentVariable["SEMMLE_DIST"] = @"C:\odasa";
-            Actions.GetEnvironmentVariable["SEMMLE_JAVA_HOME"] = @"C:\odasa\tools\java";
-            Actions.GetEnvironmentVariable["SEMMLE_PLATFORM_TOOLS"] = @"C:\odasa\tools";
-            Actions.GetEnvironmentVariable["LGTM_INDEX_VSTOOLS_VERSION"] = vsToolsVersion;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_MSBUILD_ARGUMENTS"] = msBuildArguments;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_MSBUILD_PLATFORM"] = msBuildPlatform;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_MSBUILD_CONFIGURATION"] = msBuildConfiguration;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_MSBUILD_TARGET"] = msBuildTarget;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_DOTNET_ARGUMENTS"] = dotnetArguments;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_DOTNET_VERSION"] = dotnetVersion;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_BUILD_COMMAND"] = buildCommand;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_SOLUTION"] = solution;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_IGNORE_ERRORS"] = ignoreErrors;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_BUILDLESS"] = buildless;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_ALL_SOLUTIONS"] = allSolutions;
-            Actions.GetEnvironmentVariable["LGTM_INDEX_NUGET_RESTORE"] = nugetRestore;
+            Actions.GetEnvironmentVariable["CODEQL_EXTRACTOR_CSHARP_OPTION_DOTNET_VERSION"] = dotnetVersion;
             Actions.GetEnvironmentVariable["ProgramFiles(x86)"] = isWindows ? @"C:\Program Files (x86)" : null;
             Actions.GetCurrentDirectory = cwd;
             Actions.IsWindows = isWindows;

cpp/autobuilder/Semmle.Autobuild.Cpp/CppAutobuilder.cs

@@ -26,9 +26,6 @@ namespace Semmle.Autobuild.Cpp
 
         public override BuildScript GetBuildScript()
         {
-            if (Options.BuildCommand != null)
-                return new BuildCommandRule((_, f) => f(null)).Analyse(this, false);
-
             return
                 // First try MSBuild
                 new MsBuildRule().Analyse(this, true) |

cpp/autobuilder/Semmle.Autobuild.Cpp/Program.cs

@@ -17,7 +17,7 @@ namespace Semmle.Autobuild.Cpp
                 try
                 {
                     Console.WriteLine("CodeQL C++ autobuilder");
-                    var builder = new CppAutobuilder(actions, options);
+                    using var builder = new CppAutobuilder(actions, options);
                     return builder.AttemptBuild();
                 }
                 catch (InvalidEnvironmentException ex)

cpp/downgrades/BUILD.bazel

@@ -1,4 +1,4 @@
-load("@rules_pkg//:mappings.bzl", "pkg_files", "strip_prefix")
+load("@rules_pkg//pkg:mappings.bzl", "pkg_files", "strip_prefix")
 
 pkg_files(
     name = "downgrades",

cpp/downgrades/aa7ff0ab32cd4674f6ab731d32fea64116997b05/exprs.ql

@@ -0,0 +1,13 @@
+class Expr extends @expr {
+  string toString() { none() }
+}
+
+class Location extends @location_expr {
+  string toString() { none() }
+}
+
+from Expr expr, int kind, int kind_new, Location loc
+where
+  exprs(expr, kind, loc) and
+  if kind = 363 then kind_new = 1 else kind_new = kind
+select expr, kind_new, loc

cpp/downgrades/aa7ff0ab32cd4674f6ab731d32fea64116997b05/upgrade.properties

@@ -0,0 +1,4 @@
+description: Introduce re-use expressions
+compatibility: partial
+expr_reuse.rel: delete
+exprs.rel: run exprs.qlo

cpp/downgrades/abfce5c170f93e281948f7689ece373464fdaf87/expr_reuse.ql

@@ -0,0 +1,7 @@
+class Expr extends @expr {
+  string toString() { none() }
+}
+
+from Expr reuse, Expr original
+where expr_reuse(reuse, original, _)
+select reuse, original

cpp/downgrades/abfce5c170f93e281948f7689ece373464fdaf87/expr_types.ql

@@ -0,0 +1,22 @@
+class Expr extends @expr {
+  string toString() { none() }
+}
+
+class Type extends @type {
+  string toString() { none() }
+}
+
+predicate existingType(Expr expr, Type type, int value_category) {
+  expr_types(expr, type, value_category)
+}
+
+predicate reuseType(Expr reuse, Type type, int value_category) {
+  exists(Expr original |
+    expr_reuse(reuse, original, value_category) and
+    expr_types(original, type, _)
+  )
+}
+
+from Expr expr, Type type, int value_category
+where existingType(expr, type, value_category) or reuseType(expr, type, value_category)
+select expr, type, value_category

cpp/downgrades/abfce5c170f93e281948f7689ece373464fdaf87/upgrade.properties

@@ -0,0 +1,4 @@
+description: Add value category to expr_reuse table
+compatibility: full
+expr_reuse.rel: run expr_reuse.qlo
+expr_types.rel: run expr_types.qlo

cpp/ql/lib/BUILD.bazel

@@ -1,4 +1,4 @@
-load("@rules_pkg//:mappings.bzl", "pkg_files")
+load("@rules_pkg//pkg:mappings.bzl", "pkg_files")
 
 package(default_visibility = ["//cpp:__pkg__"])
 

cpp/ql/lib/CHANGELOG.md

@@ -1,3 +1,47 @@
+## 0.13.0
+
+### Breaking Changes
+
+* Deleted the deprecated `GlobalValueNumberingImpl.qll` implementation.
+
+### New Features
+
+* Models-as-Data support has been added for C/C++. This feature allows flow sources, sinks and summaries to be expressed in compact strings as an alternative to modelling each source / sink / summary with explicit QL. See `dataflow/ExternalFlow.qll` for documentation and specification of the model format, and `models/implementations/ZMQ.qll` for a simple example of models. Importing models from `.yml` is not yet supported.
+
+### Minor Analysis Improvements
+
+* Source models have been added for the standard library function `getc` (and variations).
+* Source, sink and flow models for the ZeroMQ (ZMQ) networking library have been added.
+* Parameters of functions without definitions now have `ParameterNode`s.
+* The alias analysis used internally by various libraries has been improved to answer alias questions more conservatively. As a result, some queries may report fewer false positives.
+
+## 0.12.11
+
+No user-facing changes.
+
+## 0.12.10
+
+### New Features
+
+* Added a `TaintInheritingContent` class that can be extended to model taint flowing from a qualifier to a field.
+* Added a predicate `GuardCondition.comparesEq/4` to query whether an expression is compared to a constant. 
+* Added a predicate `GuardCondition.ensuresEq/4` to query whether a basic block is guarded by an expression being equal to a constant.
+* Added a predicate `GuardCondition.comparesLt/4` to query whether an expression is compared to a constant. 
+* Added a predicate `GuardCondition.ensuresLt/4` to query whether a basic block is guarded by an expression being less than a constant.
+* Added a predicate `GuardCondition.valueControls` to query whether a basic block is guarded by a particular `case` of a `switch` statement.
+
+### Minor Analysis Improvements
+
+* Added destructors for temporary objects with extended lifetimes to the intermediate representation.
+
+## 0.12.9
+
+No user-facing changes.
+
+## 0.12.8
+
+No user-facing changes.
+
 ## 0.12.7
 
 ### Minor Analysis Improvements

cpp/ql/lib/change-notes/released/0.12.10.md

@@ -0,0 +1,14 @@
+## 0.12.10
+
+### New Features
+
+* Added a `TaintInheritingContent` class that can be extended to model taint flowing from a qualifier to a field.
+* Added a predicate `GuardCondition.comparesEq/4` to query whether an expression is compared to a constant. 
+* Added a predicate `GuardCondition.ensuresEq/4` to query whether a basic block is guarded by an expression being equal to a constant.
+* Added a predicate `GuardCondition.comparesLt/4` to query whether an expression is compared to a constant. 
+* Added a predicate `GuardCondition.ensuresLt/4` to query whether a basic block is guarded by an expression being less than a constant.
+* Added a predicate `GuardCondition.valueControls` to query whether a basic block is guarded by a particular `case` of a `switch` statement.
+
+### Minor Analysis Improvements
+
+* Added destructors for temporary objects with extended lifetimes to the intermediate representation.

cpp/ql/lib/change-notes/released/0.12.11.md

@@ -0,0 +1,3 @@
+## 0.12.11
+
+No user-facing changes.

cpp/ql/lib/change-notes/released/0.12.8.md

@@ -0,0 +1,3 @@
+## 0.12.8
+
+No user-facing changes.

cpp/ql/lib/change-notes/released/0.12.9.md

@@ -0,0 +1,3 @@
+## 0.12.9
+
+No user-facing changes.

cpp/ql/lib/change-notes/released/0.13.0.md

@@ -0,0 +1,16 @@
+## 0.13.0
+
+### Breaking Changes
+
+* Deleted the deprecated `GlobalValueNumberingImpl.qll` implementation.
+
+### New Features
+
+* Models-as-Data support has been added for C/C++. This feature allows flow sources, sinks and summaries to be expressed in compact strings as an alternative to modelling each source / sink / summary with explicit QL. See `dataflow/ExternalFlow.qll` for documentation and specification of the model format, and `models/implementations/ZMQ.qll` for a simple example of models. Importing models from `.yml` is not yet supported.
+
+### Minor Analysis Improvements
+
+* Source models have been added for the standard library function `getc` (and variations).
+* Source, sink and flow models for the ZeroMQ (ZMQ) networking library have been added.
+* Parameters of functions without definitions now have `ParameterNode`s.
+* The alias analysis used internally by various libraries has been improved to answer alias questions more conservatively. As a result, some queries may report fewer false positives.

cpp/ql/lib/codeql-pack.release.yml

@@ -1,2 +1,2 @@
 ---
-lastReleaseVersion: 0.12.7
+lastReleaseVersion: 0.13.0

cpp/ql/lib/qlpack.yml

@@ -1,5 +1,5 @@
 name: codeql/cpp-all
-version: 0.12.7
+version: 0.13.0
 groups: cpp
 dbscheme: semmlecode.cpp.dbscheme
 extractor: cpp
@@ -7,8 +7,11 @@ library: true
 upgrades: upgrades
 dependencies:
   codeql/dataflow: ${workspace}
+  codeql/mad: ${workspace}
   codeql/rangeanalysis: ${workspace}
   codeql/ssa: ${workspace}
+  codeql/typeflow: ${workspace}
   codeql/tutorial: ${workspace}
   codeql/util: ${workspace}
+  codeql/xml: ${workspace}
 warnOnImplicitThis: true

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

@@ -309,9 +309,12 @@ class ExprNode extends AstNode {
   override AstNode getChildInternal(int childIndex) {
     result.getAst() = expr.getChild(childIndex)
     or
+    childIndex = max(int index | exists(expr.getChild(index)) or index = 0) + 1 and
+    result.getAst() = expr.(ConditionDeclExpr).getInitializingExpr()
+    or
     exists(int destructorIndex |
       result.getAst() = expr.getImplicitDestructorCall(destructorIndex) and
-      childIndex = destructorIndex + max(int index | exists(expr.getChild(index)) or index = 0) + 1
+      childIndex = destructorIndex + max(int index | exists(expr.getChild(index)) or index = 0) + 2
     )
   }
 
@@ -361,6 +364,8 @@ class ConversionNode extends ExprNode {
     childIndex = 0 and
     result.getAst() = conv.getExpr() and
     conv.getExpr() instanceof Conversion
+    or
+    result.getAst() = expr.getImplicitDestructorCall(childIndex - 1)
   }
 }
 
@@ -458,6 +463,25 @@ class StmtNode extends AstNode {
   }
 }
 
+/**
+ * A node representing a child of a `Stmt` that is itself a `Stmt`.
+ */
+class ChildStmtNode extends StmtNode {
+  Stmt childStmt;
+
+  ChildStmtNode() { exists(Stmt parent | parent.getAChild() = childStmt and childStmt = ast) }
+
+  override BaseAstNode getChildInternal(int childIndex) {
+    result = super.getChildInternal(childIndex)
+    or
+    exists(int destructorIndex |
+      result.getAst() = childStmt.getImplicitDestructorCall(destructorIndex) and
+      childIndex =
+        destructorIndex + max(int index | exists(childStmt.getChild(index)) or index = 0) + 1
+    )
+  }
+}
+
 /**
  * A node representing a `DeclStmt`.
  */
@@ -669,6 +693,13 @@ class FunctionNode extends FunctionOrGlobalOrNamespaceVariableNode {
 private string getChildAccessorWithoutConversions(Locatable parent, Element child) {
   shouldPrintDeclaration(getAnEnclosingDeclaration(parent)) and
   (
+    exists(Stmt s, int i | s.getChild(i) = parent |
+      exists(int n |
+        s.getChild(i).(Stmt).getImplicitDestructorCall(n) = child and
+        result = "getImplicitDestructorCall(" + n + ")"
+      )
+    )
+    or
     exists(Stmt s | s = parent |
       namedStmtChildPredicates(s, child, result)
       or
@@ -686,6 +717,8 @@ private string getChildAccessorWithoutConversions(Locatable parent, Element chil
       not namedExprChildPredicates(expr, child, _) and
       exists(int n | expr.getChild(n) = child and result = "getChild(" + n + ")")
       or
+      expr.(ConditionDeclExpr).getInitializingExpr() = child and result = "getInitializingExpr()"
+      or
       exists(int n |
         expr.getImplicitDestructorCall(n) = child and
         result = "getImplicitDestructorCall(" + n + ")"
@@ -857,7 +890,7 @@ private predicate namedExprChildPredicates(Expr expr, Element ele, string pred)
     or
     expr.(DeleteOrDeleteArrayExpr).getDestructorCall() = ele and pred = "getDestructorCall()"
     or
-    expr.(DeleteOrDeleteArrayExpr).getExpr() = ele and pred = "getExpr()"
+    expr.(DeleteOrDeleteArrayExpr).getExprWithReuse() = ele and pred = "getExprWithReuse()"
     or
     expr.(DestructorFieldDestruction).getExpr() = ele and pred = "getExpr()"
     or

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

@@ -590,6 +590,33 @@ class TemplateVariable extends Variable {
   Variable getAnInstantiation() { result.isConstructedFrom(this) }
 }
 
+/**
+ * A variable that is an instantiation of a template. For example
+ * the instantiation `myTemplateVariable<int>` in the following code:
+ * ```
+ * template<class T>
+ * T myTemplateVariable;
+ *
+ * void caller(int i) {
+ *   myTemplateVariable<int> = i;
+ * }
+ * ```
+ */
+class VariableTemplateInstantiation extends Variable {
+  TemplateVariable tv;
+
+  VariableTemplateInstantiation() { tv.getAnInstantiation() = this }
+
+  override string getAPrimaryQlClass() { result = "VariableTemplateInstantiation" }
+
+  /**
+   * Gets the variable template from which this instantiation was instantiated.
+   *
+   * Example: For `int x<int>`, returns `T x`.
+   */
+  TemplateVariable getTemplate() { result = tv }
+}
+
 /**
  * A non-static local variable or parameter that is not part of an
  * uninstantiated template. Uninstantiated templates are purely syntax, and

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

@@ -3,305 +3,67 @@
  */
 
 import semmle.files.FileSystem
+private import codeql.xml.Xml
 
-private class TXmlLocatable =
-  @xmldtd or @xmlelement or @xmlattribute or @xmlnamespace or @xmlcomment or @xmlcharacters;
+private module Input implements InputSig<File, Location> {
+  class XmlLocatableBase = @xmllocatable or @xmlnamespaceable;
 
-/** An XML element that has a location. */
-class XmlLocatable extends @xmllocatable, TXmlLocatable {
-  /** Gets the source location for this element. */
-  Location getLocation() { xmllocations(this, result) }
+  predicate xmllocations_(XmlLocatableBase e, Location loc) { xmllocations(e, loc) }
 
-  /**
-   * Holds if this element is at the specified location.
-   * The location spans column `startcolumn` of line `startline` to
-   * column `endcolumn` of line `endline` in file `filepath`.
-   * For more information, see
-   * [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
-   */
-  predicate hasLocationInfo(
-    string filepath, int startline, int startcolumn, int endline, int endcolumn
+  class XmlParentBase = @xmlparent;
+
+  class XmlNamespaceableBase = @xmlnamespaceable;
+
+  class XmlElementBase = @xmlelement;
+
+  class XmlFileBase = File;
+
+  predicate xmlEncoding_(XmlFileBase f, string enc) { xmlEncoding(f, enc) }
+
+  class XmlDtdBase = @xmldtd;
+
+  predicate xmlDTDs_(XmlDtdBase e, string root, string publicId, string systemId, XmlFileBase file) {
+    xmlDTDs(e, root, publicId, systemId, file)
+  }
+
+  predicate xmlElements_(
+    XmlElementBase e, string name, XmlParentBase parent, int idx, XmlFileBase file
   ) {
-    exists(File f, Location l | l = this.getLocation() |
-      locations_default(l, f, startline, startcolumn, endline, endcolumn) and
-      filepath = f.getAbsolutePath()
-    )
+    xmlElements(e, name, parent, idx, file)
   }
 
-  /** Gets a textual representation of this element. */
-  string toString() { none() } // overridden in subclasses
-}
+  class XmlAttributeBase = @xmlattribute;
 
-/**
- * An `XmlParent` is either an `XmlElement` or an `XmlFile`,
- * both of which can contain other elements.
- */
-class XmlParent extends @xmlparent {
-  XmlParent() {
-    // explicitly restrict `this` to be either an `XmlElement` or an `XmlFile`;
-    // the type `@xmlparent` currently also includes non-XML files
-    this instanceof @xmlelement or xmlEncoding(this, _)
+  predicate xmlAttrs_(
+    XmlAttributeBase e, XmlElementBase elementid, string name, string value, int idx,
+    XmlFileBase file
+  ) {
+    xmlAttrs(e, elementid, name, value, idx, file)
   }
 
-  /**
-   * Gets a printable representation of this XML parent.
-   * (Intended to be overridden in subclasses.)
-   */
-  string getName() { none() } // overridden in subclasses
+  class XmlNamespaceBase = @xmlnamespace;
 
-  /** Gets the file to which this XML parent belongs. */
-  XmlFile getFile() { result = this or xmlElements(this, _, _, _, result) }
-
-  /** Gets the child element at a specified index of this XML parent. */
-  XmlElement getChild(int index) { xmlElements(result, _, this, index, _) }
-
-  /** Gets a child element of this XML parent. */
-  XmlElement getAChild() { xmlElements(result, _, this, _, _) }
-
-  /** Gets a child element of this XML parent with the given `name`. */
-  XmlElement getAChild(string name) { xmlElements(result, _, this, _, _) and result.hasName(name) }
-
-  /** Gets a comment that is a child of this XML parent. */
-  XmlComment getAComment() { xmlComments(result, _, this, _) }
-
-  /** Gets a character sequence that is a child of this XML parent. */
-  XmlCharacters getACharactersSet() { xmlChars(result, _, this, _, _, _) }
-
-  /** Gets the depth in the tree. (Overridden in XmlElement.) */
-  int getDepth() { result = 0 }
-
-  /** Gets the number of child XML elements of this XML parent. */
-  int getNumberOfChildren() { result = count(XmlElement e | xmlElements(e, _, this, _, _)) }
-
-  /** Gets the number of places in the body of this XML parent where text occurs. */
-  int getNumberOfCharacterSets() { result = count(int pos | xmlChars(_, _, this, pos, _, _)) }
-
-  /**
-   * Gets the result of appending all the character sequences of this XML parent from
-   * left to right, separated by a space.
-   */
-  string allCharactersString() {
-    result =
-      concat(string chars, int pos | xmlChars(_, chars, this, pos, _, _) | chars, " " order by pos)
+  predicate xmlNs_(XmlNamespaceBase e, string prefixName, string uri, XmlFileBase file) {
+    xmlNs(e, prefixName, uri, file)
   }
 
-  /** Gets the text value contained in this XML parent. */
-  string getTextValue() { result = this.allCharactersString() }
+  predicate xmlHasNs_(XmlNamespaceableBase e, XmlNamespaceBase ns, XmlFileBase file) {
+    xmlHasNs(e, ns, file)
+  }
 
-  /** Gets a printable representation of this XML parent. */
-  string toString() { result = this.getName() }
-}
+  class XmlCommentBase = @xmlcomment;
 
-/** An XML file. */
-class XmlFile extends XmlParent, File {
-  XmlFile() { xmlEncoding(this, _) }
+  predicate xmlComments_(XmlCommentBase e, string text, XmlParentBase parent, XmlFileBase file) {
+    xmlComments(e, text, parent, file)
+  }
 
-  /** Gets a printable representation of this XML file. */
-  override string toString() { result = this.getName() }
+  class XmlCharactersBase = @xmlcharacters;
 
-  /** Gets the name of this XML file. */
-  override string getName() { result = File.super.getAbsolutePath() }
-
-  /** Gets the encoding of this XML file. */
-  string getEncoding() { xmlEncoding(this, result) }
-
-  /** Gets the XML file itself. */
-  override XmlFile getFile() { result = this }
-
-  /** Gets a top-most element in an XML file. */
-  XmlElement getARootElement() { result = this.getAChild() }
-
-  /** Gets a DTD associated with this XML file. */
-  XmlDtd getADtd() { xmlDTDs(result, _, _, _, this) }
-}
-
-/**
- * An XML document type definition (DTD).
- *
- * Example:
- *
- * ```
- * <!ELEMENT person (firstName, lastName?)>
- * <!ELEMENT firstName (#PCDATA)>
- * <!ELEMENT lastName (#PCDATA)>
- * ```
- */
-class XmlDtd extends XmlLocatable, @xmldtd {
-  /** Gets the name of the root element of this DTD. */
-  string getRoot() { xmlDTDs(this, result, _, _, _) }
-
-  /** Gets the public ID of this DTD. */
-  string getPublicId() { xmlDTDs(this, _, result, _, _) }
-
-  /** Gets the system ID of this DTD. */
-  string getSystemId() { xmlDTDs(this, _, _, result, _) }
-
-  /** Holds if this DTD is public. */
-  predicate isPublic() { not xmlDTDs(this, _, "", _, _) }
-
-  /** Gets the parent of this DTD. */
-  XmlParent getParent() { xmlDTDs(this, _, _, _, result) }
-
-  override string toString() {
-    this.isPublic() and
-    result = this.getRoot() + " PUBLIC '" + this.getPublicId() + "' '" + this.getSystemId() + "'"
-    or
-    not this.isPublic() and
-    result = this.getRoot() + " SYSTEM '" + this.getSystemId() + "'"
+  predicate xmlChars_(
+    XmlCharactersBase e, string text, XmlParentBase parent, int idx, int isCDATA, XmlFileBase file
+  ) {
+    xmlChars(e, text, parent, idx, isCDATA, file)
   }
 }
 
-/**
- * An XML element in an XML file.
- *
- * Example:
- *
- * ```
- * <manifest xmlns:android="http://schemas.android.com/apk/res/android"
- *           package="com.example.exampleapp" android:versionCode="1">
- * </manifest>
- * ```
- */
-class XmlElement extends @xmlelement, XmlParent, XmlLocatable {
-  /** Holds if this XML element has the given `name`. */
-  predicate hasName(string name) { name = this.getName() }
-
-  /** Gets the name of this XML element. */
-  override string getName() { xmlElements(this, result, _, _, _) }
-
-  /** Gets the XML file in which this XML element occurs. */
-  override XmlFile getFile() { xmlElements(this, _, _, _, result) }
-
-  /** Gets the parent of this XML element. */
-  XmlParent getParent() { xmlElements(this, _, result, _, _) }
-
-  /** Gets the index of this XML element among its parent's children. */
-  int getIndex() { xmlElements(this, _, _, result, _) }
-
-  /** Holds if this XML element has a namespace. */
-  predicate hasNamespace() { xmlHasNs(this, _, _) }
-
-  /** Gets the namespace of this XML element, if any. */
-  XmlNamespace getNamespace() { xmlHasNs(this, result, _) }
-
-  /** Gets the index of this XML element among its parent's children. */
-  int getElementPositionIndex() { xmlElements(this, _, _, result, _) }
-
-  /** Gets the depth of this element within the XML file tree structure. */
-  override int getDepth() { result = this.getParent().getDepth() + 1 }
-
-  /** Gets an XML attribute of this XML element. */
-  XmlAttribute getAnAttribute() { result.getElement() = this }
-
-  /** Gets the attribute with the specified `name`, if any. */
-  XmlAttribute getAttribute(string name) { result.getElement() = this and result.getName() = name }
-
-  /** Holds if this XML element has an attribute with the specified `name`. */
-  predicate hasAttribute(string name) { exists(this.getAttribute(name)) }
-
-  /** Gets the value of the attribute with the specified `name`, if any. */
-  string getAttributeValue(string name) { result = this.getAttribute(name).getValue() }
-
-  /** Gets a printable representation of this XML element. */
-  override string toString() { result = this.getName() }
-}
-
-/**
- * An attribute that occurs inside an XML element.
- *
- * Examples:
- *
- * ```
- * package="com.example.exampleapp"
- * android:versionCode="1"
- * ```
- */
-class XmlAttribute extends @xmlattribute, XmlLocatable {
-  /** Gets the name of this attribute. */
-  string getName() { xmlAttrs(this, _, result, _, _, _) }
-
-  /** Gets the XML element to which this attribute belongs. */
-  XmlElement getElement() { xmlAttrs(this, result, _, _, _, _) }
-
-  /** Holds if this attribute has a namespace. */
-  predicate hasNamespace() { xmlHasNs(this, _, _) }
-
-  /** Gets the namespace of this attribute, if any. */
-  XmlNamespace getNamespace() { xmlHasNs(this, result, _) }
-
-  /** Gets the value of this attribute. */
-  string getValue() { xmlAttrs(this, _, _, result, _, _) }
-
-  /** Gets a printable representation of this XML attribute. */
-  override string toString() { result = this.getName() + "=" + this.getValue() }
-}
-
-/**
- * A namespace used in an XML file.
- *
- * Example:
- *
- * ```
- * xmlns:android="http://schemas.android.com/apk/res/android"
- * ```
- */
-class XmlNamespace extends XmlLocatable, @xmlnamespace {
-  /** Gets the prefix of this namespace. */
-  string getPrefix() { xmlNs(this, result, _, _) }
-
-  /** Gets the URI of this namespace. */
-  string getUri() { xmlNs(this, _, result, _) }
-
-  /** Holds if this namespace has no prefix. */
-  predicate isDefault() { this.getPrefix() = "" }
-
-  override string toString() {
-    this.isDefault() and result = this.getUri()
-    or
-    not this.isDefault() and result = this.getPrefix() + ":" + this.getUri()
-  }
-}
-
-/**
- * A comment in an XML file.
- *
- * Example:
- *
- * ```
- * <!-- This is a comment. -->
- * ```
- */
-class XmlComment extends @xmlcomment, XmlLocatable {
-  /** Gets the text content of this XML comment. */
-  string getText() { xmlComments(this, result, _, _) }
-
-  /** Gets the parent of this XML comment. */
-  XmlParent getParent() { xmlComments(this, _, result, _) }
-
-  /** Gets a printable representation of this XML comment. */
-  override string toString() { result = this.getText() }
-}
-
-/**
- * A sequence of characters that occurs between opening and
- * closing tags of an XML element, excluding other elements.
- *
- * Example:
- *
- * ```
- * <content>This is a sequence of characters.</content>
- * ```
- */
-class XmlCharacters extends @xmlcharacters, XmlLocatable {
-  /** Gets the content of this character sequence. */
-  string getCharacters() { xmlChars(this, result, _, _, _, _) }
-
-  /** Gets the parent of this character sequence. */
-  XmlParent getParent() { xmlChars(this, _, result, _, _, _) }
-
-  /** Holds if this character sequence is CDATA. */
-  predicate isCDATA() { xmlChars(this, _, _, _, 1, _) }
-
-  /** Gets a printable representation of this XML character sequence. */
-  override string toString() { result = this.getCharacters() }
-}
+import Make<File, Location, Input>

cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll

@@ -20,6 +20,44 @@ private predicate isUnreachedBlock(IRBlock block) {
   block.getFirstInstruction() instanceof UnreachedInstruction
 }
 
+private newtype TAbstractValue =
+  TBooleanValue(boolean b) { b = true or b = false } or
+  TMatchValue(CaseEdge c)
+
+/**
+ * An abstract value. This is either a boolean value, or a `switch` case.
+ */
+abstract class AbstractValue extends TAbstractValue {
+  /** Gets an abstract value that represents the dual of this value, if any. */
+  abstract AbstractValue getDualValue();
+
+  /** Gets a textual representation of this abstract value. */
+  abstract string toString();
+}
+
+/** A Boolean value. */
+class BooleanValue extends AbstractValue, TBooleanValue {
+  /** Gets the underlying Boolean value. */
+  boolean getValue() { this = TBooleanValue(result) }
+
+  override BooleanValue getDualValue() { result.getValue() = this.getValue().booleanNot() }
+
+  override string toString() { result = this.getValue().toString() }
+}
+
+/** A value that represents a match against a specific `switch` case. */
+class MatchValue extends AbstractValue, TMatchValue {
+  /** Gets the case. */
+  CaseEdge getCase() { this = TMatchValue(result) }
+
+  override MatchValue getDualValue() {
+    // A `MatchValue` has no dual.
+    none()
+  }
+
+  override string toString() { result = this.getCase().toString() }
+}
+
 /**
  * A Boolean condition in the AST that guards one or more basic blocks. This includes
  * operands of logical operators but not switch statements.
@@ -34,6 +72,15 @@ class GuardCondition extends Expr {
     this.(BinaryLogicalOperation).getAnOperand() instanceof GuardCondition
   }
 
+  /**
+   * Holds if this condition controls `controlled`, meaning that `controlled` is only
+   * entered if the value of this condition is `v`.
+   *
+   * For details on what "controls" mean, see the QLDoc for `controls`.
+   */
+  cached
+  predicate valueControls(BasicBlock controlled, AbstractValue v) { none() }
+
   /**
    * Holds if this condition controls `controlled`, meaning that `controlled` is only
    * entered if the value of this condition is `testIsTrue`.
@@ -61,7 +108,9 @@ class GuardCondition extends Expr {
    * true (for `&&`) or false (for `||`) branch.
    */
   cached
-  predicate controls(BasicBlock controlled, boolean testIsTrue) { none() }
+  final predicate controls(BasicBlock controlled, boolean testIsTrue) {
+    this.valueControls(controlled, any(BooleanValue bv | bv.getValue() = testIsTrue))
+  }
 
   /** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
   cached
@@ -76,6 +125,20 @@ class GuardCondition extends Expr {
   cached
   predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) { none() }
 
+  /**
+   * Holds if (determined by this guard) `e < k` evaluates to `isLessThan` if
+   * this expression evaluates to `value`.
+   */
+  cached
+  predicate comparesLt(Expr e, int k, boolean isLessThan, AbstractValue value) { none() }
+
+  /**
+   * Holds if (determined by this guard) `e < k` must be `isLessThan` in `block`.
+   * If `isLessThan = false` then this implies `e >= k`.
+   */
+  cached
+  predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan) { none() }
+
   /** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
   cached
   predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) {
@@ -88,6 +151,17 @@ class GuardCondition extends Expr {
    */
   cached
   predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual) { none() }
+
+  /** Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression evaluates to `value`. */
+  cached
+  predicate comparesEq(Expr e, int k, boolean areEqual, AbstractValue value) { none() }
+
+  /**
+   * Holds if (determined by this guard) `e == k` must be `areEqual` in `block`.
+   * If `areEqual = false` then this implies `e != k`.
+   */
+  cached
+  predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) { none() }
 }
 
 /**
@@ -98,13 +172,13 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition {
     this.(BinaryLogicalOperation).getAnOperand() instanceof GuardCondition
   }
 
-  override predicate controls(BasicBlock controlled, boolean testIsTrue) {
+  override predicate valueControls(BasicBlock controlled, AbstractValue v) {
     exists(BinaryLogicalOperation binop, GuardCondition lhs, GuardCondition rhs |
       this = binop and
       lhs = binop.getLeftOperand() and
       rhs = binop.getRightOperand() and
-      lhs.controls(controlled, testIsTrue) and
-      rhs.controls(controlled, testIsTrue)
+      lhs.valueControls(controlled, v) and
+      rhs.valueControls(controlled, v)
     )
   }
 
@@ -116,12 +190,27 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition {
     )
   }
 
+  override predicate comparesLt(Expr e, int k, boolean isLessThan, AbstractValue value) {
+    exists(BooleanValue partValue, GuardCondition part |
+      this.(BinaryLogicalOperation)
+          .impliesValue(part, partValue.getValue(), value.(BooleanValue).getValue())
+    |
+      part.comparesLt(e, k, isLessThan, partValue)
+    )
+  }
+
   override predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) {
     exists(boolean testIsTrue |
       this.comparesLt(left, right, k, isLessThan, testIsTrue) and this.controls(block, testIsTrue)
     )
   }
 
+  override predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan) {
+    exists(AbstractValue value |
+      this.comparesLt(e, k, isLessThan, value) and this.valueControls(block, value)
+    )
+  }
+
   override predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) {
     exists(boolean partIsTrue, GuardCondition part |
       this.(BinaryLogicalOperation).impliesValue(part, partIsTrue, testIsTrue)
@@ -135,6 +224,21 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition {
       this.comparesEq(left, right, k, areEqual, testIsTrue) and this.controls(block, testIsTrue)
     )
   }
+
+  override predicate comparesEq(Expr e, int k, boolean areEqual, AbstractValue value) {
+    exists(BooleanValue partValue, GuardCondition part |
+      this.(BinaryLogicalOperation)
+          .impliesValue(part, partValue.getValue(), value.(BooleanValue).getValue())
+    |
+      part.comparesEq(e, k, areEqual, partValue)
+    )
+  }
+
+  override predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) {
+    exists(AbstractValue value |
+      this.comparesEq(e, k, areEqual, value) and this.valueControls(block, value)
+    )
+  }
 }
 
 /**
@@ -146,13 +250,12 @@ private class GuardConditionFromIR extends GuardCondition {
 
   GuardConditionFromIR() { this = ir.getUnconvertedResultExpression() }
 
-  override predicate controls(BasicBlock controlled, boolean testIsTrue) {
+  override predicate valueControls(BasicBlock controlled, AbstractValue v) {
     // This condition must determine the flow of control; that is, this
     // node must be a top-level condition.
-    this.controlsBlock(controlled, testIsTrue)
+    this.controlsBlock(controlled, v)
   }
 
-  /** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
   override predicate comparesLt(Expr left, Expr right, int k, boolean isLessThan, boolean testIsTrue) {
     exists(Instruction li, Instruction ri |
       li.getUnconvertedResultExpression() = left and
@@ -161,10 +264,13 @@ private class GuardConditionFromIR extends GuardCondition {
     )
   }
 
-  /**
-   * Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`.
-   * If `isLessThan = false` then this implies `left >= right + k`.
-   */
+  override predicate comparesLt(Expr e, int k, boolean isLessThan, AbstractValue value) {
+    exists(Instruction i |
+      i.getUnconvertedResultExpression() = e and
+      ir.comparesLt(i.getAUse(), k, isLessThan, value)
+    )
+  }
+
   override predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) {
     exists(Instruction li, Instruction ri, boolean testIsTrue |
       li.getUnconvertedResultExpression() = left and
@@ -174,7 +280,14 @@ private class GuardConditionFromIR extends GuardCondition {
     )
   }
 
-  /** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
+  override predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan) {
+    exists(Instruction i, AbstractValue value |
+      i.getUnconvertedResultExpression() = e and
+      ir.comparesLt(i.getAUse(), k, isLessThan, value) and
+      this.valueControls(block, value)
+    )
+  }
+
   override predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) {
     exists(Instruction li, Instruction ri |
       li.getUnconvertedResultExpression() = left and
@@ -183,10 +296,6 @@ private class GuardConditionFromIR extends GuardCondition {
     )
   }
 
-  /**
-   * Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
-   * If `areEqual = false` then this implies `left != right + k`.
-   */
   override predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual) {
     exists(Instruction li, Instruction ri, boolean testIsTrue |
       li.getUnconvertedResultExpression() = left and
@@ -196,15 +305,30 @@ private class GuardConditionFromIR extends GuardCondition {
     )
   }
 
+  override predicate comparesEq(Expr e, int k, boolean areEqual, AbstractValue value) {
+    exists(Instruction i |
+      i.getUnconvertedResultExpression() = e and
+      ir.comparesEq(i.getAUse(), k, areEqual, value)
+    )
+  }
+
+  override predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) {
+    exists(Instruction i, AbstractValue value |
+      i.getUnconvertedResultExpression() = e and
+      ir.comparesEq(i.getAUse(), k, areEqual, value) and
+      this.valueControls(block, value)
+    )
+  }
+
   /**
    * Holds if this condition controls `block`, meaning that `block` is only
-   * entered if the value of this condition is `testIsTrue`. This helper
+   * entered if the value of this condition is `v`. This helper
    * predicate does not necessarily hold for binary logical operations like
    * `&&` and `||`. See the detailed explanation on predicate `controls`.
    */
-  private predicate controlsBlock(BasicBlock controlled, boolean testIsTrue) {
+  private predicate controlsBlock(BasicBlock controlled, AbstractValue v) {
     exists(IRBlock irb |
-      ir.controls(irb, testIsTrue) and
+      ir.valueControls(irb, v) and
       nonExcludedIRAndBasicBlock(irb, controlled) and
       not isUnreachedBlock(irb)
     )
@@ -249,10 +373,28 @@ private predicate nonExcludedIRAndBasicBlock(IRBlock irb, BasicBlock controlled)
  */
 cached
 class IRGuardCondition extends Instruction {
-  ConditionalBranchInstruction branch;
+  Instruction branch;
 
   cached
-  IRGuardCondition() { branch = get_branch_for_condition(this) }
+  IRGuardCondition() { branch = getBranchForCondition(this) }
+
+  /**
+   * Holds if this condition controls `controlled`, meaning that `controlled` is only
+   * entered if the value of this condition is `v`.
+   *
+   * For details on what "controls" mean, see the QLDoc for `controls`.
+   */
+  cached
+  predicate valueControls(IRBlock controlled, AbstractValue v) {
+    // This condition must determine the flow of control; that is, this
+    // node must be a top-level condition.
+    this.controlsBlock(controlled, v)
+    or
+    exists(IRGuardCondition ne |
+      this = ne.(LogicalNotInstruction).getUnary() and
+      ne.valueControls(controlled, v.getDualValue())
+    )
+  }
 
   /**
    * Holds if this condition controls `controlled`, meaning that `controlled` is only
@@ -282,13 +424,25 @@ class IRGuardCondition extends Instruction {
    */
   cached
   predicate controls(IRBlock controlled, boolean testIsTrue) {
-    // This condition must determine the flow of control; that is, this
-    // node must be a top-level condition.
-    this.controlsBlock(controlled, testIsTrue)
+    this.valueControls(controlled, any(BooleanValue bv | bv.getValue() = testIsTrue))
+  }
+
+  /**
+   * Holds if the control-flow edge `(pred, succ)` may be taken only if
+   * the value of this condition is `v`.
+   */
+  cached
+  predicate valueControlsEdge(IRBlock pred, IRBlock succ, AbstractValue v) {
+    pred.getASuccessor() = succ and
+    this.valueControls(pred, v)
     or
-    exists(IRGuardCondition ne |
-      this = ne.(LogicalNotInstruction).getUnary() and
-      ne.controls(controlled, testIsTrue.booleanNot())
+    succ = this.getBranchSuccessor(v) and
+    (
+      branch.(ConditionalBranchInstruction).getCondition() = this and
+      branch.getBlock() = pred
+      or
+      branch.(SwitchInstruction).getExpression() = this and
+      branch.getBlock() = pred
     )
   }
 
@@ -297,17 +451,12 @@ class IRGuardCondition extends Instruction {
    * the value of this condition is `testIsTrue`.
    */
   cached
-  predicate controlsEdge(IRBlock pred, IRBlock succ, boolean testIsTrue) {
-    pred.getASuccessor() = succ and
-    this.controls(pred, testIsTrue)
-    or
-    succ = this.getBranchSuccessor(testIsTrue) and
-    branch.getCondition() = this and
-    branch.getBlock() = pred
+  final predicate controlsEdge(IRBlock pred, IRBlock succ, boolean testIsTrue) {
+    this.valueControlsEdge(pred, succ, any(BooleanValue bv | bv.getValue() = testIsTrue))
   }
 
   /**
-   * Gets the block to which `branch` jumps directly when this condition is `testIsTrue`.
+   * Gets the block to which `branch` jumps directly when the value of this condition is `v`.
    *
    * This predicate is intended to help with situations in which an inference can only be made
    * based on an edge between a block with multiple successors and a block with multiple
@@ -321,21 +470,39 @@ class IRGuardCondition extends Instruction {
    * return x;
    * ```
    */
-  private IRBlock getBranchSuccessor(boolean testIsTrue) {
-    branch.getCondition() = this and
-    (
-      testIsTrue = true and
-      result.getFirstInstruction() = branch.getTrueSuccessor()
+  private IRBlock getBranchSuccessor(AbstractValue v) {
+    branch.(ConditionalBranchInstruction).getCondition() = this and
+    exists(BooleanValue bv | bv = v |
+      bv.getValue() = true and
+      result.getFirstInstruction() = branch.(ConditionalBranchInstruction).getTrueSuccessor()
       or
-      testIsTrue = false and
-      result.getFirstInstruction() = branch.getFalseSuccessor()
+      bv.getValue() = false and
+      result.getFirstInstruction() = branch.(ConditionalBranchInstruction).getFalseSuccessor()
+    )
+    or
+    exists(SwitchInstruction switch, CaseEdge kind | switch = branch |
+      switch.getExpression() = this and
+      result.getFirstInstruction() = switch.getSuccessor(kind) and
+      kind = v.(MatchValue).getCase()
     )
   }
 
   /** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
   cached
   predicate comparesLt(Operand left, Operand right, int k, boolean isLessThan, boolean testIsTrue) {
-    compares_lt(this, left, right, k, isLessThan, testIsTrue)
+    exists(BooleanValue value |
+      compares_lt(this, left, right, k, isLessThan, value) and
+      value.getValue() = testIsTrue
+    )
+  }
+
+  /**
+   * Holds if (determined by this guard) `op < k` evaluates to `isLessThan` if
+   * this expression evaluates to `value`.
+   */
+  cached
+  predicate comparesLt(Operand op, int k, boolean isLessThan, AbstractValue value) {
+    compares_lt(this, op, k, isLessThan, value)
   }
 
   /**
@@ -344,8 +511,19 @@ class IRGuardCondition extends Instruction {
    */
   cached
   predicate ensuresLt(Operand left, Operand right, int k, IRBlock block, boolean isLessThan) {
-    exists(boolean testIsTrue |
-      compares_lt(this, left, right, k, isLessThan, testIsTrue) and this.controls(block, testIsTrue)
+    exists(AbstractValue value |
+      compares_lt(this, left, right, k, isLessThan, value) and this.valueControls(block, value)
+    )
+  }
+
+  /**
+   * Holds if (determined by this guard) `op < k` must be `isLessThan` in `block`.
+   * If `isLessThan = false` then this implies `op >= k`.
+   */
+  cached
+  predicate ensuresLt(Operand op, int k, IRBlock block, boolean isLessThan) {
+    exists(AbstractValue value |
+      compares_lt(this, op, k, isLessThan, value) and this.valueControls(block, value)
     )
   }
 
@@ -357,16 +535,37 @@ class IRGuardCondition extends Instruction {
   predicate ensuresLtEdge(
     Operand left, Operand right, int k, IRBlock pred, IRBlock succ, boolean isLessThan
   ) {
-    exists(boolean testIsTrue |
-      compares_lt(this, left, right, k, isLessThan, testIsTrue) and
-      this.controlsEdge(pred, succ, testIsTrue)
+    exists(AbstractValue value |
+      compares_lt(this, left, right, k, isLessThan, value) and
+      this.valueControlsEdge(pred, succ, value)
+    )
+  }
+
+  /**
+   * Holds if (determined by this guard) `op < k` must be `isLessThan` on the edge from
+   * `pred` to `succ`. If `isLessThan = false` then this implies `op >= k`.
+   */
+  cached
+  predicate ensuresLtEdge(Operand left, int k, IRBlock pred, IRBlock succ, boolean isLessThan) {
+    exists(AbstractValue value |
+      compares_lt(this, left, k, isLessThan, value) and
+      this.valueControlsEdge(pred, succ, value)
     )
   }
 
   /** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
   cached
   predicate comparesEq(Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue) {
-    compares_eq(this, left, right, k, areEqual, testIsTrue)
+    exists(BooleanValue value |
+      compares_eq(this, left, right, k, areEqual, value) and
+      value.getValue() = testIsTrue
+    )
+  }
+
+  /** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `value`. */
+  cached
+  predicate comparesEq(Operand op, int k, boolean areEqual, AbstractValue value) {
+    compares_eq(this, op, k, areEqual, value)
   }
 
   /**
@@ -375,8 +574,19 @@ class IRGuardCondition extends Instruction {
    */
   cached
   predicate ensuresEq(Operand left, Operand right, int k, IRBlock block, boolean areEqual) {
-    exists(boolean testIsTrue |
-      compares_eq(this, left, right, k, areEqual, testIsTrue) and this.controls(block, testIsTrue)
+    exists(AbstractValue value |
+      compares_eq(this, left, right, k, areEqual, value) and this.valueControls(block, value)
+    )
+  }
+
+  /**
+   * Holds if (determined by this guard) `op == k` must be `areEqual` in `block`.
+   * If `areEqual = false` then this implies `op != k`.
+   */
+  cached
+  predicate ensuresEq(Operand op, int k, IRBlock block, boolean areEqual) {
+    exists(AbstractValue value |
+      compares_eq(this, op, k, areEqual, value) and this.valueControls(block, value)
     )
   }
 
@@ -388,19 +598,31 @@ class IRGuardCondition extends Instruction {
   predicate ensuresEqEdge(
     Operand left, Operand right, int k, IRBlock pred, IRBlock succ, boolean areEqual
   ) {
-    exists(boolean testIsTrue |
-      compares_eq(this, left, right, k, areEqual, testIsTrue) and
-      this.controlsEdge(pred, succ, testIsTrue)
+    exists(AbstractValue value |
+      compares_eq(this, left, right, k, areEqual, value) and
+      this.valueControlsEdge(pred, succ, value)
+    )
+  }
+
+  /**
+   * Holds if (determined by this guard) `op == k` must be `areEqual` on the edge from
+   * `pred` to `succ`. If `areEqual = false` then this implies `op != k`.
+   */
+  cached
+  predicate ensuresEqEdge(Operand op, int k, IRBlock pred, IRBlock succ, boolean areEqual) {
+    exists(AbstractValue value |
+      compares_eq(this, op, k, areEqual, value) and
+      this.valueControlsEdge(pred, succ, value)
     )
   }
 
   /**
    * Holds if this condition controls `block`, meaning that `block` is only
-   * entered if the value of this condition is `testIsTrue`. This helper
+   * entered if the value of this condition is `v`. This helper
    * predicate does not necessarily hold for binary logical operations like
    * `&&` and `||`. See the detailed explanation on predicate `controls`.
    */
-  private predicate controlsBlock(IRBlock controlled, boolean testIsTrue) {
+  private predicate controlsBlock(IRBlock controlled, AbstractValue v) {
     not isUnreachedBlock(controlled) and
     //
     // For this block to control the block `controlled` with `testIsTrue` the
@@ -441,7 +663,7 @@ class IRGuardCondition extends Instruction {
     // that `this` strictly dominates `controlled` so that isn't necessary to check
     // directly.
     exists(IRBlock succ |
-      succ = this.getBranchSuccessor(testIsTrue) and
+      succ = this.getBranchSuccessor(v) and
       this.hasDominatingEdgeTo(succ) and
       succ.dominates(controlled)
     )
@@ -476,12 +698,14 @@ class IRGuardCondition extends Instruction {
   private IRBlock getBranchBlock() { result = branch.getBlock() }
 }
 
-private ConditionalBranchInstruction get_branch_for_condition(Instruction guard) {
-  result.getCondition() = guard
+private Instruction getBranchForCondition(Instruction guard) {
+  result.(ConditionalBranchInstruction).getCondition() = guard
   or
   exists(LogicalNotInstruction cond |
-    result = get_branch_for_condition(cond) and cond.getUnary() = guard
+    result = getBranchForCondition(cond) and cond.getUnary() = guard
   )
+  or
+  result.(SwitchInstruction).getExpression() = guard
 }
 
 /**
@@ -490,52 +714,98 @@ private ConditionalBranchInstruction get_branch_for_condition(Instruction guard)
  * Beware making mistaken logical implications here relating `areEqual` and `testIsTrue`.
  */
 private predicate compares_eq(
-  Instruction test, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue
+  Instruction test, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
 ) {
   /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
-  exists(boolean eq | simple_comparison_eq(test, left, right, k, eq) |
-    areEqual = true and testIsTrue = eq
+  exists(AbstractValue v | simple_comparison_eq(test, left, right, k, v) |
+    areEqual = true and value = v
     or
-    areEqual = false and testIsTrue = eq.booleanNot()
+    areEqual = false and value = v.getDualValue()
   )
   or
   // I think this is handled by forwarding in controlsBlock.
   //or
   //logical_comparison_eq(test, left, right, k, areEqual, testIsTrue)
   /* a == b + k => b == a - k */
-  exists(int mk | k = -mk | compares_eq(test, right, left, mk, areEqual, testIsTrue))
+  exists(int mk | k = -mk | compares_eq(test, right, left, mk, areEqual, value))
   or
-  complex_eq(test, left, right, k, areEqual, testIsTrue)
+  complex_eq(test, left, right, k, areEqual, value)
   or
   /* (x is true => (left == right + k)) => (!x is false => (left == right + k)) */
-  exists(boolean isFalse | testIsTrue = isFalse.booleanNot() |
-    compares_eq(test.(LogicalNotInstruction).getUnary(), left, right, k, areEqual, isFalse)
+  exists(AbstractValue dual | value = dual.getDualValue() |
+    compares_eq(test.(LogicalNotInstruction).getUnary(), left, right, k, areEqual, dual)
+  )
+}
+
+/** Holds if `op == k` is `areEqual` given that `test` is equal to `value`. */
+private predicate compares_eq(
+  Instruction test, Operand op, int k, boolean areEqual, AbstractValue value
+) {
+  /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
+  exists(AbstractValue v | simple_comparison_eq(test, op, k, v) |
+    areEqual = true and value = v
+    or
+    areEqual = false and value = v.getDualValue()
+  )
+  or
+  complex_eq(test, op, k, areEqual, value)
+  or
+  /* (x is true => (op == k)) => (!x is false => (op == k)) */
+  exists(AbstractValue dual | value = dual.getDualValue() |
+    compares_eq(test.(LogicalNotInstruction).getUnary(), op, k, areEqual, dual)
+  )
+  or
+  // ((test is `areEqual` => op == const + k2) and const == `k1`) =>
+  // test is `areEqual` => op == k1 + k2
+  exists(int k1, int k2, ConstantInstruction const |
+    compares_eq(test, op, const.getAUse(), k2, areEqual, value) and
+    int_value(const) = k1 and
+    k = k1 + k2
   )
 }
 
 /** Rearrange various simple comparisons into `left == right + k` form. */
 private predicate simple_comparison_eq(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual
+  CompareInstruction cmp, Operand left, Operand right, int k, AbstractValue value
 ) {
   left = cmp.getLeftOperand() and
   cmp instanceof CompareEQInstruction and
   right = cmp.getRightOperand() and
   k = 0 and
-  areEqual = true
+  value.(BooleanValue).getValue() = true
   or
   left = cmp.getLeftOperand() and
   cmp instanceof CompareNEInstruction and
   right = cmp.getRightOperand() and
   k = 0 and
-  areEqual = false
+  value.(BooleanValue).getValue() = false
+}
+
+/** Rearrange various simple comparisons into `op == k` form. */
+private predicate simple_comparison_eq(Instruction test, Operand op, int k, AbstractValue value) {
+  exists(SwitchInstruction switch, CaseEdge case |
+    test = switch.getExpression() and
+    op.getDef() = test and
+    case = value.(MatchValue).getCase() and
+    exists(switch.getSuccessor(case)) and
+    case.getValue().toInt() = k
+  )
 }
 
 private predicate complex_eq(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue
+  CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
 ) {
-  sub_eq(cmp, left, right, k, areEqual, testIsTrue)
+  sub_eq(cmp, left, right, k, areEqual, value)
   or
-  add_eq(cmp, left, right, k, areEqual, testIsTrue)
+  add_eq(cmp, left, right, k, areEqual, value)
+}
+
+private predicate complex_eq(
+  Instruction test, Operand op, int k, boolean areEqual, AbstractValue value
+) {
+  sub_eq(test, op, k, areEqual, value)
+  or
+  add_eq(test, op, k, areEqual, value)
 }
 
 /*
@@ -545,31 +815,46 @@ private predicate complex_eq(
 
 /** Holds if `left < right + k` evaluates to `isLt` given that test is `testIsTrue`. */
 private predicate compares_lt(
-  Instruction test, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue
+  Instruction test, Operand left, Operand right, int k, boolean isLt, AbstractValue value
 ) {
   /* In the simple case, the test is the comparison, so isLt = testIsTrue */
-  simple_comparison_lt(test, left, right, k) and isLt = true and testIsTrue = true
+  simple_comparison_lt(test, left, right, k) and
+  value.(BooleanValue).getValue() = isLt
   or
-  simple_comparison_lt(test, left, right, k) and isLt = false and testIsTrue = false
-  or
-  complex_lt(test, left, right, k, isLt, testIsTrue)
+  complex_lt(test, left, right, k, isLt, value)
   or
   /* (not (left < right + k)) => (left >= right + k) */
-  exists(boolean isGe | isLt = isGe.booleanNot() |
-    compares_ge(test, left, right, k, isGe, testIsTrue)
-  )
+  exists(boolean isGe | isLt = isGe.booleanNot() | compares_ge(test, left, right, k, isGe, value))
   or
   /* (x is true => (left < right + k)) => (!x is false => (left < right + k)) */
-  exists(boolean isFalse | testIsTrue = isFalse.booleanNot() |
-    compares_lt(test.(LogicalNotInstruction).getUnary(), left, right, k, isLt, isFalse)
+  exists(AbstractValue dual | value = dual.getDualValue() |
+    compares_lt(test.(LogicalNotInstruction).getUnary(), left, right, k, isLt, dual)
+  )
+}
+
+/** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
+private predicate compares_lt(Instruction test, Operand op, int k, boolean isLt, AbstractValue value) {
+  simple_comparison_lt(test, op, k, isLt, value)
+  or
+  complex_lt(test, op, k, isLt, value)
+  or
+  /* (x is true => (op < k)) => (!x is false => (op < k)) */
+  exists(AbstractValue dual | value = dual.getDualValue() |
+    compares_lt(test.(LogicalNotInstruction).getUnary(), op, k, isLt, dual)
+  )
+  or
+  exists(int k1, int k2, ConstantInstruction const |
+    compares_lt(test, op, const.getAUse(), k2, isLt, value) and
+    int_value(const) = k1 and
+    k = k1 + k2
   )
 }
 
 /** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */
 private predicate compares_ge(
-  Instruction test, Operand left, Operand right, int k, boolean isGe, boolean testIsTrue
+  Instruction test, Operand left, Operand right, int k, boolean isGe, AbstractValue value
 ) {
-  exists(int onemk | k = 1 - onemk | compares_lt(test, right, left, onemk, isGe, testIsTrue))
+  exists(int onemk | k = 1 - onemk | compares_lt(test, right, left, onemk, isGe, value))
 }
 
 /** Rearrange various simple comparisons into `left < right + k` form. */
@@ -595,55 +880,99 @@ private predicate simple_comparison_lt(CompareInstruction cmp, Operand left, Ope
   k = 1
 }
 
-private predicate complex_lt(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue
+/** Rearrange various simple comparisons into `op < k` form. */
+private predicate simple_comparison_lt(
+  Instruction test, Operand op, int k, boolean isLt, AbstractValue value
 ) {
-  sub_lt(cmp, left, right, k, isLt, testIsTrue)
+  exists(SwitchInstruction switch, CaseEdge case |
+    test = switch.getExpression() and
+    op.getDef() = test and
+    case = value.(MatchValue).getCase() and
+    exists(switch.getSuccessor(case)) and
+    case.getMaxValue() > case.getMinValue()
+  |
+    // op <= k => op < k - 1
+    isLt = true and
+    case.getMaxValue().toInt() = k - 1
+    or
+    isLt = false and
+    case.getMinValue().toInt() = k
+  )
+}
+
+private predicate complex_lt(
+  CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
+) {
+  sub_lt(cmp, left, right, k, isLt, value)
   or
-  add_lt(cmp, left, right, k, isLt, testIsTrue)
+  add_lt(cmp, left, right, k, isLt, value)
+}
+
+private predicate complex_lt(
+  Instruction test, Operand left, int k, boolean isLt, AbstractValue value
+) {
+  sub_lt(test, left, k, isLt, value)
+  or
+  add_lt(test, left, k, isLt, value)
 }
 
 // left - x < right + c => left < right + (c+x)
 // left < (right - x) + c => left < right + (c-x)
 private predicate sub_lt(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue
+  CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
 ) {
   exists(SubInstruction lhs, int c, int x |
-    compares_lt(cmp, lhs.getAUse(), right, c, isLt, testIsTrue) and
+    compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
     left = lhs.getLeftOperand() and
     x = int_value(lhs.getRight()) and
     k = c + x
   )
   or
   exists(SubInstruction rhs, int c, int x |
-    compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and
+    compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and
     right = rhs.getLeftOperand() and
     x = int_value(rhs.getRight()) and
     k = c - x
   )
   or
   exists(PointerSubInstruction lhs, int c, int x |
-    compares_lt(cmp, lhs.getAUse(), right, c, isLt, testIsTrue) and
+    compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
     left = lhs.getLeftOperand() and
     x = int_value(lhs.getRight()) and
     k = c + x
   )
   or
   exists(PointerSubInstruction rhs, int c, int x |
-    compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and
+    compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and
     right = rhs.getLeftOperand() and
     x = int_value(rhs.getRight()) and
     k = c - x
   )
 }
 
+private predicate sub_lt(Instruction test, Operand left, int k, boolean isLt, AbstractValue value) {
+  exists(SubInstruction lhs, int c, int x |
+    compares_lt(test, lhs.getAUse(), c, isLt, value) and
+    left = lhs.getLeftOperand() and
+    x = int_value(lhs.getRight()) and
+    k = c + x
+  )
+  or
+  exists(PointerSubInstruction lhs, int c, int x |
+    compares_lt(test, lhs.getAUse(), c, isLt, value) and
+    left = lhs.getLeftOperand() and
+    x = int_value(lhs.getRight()) and
+    k = c + x
+  )
+}
+
 // left + x < right + c => left < right + (c-x)
 // left < (right + x) + c => left < right + (c+x)
 private predicate add_lt(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue
+  CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
 ) {
   exists(AddInstruction lhs, int c, int x |
-    compares_lt(cmp, lhs.getAUse(), right, c, isLt, testIsTrue) and
+    compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
     (
       left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
       or
@@ -653,7 +982,7 @@ private predicate add_lt(
   )
   or
   exists(AddInstruction rhs, int c, int x |
-    compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and
+    compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and
     (
       right = rhs.getLeftOperand() and x = int_value(rhs.getRight())
       or
@@ -663,7 +992,7 @@ private predicate add_lt(
   )
   or
   exists(PointerAddInstruction lhs, int c, int x |
-    compares_lt(cmp, lhs.getAUse(), right, c, isLt, testIsTrue) and
+    compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
     (
       left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
       or
@@ -673,7 +1002,7 @@ private predicate add_lt(
   )
   or
   exists(PointerAddInstruction rhs, int c, int x |
-    compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and
+    compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and
     (
       right = rhs.getLeftOperand() and x = int_value(rhs.getRight())
       or
@@ -683,47 +1012,86 @@ private predicate add_lt(
   )
 }
 
+private predicate add_lt(Instruction test, Operand left, int k, boolean isLt, AbstractValue value) {
+  exists(AddInstruction lhs, int c, int x |
+    compares_lt(test, lhs.getAUse(), c, isLt, value) and
+    (
+      left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
+      or
+      left = lhs.getRightOperand() and x = int_value(lhs.getLeft())
+    ) and
+    k = c - x
+  )
+  or
+  exists(PointerAddInstruction lhs, int c, int x |
+    compares_lt(test, lhs.getAUse(), c, isLt, value) and
+    (
+      left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
+      or
+      left = lhs.getRightOperand() and x = int_value(lhs.getLeft())
+    ) and
+    k = c - x
+  )
+}
+
 // left - x == right + c => left == right + (c+x)
 // left == (right - x) + c => left == right + (c-x)
 private predicate sub_eq(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue
+  CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
 ) {
   exists(SubInstruction lhs, int c, int x |
-    compares_eq(cmp, lhs.getAUse(), right, c, areEqual, testIsTrue) and
+    compares_eq(cmp, lhs.getAUse(), right, c, areEqual, value) and
     left = lhs.getLeftOperand() and
     x = int_value(lhs.getRight()) and
     k = c + x
   )
   or
   exists(SubInstruction rhs, int c, int x |
-    compares_eq(cmp, left, rhs.getAUse(), c, areEqual, testIsTrue) and
+    compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and
     right = rhs.getLeftOperand() and
     x = int_value(rhs.getRight()) and
     k = c - x
   )
   or
   exists(PointerSubInstruction lhs, int c, int x |
-    compares_eq(cmp, lhs.getAUse(), right, c, areEqual, testIsTrue) and
+    compares_eq(cmp, lhs.getAUse(), right, c, areEqual, value) and
     left = lhs.getLeftOperand() and
     x = int_value(lhs.getRight()) and
     k = c + x
   )
   or
   exists(PointerSubInstruction rhs, int c, int x |
-    compares_eq(cmp, left, rhs.getAUse(), c, areEqual, testIsTrue) and
+    compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and
     right = rhs.getLeftOperand() and
     x = int_value(rhs.getRight()) and
     k = c - x
   )
 }
 
+// op - x == c => op == (c+x)
+private predicate sub_eq(Instruction test, Operand op, int k, boolean areEqual, AbstractValue value) {
+  exists(SubInstruction sub, int c, int x |
+    compares_eq(test, sub.getAUse(), c, areEqual, value) and
+    op = sub.getLeftOperand() and
+    x = int_value(sub.getRight()) and
+    k = c + x
+  )
+  or
+  exists(PointerSubInstruction sub, int c, int x |
+    compares_eq(test, sub.getAUse(), c, areEqual, value) and
+    op = sub.getLeftOperand() and
+    x = int_value(sub.getRight()) and
+    k = c + x
+  )
+}
+
 // left + x == right + c => left == right + (c-x)
 // left == (right + x) + c => left == right + (c+x)
 private predicate add_eq(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue
+  CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
 ) {
   exists(AddInstruction lhs, int c, int x |
-    compares_eq(cmp, lhs.getAUse(), right, c, areEqual, testIsTrue) and
+    compares_eq(cmp, lhs.getAUse(), right, c, areEqual, value) and
     (
       left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
       or
@@ -733,7 +1101,7 @@ private predicate add_eq(
   )
   or
   exists(AddInstruction rhs, int c, int x |
-    compares_eq(cmp, left, rhs.getAUse(), c, areEqual, testIsTrue) and
+    compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and
     (
       right = rhs.getLeftOperand() and x = int_value(rhs.getRight())
       or
@@ -743,7 +1111,7 @@ private predicate add_eq(
   )
   or
   exists(PointerAddInstruction lhs, int c, int x |
-    compares_eq(cmp, lhs.getAUse(), right, c, areEqual, testIsTrue) and
+    compares_eq(cmp, lhs.getAUse(), right, c, areEqual, value) and
     (
       left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
       or
@@ -753,7 +1121,7 @@ private predicate add_eq(
   )
   or
   exists(PointerAddInstruction rhs, int c, int x |
-    compares_eq(cmp, left, rhs.getAUse(), c, areEqual, testIsTrue) and
+    compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and
     (
       right = rhs.getLeftOperand() and x = int_value(rhs.getRight())
       or
@@ -763,5 +1131,39 @@ private predicate add_eq(
   )
 }
 
+// left + x == right + c => left == right + (c-x)
+private predicate add_eq(
+  Instruction test, Operand left, int k, boolean areEqual, AbstractValue value
+) {
+  exists(AddInstruction lhs, int c, int x |
+    compares_eq(test, lhs.getAUse(), c, areEqual, value) and
+    (
+      left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
+      or
+      left = lhs.getRightOperand() and x = int_value(lhs.getLeft())
+    ) and
+    k = c - x
+  )
+  or
+  exists(PointerAddInstruction lhs, int c, int x |
+    compares_eq(test, lhs.getAUse(), c, areEqual, value) and
+    (
+      left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
+      or
+      left = lhs.getRightOperand() and x = int_value(lhs.getLeft())
+    ) and
+    k = c - x
+  )
+}
+
+private class IntegerOrPointerConstantInstruction extends ConstantInstruction {
+  IntegerOrPointerConstantInstruction() {
+    this instanceof IntegerConstantInstruction or
+    this instanceof PointerConstantInstruction
+  }
+}
+
 /** The int value of integer constant expression. */
-private int int_value(Instruction i) { result = i.(IntegerConstantInstruction).getValue().toInt() }
+private int int_value(Instruction i) {
+  result = i.(IntegerOrPointerConstantInstruction).getValue().toInt()
+}

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

@@ -28,6 +28,6 @@ import cpp
 deprecated module DataFlow {
   private import semmle.code.cpp.dataflow.internal.DataFlowImplSpecific
   private import codeql.dataflow.DataFlow
-  import DataFlowMake<CppOldDataFlow>
+  import DataFlowMake<Location, CppOldDataFlow>
   import semmle.code.cpp.dataflow.internal.DataFlowImpl1
 }

cpp/ql/lib/semmle/code/cpp/dataflow/ExternalFlow.qll

@@ -0,0 +1,556 @@
+/**
+ * INTERNAL use only. This is an experimental API subject to change without notice.
+ *
+ * Provides classes and predicates for dealing with flow models specified in CSV format.
+ *
+ * The CSV specification has the following columns:
+ * - Sources:
+ *   `namespace; type; subtypes; name; signature; ext; output; kind`
+ * - Sinks:
+ *   `namespace; type; subtypes; name; signature; ext; input; kind`
+ * - Summaries:
+ *   `namespace; type; subtypes; name; signature; ext; input; output; kind`
+ *
+ * The interpretation of a row is similar to API-graphs with a left-to-right
+ * reading.
+ * 1. The `namespace` column selects a namespace.
+ * 2. The `type` column selects a type within that namespace.
+ * 3. The `subtypes` is a boolean that indicates whether to jump to an
+ *    arbitrary subtype of that type. Set this to `false` if leaving the `type`
+ *    blank (for example, a free function).
+ * 4. The `name` column optionally selects a specific named member of the type.
+ * 5. The `signature` column optionally restricts the named member. If
+ *    `signature` is blank then no such filtering is done. The format of the
+ *    signature is a comma-separated list of types enclosed in parentheses. The
+ *    types can be short names or fully qualified names (mixing these two options
+ *    is not allowed within a single signature).
+ * 6. The `ext` column specifies additional API-graph-like edges. Currently
+ *    there is only one valid value: "".
+ * 7. The `input` column specifies how data enters the element selected by the
+ *    first 6 columns, and the `output` column specifies how data leaves the
+ *    element selected by the first 6 columns. An `input` can be either:
+ *    - "": Selects a write to the selected element in case this is a field.
+ *    - "Argument[n]": Selects an argument in a call to the selected element.
+ *      The arguments are zero-indexed, and `-1` specifies the qualifier object,
+ *      that is, `*this`.
+ *      - one or more "*" can be added in front of the argument index to indicate
+ *        indirection, for example, `Argument[*0]` indicates the first indirection
+ *        of the 0th argument.
+ *      - `n1..n2` syntax can be used to indicate a range of arguments, inclusive
+ *        at both ends. One or more "*"s can be added in front of the whole range
+ *        to indicate that every argument in the range is indirect, for example
+ *        `*0..1` is the first indirection of both arguments 0 and 1.
+ *    - "ReturnValue": Selects a value being returned by the selected element.
+ *      One or more "*" can be added as an argument to indicate indirection, for
+ *      example, "ReturnValue[*]" indicates the first indirection of the return
+ *      value.
+ *
+ *    An `output` can be either:
+ *    - "": Selects a read of a selected field.
+ *    - "Argument[n]": Selects the post-update value of an argument in a call to
+ *      the selected element. That is, the value of the argument after the call
+ *      returns. The arguments are zero-indexed, and `-1` specifies the qualifier
+ *      object, that is, `*this`.
+ *      - one or more "*" can be added in front of the argument index to indicate
+ *        indirection, for example, `Argument[*0]` indicates the first indirection
+ *        of the 0th argument.
+ *      - `n1..n2` syntax can be used to indicate a range of arguments, inclusive
+ *        at both ends. One or more "*"s can be added in front of the whole range
+ *        to indicate that every argument in the range is indirect, for example
+ *        `*0..1` is the first indirection of both arguments 0 and 1.
+ *    - "Parameter[n]": Selects the value of a parameter of the selected element.
+ *      The syntax is the same as for "Argument", for example "Parameter[0]",
+ *      "Parameter[*0]", "Parameter[0..2]" etc.
+ *    - "ReturnValue": Selects a value being returned by the selected element.
+ *      One or more "*" can be added as an argument to indicate indirection, for
+ *      example, "ReturnValue[*]" indicates the first indirection of the return
+ *      value.
+ * 8. The `kind` column is a tag that can be referenced from QL to determine to
+ *    which classes the interpreted elements should be added. For example, for
+ *    sources "remote" indicates a default remote flow source, and for summaries
+ *    "taint" indicates a default additional taint step and "value" indicates a
+ *    globally applicable value-preserving step.
+ */
+
+import cpp
+private import new.DataFlow
+private import internal.FlowSummaryImpl
+private import internal.FlowSummaryImpl::Public
+private import internal.FlowSummaryImpl::Private
+private import internal.FlowSummaryImpl::Private::External
+private import codeql.mad.ModelValidation as SharedModelVal
+private import codeql.util.Unit
+
+/**
+ * A unit class for adding additional source model rows.
+ *
+ * Extend this class to add additional source definitions.
+ */
+class SourceModelCsv extends Unit {
+  /** Holds if `row` specifies a source definition. */
+  abstract predicate row(string row);
+}
+
+/**
+ * A unit class for adding additional sink model rows.
+ *
+ * Extend this class to add additional sink definitions.
+ */
+class SinkModelCsv extends Unit {
+  /** Holds if `row` specifies a sink definition. */
+  abstract predicate row(string row);
+}
+
+/**
+ * A unit class for adding additional summary model rows.
+ *
+ * Extend this class to add additional flow summary definitions.
+ */
+class SummaryModelCsv extends Unit {
+  /** Holds if `row` specifies a summary definition. */
+  abstract predicate row(string row);
+}
+
+/** Holds if `row` is a source model. */
+predicate sourceModel(string row) { any(SourceModelCsv s).row(row) }
+
+/** Holds if `row` is a sink model. */
+predicate sinkModel(string row) { any(SinkModelCsv s).row(row) }
+
+/** Holds if `row` is a summary model. */
+predicate summaryModel(string row) { any(SummaryModelCsv s).row(row) }
+
+/** Holds if a source model exists for the given parameters. */
+predicate sourceModel(
+  string namespace, string type, boolean subtypes, string name, string signature, string ext,
+  string output, string kind, string provenance
+) {
+  exists(string row |
+    sourceModel(row) and
+    row.splitAt(";", 0) = namespace and
+    row.splitAt(";", 1) = type and
+    row.splitAt(";", 2) = subtypes.toString() and
+    subtypes = [true, false] and
+    row.splitAt(";", 3) = name and
+    row.splitAt(";", 4) = signature and
+    row.splitAt(";", 5) = ext and
+    row.splitAt(";", 6) = output and
+    row.splitAt(";", 7) = kind
+  ) and
+  provenance = "manual"
+}
+
+/** Holds if a sink model exists for the given parameters. */
+predicate sinkModel(
+  string namespace, string type, boolean subtypes, string name, string signature, string ext,
+  string input, string kind, string provenance
+) {
+  exists(string row |
+    sinkModel(row) and
+    row.splitAt(";", 0) = namespace and
+    row.splitAt(";", 1) = type and
+    row.splitAt(";", 2) = subtypes.toString() and
+    subtypes = [true, false] and
+    row.splitAt(";", 3) = name and
+    row.splitAt(";", 4) = signature and
+    row.splitAt(";", 5) = ext and
+    row.splitAt(";", 6) = input and
+    row.splitAt(";", 7) = kind
+  ) and
+  provenance = "manual"
+}
+
+/** Holds if a summary model exists for the given parameters. */
+predicate summaryModel(
+  string namespace, string type, boolean subtypes, string name, string signature, string ext,
+  string input, string output, string kind, string provenance
+) {
+  exists(string row |
+    summaryModel(row) and
+    row.splitAt(";", 0) = namespace and
+    row.splitAt(";", 1) = type and
+    row.splitAt(";", 2) = subtypes.toString() and
+    subtypes = [true, false] and
+    row.splitAt(";", 3) = name and
+    row.splitAt(";", 4) = signature and
+    row.splitAt(";", 5) = ext and
+    row.splitAt(";", 6) = input and
+    row.splitAt(";", 7) = output and
+    row.splitAt(";", 8) = kind
+  ) and
+  provenance = "manual"
+}
+
+private predicate relevantNamespace(string namespace) {
+  sourceModel(namespace, _, _, _, _, _, _, _, _) or
+  sinkModel(namespace, _, _, _, _, _, _, _, _) or
+  summaryModel(namespace, _, _, _, _, _, _, _, _, _)
+}
+
+private predicate namespaceLink(string shortns, string longns) {
+  relevantNamespace(shortns) and
+  relevantNamespace(longns) and
+  longns.prefix(longns.indexOf("::")) = shortns
+}
+
+private predicate canonicalNamespace(string namespace) {
+  relevantNamespace(namespace) and not namespaceLink(_, namespace)
+}
+
+private predicate canonicalNamespaceLink(string namespace, string subns) {
+  canonicalNamespace(namespace) and
+  (subns = namespace or namespaceLink(namespace, subns))
+}
+
+/**
+ * Holds if CSV framework coverage of `namespace` is `n` api endpoints of the
+ * kind `(kind, part)`.
+ */
+predicate modelCoverage(string namespace, int namespaces, string kind, string part, int n) {
+  namespaces = strictcount(string subns | canonicalNamespaceLink(namespace, subns)) and
+  (
+    part = "source" and
+    n =
+      strictcount(string subns, string type, boolean subtypes, string name, string signature,
+        string ext, string output, string provenance |
+        canonicalNamespaceLink(namespace, subns) and
+        sourceModel(subns, type, subtypes, name, signature, ext, output, kind, provenance)
+      )
+    or
+    part = "sink" and
+    n =
+      strictcount(string subns, string type, boolean subtypes, string name, string signature,
+        string ext, string input, string provenance |
+        canonicalNamespaceLink(namespace, subns) and
+        sinkModel(subns, type, subtypes, name, signature, ext, input, kind, provenance)
+      )
+    or
+    part = "summary" and
+    n =
+      strictcount(string subns, string type, boolean subtypes, string name, string signature,
+        string ext, string input, string output, string provenance |
+        canonicalNamespaceLink(namespace, subns) and
+        summaryModel(subns, type, subtypes, name, signature, ext, input, output, kind, provenance)
+      )
+  )
+}
+
+/** Provides a query predicate to check the CSV data for validation errors. */
+module CsvValidation {
+  private string getInvalidModelInput() {
+    exists(string pred, AccessPath input, string part |
+      sinkModel(_, _, _, _, _, _, input, _, _) and pred = "sink"
+      or
+      summaryModel(_, _, _, _, _, _, input, _, _, _) and pred = "summary"
+    |
+      (
+        invalidSpecComponent(input, part) and
+        not part = "" and
+        not (part = "Argument" and pred = "sink") and
+        not parseArg(part, _)
+        or
+        part = input.getToken(_) and
+        parseParam(part, _)
+      ) and
+      result = "Unrecognized input specification \"" + part + "\" in " + pred + " model."
+    )
+  }
+
+  private string getInvalidModelOutput() {
+    exists(string pred, string output, string part |
+      sourceModel(_, _, _, _, _, _, output, _, _) and pred = "source"
+      or
+      summaryModel(_, _, _, _, _, _, _, output, _, _) and pred = "summary"
+    |
+      invalidSpecComponent(output, part) and
+      not part = "" and
+      not (part = ["Argument", "Parameter"] and pred = "source") and
+      result = "Unrecognized output specification \"" + part + "\" in " + pred + " model."
+    )
+  }
+
+  private module KindValConfig implements SharedModelVal::KindValidationConfigSig {
+    predicate summaryKind(string kind) { summaryModel(_, _, _, _, _, _, _, _, kind, _) }
+
+    predicate sinkKind(string kind) { sinkModel(_, _, _, _, _, _, _, kind, _) }
+
+    predicate sourceKind(string kind) { sourceModel(_, _, _, _, _, _, _, kind, _) }
+  }
+
+  private module KindVal = SharedModelVal::KindValidation<KindValConfig>;
+
+  private string getInvalidModelSubtype() {
+    exists(string pred, string row |
+      sourceModel(row) and pred = "source"
+      or
+      sinkModel(row) and pred = "sink"
+      or
+      summaryModel(row) and pred = "summary"
+    |
+      exists(string b |
+        b = row.splitAt(";", 2) and
+        not b = ["true", "false"] and
+        result = "Invalid boolean \"" + b + "\" in " + pred + " model."
+      )
+    )
+  }
+
+  private string getInvalidModelColumnCount() {
+    exists(string pred, string row, int expect |
+      sourceModel(row) and expect = 8 and pred = "source"
+      or
+      sinkModel(row) and expect = 8 and pred = "sink"
+      or
+      summaryModel(row) and expect = 9 and pred = "summary"
+    |
+      exists(int cols |
+        cols = 1 + max(int n | exists(row.splitAt(";", n))) and
+        cols != expect and
+        result =
+          "Wrong number of columns in " + pred + " model row, expected " + expect + ", got " + cols +
+            "."
+      )
+    )
+  }
+
+  private string getInvalidModelSignature() {
+    exists(string pred, string namespace, string type, string name, string signature, string ext |
+      sourceModel(namespace, type, _, name, signature, ext, _, _, _) and pred = "source"
+      or
+      sinkModel(namespace, type, _, name, signature, ext, _, _, _) and pred = "sink"
+      or
+      summaryModel(namespace, type, _, name, signature, ext, _, _, _, _) and pred = "summary"
+    |
+      not namespace.regexpMatch("[a-zA-Z0-9_\\.]+") and
+      result = "Dubious namespace \"" + namespace + "\" in " + pred + " model."
+      or
+      not type.regexpMatch("[a-zA-Z0-9_<>,\\+]+") and
+      result = "Dubious type \"" + type + "\" in " + pred + " model."
+      or
+      not name.regexpMatch("[a-zA-Z0-9_<>,]*") and
+      result = "Dubious member name \"" + name + "\" in " + pred + " model."
+      or
+      not signature.regexpMatch("|\\([a-zA-Z0-9_<>\\.\\+\\*,\\[\\]]*\\)") and
+      result = "Dubious signature \"" + signature + "\" in " + pred + " model."
+      or
+      not ext.regexpMatch("|Attribute") and
+      result = "Unrecognized extra API graph element \"" + ext + "\" in " + pred + " model."
+    )
+  }
+
+  /** Holds if some row in a CSV-based flow model appears to contain typos. */
+  query predicate invalidModelRow(string msg) {
+    msg =
+      [
+        getInvalidModelSignature(), getInvalidModelInput(), getInvalidModelOutput(),
+        getInvalidModelSubtype(), getInvalidModelColumnCount(), KindVal::getInvalidModelKind()
+      ]
+  }
+}
+
+private predicate elementSpec(
+  string namespace, string type, boolean subtypes, string name, string signature, string ext
+) {
+  sourceModel(namespace, type, subtypes, name, signature, ext, _, _, _) or
+  sinkModel(namespace, type, subtypes, name, signature, ext, _, _, _) or
+  summaryModel(namespace, type, subtypes, name, signature, ext, _, _, _, _)
+}
+
+private string paramsStringPart(Function c, int i) {
+  i = -1 and result = "(" and exists(c)
+  or
+  exists(int n, string p | c.getParameter(n).getType().toString() = p |
+    i = 2 * n and result = p
+    or
+    i = 2 * n - 1 and result = "," and n != 0
+  )
+  or
+  i = 2 * c.getNumberOfParameters() and result = ")"
+}
+
+/**
+ * Gets a parenthesized string containing all parameter types of this callable, separated by a comma.
+ *
+ * Returns the empty string if the callable has no parameters.
+ * Parameter types are represented by their type erasure.
+ */
+cached
+private string paramsString(Function c) {
+  result = concat(int i | | paramsStringPart(c, i) order by i)
+}
+
+bindingset[func]
+private predicate matchesSignature(Function func, string signature) {
+  signature = "" or
+  paramsString(func) = signature
+}
+
+/**
+ * Gets the element in module `namespace` that satisfies the following properties:
+ * 1. If the element is a member of a class-like type, then the class-like type has name `type`
+ * 2. If `subtypes = true` and the element is a member of a class-like type, then overrides of the element
+ *    are also returned.
+ * 3. The element has name `name`
+ * 4. If `signature` is non-empty, then the element has a list of parameter types described by `signature`.
+ *
+ * NOTE: `namespace` is currently not used (since we don't properly extract modules yet).
+ */
+pragma[nomagic]
+private Element interpretElement0(
+  string namespace, string type, boolean subtypes, string name, string signature
+) {
+  elementSpec(namespace, type, subtypes, name, signature, _) and
+  (
+    // Non-member functions
+    exists(Function func |
+      func.hasQualifiedName(namespace, name) and
+      type = "" and
+      matchesSignature(func, signature) and
+      subtypes = false and
+      not exists(func.getDeclaringType()) and
+      result = func
+    )
+    or
+    // Member functions
+    exists(Class namedClass, Class classWithMethod, Function method |
+      classWithMethod = method.getClassAndName(name) and
+      namedClass.hasQualifiedName(namespace, type) and
+      matchesSignature(method, signature) and
+      result = method
+    |
+      // member declared in the named type or a subtype of it
+      subtypes = true and
+      classWithMethod = namedClass.getADerivedClass*()
+      or
+      // member declared directly in the named type
+      subtypes = false and
+      classWithMethod = namedClass
+    )
+    or
+    // Member variables
+    signature = "" and
+    exists(Class namedClass, Class classWithMember, MemberVariable member |
+      member.getName() = name and
+      member = classWithMember.getAMember() and
+      namedClass.hasQualifiedName(namespace, type) and
+      result = member
+    |
+      // field declared in the named type or a subtype of it (or an extension of any)
+      subtypes = true and
+      classWithMember = namedClass.getADerivedClass*()
+      or
+      // field declared directly in the named type (or an extension of it)
+      subtypes = false and
+      classWithMember = namedClass
+    )
+    or
+    // Global or namespace variables
+    signature = "" and
+    type = "" and
+    subtypes = false and
+    result = any(GlobalOrNamespaceVariable v | v.hasQualifiedName(namespace, name))
+  )
+}
+
+/** Gets the source/sink/summary element corresponding to the supplied parameters. */
+Element interpretElement(
+  string namespace, string type, boolean subtypes, string name, string signature, string ext
+) {
+  elementSpec(namespace, type, subtypes, name, signature, ext) and
+  exists(Element e | e = interpretElement0(namespace, type, subtypes, name, signature) |
+    ext = "" and result = e
+  )
+}
+
+cached
+private module Cached {
+  /**
+   * Holds if `node` is specified as a source with the given kind in a CSV flow
+   * model.
+   */
+  cached
+  predicate sourceNode(DataFlow::Node node, string kind) {
+    exists(SourceSinkInterpretationInput::InterpretNode n |
+      isSourceNode(n, kind, _) and n.asNode() = node // TODO
+    )
+  }
+
+  /**
+   * Holds if `node` is specified as a sink with the given kind in a CSV flow
+   * model.
+   */
+  cached
+  predicate sinkNode(DataFlow::Node node, string kind) {
+    exists(SourceSinkInterpretationInput::InterpretNode n |
+      isSinkNode(n, kind, _) and n.asNode() = node // TODO
+    )
+  }
+}
+
+import Cached
+
+private predicate interpretSummary(
+  Function f, string input, string output, string kind, string provenance
+) {
+  exists(
+    string namespace, string type, boolean subtypes, string name, string signature, string ext
+  |
+    summaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, provenance) and
+    f = interpretElement(namespace, type, subtypes, name, signature, ext)
+  )
+}
+
+// adapter class for converting Mad summaries to `SummarizedCallable`s
+private class SummarizedCallableAdapter extends SummarizedCallable {
+  SummarizedCallableAdapter() { interpretSummary(this, _, _, _, _) }
+
+  private predicate relevantSummaryElementManual(string input, string output, string kind) {
+    exists(Provenance provenance |
+      interpretSummary(this, input, output, kind, provenance) and
+      provenance.isManual()
+    )
+  }
+
+  private predicate relevantSummaryElementGenerated(string input, string output, string kind) {
+    exists(Provenance provenance |
+      interpretSummary(this, input, output, kind, provenance) and
+      provenance.isGenerated()
+    )
+  }
+
+  override predicate propagatesFlow(
+    string input, string output, boolean preservesValue, string model
+  ) {
+    exists(string kind |
+      this.relevantSummaryElementManual(input, output, kind)
+      or
+      not this.relevantSummaryElementManual(_, _, _) and
+      this.relevantSummaryElementGenerated(input, output, kind)
+    |
+      if kind = "value" then preservesValue = true else preservesValue = false
+    ) and
+    model = "" // TODO
+  }
+
+  override predicate hasProvenance(Provenance provenance) {
+    interpretSummary(this, _, _, _, provenance)
+  }
+}
+
+// adapter class for converting Mad neutrals to `NeutralCallable`s
+private class NeutralCallableAdapter extends NeutralCallable {
+  string kind;
+  string provenance_;
+
+  NeutralCallableAdapter() {
+    // Neutral models have not been implemented for CPP.
+    none() and
+    exists(this) and
+    exists(kind) and
+    exists(provenance_)
+  }
+
+  override string getKind() { result = kind }
+
+  override predicate hasProvenance(Provenance provenance) { provenance = provenance_ }
+}

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

@@ -29,6 +29,6 @@ deprecated module TaintTracking {
   private import semmle.code.cpp.dataflow.internal.DataFlowImplSpecific
   private import semmle.code.cpp.dataflow.internal.TaintTrackingImplSpecific
   private import codeql.dataflow.TaintTracking
-  import TaintFlowMake<CppOldDataFlow, CppOldTaintTracking>
+  import TaintFlowMake<Location, CppOldDataFlow, CppOldTaintTracking>
   import semmle.code.cpp.dataflow.internal.tainttracking1.TaintTrackingImpl
 }

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

@@ -2,6 +2,7 @@
  * DEPRECATED: Use `semmle.code.cpp.dataflow.new.DataFlow` instead.
  */
 
+private import semmle.code.cpp.Location
 private import DataFlowImplSpecific
 private import codeql.dataflow.internal.DataFlowImpl
-import MakeImpl<CppOldDataFlow>
+import MakeImpl<Location, CppOldDataFlow>

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

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
@@ -285,6 +286,8 @@ deprecated private module Config implements FullStateConfigSig {
 
   int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
 
+  int accessPathLimit() { result = 5 }
+
   FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }
 
   predicate sourceGrouping(Node source, string sourceGroup) {

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

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
@@ -285,6 +286,8 @@ deprecated private module Config implements FullStateConfigSig {
 
   int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
 
+  int accessPathLimit() { result = 5 }
+
   FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }
 
   predicate sourceGrouping(Node source, string sourceGroup) {

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

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
@@ -285,6 +286,8 @@ deprecated private module Config implements FullStateConfigSig {
 
   int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
 
+  int accessPathLimit() { result = 5 }
+
   FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }
 
   predicate sourceGrouping(Node source, string sourceGroup) {

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

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
@@ -285,6 +286,8 @@ deprecated private module Config implements FullStateConfigSig {
 
   int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
 
+  int accessPathLimit() { result = 5 }
+
   FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }
 
   predicate sourceGrouping(Node source, string sourceGroup) {

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

@@ -2,6 +2,7 @@
  * DEPRECATED: Use `semmle.code.cpp.dataflow.new.DataFlow` instead.
  */
 
+private import semmle.code.cpp.Location
 private import DataFlowImplSpecific
 private import codeql.dataflow.internal.DataFlowImplCommon
-import MakeImplCommon<CppOldDataFlow>
+import MakeImplCommon<Location, CppOldDataFlow>

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

@@ -10,7 +10,7 @@ private import DataFlowImplSpecific
 private import TaintTrackingImplSpecific
 private import codeql.dataflow.internal.DataFlowImplConsistency
 
-private module Input implements InputSig<CppOldDataFlow> {
+private module Input implements InputSig<Location, CppOldDataFlow> {
   predicate argHasPostUpdateExclude(Private::ArgumentNode n) {
     // Is the null pointer (or something that's not really a pointer)
     exists(n.asExpr().getValue())
@@ -26,4 +26,4 @@ private module Input implements InputSig<CppOldDataFlow> {
   }
 }
 
-module Consistency = MakeConsistency<CppOldDataFlow, CppOldTaintTracking, Input>;
+module Consistency = MakeConsistency<Location, CppOldDataFlow, CppOldTaintTracking, Input>;

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

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
@@ -285,6 +286,8 @@ deprecated private module Config implements FullStateConfigSig {
 
   int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
 
+  int accessPathLimit() { result = 5 }
+
   FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }
 
   predicate sourceGrouping(Node source, string sourceGroup) {

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

@@ -4,6 +4,7 @@
  * Provides C++-specific definitions for use in the data flow library.
  */
 
+private import semmle.code.cpp.Location
 private import codeql.dataflow.DataFlow
 
 module Private {
@@ -15,7 +16,7 @@ module Public {
   import DataFlowUtil
 }
 
-module CppOldDataFlow implements InputSig {
+module CppOldDataFlow implements InputSig<Location> {
   import Private
   import Public
 

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

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

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

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

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

@@ -0,0 +1,271 @@
+/**
+ * Provides classes and predicates for defining flow summaries.
+ */
+
+private import cpp as Cpp
+private import codeql.dataflow.internal.FlowSummaryImpl
+private import codeql.dataflow.internal.AccessPathSyntax as AccessPath
+private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
+private import semmle.code.cpp.ir.dataflow.internal.DataFlowUtil
+private import semmle.code.cpp.ir.dataflow.internal.DataFlowImplSpecific as DataFlowImplSpecific
+private import semmle.code.cpp.dataflow.ExternalFlow
+private import semmle.code.cpp.ir.IR
+
+module Input implements InputSig<Location, DataFlowImplSpecific::CppDataFlow> {
+  class SummarizedCallableBase = Function;
+
+  ArgumentPosition callbackSelfParameterPosition() { result = TDirectPosition(-1) }
+
+  ReturnKind getStandardReturnValueKind() { result.(NormalReturnKind).getIndirectionIndex() = 0 }
+
+  string encodeParameterPosition(ParameterPosition pos) { result = pos.toString() }
+
+  string encodeArgumentPosition(ArgumentPosition pos) { result = pos.toString() }
+
+  string encodeReturn(ReturnKind rk, string arg) {
+    rk != getStandardReturnValueKind() and
+    result = "ReturnValue" and
+    arg = repeatStars(rk.(NormalReturnKind).getIndirectionIndex())
+  }
+
+  string encodeContent(ContentSet cs, string arg) {
+    exists(FieldContent c |
+      cs.isSingleton(c) and
+      // FieldContent indices have 0 for the address, 1 for content, so we need to subtract one.
+      result = "Field" and
+      arg = repeatStars(c.getIndirectionIndex() - 1) + c.getField().getName()
+    )
+  }
+
+  string encodeWithoutContent(ContentSet c, string arg) {
+    // used for type tracking, not currently used in C/C++.
+    result = "WithoutContent" + c and arg = ""
+  }
+
+  string encodeWithContent(ContentSet c, string arg) {
+    // used for type tracking, not currently used in C/C++.
+    result = "WithContent" + c and arg = ""
+  }
+
+  /**
+   * Decodes an argument / parameter position string, for example the `0` in `Argument[0]`.
+   * Supports ranges (`Argument[x..y]`), qualifiers (`Argument[-1]`), indirections
+   * (`Argument[*x]`) and combinations (such as `Argument[**0..1]`).
+   */
+  bindingset[argString]
+  private TPosition decodePosition(string argString) {
+    exists(int indirection, string posString, int pos |
+      argString = repeatStars(indirection) + posString and
+      pos = AccessPath::parseInt(posString) and
+      (
+        pos >= 0 and indirection = 0 and result = TDirectPosition(pos)
+        or
+        pos >= 0 and indirection > 0 and result = TIndirectionPosition(pos, indirection)
+        or
+        // `Argument[-1]` / `Parameter[-1]` is the qualifier object `*this`, not the `this` pointer itself.
+        pos = -1 and result = TIndirectionPosition(pos, indirection + 1)
+      )
+    )
+  }
+
+  bindingset[token]
+  ParameterPosition decodeUnknownParameterPosition(AccessPath::AccessPathTokenBase token) {
+    token.getName() = "Argument" and
+    result = decodePosition(token.getAnArgument())
+  }
+
+  bindingset[token]
+  ArgumentPosition decodeUnknownArgumentPosition(AccessPath::AccessPathTokenBase token) {
+    token.getName() = "Parameter" and
+    result = decodePosition(token.getAnArgument())
+  }
+
+  bindingset[token]
+  ContentSet decodeUnknownContent(AccessPath::AccessPathTokenBase token) {
+    // field content (no indirection support)
+    exists(FieldContent c |
+      result.isSingleton(c) and
+      token.getName() = c.getField().getName() and
+      not exists(token.getArgumentList()) and
+      c.getIndirectionIndex() = 1
+    )
+    or
+    // field content (with indirection support)
+    exists(FieldContent c |
+      result.isSingleton(c) and
+      token.getName() = c.getField().getName() and
+      // FieldContent indices have 0 for the address, 1 for content, so we need to subtract one.
+      token.getAnArgument() = repeatStars(c.getIndirectionIndex() - 1)
+    )
+  }
+}
+
+private import Make<Location, DataFlowImplSpecific::CppDataFlow, Input> as Impl
+
+private module StepsInput implements Impl::Private::StepsInputSig {
+  DataFlowCall getACall(Public::SummarizedCallable sc) {
+    result.getStaticCallTarget().getUnderlyingCallable() = sc
+  }
+}
+
+module SourceSinkInterpretationInput implements
+  Impl::Private::External::SourceSinkInterpretationInputSig
+{
+  class Element = Cpp::Element;
+
+  class SourceOrSinkElement = Element;
+
+  /**
+   * Holds if an external source specification exists for `e` with output specification
+   * `output`, kind `kind`, and provenance `provenance`.
+   */
+  predicate sourceElement(
+    SourceOrSinkElement e, string output, string kind, Public::Provenance provenance, string model
+  ) {
+    exists(
+      string namespace, string type, boolean subtypes, string name, string signature, string ext
+    |
+      sourceModel(namespace, type, subtypes, name, signature, ext, output, kind, provenance) and
+      e = interpretElement(namespace, type, subtypes, name, signature, ext) and
+      model = "" // TODO
+    )
+  }
+
+  /**
+   * Holds if an external sink specification exists for `e` with input specification
+   * `input`, kind `kind` and provenance `provenance`.
+   */
+  predicate sinkElement(
+    SourceOrSinkElement e, string input, string kind, Public::Provenance provenance, string model
+  ) {
+    exists(
+      string package, string type, boolean subtypes, string name, string signature, string ext
+    |
+      sinkModel(package, type, subtypes, name, signature, ext, input, kind, provenance) and
+      e = interpretElement(package, type, subtypes, name, signature, ext) and
+      model = "" // TODO
+    )
+  }
+
+  private newtype TInterpretNode =
+    TElement_(Element n) or
+    TNode_(Node n)
+
+  /** An entity used to interpret a source/sink specification. */
+  class InterpretNode extends TInterpretNode {
+    /** Gets the element that this node corresponds to, if any. */
+    SourceOrSinkElement asElement() { this = TElement_(result) }
+
+    /** Gets the data-flow node that this node corresponds to, if any. */
+    Node asNode() { this = TNode_(result) }
+
+    /** Gets the call that this node corresponds to, if any. */
+    DataFlowCall asCall() {
+      this.asElement() = result.asCallInstruction().getUnconvertedResultExpression()
+    }
+
+    /** Gets the callable that this node corresponds to, if any. */
+    DataFlowCallable asCallable() { result.getUnderlyingCallable() = this.asElement() }
+
+    /** Gets the target of this call, if any. */
+    Element getCallTarget() { result = this.asCall().getStaticCallTarget().getUnderlyingCallable() }
+
+    /** Gets a textual representation of this node. */
+    string toString() {
+      result = this.asElement().toString()
+      or
+      result = this.asNode().toString()
+      or
+      result = this.asCall().toString()
+    }
+
+    /** Gets the location of this node. */
+    Location getLocation() {
+      result = this.asElement().getLocation()
+      or
+      result = this.asNode().getLocation()
+      or
+      result = this.asCall().getLocation()
+    }
+  }
+
+  /** Provides additional sink specification logic. */
+  bindingset[c]
+  predicate interpretOutput(string c, InterpretNode mid, InterpretNode node) {
+    // Allow variables to be picked as output nodes.
+    exists(Node n, Element ast |
+      n = node.asNode() and
+      ast = mid.asElement()
+    |
+      c = "" and
+      n.asExpr().(VariableAccess).getTarget() = ast
+    )
+  }
+
+  /** Provides additional source specification logic. */
+  bindingset[c]
+  predicate interpretInput(string c, InterpretNode mid, InterpretNode node) {
+    exists(Node n, Element ast, VariableAccess e |
+      n = node.asNode() and
+      ast = mid.asElement() and
+      e.getTarget() = ast
+    |
+      // Allow variables to be picked as input nodes.
+      // We could simply do this as `e = n.asExpr()`, but that would not allow
+      // us to pick `x` as a sink in an example such as `x = source()` (but
+      // only subsequent uses of `x`) since the variable access on `x` doesn't
+      // actually load the value of `x`. So instead, we pick the instruction
+      // node corresponding to the generated `StoreInstruction` and use the
+      // expression associated with the destination instruction. This means
+      // that the `x` in `x = source()` can be marked as an input.
+      c = "" and
+      exists(StoreInstruction store |
+        store.getDestinationAddress().getUnconvertedResultExpression() = e and
+        n.asInstruction() = store
+      )
+    )
+  }
+}
+
+module Private {
+  import Impl::Private
+
+  module Steps = Impl::Private::Steps<StepsInput>;
+
+  module External {
+    import Impl::Private::External
+    import Impl::Private::External::SourceSinkInterpretation<SourceSinkInterpretationInput>
+  }
+
+  /**
+   * Provides predicates for constructing summary components.
+   */
+  module SummaryComponent {
+    private import Impl::Private::SummaryComponent as SC
+
+    predicate parameter = SC::parameter/1;
+
+    predicate argument = SC::argument/1;
+
+    predicate content = SC::content/1;
+
+    predicate withoutContent = SC::withoutContent/1;
+
+    predicate withContent = SC::withContent/1;
+  }
+
+  /**
+   * Provides predicates for constructing stacks of summary components.
+   */
+  module SummaryComponentStack {
+    private import Impl::Private::SummaryComponentStack as SCS
+
+    predicate singleton = SCS::singleton/1;
+
+    predicate push = SCS::push/2;
+
+    predicate argument = SCS::argument/1;
+  }
+}
+
+module Public = Impl::Public;

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

@@ -4,9 +4,10 @@
  * Provides C++-specific definitions for use in the taint tracking library.
  */
 
+private import semmle.code.cpp.Location
 private import codeql.dataflow.TaintTracking
 private import DataFlowImplSpecific
 
-module CppOldTaintTracking implements InputSig<CppOldDataFlow> {
+module CppOldTaintTracking implements InputSig<Location, CppOldDataFlow> {
   import TaintTrackingUtil
 }

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

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

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

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

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

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

cpp/ql/lib/semmle/code/cpp/dataflow/new/DataFlow.qll

@@ -28,6 +28,6 @@ import cpp
 module DataFlow {
   private import semmle.code.cpp.ir.dataflow.internal.DataFlowImplSpecific
   private import codeql.dataflow.DataFlow
-  import DataFlowMake<CppDataFlow>
+  import DataFlowMake<Location, CppDataFlow>
   import semmle.code.cpp.ir.dataflow.internal.DataFlowImpl1
 }

cpp/ql/lib/semmle/code/cpp/dataflow/new/TaintTracking.qll

@@ -27,6 +27,7 @@ module TaintTracking {
   private import semmle.code.cpp.ir.dataflow.internal.DataFlowImplSpecific
   private import semmle.code.cpp.ir.dataflow.internal.TaintTrackingImplSpecific
   private import codeql.dataflow.TaintTracking
-  import TaintFlowMake<CppDataFlow, CppTaintTracking>
+  private import semmle.code.cpp.Location
+  import TaintFlowMake<Location, CppDataFlow, CppTaintTracking>
   import semmle.code.cpp.ir.dataflow.internal.tainttracking1.TaintTrackingImpl
 }

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

@@ -63,6 +63,12 @@ class Expr extends StmtParent, @expr {
    * order of destruction.
    */
   DestructorCall getImplicitDestructorCall(int n) {
+    exists(Expr e |
+      e = this.(TemporaryObjectExpr).getExpr() and
+      synthetic_destructor_call(e, max(int i | synthetic_destructor_call(e, i, _)) - n, result)
+    )
+    or
+    not this = any(TemporaryObjectExpr temp).getExpr() and
     synthetic_destructor_call(this, max(int i | synthetic_destructor_call(this, i, _)) - n, result)
   }
 
@@ -1015,8 +1021,33 @@ class DeleteOrDeleteArrayExpr extends Expr, TDeleteOrDeleteArrayExpr {
   Expr getExpr() {
     // If there is a destructor call, the object being deleted is the qualifier
     // otherwise it is the third child.
-    result = this.getChild(3) or result = this.getDestructorCall().getQualifier()
+    exists(Expr exprWithReuse | exprWithReuse = this.getExprWithReuse() |
+      if not exprWithReuse instanceof ReuseExpr
+      then result = exprWithReuse
+      else result = this.getDestructorCall().getQualifier()
+    )
   }
+
+  /**
+   * Gets the object or array being deleted, and gets a `ReuseExpr` when there
+   * is a destructor call and the object is also the qualifier of the call.
+   *
+   * For example, given:
+   * ```
+   * struct HasDestructor { ~HasDestructor(); };
+   * struct PlainOldData { int x, char y; };
+   *
+   * void f(HasDestructor* hasDestructor, PlainOldData* pod) {
+   *   delete hasDestructor;
+   *   delete pod;
+   * }
+   * ```
+   * This predicate yields a `ReuseExpr` for `delete hasDestructor`, as the
+   * the deleted expression has a destructor, and that expression is also
+   * the qualifier of the destructor call. In the case of `delete pod` the
+   * predicate does not yield a `ReuseExpr`, as there is no destructor call.
+   */
+  Expr getExprWithReuse() { result = this.getChild(3) }
 }
 
 /**
@@ -1307,6 +1338,24 @@ class CoAwaitExpr extends UnaryOperation, @co_await {
   override string getOperator() { result = "co_await" }
 
   override int getPrecedence() { result = 16 }
+
+  /**
+   * Gets the Boolean expression that is used to decide if the enclosing
+   * coroutine should be suspended.
+   */
+  Expr getAwaitReady() { result = this.getChild(1) }
+
+  /**
+   * Gets the expression that represents the resume point if the enclosing
+   * coroutine was suspended.
+   */
+  Expr getAwaitResume() { result = this.getChild(2) }
+
+  /**
+   * Gets the expression that is evaluated when the enclosing coroutine is
+   * suspended.
+   */
+  Expr getAwaitSuspend() { result = this.getChild(3) }
 }
 
 /**
@@ -1321,4 +1370,50 @@ class CoYieldExpr extends UnaryOperation, @co_yield {
   override string getOperator() { result = "co_yield" }
 
   override int getPrecedence() { result = 2 }
+
+  /**
+   * Gets the Boolean expression that is used to decide if the enclosing
+   * coroutine should be suspended.
+   */
+  Expr getAwaitReady() { result = this.getChild(1) }
+
+  /**
+   * Gets the expression that represents the resume point if the enclosing
+   * coroutine was suspended.
+   */
+  Expr getAwaitResume() { result = this.getChild(2) }
+
+  /**
+   * Gets the expression that is evaluated when the enclosing coroutine is
+   * suspended.
+   */
+  Expr getAwaitSuspend() { result = this.getChild(3) }
+}
+
+/**
+ * An expression representing the re-use of another expression.
+ *
+ * In some specific cases an expression may be referred to outside its
+ * original context. A re-use expression wraps any such reference. A
+ * re-use expression can for example occur as the qualifier of an implicit
+ * destructor called on a temporary object, where the original use of the
+ * expression is in the definition of the temporary.
+ */
+class ReuseExpr extends Expr, @reuseexpr {
+  override string getAPrimaryQlClass() { result = "ReuseExpr" }
+
+  override string toString() { result = "reuse of " + this.getReusedExpr().toString() }
+
+  /**
+   * Gets the expression that is being re-used.
+   */
+  Expr getReusedExpr() { expr_reuse(underlyingElement(this), unresolveElement(result), _) }
+
+  override Type getType() { result = this.getReusedExpr().getType() }
+
+  override predicate isLValueCategory() { expr_reuse(underlyingElement(this), _, 3) }
+
+  override predicate isXValueCategory() { expr_reuse(underlyingElement(this), _, 2) }
+
+  override predicate isPRValueCategory() { expr_reuse(underlyingElement(this), _, 1) }
 }

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

@@ -24,6 +24,6 @@ import cpp
 module DataFlow {
   private import semmle.code.cpp.ir.dataflow.internal.DataFlowImplSpecific
   private import codeql.dataflow.DataFlow
-  import DataFlowMake<CppDataFlow>
+  import DataFlowMake<Location, CppDataFlow>
   import semmle.code.cpp.ir.dataflow.internal.DataFlowImpl1
 }

cpp/ql/lib/semmle/code/cpp/ir/dataflow/FlowSteps.qll

@@ -0,0 +1,20 @@
+/**
+ * This file provides an abstract class that can be used to model additional
+ * object-to-field taint-flow.
+ */
+
+private import codeql.util.Unit
+private import semmle.code.cpp.dataflow.new.DataFlow
+
+/**
+ * A `Content` that should be implicitly regarded as tainted whenever an object with such `Content`
+ * is itself tainted.
+ *
+ * For example, if we had a type `struct Container { int field; }`, then by default a tainted
+ * `Container` and a `Container` with a tainted `int` stored in its `field` are distinct.
+ *
+ * If `any(DataFlow::FieldContent fc | fc.getField().hasQualifiedName("Container", "field"))` was
+ * included in this type however, then a tainted `Container` would imply that its `field` is also
+ * tainted (but not vice versa).
+ */
+abstract class TaintInheritingContent extends DataFlow::Content { }

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

@@ -7,6 +7,7 @@ import cpp
 private import semmle.code.cpp.ir.ValueNumbering
 private import internal.DataFlowDispatch
 private import semmle.code.cpp.ir.IR
+private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
 
 /**
  * Resolve potential target function(s) for `call`.
@@ -16,8 +17,9 @@ private import semmle.code.cpp.ir.IR
  * to identify the possible target(s).
  */
 Function resolveCall(Call call) {
-  exists(CallInstruction callInstruction |
+  exists(DataFlowCall dataFlowCall, CallInstruction callInstruction |
     callInstruction.getAst() = call and
-    result = viableCallable(callInstruction)
+    callInstruction = dataFlowCall.asCallInstruction() and
+    result = viableCallable(dataFlowCall).getUnderlyingCallable()
   )
 }

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

@@ -23,6 +23,6 @@ module TaintTracking {
   private import semmle.code.cpp.ir.dataflow.internal.DataFlowImplSpecific
   private import semmle.code.cpp.ir.dataflow.internal.TaintTrackingImplSpecific
   private import codeql.dataflow.TaintTracking
-  import TaintFlowMake<CppDataFlow, CppTaintTracking>
+  import TaintFlowMake<Location, CppDataFlow, CppTaintTracking>
   import semmle.code.cpp.ir.dataflow.internal.tainttracking1.TaintTrackingImpl
 }

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

@@ -23,13 +23,13 @@ DataFlowCallable defaultViableCallable(DataFlowCall call) {
   // 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
+    callSignatureWithoutBody(qualifiedName, nparams, call.asCallInstruction()) and
+    functionSignatureWithBody(qualifiedName, nparams, result.getUnderlyingCallable()) and
     strictcount(Function other | functionSignatureWithBody(qualifiedName, nparams, other)) = 1
   )
   or
   // Virtual dispatch
-  result = call.(VirtualDispatch::DataSensitiveCall).resolve()
+  result.asSourceCallable() = call.(VirtualDispatch::DataSensitiveCall).resolve()
 }
 
 /**
@@ -40,7 +40,9 @@ DataFlowCallable viableCallable(DataFlowCall call) {
   result = defaultViableCallable(call)
   or
   // Additional call targets
-  result = any(AdditionalCallTarget additional).viableTarget(call.getUnconvertedResultExpression())
+  result.getUnderlyingCallable() =
+    any(AdditionalCallTarget additional)
+        .viableTarget(call.asCallInstruction().getUnconvertedResultExpression())
 }
 
 /**
@@ -150,7 +152,7 @@ private module VirtualDispatch {
     ReturnNode node, ReturnKind kind, DataFlowCallable callable
   ) {
     node.getKind() = kind and
-    node.getEnclosingCallable() = callable
+    node.getEnclosingCallable() = callable.getUnderlyingCallable()
   }
 
   /** Call through a function pointer. */
@@ -176,10 +178,15 @@ private module VirtualDispatch {
   /** Call to a virtual function. */
   private class DataSensitiveOverriddenFunctionCall extends DataSensitiveCall {
     DataSensitiveOverriddenFunctionCall() {
-      exists(this.getStaticCallTarget().(VirtualFunction).getAnOverridingFunction())
+      exists(
+        this.getStaticCallTarget()
+            .getUnderlyingCallable()
+            .(VirtualFunction)
+            .getAnOverridingFunction()
+      )
     }
 
-    override DataFlow::Node getDispatchValue() { result.asInstruction() = this.getThisArgument() }
+    override DataFlow::Node getDispatchValue() { result.asInstruction() = this.getArgument(-1) }
 
     override MemberFunction resolve() {
       exists(Class overridingClass |
@@ -194,7 +201,8 @@ private module VirtualDispatch {
      */
     pragma[noinline]
     private predicate overrideMayAffectCall(Class overridingClass, MemberFunction overridingFunction) {
-      overridingFunction.getAnOverriddenFunction+() = this.getStaticCallTarget().(VirtualFunction) and
+      overridingFunction.getAnOverriddenFunction+() =
+        this.getStaticCallTarget().getUnderlyingCallable().(VirtualFunction) and
       overridingFunction.getDeclaringType() = overridingClass
     }
 
@@ -256,12 +264,12 @@ predicate mayBenefitFromCallContext(DataFlowCall call) { mayBenefitFromCallConte
  * value is given as the `arg`'th argument to `f`.
  */
 private predicate mayBenefitFromCallContext(
-  VirtualDispatch::DataSensitiveCall call, Function f, int arg
+  VirtualDispatch::DataSensitiveCall call, DataFlowCallable f, int arg
 ) {
   f = pragma[only_bind_out](call).getEnclosingCallable() and
   exists(InitializeParameterInstruction init |
     not exists(call.getStaticCallTarget()) and
-    init.getEnclosingFunction() = f and
+    init.getEnclosingFunction() = f.getUnderlyingCallable() and
     call.flowsFrom(DataFlow::instructionNode(init), _) and
     init.getParameter().getIndex() = arg
   )
@@ -273,10 +281,11 @@ private predicate mayBenefitFromCallContext(
  */
 DataFlowCallable viableImplInCallContext(DataFlowCall call, DataFlowCall ctx) {
   result = viableCallable(call) and
-  exists(int i, Function f |
+  exists(int i, DataFlowCallable f |
     mayBenefitFromCallContext(pragma[only_bind_into](call), f, i) and
     f = ctx.getStaticCallTarget() and
-    result = ctx.getArgument(i).getUnconvertedResultExpression().(FunctionAccess).getTarget()
+    result.asSourceCallable() =
+      ctx.getArgument(i).getUnconvertedResultExpression().(FunctionAccess).getTarget()
   )
 }
 

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

@@ -1,3 +1,4 @@
+private import semmle.code.cpp.Location
 private import DataFlowImplSpecific
 private import codeql.dataflow.internal.DataFlowImpl
-import MakeImpl<CppDataFlow>
+import MakeImpl<Location, CppDataFlow>

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

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
@@ -285,6 +286,8 @@ deprecated private module Config implements FullStateConfigSig {
 
   int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
 
+  int accessPathLimit() { result = 5 }
+
   FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }
 
   predicate sourceGrouping(Node source, string sourceGroup) {

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

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
@@ -285,6 +286,8 @@ deprecated private module Config implements FullStateConfigSig {
 
   int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
 
+  int accessPathLimit() { result = 5 }
+
   FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }
 
   predicate sourceGrouping(Node source, string sourceGroup) {

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

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
@@ -285,6 +286,8 @@ deprecated private module Config implements FullStateConfigSig {
 
   int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
 
+  int accessPathLimit() { result = 5 }
+
   FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }
 
   predicate sourceGrouping(Node source, string sourceGroup) {

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

@@ -263,9 +263,10 @@ deprecated private module Config implements FullStateConfigSig {
 
   predicate isBarrierOut(Node node, FlowState state) { none() }
 
-  predicate isAdditionalFlowStep(Node node1, Node node2) {
+  predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
     singleConfiguration() and
-    any(Configuration config).isAdditionalFlowStep(node1, node2)
+    any(Configuration config).isAdditionalFlowStep(node1, node2) and
+    model = ""
   }
 
   predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
@@ -285,6 +286,8 @@ deprecated private module Config implements FullStateConfigSig {
 
   int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
 
+  int accessPathLimit() { result = 5 }
+
   FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }
 
   predicate sourceGrouping(Node source, string sourceGroup) {

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

@@ -1,3 +1,4 @@
+private import semmle.code.cpp.Location
 private import DataFlowImplSpecific
 private import codeql.dataflow.internal.DataFlowImplCommon
-import MakeImplCommon<CppDataFlow>
+import MakeImplCommon<Location, CppDataFlow>

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

@@ -8,7 +8,7 @@ private import DataFlowImplSpecific
 private import TaintTrackingImplSpecific
 private import codeql.dataflow.internal.DataFlowImplConsistency
 
-private module Input implements InputSig<CppDataFlow> {
+private module Input implements InputSig<Location, CppDataFlow> {
   predicate argHasPostUpdateExclude(Private::ArgumentNode n) {
     // The rules for whether an IR argument gets a post-update node are too
     // complex to model here.
@@ -16,4 +16,4 @@ private module Input implements InputSig<CppDataFlow> {
   }
 }
 
-module Consistency = MakeConsistency<CppDataFlow, CppTaintTracking, Input>;
+module Consistency = MakeConsistency<Location, CppDataFlow, CppTaintTracking, Input>;

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

@@ -3,6 +3,7 @@
  */
 
 private import codeql.dataflow.DataFlow
+private import semmle.code.cpp.Location
 
 module Private {
   import DataFlowPrivate
@@ -13,7 +14,7 @@ module Public {
   import DataFlowUtil
 }
 
-module CppDataFlow implements InputSig {
+module CppDataFlow implements InputSig<Location> {
   import Private
   import Public
 
@@ -21,9 +22,13 @@ module CppDataFlow implements InputSig {
 
   predicate getAdditionalFlowIntoCallNodeTerm = Private::getAdditionalFlowIntoCallNodeTerm/2;
 
+  predicate getSecondLevelScope = Private::getSecondLevelScope/1;
+
   predicate validParameterAliasStep = Private::validParameterAliasStep/2;
 
   predicate mayBenefitFromCallContext = Private::mayBenefitFromCallContext/1;
 
   predicate viableImplInCallContext = Private::viableImplInCallContext/2;
+
+  predicate neverSkipInPathGraph = Private::neverSkipInPathGraph/1;
 }

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

@@ -3,6 +3,7 @@ private import DataFlowUtil
 private import semmle.code.cpp.ir.IR
 private import DataFlowDispatch
 private import semmle.code.cpp.ir.internal.IRCppLanguage
+private import semmle.code.cpp.dataflow.internal.FlowSummaryImpl as FlowSummaryImpl
 private import SsaInternals as Ssa
 private import DataFlowImplCommon as DataFlowImplCommon
 private import codeql.util.Unit
@@ -77,15 +78,8 @@ module NodeStars {
     result = n.(PostUpdateNodeImpl).getIndirectionIndex()
     or
     result = n.(FinalParameterNode).getIndirectionIndex()
-  }
-
-  private int maxNumberOfIndirections() { result = max(getNumberOfIndirections(_)) }
-
-  private string repeatStars(int n) {
-    n = 0 and result = ""
     or
-    n = [1 .. maxNumberOfIndirections()] and
-    result = "*" + repeatStars(n - 1)
+    result = n.(BodyLessParameterNodeImpl).getIndirectionIndex()
   }
 
   /**
@@ -97,6 +91,11 @@ module NodeStars {
 
 import NodeStars
 
+/**
+ * A cut-down `DataFlow::Node` class that does not depend on the output of SSA.
+ * This can thus be safely used in the SSA computations themselves, as well as
+ * in construction of other node classes (`TIRDataFlowNode`).
+ */
 class Node0Impl extends TIRDataFlowNode0 {
   /**
    * INTERNAL: Do not use.
@@ -333,7 +332,9 @@ private module IndirectInstructions {
 import IndirectInstructions
 
 /** Gets the callable in which this node occurs. */
-DataFlowCallable nodeGetEnclosingCallable(Node n) { result = n.getEnclosingCallable() }
+DataFlowCallable nodeGetEnclosingCallable(Node n) {
+  result.getUnderlyingCallable() = n.getEnclosingCallable()
+}
 
 /** Holds if `p` is a `ParameterNode` of `c` with position `pos`. */
 predicate isParameterNode(ParameterNode p, DataFlowCallable c, ParameterPosition pos) {
@@ -379,12 +380,30 @@ private class SideEffectArgumentNode extends ArgumentNode, SideEffectOperandNode
   override predicate argumentOf(DataFlowCall dfCall, ArgumentPosition pos) {
     exists(int indirectionIndex |
       pos = TIndirectionPosition(argumentIndex, pragma[only_bind_into](indirectionIndex)) and
-      this.getCallInstruction() = dfCall and
+      this.getCallInstruction() = dfCall.asCallInstruction() and
       super.hasAddressOperandAndIndirectionIndex(_, pragma[only_bind_into](indirectionIndex))
     )
   }
 }
 
+/**
+ * An argument node that is part of a summary. These only occur when the
+ * summary contains a synthesized call.
+ */
+class SummaryArgumentNode extends ArgumentNode, FlowSummaryNode {
+  private SummaryCall call_;
+  private ArgumentPosition pos_;
+
+  SummaryArgumentNode() {
+    FlowSummaryImpl::Private::summaryArgumentNode(call_.getReceiver(), this.getSummaryNode(), pos_)
+  }
+
+  override predicate argumentOf(DataFlowCall call, ArgumentPosition pos) {
+    call = call_ and
+    pos = pos_
+  }
+}
+
 /** A parameter position represented by an integer. */
 class ParameterPosition = Position;
 
@@ -432,24 +451,42 @@ class IndirectionPosition extends Position, TIndirectionPosition {
 }
 
 newtype TPosition =
-  TDirectPosition(int index) { exists(any(CallInstruction c).getArgument(index)) } or
+  TDirectPosition(int argumentIndex) { exists(any(CallInstruction c).getArgument(argumentIndex)) } or
   TIndirectionPosition(int argumentIndex, int indirectionIndex) {
-    hasOperandAndIndex(_, any(CallInstruction call).getArgumentOperand(argumentIndex),
+    Ssa::hasIndirectOperand(any(CallInstruction call).getArgumentOperand(argumentIndex),
       indirectionIndex)
   }
 
 private newtype TReturnKind =
-  TNormalReturnKind(int index) {
-    exists(IndirectReturnNode return |
-      return.isNormalReturn() and
-      index = return.getIndirectionIndex() - 1 // We subtract one because the return loads the value.
-    )
+  TNormalReturnKind(int indirectionIndex) {
+    // derive a possible return indirection from SSA
+    // (this is a more durable approach if SSA infers additional indirections for any reason)
+    Ssa::hasIndirectOperand(any(ReturnValueInstruction ret).getReturnAddressOperand(),
+      indirectionIndex + 1) // We subtract one because the return loads the value.
+    or
+    // derive a possible return kind from the AST
+    // (this approach includes functions declared that have no body; they may still have flow summaries)
+    indirectionIndex =
+      [0 .. max(Cpp::Function f |
+          not exists(f.getBlock())
+        |
+          Ssa::getMaxIndirectionsForType(f.getUnspecifiedType()) - 1 // -1 because a returned value is a prvalue not a glvalue
+        )]
   } or
   TIndirectReturnKind(int argumentIndex, int indirectionIndex) {
-    exists(IndirectReturnNode return |
-      return.isParameterReturn(argumentIndex) and
-      indirectionIndex = return.getIndirectionIndex()
+    // derive a possible return argument from SSA
+    exists(Ssa::FinalParameterUse use |
+      use.getIndirectionIndex() = indirectionIndex and
+      use.getArgumentIndex() = argumentIndex
     )
+    or
+    // derive a possible return argument from the AST
+    indirectionIndex =
+      [0 .. max(Cpp::Function f |
+          not exists(f.getBlock())
+        |
+          Ssa::getMaxIndirectionsForType(f.getParameter(argumentIndex).getUnspecifiedType()) - 1 // -1 because an argument is a prvalue not a glvalue
+        )]
   }
 
 /**
@@ -457,29 +494,44 @@ private newtype TReturnKind =
  * from a callable. For C++, this is simply a function return.
  */
 class ReturnKind extends TReturnKind {
+  /**
+   * Gets the indirection index of this return kind.
+   */
+  abstract int getIndirectionIndex();
+
   /** Gets a textual representation of this return kind. */
   abstract string toString();
 }
 
-private class NormalReturnKind extends ReturnKind, TNormalReturnKind {
-  int index;
+/**
+ * A value returned from a callable using a `return` statement, that is, a "normal" return.
+ */
+class NormalReturnKind extends ReturnKind, TNormalReturnKind {
+  int indirectionIndex;
 
-  NormalReturnKind() { this = TNormalReturnKind(index) }
+  NormalReturnKind() { this = TNormalReturnKind(indirectionIndex) }
+
+  override int getIndirectionIndex() { result = indirectionIndex }
 
   override string toString() { result = "indirect return" }
 }
 
+/**
+ * A value returned from a callable through a parameter.
+ */
 private class IndirectReturnKind extends ReturnKind, TIndirectReturnKind {
   int argumentIndex;
   int indirectionIndex;
 
   IndirectReturnKind() { this = TIndirectReturnKind(argumentIndex, indirectionIndex) }
 
+  override int getIndirectionIndex() { result = 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 {
+abstract class ReturnNode extends Node {
   /** Gets the kind of this returned value. */
   abstract ReturnKind getKind();
 }
@@ -510,6 +562,17 @@ class ReturnIndirectionNode extends IndirectReturnNode, ReturnNode {
   }
 }
 
+/**
+ * A return node that is part of a summary.
+ */
+private class SummaryReturnNode extends ReturnNode, FlowSummaryNode {
+  private ReturnKind rk;
+
+  SummaryReturnNode() { FlowSummaryImpl::Private::summaryReturnNode(this.getSummaryNode(), rk) }
+
+  override ReturnKind getKind() { result = rk }
+}
+
 private Operand fullyConvertedCallStepImpl(Operand op) {
   not exists(getANonConversionUse(op)) and
   exists(Instruction instr |
@@ -616,7 +679,10 @@ predicate simpleOutNode(Node node, CallInstruction call) {
   instructionForFullyConvertedCall(node.asInstruction(), call)
 }
 
-/** A data flow node that represents the output of a call. */
+/**
+ * A data flow node that represents the output of a call (for example, a
+ * return value) at the call site.
+ */
 class OutNode extends Node {
   OutNode() {
     // Return values not hidden behind indirections
@@ -627,11 +693,15 @@ class OutNode extends Node {
     or
     // Modified arguments hidden behind indirections
     this instanceof IndirectArgumentOutNode
+    or
+    // Summary node
+    FlowSummaryImpl::Private::summaryOutNode(_, this.(FlowSummaryNode).getSummaryNode(), _)
   }
 
   /** Gets the underlying call. */
   abstract DataFlowCall getCall();
 
+  /** Gets the kind of this out node. */
   abstract ReturnKind getReturnKind();
 }
 
@@ -640,25 +710,44 @@ private class DirectCallOutNode extends OutNode {
 
   DirectCallOutNode() { simpleOutNode(this, call) }
 
-  override DataFlowCall getCall() { result = call }
+  override DataFlowCall getCall() { result.asCallInstruction() = call }
 
   override ReturnKind getReturnKind() { result = TNormalReturnKind(0) }
 }
 
 private class IndirectCallOutNode extends OutNode, IndirectReturnOutNode {
-  override DataFlowCall getCall() { result = this.getCallInstruction() }
+  override DataFlowCall getCall() { result.asCallInstruction() = this.getCallInstruction() }
 
   override ReturnKind getReturnKind() { result = TNormalReturnKind(this.getIndirectionIndex()) }
 }
 
 private class SideEffectOutNode extends OutNode, IndirectArgumentOutNode {
-  override DataFlowCall getCall() { result = this.getCallInstruction() }
+  override DataFlowCall getCall() { result.asCallInstruction() = this.getCallInstruction() }
 
   override ReturnKind getReturnKind() {
     result = TIndirectReturnKind(this.getArgumentIndex(), this.getIndirectionIndex())
   }
 }
 
+/**
+ * An output node that is part of a summary. An output node is needed when the
+ * model contains a synthesized call (`SummaryCall`) and the return value of
+ * that call is needed by the summary (for example when the model has flow from
+ * `Argument[0].ReturnValue`).
+ */
+private class SummaryOutNode extends OutNode, FlowSummaryNode {
+  private SummaryCall call;
+  private ReturnKind kind_;
+
+  SummaryOutNode() {
+    FlowSummaryImpl::Private::summaryOutNode(call.getReceiver(), this.getSummaryNode(), kind_)
+  }
+
+  override DataFlowCall getCall() { result = call }
+
+  override ReturnKind getReturnKind() { result = kind_ }
+}
+
 /**
  * Gets a node that can read the value returned from `call` with return kind
  * `kind`.
@@ -721,6 +810,10 @@ predicate jumpStep(Node n1, Node n2) {
       v = n1.asIndirectVariable(globalDef.getIndirection())
     )
   )
+  or
+  // models-as-data summarized flow
+  FlowSummaryImpl::Private::Steps::summaryJumpStep(n1.(FlowSummaryNode).getSummaryNode(),
+    n2.(FlowSummaryNode).getSummaryNode())
 }
 
 /**
@@ -729,25 +822,35 @@ predicate jumpStep(Node n1, Node n2) {
  * value of `node1`.
  *
  * The boolean `certain` is true if the destination address does not involve
- * any pointer arithmetic, and false otherwise.
+ * any pointer arithmetic, and false otherwise. This has to do with whether a
+ * store step can be used to clear a field (see `clearsContent`).
  */
-predicate storeStepImpl(Node node1, Content c, PostFieldUpdateNode node2, boolean certain) {
-  exists(int indirectionIndex1, int numberOfLoads, StoreInstruction store |
+predicate storeStepImpl(Node node1, Content c, Node node2, boolean certain) {
+  exists(
+    PostFieldUpdateNode postFieldUpdate, int indirectionIndex1, int numberOfLoads,
+    StoreInstruction store
+  |
+    postFieldUpdate = node2 and
     nodeHasInstruction(node1, store, pragma[only_bind_into](indirectionIndex1)) and
-    node2.getIndirectionIndex() = 1 and
-    numberOfLoadsFromOperand(node2.getFieldAddress(), store.getDestinationAddressOperand(),
-      numberOfLoads, certain)
+    postFieldUpdate.getIndirectionIndex() = 1 and
+    numberOfLoadsFromOperand(postFieldUpdate.getFieldAddress(),
+      store.getDestinationAddressOperand(), numberOfLoads, certain)
   |
     exists(FieldContent fc | fc = c |
-      fc.getField() = node2.getUpdatedField() and
+      fc.getField() = postFieldUpdate.getUpdatedField() and
       fc.getIndirectionIndex() = 1 + indirectionIndex1 + numberOfLoads
     )
     or
     exists(UnionContent uc | uc = c |
-      uc.getAField() = node2.getUpdatedField() and
+      uc.getAField() = postFieldUpdate.getUpdatedField() and
       uc.getIndirectionIndex() = 1 + indirectionIndex1 + numberOfLoads
     )
   )
+  or
+  // models-as-data summarized flow
+  FlowSummaryImpl::Private::Steps::summaryStoreStep(node1.(FlowSummaryNode).getSummaryNode(), c,
+    node2.(FlowSummaryNode).getSummaryNode()) and
+  certain = true
 }
 
 /**
@@ -834,6 +937,10 @@ predicate readStep(Node node1, ContentSet c, Node node2) {
       uc.getIndirectionIndex() = indirectionIndex2 + numberOfLoads
     )
   )
+  or
+  // models-as-data summarized flow
+  FlowSummaryImpl::Private::Steps::summaryReadStep(node1.(FlowSummaryNode).getSummaryNode(), c,
+    node2.(FlowSummaryNode).getSummaryNode())
 }
 
 /**
@@ -907,21 +1014,213 @@ class CastNode extends Node {
   CastNode() { none() } // stub implementation
 }
 
+cached
+private newtype TDataFlowCallable =
+  TSourceCallable(Cpp::Declaration decl) {
+    not decl instanceof FlowSummaryImpl::Public::SummarizedCallable
+  } or
+  TSummarizedCallable(FlowSummaryImpl::Public::SummarizedCallable c)
+
 /**
- * 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.
+ * A callable, which may be:
+ *  - a function (that may contain code)
+ *  - a summarized function (that may contain only `FlowSummaryNode`s)
+ *  - a variable (this is used as context for global initialization, and also
+ *    for the mid-point in interprocedural data flow between a write and read
+ *    of a global variable in different functions).
+ * 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 DataFlowCallable extends TDataFlowCallable {
+  /** Gets the location of this callable. */
+  Location getLocation() { none() }
+
+  /** Gets a textual representation of this callable. */
+  string toString() { none() }
+
+  /**
+   * Gets the `Declaration` corresponding to this callable if it exists in the database.
+   * For summarized callables (which may not exist in the database), use `asSummarizedCallable`.
+   */
+  Cpp::Declaration asSourceCallable() { this = TSourceCallable(result) }
+
+  /**
+   * Gets the underlying summarized callable, if
+   * this callable is generated from a models-as-data
+   * model.
+   */
+  FlowSummaryImpl::Public::SummarizedCallable asSummarizedCallable() {
+    this = TSummarizedCallable(result)
+  }
+
+  /**
+   * Gets the underlying `Declaration` of this `DataFlowCallable`. This
+   * predicate returns a result for both source and summarized callables.
+   */
+  Cpp::Declaration getUnderlyingCallable() {
+    result = this.asSummarizedCallable() or // SummarizedCallable = Function (in CPP)
+    result = this.asSourceCallable()
+  }
+}
+
+/**
+ * A source callable, conceptually, a function in the source code for the
+ * purpose of computing data flow. In practice this excludes functions that
+ * are summarized using models-as-data (as we don't want to create
+ * unmodeled flows or duplicate paths), and includes variables (for reasons
+ * explained in `DataFlowCallable`).
+ */
+class SourceCallable extends DataFlowCallable, TSourceCallable {
+  Cpp::Declaration decl;
+
+  SourceCallable() { this = TSourceCallable(decl) }
+
+  override string toString() { result = decl.toString() }
+
+  override Location getLocation() { result = decl.getLocation() }
+}
+
+/**
+ * A summarized callable, that is, a function synthesized from one or more
+ * models-as-data models as a place to contain the corresponding
+ * `FlowSummaryNode`s.
+ */
+class SummarizedCallable extends DataFlowCallable, TSummarizedCallable {
+  FlowSummaryImpl::Public::SummarizedCallable sc;
+
+  SummarizedCallable() { this = TSummarizedCallable(sc) }
+
+  override string toString() { result = sc.toString() }
+
+  override Location getLocation() { result = sc.getLocation() }
+}
 
 class DataFlowExpr = Expr;
 
 class DataFlowType = Type;
 
-/** A function call relevant for data flow. */
-class DataFlowCall extends CallInstruction {
-  DataFlowCallable getEnclosingCallable() { result = this.getEnclosingFunction() }
+cached
+private newtype TDataFlowCall =
+  TNormalCall(CallInstruction call) or
+  TSummaryCall(
+    FlowSummaryImpl::Public::SummarizedCallable c, FlowSummaryImpl::Private::SummaryNode receiver
+  ) {
+    FlowSummaryImpl::Private::summaryCallbackRange(c, receiver)
+  }
+
+/**
+ * A function call relevant for data flow. This includes calls from source
+ * code and calls inside library callables with a flow summary.
+ */
+class DataFlowCall extends TDataFlowCall {
+  /**
+   * Gets the underlying data flow call instruction, if any.
+   */
+  CallInstruction asCallInstruction() { none() }
+
+  /**
+   * Gets the operand the specifies the target function of the call.
+   */
+  CallTargetOperand getCallTargetOperand() { none() }
+
+  /**
+   * Gets the `Function` that the call targets, if this is statically known.
+   */
+  DataFlowCallable getStaticCallTarget() { none() }
+
+  /**
+   * Gets the `index`'th argument operand. The qualifier is considered to have index `-1`.
+   */
+  ArgumentOperand getArgumentOperand(int index) { none() }
+
+  /**
+   * Gets the argument at the specified index, or `this` if `index` is `-1`.
+   */
+  pragma[noinline]
+  final Instruction getArgument(int index) { result = this.getArgumentOperand(index).getDef() }
+
+  /**
+   * Gets the number of arguments of the call, including the `this` pointer, if any.
+   */
+  final int getNumberOfArguments() { result = count(this.getArgumentOperand(_)) }
+
+  /**
+   * Gets the enclosing callable, if any.
+   */
+  DataFlowCallable getEnclosingCallable() { none() }
+
+  /**
+   * Gets a textual representation of this call.
+   */
+  string toString() { none() }
+
+  /**
+   * Gets the location of this call.
+   */
+  Location getLocation() { none() }
+}
+
+/**
+ * A function call relevant for data flow, that exists in source code.
+ */
+private class NormalCall extends DataFlowCall, TNormalCall {
+  private CallInstruction call;
+
+  NormalCall() { this = TNormalCall(call) }
+
+  override CallInstruction asCallInstruction() { result = call }
+
+  override CallTargetOperand getCallTargetOperand() { result = call.getCallTargetOperand() }
+
+  override DataFlowCallable getStaticCallTarget() {
+    result.getUnderlyingCallable() = call.getStaticCallTarget()
+  }
+
+  override ArgumentOperand getArgumentOperand(int index) { result = call.getArgumentOperand(index) }
+
+  override DataFlowCallable getEnclosingCallable() {
+    result.getUnderlyingCallable() = call.getEnclosingFunction()
+  }
+
+  override string toString() { result = call.toString() }
+
+  override Location getLocation() { result = call.getLocation() }
+}
+
+/**
+ * A synthesized call inside a callable with a flow summary.
+ *
+ * For example, consider the function:
+ * ```
+ * int myFunction(int (*funPtr)());
+ * ```
+ * with an accompanying models-as-data flow summary involving `funPtr` (for
+ * example from `Argument[0].ReturnValue` to `ReturnValue`). A `SummaryCall`
+ * will be synthesized representing a call to `funPtr` inside `myFunction`,
+ * so that flow can be connected as described in the model.
+ */
+class SummaryCall extends DataFlowCall, TSummaryCall {
+  private FlowSummaryImpl::Public::SummarizedCallable c;
+  private FlowSummaryImpl::Private::SummaryNode receiver;
+
+  SummaryCall() { this = TSummaryCall(c, receiver) }
+
+  /**
+   * Gets the data flow node that holds the address of the function this call
+   * targets.
+   */
+  FlowSummaryImpl::Private::SummaryNode getReceiver() { result = receiver }
+
+  // no implementation for `getCallTargetOperand()`, `getStaticCallTarget()`
+  // or `getArgumentOperand(int index)`. This is because the flow summary
+  // library is responsible for finding the call target, and there are no
+  // IR nodes available for the call target operand or argument operands.
+  override DataFlowCallable getEnclosingCallable() { result = TSummarizedCallable(c) }
+
+  override string toString() { result = "[summary] call to " + receiver + " in " + c }
+
+  override UnknownLocation getLocation() { any() }
 }
 
 module IsUnreachableInCall {
@@ -950,7 +1249,7 @@ module IsUnreachableInCall {
 
   predicate isUnreachableInCall(Node n, DataFlowCall call) {
     exists(
-      DirectParameterNode paramNode, ConstantIntegralTypeArgumentNode arg,
+      InstructionDirectParameterNode paramNode, ConstantIntegralTypeArgumentNode arg,
       IntegerConstantInstruction constant, int k, Operand left, Operand right, IRBlock block
     |
       // arg flows into `paramNode`
@@ -1009,17 +1308,34 @@ predicate nodeIsHidden(Node n) {
   n instanceof InitialGlobalValue
 }
 
+predicate neverSkipInPathGraph(Node n) {
+  // Always show the right-hand side of assignments in the path graph
+  exists(n.asDefinition())
+  or
+  exists(n.asIndirectDefinition())
+}
+
 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() }
+predicate lambdaCreation(Node creation, LambdaCallKind kind, DataFlowCallable c) {
+  creation.asInstruction().(FunctionAddressInstruction).getFunctionSymbol() = c.asSourceCallable() and
+  exists(kind)
+}
 
 /** 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() }
+predicate lambdaCall(DataFlowCall call, LambdaCallKind kind, Node receiver) {
+  call.(SummaryCall).getReceiver() = receiver.(FlowSummaryNode).getSummaryNode() and
+  exists(kind)
+}
 
 /** Extra data-flow steps needed for lambda flow analysis. */
 predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preservesValue) { none() }
 
+predicate knownSourceModel(Node source, string model) { none() }
+
+predicate knownSinkModel(Node sink, string model) { none() }
+
 /**
  * Holds if flow is allowed to pass from parameter `p` and back to itself as a
  * side-effect, resulting in a summary from `p` to itself.
@@ -1027,7 +1343,15 @@ predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preserves
  * One example would be to allow flow like `p.foo = p.bar;`, which is disallowed
  * by default as a heuristic.
  */
-predicate allowParameterReturnInSelf(ParameterNode p) { p instanceof IndirectParameterNode }
+predicate allowParameterReturnInSelf(ParameterNode p) {
+  p instanceof IndirectParameterNode
+  or
+  // models-as-data summarized flow
+  exists(DataFlowCallable c, ParameterPosition pos |
+    p.isParameterOf(c, pos) and
+    FlowSummaryImpl::Private::summaryAllowParameterReturnInSelf(c.asSummarizedCallable(), pos)
+  )
+}
 
 private predicate fieldHasApproxName(Field f, string s) {
   s = f.getName().charAt(0) and
@@ -1096,7 +1420,7 @@ private predicate localFlowStepWithSummaries(Node node1, Node node2) {
   or
   readStep(node1, _, node2)
   or
-  DataFlowImplCommon::argumentValueFlowsThrough(node1, _, node2)
+  DataFlowImplCommon::argumentValueFlowsThrough(node1, _, node2, _)
 }
 
 /** Holds if `node` flows to a node that is used in a `SwitchInstruction`. */
@@ -1139,7 +1463,7 @@ private predicate getAdditionalFlowIntoCallNodeTermStep(Node node1, Node node2)
 /** Gets the `IRVariable` associated with the parameter node `p`. */
 pragma[nomagic]
 private IRVariable getIRVariableForParameterNode(ParameterNode p) {
-  result = p.(DirectParameterNode).getIRVariable()
+  result = p.(InstructionDirectParameterNode).getIRVariable()
   or
   result.getAst() = p.(IndirectParameterNode).getParameter()
 }
@@ -1259,3 +1583,85 @@ predicate validParameterAliasStep(Node node1, Node node2) {
     )
   )
 }
+
+private predicate isTopLevel(Cpp::Stmt s) { any(Function f).getBlock().getAStmt() = s }
+
+private Cpp::Stmt getAChainedBranch(Cpp::IfStmt s) {
+  result = s.getThen()
+  or
+  exists(Cpp::Stmt elseBranch | s.getElse() = elseBranch |
+    result = getAChainedBranch(elseBranch)
+    or
+    result = elseBranch and not elseBranch instanceof Cpp::IfStmt
+  )
+}
+
+private Instruction getAnInstruction(Node n) {
+  result = n.asInstruction()
+  or
+  not n instanceof InstructionNode and
+  result = n.asOperand().getUse()
+  or
+  result = n.(SsaPhiNode).getPhiNode().getBasicBlock().getFirstInstruction()
+  or
+  n.(IndirectInstruction).hasInstructionAndIndirectionIndex(result, _)
+  or
+  not n instanceof IndirectInstruction and
+  exists(Operand operand |
+    n.(IndirectOperand).hasOperandAndIndirectionIndex(operand, _) and
+    result = operand.getUse()
+  )
+  or
+  result = getAnInstruction(n.(PostUpdateNode).getPreUpdateNode())
+}
+
+private newtype TDataFlowSecondLevelScope =
+  TTopLevelIfBranch(Cpp::Stmt s) {
+    exists(Cpp::IfStmt ifstmt | s = getAChainedBranch(ifstmt) and isTopLevel(ifstmt))
+  } or
+  TTopLevelSwitchCase(Cpp::SwitchCase s) {
+    exists(Cpp::SwitchStmt switchstmt | s = switchstmt.getASwitchCase() and isTopLevel(switchstmt))
+  }
+
+/**
+ * A second-level control-flow scope in a `switch` or a chained `if` statement.
+ *
+ * This is a `switch` case or a branch of a chained `if` statement, given that
+ * the `switch` or `if` statement is top level, that is, it is not nested inside
+ * other CFG constructs.
+ */
+class DataFlowSecondLevelScope extends TDataFlowSecondLevelScope {
+  /** Gets a textual representation of this element. */
+  string toString() {
+    exists(Cpp::Stmt s | this = TTopLevelIfBranch(s) | result = s.toString())
+    or
+    exists(Cpp::SwitchCase s | this = TTopLevelSwitchCase(s) | result = s.toString())
+  }
+
+  /** Gets the primary location of this element. */
+  Cpp::Location getLocation() {
+    exists(Cpp::Stmt s | this = TTopLevelIfBranch(s) | result = s.getLocation())
+    or
+    exists(Cpp::SwitchCase s | this = TTopLevelSwitchCase(s) | result = s.getLocation())
+  }
+
+  /**
+   * Gets a statement directly contained in this scope. For an `if` branch, this
+   * is the branch itself, and for a `switch case`, this is one the statements
+   * of that case branch.
+   */
+  private Cpp::Stmt getAStmt() {
+    exists(Cpp::Stmt s | this = TTopLevelIfBranch(s) | result = s)
+    or
+    exists(Cpp::SwitchCase s | this = TTopLevelSwitchCase(s) | result = s.getAStmt())
+  }
+
+  /** Gets a data-flow node nested within this scope. */
+  Node getANode() {
+    getAnInstruction(result).getAst().(Cpp::ControlFlowNode).getEnclosingStmt().getParentStmt*() =
+      this.getAStmt()
+  }
+}
+
+/** Gets the second-level scope containing the node `n`, if any. */
+DataFlowSecondLevelScope getSecondLevelScope(Node n) { result.getANode() = n }

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

@@ -10,6 +10,7 @@ private import semmle.code.cpp.ir.ValueNumbering
 private import semmle.code.cpp.ir.IR
 private import semmle.code.cpp.controlflow.IRGuards
 private import semmle.code.cpp.models.interfaces.DataFlow
+private import semmle.code.cpp.dataflow.internal.FlowSummaryImpl as FlowSummaryImpl
 private import DataFlowPrivate
 private import ModelUtil
 private import SsaInternals as Ssa
@@ -59,7 +60,17 @@ private newtype TIRDataFlowNode =
     )
   } or
   TFinalGlobalValue(Ssa::GlobalUse globalUse) or
-  TInitialGlobalValue(Ssa::GlobalDef globalUse)
+  TInitialGlobalValue(Ssa::GlobalDef globalUse) or
+  TBodyLessParameterNodeImpl(Parameter p, int indirectionIndex) {
+    // Rule out parameters of catch blocks.
+    not exists(p.getCatchBlock()) and
+    // We subtract one because `getMaxIndirectionsForType` returns the maximum
+    // indirection for a glvalue of a given type, and this doesn't apply to
+    // parameters.
+    indirectionIndex = [0 .. Ssa::getMaxIndirectionsForType(p.getUnspecifiedType()) - 1] and
+    not any(InitializeParameterInstruction init).getParameter() = p
+  } or
+  TFlowSummaryNode(FlowSummaryImpl::Private::SummaryNode sn)
 
 /**
  * An operand that is defined by a `FieldAddressInstruction`.
@@ -387,7 +398,7 @@ class Node extends TIRDataFlowNode {
     index = 0 and
     result = this.(ExplicitParameterNode).getParameter()
     or
-    this.(IndirectParameterNode).hasInstructionAndIndirectionIndex(_, index) and
+    this.(IndirectParameterNode).getIndirectionIndex() = index and
     result = this.(IndirectParameterNode).getParameter()
   }
 
@@ -448,7 +459,7 @@ class Node extends TIRDataFlowNode {
    * For more information, see
    * [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
    */
-  predicate hasLocationInfo(
+  deprecated predicate hasLocationInfo(
     string filepath, int startline, int startcolumn, int endline, int endcolumn
   ) {
     this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
@@ -738,37 +749,65 @@ class InitialGlobalValue extends Node, TInitialGlobalValue {
 /**
  * INTERNAL: do not use.
  *
- * A node representing an indirection of a parameter.
+ * A node representing a parameter for a function with no body.
  */
-class IndirectParameterNode extends Node instanceof IndirectInstruction {
-  InitializeParameterInstruction init;
+class BodyLessParameterNodeImpl extends Node, TBodyLessParameterNodeImpl {
+  Parameter p;
+  int indirectionIndex;
 
-  IndirectParameterNode() { IndirectInstruction.super.hasInstructionAndIndirectionIndex(init, _) }
-
-  int getArgumentIndex() { init.hasIndex(result) }
-
-  /** Gets the parameter whose indirection is initialized. */
-  Parameter getParameter() { result = init.getParameter() }
+  BodyLessParameterNodeImpl() { this = TBodyLessParameterNodeImpl(p, indirectionIndex) }
 
   override Declaration getEnclosingCallable() { result = this.getFunction() }
 
-  override Declaration getFunction() { result = init.getEnclosingFunction() }
+  override Declaration getFunction() { result = p.getFunction() }
 
-  /** Gets the underlying operand and the underlying indirection index. */
-  predicate hasInstructionAndIndirectionIndex(Instruction instr, int index) {
-    IndirectInstruction.super.hasInstructionAndIndirectionIndex(instr, index)
+  /** Gets the indirection index of this node. */
+  int getIndirectionIndex() { result = indirectionIndex }
+
+  override DataFlowType getType() {
+    result = getTypeImpl(p.getUnderlyingType(), this.getIndirectionIndex())
   }
 
-  override Location getLocationImpl() { result = this.getParameter().getLocation() }
-
-  override string toStringImpl() {
-    exists(string prefix | prefix = stars(this) |
-      result = prefix + this.getParameter().toString()
-      or
-      not exists(this.getParameter()) and
-      result = prefix + "this"
-    )
+  final override Location getLocationImpl() {
+    result = unique( | | p.getLocation())
+    or
+    count(p.getLocation()) != 1 and
+    result instanceof UnknownDefaultLocation
   }
+
+  final override string toStringImpl() {
+    exists(string prefix | prefix = stars(this) | result = prefix + p.toString())
+  }
+}
+
+/**
+ * A data-flow node used to model flow summaries. That is, a dataflow node
+ * that is synthesized to represent a parameter, return value, or other part
+ * of a models-as-data modeled function.
+ */
+class FlowSummaryNode extends Node, TFlowSummaryNode {
+  /**
+   * Gets the models-as-data `SummaryNode` associated with this dataflow
+   * `FlowSummaryNode`.
+   */
+  FlowSummaryImpl::Private::SummaryNode getSummaryNode() { this = TFlowSummaryNode(result) }
+
+  /**
+   * Gets the summarized callable that this node belongs to.
+   */
+  FlowSummaryImpl::Public::SummarizedCallable getSummarizedCallable() {
+    result = this.getSummaryNode().getSummarizedCallable()
+  }
+
+  /**
+   * Gets the enclosing callable. For a `FlowSummaryNode` this is always the
+   * summarized function this node is part of.
+   */
+  override Declaration getEnclosingCallable() { result = this.getSummarizedCallable() }
+
+  override Location getLocationImpl() { result = this.getSummarizedCallable().getLocation() }
+
+  override string toStringImpl() { result = this.getSummaryNode().toString() }
 }
 
 /**
@@ -826,6 +865,9 @@ class IndirectArgumentOutNode extends PostUpdateNodeImpl {
 
   CallInstruction getCallInstruction() { result.getAnArgumentOperand() = operand }
 
+  /**
+   * Gets the `Function` that the call targets, if this is statically known.
+   */
   Function getStaticCallTarget() { result = this.getCallInstruction().getStaticCallTarget() }
 
   override string toStringImpl() {
@@ -1331,6 +1373,7 @@ private import GetConvertedResultExpression
 
 /** Holds if `node` is an `OperandNode` that should map `node.asExpr()` to `e`. */
 predicate exprNodeShouldBeOperand(OperandNode node, Expr e, int n) {
+  not exprNodeShouldBeIndirectOperand(_, e, n) and
   exists(Instruction def |
     unique( | | getAUse(def)) = node.getOperand() and
     e = getConvertedResultExpression(def, n)
@@ -1347,6 +1390,22 @@ private predicate indirectExprNodeShouldBeIndirectOperand(
   )
 }
 
+/** Holds if `node` should be an `IndirectOperand` that maps `node.asExpr()` to `e`. */
+private predicate exprNodeShouldBeIndirectOperand(IndirectOperand node, Expr e, int n) {
+  exists(ArgumentOperand operand |
+    // When an argument (qualifier or positional) is a prvalue and the
+    // parameter (qualifier or positional) is a (const) reference, IR
+    // construction introduces a temporary `IRVariable`. The `VariableAddress`
+    // instruction has the argument as its `getConvertedResultExpression`
+    // result. However, the instruction actually represents the _address_ of
+    // the argument. So to fix this mismatch, we have the indirection of the
+    // `VariableAddressInstruction` map to the expression.
+    node.hasOperandAndIndirectionIndex(operand, 1) and
+    e = getConvertedResultExpression(operand.getDef(), n) and
+    operand.getDef().(VariableAddressInstruction).getIRVariable() instanceof IRTempVariable
+  )
+}
+
 private predicate exprNodeShouldBeIndirectOutNode(IndirectArgumentOutNode node, Expr e, int n) {
   exists(CallInstruction call |
     call.getStaticCallTarget() instanceof Constructor and
@@ -1359,6 +1418,7 @@ private predicate exprNodeShouldBeIndirectOutNode(IndirectArgumentOutNode node,
 predicate exprNodeShouldBeInstruction(Node node, Expr e, int n) {
   not exprNodeShouldBeOperand(_, e, n) and
   not exprNodeShouldBeIndirectOutNode(_, e, n) and
+  not exprNodeShouldBeIndirectOperand(_, e, n) and
   e = getConvertedResultExpression(node.asInstruction(), n)
 }
 
@@ -1391,7 +1451,8 @@ abstract private class ExprNodeBase extends Node {
 private predicate exprNodeShouldBe(Expr e, int n) {
   exprNodeShouldBeInstruction(_, e, n) or
   exprNodeShouldBeOperand(_, e, n) or
-  exprNodeShouldBeIndirectOutNode(_, e, n)
+  exprNodeShouldBeIndirectOutNode(_, e, n) or
+  exprNodeShouldBeIndirectOperand(_, e, n)
 }
 
 private class InstructionExprNode extends ExprNodeBase, InstructionNode {
@@ -1533,6 +1594,12 @@ private class IndirectArgumentOutExprNode extends ExprNodeBase, IndirectArgument
   final override Expr getConvertedExpr(int n) { exprNodeShouldBeIndirectOutNode(this, result, n) }
 }
 
+private class IndirectOperandExprNode extends ExprNodeBase instanceof IndirectOperand {
+  IndirectOperandExprNode() { exprNodeShouldBeIndirectOperand(this, _, _) }
+
+  final override Expr getConvertedExpr(int n) { exprNodeShouldBeIndirectOperand(this, result, n) }
+}
+
 /**
  * An expression, viewed as a node in a data flow graph.
  */
@@ -1595,68 +1662,36 @@ class IndirectExprNode extends Node instanceof IndirectExprNodeBase {
   }
 }
 
-/**
- * The value of a parameter at function entry, viewed as a node in a data
- * flow graph. This includes both explicit parameters such as `x` in `f(x)`
- * and implicit parameters such as `this` in `x.f()`.
- *
- * To match a specific kind of parameter, consider using one of the subclasses
- * `ExplicitParameterNode`, `ThisParameterNode`, or
- * `ParameterIndirectionNode`.
- */
-class ParameterNode extends Node {
-  ParameterNode() {
-    // To avoid making this class abstract, we enumerate its values here
-    this.asInstruction() instanceof InitializeParameterInstruction
-    or
-    this instanceof IndirectParameterNode
-  }
-
+abstract private class AbstractParameterNode extends Node {
   /**
    * Holds if this node is the parameter of `f` at the specified position. The
    * implicit `this` parameter is considered to have position `-1`, and
    * pointer-indirection parameters are at further negative positions.
    */
-  predicate isParameterOf(Function f, ParameterPosition pos) { none() } // overridden by subclasses
+  abstract predicate isParameterOf(DataFlowCallable f, ParameterPosition pos);
 
   /** Gets the `Parameter` associated with this node, if it exists. */
   Parameter getParameter() { none() } // overridden by subclasses
 }
 
-/** An explicit positional parameter, including `this`, but not `...`. */
-class DirectParameterNode extends InstructionNode {
-  override InitializeParameterInstruction instr;
-
-  /**
-   * INTERNAL: Do not use.
-   *
-   * Gets the `IRVariable` that this parameter references.
-   */
-  IRVariable getIRVariable() { result = instr.getIRVariable() }
+abstract private class AbstractIndirectParameterNode extends AbstractParameterNode {
+  /** Gets the indirection index of this parameter node. */
+  abstract int getIndirectionIndex();
 }
 
-/** An explicit positional parameter, not including `this` or `...`. */
-private class ExplicitParameterNode extends ParameterNode, DirectParameterNode {
-  ExplicitParameterNode() { exists(instr.getParameter()) }
+/**
+ * INTERNAL: do not use.
+ *
+ * A node representing an indirection of a parameter.
+ */
+final class IndirectParameterNode = AbstractIndirectParameterNode;
 
-  override predicate isParameterOf(Function f, ParameterPosition pos) {
-    f.getParameter(pos.(DirectPosition).getIndex()) = instr.getParameter()
-  }
-
-  override string toStringImpl() { result = instr.getParameter().toString() }
-
-  override Parameter getParameter() { result = instr.getParameter() }
-}
-
-/** An implicit `this` parameter. */
-class ThisParameterNode extends ParameterNode, DirectParameterNode {
-  ThisParameterNode() { instr.getIRVariable() instanceof IRThisVariable }
-
-  override predicate isParameterOf(Function f, ParameterPosition pos) {
-    pos.(DirectPosition).getIndex() = -1 and instr.getEnclosingFunction() = f
-  }
-
-  override string toStringImpl() { result = "this" }
+pragma[noinline]
+private predicate indirectParameterNodeHasArgumentIndexAndIndex(
+  IndirectInstructionParameterNode node, int argumentIndex, int indirectionIndex
+) {
+  node.hasInstructionAndIndirectionIndex(_, indirectionIndex) and
+  node.getArgumentIndex() = argumentIndex
 }
 
 pragma[noinline]
@@ -1667,23 +1702,167 @@ private predicate indirectPositionHasArgumentIndexAndIndex(
   pos.getIndirectionIndex() = indirectionIndex
 }
 
-pragma[noinline]
-private predicate indirectParameterNodeHasArgumentIndexAndIndex(
-  IndirectParameterNode node, int argumentIndex, int indirectionIndex
-) {
-  node.hasInstructionAndIndirectionIndex(_, indirectionIndex) and
-  node.getArgumentIndex() = argumentIndex
-}
+private class IndirectInstructionParameterNode extends AbstractIndirectParameterNode instanceof IndirectInstruction
+{
+  InitializeParameterInstruction init;
 
-/** A synthetic parameter to model the pointed-to object of a pointer parameter. */
-class ParameterIndirectionNode extends ParameterNode instanceof IndirectParameterNode {
-  override predicate isParameterOf(Function f, ParameterPosition pos) {
-    IndirectParameterNode.super.getEnclosingCallable() = f and
+  IndirectInstructionParameterNode() {
+    IndirectInstruction.super.hasInstructionAndIndirectionIndex(init, _)
+  }
+
+  int getArgumentIndex() { init.hasIndex(result) }
+
+  override string toStringImpl() {
+    exists(string prefix | prefix = stars(this) |
+      result = prefix + this.getParameter().toString()
+      or
+      not exists(this.getParameter()) and
+      result = prefix + "this"
+    )
+  }
+
+  /** Gets the parameter whose indirection is initialized. */
+  override Parameter getParameter() { result = init.getParameter() }
+
+  override Declaration getEnclosingCallable() { result = this.getFunction() }
+
+  override Declaration getFunction() { result = init.getEnclosingFunction() }
+
+  override predicate isParameterOf(DataFlowCallable f, ParameterPosition pos) {
+    this.getEnclosingCallable() = f.getUnderlyingCallable() and
     exists(int argumentIndex, int indirectionIndex |
       indirectPositionHasArgumentIndexAndIndex(pos, argumentIndex, indirectionIndex) and
       indirectParameterNodeHasArgumentIndexAndIndex(this, argumentIndex, indirectionIndex)
     )
   }
+
+  /** Gets the underlying operand and the underlying indirection index. */
+  predicate hasInstructionAndIndirectionIndex(Instruction instr, int index) {
+    IndirectInstruction.super.hasInstructionAndIndirectionIndex(instr, index)
+  }
+
+  final override int getIndirectionIndex() { this.hasInstructionAndIndirectionIndex(init, result) }
+}
+
+/**
+ * The value of a parameter at function entry, viewed as a node in a data
+ * flow graph. This includes both explicit parameters such as `x` in `f(x)`
+ * and implicit parameters such as `this` in `x.f()`.
+ *
+ * To match a specific kind of parameter, consider using one of the subclasses
+ * `ExplicitParameterNode`, `ThisParameterNode`, or
+ * `ParameterIndirectionNode`.
+ */
+final class ParameterNode = AbstractParameterNode;
+
+abstract private class AbstractDirectParameterNode extends AbstractParameterNode { }
+
+/** An explicit positional parameter, including `this`, but not `...`. */
+final class DirectParameterNode = AbstractDirectParameterNode;
+
+/**
+ * INTERNAL: Do not use.
+ *
+ * A non-indirect parameter node that is represented as an `Instruction`.
+ */
+abstract class InstructionDirectParameterNode extends InstructionNode, AbstractDirectParameterNode {
+  final override InitializeParameterInstruction instr;
+
+  /**
+   * INTERNAL: Do not use.
+   *
+   * Gets the `IRVariable` that this parameter references.
+   */
+  final IRVariable getIRVariable() { result = instr.getIRVariable() }
+}
+
+abstract private class AbstractExplicitParameterNode extends AbstractDirectParameterNode { }
+
+final class ExplicitParameterNode = AbstractExplicitParameterNode;
+
+/** An explicit positional parameter, not including `this` or `...`. */
+private class ExplicitParameterInstructionNode extends AbstractExplicitParameterNode,
+  InstructionDirectParameterNode
+{
+  ExplicitParameterInstructionNode() { exists(instr.getParameter()) }
+
+  override predicate isParameterOf(DataFlowCallable f, ParameterPosition pos) {
+    f.getUnderlyingCallable().(Function).getParameter(pos.(DirectPosition).getIndex()) =
+      instr.getParameter()
+  }
+
+  override string toStringImpl() { result = instr.getParameter().toString() }
+
+  override Parameter getParameter() { result = instr.getParameter() }
+}
+
+/** An implicit `this` parameter. */
+class ThisParameterInstructionNode extends AbstractExplicitParameterNode,
+  InstructionDirectParameterNode
+{
+  ThisParameterInstructionNode() { instr.getIRVariable() instanceof IRThisVariable }
+
+  override predicate isParameterOf(DataFlowCallable f, ParameterPosition pos) {
+    pos.(DirectPosition).getIndex() = -1 and
+    instr.getEnclosingFunction() = f.getUnderlyingCallable()
+  }
+
+  override string toStringImpl() { result = "this" }
+}
+
+/**
+ * A parameter node that is part of a summary.
+ */
+class SummaryParameterNode extends AbstractParameterNode, FlowSummaryNode {
+  SummaryParameterNode() {
+    FlowSummaryImpl::Private::summaryParameterNode(this.getSummaryNode(), _)
+  }
+
+  private ParameterPosition getPosition() {
+    FlowSummaryImpl::Private::summaryParameterNode(this.getSummaryNode(), result)
+  }
+
+  override predicate isParameterOf(DataFlowCallable c, ParameterPosition p) {
+    c.getUnderlyingCallable() = this.getSummarizedCallable() and
+    p = this.getPosition()
+  }
+}
+
+private class DirectBodyLessParameterNode extends AbstractExplicitParameterNode,
+  BodyLessParameterNodeImpl
+{
+  DirectBodyLessParameterNode() { indirectionIndex = 0 }
+
+  override predicate isParameterOf(DataFlowCallable f, ParameterPosition pos) {
+    exists(Function func |
+      this.getFunction() = func and
+      f.asSourceCallable() = func and
+      func.getParameter(pos.(DirectPosition).getIndex()) = p
+    )
+  }
+
+  override Parameter getParameter() { result = p }
+}
+
+private class IndirectBodyLessParameterNode extends AbstractIndirectParameterNode,
+  BodyLessParameterNodeImpl
+{
+  IndirectBodyLessParameterNode() { not this instanceof DirectBodyLessParameterNode }
+
+  override predicate isParameterOf(DataFlowCallable f, ParameterPosition pos) {
+    exists(Function func, int argumentPosition |
+      this.getFunction() = func and
+      f.asSourceCallable() = func and
+      indirectPositionHasArgumentIndexAndIndex(pos, argumentPosition, indirectionIndex) and
+      func.getParameter(argumentPosition) = p
+    )
+  }
+
+  override int getIndirectionIndex() {
+    result = BodyLessParameterNodeImpl.super.getIndirectionIndex()
+  }
+
+  override Parameter getParameter() { result = p }
 }
 
 /**
@@ -1728,6 +1907,22 @@ abstract private class PartialDefinitionNode extends PostUpdateNode {
   abstract Expr getDefinedExpr();
 }
 
+/**
+ * A `PostUpdateNode` that is part of a flow summary. These are synthesized,
+ * for example, when a models-as-data summary models a write to a field since
+ * the write needs to target a `PostUpdateNode`.
+ */
+class SummaryPostUpdateNode extends FlowSummaryNode, PostUpdateNode {
+  SummaryPostUpdateNode() {
+    FlowSummaryImpl::Private::summaryPostUpdateNode(this.getSummaryNode(), _)
+  }
+
+  override Node getPreUpdateNode() {
+    FlowSummaryImpl::Private::summaryPostUpdateNode(this.getSummaryNode(),
+      result.(FlowSummaryNode).getSummaryNode())
+  }
+}
+
 /**
  * A node that represents the value of a variable after a function call that
  * may have changed the variable because it's passed by reference.
@@ -1864,10 +2059,20 @@ cached
 private module Cached {
   /**
    * Holds if data flows from `nodeFrom` to `nodeTo` in exactly one local
-   * (intra-procedural) step.
+   * (intra-procedural) step. This relation is only used for local dataflow
+   * (for example `DataFlow::localFlow(source, sink)`) so it contains
+   * special cases that should only apply to local dataflow.
    */
   cached
-  predicate localFlowStep(Node nodeFrom, Node nodeTo) { simpleLocalFlowStep(nodeFrom, nodeTo) }
+  predicate localFlowStep(Node nodeFrom, Node nodeTo) {
+    // common dataflow steps
+    simpleLocalFlowStep(nodeFrom, nodeTo, _)
+    or
+    // models-as-data summarized flow for local data flow (i.e. special case for flow
+    // through calls to modeled functions, without relying on global dataflow to join
+    // the dots).
+    FlowSummaryImpl::Private::Steps::summaryThroughStepValue(nodeFrom, nodeTo, _)
+  }
 
   private predicate indirectionOperandFlow(RawIndirectOperand nodeFrom, Node nodeTo) {
     nodeFrom != nodeTo and
@@ -1933,45 +2138,54 @@ private module Cached {
   /**
    * INTERNAL: do not use.
    *
-   * This is the local flow predicate that's used as a building block in global
-   * data flow. It may have less flow than the `localFlowStep` predicate.
+   * This is the local flow predicate that's used as a building block in both
+   * local and global data flow. It may have less flow than the `localFlowStep`
+   * predicate.
    */
   cached
-  predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo) {
-    // Post update node -> Node flow
-    Ssa::postUpdateFlow(nodeFrom, nodeTo)
-    or
-    // Def-use/Use-use flow
-    Ssa::ssaFlow(nodeFrom, nodeTo)
-    or
-    // Operand -> Instruction flow
-    simpleInstructionLocalFlowStep(nodeFrom.asOperand(), nodeTo.asInstruction())
-    or
-    // Instruction -> Operand flow
-    exists(Instruction iFrom, Operand opTo |
-      iFrom = nodeFrom.asInstruction() and opTo = nodeTo.asOperand()
-    |
-      simpleOperandLocalFlowStep(iFrom, opTo) and
-      // Omit when the instruction node also represents the operand.
-      not iFrom = Ssa::getIRRepresentationOfOperand(opTo)
-    )
-    or
-    // Phi node -> Node flow
-    Ssa::fromPhiNode(nodeFrom, nodeTo)
-    or
-    // Indirect operand -> (indirect) instruction flow
-    indirectionOperandFlow(nodeFrom, nodeTo)
-    or
-    // Indirect instruction -> indirect operand flow
-    indirectionInstructionFlow(nodeFrom, nodeTo)
+  predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo, string model) {
+    (
+      // Post update node -> Node flow
+      Ssa::postUpdateFlow(nodeFrom, nodeTo)
+      or
+      // Def-use/Use-use flow
+      Ssa::ssaFlow(nodeFrom, nodeTo)
+      or
+      // Operand -> Instruction flow
+      simpleInstructionLocalFlowStep(nodeFrom.asOperand(), nodeTo.asInstruction())
+      or
+      // Instruction -> Operand flow
+      exists(Instruction iFrom, Operand opTo |
+        iFrom = nodeFrom.asInstruction() and opTo = nodeTo.asOperand()
+      |
+        simpleOperandLocalFlowStep(iFrom, opTo) and
+        // Omit when the instruction node also represents the operand.
+        not iFrom = Ssa::getIRRepresentationOfOperand(opTo)
+      )
+      or
+      // Phi node -> Node flow
+      Ssa::fromPhiNode(nodeFrom, nodeTo)
+      or
+      // Indirect operand -> (indirect) instruction flow
+      indirectionOperandFlow(nodeFrom, nodeTo)
+      or
+      // Indirect instruction -> indirect operand flow
+      indirectionInstructionFlow(nodeFrom, nodeTo)
+    ) and
+    model = ""
     or
     // Flow through modeled functions
-    modelFlow(nodeFrom, nodeTo)
+    modelFlow(nodeFrom, nodeTo, model)
     or
     // Reverse flow: data that flows from the definition node back into the indirection returned
     // by a function. This allows data to flow 'in' through references returned by a modeled
     // function such as `operator[]`.
-    reverseFlow(nodeFrom, nodeTo)
+    reverseFlow(nodeFrom, nodeTo) and
+    model = ""
+    or
+    // models-as-data summarized flow
+    FlowSummaryImpl::Private::Steps::summaryLocalStep(nodeFrom.(FlowSummaryNode).getSummaryNode(),
+      nodeTo.(FlowSummaryNode).getSummaryNode(), true, model)
   }
 
   private predicate simpleInstructionLocalFlowStep(Operand opFrom, Instruction iTo) {
@@ -1986,12 +2200,13 @@ private module Cached {
     opTo.getDef() = iFrom
   }
 
-  private predicate modelFlow(Node nodeFrom, Node nodeTo) {
+  private predicate modelFlow(Node nodeFrom, Node nodeTo, string model) {
     exists(
       CallInstruction call, DataFlowFunction func, FunctionInput modelIn, FunctionOutput modelOut
     |
       call.getStaticCallTarget() = func and
-      func.hasDataFlow(modelIn, modelOut)
+      func.hasDataFlow(modelIn, modelOut) and
+      model = "DataFlowFunction"
     |
       nodeFrom = callInput(call, modelIn) and
       nodeTo = callOutput(call, modelOut)
@@ -2212,6 +2427,8 @@ private Field getAFieldWithSize(Union u, int bytes) {
 cached
 private newtype TContent =
   TFieldContent(Field f, int indirectionIndex) {
+    // the indirection index for field content starts at 1 (because `TFieldContent` is thought of as
+    // the address of the field, `FieldAddress` in the IR).
     indirectionIndex = [1 .. Ssa::getMaxIndirectionsForType(f.getUnspecifiedType())] and
     // Reads and writes of union fields are tracked using `UnionContent`.
     not f.getDeclaringType() instanceof Union
@@ -2221,7 +2438,8 @@ private newtype TContent =
       f = u.getAField() and
       bytes = getFieldSize(f) and
       // We key `UnionContent` by the union instead of its fields since a write to one
-      // field can be read by any read of the union's fields.
+      // field can be read by any read of the union's fields. Again, the indirection index
+      // is 1-based (because 0 is considered the address).
       indirectionIndex =
         [1 .. max(Ssa::getMaxIndirectionsForType(getAFieldWithSize(u, bytes).getUnspecifiedType()))]
     )
@@ -2255,16 +2473,14 @@ class Content extends TContent {
   abstract predicate impliesClearOf(Content c);
 }
 
+/**
+ * Gets a string consisting of `n` star characters ("*"), where n >= 0. This is
+ * used to represent indirection.
+ */
+bindingset[n]
+string repeatStars(int n) { result = concat(int i | i in [1 .. n] | "*") }
+
 private module ContentStars {
-  private int maxNumberOfIndirections() { result = max(any(Content c).getIndirectionIndex()) }
-
-  private string repeatStars(int n) {
-    n = 0 and result = ""
-    or
-    n = [1 .. maxNumberOfIndirections()] and
-    result = "*" + repeatStars(n - 1)
-  }
-
   /**
    * Gets the number of stars (i.e., `*`s) needed to produce the `toString`
    * output for `c`.
@@ -2276,8 +2492,8 @@ private import ContentStars
 
 /** A reference through a non-union instance field. */
 class FieldContent extends Content, TFieldContent {
-  Field f;
-  int indirectionIndex;
+  private Field f;
+  private int indirectionIndex;
 
   FieldContent() { this = TFieldContent(f, indirectionIndex) }
 
@@ -2304,9 +2520,9 @@ class FieldContent extends Content, TFieldContent {
 
 /** A reference through an instance field of a union. */
 class UnionContent extends Content, TUnionContent {
-  Union u;
-  int indirectionIndex;
-  int bytes;
+  private Union u;
+  private int indirectionIndex;
+  private int bytes;
 
   UnionContent() { this = TUnionContent(u, bytes, indirectionIndex) }
 
@@ -2344,6 +2560,12 @@ class UnionContent extends Content, TUnionContent {
  * stored into (`getAStoreContent`) or read from (`getAReadContent`).
  */
 class ContentSet instanceof Content {
+  /**
+   * Holds if this content set is the singleton `{c}`. At present, this is
+   * the only kind of content set supported in C/C++.
+   */
+  predicate isSingleton(Content c) { this = c }
+
   /** Gets a content that may be stored into when storing into this set. */
   Content getAStoreContent() { result = this }
 
@@ -2561,5 +2783,5 @@ class AdditionalCallTarget extends Unit {
   /**
    * Gets a viable target for `call`.
    */
-  abstract DataFlowCallable viableTarget(Call call);
+  abstract Declaration viableTarget(Call call);
 }

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

@@ -3,12 +3,26 @@
  * `toString` for `Instruction` and `Operand` dataflow nodes.
  */
 
+private import cpp
 private import semmle.code.cpp.ir.IR
 private import codeql.util.Unit
 private import Node0ToString
 private import DataFlowUtil
 private import DataFlowPrivate
 
+/**
+ * Gets the string representation of the unconverted expression `loc` if
+ * `loc` is an `Expression`.
+ *
+ * Otherwise, this gets the string representation of `loc`.
+ */
+private string unconvertedAstToString(Locatable loc) {
+  result = loc.(Expr).getUnconverted().toString()
+  or
+  not loc instanceof Expr and
+  result = loc.toString()
+}
+
 private class NormalNode0ToString extends Node0ToString {
   NormalNode0ToString() {
     // Silence warning about `this` not being bound.
@@ -18,14 +32,10 @@ private class NormalNode0ToString extends Node0ToString {
   override string instructionToString(Instruction i) {
     if i.(InitializeParameterInstruction).getIRVariable() instanceof IRThisVariable
     then result = "this"
-    else result = i.getAst().toString()
+    else result = unconvertedAstToString(i.getAst())
   }
 
-  override string operandToString(Operand op) {
-    if op.getDef().(InitializeParameterInstruction).getIRVariable() instanceof IRThisVariable
-    then result = "this"
-    else result = op.getDef().getAst().toString()
-  }
+  override string operandToString(Operand op) { result = this.instructionToString(op.getDef()) }
 
   override string toExprString(Node n) {
     result = n.asExpr(0).toString()

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

@@ -10,7 +10,7 @@ private import PrintIRUtilities
  */
 private string getFromFlow(Node node2, int order1, int order2) {
   exists(Node node1 |
-    simpleLocalFlowStep(node1, node2) and
+    simpleLocalFlowStep(node1, node2, _) and
     result = nodeId(node1, order1, order2)
   )
 }
@@ -20,7 +20,7 @@ private string getFromFlow(Node node2, int order1, int order2) {
  */
 private string getToFlow(Node node1, int order1, int order2) {
   exists(Node node2 |
-    simpleLocalFlowStep(node1, node2) and
+    simpleLocalFlowStep(node1, node2, _) and
     result = nodeId(node2, order1, order2)
   )
 }

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

@@ -10,27 +10,17 @@ private import semmle.code.cpp.models.interfaces.FunctionInputsAndOutputs as FIO
 private import semmle.code.cpp.ir.internal.IRCppLanguage
 private import semmle.code.cpp.ir.dataflow.internal.ModelUtil
 private import DataFlowPrivate
-private import ssa0.SsaInternals as SsaInternals0
 import SsaInternalsCommon
 
 private module SourceVariables {
   cached
   private newtype TSourceVariable =
-    TMkSourceVariable(SsaInternals0::SourceVariable base, int ind) {
+    TMkSourceVariable(BaseSourceVariable base, int ind) {
       ind = [0 .. countIndirectionsForCppType(base.getLanguageType()) + 1]
     }
 
-  private int maxNumberOfIndirections() { result = max(SourceVariable sv | | sv.getIndirection()) }
-
-  private string repeatStars(int n) {
-    n = 0 and result = ""
-    or
-    n = [1 .. maxNumberOfIndirections()] and
-    result = "*" + repeatStars(n - 1)
-  }
-
   class SourceVariable extends TSourceVariable {
-    SsaInternals0::SourceVariable base;
+    BaseSourceVariable base;
     int ind;
 
     SourceVariable() { this = TMkSourceVariable(base, ind) }
@@ -42,7 +32,7 @@ private module SourceVariables {
      * Gets the base source variable (i.e., the variable without any
      * indirections) of this source variable.
      */
-    SsaInternals0::SourceVariable getBaseVariable() { result = base }
+    BaseSourceVariable getBaseVariable() { result = base }
 
     /** Gets a textual representation of this element. */
     string toString() { result = repeatStars(this.getIndirection()) + base.toString() }
@@ -75,19 +65,28 @@ private module SourceVariables {
 import SourceVariables
 
 /**
- * Holds if the `(operand, indirectionIndex)` columns should be
- * assigned a `RawIndirectOperand` value.
+ * Holds if `indirectionIndex` is a valid non-zero indirection index for
+ * operand `op`. That is, `indirectionIndex` is between 1 and the maximum
+ * indirection for the operand's type.
  */
-predicate hasRawIndirectOperand(Operand op, int indirectionIndex) {
+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] and
-    not hasIRRepresentationOfIndirectOperand(op, indirectionIndex, _, _)
+    indirectionIndex = [1 .. m]
   )
 }
 
+/**
+ * Holds if the `(operand, indirectionIndex)` columns should be
+ * assigned a `RawIndirectOperand` value.
+ */
+predicate hasRawIndirectOperand(Operand op, int indirectionIndex) {
+  hasIndirectOperand(op, indirectionIndex) and
+  not hasIRRepresentationOfIndirectOperand(op, indirectionIndex, _, _)
+}
+
 /**
  * Holds if the `(instr, indirectionIndex)` columns should be
  * assigned a `RawIndirectInstruction` value.
@@ -104,17 +103,9 @@ predicate hasRawIndirectInstruction(Instruction instr, int indirectionIndex) {
 
 cached
 private newtype TDefOrUseImpl =
+  TDefAddressImpl(BaseIRVariable v) or
   TDefImpl(BaseSourceVariableInstruction base, Operand address, int indirectionIndex) {
-    isDef(_, _, address, base, _, 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
-      // Since the pruning stage doesn't know about global variables we can't use the above check to
-      // rule out dead assignments to globals.
-      base.(VariableAddressInstruction).getAstVariable() instanceof GlobalLikeVariable
-    )
+    isDef(_, _, address, base, _, indirectionIndex)
   } or
   TUseImpl(BaseSourceVariableInstruction base, Operand operand, int indirectionIndex) {
     isUse(_, operand, base, _, indirectionIndex) and
@@ -133,8 +124,7 @@ private newtype TDefOrUseImpl =
   TIteratorDef(
     Operand iteratorDerefAddress, BaseSourceVariableInstruction container, int indirectionIndex
   ) {
-    isIteratorDef(container, iteratorDerefAddress, _, _, indirectionIndex) and
-    any(SsaInternals0::Def def | def.isIteratorDef()).getAddressOperand() = iteratorDerefAddress
+    isIteratorDef(container, iteratorDerefAddress, _, _, indirectionIndex)
   } or
   TIteratorUse(
     Operand iteratorAddress, BaseSourceVariableInstruction container, int indirectionIndex
@@ -267,24 +257,64 @@ private predicate sourceVariableHasBaseAndIndex(SourceVariable v, BaseSourceVari
 }
 
 abstract class DefImpl extends DefOrUseImpl {
-  Operand address;
   int ind;
 
   bindingset[ind]
   DefImpl() { any() }
 
-  abstract int getIndirection();
-
-  abstract Node0Impl getValue();
-
-  abstract predicate isCertain();
-
-  Operand getAddressOperand() { result = address }
-
   override int getIndirectionIndex() { result = ind }
 
   override string toString() { result = "Def of " + this.getSourceVariable() }
 
+  abstract int getIndirection();
+
+  abstract predicate isCertain();
+
+  abstract Node0Impl getValue();
+}
+
+/** An initial definition of an `IRVariable`'s address. */
+private class DefAddressImpl extends DefImpl, TDefAddressImpl {
+  BaseIRVariable v;
+
+  DefAddressImpl() {
+    this = TDefAddressImpl(v) and
+    ind = 0
+  }
+
+  final override int getIndirection() { result = 0 }
+
+  final override predicate isCertain() { any() }
+
+  final override Node0Impl getValue() { none() }
+
+  final override predicate hasIndexInBlock(IRBlock block, int index) {
+    block = v.getIRVariable().getEnclosingIRFunction().getEntryBlock() and
+    index = 0
+  }
+
+  override Cpp::Location getLocation() { result = v.getIRVariable().getLocation() }
+
+  final override SourceVariable getSourceVariable() {
+    result.getBaseVariable() = v and
+    result.getIndirection() = 0
+  }
+
+  final override BaseSourceVariableInstruction getBase() { none() }
+}
+
+/**
+ * An SSA definition that has an associated `Operand` representing the address
+ * that is being written to.
+ */
+abstract private class OperandBasedDef extends DefImpl {
+  Operand address;
+
+  bindingset[ind]
+  OperandBasedDef() { any() }
+
+  Operand getAddressOperand() { result = address }
+
   override Cpp::Location getLocation() { result = this.getAddressOperand().getUse().getLocation() }
 
   final override predicate hasIndexInBlock(IRBlock block, int index) {
@@ -292,7 +322,7 @@ abstract class DefImpl extends DefOrUseImpl {
   }
 }
 
-private class DirectDef extends DefImpl, TDefImpl {
+private class DirectDef extends OperandBasedDef, TDefImpl {
   BaseSourceVariableInstruction base;
 
   DirectDef() { this = TDefImpl(base, address, ind) }
@@ -306,7 +336,7 @@ private class DirectDef extends DefImpl, TDefImpl {
   override predicate isCertain() { isDef(true, _, address, base, _, ind) }
 }
 
-private class IteratorDef extends DefImpl, TIteratorDef {
+private class IteratorDef extends OperandBasedDef, TIteratorDef {
   BaseSourceVariableInstruction container;
 
   IteratorDef() { this = TIteratorDef(address, container, ind) }
@@ -413,6 +443,8 @@ class FinalParameterUse extends UseImpl, TFinalParameterUse {
 
   Parameter getParameter() { result = p }
 
+  int getArgumentIndex() { result = p.getIndex() }
+
   override Node getNode() { finalParameterNodeHasParameterAndIndex(result, p, ind) }
 
   override int getIndirection() { result = ind + 1 }
@@ -861,7 +893,7 @@ private predicate isArgumentOfCallableInstruction(DataFlowCall call, Instruction
 }
 
 private predicate isArgumentOfCallableOperand(DataFlowCall call, Operand operand) {
-  operand.(ArgumentOperand).getCall() = call
+  operand = call.getArgumentOperand(_)
   or
   exists(FieldAddressInstruction fai |
     fai.getObjectAddressOperand() = operand and
@@ -984,17 +1016,6 @@ predicate fromPhiNode(SsaPhiNode nodeFrom, Node nodeTo) {
   )
 }
 
-/**
- * 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 = v.getBaseVariable()
-  )
-}
-
 private predicate sourceVariableIsGlobal(
   SourceVariable sv, GlobalLikeVariable global, IRFunction func, int indirectionIndex
 ) {
@@ -1018,16 +1039,14 @@ private module SsaInput implements SsaImplCommon::InputSig<Location> {
   predicate variableWrite(IRBlock bb, int i, SourceVariable v, boolean certain) {
     DataFlowImplCommon::forceCachingInSameStage() and
     (
-      variableWriteCand(bb, i, v) or
-      sourceVariableIsGlobal(v, _, _, _)
-    ) and
-    exists(DefImpl def | def.hasIndexInBlock(bb, i, v) |
-      if def.isCertain() then certain = true else certain = false
-    )
-    or
-    exists(GlobalDefImpl global |
-      global.hasIndexInBlock(bb, i, v) and
-      certain = true
+      exists(DefImpl def | def.hasIndexInBlock(bb, i, v) |
+        if def.isCertain() then certain = true else certain = false
+      )
+      or
+      exists(GlobalDefImpl global |
+        global.hasIndexInBlock(bb, i, v) and
+        certain = true
+      )
     )
   }
 
@@ -1202,7 +1221,7 @@ class UseOrPhi extends SsaDefOrUse {
 class Def extends DefOrUse {
   override DefImpl defOrUse;
 
-  Operand getAddressOperand() { result = defOrUse.getAddressOperand() }
+  Operand getAddressOperand() { result = defOrUse.(OperandBasedDef).getAddressOperand() }
 
   Instruction getAddress() { result = this.getAddressOperand().getDef() }
 

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

@@ -6,6 +6,7 @@ private import DataFlowImplCommon as DataFlowImplCommon
 private import DataFlowUtil
 private import semmle.code.cpp.models.interfaces.PointerWrapper
 private import DataFlowPrivate
+private import TypeFlow
 private import semmle.code.cpp.ir.ValueNumbering
 
 /**
@@ -955,11 +956,7 @@ private module Cached {
    * Holds if the address computed by `operand` is guaranteed to write
    * to a specific address.
    */
-  private predicate isCertainAddress(Operand operand) {
-    valueNumberOfOperand(operand).getAnInstruction() instanceof VariableAddressInstruction
-    or
-    operand.getType() instanceof Cpp::ReferenceType
-  }
+  private predicate isCertainAddress(Operand operand) { isPointerToSingleObject(operand.getDef()) }
 
   /**
    * Holds if `address` is a use of an SSA variable rooted at `base`, and the

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

@@ -4,7 +4,8 @@
 
 private import codeql.dataflow.TaintTracking
 private import DataFlowImplSpecific
+private import semmle.code.cpp.Location
 
-module CppTaintTracking implements InputSig<CppDataFlow> {
+module CppTaintTracking implements InputSig<Location, CppDataFlow> {
   import TaintTrackingUtil
 }

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

@@ -6,15 +6,26 @@ private import semmle.code.cpp.models.interfaces.SideEffect
 private import DataFlowUtil
 private import DataFlowPrivate
 private import SsaInternals as Ssa
+private import semmle.code.cpp.dataflow.internal.FlowSummaryImpl as FlowSummaryImpl
+private import semmle.code.cpp.ir.dataflow.FlowSteps
 
 /**
  * Holds if taint propagates from `nodeFrom` to `nodeTo` in exactly one local
- * (intra-procedural) step.
+ * (intra-procedural) step. This relation is only used for local taint flow
+ * (for example `TaintTracking::localTaint(source, sink)`) so it may contain
+ * special cases that should only apply to local taint flow.
  */
 predicate localTaintStep(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
+  // dataflow step
   DataFlow::localFlowStep(nodeFrom, nodeTo)
   or
-  localAdditionalTaintStep(nodeFrom, nodeTo)
+  // taint flow step
+  localAdditionalTaintStep(nodeFrom, nodeTo, _)
+  or
+  // models-as-data summarized flow for local data flow (i.e. special case for flow
+  // through calls to modeled functions, without relying on global dataflow to join
+  // the dots).
+  FlowSummaryImpl::Private::Steps::summaryThroughStepTaint(nodeFrom, nodeTo, _)
 }
 
 /**
@@ -23,10 +34,11 @@ predicate localTaintStep(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
  * different objects.
  */
 cached
-predicate localAdditionalTaintStep(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
-  operandToInstructionTaintStep(nodeFrom.asOperand(), nodeTo.asInstruction())
+predicate localAdditionalTaintStep(DataFlow::Node nodeFrom, DataFlow::Node nodeTo, string model) {
+  operandToInstructionTaintStep(nodeFrom.asOperand(), nodeTo.asInstruction()) and
+  model = ""
   or
-  modeledTaintStep(nodeFrom, nodeTo)
+  modeledTaintStep(nodeFrom, nodeTo, model)
   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`
@@ -34,9 +46,22 @@ predicate localAdditionalTaintStep(DataFlow::Node nodeFrom, DataFlow::Node nodeT
   exists(PointerArithmeticInstruction pai, int indirectionIndex |
     nodeHasOperand(nodeFrom, pai.getAnOperand(), pragma[only_bind_into](indirectionIndex)) and
     hasInstructionAndIndex(nodeTo, pai, indirectionIndex + 1)
-  )
+  ) and
+  model = ""
   or
-  any(Ssa::Indirection ind).isAdditionalTaintStep(nodeFrom, nodeTo)
+  any(Ssa::Indirection ind).isAdditionalTaintStep(nodeFrom, nodeTo) and
+  model = ""
+  or
+  // models-as-data summarized flow
+  FlowSummaryImpl::Private::Steps::summaryLocalStep(nodeFrom.(FlowSummaryNode).getSummaryNode(),
+    nodeTo.(FlowSummaryNode).getSummaryNode(), false, model)
+  or
+  // object->field conflation for content that is a `TaintInheritingContent`.
+  exists(DataFlow::ContentSet f |
+    readStep(nodeFrom, f, nodeTo) and
+    f.getAReadContent() instanceof TaintInheritingContent
+  ) and
+  model = ""
 }
 
 /**
@@ -113,8 +138,8 @@ predicate localExprTaint(Expr e1, Expr 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)
+predicate defaultAdditionalTaintStep(DataFlow::Node src, DataFlow::Node sink, string model) {
+  localAdditionalTaintStep(src, sink, model)
 }
 
 /**
@@ -134,7 +159,7 @@ predicate defaultTaintSanitizer(DataFlow::Node node) { none() }
  * Holds if taint can flow from `nodeIn` to `nodeOut` through a call to a
  * modeled function.
  */
-predicate modeledTaintStep(DataFlow::Node nodeIn, DataFlow::Node nodeOut) {
+predicate modeledTaintStep(DataFlow::Node nodeIn, DataFlow::Node nodeOut, string model) {
   // Normal taint steps
   exists(CallInstruction call, TaintFunction func, FunctionInput modelIn, FunctionOutput modelOut |
     call.getStaticCallTarget() = func and
@@ -143,7 +168,8 @@ predicate modeledTaintStep(DataFlow::Node nodeIn, DataFlow::Node nodeOut) {
     nodeIn = callInput(call, modelIn) and nodeOut = callOutput(call, modelOut)
     or
     exists(int d | nodeIn = callInput(call, modelIn, d) and nodeOut = callOutput(call, modelOut, d))
-  )
+  ) and
+  model = "TaintFunction"
   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
@@ -160,7 +186,8 @@ predicate modeledTaintStep(DataFlow::Node nodeIn, DataFlow::Node nodeOut) {
     func.(TaintFunction).hasTaintFlow(modelIn, modelMidOut) and
     func.(DataFlowFunction).hasDataFlow(modelMidIn, modelOut) and
     modelMidOut.isParameterDeref(indexMid) and
-    modelMidIn.isParameter(indexMid)
+    modelMidIn.isParameter(indexMid) and
+    model = "TaintFunction"
   )
   or
   // Taint flow from a pointer argument to an output, when the model specifies flow from the deref
@@ -173,9 +200,11 @@ predicate modeledTaintStep(DataFlow::Node nodeIn, DataFlow::Node nodeOut) {
     indirectArgument.hasAddressOperandAndIndirectionIndex(nodeIn.asOperand(), _) and
     call.getStaticCallTarget() = func and
     (
-      func.(DataFlowFunction).hasDataFlow(modelIn, modelOut)
+      func.(DataFlowFunction).hasDataFlow(modelIn, modelOut) and
+      model = "DataFlowFunction"
       or
-      func.(TaintFunction).hasTaintFlow(modelIn, modelOut)
+      func.(TaintFunction).hasTaintFlow(modelIn, modelOut) and
+      model = "TaintFunction"
     ) and
     nodeOut = callOutput(call, modelOut)
   )

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

@@ -0,0 +1,278 @@
+private import cpp
+private import semmle.code.cpp.ir.IR
+private import codeql.typeflow.TypeFlow
+
+private module Input implements TypeFlowInput<Location> {
+  /** Holds if `alloc` dynamically allocates a single object. */
+  private predicate isSingleObjectAllocation(AllocationExpr alloc) {
+    // i.e., `new int`;
+    alloc instanceof NewExpr
+    or
+    // i.e., `malloc(sizeof(int))`
+    exists(SizeofTypeOperator sizeOf | sizeOf = alloc.getSizeExpr() |
+      not sizeOf.getTypeOperand().getUnspecifiedType() instanceof ArrayType
+    )
+  }
+
+  /**
+   * Holds if `i` is the result of a dynamic allocation.
+   *
+   * `isObject` is `true` if the allocation allocated a single object,
+   * and `false` otherwise.
+   */
+  private predicate isAllocation(Instruction i, boolean isObject) {
+    exists(AllocationExpr alloc | alloc = i.getUnconvertedResultExpression() |
+      if isSingleObjectAllocation(alloc) then isObject = true else isObject = false
+    )
+  }
+
+  private predicate hasExactSingleType(Instruction i) {
+    // The address of a variable is always a single object
+    i instanceof VariableAddressInstruction
+    or
+    // A reference always points to a single object
+    i.getResultLanguageType().hasUnspecifiedType(any(ReferenceType rt), false)
+    or
+    // `this` is never an array
+    i instanceof InitializeThisInstruction
+    or
+    // An allocation of a non-array object
+    isAllocation(i, true)
+  }
+
+  private predicate hasExactBufferType(Instruction i) {
+    // Anything with an array type is a buffer
+    i.getResultLanguageType().hasUnspecifiedType(any(ArrayType at), false)
+    or
+    // An allocation expression that we couldn't conclude allocated a single
+    // expression is assigned a buffer type.
+    isAllocation(i, false)
+  }
+
+  private newtype TTypeFlowNode =
+    TInstructionNode(Instruction i) or
+    TFunctionNode(IRFunction func)
+
+  abstract class TypeFlowNode extends TTypeFlowNode {
+    /** Gets a textual representation of this node. */
+    abstract string toString();
+
+    /**
+     * Gets the type of this node. This type may not be the most precise
+     * possible type, but will be used as a starting point of the analysis.
+     */
+    abstract Type getType();
+
+    /** Gets the location of this node. */
+    abstract Location getLocation();
+
+    /** Gets the underlying `Instruction` of this node, if any. */
+    Instruction asInstruction() { none() }
+
+    /** Gets the underlying `IRFunction` of this node, if any. */
+    IRFunction asFunction() { none() }
+
+    /** Holds if the value of this node is always null. */
+    abstract predicate isNullValue();
+  }
+
+  private class InstructionNode extends TypeFlowNode, TInstructionNode {
+    Instruction instr;
+
+    InstructionNode() { this = TInstructionNode(instr) }
+
+    override string toString() { result = instr.toString() }
+
+    override Type getType() {
+      if hasExactSingleType(instr) then result.isSingle() else result.isBuffer()
+    }
+
+    override Location getLocation() { result = instr.getLocation() }
+
+    override Instruction asInstruction() { result = instr }
+
+    override predicate isNullValue() {
+      instr.(ConstantInstruction).getValue() = "0" and
+      instr.getResultIRType() instanceof IRAddressType
+    }
+  }
+
+  /** Gets the `TypeFlowNode` corresponding to `i`. */
+  additional InstructionNode instructionNode(Instruction i) { result.asInstruction() = i }
+
+  private class FunctionNode extends TypeFlowNode, TFunctionNode {
+    IRFunction func;
+
+    FunctionNode() { this = TFunctionNode(func) }
+
+    override string toString() { result = func.toString() }
+
+    Instruction getReturnValueInstruction() {
+      result = func.getReturnInstruction().(ReturnValueInstruction).getReturnValue()
+    }
+
+    override Type getType() { result = instructionNode(this.getReturnValueInstruction()).getType() }
+
+    override Location getLocation() { result = func.getLocation() }
+
+    override IRFunction asFunction() { result = func }
+
+    override predicate isNullValue() {
+      instructionNode(this.getReturnValueInstruction()).isNullValue()
+    }
+  }
+
+  /**
+   * Gets an ultimiate definition of `phi`. That is, an input to `phi` that is
+   * not itself a `PhiInstruction`.
+   */
+  private Instruction getAnUltimateLocalDefinition(PhiInstruction phi) {
+    result = phi.getAnInput*() and not result instanceof PhiInstruction
+  }
+
+  /**
+   * Holds if this function is private (i.e., cannot be accessed outside its
+   * compilation unit). This means we can use a closed-world assumption about
+   * calls to this function.
+   */
+  private predicate isPrivate(Function func) {
+    // static functions have internal linkage
+    func.isStatic()
+    or
+    // anonymous namespaces have internal linkage
+    func.getNamespace().getParentNamespace*().isAnonymous()
+    or
+    // private member functions are only called internally from inside the class
+    func.(MemberFunction).isPrivate()
+  }
+
+  /**
+   * Holds if `arg` is an argument for the parameter `p` in a private callable.
+   */
+  pragma[nomagic]
+  private predicate privateParamArg(InitializeParameterInstruction p, Instruction arg) {
+    exists(CallInstruction call, int i, Function func |
+      call.getArgument(pragma[only_bind_into](i)) = arg and
+      func = call.getStaticCallTarget() and
+      func.getParameter(pragma[only_bind_into](i)) = p.getParameter() and
+      isPrivate(func)
+    )
+  }
+
+  predicate joinStep(TypeFlowNode n1, TypeFlowNode n2) {
+    // instruction -> phi
+    getAnUltimateLocalDefinition(n2.asInstruction()) = n1.asInstruction()
+    or
+    // return value -> function
+    n2.(FunctionNode).getReturnValueInstruction() = n1.asInstruction()
+    or
+    // function -> call
+    exists(Function func | func = n1.asFunction().getFunction() |
+      not func.isVirtual() and
+      n2.asInstruction().(CallInstruction).getStaticCallTarget() = func
+    )
+    or
+    // Argument -> parameter where the parameter's enclosing function
+    // is "private".
+    exists(Instruction arg, Instruction p |
+      privateParamArg(p, arg) and
+      n1.asInstruction() = arg and
+      n2.asInstruction() = p
+    )
+  }
+
+  /**
+   * Holds if knowing whether `i1` points to a single object or buffer implies
+   * knowing whether `i2` points to a single object or buffer.
+   */
+  private predicate instructionStep(Instruction i1, Instruction i2) {
+    i2.(CopyInstruction).getSourceValue() = i1
+    or
+    i2.(CopyValueInstruction).getSourceValue() = i1
+    or
+    i2.(ConvertInstruction).getUnary() = i1
+    or
+    i2.(CheckedConvertOrNullInstruction).getUnary() = i1
+    or
+    i2.(InheritanceConversionInstruction).getUnary() = i1
+    or
+    i2.(PointerArithmeticInstruction).getLeft() = i1
+  }
+
+  predicate step(TypeFlowNode n1, TypeFlowNode n2) {
+    instructionStep(n1.asInstruction(), n2.asInstruction())
+  }
+
+  predicate isNullValue(TypeFlowNode n) { n.isNullValue() }
+
+  private newtype TType =
+    TSingle() or
+    TBuffer()
+
+  class Type extends TType {
+    string toString() {
+      this.isSingle() and
+      result = "Single"
+      or
+      this.isBuffer() and
+      result = "Buffer"
+    }
+
+    /** Holds if this type is the type that represents a single object. */
+    predicate isSingle() { this = TSingle() }
+
+    /** Holds if this type is the type that represents a buffer. */
+    predicate isBuffer() { this = TBuffer() }
+
+    /**
+     * Gets a super type of this type, if any.
+     *
+     * The type relation is `Single <: Buffer`.
+     */
+    Type getASupertype() {
+      this.isSingle() and
+      result.isBuffer()
+    }
+  }
+
+  predicate exactTypeBase(TypeFlowNode n, Type t) {
+    exists(Instruction instr | instr = n.asInstruction() |
+      hasExactSingleType(instr) and t.isSingle()
+      or
+      hasExactBufferType(instr) and t.isBuffer()
+    )
+  }
+
+  pragma[nomagic]
+  private predicate upcastCand(TypeFlowNode n, Type t1, Type t2) {
+    exists(TypeFlowNode next |
+      step(n, next)
+      or
+      joinStep(n, next)
+    |
+      n.getType() = t1 and
+      next.getType() = t2 and
+      t1 != t2
+    )
+  }
+
+  private predicate upcast(TypeFlowNode n, Type t1) {
+    exists(Type t2 | upcastCand(n, t1, t2) |
+      // No need for transitive closure since the subtyping relation is just `Single <: Buffer`
+      t1.getASupertype() = t2
+    )
+  }
+
+  predicate typeFlowBaseCand(TypeFlowNode n, Type t) { upcast(n, t) }
+}
+
+private module TypeFlow = Make<Location, Input>;
+
+/**
+ * Holds if `i` is an instruction that computes an address that points to a
+ * single object (as opposed to pointing into a buffer).
+ */
+pragma[nomagic]
+predicate isPointerToSingleObject(Instruction i) {
+  TypeFlow::bestTypeFlow(Input::instructionNode(i), any(Input::Type t | t.isSingle()), _)
+}

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

@@ -1,347 +0,0 @@
-/**
- * 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 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 semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
-private import semmle.code.cpp.ir.dataflow.internal.DataFlowUtil
-private import semmle.code.cpp.ir.dataflow.internal.SsaInternalsCommon
-
-private module SourceVariables {
-  class SourceVariable extends BaseSourceVariable {
-    /**
-     * Gets the base source variable of this `SourceVariable`.
-     */
-    BaseSourceVariable getBaseVariable() { result = this }
-  }
-}
-
-import SourceVariables
-
-private newtype TDefOrUseImpl =
-  TDefImpl(Operand address) { isDef(_, _, address, _, _, _) } or
-  TUseImpl(Operand operand) {
-    isUse(_, operand, _, _, _) and
-    not isDef(true, _, operand, _, _, _)
-  } or
-  TIteratorDef(BaseSourceVariableInstruction container, Operand iteratorAddress) {
-    isIteratorDef(container, iteratorAddress, _, _, _)
-  } or
-  TIteratorUse(BaseSourceVariableInstruction container, Operand iteratorAddress) {
-    isIteratorUse(container, iteratorAddress, _, _)
-  } or
-  TFinalParameterUse(Parameter p) {
-    any(Indirection indirection).getType() = p.getUnspecifiedType()
-  }
-
-abstract private class DefOrUseImpl extends TDefOrUseImpl {
-  /** Gets a textual representation of this element. */
-  abstract string toString();
-
-  /** Gets the block of this definition or use. */
-  final IRBlock getBlock() { this.hasIndexInBlock(result, _) }
-
-  /** 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 BaseSourceVariableInstruction getBase();
-
-  final BaseSourceVariable getBaseSourceVariable() {
-    result = this.getBase().getBaseSourceVariable()
-  }
-
-  /** Gets the variable that is defined or used. */
-  final SourceVariable getSourceVariable() {
-    result.getBaseVariable() = this.getBaseSourceVariable()
-  }
-
-  abstract predicate isCertain();
-}
-
-abstract class DefImpl extends DefOrUseImpl {
-  Operand address;
-
-  Operand getAddressOperand() { result = address }
-
-  abstract Node0Impl getValue();
-
-  override string toString() { result = address.toString() }
-
-  override Cpp::Location getLocation() { result = this.getAddressOperand().getLocation() }
-
-  final override predicate hasIndexInBlock(IRBlock block, int index) {
-    this.getAddressOperand().getUse() = block.getInstruction(index)
-  }
-}
-
-private class DirectDef extends DefImpl, TDefImpl {
-  DirectDef() { this = TDefImpl(address) }
-
-  override BaseSourceVariableInstruction getBase() { isDef(_, _, address, result, _, _) }
-
-  override Node0Impl getValue() { isDef(_, result, address, _, _, _) }
-
-  override predicate isCertain() { isDef(true, _, address, _, _, _) }
-}
-
-private class IteratorDef extends DefImpl, TIteratorDef {
-  BaseSourceVariableInstruction container;
-
-  IteratorDef() { this = TIteratorDef(container, address) }
-
-  override BaseSourceVariableInstruction getBase() { result = container }
-
-  override Node0Impl getValue() { isIteratorDef(_, address, result, _, _) }
-
-  override predicate isCertain() { none() }
-}
-
-abstract class UseImpl extends DefOrUseImpl { }
-
-abstract private class OperandBasedUse extends UseImpl {
-  Operand operand;
-
-  override string toString() { result = operand.toString() }
-
-  final override predicate hasIndexInBlock(IRBlock block, int index) {
-    // Ideally, this would just be implemented as:
-    // ```
-    // operand.getUse() = block.getInstruction(index)
-    // ```
-    // but because the IR generated for a snippet such as
-    // ```
-    // int x = *p++;
-    // ```
-    // looks like
-    // ```
-    // r1(glval<int>)   = VariableAddress[x]  :
-    // r2(glval<int *>) = VariableAddress[p]  :
-    // r3(int *)        = Load[p]             : &:r2, m1
-    // r4(int)          = Constant[1]         :
-    // r5(int *)        = PointerAdd[4]       : r3, r4
-    // m3(int *)        = Store[p]            : &:r2, r5
-    // r6(int *)        = CopyValue           : r3
-    // r7(int)          = Load[?]             : &:r6, ~m2
-    // m2(int)          = Store[x]            : &:r1, r7
-    // ```
-    // we need to ensure that the `r3` operand of the `CopyValue` instruction isn't seen as a fresh use
-    // of `p` that happens after the increment. So if the base instruction of this use comes from a
-    // post-fix crement operation we set the index of the SSA use that wraps the `r3` operand at the
-    // `CopyValue` instruction to be the same index as the `r3` operand at the `PointerAdd` instruction.
-    // This ensures that the SSA library doesn't create flow from the `PointerAdd` to `r6`.
-    exists(BaseSourceVariableInstruction base | base = this.getBase() |
-      if base.getAst() = any(Cpp::PostfixCrementOperation c).getOperand()
-      then
-        exists(Operand op |
-          op =
-            min(Operand cand, int i |
-              isUse(_, cand, base, _, _) and
-              block.getInstruction(i) = cand.getUse()
-            |
-              cand order by i
-            ) and
-          block.getInstruction(index) = op.getUse()
-        )
-      else operand.getUse() = block.getInstruction(index)
-    )
-  }
-
-  final override Cpp::Location getLocation() { result = operand.getLocation() }
-}
-
-private class DirectUse extends OperandBasedUse, TUseImpl {
-  DirectUse() { this = TUseImpl(operand) }
-
-  override BaseSourceVariableInstruction getBase() { isUse(_, operand, result, _, _) }
-
-  override predicate isCertain() { isUse(true, operand, _, _, _) }
-}
-
-private class IteratorUse extends OperandBasedUse, TIteratorUse {
-  BaseSourceVariableInstruction container;
-
-  IteratorUse() { this = TIteratorUse(container, operand) }
-
-  override BaseSourceVariableInstruction getBase() { result = container }
-
-  override predicate isCertain() { none() }
-}
-
-private class FinalParameterUse extends UseImpl, TFinalParameterUse {
-  Parameter p;
-
-  FinalParameterUse() { this = TFinalParameterUse(p) }
-
-  override string toString() { result = p.toString() }
-
-  final override predicate hasIndexInBlock(IRBlock block, int index) {
-    // Ideally, this should always be a `ReturnInstruction`, but if
-    // someone forgets to write a `return` statement in a function
-    // with a non-void return type we generate an `UnreachedInstruction`.
-    // In this case we still want to generate flow out of such functions
-    // if they write to a parameter. So we pick the index of the
-    // `UnreachedInstruction` as the index of this use.
-    // Note that a function may have both a `ReturnInstruction` and an
-    // `UnreachedInstruction`. If that's the case this predicate will
-    // return multiple results. I don't think this is detrimental to
-    // performance, however.
-    exists(Instruction return |
-      return instanceof ReturnInstruction or
-      return instanceof UnreachedInstruction
-    |
-      block.getInstruction(index) = return and
-      return.getEnclosingFunction() = p.getFunction()
-    )
-  }
-
-  final override Cpp::Location getLocation() {
-    // Parameters can have multiple locations. When there's a unique location we use
-    // that one, but if multiple locations exist we default to an unknown location.
-    result = unique( | | p.getLocation())
-    or
-    not exists(unique( | | p.getLocation())) and
-    result instanceof UnknownDefaultLocation
-  }
-
-  override BaseSourceVariableInstruction getBase() {
-    exists(InitializeParameterInstruction init |
-      init.getParameter() = p and
-      // This is always a `VariableAddressInstruction`
-      result = init.getAnOperand().getDef()
-    )
-  }
-
-  override predicate isCertain() { any() }
-}
-
-private module SsaInput implements SsaImplCommon::InputSig<Location> {
-  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(DefinitionExt 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() }
-
-  Node0Impl getValue() { result = defOrUse.getValue() }
-
-  override string toString() { result = this.asDefOrUse().toString() }
-
-  BaseSourceVariableInstruction getBase() { result = defOrUse.getBase() }
-
-  predicate isIteratorDef() { defOrUse instanceof IteratorDef }
-}
-
-private module SsaImpl = SsaImplCommon::Make<Location, SsaInput>;
-
-class PhiNode extends SsaImpl::DefinitionExt {
-  PhiNode() {
-    this instanceof SsaImpl::PhiNode or
-    this instanceof SsaImpl::PhiReadNode
-  }
-}
-
-class DefinitionExt = SsaImpl::DefinitionExt;

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

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

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

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

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

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

cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll

@@ -90,6 +90,15 @@ class CaseEdge extends EdgeKind, TCaseEdge {
    * Gets the largest value of the switch expression for which control will flow along this edge.
    */
   final string getMaxValue() { result = maxValue }
+
+  /**
+   * Gets the unique value of the switch expression for which control will
+   * flow along this edge, if any.
+   */
+  final string getValue() {
+    minValue = maxValue and
+    result = minValue
+  }
 }
 
 /**

cpp/ql/lib/semmle/code/cpp/ir/implementation/IRConfiguration.qll

@@ -41,5 +41,5 @@ class IREscapeAnalysisConfiguration extends TIREscapeAnalysisConfiguration {
    * Holds if the escape analysis done by SSA construction should be sound. By default, the SSA is
    * built assuming that no variable's address ever escapes.
    */
-  predicate useSoundEscapeAnalysis() { none() }
+  predicate useSoundEscapeAnalysis() { any() }
 }

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

@@ -247,8 +247,7 @@ class Instruction extends Construction::TStageInstruction {
    * Gets the type of the result produced by this instruction. If the instruction does not produce
    * a result, its result type will be `IRVoidType`.
    */
-  cached
-  final IRType getResultIRType() { result = this.getResultLanguageType().getIRType() }
+  final IRType getResultIRType() { result = Construction::getInstructionResultIRType(this) }
 
   /**
    * Gets the type of the result produced by this instruction. If the
@@ -995,9 +994,8 @@ class ConstantInstruction extends ConstantValueInstruction {
  */
 class IntegerConstantInstruction extends ConstantInstruction {
   IntegerConstantInstruction() {
-    exists(IRType resultType |
-      resultType = this.getResultIRType() and
-      (resultType instanceof IRIntegerType or resultType instanceof IRBooleanType)
+    exists(IRType resultType | resultType = this.getResultIRType() |
+      resultType instanceof IRIntegerType or resultType instanceof IRBooleanType
     )
   }
 }
@@ -1009,6 +1007,17 @@ class FloatConstantInstruction extends ConstantInstruction {
   FloatConstantInstruction() { this.getResultIRType() instanceof IRFloatingPointType }
 }
 
+/**
+ * An instruction whose result is a constant value of a pointer type.
+ */
+class PointerConstantInstruction extends ConstantInstruction {
+  PointerConstantInstruction() {
+    exists(IRType resultType | resultType = this.getResultIRType() |
+      resultType instanceof IRAddressType or resultType instanceof IRFunctionAddressType
+    )
+  }
+}
+
 /**
  * An instruction whose result is the address of a string literal.
  */

cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/constant/ConstantAnalysis.qll

@@ -38,6 +38,12 @@ private int getBinaryInstructionValue(BinaryInstruction instr) {
     or
     instr instanceof DivInstruction and result = div(left, right)
     or
+    instr instanceof BitOrInstruction and result = bitOr(left, right)
+    or
+    instr instanceof BitAndInstruction and result = bitAnd(left, right)
+    or
+    instr instanceof BitXorInstruction and result = bitXor(left, right)
+    or
     instr instanceof CompareEQInstruction and result = compareEQ(left, right)
     or
     instr instanceof CompareNEInstruction and result = compareNE(left, right)

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

@@ -429,6 +429,11 @@ private module Cached {
     instr = unreachedInstruction(_) and result = Language::getVoidType()
   }
 
+  cached
+  IRType getInstructionResultIRType(Instruction instr) {
+    result = instr.getResultLanguageType().getIRType()
+  }
+
   /**
    * Holds if `opcode` is the opcode that specifies the operation performed by `instr`.
    *

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

@@ -247,8 +247,7 @@ class Instruction extends Construction::TStageInstruction {
    * Gets the type of the result produced by this instruction. If the instruction does not produce
    * a result, its result type will be `IRVoidType`.
    */
-  cached
-  final IRType getResultIRType() { result = this.getResultLanguageType().getIRType() }
+  final IRType getResultIRType() { result = Construction::getInstructionResultIRType(this) }
 
   /**
    * Gets the type of the result produced by this instruction. If the
@@ -995,9 +994,8 @@ class ConstantInstruction extends ConstantValueInstruction {
  */
 class IntegerConstantInstruction extends ConstantInstruction {
   IntegerConstantInstruction() {
-    exists(IRType resultType |
-      resultType = this.getResultIRType() and
-      (resultType instanceof IRIntegerType or resultType instanceof IRBooleanType)
+    exists(IRType resultType | resultType = this.getResultIRType() |
+      resultType instanceof IRIntegerType or resultType instanceof IRBooleanType
     )
   }
 }
@@ -1009,6 +1007,17 @@ class FloatConstantInstruction extends ConstantInstruction {
   FloatConstantInstruction() { this.getResultIRType() instanceof IRFloatingPointType }
 }
 
+/**
+ * An instruction whose result is a constant value of a pointer type.
+ */
+class PointerConstantInstruction extends ConstantInstruction {
+  PointerConstantInstruction() {
+    exists(IRType resultType | resultType = this.getResultIRType() |
+      resultType instanceof IRAddressType or resultType instanceof IRFunctionAddressType
+    )
+  }
+}
+
 /**
  * An instruction whose result is the address of a string literal.
  */

cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/constant/ConstantAnalysis.qll

@@ -38,6 +38,12 @@ private int getBinaryInstructionValue(BinaryInstruction instr) {
     or
     instr instanceof DivInstruction and result = div(left, right)
     or
+    instr instanceof BitOrInstruction and result = bitOr(left, right)
+    or
+    instr instanceof BitAndInstruction and result = bitAnd(left, right)
+    or
+    instr instanceof BitXorInstruction and result = bitXor(left, right)
+    or
     instr instanceof CompareEQInstruction and result = compareEQ(left, right)
     or
     instr instanceof CompareNEInstruction and result = compareNE(left, right)

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

@@ -377,6 +377,10 @@ CppType getInstructionResultType(TStageInstruction instr) {
   result = getVoidType()
 }
 
+IRType getInstructionResultIRType(Instruction instr) {
+  result = instr.getResultLanguageType().getIRType()
+}
+
 predicate getInstructionOpcode(Opcode opcode, TStageInstruction instr) {
   getInstructionTranslatedElement(instr).hasInstruction(opcode, getInstructionTag(instr), _)
   or

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

@@ -89,7 +89,8 @@ newtype TInstructionTag =
   ImplicitDestructorTag(int index) {
     exists(Expr e | exists(e.getImplicitDestructorCall(index))) or
     exists(Stmt s | exists(s.getImplicitDestructorCall(index)))
-  }
+  } or
+  CoAwaitBranchTag()
 
 class InstructionTag extends TInstructionTag {
   final string toString() { result = getInstructionTagId(this) }
@@ -186,6 +187,8 @@ string getInstructionTagId(TInstructionTag tag) {
   or
   tag = BoolConversionCompareTag() and result = "BoolConvComp"
   or
+  tag = ResultCopyTag() and result = "ResultCopy"
+  or
   tag = LoadTag() and result = "Load" // Implicit load due to lvalue-to-rvalue conversion
   or
   tag = CatchTag() and result = "Catch"
@@ -263,4 +266,6 @@ string getInstructionTagId(TInstructionTag tag) {
   exists(int index |
     tag = ImplicitDestructorTag(index) and result = "ImplicitDestructor(" + index + ")"
   )
+  or
+  tag = CoAwaitBranchTag() and result = "CoAwaitBranch"
 }

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

@@ -40,12 +40,43 @@ IRTempVariable getIRTempVariable(Locatable ast, TempVariableTag tag) {
   result.getTag() = tag
 }
 
+/** Gets an operand of `op`. */
+private Expr getAnOperand(Operation op) { result = op.getAnOperand() }
+
+/**
+ * Gets the number of nested operands of `op`. For example,
+ * `getNumberOfNestedBinaryOperands((1 + 2) + 3))` is `3`.
+ */
+private int getNumberOfNestedBinaryOperands(Operation op) { result = count(getAnOperand*(op)) }
+
+/**
+ * Holds if `op` should not be translated to a `ConstantInstruction` as part of
+ * IR generation, even if the value of `op` is constant.
+ */
+private predicate ignoreConstantValue(Operation op) {
+  op instanceof BitwiseAndExpr
+  or
+  op instanceof BitwiseOrExpr
+  or
+  op instanceof BitwiseXorExpr
+}
+
 /**
  * Holds if `expr` is a constant of a type that can be replaced directly with
  * its value in the IR. This does not include address constants as we have no
  * means to express those as QL values.
  */
-predicate isIRConstant(Expr expr) { exists(expr.getValue()) }
+predicate isIRConstant(Expr expr) {
+  exists(expr.getValue()) and
+  // We avoid constant folding certain operations since it's often useful to
+  // mark one of those as a source in dataflow, and if the operation is
+  // constant folded it's not possible to mark its operands as a source (or
+  // sink).
+  // But to avoid creating an outrageous amount of IR from very large
+  // constant expressions we fall back to constant folding if the operation
+  // has more than 50 operands (i.e., 1 + 2 + 3 + 4 + ... + 50)
+  if ignoreConstantValue(expr) then getNumberOfNestedBinaryOperands(expr) > 50 else any()
+}
 
 // Pulled out for performance. See
 // https://github.com/github/codeql-coreql-team/issues/1044.
@@ -96,6 +127,11 @@ private predicate ignoreExprAndDescendants(Expr expr) {
   exists(BuiltInVarArgsStart vaStartExpr |
     vaStartExpr.getLastNamedParameter().getFullyConverted() = expr
   )
+  or
+  // Do not translate implicit destructor calls for unnamed temporary variables that are
+  // conditionally constructed (until we have a mechanism for calling these only when the
+  // temporary's constructor was run)
+  isConditionalTemporaryDestructorCall(expr)
 }
 
 /**
@@ -116,11 +152,6 @@ private predicate ignoreExprOnly(Expr expr) {
   or
   not translateFunction(getEnclosingFunction(expr)) and
   not Raw::varHasIRFunc(getEnclosingVariable(expr))
-  or
-  exists(DeleteOrDeleteArrayExpr deleteExpr |
-    // Ignore the destructor call, because the duplicated qualifier breaks control flow.
-    deleteExpr.getDestructorCall() = expr
-  )
 }
 
 /**
@@ -226,6 +257,42 @@ private predicate usedAsCondition(Expr expr) {
   )
 }
 
+private predicate hasThrowingChild(Expr e) {
+  e = any(ThrowExpr throw).getFullyConverted()
+  or
+  exists(Expr child |
+    e = getRealParent(child) and
+    hasThrowingChild(child)
+  )
+}
+
+private predicate isInConditionalEvaluation(Expr e) {
+  exists(ConditionalExpr cond |
+    e = cond.getThen().getFullyConverted() and not cond.isTwoOperand()
+    or
+    e = cond.getElse().getFullyConverted()
+    or
+    // If one of the operands throws then the temporaries constructed in either
+    // branch will also be attached to the ternary expression. We suppress
+    // those destructor calls as well.
+    hasThrowingChild([cond.getThen(), cond.getElse()]) and
+    e = cond.getFullyConverted()
+  )
+  or
+  e = any(LogicalAndExpr lae).getRightOperand().getFullyConverted()
+  or
+  e = any(LogicalOrExpr loe).getRightOperand().getFullyConverted()
+  or
+  isInConditionalEvaluation(getRealParent(e))
+}
+
+private predicate isConditionalTemporaryDestructorCall(DestructorCall dc) {
+  exists(TemporaryObjectExpr temp |
+    temp = dc.getQualifier().(ReuseExpr).getReusedExpr() and
+    isInConditionalEvaluation(temp)
+  )
+}
+
 /**
  * Holds if `conv` is an `InheritanceConversion` that requires a `TranslatedLoad`, despite not being
  * marked as having an lvalue-to-rvalue conversion.
@@ -477,8 +544,7 @@ private module IRDeclarationEntries {
    * 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.
+   * do not have `DeclarationEntry`s in older databases.
    *
    * So instead, the IR works with `IRDeclarationEntry`s that synthesize missing
    * `DeclarationEntry`s when there is no result for `DeclStmt::getDeclarationEntry`.
@@ -744,12 +810,26 @@ newtype TTranslatedElement =
   // The declaration/initialization part of a `ConditionDeclExpr`
   TTranslatedConditionDecl(ConditionDeclExpr expr) { not ignoreExpr(expr) } or
   // The side effects of a `Call`
-  TTranslatedCallSideEffects(CallOrAllocationExpr expr) { not ignoreSideEffects(expr) } or
+  TTranslatedCallSideEffects(CallOrAllocationExpr expr) {
+    not ignoreExpr(expr) and
+    not ignoreSideEffects(expr)
+  } or
   // The non-argument-specific side effect of a `Call`
   TTranslatedCallSideEffect(Expr expr, SideEffectOpcode opcode) {
+    not ignoreExpr(expr) and
     not ignoreSideEffects(expr) and
     opcode = getCallSideEffectOpcode(expr)
   } or
+  // The set of destructors to invoke after a `throw`. These need to be special
+  // cased because the edge kind following a throw is an `ExceptionEdge`, and
+  // we need to make sure that the edge kind is still an `ExceptionEdge` after
+  // all the destructors have run.
+  TTranslatedDestructorsAfterThrow(ThrowExpr throw) {
+    exists(DestructorCall dc |
+      dc = throw.getAnImplicitDestructorCall() and
+      not ignoreExpr(dc)
+    )
+  } or
   // A precise side effect of an argument to a `Call`
   TTranslatedArgumentExprSideEffect(Call call, Expr expr, int n, SideEffectOpcode opcode) {
     not ignoreExpr(expr) and
@@ -764,6 +844,7 @@ newtype TTranslatedElement =
   // Constructor calls lack a qualifier (`this`) expression, so we need to handle the side effects
   // on `*this` without an `Expr`.
   TTranslatedStructorQualifierSideEffect(Call call, SideEffectOpcode opcode) {
+    not ignoreExpr(call) and
     not ignoreSideEffects(call) and
     call instanceof ConstructorCall and
     opcode = getASideEffectOpcode(call, -1)

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

@@ -90,15 +90,18 @@ abstract class TranslatedExpr extends TranslatedElement {
   final override TranslatedElement getChild(int id) {
     result = this.getChildInternal(id)
     or
-    exists(int maxChildId, int destructorIndex |
-      maxChildId = max(int childId | exists(this.getChildInternal(childId))) and
-      result.(TranslatedExpr).getExpr() = expr.getImplicitDestructorCall(destructorIndex) and
-      id = maxChildId + 1 + destructorIndex
+    exists(int destructorIndex |
+      result = this.getImplicitDestructorCall(destructorIndex) and
+      id = this.getFirstDestructorCallIndex() + destructorIndex
     )
   }
 
+  final private TranslatedExpr getImplicitDestructorCall(int index) {
+    result.getExpr() = expr.getImplicitDestructorCall(index)
+  }
+
   final override predicate hasAnImplicitDestructorCall() {
-    exists(expr.getAnImplicitDestructorCall())
+    exists(this.getImplicitDestructorCall(_))
   }
 
   final override int getFirstDestructorCallIndex() {
@@ -408,6 +411,14 @@ class TranslatedLoad extends TranslatedValueCategoryAdjustment, TTranslatedLoad
       result = this.getOperand().getResult()
     )
   }
+
+  override predicate handlesDestructorsExplicitly() {
+    // The class that generates IR for `e` will (implicitly or explicitly)
+    // handle the generation of destructor calls for `e`. Without disabling
+    // destructor call generation here the destructor will get multiple
+    // parents.
+    any()
+  }
 }
 
 /**
@@ -527,6 +538,11 @@ class TranslatedResultCopy extends TranslatedExpr, TTranslatedResultCopy {
   final override predicate producesExprResult() { any() }
 
   private TranslatedCoreExpr getOperand() { result.getExpr() = expr }
+
+  override predicate handlesDestructorsExplicitly() {
+    // The destructor calls will already have been generated by the translation of `expr`.
+    any()
+  }
 }
 
 class TranslatedCommaExpr extends TranslatedNonConstantExpr {
@@ -1295,6 +1311,146 @@ class TranslatedUnaryExpr extends TranslatedSingleInstructionExpr {
   }
 }
 
+/**
+ * IR translation of a `co_await` or `co_yield` expression.
+ *
+ * The translation of `x = co_await ...` is essentially:
+ * ```cpp
+ * if (!awaiter.await_ready()) {
+ *   awaiter.await_suspend();
+ * }
+ * x = awaiter.await_resume();
+ * ```
+ * where `awaiter` is an object constructed from programmer-supplied
+ * input, and for IR construction purposes these are resolved by the C/C++
+ * front-end.
+ *
+ * See https://en.cppreference.com/w/cpp/language/coroutines#co_await for the
+ * specification on how `awaiter` is obtained.
+ */
+abstract private class TranslatedCoExpr extends TranslatedNonConstantExpr {
+  /** Gets the operand of this operation. */
+  abstract Expr getOperand();
+
+  /**
+   * Gets the expression that decides if the enclosing coroutine should be
+   * suspended.
+   */
+  abstract Expr getAwaitReady();
+
+  /**
+   * Gets the expression that is evaluated when the enclosing coroutine is
+   * suspended.
+   */
+  abstract Expr getAwaitSuspend();
+
+  /**
+   * Gets the expression that represents the resume point if the enclosing
+   * coroutine was suspended.
+   */
+  abstract Expr getAwaitResume();
+
+  final override Instruction getFirstInstruction(EdgeKind kind) {
+    result = this.getTranslatedOperand().getFirstInstruction(kind)
+  }
+
+  override Instruction getALastInstructionInternal() {
+    result = this.getTranslatedAwaitResume().getALastInstruction()
+  }
+
+  final override TranslatedElement getChildInternal(int id) {
+    id = 0 and result = this.getTranslatedOperand()
+    or
+    id = 1 and result = this.getTranslatedAwaitReady()
+    or
+    id = 2 and result = this.getTranslatedAwaitResume()
+    or
+    id = 3 and result = this.getTranslatedAwaitSuspend()
+  }
+
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
+    tag = CoAwaitBranchTag() and
+    (
+      kind instanceof TrueEdge and
+      result = this.getTranslatedAwaitResume().getFirstInstruction(any(GotoEdge goto))
+      or
+      kind instanceof FalseEdge and
+      result = this.getTranslatedAwaitSuspend().getFirstInstruction(any(GotoEdge goto))
+    )
+  }
+
+  override Instruction getResult() { result = this.getTranslatedAwaitResume().getResult() }
+
+  final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
+    child = this.getTranslatedOperand() and
+    result = this.getTranslatedAwaitReady().getFirstInstruction(kind)
+    or
+    child = this.getTranslatedAwaitReady() and
+    kind instanceof GotoEdge and
+    result = this.getInstruction(CoAwaitBranchTag())
+    or
+    child = this.getTranslatedAwaitSuspend() and
+    result = this.getTranslatedAwaitResume().getFirstInstruction(kind)
+    or
+    child = this.getTranslatedAwaitResume() and
+    result = this.getParent().getChildSuccessor(this, kind)
+  }
+
+  override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
+    tag = CoAwaitBranchTag() and
+    opcode instanceof Opcode::ConditionalBranch and
+    resultType = getVoidType()
+  }
+
+  override Instruction getInstructionRegisterOperand(InstructionTag tag, OperandTag operandTag) {
+    tag = CoAwaitBranchTag() and
+    operandTag instanceof ConditionOperandTag and
+    result = this.getTranslatedAwaitReady().getResult()
+  }
+
+  private TranslatedExpr getTranslatedOperand() {
+    result = getTranslatedExpr(this.getOperand().getFullyConverted())
+  }
+
+  private TranslatedExpr getTranslatedAwaitReady() {
+    result = getTranslatedExpr(this.getAwaitReady().getFullyConverted())
+  }
+
+  private TranslatedExpr getTranslatedAwaitResume() {
+    result = getTranslatedExpr(this.getAwaitResume().getFullyConverted())
+  }
+
+  private TranslatedExpr getTranslatedAwaitSuspend() {
+    result = getTranslatedExpr(this.getAwaitSuspend().getFullyConverted())
+  }
+}
+
+/** IR translation of `co_await`. */
+class TranslatedCoAwaitExpr extends TranslatedCoExpr {
+  override CoAwaitExpr expr;
+
+  final override Expr getOperand() { result = expr.getOperand() }
+
+  final override Expr getAwaitReady() { result = expr.getAwaitReady() }
+
+  final override Expr getAwaitSuspend() { result = expr.getAwaitSuspend() }
+
+  final override Expr getAwaitResume() { result = expr.getAwaitResume() }
+}
+
+/** IR translation of `co_yield`. */
+class TranslatedCoYieldxpr extends TranslatedCoExpr {
+  override CoYieldExpr expr;
+
+  final override Expr getOperand() { result = expr.getOperand() }
+
+  final override Expr getAwaitReady() { result = expr.getAwaitReady() }
+
+  final override Expr getAwaitSuspend() { result = expr.getAwaitSuspend() }
+
+  final override Expr getAwaitResume() { result = expr.getAwaitResume() }
+}
+
 abstract class TranslatedConversion extends TranslatedNonConstantExpr {
   override Conversion expr;
 
@@ -2012,6 +2168,13 @@ abstract class TranslatedAllocationSize extends TranslatedExpr, TTranslatedAlloc
   final override predicate producesExprResult() { none() }
 
   final override Instruction getResult() { result = this.getInstruction(AllocationSizeTag()) }
+
+  final override predicate handlesDestructorsExplicitly() {
+    // Since the enclosing `TranslatedNewOrNewArrayExpr` (implicitly) handles the destructors
+    // we need to disable the implicit handling here as otherwise the destructors will have
+    // multiple parents
+    any()
+  }
 }
 
 TranslatedAllocationSize getTranslatedAllocationSize(NewOrNewArrayExpr newExpr) {
@@ -2169,6 +2332,13 @@ class TranslatedAllocatorCall extends TTranslatedAllocatorCall, TranslatedDirect
 
   final override predicate producesExprResult() { none() }
 
+  final override predicate handlesDestructorsExplicitly() {
+    // Since the enclosing `TranslatedNewOrNewArrayExpr` (implicitly) handles the destructors
+    // we need to disable the implicit handling here as otherwise the destructors will have
+    // multiple parents
+    any()
+  }
+
   override Function getInstructionFunction(InstructionTag tag) {
     tag = CallTargetTag() and result = expr.getAllocator()
   }
@@ -2258,7 +2428,11 @@ class TranslatedDeleteOrDeleteArrayExpr extends TranslatedNonConstantExpr, Trans
 
   final override Type getCallResultType() { result = expr.getType() }
 
-  final override TranslatedExpr getQualifier() { none() }
+  final override TranslatedExpr getQualifier() {
+    result = getTranslatedExpr(expr.getDestructorCall())
+  }
+
+  final override Instruction getQualifierResult() { none() }
 
   final override predicate hasArguments() {
     // All deallocator calls have at least one argument.
@@ -2273,7 +2447,7 @@ class TranslatedDeleteOrDeleteArrayExpr extends TranslatedNonConstantExpr, Trans
   final override TranslatedExpr getArgument(int index) {
     // The only argument we define is the pointer to be deallocated.
     index = 0 and
-    result = getTranslatedExpr(expr.getExpr().getFullyConverted())
+    result = getTranslatedExpr(expr.getExprWithReuse().getFullyConverted())
   }
 
   final override predicate mayThrowException() {
@@ -2782,6 +2956,112 @@ class TranslatedTemporaryObjectExpr extends TranslatedNonConstantExpr,
   final override Instruction getResult() { result = this.getTargetAddress() }
 }
 
+/**
+ * IR translation of a `ReuseExpr`.
+ *
+ * This translation produces a copy of the glvalue instruction holding the (unconverted) result
+ * of the reused expression. In the case where the original expression was a prvalue, the
+ * result will be a copy of the glvalue operand of a `TranslatedLoad`.
+ */
+class TranslatedReuseExpr extends TranslatedNonConstantExpr {
+  override ReuseExpr expr;
+
+  override Instruction getFirstInstruction(EdgeKind kind) {
+    result = this.getInstruction(OnlyInstructionTag()) and
+    kind instanceof GotoEdge
+  }
+
+  override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
+    opcode instanceof Opcode::CopyValue and
+    tag instanceof OnlyInstructionTag and
+    resultType = this.getResultType()
+  }
+
+  override Instruction getResult() { result = this.getInstruction(OnlyInstructionTag()) }
+
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
+    tag = OnlyInstructionTag() and
+    kind instanceof GotoEdge and
+    result = this.getParent().getChildSuccessor(this, kind)
+  }
+
+  override TranslatedElement getChildInternal(int id) { none() }
+
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(OnlyInstructionTag())
+  }
+
+  override Instruction getInstructionRegisterOperand(InstructionTag tag, OperandTag operandTag) {
+    tag = OnlyInstructionTag() and
+    operandTag instanceof UnaryOperandTag and
+    if getTranslatedExpr(expr.getReusedExpr()) instanceof TranslatedLoad
+    then result = getTranslatedExpr(expr.getReusedExpr()).(TranslatedLoad).getOperand().getResult()
+    else result = getTranslatedExpr(expr.getReusedExpr()).getResult()
+  }
+}
+
+/**
+ * The IR translation of the destructor calls of the parent `TranslatedThrow`.
+ *
+ * This object does not itself generate the destructor calls. Instead, its
+ * children provide the actual calls, and this object ensures that we correctly
+ * exit with an `ExceptionEdge` after executing all the destructor calls.
+ */
+class TranslatedDestructorsAfterThrow extends TranslatedElement, TTranslatedDestructorsAfterThrow {
+  ThrowExpr throw;
+
+  TranslatedDestructorsAfterThrow() { this = TTranslatedDestructorsAfterThrow(throw) }
+
+  override string toString() { result = "Destructor calls after throw: " + throw }
+
+  private TranslatedCall getTranslatedImplicitDestructorCall(int id) {
+    result.getExpr() = throw.getImplicitDestructorCall(id)
+  }
+
+  override Instruction getFirstInstruction(EdgeKind kind) {
+    result = this.getChild(0).getFirstInstruction(kind)
+  }
+
+  override ThrowExpr getAst() { result = throw }
+
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
+
+  override TranslatedElement getChild(int id) {
+    result = this.getTranslatedImplicitDestructorCall(id)
+  }
+
+  override predicate handlesDestructorsExplicitly() { any() }
+
+  override Declaration getFunction() { result = throw.getEnclosingFunction() }
+
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
+    exists(int id | child = this.getChild(id) |
+      // Transition to the next child, if any.
+      result = this.getChild(id + 1).getFirstInstruction(kind)
+      or
+      // And otherwise, exit this element with an exceptional edge
+      not exists(this.getChild(id + 1)) and
+      kind instanceof ExceptionEdge and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+    )
+  }
+
+  override TranslatedElement getLastChild() {
+    result =
+      this.getTranslatedImplicitDestructorCall(max(int id |
+          exists(throw.getImplicitDestructorCall(id))
+        ))
+  }
+
+  override Instruction getALastInstructionInternal() {
+    result = this.getLastChild().getALastInstruction()
+  }
+
+  override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
+    none()
+  }
+}
+
 /**
  * IR translation of a `throw` expression.
  */
@@ -2796,13 +3076,22 @@ abstract class TranslatedThrowExpr extends TranslatedNonConstantExpr {
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = ThrowTag() and
-    kind instanceof ExceptionEdge and
-    result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+    (
+      result = this.getDestructors().getFirstInstruction(kind)
+      or
+      not exists(this.getDestructors()) and
+      kind instanceof ExceptionEdge and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+    )
   }
 
   override Instruction getResult() { none() }
 
   abstract Opcode getThrowOpcode();
+
+  override predicate handlesDestructorsExplicitly() { any() }
+
+  TranslatedDestructorsAfterThrow getDestructors() { result.getAst() = expr }
 }
 
 /**
@@ -2814,6 +3103,9 @@ class TranslatedThrowValueExpr extends TranslatedThrowExpr, TranslatedVariableIn
 
   final override TranslatedElement getChildInternal(int id) {
     result = TranslatedVariableInitialization.super.getChildInternal(id)
+    or
+    id = max(int i | exists(TranslatedVariableInitialization.super.getChildInternal(i))) + 1 and
+    result = this.getDestructors()
   }
 
   final override Instruction getChildSuccessorInternal(TranslatedElement elem, EdgeKind kind) {
@@ -2879,14 +3171,22 @@ class TranslatedThrowValueExpr extends TranslatedThrowExpr, TranslatedVariableIn
 class TranslatedReThrowExpr extends TranslatedThrowExpr {
   override ReThrowExpr expr;
 
-  override TranslatedElement getChildInternal(int id) { none() }
+  override TranslatedElement getChildInternal(int id) {
+    id = 0 and
+    result = this.getDestructors()
+  }
 
   override Instruction getFirstInstruction(EdgeKind kind) {
     result = this.getInstruction(ThrowTag()) and
     kind instanceof GotoEdge
   }
 
-  override Instruction getALastInstructionInternal() { result = this.getInstruction(ThrowTag()) }
+  override Instruction getALastInstructionInternal() {
+    result = this.getDestructors().getALastInstruction()
+    or
+    not this.hasAnImplicitDestructorCall() and
+    result = this.getInstruction(ThrowTag())
+  }
 
   override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) { none() }