Java: Split tests between posix and windows due to different behaviour on windows with java 21.

Java: Update buildless test expectations

.bazelrc

@@ -1,4 +1,12 @@
 common --enable_platform_specific_config
+common --enable_bzlmod
+# because we use --override_module with `%workspace%`, the lock file is not stable
+common --lockfile_mode=off
+
+# when building from this repository in isolation, the internal repository will not be found at ..
+# where `MODULE.bazel` looks for it. The following will get us past the module loading phase, so
+# that we can build things that do not rely on that
+common --override_module=semmle_code=%workspace%/misc/bazel/semmle_code_stub
 
 build --repo_env=CC=clang --repo_env=CXX=clang++
 

.bazelversion

@@ -1 +1 @@
-6.3.1
+7.1.0

.gitattributes

@@ -74,3 +74,7 @@ javascript/ql/experimental/adaptivethreatmodeling/test/endpoint_large_scale/auto
 
 # Auto-generated modeling for Python
 python/ql/lib/semmle/python/frameworks/data/internal/subclass-capture/*.yml linguist-generated=true
+
+# auto-generated bazel lock file
+ruby/extractor/cargo-bazel-lock.json linguist-generated=true
+ruby/extractor/cargo-bazel-lock.json -merge

.github/labeler.yml

@@ -20,7 +20,7 @@ JS:
 
 Kotlin:
   - java/kotlin-extractor/**/*
-  - java/ql/test/kotlin/**/*
+  - java/ql/test-kotlin*/**/*
 
 Python:
   - python/**/*

.github/workflows/compile-queries.yml

@@ -28,7 +28,7 @@ jobs:
         with: 
           key: all-queries
       - name: check formatting
-        run: find */ql -type f \( -name "*.qll" -o -name "*.ql" \) -print0 | xargs -0 -n 3000 -P 10 codeql query format -q --check-only
+        run: find shared */ql -type f \( -name "*.qll" -o -name "*.ql" \) -print0 | xargs -0 -n 3000 -P 10 codeql query format -q --check-only
       - name: compile queries - check-only
         # run with --check-only if running in a PR (github.sha != main)
         if : ${{ github.event_name == 'pull_request' }}

.github/workflows/ruby-build.yml

@@ -51,9 +51,11 @@ jobs:
         run: |
           brew install gnu-tar
           echo "/usr/local/opt/gnu-tar/libexec/gnubin" >> $GITHUB_PATH
-      - name: Install cargo-cross
-        if: runner.os == 'Linux'
-        run: cargo install cross --version 0.2.5
+      - name: Prepare Windows
+        if: runner.os == 'Windows'
+        shell: powershell
+        run: |
+          git config --global core.longpaths true
       - uses: ./.github/actions/os-version
         id: os_version
       - name: Cache entire extractor
@@ -82,16 +84,8 @@ jobs:
       - name: Run tests
         if: steps.cache-extractor.outputs.cache-hit != 'true'
         run: cd extractor && cargo test --verbose
-      # On linux, build the extractor via cross in a centos7 container.
-      # This ensures we don't depend on glibc > 2.17.
-      - name: Release build (linux)
-        if: steps.cache-extractor.outputs.cache-hit != 'true' && runner.os == 'Linux'
-        run: |
-          cd extractor
-          cross build --release
-          mv target/x86_64-unknown-linux-gnu/release/codeql-extractor-ruby target/release/
-      - name: Release build (windows and macos)
-        if: steps.cache-extractor.outputs.cache-hit != 'true' && runner.os != 'Linux'
+      - name: Release build
+        if: steps.cache-extractor.outputs.cache-hit != 'true'
         run: cd extractor && cargo build --release
       - name: Generate dbscheme
         if: ${{ matrix.os == 'ubuntu-latest' && steps.cache-extractor.outputs.cache-hit != 'true'}}
@@ -123,7 +117,7 @@ jobs:
       - name: Cache compilation cache
         id: query-cache
         uses: ./.github/actions/cache-query-compilation
-        with: 
+        with:
           key: ruby-build
       - name: Build Query Pack
         run: |
@@ -235,54 +229,3 @@ jobs:
         shell: bash
         run: |
           codeql database analyze --search-path "${{ runner.temp }}/ruby-bundle" --format=sarifv2.1.0 --output=out.sarif ../database ruby-code-scanning.qls
-
-  # This is a copy of the 'test' job that runs in a centos7 container.
-  # This tests that the extractor works correctly on systems with an old glibc.
-  test-centos7:
-    defaults:
-      run:
-        working-directory: ${{ github.workspace }}
-    strategy:
-      fail-fast: false
-    runs-on: ubuntu-latest
-    container:
-      image: centos:centos7
-      env:
-        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-    needs: [package]
-    steps:
-      - name: Install gh cli
-        run: |
-          yum-config-manager --add-repo https://cli.github.com/packages/rpm/gh-cli.repo
-          # fetch-codeql requires unzip and jq
-          # jq is available in epel-release (https://docs.fedoraproject.org/en-US/epel/)
-          yum install -y gh unzip epel-release
-          yum install -y jq
-      - uses: actions/checkout@v3
-      - name: Fetch CodeQL
-        uses: ./.github/actions/fetch-codeql
-
-      # Due to a bug in Actions, we can't use runner.temp in the run blocks here.
-      # https://github.com/actions/runner/issues/2185
-
-      - name: Download Ruby bundle
-        uses: actions/download-artifact@v3
-        with:
-          name: codeql-ruby-bundle
-          path: ${{ runner.temp }}
-      - name: Unzip Ruby bundle
-        shell: bash
-        run: unzip -q -d "$RUNNER_TEMP"/ruby-bundle "$RUNNER_TEMP"/codeql-ruby-bundle.zip
-
-      - name: Run QL test
-        shell: bash
-        run: |
-          codeql test run --search-path "$RUNNER_TEMP"/ruby-bundle --additional-packs "$RUNNER_TEMP"/ruby-bundle ruby/ql/test/library-tests/ast/constants/
-      - name: Create database
-        shell: bash
-        run: |
-          codeql database create --search-path "$RUNNER_TEMP"/ruby-bundle --language ruby --source-root ruby/ql/test/library-tests/ast/constants/ ../database
-      - name: Analyze database
-        shell: bash
-        run: |
-          codeql database analyze --search-path "$RUNNER_TEMP"/ruby-bundle --format=sarifv2.1.0 --output=out.sarif ../database ruby-code-scanning.qls

.gitignore

@@ -39,6 +39,9 @@
 # local bazel options
 /local.bazelrc
 
+# generated cmake directory
+/.bazel-cmake
+
 # CLion project files
 /.clwb
 

CODEOWNERS

@@ -25,6 +25,7 @@
 
 # Bazel (excluding BUILD.bazel files)
 WORKSPACE.bazel @github/codeql-ci-reviewers
+MODULE.bazel @github/codeql-ci-reviewers
 .bazelversion @github/codeql-ci-reviewers
 .bazelrc @github/codeql-ci-reviewers
 **/*.bzl @github/codeql-ci-reviewers

MODULE.bazel

@@ -0,0 +1,53 @@
+module(
+    name = "codeql",
+    version = "0.0",
+)
+
+# this points to our internal repository when `codeql` is checked out as a submodule thereof
+# when building things from `codeql` independently this is stubbed out in `.bazelrc`
+bazel_dep(name = "semmle_code", version = "0.0")
+local_path_override(
+    module_name = "semmle_code",
+    path = "..",
+)
+
+# 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_nodejs", version = "6.0.3")
+bazel_dep(name = "rules_python", version = "0.31.0")
+bazel_dep(name = "bazel_skylib", version = "1.5.0")
+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")
+
+pip = use_extension("@rules_python//python/extensions:pip.bzl", "pip")
+pip.parse(
+    hub_name = "codegen_deps",
+    python_version = "3.11",
+    requirements_lock = "//misc/codegen:requirements_lock.txt",
+)
+use_repo(pip, "codegen_deps")
+
+swift_deps = use_extension("//swift/third_party:load.bzl", "swift_deps")
+use_repo(
+    swift_deps,
+    "binlog",
+    "picosha2",
+    "swift_prebuilt_darwin_x86_64",
+    "swift_prebuilt_linux",
+    "swift_toolchain_linux",
+    "swift_toolchain_macos",
+)
+
+node = use_extension("@rules_nodejs//nodejs:extensions.bzl", "node")
+node.toolchain(
+    name = "nodejs",
+    node_version = "18.15.0",
+)
+use_repo(node, "nodejs", "nodejs_toolchains")
+
+register_toolchains(
+    "@nodejs_toolchains//:all",
+)

WORKSPACE.bazel

@@ -1,12 +1,2 @@
-# Please notice that any bazel targets and definitions in this repository are currently experimental
-# and for internal use only.
-
-workspace(name = "codeql")
-
-load("//misc/bazel:workspace.bzl", "codeql_workspace")
-
-codeql_workspace()
-
-load("//misc/bazel:workspace_deps.bzl", "codeql_workspace_deps")
-
-codeql_workspace_deps()
+# please use MODULE.bazel to add dependencies
+# this empty file is required by internal repositories, don't remove it

codeql-workspace.yml

@@ -6,6 +6,7 @@ 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"

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"
@@ -381,7 +255,6 @@
     "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": [
@@ -431,13 +304,6 @@
     "java/ql/src/experimental/Security/CWE/CWE-400/LocalThreadResourceAbuse.qhelp",
     "java/ql/src/experimental/Security/CWE/CWE-400/ThreadResourceAbuse.qhelp"
   ],
-  "IDE Contextual Queries": [
-    "cpp/ql/lib/IDEContextual.qll",
-    "csharp/ql/lib/IDEContextual.qll",
-    "java/ql/lib/IDEContextual.qll",
-    "javascript/ql/lib/IDEContextual.qll",
-    "python/ql/lib/analysis/IDEContextual.qll"
-  ],
   "CryptoAlgorithms Python/JS/Ruby": [
     "javascript/ql/lib/semmle/javascript/security/CryptoAlgorithms.qll",
     "python/ql/lib/semmle/python/concepts/CryptoAlgorithms.qll",

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

@@ -1,5 +1,7 @@
 using System;
+
 using Semmle.Autobuild.Shared;
+using Semmle.Util;
 
 namespace Semmle.Autobuild.Cpp
 {

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/ql/lib/CHANGELOG.md

@@ -1,3 +1,13 @@
+## 0.12.8
+
+No user-facing changes.
+
+## 0.12.7
+
+### Minor Analysis Improvements
+
+* Added destructors for named objects to the intermediate representation.
+
 ## 0.12.6
 
 ### New Features

cpp/ql/lib/IDEContextual.qll

@@ -3,6 +3,7 @@
  */
 
 import semmle.files.FileSystem
+private import codeql.util.FileSystem
 
 /**
  * Returns the `File` matching the given source file name as encoded by the VS
@@ -10,13 +11,5 @@ import semmle.files.FileSystem
  */
 cached
 File getFileBySourceArchiveName(string name) {
-  // The name provided for a file in the source archive by the VS Code extension
-  // has some differences from the absolute path in the database:
-  // 1. colons are replaced by underscores
-  // 2. there's a leading slash, even for Windows paths: "C:/foo/bar" ->
-  //    "/C_/foo/bar"
-  // 3. double slashes in UNC prefixes are replaced with a single slash
-  // We can handle 2 and 3 together by unconditionally adding a leading slash
-  // before replacing double slashes.
-  name = ("/" + result.getAbsolutePath().replaceAll(":", "_")).replaceAll("//", "/")
+  result = IdeContextual<File>::getFileBySourceArchiveName(name)
 }

cpp/ql/lib/change-notes/2024-03-15-switches-in-guard-conditions.md

@@ -0,0 +1,4 @@
+---
+category: feature
+---
+* Added a predicate `GuardCondition.valueControls` to query whether a basic block is guarded by a particular `case` of a `switch` statement.

cpp/ql/lib/change-notes/2024-03-19-predicates-for-switches-as-guards-2.md

@@ -0,0 +1,5 @@
+---
+category: feature
+---
+* 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.

cpp/ql/lib/change-notes/2024-03-19-predicates-for-switches-as-guards.md

@@ -0,0 +1,5 @@
+---
+category: feature
+---
+* 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.

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

@@ -0,0 +1,5 @@
+## 0.12.7
+
+### Minor Analysis Improvements
+
+* Added destructors for named objects to the intermediate representation.

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

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

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

@@ -1,2 +1,2 @@
 ---
-lastReleaseVersion: 0.12.6
+lastReleaseVersion: 0.12.8

cpp/ql/lib/qlpack.yml

@@ -1,5 +1,5 @@
 name: codeql/cpp-all
-version: 0.12.6
+version: 0.12.9-dev
 groups: cpp
 dbscheme: semmlecode.cpp.dbscheme
 extractor: cpp

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

@@ -60,4 +60,6 @@ Element exprEnclosingElement(Expr e) {
       )
     else result = de.getDeclaration()
   )
+  or
+  result.(Stmt).getAnImplicitDestructorCall() = e
 }

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
     )
   }
 
@@ -686,6 +689,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 + ")"

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,30 @@ 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
+  )
+}
+
 /** The int value of integer constant expression. */
 private int int_value(Instruction i) { result = i.(IntegerConstantInstruction).getValue().toInt() }

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

@@ -1,6 +1,6 @@
 // NOTE: There are two copies of this file, and they must be kept identical:
 // - semmle/code/cpp/controlflow/SubBasicBlocks.qll
-// - semmle/code/cpp/dataflow/internal/SubBasicBlocks.qll
+// - semmle/code/cpp/dataflow/internal/SubBasicBlocks.qll [now DEPRECATED]
 //
 // The second one is a private copy of the `SubBasicBlocks` library for
 // internal use by the data flow library. Having an extra copy prevents

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/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/AddressFlow.qll

@@ -1,4 +1,6 @@
 /**
+ * DEPRECATED: Use `semmle.code.cpp.dataflow.new.DataFlow` instead.
+ *
  * Provides a local analysis for identifying where a variable address
  * is effectively taken. Array-like offsets are allowed to pass through but
  * not field-like offsets.

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

@@ -1,3 +1,7 @@
+/**
+ * DEPRECATED: Use `semmle.code.cpp.dataflow.new.DataFlow` instead.
+ */
+
 private import cpp
 private import DataFlowPrivate
 private import DataFlowUtil

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

@@ -1,3 +1,8 @@
+/**
+ * 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

@@ -285,6 +285,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

@@ -285,6 +285,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

@@ -285,6 +285,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

@@ -285,6 +285,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

@@ -1,3 +1,8 @@
+/**
+ * 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

@@ -1,4 +1,6 @@
 /**
+ * DEPRECATED: Use `semmle.code.cpp.dataflow.new.DataFlow` instead.
+ *
  * Provides consistency queries for checking invariants in the language-specific
  * data-flow classes and predicates.
  */
@@ -8,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())
@@ -24,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

@@ -285,6 +285,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

@@ -1,7 +1,10 @@
 /**
+ * DEPRECATED: Use `semmle.code.cpp.dataflow.new.DataFlow` instead.
+ *
  * Provides C++-specific definitions for use in the data flow library.
  */
 
+private import semmle.code.cpp.Location
 private import codeql.dataflow.DataFlow
 
 module Private {
@@ -13,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

@@ -1,3 +1,7 @@
+/**
+ * DEPRECATED: Use `semmle.code.cpp.dataflow.new.DataFlow` instead.
+ */
+
 private import cpp
 private import DataFlowUtil
 private import DataFlowDispatch

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

@@ -1,4 +1,6 @@
 /**
+ * DEPRECATED: Use `semmle.code.cpp.dataflow.new.DataFlow` instead.
+ *
  * Provides C++-specific definitions for use in the data flow library.
  */
 
@@ -103,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)

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

@@ -1,4 +1,6 @@
 /**
+ * DEPRECATED: Use `semmle.code.cpp.dataflow.new.DataFlow` instead.
+ *
  * Provides a class for handling variables in the data flow analysis.
  */
 

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

@@ -1,6 +1,6 @@
 // NOTE: There are two copies of this file, and they must be kept identical:
 // - semmle/code/cpp/controlflow/SubBasicBlocks.qll
-// - semmle/code/cpp/dataflow/internal/SubBasicBlocks.qll
+// - semmle/code/cpp/dataflow/internal/SubBasicBlocks.qll [now DEPRECATED]
 //
 // The second one is a private copy of the `SubBasicBlocks` library for
 // internal use by the data flow library. Having an extra copy prevents

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

@@ -1,10 +1,13 @@
 /**
+ * DEPRECATED: Use `semmle.code.cpp.dataflow.new.DataFlow` instead.
+ *
  * 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

@@ -1,4 +1,6 @@
 /**
+ * DEPRECATED: Use `semmle.code.cpp.dataflow.new.DataFlow` instead.
+ *
  * Provides classes for performing local (intra-procedural) and
  * global (inter-procedural) taint-tracking analyses.
  *

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

@@ -1,3 +1,7 @@
+/**
+ * DEPRECATED: Use `Global` and `GlobalWithState` instead.
+ */
+
 import semmle.code.cpp.dataflow.internal.TaintTrackingUtil as Public
 
 module Private {

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

@@ -1,3 +1,7 @@
+/**
+ * DEPRECATED: Use `Global` and `GlobalWithState` instead.
+ */
+
 import semmle.code.cpp.dataflow.internal.TaintTrackingUtil as Public
 
 module Private {

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

@@ -1322,3 +1322,23 @@ class CoYieldExpr extends UnaryOperation, @co_yield {
 
   override int getPrecedence() { result = 2 }
 }
+
+/**
+ * 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)) }
+}

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/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/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

@@ -285,6 +285,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

@@ -285,6 +285,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

@@ -285,6 +285,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

@@ -285,6 +285,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
 

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

@@ -34,7 +34,7 @@ private import Node0ToString
 cached
 private newtype TIRDataFlowNode =
   TNode0(Node0Impl node) { DataFlowImplCommon::forceCachingInSameStage() } or
-  TVariableNode(Variable var, int indirectionIndex) {
+  TGlobalLikeVariableNode(GlobalLikeVariable var, int indirectionIndex) {
     indirectionIndex =
       [getMinIndirectionsForType(var.getUnspecifiedType()) .. Ssa::getMaxIndirectionsForType(var.getUnspecifiedType())]
   } or
@@ -55,29 +55,12 @@ private newtype TIRDataFlowNode =
   TFinalParameterNode(Parameter p, int indirectionIndex) {
     exists(Ssa::FinalParameterUse use |
       use.getParameter() = p and
-      use.getIndirectionIndex() = indirectionIndex and
-      parameterIsRedefined(p)
+      use.getIndirectionIndex() = indirectionIndex
     )
   } or
   TFinalGlobalValue(Ssa::GlobalUse globalUse) or
   TInitialGlobalValue(Ssa::GlobalDef globalUse)
 
-/**
- * Holds if the value of `*p` (or `**p`, `***p`, etc.) is redefined somewhere in the body
- * of the enclosing function of `p`.
- *
- * Only parameters satisfying this predicate will generate a `FinalParameterNode` transferring
- * flow out of the function.
- */
-private predicate parameterIsRedefined(Parameter p) {
-  exists(Ssa::Def def |
-    def.getSourceVariable().getBaseVariable().(Ssa::BaseIRVariable).getIRVariable().getAst() = p and
-    def.getIndirectionIndex() = 0 and
-    def.getIndirection() > 1 and
-    not def.getValue().asInstruction() instanceof InitializeParameterInstruction
-  )
-}
-
 /**
  * An operand that is defined by a `FieldAddressInstruction`.
  */
@@ -413,7 +396,7 @@ class Node extends TIRDataFlowNode {
    * modeling flow in and out of global variables.
    */
   Variable asVariable() {
-    this = TVariableNode(result, getMinIndirectionsForType(result.getUnspecifiedType()))
+    this = TGlobalLikeVariableNode(result, getMinIndirectionsForType(result.getUnspecifiedType()))
   }
 
   /**
@@ -423,7 +406,7 @@ class Node extends TIRDataFlowNode {
    */
   Variable asIndirectVariable(int indirectionIndex) {
     indirectionIndex > getMinIndirectionsForType(result.getUnspecifiedType()) and
-    this = TVariableNode(result, indirectionIndex)
+    this = TGlobalLikeVariableNode(result, indirectionIndex)
   }
 
   /** Gets an indirection of this node's underlying variable, if any. */
@@ -465,7 +448,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)
@@ -1348,6 +1331,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)
@@ -1364,6 +1348,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
@@ -1376,6 +1376,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)
 }
 
@@ -1408,7 +1409,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 {
@@ -1550,6 +1552,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.
  */
@@ -1768,15 +1776,18 @@ class DefinitionByReferenceNode extends IndirectArgumentOutNode {
 }
 
 /**
- * A `Node` corresponding to a variable in the program, as opposed to the
- * value of that variable at some particular point. This can be used for
- * modeling flow in and out of global variables.
+ * A `Node` corresponding to a global (or `static` local) variable in the
+ * program, as opposed to the value of that variable at some particular point.
+ * This is used to model flow through global variables (and `static` local
+ * variables).
+ *
+ * There is no `VariableNode` for non-`static` local variables.
  */
-class VariableNode extends Node, TVariableNode {
+class VariableNode extends Node, TGlobalLikeVariableNode {
   Variable v;
   int indirectionIndex;
 
-  VariableNode() { this = TVariableNode(v, indirectionIndex) }
+  VariableNode() { this = TGlobalLikeVariableNode(v, indirectionIndex) }
 
   /** Gets the variable corresponding to this node. */
   Variable getVariable() { result = v }

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

@@ -4,15 +4,18 @@ private import DataFlowUtil
 private import DataFlowImplCommon as DataFlowImplCommon
 private import semmle.code.cpp.models.interfaces.Allocation as Alloc
 private import semmle.code.cpp.models.interfaces.DataFlow as DataFlow
+private import semmle.code.cpp.models.interfaces.Taint as Taint
+private import semmle.code.cpp.models.interfaces.PartialFlow as PartialFlow
+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]
     }
 
@@ -26,7 +29,7 @@ private module SourceVariables {
   }
 
   class SourceVariable extends TSourceVariable {
-    SsaInternals0::SourceVariable base;
+    BaseSourceVariable base;
     int ind;
 
     SourceVariable() { this = TMkSourceVariable(base, ind) }
@@ -38,7 +41,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() }
@@ -100,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
@@ -129,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
@@ -138,12 +132,11 @@ private newtype TDefOrUseImpl =
     isIteratorUse(container, iteratorAddress, _, indirectionIndex)
   } or
   TFinalParameterUse(Parameter p, int indirectionIndex) {
-    // Avoid creating parameter nodes if there is no definitions of the variable other than the initializaion.
-    exists(SsaInternals0::Def def |
-      def.getSourceVariable().getBaseVariable().(BaseIRVariable).getIRVariable().getAst() = p and
-      not def.getValue().asInstruction() instanceof InitializeParameterInstruction and
-      underlyingTypeIsModifiableAt(p.getUnderlyingType(), indirectionIndex)
-    )
+    underlyingTypeIsModifiableAt(p.getUnderlyingType(), indirectionIndex) and
+    // Only create an SSA read for the final use of a parameter if there's
+    // actually a body of the enclosing function. If there's no function body
+    // then we'll never need to flow out of the function anyway.
+    p.getFunction().hasDefinition()
   }
 
 private predicate isGlobalUse(
@@ -264,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) {
@@ -289,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) }
@@ -303,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) }
@@ -796,10 +829,58 @@ private Node getAPriorDefinition(SsaDefOrUse defOrUse) {
   )
 }
 
+private predicate inOut(FIO::FunctionInput input, FIO::FunctionOutput output) {
+  exists(int indirectionIndex |
+    input.isQualifierObject(indirectionIndex) and
+    output.isQualifierObject(indirectionIndex)
+    or
+    exists(int i |
+      input.isParameterDeref(i, indirectionIndex) and
+      output.isParameterDeref(i, indirectionIndex)
+    )
+  )
+}
+
+/**
+ * Holds if there should not be use-use flow out of `n`. That is, `n` is
+ * an out-barrier to use-use flow. This includes:
+ *
+ * - an input to a call that would be assumed to have use-use flow to the same
+ *   argument as an output, but this flow should be blocked because the
+ *   function is modeled with another flow to that output (for example the
+ *   first argument of `strcpy`).
+ * - a conversion that flows to such an input.
+ */
+private predicate modeledFlowBarrier(Node n) {
+  exists(
+    FIO::FunctionInput input, FIO::FunctionOutput output, CallInstruction call,
+    PartialFlow::PartialFlowFunction partialFlowFunc
+  |
+    n = callInput(call, input) and
+    inOut(input, output) and
+    exists(callOutput(call, output)) and
+    partialFlowFunc = call.getStaticCallTarget() and
+    not partialFlowFunc.isPartialWrite(output)
+  |
+    call.getStaticCallTarget().(DataFlow::DataFlowFunction).hasDataFlow(_, output)
+    or
+    call.getStaticCallTarget().(Taint::TaintFunction).hasTaintFlow(_, output)
+  )
+  or
+  exists(Operand operand, Instruction instr, Node n0, int indirectionIndex |
+    modeledFlowBarrier(n0) and
+    nodeHasInstruction(n0, instr, indirectionIndex) and
+    conversionFlow(operand, instr, false, _) and
+    nodeHasOperand(n, operand, indirectionIndex)
+  )
+}
+
 /** Holds if there is def-use or use-use flow from `nodeFrom` to `nodeTo`. */
 predicate ssaFlow(Node nodeFrom, Node nodeTo) {
   exists(Node nFrom, boolean uncertain, SsaDefOrUse defOrUse |
-    ssaFlowImpl(defOrUse, nFrom, nodeTo, uncertain) and nodeFrom != nodeTo
+    ssaFlowImpl(defOrUse, nFrom, nodeTo, uncertain) and
+    not modeledFlowBarrier(nFrom) and
+    nodeFrom != nodeTo
   |
     if uncertain = true then nodeFrom = [nFrom, getAPriorDefinition(defOrUse)] else nodeFrom = nFrom
   )
@@ -933,17 +1014,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
 ) {
@@ -967,16 +1037,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
+      )
     )
   }
 
@@ -1151,7 +1219,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/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/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/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/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/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

@@ -11,6 +11,7 @@ private import InstructionTag
 private import TranslatedCondition
 private import TranslatedElement
 private import TranslatedExpr
+private import TranslatedCall
 private import TranslatedStmt
 private import TranslatedFunction
 private import TranslatedGlobalVar

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

@@ -85,10 +85,14 @@ newtype TInstructionTag =
   // The next three cases handle generation of branching for __except handling.
   TryExceptCompareNegativeOneBranch() or
   TryExceptCompareZeroBranch() or
-  TryExceptCompareOneBranch()
+  TryExceptCompareOneBranch() or
+  ImplicitDestructorTag(int index) {
+    exists(Expr e | exists(e.getImplicitDestructorCall(index))) or
+    exists(Stmt s | exists(s.getImplicitDestructorCall(index)))
+  }
 
 class InstructionTag extends TInstructionTag {
-  final string toString() { result = "Tag" }
+  final string toString() { result = getInstructionTagId(this) }
 }
 
 /**
@@ -255,4 +259,8 @@ string getInstructionTagId(TInstructionTag tag) {
   tag = TryExceptCompareZeroBranch() and result = "TryExceptCompareZeroBranch"
   or
   tag = TryExceptCompareOneBranch() and result = "TryExceptCompareOneBranch"
+  or
+  exists(int index |
+    tag = ImplicitDestructorTag(index) and result = "ImplicitDestructor(" + index + ")"
+  )
 }

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

@@ -27,7 +27,7 @@ private CallInstruction getTranslatedCallInstruction(Call call) {
  * of a higher-level constructor (e.g. the allocator call in a `NewExpr`).
  */
 abstract class TranslatedCall extends TranslatedExpr {
-  final override TranslatedElement getChild(int id) {
+  final override TranslatedElement getChildInternal(int id) {
     // We choose the child's id in the order of evaluation.
     // The qualifier is evaluated before the call target, because the value of
     // the call target may depend on the value of the qualifier for virtual
@@ -47,13 +47,19 @@ abstract class TranslatedCall extends TranslatedExpr {
     else result = this.getFirstCallTargetInstruction(kind)
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getSideEffects().getALastInstruction()
+  }
+
+  override TranslatedElement getLastChild() { result = this.getSideEffects() }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     tag = CallTag() and
     opcode instanceof Opcode::Call and
     resultType = getTypeForPRValue(this.getCallResultType())
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getQualifier() and
     result = this.getFirstCallTargetInstruction(kind)
     or
@@ -87,7 +93,7 @@ abstract class TranslatedCall extends TranslatedExpr {
     )
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = CallTag() and
     result = this.getSideEffects().getFirstInstruction(kind)
   }
@@ -225,7 +231,7 @@ abstract class TranslatedSideEffects extends TranslatedElement {
       )
   }
 
-  final override Instruction getChildSuccessor(TranslatedElement te, EdgeKind kind) {
+  final override Instruction getChildSuccessorInternal(TranslatedElement te, EdgeKind kind) {
     exists(int i |
       this.getChild(i) = te and
       if exists(this.getChild(i + 1))
@@ -234,6 +240,10 @@ abstract class TranslatedSideEffects extends TranslatedElement {
     )
   }
 
+  override TranslatedElement getLastChild() {
+    result = this.getChild(max(int i | exists(this.getChild(i))))
+  }
+
   final override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType type) {
     none()
   }
@@ -246,7 +256,18 @@ abstract class TranslatedSideEffects extends TranslatedElement {
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  final override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getALastInstructionInternal() {
+    if exists(this.getAChild())
+    then result = this.getChild(max(int i | exists(this.getChild(i)))).getALastInstruction()
+    else
+      // If there are no side effects, the "last" instruction should be the parent call's last
+      // instruction, so that implicit destructors can be inserted in the right place.
+      result = this.getParent().getInstruction(CallTag())
+  }
+
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
+    none()
+  }
 
   /** Gets the primary instruction to be associated with each side effect instruction. */
   abstract Instruction getPrimaryInstruction();
@@ -273,8 +294,8 @@ abstract class TranslatedDirectCall extends TranslatedCall {
     resultType = getFunctionGLValueType()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
-    result = TranslatedCall.super.getInstructionSuccessor(tag, kind)
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
+    result = TranslatedCall.super.getInstructionSuccessorInternal(tag, kind)
     or
     tag = CallTargetTag() and
     result = this.getFirstArgumentOrCallInstruction(kind)
@@ -367,6 +388,16 @@ class TranslatedStructorCall extends TranslatedFunctionCall {
       context = this.getParent() and
       result = context.getReceiver()
     )
+    or
+    exists(Stmt parent |
+      expr = parent.getAnImplicitDestructorCall() and
+      result = getTranslatedExpr(expr.getQualifier().getFullyConverted()).getResult()
+    )
+    or
+    exists(Expr parent |
+      expr = parent.getAnImplicitDestructorCall() and
+      result = getTranslatedExpr(expr.getQualifier().getFullyConverted()).getResult()
+    )
   }
 
   override predicate hasQualifier() { any() }
@@ -416,19 +447,25 @@ private int initializeAllocationGroup() { result = 3 }
 abstract class TranslatedSideEffect extends TranslatedElement {
   final override TranslatedElement getChild(int n) { none() }
 
-  final override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
+    none()
+  }
 
   final override Instruction getFirstInstruction(EdgeKind kind) {
     result = this.getInstruction(OnlyInstructionTag()) and
     kind instanceof GotoEdge
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(OnlyInstructionTag())
+  }
+
   final override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType type) {
     tag = OnlyInstructionTag() and
     this.sideEffectInstruction(opcode, type)
   }
 
-  final override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     result = this.getParent().getChildSuccessor(this, kind) and
     tag = OnlyInstructionTag()
   }

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

@@ -50,19 +50,29 @@ abstract class TranslatedFlexibleCondition extends TranslatedCondition, Conditio
 {
   TranslatedFlexibleCondition() { this = TTranslatedFlexibleCondition(expr) }
 
+  final override predicate handlesDestructorsExplicitly() { none() } // TODO: this needs to be revisted when we get unnamed destructors
+
   final override TranslatedElement getChild(int id) { id = 0 and result = this.getOperand() }
 
   final override Instruction getFirstInstruction(EdgeKind kind) {
     result = this.getOperand().getFirstInstruction(kind)
   }
 
+  final override Instruction getALastInstructionInternal() {
+    result = this.getOperand().getALastInstruction()
+  }
+
   final override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     none()
   }
 
-  final override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
+    none()
+  }
 
-  final override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
+    none()
+  }
 
   abstract TranslatedCondition getOperand();
 }
@@ -88,12 +98,16 @@ class TranslatedParenthesisCondition extends TranslatedFlexibleCondition {
 abstract class TranslatedNativeCondition extends TranslatedCondition, TTranslatedNativeCondition {
   TranslatedNativeCondition() { this = TTranslatedNativeCondition(expr) }
 
-  final override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
+    none()
+  }
 }
 
 abstract class TranslatedBinaryLogicalOperation extends TranslatedNativeCondition, ConditionContext {
   override BinaryLogicalOperation expr;
 
+  final override predicate handlesDestructorsExplicitly() { none() } // TODO: this needs to be revisted when we get unnamed destructors
+
   final override TranslatedElement getChild(int id) {
     id = 0 and result = this.getLeftOperand()
     or
@@ -104,11 +118,19 @@ abstract class TranslatedBinaryLogicalOperation extends TranslatedNativeConditio
     result = this.getLeftOperand().getFirstInstruction(kind)
   }
 
+  final override Instruction getALastInstructionInternal() {
+    result = this.getLeftOperand().getALastInstruction()
+    or
+    result = this.getRightOperand().getALastInstruction()
+  }
+
   final override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     none()
   }
 
-  final override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
+    none()
+  }
 
   final TranslatedCondition getLeftOperand() {
     result = getTranslatedCondition(expr.getLeftOperand().getFullyConverted())
@@ -162,19 +184,25 @@ class TranslatedValueCondition extends TranslatedCondition, TTranslatedValueCond
     result = this.getValueExpr().getFirstInstruction(kind)
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(ValueConditionConditionalBranchTag())
+  }
+
+  final override predicate handlesDestructorsExplicitly() { none() } // TODO: this needs to be revisted when we get unnamed destructors
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     tag = ValueConditionConditionalBranchTag() and
     opcode instanceof Opcode::ConditionalBranch and
     resultType = getVoidType()
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getValueExpr() and
     result = this.getInstruction(ValueConditionConditionalBranchTag()) and
     kind instanceof GotoEdge
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = ValueConditionConditionalBranchTag() and
     (
       kind instanceof TrueEdge and

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

@@ -60,6 +60,10 @@ abstract class TranslatedLocalVariableDeclaration extends TranslatedVariableInit
    */
   abstract LocalVariable getVariable();
 
+  final override TranslatedElement getChild(int id) {
+    result = TranslatedVariableInitialization.super.getChildInternal(id)
+  }
+
   final override Type getTargetType() { result = getVariableType(this.getVariable()) }
 
   final override TranslatedInitialization getInitialization() {
@@ -152,7 +156,13 @@ class TranslatedStaticLocalVariableDeclarationEntry extends TranslatedDeclaratio
     kind instanceof GotoEdge
   }
 
-  final override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  final override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(DynamicInitializationConditionalBranchTag())
+    or
+    result = this.getInstruction(DynamicInitializationFlagStoreTag())
+  }
+
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = DynamicInitializationFlagAddressTag() and
     kind instanceof GotoEdge and
     result = this.getInstruction(DynamicInitializationFlagLoadTag())
@@ -178,7 +188,7 @@ class TranslatedStaticLocalVariableDeclarationEntry extends TranslatedDeclaratio
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  final override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitialization() and
     result = this.getInstruction(DynamicInitializationFlagConstantTag()) and
     kind instanceof GotoEdge

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

@@ -20,10 +20,14 @@ private import SideEffects
  * they were explicit nodes in the expression tree, rather than as implicit
  * nodes as in the regular AST representation.
  */
-private Element getRealParent(Expr expr) {
+Element getRealParent(Expr expr) {
   result = expr.getParentWithConversions()
   or
   result.(Destructor).getADestruction() = expr
+  or
+  result.(Expr).getAnImplicitDestructorCall() = expr
+  or
+  result.(Stmt).getAnImplicitDestructorCall() = expr
 }
 
 IRUserVariable getIRUserVariable(Declaration decl, Variable var) {
@@ -36,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.
@@ -92,6 +127,14 @@ private predicate ignoreExprAndDescendants(Expr expr) {
   exists(BuiltInVarArgsStart vaStartExpr |
     vaStartExpr.getLastNamedParameter().getFullyConverted() = expr
   )
+  or
+  // suppress destructors of temporary variables until proper support is added for them.
+  exists(Expr parent | parent.getAnImplicitDestructorCall() = expr)
+  or
+  exists(Stmt parent |
+    parent.getAnImplicitDestructorCall() = expr and
+    expr.(DestructorCall).getQualifier() instanceof ReuseExpr
+  )
 }
 
 /**
@@ -105,12 +148,6 @@ private predicate ignoreExprOnly(Expr expr) {
     newExpr.getAllocatorCall() = expr
   )
   or
-  exists(DeleteOrDeleteArrayExpr deleteExpr |
-    // Ignore the destructor call as we don't model it yet. Don't ignore
-    // its arguments, though, as they are the arguments to the deallocator.
-    deleteExpr.getDestructorCall() = expr
-  )
-  or
   // The extractor deliberately emits an `ErrorExpr` as the first argument to
   // the allocator call, if any, of a `NewOrNewArrayExpr`. That `ErrorExpr`
   // should not be translated.
@@ -118,6 +155,11 @@ 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
+  )
 }
 
 /**
@@ -608,16 +650,27 @@ newtype TTranslatedElement =
   TTranslatedInitialization(Expr expr) {
     not ignoreExpr(expr) and
     (
-      exists(Initializer init | init.getExpr().getFullyConverted() = expr) or
-      exists(ClassAggregateLiteral initList | initList.getAFieldExpr(_).getFullyConverted() = expr) or
+      exists(Initializer init | init.getExpr().getFullyConverted() = expr)
+      or
+      exists(ClassAggregateLiteral initList | initList.getAFieldExpr(_).getFullyConverted() = expr)
+      or
       exists(ArrayOrVectorAggregateLiteral initList |
         initList.getAnElementExpr(_).getFullyConverted() = expr
-      ) or
-      exists(ReturnStmt returnStmt | returnStmt.getExpr().getFullyConverted() = expr) or
-      exists(ConstructorFieldInit fieldInit | fieldInit.getExpr().getFullyConverted() = expr) or
-      exists(NewExpr newExpr | newExpr.getInitializer().getFullyConverted() = expr) or
-      exists(ThrowExpr throw | throw.getExpr().getFullyConverted() = expr) or
-      exists(TemporaryObjectExpr temp | temp.getExpr() = expr) or
+      )
+      or
+      exists(ReturnStmt returnStmt |
+        returnStmt.getExpr().getFullyConverted() = expr and
+        hasReturnValue(returnStmt.getEnclosingFunction())
+      )
+      or
+      exists(ConstructorFieldInit fieldInit | fieldInit.getExpr().getFullyConverted() = expr)
+      or
+      exists(NewExpr newExpr | newExpr.getInitializer().getFullyConverted() = expr)
+      or
+      exists(ThrowExpr throw | throw.getExpr().getFullyConverted() = expr)
+      or
+      exists(TemporaryObjectExpr temp | temp.getExpr() = expr)
+      or
       exists(LambdaExpression lambda | lambda.getInitializer().getFullyConverted() = expr)
     )
   } or
@@ -730,9 +783,13 @@ 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
@@ -750,9 +807,8 @@ 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
-    // Don't bother with destructor calls for now, since we won't see very many of them in the IR
-    // until we start injecting implicit destructor calls.
     call instanceof ConstructorCall and
     opcode = getASideEffectOpcode(call, -1)
   } or
@@ -866,6 +922,23 @@ abstract class TranslatedElement extends TTranslatedElement {
       1 + sum(TranslatedElement child | child = this.getChildByRank(_) | child.getDescendantCount())
   }
 
+  /**
+   * Holds if this element has implicit destructor calls that should follow it.
+   */
+  predicate hasAnImplicitDestructorCall() { none() }
+
+  /**
+   * Gets the child index of the first destructor call that should be executed after this `TranslatedElement`
+   */
+  int getFirstDestructorCallIndex() { none() }
+
+  /**
+   * Holds if this `TranslatedElement` includes any destructor calls that must be performed after
+   * it in its `getChildSuccessorInternal`, `getInstructionSuccessorInternal`, and
+   * `getALastInstructionInternal` relations, rather than needing them inserted.
+   */
+  predicate handlesDestructorsExplicitly() { none() }
+
   private int getUniqueId() {
     if not exists(this.getParent())
     then result = 0
@@ -901,15 +974,81 @@ abstract class TranslatedElement extends TTranslatedElement {
   /**
    * Gets the successor instruction of the instruction that was generated by
    * this element for tag `tag`. The successor edge kind is specified by `kind`.
+   * This predicate does not usually include destructors, which are inserted as
+   * part of `getInstructionSuccessor` unless `handlesDestructorsExplicitly`
+   * holds.
    */
-  abstract Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind);
+  abstract Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind);
+
+  /**
+   * Gets the successor instruction of the instruction that was generated by
+   * this element for tag `tag`. The successor edge kind is specified by `kind`.
+   */
+  final Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+    if
+      this.hasAnImplicitDestructorCall() and
+      this.getInstruction(tag) = this.getALastInstructionInternal() and
+      not this.handlesDestructorsExplicitly()
+    then
+      result = this.getChild(this.getFirstDestructorCallIndex()).getFirstInstruction(kind) and
+      kind instanceof GotoEdge
+    else result = this.getInstructionSuccessorInternal(tag, kind)
+  }
+
+  /**
+   * Gets an instruction within this `TranslatedElement` (including its transitive children) which
+   * will be followed by an instruction outside the `TranslatedElement`.
+   */
+  final Instruction getALastInstruction() {
+    if this.hasAnImplicitDestructorCall() and not this.handlesDestructorsExplicitly()
+    then result = this.getChild(max(int n | exists(this.getChild(n)))).getALastInstruction() // last destructor
+    else result = this.getALastInstructionInternal()
+  }
+
+  /**
+   * Gets an instruction within this `TranslatedElement` (including its transitive children) which
+   * will be followed by an instruction outside the `TranslatedElement`.
+   * This predicate does not usually include destructors, which are inserted as
+   * part of `getALastInstruction` unless `handlesDestructorsExplicitly` holds.
+   */
+  abstract Instruction getALastInstructionInternal();
+
+  TranslatedElement getLastChild() { none() }
+
+  /**
+   * Gets the successor instruction to which control should flow after the
+   * child element specified by `child` has finished execution. The successor
+   * edge kind is specified by `kind`.
+   * This predicate does not usually include destructors, which are inserted as
+   * part of `getChildSuccessor` unless `handlesDestructorsExplicitly` holds.
+   */
+  Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) { none() }
 
   /**
    * Gets the successor instruction to which control should flow after the
    * child element specified by `child` has finished execution. The successor
    * edge kind is specified by `kind`.
    */
-  abstract Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind);
+  final Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+    (
+      if
+        // this is the last child and we need to handle destructors for it
+        this.hasAnImplicitDestructorCall() and
+        not this.handlesDestructorsExplicitly() and
+        child = this.getLastChild()
+      then result = this.getChild(this.getFirstDestructorCallIndex()).getFirstInstruction(kind)
+      else result = this.getChildSuccessorInternal(child, kind)
+    )
+    or
+    not this.handlesDestructorsExplicitly() and
+    exists(int id |
+      id >= this.getFirstDestructorCallIndex() and
+      child = this.getChild(id) and
+      if id = max(int n | exists(this.getChild(n)))
+      then result = this.getParent().getChildSuccessor(this, kind)
+      else result = this.getChild(id + 1).getFirstInstruction(kind)
+    )
+  }
 
   /**
    * Gets the instruction to which control should flow if an exception is thrown

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

@@ -114,7 +114,11 @@ class TranslatedFunction extends TranslatedRootElement, TTranslatedFunction {
     kind instanceof GotoEdge
   }
 
-  final override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(ExitFunctionTag())
+  }
+
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     kind instanceof GotoEdge and
     (
       tag = EnterFunctionTag() and
@@ -150,7 +154,7 @@ class TranslatedFunction extends TranslatedRootElement, TTranslatedFunction {
     )
   }
 
-  final override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     exists(int paramIndex | child = this.getParameter(paramIndex) |
       if
         exists(func.getParameter(paramIndex + 1)) or
@@ -379,7 +383,13 @@ abstract class TranslatedParameter extends TranslatedElement {
     kind instanceof GotoEdge
   }
 
-  final override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getALastInstructionInternal() {
+    if this.hasIndirection()
+    then result = this.getInstruction(InitializerIndirectStoreTag())
+    else result = this.getInstruction(InitializerStoreTag())
+  }
+
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     kind instanceof GotoEdge and
     tag = InitializerVariableAddressTag() and
     result = this.getInstruction(InitializerStoreTag())
@@ -397,7 +407,9 @@ abstract class TranslatedParameter extends TranslatedElement {
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  final override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
+    none()
+  }
 
   final override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     tag = InitializerVariableAddressTag() and
@@ -611,15 +623,23 @@ class TranslatedConstructorInitList extends TranslatedElement, InitializationCon
     else result = this.getParent().getChildSuccessor(this, kind)
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getLastChild().getALastInstruction()
+  }
+
+  override TranslatedElement getLastChild() {
+    result = this.getChild(max(int id | exists(this.getChild(id))))
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     none()
   }
 
   override Function getFunction() { result = func }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     exists(int id |
       child = this.getChild(id) and
       if exists(this.getChild(id + 1))
@@ -678,15 +698,23 @@ class TranslatedDestructorDestructionList extends TranslatedElement,
     else result = this.getParent().getChildSuccessor(this, kind)
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getChild(max(int id | exists(this.getChild(id)))).getALastInstruction()
+  }
+
+  override TranslatedElement getLastChild() {
+    result = this.getChild(max(int id | exists(this.getChild(id))))
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     none()
   }
 
   override Function getFunction() { result = func }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     exists(int id |
       child = this.getChild(id) and
       if exists(this.getChild(id + 1))
@@ -728,7 +756,20 @@ class TranslatedReadEffects extends TranslatedElement, TTranslatedReadEffects {
     else result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getALastInstructionInternal() {
+    if exists(this.getAChild())
+    then
+      result =
+        max(TranslatedElement child, int id | child = this.getChild(id) | child order by id)
+            .getFirstInstruction(any(GotoEdge goto))
+    else result = this.getParent().getChildSuccessor(this, any(GotoEdge goto))
+  }
+
+  override TranslatedElement getLastChild() {
+    result = this.getChild(max(int id | exists(this.getChild(id))))
+  }
+
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     exists(int id | child = this.getChild(id) |
       if exists(TranslatedReadEffect child2, int id2 | id2 > id and child2 = this.getChild(id2))
       then
@@ -746,7 +787,7 @@ class TranslatedReadEffects extends TranslatedElement, TTranslatedReadEffects {
     none()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
 }
 
 private TranslatedThisReadEffect getTranslatedThisReadEffect(Function func) {
@@ -760,9 +801,9 @@ private TranslatedParameterReadEffect getTranslatedParameterReadEffect(Parameter
 abstract class TranslatedReadEffect extends TranslatedElement {
   override TranslatedElement getChild(int id) { none() }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) { none() }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = OnlyInstructionTag() and
     result = this.getParent().getChildSuccessor(this, kind)
   }
@@ -772,6 +813,10 @@ abstract class TranslatedReadEffect extends TranslatedElement {
     kind instanceof GotoEdge
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(OnlyInstructionTag())
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     opcode instanceof Opcode::ReturnIndirection and
     tag = OnlyInstructionTag() and

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

@@ -27,6 +27,10 @@ class TranslatedStaticStorageDurationVarInit extends TranslatedRootElement,
     kind instanceof GotoEdge
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(ExitFunctionTag())
+  }
+
   override TranslatedElement getChild(int n) {
     n = 1 and
     result = getTranslatedInitialization(var.getInitializer().getExpr().getFullyConverted())
@@ -58,7 +62,7 @@ class TranslatedStaticStorageDurationVarInit extends TranslatedRootElement,
     type = getVoidType()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     kind instanceof GotoEdge and
     (
       tag = EnterFunctionTag() and
@@ -81,7 +85,7 @@ class TranslatedStaticStorageDurationVarInit extends TranslatedRootElement,
     )
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getChild(1) and
     result = this.getInstruction(ReturnTag()) and
     kind instanceof GotoEdge

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

@@ -35,13 +35,19 @@ abstract class InitializationContext extends TranslatedElement {
  * declarations, `return` statements, and `throw` expressions.
  */
 abstract class TranslatedVariableInitialization extends TranslatedElement, InitializationContext {
-  final override TranslatedElement getChild(int id) { id = 0 and result = this.getInitialization() }
+  TranslatedElement getChildInternal(int id) { id = 0 and result = this.getInitialization() }
 
   final override Instruction getFirstInstruction(EdgeKind kind) {
     result = this.getInstruction(InitializerVariableAddressTag()) and
     kind instanceof GotoEdge
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInitialization().getALastInstruction()
+    or
+    not exists(this.getInitialization()) and result = this.getInstruction(OnlyInstructionTag())
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     tag = InitializerVariableAddressTag() and
     opcode instanceof Opcode::VariableAddress and
@@ -53,7 +59,7 @@ abstract class TranslatedVariableInitialization extends TranslatedElement, Initi
     resultType = getTypeForPRValue(this.getTargetType())
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     (
       tag = InitializerVariableAddressTag() and
       if this.hasUninitializedInstruction()
@@ -71,7 +77,7 @@ abstract class TranslatedVariableInitialization extends TranslatedElement, Initi
     )
   }
 
-  final override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitialization() and
     result = this.getInitializationSuccessor(kind)
   }
@@ -177,7 +183,11 @@ abstract class TranslatedListInitialization extends TranslatedInitialization, In
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getALastInstructionInternal() {
+    result = this.getChild(max(int i | exists(this.getChild(i)))).getALastInstruction()
+  }
+
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     exists(int index |
       child = this.getChild(index) and
       if exists(this.getChild(index + 1))
@@ -190,7 +200,9 @@ abstract class TranslatedListInitialization extends TranslatedInitialization, In
     none()
   }
 
-  final override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
+    none()
+  }
 
   override Instruction getTargetAddress() { result = this.getContext().getTargetAddress() }
 
@@ -260,18 +272,22 @@ class TranslatedSimpleDirectInitialization extends TranslatedDirectInitializatio
     not expr instanceof StringLiteral
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(InitializerStoreTag())
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     tag = InitializerStoreTag() and
     opcode instanceof Opcode::Store and
     resultType = getTypeForPRValue(this.getContext().getTargetType())
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = InitializerStoreTag() and
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitializer() and
     result = this.getInstruction(InitializerStoreTag()) and
     kind instanceof GotoEdge
@@ -296,6 +312,12 @@ class TranslatedSimpleDirectInitialization extends TranslatedDirectInitializatio
 class TranslatedStringLiteralInitialization extends TranslatedDirectInitialization {
   override StringLiteral expr;
 
+  override Instruction getALastInstructionInternal() {
+    if this.zeroInitRange(_, _)
+    then result = this.getInstruction(ZeroPadStringStoreTag())
+    else result = this.getInstruction(InitializerStoreTag())
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     // Load the string literal to make it a prvalue of type `char[len]`
     tag = InitializerLoadStringTag() and
@@ -337,7 +359,7 @@ class TranslatedStringLiteralInitialization extends TranslatedDirectInitializati
     )
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     kind instanceof GotoEdge and
     tag = InitializerLoadStringTag() and
     result = this.getInstruction(InitializerStoreTag())
@@ -367,7 +389,7 @@ class TranslatedStringLiteralInitialization extends TranslatedDirectInitializati
     )
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitializer() and
     result = this.getInstruction(InitializerLoadStringTag()) and
     kind instanceof GotoEdge
@@ -457,16 +479,22 @@ class TranslatedConstructorInitialization extends TranslatedDirectInitialization
 {
   override ConstructorCall expr;
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInitializer().getALastInstruction()
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     none()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitializer() and result = this.getParent().getChildSuccessor(this, kind)
   }
 
+  override TranslatedElement getLastChild() { result = this.getInitializer() }
+
   override Instruction getInstructionRegisterOperand(InstructionTag tag, OperandTag operandTag) {
     none()
   }
@@ -558,23 +586,29 @@ class TranslatedExplicitFieldInitialization extends TranslatedFieldInitializatio
     this = TTranslatedExplicitFieldInitialization(ast, field, expr, position)
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInitialization().getALastInstruction()
+  }
+
   override Instruction getTargetAddress() {
     result = this.getInstruction(this.getFieldAddressTag())
   }
 
   override Type getTargetType() { result = field.getUnspecifiedType() }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = this.getFieldAddressTag() and
     result = this.getInitialization().getFirstInstruction(kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitialization() and result = this.getParent().getChildSuccessor(this, kind)
   }
 
   override TranslatedElement getChild(int id) { id = 0 and result = this.getInitialization() }
 
+  override TranslatedElement getLastChild() { result = this.getInitialization() }
+
   private TranslatedInitialization getInitialization() {
     result = getTranslatedInitialization(expr)
   }
@@ -595,6 +629,10 @@ class TranslatedFieldValueInitialization extends TranslatedFieldInitialization,
 {
   TranslatedFieldValueInitialization() { this = TTranslatedFieldValueInitialization(ast, field) }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(this.getFieldDefaultValueStoreTag())
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     TranslatedFieldInitialization.super.hasInstruction(opcode, tag, resultType)
     or
@@ -607,7 +645,7 @@ class TranslatedFieldValueInitialization extends TranslatedFieldInitialization,
     resultType = getTypeForPRValue(field.getUnspecifiedType())
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     kind instanceof GotoEdge and
     (
       tag = this.getFieldAddressTag() and
@@ -639,7 +677,7 @@ class TranslatedFieldValueInitialization extends TranslatedFieldInitialization,
     )
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) { none() }
 
   override TranslatedElement getChild(int id) { none() }
 
@@ -689,7 +727,7 @@ abstract class TranslatedElementInitialization extends TranslatedElement {
     resultType = getTypeForGLValue(this.getElementType())
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = this.getElementIndexTag() and
     result = this.getInstruction(this.getElementAddressTag()) and
     kind instanceof GotoEdge
@@ -743,20 +781,24 @@ class TranslatedExplicitElementInitialization extends TranslatedElementInitializ
     this = TTranslatedExplicitElementInitialization(initList, elementIndex, position)
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInitialization().getALastInstruction()
+  }
+
   override Instruction getTargetAddress() {
     result = this.getInstruction(this.getElementAddressTag())
   }
 
   override Type getTargetType() { result = this.getElementType() }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
-    result = TranslatedElementInitialization.super.getInstructionSuccessor(tag, kind)
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
+    result = TranslatedElementInitialization.super.getInstructionSuccessorInternal(tag, kind)
     or
     tag = this.getElementAddressTag() and
     result = this.getInitialization().getFirstInstruction(kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitialization() and result = this.getParent().getChildSuccessor(this, kind)
   }
 
@@ -788,6 +830,10 @@ class TranslatedElementValueInitialization extends TranslatedElementInitializati
     this = TTranslatedElementValueInitialization(initList, elementIndex, elementCount)
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(this.getElementDefaultValueStoreTag())
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     TranslatedElementInitialization.super.hasInstruction(opcode, tag, resultType)
     or
@@ -800,8 +846,8 @@ class TranslatedElementValueInitialization extends TranslatedElementInitializati
     resultType = this.getDefaultValueType()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
-    result = TranslatedElementInitialization.super.getInstructionSuccessor(tag, kind)
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
+    result = TranslatedElementInitialization.super.getInstructionSuccessorInternal(tag, kind)
     or
     kind instanceof GotoEdge and
     (
@@ -836,7 +882,7 @@ class TranslatedElementValueInitialization extends TranslatedElementInitializati
     )
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) { none() }
 
   override TranslatedElement getChild(int id) { none() }
 
@@ -876,11 +922,13 @@ abstract class TranslatedStructorCallFromStructor extends TranslatedElement, Str
 
   final override Function getFunction() { result = getEnclosingFunction(call) }
 
-  final override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getStructorCall() and
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
+  override TranslatedElement getLastChild() { result = this.getStructorCall() }
+
   final TranslatedExpr getStructorCall() { result = getTranslatedExpr(call) }
 }
 
@@ -894,13 +942,17 @@ abstract class TranslatedBaseStructorCall extends TranslatedStructorCallFromStru
     kind instanceof GotoEdge
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getStructorCall().getALastInstruction()
+  }
+
   final override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     tag = OnlyInstructionTag() and
     opcode instanceof Opcode::ConvertToNonVirtualBase and
     resultType = getTypeForGLValue(call.getTarget().getDeclaringType())
   }
 
-  final override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = OnlyInstructionTag() and
     result = this.getStructorCall().getFirstInstruction(kind)
   }
@@ -947,11 +999,17 @@ class TranslatedConstructorDelegationInit extends TranslatedConstructorCallFromC
     result = this.getStructorCall().getFirstInstruction(kind)
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getStructorCall().getALastInstruction()
+  }
+
   final override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     none()
   }
 
-  final override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
+    none()
+  }
 
   final override Instruction getReceiver() {
     result = getTranslatedFunction(this.getFunction()).getInitializeThisInstruction()
@@ -1009,6 +1067,8 @@ class TranslatedConstructorBareInit extends TranslatedElement, TTranslatedConstr
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
+  override Instruction getALastInstructionInternal() { none() }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     none()
   }
@@ -1017,9 +1077,9 @@ class TranslatedConstructorBareInit extends TranslatedElement, TTranslatedConstr
 
   override Declaration getFunction() { result = this.getParent().getFunction() }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) { none() }
 }
 
 TranslatedConstructorBareInit getTranslatedConstructorBareInit(ConstructorInit init) {

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

@@ -138,7 +138,7 @@ class TranslatedMicrosoftTryExceptHandler extends TranslatedElement,
     result = "1"
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     // Generate -1 -> Compare condition
     tag = TryExceptGenerateNegativeOne() and
     kind instanceof GotoEdge and
@@ -202,7 +202,7 @@ class TranslatedMicrosoftTryExceptHandler extends TranslatedElement,
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     kind instanceof GotoEdge and
     child = this.getTranslatedCondition() and
     result = this.getInstruction(TryExceptGenerateNegativeOne())
@@ -211,6 +211,14 @@ class TranslatedMicrosoftTryExceptHandler extends TranslatedElement,
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
+  override TranslatedElement getLastChild() { result = this.getTranslatedHandler() }
+
+  override Instruction getALastInstructionInternal() {
+    result = this.getTranslatedHandler().getALastInstruction()
+    or
+    result = this.getInstruction(UnwindTag())
+  }
+
   private TranslatedExpr getTranslatedCondition() {
     result = getTranslatedExpr(tryExcept.getCondition())
   }
@@ -235,6 +243,41 @@ abstract class TranslatedStmt extends TranslatedElement, TTranslatedStmt {
 
   TranslatedStmt() { this = TTranslatedStmt(stmt) }
 
+  abstract TranslatedElement getChildInternal(int id);
+
+  final override TranslatedElement getChild(int id) {
+    result = this.getChildInternal(id)
+    or
+    exists(int destructorIndex, int tempDestructorCount |
+      result.(TranslatedExpr).getExpr() = stmt.getImplicitDestructorCall(destructorIndex) and
+      id = this.getFirstDestructorCallIndex() + destructorIndex - tempDestructorCount and
+      // suppress destructors of temporary variables until proper support is added for them.
+      tempDestructorCount =
+        count(DestructorCall call, int tempIndex |
+          stmt.getImplicitDestructorCall(tempIndex) = call and
+          tempIndex < destructorIndex and
+          call.getQualifier() instanceof ReuseExpr
+        |
+          call
+        ) and
+      not stmt.getImplicitDestructorCall(destructorIndex).getQualifier() instanceof ReuseExpr
+    )
+  }
+
+  final override int getFirstDestructorCallIndex() {
+    result = max(int childId | exists(this.getChildInternal(childId))) + 1
+    or
+    not exists(this.getChildInternal(_)) and result = 0
+  }
+
+  final override predicate hasAnImplicitDestructorCall() {
+    exists(stmt.getAnImplicitDestructorCall()) and
+    // suppress destructors of temporary variables until proper support is added for them.
+    exists(Expr expr | stmt.getAnImplicitDestructorCall().getQualifier() = expr |
+      not expr instanceof ReuseExpr
+    )
+  }
+
   final override string toString() { result = stmt.toString() }
 
   final override Locatable getAst() { result = stmt }
@@ -252,25 +295,29 @@ class TranslatedEmptyStmt extends TranslatedStmt {
     stmt instanceof SwitchCase
   }
 
-  override TranslatedElement getChild(int id) { none() }
+  override TranslatedElement getChildInternal(int id) { none() }
 
   override Instruction getFirstInstruction(EdgeKind kind) {
     result = this.getInstruction(OnlyInstructionTag()) and
     kind instanceof GotoEdge
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(OnlyInstructionTag())
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     tag = OnlyInstructionTag() and
     opcode instanceof Opcode::NoOp and
     resultType = getVoidType()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = OnlyInstructionTag() and
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) { none() }
 }
 
 /**
@@ -281,7 +328,7 @@ class TranslatedEmptyStmt extends TranslatedStmt {
 class TranslatedDeclStmt extends TranslatedStmt {
   override DeclStmt stmt;
 
-  override TranslatedElement getChild(int id) { result = this.getDeclarationEntry(id) }
+  override TranslatedElement getChildInternal(int id) { result = this.getDeclarationEntry(id) }
 
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     none()
@@ -294,6 +341,12 @@ class TranslatedDeclStmt extends TranslatedStmt {
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getChild(this.getChildCount() - 1).getALastInstruction()
+  }
+
+  override TranslatedElement getLastChild() { result = this.getChild(this.getChildCount() - 1) }
+
   private int getChildCount() { result = count(this.getDeclarationEntry(_)) }
 
   IRDeclarationEntry getIRDeclarationEntry(int index) {
@@ -318,9 +371,9 @@ class TranslatedDeclStmt extends TranslatedStmt {
       )
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     exists(int index |
       child = this.getDeclarationEntry(index) and
       if index = (this.getChildCount() - 1)
@@ -335,7 +388,7 @@ class TranslatedExprStmt extends TranslatedStmt {
 
   TranslatedExpr getExpr() { result = getTranslatedExpr(stmt.getExpr().getFullyConverted()) }
 
-  override TranslatedElement getChild(int id) { id = 0 and result = this.getExpr() }
+  override TranslatedElement getChildInternal(int id) { id = 0 and result = this.getExpr() }
 
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     none()
@@ -345,9 +398,15 @@ class TranslatedExprStmt extends TranslatedStmt {
     result = this.getExpr().getFirstInstruction(kind)
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getALastInstructionInternal() {
+    result = this.getExpr().getALastInstruction()
+  }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override TranslatedElement getLastChild() { result = this.getExpr() }
+
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
+
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getExpr() and
     result = this.getParent().getChildSuccessor(this, kind)
   }
@@ -359,6 +418,21 @@ abstract class TranslatedReturnStmt extends TranslatedStmt {
   final TranslatedFunction getEnclosingFunction() {
     result = getTranslatedFunction(stmt.getEnclosingFunction())
   }
+
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
+    exists(int id |
+      child = this.getChild(id) and
+      id >= this.getFirstDestructorCallIndex() and
+      (
+        result = this.getChild(id + 1).getFirstInstruction(kind)
+        or
+        not exists(this.getChild(id + 1)) and
+        result = this.getEnclosingFunction().getReturnSuccessorInstruction(kind)
+      )
+    )
+  }
+
+  final override predicate handlesDestructorsExplicitly() { any() }
 }
 
 /**
@@ -368,7 +442,19 @@ class TranslatedReturnValueStmt extends TranslatedReturnStmt, TranslatedVariable
   TranslatedReturnValueStmt() { stmt.hasExpr() and hasReturnValue(stmt.getEnclosingFunction()) }
 
   final override Instruction getInitializationSuccessor(EdgeKind kind) {
-    result = this.getEnclosingFunction().getReturnSuccessorInstruction(kind)
+    if this.hasAnImplicitDestructorCall()
+    then result = this.getChild(1).getFirstInstruction(kind)
+    else result = this.getEnclosingFunction().getReturnSuccessorInstruction(kind)
+  }
+
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
+    result = TranslatedVariableInitialization.super.getChildSuccessorInternal(child, kind)
+    or
+    result = TranslatedReturnStmt.super.getChildSuccessorInternal(child, kind)
+  }
+
+  final override TranslatedElement getChildInternal(int id) {
+    result = TranslatedVariableInitialization.super.getChildInternal(id)
   }
 
   final override Type getTargetType() { result = this.getEnclosingFunction().getReturnType() }
@@ -390,7 +476,7 @@ class TranslatedReturnVoidExpressionStmt extends TranslatedReturnStmt {
     stmt.hasExpr() and not hasReturnValue(stmt.getEnclosingFunction())
   }
 
-  override TranslatedElement getChild(int id) {
+  override TranslatedElement getChildInternal(int id) {
     id = 0 and
     result = this.getExpr()
   }
@@ -399,21 +485,31 @@ class TranslatedReturnVoidExpressionStmt extends TranslatedReturnStmt {
     result = this.getExpr().getFirstInstruction(kind)
   }
 
+  override Instruction getALastInstructionInternal() {
+    if this.hasAnImplicitDestructorCall()
+    then result = this.getChild(max(int id | exists(this.getChild(id)))).getALastInstruction()
+    else result = this.getInstruction(OnlyInstructionTag())
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     tag = OnlyInstructionTag() and
     opcode instanceof Opcode::NoOp and
     resultType = getVoidType()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = OnlyInstructionTag() and
-    result = this.getEnclosingFunction().getReturnSuccessorInstruction(kind)
+    if this.hasAnImplicitDestructorCall()
+    then result = this.getChild(1).getFirstInstruction(kind)
+    else result = this.getEnclosingFunction().getReturnSuccessorInstruction(kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getExpr() and
     result = this.getInstruction(OnlyInstructionTag()) and
     kind instanceof GotoEdge
+    or
+    result = TranslatedReturnStmt.super.getChildSuccessorInternal(child, kind)
   }
 
   private TranslatedExpr getExpr() { result = getTranslatedExpr(stmt.getExpr()) }
@@ -428,25 +524,43 @@ class TranslatedReturnVoidStmt extends TranslatedReturnStmt {
     not stmt.hasExpr() and not hasReturnValue(stmt.getEnclosingFunction())
   }
 
-  override TranslatedElement getChild(int id) { none() }
+  override TranslatedElement getChildInternal(int id) { none() }
 
   override Instruction getFirstInstruction(EdgeKind kind) {
     result = this.getInstruction(OnlyInstructionTag()) and
     kind instanceof GotoEdge
   }
 
+  override Instruction getALastInstructionInternal() {
+    if this.hasAnImplicitDestructorCall()
+    then result = this.getChild(max(int id | exists(this.getChild(id)))).getALastInstruction()
+    else result = this.getInstruction(OnlyInstructionTag())
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     tag = OnlyInstructionTag() and
     opcode instanceof Opcode::NoOp and
     resultType = getVoidType()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = OnlyInstructionTag() and
-    result = this.getEnclosingFunction().getReturnSuccessorInstruction(kind)
+    if this.hasAnImplicitDestructorCall()
+    then result = this.getChild(0).getFirstInstruction(kind)
+    else result = this.getEnclosingFunction().getReturnSuccessorInstruction(kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
+    exists(int id |
+      this.getChild(id) = child and
+      (
+        result = this.getChild(id + 1).getFirstInstruction(kind)
+        or
+        not exists(this.getChild(id + 1)) and
+        result = this.getEnclosingFunction().getReturnSuccessorInstruction(kind)
+      )
+    )
+  }
 }
 
 /**
@@ -464,6 +578,16 @@ class TranslatedNoValueReturnStmt extends TranslatedReturnStmt, TranslatedVariab
     result = this.getEnclosingFunction().getReturnSuccessorInstruction(kind)
   }
 
+  final override TranslatedElement getChildInternal(int id) {
+    result = TranslatedVariableInitialization.super.getChildInternal(id)
+  }
+
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
+    result = TranslatedVariableInitialization.super.getChildSuccessorInternal(child, kind)
+    or
+    result = TranslatedReturnStmt.super.getChildSuccessorInternal(child, kind)
+  }
+
   final override Type getTargetType() { result = this.getEnclosingFunction().getReturnType() }
 
   final override TranslatedInitialization getInitialization() { none() }
@@ -518,7 +642,7 @@ private class TryOrMicrosoftTryStmt extends Stmt {
 class TranslatedTryStmt extends TranslatedStmt {
   override TryOrMicrosoftTryStmt stmt;
 
-  override TranslatedElement getChild(int id) {
+  override TranslatedElement getChildInternal(int id) {
     id = 0 and result = this.getBody()
     or
     result = this.getHandler(id - 1)
@@ -531,13 +655,23 @@ class TranslatedTryStmt extends TranslatedStmt {
     none()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
 
   override Instruction getFirstInstruction(EdgeKind kind) {
     result = this.getBody().getFirstInstruction(kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getALastInstructionInternal() {
+    result = this.getLastChild().getALastInstruction()
+  }
+
+  override TranslatedElement getLastChild() {
+    if exists(this.getFinally())
+    then result = this.getFinally()
+    else result = [this.getBody(), this.getHandler(_)]
+  }
+
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     // All non-finally children go to the successor of the `try` if
     // there is no finally block, but if there is a finally block
     // then we go to that one.
@@ -581,7 +715,7 @@ class TranslatedTryStmt extends TranslatedStmt {
 class TranslatedBlock extends TranslatedStmt {
   override BlockStmt stmt;
 
-  override TranslatedElement getChild(int id) { result = this.getStmt(id) }
+  override TranslatedElement getChildInternal(int id) { result = this.getStmt(id) }
 
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     this.isEmpty() and
@@ -596,18 +730,26 @@ class TranslatedBlock extends TranslatedStmt {
     else result = this.getStmt(0).getFirstInstruction(kind)
   }
 
+  override Instruction getALastInstructionInternal() {
+    if this.isEmpty()
+    then result = this.getInstruction(OnlyInstructionTag())
+    else result = this.getStmt(this.getStmtCount() - 1).getFirstInstruction(any(GotoEdge goto))
+  }
+
+  override TranslatedElement getLastChild() { result = this.getStmt(this.getStmtCount() - 1) }
+
   private predicate isEmpty() { not exists(stmt.getStmt(0)) }
 
   private TranslatedStmt getStmt(int index) { result = getTranslatedStmt(stmt.getStmt(index)) }
 
   private int getStmtCount() { result = stmt.getNumStmt() }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = OnlyInstructionTag() and
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     exists(int index |
       child = this.getStmt(index) and
       if index = (this.getStmtCount() - 1)
@@ -623,14 +765,20 @@ class TranslatedBlock extends TranslatedStmt {
 abstract class TranslatedHandler extends TranslatedStmt {
   override Handler stmt;
 
-  override TranslatedElement getChild(int id) { id = 1 and result = this.getBlock() }
+  override TranslatedElement getChildInternal(int id) { id = 1 and result = this.getBlock() }
 
   override Instruction getFirstInstruction(EdgeKind kind) {
     result = this.getInstruction(CatchTag()) and
     kind instanceof GotoEdge
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getALastInstructionInternal() {
+    result = this.getBlock().getALastInstruction()
+  }
+
+  override TranslatedElement getLastChild() { result = this.getBlock() }
+
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getBlock() and result = this.getParent().getChildSuccessor(this, kind)
   }
 
@@ -656,20 +804,20 @@ class TranslatedCatchByTypeHandler extends TranslatedHandler {
     resultType = getVoidType()
   }
 
-  override TranslatedElement getChild(int id) {
-    result = super.getChild(id)
+  override TranslatedElement getChildInternal(int id) {
+    result = super.getChildInternal(id)
     or
     id = 0 and result = this.getParameter()
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
-    result = super.getChildSuccessor(child, kind)
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
+    result = super.getChildSuccessorInternal(child, kind)
     or
     child = this.getParameter() and
     result = this.getBlock().getFirstInstruction(kind)
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = CatchTag() and
     (
       kind instanceof GotoEdge and
@@ -702,7 +850,7 @@ class TranslatedCatchAnyHandler extends TranslatedHandler {
     resultType = getVoidType()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = CatchTag() and
     result = this.getBlock().getFirstInstruction(kind)
   }
@@ -717,7 +865,13 @@ class TranslatedIfStmt extends TranslatedStmt, ConditionContext {
     else result = this.getFirstConditionInstruction(kind)
   }
 
-  override TranslatedElement getChild(int id) {
+  override Instruction getALastInstructionInternal() {
+    result = this.getElse().getALastInstruction() or result = this.getThen().getALastInstruction()
+  }
+
+  override TranslatedElement getLastChild() { result = this.getElse() or result = this.getThen() }
+
+  override TranslatedElement getChildInternal(int id) {
     id = 0 and result = this.getInitialization()
     or
     id = 1 and result = this.getCondition()
@@ -747,7 +901,7 @@ class TranslatedIfStmt extends TranslatedStmt, ConditionContext {
 
   private predicate hasElse() { exists(stmt.getElse()) }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
 
   override Instruction getChildTrueSuccessor(TranslatedCondition child, EdgeKind kind) {
     child = this.getCondition() and
@@ -761,7 +915,7 @@ class TranslatedIfStmt extends TranslatedStmt, ConditionContext {
     else result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitialization() and
     result = this.getFirstConditionInstruction(kind)
     or
@@ -783,7 +937,7 @@ class TranslatedConstExprIfStmt extends TranslatedStmt, ConditionContext {
     else result = this.getFirstConditionInstruction(kind)
   }
 
-  override TranslatedElement getChild(int id) {
+  override TranslatedElement getChildInternal(int id) {
     id = 0 and result = this.getInitialization()
     or
     id = 1 and result = this.getCondition()
@@ -813,7 +967,7 @@ class TranslatedConstExprIfStmt extends TranslatedStmt, ConditionContext {
 
   private predicate hasElse() { exists(stmt.getElse()) }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
 
   override Instruction getChildTrueSuccessor(TranslatedCondition child, EdgeKind kind) {
     child = this.getCondition() and
@@ -827,7 +981,7 @@ class TranslatedConstExprIfStmt extends TranslatedStmt, ConditionContext {
     else result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitialization() and
     result = this.getFirstConditionInstruction(kind)
     or
@@ -838,11 +992,23 @@ class TranslatedConstExprIfStmt extends TranslatedStmt, ConditionContext {
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     none()
   }
+
+  override Instruction getALastInstructionInternal() {
+    result = this.getThen().getALastInstruction()
+    or
+    result = this.getElse().getALastInstruction()
+  }
 }
 
 abstract class TranslatedLoop extends TranslatedStmt, ConditionContext {
   override Loop stmt;
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getCondition().getALastInstruction()
+  }
+
+  override TranslatedElement getLastChild() { result = this.getCondition() }
+
   final TranslatedCondition getCondition() {
     result = getTranslatedCondition(stmt.getCondition().getFullyConverted())
   }
@@ -857,7 +1023,7 @@ abstract class TranslatedLoop extends TranslatedStmt, ConditionContext {
 
   final predicate hasCondition() { exists(stmt.getCondition()) }
 
-  override TranslatedElement getChild(int id) {
+  override TranslatedElement getChildInternal(int id) {
     id = 0 and result = this.getCondition()
     or
     id = 1 and result = this.getBody()
@@ -867,13 +1033,15 @@ abstract class TranslatedLoop extends TranslatedStmt, ConditionContext {
     none()
   }
 
-  final override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
+    none()
+  }
 
   final override Instruction getChildTrueSuccessor(TranslatedCondition child, EdgeKind kind) {
     child = this.getCondition() and result = this.getBody().getFirstInstruction(kind)
   }
 
-  final override Instruction getChildFalseSuccessor(TranslatedCondition child, EdgeKind kind) {
+  override Instruction getChildFalseSuccessor(TranslatedCondition child, EdgeKind kind) {
     child = this.getCondition() and
     result = this.getParent().getChildSuccessor(this, kind)
   }
@@ -882,13 +1050,36 @@ abstract class TranslatedLoop extends TranslatedStmt, ConditionContext {
 class TranslatedWhileStmt extends TranslatedLoop {
   TranslatedWhileStmt() { stmt instanceof WhileStmt }
 
+  override TranslatedElement getChildInternal(int id) {
+    id = 0 and result = this.getCondition()
+    or
+    id = 1 and result = this.getBody()
+    or
+    exists(int n |
+      result.getAst() = stmt.getImplicitDestructorCall(n) and
+      id = 2 + n
+    )
+  }
+
+  override predicate handlesDestructorsExplicitly() { any() }
+
+  final override Instruction getChildFalseSuccessor(TranslatedCondition child, EdgeKind kind) {
+    child = this.getCondition() and
+    if this.hasAnImplicitDestructorCall()
+    then result = this.getChild(this.getFirstDestructorCallIndex()).getFirstInstruction(kind)
+    else result = this.getParent().getChildSuccessor(this, kind)
+  }
+
   override Instruction getFirstInstruction(EdgeKind kind) {
     result = this.getFirstConditionInstruction(kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getBody() and
     result = this.getFirstConditionInstruction(kind)
+    or
+    child = this.getChild(this.getFirstDestructorCallIndex()) and
+    result = this.getParent().getChildSuccessor(this, kind)
   }
 }
 
@@ -899,7 +1090,7 @@ class TranslatedDoStmt extends TranslatedLoop {
     result = this.getBody().getFirstInstruction(kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getBody() and
     result = this.getFirstConditionInstruction(kind)
   }
@@ -908,7 +1099,16 @@ class TranslatedDoStmt extends TranslatedLoop {
 class TranslatedForStmt extends TranslatedLoop {
   override ForStmt stmt;
 
-  override TranslatedElement getChild(int id) {
+  override predicate handlesDestructorsExplicitly() { any() }
+
+  final override Instruction getChildFalseSuccessor(TranslatedCondition child, EdgeKind kind) {
+    child = this.getCondition() and
+    if this.hasAnImplicitDestructorCall()
+    then result = this.getChild(this.getFirstDestructorCallIndex()).getFirstInstruction(kind)
+    else result = this.getParent().getChildSuccessor(this, kind)
+  }
+
+  override TranslatedElement getChildInternal(int id) {
     id = 0 and result = this.getInitialization()
     or
     id = 1 and result = this.getCondition()
@@ -916,6 +1116,11 @@ class TranslatedForStmt extends TranslatedLoop {
     id = 2 and result = this.getUpdate()
     or
     id = 3 and result = this.getBody()
+    or
+    exists(int n |
+      result.getAst() = stmt.getImplicitDestructorCall(n) and
+      id = 4 + n
+    )
   }
 
   private TranslatedStmt getInitialization() {
@@ -934,7 +1139,7 @@ class TranslatedForStmt extends TranslatedLoop {
     else result = this.getFirstConditionInstruction(kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitialization() and
     result = this.getFirstConditionInstruction(kind)
     or
@@ -946,6 +1151,19 @@ class TranslatedForStmt extends TranslatedLoop {
     )
     or
     child = this.getUpdate() and result = this.getFirstConditionInstruction(kind)
+    or
+    exists(int destructorId |
+      destructorId >= this.getFirstDestructorCallIndex() and
+      child = this.getChild(destructorId) and
+      result = this.getChild(destructorId + 1).getFirstInstruction(kind)
+    )
+    or
+    exists(int lastDestructorIndex |
+      lastDestructorIndex =
+        max(int n | exists(this.getChild(n)) and n >= this.getFirstDestructorCallIndex()) and
+      child = this.getChild(lastDestructorIndex) and
+      result = this.getParent().getChildSuccessor(this, kind)
+    )
   }
 }
 
@@ -959,7 +1177,7 @@ class TranslatedForStmt extends TranslatedLoop {
 class TranslatedRangeBasedForStmt extends TranslatedStmt, ConditionContext {
   override RangeBasedForStmt stmt;
 
-  override TranslatedElement getChild(int id) {
+  override TranslatedElement getChildInternal(int id) {
     id = 0 and result = this.getInitialization()
     or
     id = 1 and result = this.getRangeVariableDeclStmt()
@@ -988,7 +1206,13 @@ class TranslatedRangeBasedForStmt extends TranslatedStmt, ConditionContext {
     else result = this.getFirstRangeVariableDeclStmtInstruction(kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getALastInstructionInternal() {
+    result = this.getCondition().getALastInstruction()
+  }
+
+  override TranslatedElement getLastChild() { result = this.getCondition() }
+
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitialization() and
     result = this.getFirstRangeVariableDeclStmtInstruction(kind)
     or
@@ -1012,7 +1236,7 @@ class TranslatedRangeBasedForStmt extends TranslatedStmt, ConditionContext {
     none()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
 
   override Instruction getChildTrueSuccessor(TranslatedCondition child, EdgeKind kind) {
     child = this.getCondition() and
@@ -1070,7 +1294,11 @@ class TranslatedJumpStmt extends TranslatedStmt {
     kind instanceof GotoEdge
   }
 
-  override TranslatedElement getChild(int id) { none() }
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(OnlyInstructionTag())
+  }
+
+  override TranslatedElement getChildInternal(int id) { none() }
 
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     tag = OnlyInstructionTag() and
@@ -1078,12 +1306,12 @@ class TranslatedJumpStmt extends TranslatedStmt {
     resultType = getVoidType()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = OnlyInstructionTag() and
     result = getTranslatedStmt(stmt.getTarget()).getFirstInstruction(kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) { none() }
 }
 
 private EdgeKind getCaseEdge(SwitchCase switchCase) {
@@ -1114,7 +1342,13 @@ class TranslatedSwitchStmt extends TranslatedStmt {
     else result = this.getFirstExprInstruction(kind)
   }
 
-  override TranslatedElement getChild(int id) {
+  override Instruction getALastInstructionInternal() {
+    result = this.getBody().getALastInstruction()
+  }
+
+  override TranslatedElement getLastChild() { result = this.getBody() }
+
+  override TranslatedElement getChildInternal(int id) {
     id = 0 and result = this.getInitialization()
     or
     id = 1 and result = this.getExpr()
@@ -1140,7 +1374,7 @@ class TranslatedSwitchStmt extends TranslatedStmt {
     result = this.getExpr().getResult()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = SwitchBranchTag() and
     exists(SwitchCase switchCase |
       switchCase = stmt.getASwitchCase() and
@@ -1154,7 +1388,7 @@ class TranslatedSwitchStmt extends TranslatedStmt {
     result = this.getParent().getChildSuccessor(this, any(GotoEdge edge))
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getInitialization() and
     result = this.getFirstExprInstruction(kind)
     or
@@ -1169,7 +1403,7 @@ class TranslatedSwitchStmt extends TranslatedStmt {
 class TranslatedAsmStmt extends TranslatedStmt {
   override AsmStmt stmt;
 
-  override TranslatedExpr getChild(int id) {
+  override TranslatedExpr getChildInternal(int id) {
     result = getTranslatedExpr(stmt.getChild(id).(Expr).getFullyConverted())
   }
 
@@ -1181,6 +1415,8 @@ class TranslatedAsmStmt extends TranslatedStmt {
     )
   }
 
+  override Instruction getALastInstructionInternal() { result = this.getInstruction(AsmTag()) }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     tag = AsmTag() and
     opcode instanceof Opcode::InlineAsm and
@@ -1191,7 +1427,7 @@ class TranslatedAsmStmt extends TranslatedStmt {
     exists(int index |
       tag = AsmTag() and
       operandTag = asmOperand(index) and
-      result = this.getChild(index).getResult()
+      result = this.getChildInternal(index).getResult()
     )
   }
 
@@ -1203,12 +1439,12 @@ class TranslatedAsmStmt extends TranslatedStmt {
     result = getUnknownType()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = AsmTag() and
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     exists(int index |
       child = this.getChild(index) and
       if exists(this.getChild(index + 1))
@@ -1223,7 +1459,7 @@ class TranslatedAsmStmt extends TranslatedStmt {
 class TranslatedVlaDimensionStmt extends TranslatedStmt {
   override VlaDimensionStmt stmt;
 
-  override TranslatedExpr getChild(int id) {
+  override TranslatedExpr getChildInternal(int id) {
     id = 0 and
     result = getTranslatedExpr(stmt.getDimensionExpr().getFullyConverted())
   }
@@ -1232,13 +1468,19 @@ class TranslatedVlaDimensionStmt extends TranslatedStmt {
     result = this.getChild(0).getFirstInstruction(kind)
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getChild(0).getALastInstruction()
+  }
+
+  override TranslatedElement getLastChild() { result = this.getChild(0) }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     none()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) { none() }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) {
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
     child = this.getChild(0) and
     result = this.getParent().getChildSuccessor(this, kind)
   }
@@ -1247,13 +1489,17 @@ class TranslatedVlaDimensionStmt extends TranslatedStmt {
 class TranslatedVlaDeclarationStmt extends TranslatedStmt {
   override VlaDeclStmt stmt;
 
-  override TranslatedExpr getChild(int id) { none() }
+  override TranslatedExpr getChildInternal(int id) { none() }
 
   override Instruction getFirstInstruction(EdgeKind kind) {
     result = this.getInstruction(OnlyInstructionTag()) and
     kind instanceof GotoEdge
   }
 
+  override Instruction getALastInstructionInternal() {
+    result = this.getInstruction(OnlyInstructionTag())
+  }
+
   override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
     // TODO: This needs a new kind of instruction that represents initialization of a VLA.
     // For now we just emit a `NoOp` instruction so that the CFG isn't incomplete.
@@ -1262,10 +1508,10 @@ class TranslatedVlaDeclarationStmt extends TranslatedStmt {
     resultType = getVoidType()
   }
 
-  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
+  override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = OnlyInstructionTag() and
     result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getChildSuccessor(TranslatedElement child, EdgeKind kind) { none() }
+  override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) { none() }
 }

cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_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/internal/CppType.qll

@@ -11,7 +11,7 @@ private int getTypeSizeWorkaround(Type type) {
   exists(Type unspecifiedType |
     unspecifiedType = type.getUnspecifiedType() and
     (
-      unspecifiedType instanceof FunctionReferenceType and
+      (unspecifiedType instanceof FunctionReferenceType or unspecifiedType instanceof RoutineType) and
       result = getPointerSize()
       or
       exists(PointerToMemberType ptmType |
@@ -176,7 +176,7 @@ private IRType getIRTypeForPRValue(Type type) {
     isPointerIshType(unspecifiedType) and
     result.(IRAddressType).getByteSize() = getTypeSize(unspecifiedType)
     or
-    unspecifiedType instanceof FunctionPointerIshType and
+    (unspecifiedType instanceof FunctionPointerIshType or unspecifiedType instanceof RoutineType) and
     result.(IRFunctionAddressType).getByteSize() = getTypeSize(type)
     or
     unspecifiedType instanceof VoidType and result instanceof IRVoidType

cpp/ql/lib/semmle/code/cpp/ir/internal/IntegerPartial.qll

@@ -89,6 +89,18 @@ int compareLE(int a, int b) { if a <= b then result = 1 else result = 0 }
 bindingset[a, b]
 int compareGE(int a, int b) { if a >= b then result = 1 else result = 0 }
 
+/** Returns `a | b`. */
+bindingset[a, b]
+int bitOr(int a, int b) { result = a.bitOr(b) }
+
+/** Returns `a & b`. */
+bindingset[a, b]
+int bitAnd(int a, int b) { result = a.bitAnd(b) }
+
+/** Returns `a ^ b`. */
+bindingset[a, b]
+int bitXor(int a, int b) { result = a.bitXor(b) }
+
 /**
  * Returns `-a`. If the negation would overflow, there is no result.
  */

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

@@ -36,7 +36,9 @@ private class MallocAllocationFunction extends AllocationFunction {
         "CRYPTO_malloc", // CRYPTO_malloc(size_t num, const char *file, int line)
         "CRYPTO_zalloc", // CRYPTO_zalloc(size_t num, const char *file, int line)
         "CRYPTO_secure_malloc", // CRYPTO_secure_malloc(size_t num, const char *file, int line)
-        "CRYPTO_secure_zalloc" // CRYPTO_secure_zalloc(size_t num, const char *file, int line)
+        "CRYPTO_secure_zalloc", // CRYPTO_secure_zalloc(size_t num, const char *file, int line)
+        "g_malloc", // g_malloc (n_bytes);
+        "g_try_malloc" // g_try_malloc(n_bytes);
       ]) and
     sizeArg = 0
     or
@@ -139,7 +141,9 @@ private class ReallocAllocationFunction extends AllocationFunction, TaintFunctio
         // --- Windows COM allocation
         "CoTaskMemRealloc", // CoTaskMemRealloc(ptr, size)
         // --- OpenSSL memory allocation
-        "CRYPTO_realloc" // CRYPTO_realloc(void *addr, size_t num, const char *file, int line)
+        "CRYPTO_realloc", // CRYPTO_realloc(void *addr, size_t num, const char *file, int line)
+        "g_realloc", // g_realloc(mem, n_bytes);
+        "g_try_realloc" // g_try_realloc(mem, n_bytes);
       ]) and
     sizeArg = 1 and
     reallocArg = 0

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

@@ -20,8 +20,10 @@ private class StandardDeallocationFunction extends DeallocationFunction {
     freedArg = 0
     or
     this.hasGlobalName([
-        // --- OpenSSL memory allocation
-        "CRYPTO_free", "CRYPTO_secure_free"
+        // --- OpenSSL memory deallocation
+        "CRYPTO_free", "CRYPTO_secure_free",
+        // --- glib memory deallocation
+        "g_free"
       ]) and
     freedArg = 0
     or

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

@@ -15,6 +15,8 @@ private class GetDelimFunction extends TaintFunction, AliasFunction, SideEffectF
     i.isParameter(3) and o.isParameterDeref(0)
   }
 
+  override predicate isPartialWrite(FunctionOutput o) { o.isParameterDeref(3) }
+
   override predicate parameterNeverEscapes(int index) { index = [0, 1, 3] }
 
   override predicate parameterEscapesOnlyViaReturn(int index) { none() }

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

@@ -27,6 +27,8 @@ private class FgetsFunction extends DataFlowFunction, TaintFunction, ArrayFuncti
     output.isReturnValue()
   }
 
+  override predicate isPartialWrite(FunctionOutput output) { output.isParameterDeref(2) }
+
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     input.isParameter(2) and
     output.isParameterDeref(0)

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

@@ -20,6 +20,8 @@ private class InetAton extends TaintFunction, ArrayFunction {
     output.isParameterDeref(1)
   }
 
+  override predicate isPartialWrite(FunctionOutput output) { output.isParameterDeref(1) }
+
   override predicate hasArrayInput(int bufParam) { bufParam = 0 }
 
   override predicate hasArrayOutput(int bufParam) { bufParam = 1 }

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

@@ -9,6 +9,8 @@ import cpp
 import semmle.code.cpp.models.interfaces.Taint
 import semmle.code.cpp.models.interfaces.DataFlow
 import semmle.code.cpp.models.interfaces.Iterator
+import semmle.code.cpp.models.interfaces.Alias
+import semmle.code.cpp.models.interfaces.SideEffect
 
 /**
  * An instantiation of the `std::iterator_traits` template.
@@ -438,7 +440,7 @@ private class IteratorAssignmentMemberOperatorModel extends IteratorAssignmentMe
  * A `begin` or `end` member function, or a related member function, that
  * returns an iterator.
  */
-private class BeginOrEndFunction extends MemberFunction, TaintFunction, GetIteratorFunction {
+class BeginOrEndFunction extends MemberFunction {
   BeginOrEndFunction() {
     this.hasName([
         "begin", "cbegin", "rbegin", "crbegin", "end", "cend", "rend", "crend", "before_begin",
@@ -446,7 +448,11 @@ private class BeginOrEndFunction extends MemberFunction, TaintFunction, GetItera
       ]) and
     this.getType().getUnspecifiedType() instanceof Iterator
   }
+}
 
+private class BeginOrEndFunctionModels extends BeginOrEndFunction, TaintFunction,
+  GetIteratorFunction, AliasFunction, SideEffectFunction
+{
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     input.isQualifierObject() and
     output.isReturnValue()
@@ -456,6 +462,22 @@ private class BeginOrEndFunction extends MemberFunction, TaintFunction, GetItera
     input.isQualifierObject() and
     output.isReturnValue()
   }
+
+  override predicate parameterNeverEscapes(int index) { index = -1 }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) { none() }
+
+  override predicate hasOnlySpecificReadSideEffects() { any() }
+
+  override predicate hasOnlySpecificWriteSideEffects() { any() }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    none()
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
 }
 
 /**

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

@@ -168,3 +168,57 @@ private class SmartPtrSetterFunction extends MemberFunction, AliasFunction, Side
     )
   }
 }
+
+/** A destructor assocaited with a smart pointer. */
+private class SmartPtrDestructor extends Destructor, SideEffectFunction, AliasFunction {
+  SmartPtr declaringType;
+
+  SmartPtrDestructor() {
+    declaringType = this.getDeclaringType() and not this.isFromUninstantiatedTemplate(_)
+  }
+
+  /**
+   * Gets the destructor associated with the base type of this smart pointer.
+   */
+  private Destructor getBaseTypeDestructor() {
+    result.getDeclaringType() = declaringType.getBaseType()
+  }
+
+  override predicate hasOnlySpecificReadSideEffects() {
+    this.getBaseTypeDestructor().(SideEffectFunction).hasOnlySpecificReadSideEffects()
+    or
+    // If there's no declared destructor for the base type then it won't have
+    // any strange read side effects.
+    not exists(this.getBaseTypeDestructor())
+  }
+
+  override predicate hasOnlySpecificWriteSideEffects() {
+    this.getBaseTypeDestructor().(SideEffectFunction).hasOnlySpecificWriteSideEffects()
+    or
+    // If there's no declared destructor for the base type then it won't have
+    // any strange write side effects.
+    not exists(this.getBaseTypeDestructor())
+  }
+
+  override predicate hasSpecificReadSideEffect(ParameterIndex i, boolean buffer) {
+    i = -1 and buffer = false
+  }
+
+  override predicate hasSpecificWriteSideEffect(ParameterIndex i, boolean buffer, boolean mustWrite) {
+    i = -1 and buffer = false and mustWrite = true
+  }
+
+  override predicate parameterNeverEscapes(int index) {
+    this.getBaseTypeDestructor().(AliasFunction).parameterNeverEscapes(index)
+    or
+    // If there's no declared destructor for the base type then it won't cause
+    // anything to escape.
+    not exists(this.getBaseTypeDestructor()) and
+    index = -1
+  }
+
+  override predicate parameterEscapesOnlyViaReturn(int index) {
+    // A destructor call does not have a return value
+    none()
+  }
+}

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

@@ -118,6 +118,8 @@ private class StdSequenceContainerData extends TaintFunction {
     input.isReturnValueDeref() and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -147,6 +149,8 @@ private class StdSequenceContainerPushModel extends StdSequenceContainerPush, Ta
     input.isParameterDeref(0) and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -207,6 +211,8 @@ private class StdSequenceContainerInsertModel extends StdSequenceContainerInsert
       output.isReturnValue()
     )
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -247,13 +253,15 @@ private class StdSequenceContainerAssign extends TaintFunction {
 /**
  * The standard container functions `at` and `operator[]`.
  */
-private class StdSequenceContainerAt extends TaintFunction {
+class StdSequenceContainerAt extends MemberFunction {
   StdSequenceContainerAt() {
     this.getClassAndName(["at", "operator[]"]) instanceof Array or
     this.getClassAndName(["at", "operator[]"]) instanceof Deque or
     this.getClassAndName(["at", "operator[]"]) instanceof Vector
   }
+}
 
+private class StdSequenceContainerAtModel extends StdSequenceContainerAt, TaintFunction {
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     // flow from qualifier to referenced return value
     input.isQualifierObject() and
@@ -263,6 +271,8 @@ private class StdSequenceContainerAt extends TaintFunction {
     input.isReturnValueDeref() and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -297,6 +307,8 @@ private class StdSequenceEmplaceModel extends StdSequenceEmplace, TaintFunction
       output.isReturnValue()
     )
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -335,6 +347,8 @@ private class StdSequenceEmplaceBackModel extends StdSequenceEmplaceBack, TaintF
     input.isParameterDeref([0 .. this.getNumberOfParameters() - 1]) and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**

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

@@ -3,6 +3,7 @@
  */
 
 import semmle.code.cpp.models.interfaces.Taint
+import semmle.code.cpp.models.interfaces.DataFlow
 import semmle.code.cpp.models.interfaces.Iterator
 
 /**
@@ -53,6 +54,8 @@ private class StdMapInsert extends TaintFunction {
       output.isReturnValue()
     )
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -75,6 +78,8 @@ private class StdMapEmplace extends TaintFunction {
     input.isQualifierObject() and
     output.isReturnValue()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -102,6 +107,8 @@ private class StdMapTryEmplace extends TaintFunction {
     input.isQualifierObject() and
     output.isReturnValue()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -115,14 +122,18 @@ private class StdMapMerge extends TaintFunction {
     input.isParameterDeref(0) and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
  * The standard map functions `at` and `operator[]`.
  */
-private class StdMapAt extends TaintFunction {
+class StdMapAt extends MemberFunction {
   StdMapAt() { this.getClassAndName(["at", "operator[]"]) instanceof MapOrUnorderedMap }
+}
 
+private class StdMapAtModels extends StdMapAt, TaintFunction {
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     // flow from qualifier to referenced return value
     input.isQualifierObject() and
@@ -132,6 +143,8 @@ private class StdMapAt extends TaintFunction {
     input.isReturnValueDeref() and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**

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

@@ -61,6 +61,8 @@ private class StdSetInsert extends TaintFunction {
       output.isReturnValue()
     )
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -82,6 +84,8 @@ private class StdSetEmplace extends TaintFunction {
     input.isQualifierObject() and
     output.isReturnValue()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -95,6 +99,8 @@ private class StdSetMerge extends TaintFunction {
     input.isParameterDeref(0) and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**

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

@@ -129,6 +129,8 @@ private class StdStringDataModel extends StdStringData, StdStringTaintFunction {
     input.isReturnValueDeref() and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -142,6 +144,8 @@ private class StdStringPush extends StdStringTaintFunction {
     input.isParameter(0) and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -204,6 +208,8 @@ private class StdStringAppend extends StdStringTaintFunction {
     input.isReturnValueDeref() and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -237,6 +243,8 @@ private class StdStringInsert extends StdStringTaintFunction {
     input.isReturnValueDeref() and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -305,6 +313,8 @@ private class StdStringAt extends StdStringTaintFunction {
     input.isReturnValueDeref() and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -338,6 +348,8 @@ private class StdIStreamIn extends DataFlowFunction, TaintFunction {
     input.isReturnValueDeref() and
     output.isQualifierObject()
   }
+
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
 }
 
 /**
@@ -358,6 +370,8 @@ private class StdIStreamInNonMember extends DataFlowFunction, TaintFunction {
     output.isReturnValueDeref()
   }
 
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
+
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     // flow from first parameter to second parameter
     input.isParameterDeref(0) and
@@ -403,6 +417,8 @@ private class StdIStreamRead extends DataFlowFunction, TaintFunction {
     output.isReturnValueDeref()
   }
 
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
+
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     // flow from qualifier to first parameter
     input.isQualifierObject() and
@@ -442,6 +458,8 @@ private class StdIStreamPutBack extends DataFlowFunction, TaintFunction {
     output.isReturnValueDeref()
   }
 
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
+
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     // flow from first parameter (value or pointer) to qualifier
     input.isParameter(0) and
@@ -478,6 +496,8 @@ private class StdIStreamGetLine extends DataFlowFunction, TaintFunction {
     output.isReturnValueDeref()
   }
 
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
+
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     // flow from qualifier to first parameter
     input.isQualifierObject() and
@@ -540,6 +560,8 @@ private class StdOStreamOut extends DataFlowFunction, TaintFunction {
     output.isReturnValueDeref()
   }
 
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
+
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     // flow from first parameter (value or pointer) to qualifier
     input.isParameter(0) and
@@ -579,6 +601,8 @@ private class StdOStreamOutNonMember extends DataFlowFunction, TaintFunction {
     output.isReturnValueDeref()
   }
 
+  override predicate isPartialWrite(FunctionOutput output) { output.isParameterDeref(0) }
+
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     // flow from second parameter to first parameter
     input.isParameterDeref(1) and
@@ -672,6 +696,8 @@ private class StdStreamFunction extends DataFlowFunction, TaintFunction {
     output.isReturnValueDeref()
   }
 
+  override predicate isPartialWrite(FunctionOutput output) { output.isQualifierObject() }
+
   override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
     // reverse flow from returned reference to the qualifier
     input.isReturnValueDeref() and

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

@@ -36,6 +36,8 @@ private class Strcrement extends ArrayFunction, TaintFunction, SideEffectFunctio
       input.isParameter(index) and output.isReturnValue()
       or
       input.isParameterDeref(index) and output.isReturnValueDeref()
+      or
+      input.isParameterDeref(index) and output.isParameterDeref(index)
     )
   }
 

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

@@ -10,6 +10,7 @@
 import semmle.code.cpp.Function
 import FunctionInputsAndOutputs
 import semmle.code.cpp.models.Models
+import PartialFlow
 
 /**
  * A library function for which a value is or may be copied from a parameter
@@ -18,7 +19,7 @@ import semmle.code.cpp.models.Models
  * Note that this does not include partial copying of values or partial writes
  * to destinations; that is covered by `TaintModel.qll`.
  */
-abstract class DataFlowFunction extends Function {
+abstract class DataFlowFunction extends PartialFlowFunction {
   /**
    * Holds if data can be copied from the argument, qualifier, or buffer
    * represented by `input` to the return value or buffer represented by

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

@@ -0,0 +1,31 @@
+/**
+ * Provides an abstract class to override the implicit assumption that a
+ * dataflow/taint-tracking model always fully override the parameters they are
+ * are modeled as writing to. To use this QL library, create a QL class
+ * extending `PartialFlowFunction` with a characteristic predicate that selects
+ * the function or set of functions you are modeling and override the
+ * `isPartialWrite` predicate.
+ *
+ * Note: Since both `DataFlowFunction` and `TaintFunction` extend this class
+ * you don't need to explicitly add this as a base class if your QL class
+ * already extends either `DataFlowFunction` or `TaintFunction`.
+ */
+
+import semmle.code.cpp.Function
+import FunctionInputsAndOutputs
+import semmle.code.cpp.models.Models
+
+/**
+ * A function that may update part of a `FunctionOutput`.
+ *
+ * For example, the destination argument of `strcat` only updates part of the
+ * argument.
+ */
+abstract class PartialFlowFunction extends Function {
+  /**
+   * Holds if the write to output does not overwrite the entire value that was
+   * there before, or does not do so reliably. For example the destination
+   * argument of `strcat` is modified but not overwritten.
+   */
+  predicate isPartialWrite(FunctionOutput output) { none() }
+}

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

@@ -10,6 +10,7 @@
 import semmle.code.cpp.Function
 import FunctionInputsAndOutputs
 import semmle.code.cpp.models.Models
+import PartialFlow
 
 /**
  * A library function for which a taint-tracking library should propagate taint
@@ -23,7 +24,7 @@ import semmle.code.cpp.models.Models
  * altered (for example copying a string with `strncpy`), this is also considered
  * data flow.
  */
-abstract class TaintFunction extends Function {
+abstract class TaintFunction extends PartialFlowFunction {
   /**
    * Holds if data passed into the argument, qualifier, or buffer represented by
    * `input` influences the return value or buffer represented by `output`