Merge remote-tracking branch 'origin/main' into redsun82/just2

The parallel attribute causes concurrent sembuild calls that conflict
with each other.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

.github/workflows/go-version-update.yml

@@ -1,206 +0,0 @@
-name: Update Go version
-
-on:
-  workflow_dispatch:
-  schedule:
-    - cron: "0 3 * * 1"  # Run weekly on Mondays at 3 AM UTC (1 = Monday)
-
-permissions:
-  contents: write
-  pull-requests: write
-
-jobs:
-  update-go-version:
-    name: Check and update Go version
-    if: github.repository == 'github/codeql'
-    runs-on: ubuntu-latest
-
-    steps:
-      - name: Checkout repository
-        uses: actions/checkout@v5
-        with:
-          fetch-depth: 0
-
-      - name: Set up Git
-        run: |
-          git config user.name "github-actions[bot]"
-          git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
-
-      - name: Fetch latest Go version
-        id: fetch-version
-        run: |
-          LATEST_GO_VERSION=$(curl -s https://go.dev/dl/?mode=json | jq -r '.[0].version')
-          
-          if [ -z "$LATEST_GO_VERSION" ] || [ "$LATEST_GO_VERSION" = "null" ]; then
-            echo "Error: Failed to fetch latest Go version from go.dev"
-            exit 1
-          fi
-          
-          echo "Latest Go version from go.dev: $LATEST_GO_VERSION"
-          echo "version=$LATEST_GO_VERSION" >> $GITHUB_OUTPUT
-          
-          # Extract version numbers (e.g., go1.26.0 -> 1.26.0)
-          LATEST_VERSION_NUM=$(echo $LATEST_GO_VERSION | sed 's/^go//')
-          echo "version_num=$LATEST_VERSION_NUM" >> $GITHUB_OUTPUT
-          
-          # Extract major.minor version (e.g., 1.26.0 -> 1.26)
-          LATEST_MAJOR_MINOR=$(echo $LATEST_VERSION_NUM | sed -E 's/^([0-9]+\.[0-9]+).*/\1/')
-          echo "major_minor=$LATEST_MAJOR_MINOR" >> $GITHUB_OUTPUT
-
-      - name: Check current Go version
-        id: current-version
-        run: |
-          CURRENT_VERSION=$(sed -n 's/.*go_sdk\.download(version = \"\([^\"]*\)\".*/\1/p' MODULE.bazel)
-          
-          if [ -z "$CURRENT_VERSION" ]; then
-            echo "Error: Could not extract Go version from MODULE.bazel"
-            exit 1
-          fi
-          
-          echo "Current Go version in MODULE.bazel: $CURRENT_VERSION"
-          echo "version=$CURRENT_VERSION" >> $GITHUB_OUTPUT
-          
-          # Extract major.minor version
-          CURRENT_MAJOR_MINOR=$(echo $CURRENT_VERSION | sed -E 's/^([0-9]+\.[0-9]+).*/\1/')
-          echo "major_minor=$CURRENT_MAJOR_MINOR" >> $GITHUB_OUTPUT
-
-      - name: Compare versions
-        id: compare
-        run: |
-          LATEST="${{ steps.fetch-version.outputs.version_num }}"
-          CURRENT="${{ steps.current-version.outputs.version }}"
-          
-          echo "Latest: $LATEST"
-          echo "Current: $CURRENT"
-          
-          if [ "$LATEST" = "$CURRENT" ]; then
-            echo "Go version is up to date"
-            echo "needs_update=false" >> $GITHUB_OUTPUT
-          else
-            echo "Go version needs update from $CURRENT to $LATEST"
-            echo "needs_update=true" >> $GITHUB_OUTPUT
-          fi
-
-      - name: Update Go version in files
-        if: steps.compare.outputs.needs_update == 'true'
-        run: |
-          LATEST_VERSION_NUM="${{ steps.fetch-version.outputs.version_num }}"
-          LATEST_MAJOR_MINOR="${{ steps.fetch-version.outputs.major_minor }}"
-          CURRENT_VERSION="${{ steps.current-version.outputs.version }}"
-          CURRENT_MAJOR_MINOR="${{ steps.current-version.outputs.major_minor }}"
-          
-          echo "Updating from $CURRENT_VERSION to $LATEST_VERSION_NUM"
-          
-          # Escape dots in current version strings for use in sed patterns
-          CURRENT_VERSION_ESCAPED=$(echo "$CURRENT_VERSION" | sed 's/\./\\./g')
-          CURRENT_MAJOR_MINOR_ESCAPED=$(echo "$CURRENT_MAJOR_MINOR" | sed 's/\./\\./g')
-          
-          # Update MODULE.bazel
-          if ! sed -i "s/go_sdk\.download(version = \"$CURRENT_VERSION_ESCAPED\")/go_sdk.download(version = \"$LATEST_VERSION_NUM\")/" MODULE.bazel; then
-            echo "Warning: Failed to update MODULE.bazel"
-          fi
-          
-          # Update go/extractor/go.mod
-          if ! sed -i "s/^go $CURRENT_MAJOR_MINOR_ESCAPED\$/go $LATEST_MAJOR_MINOR/" go/extractor/go.mod; then
-            echo "Warning: Failed to update go directive in go.mod"
-          fi
-          if ! sed -i "s/^toolchain go$CURRENT_VERSION_ESCAPED\$/toolchain go$LATEST_VERSION_NUM/" go/extractor/go.mod; then
-            echo "Warning: Failed to update toolchain in go.mod"
-          fi
-          
-          # Update go/extractor/autobuilder/build-environment.go
-          if ! sed -i "s/var maxGoVersion = util\.NewSemVer(\"$CURRENT_MAJOR_MINOR_ESCAPED\")/var maxGoVersion = util.NewSemVer(\"$LATEST_MAJOR_MINOR\")/" go/extractor/autobuilder/build-environment.go; then
-            echo "Warning: Failed to update build-environment.go"
-          fi
-          
-          # Update go/actions/test/action.yml
-          if ! sed -i "s/default: \"~$CURRENT_VERSION_ESCAPED\"/default: \"~$LATEST_VERSION_NUM\"/" go/actions/test/action.yml; then
-            echo "Warning: Failed to update action.yml"
-          fi
-          
-          # Show what changed
-          git diff
-
-      - name: Check for changes
-        id: check-changes
-        if: steps.compare.outputs.needs_update == 'true'
-        run: |
-          if git diff --quiet; then
-            echo "No changes detected"
-            echo "has_changes=false" >> $GITHUB_OUTPUT
-          else
-            echo "Changes detected"
-            echo "has_changes=true" >> $GITHUB_OUTPUT
-          fi
-
-      - name: Check for existing PR
-        if: steps.check-changes.outputs.has_changes == 'true'
-        id: check-pr
-        env:
-          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        run: |
-          BRANCH_NAME="workflow/go-version-update"
-          PR_NUMBER=$(gh pr list --head "$BRANCH_NAME" --state open --json number --jq '.[0].number')
-          
-          if [ -n "$PR_NUMBER" ]; then
-            echo "Existing PR found: #$PR_NUMBER"
-            echo "pr_exists=true" >> $GITHUB_OUTPUT
-            echo "pr_number=$PR_NUMBER" >> $GITHUB_OUTPUT
-          else
-            echo "No existing PR found"
-            echo "pr_exists=false" >> $GITHUB_OUTPUT
-          fi
-
-      - name: Commit and push changes
-        if: steps.check-changes.outputs.has_changes == 'true'
-        run: |
-          BRANCH_NAME="workflow/go-version-update"
-          LATEST_VERSION_NUM="${{ steps.fetch-version.outputs.version_num }}"
-          LATEST_MAJOR_MINOR="${{ steps.fetch-version.outputs.major_minor }}"
-          
-          # Create or switch to branch
-          git checkout -B "$BRANCH_NAME"
-          
-          # Stage and commit changes
-          git add MODULE.bazel go/extractor/go.mod go/extractor/autobuilder/build-environment.go go/actions/test/action.yml
-          git commit -m "Go: Update to $LATEST_MAJOR_MINOR"
-          
-          # Push changes
-          git push -f origin "$BRANCH_NAME"
-
-      - name: Create or update PR
-        if: steps.check-changes.outputs.has_changes == 'true'
-        env:
-          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        run: |
-          BRANCH_NAME="workflow/go-version-update"
-          LATEST_MAJOR_MINOR="${{ steps.fetch-version.outputs.major_minor }}"
-          CURRENT_MAJOR_MINOR="${{ steps.current-version.outputs.major_minor }}"
-          
-          PR_TITLE="Go: Update to $LATEST_MAJOR_MINOR"
-          
-          PR_BODY=$(cat <<EOF
-          This PR updates Go from $CURRENT_MAJOR_MINOR to $LATEST_MAJOR_MINOR.
-
-          Updated files:
-          - \`MODULE.bazel\` - go_sdk.download version
-          - \`go/extractor/go.mod\` - go directive and toolchain
-          - \`go/extractor/autobuilder/build-environment.go\` - maxGoVersion
-          - \`go/actions/test/action.yml\` - default go-test-version
-
-          This PR was automatically created by the [Go version update workflow](https://github.com/${{ github.repository }}/blob/main/.github/workflows/go-version-update.yml).
-          EOF
-          )
-          
-          if [ "${{ steps.check-pr.outputs.pr_exists }}" = "true" ]; then
-            echo "Updating existing PR #${{ steps.check-pr.outputs.pr_number }}"
-            gh pr edit "${{ steps.check-pr.outputs.pr_number }}" --title "$PR_TITLE" --body "$PR_BODY"
-          else
-            echo "Creating new PR"
-            gh pr create \
-              --title "$PR_TITLE" \
-              --body "$PR_BODY" \
-              --base main \
-              --head "$BRANCH_NAME" \
-              --label "Go"
-          fi

actions/justfile

@@ -0,0 +1,7 @@
+import '../lib.just'
+
+[group('build')]
+build: (_build_dist "actions")
+
+[group('test')]
+language-tests *EXTRA_ARGS: (_language_tests EXTRA_ARGS source_dir() 'ql/test')

actions/ql/integration-tests/justfile

@@ -0,0 +1,4 @@
+import "../../../lib.just"
+
+[no-cd]
+test *ARGS=".": (_integration_test ARGS)

actions/ql/justfile

@@ -0,0 +1,6 @@
+import "../../lib.just"
+
+[no-cd]
+format *ARGS=".": (_format_ql ARGS)
+
+consistency_queries := ""

actions/ql/lib/CHANGELOG.md

@@ -1,9 +1,3 @@
-## 0.4.34
-
-### Minor Analysis Improvements
-
-* Removed false positive injection sink models for the `context` input of `docker/build-push-action` and the `allowed-endpoints` input of `step-security/harden-runner`.
-
 ## 0.4.33
 
 No user-facing changes.

actions/ql/lib/change-notes/released/0.4.34.md

@@ -1,5 +0,0 @@
-## 0.4.34
-
-### Minor Analysis Improvements
-
-* Removed false positive injection sink models for the `context` input of `docker/build-push-action` and the `allowed-endpoints` input of `step-security/harden-runner`.

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

@@ -1,2 +1,2 @@
 ---
-lastReleaseVersion: 0.4.34
+lastReleaseVersion: 0.4.33

actions/ql/lib/ext/manual/docker_build-push-action.model.yml

@@ -0,0 +1,6 @@
+extensions:
+  - addsTo:
+      pack: codeql/actions-all
+      extensible: actionsSinkModel
+    data:
+      - ["docker/build-push-action", "*", "input.context", "code-injection", "manual"]

actions/ql/lib/ext/manual/step-security_harden-runner.model.yml

@@ -0,0 +1,6 @@
+extensions:
+  - addsTo:
+      pack: codeql/actions-all
+      extensible: actionsSinkModel
+    data:
+      - ["step-security/harden-runner", "*", "input.allowed-endpoints", "command-injection", "manual"]

actions/ql/lib/qlpack.yml

@@ -1,5 +1,5 @@
 name: codeql/actions-all
-version: 0.4.35-dev
+version: 0.4.34-dev
 library: true
 warnOnImplicitThis: true
 dependencies:

actions/ql/src/CHANGELOG.md

@@ -1,13 +1,3 @@
-## 0.6.26
-
-### Major Analysis Improvements
-
-* Fixed alert messages in `actions/artifact-poisoning/critical` and `actions/artifact-poisoning/medium` as they previously included a redundant placeholder in the alert message that would on occasion contain a long block of yml that makes the alert difficult to understand. Also improved the wording to make it clearer that it is not the artifact that is being poisoned, but instead a potentially untrusted artifact that is consumed. Finally, changed the alert location to be the source, to align more with other queries reporting an artifact (e.g. zipslip) which is more useful.
-
-### Minor Analysis Improvements
-
-* The query `actions/missing-workflow-permissions` no longer produces false positive results on reusable workflows where all callers set permissions.
-
 ## 0.6.25
 
 No user-facing changes.
@@ -173,7 +163,7 @@ No user-facing changes.
   * `actions/if-expression-always-true/critical`
   * `actions/if-expression-always-true/high`
   * `actions/unnecessary-use-of-advanced-config`
-
+  
 * The following query has been moved from the `code-scanning` suite to the `security-extended`
   suite. Any existing alerts for this query will be closed automatically unless the analysis is
   configured to use the `security-extended` suite.

actions/ql/src/change-notes/2026-04-02-alert-msg-poisoning.md

@@ -0,0 +1,4 @@
+---
+category: majorAnalysis
+---
+* Fixed alert messages in `actions/artifact-poisoning/critical` and `actions/artifact-poisoning/medium` as they previously included a redundant placeholder in the alert message that would on occasion contain a long block of yml that makes the alert difficult to understand. Also clarify the wording to make it clear that it is not the artifact that is being poisoned, but instead a potentially untrusted artifact that is consumed. Also change the alert location to be the source, to align more with other queries reporting an artifact (e.g. zipslip) which is more useful.

actions/ql/src/change-notes/2026-04-02-permissions.md

@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* The query `actions/missing-workflow-permissions` no longer produces false positive results on reusable workflows where all callers set permissions.

actions/ql/src/change-notes/released/0.6.26.md

@@ -1,9 +0,0 @@
-## 0.6.26
-
-### Major Analysis Improvements
-
-* Fixed alert messages in `actions/artifact-poisoning/critical` and `actions/artifact-poisoning/medium` as they previously included a redundant placeholder in the alert message that would on occasion contain a long block of yml that makes the alert difficult to understand. Also improved the wording to make it clearer that it is not the artifact that is being poisoned, but instead a potentially untrusted artifact that is consumed. Finally, changed the alert location to be the source, to align more with other queries reporting an artifact (e.g. zipslip) which is more useful.
-
-### Minor Analysis Improvements
-
-* The query `actions/missing-workflow-permissions` no longer produces false positive results on reusable workflows where all callers set permissions.

actions/ql/src/codeql-pack.release.yml

@@ -1,2 +1,2 @@
 ---
-lastReleaseVersion: 0.6.26
+lastReleaseVersion: 0.6.25

actions/ql/src/qlpack.yml

@@ -1,5 +1,5 @@
 name: codeql/actions-queries
-version: 0.6.27-dev
+version: 0.6.26-dev
 library: false
 warnOnImplicitThis: true
 groups: [actions, queries]

actions/ql/test/justfile

@@ -0,0 +1,8 @@
+import "../justfile"
+
+base_flags := ""
+
+all_checks := default_db_checks
+
+[no-cd]
+test *ARGS=".": (_codeql_test "actions" base_flags all_checks ARGS)

cpp/justfile

@@ -0,0 +1,8 @@
+import '../lib.just'
+import? '../../cpp-coding-standards.just'
+
+[group('build')]
+build: (_build_dist "cpp")
+
+[group('test')]
+language-tests *EXTRA_ARGS: (_language_tests EXTRA_ARGS source_dir() 'ql/test' '../../semmlecode-cpp-tests')

cpp/ql/consistency-queries/badLocations.ql

@@ -0,0 +1,9 @@
+import cpp
+
+// Locations should either be :0:0:0:0 locations (UnknownLocation, or
+// a whole file), or all 4 fields should be positive.
+from Location l
+where
+  [l.getStartLine(), l.getEndLine(), l.getStartColumn(), l.getEndColumn()] != 0 and
+  [l.getStartLine(), l.getEndLine(), l.getStartColumn(), l.getEndColumn()] < 1
+select l

cpp/ql/consistency-queries/nullInToString.ql

@@ -0,0 +1,5 @@
+import cpp
+
+from Element e
+where e.toString().matches("%(null)%")
+select e

cpp/ql/consistency-queries/qlpack.yml

@@ -0,0 +1,5 @@
+name: codeql/cpp-consistency-queries
+groups: [cpp, test, consistency-queries]
+dependencies:
+  codeql/cpp-all: ${workspace}
+extractor: cpp

cpp/ql/consistency-queries/unusedLocations.ql

@@ -0,0 +1,10 @@
+import cpp
+
+from Location l
+where
+  not any(Element e).getLocation() = l and
+  not any(LambdaCapture lc).getLocation() = l and
+  not any(MacroAccess ma).getActualLocation() = l and
+  not any(NamespaceDeclarationEntry nde).getBodyLocation() = l and
+  not any(XmlLocatable xml).getLocation() = l
+select l

cpp/ql/consistency-queries/variableDeclarationsWithoutTypes.ql

@@ -0,0 +1,5 @@
+import cpp
+
+from VariableDeclarationEntry i
+where not exists(i.getType())
+select i

cpp/ql/consistency-queries/variablesWithoutTypes.ql

@@ -0,0 +1,5 @@
+import cpp
+
+from Variable i
+where not exists(i.getType())
+select i

cpp/ql/integration-tests/justfile

@@ -0,0 +1,4 @@
+import "../../../lib.just"
+
+[no-cd]
+test *ARGS=".": (_integration_test ARGS)

cpp/ql/justfile

@@ -0,0 +1,6 @@
+import "../../lib.just"
+
+[no-cd]
+format *ARGS=".": (_format_ql ARGS)
+
+consistency_queries := source_dir() / "consistency-queries"

cpp/ql/lib/CHANGELOG.md

@@ -1,14 +1,3 @@
-## 10.0.0
-
-### Breaking Changes
-
-* The deprecated `NonThrowingFunction` class has been removed, use `NonCppThrowingFunction` instead.
-* The deprecated `ThrowingFunction` class has been removed, use `AlwaysSehThrowingFunction` instead.
-
-### New Features
-
-* Added a subclass `AutoconfConfigureTestFile` of `ConfigurationTestFile` that represents files created by GNU autoconf configure scripts to test the build configuration.
-
 ## 9.0.0
 
 ### Breaking Changes

cpp/ql/lib/change-notes/2026-03-20-data-extensions-barriers.md

@@ -1,4 +0,0 @@
----
-category: feature
----
-* Data flow barriers and barrier guards can now be added using data extensions. For more information see [Customizing library models for C and C++](https://codeql.github.com/docs/codeql-language-guides/customizing-library-models-for-cpp/).

cpp/ql/lib/change-notes/2026-04-07-autoconf.md

@@ -0,0 +1,4 @@
+---
+category: feature
+---
+* Added a subclass `AutoconfConfigureTestFile` of `ConfigurationTestFile` that represents files created by GNU autoconf configure scripts to test the build configuration.

cpp/ql/lib/change-notes/2026-04-14-throwing.md

@@ -0,0 +1,5 @@
+---
+category: breaking
+---
+* The deprecated `NonThrowingFunction` class has been removed, use `NonCppThrowingFunction` instead.
+* The deprecated `ThrowingFunction` class has been removed, use `AlwaysSehThrowingFunction` instead.

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

@@ -1,10 +0,0 @@
-## 10.0.0
-
-### Breaking Changes
-
-* The deprecated `NonThrowingFunction` class has been removed, use `NonCppThrowingFunction` instead.
-* The deprecated `ThrowingFunction` class has been removed, use `AlwaysSehThrowingFunction` instead.
-
-### New Features
-
-* Added a subclass `AutoconfConfigureTestFile` of `ConfigurationTestFile` that represents files created by GNU autoconf configure scripts to test the build configuration.

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

@@ -1,2 +1,2 @@
 ---
-lastReleaseVersion: 10.0.0
+lastReleaseVersion: 9.0.0

cpp/ql/lib/ext/allocation/Std.allocation.model.yml

@@ -12,7 +12,4 @@ extensions:
       - ["", "", False, "_malloca", "0", "", "", False]
       - ["", "", False, "calloc", "1", "0", "", True]
       - ["std", "", False, "calloc", "1", "0", "", True]
-      - ["bsl", "", False, "calloc", "1", "0", "", True]
-      - ["", "", False, "aligned_alloc", "1", "", "", True]
-      - ["std", "", False, "aligned_alloc", "1", "", "", True]
-      - ["bsl", "", False, "aligned_alloc", "1", "", "", True]
+      - ["bsl", "", False, "calloc", "1", "0", "", True]

cpp/ql/lib/qlpack.yml

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

cpp/ql/src/CHANGELOG.md

@@ -1,14 +1,3 @@
-## 1.6.1
-
-### Minor Analysis Improvements
-
-* Added `AllocationFunction` models for `aligned_alloc`, `std::aligned_alloc`, and `bsl::aligned_alloc`.
-* The "Comparison of narrow type with wide type in loop condition" (`cpp/comparison-with-wider-type`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.
-* The "Multiplication result converted to larger type" (`cpp/integer-multiplication-cast-to-long`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.
-* The "Suspicious add with sizeof" (`cpp/suspicious-add-sizeof`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.
-* The "Wrong type of arguments to formatting function" (`cpp/wrong-type-format-argument`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.
-* The "Implicit function declaration" (`cpp/implicit-function-declaration`) query has been upgraded to `high` precision. However, for `build mode: none` databases, it no longer produces any results. The results in this mode were found to be very noisy and fundamentally imprecise.
-
 ## 1.6.0
 
 ### Query Metadata Changes
@@ -366,7 +355,7 @@ No user-facing changes.
 ### Minor Analysis Improvements
 
 * The "non-constant format string" query (`cpp/non-constant-format`) has been updated to produce fewer false positives.
-* Added dataflow models for the `gettext` function variants.
+* Added dataflow models for the `gettext` function variants. 
 
 ## 0.9.4
 

cpp/ql/src/change-notes/2026-03-23-implicit-function-declaration.md

@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* The "Implicit function declaration" (`cpp/implicit-function-declaration`) query no longer produces results on `build mode: none` databases. These results were found to be very noisy and fundamentally imprecise in this mode.

cpp/ql/src/change-notes/2026-04-02-comparison-with-wider-type.md

@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* The "Comparison of narrow type with wide type in loop condition" (`cpp/comparison-with-wider-type`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.

cpp/ql/src/change-notes/2026-04-02-implicit-function-declaration.md

@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* The "Implicit function declaration" (`cpp/implicit-function-declaration`) query has been upgraded to `high` precision.

cpp/ql/src/change-notes/2026-04-02-integer-multiplication-cast-to-long.md

@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* The "Multiplication result converted to larger type" (`cpp/integer-multiplication-cast-to-long`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.

cpp/ql/src/change-notes/2026-04-02-suspicious-add-sizeof.md

@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* The "Suspicious add with sizeof" (`cpp/suspicious-add-sizeof`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.

cpp/ql/src/change-notes/2026-04-02-wrong-type-format-argument.md

@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* The "Wrong type of arguments to formatting function" (`cpp/wrong-type-format-argument`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.

cpp/ql/src/change-notes/released/1.6.1.md

@@ -1,10 +0,0 @@
-## 1.6.1
-
-### Minor Analysis Improvements
-
-* Added `AllocationFunction` models for `aligned_alloc`, `std::aligned_alloc`, and `bsl::aligned_alloc`.
-* The "Comparison of narrow type with wide type in loop condition" (`cpp/comparison-with-wider-type`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.
-* The "Multiplication result converted to larger type" (`cpp/integer-multiplication-cast-to-long`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.
-* The "Suspicious add with sizeof" (`cpp/suspicious-add-sizeof`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.
-* The "Wrong type of arguments to formatting function" (`cpp/wrong-type-format-argument`) query has been upgraded to `high` precision. This query will now run in the default code scanning suite.
-* The "Implicit function declaration" (`cpp/implicit-function-declaration`) query has been upgraded to `high` precision. However, for `build mode: none` databases, it no longer produces any results. The results in this mode were found to be very noisy and fundamentally imprecise.

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

@@ -1,2 +1,2 @@
 ---
-lastReleaseVersion: 1.6.1
+lastReleaseVersion: 1.6.0

cpp/ql/src/qlpack.yml

@@ -1,5 +1,5 @@
 name: codeql/cpp-queries
-version: 1.6.2-dev
+version: 1.6.1-dev
 groups:
   - cpp
   - queries

cpp/ql/test/justfile

@@ -0,0 +1,12 @@
+import "../justfile"
+
+base_flags := "--include-location-in-star"
+
+all_checks := f"""\
+    {{default_db_checks}}\
+    --check-undefined-labels \
+    --check-unused-labels \
+    --consistency-queries={{consistency_queries}}"""
+
+[no-cd]
+test *ARGS=".": (_codeql_test "cpp" base_flags all_checks ARGS)

csharp/justfile

@@ -0,0 +1,7 @@
+import '../lib.just'
+
+[group('build')]
+build: (_build_dist "csharp")
+
+[group('test')]
+language-tests *EXTRA_ARGS: (_language_tests EXTRA_ARGS source_dir() 'ql/test')

csharp/ql/campaigns/Solorigate/lib/CHANGELOG.md

@@ -1,7 +1,3 @@
-## 1.7.65
-
-No user-facing changes.
-
 ## 1.7.64
 
 No user-facing changes.

csharp/ql/campaigns/Solorigate/lib/change-notes/released/1.7.65.md

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

csharp/ql/campaigns/Solorigate/lib/codeql-pack.release.yml

@@ -1,2 +1,2 @@
 ---
-lastReleaseVersion: 1.7.65
+lastReleaseVersion: 1.7.64

csharp/ql/campaigns/Solorigate/lib/qlpack.yml

@@ -1,5 +1,5 @@
 name: codeql/csharp-solorigate-all
-version: 1.7.66-dev
+version: 1.7.65-dev
 groups:
   - csharp
   - solorigate

csharp/ql/campaigns/Solorigate/src/CHANGELOG.md

@@ -1,7 +1,3 @@
-## 1.7.65
-
-No user-facing changes.
-
 ## 1.7.64
 
 No user-facing changes.

csharp/ql/campaigns/Solorigate/src/ModifiedFnvFunctionDetection.ql

@@ -13,13 +13,11 @@ import csharp
 import Solorigate
 import experimental.code.csharp.Cryptography.NonCryptographicHashes
 
-ControlFlowNode loopExitNode(LoopStmt loop) { result.isAfter(loop) }
-
 from Variable v, Literal l, LoopStmt loop, Expr additional_xor
 where
   maybeUsedInFnvFunction(v, _, _, loop) and
   exists(BitwiseXorOperation xor2 | xor2.getAnOperand() = l and additional_xor = xor2 |
-    loopExitNode(loop).getASuccessor*() = xor2.getControlFlowNode() and
+    loop.getAControlFlowExitNode().getASuccessor*() = xor2.getAControlFlowNode() and
     xor2.getAnOperand() = v.getAnAccess()
   )
 select l, "This literal is used in an $@ after an FNV-like hash calculation with variable $@.",

csharp/ql/campaigns/Solorigate/src/change-notes/released/1.7.65.md

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

csharp/ql/campaigns/Solorigate/src/codeql-pack.release.yml

@@ -1,2 +1,2 @@
 ---
-lastReleaseVersion: 1.7.65
+lastReleaseVersion: 1.7.64

csharp/ql/campaigns/Solorigate/src/qlpack.yml

@@ -1,5 +1,5 @@
 name: codeql/csharp-solorigate-queries
-version: 1.7.66-dev
+version: 1.7.65-dev
 groups:
   - csharp
   - solorigate

csharp/ql/consistency-queries/CfgConsistency.ql

@@ -1,2 +1,5 @@
 import csharp
-import ControlFlow::Consistency
+import semmle.code.csharp.controlflow.internal.Completion
+import ControlFlow
+import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl::Consistency
+import semmle.code.csharp.controlflow.internal.Splitting

csharp/ql/consistency-queries/DataFlowConsistency.ql

@@ -1,4 +1,5 @@
 import csharp
+private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl as ControlFlowGraphImpl
 private import semmle.code.csharp.dataflow.internal.DataFlowImplSpecific
 private import semmle.code.csharp.dataflow.internal.TaintTrackingImplSpecific
 private import codeql.dataflow.internal.DataFlowImplConsistency
@@ -6,6 +7,20 @@ private import codeql.dataflow.internal.DataFlowImplConsistency
 private module Input implements InputSig<Location, CsharpDataFlow> {
   private import CsharpDataFlow
 
+  private predicate isStaticAssignable(Assignable a) { a.(Modifiable).isStatic() }
+
+  predicate uniqueEnclosingCallableExclude(Node node) {
+    // TODO: Remove once static initializers are folded into the
+    // static constructors
+    isStaticAssignable(ControlFlowGraphImpl::getNodeCfgScope(node.getControlFlowNode()))
+  }
+
+  predicate uniqueCallEnclosingCallableExclude(DataFlowCall call) {
+    // TODO: Remove once static initializers are folded into the
+    // static constructors
+    isStaticAssignable(ControlFlowGraphImpl::getNodeCfgScope(call.getControlFlowNode()))
+  }
+
   predicate uniqueNodeLocationExclude(Node n) {
     // Methods with multiple implementations
     n instanceof ParameterNode
@@ -55,14 +70,17 @@ private module Input implements InputSig<Location, CsharpDataFlow> {
           init.getInitializer().getNumberOfChildren() > 1
         )
       or
-      call.(NonDelegateDataFlowCall).getDispatchCall().isReflection()
-      or
-      // Exclude calls that are both getter and setter calls, as they share the same argument nodes.
-      exists(AccessorCall ac |
-        call.(NonDelegateDataFlowCall).getDispatchCall().getCall() = ac and
-        ac instanceof AssignableRead and
-        ac instanceof AssignableWrite
+      exists(ControlFlow::Nodes::ElementNode cfn, ControlFlow::Nodes::Split split |
+        exists(arg.asExprAtNode(cfn))
+      |
+        split = cfn.getASplit() and
+        not split = call.getControlFlowNode().getASplit()
+        or
+        split = call.getControlFlowNode().getASplit() and
+        not split = cfn.getASplit()
       )
+      or
+      call.(NonDelegateDataFlowCall).getDispatchCall().isReflection()
     )
   }
 }

csharp/ql/consistency-queries/VariableCaptureConsistency.ql

@@ -1,6 +1,13 @@
 import csharp
 import semmle.code.csharp.dataflow.internal.DataFlowPrivate::VariableCapture::Flow::ConsistencyChecks
 private import semmle.code.csharp.dataflow.internal.DataFlowPrivate::VariableCapture::Flow::ConsistencyChecks as ConsistencyChecks
+private import semmle.code.csharp.controlflow.BasicBlocks
+private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl
+
+query predicate uniqueEnclosingCallable(BasicBlock bb, string msg) {
+  ConsistencyChecks::uniqueEnclosingCallable(bb, msg) and
+  getNodeCfgScope(bb.getFirstNode()) instanceof Callable
+}
 
 query predicate consistencyOverview(string msg, int n) { none() }
 

csharp/ql/integration-tests/justfile

@@ -0,0 +1,4 @@
+import "../../../lib.just"
+
+[no-cd]
+test *ARGS=".": (_integration_test ARGS)

csharp/ql/justfile

@@ -0,0 +1,6 @@
+import "../../lib.just"
+
+[no-cd]
+format *ARGS=".": (_format_ql ARGS)
+
+consistency_queries := source_dir() / "consistency-queries"

csharp/ql/lib/CHANGELOG.md

@@ -1,9 +1,3 @@
-## 5.5.0
-
-### Deprecated APIs
-
-* The predicates `get[L|R]Value` in the class `Assignment` have been deprecated. Use `get[Left|Right]Operand` instead.
-
 ## 5.4.12
 
 ### Minor Analysis Improvements

csharp/ql/lib/Linq/Helpers.qll

@@ -121,17 +121,15 @@ predicate missedOfTypeOpportunity(ForeachStmtEnumerable fes, LocalVariableDeclSt
 /**
  * Holds if `foreach` statement `fes` can be converted to a `.Select()` call.
  * That is, the loop variable is accessed only in the first statement of the
- * block, the access is not a cast, the first statement is a
- * local variable declaration statement `s`, and the initializer does not
- * contain an `await` expression (since `Select` does not support async lambdas).
+ * block, the access is not a cast, and the first statement is a
+ * local variable declaration statement `s`.
  */
 predicate missedSelectOpportunity(ForeachStmtGenericEnumerable fes, LocalVariableDeclStmt s) {
   s = firstStmt(fes) and
   forex(VariableAccess va | va = fes.getVariable().getAnAccess() |
     va = s.getAVariableDeclExpr().getAChildExpr*()
   ) and
-  not s.getAVariableDeclExpr().getInitializer() instanceof Cast and
-  not s.getAVariableDeclExpr().getInitializer().getAChildExpr*() instanceof AwaitExpr
+  not s.getAVariableDeclExpr().getInitializer() instanceof Cast
 }
 
 /**

csharp/ql/lib/change-notes/2026-03-20-data-extensions-barriers.md

@@ -1,4 +0,0 @@
----
-category: feature
----
-* Data flow barriers and barrier guards can now be added using data extensions. For more information see [Customizing library models for C#](https://codeql.github.com/docs/codeql-language-guides/customizing-library-models-for-csharp/).

csharp/ql/lib/change-notes/2026-04-01-asp-remote-sources.md

@@ -1,4 +0,0 @@
----
-category: minorAnalysis
----
-* Expanded ASP and ASP.NET remote source modeling to cover additional sources, including fields of tainted parameters as well as properties and fields that become tainted transitively.

csharp/ql/lib/change-notes/2026-04-01-getlrvalue.md

@@ -1,5 +1,4 @@
-## 5.5.0
-
-### Deprecated APIs
-
+---
+category: deprecated
+---
 * The predicates `get[L|R]Value` in the class `Assignment` have been deprecated. Use `get[Left|Right]Operand` instead.

csharp/ql/lib/change-notes/2026-04-13-cfg.md

@@ -1,20 +0,0 @@
----
-category: breaking
----
-* The C# control flow graph (CFG) implementation has been completely
-  rewritten. The CFG now includes additional nodes to more accurately represent
-  certain constructs. This also means that any existing code that implicitly
-  relies on very specific details about the CFG may need to be updated.
-  The CFG no longer uses splitting, which means that AST nodes now have a unique
-  CFG node representation.
-  Additionally, the following breaking changes have been made:
-  - `ControlFlow::Node` has been renamed to `ControlFlowNode`.
-  - `ControlFlow::Nodes` has been renamed to `ControlFlowNodes`.
-  - `BasicBlock.getCallable` has been renamed to `BasicBlock.getEnclosingCallable`.
-  - `BasicBlocks.qll` has been deleted.
-  - `ControlFlowNode.getAstNode` has changed its meaning. The AST-to-CFG
-    mapping remains one-to-many, but now for a different reason. It used to be
-    because of splitting, but now it's because of additional "helper" CFG
-    nodes. To get the (now canonical) CFG node for a given AST node, use
-    `ControlFlowNode.asExpr()` or `ControlFlowNode.asStmt()` or
-    `ControlFlowElement.getControlFlowNode()` instead.

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

@@ -1,2 +1,2 @@
 ---
-lastReleaseVersion: 5.5.0
+lastReleaseVersion: 5.4.12

csharp/ql/lib/experimental/code/csharp/Cryptography/NonCryptographicHashes.qll

@@ -30,7 +30,7 @@ predicate maybeUsedInFnvFunction(Variable v, Operation xor, Operation mul, LoopS
     e2.getAChild*() = v.getAnAccess() and
     e1 = xor.getAnOperand() and
     e2 = mul.getAnOperand() and
-    xor.getControlFlowNode().getASuccessor*() = mul.getControlFlowNode() and
+    xor.getAControlFlowNode().getASuccessor*() = mul.getAControlFlowNode() and
     (xor instanceof AssignXorExpr or xor instanceof BitwiseXorExpr) and
     (mul instanceof AssignMulExpr or mul instanceof MulExpr)
   ) and
@@ -55,11 +55,11 @@ private predicate maybeUsedInElfHashFunction(Variable v, Operation xor, Operatio
     v = addAssign.getTargetVariable() and
     addAssign.getAChild*() = add and
     (xor instanceof BitwiseXorExpr or xor instanceof AssignXorExpr) and
-    addAssign.getControlFlowNode().getASuccessor*() = xor.getControlFlowNode() and
+    addAssign.getAControlFlowNode().getASuccessor*() = xor.getAControlFlowNode() and
     xorAssign.getAChild*() = xor and
     v = xorAssign.getTargetVariable() and
     (notOp instanceof UnaryBitwiseOperation or notOp instanceof AssignBitwiseOperation) and
-    xor.getControlFlowNode().getASuccessor*() = notOp.getControlFlowNode() and
+    xor.getAControlFlowNode().getASuccessor*() = notOp.getAControlFlowNode() and
     notAssign.getAChild*() = notOp and
     v = notAssign.getTargetVariable() and
     loop.getAChild*() = add.getEnclosingStmt() and

csharp/ql/lib/printCfg.ql

@@ -7,7 +7,7 @@
  * @tags ide-contextual-queries/print-cfg
  */
 
-import csharp
+private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl
 
 external string selectedSourceFile();
 
@@ -21,7 +21,7 @@ external int selectedSourceColumn();
 
 private predicate selectedSourceColumnAlias = selectedSourceColumn/0;
 
-module ViewCfgQueryInput implements ControlFlow::ViewCfgQueryInputSig<File> {
+module ViewCfgQueryInput implements ViewCfgQueryInputSig<File> {
   predicate selectedSourceFile = selectedSourceFileAlias/0;
 
   predicate selectedSourceLine = selectedSourceLineAlias/0;
@@ -29,7 +29,7 @@ module ViewCfgQueryInput implements ControlFlow::ViewCfgQueryInputSig<File> {
   predicate selectedSourceColumn = selectedSourceColumnAlias/0;
 
   predicate cfgScopeSpan(
-    Callable scope, File file, int startLine, int startColumn, int endLine, int endColumn
+    CfgScope scope, File file, int startLine, int startColumn, int endLine, int endColumn
   ) {
     file = scope.getFile() and
     scope.getLocation().getStartLine() = startLine and
@@ -40,20 +40,11 @@ module ViewCfgQueryInput implements ControlFlow::ViewCfgQueryInputSig<File> {
     |
       loc = scope.(Callable).getBody().getLocation()
       or
-      loc = any(AssignExpr init | scope.(ObjectInitMethod).initializes(init)).getLocation()
+      loc = scope.(Field).getInitializer().getLocation()
       or
-      exists(AssignableMember a, Constructor ctor |
-        scope = ctor and
-        ctor.isStatic() and
-        a.isStatic() and
-        a.getDeclaringType() = ctor.getDeclaringType()
-      |
-        loc = a.(Field).getInitializer().getLocation()
-        or
-        loc = a.(Property).getInitializer().getLocation()
-      )
+      loc = scope.(Property).getInitializer().getLocation()
     )
   }
 }
 
-import ControlFlow::ViewCfgQuery<File, ViewCfgQueryInput>
+import ViewCfgQuery<File, ViewCfgQueryInput>

csharp/ql/lib/qlpack.yml

@@ -1,5 +1,5 @@
 name: codeql/csharp-all
-version: 5.5.1-dev
+version: 5.4.13-dev
 groups: csharp
 dbscheme: semmlecode.csharp.dbscheme
 extractor: csharp

csharp/ql/lib/semmle/code/csharp/Assignable.qll

@@ -85,8 +85,8 @@ class AssignableRead extends AssignableAccess {
   }
 
   pragma[noinline]
-  private ControlFlowNode getAnAdjacentReadSameVar() {
-    SsaImpl::adjacentReadPairSameVar(_, this.getControlFlowNode(), result)
+  private ControlFlow::Node getAnAdjacentReadSameVar() {
+    SsaImpl::adjacentReadPairSameVar(_, this.getAControlFlowNode(), result)
   }
 
   /**
@@ -114,7 +114,11 @@ class AssignableRead extends AssignableAccess {
    * - The read of `this.Field` on line 11 is next to the read on line 10.
    */
   pragma[nomagic]
-  AssignableRead getANextRead() { result.getControlFlowNode() = this.getAnAdjacentReadSameVar() }
+  AssignableRead getANextRead() {
+    forex(ControlFlow::Node cfn | cfn = result.getAControlFlowNode() |
+      cfn = this.getAnAdjacentReadSameVar()
+    )
+  }
 }
 
 /**
@@ -406,7 +410,7 @@ private import AssignableInternal
  */
 class AssignableDefinition extends TAssignableDefinition {
   /**
-   * DEPRECATED: Use `this.getExpr().getControlFlowNode()` instead.
+   * DEPRECATED: Use `this.getExpr().getAControlFlowNode()` instead.
    *
    * Gets a control flow node that updates the targeted assignable when
    * reached.
@@ -415,7 +419,9 @@ class AssignableDefinition extends TAssignableDefinition {
    * the definitions of `x` and `y` in `M(out x, out y)` and `(x, y) = (0, 1)`
    * relate to the same call to `M` and assignment node, respectively.
    */
-  deprecated ControlFlowNode getAControlFlowNode() { result = this.getExpr().getControlFlowNode() }
+  deprecated ControlFlow::Node getAControlFlowNode() {
+    result = this.getExpr().getAControlFlowNode()
+  }
 
   /**
    * Gets the underlying expression that updates the targeted assignable when
@@ -488,7 +494,7 @@ class AssignableDefinition extends TAssignableDefinition {
    */
   pragma[nomagic]
   AssignableRead getAFirstRead() {
-    exists(ControlFlowNode cfn | cfn = result.getControlFlowNode() |
+    forex(ControlFlow::Node cfn | cfn = result.getAControlFlowNode() |
       exists(Ssa::ExplicitDefinition def | result = def.getAFirstReadAtNode(cfn) |
         this = def.getADefinition()
       )
@@ -566,9 +572,11 @@ module AssignableDefinitions {
   }
 
   /** Holds if a node in basic block `bb` assigns to `ref` parameter `p` via definition `def`. */
-  private predicate basicBlockRefParamDef(BasicBlock bb, Parameter p, AssignableDefinition def) {
+  private predicate basicBlockRefParamDef(
+    ControlFlow::BasicBlock bb, Parameter p, AssignableDefinition def
+  ) {
     def = any(RefArg arg).getAnAnalyzableRefDef(p) and
-    bb.getANode() = def.getExpr().getControlFlowNode()
+    bb.getANode() = def.getExpr().getAControlFlowNode()
   }
 
   /**
@@ -577,7 +585,7 @@ module AssignableDefinitions {
    * any assignments to `p`.
    */
   pragma[nomagic]
-  private predicate parameterReachesWithoutDef(Parameter p, BasicBlock bb) {
+  private predicate parameterReachesWithoutDef(Parameter p, ControlFlow::BasicBlock bb) {
     forall(AssignableDefinition def | basicBlockRefParamDef(bb, p, def) |
       isUncertainRefCall(def.getTargetAccess())
     ) and
@@ -585,7 +593,9 @@ module AssignableDefinitions {
       any(RefArg arg).isAnalyzable(p) and
       p.getCallable().getEntryPoint() = bb.getFirstNode()
       or
-      exists(BasicBlock mid | parameterReachesWithoutDef(p, mid) | bb = mid.getASuccessor())
+      exists(ControlFlow::BasicBlock mid | parameterReachesWithoutDef(p, mid) |
+        bb = mid.getASuccessor()
+      )
     )
   }
 
@@ -597,7 +607,7 @@ module AssignableDefinitions {
   cached
   predicate isUncertainRefCall(RefArg arg) {
     arg.isPotentialAssignment() and
-    exists(BasicBlock bb, Parameter p | arg.isAnalyzable(p) |
+    exists(ControlFlow::BasicBlock bb, Parameter p | arg.isAnalyzable(p) |
       parameterReachesWithoutDef(p, bb) and
       bb.getLastNode() = p.getCallable().getExitPoint()
     )
@@ -678,7 +688,7 @@ module AssignableDefinitions {
     /** Gets the underlying parameter. */
     Parameter getParameter() { result = p }
 
-    deprecated override ControlFlowNode getAControlFlowNode() {
+    deprecated override ControlFlow::Node getAControlFlowNode() {
       result = p.getCallable().getEntryPoint()
     }
 

csharp/ql/lib/semmle/code/csharp/Caching.qll

@@ -7,6 +7,23 @@ private import csharp
  * in the same stage across different files.
  */
 module Stages {
+  cached
+  module ControlFlowStage {
+    private import semmle.code.csharp.controlflow.internal.Splitting
+
+    cached
+    predicate forceCachingInSameStage() { any() }
+
+    cached
+    private predicate forceCachingInSameStageRev() {
+      exists(Split s)
+      or
+      exists(ControlFlow::Node n)
+      or
+      forceCachingInSameStageRev()
+    }
+  }
+
   cached
   module GuardsStage {
     private import semmle.code.csharp.controlflow.Guards

csharp/ql/lib/semmle/code/csharp/Callable.qll

@@ -22,7 +22,7 @@ private import TypeRef
  * an anonymous function (`AnonymousFunctionExpr`), or a local function
  * (`LocalFunction`).
  */
-class Callable extends Parameterizable, ControlFlowElementOrCallable, @callable {
+class Callable extends Parameterizable, ExprOrStmtParent, @callable {
   /** Gets the return type of this callable. */
   Type getReturnType() { none() }
 
@@ -157,10 +157,10 @@ class Callable extends Parameterizable, ControlFlowElementOrCallable, @callable
   final predicate hasExpressionBody() { exists(this.getExpressionBody()) }
 
   /** Gets the entry point in the control graph for this callable. */
-  ControlFlow::EntryNode getEntryPoint() { result.getEnclosingCallable() = this }
+  ControlFlow::Nodes::EntryNode getEntryPoint() { result.getCallable() = this }
 
   /** Gets the exit point in the control graph for this callable. */
-  ControlFlow::ExitNode getExitPoint() { result.getEnclosingCallable() = this }
+  ControlFlow::Nodes::ExitNode getExitPoint() { result.getCallable() = this }
 
   /**
    * Gets the enclosing callable of this callable, if any.

csharp/ql/lib/semmle/code/csharp/ExprOrStmtParent.qll

@@ -129,6 +129,13 @@ private module Cached {
     result = parent.getAChildStmt()
   }
 
+  pragma[inline]
+  private ControlFlowElement enclosingStart(ControlFlowElement cfe) {
+    result = cfe
+    or
+    getAChild(result).(AnonymousFunctionExpr) = cfe
+  }
+
   private predicate parent(ControlFlowElement child, ExprOrStmtParent parent) {
     child = getAChild(parent) and
     not child = getBody(_)
@@ -138,7 +145,7 @@ private module Cached {
   cached
   predicate enclosingBody(ControlFlowElement cfe, ControlFlowElement body) {
     body = getBody(_) and
-    parent*(cfe, body)
+    parent*(enclosingStart(cfe), body)
   }
 
   /** Holds if the enclosing callable of `cfe` is `c`. */
@@ -146,7 +153,7 @@ private module Cached {
   predicate enclosingCallable(ControlFlowElement cfe, Callable c) {
     enclosingBody(cfe, getBody(c))
     or
-    parent*(cfe, c.(Constructor).getInitializer())
+    parent*(enclosingStart(cfe), c.(Constructor).getInitializer())
     or
     parent*(cfe, c.(Constructor).getObjectInitializerCall())
     or

csharp/ql/lib/semmle/code/csharp/commons/Collections.qll

@@ -54,44 +54,21 @@ private string genericCollectionTypeName() {
     ]
 }
 
-/** A collection type */
-abstract private class CollectionTypeImpl extends RefType {
-  /**
-   * Gets the element type of this collection, for example `int` in `List<int>`.
-   */
-  abstract Type getElementType();
-}
-
-private class GenericCollectionType extends CollectionTypeImpl {
-  private ConstructedType base;
-
-  GenericCollectionType() {
-    base = this.getABaseType*() and
-    base.getUnboundGeneric()
-        .hasFullyQualifiedName(genericCollectionNamespaceName(), genericCollectionTypeName())
-  }
-
-  override Type getElementType() {
-    result = base.getTypeArgument(0) and base.getNumberOfTypeArguments() = 1
-  }
-}
-
-private class NonGenericCollectionType extends CollectionTypeImpl {
-  NonGenericCollectionType() {
+/** A collection type. */
+class CollectionType extends RefType {
+  CollectionType() {
     exists(RefType base | base = this.getABaseType*() |
       base.hasFullyQualifiedName(collectionNamespaceName(), collectionTypeName())
+      or
+      base.(ConstructedType)
+          .getUnboundGeneric()
+          .hasFullyQualifiedName(genericCollectionNamespaceName(), genericCollectionTypeName())
     )
+    or
+    this instanceof ArrayType
   }
-
-  override Type getElementType() { none() }
 }
 
-private class ArrayCollectionType extends CollectionTypeImpl instanceof ArrayType {
-  override Type getElementType() { result = ArrayType.super.getElementType() }
-}
-
-final class CollectionType = CollectionTypeImpl;
-
 /**
  * A collection type that can be used as a `params` parameter type.
  */

csharp/ql/lib/semmle/code/csharp/commons/Strings.qll

@@ -29,7 +29,7 @@ class ImplicitToStringExpr extends Expr {
       m = p.getCallable()
     |
       m = any(SystemTextStringBuilderClass c).getAMethod() and
-      m.getName() = "Append" and
+      m.getName().regexpMatch("Append(Line)?") and
       not p.getType() instanceof ArrayType
       or
       p instanceof StringFormatItemParameter and

csharp/ql/lib/semmle/code/csharp/controlflow/BasicBlocks.qll

@@ -0,0 +1,356 @@
+/**
+ * Provides classes representing basic blocks.
+ */
+
+import csharp
+private import ControlFlow
+private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl as CfgImpl
+private import CfgImpl::BasicBlocks as BasicBlocksImpl
+private import codeql.controlflow.BasicBlock as BB
+
+/**
+ * A basic block, that is, a maximal straight-line sequence of control flow nodes
+ * without branches or joins.
+ */
+final class BasicBlock extends BasicBlocksImpl::BasicBlock {
+  /** Gets an immediate successor of this basic block of a given type, if any. */
+  BasicBlock getASuccessor(ControlFlow::SuccessorType t) { result = super.getASuccessor(t) }
+
+  /** DEPRECATED: Use `getASuccessor` instead. */
+  deprecated BasicBlock getASuccessorByType(ControlFlow::SuccessorType t) {
+    result = this.getASuccessor(t)
+  }
+
+  /** Gets an immediate predecessor of this basic block of a given type, if any. */
+  BasicBlock getAPredecessorByType(ControlFlow::SuccessorType t) {
+    result = this.getAPredecessor(t)
+  }
+
+  /**
+   * Gets an immediate `true` successor, if any.
+   *
+   * An immediate `true` successor is a successor that is reached when
+   * the condition that ends this basic block evaluates to `true`.
+   *
+   * Example:
+   *
+   * ```csharp
+   * if (x < 0)
+   *   x = -x;
+   * ```
+   *
+   * The basic block on line 2 is an immediate `true` successor of the
+   * basic block on line 1.
+   */
+  BasicBlock getATrueSuccessor() { result.getFirstNode() = this.getLastNode().getATrueSuccessor() }
+
+  /**
+   * Gets an immediate `false` successor, if any.
+   *
+   * An immediate `false` successor is a successor that is reached when
+   * the condition that ends this basic block evaluates to `false`.
+   *
+   * Example:
+   *
+   * ```csharp
+   * if (!(x >= 0))
+   *   x = -x;
+   * ```
+   *
+   * The basic block on line 2 is an immediate `false` successor of the
+   * basic block on line 1.
+   */
+  BasicBlock getAFalseSuccessor() {
+    result.getFirstNode() = this.getLastNode().getAFalseSuccessor()
+  }
+
+  BasicBlock getASuccessor() { result = super.getASuccessor() }
+
+  /** Gets the control flow node at a specific (zero-indexed) position in this basic block. */
+  ControlFlow::Node getNode(int pos) { result = super.getNode(pos) }
+
+  /** Gets a control flow node in this basic block. */
+  ControlFlow::Node getANode() { result = super.getANode() }
+
+  /** Gets the first control flow node in this basic block. */
+  ControlFlow::Node getFirstNode() { result = super.getFirstNode() }
+
+  /** Gets the last control flow node in this basic block. */
+  ControlFlow::Node getLastNode() { result = super.getLastNode() }
+
+  /** Gets the callable that this basic block belongs to. */
+  final Callable getCallable() { result = this.getFirstNode().getEnclosingCallable() }
+
+  /**
+   * Holds if this basic block immediately dominates basic block `bb`.
+   *
+   * That is, this basic block is the unique basic block satisfying:
+   * 1. This basic block strictly dominates `bb`
+   * 2. There exists no other basic block that is strictly dominated by this
+   *    basic block and which strictly dominates `bb`.
+   *
+   * All basic blocks, except entry basic blocks, have a unique immediate
+   * dominator.
+   *
+   * Example:
+   *
+   * ```csharp
+   * int M(string s) {
+   *   if (s == null)
+   *     throw new ArgumentNullException(nameof(s));
+   *   return s.Length;
+   * }
+   * ```
+   *
+   * The basic block starting on line 2 strictly dominates the
+   * basic block on line 4 (all paths from the entry point of `M`
+   * to `return s.Length;` must go through the null check).
+   */
+  predicate immediatelyDominates(BasicBlock bb) { super.immediatelyDominates(bb) }
+
+  /**
+   * Holds if this basic block strictly dominates basic block `bb`.
+   *
+   * That is, all paths reaching basic block `bb` from some entry point
+   * basic block must go through this basic block (which must be different
+   * from `bb`).
+   *
+   * Example:
+   *
+   * ```csharp
+   * int M(string s) {
+   *   if (s == null)
+   *     throw new ArgumentNullException(nameof(s));
+   *   return s.Length;
+   * }
+   * ```
+   *
+   * The basic block starting on line 2 strictly dominates the
+   * basic block on line 4 (all paths from the entry point of `M`
+   * to `return s.Length;` must go through the null check).
+   */
+  predicate strictlyDominates(BasicBlock bb) { super.strictlyDominates(bb) }
+
+  /**
+   * Holds if this basic block dominates basic block `bb`.
+   *
+   * That is, all paths reaching basic block `bb` from some entry point
+   * basic block must go through this basic block.
+   *
+   * Example:
+   *
+   * ```csharp
+   * int M(string s) {
+   *   if (s == null)
+   *     throw new ArgumentNullException(nameof(s));
+   *   return s.Length;
+   * }
+   * ```
+   *
+   * The basic block starting on line 2 dominates the basic
+   * block on line 4 (all paths from the entry point of `M` to
+   * `return s.Length;` must go through the null check).
+   *
+   * This predicate is *reflexive*, so for example `if (s == null)` dominates
+   * itself.
+   */
+  predicate dominates(BasicBlock bb) {
+    bb = this or
+    this.strictlyDominates(bb)
+  }
+
+  /**
+   * Holds if `df` is in the dominance frontier of this basic block.
+   * That is, this basic block dominates a predecessor of `df`, but
+   * does not dominate `df` itself.
+   *
+   * Example:
+   *
+   * ```csharp
+   * if (x < 0) {
+   *   x = -x;
+   *   if (x > 10)
+   *     x--;
+   * }
+   * Console.Write(x);
+   * ```
+   *
+   * The basic block on line 6 is in the dominance frontier
+   * of the basic block starting on line 2 because that block
+   * dominates the basic block on line 4, which is a predecessor of
+   * `Console.Write(x);`. Also, the basic block starting on line 2
+   * does not dominate the basic block on line 6.
+   */
+  predicate inDominanceFrontier(BasicBlock df) { super.inDominanceFrontier(df) }
+
+  /**
+   * Gets the basic block that immediately dominates this basic block, if any.
+   *
+   * That is, the result is the unique basic block satisfying:
+   * 1. The result strictly dominates this basic block.
+   * 2. There exists no other basic block that is strictly dominated by the
+   *    result and which strictly dominates this basic block.
+   *
+   * All basic blocks, except entry basic blocks, have a unique immediate
+   * dominator.
+   *
+   * Example:
+   *
+   * ```csharp
+   * int M(string s) {
+   *   if (s == null)
+   *     throw new ArgumentNullException(nameof(s));
+   *   return s.Length;
+   * }
+   * ```
+   *
+   * The basic block starting on line 2 is an immediate dominator of
+   * the basic block online 4 (all paths from the entry point of `M`
+   * to `return s.Length;` must go through the null check.
+   */
+  BasicBlock getImmediateDominator() { result = super.getImmediateDominator() }
+
+  /**
+   * Holds if the edge with successor type `s` out of this basic block is a
+   * dominating edge for `dominated`.
+   *
+   * That is, all paths reaching `dominated` from the entry point basic
+   * block must go through the `s` edge out of this basic block.
+   *
+   * Edge dominance is similar to node dominance except it concerns edges
+   * instead of nodes: A basic block is dominated by a _basic block_ `bb` if it
+   * can only be reached through `bb` and dominated by an _edge_ `e` if it can
+   * only be reached through `e`.
+   *
+   * Note that where all basic blocks (except the entry basic block) are
+   * strictly dominated by at least one basic block, a basic block may not be
+   * dominated by any edge. If an edge dominates a basic block `bb`, then
+   * both endpoints of the edge dominates `bb`. The converse is not the case,
+   * as there may be multiple paths between the endpoints with none of them
+   * dominating.
+   */
+  predicate edgeDominates(BasicBlock dominated, ControlFlow::SuccessorType s) {
+    super.edgeDominates(dominated, s)
+  }
+
+  /**
+   * Holds if this basic block strictly post-dominates basic block `bb`.
+   *
+   * That is, all paths reaching a normal exit point basic block from basic
+   * block `bb` must go through this basic block (which must be different
+   * from `bb`).
+   *
+   * Example:
+   *
+   * ```csharp
+   * int M(string s) {
+   *   try {
+   *     return s.Length;
+   *   }
+   *   finally {
+   *     Console.WriteLine("M");
+   *   }
+   * }
+   * ```
+   *
+   * The basic block on line 6 strictly post-dominates the basic block on
+   * line 3 (all paths to the exit point of `M` from `return s.Length;`
+   * must go through the `WriteLine` call).
+   */
+  predicate strictlyPostDominates(BasicBlock bb) { super.strictlyPostDominates(bb) }
+
+  /**
+   * Holds if this basic block post-dominates basic block `bb`.
+   *
+   * That is, all paths reaching a normal exit point basic block from basic
+   * block `bb` must go through this basic block.
+   *
+   * Example:
+   *
+   * ```csharp
+   * int M(string s) {
+   *   try {
+   *     return s.Length;
+   *   }
+   *   finally {
+   *     Console.WriteLine("M");
+   *   }
+   * }
+   * ```
+   *
+   * The basic block on line 6 post-dominates the basic block on line 3
+   * (all paths to the exit point of `M` from `return s.Length;` must go
+   * through the `WriteLine` call).
+   *
+   * This predicate is *reflexive*, so for example `Console.WriteLine("M");`
+   * post-dominates itself.
+   */
+  predicate postDominates(BasicBlock bb) { super.postDominates(bb) }
+
+  /**
+   * Holds if this basic block is in a loop in the control flow graph. This
+   * includes loops created by `goto` statements. This predicate may not hold
+   * even if this basic block is syntactically inside a `while` loop if the
+   * necessary back edges are unreachable.
+   */
+  predicate inLoop() { this.getASuccessor+() = this }
+}
+
+/**
+ * An entry basic block, that is, a basic block whose first node is
+ * an entry node.
+ */
+final class EntryBasicBlock extends BasicBlock, BasicBlocksImpl::EntryBasicBlock { }
+
+/**
+ * An annotated exit basic block, that is, a basic block that contains an
+ * annotated exit node.
+ */
+final class AnnotatedExitBasicBlock extends BasicBlock, BasicBlocksImpl::AnnotatedExitBasicBlock { }
+
+/**
+ * An exit basic block, that is, a basic block whose last node is
+ * an exit node.
+ */
+final class ExitBasicBlock extends BasicBlock, BasicBlocksImpl::ExitBasicBlock { }
+
+/** A basic block with more than one predecessor. */
+final class JoinBlock extends BasicBlock, BasicBlocksImpl::JoinBasicBlock {
+  JoinBlockPredecessor getJoinBlockPredecessor(int i) { result = super.getJoinBlockPredecessor(i) }
+}
+
+/** A basic block that is an immediate predecessor of a join block. */
+final class JoinBlockPredecessor extends BasicBlock, BasicBlocksImpl::JoinPredecessorBasicBlock { }
+
+/**
+ * A basic block that terminates in a condition, splitting the subsequent
+ * control flow.
+ */
+final class ConditionBlock extends BasicBlock, BasicBlocksImpl::ConditionBasicBlock {
+  /** DEPRECATED: Use `edgeDominates` instead. */
+  deprecated predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) {
+    this.getASuccessor(s) = succ and
+    BasicBlocksImpl::dominatingEdge(this, succ)
+  }
+
+  /** DEPRECATED: Use `edgeDominates` instead. */
+  deprecated predicate controls(BasicBlock controlled, ConditionalSuccessor s) {
+    super.edgeDominates(controlled, s)
+  }
+}
+
+private class BasicBlockAlias = BasicBlock;
+
+private class EntryBasicBlockAlias = EntryBasicBlock;
+
+module Cfg implements BB::CfgSig<Location> {
+  class ControlFlowNode = ControlFlow::Node;
+
+  class BasicBlock = BasicBlockAlias;
+
+  class EntryBasicBlock = EntryBasicBlockAlias;
+
+  predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) {
+    BasicBlocksImpl::dominatingEdge(bb1, bb2)
+  }
+}

csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowElement.qll

@@ -4,21 +4,20 @@ import csharp
 private import semmle.code.csharp.ExprOrStmtParent
 private import semmle.code.csharp.commons.Compilation
 private import ControlFlow
+private import ControlFlow::BasicBlocks
 private import semmle.code.csharp.Caching
-
-private class TControlFlowElementOrCallable = @callable or @control_flow_element;
-
-/** A `ControlFlowElement` or a `Callable`. */
-class ControlFlowElementOrCallable extends ExprOrStmtParent, TControlFlowElementOrCallable { }
+private import internal.ControlFlowGraphImpl as Impl
 
 /**
  * A program element that can possess control flow. That is, either a statement or
  * an expression.
  *
- * A control flow element can be mapped to a control flow node (`ControlFlowNode`)
- * via `getControlFlowNode()`.
+ * A control flow element can be mapped to a control flow node (`ControlFlow::Node`)
+ * via `getAControlFlowNode()`. There is a one-to-many relationship between
+ * control flow elements and control flow nodes. This allows control flow
+ * splitting, for example modeling the control flow through `finally` blocks.
  */
-class ControlFlowElement extends ControlFlowElementOrCallable, @control_flow_element {
+class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
   /** Gets the enclosing callable of this element, if any. */
   Callable getEnclosingCallable() { none() }
 
@@ -31,26 +30,41 @@ class ControlFlowElement extends ControlFlowElementOrCallable, @control_flow_ele
   }
 
   /**
-   * DEPRECATED: Use `getControlFlowNode()` instead.
-   *
    * Gets a control flow node for this element. That is, a node in the
    * control flow graph that corresponds to this element.
+   *
+   * Typically, there is exactly one `ControlFlow::Node` associated with a
+   * `ControlFlowElement`, but a `ControlFlowElement` may be split into
+   * several `ControlFlow::Node`s, for example to represent the continuation
+   * flow in a `try/catch/finally` construction.
    */
-  deprecated ControlFlowNodes::ElementNode getAControlFlowNode() {
-    result = this.getControlFlowNode()
-  }
+  Nodes::ElementNode getAControlFlowNode() { result.getAstNode() = this }
 
-  /** Gets the control flow node for this element, if any. */
-  ControlFlowNode getControlFlowNode() { result.injects(this) }
+  /** Gets the control flow node for this element. */
+  ControlFlow::Node getControlFlowNode() { result.getAstNode() = this }
 
   /** Gets the basic block in which this element occurs. */
-  BasicBlock getBasicBlock() { result = this.getControlFlowNode().getBasicBlock() }
+  BasicBlock getBasicBlock() { result = this.getAControlFlowNode().getBasicBlock() }
+
+  /**
+   * Gets a first control flow node executed within this element.
+   */
+  Nodes::ElementNode getAControlFlowEntryNode() {
+    result = Impl::getAControlFlowEntryNode(this).(ControlFlowElement).getAControlFlowNode()
+  }
+
+  /**
+   * Gets a potential last control flow node executed within this element.
+   */
+  Nodes::ElementNode getAControlFlowExitNode() {
+    result = Impl::getAControlFlowExitNode(this).(ControlFlowElement).getAControlFlowNode()
+  }
 
   /**
    * Holds if this element is live, that is this element can be reached
    * from the entry point of its enclosing callable.
    */
-  predicate isLive() { exists(this.getControlFlowNode()) }
+  predicate isLive() { exists(this.getAControlFlowNode()) }
 
   /** Holds if the current element is reachable from `src`. */
   // potentially very large predicate, so must be inlined
@@ -63,13 +77,31 @@ class ControlFlowElement extends ControlFlowElementOrCallable, @control_flow_ele
   ControlFlowElement getAReachableElement() {
     // Reachable in same basic block
     exists(BasicBlock bb, int i, int j |
-      bb.getNode(i) = this.getControlFlowNode() and
-      bb.getNode(j) = result.getControlFlowNode() and
+      bb.getNode(i) = this.getAControlFlowNode() and
+      bb.getNode(j) = result.getAControlFlowNode() and
       i < j
     )
     or
     // Reachable in different basic blocks
-    this.getControlFlowNode().getBasicBlock().getASuccessor+().getANode() =
-      result.getControlFlowNode()
+    this.getAControlFlowNode().getBasicBlock().getASuccessor+().getANode() =
+      result.getAControlFlowNode()
+  }
+
+  /**
+   * DEPRECATED: Use `Guard` class instead.
+   *
+   * Holds if basic block `controlled` is controlled by this control flow element
+   * with conditional value `s`. That is, `controlled` can only be reached from
+   * the callable entry point by going via the `s` edge out of *some* basic block
+   * ending with this element.
+   *
+   * `cb` records all of the possible condition blocks for this control flow element
+   * that a path from the callable entry point to `controlled` may go through.
+   */
+  deprecated predicate controlsBlock(
+    BasicBlock controlled, ConditionalSuccessor s, ConditionBlock cb
+  ) {
+    cb.getLastNode() = this.getAControlFlowNode() and
+    cb.edgeDominates(controlled, s)
   }
 }

csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowGraph.qll

@@ -1,577 +1,315 @@
+import csharp
+
 /**
  * Provides classes representing the control flow graph within callables.
  */
-
-import csharp
-private import codeql.controlflow.ControlFlowGraph
-private import codeql.controlflow.SuccessorType
-private import semmle.code.csharp.commons.Compilation
-private import semmle.code.csharp.controlflow.internal.NonReturning as NonReturning
-
-private module Cfg0 = Make0<Location, Ast>;
-
-private module Cfg1 = Make1<Input>;
-
-private module Cfg2 = Make2<Input>;
-
-private import Cfg0
-private import Cfg1
-private import Cfg2
-import Public
-
-/** Provides an implementation of the AST signature for C#. */
-private module Ast implements AstSig<Location> {
-  private import csharp as CS
-
-  class AstNode = ControlFlowElementOrCallable;
-
-  additional predicate skipControlFlow(AstNode e) {
-    e instanceof TypeAccess and
-    not e instanceof TypeAccessPatternExpr
-    or
-    not e.getFile().fromSource()
-  }
-
-  private AstNode getExprChild0(Expr e, int i) {
-    not e instanceof NameOfExpr and
-    not e instanceof AnonymousFunctionExpr and
-    not skipControlFlow(result) and
-    result = e.getChild(i)
-  }
-
-  private AstNode getStmtChild0(Stmt s, int i) {
-    not s instanceof FixedStmt and
-    not s instanceof UsingBlockStmt and
-    result = s.getChild(i)
-    or
-    s =
-      any(FixedStmt fs |
-        result = fs.getVariableDeclExpr(i)
-        or
-        result = fs.getBody() and
-        i = max(int j | exists(fs.getVariableDeclExpr(j))) + 1
-      )
-    or
-    s =
-      any(UsingBlockStmt us |
-        result = us.getExpr() and
-        i = 0
-        or
-        result = us.getVariableDeclExpr(i)
-        or
-        result = us.getBody() and
-        i = max([1, count(us.getVariableDeclExpr(_))])
-      )
-  }
-
-  AstNode getChild(AstNode n, int index) {
-    result = getStmtChild0(n, index)
-    or
-    result = getExprChild0(n, index)
-  }
-
-  private AstNode getParent(AstNode n) { n = getChild(result, _) }
-
-  Callable getEnclosingCallable(AstNode node) {
-    result = node.(ControlFlowElement).getEnclosingCallable() or
-    result.(ObjectInitMethod).initializes(getParent*(node)) or
-    Initializers::staticMemberInitializer(result, getParent*(node))
-  }
-
-  class Callable = CS::Callable;
-
-  AstNode callableGetBody(Callable c) {
-    not skipControlFlow(result) and
-    result = c.getBody()
-  }
-
-  class Stmt = CS::Stmt;
-
-  class Expr = CS::Expr;
-
-  class BlockStmt = CS::BlockStmt;
-
-  class ExprStmt = CS::ExprStmt;
-
-  class IfStmt = CS::IfStmt;
-
-  class LoopStmt = CS::LoopStmt;
-
-  class WhileStmt = CS::WhileStmt;
-
-  class DoStmt = CS::DoStmt;
-
-  final private class FinalForStmt = CS::ForStmt;
-
-  class ForStmt extends FinalForStmt {
-    Expr getInit(int index) { result = this.getInitializer(index) }
-  }
-
-  final private class FinalForeachStmt = CS::ForeachStmt;
-
-  class ForeachStmt extends FinalForeachStmt {
-    Expr getVariable() {
-      result = this.getVariableDeclExpr() or result = this.getVariableDeclTuple()
-    }
-
-    Expr getCollection() { result = this.getIterableExpr() }
-  }
-
-  class BreakStmt = CS::BreakStmt;
-
-  class ContinueStmt = CS::ContinueStmt;
-
-  class GotoStmt = CS::GotoStmt;
-
-  class ReturnStmt = CS::ReturnStmt;
-
-  class Throw = CS::ThrowElement;
-
-  final private class FinalTryStmt = CS::TryStmt;
-
-  class TryStmt extends FinalTryStmt {
-    Stmt getBody() { result = this.getBlock() }
-
-    CatchClause getCatch(int index) { result = this.getCatchClause(index) }
-
-    Stmt getFinally() { result = super.getFinally() }
-  }
-
-  final private class FinalCatchClause = CS::CatchClause;
-
-  class CatchClause extends FinalCatchClause {
-    AstNode getVariable() { result = this.(CS::SpecificCatchClause).getVariableDeclExpr() }
-
-    Expr getCondition() { result = this.getFilterClause() }
-
-    Stmt getBody() { result = this.getBlock() }
-  }
-
-  final private class FinalSwitch = CS::Switch;
-
-  class Switch extends FinalSwitch {
-    Case getCase(int index) { result = super.getCase(index) }
-
-    Stmt getStmt(int index) { result = this.(CS::SwitchStmt).getStmt(index) }
-  }
-
-  final private class FinalCase = CS::Case;
-
-  class Case extends FinalCase {
-    AstNode getAPattern() { result = this.getPattern() }
-
-    Expr getGuard() { result = this.getCondition() }
-
-    AstNode getBody() { result = super.getBody() }
-  }
-
-  class DefaultCase extends Case instanceof CS::DefaultCase { }
-
-  class ConditionalExpr = CS::ConditionalExpr;
-
-  class BinaryExpr = CS::BinaryOperation;
-
-  class LogicalAndExpr = CS::LogicalAndExpr;
-
-  class LogicalOrExpr = CS::LogicalOrExpr;
-
-  class NullCoalescingExpr = CS::NullCoalescingExpr;
-
-  class UnaryExpr = CS::UnaryOperation;
-
-  class LogicalNotExpr = CS::LogicalNotExpr;
-
-  class Assignment = CS::Assignment;
-
-  class AssignExpr = CS::AssignExpr;
-
-  class CompoundAssignment = CS::AssignOperation;
-
-  class AssignLogicalAndExpr extends CompoundAssignment {
-    AssignLogicalAndExpr() { none() }
-  }
-
-  class AssignLogicalOrExpr extends CompoundAssignment {
-    AssignLogicalOrExpr() { none() }
-  }
-
-  class AssignNullCoalescingExpr = CS::AssignCoalesceExpr;
-
-  final private class FinalBoolLiteral = CS::BoolLiteral;
-
-  class BooleanLiteral extends FinalBoolLiteral {
-    boolean getValue() { result = this.getBoolValue() }
-  }
-
-  final private class FinalIsExpr = CS::IsExpr;
-
-  class PatternMatchExpr extends FinalIsExpr {
-    AstNode getPattern() { result = super.getPattern() }
-  }
-}
-
-/**
- * A compilation.
- *
- * Unlike the standard `Compilation` class, this class also supports buildless
- * extraction.
- */
-private newtype TCompilationExt =
-  TCompilation(Compilation c) { not extractionIsStandalone() } or
-  TBuildless() { extractionIsStandalone() }
-
-private class CompilationExt extends TCompilationExt {
-  string toString() {
-    exists(Compilation c |
-      this = TCompilation(c) and
-      result = c.toString()
-    )
-    or
-    this = TBuildless() and result = "buildless compilation"
-  }
-}
-
-/** Gets the compilation that source file `f` belongs to. */
-private CompilationExt getCompilation(File f) {
-  exists(Compilation c |
-    f = c.getAFileCompiled() and
-    result = TCompilation(c)
-  )
-  or
-  result = TBuildless()
-}
-
-private module Initializers {
-  private import semmle.code.csharp.ExprOrStmtParent as ExprOrStmtParent
+module ControlFlow {
+  private import semmle.code.csharp.controlflow.BasicBlocks as BBs
+  import semmle.code.csharp.controlflow.internal.SuccessorType
+  private import internal.ControlFlowGraphImpl as Impl
+  private import internal.Splitting as Splitting
 
   /**
-   * The `expr_parent_top_level_adjusted()` relation restricted to exclude relations
-   * between properties and their getters' expression bodies in properties such as
-   * `int P => 0`.
+   * A control flow node.
    *
-   * This is in order to only associate the expression body with one CFG scope, namely
-   * the getter (and not the declaration itself).
+   * Either a callable entry node (`EntryNode`), a callable exit node (`ExitNode`),
+   * or a control flow node for a control flow element, that is, an expression or a
+   * statement (`ElementNode`).
+   *
+   * A control flow node is a node in the control flow graph (CFG). There is a
+   * many-to-one relationship between `ElementNode`s and `ControlFlowElement`s.
+   * This allows control flow splitting, for example modeling the control flow
+   * through `finally` blocks.
+   *
+   * Only nodes that can be reached from the callable entry point are included in
+   * the CFG.
    */
-  private predicate expr_parent_top_level_adjusted2(
-    Expr child, int i, @top_level_exprorstmt_parent parent
-  ) {
-    ExprOrStmtParent::expr_parent_top_level_adjusted(child, i, parent) and
-    not exists(Getter g |
-      g.getDeclaration() = parent and
-      i = 0
-    )
-  }
+  class Node extends Impl::Node {
+    /** Gets the control flow element that this node corresponds to, if any. */
+    final ControlFlowElement getAstNode() { result = super.getAstNode() }
 
-  /**
-   * Holds if `init` is a static member initializer and `staticCtor` is the
-   * static constructor in the same declaring type. Hence, `staticCtor` can be
-   * considered to execute `init` prior to the execution of its body.
-   */
-  predicate staticMemberInitializer(Constructor staticCtor, Expr init) {
-    exists(Assignable a |
-      a.(Modifiable).isStatic() and
-      expr_parent_top_level_adjusted2(init, _, a) and
-      a.getDeclaringType() = staticCtor.getDeclaringType() and
-      staticCtor.isStatic()
-    )
-  }
+    /** Gets the basic block that this control flow node belongs to. */
+    BasicBlock getBasicBlock() { result.getANode() = this }
 
-  /**
-   * Gets the `i`th static member initializer expression for static constructor `staticCtor`.
-   */
-  Expr initializedStaticMemberOrder(Constructor staticCtor, int i) {
-    result =
-      rank[i + 1](Expr init, Location l, string filepath, int startline, int startcolumn |
-        staticMemberInitializer(staticCtor, init) and
-        l = init.getLocation() and
-        l.hasLocationInfo(filepath, startline, startcolumn, _, _)
-      |
-        init order by startline, startcolumn, filepath
-      )
-  }
-
-  /**
-   * Gets the `i`th member initializer expression for object initializer method `obinit`.
-   */
-  AssignExpr initializedInstanceMemberOrder(ObjectInitMethod obinit, int i) {
-    result =
-      rank[i + 1](AssignExpr ae0, Location l, string filepath, int startline, int startcolumn |
-        obinit.initializes(ae0) and
-        l = ae0.getLocation() and
-        l.hasLocationInfo(filepath, startline, startcolumn, _, _)
-      |
-        ae0 order by startline, startcolumn, filepath
-      )
-  }
-}
-
-private module Exceptions {
-  private import semmle.code.csharp.commons.Assertions
-
-  private class Overflowable extends UnaryOperation {
-    Overflowable() {
-      not this instanceof UnaryBitwiseOperation and
-      this.getType() instanceof IntegralType
-    }
-  }
-
-  /** Holds if `cfe` is a control flow element that may throw an exception. */
-  predicate mayThrowException(ControlFlowElement cfe) {
-    cfe.(TriedControlFlowElement).mayThrowException()
-    or
-    cfe instanceof Assertion
-  }
-
-  /** A control flow element that is inside a `try` block. */
-  private class TriedControlFlowElement extends ControlFlowElement {
-    TriedControlFlowElement() {
-      this = any(TryStmt try).getATriedElement() and
-      not this instanceof NonReturning::NonReturningCall
+    /**
+     * Holds if this node dominates `that` node.
+     *
+     * That is, all paths reaching `that` node from some callable entry
+     * node (`EntryNode`) must go through this node.
+     *
+     * Example:
+     *
+     * ```csharp
+     * int M(string s)
+     * {
+     *     if (s == null)
+     *         throw new ArgumentNullException(nameof(s));
+     *     return s.Length;
+     * }
+     * ```
+     *
+     * The node on line 3 dominates the node on line 5 (all paths from the
+     * entry point of `M` to `return s.Length;` must go through the null check).
+     *
+     * This predicate is *reflexive*, so for example `if (s == null)` dominates
+     * itself.
+     */
+    // potentially very large predicate, so must be inlined
+    pragma[inline]
+    predicate dominates(Node that) {
+      this.strictlyDominates(that)
+      or
+      this = that
     }
 
     /**
-     * Holds if this element may potentially throw an exception.
+     * Holds if this node strictly dominates `that` node.
+     *
+     * That is, all paths reaching `that` node from some callable entry
+     * node (`EntryNode`) must go through this node (which must
+     * be different from `that` node).
+     *
+     * Example:
+     *
+     * ```csharp
+     * int M(string s)
+     * {
+     *     if (s == null)
+     *         throw new ArgumentNullException(nameof(s));
+     *     return s.Length;
+     * }
+     * ```
+     *
+     * The node on line 3 strictly dominates the node on line 5
+     * (all paths from the entry point of `M` to `return s.Length;` must go
+     * through the null check).
      */
-    predicate mayThrowException() {
-      this instanceof Overflowable
+    // potentially very large predicate, so must be inlined
+    pragma[inline]
+    predicate strictlyDominates(Node that) {
+      this.getBasicBlock().strictlyDominates(that.getBasicBlock())
       or
-      this.(CastExpr).getType() instanceof IntegralType
-      or
-      invalidCastCandidate(this)
-      or
-      this instanceof Call
-      or
-      this =
-        any(MemberAccess ma |
-          not ma.isConditional() and
-          ma.getQualifier() = any(Expr e | not e instanceof TypeAccess)
-        )
-      or
-      this instanceof DelegateCreation
-      or
-      this instanceof ArrayCreation
-      or
-      this =
-        any(AddOperation ae |
-          ae.getType() instanceof StringType
-          or
-          ae.getType() instanceof IntegralType
-        )
-      or
-      this = any(SubOperation se | se.getType() instanceof IntegralType)
-      or
-      this = any(MulOperation me | me.getType() instanceof IntegralType)
-      or
-      this = any(DivOperation de | not de.getDenominator().getValue().toFloat() != 0)
-      or
-      this instanceof RemOperation
-      or
-      this instanceof DynamicExpr
+      exists(BasicBlock bb, int i, int j |
+        bb.getNode(i) = this and
+        bb.getNode(j) = that and
+        i < j
+      )
     }
-  }
 
-  pragma[nomagic]
-  private ValueOrRefType getACastExprBaseType(CastExpr ce) {
-    result = ce.getType().(ValueOrRefType).getABaseType()
-    or
-    result = getACastExprBaseType(ce).getABaseType()
-  }
-
-  pragma[nomagic]
-  private predicate invalidCastCandidate(CastExpr ce) {
-    ce.getExpr().getType() = getACastExprBaseType(ce)
-  }
-}
-
-private module Input implements InputSig1, InputSig2 {
-  predicate cfgCachedStageRef() { CfgCachedStage::ref() }
-
-  predicate catchAll(Ast::CatchClause catch) { catch instanceof GeneralCatchClause }
-
-  predicate matchAll(Ast::Case c) { c instanceof DefaultCase or c.(SwitchCaseExpr).matchesAll() }
-
-  private newtype TLabel =
-    TLblGoto(string label) { any(GotoLabelStmt goto).getLabel() = label } or
-    TLblSwitchCase(string value) { any(GotoCaseStmt goto).getLabel() = value } or
-    TLblSwitchDefault()
-
-  class Label extends TLabel {
-    string toString() {
-      this = TLblGoto(result)
+    /**
+     * Holds if this node post-dominates `that` node.
+     *
+     * That is, all paths reaching a normal callable exit node (an `AnnotatedExitNode`
+     * with a normal exit type) from `that` node must go through this node.
+     *
+     * Example:
+     *
+     * ```csharp
+     * int M(string s)
+     * {
+     *     try
+     *     {
+     *         return s.Length;
+     *     }
+     *     finally
+     *     {
+     *         Console.WriteLine("M");
+     *     }
+     * }
+     * ```
+     *
+     * The node on line 9 post-dominates the node on line 5 (all paths to the
+     * exit point of `M` from `return s.Length;` must go through the `WriteLine`
+     * call).
+     *
+     * This predicate is *reflexive*, so for example `Console.WriteLine("M");`
+     * post-dominates itself.
+     */
+    // potentially very large predicate, so must be inlined
+    pragma[inline]
+    predicate postDominates(Node that) {
+      this.strictlyPostDominates(that)
       or
-      this = TLblSwitchCase(result)
-      or
-      this = TLblSwitchDefault() and result = "default"
+      this = that
     }
-  }
 
-  predicate hasLabel(Ast::AstNode n, Label l) {
-    l = TLblGoto(n.(GotoLabelStmt).getLabel())
-    or
-    l = TLblSwitchCase(n.(GotoCaseStmt).getLabel())
-    or
-    l = TLblSwitchDefault() and n instanceof GotoDefaultStmt
-    or
-    l = TLblGoto(n.(LabelStmt).getLabel())
-  }
-
-  class CallableBodyPartContext = CompilationExt;
-
-  pragma[nomagic]
-  Ast::AstNode callableGetBodyPart(Callable c, CallableBodyPartContext ctx, int index) {
-    not Ast::skipControlFlow(result) and
-    ctx = getCompilation(result.getFile()) and
-    (
-      result = Initializers::initializedInstanceMemberOrder(c, index)
+    /**
+     * Holds if this node strictly post-dominates `that` node.
+     *
+     * That is, all paths reaching a normal callable exit node (an `AnnotatedExitNode`
+     * with a normal exit type) from `that` node must go through this node
+     * (which must be different from `that` node).
+     *
+     * Example:
+     *
+     * ```csharp
+     * int M(string s)
+     * {
+     *     try
+     *     {
+     *         return s.Length;
+     *     }
+     *     finally
+     *     {
+     *          Console.WriteLine("M");
+     *     }
+     * }
+     * ```
+     *
+     * The node on line 9 strictly post-dominates the node on line 5 (all
+     * paths to the exit point of `M` from `return s.Length;` must go through
+     * the `WriteLine` call).
+     */
+    // potentially very large predicate, so must be inlined
+    pragma[inline]
+    predicate strictlyPostDominates(Node that) {
+      this.getBasicBlock().strictlyPostDominates(that.getBasicBlock())
       or
-      result = Initializers::initializedStaticMemberOrder(c, index)
-      or
-      exists(Constructor ctor, int i, int staticMembers |
-        c = ctor and
-        staticMembers = count(Expr init | Initializers::staticMemberInitializer(ctor, init)) and
-        index = staticMembers + i + 1
-      |
-        i = 0 and result = ctor.getObjectInitializerCall()
-        or
-        i = 1 and result = ctor.getInitializer()
-        or
-        i = 2 and result = ctor.getBody()
+      exists(BasicBlock bb, int i, int j |
+        bb.getNode(i) = this and
+        bb.getNode(j) = that and
+        i > j
       )
-    )
+    }
+
+    /** Gets a successor node of a given type, if any. */
+    Node getASuccessorByType(SuccessorType t) { result = this.getASuccessor(t) }
+
+    /** Gets an immediate successor, if any. */
+    Node getASuccessor() { result = this.getASuccessorByType(_) }
+
+    /** Gets an immediate predecessor node of a given flow type, if any. */
+    Node getAPredecessorByType(SuccessorType t) { result.getASuccessorByType(t) = this }
+
+    /** Gets an immediate predecessor, if any. */
+    Node getAPredecessor() { result = this.getAPredecessorByType(_) }
+
+    /**
+     * Gets an immediate `true` successor, if any.
+     *
+     * An immediate `true` successor is a successor that is reached when
+     * this condition evaluates to `true`.
+     *
+     * Example:
+     *
+     * ```csharp
+     * if (x < 0)
+     *     x = -x;
+     * ```
+     *
+     * The node on line 2 is an immediate `true` successor of the node
+     * on line 1.
+     */
+    Node getATrueSuccessor() {
+      result = this.getASuccessorByType(any(BooleanSuccessor t | t.getValue() = true))
+    }
+
+    /**
+     * Gets an immediate `false` successor, if any.
+     *
+     * An immediate `false` successor is a successor that is reached when
+     * this condition evaluates to `false`.
+     *
+     * Example:
+     *
+     * ```csharp
+     * if (!(x >= 0))
+     *     x = -x;
+     * ```
+     *
+     * The node on line 2 is an immediate `false` successor of the node
+     * on line 1.
+     */
+    Node getAFalseSuccessor() {
+      result = this.getASuccessorByType(any(BooleanSuccessor t | t.getValue() = false))
+    }
+
+    /** Gets the enclosing callable of this control flow node. */
+    final Callable getEnclosingCallable() { result = Impl::getNodeCfgScope(this) }
   }
 
-  private Expr getQualifier(QualifiableExpr qe) {
-    result = qe.getQualifier() or
-    result = qe.(ExtensionMethodCall).getArgument(0)
+  /** Provides different types of control flow nodes. */
+  module Nodes {
+    /** A node for a callable entry point. */
+    class EntryNode extends Node instanceof Impl::EntryNode {
+      /** Gets the callable that this entry applies to. */
+      Callable getCallable() { result = this.getScope() }
+
+      override BasicBlocks::EntryBlock getBasicBlock() { result = Node.super.getBasicBlock() }
+    }
+
+    /** A node for a callable exit point, annotated with the type of exit. */
+    class AnnotatedExitNode extends Node instanceof Impl::AnnotatedExitNode {
+      /** Holds if this node represent a normal exit. */
+      final predicate isNormal() { super.isNormal() }
+
+      /** Gets the callable that this exit applies to. */
+      Callable getCallable() { result = this.getScope() }
+
+      override BasicBlocks::AnnotatedExitBlock getBasicBlock() {
+        result = Node.super.getBasicBlock()
+      }
+    }
+
+    /** A control flow node indicating normal termination of a callable. */
+    class NormalExitNode extends AnnotatedExitNode instanceof Impl::NormalExitNode { }
+
+    /** A node for a callable exit point. */
+    class ExitNode extends Node instanceof Impl::ExitNode {
+      /** Gets the callable that this exit applies to. */
+      Callable getCallable() { result = this.getScope() }
+
+      override BasicBlocks::ExitBlock getBasicBlock() { result = Node.super.getBasicBlock() }
+    }
+
+    /**
+     * A node for a control flow element, that is, an expression or a statement.
+     *
+     * Each control flow element maps to zero or more `ElementNode`s: zero when
+     * the element is in unreachable (dead) code, and multiple when there are
+     * different splits for the element.
+     */
+    class ElementNode extends Node instanceof Impl::AstCfgNode {
+      /** Gets a comma-separated list of strings for each split in this node, if any. */
+      final string getSplitsString() { result = super.getSplitsString() }
+
+      /** Gets a split for this control flow node, if any. */
+      final Split getASplit() { result = super.getASplit() }
+    }
+
+    /** A control-flow node for an expression. */
+    class ExprNode extends ElementNode {
+      Expr e;
+
+      ExprNode() { e = unique(Expr e_ | e_ = this.getAstNode() | e_) }
+
+      /** Gets the expression that this control-flow node belongs to. */
+      Expr getExpr() { result = e }
+
+      /** Gets the value of this expression node, if any. */
+      string getValue() { result = e.getValue() }
+
+      /** Gets the type of this expression node. */
+      Type getType() { result = e.getType() }
+    }
+
+    class Split = Splitting::Split;
   }
 
-  predicate inConditionalContext(Ast::AstNode n, ConditionKind kind) {
-    kind.isNullness() and
-    exists(QualifiableExpr qe | qe.isConditional() | n = getQualifier(qe))
-  }
+  class BasicBlock = BBs::BasicBlock;
 
-  predicate postOrInOrder(Ast::AstNode n) { n instanceof YieldStmt or n instanceof Call }
+  /** Provides different types of basic blocks. */
+  module BasicBlocks {
+    class EntryBlock = BBs::EntryBasicBlock;
 
-  predicate beginAbruptCompletion(
-    Ast::AstNode ast, PreControlFlowNode n, AbruptCompletion c, boolean always
-  ) {
-    // `yield break` behaves like a return statement
-    ast instanceof YieldBreakStmt and
-    n.isIn(ast) and
-    c.asSimpleAbruptCompletion() instanceof ReturnSuccessor and
-    always = true
-    or
-    Exceptions::mayThrowException(ast) and
-    n.isIn(ast) and
-    c.asSimpleAbruptCompletion() instanceof ExceptionSuccessor and
-    always = false
-    or
-    ast instanceof NonReturning::NonReturningCall and
-    n.isIn(ast) and
-    c.asSimpleAbruptCompletion() instanceof ExceptionSuccessor and
-    always = true
-  }
+    class AnnotatedExitBlock = BBs::AnnotatedExitBasicBlock;
 
-  predicate endAbruptCompletion(Ast::AstNode ast, PreControlFlowNode n, AbruptCompletion c) {
-    exists(SwitchStmt switch, Label l, Ast::Case case |
-      ast.(Stmt).getParent() = switch and
-      c.getSuccessorType() instanceof GotoSuccessor and
-      c.hasLabel(l) and
-      n.isAfterValue(case, any(MatchingSuccessor t | t.getValue() = true))
-    |
-      exists(string value, ConstCase cc |
-        l = TLblSwitchCase(value) and
-        switch.getAConstCase() = cc and
-        cc.getLabel() = value and
-        cc = case
-      )
-      or
-      l = TLblSwitchDefault() and switch.getDefaultCase() = case
-    )
-  }
+    class ExitBlock = BBs::ExitBasicBlock;
 
-  predicate step(PreControlFlowNode n1, PreControlFlowNode n2) {
-    exists(QualifiableExpr qe | qe.isConditional() |
-      n1.isBefore(qe) and n2.isBefore(getQualifier(qe))
-      or
-      exists(NullnessSuccessor t | n1.isAfterValue(getQualifier(qe), t) |
-        if t.isNull()
-        then (
-          // if `q` is null in `q?.f = x` then the assignment is skipped. This
-          // holds for both regular, compound, and null-coalescing assignments.
-          // On the other hand, the CFG definition for the assignment can treat
-          // the LHS the same regardless of whether it's a conditionally
-          // qualified access or not, as it just connects to the "before" and
-          // "after" nodes of the LHS, and the "after" node is skipped in this
-          // case.
-          exists(AssignableDefinition def |
-            def.getTargetAccess() = qe and
-            n2.isAfterValue(def.getExpr(), t)
-          )
-          or
-          not qe instanceof AssignableWrite and
-          n2.isAfterValue(qe, t)
-        ) else (
-          n2.isBefore(Ast::getChild(qe, 0))
-          or
-          n2.isIn(qe) and not exists(Ast::getChild(qe, 0))
-        )
-      )
-      or
-      exists(int i | i >= 0 and n1.isAfter(Ast::getChild(qe, i)) |
-        n2.isBefore(Ast::getChild(qe, i + 1))
-        or
-        not exists(Ast::getChild(qe, i + 1)) and n2.isIn(qe)
-      )
-      or
-      n1.isIn(qe) and n2.isAfter(qe) and not beginAbruptCompletion(qe, n1, _, true)
-    )
-    or
-    exists(ObjectCreation oc |
-      n1.isBefore(oc) and n2.isBefore(oc.getArgument(0))
-      or
-      n1.isBefore(oc) and n2.isIn(oc) and not exists(oc.getAnArgument())
-      or
-      exists(int i | n1.isAfter(oc.getArgument(i)) |
-        n2.isBefore(oc.getArgument(i + 1))
-        or
-        not exists(oc.getArgument(i + 1)) and n2.isIn(oc)
-      )
-      or
-      n1.isIn(oc) and n2.isBefore(oc.getInitializer())
-      or
-      n1.isIn(oc) and n2.isAfter(oc) and not exists(oc.getInitializer())
-      or
-      n1.isAfter(oc.getInitializer()) and n2.isAfter(oc)
-    )
-  }
-}
-
-/** Provides different types of control flow nodes. */
-module ControlFlowNodes {
-  /**
-   * A node for a control flow element, that is, an expression or a statement.
-   *
-   * Each control flow element maps to zero or one `ElementNode`s: zero when
-   * the element is in unreachable (dead) code, and otherwise one.
-   */
-  class ElementNode extends ControlFlowNode {
-    ElementNode() { exists(this.asExpr()) or exists(this.asStmt()) }
-  }
-
-  /** A control-flow node for an expression. */
-  class ExprNode extends ElementNode {
-    Expr e;
-
-    ExprNode() { e = this.asExpr() }
-
-    /** Gets the expression that this control-flow node belongs to. */
-    Expr getExpr() { result = e }
-
-    /** Gets the value of this expression node, if any. */
-    string getValue() { result = e.getValue() }
-
-    /** Gets the type of this expression node. */
-    Type getType() { result = e.getType() }
+    class JoinBlock = BBs::JoinBlock;
+
+    class JoinBlockPredecessor = BBs::JoinBlockPredecessor;
+
+    class ConditionBlock = BBs::ConditionBlock;
   }
 }

csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowReachability.qll

@@ -4,13 +4,16 @@
 
 import csharp
 private import codeql.controlflow.ControlFlowReachability
+private import semmle.code.csharp.controlflow.BasicBlocks
 private import semmle.code.csharp.controlflow.Guards as Guards
 private import semmle.code.csharp.ExprOrStmtParent
 
-private module ControlFlowInput implements InputSig<Location, ControlFlowNode, BasicBlock> {
+private module ControlFlowInput implements
+  InputSig<Location, ControlFlow::Node, ControlFlow::BasicBlock>
+{
   private import csharp as CS
 
-  AstNode getEnclosingAstNode(ControlFlowNode node) {
+  AstNode getEnclosingAstNode(ControlFlow::Node node) {
     node.getAstNode() = result
     or
     not exists(node.getAstNode()) and result = node.getEnclosingCallable()

csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll

@@ -7,16 +7,20 @@ private import ControlFlow
 private import semmle.code.csharp.commons.Assertions
 private import semmle.code.csharp.commons.ComparisonTest
 private import semmle.code.csharp.commons.StructuralComparison as SC
+private import semmle.code.csharp.controlflow.BasicBlocks
+private import semmle.code.csharp.controlflow.internal.Completion
 private import semmle.code.csharp.frameworks.System
 private import semmle.code.csharp.frameworks.system.Linq
 private import semmle.code.csharp.frameworks.system.Collections
 private import semmle.code.csharp.frameworks.system.collections.Generic
 private import codeql.controlflow.Guards as SharedGuards
 
-private module GuardsInput implements SharedGuards::InputSig<Location, ControlFlowNode, BasicBlock> {
+private module GuardsInput implements
+  SharedGuards::InputSig<Location, ControlFlow::Node, ControlFlow::BasicBlock>
+{
   private import csharp as CS
 
-  class NormalExitNode = ControlFlow::NormalExitNode;
+  class NormalExitNode = ControlFlow::Nodes::NormalExitNode;
 
   class AstNode = ControlFlowElement;
 
@@ -83,14 +87,21 @@ private module GuardsInput implements SharedGuards::InputSig<Location, ControlFl
 
     ConstantExpr asConstantCase() { super.getPattern() = result }
 
+    private predicate hasEdge(BasicBlock bb1, BasicBlock bb2, MatchingCompletion c) {
+      exists(PatternExpr pe |
+        super.getPattern() = pe and
+        c.isValidFor(pe) and
+        bb1.getLastNode() = pe.getAControlFlowNode() and
+        bb1.getASuccessor(c.getAMatchingSuccessorType()) = bb2
+      )
+    }
+
     predicate matchEdge(BasicBlock bb1, BasicBlock bb2) {
-      bb1.getASuccessor(any(MatchingSuccessor s | s.getValue() = true)) = bb2 and
-      bb1.getLastNode() = AstNode.super.getControlFlowNode()
+      exists(MatchingCompletion c | this.hasEdge(bb1, bb2, c) and c.isMatch())
     }
 
     predicate nonMatchEdge(BasicBlock bb1, BasicBlock bb2) {
-      bb1.getASuccessor(any(MatchingSuccessor s | s.getValue() = false)) = bb2 and
-      bb1.getLastNode() = AstNode.super.getControlFlowNode()
+      exists(MatchingCompletion c | this.hasEdge(bb1, bb2, c) and c.isNonMatch())
     }
   }
 
@@ -302,7 +313,7 @@ class Guard extends Guards::Guard {
    * In case `cfn` or `sub` access an SSA variable in their left-most qualifier, then
    * so must the other (accessing the same SSA variable).
    */
-  predicate controlsNode(ControlFlowNodes::ElementNode cfn, AccessOrCallExpr sub, GuardValue v) {
+  predicate controlsNode(ControlFlow::Nodes::ElementNode cfn, AccessOrCallExpr sub, GuardValue v) {
     isGuardedByNode(cfn, this, sub, v)
   }
 
@@ -312,7 +323,7 @@ class Guard extends Guards::Guard {
    * Note: This predicate is inlined.
    */
   pragma[inline]
-  predicate controlsNode(ControlFlowNodes::ElementNode cfn, GuardValue v) {
+  predicate controlsNode(ControlFlow::Nodes::ElementNode cfn, GuardValue v) {
     guardControls(this, cfn.getBasicBlock(), v)
   }
 
@@ -430,8 +441,7 @@ class DereferenceableExpr extends Expr {
   predicate guardSuggestsMaybeNull(Guards::Guard guard) {
     not nonNullValueImplied(this) and
     (
-      exists(guard.getControlFlowNode().getASuccessor(any(NullnessSuccessor n | n.isNull()))) and
-      guard = this
+      exists(NullnessCompletion c | c.isValidFor(this) and c.isNull() and guard = this)
       or
       LogicInput::additionalNullCheck(guard, _, this, true)
       or
@@ -586,7 +596,7 @@ class AccessOrCallExpr extends Expr {
    * An expression can have more than one SSA qualifier in the presence
    * of control flow splitting.
    */
-  Ssa::Definition getAnSsaQualifier(ControlFlowNode cfn) { result = getAnSsaQualifier(this, cfn) }
+  Ssa::Definition getAnSsaQualifier(ControlFlow::Node cfn) { result = getAnSsaQualifier(this, cfn) }
 }
 
 private Declaration getDeclarationTarget(Expr e) {
@@ -594,14 +604,14 @@ private Declaration getDeclarationTarget(Expr e) {
   result = e.(Call).getTarget()
 }
 
-private Ssa::Definition getAnSsaQualifier(Expr e, ControlFlowNode cfn) {
+private Ssa::Definition getAnSsaQualifier(Expr e, ControlFlow::Node cfn) {
   e = getATrackedAccess(result, cfn)
   or
   not e = getATrackedAccess(_, _) and
   result = getAnSsaQualifier(e.(QualifiableExpr).getQualifier(), cfn)
 }
 
-private AssignableAccess getATrackedAccess(Ssa::Definition def, ControlFlowNode cfn) {
+private AssignableAccess getATrackedAccess(Ssa::Definition def, ControlFlow::Node cfn) {
   result = def.getAReadAtNode(cfn)
   or
   result = def.(Ssa::ExplicitDefinition).getADefinition().getTargetAccess() and
@@ -710,7 +720,7 @@ class GuardedExpr extends AccessOrCallExpr {
  * In the example above, the node for `x.ToString()` is null-guarded in the
  * split `b == true`, but not in the split `b == false`.
  */
-class GuardedControlFlowNode extends ControlFlowNodes::ElementNode {
+class GuardedControlFlowNode extends ControlFlow::Nodes::ElementNode {
   private Guard g;
   private AccessOrCallExpr sub0;
   private GuardValue v0;
@@ -766,7 +776,7 @@ class GuardedDataFlowNode extends DataFlow::ExprNode {
   private GuardValue v0;
 
   GuardedDataFlowNode() {
-    exists(ControlFlowNodes::ElementNode cfn | exists(this.getExprAtNode(cfn)) |
+    exists(ControlFlow::Nodes::ElementNode cfn | exists(this.getExprAtNode(cfn)) |
       g.controlsNode(cfn, sub0, v0)
     )
   }
@@ -1064,7 +1074,7 @@ module Internal {
       candidateAux(x, d, bb) and
       y =
         any(AccessOrCallExpr e |
-          e.getControlFlowNode().getBasicBlock() = bb and
+          e.getAControlFlowNode().getBasicBlock() = bb and
           e.getTarget() = d
         )
     )
@@ -1096,11 +1106,11 @@ module Internal {
 
     pragma[nomagic]
     private predicate nodeIsGuardedBySameSubExpr0(
-      ControlFlowNode guardedCfn, BasicBlock guardedBB, AccessOrCallExpr guarded, Guard g,
+      ControlFlow::Node guardedCfn, BasicBlock guardedBB, AccessOrCallExpr guarded, Guard g,
       AccessOrCallExpr sub, GuardValue v
     ) {
       Stages::GuardsStage::forceCachingInSameStage() and
-      guardedCfn = guarded.getControlFlowNode() and
+      guardedCfn = guarded.getAControlFlowNode() and
       guardedBB = guardedCfn.getBasicBlock() and
       guardControls(g, guardedBB, v) and
       guardControlsSubSame(g, guardedBB, sub) and
@@ -1109,7 +1119,7 @@ module Internal {
 
     pragma[nomagic]
     private predicate nodeIsGuardedBySameSubExpr(
-      ControlFlowNode guardedCfn, BasicBlock guardedBB, AccessOrCallExpr guarded, Guard g,
+      ControlFlow::Node guardedCfn, BasicBlock guardedBB, AccessOrCallExpr guarded, Guard g,
       AccessOrCallExpr sub, GuardValue v
     ) {
       nodeIsGuardedBySameSubExpr0(guardedCfn, guardedBB, guarded, g, sub, v) and
@@ -1118,8 +1128,8 @@ module Internal {
 
     pragma[nomagic]
     private predicate nodeIsGuardedBySameSubExprSsaDef0(
-      ControlFlowNode cfn, BasicBlock guardedBB, AccessOrCallExpr guarded, Guard g,
-      ControlFlowNode subCfn, BasicBlock subCfnBB, AccessOrCallExpr sub, GuardValue v,
+      ControlFlow::Node cfn, BasicBlock guardedBB, AccessOrCallExpr guarded, Guard g,
+      ControlFlow::Node subCfn, BasicBlock subCfnBB, AccessOrCallExpr sub, GuardValue v,
       Ssa::Definition def
     ) {
       nodeIsGuardedBySameSubExpr(cfn, guardedBB, guarded, g, sub, v) and
@@ -1129,7 +1139,7 @@ module Internal {
 
     pragma[nomagic]
     private predicate nodeIsGuardedBySameSubExprSsaDef(
-      ControlFlowNode guardedCfn, AccessOrCallExpr guarded, Guard g, ControlFlowNode subCfn,
+      ControlFlow::Node guardedCfn, AccessOrCallExpr guarded, Guard g, ControlFlow::Node subCfn,
       AccessOrCallExpr sub, GuardValue v, Ssa::Definition def
     ) {
       exists(BasicBlock guardedBB, BasicBlock subCfnBB |
@@ -1143,13 +1153,15 @@ module Internal {
     private predicate isGuardedByExpr0(
       AccessOrCallExpr guarded, Guard g, AccessOrCallExpr sub, GuardValue v
     ) {
-      nodeIsGuardedBySameSubExpr(guarded.getControlFlowNode(), _, guarded, g, sub, v)
+      forex(ControlFlow::Node cfn | cfn = guarded.getAControlFlowNode() |
+        nodeIsGuardedBySameSubExpr(cfn, _, guarded, g, sub, v)
+      )
     }
 
     cached
     predicate isGuardedByExpr(AccessOrCallExpr guarded, Guard g, AccessOrCallExpr sub, GuardValue v) {
       isGuardedByExpr0(guarded, g, sub, v) and
-      forall(ControlFlowNode subCfn, Ssa::Definition def |
+      forall(ControlFlow::Node subCfn, Ssa::Definition def |
         nodeIsGuardedBySameSubExprSsaDef(_, guarded, g, subCfn, sub, v, def)
       |
         def = guarded.getAnSsaQualifier(_)
@@ -1158,14 +1170,17 @@ module Internal {
 
     cached
     predicate isGuardedByNode(
-      ControlFlowNodes::ElementNode guarded, Guard g, AccessOrCallExpr sub, GuardValue v
+      ControlFlow::Nodes::ElementNode guarded, Guard g, AccessOrCallExpr sub, GuardValue v
     ) {
       nodeIsGuardedBySameSubExpr(guarded, _, _, g, sub, v) and
-      forall(ControlFlowNode subCfn, Ssa::Definition def |
+      forall(ControlFlow::Node subCfn, Ssa::Definition def |
         nodeIsGuardedBySameSubExprSsaDef(guarded, _, g, subCfn, sub, v, def)
       |
         def =
-          guarded.asExpr().(AccessOrCallExpr).getAnSsaQualifier(guarded.getBasicBlock().getANode())
+          guarded
+              .getAstNode()
+              .(AccessOrCallExpr)
+              .getAnSsaQualifier(guarded.getBasicBlock().getANode())
       )
     }
   }

csharp/ql/lib/semmle/code/csharp/controlflow/internal/Completion.qll

@@ -0,0 +1,896 @@
+/**
+ * INTERNAL: Do not use.
+ *
+ * Provides classes representing control flow completions.
+ *
+ * A completion represents how a statement or expression terminates.
+ *
+ * There are six kinds of completions: normal completion,
+ * `return` completion, `break` completion, `continue` completion,
+ * `goto` completion, and `throw` completion.
+ *
+ * Normal completions are further subdivided into Boolean completions and all
+ * other normal completions. A Boolean completion adds the information that the
+ * expression terminated with the given boolean value due to a subexpression
+ * terminating with the other given Boolean value. This is only relevant for
+ * conditional contexts in which the value controls the control-flow successor.
+ *
+ * Goto successors are further subdivided into label gotos, case gotos, and
+ * default gotos.
+ */
+
+import csharp
+private import semmle.code.csharp.commons.Assertions
+private import semmle.code.csharp.commons.Constants
+private import semmle.code.csharp.frameworks.System
+private import ControlFlowGraphImpl
+private import NonReturning
+private import SuccessorType
+
+private newtype TCompletion =
+  TSimpleCompletion() or
+  TBooleanCompletion(boolean b) { b = true or b = false } or
+  TNullnessCompletion(boolean isNull) { isNull = true or isNull = false } or
+  TMatchingCompletion(boolean isMatch) { isMatch = true or isMatch = false } or
+  TEmptinessCompletion(boolean isEmpty) { isEmpty = true or isEmpty = false } or
+  TReturnCompletion() or
+  TBreakCompletion() or
+  TContinueCompletion() or
+  TGotoCompletion(string label) { label = any(GotoStmt gs).getLabel() } or
+  TThrowCompletion(ExceptionClass ec) or
+  TExitCompletion() or
+  TNestedCompletion(Completion inner, Completion outer, int nestLevel) {
+    inner = TBreakCompletion() and
+    outer instanceof NonNestedNormalCompletion and
+    nestLevel = 0
+    or
+    inner instanceof NormalCompletion and
+    nestedFinallyCompletion(outer, nestLevel)
+  }
+
+pragma[nomagic]
+private int getAFinallyNestLevel() { result = any(Statements::TryStmtTree t).nestLevel() }
+
+pragma[nomagic]
+private predicate nestedFinallyCompletion(Completion outer, int nestLevel) {
+  (
+    outer = TReturnCompletion()
+    or
+    outer = TBreakCompletion()
+    or
+    outer = TContinueCompletion()
+    or
+    outer = TGotoCompletion(_)
+    or
+    outer = TThrowCompletion(_)
+    or
+    outer = TExitCompletion()
+  ) and
+  nestLevel = getAFinallyNestLevel()
+}
+
+pragma[noinline]
+private predicate completionIsValidForStmt(Stmt s, Completion c) {
+  s instanceof BreakStmt and
+  c = TBreakCompletion()
+  or
+  s instanceof ContinueStmt and
+  c = TContinueCompletion()
+  or
+  s instanceof GotoStmt and
+  c = TGotoCompletion(s.(GotoStmt).getLabel())
+  or
+  s instanceof ReturnStmt and
+  c = TReturnCompletion()
+  or
+  s instanceof YieldBreakStmt and
+  // `yield break` behaves like a return statement
+  c = TReturnCompletion()
+  or
+  mustHaveEmptinessCompletion(s) and
+  c = TEmptinessCompletion(_)
+}
+
+/**
+ * A completion of a statement or an expression.
+ */
+abstract class Completion extends TCompletion {
+  /**
+   * Holds if this completion is valid for control flow element `cfe`.
+   *
+   * If `cfe` is part of a `try` statement and `cfe` may throw an exception, this
+   * completion can be a throw completion.
+   *
+   * If `cfe` is used in a Boolean context, this completion is a Boolean completion,
+   * otherwise it is a normal non-Boolean completion.
+   */
+  predicate isValidFor(ControlFlowElement cfe) {
+    this = cfe.(NonReturningCall).getACompletion()
+    or
+    this = TThrowCompletion(cfe.(TriedControlFlowElement).getAThrownException())
+    or
+    cfe instanceof ThrowElement and
+    this = TThrowCompletion(cfe.(ThrowElement).getThrownExceptionType())
+    or
+    this = assertionCompletion(cfe, _)
+    or
+    completionIsValidForStmt(cfe, this)
+    or
+    mustHaveBooleanCompletion(cfe) and
+    (
+      exists(boolean value | isBooleanConstant(cfe, value) | this = TBooleanCompletion(value))
+      or
+      not isBooleanConstant(cfe, _) and
+      this = TBooleanCompletion(_)
+      or
+      // Corner case: In `if (x ?? y) { ... }`, `x` must have both a `true`
+      // completion, a `false` completion, and a `null` completion (but not a
+      // non-`null` completion)
+      mustHaveNullnessCompletion(cfe) and
+      this = TNullnessCompletion(true)
+    )
+    or
+    mustHaveNullnessCompletion(cfe) and
+    not mustHaveBooleanCompletion(cfe) and
+    (
+      exists(boolean value | isNullnessConstant(cfe, value) | this = TNullnessCompletion(value))
+      or
+      not isNullnessConstant(cfe, _) and
+      this = TNullnessCompletion(_)
+    )
+    or
+    mustHaveMatchingCompletion(cfe) and
+    (
+      exists(boolean value | isMatchingConstant(cfe, value) | this = TMatchingCompletion(value))
+      or
+      not isMatchingConstant(cfe, _) and
+      this = TMatchingCompletion(_)
+    )
+    or
+    not cfe instanceof NonReturningCall and
+    not cfe instanceof ThrowElement and
+    not cfe instanceof BreakStmt and
+    not cfe instanceof ContinueStmt and
+    not cfe instanceof GotoStmt and
+    not cfe instanceof ReturnStmt and
+    not cfe instanceof YieldBreakStmt and
+    not mustHaveBooleanCompletion(cfe) and
+    not mustHaveNullnessCompletion(cfe) and
+    not mustHaveMatchingCompletion(cfe) and
+    not mustHaveEmptinessCompletion(cfe) and
+    this = TSimpleCompletion()
+  }
+
+  /**
+   * Holds if this completion will continue a loop when it is the completion
+   * of a loop body.
+   */
+  predicate continuesLoop() {
+    this instanceof NormalCompletion or
+    this instanceof ContinueCompletion
+  }
+
+  /**
+   * Gets the inner completion. This is either the inner completion,
+   * when the completion is nested, or the completion itself.
+   */
+  Completion getInnerCompletion() { result = this }
+
+  /**
+   * Gets the outer completion. This is either the outer completion,
+   * when the completion is nested, or the completion itself.
+   */
+  Completion getOuterCompletion() { result = this }
+
+  /** Gets a successor type that matches this completion. */
+  abstract SuccessorType getAMatchingSuccessorType();
+
+  /** Gets a textual representation of this completion. */
+  abstract string toString();
+}
+
+/** Holds if expression `e` has the Boolean constant value `value`. */
+private predicate isBooleanConstant(Expr e, boolean value) {
+  mustHaveBooleanCompletion(e) and
+  (
+    e.getValue() = "true" and
+    value = true
+    or
+    e.getValue() = "false" and
+    value = false
+    or
+    isConstantComparison(e, value)
+    or
+    exists(Method m, Call c, Expr expr |
+      m = any(SystemStringClass s).getIsNullOrEmptyMethod() and
+      c.getTarget() = m and
+      e = c and
+      expr = c.getArgument(0) and
+      expr.hasValue() and
+      if expr.getValue().length() > 0 and not expr instanceof NullLiteral
+      then value = false
+      else value = true
+    )
+  )
+}
+
+/**
+ * Holds if expression `e` is constantly `null` (`value = true`) or constantly
+ * non-`null` (`value = false`).
+ */
+private predicate isNullnessConstant(Expr e, boolean value) {
+  mustHaveNullnessCompletion(e) and
+  exists(Expr stripped | stripped = e.stripCasts() |
+    stripped.getType() =
+      any(ValueType t |
+        not t instanceof NullableType and
+        // Extractor bug: the type of `x?.Length` is reported as `int`, but it should
+        // be `int?`
+        not getQualifier*(stripped).(QualifiableExpr).isConditional()
+      ) and
+    value = false
+    or
+    stripped instanceof NullLiteral and
+    value = true
+    or
+    stripped.hasValue() and
+    not stripped instanceof NullLiteral and
+    value = false
+  )
+}
+
+private Expr getQualifier(QualifiableExpr e) {
+  // `e.getQualifier()` does not work for calls to extension methods
+  result = e.getChildExpr(-1)
+}
+
+pragma[noinline]
+private predicate typePatternMustHaveMatchingCompletion(
+  TypePatternExpr tpe, Type t, Type strippedType
+) {
+  exists(Expr e, Expr stripped | mustHaveMatchingCompletion(e, tpe) |
+    stripped = e.stripCasts() and
+    t = tpe.getCheckedType() and
+    strippedType = stripped.getType() and
+    not t.containsTypeParameters() and
+    not strippedType.containsTypeParameters()
+  )
+}
+
+pragma[noinline]
+private Type typePatternCommonSubTypeLeft(Type t) {
+  typePatternMustHaveMatchingCompletion(_, t, _) and
+  result.isImplicitlyConvertibleTo(t) and
+  not result instanceof DynamicType
+}
+
+pragma[noinline]
+private Type typePatternCommonSubTypeRight(Type strippedType) {
+  typePatternMustHaveMatchingCompletion(_, _, strippedType) and
+  result.isImplicitlyConvertibleTo(strippedType) and
+  not result instanceof DynamicType
+}
+
+pragma[noinline]
+private predicate typePatternCommonSubType(Type t, Type strippedType) {
+  typePatternCommonSubTypeLeft(t) = typePatternCommonSubTypeRight(strippedType)
+}
+
+/**
+ * Holds if pattern expression `pe` constantly matches (`value = true`) or
+ * constantly non-matches (`value = false`).
+ */
+private predicate isMatchingConstant(PatternExpr pe, boolean value) {
+  exists(Expr e, string exprValue, string patternValue |
+    mustHaveMatchingCompletion(e, pe) and
+    exprValue = e.stripCasts().getValue() and
+    patternValue = pe.getValue() and
+    if exprValue = patternValue then value = true else value = false
+  )
+  or
+  pe instanceof DiscardPatternExpr and
+  value = true
+  or
+  exists(Type t, Type strippedType |
+    not t instanceof UnknownType and
+    not strippedType instanceof UnknownType and
+    typePatternMustHaveMatchingCompletion(pe, t, strippedType) and
+    not typePatternCommonSubType(t, strippedType) and
+    value = false
+  )
+}
+
+private class Overflowable extends UnaryOperation {
+  Overflowable() {
+    not this instanceof UnaryBitwiseOperation and
+    this.getType() instanceof IntegralType
+  }
+}
+
+/** A control flow element that is inside a `try` block. */
+private class TriedControlFlowElement extends ControlFlowElement {
+  TriedControlFlowElement() {
+    this = any(TryStmt try).getATriedElement() and
+    not this instanceof NonReturningCall
+  }
+
+  /**
+   * Gets an exception class that is potentially thrown by this element, if any.
+   */
+  Class getAThrownException() {
+    this instanceof Overflowable and
+    result instanceof SystemOverflowExceptionClass
+    or
+    this.(CastExpr).getType() instanceof IntegralType and
+    result instanceof SystemOverflowExceptionClass
+    or
+    invalidCastCandidate(this) and
+    result instanceof SystemInvalidCastExceptionClass
+    or
+    this instanceof Call and
+    result instanceof SystemExceptionClass
+    or
+    this =
+      any(MemberAccess ma |
+        not ma.isConditional() and
+        ma.getQualifier() = any(Expr e | not e instanceof TypeAccess) and
+        result instanceof SystemNullReferenceExceptionClass
+      )
+    or
+    this instanceof DelegateCreation and
+    result instanceof SystemOutOfMemoryExceptionClass
+    or
+    this instanceof ArrayCreation and
+    result instanceof SystemOutOfMemoryExceptionClass
+    or
+    this =
+      any(AddOperation ae |
+        ae.getType() instanceof StringType and
+        result instanceof SystemOutOfMemoryExceptionClass
+        or
+        ae.getType() instanceof IntegralType and
+        result instanceof SystemOverflowExceptionClass
+      )
+    or
+    this =
+      any(SubOperation se |
+        se.getType() instanceof IntegralType and
+        result instanceof SystemOverflowExceptionClass
+      )
+    or
+    this =
+      any(MulOperation me |
+        me.getType() instanceof IntegralType and
+        result instanceof SystemOverflowExceptionClass
+      )
+    or
+    this =
+      any(DivOperation de |
+        not de.getDenominator().getValue().toFloat() != 0 and
+        result instanceof SystemDivideByZeroExceptionClass
+      )
+    or
+    this instanceof RemOperation and
+    result instanceof SystemDivideByZeroExceptionClass
+    or
+    this instanceof DynamicExpr and
+    result instanceof SystemExceptionClass
+  }
+}
+
+pragma[nomagic]
+private ValueOrRefType getACastExprBaseType(CastExpr ce) {
+  result = ce.getType().(ValueOrRefType).getABaseType()
+  or
+  result = getACastExprBaseType(ce).getABaseType()
+}
+
+pragma[nomagic]
+private predicate invalidCastCandidate(CastExpr ce) {
+  ce.getExpr().getType() = getACastExprBaseType(ce)
+}
+
+/** Gets a valid completion when argument `i` fails in assertion `a`. */
+Completion assertionCompletion(Assertion a, int i) {
+  exists(AssertMethod am | am = a.getAssertMethod() |
+    if am.getAssertionFailure(i).isExit()
+    then result = TExitCompletion()
+    else
+      exists(Class c |
+        am.getAssertionFailure(i).isException(c) and
+        result = TThrowCompletion(c)
+      )
+  )
+}
+
+/**
+ * Holds if a normal completion of `e` must be a Boolean completion.
+ */
+private predicate mustHaveBooleanCompletion(Expr e) {
+  inBooleanContext(e) and
+  not e instanceof NonReturningCall
+}
+
+/**
+ * Holds if `e` is used in a Boolean context. That is, whether the value
+ * that `e` evaluates to determines a true/false branch successor.
+ */
+private predicate inBooleanContext(Expr e) {
+  e = any(IfStmt is).getCondition()
+  or
+  e = any(LoopStmt ls).getCondition()
+  or
+  e = any(Case c).getCondition()
+  or
+  e = any(SpecificCatchClause scc).getFilterClause()
+  or
+  e = any(LogicalNotExpr lne | inBooleanContext(lne)).getAnOperand()
+  or
+  exists(LogicalAndExpr lae |
+    lae.getLeftOperand() = e
+    or
+    inBooleanContext(lae) and
+    lae.getRightOperand() = e
+  )
+  or
+  exists(LogicalOrExpr lae |
+    lae.getLeftOperand() = e
+    or
+    inBooleanContext(lae) and
+    lae.getRightOperand() = e
+  )
+  or
+  exists(ConditionalExpr ce |
+    ce.getCondition() = e
+    or
+    inBooleanContext(ce) and
+    e in [ce.getThen(), ce.getElse()]
+  )
+  or
+  e = any(NullCoalescingOperation nce | inBooleanContext(nce)).getAnOperand()
+  or
+  e = any(SwitchExpr se | inBooleanContext(se)).getACase()
+  or
+  e = any(SwitchCaseExpr sce | inBooleanContext(sce)).getBody()
+}
+
+/**
+ * Holds if a normal completion of `e` must be a nullness completion.
+ */
+private predicate mustHaveNullnessCompletion(Expr e) {
+  inNullnessContext(e) and
+  not e instanceof NonReturningCall
+}
+
+/**
+ * Holds if `e` is used in a nullness context. That is, whether the value
+ * that `e` evaluates to determines a `null`/non-`null` branch successor.
+ */
+private predicate inNullnessContext(Expr e) {
+  e = any(NullCoalescingOperation nce).getLeftOperand()
+  or
+  exists(QualifiableExpr qe | qe.isConditional() | e = qe.getChildExpr(-1))
+  or
+  exists(ConditionalExpr ce | inNullnessContext(ce) | (e = ce.getThen() or e = ce.getElse()))
+  or
+  exists(NullCoalescingOperation nce | inNullnessContext(nce) | e = nce.getRightOperand())
+  or
+  e = any(SwitchExpr se | inNullnessContext(se)).getACase()
+  or
+  e = any(SwitchCaseExpr sce | inNullnessContext(sce)).getBody()
+}
+
+/**
+ * Holds if `pe` is the pattern inside case `c`, belonging to `switch` `s`, that
+ * has the matching completion.
+ */
+predicate switchMatching(Switch s, Case c, PatternExpr pe) {
+  s.getACase() = c and
+  pe = c.getPattern()
+}
+
+/**
+ * Holds if a normal completion of `cfe` must be a matching completion. Thats is,
+ * whether `cfe` determines a match in a `switch/if` statement or `catch` clause.
+ */
+private predicate mustHaveMatchingCompletion(ControlFlowElement cfe) {
+  switchMatching(_, _, cfe)
+  or
+  cfe instanceof SpecificCatchClause
+  or
+  cfe = any(IsExpr ie | inBooleanContext(ie)).getPattern()
+  or
+  cfe = any(RecursivePatternExpr rpe).getAChildExpr()
+  or
+  cfe = any(PositionalPatternExpr ppe).getPattern(_)
+  or
+  cfe = any(PropertyPatternExpr ppe).getPattern(_)
+  or
+  cfe = any(UnaryPatternExpr upe | mustHaveMatchingCompletion(upe)).getPattern()
+  or
+  cfe = any(BinaryPatternExpr bpe).getAnOperand()
+}
+
+/**
+ * Holds if `pe` must have a matching completion, and `e` is the expression
+ * that is being matched.
+ */
+private predicate mustHaveMatchingCompletion(Expr e, PatternExpr pe) {
+  exists(Switch s |
+    switchMatching(s, _, pe) and
+    e = s.getExpr()
+  )
+  or
+  e = any(IsExpr ie | pe = ie.getPattern()).getExpr() and
+  mustHaveMatchingCompletion(pe)
+  or
+  exists(PatternExpr mid | mustHaveMatchingCompletion(e, mid) |
+    pe = mid.(UnaryPatternExpr).getPattern()
+    or
+    pe = mid.(RecursivePatternExpr).getAChildExpr()
+    or
+    pe = mid.(BinaryPatternExpr).getAnOperand()
+  )
+}
+
+/**
+ * Holds if `cfe` is the element inside foreach statement `fs` that has the emptiness
+ * completion.
+ */
+predicate foreachEmptiness(ForeachStmt fs, ControlFlowElement cfe) {
+  cfe = fs // use `foreach` statement itself to represent the emptiness test
+}
+
+/**
+ * Holds if a normal completion of `cfe` must be an emptiness completion. Thats is,
+ * whether `cfe` determines whether to execute the body of a `foreach` statement.
+ */
+private predicate mustHaveEmptinessCompletion(ControlFlowElement cfe) { foreachEmptiness(_, cfe) }
+
+/**
+ * A completion that represents normal evaluation of a statement or an
+ * expression.
+ */
+abstract class NormalCompletion extends Completion { }
+
+abstract private class NonNestedNormalCompletion extends NormalCompletion { }
+
+/** A simple (normal) completion. */
+class SimpleCompletion extends NonNestedNormalCompletion, TSimpleCompletion {
+  override DirectSuccessor getAMatchingSuccessorType() { any() }
+
+  override string toString() { result = "normal" }
+}
+
+/**
+ * A completion that represents evaluation of an expression, whose value determines
+ * the successor. Either a Boolean completion (`BooleanCompletion`), a nullness
+ * completion (`NullnessCompletion`), a matching completion (`MatchingCompletion`),
+ * or an emptiness completion (`EmptinessCompletion`).
+ */
+abstract class ConditionalCompletion extends NonNestedNormalCompletion {
+  /** Gets the Boolean value of this completion. */
+  abstract boolean getValue();
+
+  /** Gets the dual completion. */
+  abstract ConditionalCompletion getDual();
+}
+
+/**
+ * A completion that represents evaluation of an expression
+ * with a Boolean value.
+ */
+class BooleanCompletion extends ConditionalCompletion {
+  private boolean value;
+
+  BooleanCompletion() { this = TBooleanCompletion(value) }
+
+  override boolean getValue() { result = value }
+
+  override BooleanCompletion getDual() { result = TBooleanCompletion(value.booleanNot()) }
+
+  override BooleanSuccessor getAMatchingSuccessorType() { result.getValue() = value }
+
+  override string toString() { result = value.toString() }
+}
+
+/** A Boolean `true` completion. */
+class TrueCompletion extends BooleanCompletion {
+  TrueCompletion() { this.getValue() = true }
+}
+
+/** A Boolean `false` completion. */
+class FalseCompletion extends BooleanCompletion {
+  FalseCompletion() { this.getValue() = false }
+}
+
+/**
+ * A completion that represents evaluation of an expression that is either
+ * `null` or non-`null`.
+ */
+class NullnessCompletion extends ConditionalCompletion, TNullnessCompletion {
+  private boolean value;
+
+  NullnessCompletion() { this = TNullnessCompletion(value) }
+
+  /** Holds if the last sub expression of this expression evaluates to `null`. */
+  predicate isNull() { value = true }
+
+  /** Holds if the last sub expression of this expression evaluates to a non-`null` value. */
+  predicate isNonNull() { value = false }
+
+  override boolean getValue() { result = value }
+
+  override NullnessCompletion getDual() { result = TNullnessCompletion(value.booleanNot()) }
+
+  override NullnessSuccessor getAMatchingSuccessorType() { result.getValue() = value }
+
+  override string toString() { if this.isNull() then result = "null" else result = "non-null" }
+}
+
+/**
+ * A completion that represents matching, for example a `case` statement in a
+ * `switch` statement.
+ */
+class MatchingCompletion extends ConditionalCompletion, TMatchingCompletion {
+  private boolean value;
+
+  MatchingCompletion() { this = TMatchingCompletion(value) }
+
+  /** Holds if there is a match. */
+  predicate isMatch() { value = true }
+
+  /** Holds if there is not a match. */
+  predicate isNonMatch() { value = false }
+
+  override boolean getValue() { result = value }
+
+  override MatchingCompletion getDual() { result = TMatchingCompletion(value.booleanNot()) }
+
+  override MatchingSuccessor getAMatchingSuccessorType() { result.getValue() = value }
+
+  override string toString() { if this.isMatch() then result = "match" else result = "no-match" }
+}
+
+/**
+ * A completion that represents evaluation of an emptiness test, for example
+ * a test in a `foreach` statement.
+ */
+class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
+  private boolean value;
+
+  EmptinessCompletion() { this = TEmptinessCompletion(value) }
+
+  /** Holds if the emptiness test evaluates to `true`. */
+  predicate isEmpty() { value = true }
+
+  override boolean getValue() { result = value }
+
+  override EmptinessCompletion getDual() { result = TEmptinessCompletion(value.booleanNot()) }
+
+  override EmptinessSuccessor getAMatchingSuccessorType() { result.getValue() = value }
+
+  override string toString() { if this.isEmpty() then result = "empty" else result = "non-empty" }
+}
+
+/**
+ * A nested completion. For example, in
+ *
+ * ```csharp
+ * void M(bool b1, bool b2)
+ * {
+ *     try
+ *     {
+ *         if (b1)
+ *            throw new Exception();
+ *     }
+ *     finally
+ *     {
+ *         if (b2)
+ *             System.Console.WriteLine("M called");
+ *     }
+ * }
+ * ```
+ *
+ * `b2` has an outer throw completion (inherited from `throw new Exception`)
+ * and an inner `false` completion. `b2` also has a (normal) `true` completion.
+ */
+class NestedCompletion extends Completion, TNestedCompletion {
+  Completion inner;
+  Completion outer;
+  int nestLevel;
+
+  NestedCompletion() { this = TNestedCompletion(inner, outer, nestLevel) }
+
+  /** Gets a completion that is compatible with the inner completion. */
+  Completion getAnInnerCompatibleCompletion() {
+    result.getOuterCompletion() = this.getInnerCompletion()
+  }
+
+  /** Gets the level of this nested completion. */
+  int getNestLevel() { result = nestLevel }
+
+  override Completion getInnerCompletion() { result = inner }
+
+  override Completion getOuterCompletion() { result = outer }
+
+  override SuccessorType getAMatchingSuccessorType() { none() }
+
+  override string toString() { result = outer + " [" + inner + "] (" + nestLevel + ")" }
+}
+
+/**
+ * A nested completion for a loop that exists with a `break`.
+ *
+ * This completion is added for technical reasons only: when a loop
+ * body can complete with a break completion, the loop itself completes
+ * normally. However, if we choose `TSimpleCompletion` as the completion
+ * of the loop, we lose the information that the last element actually
+ * completed with a break, meaning that the control flow edge out of the
+ * breaking node cannot be marked with a `break` label.
+ *
+ * Example:
+ *
+ * ```csharp
+ * while (...) {
+ *    ...
+ *    break;
+ * }
+ * return;
+ * ```
+ *
+ * The `break` on line 3 completes with a `TBreakCompletion`, therefore
+ * the `while` loop can complete with a `NestedBreakCompletion`, so we
+ * get an edge `break --break--> return`. (If we instead used a
+ * `TSimpleCompletion`, we would get a less precise edge
+ * `break --normal--> return`.)
+ */
+class NestedBreakCompletion extends NormalCompletion, NestedCompletion {
+  NestedBreakCompletion() {
+    inner = TBreakCompletion() and
+    outer instanceof NonNestedNormalCompletion
+  }
+
+  override BreakCompletion getInnerCompletion() { result = inner }
+
+  override NonNestedNormalCompletion getOuterCompletion() { result = outer }
+
+  override Completion getAnInnerCompatibleCompletion() {
+    result = inner and
+    outer = TSimpleCompletion()
+    or
+    result = TNestedCompletion(outer, inner, _)
+  }
+
+  override SuccessorType getAMatchingSuccessorType() {
+    outer instanceof SimpleCompletion and
+    result instanceof BreakSuccessor
+    or
+    result = outer.(ConditionalCompletion).getAMatchingSuccessorType()
+  }
+}
+
+/**
+ * A completion that represents evaluation of a statement or an
+ * expression resulting in a return from a callable.
+ */
+class ReturnCompletion extends Completion {
+  ReturnCompletion() {
+    this = TReturnCompletion() or
+    this = TNestedCompletion(_, TReturnCompletion(), _)
+  }
+
+  override ReturnSuccessor getAMatchingSuccessorType() { any() }
+
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TReturnCompletion() and result = "return"
+  }
+}
+
+/**
+ * A completion that represents evaluation of a statement or an
+ * expression resulting in a break (in a loop or in a `switch`
+ * statement).
+ */
+class BreakCompletion extends Completion {
+  BreakCompletion() {
+    this = TBreakCompletion() or
+    this = TNestedCompletion(_, TBreakCompletion(), _)
+  }
+
+  override BreakSuccessor getAMatchingSuccessorType() { any() }
+
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TBreakCompletion() and result = "break"
+  }
+}
+
+/**
+ * A completion that represents evaluation of a statement or an
+ * expression resulting in a loop continuation (a `continue`
+ * statement).
+ */
+class ContinueCompletion extends Completion {
+  ContinueCompletion() {
+    this = TContinueCompletion() or
+    this = TNestedCompletion(_, TContinueCompletion(), _)
+  }
+
+  override ContinueSuccessor getAMatchingSuccessorType() { any() }
+
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TContinueCompletion() and result = "continue"
+  }
+}
+
+/**
+ * A completion that represents evaluation of a statement or an
+ * expression resulting in a `goto` jump.
+ */
+class GotoCompletion extends Completion {
+  private string label;
+
+  GotoCompletion() {
+    this = TGotoCompletion(label) or
+    this = TNestedCompletion(_, TGotoCompletion(label), _)
+  }
+
+  /** Gets the label of the `goto` completion. */
+  string getLabel() { result = label }
+
+  override GotoSuccessor getAMatchingSuccessorType() { any() }
+
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TGotoCompletion(label) and result = "goto(" + label + ")"
+  }
+}
+
+/**
+ * A completion that represents evaluation of a statement or an
+ * expression resulting in a thrown exception.
+ */
+class ThrowCompletion extends Completion {
+  private ExceptionClass ec;
+
+  ThrowCompletion() {
+    this = TThrowCompletion(ec) or
+    this = TNestedCompletion(_, TThrowCompletion(ec), _)
+  }
+
+  /** Gets the type of the exception being thrown. */
+  ExceptionClass getExceptionClass() { result = ec }
+
+  override ExceptionSuccessor getAMatchingSuccessorType() { any() }
+
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TThrowCompletion(ec) and result = "throw(" + ec + ")"
+  }
+}
+
+/**
+ * A completion that represents evaluation of a statement or an
+ * expression resulting in a program exit, for example
+ * `System.Environment.Exit(0)`.
+ *
+ * An exit completion is different from a `return` completion; the former
+ * exits the whole application, and exists inside `try` statements skip
+ * `finally` blocks.
+ */
+class ExitCompletion extends Completion {
+  ExitCompletion() {
+    this = TExitCompletion() or
+    this = TNestedCompletion(_, TExitCompletion(), _)
+  }
+
+  override ExitSuccessor getAMatchingSuccessorType() { any() }
+
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TExitCompletion() and result = "exit"
+  }
+}

csharp/ql/lib/semmle/code/csharp/controlflow/internal/NonReturning.qll

@@ -9,9 +9,13 @@ import csharp
 private import semmle.code.csharp.ExprOrStmtParent
 private import semmle.code.csharp.commons.Assertions
 private import semmle.code.csharp.frameworks.System
+private import Completion
 
 /** A call that definitely does not return (conservative analysis). */
-abstract class NonReturningCall extends Call { }
+abstract class NonReturningCall extends Call {
+  /** Gets a valid completion for this non-returning call. */
+  abstract Completion getACompletion();
+}
 
 private class ExitingCall extends NonReturningCall {
   ExitingCall() {
@@ -19,21 +23,36 @@ private class ExitingCall extends NonReturningCall {
     or
     this = any(FailingAssertion fa | fa.getAssertionFailure().isExit())
   }
+
+  override ExitCompletion getACompletion() { not result instanceof NestedCompletion }
 }
 
 private class ThrowingCall extends NonReturningCall {
+  private ThrowCompletion c;
+
   ThrowingCall() {
-    this.getTarget() instanceof ThrowingCallable
-    or
-    this.(FailingAssertion).getAssertionFailure().isException(_)
-    or
-    this =
-      any(MethodCall mc |
-        mc.getTarget()
-            .hasFullyQualifiedName("System.Runtime.ExceptionServices", "ExceptionDispatchInfo",
-              "Throw")
-      )
+    not c instanceof NestedCompletion and
+    (
+      c = this.getTarget().(ThrowingCallable).getACallCompletion()
+      or
+      this.(FailingAssertion).getAssertionFailure().isException(c.getExceptionClass())
+      or
+      this =
+        any(MethodCall mc |
+          mc.getTarget()
+              .hasFullyQualifiedName("System.Runtime.ExceptionServices", "ExceptionDispatchInfo",
+                "Throw") and
+          (
+            mc.hasNoArguments() and
+            c.getExceptionClass() instanceof SystemExceptionClass
+            or
+            c.getExceptionClass() = mc.getArgument(0).getType()
+          )
+        )
+    )
   }
+
+  override ThrowCompletion getACompletion() { result = c }
 }
 
 /** Holds if accessor `a` has an auto-implementation. */
@@ -88,35 +107,44 @@ private Stmt getAnExitingStmt() {
 
 private class ThrowingCallable extends NonReturningCallable {
   ThrowingCallable() {
-    forex(ControlFlowElement body | body = this.getBody() | body = getAThrowingElement())
+    forex(ControlFlowElement body | body = this.getBody() | body = getAThrowingElement(_))
   }
+
+  /** Gets a valid completion for a call to this throwing callable. */
+  ThrowCompletion getACallCompletion() { this.getBody() = getAThrowingElement(result) }
 }
 
-private predicate directlyThrows(ThrowElement te) {
+private predicate directlyThrows(ThrowElement te, ThrowCompletion c) {
+  c.getExceptionClass() = te.getThrownExceptionType() and
+  not c instanceof NestedCompletion and
   // For stub implementations, there may exist proper implementations that are not seen
   // during compilation, so we conservatively rule those out
   not isStub(te)
 }
 
-private ControlFlowElement getAThrowingElement() {
-  result instanceof ThrowingCall
+private ControlFlowElement getAThrowingElement(ThrowCompletion c) {
+  c = result.(ThrowingCall).getACompletion()
   or
-  directlyThrows(result)
+  directlyThrows(result, c)
   or
-  result = getAThrowingStmt()
+  result = getAThrowingStmt(c)
 }
 
-private Stmt getAThrowingStmt() {
-  directlyThrows(result)
+private Stmt getAThrowingStmt(ThrowCompletion c) {
+  directlyThrows(result, c)
   or
-  result.(ExprStmt).getExpr() = getAThrowingElement()
+  result.(ExprStmt).getExpr() = getAThrowingElement(c)
   or
-  result.(BlockStmt).getFirstStmt() = getAThrowingStmt()
+  result.(BlockStmt).getFirstStmt() = getAThrowingStmt(c)
   or
-  exists(IfStmt ifStmt |
+  exists(IfStmt ifStmt, ThrowCompletion c1, ThrowCompletion c2 |
     result = ifStmt and
-    ifStmt.getThen() = getAThrowingStmt() and
-    ifStmt.getElse() = getAThrowingStmt()
+    ifStmt.getThen() = getAThrowingStmt(c1) and
+    ifStmt.getElse() = getAThrowingStmt(c2)
+  |
+    c = c1
+    or
+    c = c2
   )
 }
 

csharp/ql/lib/semmle/code/csharp/controlflow/internal/Splitting.qll

@@ -0,0 +1,124 @@
+/**
+ * INTERNAL: Do not use.
+ *
+ * Provides classes and predicates relevant for splitting the control flow graph.
+ */
+
+import csharp
+private import Completion as Comp
+private import Comp
+private import ControlFlowGraphImpl
+private import semmle.code.csharp.controlflow.ControlFlowGraph::ControlFlow as Cfg
+
+cached
+private module Cached {
+  private import semmle.code.csharp.Caching
+
+  cached
+  newtype TSplitKind = TConditionalCompletionSplitKind()
+
+  cached
+  newtype TSplit = TConditionalCompletionSplit(ConditionalCompletion c)
+}
+
+import Cached
+
+/**
+ * A split for a control flow element. For example, a tag that determines how to
+ * continue execution after leaving a `finally` block.
+ */
+class Split extends TSplit {
+  /** Gets a textual representation of this split. */
+  string toString() { none() }
+}
+
+module ConditionalCompletionSplitting {
+  /**
+   * A split for conditional completions. For example, in
+   *
+   * ```csharp
+   * void M(int i)
+   * {
+   *     if (x && !y)
+   *         System.Console.WriteLine("true")
+   * }
+   * ```
+   *
+   * we record whether `x`, `y`, and `!y` evaluate to `true` or `false`, and restrict
+   * the edges out of `!y` and `x && !y` accordingly.
+   */
+  class ConditionalCompletionSplit extends Split, TConditionalCompletionSplit {
+    ConditionalCompletion completion;
+
+    ConditionalCompletionSplit() { this = TConditionalCompletionSplit(completion) }
+
+    ConditionalCompletion getCompletion() { result = completion }
+
+    override string toString() { result = completion.toString() }
+  }
+
+  private class ConditionalCompletionSplitKind_ extends SplitKind, TConditionalCompletionSplitKind {
+    override int getListOrder() { result = 0 }
+
+    override predicate isEnabled(AstNode cfe) { this.appliesTo(cfe) }
+
+    override string toString() { result = "ConditionalCompletion" }
+  }
+
+  module ConditionalCompletionSplittingInput {
+    private import Completion as Comp
+
+    class ConditionalCompletion = Comp::ConditionalCompletion;
+
+    class ConditionalCompletionSplitKind extends ConditionalCompletionSplitKind_, TSplitKind { }
+
+    class ConditionalCompletionSplit = ConditionalCompletionSplitting::ConditionalCompletionSplit;
+
+    bindingset[parent, parentCompletion]
+    predicate condPropagateExpr(
+      AstNode parent, ConditionalCompletion parentCompletion, AstNode child,
+      ConditionalCompletion childCompletion
+    ) {
+      child = parent.(LogicalNotExpr).getOperand() and
+      childCompletion.getDual() = parentCompletion
+      or
+      childCompletion = parentCompletion and
+      (
+        child = parent.(LogicalAndExpr).getAnOperand()
+        or
+        child = parent.(LogicalOrExpr).getAnOperand()
+        or
+        parent = any(ConditionalExpr ce | child = [ce.getThen(), ce.getElse()])
+        or
+        child = parent.(SwitchExpr).getACase()
+        or
+        child = parent.(SwitchCaseExpr).getBody()
+        or
+        parent =
+          any(NullCoalescingOperation nce |
+            if childCompletion instanceof NullnessCompletion
+            then child = nce.getRightOperand()
+            else child = nce.getAnOperand()
+          )
+      )
+      or
+      child = parent.(NotPatternExpr).getPattern() and
+      childCompletion.getDual() = parentCompletion
+      or
+      child = parent.(IsExpr).getPattern() and
+      parentCompletion.(BooleanCompletion).getValue() =
+        childCompletion.(MatchingCompletion).getValue()
+      or
+      childCompletion = parentCompletion and
+      (
+        child = parent.(AndPatternExpr).getAnOperand()
+        or
+        child = parent.(OrPatternExpr).getAnOperand()
+        or
+        child = parent.(RecursivePatternExpr).getAChildExpr()
+        or
+        child = parent.(PropertyPatternExpr).getPattern(_)
+      )
+    }
+  }
+}

csharp/ql/lib/semmle/code/csharp/dataflow/Nullness.qll

@@ -126,7 +126,7 @@ private predicate nonNullDef(Ssa::ExplicitDefinition def) {
 /**
  * Holds if `node` is a dereference `d` of SSA definition `def`.
  */
-private predicate dereferenceAt(ControlFlowNode node, Ssa::Definition def, Dereference d) {
+private predicate dereferenceAt(ControlFlow::Node node, Ssa::Definition def, Dereference d) {
   d = def.getAReadAtNode(node)
 }
 
@@ -192,7 +192,9 @@ private predicate isNullDefaultArgument(Ssa::ImplicitParameterDefinition def, Al
 }
 
 /** Holds if `def` is an SSA definition that may be `null`. */
-private predicate defMaybeNull(Ssa::Definition def, ControlFlowNode node, string msg, Element reason) {
+private predicate defMaybeNull(
+  Ssa::Definition def, ControlFlow::Node node, string msg, Element reason
+) {
   not nonNullDef(def) and
   (
     // A variable compared to `null` might be `null`
@@ -222,7 +224,7 @@ private predicate defMaybeNull(Ssa::Definition def, ControlFlowNode node, string
     or
     // If the source of a variable is `null` then the variable may be `null`
     exists(AssignableDefinition adef | adef = def.(Ssa::ExplicitDefinition).getADefinition() |
-      adef.getSource() = maybeNullExpr(node.asExpr()) and
+      adef.getSource() = maybeNullExpr(node.getAstNode()) and
       reason = adef.getExpr() and
       msg = "because of $@ assignment"
     )
@@ -254,19 +256,19 @@ private Ssa::Definition getAnUltimateDefinition(Ssa::Definition def) {
  * through an intermediate dereference that always throws a null reference
  * exception.
  */
-private predicate defReaches(Ssa::Definition def, ControlFlowNode cfn) {
+private predicate defReaches(Ssa::Definition def, ControlFlow::Node cfn) {
   exists(def.getAFirstReadAtNode(cfn))
   or
-  exists(ControlFlowNode mid | defReaches(def, mid) |
+  exists(ControlFlow::Node mid | defReaches(def, mid) |
     SsaImpl::adjacentReadPairSameVar(_, mid, cfn) and
-    not mid = any(Dereference d | d.isAlwaysNull(def.getSourceVariable())).getControlFlowNode()
+    not mid = any(Dereference d | d.isAlwaysNull(def.getSourceVariable())).getAControlFlowNode()
   )
 }
 
 private module NullnessConfig implements ControlFlowReachability::ConfigSig {
-  predicate source(ControlFlowNode node, Ssa::Definition def) { defMaybeNull(def, node, _, _) }
+  predicate source(ControlFlow::Node node, Ssa::Definition def) { defMaybeNull(def, node, _, _) }
 
-  predicate sink(ControlFlowNode node, Ssa::Definition def) {
+  predicate sink(ControlFlow::Node node, Ssa::Definition def) {
     exists(Dereference d |
       dereferenceAt(node, def, d) and
       not d instanceof NonNullExpr
@@ -281,7 +283,9 @@ private module NullnessConfig implements ControlFlowReachability::ConfigSig {
 private module NullnessFlow = ControlFlowReachability::Flow<NullnessConfig>;
 
 predicate maybeNullDeref(Dereference d, Ssa::SourceVariable v, string msg, Element reason) {
-  exists(Ssa::Definition origin, Ssa::Definition ssa, ControlFlowNode src, ControlFlowNode sink |
+  exists(
+    Ssa::Definition origin, Ssa::Definition ssa, ControlFlow::Node src, ControlFlow::Node sink
+  |
     defMaybeNull(origin, src, msg, reason) and
     NullnessFlow::flow(src, origin, sink, ssa) and
     ssa.getSourceVariable() = v and
@@ -384,6 +388,6 @@ class Dereference extends G::DereferenceableExpr {
    */
   predicate isFirstAlwaysNull(Ssa::SourceVariable v) {
     this.isAlwaysNull(v) and
-    defReaches(v.getAnSsaDefinition(), this.getControlFlowNode())
+    defReaches(v.getAnSsaDefinition(), this.getAControlFlowNode())
   }
 }

csharp/ql/lib/semmle/code/csharp/dataflow/SSA.qll

@@ -164,8 +164,10 @@ module Ssa {
    */
   class Definition extends SsaImpl::Definition {
     /** Gets the control flow node of this SSA definition. */
-    final ControlFlowNode getControlFlowNode() {
-      exists(BasicBlock bb, int i | this.definesAt(_, bb, i) | result = bb.getNode(0.maximum(i)))
+    final ControlFlow::Node getControlFlowNode() {
+      exists(ControlFlow::BasicBlock bb, int i | this.definesAt(_, bb, i) |
+        result = bb.getNode(0.maximum(i))
+      )
     }
 
     /**
@@ -174,7 +176,9 @@ module Ssa {
      * point it is still live, without crossing another SSA definition of the
      * same source variable.
      */
-    final predicate isLiveAtEndOfBlock(BasicBlock bb) { SsaImpl::isLiveAtEndOfBlock(this, bb) }
+    final predicate isLiveAtEndOfBlock(ControlFlow::BasicBlock bb) {
+      SsaImpl::isLiveAtEndOfBlock(this, bb)
+    }
 
     /**
      * Gets a read of the source variable underlying this SSA definition that
@@ -232,7 +236,7 @@ module Ssa {
      * - The reads of `this.Field` on lines 10 and 11 can be reached from the phi
      *   node between lines 9 and 10.
      */
-    final AssignableRead getAReadAtNode(ControlFlowNode cfn) {
+    final AssignableRead getAReadAtNode(ControlFlow::Node cfn) {
       result = SsaImpl::getAReadAtNode(this, cfn)
     }
 
@@ -306,9 +310,72 @@ module Ssa {
      * Subsequent reads can be found by following the steps defined by
      * `AssignableRead.getANextRead()`.
      */
-    final AssignableRead getAFirstReadAtNode(ControlFlowNode cfn) {
+    final AssignableRead getAFirstReadAtNode(ControlFlow::Node cfn) {
       SsaImpl::firstReadSameVar(this, cfn) and
-      result.getControlFlowNode() = cfn
+      result.getAControlFlowNode() = cfn
+    }
+
+    /**
+     * Gets a last read of the source variable underlying this SSA definition.
+     * That is, a read that can reach the end of the enclosing callable, or
+     * another SSA definition for the source variable, without passing through
+     * any other read. Example:
+     *
+     * ```csharp
+     * int Field;
+     *
+     * void SetField(int i) {
+     *   this.Field = i;
+     *   Use(this.Field);
+     *   if (i > 0)
+     *     this.Field = i - 1;
+     *   else if (i < 0)
+     *     SetField(1);
+     *   Use(this.Field);
+     *   Use(this.Field);
+     * }
+     * ```
+     *
+     * - The reads of `i` on lines 7 and 8 are the last reads for the implicit
+     *   parameter definition on line 3.
+     * - The read of `this.Field` on line 5 is a last read of the definition on
+     *   line 4.
+     * - The read of `this.Field` on line 11 is a last read of the phi node
+     *   between lines 9 and 10.
+     */
+    deprecated final AssignableRead getALastRead() { result = this.getALastReadAtNode(_) }
+
+    /**
+     * Gets a last read of the source variable underlying this SSA definition at
+     * control flow node `cfn`. That is, a read that can reach the end of the
+     * enclosing callable, or another SSA definition for the source variable,
+     * without passing through any other read. Example:
+     *
+     * ```csharp
+     * int Field;
+     *
+     * void SetField(int i) {
+     *   this.Field = i;
+     *   Use(this.Field);
+     *   if (i > 0)
+     *     this.Field = i - 1;
+     *   else if (i < 0)
+     *     SetField(1);
+     *   Use(this.Field);
+     *   Use(this.Field);
+     * }
+     * ```
+     *
+     * - The reads of `i` on lines 7 and 8 are the last reads for the implicit
+     *   parameter definition on line 3.
+     * - The read of `this.Field` on line 5 is a last read of the definition on
+     *   line 4.
+     * - The read of `this.Field` on line 11 is a last read of the phi node
+     *   between lines 9 and 10.
+     */
+    deprecated final AssignableRead getALastReadAtNode(ControlFlow::Node cfn) {
+      SsaImpl::lastReadSameVar(this, cfn) and
+      result.getAControlFlowNode() = cfn
     }
 
     /**
@@ -359,9 +426,7 @@ module Ssa {
      * This is either an expression, for example `x = 0`, a parameter, or a
      * callable. Phi nodes have no associated syntax element.
      */
-    Element getElement() {
-      result.(ControlFlowElement).getControlFlowNode() = this.getControlFlowNode()
-    }
+    Element getElement() { result = this.getControlFlowNode().getAstNode() }
 
     /** Gets the callable to which this SSA definition belongs. */
     final Callable getEnclosingCallable() {
@@ -419,7 +484,7 @@ module Ssa {
      * `M2` via the call on line 6.
      */
     deprecated final predicate isCapturedVariableDefinitionFlowIn(
-      ImplicitEntryDefinition def, ControlFlowNodes::ElementNode c, boolean additionalCalls
+      ImplicitEntryDefinition def, ControlFlow::Nodes::ElementNode c, boolean additionalCalls
     ) {
       none()
     }
@@ -455,7 +520,9 @@ module Ssa {
 
     override Element getElement() { result = ad.getElement() }
 
-    override string toString() { result = "SSA def(" + this.getSourceVariable() + ")" }
+    override string toString() {
+      result = SsaImpl::getToStringPrefix(this) + "SSA def(" + this.getSourceVariable() + ")"
+    }
 
     override Location getLocation() { result = ad.getLocation() }
   }
@@ -469,7 +536,7 @@ module Ssa {
    */
   class ImplicitDefinition extends Definition, SsaImpl::WriteDefinition {
     ImplicitDefinition() {
-      exists(BasicBlock bb, SourceVariable v, int i | this.definesAt(v, bb, i) |
+      exists(ControlFlow::BasicBlock bb, SourceVariable v, int i | this.definesAt(v, bb, i) |
         SsaImpl::implicitEntryDefinition(bb, v) and
         i = -1
         or
@@ -487,21 +554,25 @@ module Ssa {
    */
   class ImplicitEntryDefinition extends ImplicitDefinition {
     ImplicitEntryDefinition() {
-      exists(BasicBlock bb, SourceVariable v |
+      exists(ControlFlow::BasicBlock bb, SourceVariable v |
         this.definesAt(v, bb, -1) and
         SsaImpl::implicitEntryDefinition(bb, v)
       )
     }
 
     /** Gets the callable that this entry definition belongs to. */
-    final Callable getCallable() { result = this.getBasicBlock().getEnclosingCallable() }
+    final Callable getCallable() { result = this.getBasicBlock().getCallable() }
 
     override Element getElement() { result = this.getCallable() }
 
     override string toString() {
       if this.getSourceVariable().getAssignable() instanceof LocalScopeVariable
-      then result = "SSA capture def(" + this.getSourceVariable() + ")"
-      else result = "SSA entry def(" + this.getSourceVariable() + ")"
+      then
+        result =
+          SsaImpl::getToStringPrefix(this) + "SSA capture def(" + this.getSourceVariable() + ")"
+      else
+        result =
+          SsaImpl::getToStringPrefix(this) + "SSA entry def(" + this.getSourceVariable() + ")"
     }
 
     override Location getLocation() { result = this.getCallable().getLocation() }
@@ -511,7 +582,7 @@ module Ssa {
     class C = ImplicitParameterDefinition;
 
     predicate relevantLocations(ImplicitParameterDefinition def, Location l1, Location l2) {
-      not def.getBasicBlock() instanceof EntryBasicBlock and
+      not def.getBasicBlock() instanceof ControlFlow::BasicBlocks::EntryBlock and
       l1 = def.getParameter().getALocation() and
       l2 = def.getBasicBlock().getLocation()
     }
@@ -543,7 +614,7 @@ module Ssa {
     override Element getElement() { result = this.getParameter() }
 
     override string toString() {
-      result = "SSA param(" + pragma[only_bind_out](this.getParameter()) + ")"
+      result = SsaImpl::getToStringPrefix(this) + "SSA param(" + this.getParameter() + ")"
     }
 
     override Location getLocation() {
@@ -563,7 +634,7 @@ module Ssa {
     private Call c;
 
     ImplicitCallDefinition() {
-      exists(BasicBlock bb, SourceVariable v, int i |
+      exists(ControlFlow::BasicBlock bb, SourceVariable v, int i |
         this.definesAt(v, bb, i) and
         SsaImpl::updatesNamedFieldOrProp(bb, i, c, v, _)
       )
@@ -585,7 +656,9 @@ module Ssa {
       )
     }
 
-    override string toString() { result = "SSA call def(" + this.getSourceVariable() + ")" }
+    override string toString() {
+      result = SsaImpl::getToStringPrefix(this) + "SSA call def(" + this.getSourceVariable() + ")"
+    }
 
     override Location getLocation() { result = this.getCall().getLocation() }
   }
@@ -598,7 +671,9 @@ module Ssa {
     private Definition q;
 
     ImplicitQualifierDefinition() {
-      exists(BasicBlock bb, int i, SourceVariables::QualifiedFieldOrPropSourceVariable v |
+      exists(
+        ControlFlow::BasicBlock bb, int i, SourceVariables::QualifiedFieldOrPropSourceVariable v
+      |
         this.definesAt(v, bb, i)
       |
         SsaImpl::variableWriteQualifier(bb, i, v, _) and
@@ -609,7 +684,10 @@ module Ssa {
     /** Gets the SSA definition for the qualifier. */
     final Definition getQualifierDefinition() { result = q }
 
-    override string toString() { result = "SSA qualifier def(" + this.getSourceVariable() + ")" }
+    override string toString() {
+      result =
+        SsaImpl::getToStringPrefix(this) + "SSA qualifier def(" + this.getSourceVariable() + ")"
+    }
 
     override Location getLocation() { result = this.getQualifierDefinition().getLocation() }
   }
@@ -645,11 +723,13 @@ module Ssa {
     final Definition getAnInput() { this.hasInputFromBlock(result, _) }
 
     /** Holds if `inp` is an input to this phi node along the edge originating in `bb`. */
-    predicate hasInputFromBlock(Definition inp, BasicBlock bb) {
+    predicate hasInputFromBlock(Definition inp, ControlFlow::BasicBlock bb) {
       inp = SsaImpl::phiHasInputFromBlock(this, bb)
     }
 
-    override string toString() { result = "SSA phi(" + this.getSourceVariable() + ")" }
+    override string toString() {
+      result = SsaImpl::getToStringPrefix(this) + "SSA phi(" + this.getSourceVariable() + ")"
+    }
 
     /*
      * The location of a phi node is the same as the location of the first node

csharp/ql/lib/semmle/code/csharp/dataflow/SignAnalysis.qll

@@ -11,32 +11,36 @@ private import semmle.code.csharp.dataflow.internal.rangeanalysis.SignAnalysisCo
 
 /** Holds if `e` can be positive and cannot be negative. */
 predicate positiveExpr(Expr e) {
-  exists(ControlFlowNode cfn | cfn = e.getControlFlowNode() |
+  forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() |
     positive(cfn) or strictlyPositive(cfn)
   )
 }
 
 /** Holds if `e` can be negative and cannot be positive. */
 predicate negativeExpr(Expr e) {
-  exists(ControlFlowNode cfn | cfn = e.getControlFlowNode() |
+  forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() |
     negative(cfn) or strictlyNegative(cfn)
   )
 }
 
 /** Holds if `e` is strictly positive. */
-predicate strictlyPositiveExpr(Expr e) { strictlyPositive(e.getControlFlowNode()) }
+predicate strictlyPositiveExpr(Expr e) {
+  forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() | strictlyPositive(cfn))
+}
 
 /** Holds if `e` is strictly negative. */
-predicate strictlyNegativeExpr(Expr e) { strictlyNegative(e.getControlFlowNode()) }
+predicate strictlyNegativeExpr(Expr e) {
+  forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() | strictlyNegative(cfn))
+}
 
 /** Holds if `e` can be positive and cannot be negative. */
-predicate positive(ControlFlowNodes::ExprNode e) { Common::positive(e) }
+predicate positive(ControlFlow::Nodes::ExprNode e) { Common::positive(e) }
 
 /** Holds if `e` can be negative and cannot be positive. */
-predicate negative(ControlFlowNodes::ExprNode e) { Common::negative(e) }
+predicate negative(ControlFlow::Nodes::ExprNode e) { Common::negative(e) }
 
 /** Holds if `e` is strictly positive. */
-predicate strictlyPositive(ControlFlowNodes::ExprNode e) { Common::strictlyPositive(e) }
+predicate strictlyPositive(ControlFlow::Nodes::ExprNode e) { Common::strictlyPositive(e) }
 
 /** Holds if `e` is strictly negative. */
-predicate strictlyNegative(ControlFlowNodes::ExprNode e) { Common::strictlyNegative(e) }
+predicate strictlyNegative(ControlFlow::Nodes::ExprNode e) { Common::strictlyNegative(e) }

csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll

@@ -5,25 +5,17 @@ import csharp
  */
 module BaseSsa {
   private import AssignableDefinitions
+  private import semmle.code.csharp.controlflow.BasicBlocks as BasicBlocks
   private import codeql.ssa.Ssa as SsaImplCommon
 
-  cached
-  private module BaseSsaStage {
-    cached
-    predicate ref() { any() }
-
-    cached
-    predicate backref() { (exists(any(SsaDefinition def).getARead()) implies any()) }
-  }
-
   /**
    * Holds if the `i`th node of basic block `bb` is assignable definition `def`,
    * targeting local scope variable `v`.
    */
   private predicate definitionAt(
-    AssignableDefinition def, BasicBlock bb, int i, SsaImplInput::SourceVariable v
+    AssignableDefinition def, ControlFlow::BasicBlock bb, int i, SsaInput::SourceVariable v
   ) {
-    bb.getNode(i) = def.getExpr().getControlFlowNode() and
+    bb.getNode(i) = def.getExpr().getAControlFlowNode() and
     v = def.getTarget() and
     // In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
     not exists(TupleAssignmentDefinition first, TupleAssignmentDefinition second | first = def |
@@ -33,9 +25,11 @@ module BaseSsa {
     )
   }
 
-  private predicate entryDef(Callable c, BasicBlock bb, SsaImplInput::SourceVariable v) {
-    exists(EntryBasicBlock entry |
-      c = entry.getEnclosingCallable() and
+  private predicate implicitEntryDef(
+    Callable c, ControlFlow::BasicBlocks::EntryBlock bb, SsaInput::SourceVariable v
+  ) {
+    exists(ControlFlow::BasicBlocks::EntryBlock entry |
+      c = entry.getCallable() and
       // In case `c` has multiple bodies, we want each body to get its own implicit
       // entry definition. In case `c` doesn't have multiple bodies, the line below
       // is simply the same as `bb = entry`, because `entry.getFirstNode().getASuccessor()`
@@ -88,59 +82,77 @@ module BaseSsa {
     }
   }
 
-  private module SsaImplInput implements SsaImplCommon::InputSig<Location, BasicBlock> {
+  private module SsaInput implements SsaImplCommon::InputSig<Location, ControlFlow::BasicBlock> {
     class SourceVariable = SimpleLocalScopeVariable;
 
-    predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
-      BaseSsaStage::ref() and
+    predicate variableWrite(ControlFlow::BasicBlock bb, int i, SourceVariable v, boolean certain) {
       exists(AssignableDefinition def |
         definitionAt(def, bb, i, v) and
         if def.isCertain() then certain = true else certain = false
       )
       or
-      entryDef(_, bb, v) and
+      implicitEntryDef(_, bb, v) and
       i = -1 and
       certain = true
     }
 
-    predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+    predicate variableRead(ControlFlow::BasicBlock bb, int i, SourceVariable v, boolean certain) {
       exists(AssignableRead read |
-        read.getControlFlowNode() = bb.getNode(i) and
+        read.getAControlFlowNode() = bb.getNode(i) and
         read.getTarget() = v and
         certain = true
       )
     }
   }
 
-  private module SsaImpl = SsaImplCommon::Make<Location, Cfg, SsaImplInput>;
+  private module SsaImpl = SsaImplCommon::Make<Location, BasicBlocks::Cfg, SsaInput>;
 
-  private module SsaInput implements SsaImpl::SsaInputSig {
-    private import csharp as CS
-
-    class Expr = CS::Expr;
-
-    class Parameter = CS::Parameter;
-
-    class VariableWrite extends AssignableDefinition {
-      Expr asExpr() { result = this.getExpr() }
-
-      Expr getValue() { result = this.getSource() }
-
-      predicate isParameterInit(Parameter p) {
-        this.(ImplicitParameterDefinition).getParameter() = p
-      }
+  class Definition extends SsaImpl::Definition {
+    final AssignableRead getARead() {
+      exists(ControlFlow::BasicBlock bb, int i |
+        SsaImpl::ssaDefReachesRead(_, this, bb, i) and
+        result.getAControlFlowNode() = bb.getNode(i)
+      )
     }
 
-    predicate explicitWrite(VariableWrite w, BasicBlock bb, int i, SsaImplInput::SourceVariable v) {
-      definitionAt(w, bb, i, v)
+    final AssignableDefinition getDefinition() {
+      exists(ControlFlow::BasicBlock bb, int i, SsaInput::SourceVariable v |
+        this.definesAt(v, bb, i) and
+        definitionAt(result, bb, i, v)
+      )
+    }
+
+    final predicate isImplicitEntryDefinition(SsaInput::SourceVariable v) {
+      exists(ControlFlow::BasicBlock bb |
+        this.definesAt(v, bb, -1) and
+        implicitEntryDef(_, bb, v)
+      )
+    }
+
+    private Definition getAPhiInputOrPriorDefinition() {
+      result = this.(PhiNode).getAnInput() or
+      SsaImpl::uncertainWriteDefinitionInput(this, result)
+    }
+
+    final Definition getAnUltimateDefinition() {
+      result = this.getAPhiInputOrPriorDefinition*() and
+      not result instanceof PhiNode
+    }
+
+    override Location getLocation() {
+      result = this.getDefinition().getLocation()
       or
-      entryDef(_, bb, v) and
-      i = -1 and
-      w.isParameterInit(v)
+      exists(Callable c, ControlFlow::BasicBlock bb, SsaInput::SourceVariable v |
+        this.definesAt(v, bb, -1) and
+        implicitEntryDef(c, bb, v) and
+        result = c.getLocation()
+      )
     }
   }
 
-  module Ssa = SsaImpl::MakeSsa<SsaInput>;
+  class PhiNode extends SsaImpl::PhiNode, Definition {
+    override Location getLocation() { result = this.getBasicBlock().getLocation() }
 
-  import Ssa
+    final Definition getAnInput() { SsaImpl::phiHasInputFromBlock(this, result, _) }
+  }
 }

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

@@ -28,8 +28,8 @@ newtype TReturnKind =
 private predicate hasMultipleSourceLocations(Callable c) { strictcount(getASourceLocation(c)) > 1 }
 
 private predicate objectInitEntry(ObjectInitMethod m, ControlFlowElement first) {
-  exists(ControlFlow::EntryNode en |
-    en.getEnclosingCallable() = m and first = en.getASuccessor().getAstNode()
+  exists(ControlFlow::Nodes::EntryNode en |
+    en.getCallable() = m and first.getControlFlowNode() = en.getASuccessor()
   )
 }
 
@@ -73,12 +73,12 @@ private module Cached {
 
   cached
   newtype TDataFlowCall =
-    TNonDelegateCall(ControlFlowNodes::ElementNode cfn, DispatchCall dc) {
+    TNonDelegateCall(ControlFlow::Nodes::ElementNode cfn, DispatchCall dc) {
       DataFlowImplCommon::forceCachingInSameStage() and
-      cfn.asExpr() = dc.getCall()
+      cfn.getAstNode() = dc.getCall()
     } or
-    TExplicitDelegateLikeCall(ControlFlowNodes::ElementNode cfn, DelegateLikeCall dc) {
-      cfn.asExpr() = dc
+    TExplicitDelegateLikeCall(ControlFlow::Nodes::ElementNode cfn, DelegateLikeCall dc) {
+      cfn.getAstNode() = dc
     } or
     TSummaryCall(FlowSummary::SummarizedCallable c, FlowSummaryImpl::Private::SummaryNode receiver) {
       FlowSummaryImpl::Private::summaryCallbackRange(c, receiver)
@@ -210,63 +210,60 @@ class DataFlowCallable extends TDataFlowCallable {
   }
 
   pragma[nomagic]
-  private BasicBlock getAMultiBodyEntryBlock() {
+  private ControlFlow::Nodes::ElementNode getAMultiBodyEntryNode(ControlFlow::BasicBlock bb, int i) {
     this.isMultiBodied() and
     exists(ControlFlowElement body, Location l |
       body = this.asCallable(l).getBody() or
       objectInitEntry(this.asCallable(l), body)
     |
       NearestLocation<NearestBodyLocationInput>::nearestLocation(body, l, _) and
-      result.getANode().isBefore(body)
+      result = body.getAControlFlowEntryNode()
+    ) and
+    bb.getNode(i) = result
+  }
+
+  pragma[nomagic]
+  private ControlFlow::Nodes::ElementNode getAMultiBodyControlFlowNodePred() {
+    result = this.getAMultiBodyEntryNode(_, _).getAPredecessor()
+    or
+    result = this.getAMultiBodyControlFlowNodePred().getAPredecessor()
+  }
+
+  pragma[nomagic]
+  private ControlFlow::Nodes::ElementNode getAMultiBodyControlFlowNodeSuccSameBasicBlock() {
+    exists(ControlFlow::BasicBlock bb, int i, int j |
+      exists(this.getAMultiBodyEntryNode(bb, i)) and
+      result = bb.getNode(j) and
+      j > i
     )
   }
 
   pragma[nomagic]
-  private BasicBlock getAMultiBodyControlFlowPred() {
-    result = this.getAMultiBodyEntryBlock().getAPredecessor()
-    or
-    result = this.getAMultiBodyControlFlowPred().getAPredecessor()
-  }
-
-  pragma[nomagic]
-  private BasicBlock getAMultiBodyBasicBlockSucc() {
-    result = this.getAMultiBodyEntryBlock().getASuccessor()
+  private ControlFlow::BasicBlock getAMultiBodyBasicBlockSucc() {
+    result = this.getAMultiBodyEntryNode(_, _).getBasicBlock().getASuccessor()
     or
     result = this.getAMultiBodyBasicBlockSucc().getASuccessor()
   }
 
-  pragma[nomagic]
-  private BasicBlock getAMultiBodyBasicBlock() {
+  pragma[inline]
+  private ControlFlow::Nodes::ElementNode getAMultiBodyControlFlowNode() {
     result =
       [
-        this.getAMultiBodyEntryBlock(), this.getAMultiBodyControlFlowPred(),
-        this.getAMultiBodyBasicBlockSucc()
+        this.getAMultiBodyEntryNode(_, _), this.getAMultiBodyControlFlowNodePred(),
+        this.getAMultiBodyControlFlowNodeSuccSameBasicBlock(),
+        this.getAMultiBodyBasicBlockSucc().getANode()
       ]
   }
 
-  pragma[inline]
-  private ControlFlowNode getAMultiBodyControlFlowNode() {
-    result = this.getAMultiBodyBasicBlock().getANode()
-  }
-
   /** Gets a control flow node belonging to this callable. */
   pragma[inline]
-  ControlFlowNode getAControlFlowNode() {
+  ControlFlow::Node getAControlFlowNode() {
     result = this.getAMultiBodyControlFlowNode()
     or
     not this.isMultiBodied() and
     result.getEnclosingCallable() = this.asCallable(_)
   }
 
-  /** Gets a basic block belonging to this callable. */
-  pragma[inline]
-  BasicBlock getABasicBlock() {
-    result = this.getAMultiBodyBasicBlock()
-    or
-    not this.isMultiBodied() and
-    result.getEnclosingCallable() = this.asCallable(_)
-  }
-
   /** Gets the underlying summarized callable, if any. */
   FlowSummary::SummarizedCallable asSummarizedCallable() { this = TSummarizedCallable(result) }
 
@@ -310,7 +307,7 @@ abstract class DataFlowCall extends TDataFlowCall {
   abstract DataFlowCallable getARuntimeTarget();
 
   /** Gets the control flow node where this call happens, if any. */
-  abstract ControlFlowNodes::ElementNode getControlFlowNode();
+  abstract ControlFlow::Nodes::ElementNode getControlFlowNode();
 
   /** Gets the data flow node corresponding to this call, if any. */
   abstract DataFlow::Node getNode();
@@ -366,7 +363,7 @@ private predicate folderDist(Folder f1, Folder f2, int i) =
 
 /** A non-delegate C# call relevant for data flow. */
 class NonDelegateDataFlowCall extends DataFlowCall, TNonDelegateCall {
-  private ControlFlowNodes::ElementNode cfn;
+  private ControlFlow::Nodes::ElementNode cfn;
   private DispatchCall dc;
 
   NonDelegateDataFlowCall() { this = TNonDelegateCall(cfn, dc) }
@@ -439,7 +436,7 @@ class NonDelegateDataFlowCall extends DataFlowCall, TNonDelegateCall {
     not dc.isReflection()
   }
 
-  override ControlFlowNodes::ElementNode getControlFlowNode() { result = cfn }
+  override ControlFlow::Nodes::ElementNode getControlFlowNode() { result = cfn }
 
   override DataFlow::ExprNode getNode() { result.getControlFlowNode() = cfn }
 
@@ -455,7 +452,7 @@ abstract class DelegateDataFlowCall extends DataFlowCall { }
 
 /** An explicit delegate or function pointer call relevant for data flow. */
 class ExplicitDelegateLikeDataFlowCall extends DelegateDataFlowCall, TExplicitDelegateLikeCall {
-  private ControlFlowNodes::ElementNode cfn;
+  private ControlFlow::Nodes::ElementNode cfn;
   private DelegateLikeCall dc;
 
   ExplicitDelegateLikeDataFlowCall() { this = TExplicitDelegateLikeCall(cfn, dc) }
@@ -467,7 +464,7 @@ class ExplicitDelegateLikeDataFlowCall extends DelegateDataFlowCall, TExplicitDe
     none() // handled by the shared library
   }
 
-  override ControlFlowNodes::ElementNode getControlFlowNode() { result = cfn }
+  override ControlFlow::Nodes::ElementNode getControlFlowNode() { result = cfn }
 
   override DataFlow::ExprNode getNode() { result.getControlFlowNode() = cfn }
 
@@ -498,7 +495,7 @@ class SummaryCall extends DelegateDataFlowCall, TSummaryCall {
     none() // handled by the shared library
   }
 
-  override ControlFlowNodes::ElementNode getControlFlowNode() { none() }
+  override ControlFlow::Nodes::ElementNode getControlFlowNode() { none() }
 
   override DataFlow::Node getNode() { none() }
 

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

@@ -41,13 +41,13 @@ predicate isArgumentNode(ArgumentNode arg, DataFlowCall c, ArgumentPosition pos)
  * Gets a control flow node used for data flow purposes for the primary constructor
  * parameter access `pa`.
  */
-private ControlFlowNode getAPrimaryConstructorParameterCfn(ParameterAccess pa) {
+private ControlFlow::Node getAPrimaryConstructorParameterCfn(ParameterAccess pa) {
   pa.getTarget().getCallable() instanceof PrimaryConstructor and
   (
-    result = pa.(ParameterRead).getControlFlowNode()
+    result = pa.(ParameterRead).getAControlFlowNode()
     or
     pa =
-      any(AssignableDefinition def | result = def.getExpr().getControlFlowNode()).getTargetAccess()
+      any(AssignableDefinition def | result = def.getExpr().getAControlFlowNode()).getTargetAccess()
   )
 }
 
@@ -72,7 +72,7 @@ abstract class NodeImpl extends Node {
 
   /** Do not call: use `getControlFlowNode()` instead. */
   cached
-  abstract ControlFlowNode getControlFlowNodeImpl();
+  abstract ControlFlow::Node getControlFlowNodeImpl();
 
   /** Do not call: use `getLocation()` instead. */
   cached
@@ -83,9 +83,22 @@ abstract class NodeImpl extends Node {
   abstract string toStringImpl();
 }
 
+// TODO: Remove once static initializers are folded into the
+// static constructors
+private DataFlowCallable getEnclosingStaticFieldOrProperty(Expr e) {
+  result.asFieldOrProperty() =
+    any(FieldOrProperty f |
+      f.isStatic() and
+      e = f.getAChild+() and
+      not exists(e.getEnclosingCallable())
+    )
+}
+
 private class ExprNodeImpl extends ExprNode, NodeImpl {
   override DataFlowCallable getEnclosingCallableImpl() {
     result.getAControlFlowNode() = this.getControlFlowNodeImpl()
+    or
+    result = getEnclosingStaticFieldOrProperty(this.asExpr())
   }
 
   override Type getTypeImpl() {
@@ -93,7 +106,7 @@ private class ExprNodeImpl extends ExprNode, NodeImpl {
     result = this.getExpr().getType()
   }
 
-  override ControlFlowNodes::ElementNode getControlFlowNodeImpl() {
+  override ControlFlow::Nodes::ElementNode getControlFlowNodeImpl() {
     forceCachingInSameStage() and this = TExprNode(result)
   }
 
@@ -114,13 +127,13 @@ private class ExprNodeImpl extends ExprNode, NodeImpl {
  * as if they were lambdas.
  */
 abstract private class LocalFunctionCreationNode extends NodeImpl, TLocalFunctionCreationNode {
-  ControlFlowNodes::ElementNode cfn;
+  ControlFlow::Nodes::ElementNode cfn;
   LocalFunction function;
   boolean isPostUpdate;
 
   LocalFunctionCreationNode() {
     this = TLocalFunctionCreationNode(cfn, isPostUpdate) and
-    function = cfn.asStmt().(LocalFunctionStmt).getLocalFunction()
+    function = cfn.getAstNode().(LocalFunctionStmt).getLocalFunction()
   }
 
   LocalFunction getFunction() { result = function }
@@ -138,9 +151,9 @@ abstract private class LocalFunctionCreationNode extends NodeImpl, TLocalFunctio
 
   override DataFlowType getDataFlowType() { result.asDelegate() = function }
 
-  override ControlFlowNodes::ElementNode getControlFlowNodeImpl() { none() }
+  override ControlFlow::Nodes::ElementNode getControlFlowNodeImpl() { none() }
 
-  ControlFlowNodes::ElementNode getUnderlyingControlFlowNode() { result = cfn }
+  ControlFlow::Nodes::ElementNode getUnderlyingControlFlowNode() { result = cfn }
 
   override Location getLocationImpl() { result = cfn.getLocation() }
 }
@@ -153,11 +166,13 @@ private class LocalFunctionCreationPreNode extends LocalFunctionCreationNode {
 
 /** Calculation of the relative order in which `this` references are read. */
 private module ThisFlow {
+  private class BasicBlock = ControlFlow::BasicBlock;
+
   /** Holds if `e` is a `this` access. */
   predicate thisAccessExpr(Expr e) { e instanceof ThisAccess or e instanceof BaseAccess }
 
   /** Holds if `n` is a `this` access at control flow node `cfn`. */
-  private predicate thisAccess(Node n, ControlFlowNode cfn) {
+  private predicate thisAccess(Node n, ControlFlow::Node cfn) {
     thisAccessExpr(n.asExprAtNode(cfn))
     or
     cfn = n.(InstanceParameterAccessPreNode).getUnderlyingControlFlowNode()
@@ -166,7 +181,7 @@ private module ThisFlow {
   private predicate primaryConstructorThisAccess(Node n, BasicBlock bb, int ppos) {
     exists(Parameter p |
       n.(PrimaryConstructorThisAccessPreNode).getParameter() = p and
-      bb.getEnclosingCallable() = p.getCallable() and
+      bb.getCallable() = p.getCallable() and
       ppos = p.getPosition()
     )
   }
@@ -183,9 +198,9 @@ private module ThisFlow {
       i = ppos - numberOfPrimaryConstructorParameters(bb)
     )
     or
-    exists(DataFlowCallable c, EntryBasicBlock entry |
+    exists(DataFlowCallable c, ControlFlow::BasicBlocks::EntryBlock entry |
       n.(InstanceParameterNode).isParameterOf(c, _) and
-      exists(ControlFlowNode succ |
+      exists(ControlFlow::Node succ |
         succ = c.getAControlFlowNode() and
         succ = entry.getFirstNode().getASuccessor() and
         // In case `c` has multiple bodies, we want each body to gets its own implicit
@@ -246,8 +261,9 @@ private module ThisFlow {
 /** Provides logic related to captured variables. */
 module VariableCapture {
   private import codeql.dataflow.VariableCapture as Shared
+  private import semmle.code.csharp.controlflow.BasicBlocks as BasicBlocks
 
-  private predicate closureFlowStep(ControlFlowNodes::ExprNode e1, ControlFlowNodes::ExprNode e2) {
+  private predicate closureFlowStep(ControlFlow::Nodes::ExprNode e1, ControlFlow::Nodes::ExprNode e2) {
     e1.getExpr() = LocalFlow::getALastEvalNode(e2.getExpr())
     or
     exists(Ssa::Definition def, AssignableDefinition adef |
@@ -257,19 +273,21 @@ module VariableCapture {
     )
   }
 
-  private module CaptureInput implements Shared::InputSig<Location, BasicBlock> {
+  private module CaptureInput implements Shared::InputSig<Location, BasicBlocks::BasicBlock> {
     private import csharp as CS
     private import semmle.code.csharp.controlflow.ControlFlowGraph as Cfg
     private import TaintTrackingPrivate as TaintTrackingPrivate
 
-    Callable basicBlockGetEnclosingCallable(BasicBlock bb) { result = bb.getEnclosingCallable() }
+    Callable basicBlockGetEnclosingCallable(BasicBlocks::BasicBlock bb) {
+      result = bb.getCallable()
+    }
 
-    private predicate thisAccess(ControlFlowNode cfn, InstanceCallable c) {
-      ThisFlow::thisAccessExpr(cfn.asExpr()) and
+    private predicate thisAccess(ControlFlow::Node cfn, InstanceCallable c) {
+      ThisFlow::thisAccessExpr(cfn.getAstNode()) and
       cfn.getEnclosingCallable().getEnclosingCallable*() = c
     }
 
-    private predicate capturedThisAccess(ControlFlowNode cfn, InstanceCallable c) {
+    private predicate capturedThisAccess(ControlFlow::Node cfn, InstanceCallable c) {
       thisAccess(cfn, c) and
       cfn.getEnclosingCallable() != c
     }
@@ -329,8 +347,8 @@ module VariableCapture {
       }
     }
 
-    class Expr extends ControlFlowNode {
-      predicate hasCfgNode(BasicBlock bb, int i) { this = bb.getNode(i) }
+    class Expr extends ControlFlow::Node {
+      predicate hasCfgNode(BasicBlocks::BasicBlock bb, int i) { this = bb.getNode(i) }
     }
 
     class VariableWrite extends Expr {
@@ -339,10 +357,10 @@ module VariableCapture {
 
       VariableWrite() {
         def.getTarget() = v.asLocalScopeVariable() and
-        this = def.getExpr().getControlFlowNode()
+        this = def.getExpr().getAControlFlowNode()
       }
 
-      ControlFlowNode getRhs() { LocalFlow::defAssigns(def, this, _, result) }
+      ControlFlow::Node getRhs() { LocalFlow::defAssigns(def, this, _, result) }
 
       CapturedVariable getVariable() { result = v }
     }
@@ -351,7 +369,7 @@ module VariableCapture {
       CapturedVariable v;
 
       VariableRead() {
-        this.asExpr().(AssignableRead).getTarget() = v.asLocalScopeVariable()
+        this.getAstNode().(AssignableRead).getTarget() = v.asLocalScopeVariable()
         or
         thisAccess(this, v.asThis())
       }
@@ -362,16 +380,14 @@ module VariableCapture {
     class ClosureExpr extends Expr {
       Callable c;
 
-      ClosureExpr() {
-        lambdaCreationExpr(any(ControlFlowElement e | e.getControlFlowNode() = this), c)
-      }
+      ClosureExpr() { lambdaCreationExpr(this.getAstNode(), c) }
 
       predicate hasBody(Callable body) { body = c }
 
       predicate hasAliasedAccess(Expr f) {
         closureFlowStep+(this, f) and not closureFlowStep(f, _)
         or
-        isLocalFunctionCallReceiver(_, f.asExpr(), c)
+        isLocalFunctionCallReceiver(_, f.getAstNode(), c)
       }
     }
 
@@ -384,7 +400,7 @@ module VariableCapture {
 
   class ClosureExpr = CaptureInput::ClosureExpr;
 
-  module Flow = Shared::Flow<Location, Cfg, CaptureInput>;
+  module Flow = Shared::Flow<Location, BasicBlocks::Cfg, CaptureInput>;
 
   private Flow::ClosureNode asClosureNode(Node n) {
     result = n.(CaptureNode).getSynthesizedCaptureNode()
@@ -548,15 +564,15 @@ module LocalFlow {
   }
 
   predicate defAssigns(
-    AssignableDefinition def, ControlFlowNode cfnDef, Expr value, ControlFlowNode valueCfn
+    AssignableDefinition def, ControlFlow::Node cfnDef, Expr value, ControlFlow::Node valueCfn
   ) {
     def.getSource() = value and
     valueCfn = value.getControlFlowNode() and
-    cfnDef = def.getExpr().getControlFlowNode()
+    cfnDef = def.getExpr().getAControlFlowNode()
   }
 
   private predicate defAssigns(ExprNode value, AssignableDefinitionNode defNode) {
-    exists(ControlFlowNode cfn, AssignableDefinition def, ControlFlowNode cfnDef |
+    exists(ControlFlow::Node cfn, AssignableDefinition def, ControlFlow::Node cfnDef |
       defAssigns(def, cfnDef, value.getExpr(), _) and
       cfn = value.getControlFlowNode() and
       defNode = TAssignableDefinitionNode(def, cfnDef)
@@ -580,7 +596,7 @@ module LocalFlow {
     or
     ThisFlow::adjacentThisRefs(nodeFrom.(PostUpdateNode).getPreUpdateNode(), nodeTo)
     or
-    exists(AssignableDefinition def, ControlFlowNode cfn, Ssa::ExplicitDefinition ssaDef |
+    exists(AssignableDefinition def, ControlFlow::Node cfn, Ssa::ExplicitDefinition ssaDef |
       ssaDef.getADefinition() = def and
       ssaDef.getControlFlowNode() = cfn and
       nodeFrom = TAssignableDefinitionNode(def, cfn) and
@@ -748,7 +764,6 @@ private class Argument extends Expr {
  *
  * `postUpdate` indicates whether the store targets a post-update node.
  */
-pragma[nomagic]
 private predicate fieldOrPropertyStore(ContentSet c, Expr src, Expr q, boolean postUpdate) {
   exists(FieldOrProperty f |
     c = f.getContentSet() and
@@ -796,9 +811,9 @@ private predicate fieldOrPropertyStore(ContentSet c, Expr src, Expr q, boolean p
     // Tuple element, `(..., src, ...)` `f` is `ItemX` of tuple `q`
     exists(TupleExpr te, int i |
       te = q and
-      src = te.getArgument(pragma[only_bind_into](i)) and
+      src = te.getArgument(i) and
       te.isConstruction() and
-      f = q.getType().(TupleType).getElement(pragma[only_bind_into](i)) and
+      f = q.getType().(TupleType).getElement(i) and
       postUpdate = false
     )
   )
@@ -1009,10 +1024,10 @@ private module Cached {
 
   cached
   newtype TNode =
-    TExprNode(ControlFlowNodes::ElementNode cfn) { exists(cfn.asExpr()) } or
+    TExprNode(ControlFlow::Nodes::ElementNode cfn) { cfn.getAstNode() instanceof Expr } or
     TSsaNode(SsaImpl::DataFlowIntegration::SsaNode node) or
-    TAssignableDefinitionNode(AssignableDefinition def, ControlFlowNode cfn) {
-      cfn = def.getExpr().getControlFlowNode()
+    TAssignableDefinitionNode(AssignableDefinition def, ControlFlow::Node cfn) {
+      cfn = def.getExpr().getAControlFlowNode()
     } or
     TExplicitParameterNode(Parameter p, DataFlowCallable c) {
       p = c.asCallable(_).(CallableUsedInSource).getAParameter()
@@ -1023,20 +1038,20 @@ private module Cached {
       l = c.getARelevantLocation()
     } or
     TDelegateSelfReferenceNode(Callable c) { lambdaCreationExpr(_, c) } or
-    TLocalFunctionCreationNode(ControlFlowNodes::ElementNode cfn, Boolean isPostUpdate) {
-      cfn.asStmt() instanceof LocalFunctionStmt
+    TLocalFunctionCreationNode(ControlFlow::Nodes::ElementNode cfn, Boolean isPostUpdate) {
+      cfn.getAstNode() instanceof LocalFunctionStmt
     } or
-    TYieldReturnNode(ControlFlowNodes::ElementNode cfn) {
-      any(Callable c).canYieldReturn(cfn.asExpr())
+    TYieldReturnNode(ControlFlow::Nodes::ElementNode cfn) {
+      any(Callable c).canYieldReturn(cfn.getAstNode())
     } or
-    TAsyncReturnNode(ControlFlowNodes::ElementNode cfn) {
-      any(Callable c | c.(Modifiable).isAsync()).canReturn(cfn.asExpr())
+    TAsyncReturnNode(ControlFlow::Nodes::ElementNode cfn) {
+      any(Callable c | c.(Modifiable).isAsync()).canReturn(cfn.getAstNode())
     } or
-    TMallocNode(ControlFlowNodes::ElementNode cfn) { cfn.asExpr() instanceof ObjectCreation } or
-    TObjectInitializerNode(ControlFlowNodes::ElementNode cfn) {
-      cfn.asExpr().(ObjectCreation).hasInitializer()
+    TMallocNode(ControlFlow::Nodes::ElementNode cfn) { cfn.getAstNode() instanceof ObjectCreation } or
+    TObjectInitializerNode(ControlFlow::Nodes::ElementNode cfn) {
+      cfn.getAstNode().(ObjectCreation).hasInitializer()
     } or
-    TExprPostUpdateNode(ControlFlowNodes::ExprNode cfn) {
+    TExprPostUpdateNode(ControlFlow::Nodes::ExprNode cfn) {
       (
         cfn.getExpr() instanceof Argument
         or
@@ -1055,7 +1070,7 @@ private module Cached {
         // needed for reverse stores; e.g. `x.f1.f2 = y` induces
         // a store step of `f1` into `x`
         exists(TExprPostUpdateNode upd, Expr read |
-          upd = TExprPostUpdateNode(read.getControlFlowNode())
+          upd = TExprPostUpdateNode(read.getAControlFlowNode())
         |
           fieldOrPropertyRead(e, _, read)
           or
@@ -1070,12 +1085,12 @@ private module Cached {
     TFlowSummaryNode(FlowSummaryImpl::Private::SummaryNode sn) {
       sn.getSummarizedCallable() instanceof CallableUsedInSource
     } or
-    TParamsArgumentNode(ControlFlowNode callCfn) {
-      callCfn = any(Call c | isParamsArg(c, _, _)).getControlFlowNode()
+    TParamsArgumentNode(ControlFlow::Node callCfn) {
+      callCfn = any(Call c | isParamsArg(c, _, _)).getAControlFlowNode()
     } or
     TFlowInsensitiveFieldNode(FieldOrPropertyUsedInSource f) { f.isFieldLike() } or
     TFlowInsensitiveCapturedVariableNode(LocalScopeVariable v) { v.isCaptured() } or
-    TInstanceParameterAccessNode(ControlFlowNode cfn, Boolean isPostUpdate) {
+    TInstanceParameterAccessNode(ControlFlow::Node cfn, Boolean isPostUpdate) {
       cfn = getAPrimaryConstructorParameterCfn(_)
     } or
     TPrimaryConstructorThisAccessNode(Parameter p, Boolean isPostUpdate, DataFlowCallable c) {
@@ -1213,12 +1228,12 @@ class SsaNode extends NodeImpl, TSsaNode {
   SsaNode() { this = TSsaNode(node) }
 
   override DataFlowCallable getEnclosingCallableImpl() {
-    result.getABasicBlock() = node.getBasicBlock()
+    result.getAControlFlowNode().getBasicBlock() = node.getBasicBlock()
   }
 
   override Type getTypeImpl() { result = node.getSourceVariable().getType() }
 
-  override ControlFlowNode getControlFlowNodeImpl() { none() }
+  override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
   override Location getLocationImpl() { result = node.getLocation() }
 
@@ -1231,7 +1246,7 @@ class SsaDefinitionNode extends SsaNode {
 
   Ssa::Definition getDefinition() { result = node.getDefinition() }
 
-  override ControlFlowNode getControlFlowNodeImpl() {
+  override ControlFlow::Node getControlFlowNodeImpl() {
     result = this.getDefinition().getControlFlowNode()
   }
 }
@@ -1239,7 +1254,7 @@ class SsaDefinitionNode extends SsaNode {
 /** A definition, viewed as a node in a data flow graph. */
 class AssignableDefinitionNodeImpl extends NodeImpl, TAssignableDefinitionNode {
   private AssignableDefinition def;
-  private ControlFlowNode cfn_;
+  private ControlFlow::Node cfn_;
 
   AssignableDefinitionNodeImpl() { this = TAssignableDefinitionNode(def, cfn_) }
 
@@ -1247,7 +1262,7 @@ class AssignableDefinitionNodeImpl extends NodeImpl, TAssignableDefinitionNode {
   AssignableDefinition getDefinition() { result = def }
 
   /** Gets the underlying definition, at control flow node `cfn`, if any. */
-  AssignableDefinition getDefinitionAtNode(ControlFlowNode cfn) {
+  AssignableDefinition getDefinitionAtNode(ControlFlow::Node cfn) {
     result = def and
     cfn = cfn_
   }
@@ -1256,7 +1271,7 @@ class AssignableDefinitionNodeImpl extends NodeImpl, TAssignableDefinitionNode {
 
   override Type getTypeImpl() { result = def.getTarget().getType() }
 
-  override ControlFlowNode getControlFlowNodeImpl() { result = cfn_ }
+  override ControlFlow::Node getControlFlowNodeImpl() { result = cfn_ }
 
   override Location getLocationImpl() {
     result = def.getTargetAccess().getLocation()
@@ -1359,7 +1374,7 @@ private module ParameterNodes {
 
     override Type getTypeImpl() { result = parameter.getType() }
 
-    override ControlFlowNode getControlFlowNodeImpl() { none() }
+    override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
     override Location getLocationImpl() { result = this.getParameterLocation(_) }
 
@@ -1384,7 +1399,7 @@ private module ParameterNodes {
 
     override Type getTypeImpl() { result = callable.getDeclaringType() }
 
-    override ControlFlowNode getControlFlowNodeImpl() { none() }
+    override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
     override Location getLocationImpl() { result = location }
 
@@ -1409,7 +1424,7 @@ private module ParameterNodes {
       callable = c.asCallable(_) and pos.isDelegateSelf()
     }
 
-    override ControlFlowNode getControlFlowNodeImpl() { none() }
+    override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
     override DataFlowCallable getEnclosingCallableImpl() { result.asCallable(_) = callable }
 
@@ -1493,7 +1508,7 @@ private module ArgumentNodes {
    * the constructor has run.
    */
   class MallocNode extends ArgumentNodeImpl, NodeImpl, TMallocNode {
-    private ControlFlowNodes::ElementNode cfn;
+    private ControlFlow::Nodes::ElementNode cfn;
 
     MallocNode() { this = TMallocNode(cfn) }
 
@@ -1502,11 +1517,15 @@ private module ArgumentNodes {
       pos.isQualifier()
     }
 
-    override ControlFlowNode getControlFlowNodeImpl() { result = cfn }
+    override ControlFlow::Node getControlFlowNodeImpl() { result = cfn }
 
-    override DataFlowCallable getEnclosingCallableImpl() { result.getAControlFlowNode() = cfn }
+    override DataFlowCallable getEnclosingCallableImpl() {
+      result.getAControlFlowNode() = cfn
+      or
+      result = getEnclosingStaticFieldOrProperty(cfn.getAstNode())
+    }
 
-    override Type getTypeImpl() { result = cfn.asExpr().getType() }
+    override Type getTypeImpl() { result = cfn.getAstNode().(Expr).getType() }
 
     override Location getLocationImpl() { result = cfn.getLocation() }
 
@@ -1528,12 +1547,12 @@ private module ArgumentNodes {
    * `Foo(new[] { "a", "b", "c" })`.
    */
   class ParamsArgumentNode extends ArgumentNodeImpl, NodeImpl, TParamsArgumentNode {
-    private ControlFlowNode callCfn;
+    private ControlFlow::Node callCfn;
 
     ParamsArgumentNode() { this = TParamsArgumentNode(callCfn) }
 
     private Parameter getParameter() {
-      callCfn = any(Call c | isParamsArg(c, _, result)).getControlFlowNode()
+      callCfn = any(Call c | isParamsArg(c, _, result)).getAControlFlowNode()
     }
 
     override predicate argumentOf(DataFlowCall call, ArgumentPosition pos) {
@@ -1541,11 +1560,15 @@ private module ArgumentNodes {
       pos.getPosition() = this.getParameter().getPosition()
     }
 
-    override DataFlowCallable getEnclosingCallableImpl() { result.getAControlFlowNode() = callCfn }
+    override DataFlowCallable getEnclosingCallableImpl() {
+      result.getAControlFlowNode() = callCfn
+      or
+      result = getEnclosingStaticFieldOrProperty(callCfn.getAstNode())
+    }
 
     override Type getTypeImpl() { result = this.getParameter().getType() }
 
-    override ControlFlowNode getControlFlowNodeImpl() { none() }
+    override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
     override Location getLocationImpl() { result = callCfn.getLocation() }
 
@@ -1616,10 +1639,10 @@ private module ReturnNodes {
    * to `yield return e [e]`.
    */
   class YieldReturnNode extends ReturnNode, NodeImpl, TYieldReturnNode {
-    private ControlFlowNodes::ElementNode cfn;
+    private ControlFlow::Nodes::ElementNode cfn;
     private YieldReturnStmt yrs;
 
-    YieldReturnNode() { this = TYieldReturnNode(cfn) and yrs.getExpr().getControlFlowNode() = cfn }
+    YieldReturnNode() { this = TYieldReturnNode(cfn) and yrs.getExpr().getAControlFlowNode() = cfn }
 
     YieldReturnStmt getYieldReturnStmt() { result = yrs }
 
@@ -1629,7 +1652,7 @@ private module ReturnNodes {
 
     override Type getTypeImpl() { result = yrs.getEnclosingCallable().getReturnType() }
 
-    override ControlFlowNode getControlFlowNodeImpl() { result = cfn }
+    override ControlFlow::Node getControlFlowNodeImpl() { result = cfn }
 
     override Location getLocationImpl() { result = yrs.getLocation() }
 
@@ -1640,10 +1663,10 @@ private module ReturnNodes {
    * A synthesized `return` node for returned expressions inside `async` methods.
    */
   class AsyncReturnNode extends ReturnNode, NodeImpl, TAsyncReturnNode {
-    private ControlFlowNodes::ElementNode cfn;
+    private ControlFlow::Nodes::ElementNode cfn;
     private Expr expr;
 
-    AsyncReturnNode() { this = TAsyncReturnNode(cfn) and expr = cfn.asExpr() }
+    AsyncReturnNode() { this = TAsyncReturnNode(cfn) and expr = cfn.getAstNode() }
 
     Expr getExpr() { result = expr }
 
@@ -1653,7 +1676,7 @@ private module ReturnNodes {
 
     override Type getTypeImpl() { result = expr.getEnclosingCallable().getReturnType() }
 
-    override ControlFlowNode getControlFlowNodeImpl() { result = cfn }
+    override ControlFlow::Node getControlFlowNodeImpl() { result = cfn }
 
     override Location getLocationImpl() { result = expr.getLocation() }
 
@@ -1705,7 +1728,7 @@ private module OutNodes {
   private import semmle.code.csharp.frameworks.system.Collections
   private import semmle.code.csharp.frameworks.system.collections.Generic
 
-  private DataFlowCall csharpCall(Expr e, ControlFlowNode cfn) {
+  private DataFlowCall csharpCall(Expr e, ControlFlow::Node cfn) {
     e = any(DispatchCall dc | result = TNonDelegateCall(cfn, dc)).getCall() or
     result = TExplicitDelegateLikeCall(cfn, e)
   }
@@ -1735,7 +1758,7 @@ private module OutNodes {
    */
   class ParamOutNode extends OutNode, AssignableDefinitionNode {
     private AssignableDefinitions::OutRefDefinition outRefDef;
-    private ControlFlowNode cfn;
+    private ControlFlow::Node cfn;
 
     ParamOutNode() { outRefDef = this.getDefinitionAtNode(cfn) }
 
@@ -1780,7 +1803,7 @@ class FlowSummaryNode extends NodeImpl, TFlowSummaryNode {
 
   override Type getTypeImpl() { none() }
 
-  override ControlFlowNode getControlFlowNodeImpl() { none() }
+  override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
   override Location getLocationImpl() { result = this.getSummarizedCallable().getLocation() }
 
@@ -1804,7 +1827,7 @@ class FlowSummaryNode extends NodeImpl, TFlowSummaryNode {
  * all of which are represented by an `InstanceParameterAccessNode` node.
  */
 abstract private class InstanceParameterAccessNode extends NodeImpl, TInstanceParameterAccessNode {
-  ControlFlowNode cfn;
+  ControlFlow::Node cfn;
   boolean isPostUpdate;
   Parameter p;
 
@@ -1817,14 +1840,14 @@ abstract private class InstanceParameterAccessNode extends NodeImpl, TInstancePa
 
   override Type getTypeImpl() { result = cfn.getEnclosingCallable().getDeclaringType() }
 
-  override ControlFlowNodes::ElementNode getControlFlowNodeImpl() { none() }
+  override ControlFlow::Nodes::ElementNode getControlFlowNodeImpl() { none() }
 
   override Location getLocationImpl() { result = cfn.getLocation() }
 
   /**
    * Gets the underlying control flow node.
    */
-  ControlFlowNode getUnderlyingControlFlowNode() { result = cfn }
+  ControlFlow::Node getUnderlyingControlFlowNode() { result = cfn }
 
   /**
    * Gets the primary constructor parameter that this is a this access to.
@@ -1866,7 +1889,7 @@ abstract private class PrimaryConstructorThisAccessNode extends NodeImpl,
 
   override Type getTypeImpl() { result = p.getCallable().getDeclaringType() }
 
-  override ControlFlowNodes::ElementNode getControlFlowNodeImpl() { none() }
+  override ControlFlow::Nodes::ElementNode getControlFlowNodeImpl() { none() }
 
   override Location getLocationImpl() {
     NearestLocation<NearestLocationInputParamAfterCallable>::nearestLocation(p,
@@ -1904,7 +1927,7 @@ class CaptureNode extends NodeImpl, TCaptureNode {
   VariableCapture::Flow::SynthesizedCaptureNode getSynthesizedCaptureNode() { result = cn }
 
   override DataFlowCallable getEnclosingCallableImpl() {
-    result.getABasicBlock() = cn.getBasicBlock()
+    result.getAControlFlowNode().getBasicBlock() = cn.getBasicBlock()
   }
 
   override Type getTypeImpl() {
@@ -1917,7 +1940,7 @@ class CaptureNode extends NodeImpl, TCaptureNode {
     else result = super.getDataFlowType()
   }
 
-  override ControlFlowNode getControlFlowNodeImpl() { none() }
+  override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
   override Location getLocationImpl() { result = cn.getLocation() }
 
@@ -2028,7 +2051,7 @@ class FlowInsensitiveFieldNode extends NodeImpl, TFlowInsensitiveFieldNode {
 
   override Type getTypeImpl() { result = f.getType() }
 
-  override ControlFlowNode getControlFlowNodeImpl() { none() }
+  override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
   override Location getLocationImpl() { result = f.getLocation() }
 
@@ -2052,7 +2075,7 @@ class FlowInsensitiveCapturedVariableNode extends NodeImpl, TFlowInsensitiveCapt
 
   override Type getTypeImpl() { result = v.getType() }
 
-  override ControlFlowNode getControlFlowNodeImpl() { none() }
+  override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
   override Location getLocationImpl() { result = v.getLocation() }
 
@@ -2095,7 +2118,7 @@ private ContentSet getResultContent() {
 private predicate primaryConstructorParameterStore(
   AssignableDefinitionNode node1, PrimaryConstructorParameterContent c, Node node2
 ) {
-  exists(AssignableDefinition def, ControlFlowNode cfn, Parameter p |
+  exists(AssignableDefinition def, ControlFlow::Node cfn, Parameter p |
     node1 = TAssignableDefinitionNode(def, cfn) and
     p = def.getTarget() and
     node2 = TInstanceParameterAccessNode(cfn, true) and
@@ -2338,7 +2361,7 @@ predicate expectsContent(Node n, ContentSet c) {
   n.asExpr() instanceof SpreadElementExpr and c.isElement()
 }
 
-class NodeRegion instanceof BasicBlock {
+class NodeRegion instanceof ControlFlow::BasicBlock {
   string toString() { result = "NodeRegion" }
 
   predicate contains(Node n) { this = n.getControlFlowNode().getBasicBlock() }
@@ -2404,10 +2427,10 @@ DataFlowType getNodeType(Node n) {
   not lambdaCreation(n, _, _) and
   not isLocalFunctionCallReceiver(_, n.asExpr(), _)
   or
-  n.asExpr() = result.getADelegateCreation()
-  or
-  n.(LocalFunctionCreationPreNode).getUnderlyingControlFlowNode() =
-    result.getADelegateCreation().getControlFlowNode()
+  [
+    n.asExpr().(ControlFlowElement),
+    n.(LocalFunctionCreationPreNode).getUnderlyingControlFlowNode().getAstNode()
+  ] = result.getADelegateCreation()
 }
 
 private class DataFlowNullType extends Gvn::GvnType {
@@ -2534,10 +2557,10 @@ module PostUpdateNodes {
   class ObjectCreationNode extends SourcePostUpdateNode, ExprNode, TExprNode {
     private ObjectCreation oc;
 
-    ObjectCreationNode() { this = TExprNode(oc.getControlFlowNode()) }
+    ObjectCreationNode() { this = TExprNode(oc.getAControlFlowNode()) }
 
     override Node getPreUpdateSourceNode() {
-      exists(ControlFlowNodes::ElementNode cfn | this = TExprNode(cfn) |
+      exists(ControlFlow::Nodes::ElementNode cfn | this = TExprNode(cfn) |
         result = TObjectInitializerNode(cfn)
         or
         not oc.hasInitializer() and
@@ -2557,11 +2580,11 @@ module PostUpdateNodes {
     TObjectInitializerNode
   {
     private ObjectCreation oc;
-    private ControlFlowNodes::ElementNode cfn;
+    private ControlFlow::Nodes::ElementNode cfn;
 
     ObjectInitializerNode() {
       this = TObjectInitializerNode(cfn) and
-      cfn = oc.getControlFlowNode()
+      cfn = oc.getAControlFlowNode()
     }
 
     /** Gets the initializer to which this initializer node belongs. */
@@ -2580,11 +2603,15 @@ module PostUpdateNodes {
       )
     }
 
-    override DataFlowCallable getEnclosingCallableImpl() { result.getAControlFlowNode() = cfn }
+    override DataFlowCallable getEnclosingCallableImpl() {
+      result.getAControlFlowNode() = cfn
+      or
+      result = getEnclosingStaticFieldOrProperty(oc)
+    }
 
     override Type getTypeImpl() { result = oc.getType() }
 
-    override ControlFlowNodes::ElementNode getControlFlowNodeImpl() { result = cfn }
+    override ControlFlow::Nodes::ElementNode getControlFlowNodeImpl() { result = cfn }
 
     override Location getLocationImpl() { result = cfn.getLocation() }
 
@@ -2592,17 +2619,21 @@ module PostUpdateNodes {
   }
 
   class ExprPostUpdateNode extends SourcePostUpdateNode, NodeImpl, TExprPostUpdateNode {
-    private ControlFlowNodes::ElementNode cfn;
+    private ControlFlow::Nodes::ElementNode cfn;
 
     ExprPostUpdateNode() { this = TExprPostUpdateNode(cfn) }
 
     override ExprNode getPreUpdateSourceNode() { result = TExprNode(cfn) }
 
-    override DataFlowCallable getEnclosingCallableImpl() { result.getAControlFlowNode() = cfn }
+    override DataFlowCallable getEnclosingCallableImpl() {
+      result.getAControlFlowNode() = cfn
+      or
+      result = getEnclosingStaticFieldOrProperty(cfn.getAstNode())
+    }
 
-    override Type getTypeImpl() { result = cfn.asExpr().getType() }
+    override Type getTypeImpl() { result = cfn.getAstNode().(Expr).getType() }
 
-    override ControlFlowNode getControlFlowNodeImpl() { none() }
+    override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
     override Location getLocationImpl() { result = cfn.getLocation() }
 
@@ -2731,7 +2762,7 @@ private predicate isLocalFunctionCallReceiver(
   f = receiver.getTarget().getUnboundDeclaration()
 }
 
-private predicate lambdaCallExpr(DataFlowCall call, Expr receiver, ControlFlowNode receiverCfn) {
+private predicate lambdaCallExpr(DataFlowCall call, Expr receiver, ControlFlow::Node receiverCfn) {
   exists(DelegateLikeCall dc |
     call.(ExplicitDelegateLikeDataFlowCall).getCall() = dc and
     receiver = dc.getExpr() and
@@ -2752,7 +2783,7 @@ predicate lambdaCall(DataFlowCall call, LambdaCallKind kind, Node receiver) {
   (
     lambdaCallExpr(call, receiver.asExpr(), _) and
     // local function calls can be resolved directly without a flow analysis
-    not call.getControlFlowNode().asExpr() instanceof LocalFunctionCall
+    not call.getControlFlowNode().getAstNode() instanceof LocalFunctionCall
     or
     receiver.(FlowSummaryNode).getSummaryNode() = call.(SummaryCall).getReceiver()
   ) and

csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPublic.qll

@@ -17,7 +17,7 @@ class Node extends TNode {
    * Gets the expression corresponding to this node, at control flow node `cfn`,
    * if any.
    */
-  Expr asExprAtNode(ControlFlowNodes::ElementNode cfn) {
+  Expr asExprAtNode(ControlFlow::Nodes::ElementNode cfn) {
     result = this.(ExprNode).getExprAtNode(cfn)
   }
 
@@ -31,7 +31,7 @@ class Node extends TNode {
    * Gets the definition corresponding to this node, at control flow node `cfn`,
    * if any.
    */
-  AssignableDefinition asDefinitionAtNode(ControlFlowNode cfn) {
+  AssignableDefinition asDefinitionAtNode(ControlFlow::Node cfn) {
     result = this.(AssignableDefinitionNode).getDefinitionAtNode(cfn)
   }
 
@@ -44,7 +44,7 @@ class Node extends TNode {
   }
 
   /** Gets the control flow node corresponding to this node, if any. */
-  final ControlFlowNode getControlFlowNode() { result = this.(NodeImpl).getControlFlowNodeImpl() }
+  final ControlFlow::Node getControlFlowNode() { result = this.(NodeImpl).getControlFlowNodeImpl() }
 
   /** Gets a textual representation of this node. */
   final string toString() { result = this.(NodeImpl).toStringImpl() }
@@ -71,7 +71,7 @@ class Node extends TNode {
  *
  * Note that because of control-flow splitting, one `Expr` may correspond
  * to multiple `ExprNode`s, just like it may correspond to multiple
- * `ControlFlowNode`s.
+ * `ControlFlow::Node`s.
  */
 class ExprNode extends Node, TExprNode {
   /** Gets the expression corresponding to this node. */
@@ -81,9 +81,9 @@ class ExprNode extends Node, TExprNode {
    * Gets the expression corresponding to this node, at control flow node `cfn`,
    * if any.
    */
-  Expr getExprAtNode(ControlFlowNodes::ElementNode cfn) {
+  Expr getExprAtNode(ControlFlow::Nodes::ElementNode cfn) {
     this = TExprNode(cfn) and
-    result = cfn.asExpr()
+    result = cfn.getAstNode()
   }
 }
 
@@ -113,7 +113,7 @@ class AssignableDefinitionNode extends Node instanceof AssignableDefinitionNodeI
   AssignableDefinition getDefinition() { result = super.getDefinition() }
 
   /** Gets the underlying definition, at control flow node `cfn`, if any. */
-  AssignableDefinition getDefinitionAtNode(ControlFlowNode cfn) {
+  AssignableDefinition getDefinitionAtNode(ControlFlow::Node cfn) {
     result = super.getDefinitionAtNode(cfn)
   }
 }
@@ -133,14 +133,12 @@ AssignableDefinitionNode assignableDefinitionNode(AssignableDefinition def) {
 
 predicate localFlowStep = localFlowStepImpl/2;
 
-private predicate localFlowStepPlus(Node source, Node sink) = fastTC(localFlowStep/2)(source, sink)
-
 /**
  * Holds if data flows from `source` to `sink` in zero or more local
  * (intra-procedural) steps.
  */
 pragma[inline]
-predicate localFlow(Node source, Node sink) { localFlowStepPlus(source, sink) or source = sink }
+predicate localFlow(Node source, Node sink) { localFlowStep*(source, sink) }
 
 /**
  * Holds if data can flow from `e1` to `e2` in zero or more

csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll

@@ -5,10 +5,11 @@
 import csharp
 private import codeql.ssa.Ssa as SsaImplCommon
 private import AssignableDefinitions
+private import semmle.code.csharp.controlflow.BasicBlocks as BasicBlocks
 private import semmle.code.csharp.controlflow.Guards as Guards
 private import semmle.code.csharp.dataflow.internal.BaseSSA
 
-private module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock> {
+private module SsaInput implements SsaImplCommon::InputSig<Location, ControlFlow::BasicBlock> {
   class SourceVariable = Ssa::SourceVariable;
 
   /**
@@ -17,7 +18,7 @@ private module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock>
    *
    * This includes implicit writes via calls.
    */
-  predicate variableWrite(BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
+  predicate variableWrite(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
     variableWriteDirect(bb, i, v, certain)
     or
     variableWriteQualifier(bb, i, v, certain)
@@ -31,7 +32,7 @@ private module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock>
    *
    * This includes implicit reads via calls.
    */
-  predicate variableRead(BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
+  predicate variableRead(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
     variableReadActual(bb, i, v) and
     certain = true
     or
@@ -40,7 +41,7 @@ private module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock>
   }
 }
 
-import SsaImplCommon::Make<Location, Cfg, SsaInput> as Impl
+import SsaImplCommon::Make<Location, BasicBlocks::Cfg, SsaInput> as Impl
 
 class Definition = Impl::Definition;
 
@@ -55,8 +56,8 @@ module Consistency = Impl::Consistency;
 /**
  * Holds if the `i`th node of basic block `bb` reads source variable `v`.
  */
-private predicate variableReadActual(BasicBlock bb, int i, Ssa::SourceVariable v) {
-  v.getAnAccess().(AssignableRead) = bb.getNode(i).asExpr()
+private predicate variableReadActual(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v) {
+  v.getAnAccess().(AssignableRead) = bb.getNode(i).getAstNode()
 }
 
 private module SourceVariableImpl {
@@ -124,9 +125,11 @@ private module SourceVariableImpl {
    * Holds if the `i`th node of basic block `bb` is assignable definition `ad`
    * targeting source variable `v`.
    */
-  predicate variableDefinition(BasicBlock bb, int i, Ssa::SourceVariable v, AssignableDefinition ad) {
+  predicate variableDefinition(
+    ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, AssignableDefinition ad
+  ) {
     ad = v.getADefinition() and
-    ad.getExpr().getControlFlowNode() = bb.getNode(i) and
+    ad.getExpr().getAControlFlowNode() = bb.getNode(i) and
     // In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
     not exists(TupleAssignmentDefinition first, TupleAssignmentDefinition second | first = ad |
       second.getAssignment() = first.getAssignment() and
@@ -156,7 +159,9 @@ private module SourceVariableImpl {
    *
    * This excludes implicit writes via calls.
    */
-  predicate variableWriteDirect(BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
+  predicate variableWriteDirect(
+    ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain
+  ) {
     exists(AssignableDefinition ad | variableDefinition(bb, i, v, ad) |
       if any(AssignableDefinition ad0 | ad0 = ad or ad0 = getASameOutRefDefAfter(v, ad)).isCertain()
       then certain = true
@@ -181,12 +186,13 @@ private module SourceVariableImpl {
    * }
    * ```
    */
-  predicate outRefExitRead(BasicBlock bb, int i, LocalScopeSourceVariable v) {
-    exists(ControlFlow::NormalExitNode exit |
+  predicate outRefExitRead(ControlFlow::BasicBlock bb, int i, LocalScopeSourceVariable v) {
+    exists(ControlFlow::Nodes::AnnotatedExitNode exit |
+      exit.isNormal() and
       exists(LocalScopeVariable lsv |
         lsv = v.getAssignable() and
         bb.getNode(i) = exit and
-        exit.getEnclosingCallable() = lsv.getCallable()
+        exit.getCallable() = lsv.getCallable()
       |
         lsv.(Parameter).isOutOrRef()
         or
@@ -212,12 +218,12 @@ private module SourceVariableImpl {
    * The pseudo read is inserted at the CFG node `i` on the left-hand side of the
    * assignment on line 3.
    */
-  predicate refReadBeforeWrite(BasicBlock bb, int i, LocalScopeSourceVariable v) {
+  predicate refReadBeforeWrite(ControlFlow::BasicBlock bb, int i, LocalScopeSourceVariable v) {
     exists(AssignableDefinitions::AssignmentDefinition def, LocalVariable lv |
       def.getTarget() = lv and
       lv.isRef() and
       lv = v.getAssignable() and
-      bb.getNode(i) = def.getExpr().getControlFlowNode() and
+      bb.getNode(i) = def.getExpr().getAControlFlowNode() and
       not def.getAssignment() instanceof LocalVariableDeclAndInitExpr
     )
   }
@@ -270,17 +276,15 @@ private module CallGraph {
    *
    * the constructor call `new Lazy<int>(M2)` includes `M2` as a target.
    */
-  Callable getARuntimeTarget(Call c, ControlFlowNode n, boolean libraryDelegateCall) {
+  Callable getARuntimeTarget(Call c, boolean libraryDelegateCall) {
     // Non-delegate call: use dispatch library
     exists(DispatchCall dc | dc.getCall() = c |
-      n = dc.getControlFlowNode() and
       result = dc.getADynamicTarget().getUnboundDeclaration() and
       libraryDelegateCall = false
     )
     or
     // Delegate call: use simple analysis
-    result = SimpleDelegateAnalysis::getARuntimeDelegateTarget(c, libraryDelegateCall) and
-    n = c.getControlFlowNode()
+    result = SimpleDelegateAnalysis::getARuntimeDelegateTarget(c, libraryDelegateCall)
   }
 
   private module SimpleDelegateAnalysis {
@@ -467,7 +471,7 @@ private module CallGraph {
 
   /** Holds if `(c1,c2)` is an edge in the call graph. */
   predicate callEdge(Callable c1, Callable c2) {
-    exists(Call c | c.getEnclosingCallable() = c1 and c2 = getARuntimeTarget(c, _, _))
+    exists(Call c | c.getEnclosingCallable() = c1 and c2 = getARuntimeTarget(c, _))
   }
 }
 
@@ -601,7 +605,7 @@ private module FieldOrPropsImpl {
   private predicate intraInstanceCallEdge(Callable c1, InstanceCallable c2) {
     exists(Call c |
       c.getEnclosingCallable() = c1 and
-      c2 = getARuntimeTarget(c, _, _) and
+      c2 = getARuntimeTarget(c, _) and
       c.(QualifiableExpr).targetIsLocalInstance()
     )
   }
@@ -616,8 +620,9 @@ private module FieldOrPropsImpl {
   }
 
   pragma[noinline]
-  predicate callAt(BasicBlock bb, int i, Call call) {
-    getARuntimeTarget(call, bb.getNode(i), _).hasBody()
+  predicate callAt(ControlFlow::BasicBlock bb, int i, Call call) {
+    bb.getNode(i) = call.getAControlFlowNode() and
+    getARuntimeTarget(call, _).hasBody()
   }
 
   /**
@@ -625,7 +630,9 @@ private module FieldOrPropsImpl {
    * an update somewhere, and `fp` is likely to be live in `bb` at index
    * `i`.
    */
-  predicate updateCandidate(BasicBlock bb, int i, FieldOrPropSourceVariable fp, Call call) {
+  predicate updateCandidate(
+    ControlFlow::BasicBlock bb, int i, FieldOrPropSourceVariable fp, Call call
+  ) {
     callAt(bb, i, call) and
     call.getEnclosingCallable() = fp.getEnclosingCallable() and
     relevantDefinition(_, fp.getAssignable(), _) and
@@ -636,7 +643,7 @@ private module FieldOrPropsImpl {
     Call call, FieldOrPropSourceVariable fps, FieldOrProp fp, Callable c, boolean fresh
   ) {
     updateCandidate(_, _, fps, call) and
-    c = getARuntimeTarget(call, _, _) and
+    c = getARuntimeTarget(call, _) and
     fp = fps.getAssignable() and
     if c instanceof Constructor then fresh = true else fresh = false
   }
@@ -707,12 +714,71 @@ private module FieldOrPropsImpl {
   }
 }
 
-private predicate variableReadPseudo(BasicBlock bb, int i, Ssa::SourceVariable v) {
+private predicate variableReadPseudo(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v) {
   outRefExitRead(bb, i, v)
   or
   refReadBeforeWrite(bb, i, v)
 }
 
+pragma[noinline]
+deprecated private predicate adjacentDefRead(
+  Definition def, ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2,
+  SsaInput::SourceVariable v
+) {
+  Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
+  v = def.getSourceVariable()
+}
+
+deprecated private predicate adjacentDefReachesRead(
+  Definition def, SsaInput::SourceVariable v, ControlFlow::BasicBlock bb1, int i1,
+  ControlFlow::BasicBlock bb2, int i2
+) {
+  adjacentDefRead(def, bb1, i1, bb2, i2, v) and
+  (
+    def.definesAt(v, bb1, i1)
+    or
+    SsaInput::variableRead(bb1, i1, v, true)
+  )
+  or
+  exists(ControlFlow::BasicBlock bb3, int i3 |
+    adjacentDefReachesRead(def, v, bb1, i1, bb3, i3) and
+    SsaInput::variableRead(bb3, i3, _, false) and
+    Impl::adjacentDefRead(def, bb3, i3, bb2, i2)
+  )
+}
+
+deprecated private predicate adjacentDefReachesUncertainRead(
+  Definition def, ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2
+) {
+  exists(SsaInput::SourceVariable v |
+    adjacentDefReachesRead(def, v, bb1, i1, bb2, i2) and
+    SsaInput::variableRead(bb2, i2, v, false)
+  )
+}
+
+/** Same as `lastRefRedef`, but skips uncertain reads. */
+pragma[nomagic]
+deprecated private predicate lastRefSkipUncertainReads(
+  Definition def, ControlFlow::BasicBlock bb, int i
+) {
+  Impl::lastRef(def, bb, i) and
+  not SsaInput::variableRead(bb, i, def.getSourceVariable(), false)
+  or
+  exists(ControlFlow::BasicBlock bb0, int i0 |
+    Impl::lastRef(def, bb0, i0) and
+    adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
+  )
+}
+
+pragma[nomagic]
+deprecated predicate lastReadSameVar(Definition def, ControlFlow::Node cfn) {
+  exists(ControlFlow::BasicBlock bb, int i |
+    lastRefSkipUncertainReads(def, bb, i) and
+    variableReadActual(bb, i, _) and
+    cfn = bb.getNode(i)
+  )
+}
+
 cached
 private module Cached {
   cached
@@ -752,9 +818,9 @@ private module Cached {
   }
 
   cached
-  predicate implicitEntryDefinition(BasicBlock bb, Ssa::SourceVariable v) {
-    exists(EntryBasicBlock entry, Callable c |
-      c = entry.getEnclosingCallable() and
+  predicate implicitEntryDefinition(ControlFlow::BasicBlock bb, Ssa::SourceVariable v) {
+    exists(ControlFlow::BasicBlocks::EntryBlock entry, Callable c |
+      c = entry.getCallable() and
       // In case `c` has multiple bodies, we want each body to get its own implicit
       // entry definition. In case `c` doesn't have multiple bodies, the line below
       // is simply the same as `bb = entry`, because `entry.getFirstNode().getASuccessor()`
@@ -790,7 +856,7 @@ private module Cached {
    */
   cached
   predicate updatesNamedFieldOrProp(
-    BasicBlock bb, int i, Call c, FieldOrPropSourceVariable fp, Callable setter
+    ControlFlow::BasicBlock bb, int i, Call c, FieldOrPropSourceVariable fp, Callable setter
   ) {
     FieldOrPropsImpl::updateCandidate(bb, i, fp, c) and
     FieldOrPropsImpl::updatesNamedFieldOrProp(fp, c, setter)
@@ -798,7 +864,7 @@ private module Cached {
 
   cached
   predicate variableWriteQualifier(
-    BasicBlock bb, int i, QualifiedFieldOrPropSourceVariable v, boolean certain
+    ControlFlow::BasicBlock bb, int i, QualifiedFieldOrPropSourceVariable v, boolean certain
   ) {
     SsaInput::variableWrite(bb, i, v.getQualifier(), certain) and
     // Eliminate corner case where a call definition can overlap with a
@@ -811,29 +877,29 @@ private module Cached {
 
   cached
   predicate explicitDefinition(WriteDefinition def, Ssa::SourceVariable v, AssignableDefinition ad) {
-    exists(BasicBlock bb, int i |
+    exists(ControlFlow::BasicBlock bb, int i |
       def.definesAt(v, bb, i) and
       variableDefinition(bb, i, v, ad)
     )
   }
 
   cached
-  predicate isLiveAtEndOfBlock(Definition def, BasicBlock bb) {
+  predicate isLiveAtEndOfBlock(Definition def, ControlFlow::BasicBlock bb) {
     Impl::ssaDefReachesEndOfBlock(bb, def, _)
   }
 
   cached
-  Definition phiHasInputFromBlock(Ssa::PhiNode phi, BasicBlock bb) {
+  Definition phiHasInputFromBlock(Ssa::PhiNode phi, ControlFlow::BasicBlock bb) {
     Impl::phiHasInputFromBlock(phi, result, bb)
   }
 
   cached
-  AssignableRead getAReadAtNode(Definition def, ControlFlowNode cfn) {
-    exists(Ssa::SourceVariable v, BasicBlock bb, int i |
+  AssignableRead getAReadAtNode(Definition def, ControlFlow::Node cfn) {
+    exists(Ssa::SourceVariable v, ControlFlow::BasicBlock bb, int i |
       Impl::ssaDefReachesRead(v, def, bb, i) and
       variableReadActual(bb, i, v) and
       cfn = bb.getNode(i) and
-      result.getControlFlowNode() = cfn
+      result.getAControlFlowNode() = cfn
     )
   }
 
@@ -842,8 +908,10 @@ private module Cached {
    * without passing through any other read.
    */
   cached
-  predicate firstReadSameVar(Definition def, ControlFlowNode cfn) {
-    exists(BasicBlock bb, int i | Impl::firstUse(def, bb, i, true) and cfn = bb.getNode(i))
+  predicate firstReadSameVar(Definition def, ControlFlow::Node cfn) {
+    exists(ControlFlow::BasicBlock bb, int i |
+      Impl::firstUse(def, bb, i, true) and cfn = bb.getNode(i)
+    )
   }
 
   /**
@@ -852,8 +920,11 @@ private module Cached {
    * passing through another read.
    */
   cached
-  predicate adjacentReadPairSameVar(Definition def, ControlFlowNode cfn1, ControlFlowNode cfn2) {
-    exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2, Ssa::SourceVariable v |
+  predicate adjacentReadPairSameVar(Definition def, ControlFlow::Node cfn1, ControlFlow::Node cfn2) {
+    exists(
+      ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2,
+      Ssa::SourceVariable v
+    |
       Impl::ssaDefReachesRead(v, def, bb1, i1) and
       Impl::adjacentUseUse(bb1, i1, bb2, i2, v, true) and
       cfn1 = bb1.getNode(i1) and
@@ -869,7 +940,7 @@ private module Cached {
   cached
   predicate isLiveOutRefParameterDefinition(Ssa::Definition def, Parameter p) {
     p.isOutOrRef() and
-    exists(Ssa::SourceVariable v, Ssa::Definition def0, BasicBlock bb, int i |
+    exists(Ssa::SourceVariable v, Ssa::Definition def0, ControlFlow::BasicBlock bb, int i |
       v = def.getSourceVariable() and
       p = v.getAssignable() and
       def = def0.getAnUltimateDefinition() and
@@ -951,11 +1022,31 @@ private module Cached {
 
 import Cached
 
+private string getSplitString(Definition def) {
+  exists(ControlFlow::BasicBlock bb, int i, ControlFlow::Node cfn |
+    def.definesAt(_, bb, i) and
+    result = cfn.(ControlFlow::Nodes::ElementNode).getSplitsString()
+  |
+    cfn = bb.getNode(i)
+    or
+    not exists(bb.getNode(i)) and
+    cfn = bb.getFirstNode()
+  )
+}
+
+string getToStringPrefix(Definition def) {
+  result = "[" + getSplitString(def) + "] "
+  or
+  not exists(getSplitString(def)) and
+  result = ""
+}
+
 private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
+  private import semmle.code.csharp.controlflow.BasicBlocks
   private import codeql.util.Boolean
 
-  class Expr extends ControlFlowNode {
-    predicate hasCfgNode(BasicBlock bb, int i) { this = bb.getNode(i) }
+  class Expr extends ControlFlow::Node {
+    predicate hasCfgNode(ControlFlow::BasicBlock bb, int i) { this = bb.getNode(i) }
   }
 
   Expr getARead(Definition def) { exists(getAReadAtNode(def, result)) }

csharp/ql/lib/semmle/code/csharp/dataflow/internal/Steps.qll

@@ -15,8 +15,8 @@ module Steps {
    * Gets a read that may read the value assigned at definition `def`.
    */
   private AssignableRead getARead(AssignableDefinition def) {
-    exists(BaseSsa::SsaDefinition ssaDef |
-      ssaDef.getAnUltimateDefinition().(BaseSsa::SsaExplicitWrite).getDefinition() = def and
+    exists(BaseSsa::Definition ssaDef |
+      ssaDef.getAnUltimateDefinition().getDefinition() = def and
       result = ssaDef.getARead()
     )
     or

csharp/ql/lib/semmle/code/csharp/dataflow/internal/TaintTrackingPublic.qll

@@ -1,17 +1,12 @@
 private import csharp
 private import TaintTrackingPrivate
 
-private predicate localTaintStepPlus(DataFlow::Node source, DataFlow::Node sink) =
-  fastTC(localTaintStep/2)(source, sink)
-
 /**
  * Holds if taint propagates from `source` to `sink` in zero or more local
  * (intra-procedural) steps.
  */
 pragma[inline]
-predicate localTaint(DataFlow::Node source, DataFlow::Node sink) {
-  localTaintStepPlus(source, sink) or source = sink
-}
+predicate localTaint(DataFlow::Node source, DataFlow::Node sink) { localTaintStep*(source, sink) }
 
 /**
  * Holds if taint can flow from `e1` to `e2` in zero or more

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundSpecific.qll

@@ -10,7 +10,7 @@ private import semmle.code.csharp.dataflow.internal.rangeanalysis.SsaUtils as SU
 
 class SsaVariable = SU::SsaVariable;
 
-class Expr = CS::ControlFlowNodes::ExprNode;
+class Expr = CS::ControlFlow::Nodes::ExprNode;
 
 class Location = CS::Location;
 

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/ConstantUtils.qll

@@ -7,7 +7,7 @@ private import Ssa
 private import SsaUtils
 private import RangeUtils
 
-private class ExprNode = ControlFlowNodes::ExprNode;
+private class ExprNode = ControlFlow::Nodes::ExprNode;
 
 /**
  * Holds if `pa` is an access to the `Length` property of an array.

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll

@@ -4,14 +4,15 @@ module Private {
   private import semmle.code.csharp.dataflow.internal.rangeanalysis.RangeUtils as RU
   private import SsaUtils as SU
   private import SsaReadPositionCommon
+  private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl as CfgImpl
 
-  class BasicBlock = CS::BasicBlock;
+  class BasicBlock = CS::ControlFlow::BasicBlock;
 
   class SsaVariable = SU::SsaVariable;
 
   class SsaPhiNode = CS::Ssa::PhiNode;
 
-  class Expr = CS::ControlFlowNodes::ExprNode;
+  class Expr = CS::ControlFlow::Nodes::ExprNode;
 
   class Guard = RU::Guard;
 

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll

@@ -9,7 +9,7 @@ private module Impl {
   private import SsaReadPositionCommon
   private import semmle.code.csharp.controlflow.Guards as G
 
-  private class ExprNode = ControlFlowNodes::ExprNode;
+  private class ExprNode = ControlFlow::Nodes::ExprNode;
 
   /** Holds if `parent` having child `child` implies `parentNode` having child `childNode`. */
   predicate hasChild(Expr parent, Expr child, ExprNode parentNode, ExprNode childNode) {
@@ -20,7 +20,7 @@ private module Impl {
 
   /** Holds if SSA definition `def` equals `e + delta`. */
   predicate ssaUpdateStep(ExplicitDefinition def, ExprNode e, int delta) {
-    exists(ControlFlowNode cfn | cfn = def.getControlFlowNode() |
+    exists(ControlFlow::Node cfn | cfn = def.getControlFlowNode() |
       e = cfn.(ExprNode::Assignment).getRightOperand() and
       delta = 0 and
       not cfn instanceof ExprNode::AssignOperation
@@ -83,7 +83,9 @@ private module Impl {
     /**
      * Holds if basic block `bb` is guarded by this guard having value `v`.
      */
-    predicate controlsBasicBlock(BasicBlock bb, G::GuardValue v) { super.controlsBasicBlock(bb, v) }
+    predicate controlsBasicBlock(ControlFlow::BasicBlock bb, G::GuardValue v) {
+      super.controlsBasicBlock(bb, v)
+    }
 
     /**
      * Holds if this guard is an equality test between `e1` and `e2`. If the test is
@@ -158,7 +160,7 @@ import Impl
 module ExprNode {
   private import csharp as CS
 
-  private class ExprNode = CS::ControlFlowNodes::ExprNode;
+  private class ExprNode = CS::ControlFlow::Nodes::ExprNode;
 
   private import Sign
 

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll

@@ -33,7 +33,7 @@ module Private {
 
   class Type = CS::Type;
 
-  class Expr = CS::ControlFlowNodes::ExprNode;
+  class Expr = CS::ControlFlow::Nodes::ExprNode;
 
   class VariableUpdate = CS::Ssa::ExplicitDefinition;
 
@@ -63,7 +63,7 @@ private module Impl {
   private import SsaReadPositionCommon
   private import semmle.code.csharp.commons.ComparisonTest
 
-  private class ExprNode = ControlFlowNodes::ExprNode;
+  private class ExprNode = ControlFlow::Nodes::ExprNode;
 
   /** Gets the character value of expression `e`. */
   string getCharValue(ExprNode e) { result = e.getValue() and e.getType() instanceof CharType }
@@ -254,7 +254,7 @@ private module Impl {
   Guard getComparisonGuard(ComparisonExpr ce) { result = ce.getExpr() }
 
   private newtype TComparisonExpr =
-    MkComparisonExpr(ComparisonTest ct, ExprNode e) { e = ct.getExpr().getControlFlowNode() }
+    MkComparisonExpr(ComparisonTest ct, ExprNode e) { e = ct.getExpr().getAControlFlowNode() }
 
   /** A relational comparison */
   class ComparisonExpr extends MkComparisonExpr {