mirror of
https://github.com/github/codeql.git
synced 2026-07-06 20:15:37 +02:00
Compare commits
25 Commits
codeql-cli
...
kaeluka/at
| Author | SHA1 | Date | |
|---|---|---|---|
|
9228ff5473 | ||
|
|
090ae20909 | ||
|
|
6299753a2a | ||
|
|
5ff3d7287b | ||
|
|
965551e65d | ||
|
|
ea13a999cc | ||
|
|
ea88253501 | ||
|
|
e2ad791983 | ||
|
|
a4a95f0cda | ||
|
|
e6e06b9530 | ||
|
|
5ca8509759 | ||
|
|
a201b77b11 | ||
|
|
afd10e3949 | ||
|
|
510a394307 | ||
|
|
e0ea4c4ccb | ||
|
|
d4f3f6516c | ||
|
|
b84e5af050 | ||
|
|
57812c6934 | ||
|
|
22bbe9cc5d | ||
|
|
62667f431c | ||
|
|
8de583b51b | ||
|
|
a1a93ec9ae | ||
|
|
ccf76c9567 | ||
|
|
31c5c97b7d | ||
|
|
c6fb05636e |
@@ -1 +0,0 @@
|
||||
5.0.0
|
||||
14
.github/actions/fetch-codeql/action.yml
vendored
14
.github/actions/fetch-codeql/action.yml
vendored
@@ -3,22 +3,12 @@ description: Fetches the latest version of CodeQL
|
||||
runs:
|
||||
using: composite
|
||||
steps:
|
||||
- name: Select platform - Linux
|
||||
if: runner.os == 'Linux'
|
||||
shell: bash
|
||||
run: echo "GA_CODEQL_CLI_PLATFORM=linux64" >> $GITHUB_ENV
|
||||
|
||||
- name: Select platform - MacOS
|
||||
if: runner.os == 'MacOS'
|
||||
shell: bash
|
||||
run: echo "GA_CODEQL_CLI_PLATFORM=osx64" >> $GITHUB_ENV
|
||||
|
||||
- name: Fetch CodeQL
|
||||
shell: bash
|
||||
run: |
|
||||
LATEST=$(gh release list --repo https://github.com/github/codeql-cli-binaries | cut -f 1 | grep -v beta | sort --version-sort | tail -1)
|
||||
gh release download --repo https://github.com/github/codeql-cli-binaries --pattern codeql-$GA_CODEQL_CLI_PLATFORM.zip "$LATEST"
|
||||
unzip -q -d "${RUNNER_TEMP}" codeql-$GA_CODEQL_CLI_PLATFORM.zip
|
||||
gh release download --repo https://github.com/github/codeql-cli-binaries --pattern codeql-linux64.zip "$LATEST"
|
||||
unzip -q -d "${RUNNER_TEMP}" codeql-linux64.zip
|
||||
echo "${RUNNER_TEMP}/codeql" >> "${GITHUB_PATH}"
|
||||
env:
|
||||
GITHUB_TOKEN: ${{ github.token }}
|
||||
|
||||
53
.github/workflows/post-pr-comment.yml
vendored
53
.github/workflows/post-pr-comment.yml
vendored
@@ -1,17 +1,12 @@
|
||||
# This workflow is the second part of the process described in
|
||||
# .github/workflows/qhelp-pr-preview.yml
|
||||
# See that file for more info.
|
||||
|
||||
name: Post PR comment
|
||||
name: Post pull-request comment
|
||||
on:
|
||||
workflow_run:
|
||||
workflows: [Render QHelp changes]
|
||||
workflows: ["Query help preview"]
|
||||
types:
|
||||
- completed
|
||||
|
||||
permissions:
|
||||
pull-requests: write
|
||||
actions: read
|
||||
|
||||
jobs:
|
||||
post_comment:
|
||||
@@ -22,53 +17,15 @@ jobs:
|
||||
env:
|
||||
GITHUB_TOKEN: ${{ github.token }}
|
||||
WORKFLOW_RUN_ID: ${{ github.event.workflow_run.id }}
|
||||
|
||||
- name: Check that PR SHA matches workflow SHA
|
||||
run: |
|
||||
PR="$(grep -o '^[0-9]\+$' pr_number.txt)"
|
||||
- run: |
|
||||
PR="$(grep -o '^[0-9]\+$' pr.txt)"
|
||||
PR_HEAD_SHA="$(gh api "/repos/${GITHUB_REPOSITORY}/pulls/${PR}" --jq .head.sha)"
|
||||
# Check that the pull-request head SHA matches the head SHA of the workflow run
|
||||
if [ "${WORKFLOW_RUN_HEAD_SHA}" != "${PR_HEAD_SHA}" ]; then
|
||||
echo "PR head SHA ${PR_HEAD_SHA} does not match workflow_run event SHA ${WORKFLOW_RUN_HEAD_SHA}. Stopping." 1>&2
|
||||
exit 1
|
||||
fi
|
||||
gh pr comment "${PR}" --repo "${GITHUB_REPOSITORY}" -F comment.txt
|
||||
env:
|
||||
GITHUB_TOKEN: ${{ github.token }}
|
||||
WORKFLOW_RUN_HEAD_SHA: ${{ github.event.workflow_run.head_commit.id }}
|
||||
|
||||
- name: Create or update comment
|
||||
run: |
|
||||
COMMENT_PREFIX="QHelp previews"
|
||||
COMMENT_AUTHOR="github-actions[bot]"
|
||||
PR_NUMBER="$(grep -o '^[0-9]\+$' pr_number.txt)"
|
||||
|
||||
# If there is no existing comment, comment_id.txt will contain just a
|
||||
# newline (due to jq & gh behaviour). This will cause grep to fail, so
|
||||
# we catch that.
|
||||
RAW_COMMENT_ID=$(grep -o '^[0-9]\+$' comment_id.txt || true)
|
||||
|
||||
if [ $RAW_COMMENT_ID ]
|
||||
then
|
||||
# Fetch existing comment, and validate:
|
||||
# - comment belongs to the PR with number $PR_NUMBER
|
||||
# - comment starts with the expected prefix ("QHelp previews")
|
||||
# - comment author is github-actions[bot]
|
||||
FILTER='select(.issue_url | endswith($repo+"/issues/"+$pr))
|
||||
| select(.body | startswith($prefix))
|
||||
| select(.user.login == $author)
|
||||
| .id'
|
||||
COMMENT_ID=$(gh api "repos/${GITHUB_REPOSITORY}/issues/comments/${RAW_COMMENT_ID}" | jq --arg repo "${GITHUB_REPOSITORY}" --arg pr "${PR_NUMBER}" --arg prefix "${COMMENT_PREFIX}" --arg author "${COMMENT_AUTHOR}" "${FILTER}")
|
||||
if [ $COMMENT_ID ]
|
||||
then
|
||||
# Update existing comment
|
||||
jq --rawfile body comment_body.txt '{"body":$body}' -n | gh api "repos/${GITHUB_REPOSITORY}/issues/comments/${COMMENT_ID}" -X PATCH --input -
|
||||
else
|
||||
echo "Comment ${RAW_COMMENT_ID} did not pass validations: not editing." >&2
|
||||
exit 1
|
||||
fi
|
||||
else
|
||||
# Create new comment
|
||||
jq --rawfile body comment_body.txt '{"body":$body}' -n | gh api "repos/${GITHUB_REPOSITORY}/issues/${PR_NUMBER}/comments" -X POST --input -
|
||||
fi
|
||||
env:
|
||||
GITHUB_TOKEN: ${{ github.token }}
|
||||
|
||||
51
.github/workflows/qhelp-pr-preview.yml
vendored
51
.github/workflows/qhelp-pr-preview.yml
vendored
@@ -1,25 +1,7 @@
|
||||
# This workflow checks for any changes in .qhelp files in pull requests.
|
||||
# For any changed files, it renders them to markdown in a file called `comment_body.txt`.
|
||||
# It then checks if there's an existing comment on the pull request generated by
|
||||
# this workflow, and writes the comment ID to `comment_id.txt`.
|
||||
# It also writes the PR number to `pr_number.txt`.
|
||||
# These three files are uploaded as an artifact.
|
||||
|
||||
# When this workflow completes, the workflow "Post PR comment" runs.
|
||||
# It downloads the artifact and adds a comment to the PR with the rendered
|
||||
# QHelp.
|
||||
|
||||
# The task is split like this because creating PR comments requires extra
|
||||
# permissions that we don't want to expose to PRs from external forks.
|
||||
|
||||
# For more info see:
|
||||
# https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run
|
||||
# https://docs.github.com/en/actions/security-guides/automatic-token-authentication#permissions-for-the-github_token
|
||||
name: Render QHelp changes
|
||||
name: Query help preview
|
||||
|
||||
permissions:
|
||||
contents: read
|
||||
pull-requests: read
|
||||
|
||||
on:
|
||||
pull_request:
|
||||
@@ -33,16 +15,12 @@ jobs:
|
||||
qhelp:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- run: echo "${PR_NUMBER}" > pr_number.txt
|
||||
env:
|
||||
PR_NUMBER: ${{ github.event.number }}
|
||||
- run: echo "${{ github.event.number }}" > pr.txt
|
||||
- uses: actions/upload-artifact@v2
|
||||
with:
|
||||
name: comment
|
||||
path: pr_number.txt
|
||||
if-no-files-found: error
|
||||
path: pr.txt
|
||||
retention-days: 1
|
||||
|
||||
- uses: actions/checkout@v2
|
||||
with:
|
||||
fetch-depth: 2
|
||||
@@ -58,7 +36,7 @@ jobs:
|
||||
- name: QHelp preview
|
||||
run: |
|
||||
EXIT_CODE=0
|
||||
echo "QHelp previews:" > comment_body.txt
|
||||
echo "QHelp previews:" > comment.txt
|
||||
while read -r -d $'\0' path; do
|
||||
if [ ! -f "${path}" ]; then
|
||||
exit 1
|
||||
@@ -74,29 +52,12 @@ jobs:
|
||||
echo '```'
|
||||
fi
|
||||
echo "</details>"
|
||||
done < "${RUNNER_TEMP}/paths.txt" >> comment_body.txt
|
||||
done < "${RUNNER_TEMP}/paths.txt" >> comment.txt
|
||||
exit "${EXIT_CODE}"
|
||||
|
||||
- if: always()
|
||||
uses: actions/upload-artifact@v2
|
||||
with:
|
||||
name: comment
|
||||
path: comment_body.txt
|
||||
if-no-files-found: error
|
||||
retention-days: 1
|
||||
|
||||
- name: Save ID of existing QHelp comment (if it exists)
|
||||
run: |
|
||||
# Find the latest comment starting with "QHelp previews"
|
||||
COMMENT_PREFIX="QHelp previews"
|
||||
gh api "repos/${GITHUB_REPOSITORY}/issues/${PR_NUMBER}/comments" --paginate | jq --arg prefix "${COMMENT_PREFIX}" '[.[] | select(.body|startswith($prefix)) | .id] | max' > comment_id.txt
|
||||
env:
|
||||
GITHUB_TOKEN: ${{ github.token }}
|
||||
PR_NUMBER: ${{ github.event.number }}
|
||||
|
||||
- uses: actions/upload-artifact@v2
|
||||
with:
|
||||
name: comment
|
||||
path: comment_id.txt
|
||||
if-no-files-found: error
|
||||
path: comment.txt
|
||||
retention-days: 1
|
||||
|
||||
51
.github/workflows/swift-qltest.yml
vendored
51
.github/workflows/swift-qltest.yml
vendored
@@ -1,51 +0,0 @@
|
||||
name: "Swift: Run QL Tests"
|
||||
|
||||
on:
|
||||
pull_request:
|
||||
paths:
|
||||
- "swift/**"
|
||||
- .github/workflows/swift-qltest.yml
|
||||
branches:
|
||||
- main
|
||||
defaults:
|
||||
run:
|
||||
working-directory: swift
|
||||
|
||||
jobs:
|
||||
qlformat:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- uses: actions/checkout@v2
|
||||
- uses: ./.github/actions/fetch-codeql
|
||||
- name: Check QL formatting
|
||||
run: find ql "(" -name "*.ql" -or -name "*.qll" ")" -print0 | xargs -0 codeql query format --check-only
|
||||
qltest:
|
||||
runs-on: ${{ matrix.os }}
|
||||
strategy:
|
||||
fail-fast: false
|
||||
matrix:
|
||||
os : [ubuntu-20.04, macos-latest]
|
||||
steps:
|
||||
- uses: actions/checkout@v2
|
||||
- uses: ./.github/actions/fetch-codeql
|
||||
- name: Install bazelisk - Linux
|
||||
if: runner.os == 'Linux'
|
||||
run: |
|
||||
sudo apt-get update
|
||||
sudo apt-get install -y wget
|
||||
wget https://github.com/bazelbuild/bazelisk/releases/download/v1.11.0/bazelisk-linux-amd64
|
||||
mv bazelisk-linux-amd64 /usr/local/bin/bazel
|
||||
chmod +x /usr/local/bin/bazel
|
||||
- name: Install bazelisk - macOS
|
||||
if: runner.os == 'MacOS'
|
||||
run: |
|
||||
brew install bazelisk
|
||||
- name: Build Swift extractor
|
||||
run: |
|
||||
bazel run //swift:create-extractor-pack
|
||||
- name: Run QL tests
|
||||
run: |
|
||||
codeql test run --threads=0 --ram 5000 --search-path "${{ github.workspace }}/swift/extractor-pack" --check-databases --check-unused-labels --check-repeated-labels --check-redefined-labels --check-use-before-definition ql/test
|
||||
env:
|
||||
GITHUB_TOKEN: ${{ github.token }}
|
||||
|
||||
5
.gitignore
vendored
5
.gitignore
vendored
@@ -31,8 +31,5 @@ csharp/extractor/Semmle.Extraction.CSharp.Driver/Properties/launchSettings.json
|
||||
# Compiled class file
|
||||
*.class
|
||||
|
||||
# links created by bazel
|
||||
# links create by bazel
|
||||
/bazel-*
|
||||
|
||||
# CLion project files
|
||||
/.clwb
|
||||
|
||||
@@ -27,7 +27,3 @@
|
||||
# Bazel
|
||||
**/*.bazel @github/codeql-ci-reviewers
|
||||
**/*.bzl @github/codeql-ci-reviewers
|
||||
|
||||
# Documentation etc
|
||||
/*.md @github/code-scanning-product
|
||||
/LICENSE @github/code-scanning-product
|
||||
|
||||
@@ -13,9 +13,7 @@ We welcome contributions to our standard library and standard checks. Do you hav
|
||||
|
||||
## License
|
||||
|
||||
The code in this repository is licensed under the [MIT License](LICENSE) by [GitHub](https://github.com).
|
||||
|
||||
The CodeQL CLI (including the CodeQL engine) is hosted in a [different repository](https://github.com/github/codeql-cli-binaries) and is [licensed separately](https://github.com/github/codeql-cli-binaries/blob/main/LICENSE.md). If you'd like to use the CodeQL CLI to analyze closed-source code, you will need a separate commercial license; please [contact us](https://github.com/enterprise/contact) for further help.
|
||||
The code in this repository is licensed under the [MIT License](LICENSE) by [GitHub](https://github.com). The use of CodeQL on open source code is licensed under specific [Terms & Conditions](https://securitylab.github.com/tools/codeql/license/) UNLESS you have a commercial license in place. If you'd like to use CodeQL with a commercial codebase, please [contact us](https://github.com/enterprise/contact) for further help.
|
||||
|
||||
## Visual Studio Code integration
|
||||
|
||||
|
||||
@@ -1,12 +1,2 @@
|
||||
# Please notice that any bazel targets and definitions in this repository are currently experimental
|
||||
# and for internal use only.
|
||||
|
||||
workspace(name = "codeql")
|
||||
|
||||
load("//misc/bazel:workspace.bzl", "codeql_workspace")
|
||||
|
||||
codeql_workspace()
|
||||
|
||||
load("//misc/bazel:workspace_deps.bzl", "codeql_workspace_deps")
|
||||
|
||||
codeql_workspace_deps()
|
||||
|
||||
@@ -383,8 +383,7 @@
|
||||
"csharp/ql/test/TestUtilities/InlineExpectationsTest.qll",
|
||||
"java/ql/test/TestUtilities/InlineExpectationsTest.qll",
|
||||
"python/ql/test/TestUtilities/InlineExpectationsTest.qll",
|
||||
"ruby/ql/test/TestUtilities/InlineExpectationsTest.qll",
|
||||
"ql/ql/test/TestUtilities/InlineExpectationsTest.qll"
|
||||
"ruby/ql/test/TestUtilities/InlineExpectationsTest.qll"
|
||||
],
|
||||
"C++ ExternalAPIs": [
|
||||
"cpp/ql/src/Security/CWE/CWE-020/ExternalAPIs.qll",
|
||||
|
||||
@@ -1,40 +1,3 @@
|
||||
## 0.1.0
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
* The recently added flow-state versions of `isBarrierIn`, `isBarrierOut`, `isSanitizerIn`, and `isSanitizerOut` in the data flow and taint tracking libraries have been removed.
|
||||
|
||||
### New Features
|
||||
|
||||
* A new library `semmle.code.cpp.security.PrivateData` has been added. The new library heuristically detects variables and functions dealing with sensitive private data, such as e-mail addresses and credit card numbers.
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* The `semmle.code.cpp.security.SensitiveExprs` library has been enhanced with some additional rules for detecting credentials.
|
||||
|
||||
## 0.0.13
|
||||
|
||||
## 0.0.12
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
* The flow state variants of `isBarrier` and `isAdditionalFlowStep` are no longer exposed in the taint tracking library. The `isSanitizer` and `isAdditionalTaintStep` predicates should be used instead.
|
||||
|
||||
### Deprecated APIs
|
||||
|
||||
* Many classes/predicates/modules that had upper-case acronyms have been renamed to follow our style-guide.
|
||||
The old name still exists as a deprecated alias.
|
||||
|
||||
### New Features
|
||||
|
||||
* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states.
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* `DefaultOptions::exits` now holds for C11 functions with the `_Noreturn` or `noreturn` specifier.
|
||||
* `hasImplicitCopyConstructor` and `hasImplicitCopyAssignmentOperator` now correctly handle implicitly-deleted operators in templates.
|
||||
* All deprecated predicates/classes/modules that have been deprecated for over a year have been deleted.
|
||||
|
||||
## 0.0.11
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* All deprecated predicates/classes/modules that have been deprecated for over a year have been deleted.
|
||||
@@ -0,0 +1,5 @@
|
||||
---
|
||||
category: deprecated
|
||||
---
|
||||
* Many classes/predicates/modules that had upper-case acronyms have been renamed to follow our style-guide.
|
||||
The old name still exists as a deprecated alias.
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* `hasImplicitCopyConstructor` and `hasImplicitCopyAssignmentOperator` now correctly handle implicitly-deleted operators in templates.
|
||||
4
cpp/ql/lib/change-notes/2022-03-14-c11-noreturn.md
Normal file
4
cpp/ql/lib/change-notes/2022-03-14-c11-noreturn.md
Normal file
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* `DefaultOptions::exits` now holds for C11 functions with the `_Noreturn` or `noreturn` specifier.
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: feature
|
||||
---
|
||||
* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states.
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: breaking
|
||||
---
|
||||
* The flow state variants of `isBarrier` and `isAdditionalFlowStep` are no longer exposed in the taint tracking library. The `isSanitizer` and `isAdditionalTaintStep` predicates should be used instead.
|
||||
4
cpp/ql/lib/change-notes/2022-03-28-private-data.md
Normal file
4
cpp/ql/lib/change-notes/2022-03-28-private-data.md
Normal file
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: feature
|
||||
---
|
||||
* A new library `semmle.code.cpp.security.PrivateData` has been added. The new library heuristically detects variables and functions dealing with sensitive private data, such as e-mail addresses and credit card numbers.
|
||||
4
cpp/ql/lib/change-notes/2022-03-31-sensitive-exprs.md
Normal file
4
cpp/ql/lib/change-notes/2022-03-31-sensitive-exprs.md
Normal file
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* The `semmle.code.cpp.security.SensitiveExprs` library has been enhanced with some additional rules for detecting credentials.
|
||||
@@ -1,20 +0,0 @@
|
||||
## 0.0.12
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
* The flow state variants of `isBarrier` and `isAdditionalFlowStep` are no longer exposed in the taint tracking library. The `isSanitizer` and `isAdditionalTaintStep` predicates should be used instead.
|
||||
|
||||
### Deprecated APIs
|
||||
|
||||
* Many classes/predicates/modules that had upper-case acronyms have been renamed to follow our style-guide.
|
||||
The old name still exists as a deprecated alias.
|
||||
|
||||
### New Features
|
||||
|
||||
* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states.
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* `DefaultOptions::exits` now holds for C11 functions with the `_Noreturn` or `noreturn` specifier.
|
||||
* `hasImplicitCopyConstructor` and `hasImplicitCopyAssignmentOperator` now correctly handle implicitly-deleted operators in templates.
|
||||
* All deprecated predicates/classes/modules that have been deprecated for over a year have been deleted.
|
||||
@@ -1 +0,0 @@
|
||||
## 0.0.13
|
||||
@@ -1,13 +0,0 @@
|
||||
## 0.1.0
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
* The recently added flow-state versions of `isBarrierIn`, `isBarrierOut`, `isSanitizerIn`, and `isSanitizerOut` in the data flow and taint tracking libraries have been removed.
|
||||
|
||||
### New Features
|
||||
|
||||
* A new library `semmle.code.cpp.security.PrivateData` has been added. The new library heuristically detects variables and functions dealing with sensitive private data, such as e-mail addresses and credit card numbers.
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* The `semmle.code.cpp.security.SensitiveExprs` library has been enhanced with some additional rules for detecting credentials.
|
||||
@@ -1,2 +1,2 @@
|
||||
---
|
||||
lastReleaseVersion: 0.1.0
|
||||
lastReleaseVersion: 0.0.11
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
name: codeql/cpp-all
|
||||
version: 0.1.0
|
||||
version: 0.0.12-dev
|
||||
groups: cpp
|
||||
dbscheme: semmlecode.cpp.dbscheme
|
||||
extractor: cpp
|
||||
|
||||
@@ -84,7 +84,6 @@ private int fileHeaderLimit(File f) {
|
||||
fc = fileFirstComment(f) and
|
||||
result =
|
||||
min(int line |
|
||||
// code ending the initial comments
|
||||
exists(DeclarationEntry de, Location l |
|
||||
l = de.getLocation() and
|
||||
l.getFile() = f and
|
||||
@@ -106,13 +105,7 @@ private int fileHeaderLimit(File f) {
|
||||
line > fc
|
||||
)
|
||||
or
|
||||
// end of the file
|
||||
line = f.getMetrics().getNumberOfLines()
|
||||
or
|
||||
// rarely, we've seen extremely long sequences of initial comments
|
||||
// (and/or limitations in the above constraints) cause an overflow of
|
||||
// the maximum string length. So don't look past 1000 lines regardless.
|
||||
line = 1000
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -109,7 +109,10 @@ class Element extends ElementBase {
|
||||
then
|
||||
exists(MacroInvocation mi |
|
||||
this = mi.getAGeneratedElement() and
|
||||
not hasCloserMacroInvocation(this, mi) and
|
||||
not exists(MacroInvocation closer |
|
||||
this = closer.getAGeneratedElement() and
|
||||
mi = closer.getParentInvocation+()
|
||||
) and
|
||||
result = mi.getMacro()
|
||||
)
|
||||
else result = this
|
||||
@@ -233,14 +236,6 @@ class Element extends ElementBase {
|
||||
}
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate hasCloserMacroInvocation(Element elem, MacroInvocation mi) {
|
||||
exists(MacroInvocation closer |
|
||||
elem = closer.getAGeneratedElement() and
|
||||
mi = closer.getParentInvocation()
|
||||
)
|
||||
}
|
||||
|
||||
private predicate isFromTemplateInstantiationRec(Element e, Element instantiation) {
|
||||
instantiation.(Function).isConstructedFrom(_) and
|
||||
e = instantiation
|
||||
|
||||
@@ -80,11 +80,7 @@ abstract class StackVariableReachability extends string {
|
||||
j > i and
|
||||
sink = bb.getNode(j) and
|
||||
this.isSink(sink, v) and
|
||||
not exists(int k, ControlFlowNode node |
|
||||
node = bb.getNode(k) and this.isBarrier(pragma[only_bind_into](node), v)
|
||||
|
|
||||
k in [i + 1 .. j - 1]
|
||||
)
|
||||
not exists(int k | this.isBarrier(bb.getNode(k), v) | k in [i + 1 .. j - 1])
|
||||
)
|
||||
or
|
||||
not exists(int k | this.isBarrier(bb.getNode(k), v) | k > i) and
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
|
||||
@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
|
||||
@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
|
||||
@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
|
||||
@@ -25,7 +25,6 @@ predicate guardedAbs(Operation e, Expr use) {
|
||||
* Holds if the value of `use` is guarded to be less than something, and `e`
|
||||
* is in code controlled by that guard (where the guard condition held).
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate guardedLesser(Operation e, Expr use) {
|
||||
exists(GuardCondition c | c.ensuresLt(use, _, _, e.getBasicBlock(), true))
|
||||
or
|
||||
@@ -36,7 +35,6 @@ predicate guardedLesser(Operation e, Expr use) {
|
||||
* Holds if the value of `use` is guarded to be greater than something, and `e`
|
||||
* is in code controlled by that guard (where the guard condition held).
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate guardedGreater(Operation e, Expr use) {
|
||||
exists(GuardCondition c | c.ensuresLt(use, _, _, e.getBasicBlock(), false))
|
||||
or
|
||||
|
||||
@@ -1,21 +1,3 @@
|
||||
## 0.1.0
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* The `cpp/cleartext-transmission` query now recognizes additional sources, for sensitive private data such as e-mail addresses and credit card numbers.
|
||||
* The `cpp/unused-local-variable` no longer ignores functions that include lambda expressions capturing trivially copyable objects.
|
||||
* The `cpp/command-line-injection` query now takes into account calling contexts across string concatenations. This removes false positives due to mismatched calling contexts before and after string concatenations.
|
||||
* A new query, "Potential exposure of sensitive system data to an unauthorized control sphere" (`cpp/potential-system-data-exposure`) has been added. This query is focused on exposure of information that is highly likely to be sensitive, whereas the similar query "Exposure of system data to an unauthorized control sphere" (`cpp/system-data-exposure`) is focused on exposure of information on a channel that is more likely to be intercepted by an attacker.
|
||||
|
||||
## 0.0.13
|
||||
|
||||
## 0.0.12
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* The `cpp/overflow-destination`, `cpp/unclear-array-index-validation`, and `cpp/uncontrolled-allocation-size` queries have been modernized and converted to `path-problem` queries and provide more true positive results.
|
||||
* The `cpp/system-data-exposure` query has been increased from `medium` to `high` precision, following a number of improvements to the query logic.
|
||||
|
||||
## 0.0.11
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
@@ -116,8 +116,8 @@ class ExecTaintConfiguration extends TaintTracking::Configuration {
|
||||
state instanceof ConcatState
|
||||
}
|
||||
|
||||
override predicate isSanitizerOut(DataFlow::Node node) {
|
||||
isSink(node, _) // Prevent duplicates along a call chain, since `shellCommand` will include wrappers
|
||||
override predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
isSink(node, state) // Prevent duplicates along a call chain, since `shellCommand` will include wrappers
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* A new query, "Potential exposure of sensitive system data to an unauthorized control sphere" (`cpp/potential-system-data-exposure`) has been added. This query is focused on exposure of information that is highly likely to be sensitive, whereas the similar query "Exposure of system data to an unauthorized control sphere" (`cpp/system-data-exposure`) is focused on exposure of information on a channel that is more likely to be intercepted by an attacker.
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* The `cpp/system-data-exposure` query has been increased from `medium` to `high` precision, following a number of improvements to the query logic.
|
||||
@@ -1,6 +1,4 @@
|
||||
## 0.0.12
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* The `cpp/overflow-destination`, `cpp/unclear-array-index-validation`, and `cpp/uncontrolled-allocation-size` queries have been modernized and converted to `path-problem` queries and provide more true positive results.
|
||||
* The `cpp/system-data-exposure` query has been increased from `medium` to `high` precision, following a number of improvements to the query logic.
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* The `cpp/command-line-injection` query now takes into account calling contexts across string concatenations. This removes false positives due to mismatched calling contexts before and after string concatenations.
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* The `cpp/unused-local-variable` no longer ignores functions that include lambda expressions capturing trivially copyable objects.
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* The `cpp/cleartext-transmission` query now recognizes additional sources, for sensitive private data such as e-mail addresses and credit card numbers.
|
||||
@@ -1 +0,0 @@
|
||||
## 0.0.13
|
||||
@@ -1,8 +0,0 @@
|
||||
## 0.1.0
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* The `cpp/cleartext-transmission` query now recognizes additional sources, for sensitive private data such as e-mail addresses and credit card numbers.
|
||||
* The `cpp/unused-local-variable` no longer ignores functions that include lambda expressions capturing trivially copyable objects.
|
||||
* The `cpp/command-line-injection` query now takes into account calling contexts across string concatenations. This removes false positives due to mismatched calling contexts before and after string concatenations.
|
||||
* A new query, "Potential exposure of sensitive system data to an unauthorized control sphere" (`cpp/potential-system-data-exposure`) has been added. This query is focused on exposure of information that is highly likely to be sensitive, whereas the similar query "Exposure of system data to an unauthorized control sphere" (`cpp/system-data-exposure`) is focused on exposure of information on a channel that is more likely to be intercepted by an attacker.
|
||||
@@ -1,2 +1,2 @@
|
||||
---
|
||||
lastReleaseVersion: 0.1.0
|
||||
lastReleaseVersion: 0.0.11
|
||||
|
||||
@@ -21,7 +21,7 @@ class WriteAccessCheckMacro extends Macro {
|
||||
VariableAccess va;
|
||||
|
||||
WriteAccessCheckMacro() {
|
||||
this.getName() = ["user_write_access_begin", "user_access_begin", "access_ok"] and
|
||||
this.getName() = ["user_write_access_begin", "user_access_begin"] and
|
||||
va.getEnclosingElement() = this.getAnInvocation().getAnExpandedElement()
|
||||
}
|
||||
|
||||
@@ -37,8 +37,7 @@ class UnSafePutUserMacro extends Macro {
|
||||
}
|
||||
|
||||
Expr getUserModePtr() {
|
||||
result = writeUserPtr.getOperand().(AddressOfExpr).getOperand().(FieldAccess).getQualifier() or
|
||||
result = writeUserPtr.getOperand()
|
||||
result = writeUserPtr.getOperand().(AddressOfExpr).getOperand().(FieldAccess).getQualifier()
|
||||
}
|
||||
}
|
||||
|
||||
@@ -47,13 +46,11 @@ class ExploitableUserModePtrParam extends Parameter {
|
||||
not exists(WriteAccessCheckMacro writeAccessCheck |
|
||||
DataFlow::localFlow(DataFlow::parameterNode(this),
|
||||
DataFlow::exprNode(writeAccessCheck.getArgument()))
|
||||
) and
|
||||
exists(UnSafePutUserMacro unsafePutUser |
|
||||
DataFlow::localFlow(DataFlow::parameterNode(this),
|
||||
DataFlow::exprNode(unsafePutUser.getUserModePtr()))
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
from ExploitableUserModePtrParam p
|
||||
from ExploitableUserModePtrParam p, UnSafePutUserMacro unsafePutUser
|
||||
where
|
||||
DataFlow::localFlow(DataFlow::parameterNode(p), DataFlow::exprNode(unsafePutUser.getUserModePtr()))
|
||||
select p, "unsafe_put_user write user-mode pointer $@ without check.", p, p.toString()
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
name: codeql/cpp-queries
|
||||
version: 0.1.0
|
||||
version: 0.0.12-dev
|
||||
groups:
|
||||
- cpp
|
||||
- queries
|
||||
|
||||
@@ -1,4 +1,5 @@
|
||||
name: codeql/csharp-downgrades
|
||||
groups: csharp
|
||||
version: 0.0.6-dev
|
||||
downgrades: .
|
||||
library: true
|
||||
library: true
|
||||
@@ -1,9 +1,3 @@
|
||||
## 1.1.0
|
||||
|
||||
## 1.0.7
|
||||
|
||||
## 1.0.6
|
||||
|
||||
## 1.0.5
|
||||
|
||||
## 1.0.4
|
||||
|
||||
@@ -1 +0,0 @@
|
||||
## 1.0.6
|
||||
@@ -1 +0,0 @@
|
||||
## 1.0.7
|
||||
@@ -1 +0,0 @@
|
||||
## 1.1.0
|
||||
@@ -1,2 +1,2 @@
|
||||
---
|
||||
lastReleaseVersion: 1.1.0
|
||||
lastReleaseVersion: 1.0.5
|
||||
|
||||
@@ -1,8 +1,8 @@
|
||||
name: codeql/csharp-solorigate-all
|
||||
version: 1.1.0
|
||||
version: 1.0.6-dev
|
||||
groups:
|
||||
- csharp
|
||||
- solorigate
|
||||
library: true
|
||||
dependencies:
|
||||
codeql/csharp-all: "*"
|
||||
codeql/csharp-all: ~0.0.3
|
||||
|
||||
@@ -1,9 +1,3 @@
|
||||
## 1.1.0
|
||||
|
||||
## 1.0.7
|
||||
|
||||
## 1.0.6
|
||||
|
||||
## 1.0.5
|
||||
|
||||
## 1.0.4
|
||||
|
||||
@@ -1 +0,0 @@
|
||||
## 1.0.6
|
||||
@@ -1 +0,0 @@
|
||||
## 1.0.7
|
||||
@@ -1 +0,0 @@
|
||||
## 1.1.0
|
||||
@@ -1,2 +1,2 @@
|
||||
---
|
||||
lastReleaseVersion: 1.1.0
|
||||
lastReleaseVersion: 1.0.5
|
||||
|
||||
@@ -1,9 +1,9 @@
|
||||
name: codeql/csharp-solorigate-queries
|
||||
version: 1.1.0
|
||||
version: 1.0.6-dev
|
||||
groups:
|
||||
- csharp
|
||||
- solorigate
|
||||
defaultSuiteFile: codeql-suites/solorigate.qls
|
||||
dependencies:
|
||||
codeql/csharp-all: "*"
|
||||
codeql/csharp-solorigate-all: "*"
|
||||
codeql/csharp-all: ~0.0.3
|
||||
codeql/csharp-solorigate-all: ^1.0
|
||||
|
||||
@@ -1,30 +1,3 @@
|
||||
## 0.1.0
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
* The recently added flow-state versions of `isBarrierIn`, `isBarrierOut`, `isSanitizerIn`, and `isSanitizerOut` in the data flow and taint tracking libraries have been removed.
|
||||
|
||||
## 0.0.13
|
||||
|
||||
## 0.0.12
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
* The flow state variants of `isBarrier` and `isAdditionalFlowStep` are no longer exposed in the taint tracking library. The `isSanitizer` and `isAdditionalTaintStep` predicates should be used instead.
|
||||
|
||||
### Deprecated APIs
|
||||
|
||||
* Many classes/predicates/modules that had upper-case acronyms have been renamed to follow our style-guide.
|
||||
The old name still exists as a deprecated alias.
|
||||
|
||||
### New Features
|
||||
|
||||
* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states.
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* All deprecated predicates/classes/modules that have been deprecated for over a year have been deleted.
|
||||
|
||||
## 0.0.11
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: minorAnalysis
|
||||
---
|
||||
* All deprecated predicates/classes/modules that have been deprecated for over a year have been deleted.
|
||||
@@ -0,0 +1,5 @@
|
||||
---
|
||||
category: deprecated
|
||||
---
|
||||
* Many classes/predicates/modules that had upper-case acronyms have been renamed to follow our style-guide.
|
||||
The old name still exists as a deprecated alias.
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: feature
|
||||
---
|
||||
* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states.
|
||||
@@ -0,0 +1,4 @@
|
||||
---
|
||||
category: breaking
|
||||
---
|
||||
* The flow state variants of `isBarrier` and `isAdditionalFlowStep` are no longer exposed in the taint tracking library. The `isSanitizer` and `isAdditionalTaintStep` predicates should be used instead.
|
||||
@@ -1,18 +0,0 @@
|
||||
## 0.0.12
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
* The flow state variants of `isBarrier` and `isAdditionalFlowStep` are no longer exposed in the taint tracking library. The `isSanitizer` and `isAdditionalTaintStep` predicates should be used instead.
|
||||
|
||||
### Deprecated APIs
|
||||
|
||||
* Many classes/predicates/modules that had upper-case acronyms have been renamed to follow our style-guide.
|
||||
The old name still exists as a deprecated alias.
|
||||
|
||||
### New Features
|
||||
|
||||
* The data flow and taint tracking libraries have been extended with versions of `isBarrierIn`, `isBarrierOut`, and `isBarrierGuard`, respectively `isSanitizerIn`, `isSanitizerOut`, and `isSanitizerGuard`, that support flow states.
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
* All deprecated predicates/classes/modules that have been deprecated for over a year have been deleted.
|
||||
@@ -1 +0,0 @@
|
||||
## 0.0.13
|
||||
@@ -1,5 +0,0 @@
|
||||
## 0.1.0
|
||||
|
||||
### Breaking Changes
|
||||
|
||||
* The recently added flow-state versions of `isBarrierIn`, `isBarrierOut`, `isSanitizerIn`, and `isSanitizerOut` in the data flow and taint tracking libraries have been removed.
|
||||
@@ -1,2 +1,2 @@
|
||||
---
|
||||
lastReleaseVersion: 0.1.0
|
||||
lastReleaseVersion: 0.0.11
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
name: codeql/csharp-all
|
||||
version: 0.1.0
|
||||
version: 0.0.12-dev
|
||||
groups: csharp
|
||||
dbscheme: semmlecode.csharp.dbscheme
|
||||
extractor: csharp
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -87,9 +87,21 @@ abstract class Configuration extends string {
|
||||
/** Holds if data flow into `node` is prohibited. */
|
||||
predicate isBarrierIn(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow into `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierIn(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow out of `node` is prohibited. */
|
||||
predicate isBarrierOut(Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if data flow out of `node` is prohibited when the flow state is
|
||||
* `state`
|
||||
*/
|
||||
predicate isBarrierOut(Node node, FlowState state) { none() }
|
||||
|
||||
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
|
||||
predicate isBarrierGuard(BarrierGuard guard) { none() }
|
||||
|
||||
@@ -309,7 +321,7 @@ private class RetNodeEx extends NodeEx {
|
||||
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
|
||||
}
|
||||
|
||||
private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
private predicate fullInBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n)
|
||||
@@ -318,7 +330,16 @@ private predicate inBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierIn(n, state)
|
||||
|
|
||||
config.isSource(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fullOutBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n)
|
||||
@@ -327,6 +348,15 @@ private predicate outBarrier(NodeEx node, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
|
||||
exists(Node n |
|
||||
node.asNode() = n and
|
||||
config.isBarrierOut(n, state)
|
||||
|
|
||||
config.isSink(n, state)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fullBarrier(NodeEx node, Configuration config) {
|
||||
exists(Node n | node.asNode() = n |
|
||||
@@ -352,6 +382,12 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
|
||||
exists(Node n | node.asNode() = n |
|
||||
config.isBarrier(n, state)
|
||||
or
|
||||
config.isBarrierIn(n, state) and
|
||||
not config.isSource(n, state)
|
||||
or
|
||||
config.isBarrierOut(n, state) and
|
||||
not config.isSink(n, state)
|
||||
or
|
||||
exists(BarrierGuard g |
|
||||
config.isBarrierGuard(g, state) and
|
||||
n = g.getAGuardedNode()
|
||||
@@ -384,8 +420,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
|
||||
/** Provides the relevant barriers for a step from `node1` to `node2`. */
|
||||
pragma[inline]
|
||||
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
not fullOutBarrier(node1, config) and
|
||||
not fullInBarrier(node2, config) and
|
||||
not fullBarrier(node1, config) and
|
||||
not fullBarrier(node2, config)
|
||||
}
|
||||
@@ -438,6 +474,8 @@ private predicate additionalLocalStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config)
|
||||
)
|
||||
@@ -479,6 +517,8 @@ private predicate additionalJumpStateStep(
|
||||
config.isAdditionalFlowStep(n1, s1, n2, s2) and
|
||||
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
|
||||
stepFilter(node1, node2, config) and
|
||||
not stateOutBarrier(node1, s1, config) and
|
||||
not stateInBarrier(node2, s2, config) and
|
||||
not stateBarrier(node1, s1, config) and
|
||||
not stateBarrier(node2, s2, config) and
|
||||
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
|
||||
@@ -878,8 +918,8 @@ private module Stage1 {
|
||||
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
|
||||
revFlow(node, true, config) and
|
||||
fwdFlow(node, true, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
not fullInBarrier(node, config) and
|
||||
not fullOutBarrier(node, config)
|
||||
}
|
||||
|
||||
/** Holds if flow may return from `callable`. */
|
||||
@@ -974,8 +1014,8 @@ private predicate flowOutOfCallNodeCand1(
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
not fullOutBarrier(ret, config) and
|
||||
not fullInBarrier(out, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
@@ -996,8 +1036,8 @@ private predicate flowIntoCallNodeCand1(
|
||||
) {
|
||||
viableParamArgNodeCand1(call, p, arg, config) and
|
||||
Stage1::revFlow(p, config) and
|
||||
not outBarrier(arg, config) and
|
||||
not inBarrier(p, config)
|
||||
not fullOutBarrier(arg, config) and
|
||||
not fullInBarrier(p, config)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1118,8 +1158,8 @@ private module Stage2 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
bindingset[node1, state1, config]
|
||||
bindingset[node2, state2, config]
|
||||
@@ -1206,7 +1246,7 @@ private module Stage2 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -1911,8 +1951,8 @@ private module Stage3 {
|
||||
bindingset[call, c, innercc]
|
||||
private CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) { any() }
|
||||
|
||||
private predicate localStep(
|
||||
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
|
||||
@@ -1995,7 +2035,7 @@ private module Stage3 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -2725,11 +2765,12 @@ private module Stage4 {
|
||||
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
|
||||
}
|
||||
|
||||
bindingset[node, cc]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc) {
|
||||
bindingset[node, cc, config]
|
||||
private LocalCc getLocalCc(NodeEx node, Cc cc, Configuration config) {
|
||||
result =
|
||||
getLocalCallContext(pragma[only_bind_into](pragma[only_bind_out](cc)),
|
||||
node.getEnclosingCallable())
|
||||
node.getEnclosingCallable()) and
|
||||
exists(config)
|
||||
}
|
||||
|
||||
private predicate localStep(
|
||||
@@ -2822,7 +2863,7 @@ private module Stage4 {
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
localCc = getLocalCc(mid, cc, config)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
ap = ap0
|
||||
@@ -5007,7 +5048,6 @@ private module FlowExploration {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revPartialPathStep(
|
||||
PartialPathNodeRev mid, NodeEx node, FlowState state, TRevSummaryCtx1 sc1, TRevSummaryCtx2 sc2,
|
||||
TRevSummaryCtx3 sc3, RevPartialAccessPath ap, Configuration config
|
||||
|
||||
@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
|
||||
@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
|
||||
@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
|
||||
@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
|
||||
@@ -109,6 +109,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
/** Holds if taint propagation into `node` is prohibited. */
|
||||
predicate isSanitizerIn(DataFlow::Node node) { none() }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation into `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerIn(node, state)
|
||||
}
|
||||
|
||||
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
|
||||
|
||||
/** Holds if taint propagation out of `node` is prohibited. */
|
||||
@@ -116,6 +126,16 @@ abstract class Configuration extends DataFlow::Configuration {
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
|
||||
|
||||
/**
|
||||
* Holds if taint propagation out of `node` is prohibited when the flow state is
|
||||
* `state`.
|
||||
*/
|
||||
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
|
||||
|
||||
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
|
||||
this.isSanitizerOut(node, state)
|
||||
}
|
||||
|
||||
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
|
||||
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
|
||||
|
||||
|
||||
@@ -1,9 +1,3 @@
|
||||
## 0.1.0
|
||||
|
||||
## 0.0.13
|
||||
|
||||
## 0.0.12
|
||||
|
||||
## 0.0.11
|
||||
|
||||
### Minor Analysis Improvements
|
||||
|
||||
@@ -1 +0,0 @@
|
||||
## 0.0.12
|
||||
@@ -1 +0,0 @@
|
||||
## 0.0.13
|
||||
@@ -1 +0,0 @@
|
||||
## 0.1.0
|
||||
@@ -1,2 +1,2 @@
|
||||
---
|
||||
lastReleaseVersion: 0.1.0
|
||||
lastReleaseVersion: 0.0.11
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
name: codeql/csharp-queries
|
||||
version: 0.1.0
|
||||
version: 0.0.12-dev
|
||||
groups:
|
||||
- csharp
|
||||
- queries
|
||||
|
||||
@@ -1,9 +1,7 @@
|
||||
/**
|
||||
* @name Capture sink models.
|
||||
* @description Finds public methods that act as sinks as they flow into a a known sink.
|
||||
* @kind diagnostic
|
||||
* @id cs/utils/model-generator/sink-models
|
||||
* @tags model-generator
|
||||
*/
|
||||
|
||||
private import internal.CaptureModels
|
||||
|
||||
@@ -1,9 +1,7 @@
|
||||
/**
|
||||
* @name Capture source models.
|
||||
* @description Finds APIs that act as sources as they expose already known sources.
|
||||
* @kind diagnostic
|
||||
* @id cs/utils/model-generator/source-models
|
||||
* @tags model-generator
|
||||
*/
|
||||
|
||||
private import internal.CaptureModels
|
||||
|
||||
@@ -1,9 +1,7 @@
|
||||
/**
|
||||
* @name Capture summary models.
|
||||
* @description Finds applicable summary models to be used by other queries.
|
||||
* @kind diagnostic
|
||||
* @id cs/utils/model-generator/summary-models
|
||||
* @tags model-generator
|
||||
*/
|
||||
|
||||
private import semmle.code.csharp.dataflow.ExternalFlow
|
||||
|
||||
5
defs.bzl
5
defs.bzl
@@ -1,5 +0,0 @@
|
||||
codeql_platform = select({
|
||||
"@platforms//os:linux": "linux64",
|
||||
"@platforms//os:macos": "osx64",
|
||||
"@platforms//os:windows": "win64",
|
||||
})
|
||||
@@ -100,12 +100,12 @@ As a consequence, ``A != B`` has a very different meaning to the :ref:`negation
|
||||
- ``1 = [1 .. 2]`` holds, because ``1 = 1``.
|
||||
- ``not 1 = [1 .. 2]`` doesn't hold, because there is a common value (``1``).
|
||||
|
||||
#. Compare ``1`` and ``int empty() { none() }`` (a predicate defining the empty set of integers):
|
||||
- ``1 != empty()`` doesn't hold, because there are no values in ``empty()``, so no values
|
||||
#. Compare ``1`` and ``none()`` (the "empty set"):
|
||||
- ``1 != none()`` doesn't hold, because there are no values in ``none()``, so no values
|
||||
that are not equal to ``1``.
|
||||
- ``1 = empty()`` also doesn't hold, because there are no values in ``empty()``, so no values
|
||||
- ``1 = none()`` also doesn't hold, because there are no values in ``none()``, so no values
|
||||
that are equal to ``1``.
|
||||
- ``not 1 = empty()`` holds, because there are no common values.
|
||||
- ``not 1 = none()`` holds, because there are no common values.
|
||||
|
||||
.. index:: instanceof
|
||||
.. _type-checks:
|
||||
@@ -295,48 +295,9 @@ necessary, since they highlight the default precedence. You usually only add par
|
||||
override the default precedence, but you can also add them to make your code easier to read
|
||||
(even if they aren't required).
|
||||
|
||||
QL also has two nullary connectives indicating the always true formula,
|
||||
``any()``, and the always false formula, ``none()``.
|
||||
|
||||
The logical connectives in QL work similarly to Boolean connectives in other programming
|
||||
languages. Here is a brief overview:
|
||||
|
||||
.. index:: any, true
|
||||
.. _true:
|
||||
|
||||
``any()``
|
||||
=========
|
||||
|
||||
The built-in predicate ``any()`` is a formula that always holds.
|
||||
|
||||
**Example**
|
||||
|
||||
The following predicate defines the set of all expressions.
|
||||
|
||||
.. code-block:: ql
|
||||
|
||||
Expr allExpressions() {
|
||||
any()
|
||||
}
|
||||
|
||||
.. index:: none, false
|
||||
.. _false:
|
||||
|
||||
``none()``
|
||||
==========
|
||||
|
||||
The built-in predicate ``none()`` is a formula that never holds.
|
||||
|
||||
**Example**
|
||||
|
||||
The following predicate defines the empty set of integers.
|
||||
|
||||
.. code-block:: ql
|
||||
|
||||
int emptySet() {
|
||||
none()
|
||||
}
|
||||
|
||||
.. index:: not, negation
|
||||
.. _negation:
|
||||
|
||||
|
||||
Some files were not shown because too many files have changed in this diff Show More
Reference in New Issue
Block a user