Merge branch 'main' into ihsinme-patch-259

.github/workflows/check-change-note.yml

@@ -1,3 +1,5 @@
+name: Check change note
+
 on:
   pull_request_target:
     types: [labeled, unlabeled, opened, synchronize, reopened, ready_for_review]

.github/workflows/close-stale.yml

@@ -0,0 +1,30 @@
+name: Mark stale issues
+
+on:
+  workflow_dispatch:
+  schedule:
+    - cron: "30 1 * * *"
+
+jobs:
+  stale:
+    if: github.repository == 'github/codeql'
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/stale@v3
+      with:
+        repo-token: ${{ secrets.GITHUB_TOKEN }}
+        stale-issue-message: 'This issue is stale because it has been open 14 days with no activity. Comment or remove the `stale` label in order to avoid having this issue closed in 7 days.'
+        close-issue-message: 'This issue was closed because it has been inactive for 7 days.'
+        days-before-stale: 14
+        days-before-close: 7
+        only-labels: question
+        
+        # do not mark PRs as stale
+        days-before-pr-stale: -1
+        days-before-pr-close: -1
+        
+        # Uncomment for dry-run
+        # debug-only: true
+        # operations-per-run: 1000

.github/workflows/docs-review.yml

@@ -1,29 +0,0 @@
-# When a PR is labelled with 'ready-for-docs-review',
-# this workflow comments on the PR to notify the GitHub CodeQL docs team.
-name: Request docs review
-on:
-  # Runs in the context of the base repo.
-  # This gives the workflow write access to comment on PRs.
-  # The workflow should not check out or build the given ref,
-  # or use untrusted data from the event payload in a command line.
-  pull_request_target:
-    types: [labeled]
-
-jobs:
-  request-docs-review:
-    name: Request docs review
-    # Run only on labelled PRs to the main repository.
-    # Do not run on PRs to forks.
-    if:
-      github.event.label.name == 'ready-for-docs-review'
-      && github.event.pull_request.draft == false
-      && github.event.pull_request.base.repo.full_name == 'github/codeql'
-    runs-on: ubuntu-latest
-    steps:
-      - name: Comment to request docs review
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-          PR_NUMBER: ${{ github.event.pull_request.number }}
-        run: |
-          gh pr comment "$PR_NUMBER" --repo "github/codeql" \
-            --body "Hello @github/docs-content-codeql: this PR is ready for docs review."

.github/workflows/generate-query-help-docs.yml

@@ -1,60 +0,0 @@
-name: Generate CodeQL query help documentation using Sphinx
-
-on:
-  workflow_dispatch:
-      inputs:
-        description:
-          description: A description of the purpose of this job. For human consumption.
-          required: false
-  push:
-    branches:
-     - 'lgtm.com'
-  pull_request:
-    paths:
-      - '.github/workflows/generate-query-help-docs.yml'
-      - 'docs/codeql/query-help/**'
-      
-jobs:
-  build:
-    runs-on: ubuntu-latest
-    steps:
-    - name: Clone github/codeql
-      uses: actions/checkout@v2
-      with:
-        path: codeql
-    - name: Clone github/codeql-go
-      uses: actions/checkout@v2
-      with:
-        repository: 'github/codeql-go'
-        path: codeql-go
-    - name: Set up Python 3.8
-      uses: actions/setup-python@v2
-      with:
-        python-version: 3.8
-    - name: Download CodeQL CLI
-      uses: dsaltares/fetch-gh-release-asset@aa37ae5c44d3c9820bc12fe675e8670ecd93bd1c
-      with:
-        repo: "github/codeql-cli-binaries"
-        version: "latest"
-        file: "codeql-linux64.zip"
-        token: ${{ secrets.GITHUB_TOKEN }}
-    - name: Unzip CodeQL CLI
-      run: unzip -d codeql-cli codeql-linux64.zip
-    - name: Set up query help docs folder  
-      run: |
-        cp -r codeql/docs/codeql/** .
-    - name: Query help to markdown
-      run: |
-        PATH="$PATH:codeql-cli/codeql" python codeql/docs/codeql/query-help-markdown.py
-    - name: Run Sphinx for query help
-      uses: ammaraskar/sphinx-action@8b4f60114d7fd1faeba1a712269168508d4750d2 # v0.4
-      with:
-        docs-folder: "query-help/"
-        pre-build-command: "python -m pip install --upgrade recommonmark && python -m pip install --upgrade sphinx-markdown-tables"
-        build-command: "sphinx-build -b dirhtml . _build" 
-    - name: Upload HTML artifacts
-      uses: actions/upload-artifact@v2
-      with:
-        name: query-help-html
-        path: query-help/_build
-    

.vscode/settings.json

@@ -1,3 +1,3 @@
 {
     "omnisharp.autoStart": false
-}
+}

CONTRIBUTING.md

@@ -38,7 +38,7 @@ If you have an idea for a query that you would like to share with other CodeQL u
 
     - The queries and libraries must be autoformatted, for example using the "Format Document" command in [CodeQL for Visual Studio Code](https://help.semmle.com/codeql/codeql-for-vscode/procedures/about-codeql-for-vscode.html).
 
-    If you prefer, you can use this [pre-commit hook](misc/scripts/pre-commit) that automatically checks whether your files are correctly formatted. See the [pre-commit hook installation guide](docs/install-pre-commit-hook.md) for instructions on how to install the hook.
+    If you prefer, you can use this [pre-commit hook](misc/scripts/pre-commit) that automatically checks whether your files are correctly formatted. See the [pre-commit hook installation guide](docs/pre-commit-hook-setup.md) for instructions on how to install the hook.
 
 4. **Compilation**
 

config/identical-files.json

@@ -36,6 +36,7 @@
     "cpp/ql/src/semmle/code/cpp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll",
     "cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/tainttracking1/TaintTrackingImpl.qll",
     "cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/tainttracking2/TaintTrackingImpl.qll",
+    "cpp/ql/src/semmle/code/cpp/ir/dataflow/internal/tainttracking3/TaintTrackingImpl.qll",
     "csharp/ql/src/semmle/code/csharp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll",
     "csharp/ql/src/semmle/code/csharp/dataflow/internal/tainttracking2/TaintTrackingImpl.qll",
     "csharp/ql/src/semmle/code/csharp/dataflow/internal/tainttracking3/TaintTrackingImpl.qll",
@@ -55,6 +56,10 @@
     "csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImplConsistency.qll",
     "python/ql/src/semmle/python/dataflow/new/internal/DataFlowImplConsistency.qll"
   ],
+  "DataFlow Java/C# Flow Summaries": [
+    "java/ql/src/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll",
+    "csharp/ql/src/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll"
+  ],
   "SsaReadPosition Java/C#": [
     "java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll",
     "csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll"
@@ -376,7 +381,6 @@
   ],
   "DuplicationProblems.inc.qhelp": [
     "cpp/ql/src/Metrics/Files/DuplicationProblems.inc.qhelp",
-    "csharp/ql/src/Metrics/Files/DuplicationProblems.inc.qhelp",
     "javascript/ql/src/Metrics/DuplicationProblems.inc.qhelp",
     "python/ql/src/Metrics/DuplicationProblems.inc.qhelp"
   ],
@@ -429,10 +433,11 @@
   "SSA C#": [
     "csharp/ql/src/semmle/code/csharp/dataflow/internal/SsaImplCommon.qll",
     "csharp/ql/src/semmle/code/csharp/controlflow/internal/pressa/SsaImplCommon.qll",
-    "csharp/ql/src/semmle/code/csharp/dataflow/internal/basessa/SsaImplCommon.qll"
+    "csharp/ql/src/semmle/code/csharp/dataflow/internal/basessa/SsaImplCommon.qll",
+    "csharp/ql/src/semmle/code/cil/internal/SsaImplCommon.qll"
   ],
   "CryptoAlgorithms Python/JS": [
     "javascript/ql/src/semmle/javascript/security/CryptoAlgorithms.qll",
     "python/ql/src/semmle/crypto/Crypto.qll"
   ]
-}
+}

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

@@ -5,6 +5,7 @@ using System;
 using System.Linq;
 using Microsoft.Build.Construction;
 using System.Xml;
+using System.IO;
 
 namespace Semmle.Autobuild.Cpp.Tests
 {
@@ -43,6 +44,8 @@ namespace Semmle.Autobuild.Cpp.Tests
         public IDictionary<string, int> RunProcess = new Dictionary<string, int>();
         public IDictionary<string, string> RunProcessOut = new Dictionary<string, string>();
         public IDictionary<string, string> RunProcessWorkingDirectory = new Dictionary<string, string>();
+        public HashSet<string> CreateDirectories { get; } = new HashSet<string>();
+        public HashSet<(string, string)> DownloadFiles { get; } = new HashSet<(string, string)>();
 
         int IBuildActions.RunProcess(string cmd, string args, string? workingDirectory, IDictionary<string, string>? env, out IList<string> stdOut)
         {
@@ -135,6 +138,14 @@ namespace Semmle.Autobuild.Cpp.Tests
 
         string IBuildActions.GetFullPath(string path) => path;
 
+        string? IBuildActions.GetFileName(string? path) => Path.GetFileName(path?.Replace('\\', '/'));
+
+        public string? GetDirectoryName(string? path)
+        {
+            var dir = Path.GetDirectoryName(path?.Replace('\\', '/'));
+            return dir is null ? path : path?.Substring(0, dir.Length);
+        }
+
         void IBuildActions.WriteAllText(string filename, string contents)
         {
         }
@@ -153,6 +164,18 @@ namespace Semmle.Autobuild.Cpp.Tests
                 s = s.Replace($"%{kvp.Key}%", kvp.Value);
             return s;
         }
+
+        public void CreateDirectory(string path)
+        {
+            if (!CreateDirectories.Contains(path))
+                throw new ArgumentException($"Missing CreateDirectory, {path}");
+        }
+
+        public void DownloadFile(string address, string fileName)
+        {
+            if (!DownloadFiles.Contains((address, fileName)))
+                throw new ArgumentException($"Missing DownloadFile, {address}, {fileName}");
+        }
     }
 
     /// <summary>
@@ -213,6 +236,7 @@ namespace Semmle.Autobuild.Cpp.Tests
             Actions.GetEnvironmentVariable[$"CODEQL_EXTRACTOR_{codeqlUpperLanguage}_SOURCE_ARCHIVE_DIR"] = "";
             Actions.GetEnvironmentVariable[$"CODEQL_EXTRACTOR_{codeqlUpperLanguage}_ROOT"] = $@"C:\codeql\{codeqlUpperLanguage.ToLowerInvariant()}";
             Actions.GetEnvironmentVariable["CODEQL_JAVA_HOME"] = @"C:\codeql\tools\java";
+            Actions.GetEnvironmentVariable["CODEQL_PLATFORM"] = "win64";
             Actions.GetEnvironmentVariable["SEMMLE_DIST"] = @"C:\odasa";
             Actions.GetEnvironmentVariable["SEMMLE_JAVA_HOME"] = @"C:\odasa\tools\java";
             Actions.GetEnvironmentVariable["SEMMLE_PLATFORM_TOOLS"] = @"C:\odasa\tools";
@@ -273,7 +297,8 @@ namespace Semmle.Autobuild.Cpp.Tests
         [Fact]
         public void TestCppAutobuilderSuccess()
         {
-            Actions.RunProcess[@"cmd.exe /C C:\odasa\tools\csharp\nuget\nuget.exe restore C:\Project\test.sln"] = 1;
+            Actions.RunProcess[@"cmd.exe /C nuget restore C:\Project\test.sln -DisableParallelProcessing"] = 1;
+            Actions.RunProcess[@"cmd.exe /C C:\Project\.nuget\nuget.exe restore C:\Project\test.sln -DisableParallelProcessing"] = 0;
             Actions.RunProcess[@"cmd.exe /C CALL ^""C:\Program Files ^(x86^)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat^"" && set Platform=&& type NUL && C:\odasa\tools\odasa index --auto msbuild C:\Project\test.sln /p:UseSharedCompilation=false /t:rebuild /p:Platform=""x86"" /p:Configuration=""Release"" /p:MvcBuildViews=true"] = 0;
             Actions.RunProcessOut[@"C:\Program Files (x86)\Microsoft Visual Studio\Installer\vswhere.exe -prerelease -legacy -property installationPath"] = "";
             Actions.RunProcess[@"C:\Program Files (x86)\Microsoft Visual Studio\Installer\vswhere.exe -prerelease -legacy -property installationPath"] = 1;
@@ -286,11 +311,13 @@ namespace Semmle.Autobuild.Cpp.Tests
             Actions.FileExists[@"C:\Program Files (x86)\Microsoft Visual Studio\Installer\vswhere.exe"] = true;
             Actions.EnumerateFiles[@"C:\Project"] = "foo.cs\ntest.slx";
             Actions.EnumerateDirectories[@"C:\Project"] = "";
+            Actions.CreateDirectories.Add(@"C:\Project\.nuget");
+            Actions.DownloadFiles.Add(("https://dist.nuget.org/win-x86-commandline/latest/nuget.exe", @"C:\Project\.nuget\nuget.exe"));
 
             var autobuilder = CreateAutoBuilder(true);
             var solution = new TestSolution(@"C:\Project\test.sln");
             autobuilder.ProjectsOrSolutionsToBuild.Add(solution);
-            TestAutobuilderScript(autobuilder, 0, 2);
+            TestAutobuilderScript(autobuilder, 0, 3);
         }
     }
 }

cpp/autobuilder/Semmle.Autobuild.Cpp/Semmle.Autobuild.Cpp.csproj

@@ -17,7 +17,7 @@
   </ItemGroup>
 
   <ItemGroup>
-    <PackageReference Include="Microsoft.Build" Version="16.0.461" />
+    <PackageReference Include="Microsoft.Build" Version="16.9.0" />
   </ItemGroup>
 
   <ItemGroup>

cpp/change-notes/2021-03-11-failed-extractions.md

@@ -0,0 +1,2 @@
+codescanning
+* Added cpp/diagnostics/failed-extractions. This query gives information about which extractions did not run to completion.

cpp/change-notes/2021-03-17-av-rule-79.md

@@ -0,0 +1,2 @@
+lgtm,codescanning
+* The 'Resource not released in destructor' (cpp/resource-not-released-in-destructor) query has been improved to recognize more releases of resources.

cpp/change-notes/2021-04-06-assign-where-compare-meant.md

@@ -0,0 +1,2 @@
+lgtm,codescanning
+* The 'Assignment where comparison was intended' (cpp/assign-where-compare-meant) query has been improved to flag fewer benign assignments in conditionals.

cpp/change-notes/2021-04-13-arithmetic-queries.md

@@ -0,0 +1,2 @@
+lgtm
+* The queries cpp/tainted-arithmetic, cpp/uncontrolled-arithmetic, and cpp/arithmetic-with-extreme-values have been improved to produce fewer false positives.

cpp/ql/src/Critical/DeadCodeCondition.qhelp

@@ -9,7 +9,7 @@
 It is likely that these conditions indicate an error in the branching condition. 
 Alternatively, the conditions may have been left behind after debugging.</p>
 
-<include src="aliasAnalysisWarning.qhelp" />
+<include src="aliasAnalysisWarning.inc.qhelp" />
 </overview>
 
 <recommendation>

cpp/ql/src/Critical/DeadCodeFunction.qhelp

@@ -13,7 +13,7 @@ If left in the code base they increase object code size, decrease code comprehen
 This type of function may be part of the program's API and could be used by external programs.
 </p>
 
-<include src="callGraphWarning.qhelp" />
+<include src="callGraphWarning.inc.qhelp" />
 </overview>
 
 <recommendation>

cpp/ql/src/Critical/DescriptorMayNotBeClosed.qhelp

@@ -10,7 +10,7 @@ This query looks at functions that return file or socket descriptors, but may re
 This can occur when an operation performed on the open descriptor fails, and the function returns with an error before it closes the open resource. An improperly handled error could cause the function to leak resource descriptors. Failing to close resources in the function that opened them also makes it more difficult to detect leaks.
 </p> 
 
-<include src="dataFlowWarning.qhelp" />
+<include src="dataFlowWarning.inc.qhelp" />
 </overview>
 
 <recommendation>

cpp/ql/src/Critical/DescriptorNeverClosed.qhelp

@@ -10,7 +10,7 @@ This rule finds calls to <code>socket</code> where there is no corresponding <co
 Leaving descriptors open will cause a resource leak that will persist even after the program terminates.
 </p>
 
-<include src="aliasAnalysisWarning.qhelp" />
+<include src="aliasAnalysisWarning.inc.qhelp" />
 </overview>
 
 <recommendation>

cpp/ql/src/Critical/FileMayNotBeClosed.qhelp

@@ -10,7 +10,7 @@ This rule looks at functions that return a <code>FILE*</code>, but may return an
 This can occur when an operation performed on the open descriptor fails, and the function returns with an error before closing the open resource. An improperly handled error may cause the function to leak file descriptors.
 </p> 
 
-<include src="dataFlowWarning.qhelp" />
+<include src="dataFlowWarning.inc.qhelp" />
 
 </overview>
 <recommendation>

cpp/ql/src/Critical/FileNeverClosed.qhelp

@@ -10,7 +10,7 @@ This rule finds calls to <code>fopen</code> with no corresponding <code>fclose</
 Leaving files open will cause a resource leak that will persist even after the program terminates.
 </p>
 
-<include src="aliasAnalysisWarning.qhelp" />
+<include src="aliasAnalysisWarning.inc.qhelp" />
 
 </overview>
 <recommendation>

cpp/ql/src/Critical/GlobalUseBeforeInit.qhelp

@@ -10,7 +10,7 @@ Not all compilers generate code that zero-out memory, especially when optimizati
 is not compliant with the latest language standards. Accessing uninitialized memory will lead to undefined results.
 </p>
 
-<include src="dataFlowWarning.qhelp" />
+<include src="dataFlowWarning.inc.qhelp" />
 </overview>
 
 <recommendation>

cpp/ql/src/Critical/InconsistentNullnessTesting.qhelp

@@ -12,7 +12,7 @@ Dereferencing a null pointer and attempting to modify its contents can lead to a
 important system data (including the interrupt table in some architectures).
 </p>
 
-<include src="pointsToWarning.qhelp" />
+<include src="pointsToWarning.inc.qhelp" />
 </overview>
 
 <recommendation>

cpp/ql/src/Critical/InitialisationNotRun.qhelp

@@ -11,7 +11,7 @@ Uninitialized variables may contain any value, as not all compilers generate cod
 optimizations are enabled or the compiler is not compliant with the latest language standards.
 </p>
 
-<include src="callGraphWarning.qhelp" />
+<include src="callGraphWarning.inc.qhelp" />
 </overview>
 
 <recommendation>

cpp/ql/src/Critical/LateNegativeTest.qhelp

@@ -13,7 +13,7 @@ after. Otherwise, if the value is negative then the program will have failed
 before performing the test.
 </p>
 
-<include src="dataFlowWarning.qhelp" />
+<include src="dataFlowWarning.inc.qhelp" />
 </overview>
 
 <recommendation>

cpp/ql/src/Critical/MemoryMayNotBeFreed.qhelp

@@ -9,7 +9,7 @@
 This rule looks for functions that allocate memory, but may return without freeing it.  This can occur when an operation performed on the memory block fails, and the function returns with an error before freeing the allocated block.  This causes the function to leak memory and may eventually lead to software failure.
 </p> 
 
-<include src="dataFlowWarning.qhelp" />
+<include src="dataFlowWarning.inc.qhelp" />
 
 </overview>
 <recommendation>

cpp/ql/src/Critical/MemoryNeverFreed.qhelp

@@ -10,7 +10,7 @@ This rule finds calls to the <code>alloc</code> family of functions without a co
 This leads to memory leaks.
 </p>
 
-<include src="aliasAnalysisWarning.qhelp" />
+<include src="aliasAnalysisWarning.inc.qhelp" />
 
 </overview>
 <recommendation>

cpp/ql/src/Critical/MissingNegativityTest.qhelp

@@ -16,7 +16,7 @@ buffer overruns.
 The query looks only at the return values of functions that may return a negative value (not all functions).
 </p>
 
-<include src="dataFlowWarning.qhelp" />
+<include src="dataFlowWarning.inc.qhelp" />
 </overview>
 
 <recommendation>

cpp/ql/src/Critical/NewArrayDeleteMismatch.qhelp

@@ -63,7 +63,7 @@ destructors likely not be called (as previously noted), but the pointer will als
 potentially less of a serious issue than that posed by the first approach, but it should still be avoided.</li>
 </ul>
 
-<include src="pointsToWarning.qhelp" />
+<include src="pointsToWarning.inc.qhelp" />
 
 </overview>
 <recommendation>

cpp/ql/src/Critical/NewDeleteArrayMismatch.qhelp

@@ -18,7 +18,7 @@ an array (which could have header data specifying the length of the array) and w
 element of the 'array', which would likely lead to a segfault due to the invalid header data.
 </p>
 
-<include src="pointsToWarning.qhelp" />
+<include src="pointsToWarning.inc.qhelp" />
 
 </overview>
 <recommendation>

cpp/ql/src/Critical/OverflowCalculated.qhelp

@@ -19,7 +19,7 @@ the data being copied. Buffer overflows can result to anything from a segmentati
 if the array is on stack-allocated memory).
 </p>
 
-<include src="aliasAnalysisWarning.qhelp" />
+<include src="aliasAnalysisWarning.inc.qhelp" />
 </overview>
 
 <recommendation>

cpp/ql/src/Critical/OverflowDestination.qhelp

@@ -14,7 +14,7 @@ Buffer overflows can lead to anything from a segmentation fault to a security vu
 Ensure that the size parameter is derived from the size of the destination buffer, and 
 not the source buffer.</p>
 
-<include src="aliasAnalysisWarning.qhelp" />
+<include src="aliasAnalysisWarning.inc.qhelp" />
 </recommendation>
 
 

cpp/ql/src/Critical/ReturnStackAllocatedObject.qhelp

@@ -12,7 +12,7 @@ the contents of that memory become undefined after that. Clearly, using a pointe
 memory after the function has already returned will have undefined results.
 </p>
 
-<include src="pointsToWarning.qhelp" />
+<include src="pointsToWarning.inc.qhelp" />
 </overview>
 
 <recommendation>

cpp/ql/src/Critical/UseAfterFree.qhelp

@@ -12,7 +12,7 @@ from a segfault to memory corruption that would cause subsequent calls to the dy
 erratically, to a possible security vulnerability.
 </p>
 
-<include src="pointsToWarning.qhelp" />
+<include src="pointsToWarning.inc.qhelp" />
 
 </overview>
 <recommendation>

cpp/ql/src/Diagnostics/ExtractionErrors.ql

@@ -0,0 +1,16 @@
+/**
+ * @name Extraction errors
+ * @description List all extraction errors for files in the source code directory.
+ * @kind diagnostic
+ * @id cpp/diagnostics/extraction-errors
+ */
+
+import cpp
+import ExtractionErrors
+
+from ExtractionError error
+where
+  error instanceof ExtractionUnknownError or
+  exists(error.getFile().getRelativePath())
+select error, "Extraction failed in " + error.getFile() + " with error " + error.getErrorMessage(),
+  error.getSeverity()

cpp/ql/src/Diagnostics/ExtractionErrors.qll

@@ -0,0 +1,137 @@
+/**
+ * Provides a common hierarchy of all types of errors that can occur during extraction.
+ */
+
+import cpp
+
+/*
+ * A note about how the C/C++ extractor emits diagnostics:
+ * When the extractor frontend encounters an error, it emits a diagnostic message,
+ * that includes a message, location and severity.
+ * However, that process is best-effort and may fail (e.g. due to lack of memory).
+ * Thus, if the extractor emitted at least one diagnostic of severity discretionary
+ * error (or higher), it *also* emits a simple "There was an error during this compilation"
+ * error diagnostic, without location information.
+ * In the common case, this means that a compilation during which one or more errors happened also gets
+ * the catch-all diagnostic.
+ * This diagnostic has the empty string as file path.
+ * We filter out these useless diagnostics if there is at least one error-level diagnostic
+ * for the affected compilation in the database.
+ * Otherwise, we show it to indicate that something went wrong and that we
+ * don't know what exactly happened.
+ */
+
+/**
+ * An error that, if present, leads to a file being marked as non-successfully extracted.
+ */
+class ReportableError extends Diagnostic {
+  ReportableError() {
+    (
+      this instanceof CompilerDiscretionaryError or
+      this instanceof CompilerError or
+      this instanceof CompilerCatastrophe
+    ) and
+    // Filter for the catch-all diagnostic, see note above.
+    not this.getFile().getAbsolutePath() = ""
+  }
+}
+
+private newtype TExtractionError =
+  TReportableError(ReportableError err) or
+  TCompilationFailed(Compilation c, File f) {
+    f = c.getAFileCompiled() and not c.normalTermination()
+  } or
+  // Show the catch-all diagnostic (see note above) only if we haven't seen any other error-level diagnostic
+  // for that compilation
+  TUnknownError(CompilerError err) {
+    not exists(ReportableError e | e.getCompilation() = err.getCompilation())
+  }
+
+/**
+ * Superclass for the extraction error hierarchy.
+ */
+class ExtractionError extends TExtractionError {
+  /** Gets the string representation of the error. */
+  string toString() { none() }
+
+  /** Gets the error message for this error. */
+  string getErrorMessage() { none() }
+
+  /** Gets the file this error occured in. */
+  File getFile() { none() }
+
+  /** Gets the location this error occured in. */
+  Location getLocation() { none() }
+
+  /** Gets the SARIF severity of this error. */
+  int getSeverity() {
+    // Unfortunately, we can't distinguish between errors and fatal errors in SARIF,
+    // so all errors have severity 2.
+    result = 2
+  }
+}
+
+/**
+ * An unrecoverable extraction error, where extraction was unable to finish.
+ * This can be caused by a multitude of reasons, for example:
+ *  - hitting a frontend assertion
+ *  - crashing due to dereferencing an invalid pointer
+ *  - stack overflow
+ *  - out of memory
+ */
+class ExtractionUnrecoverableError extends ExtractionError, TCompilationFailed {
+  Compilation c;
+  File f;
+
+  ExtractionUnrecoverableError() { this = TCompilationFailed(c, f) }
+
+  override string toString() {
+    result = "Unrecoverable extraction error while compiling " + f.toString()
+  }
+
+  override string getErrorMessage() { result = "unrecoverable compilation failure." }
+
+  override File getFile() { result = f }
+
+  override Location getLocation() { result = f.getLocation() }
+}
+
+/**
+ * A recoverable extraction error.
+ * These are compiler errors from the frontend.
+ * Upon encountering one of these, we still continue extraction, but the
+ * database will be incomplete for that file.
+ */
+class ExtractionRecoverableError extends ExtractionError, TReportableError {
+  ReportableError err;
+
+  ExtractionRecoverableError() { this = TReportableError(err) }
+
+  override string toString() { result = "Recoverable extraction error: " + err }
+
+  override string getErrorMessage() { result = err.getFullMessage() }
+
+  override File getFile() { result = err.getFile() }
+
+  override Location getLocation() { result = err.getLocation() }
+}
+
+/**
+ * An unknown error happened during extraction.
+ * These are only displayed if we know that we encountered an error during extraction,
+ * but, for some reason, failed to emit a proper diagnostic with location information
+ * and error message.
+ */
+class ExtractionUnknownError extends ExtractionError, TUnknownError {
+  CompilerError err;
+
+  ExtractionUnknownError() { this = TUnknownError(err) }
+
+  override string toString() { result = "Unknown extraction error: " + err }
+
+  override string getErrorMessage() { result = err.getFullMessage() }
+
+  override File getFile() { result = err.getFile() }
+
+  override Location getLocation() { result = err.getLocation() }
+}

cpp/ql/src/Diagnostics/FailedExtractorInvocations.ql

@@ -0,0 +1,22 @@
+/**
+ * @name Failed extractor invocations
+ * @description Gives the command line of compilations for which extraction did not run to completion.
+ * @kind diagnostic
+ * @id cpp/diagnostics/failed-extractor-invocations
+ */
+
+import cpp
+
+class AnonymousCompilation extends Compilation {
+  override string toString() { result = "<compilation>" }
+}
+
+string describe(Compilation c) {
+  if c.getArgument(1) = "--mimic"
+  then result = "compiler invocation " + concat(int i | i > 1 | c.getArgument(i), " " order by i)
+  else result = "extractor invocation " + concat(int i | | c.getArgument(i), " " order by i)
+}
+
+from Compilation c
+where not c.normalTermination()
+select c, "Extraction aborted for " + describe(c), 2

cpp/ql/src/Diagnostics/SuccessfullyExtractedFiles.ql

@@ -0,0 +1,15 @@
+/**
+ * @name Successfully extracted files
+ * @description Lists all files in the source code directory that were extracted without encountering an error in the file.
+ * @kind diagnostic
+ * @id cpp/diagnostics/successfully-extracted-files
+ */
+
+import cpp
+import ExtractionErrors
+
+from File f
+where
+  not exists(ExtractionError e | e.getFile() = f) and
+  exists(f.getRelativePath())
+select f, ""

cpp/ql/src/Likely Bugs/Leap Year/Adding365DaysPerYear.qhelp

@@ -3,7 +3,7 @@
   "qhelp.dtd">
 <qhelp>
 <overview>
-  <include src="LeapYear.qhelp" />
+  <include src="LeapYear.inc.qhelp" />
 
 <p>When performing arithmetic operations on a variable that represents a date, leap years must be taken into account.
 It is not safe to assume that a year is 365 days long.</p>

cpp/ql/src/Likely Bugs/Leap Year/UncheckedLeapYearAfterYearModification.qhelp

@@ -3,7 +3,7 @@
   "qhelp.dtd">
 <qhelp>
 <overview>
-  <include src="LeapYear.qhelp" />
+  <include src="LeapYear.inc.qhelp" />
   
 <p>When performing arithmetic operations on a variable that represents a year, it is important to consider that the resulting value may not be a valid date.</p>
 <p>The typical example is doing simple year arithmetic (i.e. <code>date.year++</code>) without considering if the resulting value will be a valid date or not.</p>

cpp/ql/src/Likely Bugs/Leap Year/UncheckedReturnValueForTimeFunctions.qhelp

@@ -3,7 +3,7 @@
   "qhelp.dtd">
 <qhelp>
 <overview>
-  <include src="LeapYear.qhelp" />
+  <include src="LeapYear.inc.qhelp" />
   
 <p>When using a function that transforms a date structure, and the year on the input argument for the API has been manipulated, it is important to check for the return value of the function to make sure it succeeded.</p>
 <p>Otherwise, the function may have failed, and the output parameter may contain invalid data that can cause any number of problems on the affected system.</p>

cpp/ql/src/Likely Bugs/Leap Year/UnsafeArrayForDaysOfYear.qhelp

@@ -3,7 +3,7 @@
   "qhelp.dtd">
 <qhelp>
 <overview>
-  <include src="LeapYear.qhelp" />
+  <include src="LeapYear.inc.qhelp" />
 
 <p>This query helps to detect when a developer allocates an array or other fixed-length data structure such as <code>std::vector</code> with 365 elements – one for each day of the year.</p>
 <p>Since leap years have 366 days, there will be no allocated element on December 31st at the end of a leap year; which will lead to a buffer overflow on a leap year.</p>

cpp/ql/src/Likely Bugs/Likely Typos/AssignWhereCompareMeant.ql

@@ -54,7 +54,7 @@ class BooleanControllingAssignmentInExpr extends BooleanControllingAssignment {
   override predicate isWhitelisted() {
     this.getConversion().(ParenthesisExpr).isParenthesised()
     or
-    // whitelist this assignment if all comparison operations in the expression that this
+    // Allow this assignment if all comparison operations in the expression that this
     // assignment is part of, are not parenthesized. In that case it seems like programmer
     // is fine with unparenthesized comparison operands to binary logical operators, and
     // the parenthesis around this assignment was used to call it out as an assignment.
@@ -62,6 +62,21 @@ class BooleanControllingAssignmentInExpr extends BooleanControllingAssignment {
     forex(ComparisonOperation op | op = getComparisonOperand*(this.getParent+()) |
       not op.isParenthesised()
     )
+    or
+    // Match a pattern like:
+    // ```
+    // if((a = b) && use_value(a)) { ... }
+    // ```
+    // where the assignment is meant to update the value of `a` before it's used in some other boolean
+    // subexpression that is guarenteed to be evaluate _after_ the assignment.
+    this.isParenthesised() and
+    exists(LogicalAndExpr parent, Variable var, VariableAccess access |
+      var = this.getLValue().(VariableAccess).getTarget() and
+      access = var.getAnAccess() and
+      not access.isUsedAsLValue() and
+      parent.getRightOperand() = access.getParent*() and
+      parent.getLeftOperand() = this.getParent*()
+    )
   }
 }
 

cpp/ql/src/Metrics/Dependencies/ExternalDependencies.ql

@@ -5,7 +5,6 @@
  * @kind treemap
  * @treemap.warnOn highValues
  * @metricType externalDependency
- * @precision medium
  * @id cpp/external-dependencies
  * @tags modularity
  */

cpp/ql/src/Metrics/Files/FLinesOfCode.ql

@@ -7,7 +7,6 @@
  * @treemap.warnOn highValues
  * @metricType file
  * @metricAggregate avg sum max
- * @precision very-high
  * @id cpp/lines-of-code-in-files
  * @tags maintainability
  *       complexity

cpp/ql/src/Metrics/Files/FLinesOfCommentedOutCode.ql

@@ -5,7 +5,6 @@
  * @treemap.warnOn highValues
  * @metricType file
  * @metricAggregate avg sum max
- * @precision high
  * @id cpp/lines-of-commented-out-code-in-files
  * @tags documentation
  */

cpp/ql/src/Metrics/Files/FLinesOfComments.ql

@@ -7,7 +7,6 @@
  * @treemap.warnOn lowValues
  * @metricType file
  * @metricAggregate avg sum max
- * @precision very-high
  * @id cpp/lines-of-comments-in-files
  * @tags maintainability
  *       documentation

cpp/ql/src/Metrics/Files/FLinesOfDuplicatedCode.ql

@@ -8,7 +8,6 @@
  * @treemap.warnOn highValues
  * @metricType file
  * @metricAggregate avg sum max
- * @precision high
  * @id cpp/duplicated-lines-in-files
  * @tags testability
  *       modularity

cpp/ql/src/Metrics/Files/FNumberOfTests.ql

@@ -5,7 +5,6 @@
  * @treemap.warnOn lowValues
  * @metricType file
  * @metricAggregate avg sum max
- * @precision medium
  * @id cpp/tests-in-files
  * @tags maintainability
  */

cpp/ql/src/Security/CWE/CWE-014/MemsetMayBeDeleted.ql

@@ -38,23 +38,38 @@ predicate isNonEscapingArgument(Expr escaped) {
   )
 }
 
-from FunctionCall call, LocalVariable v, MemsetFunction memset
-where
-  call.getTarget() = memset and
-  not isFromMacroDefinition(call) and
-  // `v` escapes as the argument to `memset`
-  variableAddressEscapesTree(v.getAnAccess(), call.getArgument(0).getFullyConverted()) and
-  // ... and `v` doesn't escape anywhere else.
-  forall(Expr escape | variableAddressEscapesTree(v.getAnAccess(), escape) |
-    isNonEscapingArgument(escape)
-  ) and
+pragma[noinline]
+predicate callToMemsetWithRelevantVariable(
+  LocalVariable v, VariableAccess acc, FunctionCall call, MemsetFunction memset
+) {
   not v.isStatic() and
   // Reference-typed variables get special treatment in `variableAddressEscapesTree` so we leave them
   // out of this query.
   not v.getUnspecifiedType() instanceof ReferenceType and
-  // `v` is not only just used in the call to `memset`.
-  exists(Access acc |
-    acc = v.getAnAccess() and not call.getArgument(0).getAChild*() = acc and not acc.isUnevaluated()
+  call.getTarget() = memset and
+  acc = v.getAnAccess() and
+  // `v` escapes as the argument to `memset`
+  variableAddressEscapesTree(acc, call.getArgument(0).getFullyConverted())
+}
+
+pragma[noinline]
+predicate relevantVariable(LocalVariable v, FunctionCall call, MemsetFunction memset) {
+  exists(VariableAccess acc, VariableAccess anotherAcc |
+    callToMemsetWithRelevantVariable(v, acc, call, memset) and
+    // `v` is not only just used in the call to `memset`.
+    anotherAcc = v.getAnAccess() and
+    acc != anotherAcc and
+    not anotherAcc.isUnevaluated()
+  )
+}
+
+from FunctionCall call, LocalVariable v, MemsetFunction memset
+where
+  relevantVariable(v, call, memset) and
+  not isFromMacroDefinition(call) and
+  // `v` doesn't escape anywhere else.
+  forall(Expr escape | variableAddressEscapesTree(v.getAnAccess(), escape) |
+    isNonEscapingArgument(escape)
   ) and
   // There is no later use of `v`.
   not v.getAnAccess() = call.getASuccessor*() and

cpp/ql/src/Security/CWE/CWE-311/CleartextBufferWrite.qhelp

@@ -2,4 +2,4 @@
   "-//Semmle//qhelp//EN"
   "qhelp.dtd">
 <qhelp>
-<include src="CleartextStorage.qhelp" /></qhelp>
+<include src="CleartextStorage.inc.qhelp" /></qhelp>

cpp/ql/src/Security/CWE/CWE-311/CleartextFileWrite.qhelp

@@ -2,4 +2,4 @@
   "-//Semmle//qhelp//EN"
   "qhelp.dtd">
 <qhelp>
-<include src="CleartextStorage.qhelp" /></qhelp>
+<include src="CleartextStorage.inc.qhelp" /></qhelp>

cpp/ql/src/Security/CWE/CWE-428/UnsafeCreateProcessCall.ql

@@ -93,7 +93,7 @@ class QuotedCommandInCreateProcessFunctionConfiguration extends DataFlow2::Confi
 
 bindingset[s]
 predicate isQuotedOrNoSpaceApplicationNameOnCmd(string s) {
-  s.regexpMatch("\"([^\"])*\"(\\s|.)*") // The first element (path) is quoted
+  s.regexpMatch("\"([^\"])*\"[\\s\\S]*") // The first element (path) is quoted
   or
   s.regexpMatch("[^\\s]+") // There are no spaces in the string
 }

cpp/ql/src/Summary/LinesOfCode.ql

@@ -0,0 +1,11 @@
+/**
+ * @id cpp/summary/lines-of-code
+ * @name Total lines of C/C++ code in the database
+ * @description The total number of lines of C/C++ code across all files, including system headers, libraries, and auto-generated files. This is a useful metric of the size of a database. For all files that were seen during the build, this query counts the lines of code, excluding whitespace or comments.
+ * @kind metric
+ * @tags summary
+ */
+
+import cpp
+
+select sum(File f | f.fromSource() | f.getMetrics().getNumberOfLinesOfCode())

cpp/ql/src/experimental/Security/CWE/CWE-020/LateCheckOfFunctionArgument.c

@@ -0,0 +1,7 @@
+if(len<0) return 1;
+memset(dest, source, len); // GOOD: variable `len` checked before call
+
+...
+
+memset(dest, source, len); // BAD: variable `len` checked after call
+if(len<0) return 1;

cpp/ql/src/experimental/Security/CWE/CWE-020/LateCheckOfFunctionArgument.qhelp

@@ -0,0 +1,28 @@
+<!DOCTYPE qhelp PUBLIC
+  "-//Semmle//qhelp//EN"
+  "qhelp.dtd">
+<qhelp>
+<overview>
+<p>Checking the function argument after calling the function itself. This situation looks suspicious and requires the attention of the developer. It may be necessary to add validation before calling the function</p>
+
+
+</overview>
+<recommendation>
+
+<p>We recommend checking before calling the function.</p>
+
+</recommendation>
+<example>
+<p>The following example demonstrates an erroneous and fixed use of function argument validation.</p>
+<sample src="LateCheckOfFunctionArgument.c" />
+
+</example>
+<references>
+
+<li>
+  CWE Common Weakness Enumeration:
+  <a href="https://cwe.mitre.org/data/definitions/20.html"> CWE-20: Improper Input Validation</a>.
+</li>
+
+</references>
+</qhelp>

cpp/ql/src/experimental/Security/CWE/CWE-020/LateCheckOfFunctionArgument.ql

@@ -0,0 +1,66 @@
+/**
+ * @name Late Check Of Function Argument
+ * @description --Checking the function argument after calling the function itself.
+ *              --This situation looks suspicious and requires the attention of the developer.
+ *              --It may be necessary to add validation before calling the function.
+ * @kind problem
+ * @id cpp/late-check-of-function-argument
+ * @problem.severity warning
+ * @precision medium
+ * @tags correctness
+ *       security
+ *       external/cwe/cwe-20
+ */
+
+import cpp
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+/** Holds for a function `f` that has an argument at index `apos` used for positioning in a buffer. */
+predicate numberArgument(Function f, int apos) {
+  f.hasGlobalOrStdName("write") and apos = 2
+  or
+  f.hasGlobalOrStdName("read") and apos = 2
+  or
+  f.hasGlobalOrStdName("lseek") and apos = 1
+  or
+  f.hasGlobalOrStdName("memmove") and apos = 2
+  or
+  f.hasGlobalOrStdName("memset") and apos = 2
+  or
+  f.hasGlobalOrStdName("memcpy") and apos = 2
+  or
+  f.hasGlobalOrStdName("memcmp") and apos = 2
+  or
+  f.hasGlobalOrStdName("strncat") and apos = 2
+  or
+  f.hasGlobalOrStdName("strncpy") and apos = 2
+  or
+  f.hasGlobalOrStdName("strncmp") and apos = 2
+  or
+  f.hasGlobalOrStdName("snprintf") and apos = 1
+  or
+  f.hasGlobalOrStdName("strndup") and apos = 2
+}
+
+class IfCompareWithZero extends IfStmt {
+  IfCompareWithZero() { this.getCondition().(RelationalOperation).getAChild().getValue() = "0" }
+
+  Expr noZerroOperand() {
+    if this.getCondition().(RelationalOperation).getGreaterOperand().getValue() = "0"
+    then result = this.getCondition().(RelationalOperation).getLesserOperand()
+    else result = this.getCondition().(RelationalOperation).getGreaterOperand()
+  }
+}
+
+from FunctionCall fc, IfCompareWithZero ifc, int na
+where
+  numberArgument(fc.getTarget(), na) and
+  globalValueNumber(fc.getArgument(na)) = globalValueNumber(ifc.noZerroOperand()) and
+  dominates(fc, ifc) and
+  not exists(IfStmt ifc1 |
+    dominates(ifc1, fc) and
+    globalValueNumber(fc.getArgument(na)) = globalValueNumber(ifc1.getCondition().getAChild*())
+  )
+select fc,
+  "The value of argument '$@' appears to be checked after the call, rather than before it.",
+  fc.getArgument(na), fc.getArgument(na).toString()

cpp/ql/src/experimental/Security/CWE/CWE-570/WrongInDetectingAndHandlingMemoryAllocationErrors.ql

@@ -72,9 +72,9 @@ class WrongCheckErrorOperatorNew extends FunctionCall {
   }
 
   /**
-   * Holds if `(std::nothrow)` exists in call `operator new`.
+   * Holds if `(std::nothrow)` or `(std::noexcept)` exists in call `operator new`.
    */
-  predicate isExistsNothrow() { this.getAChild().toString() = "nothrow" }
+  predicate isExistsNothrow() { getTarget().isNoExcept() or getTarget().isNoThrow() }
 }
 
 from WrongCheckErrorOperatorNew op

cpp/ql/src/experimental/Security/CWE/CWE-691/InsufficientControlFlowManagementWhenUsingBitOperations.c

@@ -0,0 +1,4 @@
+if(len>0 & memset(buf,0,len)) return 1; // BAD: `memset` will be called regardless of the value of the `len` variable. moreover, one cannot be sure that it will happen after verification
+...
+if(len>0 && memset(buf,0,len)) return 1; // GOOD: `memset` will be called after the `len` variable has been checked.
+...

cpp/ql/src/experimental/Security/CWE/CWE-691/InsufficientControlFlowManagementWhenUsingBitOperations.qhelp

@@ -0,0 +1,28 @@
+<!DOCTYPE qhelp PUBLIC
+  "-//Semmle//qhelp//EN"
+  "qhelp.dtd">
+<qhelp>
+<overview>
+<p>Using bitwise operations can be a mistake in some situations. For example, if parameters are evaluated in an expression and the function should be called only upon certain test results. These bitwise operations look suspicious and require developer attention.</p>
+
+
+</overview>
+<recommendation>
+
+<p>We recommend that you evaluate the correctness of using the specified bit operations.</p>
+
+</recommendation>
+<example>
+<p>The following example demonstrates the erroneous and fixed use of bit and logical operations.</p>
+<sample src="InsufficientControlFlowManagementWhenUsingBitOperations.c" />
+
+</example>
+<references>
+
+<li>
+  CWE Common Weakness Enumeration:
+  <a href="https://cwe.mitre.org/data/definitions/691.html"> CWE-691: Insufficient Control Flow Management</a>.
+</li>
+
+</references>
+</qhelp>

cpp/ql/src/experimental/Security/CWE/CWE-691/InsufficientControlFlowManagementWhenUsingBitOperations.ql

@@ -0,0 +1,78 @@
+/**
+ * @name Errors When Using Bit Operations
+ * @description Unlike the binary operations `||` and `&&`, there is no sequence point after evaluating an
+ *              operand of a bitwise operation like `|` or `&`. If left-to-right evaluation is expected this may be confusing.
+ * @kind problem
+ * @id cpp/errors-when-using-bit-operations
+ * @problem.severity warning
+ * @precision medium
+ * @tags correctness
+ *       security
+ *       external/cwe/cwe-691
+ */
+
+import cpp
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+/**
+ * Dangerous uses of bit operations.
+ * For example: `if(intA>0 & intA<10 & charBuf&myFunc(charBuf[intA]))`.
+ * In this case, the function will be called in any case, and even the sequence of the call is not guaranteed.
+ */
+class DangerousBitOperations extends BinaryBitwiseOperation {
+  FunctionCall bfc;
+
+  /**
+   * The assignment indicates the conscious use of the bit operator.
+   * Use in comparison, conversion, or return value indicates conscious use of the bit operator.
+   * The use of shifts and bitwise operations on any element of an expression indicates a conscious use of the bitwise operator.
+   */
+  DangerousBitOperations() {
+    bfc = this.getRightOperand() and
+    not this.getParent*() instanceof Assignment and
+    not this.getParent*() instanceof Initializer and
+    not this.getParent*() instanceof ReturnStmt and
+    not this.getParent*() instanceof EqualityOperation and
+    not this.getParent*() instanceof UnaryLogicalOperation and
+    not this.getParent*() instanceof BinaryLogicalOperation and
+    not this.getAChild*() instanceof BitwiseXorExpr and
+    not this.getAChild*() instanceof LShiftExpr and
+    not this.getAChild*() instanceof RShiftExpr
+  }
+
+  /** Holds when part of a bit expression is used in a logical operation. */
+  predicate useInLogicalOperations() {
+    exists(BinaryLogicalOperation blop, Expr exp |
+      blop.getAChild*() = exp and
+      exp.(FunctionCall).getTarget() = bfc.getTarget() and
+      not exp.getParent() instanceof ComparisonOperation and
+      not exp.getParent() instanceof BinaryBitwiseOperation
+    )
+  }
+
+  /** Holds when part of a bit expression is used as part of another supply. For example, as an argument to another function. */
+  predicate useInOtherCalls() {
+    bfc.hasQualifier() or
+    bfc.getTarget() instanceof Operator or
+    exists(FunctionCall fc | fc.getAnArgument().getAChild*() = this) or
+    bfc.getTarget() instanceof BuiltInFunction
+  }
+
+  /** Holds when the bit expression contains both arguments and a function call. */
+  predicate dangerousArgumentChecking() {
+    not this.getLeftOperand() instanceof Call and
+    globalValueNumber(this.getLeftOperand().getAChild*()) = globalValueNumber(bfc.getAnArgument())
+  }
+
+  /** Holds when function calls are present in the bit expression. */
+  predicate functionCallsInBitsExpression() {
+    this.getLeftOperand().getAChild*() instanceof FunctionCall
+  }
+}
+
+from DangerousBitOperations dbo
+where
+  not dbo.useInOtherCalls() and
+  dbo.useInLogicalOperations() and
+  (not dbo.functionCallsInBitsExpression() or dbo.dangerousArgumentChecking())
+select dbo, "This bitwise operation appears in a context where a Boolean operation is expected."

cpp/ql/src/experimental/Security/CWE/CWE-783/OperatorPrecedenceLogicErrorWhenUseBoolType.c

@@ -0,0 +1,11 @@
+if(len=funcReadData()==0) return 1; // BAD: variable `len` will not equal the value returned by function `funcReadData()`
+...
+if((len=funcReadData())==0) return 1; // GOOD: variable `len` equal the value returned by function `funcReadData()`
+...
+bool a=true;
+a++;// BAD: variable `a` does not change its meaning
+bool b;
+b=-a;// BAD: variable `b` equal `true`
+...
+a=false;// GOOD: variable `a` equal `false`
+b=!a;// GOOD: variable `b` equal `false`

cpp/ql/src/experimental/Security/CWE/CWE-783/OperatorPrecedenceLogicErrorWhenUseBoolType.qhelp

@@ -0,0 +1,28 @@
+<!DOCTYPE qhelp PUBLIC
+  "-//Semmle//qhelp//EN"
+  "qhelp.dtd">
+<qhelp>
+<overview>
+<p>Finding places of confusing use of boolean type. For example, a unary minus does not work before a boolean type and an increment always gives true.</p>
+
+
+</overview>
+<recommendation>
+
+<p>we recommend making the code simpler.</p>
+
+</recommendation>
+<example>
+<p>The following example demonstrates erroneous and fixed methods for using a boolean data type.</p>
+<sample src="OperatorPrecedenceLogicErrorWhenUseBoolType.c" />
+
+</example>
+<references>
+
+<li>
+  CERT C Coding Standard:
+  <a href="https://wiki.sei.cmu.edu/confluence/display/c/EXP00-C.+Use+parentheses+for+precedence+of+operation">EXP00-C. Use parentheses for precedence of operation</a>.
+</li>
+
+</references>
+</qhelp>

cpp/ql/src/experimental/Security/CWE/CWE-783/OperatorPrecedenceLogicErrorWhenUseBoolType.ql

@@ -0,0 +1,54 @@
+/**
+ * @name Operator Precedence Logic Error When Use Bool Type
+ * @description --Finding places of confusing use of boolean type.
+ *              --For example, a unary minus does not work before a boolean type and an increment always gives true.
+ * @kind problem
+ * @id cpp/operator-precedence-logic-error-when-use-bool-type
+ * @problem.severity warning
+ * @precision medium
+ * @tags correctness
+ *       security
+ *       external/cwe/cwe-783
+ *       external/cwe/cwe-480
+ */
+
+import cpp
+import semmle.code.cpp.valuenumbering.HashCons
+
+/** Holds if `exp` increments a boolean value. */
+predicate incrementBoolType(IncrementOperation exp) {
+  exp.getOperand().getType() instanceof BoolType
+}
+
+/** Holds if `exp` applies the unary minus operator to a boolean type. */
+predicate revertSignBoolType(UnaryMinusExpr exp) {
+  exp.getAnOperand().getType() instanceof BoolType and
+  exp.getFullyConverted().getType() instanceof BoolType
+}
+
+/** Holds, if this is an expression, uses comparison and assignment outside of execution precedence. */
+predicate assignBoolType(Expr exp) {
+  exists(ComparisonOperation co |
+    exp.(AssignExpr).getRValue() = co and
+    exp.isCondition() and
+    not co.isParenthesised() and
+    not exp.(AssignExpr).getLValue().getType() instanceof BoolType and
+    not exists(Expr exbl |
+      hashCons(exbl.(AssignExpr).getLValue()) = hashCons(exp.(AssignExpr).getLValue()) and
+      not exbl.isCondition() and
+      exbl.(AssignExpr).getRValue().getType() instanceof BoolType and
+      exbl.(AssignExpr).getLValue().getType() = exp.(AssignExpr).getLValue().getType()
+    ) and
+    co.getLeftOperand() instanceof FunctionCall and
+    not co.getRightOperand().getType() instanceof BoolType and
+    not co.getRightOperand().getValue() = "0" and
+    not co.getRightOperand().getValue() = "1"
+  )
+}
+
+from Expr exp
+where
+  incrementBoolType(exp) or
+  revertSignBoolType(exp) or
+  assignBoolType(exp)
+select exp, "this expression needs attention"

cpp/ql/src/experimental/Security/CWE/CWE-788/AccessOfMemoryLocationAfterEndOfBufferUsingStrlen.ql

@@ -3,7 +3,7 @@
  * @description The expression `buffer [strlen (buffer)] = 0` is potentially dangerous, if the variable `buffer` does not have a terminal zero, then access beyond the bounds of the allocated memory is possible, which will lead to undefined behavior.
  *              If terminal zero is present, then the specified expression is meaningless.
  * @kind problem
- * @id cpp/access-memory-location-after-end-buffer
+ * @id cpp/access-memory-location-after-end-buffer-strlen
  * @problem.severity warning
  * @precision medium
  * @tags correctness

cpp/ql/src/experimental/Security/CWE/CWE-788/AccessOfMemoryLocationAfterEndOfBufferUsingStrncat.ql

@@ -2,7 +2,7 @@
  * @name Access Of Memory Location After The End Of A Buffer Using Strncat
  * @description Calls of the form `strncat(dest, source, sizeof (dest) - strlen (dest))` set the third argument to one more than possible. So when `dest` is full, the expression `sizeof(dest) - strlen (dest)` will be equal to one, and not zero as the programmer might think. Making a call of this type may result in a zero byte being written just outside the `dest` buffer.
  * @kind problem
- * @id cpp/access-memory-location-after-end-buffer
+ * @id cpp/access-memory-location-after-end-buffer-strncat
  * @problem.severity warning
  * @precision medium
  * @tags correctness

cpp/ql/src/external/tests/DefectFilter.ql

@@ -1,12 +0,0 @@
-/**
- * @name Defect filter
- * @description Only include results in large files (200) lines of code, and change the message.
- * @tags filter
- */
-
-import cpp
-import external.DefectFilter
-
-from DefectResult res
-where res.getFile().getMetrics().getNumberOfLinesOfCode() > 200
-select res, "Large files: " + res.getMessage()

cpp/ql/src/external/tests/DefectFromExternalData.ql

@@ -1,18 +0,0 @@
-/**
- * @name Defect from external data
- * @description Insert description here...
- * @kind problem
- * @problem.severity warning
- * @tags external-data
- */
-
-import cpp
-import external.ExternalArtifact
-
-from ExternalData d, File u
-where
-  d.getQueryPath() = "external-data.ql" and
-  u.getShortName() = d.getField(0)
-select u,
-  d.getField(5) + ", " + d.getFieldAsDate(1) + ", " + d.getField(2) + ", " + d.getFieldAsFloat(3) +
-    ", " + d.getFieldAsInt(4) + ": " + d.getNumFields()

cpp/ql/src/external/tests/MetricFilter.ql

@@ -1,12 +0,0 @@
-/**
- * @name Metric filter
- * @description Only include results in large files (200) lines of code.
- * @tags filter
- */
-
-import cpp
-import external.MetricFilter
-
-from MetricResult res
-where res.getFile().getMetrics().getNumberOfLinesOfCode() > 200
-select res, res.getValue()

cpp/ql/src/filters/FilterAutogenerated.ql

@@ -1,16 +0,0 @@
-/**
- * @name Filter: exclude results from files that are autogenerated
- * @description Use this filter to return results only if they are
- *              located in files that are maintained manually.
- * @kind problem
- * @id cpp/autogenerated-filter
- * @tags filter
- */
-
-import cpp
-import semmle.code.cpp.AutogeneratedFile
-import external.DefectFilter
-
-from DefectResult res
-where not res.getFile() instanceof AutogeneratedFile
-select res, res.getMessage()

cpp/ql/src/filters/FilterAutogeneratedForMetric.ql

@@ -1,16 +0,0 @@
-/**
- * @name Metric filter: exclude results from files that are autogenerated
- * @description Use this filter to return results only if they are
- *              located in files that are maintained manually.
- * @kind treemap
- * @id cpp/autogenerated-for-metric-filter
- * @tags filter
- */
-
-import cpp
-import semmle.code.cpp.AutogeneratedFile
-import external.MetricFilter
-
-from MetricResult res
-where not res.getFile() instanceof AutogeneratedFile
-select res, res.getValue()

cpp/ql/src/filters/FromSource.ql

@@ -1,16 +0,0 @@
-/**
- * @name Filter: exclude results from files for which we do not have
- *       source code
- * @description Use this filter to return results only if they are
- *              located in files for which we have source code.
- * @kind problem
- * @id cpp/from-source-filter
- * @tags filter
- */
-
-import cpp
-import external.DefectFilter
-
-from DefectResult res
-where res.getFile().fromSource()
-select res, res.getMessage()

cpp/ql/src/filters/Macros.ql

@@ -1,36 +0,0 @@
-/**
- * @name Filter: exclude results on lines covered by a macro expansion
- * @description Use this filter to return results only when there is no
- *              macro expansion whose location spans all the lines of
- *              the result's location.
- * @kind problem
- * @id cpp/macros-filter
- * @tags filter
- */
-
-import cpp
-import external.DefectFilter
-
-predicate macroLocation(File f, int startLine, int endLine) {
-  exists(MacroInvocation mi, Location l |
-    l = mi.getLocation() and
-    l.getFile() = f and
-    l.getStartLine() = startLine and
-    l.getEndLine() = endLine
-  )
-}
-
-predicate macroCovering(DefectResult r) {
-  exists(File f, int macroStart, int macroEnd, int defectStart, int defectEnd |
-    f = r.getFile() and
-    defectStart = r.getStartLine() and
-    defectEnd = r.getEndLine() and
-    macroLocation(f, macroStart, macroEnd) and
-    macroStart <= defectStart and
-    macroEnd >= defectEnd
-  )
-}
-
-from DefectResult res
-where not macroCovering(res)
-select res, res.getMessage()

cpp/ql/src/jsf/4.05 Libraries/AV Rule 24.qhelp

@@ -7,7 +7,7 @@
 <overview>
 
 <!-- Mention that this rule may not be applicable in projects that don't follow the JSF standard. -->
-<include src="../jsfNote.qhelp" />
+<include src="../jsfNote.inc.qhelp" />
 
 <p>
 This query highlights calls to the standard library functions <code>abort, exit, getenv</code> and <code>system</code>.

cpp/ql/src/jsf/4.10 Classes/AV Rule 79.ql

@@ -13,6 +13,7 @@
 
 import cpp
 import Critical.NewDelete
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
 
 /**
  * An expression that acquires a resource, and the kind of resource that is acquired.  The
@@ -90,15 +91,17 @@ private predicate exprReleases(Expr e, Expr released, string kind) {
   // `e` is a call to a release function and `released` is the released argument
   releaseExpr(e, released, kind)
   or
-  exists(Function f, int arg |
+  exists(int arg, VariableAccess access, Function f |
     // `e` is a call to a function that releases one of it's parameters,
     // and `released` is the corresponding argument
     (
       e.(FunctionCall).getTarget() = f or
       e.(FunctionCall).getTarget().(MemberFunction).getAnOverridingFunction+() = f
     ) and
+    access = f.getParameter(arg).getAnAccess() and
     e.(FunctionCall).getArgument(arg) = released and
-    exprReleases(_, exprOrDereference(f.getParameter(arg).getAnAccess()), kind)
+    exprReleases(_,
+      pragma[only_bind_into](exprOrDereference(globalValueNumber(access).getAnExpr())), kind)
   )
   or
   exists(Function f, ThisExpr innerThis |
@@ -110,7 +113,7 @@ private predicate exprReleases(Expr e, Expr released, string kind) {
     ) and
     e.(FunctionCall).getQualifier() = exprOrDereference(released) and
     innerThis.getEnclosingFunction() = f and
-    exprReleases(_, innerThis, kind)
+    exprReleases(_, pragma[only_bind_into](globalValueNumber(innerThis).getAnExpr()), kind)
   )
 }
 

cpp/ql/src/jsf/4.10 Classes/AV Rule 85.qhelp

@@ -7,7 +7,7 @@
 <overview>
 
 <!-- Mention that this rule may not be applicable in projects that don't follow the JSF standard. -->
-<include src="../jsfNote.qhelp" />
+<include src="../jsfNote.inc.qhelp" />
 
 <p>
 This query ensures that all operators with opposites (e.g. == and !=) are both defined, and

cpp/ql/src/jsf/4.13 Functions/AV Rule 111.qhelp

@@ -7,7 +7,7 @@
 <overview>
 
 <!-- Mention that this rule may not be applicable in projects that don't follow the JSF standard. -->
-<include src="../jsfNote.qhelp" />
+<include src="../jsfNote.inc.qhelp" />
 
 <p>
 This query highlights return statements that return pointers to an object allocated on the stack. The lifetime
@@ -18,7 +18,7 @@ memory after the function has already returned will have undefined results.
 
 
 <!-- Mention how the results could be probabilistic (uses pointsto) -->
-<include src="../../Critical/pointsToWarning.qhelp" />
+<include src="../../Critical/pointsToWarning.inc.qhelp" />
 
 </overview>
 <recommendation>

cpp/ql/src/jsf/4.13 Functions/AV Rule 114.qhelp

@@ -12,7 +12,7 @@ calling convention for x86, it would be whatever value was in the AX/EAX registe
 assuming the function had a non-float return type that can fit in a machine word.
 </p>
 
-<include src="../../Critical/dataFlowWarning.qhelp" />
+<include src="../../Critical/dataFlowWarning.inc.qhelp" />
 
 <!--/*FALSEPOSITIVE_WARNING*/-->
 

cpp/ql/src/jsf/4.15 Declarations and Definitions/AV Rule 135.qhelp

@@ -7,7 +7,7 @@
 <overview>
 
 <!-- Mention that this rule may not be applicable in projects that don't follow the JSF standard. -->
-<include src="../jsfNote.qhelp" />
+<include src="../jsfNote.inc.qhelp" />
 
 <p>
 This query highlights identifiers in an inner scope that hide (have the same name as) an identifier in an outer scope.

cpp/ql/src/jsf/4.15 Declarations and Definitions/AV Rule 140.qhelp

@@ -7,7 +7,7 @@
 <overview>
 
 <!-- Mention that this rule may not be applicable in projects that don't follow the JSF standard. -->
-<include src="../jsfNote.qhelp" />
+<include src="../jsfNote.inc.qhelp" />
 
 <p>
 This query highlights variables with the <code>register</code> storage class specifier. Modern compilers are now capable of

cpp/ql/src/jsf/4.17 Types/AV Rule 147.qhelp

@@ -7,7 +7,7 @@
 <overview>
 
 <!-- Mention that this rule may not be applicable in projects that don't follow the JSF standard. -->
-<include src="../jsfNote.qhelp" />
+<include src="../jsfNote.inc.qhelp" />
 
 <p>
 This query highlights portions of code that can expose the floating point implementation of the underlying

cpp/ql/src/jsf/4.18 Constants/AV Rule 151.1.qhelp

@@ -7,7 +7,7 @@
 <overview>
 
 <!-- Mention that this rule may not be applicable in projects that don't follow the JSF standard. -->
-<include src="../jsfNote.qhelp" />
+<include src="../jsfNote.inc.qhelp" />
 
 <p>
 This query highlights string literals that are assigned to a non-<code>const</code> variable. String literals

cpp/ql/src/jsf/4.20 Unions and Bit Fields/AV Rule 154.qhelp

@@ -7,7 +7,7 @@
 <overview>
 
 <!-- Mention that this rule may not be applicable in projects that don't follow the JSF standard. -->
-<include src="../jsfNote.qhelp" />
+<include src="../jsfNote.inc.qhelp" />
 
 <p>
 This query finds bit fields with members that are not explicitly declared to be unsigned.

cpp/ql/src/jsf/4.21 Operators/AV Rule 165.qhelp

@@ -7,7 +7,7 @@
 <overview>
 
 <!-- Mention that this rule may not be applicable in projects that don't follow the JSF standard. -->
-<include src="../jsfNote.qhelp" />
+<include src="../jsfNote.inc.qhelp" />
 
 <p>
 This query finds unsigned values that are being negated. Behavior is undefined in such cases.

cpp/ql/src/jsf/4.24 Control Flow Structures/AV Rule 189.qhelp

@@ -6,7 +6,7 @@
 <overview>
 
 <!-- Mention that this rule may not be applicable in projects that don't follow the JSF standard. -->
-<include src="../jsfNote.qhelp" />
+<include src="../jsfNote.inc.qhelp" />
 
 <p>Use of goto statements makes code more difficult to understand and maintain. Consequently, the use 
 of goto statements is deprecated except as a mechanism for breaking out of multiple nested loops. 

cpp/ql/src/semmle/code/cpp/Diagnostics.qll

@@ -6,6 +6,9 @@ import semmle.code.cpp.Location
 
 /** A compiler-generated error, warning or remark. */
 class Diagnostic extends Locatable, @diagnostic {
+  /** Gets the compilation that generated this diagnostic. */
+  Compilation getCompilation() { diagnostic_for(underlyingElement(this), result, _, _) }
+
   /**
    * Gets the severity of the message, on a range from 1 to 5: 1=remark,
    * 2=warning, 3=discretionary error, 4=error, 5=catastrophic error.

cpp/ql/src/semmle/code/cpp/File.qll

@@ -276,7 +276,10 @@ class File extends Container, @file {
       c.getAFileCompiled() = this and
       (
         c.getAnArgument() = "--microsoft" or
-        c.getAnArgument().toLowerCase().replaceAll("\\", "/").matches("%/cl.exe")
+        c.getAnArgument()
+            .toLowerCase()
+            .replaceAll("\\", "/")
+            .matches(["%/cl.exe", "%/clang-cl.exe"])
       )
     )
     or

cpp/ql/src/semmle/code/cpp/Location.qll

@@ -72,6 +72,7 @@ class Location extends @location {
   }
 
   /** Holds if `this` comes on a line strictly before `l`. */
+  pragma[inline]
   predicate isBefore(Location l) {
     this.getFile() = l.getFile() and this.getEndLine() < l.getStartLine()
   }

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

@@ -15,6 +15,7 @@
  */
 
 private import cpp
+private import semmle.code.cpp.models.interfaces.PointerWrapper
 
 /**
  * Holds if `f` is an instantiation of the `std::move` or `std::forward`
@@ -94,6 +95,12 @@ private predicate pointerToPointerStep(Expr pointerIn, Expr pointerOut) {
 
 private predicate lvalueToReferenceStep(Expr lvalueIn, Expr referenceOut) {
   lvalueIn.getConversion() = referenceOut.(ReferenceToExpr)
+  or
+  exists(PointerWrapper wrapper, Call call | call = referenceOut |
+    referenceOut.getUnspecifiedType() instanceof ReferenceType and
+    call = wrapper.getAnUnwrapperFunction().getACallToThisFunction() and
+    lvalueIn = call.getQualifier().getFullyConverted()
+  )
 }
 
 private predicate referenceToLvalueStep(Expr referenceIn, Expr lvalueOut) {
@@ -106,6 +113,13 @@ private predicate referenceToPointerStep(Expr referenceIn, Expr pointerOut) {
       stdAddressOf(call.getTarget()) and
       referenceIn = call.getArgument(0).getFullyConverted()
     )
+  or
+  exists(CopyConstructor copy, Call call | call = pointerOut |
+    copy.getDeclaringType() instanceof PointerWrapper and
+    call.getTarget() = copy and
+    // The 0'th argument is the value being copied.
+    referenceIn = call.getArgument(0).getFullyConverted()
+  )
 }
 
 private predicate referenceToReferenceStep(Expr referenceIn, Expr referenceOut) {
@@ -190,6 +204,19 @@ private predicate pointerToUpdate(Expr pointer, Expr outer, ControlFlowNode node
         // See the `lvalueToUpdate` case for an explanation of this conjunct.
         call.getType().isDeeplyConstBelow()
       )
+      or
+      // Pointer wrappers behave as raw pointers for dataflow purposes.
+      outer = call.getAnArgument().getFullyConverted() and
+      exists(PointerWrapper wrapper | wrapper = outer.getType().stripTopLevelSpecifiers() |
+        not wrapper.pointsToConst()
+      )
+      or
+      outer = call.getQualifier().getFullyConverted() and
+      outer.getUnspecifiedType() instanceof PointerWrapper and
+      not (
+        call.getTarget().hasSpecifier("const") and
+        call.getType().isDeeplyConstBelow()
+      )
     )
     or
     exists(PointerFieldAccess fa |
@@ -218,7 +245,9 @@ private predicate referenceToUpdate(Expr reference, Expr outer, ControlFlowNode
     not stdIdentityFunction(call.getTarget()) and
     not stdAddressOf(call.getTarget()) and
     exists(ReferenceType rt | rt = outer.getType().stripTopLevelSpecifiers() |
-      not rt.getBaseType().isConst()
+      not rt.getBaseType().isConst() or
+      rt.getBaseType().getUnspecifiedType() =
+        any(PointerWrapper wrapper | not wrapper.pointsToConst())
     )
   ) and
   reference = outer

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

@@ -207,18 +207,6 @@ private predicate fullBarrier(Node node, Configuration config) {
   )
 }
 
-private class AdditionalFlowStepSource extends Node {
-  AdditionalFlowStepSource() { any(Configuration c).isAdditionalFlowStep(this, _) }
-}
-
-pragma[noinline]
-private predicate isAdditionalFlowStep(
-  AdditionalFlowStepSource node1, Node node2, DataFlowCallable callable1, Configuration config
-) {
-  config.isAdditionalFlowStep(node1, node2) and
-  callable1 = node1.getEnclosingCallable()
-}
-
 /**
  * Holds if data can flow in one local step from `node1` to `node2`.
  */
@@ -237,7 +225,8 @@ private predicate localFlowStep(Node node1, Node node2, Configuration config) {
  * Holds if the additional step from `node1` to `node2` does not jump between callables.
  */
 private predicate additionalLocalFlowStep(Node node1, Node node2, Configuration config) {
-  isAdditionalFlowStep(node1, node2, node2.getEnclosingCallable(), config) and
+  config.isAdditionalFlowStep(node1, node2) and
+  getNodeEnclosingCallable(node1) = getNodeEnclosingCallable(node2) and
   not outBarrier(node1, config) and
   not inBarrier(node2, config) and
   not fullBarrier(node1, config) and
@@ -259,14 +248,12 @@ private predicate jumpStep(Node node1, Node node2, Configuration config) {
  * Holds if the additional step from `node1` to `node2` jumps between callables.
  */
 private predicate additionalJumpStep(Node node1, Node node2, Configuration config) {
-  exists(DataFlowCallable callable1 |
-    isAdditionalFlowStep(node1, node2, callable1, config) and
-    node2.getEnclosingCallable() != callable1 and
-    not outBarrier(node1, config) and
-    not inBarrier(node2, config) and
-    not fullBarrier(node1, config) and
-    not fullBarrier(node2, config)
-  )
+  config.isAdditionalFlowStep(node1, node2) and
+  getNodeEnclosingCallable(node1) != getNodeEnclosingCallable(node2) and
+  not outBarrier(node1, config) and
+  not inBarrier(node2, config) and
+  not fullBarrier(node1, config) and
+  not fullBarrier(node2, config)
 }
 
 /**
@@ -457,8 +444,8 @@ private module Stage1 {
     // read
     exists(Node mid, Content c |
       read(node, c, mid) and
-      fwdFlowConsCand(c, unbind(config)) and
-      revFlow(mid, toReturn, config)
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
+      revFlow(mid, toReturn, pragma[only_bind_into](config))
     )
     or
     // flow into a callable
@@ -484,18 +471,18 @@ private module Stage1 {
   pragma[nomagic]
   private predicate revFlowConsCand(Content c, Configuration config) {
     exists(Node mid, Node node |
-      fwdFlow(node, unbind(config)) and
+      fwdFlow(node, pragma[only_bind_into](config)) and
       read(node, c, mid) and
-      fwdFlowConsCand(c, unbind(config)) and
-      revFlow(mid, _, config)
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
+      revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
     )
   }
 
   pragma[nomagic]
   private predicate revFlowStore(Content c, Node node, boolean toReturn, Configuration config) {
     exists(Node mid, TypedContent tc |
-      revFlow(mid, toReturn, config) and
-      fwdFlowConsCand(c, unbind(config)) and
+      revFlow(mid, toReturn, pragma[only_bind_into](config)) and
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
       store(node, tc, mid, _) and
       c = tc.getContent()
     )
@@ -565,8 +552,8 @@ private module Stage1 {
     Node node1, Ap ap1, TypedContent tc, Node node2, DataFlowType contentType, Configuration config
   ) {
     exists(Content c |
-      revFlowIsReadAndStored(c, config) and
-      revFlow(node2, unbind(config)) and
+      revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
+      revFlow(node2, pragma[only_bind_into](config)) and
       store(node1, tc, node2, contentType) and
       c = tc.getContent() and
       exists(ap1)
@@ -575,8 +562,8 @@ private module Stage1 {
 
   pragma[nomagic]
   predicate readStepCand(Node n1, Content c, Node n2, Configuration config) {
-    revFlowIsReadAndStored(c, config) and
-    revFlow(n2, unbind(config)) and
+    revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
+    revFlow(n2, pragma[only_bind_into](config)) and
     read(n1, c, n2)
   }
 
@@ -601,7 +588,7 @@ private module Stage1 {
   ) {
     exists(ReturnNodeExt ret |
       throughFlowNodeCand(ret, config) and
-      callable = ret.getEnclosingCallable() and
+      callable = getNodeEnclosingCallable(ret) and
       kind = ret.getKind()
     )
   }
@@ -614,7 +601,7 @@ private module Stage1 {
     exists(ReturnKindExt kind |
       throughFlowNodeCand(p, config) and
       returnFlowCallableNodeCand(c, kind, config) and
-      p.getEnclosingCallable() = c and
+      getNodeEnclosingCallable(p) = c and
       exists(ap) and
       // we don't expect a parameter to return stored in itself
       not exists(int pos |
@@ -639,9 +626,6 @@ private module Stage1 {
   /* End: Stage 1 logic. */
 }
 
-bindingset[result, b]
-private boolean unbindBool(boolean b) { result != b.booleanNot() }
-
 pragma[noinline]
 private predicate localFlowStepNodeCand1(Node node1, Node node2, Configuration config) {
   Stage1::revFlow(node2, config) and
@@ -778,7 +762,7 @@ private module Stage2 {
   bindingset[result, ap]
   private ApApprox getApprox(Ap ap) { any() }
 
-  private ApNil getApNil(Node node) { any() }
+  private ApNil getApNil(Node node) { PrevStage::revFlow(node, _) and exists(result) }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result = true and exists(tc) and exists(tail) }
@@ -877,16 +861,16 @@ private module Stage2 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -966,7 +950,7 @@ private module Stage2 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -985,7 +969,7 @@ private module Stage2 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -1058,9 +1042,9 @@ private module Stage2 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -1072,9 +1056,9 @@ private module Stage2 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -1127,9 +1111,10 @@ private module Stage2 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -1195,9 +1180,10 @@ private module Stage2 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ unbindBool(ap2), _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -1216,13 +1202,13 @@ private module Stage2 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -1253,8 +1239,8 @@ private predicate flowOutOfCallNodeCand2(
   DataFlowCall call, ReturnNodeExt node1, Node node2, boolean allowsFieldFlow, Configuration config
 ) {
   flowOutOfCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
-  Stage2::revFlow(node2, config) and
-  Stage2::revFlow(node1, unbind(config))
+  Stage2::revFlow(node2, pragma[only_bind_into](config)) and
+  Stage2::revFlow(node1, pragma[only_bind_into](config))
 }
 
 pragma[nomagic]
@@ -1263,8 +1249,8 @@ private predicate flowIntoCallNodeCand2(
   Configuration config
 ) {
   flowIntoCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
-  Stage2::revFlow(node2, config) and
-  Stage2::revFlow(node1, unbind(config))
+  Stage2::revFlow(node2, pragma[only_bind_into](config)) and
+  Stage2::revFlow(node1, pragma[only_bind_into](config))
 }
 
 private module LocalFlowBigStep {
@@ -1319,8 +1305,8 @@ private module LocalFlowBigStep {
   pragma[noinline]
   private predicate additionalLocalFlowStepNodeCand2(Node node1, Node node2, Configuration config) {
     additionalLocalFlowStepNodeCand1(node1, node2, config) and
-    Stage2::revFlow(node1, _, _, false, config) and
-    Stage2::revFlow(node2, _, _, false, unbind(config))
+    Stage2::revFlow(node1, _, _, false, pragma[only_bind_into](config)) and
+    Stage2::revFlow(node2, _, _, false, pragma[only_bind_into](config))
   }
 
   /**
@@ -1337,7 +1323,7 @@ private module LocalFlowBigStep {
   ) {
     not isUnreachableInCall(node2, cc.(LocalCallContextSpecificCall).getCall()) and
     (
-      localFlowEntry(node1, config) and
+      localFlowEntry(node1, pragma[only_bind_into](config)) and
       (
         localFlowStepNodeCand1(node1, node2, config) and
         preservesValue = true and
@@ -1348,24 +1334,24 @@ private module LocalFlowBigStep {
         t = getNodeType(node2)
       ) and
       node1 != node2 and
-      cc.relevantFor(node1.getEnclosingCallable()) and
+      cc.relevantFor(getNodeEnclosingCallable(node1)) and
       not isUnreachableInCall(node1, cc.(LocalCallContextSpecificCall).getCall()) and
-      Stage2::revFlow(node2, unbind(config))
+      Stage2::revFlow(node2, pragma[only_bind_into](config))
       or
       exists(Node mid |
-        localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
+        localFlowStepPlus(node1, mid, preservesValue, t, pragma[only_bind_into](config), cc) and
         localFlowStepNodeCand1(mid, node2, config) and
         not mid instanceof FlowCheckNode and
-        Stage2::revFlow(node2, unbind(config))
+        Stage2::revFlow(node2, pragma[only_bind_into](config))
       )
       or
       exists(Node mid |
-        localFlowStepPlus(node1, mid, _, _, config, cc) and
+        localFlowStepPlus(node1, mid, _, _, pragma[only_bind_into](config), cc) and
         additionalLocalFlowStepNodeCand2(mid, node2, config) and
         not mid instanceof FlowCheckNode and
         preservesValue = false and
         t = getNodeType(node2) and
-        Stage2::revFlow(node2, unbind(config))
+        Stage2::revFlow(node2, pragma[only_bind_into](config))
       )
     )
   }
@@ -1397,7 +1383,9 @@ private module Stage3 {
 
   private ApApprox getApprox(Ap ap) { result = ap.toBoolNonEmpty() }
 
-  private ApNil getApNil(Node node) { result = TFrontNil(getNodeType(node)) }
+  private ApNil getApNil(Node node) {
+    PrevStage::revFlow(node, _) and result = TFrontNil(getNodeType(node))
+  }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result.getHead() = tc and exists(tail) }
@@ -1470,6 +1458,13 @@ private module Stage3 {
     PrevStage::revFlow(node, _, _, apa, config)
   }
 
+  bindingset[result, apa]
+  private ApApprox unbindApa(ApApprox apa) {
+    exists(ApApprox apa0 |
+      apa = pragma[only_bind_into](apa0) and result = pragma[only_bind_into](apa0)
+    )
+  }
+
   /**
    * Holds if `node` is reachable with access path `ap` from a source in the
    * configuration `config`.
@@ -1481,7 +1476,7 @@ private module Stage3 {
   pragma[nomagic]
   predicate fwdFlow(Node node, Cc cc, ApOption argAp, Ap ap, Configuration config) {
     fwdFlow0(node, cc, argAp, ap, config) and
-    flowCand(node, unbindBool(getApprox(ap)), config) and
+    flowCand(node, unbindApa(getApprox(ap)), config) and
     filter(node, ap)
   }
 
@@ -1505,16 +1500,16 @@ private module Stage3 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -1559,7 +1554,7 @@ private module Stage3 {
   ) {
     exists(DataFlowType contentType |
       fwdFlow(node1, cc, argAp, ap1, config) and
-      PrevStage::storeStepCand(node1, unbindBool(getApprox(ap1)), tc, node2, contentType, config) and
+      PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
       typecheckStore(ap1, contentType)
     )
   }
@@ -1594,7 +1589,7 @@ private module Stage3 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -1613,7 +1608,7 @@ private module Stage3 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -1638,7 +1633,7 @@ private module Stage3 {
   ) {
     exists(ParameterNode p |
       fwdFlowIn(call, p, cc, _, argAp, ap, config) and
-      PrevStage::parameterMayFlowThrough(p, _, unbindBool(getApprox(ap)), config)
+      PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
     )
   }
 
@@ -1686,9 +1681,9 @@ private module Stage3 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -1700,9 +1695,9 @@ private module Stage3 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -1755,9 +1750,10 @@ private module Stage3 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -1823,9 +1819,10 @@ private module Stage3 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ ap2, _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -1844,13 +1841,13 @@ private module Stage3 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -2090,7 +2087,9 @@ private module Stage4 {
 
   private ApApprox getApprox(Ap ap) { result = ap.getFront() }
 
-  private ApNil getApNil(Node node) { result = TNil(getNodeType(node)) }
+  private ApNil getApNil(Node node) {
+    PrevStage::revFlow(node, _) and result = TNil(getNodeType(node))
+  }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result = push(tc, tail) }
@@ -2135,7 +2134,7 @@ private module Stage4 {
   bindingset[node, cc, config]
   private LocalCc getLocalCc(Node node, Cc cc, Configuration config) {
     localFlowEntry(node, config) and
-    result = getLocalCallContext(cc, node.getEnclosingCallable())
+    result = getLocalCallContext(pragma[only_bind_out](cc), getNodeEnclosingCallable(node))
   }
 
   private predicate localStep(
@@ -2150,8 +2149,8 @@ private module Stage4 {
     Configuration config
   ) {
     flowOutOfCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
-    PrevStage::revFlow(node2, _, _, _, config) and
-    PrevStage::revFlow(node1, _, _, _, unbind(config))
+    PrevStage::revFlow(node2, _, _, _, pragma[only_bind_into](config)) and
+    PrevStage::revFlow(node1, _, _, _, pragma[only_bind_into](config))
   }
 
   pragma[nomagic]
@@ -2160,8 +2159,8 @@ private module Stage4 {
     Configuration config
   ) {
     flowIntoCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
-    PrevStage::revFlow(node2, _, _, _, config) and
-    PrevStage::revFlow(node1, _, _, _, unbind(config))
+    PrevStage::revFlow(node2, _, _, _, pragma[only_bind_into](config)) and
+    PrevStage::revFlow(node1, _, _, _, pragma[only_bind_into](config))
   }
 
   bindingset[node, ap]
@@ -2176,6 +2175,13 @@ private module Stage4 {
     PrevStage::revFlow(node, _, _, apa, config)
   }
 
+  bindingset[result, apa]
+  private ApApprox unbindApa(ApApprox apa) {
+    exists(ApApprox apa0 |
+      apa = pragma[only_bind_into](apa0) and result = pragma[only_bind_into](apa0)
+    )
+  }
+
   /**
    * Holds if `node` is reachable with access path `ap` from a source in the
    * configuration `config`.
@@ -2187,7 +2193,7 @@ private module Stage4 {
   pragma[nomagic]
   predicate fwdFlow(Node node, Cc cc, ApOption argAp, Ap ap, Configuration config) {
     fwdFlow0(node, cc, argAp, ap, config) and
-    flowCand(node, getApprox(ap), config) and
+    flowCand(node, unbindApa(getApprox(ap)), config) and
     filter(node, ap)
   }
 
@@ -2211,16 +2217,16 @@ private module Stage4 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -2265,7 +2271,7 @@ private module Stage4 {
   ) {
     exists(DataFlowType contentType |
       fwdFlow(node1, cc, argAp, ap1, config) and
-      PrevStage::storeStepCand(node1, getApprox(ap1), tc, node2, contentType, config) and
+      PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
       typecheckStore(ap1, contentType)
     )
   }
@@ -2300,7 +2306,7 @@ private module Stage4 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -2319,7 +2325,7 @@ private module Stage4 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -2344,7 +2350,7 @@ private module Stage4 {
   ) {
     exists(ParameterNode p |
       fwdFlowIn(call, p, cc, _, argAp, ap, config) and
-      PrevStage::parameterMayFlowThrough(p, _, getApprox(ap), config)
+      PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
     )
   }
 
@@ -2392,9 +2398,9 @@ private module Stage4 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -2406,9 +2412,9 @@ private module Stage4 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -2461,9 +2467,10 @@ private module Stage4 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -2529,9 +2536,10 @@ private module Stage4 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ ap2, _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -2550,13 +2558,13 @@ private module Stage4 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -2583,14 +2591,16 @@ private module Stage4 {
 }
 
 bindingset[conf, result]
-private Configuration unbind(Configuration conf) { result >= conf and result <= conf }
+private Configuration unbindConf(Configuration conf) {
+  exists(Configuration c | result = pragma[only_bind_into](c) and conf = pragma[only_bind_into](c))
+}
 
 private predicate nodeMayUseSummary(Node n, AccessPathApprox apa, Configuration config) {
   exists(DataFlowCallable c, AccessPathApprox apa0 |
     Stage4::parameterMayFlowThrough(_, c, apa, _) and
     Stage4::revFlow(n, true, _, apa0, config) and
     Stage4::fwdFlow(n, any(CallContextCall ccc), TAccessPathApproxSome(apa), apa0, config) and
-    n.getEnclosingCallable() = c
+    getNodeEnclosingCallable(n) = c
   )
 }
 
@@ -2753,13 +2763,13 @@ private newtype TPathNode =
     // ... or a step from an existing PathNode to another node.
     exists(PathNodeMid mid |
       pathStep(mid, node, cc, sc, ap) and
-      config = mid.getConfiguration() and
-      Stage4::revFlow(node, _, _, ap.getApprox(), unbind(config))
+      pragma[only_bind_into](config) = mid.getConfiguration() and
+      Stage4::revFlow(node, _, _, ap.getApprox(), pragma[only_bind_into](config))
     )
   } or
   TPathNodeSink(Node node, Configuration config) {
-    config.isSink(node) and
-    Stage4::revFlow(node, unbind(config)) and
+    pragma[only_bind_into](config).isSink(node) and
+    Stage4::revFlow(node, pragma[only_bind_into](config)) and
     (
       // A sink that is also a source ...
       config.isSource(node)
@@ -2767,7 +2777,7 @@ private newtype TPathNode =
       // ... or a sink that can be reached from a source
       exists(PathNodeMid mid |
         pathStep(mid, node, _, _, TAccessPathNil(_)) and
-        config = unbind(mid.getConfiguration())
+        pragma[only_bind_into](config) = mid.getConfiguration()
       )
     )
   }
@@ -3064,7 +3074,7 @@ private class PathNodeMid extends PathNodeImpl, TPathNodeMid {
 
   private PathNodeMid getSuccMid() {
     pathStep(this, result.getNode(), result.getCallContext(), result.getSummaryCtx(), result.getAp()) and
-    result.getConfiguration() = unbind(this.getConfiguration())
+    result.getConfiguration() = unbindConf(this.getConfiguration())
   }
 
   override PathNodeImpl getASuccessorImpl() {
@@ -3076,7 +3086,7 @@ private class PathNodeMid extends PathNodeImpl, TPathNodeMid {
       mid = getSuccMid() and
       mid.getNode() = sink.getNode() and
       mid.getAp() instanceof AccessPathNil and
-      sink.getConfiguration() = unbind(mid.getConfiguration()) and
+      sink.getConfiguration() = unbindConf(mid.getConfiguration()) and
       result = sink
     )
   }
@@ -3119,7 +3129,7 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
     conf = mid.getConfiguration() and
     cc = mid.getCallContext() and
     sc = mid.getSummaryCtx() and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(pragma[only_bind_out](cc), getNodeEnclosingCallable(midnode)) and
     ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, _, conf, localCC) and
@@ -3307,7 +3317,7 @@ private predicate pathThroughCallable0(
 ) {
   exists(CallContext innercc, SummaryCtx sc |
     pathIntoCallable(mid, _, cc, innercc, sc, call) and
-    paramFlowsThrough(kind, innercc, sc, ap, apa, unbind(mid.getConfiguration()))
+    paramFlowsThrough(kind, innercc, sc, ap, apa, unbindConf(mid.getConfiguration()))
   )
 }
 
@@ -3319,7 +3329,7 @@ pragma[noinline]
 private predicate pathThroughCallable(PathNodeMid mid, Node out, CallContext cc, AccessPath ap) {
   exists(DataFlowCall call, ReturnKindExt kind, AccessPathApprox apa |
     pathThroughCallable0(call, mid, kind, cc, ap, apa) and
-    out = getAnOutNodeFlow(kind, call, apa, unbind(mid.getConfiguration()))
+    out = getAnOutNodeFlow(kind, call, apa, unbindConf(mid.getConfiguration()))
   )
 }
 
@@ -3405,14 +3415,14 @@ private module FlowExploration {
       // flow out of a callable
       viableReturnPosOut(_, getReturnPosition(node1), node2)
     |
-      c1 = node1.getEnclosingCallable() and
-      c2 = node2.getEnclosingCallable() and
+      c1 = getNodeEnclosingCallable(node1) and
+      c2 = getNodeEnclosingCallable(node2) and
       c1 != c2
     )
   }
 
   private predicate interestingCallableSrc(DataFlowCallable c, Configuration config) {
-    exists(Node n | config.isSource(n) and c = n.getEnclosingCallable())
+    exists(Node n | config.isSource(n) and c = getNodeEnclosingCallable(n))
     or
     exists(DataFlowCallable mid |
       interestingCallableSrc(mid, config) and callableStep(mid, c, config)
@@ -3420,7 +3430,7 @@ private module FlowExploration {
   }
 
   private predicate interestingCallableSink(DataFlowCallable c, Configuration config) {
-    exists(Node n | config.isSink(n) and c = n.getEnclosingCallable())
+    exists(Node n | config.isSink(n) and c = getNodeEnclosingCallable(n))
     or
     exists(DataFlowCallable mid |
       interestingCallableSink(mid, config) and callableStep(c, mid, config)
@@ -3442,20 +3452,20 @@ private module FlowExploration {
   private predicate callableExtStepFwd(TCallableExt ce1, TCallableExt ce2) {
     exists(DataFlowCallable c1, DataFlowCallable c2, Configuration config |
       callableStep(c1, c2, config) and
-      ce1 = TCallable(c1, config) and
-      ce2 = TCallable(c2, unbind(config))
+      ce1 = TCallable(c1, pragma[only_bind_into](config)) and
+      ce2 = TCallable(c2, pragma[only_bind_into](config))
     )
     or
     exists(Node n, Configuration config |
       ce1 = TCallableSrc() and
       config.isSource(n) and
-      ce2 = TCallable(n.getEnclosingCallable(), config)
+      ce2 = TCallable(getNodeEnclosingCallable(n), config)
     )
     or
     exists(Node n, Configuration config |
       ce2 = TCallableSink() and
       config.isSink(n) and
-      ce1 = TCallable(n.getEnclosingCallable(), config)
+      ce1 = TCallable(getNodeEnclosingCallable(n), config)
     )
   }
 
@@ -3586,7 +3596,7 @@ private module FlowExploration {
       exists(config.explorationLimit())
       or
       partialPathNodeMk0(node, cc, sc1, sc2, ap, config) and
-      distSrc(node.getEnclosingCallable(), config) <= config.explorationLimit()
+      distSrc(getNodeEnclosingCallable(node), config) <= config.explorationLimit()
     } or
     TPartialPathNodeRev(
       Node node, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2, RevPartialAccessPath ap,
@@ -3603,7 +3613,7 @@ private module FlowExploration {
         revPartialPathStep(mid, node, sc1, sc2, ap, config) and
         not clearsContent(node, ap.getHead()) and
         not fullBarrier(node, config) and
-        distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
+        distSink(getNodeEnclosingCallable(node), config) <= config.explorationLimit()
       )
     }
 
@@ -3662,7 +3672,7 @@ private module FlowExploration {
      * of interprocedural steps.
      */
     int getSourceDistance() {
-      result = distSrc(this.getNode().getEnclosingCallable(), this.getConfiguration())
+      result = distSrc(getNodeEnclosingCallable(this.getNode()), this.getConfiguration())
     }
 
     /**
@@ -3670,7 +3680,7 @@ private module FlowExploration {
      * of interprocedural steps.
      */
     int getSinkDistance() {
-      result = distSink(this.getNode().getEnclosingCallable(), this.getConfiguration())
+      result = distSink(getNodeEnclosingCallable(this.getNode()), this.getConfiguration())
     }
 
     private string ppAp() {

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

@@ -207,18 +207,6 @@ private predicate fullBarrier(Node node, Configuration config) {
   )
 }
 
-private class AdditionalFlowStepSource extends Node {
-  AdditionalFlowStepSource() { any(Configuration c).isAdditionalFlowStep(this, _) }
-}
-
-pragma[noinline]
-private predicate isAdditionalFlowStep(
-  AdditionalFlowStepSource node1, Node node2, DataFlowCallable callable1, Configuration config
-) {
-  config.isAdditionalFlowStep(node1, node2) and
-  callable1 = node1.getEnclosingCallable()
-}
-
 /**
  * Holds if data can flow in one local step from `node1` to `node2`.
  */
@@ -237,7 +225,8 @@ private predicate localFlowStep(Node node1, Node node2, Configuration config) {
  * Holds if the additional step from `node1` to `node2` does not jump between callables.
  */
 private predicate additionalLocalFlowStep(Node node1, Node node2, Configuration config) {
-  isAdditionalFlowStep(node1, node2, node2.getEnclosingCallable(), config) and
+  config.isAdditionalFlowStep(node1, node2) and
+  getNodeEnclosingCallable(node1) = getNodeEnclosingCallable(node2) and
   not outBarrier(node1, config) and
   not inBarrier(node2, config) and
   not fullBarrier(node1, config) and
@@ -259,14 +248,12 @@ private predicate jumpStep(Node node1, Node node2, Configuration config) {
  * Holds if the additional step from `node1` to `node2` jumps between callables.
  */
 private predicate additionalJumpStep(Node node1, Node node2, Configuration config) {
-  exists(DataFlowCallable callable1 |
-    isAdditionalFlowStep(node1, node2, callable1, config) and
-    node2.getEnclosingCallable() != callable1 and
-    not outBarrier(node1, config) and
-    not inBarrier(node2, config) and
-    not fullBarrier(node1, config) and
-    not fullBarrier(node2, config)
-  )
+  config.isAdditionalFlowStep(node1, node2) and
+  getNodeEnclosingCallable(node1) != getNodeEnclosingCallable(node2) and
+  not outBarrier(node1, config) and
+  not inBarrier(node2, config) and
+  not fullBarrier(node1, config) and
+  not fullBarrier(node2, config)
 }
 
 /**
@@ -457,8 +444,8 @@ private module Stage1 {
     // read
     exists(Node mid, Content c |
       read(node, c, mid) and
-      fwdFlowConsCand(c, unbind(config)) and
-      revFlow(mid, toReturn, config)
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
+      revFlow(mid, toReturn, pragma[only_bind_into](config))
     )
     or
     // flow into a callable
@@ -484,18 +471,18 @@ private module Stage1 {
   pragma[nomagic]
   private predicate revFlowConsCand(Content c, Configuration config) {
     exists(Node mid, Node node |
-      fwdFlow(node, unbind(config)) and
+      fwdFlow(node, pragma[only_bind_into](config)) and
       read(node, c, mid) and
-      fwdFlowConsCand(c, unbind(config)) and
-      revFlow(mid, _, config)
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
+      revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
     )
   }
 
   pragma[nomagic]
   private predicate revFlowStore(Content c, Node node, boolean toReturn, Configuration config) {
     exists(Node mid, TypedContent tc |
-      revFlow(mid, toReturn, config) and
-      fwdFlowConsCand(c, unbind(config)) and
+      revFlow(mid, toReturn, pragma[only_bind_into](config)) and
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
       store(node, tc, mid, _) and
       c = tc.getContent()
     )
@@ -565,8 +552,8 @@ private module Stage1 {
     Node node1, Ap ap1, TypedContent tc, Node node2, DataFlowType contentType, Configuration config
   ) {
     exists(Content c |
-      revFlowIsReadAndStored(c, config) and
-      revFlow(node2, unbind(config)) and
+      revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
+      revFlow(node2, pragma[only_bind_into](config)) and
       store(node1, tc, node2, contentType) and
       c = tc.getContent() and
       exists(ap1)
@@ -575,8 +562,8 @@ private module Stage1 {
 
   pragma[nomagic]
   predicate readStepCand(Node n1, Content c, Node n2, Configuration config) {
-    revFlowIsReadAndStored(c, config) and
-    revFlow(n2, unbind(config)) and
+    revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
+    revFlow(n2, pragma[only_bind_into](config)) and
     read(n1, c, n2)
   }
 
@@ -601,7 +588,7 @@ private module Stage1 {
   ) {
     exists(ReturnNodeExt ret |
       throughFlowNodeCand(ret, config) and
-      callable = ret.getEnclosingCallable() and
+      callable = getNodeEnclosingCallable(ret) and
       kind = ret.getKind()
     )
   }
@@ -614,7 +601,7 @@ private module Stage1 {
     exists(ReturnKindExt kind |
       throughFlowNodeCand(p, config) and
       returnFlowCallableNodeCand(c, kind, config) and
-      p.getEnclosingCallable() = c and
+      getNodeEnclosingCallable(p) = c and
       exists(ap) and
       // we don't expect a parameter to return stored in itself
       not exists(int pos |
@@ -639,9 +626,6 @@ private module Stage1 {
   /* End: Stage 1 logic. */
 }
 
-bindingset[result, b]
-private boolean unbindBool(boolean b) { result != b.booleanNot() }
-
 pragma[noinline]
 private predicate localFlowStepNodeCand1(Node node1, Node node2, Configuration config) {
   Stage1::revFlow(node2, config) and
@@ -778,7 +762,7 @@ private module Stage2 {
   bindingset[result, ap]
   private ApApprox getApprox(Ap ap) { any() }
 
-  private ApNil getApNil(Node node) { any() }
+  private ApNil getApNil(Node node) { PrevStage::revFlow(node, _) and exists(result) }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result = true and exists(tc) and exists(tail) }
@@ -877,16 +861,16 @@ private module Stage2 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -966,7 +950,7 @@ private module Stage2 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -985,7 +969,7 @@ private module Stage2 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -1058,9 +1042,9 @@ private module Stage2 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -1072,9 +1056,9 @@ private module Stage2 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -1127,9 +1111,10 @@ private module Stage2 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -1195,9 +1180,10 @@ private module Stage2 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ unbindBool(ap2), _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -1216,13 +1202,13 @@ private module Stage2 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -1253,8 +1239,8 @@ private predicate flowOutOfCallNodeCand2(
   DataFlowCall call, ReturnNodeExt node1, Node node2, boolean allowsFieldFlow, Configuration config
 ) {
   flowOutOfCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
-  Stage2::revFlow(node2, config) and
-  Stage2::revFlow(node1, unbind(config))
+  Stage2::revFlow(node2, pragma[only_bind_into](config)) and
+  Stage2::revFlow(node1, pragma[only_bind_into](config))
 }
 
 pragma[nomagic]
@@ -1263,8 +1249,8 @@ private predicate flowIntoCallNodeCand2(
   Configuration config
 ) {
   flowIntoCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
-  Stage2::revFlow(node2, config) and
-  Stage2::revFlow(node1, unbind(config))
+  Stage2::revFlow(node2, pragma[only_bind_into](config)) and
+  Stage2::revFlow(node1, pragma[only_bind_into](config))
 }
 
 private module LocalFlowBigStep {
@@ -1319,8 +1305,8 @@ private module LocalFlowBigStep {
   pragma[noinline]
   private predicate additionalLocalFlowStepNodeCand2(Node node1, Node node2, Configuration config) {
     additionalLocalFlowStepNodeCand1(node1, node2, config) and
-    Stage2::revFlow(node1, _, _, false, config) and
-    Stage2::revFlow(node2, _, _, false, unbind(config))
+    Stage2::revFlow(node1, _, _, false, pragma[only_bind_into](config)) and
+    Stage2::revFlow(node2, _, _, false, pragma[only_bind_into](config))
   }
 
   /**
@@ -1337,7 +1323,7 @@ private module LocalFlowBigStep {
   ) {
     not isUnreachableInCall(node2, cc.(LocalCallContextSpecificCall).getCall()) and
     (
-      localFlowEntry(node1, config) and
+      localFlowEntry(node1, pragma[only_bind_into](config)) and
       (
         localFlowStepNodeCand1(node1, node2, config) and
         preservesValue = true and
@@ -1348,24 +1334,24 @@ private module LocalFlowBigStep {
         t = getNodeType(node2)
       ) and
       node1 != node2 and
-      cc.relevantFor(node1.getEnclosingCallable()) and
+      cc.relevantFor(getNodeEnclosingCallable(node1)) and
       not isUnreachableInCall(node1, cc.(LocalCallContextSpecificCall).getCall()) and
-      Stage2::revFlow(node2, unbind(config))
+      Stage2::revFlow(node2, pragma[only_bind_into](config))
       or
       exists(Node mid |
-        localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
+        localFlowStepPlus(node1, mid, preservesValue, t, pragma[only_bind_into](config), cc) and
         localFlowStepNodeCand1(mid, node2, config) and
         not mid instanceof FlowCheckNode and
-        Stage2::revFlow(node2, unbind(config))
+        Stage2::revFlow(node2, pragma[only_bind_into](config))
       )
       or
       exists(Node mid |
-        localFlowStepPlus(node1, mid, _, _, config, cc) and
+        localFlowStepPlus(node1, mid, _, _, pragma[only_bind_into](config), cc) and
         additionalLocalFlowStepNodeCand2(mid, node2, config) and
         not mid instanceof FlowCheckNode and
         preservesValue = false and
         t = getNodeType(node2) and
-        Stage2::revFlow(node2, unbind(config))
+        Stage2::revFlow(node2, pragma[only_bind_into](config))
       )
     )
   }
@@ -1397,7 +1383,9 @@ private module Stage3 {
 
   private ApApprox getApprox(Ap ap) { result = ap.toBoolNonEmpty() }
 
-  private ApNil getApNil(Node node) { result = TFrontNil(getNodeType(node)) }
+  private ApNil getApNil(Node node) {
+    PrevStage::revFlow(node, _) and result = TFrontNil(getNodeType(node))
+  }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result.getHead() = tc and exists(tail) }
@@ -1470,6 +1458,13 @@ private module Stage3 {
     PrevStage::revFlow(node, _, _, apa, config)
   }
 
+  bindingset[result, apa]
+  private ApApprox unbindApa(ApApprox apa) {
+    exists(ApApprox apa0 |
+      apa = pragma[only_bind_into](apa0) and result = pragma[only_bind_into](apa0)
+    )
+  }
+
   /**
    * Holds if `node` is reachable with access path `ap` from a source in the
    * configuration `config`.
@@ -1481,7 +1476,7 @@ private module Stage3 {
   pragma[nomagic]
   predicate fwdFlow(Node node, Cc cc, ApOption argAp, Ap ap, Configuration config) {
     fwdFlow0(node, cc, argAp, ap, config) and
-    flowCand(node, unbindBool(getApprox(ap)), config) and
+    flowCand(node, unbindApa(getApprox(ap)), config) and
     filter(node, ap)
   }
 
@@ -1505,16 +1500,16 @@ private module Stage3 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -1559,7 +1554,7 @@ private module Stage3 {
   ) {
     exists(DataFlowType contentType |
       fwdFlow(node1, cc, argAp, ap1, config) and
-      PrevStage::storeStepCand(node1, unbindBool(getApprox(ap1)), tc, node2, contentType, config) and
+      PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
       typecheckStore(ap1, contentType)
     )
   }
@@ -1594,7 +1589,7 @@ private module Stage3 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -1613,7 +1608,7 @@ private module Stage3 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -1638,7 +1633,7 @@ private module Stage3 {
   ) {
     exists(ParameterNode p |
       fwdFlowIn(call, p, cc, _, argAp, ap, config) and
-      PrevStage::parameterMayFlowThrough(p, _, unbindBool(getApprox(ap)), config)
+      PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
     )
   }
 
@@ -1686,9 +1681,9 @@ private module Stage3 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -1700,9 +1695,9 @@ private module Stage3 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -1755,9 +1750,10 @@ private module Stage3 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -1823,9 +1819,10 @@ private module Stage3 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ ap2, _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -1844,13 +1841,13 @@ private module Stage3 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -2090,7 +2087,9 @@ private module Stage4 {
 
   private ApApprox getApprox(Ap ap) { result = ap.getFront() }
 
-  private ApNil getApNil(Node node) { result = TNil(getNodeType(node)) }
+  private ApNil getApNil(Node node) {
+    PrevStage::revFlow(node, _) and result = TNil(getNodeType(node))
+  }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result = push(tc, tail) }
@@ -2135,7 +2134,7 @@ private module Stage4 {
   bindingset[node, cc, config]
   private LocalCc getLocalCc(Node node, Cc cc, Configuration config) {
     localFlowEntry(node, config) and
-    result = getLocalCallContext(cc, node.getEnclosingCallable())
+    result = getLocalCallContext(pragma[only_bind_out](cc), getNodeEnclosingCallable(node))
   }
 
   private predicate localStep(
@@ -2150,8 +2149,8 @@ private module Stage4 {
     Configuration config
   ) {
     flowOutOfCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
-    PrevStage::revFlow(node2, _, _, _, config) and
-    PrevStage::revFlow(node1, _, _, _, unbind(config))
+    PrevStage::revFlow(node2, _, _, _, pragma[only_bind_into](config)) and
+    PrevStage::revFlow(node1, _, _, _, pragma[only_bind_into](config))
   }
 
   pragma[nomagic]
@@ -2160,8 +2159,8 @@ private module Stage4 {
     Configuration config
   ) {
     flowIntoCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
-    PrevStage::revFlow(node2, _, _, _, config) and
-    PrevStage::revFlow(node1, _, _, _, unbind(config))
+    PrevStage::revFlow(node2, _, _, _, pragma[only_bind_into](config)) and
+    PrevStage::revFlow(node1, _, _, _, pragma[only_bind_into](config))
   }
 
   bindingset[node, ap]
@@ -2176,6 +2175,13 @@ private module Stage4 {
     PrevStage::revFlow(node, _, _, apa, config)
   }
 
+  bindingset[result, apa]
+  private ApApprox unbindApa(ApApprox apa) {
+    exists(ApApprox apa0 |
+      apa = pragma[only_bind_into](apa0) and result = pragma[only_bind_into](apa0)
+    )
+  }
+
   /**
    * Holds if `node` is reachable with access path `ap` from a source in the
    * configuration `config`.
@@ -2187,7 +2193,7 @@ private module Stage4 {
   pragma[nomagic]
   predicate fwdFlow(Node node, Cc cc, ApOption argAp, Ap ap, Configuration config) {
     fwdFlow0(node, cc, argAp, ap, config) and
-    flowCand(node, getApprox(ap), config) and
+    flowCand(node, unbindApa(getApprox(ap)), config) and
     filter(node, ap)
   }
 
@@ -2211,16 +2217,16 @@ private module Stage4 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -2265,7 +2271,7 @@ private module Stage4 {
   ) {
     exists(DataFlowType contentType |
       fwdFlow(node1, cc, argAp, ap1, config) and
-      PrevStage::storeStepCand(node1, getApprox(ap1), tc, node2, contentType, config) and
+      PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
       typecheckStore(ap1, contentType)
     )
   }
@@ -2300,7 +2306,7 @@ private module Stage4 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -2319,7 +2325,7 @@ private module Stage4 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -2344,7 +2350,7 @@ private module Stage4 {
   ) {
     exists(ParameterNode p |
       fwdFlowIn(call, p, cc, _, argAp, ap, config) and
-      PrevStage::parameterMayFlowThrough(p, _, getApprox(ap), config)
+      PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
     )
   }
 
@@ -2392,9 +2398,9 @@ private module Stage4 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -2406,9 +2412,9 @@ private module Stage4 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -2461,9 +2467,10 @@ private module Stage4 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -2529,9 +2536,10 @@ private module Stage4 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ ap2, _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -2550,13 +2558,13 @@ private module Stage4 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -2583,14 +2591,16 @@ private module Stage4 {
 }
 
 bindingset[conf, result]
-private Configuration unbind(Configuration conf) { result >= conf and result <= conf }
+private Configuration unbindConf(Configuration conf) {
+  exists(Configuration c | result = pragma[only_bind_into](c) and conf = pragma[only_bind_into](c))
+}
 
 private predicate nodeMayUseSummary(Node n, AccessPathApprox apa, Configuration config) {
   exists(DataFlowCallable c, AccessPathApprox apa0 |
     Stage4::parameterMayFlowThrough(_, c, apa, _) and
     Stage4::revFlow(n, true, _, apa0, config) and
     Stage4::fwdFlow(n, any(CallContextCall ccc), TAccessPathApproxSome(apa), apa0, config) and
-    n.getEnclosingCallable() = c
+    getNodeEnclosingCallable(n) = c
   )
 }
 
@@ -2753,13 +2763,13 @@ private newtype TPathNode =
     // ... or a step from an existing PathNode to another node.
     exists(PathNodeMid mid |
       pathStep(mid, node, cc, sc, ap) and
-      config = mid.getConfiguration() and
-      Stage4::revFlow(node, _, _, ap.getApprox(), unbind(config))
+      pragma[only_bind_into](config) = mid.getConfiguration() and
+      Stage4::revFlow(node, _, _, ap.getApprox(), pragma[only_bind_into](config))
     )
   } or
   TPathNodeSink(Node node, Configuration config) {
-    config.isSink(node) and
-    Stage4::revFlow(node, unbind(config)) and
+    pragma[only_bind_into](config).isSink(node) and
+    Stage4::revFlow(node, pragma[only_bind_into](config)) and
     (
       // A sink that is also a source ...
       config.isSource(node)
@@ -2767,7 +2777,7 @@ private newtype TPathNode =
       // ... or a sink that can be reached from a source
       exists(PathNodeMid mid |
         pathStep(mid, node, _, _, TAccessPathNil(_)) and
-        config = unbind(mid.getConfiguration())
+        pragma[only_bind_into](config) = mid.getConfiguration()
       )
     )
   }
@@ -3064,7 +3074,7 @@ private class PathNodeMid extends PathNodeImpl, TPathNodeMid {
 
   private PathNodeMid getSuccMid() {
     pathStep(this, result.getNode(), result.getCallContext(), result.getSummaryCtx(), result.getAp()) and
-    result.getConfiguration() = unbind(this.getConfiguration())
+    result.getConfiguration() = unbindConf(this.getConfiguration())
   }
 
   override PathNodeImpl getASuccessorImpl() {
@@ -3076,7 +3086,7 @@ private class PathNodeMid extends PathNodeImpl, TPathNodeMid {
       mid = getSuccMid() and
       mid.getNode() = sink.getNode() and
       mid.getAp() instanceof AccessPathNil and
-      sink.getConfiguration() = unbind(mid.getConfiguration()) and
+      sink.getConfiguration() = unbindConf(mid.getConfiguration()) and
       result = sink
     )
   }
@@ -3119,7 +3129,7 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
     conf = mid.getConfiguration() and
     cc = mid.getCallContext() and
     sc = mid.getSummaryCtx() and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(pragma[only_bind_out](cc), getNodeEnclosingCallable(midnode)) and
     ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, _, conf, localCC) and
@@ -3307,7 +3317,7 @@ private predicate pathThroughCallable0(
 ) {
   exists(CallContext innercc, SummaryCtx sc |
     pathIntoCallable(mid, _, cc, innercc, sc, call) and
-    paramFlowsThrough(kind, innercc, sc, ap, apa, unbind(mid.getConfiguration()))
+    paramFlowsThrough(kind, innercc, sc, ap, apa, unbindConf(mid.getConfiguration()))
   )
 }
 
@@ -3319,7 +3329,7 @@ pragma[noinline]
 private predicate pathThroughCallable(PathNodeMid mid, Node out, CallContext cc, AccessPath ap) {
   exists(DataFlowCall call, ReturnKindExt kind, AccessPathApprox apa |
     pathThroughCallable0(call, mid, kind, cc, ap, apa) and
-    out = getAnOutNodeFlow(kind, call, apa, unbind(mid.getConfiguration()))
+    out = getAnOutNodeFlow(kind, call, apa, unbindConf(mid.getConfiguration()))
   )
 }
 
@@ -3405,14 +3415,14 @@ private module FlowExploration {
       // flow out of a callable
       viableReturnPosOut(_, getReturnPosition(node1), node2)
     |
-      c1 = node1.getEnclosingCallable() and
-      c2 = node2.getEnclosingCallable() and
+      c1 = getNodeEnclosingCallable(node1) and
+      c2 = getNodeEnclosingCallable(node2) and
       c1 != c2
     )
   }
 
   private predicate interestingCallableSrc(DataFlowCallable c, Configuration config) {
-    exists(Node n | config.isSource(n) and c = n.getEnclosingCallable())
+    exists(Node n | config.isSource(n) and c = getNodeEnclosingCallable(n))
     or
     exists(DataFlowCallable mid |
       interestingCallableSrc(mid, config) and callableStep(mid, c, config)
@@ -3420,7 +3430,7 @@ private module FlowExploration {
   }
 
   private predicate interestingCallableSink(DataFlowCallable c, Configuration config) {
-    exists(Node n | config.isSink(n) and c = n.getEnclosingCallable())
+    exists(Node n | config.isSink(n) and c = getNodeEnclosingCallable(n))
     or
     exists(DataFlowCallable mid |
       interestingCallableSink(mid, config) and callableStep(c, mid, config)
@@ -3442,20 +3452,20 @@ private module FlowExploration {
   private predicate callableExtStepFwd(TCallableExt ce1, TCallableExt ce2) {
     exists(DataFlowCallable c1, DataFlowCallable c2, Configuration config |
       callableStep(c1, c2, config) and
-      ce1 = TCallable(c1, config) and
-      ce2 = TCallable(c2, unbind(config))
+      ce1 = TCallable(c1, pragma[only_bind_into](config)) and
+      ce2 = TCallable(c2, pragma[only_bind_into](config))
     )
     or
     exists(Node n, Configuration config |
       ce1 = TCallableSrc() and
       config.isSource(n) and
-      ce2 = TCallable(n.getEnclosingCallable(), config)
+      ce2 = TCallable(getNodeEnclosingCallable(n), config)
     )
     or
     exists(Node n, Configuration config |
       ce2 = TCallableSink() and
       config.isSink(n) and
-      ce1 = TCallable(n.getEnclosingCallable(), config)
+      ce1 = TCallable(getNodeEnclosingCallable(n), config)
     )
   }
 
@@ -3586,7 +3596,7 @@ private module FlowExploration {
       exists(config.explorationLimit())
       or
       partialPathNodeMk0(node, cc, sc1, sc2, ap, config) and
-      distSrc(node.getEnclosingCallable(), config) <= config.explorationLimit()
+      distSrc(getNodeEnclosingCallable(node), config) <= config.explorationLimit()
     } or
     TPartialPathNodeRev(
       Node node, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2, RevPartialAccessPath ap,
@@ -3603,7 +3613,7 @@ private module FlowExploration {
         revPartialPathStep(mid, node, sc1, sc2, ap, config) and
         not clearsContent(node, ap.getHead()) and
         not fullBarrier(node, config) and
-        distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
+        distSink(getNodeEnclosingCallable(node), config) <= config.explorationLimit()
       )
     }
 
@@ -3662,7 +3672,7 @@ private module FlowExploration {
      * of interprocedural steps.
      */
     int getSourceDistance() {
-      result = distSrc(this.getNode().getEnclosingCallable(), this.getConfiguration())
+      result = distSrc(getNodeEnclosingCallable(this.getNode()), this.getConfiguration())
     }
 
     /**
@@ -3670,7 +3680,7 @@ private module FlowExploration {
      * of interprocedural steps.
      */
     int getSinkDistance() {
-      result = distSink(this.getNode().getEnclosingCallable(), this.getConfiguration())
+      result = distSink(getNodeEnclosingCallable(this.getNode()), this.getConfiguration())
     }
 
     private string ppAp() {

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

@@ -207,18 +207,6 @@ private predicate fullBarrier(Node node, Configuration config) {
   )
 }
 
-private class AdditionalFlowStepSource extends Node {
-  AdditionalFlowStepSource() { any(Configuration c).isAdditionalFlowStep(this, _) }
-}
-
-pragma[noinline]
-private predicate isAdditionalFlowStep(
-  AdditionalFlowStepSource node1, Node node2, DataFlowCallable callable1, Configuration config
-) {
-  config.isAdditionalFlowStep(node1, node2) and
-  callable1 = node1.getEnclosingCallable()
-}
-
 /**
  * Holds if data can flow in one local step from `node1` to `node2`.
  */
@@ -237,7 +225,8 @@ private predicate localFlowStep(Node node1, Node node2, Configuration config) {
  * Holds if the additional step from `node1` to `node2` does not jump between callables.
  */
 private predicate additionalLocalFlowStep(Node node1, Node node2, Configuration config) {
-  isAdditionalFlowStep(node1, node2, node2.getEnclosingCallable(), config) and
+  config.isAdditionalFlowStep(node1, node2) and
+  getNodeEnclosingCallable(node1) = getNodeEnclosingCallable(node2) and
   not outBarrier(node1, config) and
   not inBarrier(node2, config) and
   not fullBarrier(node1, config) and
@@ -259,14 +248,12 @@ private predicate jumpStep(Node node1, Node node2, Configuration config) {
  * Holds if the additional step from `node1` to `node2` jumps between callables.
  */
 private predicate additionalJumpStep(Node node1, Node node2, Configuration config) {
-  exists(DataFlowCallable callable1 |
-    isAdditionalFlowStep(node1, node2, callable1, config) and
-    node2.getEnclosingCallable() != callable1 and
-    not outBarrier(node1, config) and
-    not inBarrier(node2, config) and
-    not fullBarrier(node1, config) and
-    not fullBarrier(node2, config)
-  )
+  config.isAdditionalFlowStep(node1, node2) and
+  getNodeEnclosingCallable(node1) != getNodeEnclosingCallable(node2) and
+  not outBarrier(node1, config) and
+  not inBarrier(node2, config) and
+  not fullBarrier(node1, config) and
+  not fullBarrier(node2, config)
 }
 
 /**
@@ -457,8 +444,8 @@ private module Stage1 {
     // read
     exists(Node mid, Content c |
       read(node, c, mid) and
-      fwdFlowConsCand(c, unbind(config)) and
-      revFlow(mid, toReturn, config)
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
+      revFlow(mid, toReturn, pragma[only_bind_into](config))
     )
     or
     // flow into a callable
@@ -484,18 +471,18 @@ private module Stage1 {
   pragma[nomagic]
   private predicate revFlowConsCand(Content c, Configuration config) {
     exists(Node mid, Node node |
-      fwdFlow(node, unbind(config)) and
+      fwdFlow(node, pragma[only_bind_into](config)) and
       read(node, c, mid) and
-      fwdFlowConsCand(c, unbind(config)) and
-      revFlow(mid, _, config)
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
+      revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
     )
   }
 
   pragma[nomagic]
   private predicate revFlowStore(Content c, Node node, boolean toReturn, Configuration config) {
     exists(Node mid, TypedContent tc |
-      revFlow(mid, toReturn, config) and
-      fwdFlowConsCand(c, unbind(config)) and
+      revFlow(mid, toReturn, pragma[only_bind_into](config)) and
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
       store(node, tc, mid, _) and
       c = tc.getContent()
     )
@@ -565,8 +552,8 @@ private module Stage1 {
     Node node1, Ap ap1, TypedContent tc, Node node2, DataFlowType contentType, Configuration config
   ) {
     exists(Content c |
-      revFlowIsReadAndStored(c, config) and
-      revFlow(node2, unbind(config)) and
+      revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
+      revFlow(node2, pragma[only_bind_into](config)) and
       store(node1, tc, node2, contentType) and
       c = tc.getContent() and
       exists(ap1)
@@ -575,8 +562,8 @@ private module Stage1 {
 
   pragma[nomagic]
   predicate readStepCand(Node n1, Content c, Node n2, Configuration config) {
-    revFlowIsReadAndStored(c, config) and
-    revFlow(n2, unbind(config)) and
+    revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
+    revFlow(n2, pragma[only_bind_into](config)) and
     read(n1, c, n2)
   }
 
@@ -601,7 +588,7 @@ private module Stage1 {
   ) {
     exists(ReturnNodeExt ret |
       throughFlowNodeCand(ret, config) and
-      callable = ret.getEnclosingCallable() and
+      callable = getNodeEnclosingCallable(ret) and
       kind = ret.getKind()
     )
   }
@@ -614,7 +601,7 @@ private module Stage1 {
     exists(ReturnKindExt kind |
       throughFlowNodeCand(p, config) and
       returnFlowCallableNodeCand(c, kind, config) and
-      p.getEnclosingCallable() = c and
+      getNodeEnclosingCallable(p) = c and
       exists(ap) and
       // we don't expect a parameter to return stored in itself
       not exists(int pos |
@@ -639,9 +626,6 @@ private module Stage1 {
   /* End: Stage 1 logic. */
 }
 
-bindingset[result, b]
-private boolean unbindBool(boolean b) { result != b.booleanNot() }
-
 pragma[noinline]
 private predicate localFlowStepNodeCand1(Node node1, Node node2, Configuration config) {
   Stage1::revFlow(node2, config) and
@@ -778,7 +762,7 @@ private module Stage2 {
   bindingset[result, ap]
   private ApApprox getApprox(Ap ap) { any() }
 
-  private ApNil getApNil(Node node) { any() }
+  private ApNil getApNil(Node node) { PrevStage::revFlow(node, _) and exists(result) }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result = true and exists(tc) and exists(tail) }
@@ -877,16 +861,16 @@ private module Stage2 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -966,7 +950,7 @@ private module Stage2 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -985,7 +969,7 @@ private module Stage2 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -1058,9 +1042,9 @@ private module Stage2 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -1072,9 +1056,9 @@ private module Stage2 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -1127,9 +1111,10 @@ private module Stage2 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -1195,9 +1180,10 @@ private module Stage2 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ unbindBool(ap2), _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -1216,13 +1202,13 @@ private module Stage2 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -1253,8 +1239,8 @@ private predicate flowOutOfCallNodeCand2(
   DataFlowCall call, ReturnNodeExt node1, Node node2, boolean allowsFieldFlow, Configuration config
 ) {
   flowOutOfCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
-  Stage2::revFlow(node2, config) and
-  Stage2::revFlow(node1, unbind(config))
+  Stage2::revFlow(node2, pragma[only_bind_into](config)) and
+  Stage2::revFlow(node1, pragma[only_bind_into](config))
 }
 
 pragma[nomagic]
@@ -1263,8 +1249,8 @@ private predicate flowIntoCallNodeCand2(
   Configuration config
 ) {
   flowIntoCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
-  Stage2::revFlow(node2, config) and
-  Stage2::revFlow(node1, unbind(config))
+  Stage2::revFlow(node2, pragma[only_bind_into](config)) and
+  Stage2::revFlow(node1, pragma[only_bind_into](config))
 }
 
 private module LocalFlowBigStep {
@@ -1319,8 +1305,8 @@ private module LocalFlowBigStep {
   pragma[noinline]
   private predicate additionalLocalFlowStepNodeCand2(Node node1, Node node2, Configuration config) {
     additionalLocalFlowStepNodeCand1(node1, node2, config) and
-    Stage2::revFlow(node1, _, _, false, config) and
-    Stage2::revFlow(node2, _, _, false, unbind(config))
+    Stage2::revFlow(node1, _, _, false, pragma[only_bind_into](config)) and
+    Stage2::revFlow(node2, _, _, false, pragma[only_bind_into](config))
   }
 
   /**
@@ -1337,7 +1323,7 @@ private module LocalFlowBigStep {
   ) {
     not isUnreachableInCall(node2, cc.(LocalCallContextSpecificCall).getCall()) and
     (
-      localFlowEntry(node1, config) and
+      localFlowEntry(node1, pragma[only_bind_into](config)) and
       (
         localFlowStepNodeCand1(node1, node2, config) and
         preservesValue = true and
@@ -1348,24 +1334,24 @@ private module LocalFlowBigStep {
         t = getNodeType(node2)
       ) and
       node1 != node2 and
-      cc.relevantFor(node1.getEnclosingCallable()) and
+      cc.relevantFor(getNodeEnclosingCallable(node1)) and
       not isUnreachableInCall(node1, cc.(LocalCallContextSpecificCall).getCall()) and
-      Stage2::revFlow(node2, unbind(config))
+      Stage2::revFlow(node2, pragma[only_bind_into](config))
       or
       exists(Node mid |
-        localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
+        localFlowStepPlus(node1, mid, preservesValue, t, pragma[only_bind_into](config), cc) and
         localFlowStepNodeCand1(mid, node2, config) and
         not mid instanceof FlowCheckNode and
-        Stage2::revFlow(node2, unbind(config))
+        Stage2::revFlow(node2, pragma[only_bind_into](config))
       )
       or
       exists(Node mid |
-        localFlowStepPlus(node1, mid, _, _, config, cc) and
+        localFlowStepPlus(node1, mid, _, _, pragma[only_bind_into](config), cc) and
         additionalLocalFlowStepNodeCand2(mid, node2, config) and
         not mid instanceof FlowCheckNode and
         preservesValue = false and
         t = getNodeType(node2) and
-        Stage2::revFlow(node2, unbind(config))
+        Stage2::revFlow(node2, pragma[only_bind_into](config))
       )
     )
   }
@@ -1397,7 +1383,9 @@ private module Stage3 {
 
   private ApApprox getApprox(Ap ap) { result = ap.toBoolNonEmpty() }
 
-  private ApNil getApNil(Node node) { result = TFrontNil(getNodeType(node)) }
+  private ApNil getApNil(Node node) {
+    PrevStage::revFlow(node, _) and result = TFrontNil(getNodeType(node))
+  }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result.getHead() = tc and exists(tail) }
@@ -1470,6 +1458,13 @@ private module Stage3 {
     PrevStage::revFlow(node, _, _, apa, config)
   }
 
+  bindingset[result, apa]
+  private ApApprox unbindApa(ApApprox apa) {
+    exists(ApApprox apa0 |
+      apa = pragma[only_bind_into](apa0) and result = pragma[only_bind_into](apa0)
+    )
+  }
+
   /**
    * Holds if `node` is reachable with access path `ap` from a source in the
    * configuration `config`.
@@ -1481,7 +1476,7 @@ private module Stage3 {
   pragma[nomagic]
   predicate fwdFlow(Node node, Cc cc, ApOption argAp, Ap ap, Configuration config) {
     fwdFlow0(node, cc, argAp, ap, config) and
-    flowCand(node, unbindBool(getApprox(ap)), config) and
+    flowCand(node, unbindApa(getApprox(ap)), config) and
     filter(node, ap)
   }
 
@@ -1505,16 +1500,16 @@ private module Stage3 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -1559,7 +1554,7 @@ private module Stage3 {
   ) {
     exists(DataFlowType contentType |
       fwdFlow(node1, cc, argAp, ap1, config) and
-      PrevStage::storeStepCand(node1, unbindBool(getApprox(ap1)), tc, node2, contentType, config) and
+      PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
       typecheckStore(ap1, contentType)
     )
   }
@@ -1594,7 +1589,7 @@ private module Stage3 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -1613,7 +1608,7 @@ private module Stage3 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -1638,7 +1633,7 @@ private module Stage3 {
   ) {
     exists(ParameterNode p |
       fwdFlowIn(call, p, cc, _, argAp, ap, config) and
-      PrevStage::parameterMayFlowThrough(p, _, unbindBool(getApprox(ap)), config)
+      PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
     )
   }
 
@@ -1686,9 +1681,9 @@ private module Stage3 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -1700,9 +1695,9 @@ private module Stage3 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -1755,9 +1750,10 @@ private module Stage3 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -1823,9 +1819,10 @@ private module Stage3 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ ap2, _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -1844,13 +1841,13 @@ private module Stage3 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -2090,7 +2087,9 @@ private module Stage4 {
 
   private ApApprox getApprox(Ap ap) { result = ap.getFront() }
 
-  private ApNil getApNil(Node node) { result = TNil(getNodeType(node)) }
+  private ApNil getApNil(Node node) {
+    PrevStage::revFlow(node, _) and result = TNil(getNodeType(node))
+  }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result = push(tc, tail) }
@@ -2135,7 +2134,7 @@ private module Stage4 {
   bindingset[node, cc, config]
   private LocalCc getLocalCc(Node node, Cc cc, Configuration config) {
     localFlowEntry(node, config) and
-    result = getLocalCallContext(cc, node.getEnclosingCallable())
+    result = getLocalCallContext(pragma[only_bind_out](cc), getNodeEnclosingCallable(node))
   }
 
   private predicate localStep(
@@ -2150,8 +2149,8 @@ private module Stage4 {
     Configuration config
   ) {
     flowOutOfCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
-    PrevStage::revFlow(node2, _, _, _, config) and
-    PrevStage::revFlow(node1, _, _, _, unbind(config))
+    PrevStage::revFlow(node2, _, _, _, pragma[only_bind_into](config)) and
+    PrevStage::revFlow(node1, _, _, _, pragma[only_bind_into](config))
   }
 
   pragma[nomagic]
@@ -2160,8 +2159,8 @@ private module Stage4 {
     Configuration config
   ) {
     flowIntoCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
-    PrevStage::revFlow(node2, _, _, _, config) and
-    PrevStage::revFlow(node1, _, _, _, unbind(config))
+    PrevStage::revFlow(node2, _, _, _, pragma[only_bind_into](config)) and
+    PrevStage::revFlow(node1, _, _, _, pragma[only_bind_into](config))
   }
 
   bindingset[node, ap]
@@ -2176,6 +2175,13 @@ private module Stage4 {
     PrevStage::revFlow(node, _, _, apa, config)
   }
 
+  bindingset[result, apa]
+  private ApApprox unbindApa(ApApprox apa) {
+    exists(ApApprox apa0 |
+      apa = pragma[only_bind_into](apa0) and result = pragma[only_bind_into](apa0)
+    )
+  }
+
   /**
    * Holds if `node` is reachable with access path `ap` from a source in the
    * configuration `config`.
@@ -2187,7 +2193,7 @@ private module Stage4 {
   pragma[nomagic]
   predicate fwdFlow(Node node, Cc cc, ApOption argAp, Ap ap, Configuration config) {
     fwdFlow0(node, cc, argAp, ap, config) and
-    flowCand(node, getApprox(ap), config) and
+    flowCand(node, unbindApa(getApprox(ap)), config) and
     filter(node, ap)
   }
 
@@ -2211,16 +2217,16 @@ private module Stage4 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -2265,7 +2271,7 @@ private module Stage4 {
   ) {
     exists(DataFlowType contentType |
       fwdFlow(node1, cc, argAp, ap1, config) and
-      PrevStage::storeStepCand(node1, getApprox(ap1), tc, node2, contentType, config) and
+      PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
       typecheckStore(ap1, contentType)
     )
   }
@@ -2300,7 +2306,7 @@ private module Stage4 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -2319,7 +2325,7 @@ private module Stage4 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -2344,7 +2350,7 @@ private module Stage4 {
   ) {
     exists(ParameterNode p |
       fwdFlowIn(call, p, cc, _, argAp, ap, config) and
-      PrevStage::parameterMayFlowThrough(p, _, getApprox(ap), config)
+      PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
     )
   }
 
@@ -2392,9 +2398,9 @@ private module Stage4 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -2406,9 +2412,9 @@ private module Stage4 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -2461,9 +2467,10 @@ private module Stage4 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -2529,9 +2536,10 @@ private module Stage4 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ ap2, _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -2550,13 +2558,13 @@ private module Stage4 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -2583,14 +2591,16 @@ private module Stage4 {
 }
 
 bindingset[conf, result]
-private Configuration unbind(Configuration conf) { result >= conf and result <= conf }
+private Configuration unbindConf(Configuration conf) {
+  exists(Configuration c | result = pragma[only_bind_into](c) and conf = pragma[only_bind_into](c))
+}
 
 private predicate nodeMayUseSummary(Node n, AccessPathApprox apa, Configuration config) {
   exists(DataFlowCallable c, AccessPathApprox apa0 |
     Stage4::parameterMayFlowThrough(_, c, apa, _) and
     Stage4::revFlow(n, true, _, apa0, config) and
     Stage4::fwdFlow(n, any(CallContextCall ccc), TAccessPathApproxSome(apa), apa0, config) and
-    n.getEnclosingCallable() = c
+    getNodeEnclosingCallable(n) = c
   )
 }
 
@@ -2753,13 +2763,13 @@ private newtype TPathNode =
     // ... or a step from an existing PathNode to another node.
     exists(PathNodeMid mid |
       pathStep(mid, node, cc, sc, ap) and
-      config = mid.getConfiguration() and
-      Stage4::revFlow(node, _, _, ap.getApprox(), unbind(config))
+      pragma[only_bind_into](config) = mid.getConfiguration() and
+      Stage4::revFlow(node, _, _, ap.getApprox(), pragma[only_bind_into](config))
     )
   } or
   TPathNodeSink(Node node, Configuration config) {
-    config.isSink(node) and
-    Stage4::revFlow(node, unbind(config)) and
+    pragma[only_bind_into](config).isSink(node) and
+    Stage4::revFlow(node, pragma[only_bind_into](config)) and
     (
       // A sink that is also a source ...
       config.isSource(node)
@@ -2767,7 +2777,7 @@ private newtype TPathNode =
       // ... or a sink that can be reached from a source
       exists(PathNodeMid mid |
         pathStep(mid, node, _, _, TAccessPathNil(_)) and
-        config = unbind(mid.getConfiguration())
+        pragma[only_bind_into](config) = mid.getConfiguration()
       )
     )
   }
@@ -3064,7 +3074,7 @@ private class PathNodeMid extends PathNodeImpl, TPathNodeMid {
 
   private PathNodeMid getSuccMid() {
     pathStep(this, result.getNode(), result.getCallContext(), result.getSummaryCtx(), result.getAp()) and
-    result.getConfiguration() = unbind(this.getConfiguration())
+    result.getConfiguration() = unbindConf(this.getConfiguration())
   }
 
   override PathNodeImpl getASuccessorImpl() {
@@ -3076,7 +3086,7 @@ private class PathNodeMid extends PathNodeImpl, TPathNodeMid {
       mid = getSuccMid() and
       mid.getNode() = sink.getNode() and
       mid.getAp() instanceof AccessPathNil and
-      sink.getConfiguration() = unbind(mid.getConfiguration()) and
+      sink.getConfiguration() = unbindConf(mid.getConfiguration()) and
       result = sink
     )
   }
@@ -3119,7 +3129,7 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
     conf = mid.getConfiguration() and
     cc = mid.getCallContext() and
     sc = mid.getSummaryCtx() and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(pragma[only_bind_out](cc), getNodeEnclosingCallable(midnode)) and
     ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, _, conf, localCC) and
@@ -3307,7 +3317,7 @@ private predicate pathThroughCallable0(
 ) {
   exists(CallContext innercc, SummaryCtx sc |
     pathIntoCallable(mid, _, cc, innercc, sc, call) and
-    paramFlowsThrough(kind, innercc, sc, ap, apa, unbind(mid.getConfiguration()))
+    paramFlowsThrough(kind, innercc, sc, ap, apa, unbindConf(mid.getConfiguration()))
   )
 }
 
@@ -3319,7 +3329,7 @@ pragma[noinline]
 private predicate pathThroughCallable(PathNodeMid mid, Node out, CallContext cc, AccessPath ap) {
   exists(DataFlowCall call, ReturnKindExt kind, AccessPathApprox apa |
     pathThroughCallable0(call, mid, kind, cc, ap, apa) and
-    out = getAnOutNodeFlow(kind, call, apa, unbind(mid.getConfiguration()))
+    out = getAnOutNodeFlow(kind, call, apa, unbindConf(mid.getConfiguration()))
   )
 }
 
@@ -3405,14 +3415,14 @@ private module FlowExploration {
       // flow out of a callable
       viableReturnPosOut(_, getReturnPosition(node1), node2)
     |
-      c1 = node1.getEnclosingCallable() and
-      c2 = node2.getEnclosingCallable() and
+      c1 = getNodeEnclosingCallable(node1) and
+      c2 = getNodeEnclosingCallable(node2) and
       c1 != c2
     )
   }
 
   private predicate interestingCallableSrc(DataFlowCallable c, Configuration config) {
-    exists(Node n | config.isSource(n) and c = n.getEnclosingCallable())
+    exists(Node n | config.isSource(n) and c = getNodeEnclosingCallable(n))
     or
     exists(DataFlowCallable mid |
       interestingCallableSrc(mid, config) and callableStep(mid, c, config)
@@ -3420,7 +3430,7 @@ private module FlowExploration {
   }
 
   private predicate interestingCallableSink(DataFlowCallable c, Configuration config) {
-    exists(Node n | config.isSink(n) and c = n.getEnclosingCallable())
+    exists(Node n | config.isSink(n) and c = getNodeEnclosingCallable(n))
     or
     exists(DataFlowCallable mid |
       interestingCallableSink(mid, config) and callableStep(c, mid, config)
@@ -3442,20 +3452,20 @@ private module FlowExploration {
   private predicate callableExtStepFwd(TCallableExt ce1, TCallableExt ce2) {
     exists(DataFlowCallable c1, DataFlowCallable c2, Configuration config |
       callableStep(c1, c2, config) and
-      ce1 = TCallable(c1, config) and
-      ce2 = TCallable(c2, unbind(config))
+      ce1 = TCallable(c1, pragma[only_bind_into](config)) and
+      ce2 = TCallable(c2, pragma[only_bind_into](config))
     )
     or
     exists(Node n, Configuration config |
       ce1 = TCallableSrc() and
       config.isSource(n) and
-      ce2 = TCallable(n.getEnclosingCallable(), config)
+      ce2 = TCallable(getNodeEnclosingCallable(n), config)
     )
     or
     exists(Node n, Configuration config |
       ce2 = TCallableSink() and
       config.isSink(n) and
-      ce1 = TCallable(n.getEnclosingCallable(), config)
+      ce1 = TCallable(getNodeEnclosingCallable(n), config)
     )
   }
 
@@ -3586,7 +3596,7 @@ private module FlowExploration {
       exists(config.explorationLimit())
       or
       partialPathNodeMk0(node, cc, sc1, sc2, ap, config) and
-      distSrc(node.getEnclosingCallable(), config) <= config.explorationLimit()
+      distSrc(getNodeEnclosingCallable(node), config) <= config.explorationLimit()
     } or
     TPartialPathNodeRev(
       Node node, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2, RevPartialAccessPath ap,
@@ -3603,7 +3613,7 @@ private module FlowExploration {
         revPartialPathStep(mid, node, sc1, sc2, ap, config) and
         not clearsContent(node, ap.getHead()) and
         not fullBarrier(node, config) and
-        distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
+        distSink(getNodeEnclosingCallable(node), config) <= config.explorationLimit()
       )
     }
 
@@ -3662,7 +3672,7 @@ private module FlowExploration {
      * of interprocedural steps.
      */
     int getSourceDistance() {
-      result = distSrc(this.getNode().getEnclosingCallable(), this.getConfiguration())
+      result = distSrc(getNodeEnclosingCallable(this.getNode()), this.getConfiguration())
     }
 
     /**
@@ -3670,7 +3680,7 @@ private module FlowExploration {
      * of interprocedural steps.
      */
     int getSinkDistance() {
-      result = distSink(this.getNode().getEnclosingCallable(), this.getConfiguration())
+      result = distSink(getNodeEnclosingCallable(this.getNode()), this.getConfiguration())
     }
 
     private string ppAp() {

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

@@ -207,18 +207,6 @@ private predicate fullBarrier(Node node, Configuration config) {
   )
 }
 
-private class AdditionalFlowStepSource extends Node {
-  AdditionalFlowStepSource() { any(Configuration c).isAdditionalFlowStep(this, _) }
-}
-
-pragma[noinline]
-private predicate isAdditionalFlowStep(
-  AdditionalFlowStepSource node1, Node node2, DataFlowCallable callable1, Configuration config
-) {
-  config.isAdditionalFlowStep(node1, node2) and
-  callable1 = node1.getEnclosingCallable()
-}
-
 /**
  * Holds if data can flow in one local step from `node1` to `node2`.
  */
@@ -237,7 +225,8 @@ private predicate localFlowStep(Node node1, Node node2, Configuration config) {
  * Holds if the additional step from `node1` to `node2` does not jump between callables.
  */
 private predicate additionalLocalFlowStep(Node node1, Node node2, Configuration config) {
-  isAdditionalFlowStep(node1, node2, node2.getEnclosingCallable(), config) and
+  config.isAdditionalFlowStep(node1, node2) and
+  getNodeEnclosingCallable(node1) = getNodeEnclosingCallable(node2) and
   not outBarrier(node1, config) and
   not inBarrier(node2, config) and
   not fullBarrier(node1, config) and
@@ -259,14 +248,12 @@ private predicate jumpStep(Node node1, Node node2, Configuration config) {
  * Holds if the additional step from `node1` to `node2` jumps between callables.
  */
 private predicate additionalJumpStep(Node node1, Node node2, Configuration config) {
-  exists(DataFlowCallable callable1 |
-    isAdditionalFlowStep(node1, node2, callable1, config) and
-    node2.getEnclosingCallable() != callable1 and
-    not outBarrier(node1, config) and
-    not inBarrier(node2, config) and
-    not fullBarrier(node1, config) and
-    not fullBarrier(node2, config)
-  )
+  config.isAdditionalFlowStep(node1, node2) and
+  getNodeEnclosingCallable(node1) != getNodeEnclosingCallable(node2) and
+  not outBarrier(node1, config) and
+  not inBarrier(node2, config) and
+  not fullBarrier(node1, config) and
+  not fullBarrier(node2, config)
 }
 
 /**
@@ -457,8 +444,8 @@ private module Stage1 {
     // read
     exists(Node mid, Content c |
       read(node, c, mid) and
-      fwdFlowConsCand(c, unbind(config)) and
-      revFlow(mid, toReturn, config)
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
+      revFlow(mid, toReturn, pragma[only_bind_into](config))
     )
     or
     // flow into a callable
@@ -484,18 +471,18 @@ private module Stage1 {
   pragma[nomagic]
   private predicate revFlowConsCand(Content c, Configuration config) {
     exists(Node mid, Node node |
-      fwdFlow(node, unbind(config)) and
+      fwdFlow(node, pragma[only_bind_into](config)) and
       read(node, c, mid) and
-      fwdFlowConsCand(c, unbind(config)) and
-      revFlow(mid, _, config)
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
+      revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
     )
   }
 
   pragma[nomagic]
   private predicate revFlowStore(Content c, Node node, boolean toReturn, Configuration config) {
     exists(Node mid, TypedContent tc |
-      revFlow(mid, toReturn, config) and
-      fwdFlowConsCand(c, unbind(config)) and
+      revFlow(mid, toReturn, pragma[only_bind_into](config)) and
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
       store(node, tc, mid, _) and
       c = tc.getContent()
     )
@@ -565,8 +552,8 @@ private module Stage1 {
     Node node1, Ap ap1, TypedContent tc, Node node2, DataFlowType contentType, Configuration config
   ) {
     exists(Content c |
-      revFlowIsReadAndStored(c, config) and
-      revFlow(node2, unbind(config)) and
+      revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
+      revFlow(node2, pragma[only_bind_into](config)) and
       store(node1, tc, node2, contentType) and
       c = tc.getContent() and
       exists(ap1)
@@ -575,8 +562,8 @@ private module Stage1 {
 
   pragma[nomagic]
   predicate readStepCand(Node n1, Content c, Node n2, Configuration config) {
-    revFlowIsReadAndStored(c, config) and
-    revFlow(n2, unbind(config)) and
+    revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
+    revFlow(n2, pragma[only_bind_into](config)) and
     read(n1, c, n2)
   }
 
@@ -601,7 +588,7 @@ private module Stage1 {
   ) {
     exists(ReturnNodeExt ret |
       throughFlowNodeCand(ret, config) and
-      callable = ret.getEnclosingCallable() and
+      callable = getNodeEnclosingCallable(ret) and
       kind = ret.getKind()
     )
   }
@@ -614,7 +601,7 @@ private module Stage1 {
     exists(ReturnKindExt kind |
       throughFlowNodeCand(p, config) and
       returnFlowCallableNodeCand(c, kind, config) and
-      p.getEnclosingCallable() = c and
+      getNodeEnclosingCallable(p) = c and
       exists(ap) and
       // we don't expect a parameter to return stored in itself
       not exists(int pos |
@@ -639,9 +626,6 @@ private module Stage1 {
   /* End: Stage 1 logic. */
 }
 
-bindingset[result, b]
-private boolean unbindBool(boolean b) { result != b.booleanNot() }
-
 pragma[noinline]
 private predicate localFlowStepNodeCand1(Node node1, Node node2, Configuration config) {
   Stage1::revFlow(node2, config) and
@@ -778,7 +762,7 @@ private module Stage2 {
   bindingset[result, ap]
   private ApApprox getApprox(Ap ap) { any() }
 
-  private ApNil getApNil(Node node) { any() }
+  private ApNil getApNil(Node node) { PrevStage::revFlow(node, _) and exists(result) }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result = true and exists(tc) and exists(tail) }
@@ -877,16 +861,16 @@ private module Stage2 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -966,7 +950,7 @@ private module Stage2 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -985,7 +969,7 @@ private module Stage2 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -1058,9 +1042,9 @@ private module Stage2 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -1072,9 +1056,9 @@ private module Stage2 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -1127,9 +1111,10 @@ private module Stage2 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -1195,9 +1180,10 @@ private module Stage2 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ unbindBool(ap2), _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -1216,13 +1202,13 @@ private module Stage2 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -1253,8 +1239,8 @@ private predicate flowOutOfCallNodeCand2(
   DataFlowCall call, ReturnNodeExt node1, Node node2, boolean allowsFieldFlow, Configuration config
 ) {
   flowOutOfCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
-  Stage2::revFlow(node2, config) and
-  Stage2::revFlow(node1, unbind(config))
+  Stage2::revFlow(node2, pragma[only_bind_into](config)) and
+  Stage2::revFlow(node1, pragma[only_bind_into](config))
 }
 
 pragma[nomagic]
@@ -1263,8 +1249,8 @@ private predicate flowIntoCallNodeCand2(
   Configuration config
 ) {
   flowIntoCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
-  Stage2::revFlow(node2, config) and
-  Stage2::revFlow(node1, unbind(config))
+  Stage2::revFlow(node2, pragma[only_bind_into](config)) and
+  Stage2::revFlow(node1, pragma[only_bind_into](config))
 }
 
 private module LocalFlowBigStep {
@@ -1319,8 +1305,8 @@ private module LocalFlowBigStep {
   pragma[noinline]
   private predicate additionalLocalFlowStepNodeCand2(Node node1, Node node2, Configuration config) {
     additionalLocalFlowStepNodeCand1(node1, node2, config) and
-    Stage2::revFlow(node1, _, _, false, config) and
-    Stage2::revFlow(node2, _, _, false, unbind(config))
+    Stage2::revFlow(node1, _, _, false, pragma[only_bind_into](config)) and
+    Stage2::revFlow(node2, _, _, false, pragma[only_bind_into](config))
   }
 
   /**
@@ -1337,7 +1323,7 @@ private module LocalFlowBigStep {
   ) {
     not isUnreachableInCall(node2, cc.(LocalCallContextSpecificCall).getCall()) and
     (
-      localFlowEntry(node1, config) and
+      localFlowEntry(node1, pragma[only_bind_into](config)) and
       (
         localFlowStepNodeCand1(node1, node2, config) and
         preservesValue = true and
@@ -1348,24 +1334,24 @@ private module LocalFlowBigStep {
         t = getNodeType(node2)
       ) and
       node1 != node2 and
-      cc.relevantFor(node1.getEnclosingCallable()) and
+      cc.relevantFor(getNodeEnclosingCallable(node1)) and
       not isUnreachableInCall(node1, cc.(LocalCallContextSpecificCall).getCall()) and
-      Stage2::revFlow(node2, unbind(config))
+      Stage2::revFlow(node2, pragma[only_bind_into](config))
       or
       exists(Node mid |
-        localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
+        localFlowStepPlus(node1, mid, preservesValue, t, pragma[only_bind_into](config), cc) and
         localFlowStepNodeCand1(mid, node2, config) and
         not mid instanceof FlowCheckNode and
-        Stage2::revFlow(node2, unbind(config))
+        Stage2::revFlow(node2, pragma[only_bind_into](config))
       )
       or
       exists(Node mid |
-        localFlowStepPlus(node1, mid, _, _, config, cc) and
+        localFlowStepPlus(node1, mid, _, _, pragma[only_bind_into](config), cc) and
         additionalLocalFlowStepNodeCand2(mid, node2, config) and
         not mid instanceof FlowCheckNode and
         preservesValue = false and
         t = getNodeType(node2) and
-        Stage2::revFlow(node2, unbind(config))
+        Stage2::revFlow(node2, pragma[only_bind_into](config))
       )
     )
   }
@@ -1397,7 +1383,9 @@ private module Stage3 {
 
   private ApApprox getApprox(Ap ap) { result = ap.toBoolNonEmpty() }
 
-  private ApNil getApNil(Node node) { result = TFrontNil(getNodeType(node)) }
+  private ApNil getApNil(Node node) {
+    PrevStage::revFlow(node, _) and result = TFrontNil(getNodeType(node))
+  }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result.getHead() = tc and exists(tail) }
@@ -1470,6 +1458,13 @@ private module Stage3 {
     PrevStage::revFlow(node, _, _, apa, config)
   }
 
+  bindingset[result, apa]
+  private ApApprox unbindApa(ApApprox apa) {
+    exists(ApApprox apa0 |
+      apa = pragma[only_bind_into](apa0) and result = pragma[only_bind_into](apa0)
+    )
+  }
+
   /**
    * Holds if `node` is reachable with access path `ap` from a source in the
    * configuration `config`.
@@ -1481,7 +1476,7 @@ private module Stage3 {
   pragma[nomagic]
   predicate fwdFlow(Node node, Cc cc, ApOption argAp, Ap ap, Configuration config) {
     fwdFlow0(node, cc, argAp, ap, config) and
-    flowCand(node, unbindBool(getApprox(ap)), config) and
+    flowCand(node, unbindApa(getApprox(ap)), config) and
     filter(node, ap)
   }
 
@@ -1505,16 +1500,16 @@ private module Stage3 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -1559,7 +1554,7 @@ private module Stage3 {
   ) {
     exists(DataFlowType contentType |
       fwdFlow(node1, cc, argAp, ap1, config) and
-      PrevStage::storeStepCand(node1, unbindBool(getApprox(ap1)), tc, node2, contentType, config) and
+      PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
       typecheckStore(ap1, contentType)
     )
   }
@@ -1594,7 +1589,7 @@ private module Stage3 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -1613,7 +1608,7 @@ private module Stage3 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -1638,7 +1633,7 @@ private module Stage3 {
   ) {
     exists(ParameterNode p |
       fwdFlowIn(call, p, cc, _, argAp, ap, config) and
-      PrevStage::parameterMayFlowThrough(p, _, unbindBool(getApprox(ap)), config)
+      PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
     )
   }
 
@@ -1686,9 +1681,9 @@ private module Stage3 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -1700,9 +1695,9 @@ private module Stage3 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -1755,9 +1750,10 @@ private module Stage3 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -1823,9 +1819,10 @@ private module Stage3 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ ap2, _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -1844,13 +1841,13 @@ private module Stage3 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -2090,7 +2087,9 @@ private module Stage4 {
 
   private ApApprox getApprox(Ap ap) { result = ap.getFront() }
 
-  private ApNil getApNil(Node node) { result = TNil(getNodeType(node)) }
+  private ApNil getApNil(Node node) {
+    PrevStage::revFlow(node, _) and result = TNil(getNodeType(node))
+  }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result = push(tc, tail) }
@@ -2135,7 +2134,7 @@ private module Stage4 {
   bindingset[node, cc, config]
   private LocalCc getLocalCc(Node node, Cc cc, Configuration config) {
     localFlowEntry(node, config) and
-    result = getLocalCallContext(cc, node.getEnclosingCallable())
+    result = getLocalCallContext(pragma[only_bind_out](cc), getNodeEnclosingCallable(node))
   }
 
   private predicate localStep(
@@ -2150,8 +2149,8 @@ private module Stage4 {
     Configuration config
   ) {
     flowOutOfCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
-    PrevStage::revFlow(node2, _, _, _, config) and
-    PrevStage::revFlow(node1, _, _, _, unbind(config))
+    PrevStage::revFlow(node2, _, _, _, pragma[only_bind_into](config)) and
+    PrevStage::revFlow(node1, _, _, _, pragma[only_bind_into](config))
   }
 
   pragma[nomagic]
@@ -2160,8 +2159,8 @@ private module Stage4 {
     Configuration config
   ) {
     flowIntoCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
-    PrevStage::revFlow(node2, _, _, _, config) and
-    PrevStage::revFlow(node1, _, _, _, unbind(config))
+    PrevStage::revFlow(node2, _, _, _, pragma[only_bind_into](config)) and
+    PrevStage::revFlow(node1, _, _, _, pragma[only_bind_into](config))
   }
 
   bindingset[node, ap]
@@ -2176,6 +2175,13 @@ private module Stage4 {
     PrevStage::revFlow(node, _, _, apa, config)
   }
 
+  bindingset[result, apa]
+  private ApApprox unbindApa(ApApprox apa) {
+    exists(ApApprox apa0 |
+      apa = pragma[only_bind_into](apa0) and result = pragma[only_bind_into](apa0)
+    )
+  }
+
   /**
    * Holds if `node` is reachable with access path `ap` from a source in the
    * configuration `config`.
@@ -2187,7 +2193,7 @@ private module Stage4 {
   pragma[nomagic]
   predicate fwdFlow(Node node, Cc cc, ApOption argAp, Ap ap, Configuration config) {
     fwdFlow0(node, cc, argAp, ap, config) and
-    flowCand(node, getApprox(ap), config) and
+    flowCand(node, unbindApa(getApprox(ap)), config) and
     filter(node, ap)
   }
 
@@ -2211,16 +2217,16 @@ private module Stage4 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -2265,7 +2271,7 @@ private module Stage4 {
   ) {
     exists(DataFlowType contentType |
       fwdFlow(node1, cc, argAp, ap1, config) and
-      PrevStage::storeStepCand(node1, getApprox(ap1), tc, node2, contentType, config) and
+      PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
       typecheckStore(ap1, contentType)
     )
   }
@@ -2300,7 +2306,7 @@ private module Stage4 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -2319,7 +2325,7 @@ private module Stage4 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -2344,7 +2350,7 @@ private module Stage4 {
   ) {
     exists(ParameterNode p |
       fwdFlowIn(call, p, cc, _, argAp, ap, config) and
-      PrevStage::parameterMayFlowThrough(p, _, getApprox(ap), config)
+      PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
     )
   }
 
@@ -2392,9 +2398,9 @@ private module Stage4 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -2406,9 +2412,9 @@ private module Stage4 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -2461,9 +2467,10 @@ private module Stage4 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -2529,9 +2536,10 @@ private module Stage4 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ ap2, _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -2550,13 +2558,13 @@ private module Stage4 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -2583,14 +2591,16 @@ private module Stage4 {
 }
 
 bindingset[conf, result]
-private Configuration unbind(Configuration conf) { result >= conf and result <= conf }
+private Configuration unbindConf(Configuration conf) {
+  exists(Configuration c | result = pragma[only_bind_into](c) and conf = pragma[only_bind_into](c))
+}
 
 private predicate nodeMayUseSummary(Node n, AccessPathApprox apa, Configuration config) {
   exists(DataFlowCallable c, AccessPathApprox apa0 |
     Stage4::parameterMayFlowThrough(_, c, apa, _) and
     Stage4::revFlow(n, true, _, apa0, config) and
     Stage4::fwdFlow(n, any(CallContextCall ccc), TAccessPathApproxSome(apa), apa0, config) and
-    n.getEnclosingCallable() = c
+    getNodeEnclosingCallable(n) = c
   )
 }
 
@@ -2753,13 +2763,13 @@ private newtype TPathNode =
     // ... or a step from an existing PathNode to another node.
     exists(PathNodeMid mid |
       pathStep(mid, node, cc, sc, ap) and
-      config = mid.getConfiguration() and
-      Stage4::revFlow(node, _, _, ap.getApprox(), unbind(config))
+      pragma[only_bind_into](config) = mid.getConfiguration() and
+      Stage4::revFlow(node, _, _, ap.getApprox(), pragma[only_bind_into](config))
     )
   } or
   TPathNodeSink(Node node, Configuration config) {
-    config.isSink(node) and
-    Stage4::revFlow(node, unbind(config)) and
+    pragma[only_bind_into](config).isSink(node) and
+    Stage4::revFlow(node, pragma[only_bind_into](config)) and
     (
       // A sink that is also a source ...
       config.isSource(node)
@@ -2767,7 +2777,7 @@ private newtype TPathNode =
       // ... or a sink that can be reached from a source
       exists(PathNodeMid mid |
         pathStep(mid, node, _, _, TAccessPathNil(_)) and
-        config = unbind(mid.getConfiguration())
+        pragma[only_bind_into](config) = mid.getConfiguration()
       )
     )
   }
@@ -3064,7 +3074,7 @@ private class PathNodeMid extends PathNodeImpl, TPathNodeMid {
 
   private PathNodeMid getSuccMid() {
     pathStep(this, result.getNode(), result.getCallContext(), result.getSummaryCtx(), result.getAp()) and
-    result.getConfiguration() = unbind(this.getConfiguration())
+    result.getConfiguration() = unbindConf(this.getConfiguration())
   }
 
   override PathNodeImpl getASuccessorImpl() {
@@ -3076,7 +3086,7 @@ private class PathNodeMid extends PathNodeImpl, TPathNodeMid {
       mid = getSuccMid() and
       mid.getNode() = sink.getNode() and
       mid.getAp() instanceof AccessPathNil and
-      sink.getConfiguration() = unbind(mid.getConfiguration()) and
+      sink.getConfiguration() = unbindConf(mid.getConfiguration()) and
       result = sink
     )
   }
@@ -3119,7 +3129,7 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
     conf = mid.getConfiguration() and
     cc = mid.getCallContext() and
     sc = mid.getSummaryCtx() and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(pragma[only_bind_out](cc), getNodeEnclosingCallable(midnode)) and
     ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, _, conf, localCC) and
@@ -3307,7 +3317,7 @@ private predicate pathThroughCallable0(
 ) {
   exists(CallContext innercc, SummaryCtx sc |
     pathIntoCallable(mid, _, cc, innercc, sc, call) and
-    paramFlowsThrough(kind, innercc, sc, ap, apa, unbind(mid.getConfiguration()))
+    paramFlowsThrough(kind, innercc, sc, ap, apa, unbindConf(mid.getConfiguration()))
   )
 }
 
@@ -3319,7 +3329,7 @@ pragma[noinline]
 private predicate pathThroughCallable(PathNodeMid mid, Node out, CallContext cc, AccessPath ap) {
   exists(DataFlowCall call, ReturnKindExt kind, AccessPathApprox apa |
     pathThroughCallable0(call, mid, kind, cc, ap, apa) and
-    out = getAnOutNodeFlow(kind, call, apa, unbind(mid.getConfiguration()))
+    out = getAnOutNodeFlow(kind, call, apa, unbindConf(mid.getConfiguration()))
   )
 }
 
@@ -3405,14 +3415,14 @@ private module FlowExploration {
       // flow out of a callable
       viableReturnPosOut(_, getReturnPosition(node1), node2)
     |
-      c1 = node1.getEnclosingCallable() and
-      c2 = node2.getEnclosingCallable() and
+      c1 = getNodeEnclosingCallable(node1) and
+      c2 = getNodeEnclosingCallable(node2) and
       c1 != c2
     )
   }
 
   private predicate interestingCallableSrc(DataFlowCallable c, Configuration config) {
-    exists(Node n | config.isSource(n) and c = n.getEnclosingCallable())
+    exists(Node n | config.isSource(n) and c = getNodeEnclosingCallable(n))
     or
     exists(DataFlowCallable mid |
       interestingCallableSrc(mid, config) and callableStep(mid, c, config)
@@ -3420,7 +3430,7 @@ private module FlowExploration {
   }
 
   private predicate interestingCallableSink(DataFlowCallable c, Configuration config) {
-    exists(Node n | config.isSink(n) and c = n.getEnclosingCallable())
+    exists(Node n | config.isSink(n) and c = getNodeEnclosingCallable(n))
     or
     exists(DataFlowCallable mid |
       interestingCallableSink(mid, config) and callableStep(c, mid, config)
@@ -3442,20 +3452,20 @@ private module FlowExploration {
   private predicate callableExtStepFwd(TCallableExt ce1, TCallableExt ce2) {
     exists(DataFlowCallable c1, DataFlowCallable c2, Configuration config |
       callableStep(c1, c2, config) and
-      ce1 = TCallable(c1, config) and
-      ce2 = TCallable(c2, unbind(config))
+      ce1 = TCallable(c1, pragma[only_bind_into](config)) and
+      ce2 = TCallable(c2, pragma[only_bind_into](config))
     )
     or
     exists(Node n, Configuration config |
       ce1 = TCallableSrc() and
       config.isSource(n) and
-      ce2 = TCallable(n.getEnclosingCallable(), config)
+      ce2 = TCallable(getNodeEnclosingCallable(n), config)
     )
     or
     exists(Node n, Configuration config |
       ce2 = TCallableSink() and
       config.isSink(n) and
-      ce1 = TCallable(n.getEnclosingCallable(), config)
+      ce1 = TCallable(getNodeEnclosingCallable(n), config)
     )
   }
 
@@ -3586,7 +3596,7 @@ private module FlowExploration {
       exists(config.explorationLimit())
       or
       partialPathNodeMk0(node, cc, sc1, sc2, ap, config) and
-      distSrc(node.getEnclosingCallable(), config) <= config.explorationLimit()
+      distSrc(getNodeEnclosingCallable(node), config) <= config.explorationLimit()
     } or
     TPartialPathNodeRev(
       Node node, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2, RevPartialAccessPath ap,
@@ -3603,7 +3613,7 @@ private module FlowExploration {
         revPartialPathStep(mid, node, sc1, sc2, ap, config) and
         not clearsContent(node, ap.getHead()) and
         not fullBarrier(node, config) and
-        distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
+        distSink(getNodeEnclosingCallable(node), config) <= config.explorationLimit()
       )
     }
 
@@ -3662,7 +3672,7 @@ private module FlowExploration {
      * of interprocedural steps.
      */
     int getSourceDistance() {
-      result = distSrc(this.getNode().getEnclosingCallable(), this.getConfiguration())
+      result = distSrc(getNodeEnclosingCallable(this.getNode()), this.getConfiguration())
     }
 
     /**
@@ -3670,7 +3680,7 @@ private module FlowExploration {
      * of interprocedural steps.
      */
     int getSinkDistance() {
-      result = distSink(this.getNode().getEnclosingCallable(), this.getConfiguration())
+      result = distSink(getNodeEnclosingCallable(this.getNode()), this.getConfiguration())
     }
 
     private string ppAp() {

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

@@ -26,15 +26,243 @@ predicate accessPathCostLimits(int apLimit, int tupleLimit) {
   tupleLimit = 1000
 }
 
+/**
+ * Provides a simple data-flow analysis for resolving lambda calls. The analysis
+ * currently excludes read-steps, store-steps, and flow-through.
+ *
+ * The analysis uses non-linear recursion: When computing a flow path in or out
+ * of a call, we use the results of the analysis recursively to resolve lamba
+ * calls. For this reason, we cannot reuse the code from `DataFlowImpl.qll` directly.
+ */
+private module LambdaFlow {
+  private predicate viableParamNonLambda(DataFlowCall call, int i, ParameterNode p) {
+    p.isParameterOf(viableCallable(call), i)
+  }
+
+  private predicate viableParamLambda(DataFlowCall call, int i, ParameterNode p) {
+    p.isParameterOf(viableCallableLambda(call, _), i)
+  }
+
+  private predicate viableParamArgNonLambda(DataFlowCall call, ParameterNode p, ArgumentNode arg) {
+    exists(int i |
+      viableParamNonLambda(call, i, p) and
+      arg.argumentOf(call, i)
+    )
+  }
+
+  private predicate viableParamArgLambda(DataFlowCall call, ParameterNode p, ArgumentNode arg) {
+    exists(int i |
+      viableParamLambda(call, i, p) and
+      arg.argumentOf(call, i)
+    )
+  }
+
+  private newtype TReturnPositionSimple =
+    TReturnPositionSimple0(DataFlowCallable c, ReturnKind kind) {
+      exists(ReturnNode ret |
+        c = getNodeEnclosingCallable(ret) and
+        kind = ret.getKind()
+      )
+    }
+
+  pragma[noinline]
+  private TReturnPositionSimple getReturnPositionSimple(ReturnNode ret, ReturnKind kind) {
+    result = TReturnPositionSimple0(getNodeEnclosingCallable(ret), kind)
+  }
+
+  pragma[nomagic]
+  private TReturnPositionSimple viableReturnPosNonLambda(DataFlowCall call, ReturnKind kind) {
+    result = TReturnPositionSimple0(viableCallable(call), kind)
+  }
+
+  pragma[nomagic]
+  private TReturnPositionSimple viableReturnPosLambda(
+    DataFlowCall call, DataFlowCallOption lastCall, ReturnKind kind
+  ) {
+    result = TReturnPositionSimple0(viableCallableLambda(call, lastCall), kind)
+  }
+
+  private predicate viableReturnPosOutNonLambda(
+    DataFlowCall call, TReturnPositionSimple pos, OutNode out
+  ) {
+    exists(ReturnKind kind |
+      pos = viableReturnPosNonLambda(call, kind) and
+      out = getAnOutNode(call, kind)
+    )
+  }
+
+  private predicate viableReturnPosOutLambda(
+    DataFlowCall call, DataFlowCallOption lastCall, TReturnPositionSimple pos, OutNode out
+  ) {
+    exists(ReturnKind kind |
+      pos = viableReturnPosLambda(call, lastCall, kind) and
+      out = getAnOutNode(call, kind)
+    )
+  }
+
+  /**
+   * Holds if data can flow (inter-procedurally) from `node` (of type `t`) to
+   * the lambda call `lambdaCall`.
+   *
+   * The parameter `toReturn` indicates whether the path from `node` to
+   * `lambdaCall` goes through a return, and `toJump` whether the path goes
+   * through a jump step.
+   *
+   * The call context `lastCall` records the last call on the path from `node`
+   * to `lambdaCall`, if any. That is, `lastCall` is able to target the enclosing
+   * callable of `lambdaCall`.
+   */
+  pragma[nomagic]
+  predicate revLambdaFlow(
+    DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
+    boolean toJump, DataFlowCallOption lastCall
+  ) {
+    revLambdaFlow0(lambdaCall, kind, node, t, toReturn, toJump, lastCall) and
+    if node instanceof CastNode or node instanceof ArgumentNode or node instanceof ReturnNode
+    then compatibleTypes(t, getNodeType(node))
+    else any()
+  }
+
+  pragma[nomagic]
+  predicate revLambdaFlow0(
+    DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
+    boolean toJump, DataFlowCallOption lastCall
+  ) {
+    lambdaCall(lambdaCall, kind, node) and
+    t = getNodeType(node) and
+    toReturn = false and
+    toJump = false and
+    lastCall = TDataFlowCallNone()
+    or
+    // local flow
+    exists(Node mid, DataFlowType t0 |
+      revLambdaFlow(lambdaCall, kind, mid, t0, toReturn, toJump, lastCall)
+    |
+      simpleLocalFlowStep(node, mid) and
+      t = t0
+      or
+      exists(boolean preservesValue |
+        additionalLambdaFlowStep(node, mid, preservesValue) and
+        getNodeEnclosingCallable(node) = getNodeEnclosingCallable(mid)
+      |
+        preservesValue = false and
+        t = getNodeType(node)
+        or
+        preservesValue = true and
+        t = t0
+      )
+    )
+    or
+    // jump step
+    exists(Node mid, DataFlowType t0 |
+      revLambdaFlow(lambdaCall, kind, mid, t0, _, _, _) and
+      toReturn = false and
+      toJump = true and
+      lastCall = TDataFlowCallNone()
+    |
+      jumpStep(node, mid) and
+      t = t0
+      or
+      exists(boolean preservesValue |
+        additionalLambdaFlowStep(node, mid, preservesValue) and
+        getNodeEnclosingCallable(node) != getNodeEnclosingCallable(mid)
+      |
+        preservesValue = false and
+        t = getNodeType(node)
+        or
+        preservesValue = true and
+        t = t0
+      )
+    )
+    or
+    // flow into a callable
+    exists(ParameterNode p, DataFlowCallOption lastCall0, DataFlowCall call |
+      revLambdaFlowIn(lambdaCall, kind, p, t, toJump, lastCall0) and
+      (
+        if lastCall0 = TDataFlowCallNone() and toJump = false
+        then lastCall = TDataFlowCallSome(call)
+        else lastCall = lastCall0
+      ) and
+      toReturn = false
+    |
+      viableParamArgNonLambda(call, p, node)
+      or
+      viableParamArgLambda(call, p, node) // non-linear recursion
+    )
+    or
+    // flow out of a callable
+    exists(TReturnPositionSimple pos |
+      revLambdaFlowOut(lambdaCall, kind, pos, t, toJump, lastCall) and
+      getReturnPositionSimple(node, node.(ReturnNode).getKind()) = pos and
+      toReturn = true
+    )
+  }
+
+  pragma[nomagic]
+  predicate revLambdaFlowOutLambdaCall(
+    DataFlowCall lambdaCall, LambdaCallKind kind, OutNode out, DataFlowType t, boolean toJump,
+    DataFlowCall call, DataFlowCallOption lastCall
+  ) {
+    revLambdaFlow(lambdaCall, kind, out, t, _, toJump, lastCall) and
+    exists(ReturnKindExt rk |
+      out = rk.getAnOutNode(call) and
+      lambdaCall(call, _, _)
+    )
+  }
+
+  pragma[nomagic]
+  predicate revLambdaFlowOut(
+    DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
+    boolean toJump, DataFlowCallOption lastCall
+  ) {
+    exists(DataFlowCall call, OutNode out |
+      revLambdaFlow(lambdaCall, kind, out, t, _, toJump, lastCall) and
+      viableReturnPosOutNonLambda(call, pos, out)
+      or
+      // non-linear recursion
+      revLambdaFlowOutLambdaCall(lambdaCall, kind, out, t, toJump, call, lastCall) and
+      viableReturnPosOutLambda(call, _, pos, out)
+    )
+  }
+
+  pragma[nomagic]
+  predicate revLambdaFlowIn(
+    DataFlowCall lambdaCall, LambdaCallKind kind, ParameterNode p, DataFlowType t, boolean toJump,
+    DataFlowCallOption lastCall
+  ) {
+    revLambdaFlow(lambdaCall, kind, p, t, false, toJump, lastCall)
+  }
+}
+
+private DataFlowCallable viableCallableExt(DataFlowCall call) {
+  result = viableCallable(call)
+  or
+  result = viableCallableLambda(call, _)
+}
+
 cached
 private module Cached {
+  /**
+   * Gets a viable target for the lambda call `call`.
+   *
+   * `lastCall` records the call required to reach `call` in order for the result
+   * to be a viable target, if any.
+   */
+  cached
+  DataFlowCallable viableCallableLambda(DataFlowCall call, DataFlowCallOption lastCall) {
+    exists(Node creation, LambdaCallKind kind |
+      LambdaFlow::revLambdaFlow(call, kind, creation, _, _, _, lastCall) and
+      lambdaCreation(creation, kind, result)
+    )
+  }
+
   /**
    * Holds if `p` is the `i`th parameter of a viable dispatch target of `call`.
    * The instance parameter is considered to have index `-1`.
    */
   pragma[nomagic]
   private predicate viableParam(DataFlowCall call, int i, ParameterNode p) {
-    p.isParameterOf(viableCallable(call), i)
+    p.isParameterOf(viableCallableExt(call), i)
   }
 
   /**
@@ -52,7 +280,7 @@ private module Cached {
 
   pragma[nomagic]
   private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKindExt kind) {
-    viableCallable(call) = result.getCallable() and
+    viableCallableExt(call) = result.getCallable() and
     kind = result.getKind()
   }
 
@@ -317,6 +545,35 @@ private module Cached {
 
   cached
   private module DispatchWithCallContext {
+    /**
+     * Holds if the set of viable implementations that can be called by `call`
+     * might be improved by knowing the call context.
+     */
+    pragma[nomagic]
+    private predicate mayBenefitFromCallContextExt(DataFlowCall call, DataFlowCallable callable) {
+      mayBenefitFromCallContext(call, callable)
+      or
+      callable = call.getEnclosingCallable() and
+      exists(viableCallableLambda(call, TDataFlowCallSome(_)))
+    }
+
+    /**
+     * Gets a viable dispatch target of `call` in the context `ctx`. This is
+     * restricted to those `call`s for which a context might make a difference.
+     */
+    pragma[nomagic]
+    private DataFlowCallable viableImplInCallContextExt(DataFlowCall call, DataFlowCall ctx) {
+      result = viableImplInCallContext(call, ctx)
+      or
+      result = viableCallableLambda(call, TDataFlowCallSome(ctx))
+      or
+      exists(DataFlowCallable enclosing |
+        mayBenefitFromCallContextExt(call, enclosing) and
+        enclosing = viableCallableExt(ctx) and
+        result = viableCallableLambda(call, TDataFlowCallNone())
+      )
+    }
+
     /**
      * Holds if the call context `ctx` reduces the set of viable run-time
      * dispatch targets of call `call` in `c`.
@@ -324,10 +581,10 @@ private module Cached {
     cached
     predicate reducedViableImplInCallContext(DataFlowCall call, DataFlowCallable c, DataFlowCall ctx) {
       exists(int tgts, int ctxtgts |
-        mayBenefitFromCallContext(call, c) and
-        c = viableCallable(ctx) and
-        ctxtgts = count(viableImplInCallContext(call, ctx)) and
-        tgts = strictcount(viableCallable(call)) and
+        mayBenefitFromCallContextExt(call, c) and
+        c = viableCallableExt(ctx) and
+        ctxtgts = count(viableImplInCallContextExt(call, ctx)) and
+        tgts = strictcount(viableCallableExt(call)) and
         ctxtgts < tgts
       )
     }
@@ -339,7 +596,7 @@ private module Cached {
      */
     cached
     DataFlowCallable prunedViableImplInCallContext(DataFlowCall call, DataFlowCall ctx) {
-      result = viableImplInCallContext(call, ctx) and
+      result = viableImplInCallContextExt(call, ctx) and
       reducedViableImplInCallContext(call, _, ctx)
     }
 
@@ -351,10 +608,10 @@ private module Cached {
     cached
     predicate reducedViableImplInReturn(DataFlowCallable c, DataFlowCall call) {
       exists(int tgts, int ctxtgts |
-        mayBenefitFromCallContext(call, _) and
-        c = viableCallable(call) and
-        ctxtgts = count(DataFlowCall ctx | c = viableImplInCallContext(call, ctx)) and
-        tgts = strictcount(DataFlowCall ctx | viableCallable(ctx) = call.getEnclosingCallable()) and
+        mayBenefitFromCallContextExt(call, _) and
+        c = viableCallableExt(call) and
+        ctxtgts = count(DataFlowCall ctx | c = viableImplInCallContextExt(call, ctx)) and
+        tgts = strictcount(DataFlowCall ctx | viableCallableExt(ctx) = call.getEnclosingCallable()) and
         ctxtgts < tgts
       )
     }
@@ -367,7 +624,7 @@ private module Cached {
      */
     cached
     DataFlowCallable prunedViableImplInCallContextReverse(DataFlowCall call, DataFlowCall ctx) {
-      result = viableImplInCallContext(call, ctx) and
+      result = viableImplInCallContextExt(call, ctx) and
       reducedViableImplInReturn(result, call)
     }
   }
@@ -447,7 +704,7 @@ private module Cached {
   predicate recordDataFlowCallSite(DataFlowCall call, DataFlowCallable callable) {
     reducedViableImplInCallContext(_, callable, call)
     or
-    exists(Node n | n.getEnclosingCallable() = callable | isUnreachableInCall(n, call))
+    exists(Node n | getNodeEnclosingCallable(n) = callable | isUnreachableInCall(n, call))
   }
 
   cached
@@ -481,6 +738,11 @@ private module Cached {
     TBooleanNone() or
     TBooleanSome(boolean b) { b = true or b = false }
 
+  cached
+  newtype TDataFlowCallOption =
+    TDataFlowCallNone() or
+    TDataFlowCallSome(DataFlowCall call)
+
   cached
   newtype TTypedContent = MkTypedContent(Content c, DataFlowType t) { store(_, c, _, _, t) }
 
@@ -592,7 +854,7 @@ class CallContextSomeCall extends CallContextCall, TSomeCall {
   override string toString() { result = "CcSomeCall" }
 
   override predicate relevantFor(DataFlowCallable callable) {
-    exists(ParameterNode p | p.getEnclosingCallable() = callable)
+    exists(ParameterNode p | getNodeEnclosingCallable(p) = callable)
   }
 
   override predicate matchesCall(DataFlowCall call) { any() }
@@ -637,7 +899,7 @@ class LocalCallContextSpecificCall extends LocalCallContext, TSpecificLocalCall
 }
 
 private predicate relevantLocalCCtx(DataFlowCall call, DataFlowCallable callable) {
-  exists(Node n | n.getEnclosingCallable() = callable and isUnreachableInCall(n, call))
+  exists(Node n | getNodeEnclosingCallable(n) = callable and isUnreachableInCall(n, call))
 }
 
 /**
@@ -746,9 +1008,22 @@ class ReturnPosition extends TReturnPosition0 {
   string toString() { result = "[" + kind + "] " + c }
 }
 
+/**
+ * Gets the enclosing callable of `n`. Unlike `n.getEnclosingCallable()`, this
+ * predicate ensures that joins go from `n` to the result instead of the other
+ * way around.
+ */
+pragma[inline]
+DataFlowCallable getNodeEnclosingCallable(Node n) {
+  exists(Node n0 |
+    pragma[only_bind_into](n0) = n and
+    pragma[only_bind_into](result) = n0.getEnclosingCallable()
+  )
+}
+
 pragma[noinline]
 private DataFlowCallable returnNodeGetEnclosingCallable(ReturnNodeExt ret) {
-  result = ret.getEnclosingCallable()
+  result = getNodeEnclosingCallable(ret)
 }
 
 pragma[noinline]
@@ -764,7 +1039,7 @@ ReturnPosition getReturnPosition(ReturnNodeExt ret) {
 
 bindingset[cc, callable]
 predicate resolveReturn(CallContext cc, DataFlowCallable callable, DataFlowCall call) {
-  cc instanceof CallContextAny and callable = viableCallable(call)
+  cc instanceof CallContextAny and callable = viableCallableExt(call)
   or
   exists(DataFlowCallable c0, DataFlowCall call0 |
     call0.getEnclosingCallable() = callable and
@@ -778,14 +1053,14 @@ DataFlowCallable resolveCall(DataFlowCall call, CallContext cc) {
   exists(DataFlowCall ctx | cc = TSpecificCall(ctx) |
     if reducedViableImplInCallContext(call, _, ctx)
     then result = prunedViableImplInCallContext(call, ctx)
-    else result = viableCallable(call)
+    else result = viableCallableExt(call)
   )
   or
-  result = viableCallable(call) and cc instanceof CallContextSomeCall
+  result = viableCallableExt(call) and cc instanceof CallContextSomeCall
   or
-  result = viableCallable(call) and cc instanceof CallContextAny
+  result = viableCallableExt(call) and cc instanceof CallContextAny
   or
-  result = viableCallable(call) and cc instanceof CallContextReturn
+  result = viableCallableExt(call) and cc instanceof CallContextReturn
 }
 
 predicate read = readStep/3;
@@ -799,6 +1074,19 @@ class BooleanOption extends TBooleanOption {
   }
 }
 
+/** An optional `DataFlowCall`. */
+class DataFlowCallOption extends TDataFlowCallOption {
+  string toString() {
+    this = TDataFlowCallNone() and
+    result = "(none)"
+    or
+    exists(DataFlowCall call |
+      this = TDataFlowCallSome(call) and
+      result = call.toString()
+    )
+  }
+}
+
 /** Content tagged with the type of a containing object. */
 class TypedContent extends MkTypedContent {
   private Content c;

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

@@ -207,18 +207,6 @@ private predicate fullBarrier(Node node, Configuration config) {
   )
 }
 
-private class AdditionalFlowStepSource extends Node {
-  AdditionalFlowStepSource() { any(Configuration c).isAdditionalFlowStep(this, _) }
-}
-
-pragma[noinline]
-private predicate isAdditionalFlowStep(
-  AdditionalFlowStepSource node1, Node node2, DataFlowCallable callable1, Configuration config
-) {
-  config.isAdditionalFlowStep(node1, node2) and
-  callable1 = node1.getEnclosingCallable()
-}
-
 /**
  * Holds if data can flow in one local step from `node1` to `node2`.
  */
@@ -237,7 +225,8 @@ private predicate localFlowStep(Node node1, Node node2, Configuration config) {
  * Holds if the additional step from `node1` to `node2` does not jump between callables.
  */
 private predicate additionalLocalFlowStep(Node node1, Node node2, Configuration config) {
-  isAdditionalFlowStep(node1, node2, node2.getEnclosingCallable(), config) and
+  config.isAdditionalFlowStep(node1, node2) and
+  getNodeEnclosingCallable(node1) = getNodeEnclosingCallable(node2) and
   not outBarrier(node1, config) and
   not inBarrier(node2, config) and
   not fullBarrier(node1, config) and
@@ -259,14 +248,12 @@ private predicate jumpStep(Node node1, Node node2, Configuration config) {
  * Holds if the additional step from `node1` to `node2` jumps between callables.
  */
 private predicate additionalJumpStep(Node node1, Node node2, Configuration config) {
-  exists(DataFlowCallable callable1 |
-    isAdditionalFlowStep(node1, node2, callable1, config) and
-    node2.getEnclosingCallable() != callable1 and
-    not outBarrier(node1, config) and
-    not inBarrier(node2, config) and
-    not fullBarrier(node1, config) and
-    not fullBarrier(node2, config)
-  )
+  config.isAdditionalFlowStep(node1, node2) and
+  getNodeEnclosingCallable(node1) != getNodeEnclosingCallable(node2) and
+  not outBarrier(node1, config) and
+  not inBarrier(node2, config) and
+  not fullBarrier(node1, config) and
+  not fullBarrier(node2, config)
 }
 
 /**
@@ -457,8 +444,8 @@ private module Stage1 {
     // read
     exists(Node mid, Content c |
       read(node, c, mid) and
-      fwdFlowConsCand(c, unbind(config)) and
-      revFlow(mid, toReturn, config)
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
+      revFlow(mid, toReturn, pragma[only_bind_into](config))
     )
     or
     // flow into a callable
@@ -484,18 +471,18 @@ private module Stage1 {
   pragma[nomagic]
   private predicate revFlowConsCand(Content c, Configuration config) {
     exists(Node mid, Node node |
-      fwdFlow(node, unbind(config)) and
+      fwdFlow(node, pragma[only_bind_into](config)) and
       read(node, c, mid) and
-      fwdFlowConsCand(c, unbind(config)) and
-      revFlow(mid, _, config)
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
+      revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
     )
   }
 
   pragma[nomagic]
   private predicate revFlowStore(Content c, Node node, boolean toReturn, Configuration config) {
     exists(Node mid, TypedContent tc |
-      revFlow(mid, toReturn, config) and
-      fwdFlowConsCand(c, unbind(config)) and
+      revFlow(mid, toReturn, pragma[only_bind_into](config)) and
+      fwdFlowConsCand(c, pragma[only_bind_into](config)) and
       store(node, tc, mid, _) and
       c = tc.getContent()
     )
@@ -565,8 +552,8 @@ private module Stage1 {
     Node node1, Ap ap1, TypedContent tc, Node node2, DataFlowType contentType, Configuration config
   ) {
     exists(Content c |
-      revFlowIsReadAndStored(c, config) and
-      revFlow(node2, unbind(config)) and
+      revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
+      revFlow(node2, pragma[only_bind_into](config)) and
       store(node1, tc, node2, contentType) and
       c = tc.getContent() and
       exists(ap1)
@@ -575,8 +562,8 @@ private module Stage1 {
 
   pragma[nomagic]
   predicate readStepCand(Node n1, Content c, Node n2, Configuration config) {
-    revFlowIsReadAndStored(c, config) and
-    revFlow(n2, unbind(config)) and
+    revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
+    revFlow(n2, pragma[only_bind_into](config)) and
     read(n1, c, n2)
   }
 
@@ -601,7 +588,7 @@ private module Stage1 {
   ) {
     exists(ReturnNodeExt ret |
       throughFlowNodeCand(ret, config) and
-      callable = ret.getEnclosingCallable() and
+      callable = getNodeEnclosingCallable(ret) and
       kind = ret.getKind()
     )
   }
@@ -614,7 +601,7 @@ private module Stage1 {
     exists(ReturnKindExt kind |
       throughFlowNodeCand(p, config) and
       returnFlowCallableNodeCand(c, kind, config) and
-      p.getEnclosingCallable() = c and
+      getNodeEnclosingCallable(p) = c and
       exists(ap) and
       // we don't expect a parameter to return stored in itself
       not exists(int pos |
@@ -639,9 +626,6 @@ private module Stage1 {
   /* End: Stage 1 logic. */
 }
 
-bindingset[result, b]
-private boolean unbindBool(boolean b) { result != b.booleanNot() }
-
 pragma[noinline]
 private predicate localFlowStepNodeCand1(Node node1, Node node2, Configuration config) {
   Stage1::revFlow(node2, config) and
@@ -778,7 +762,7 @@ private module Stage2 {
   bindingset[result, ap]
   private ApApprox getApprox(Ap ap) { any() }
 
-  private ApNil getApNil(Node node) { any() }
+  private ApNil getApNil(Node node) { PrevStage::revFlow(node, _) and exists(result) }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result = true and exists(tc) and exists(tail) }
@@ -877,16 +861,16 @@ private module Stage2 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -966,7 +950,7 @@ private module Stage2 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -985,7 +969,7 @@ private module Stage2 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -1058,9 +1042,9 @@ private module Stage2 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -1072,9 +1056,9 @@ private module Stage2 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -1127,9 +1111,10 @@ private module Stage2 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -1195,9 +1180,10 @@ private module Stage2 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ unbindBool(ap2), _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -1216,13 +1202,13 @@ private module Stage2 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -1253,8 +1239,8 @@ private predicate flowOutOfCallNodeCand2(
   DataFlowCall call, ReturnNodeExt node1, Node node2, boolean allowsFieldFlow, Configuration config
 ) {
   flowOutOfCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
-  Stage2::revFlow(node2, config) and
-  Stage2::revFlow(node1, unbind(config))
+  Stage2::revFlow(node2, pragma[only_bind_into](config)) and
+  Stage2::revFlow(node1, pragma[only_bind_into](config))
 }
 
 pragma[nomagic]
@@ -1263,8 +1249,8 @@ private predicate flowIntoCallNodeCand2(
   Configuration config
 ) {
   flowIntoCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
-  Stage2::revFlow(node2, config) and
-  Stage2::revFlow(node1, unbind(config))
+  Stage2::revFlow(node2, pragma[only_bind_into](config)) and
+  Stage2::revFlow(node1, pragma[only_bind_into](config))
 }
 
 private module LocalFlowBigStep {
@@ -1319,8 +1305,8 @@ private module LocalFlowBigStep {
   pragma[noinline]
   private predicate additionalLocalFlowStepNodeCand2(Node node1, Node node2, Configuration config) {
     additionalLocalFlowStepNodeCand1(node1, node2, config) and
-    Stage2::revFlow(node1, _, _, false, config) and
-    Stage2::revFlow(node2, _, _, false, unbind(config))
+    Stage2::revFlow(node1, _, _, false, pragma[only_bind_into](config)) and
+    Stage2::revFlow(node2, _, _, false, pragma[only_bind_into](config))
   }
 
   /**
@@ -1337,7 +1323,7 @@ private module LocalFlowBigStep {
   ) {
     not isUnreachableInCall(node2, cc.(LocalCallContextSpecificCall).getCall()) and
     (
-      localFlowEntry(node1, config) and
+      localFlowEntry(node1, pragma[only_bind_into](config)) and
       (
         localFlowStepNodeCand1(node1, node2, config) and
         preservesValue = true and
@@ -1348,24 +1334,24 @@ private module LocalFlowBigStep {
         t = getNodeType(node2)
       ) and
       node1 != node2 and
-      cc.relevantFor(node1.getEnclosingCallable()) and
+      cc.relevantFor(getNodeEnclosingCallable(node1)) and
       not isUnreachableInCall(node1, cc.(LocalCallContextSpecificCall).getCall()) and
-      Stage2::revFlow(node2, unbind(config))
+      Stage2::revFlow(node2, pragma[only_bind_into](config))
       or
       exists(Node mid |
-        localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
+        localFlowStepPlus(node1, mid, preservesValue, t, pragma[only_bind_into](config), cc) and
         localFlowStepNodeCand1(mid, node2, config) and
         not mid instanceof FlowCheckNode and
-        Stage2::revFlow(node2, unbind(config))
+        Stage2::revFlow(node2, pragma[only_bind_into](config))
       )
       or
       exists(Node mid |
-        localFlowStepPlus(node1, mid, _, _, config, cc) and
+        localFlowStepPlus(node1, mid, _, _, pragma[only_bind_into](config), cc) and
         additionalLocalFlowStepNodeCand2(mid, node2, config) and
         not mid instanceof FlowCheckNode and
         preservesValue = false and
         t = getNodeType(node2) and
-        Stage2::revFlow(node2, unbind(config))
+        Stage2::revFlow(node2, pragma[only_bind_into](config))
       )
     )
   }
@@ -1397,7 +1383,9 @@ private module Stage3 {
 
   private ApApprox getApprox(Ap ap) { result = ap.toBoolNonEmpty() }
 
-  private ApNil getApNil(Node node) { result = TFrontNil(getNodeType(node)) }
+  private ApNil getApNil(Node node) {
+    PrevStage::revFlow(node, _) and result = TFrontNil(getNodeType(node))
+  }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result.getHead() = tc and exists(tail) }
@@ -1470,6 +1458,13 @@ private module Stage3 {
     PrevStage::revFlow(node, _, _, apa, config)
   }
 
+  bindingset[result, apa]
+  private ApApprox unbindApa(ApApprox apa) {
+    exists(ApApprox apa0 |
+      apa = pragma[only_bind_into](apa0) and result = pragma[only_bind_into](apa0)
+    )
+  }
+
   /**
    * Holds if `node` is reachable with access path `ap` from a source in the
    * configuration `config`.
@@ -1481,7 +1476,7 @@ private module Stage3 {
   pragma[nomagic]
   predicate fwdFlow(Node node, Cc cc, ApOption argAp, Ap ap, Configuration config) {
     fwdFlow0(node, cc, argAp, ap, config) and
-    flowCand(node, unbindBool(getApprox(ap)), config) and
+    flowCand(node, unbindApa(getApprox(ap)), config) and
     filter(node, ap)
   }
 
@@ -1505,16 +1500,16 @@ private module Stage3 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -1559,7 +1554,7 @@ private module Stage3 {
   ) {
     exists(DataFlowType contentType |
       fwdFlow(node1, cc, argAp, ap1, config) and
-      PrevStage::storeStepCand(node1, unbindBool(getApprox(ap1)), tc, node2, contentType, config) and
+      PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
       typecheckStore(ap1, contentType)
     )
   }
@@ -1594,7 +1589,7 @@ private module Stage3 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -1613,7 +1608,7 @@ private module Stage3 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -1638,7 +1633,7 @@ private module Stage3 {
   ) {
     exists(ParameterNode p |
       fwdFlowIn(call, p, cc, _, argAp, ap, config) and
-      PrevStage::parameterMayFlowThrough(p, _, unbindBool(getApprox(ap)), config)
+      PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
     )
   }
 
@@ -1686,9 +1681,9 @@ private module Stage3 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -1700,9 +1695,9 @@ private module Stage3 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -1755,9 +1750,10 @@ private module Stage3 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -1823,9 +1819,10 @@ private module Stage3 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ ap2, _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -1844,13 +1841,13 @@ private module Stage3 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -2090,7 +2087,9 @@ private module Stage4 {
 
   private ApApprox getApprox(Ap ap) { result = ap.getFront() }
 
-  private ApNil getApNil(Node node) { result = TNil(getNodeType(node)) }
+  private ApNil getApNil(Node node) {
+    PrevStage::revFlow(node, _) and result = TNil(getNodeType(node))
+  }
 
   bindingset[tc, tail]
   private Ap apCons(TypedContent tc, Ap tail) { result = push(tc, tail) }
@@ -2135,7 +2134,7 @@ private module Stage4 {
   bindingset[node, cc, config]
   private LocalCc getLocalCc(Node node, Cc cc, Configuration config) {
     localFlowEntry(node, config) and
-    result = getLocalCallContext(cc, node.getEnclosingCallable())
+    result = getLocalCallContext(pragma[only_bind_out](cc), getNodeEnclosingCallable(node))
   }
 
   private predicate localStep(
@@ -2150,8 +2149,8 @@ private module Stage4 {
     Configuration config
   ) {
     flowOutOfCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
-    PrevStage::revFlow(node2, _, _, _, config) and
-    PrevStage::revFlow(node1, _, _, _, unbind(config))
+    PrevStage::revFlow(node2, _, _, _, pragma[only_bind_into](config)) and
+    PrevStage::revFlow(node1, _, _, _, pragma[only_bind_into](config))
   }
 
   pragma[nomagic]
@@ -2160,8 +2159,8 @@ private module Stage4 {
     Configuration config
   ) {
     flowIntoCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
-    PrevStage::revFlow(node2, _, _, _, config) and
-    PrevStage::revFlow(node1, _, _, _, unbind(config))
+    PrevStage::revFlow(node2, _, _, _, pragma[only_bind_into](config)) and
+    PrevStage::revFlow(node1, _, _, _, pragma[only_bind_into](config))
   }
 
   bindingset[node, ap]
@@ -2176,6 +2175,13 @@ private module Stage4 {
     PrevStage::revFlow(node, _, _, apa, config)
   }
 
+  bindingset[result, apa]
+  private ApApprox unbindApa(ApApprox apa) {
+    exists(ApApprox apa0 |
+      apa = pragma[only_bind_into](apa0) and result = pragma[only_bind_into](apa0)
+    )
+  }
+
   /**
    * Holds if `node` is reachable with access path `ap` from a source in the
    * configuration `config`.
@@ -2187,7 +2193,7 @@ private module Stage4 {
   pragma[nomagic]
   predicate fwdFlow(Node node, Cc cc, ApOption argAp, Ap ap, Configuration config) {
     fwdFlow0(node, cc, argAp, ap, config) and
-    flowCand(node, getApprox(ap), config) and
+    flowCand(node, unbindApa(getApprox(ap)), config) and
     filter(node, ap)
   }
 
@@ -2211,16 +2217,16 @@ private module Stage4 {
     )
     or
     exists(Node mid |
-      fwdFlow(mid, _, _, ap, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, ap, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       jumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone()
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(mid, _, _, nil, config) and
-      flowCand(node, _, unbind(config)) and
+      fwdFlow(mid, _, _, nil, pragma[only_bind_into](config)) and
+      flowCand(node, _, pragma[only_bind_into](config)) and
       additionalJumpStep(mid, node, config) and
       cc = ccNone() and
       argAp = apNone() and
@@ -2265,7 +2271,7 @@ private module Stage4 {
   ) {
     exists(DataFlowType contentType |
       fwdFlow(node1, cc, argAp, ap1, config) and
-      PrevStage::storeStepCand(node1, getApprox(ap1), tc, node2, contentType, config) and
+      PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
       typecheckStore(ap1, contentType)
     )
   }
@@ -2300,7 +2306,7 @@ private module Stage4 {
     exists(ArgumentNode arg, boolean allowsFieldFlow |
       fwdFlow(arg, outercc, argAp, ap, config) and
       flowIntoCall(call, arg, p, allowsFieldFlow, config) and
-      innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc)
+      innercc = getCallContextCall(call, getNodeEnclosingCallable(p), outercc)
     |
       ap instanceof ApNil or allowsFieldFlow = true
     )
@@ -2319,7 +2325,7 @@ private module Stage4 {
     exists(ReturnNodeExt ret, boolean allowsFieldFlow, DataFlowCallable inner |
       fwdFlow(ret, innercc, argAp, ap, config) and
       flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
-      inner = ret.getEnclosingCallable() and
+      inner = getNodeEnclosingCallable(ret) and
       checkCallContextReturn(innercc, inner, call) and
       ccOut = getCallContextReturn(inner, call)
     |
@@ -2344,7 +2350,7 @@ private module Stage4 {
   ) {
     exists(ParameterNode p |
       fwdFlowIn(call, p, cc, _, argAp, ap, config) and
-      PrevStage::parameterMayFlowThrough(p, _, getApprox(ap), config)
+      PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
     )
   }
 
@@ -2392,9 +2398,9 @@ private module Stage4 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       localStep(node, mid, false, _, config, _) and
-      revFlow(mid, toReturn, returnAp, nil, config) and
+      revFlow(mid, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
       ap instanceof ApNil
     )
     or
@@ -2406,9 +2412,9 @@ private module Stage4 {
     )
     or
     exists(Node mid, ApNil nil |
-      fwdFlow(node, _, _, ap, config) and
+      fwdFlow(node, _, _, ap, pragma[only_bind_into](config)) and
       additionalJumpStep(node, mid, config) and
-      revFlow(mid, _, _, nil, config) and
+      revFlow(pragma[only_bind_into](mid), _, _, nil, pragma[only_bind_into](config)) and
       toReturn = false and
       returnAp = apNone() and
       ap instanceof ApNil
@@ -2461,9 +2467,10 @@ private module Stage4 {
    */
   pragma[nomagic]
   private predicate revFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
-    exists(Node mid |
+    exists(Node mid, Ap tail0 |
       revFlow(mid, _, _, tail, config) and
-      readStepFwd(_, cons, c, mid, tail, config)
+      tail = pragma[only_bind_into](tail0) and
+      readStepFwd(_, cons, c, mid, tail0, config)
     )
   }
 
@@ -2529,9 +2536,10 @@ private module Stage4 {
 
   predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
     exists(Ap ap1, Ap ap2 |
-      revFlow(node2, _, _, ap2, config) and
+      revFlow(node2, _, _, pragma[only_bind_into](ap2), pragma[only_bind_into](config)) and
       readStepFwd(node1, ap1, c, node2, ap2, config) and
-      revFlowStore(ap1, c, /*unbind*/ ap2, _, _, _, _, _, unbind(config))
+      revFlowStore(ap1, c, pragma[only_bind_into](ap2), _, _, _, _, _,
+        pragma[only_bind_into](config))
     )
   }
 
@@ -2550,13 +2558,13 @@ private module Stage4 {
     ParameterNode p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
   ) {
     revFlow(p, true, apSome(ap0), ap, config) and
-    c = p.getEnclosingCallable()
+    c = getNodeEnclosingCallable(p)
   }
 
   predicate parameterMayFlowThrough(ParameterNode p, DataFlowCallable c, Ap ap, Configuration config) {
     exists(ReturnNodeExt ret, Ap ap0, ReturnKindExt kind, int pos |
       parameterFlow(p, ap, ap0, c, config) and
-      c = ret.getEnclosingCallable() and
+      c = getNodeEnclosingCallable(ret) and
       revFlow(ret, true, apSome(_), ap0, config) and
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
@@ -2583,14 +2591,16 @@ private module Stage4 {
 }
 
 bindingset[conf, result]
-private Configuration unbind(Configuration conf) { result >= conf and result <= conf }
+private Configuration unbindConf(Configuration conf) {
+  exists(Configuration c | result = pragma[only_bind_into](c) and conf = pragma[only_bind_into](c))
+}
 
 private predicate nodeMayUseSummary(Node n, AccessPathApprox apa, Configuration config) {
   exists(DataFlowCallable c, AccessPathApprox apa0 |
     Stage4::parameterMayFlowThrough(_, c, apa, _) and
     Stage4::revFlow(n, true, _, apa0, config) and
     Stage4::fwdFlow(n, any(CallContextCall ccc), TAccessPathApproxSome(apa), apa0, config) and
-    n.getEnclosingCallable() = c
+    getNodeEnclosingCallable(n) = c
   )
 }
 
@@ -2753,13 +2763,13 @@ private newtype TPathNode =
     // ... or a step from an existing PathNode to another node.
     exists(PathNodeMid mid |
       pathStep(mid, node, cc, sc, ap) and
-      config = mid.getConfiguration() and
-      Stage4::revFlow(node, _, _, ap.getApprox(), unbind(config))
+      pragma[only_bind_into](config) = mid.getConfiguration() and
+      Stage4::revFlow(node, _, _, ap.getApprox(), pragma[only_bind_into](config))
     )
   } or
   TPathNodeSink(Node node, Configuration config) {
-    config.isSink(node) and
-    Stage4::revFlow(node, unbind(config)) and
+    pragma[only_bind_into](config).isSink(node) and
+    Stage4::revFlow(node, pragma[only_bind_into](config)) and
     (
       // A sink that is also a source ...
       config.isSource(node)
@@ -2767,7 +2777,7 @@ private newtype TPathNode =
       // ... or a sink that can be reached from a source
       exists(PathNodeMid mid |
         pathStep(mid, node, _, _, TAccessPathNil(_)) and
-        config = unbind(mid.getConfiguration())
+        pragma[only_bind_into](config) = mid.getConfiguration()
       )
     )
   }
@@ -3064,7 +3074,7 @@ private class PathNodeMid extends PathNodeImpl, TPathNodeMid {
 
   private PathNodeMid getSuccMid() {
     pathStep(this, result.getNode(), result.getCallContext(), result.getSummaryCtx(), result.getAp()) and
-    result.getConfiguration() = unbind(this.getConfiguration())
+    result.getConfiguration() = unbindConf(this.getConfiguration())
   }
 
   override PathNodeImpl getASuccessorImpl() {
@@ -3076,7 +3086,7 @@ private class PathNodeMid extends PathNodeImpl, TPathNodeMid {
       mid = getSuccMid() and
       mid.getNode() = sink.getNode() and
       mid.getAp() instanceof AccessPathNil and
-      sink.getConfiguration() = unbind(mid.getConfiguration()) and
+      sink.getConfiguration() = unbindConf(mid.getConfiguration()) and
       result = sink
     )
   }
@@ -3119,7 +3129,7 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, SummaryCt
     conf = mid.getConfiguration() and
     cc = mid.getCallContext() and
     sc = mid.getSummaryCtx() and
-    localCC = getLocalCallContext(cc, midnode.getEnclosingCallable()) and
+    localCC = getLocalCallContext(pragma[only_bind_out](cc), getNodeEnclosingCallable(midnode)) and
     ap0 = mid.getAp()
   |
     localFlowBigStep(midnode, node, true, _, conf, localCC) and
@@ -3307,7 +3317,7 @@ private predicate pathThroughCallable0(
 ) {
   exists(CallContext innercc, SummaryCtx sc |
     pathIntoCallable(mid, _, cc, innercc, sc, call) and
-    paramFlowsThrough(kind, innercc, sc, ap, apa, unbind(mid.getConfiguration()))
+    paramFlowsThrough(kind, innercc, sc, ap, apa, unbindConf(mid.getConfiguration()))
   )
 }
 
@@ -3319,7 +3329,7 @@ pragma[noinline]
 private predicate pathThroughCallable(PathNodeMid mid, Node out, CallContext cc, AccessPath ap) {
   exists(DataFlowCall call, ReturnKindExt kind, AccessPathApprox apa |
     pathThroughCallable0(call, mid, kind, cc, ap, apa) and
-    out = getAnOutNodeFlow(kind, call, apa, unbind(mid.getConfiguration()))
+    out = getAnOutNodeFlow(kind, call, apa, unbindConf(mid.getConfiguration()))
   )
 }
 
@@ -3405,14 +3415,14 @@ private module FlowExploration {
       // flow out of a callable
       viableReturnPosOut(_, getReturnPosition(node1), node2)
     |
-      c1 = node1.getEnclosingCallable() and
-      c2 = node2.getEnclosingCallable() and
+      c1 = getNodeEnclosingCallable(node1) and
+      c2 = getNodeEnclosingCallable(node2) and
       c1 != c2
     )
   }
 
   private predicate interestingCallableSrc(DataFlowCallable c, Configuration config) {
-    exists(Node n | config.isSource(n) and c = n.getEnclosingCallable())
+    exists(Node n | config.isSource(n) and c = getNodeEnclosingCallable(n))
     or
     exists(DataFlowCallable mid |
       interestingCallableSrc(mid, config) and callableStep(mid, c, config)
@@ -3420,7 +3430,7 @@ private module FlowExploration {
   }
 
   private predicate interestingCallableSink(DataFlowCallable c, Configuration config) {
-    exists(Node n | config.isSink(n) and c = n.getEnclosingCallable())
+    exists(Node n | config.isSink(n) and c = getNodeEnclosingCallable(n))
     or
     exists(DataFlowCallable mid |
       interestingCallableSink(mid, config) and callableStep(c, mid, config)
@@ -3442,20 +3452,20 @@ private module FlowExploration {
   private predicate callableExtStepFwd(TCallableExt ce1, TCallableExt ce2) {
     exists(DataFlowCallable c1, DataFlowCallable c2, Configuration config |
       callableStep(c1, c2, config) and
-      ce1 = TCallable(c1, config) and
-      ce2 = TCallable(c2, unbind(config))
+      ce1 = TCallable(c1, pragma[only_bind_into](config)) and
+      ce2 = TCallable(c2, pragma[only_bind_into](config))
     )
     or
     exists(Node n, Configuration config |
       ce1 = TCallableSrc() and
       config.isSource(n) and
-      ce2 = TCallable(n.getEnclosingCallable(), config)
+      ce2 = TCallable(getNodeEnclosingCallable(n), config)
     )
     or
     exists(Node n, Configuration config |
       ce2 = TCallableSink() and
       config.isSink(n) and
-      ce1 = TCallable(n.getEnclosingCallable(), config)
+      ce1 = TCallable(getNodeEnclosingCallable(n), config)
     )
   }
 
@@ -3586,7 +3596,7 @@ private module FlowExploration {
       exists(config.explorationLimit())
       or
       partialPathNodeMk0(node, cc, sc1, sc2, ap, config) and
-      distSrc(node.getEnclosingCallable(), config) <= config.explorationLimit()
+      distSrc(getNodeEnclosingCallable(node), config) <= config.explorationLimit()
     } or
     TPartialPathNodeRev(
       Node node, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2, RevPartialAccessPath ap,
@@ -3603,7 +3613,7 @@ private module FlowExploration {
         revPartialPathStep(mid, node, sc1, sc2, ap, config) and
         not clearsContent(node, ap.getHead()) and
         not fullBarrier(node, config) and
-        distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
+        distSink(getNodeEnclosingCallable(node), config) <= config.explorationLimit()
       )
     }
 
@@ -3662,7 +3672,7 @@ private module FlowExploration {
      * of interprocedural steps.
      */
     int getSourceDistance() {
-      result = distSrc(this.getNode().getEnclosingCallable(), this.getConfiguration())
+      result = distSrc(getNodeEnclosingCallable(this.getNode()), this.getConfiguration())
     }
 
     /**
@@ -3670,7 +3680,7 @@ private module FlowExploration {
      * of interprocedural steps.
      */
     int getSinkDistance() {
-      result = distSink(this.getNode().getEnclosingCallable(), this.getConfiguration())
+      result = distSink(getNodeEnclosingCallable(this.getNode()), this.getConfiguration())
     }
 
     private string ppAp() {