hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-07-20 18:58:36 +02:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'main' into mathiasvp/replace-ast-with-ir-use-usedataflow

Browse Source
This commit is contained in:
Mathias Vorreiter Pedersen
2023-01-23 15:49:36 +00:00
parent 3f9deb66ce 0a0d6d0841
commit 79b77b01fd
942 changed files with 231363 additions and 11593 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
.github/actions/fetch-codeql/action.yml vendored
View File

@@ -19,4 +19,6 @@ runs:
gh extension install github/gh-codeql
gh codeql set-channel "$CHANNEL"
gh codeql version
printf "CODEQL_FETCHED_CODEQL_PATH=" >> "${GITHUB_ENV}"
gh codeql version --format=json | jq -r .unpackedLocation >> "${GITHUB_ENV}"
gh codeql version --format=json | jq -r .unpackedLocation >> "${GITHUB_PATH}"

32
.github/actions/os-version/action.yml vendored Normal file
View File

@@ -0,0 +1,32 @@
name: OS Version
description: Get OS version.
outputs:
version:
description: "OS version"
value: ${{ steps.version.outputs.version }}
runs:
using: composite
steps:
- if: runner.os == 'Linux'
shell: bash
run: |
. /etc/os-release
echo "VERSION=${NAME} ${VERSION}" >> $GITHUB_ENV
- if: runner.os == 'Windows'
shell: powershell
run: |
$objects = systeminfo.exe /FO CSV | ConvertFrom-Csv
"VERSION=$($objects.'OS Name') $($objects.'OS Version')" >> $env:GITHUB_ENV
- if: runner.os == 'macOS'
shell: bash
run: |
echo "VERSION=$(sw_vers -productName) $(sw_vers -productVersion)" >> $GITHUB_ENV
- name: Emit OS version
id: version
shell: bash
run: |
echo "$VERSION"
echo "version=${VERSION}" >> $GITHUB_OUTPUT

10
.github/workflows/mad_modelDiff.yml vendored
View File

@@ -11,7 +11,7 @@ on:
branches:
- main
paths:
- "java/ql/src/utils/model-generator/**/*.*"
- "java/ql/src/utils/modelgenerator/**/*.*"
- ".github/workflows/mad_modelDiff.yml"
permissions:
@@ -40,12 +40,12 @@ jobs:
- name: Download database
env:
SLUG: ${{ matrix.slug }}
GH_TOKEN: ${{ github.token }}
run: |
set -x
mkdir lib-dbs
SHORTNAME=${SLUG//[^a-zA-Z0-9_]/}
projectId=`curl -s https://lgtm.com/api/v1.0/projects/g/${SLUG} | jq .id`
curl -L "https://lgtm.com/api/v1.0/snapshots/$projectId/java" -o "$SHORTNAME.zip"
gh api -H "Accept: application/zip" "/repos/${SLUG}/code-scanning/codeql/databases/java" > "$SHORTNAME.zip"
unzip -q -d "${SHORTNAME}-db" "${SHORTNAME}.zip"
mkdir "lib-dbs/$SHORTNAME/"
mv "${SHORTNAME}-db/"$(ls -1 "${SHORTNAME}"-db)/* "lib-dbs/${SHORTNAME}/"
@@ -61,7 +61,7 @@ jobs:
DATABASE=$2
cd codeql-$QL_VARIANT
SHORTNAME=`basename $DATABASE`
python java/ql/src/utils/model-generator/GenerateFlowModel.py --with-summaries --with-sinks $DATABASE ${SHORTNAME}.temp.model.yml
python java/ql/src/utils/modelgenerator/GenerateFlowModel.py --with-summaries --with-sinks $DATABASE ${SHORTNAME}.temp.model.yml
mv java/ql/lib/ext/generated/${SHORTNAME}.temp.model.yml $MODELS/${SHORTNAME}Generated_${QL_VARIANT}.model.yml
cd ..
}
@@ -100,4 +100,6 @@ jobs:
with:
name: diffs
path: tmp-models/*.html
# An html file is only produced if the generated models differ.
if-no-files-found: ignore
retention-days: 20

2
.github/workflows/mad_regenerate-models.yml vendored
View File

@@ -50,7 +50,7 @@ jobs:
SLUG: ${{ matrix.slug }}
run: |
SHORTNAME=${SLUG//[^a-zA-Z0-9_]/}
java/ql/src/utils/model-generator/RegenerateModels.py "${SLUG}" dbs/${SHORTNAME}
java/ql/src/utils/modelgenerator/RegenerateModels.py "${SLUG}" dbs/${SHORTNAME}
- name: Stage changes
run: |
find java -name "*.model.yml" -print0 | xargs -0 git add

20
.github/workflows/ql-for-ql-build.yml vendored
View File

@@ -27,7 +27,7 @@ jobs:
uses: ./.github/actions/find-latest-bundle
- name: Find codeql
id: find-codeql
uses: github/codeql-action/init@77a8d2d10c0b403a8b4aadbd223dc489ecd22683
uses: github/codeql-action/init@45955cb1830b640e2c1603ad72ad542a49d47b96
with:
languages: javascript # does not matter
tools: ${{ steps.find-latest-bundle.outputs.url }}
@@ -38,12 +38,14 @@ jobs:
shell: bash
env:
CODEQL: ${{ steps.find-codeql.outputs.codeql-path }}
- uses: ./.github/actions/os-version
id: os_version
- name: Cache entire pack
id: cache-pack
uses: actions/cache@v3
with:
path: ${{ runner.temp }}/pack
key: ${{ runner.os }}-pack-${{ hashFiles('ql/**/Cargo.lock') }}-${{ hashFiles('ql/**/*.rs') }}-${{ hashFiles('ql/**/*.ql*') }}-${{ hashFiles('ql/**/qlpack.yml') }}-${{ hashFiles('ql/ql/src/ql.dbscheme*') }}-${{ steps.get-codeql-version.outputs.version }}--${{ hashFiles('.github/workflows/ql-for-ql-build.yml') }}
key: ${{ runner.os }}-${{ steps.os_version.outputs.version }}-pack-${{ hashFiles('ql/**/Cargo.lock') }}-${{ hashFiles('ql/**/*.rs') }}-${{ hashFiles('ql/**/*.ql*') }}-${{ hashFiles('ql/**/qlpack.yml') }}-${{ hashFiles('ql/ql/src/ql.dbscheme*') }}-${{ steps.get-codeql-version.outputs.version }}--${{ hashFiles('.github/workflows/ql-for-ql-build.yml') }}
- name: Cache queries
if: steps.cache-pack.outputs.cache-hit != 'true'
id: cache-queries
@@ -77,7 +79,7 @@ jobs:
ql/target/release/ql-autobuilder.exe
ql/target/release/ql-extractor
ql/target/release/ql-extractor.exe
key: ${{ runner.os }}-extractor-${{ hashFiles('ql/**/Cargo.lock') }}-${{ hashFiles('ql/**/*.rs') }}
key: ${{ runner.os }}-${{ steps.os_version.outputs.version }}-extractor-${{ hashFiles('ql/**/Cargo.lock') }}-${{ hashFiles('ql/**/*.rs') }}
- name: Cache cargo
if: steps.cache-extractor.outputs.cache-hit != 'true' && steps.cache-pack.outputs.cache-hit != 'true'
uses: actions/cache@v3
@@ -86,7 +88,7 @@ jobs:
~/.cargo/registry
~/.cargo/git
ql/target
key: ${{ runner.os }}-rust-cargo-${{ hashFiles('ql/**/Cargo.lock') }}
key: ${{ runner.os }}-${{ steps.os_version.outputs.version }}-rust-cargo-${{ hashFiles('ql/**/Cargo.lock') }}
- name: Check formatting
if: steps.cache-extractor.outputs.cache-hit != 'true' && steps.cache-pack.outputs.cache-hit != 'true'
run: cd ql; cargo fmt --all -- --check
@@ -137,20 +139,20 @@ jobs:
env:
CONF: ./ql-for-ql-config.yml
- name: Initialize CodeQL
uses: github/codeql-action/init@77a8d2d10c0b403a8b4aadbd223dc489ecd22683
uses: github/codeql-action/init@45955cb1830b640e2c1603ad72ad542a49d47b96
with:
languages: ql
db-location: ${{ runner.temp }}/db
config-file: ./ql-for-ql-config.yml
tools: ${{ steps.find-latest-bundle.outputs.url }}
- name: Move pack cache
- name: Move pack queries
run: |
cp -r ${PACK}/.cache ql/ql/src/.cache
cp -r ${PACK}/queries ql/ql/src
env:
PACK: ${{ runner.temp }}/pack
- name: Perform CodeQL Analysis
uses: github/codeql-action/analyze@77a8d2d10c0b403a8b4aadbd223dc489ecd22683
uses: github/codeql-action/analyze@45955cb1830b640e2c1603ad72ad542a49d47b96
with:
category: "ql-for-ql"
- name: Copy sarif file to CWD
@@ -172,4 +174,4 @@ jobs:
with:
name: ql-for-ql-langs
path: split-sarif
retention-days: 1
retention-days: 1

6
.github/workflows/ql-for-ql-dataset_measure.yml vendored
View File

@@ -25,16 +25,18 @@ jobs:
- name: Find codeql
id: find-codeql
uses: github/codeql-action/init@77a8d2d10c0b403a8b4aadbd223dc489ecd22683
uses: github/codeql-action/init@45955cb1830b640e2c1603ad72ad542a49d47b96
with:
languages: javascript # does not matter
- uses: ./.github/actions/os-version
id: os_version
- uses: actions/cache@v3
with:
path: |
~/.cargo/registry
~/.cargo/git
ql/target
key: ${{ runner.os }}-qltest-cargo-${{ hashFiles('ql/**/Cargo.lock') }}
key: ${{ runner.os }}-${{ steps.os_version.outputs.version }}-qltest-cargo-${{ hashFiles('ql/**/Cargo.lock') }}
- name: Build Extractor
run: cd ql; env "PATH=$PATH:`dirname ${CODEQL}`" ./scripts/create-extractor-pack.sh
env:

66
.github/workflows/ql-for-ql-tests.yml vendored
View File

@@ -22,28 +22,84 @@ jobs:
- uses: actions/checkout@v3
- name: Find codeql
id: find-codeql
uses: github/codeql-action/init@77a8d2d10c0b403a8b4aadbd223dc489ecd22683
uses: github/codeql-action/init@45955cb1830b640e2c1603ad72ad542a49d47b96
with:
languages: javascript # does not matter
- uses: ./.github/actions/os-version
id: os_version
- uses: actions/cache@v3
with:
path: |
~/.cargo/registry
~/.cargo/git
ql/target
key: ${{ runner.os }}-qltest-cargo-${{ hashFiles('ql/**/Cargo.lock') }}
key: ${{ runner.os }}-${{ steps.os_version.outputs.version }}-qltest-cargo-${{ hashFiles('ql/rust-toolchain.toml', 'ql/**/Cargo.lock') }}
- name: Build extractor
run: |
cd ql;
codeqlpath=$(dirname ${{ steps.find-codeql.outputs.codeql-path }});
env "PATH=$PATH:$codeqlpath" ./scripts/create-extractor-pack.sh
- name: Cache compilation cache
id: query-cache
uses: ./.github/actions/cache-query-compilation
with:
key: ql-for-ql-tests
- name: Run QL tests
run: |
"${CODEQL}" test run --check-databases --check-unused-labels --check-repeated-labels --check-redefined-labels --check-use-before-definition --search-path "${{ github.workspace }}/ql/extractor-pack" --consistency-queries ql/ql/consistency-queries ql/ql/test
"${CODEQL}" test run --check-databases --check-unused-labels --check-repeated-labels --check-redefined-labels --check-use-before-definition --search-path "${{ github.workspace }}/ql/extractor-pack" --consistency-queries ql/ql/consistency-queries --compilation-cache "${{ steps.query-cache.outputs.cache-dir }}" ql/ql/test
env:
CODEQL: ${{ steps.find-codeql.outputs.codeql-path }}
- name: Check QL formatting
other-os:
strategy:
matrix:
os: [macos-latest, windows-latest]
needs: [qltest]
runs-on: ${{ matrix.os }}
steps:
- uses: actions/checkout@v3
- name: Install GNU tar
if: runner.os == 'macOS'
run: |
find ql/ql/src "(" -name "*.ql" -or -name "*.qll" ")" -print0 | xargs -0 "${CODEQL}" query format --check-only
brew install gnu-tar
echo "/usr/local/opt/gnu-tar/libexec/gnubin" >> $GITHUB_PATH
- name: Find codeql
id: find-codeql
uses: github/codeql-action/init@77a8d2d10c0b403a8b4aadbd223dc489ecd22683
with:
languages: javascript # does not matter
- uses: ./.github/actions/os-version
id: os_version
- uses: actions/cache@v3
with:
path: |
~/.cargo/registry
~/.cargo/git
ql/target
key: ${{ runner.os }}-${{ steps.os_version.outputs.version }}-qltest-cargo-${{ hashFiles('ql/rust-toolchain.toml', 'ql/**/Cargo.lock') }}
- name: Build extractor
if: runner.os != 'Windows'
run: |
cd ql;
codeqlpath=$(dirname ${{ steps.find-codeql.outputs.codeql-path }});
env "PATH=$PATH:$codeqlpath" ./scripts/create-extractor-pack.sh
- name: Build extractor (Windows)
if: runner.os == 'Windows'
shell: pwsh
run: |
cd ql;
$Env:PATH += ";$(dirname ${{ steps.find-codeql.outputs.codeql-path }})"
pwsh ./scripts/create-extractor-pack.ps1
- name: Run a single QL tests - Unix
if: runner.os != 'Windows'
run: |
"${CODEQL}" test run --check-databases --search-path "${{ github.workspace }}/ql/extractor-pack" ql/ql/test/queries/style/DeadCode/DeadCode.qlref
env:
CODEQL: ${{ steps.find-codeql.outputs.codeql-path }}
- name: Run a single QL tests - Windows
if: runner.os == 'Windows'
shell: pwsh
run: |
$Env:PATH += ";$(dirname ${{ steps.find-codeql.outputs.codeql-path }})"
codeql test run --check-databases --search-path "${{ github.workspace }}/ql/extractor-pack" ql/ql/test/queries/style/DeadCode/DeadCode.qlref

28
.github/workflows/ruby-build.yml vendored
View File

@@ -48,6 +48,8 @@ jobs:
run: |
brew install gnu-tar
echo "/usr/local/opt/gnu-tar/libexec/gnubin" >> $GITHUB_PATH
- uses: ./.github/actions/os-version
id: os_version
- name: Cache entire extractor
uses: actions/cache@v3
id: cache-extractor
@@ -58,7 +60,7 @@ jobs:
ruby/target/release/ruby-extractor
ruby/target/release/ruby-extractor.exe
ruby/ql/lib/codeql/ruby/ast/internal/TreeSitter.qll
key: ${{ runner.os }}-ruby-extractor-${{ hashFiles('ruby/rust-toolchain.toml', 'ruby/**/Cargo.lock') }}--${{ hashFiles('ruby/**/*.rs') }}
key: ${{ runner.os }}-${{ steps.os_version.outputs.version }}-ruby-extractor-${{ hashFiles('ruby/rust-toolchain.toml', 'ruby/**/Cargo.lock') }}--${{ hashFiles('ruby/**/*.rs') }}
- uses: actions/cache@v3
if: steps.cache-extractor.outputs.cache-hit != 'true'
with:
@@ -66,7 +68,7 @@ jobs:
~/.cargo/registry
~/.cargo/git
ruby/target
key: ${{ runner.os }}-ruby-rust-cargo-${{ hashFiles('ruby/rust-toolchain.toml', 'ruby/**/Cargo.lock') }}
key: ${{ runner.os }}-${{ steps.os_version.outputs.version }}-ruby-rust-cargo-${{ hashFiles('ruby/rust-toolchain.toml', 'ruby/**/Cargo.lock') }}
- name: Check formatting
if: steps.cache-extractor.outputs.cache-hit != 'true'
run: cargo fmt --all -- --check
@@ -203,11 +205,6 @@ jobs:
- name: Fetch CodeQL
uses: ./.github/actions/fetch-codeql
- uses: actions/checkout@v3
with:
repository: Shopify/example-ruby-app
ref: 67a0decc5eb550f3a9228eda53925c3afd40dfe9
- name: Download Ruby bundle
uses: actions/download-artifact@v3
with:
@@ -216,26 +213,15 @@ jobs:
- name: Unzip Ruby bundle
shell: bash
run: unzip -q -d "${{ runner.temp }}/ruby-bundle" "${{ runner.temp }}/codeql-ruby-bundle.zip"
- name: Prepare test files
shell: bash
run: |
echo "import codeql.ruby.AST select count(File f)" > "test.ql"
echo "| 4 |" > "test.expected"
echo 'name: sample-tests
version: 0.0.0
dependencies:
codeql/ruby-all: "*"
extractor: ruby
tests: .
' > qlpack.yml
- name: Run QL test
shell: bash
run: |
codeql test run --search-path "${{ runner.temp }}/ruby-bundle" --additional-packs "${{ runner.temp }}/ruby-bundle" .
codeql test run --search-path "${{ runner.temp }}/ruby-bundle" --additional-packs "${{ runner.temp }}/ruby-bundle" ruby/ql/test/library-tests/ast/constants/
- name: Create database
shell: bash
run: |
codeql database create --search-path "${{ runner.temp }}/ruby-bundle" --language ruby --source-root . ../database
codeql database create --search-path "${{ runner.temp }}/ruby-bundle" --language ruby --source-root ruby/ql/test/library-tests/ast/constants/ ../database
- name: Analyze database
shell: bash
run: |

1
CONTRIBUTING.md
View File

@@ -25,6 +25,7 @@ If you have an idea for a query that you would like to share with other CodeQL u
Each language-specific directory contains further subdirectories that group queries based on their `@tags` or purpose.
- Experimental queries and libraries are stored in the `experimental` subdirectory within each language-specific directory in the [CodeQL repository](https://github.com/github/codeql). For example, experimental Java queries and libraries are stored in `java/ql/src/experimental` and any corresponding tests in `java/ql/test/experimental`.
- Experimental queries need to include `experimental` in their `@tags`
- The structure of an `experimental` subdirectory mirrors the structure of its parent directory.
- Select or create an appropriate directory in `experimental` based on the existing directory structure of `experimental` or its parent directory.

2
README.md
View File

@@ -10,6 +10,8 @@ There is [extensive documentation](https://codeql.github.com/docs/) on getting s
We welcome contributions to our standard library and standard checks. Do you have an idea for a new check, or how to improve an existing query? Then please go ahead and open a pull request! Before you do, though, please take the time to read our [contributing guidelines](CONTRIBUTING.md). You can also consult our [style guides](https://github.com/github/codeql/tree/main/docs) to learn how to format your code for consistency and clarity, how to write query metadata, and how to write query help documentation for your query.
For information on contributing to CodeQL documentation, see the "[contributing guide](docs/codeql/CONTRIBUTING.md)" for docs.
## License
The code in this repository is licensed under the [MIT License](LICENSE) by [GitHub](https://github.com).

1
config/identical-files.json
View File

@@ -29,6 +29,7 @@
"csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImplForContentDataFlow.qll",
"go/ql/lib/semmle/go/dataflow/internal/DataFlowImpl.qll",
"go/ql/lib/semmle/go/dataflow/internal/DataFlowImpl2.qll",
"go/ql/lib/semmle/go/dataflow/internal/DataFlowImplForStringsNewReplacer.qll",
"python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll",
"python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl2.qll",
"python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl3.qll",

4
cpp/ql/lib/CHANGELOG.md
View File

@@ -1,3 +1,7 @@
## 0.5.1
No user-facing changes.
## 0.5.0
### Breaking Changes

3
cpp/ql/lib/change-notes/released/0.5.1.md Normal file
View File

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

2
cpp/ql/lib/codeql-pack.release.yml
View File

@@ -1,2 +1,2 @@
---
lastReleaseVersion: 0.5.0
lastReleaseVersion: 0.5.1

15
cpp/ql/lib/definitions.qll
View File

@@ -123,6 +123,13 @@ private predicate constructorCallTypeMention(ConstructorCall cc, TypeMention tm)
)
}
/** Holds if `loc` has the container `container` and is on the line starting at `startLine`. */
pragma[nomagic]
private predicate hasContainerAndStartLine(Location loc, Container container, int startLine) {
loc.getStartLine() = startLine and
loc.getContainer() = container
}
/**
* Gets an element, of kind `kind`, that element `e` uses, if any.
* Attention: This predicate yields multiple definitions for a single location.
@@ -184,11 +191,9 @@ Top definitionOf(Top e, string kind) {
kind = "I" and
result = e.(Include).getIncludedFile() and
// exclude `#include` directives containing macros
not exists(MacroInvocation mi, Location l1, Location l2 |
l1 = e.(Include).getLocation() and
l2 = mi.getLocation() and
l1.getContainer() = l2.getContainer() and
l1.getStartLine() = l2.getStartLine()
not exists(MacroInvocation mi, Container container, int startLine |
hasContainerAndStartLine(e.(Include).getLocation(), container, startLine) and
hasContainerAndStartLine(mi.getLocation(), container, startLine)
// (an #include directive must be always on it's own line)
)
) and

12
cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImplConsistency.qll
View File

@@ -45,6 +45,16 @@ module Consistency {
) {
none()
}
/** Holds if `(c, pos, p)` should be excluded from the consistency test `uniqueParameterNodeAtPosition`. */
predicate uniqueParameterNodeAtPositionExclude(DataFlowCallable c, ParameterPosition pos, Node p) {
none()
}
/** Holds if `(c, pos, p)` should be excluded from the consistency test `uniqueParameterNodePosition`. */
predicate uniqueParameterNodePositionExclude(DataFlowCallable c, ParameterPosition pos, Node p) {
none()
}
}
private class RelevantNode extends Node {
@@ -246,6 +256,7 @@ module Consistency {
query predicate uniqueParameterNodeAtPosition(
DataFlowCallable c, ParameterPosition pos, Node p, string msg
) {
not any(ConsistencyConfiguration conf).uniqueParameterNodeAtPositionExclude(c, pos, p) and
isParameterNode(p, c, pos) and
not exists(unique(Node p0 | isParameterNode(p0, c, pos))) and
msg = "Parameters with overlapping positions."
@@ -254,6 +265,7 @@ module Consistency {
query predicate uniqueParameterNodePosition(
DataFlowCallable c, ParameterPosition pos, Node p, string msg
) {
not any(ConsistencyConfiguration conf).uniqueParameterNodePositionExclude(c, pos, p) and
isParameterNode(p, c, pos) and
not exists(unique(ParameterPosition pos0 | isParameterNode(p, c, pos0))) and
msg = "Parameter node with multiple positions."

29
cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/FloatDelta.qll Normal file
View File

@@ -0,0 +1,29 @@
private import RangeAnalysisStage
module FloatDelta implements DeltaSig {
class Delta = float;
bindingset[d]
bindingset[result]
float toFloat(Delta d) { result = d }
bindingset[d]
bindingset[result]
int toInt(Delta d) { result = d }
bindingset[n]
bindingset[result]
Delta fromInt(int n) { result = n }
bindingset[f]
Delta fromFloat(float f) {
result =
min(float diff, float res |
diff = (res - f) and res = f.ceil()
or
diff = (f - res) and res = f.floor()
|
res order by diff
)
}
}

601
cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/ModulusAnalysis.qll
View File

@@ -14,321 +14,328 @@ private import ModulusAnalysisSpecific::Private
private import experimental.semmle.code.cpp.semantic.Semantic
private import ConstantAnalysis
private import RangeUtils
private import RangeAnalysisStage
/**
* Holds if `e + delta` equals `v` at `pos`.
*/
private predicate valueFlowStepSsa(SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta) {
semSsaUpdateStep(v, e, delta) and pos.hasReadOfVar(v)
or
exists(SemGuard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = semEqFlowCond(v, e, delta, true, testIsTrue) and
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue)
)
}
/**
* Holds if `add` is the addition of `larg` and `rarg`, neither of which are
* `ConstantIntegerExpr`s.
*/
private predicate nonConstAddition(SemExpr add, SemExpr larg, SemExpr rarg) {
exists(SemAddExpr a | a = add |
larg = a.getLeftOperand() and
rarg = a.getRightOperand()
) and
not larg instanceof SemConstantIntegerExpr and
not rarg instanceof SemConstantIntegerExpr
}
/**
* Holds if `sub` is the subtraction of `larg` and `rarg`, where `rarg` is not
* a `ConstantIntegerExpr`.
*/
private predicate nonConstSubtraction(SemExpr sub, SemExpr larg, SemExpr rarg) {
exists(SemSubExpr s | s = sub |
larg = s.getLeftOperand() and
rarg = s.getRightOperand()
) and
not rarg instanceof SemConstantIntegerExpr
}
/** Gets an expression that is the remainder modulo `mod` of `arg`. */
private SemExpr modExpr(SemExpr arg, int mod) {
exists(SemRemExpr rem |
result = rem and
arg = rem.getLeftOperand() and
rem.getRightOperand().(SemConstantIntegerExpr).getIntValue() = mod and
mod >= 2
)
or
exists(SemConstantIntegerExpr c |
mod = 2.pow([1 .. 30]) and
c.getIntValue() = mod - 1 and
result.(SemBitAndExpr).hasOperands(arg, c)
)
}
/**
* Gets a guard that tests whether `v` is congruent with `val` modulo `mod` on
* its `testIsTrue` branch.
*/
private SemGuard moduloCheck(SemSsaVariable v, int val, int mod, boolean testIsTrue) {
exists(SemExpr rem, SemConstantIntegerExpr c, int r, boolean polarity |
result.isEquality(rem, c, polarity) and
c.getIntValue() = r and
rem = modExpr(v.getAUse(), mod) and
(
testIsTrue = polarity and val = r
or
testIsTrue = polarity.booleanNot() and
mod = 2 and
val = 1 - r and
(r = 0 or r = 1)
)
)
}
/**
* Holds if a guard ensures that `v` at `pos` is congruent with `val` modulo `mod`.
*/
private predicate moduloGuardedRead(SemSsaVariable v, SemSsaReadPosition pos, int val, int mod) {
exists(SemGuard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = moduloCheck(v, val, mod, testIsTrue) and
semGuardControlsSsaRead(guard, pos, testIsTrue)
)
}
/** Holds if `factor` is a power of 2 that divides `mask`. */
bindingset[mask]
private predicate andmaskFactor(int mask, int factor) {
mask % factor = 0 and
factor = 2.pow([1 .. 30])
}
/** Holds if `e` is evenly divisible by `factor`. */
private predicate evenlyDivisibleExpr(SemExpr e, int factor) {
exists(SemConstantIntegerExpr c, int k | k = c.getIntValue() |
e.(SemMulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2
or
e.(SemShiftLeftExpr).getRightOperand() = c and factor = 2.pow(k) and k > 0
or
e.(SemBitAndExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
)
}
/**
* Holds if `rix` is the number of input edges to `phi`.
*/
private predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
rix = max(int r | rankedPhiInput(phi, _, _, r))
}
/**
* Gets the remainder of `val` modulo `mod`.
*
* For `mod = 0` the result equals `val` and for `mod > 1` the result is within
* the range `[0 .. mod-1]`.
*/
bindingset[val, mod]
private int remainder(int val, int mod) {
mod = 0 and result = val
or
mod > 1 and result = ((val % mod) + mod) % mod
}
/**
* Holds if `inp` is an input to `phi` and equals `phi` modulo `mod` along `edge`.
*/
private predicate phiSelfModulus(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int mod
) {
exists(SemSsaBound phibound, int v, int m |
edge.phiInput(phi, inp) and
phibound.getAVariable() = phi and
ssaModulus(inp, edge, phibound, v, m) and
mod = m.gcd(v) and
mod != 1
)
}
/**
* Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
*/
private predicate phiModulusInit(SemSsaPhiNode phi, SemBound b, int val, int mod) {
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
edge.phiInput(phi, inp) and
ssaModulus(inp, edge, b, val, mod)
)
}
/**
* Holds if all inputs to `phi` numbered `1` to `rix` are equal to `b + val` modulo `mod`.
*/
pragma[nomagic]
private predicate phiModulusRankStep(SemSsaPhiNode phi, SemBound b, int val, int mod, int rix) {
/*
* base case. If any phi input is equal to `b + val` modulo `mod`, that's a potential congruence
* class for the phi node.
module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
/**
* Holds if `e + delta` equals `v` at `pos`.
*/
private predicate valueFlowStepSsa(SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta) {
U::semSsaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
or
exists(SemGuard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue)
)
}
rix = 0 and
phiModulusInit(phi, b, val, mod)
or
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int v1, int m1 |
mod != 1 and
val = remainder(v1, mod)
|
/**
* Holds if `add` is the addition of `larg` and `rarg`, neither of which are
* `ConstantIntegerExpr`s.
*/
private predicate nonConstAddition(SemExpr add, SemExpr larg, SemExpr rarg) {
exists(SemAddExpr a | a = add |
larg = a.getLeftOperand() and
rarg = a.getRightOperand()
) and
not larg instanceof SemConstantIntegerExpr and
not rarg instanceof SemConstantIntegerExpr
}
/**
* Holds if `sub` is the subtraction of `larg` and `rarg`, where `rarg` is not
* a `ConstantIntegerExpr`.
*/
private predicate nonConstSubtraction(SemExpr sub, SemExpr larg, SemExpr rarg) {
exists(SemSubExpr s | s = sub |
larg = s.getLeftOperand() and
rarg = s.getRightOperand()
) and
not rarg instanceof SemConstantIntegerExpr
}
/** Gets an expression that is the remainder modulo `mod` of `arg`. */
private SemExpr modExpr(SemExpr arg, int mod) {
exists(SemRemExpr rem |
result = rem and
arg = rem.getLeftOperand() and
rem.getRightOperand().(SemConstantIntegerExpr).getIntValue() = mod and
mod >= 2
)
or
exists(SemConstantIntegerExpr c |
mod = 2.pow([1 .. 30]) and
c.getIntValue() = mod - 1 and
result.(SemBitAndExpr).hasOperands(arg, c)
)
}
/**
* Gets a guard that tests whether `v` is congruent with `val` modulo `mod` on
* its `testIsTrue` branch.
*/
private SemGuard moduloCheck(SemSsaVariable v, int val, int mod, boolean testIsTrue) {
exists(SemExpr rem, SemConstantIntegerExpr c, int r, boolean polarity |
result.isEquality(rem, c, polarity) and
c.getIntValue() = r and
rem = modExpr(v.getAUse(), mod) and
(
testIsTrue = polarity and val = r
or
testIsTrue = polarity.booleanNot() and
mod = 2 and
val = 1 - r and
(r = 0 or r = 1)
)
)
}
/**
* Holds if a guard ensures that `v` at `pos` is congruent with `val` modulo `mod`.
*/
private predicate moduloGuardedRead(SemSsaVariable v, SemSsaReadPosition pos, int val, int mod) {
exists(SemGuard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = moduloCheck(v, val, mod, testIsTrue) and
semGuardControlsSsaRead(guard, pos, testIsTrue)
)
}
/** Holds if `factor` is a power of 2 that divides `mask`. */
bindingset[mask]
private predicate andmaskFactor(int mask, int factor) {
mask % factor = 0 and
factor = 2.pow([1 .. 30])
}
/** Holds if `e` is evenly divisible by `factor`. */
private predicate evenlyDivisibleExpr(SemExpr e, int factor) {
exists(SemConstantIntegerExpr c, int k | k = c.getIntValue() |
e.(SemMulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2
or
e.(SemShiftLeftExpr).getRightOperand() = c and factor = 2.pow(k) and k > 0
or
e.(SemBitAndExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
)
}
/**
* Holds if `rix` is the number of input edges to `phi`.
*/
private predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
rix = max(int r | rankedPhiInput(phi, _, _, r))
}
/**
* Gets the remainder of `val` modulo `mod`.
*
* For `mod = 0` the result equals `val` and for `mod > 1` the result is within
* the range `[0 .. mod-1]`.
*/
bindingset[val, mod]
private int remainder(int val, int mod) {
mod = 0 and result = val
or
mod > 1 and result = ((val % mod) + mod) % mod
}
/**
* Holds if `inp` is an input to `phi` and equals `phi` modulo `mod` along `edge`.
*/
private predicate phiSelfModulus(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int mod
) {
exists(Bounds::SemSsaBound phibound, int v, int m |
edge.phiInput(phi, inp) and
phibound.getAVariable() = phi and
ssaModulus(inp, edge, phibound, v, m) and
mod = m.gcd(v) and
mod != 1
)
}
/**
* Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
*/
private predicate phiModulusInit(SemSsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
edge.phiInput(phi, inp) and
ssaModulus(inp, edge, b, val, mod)
)
}
/**
* Holds if all inputs to `phi` numbered `1` to `rix` are equal to `b + val` modulo `mod`.
*/
pragma[nomagic]
private predicate phiModulusRankStep(
SemSsaPhiNode phi, Bounds::SemBound b, int val, int mod, int rix
) {
/*
* Recursive case. If `inp` = `b + v2` mod `m2`, we combine that with the preceding potential
* congruence class `b + v1` mod `m1`. The result will be the congruence class of `v1` modulo
* the greatest common denominator of `m1`, `m2`, and `v1 - v2`.
* base case. If any phi input is equal to `b + val` modulo `mod`, that's a potential congruence
* class for the phi node.
*/
exists(int v2, int m2 |
rankedPhiInput(pragma[only_bind_out](phi), inp, edge, rix) and
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
ssaModulus(inp, edge, b, v2, m2) and
mod = m1.gcd(m2).gcd(v1 - v2)
rix = 0 and
phiModulusInit(phi, b, val, mod)
or
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int v1, int m1 |
mod != 1 and
val = remainder(v1, mod)
|
/*
* Recursive case. If `inp` = `b + v2` mod `m2`, we combine that with the preceding potential
* congruence class `b + v1` mod `m1`. The result will be the congruence class of `v1` modulo
* the greatest common denominator of `m1`, `m2`, and `v1 - v2`.
*/
exists(int v2, int m2 |
rankedPhiInput(pragma[only_bind_out](phi), inp, edge, rix) and
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
ssaModulus(inp, edge, b, v2, m2) and
mod = m1.gcd(m2).gcd(v1 - v2)
)
or
/*
* Recursive case. If `inp` = `phi` mod `m2`, we combine that with the preceding potential
* congruence class `b + v1` mod `m1`. The result will be a congruence class modulo the greatest
* common denominator of `m1` and `m2`.
*/
exists(int m2 |
rankedPhiInput(phi, inp, edge, rix) and
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
phiSelfModulus(phi, inp, edge, m2) and
mod = m1.gcd(m2)
)
)
or
/*
* Recursive case. If `inp` = `phi` mod `m2`, we combine that with the preceding potential
* congruence class `b + v1` mod `m1`. The result will be a congruence class modulo the greatest
* common denominator of `m1` and `m2`.
*/
}
exists(int m2 |
rankedPhiInput(phi, inp, edge, rix) and
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
phiSelfModulus(phi, inp, edge, m2) and
mod = m1.gcd(m2)
/**
* Holds if `phi` is equal to `b + val` modulo `mod`.
*/
private predicate phiModulus(SemSsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
exists(int r |
maxPhiInputRank(phi, r) and
phiModulusRankStep(phi, b, val, mod, r)
)
)
}
}
/**
* Holds if `phi` is equal to `b + val` modulo `mod`.
*/
private predicate phiModulus(SemSsaPhiNode phi, SemBound b, int val, int mod) {
exists(int r |
maxPhiInputRank(phi, r) and
phiModulusRankStep(phi, b, val, mod, r)
)
}
/**
* Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
*/
private predicate ssaModulus(SemSsaVariable v, SemSsaReadPosition pos, SemBound b, int val, int mod) {
phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
or
b.(SemSsaBound).getAVariable() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
or
exists(SemExpr e, int val0, int delta |
semExprModulus(e, b, val0, mod) and
valueFlowStepSsa(v, pos, e, delta) and
val = remainder(val0 + delta, mod)
)
or
moduloGuardedRead(v, pos, val, mod) and b instanceof SemZeroBound
}
/**
* Holds if `e` is equal to `b + val` modulo `mod`.
*
* There are two cases for the modulus:
* - `mod = 0`: The equality `e = b + val` is an ordinary equality.
* - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
*/
cached
predicate semExprModulus(SemExpr e, SemBound b, int val, int mod) {
not ignoreExprModulus(e) and
(
e = b.getExpr(val) and mod = 0
/**
* Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
*/
private predicate ssaModulus(
SemSsaVariable v, SemSsaReadPosition pos, Bounds::SemBound b, int val, int mod
) {
phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
or
evenlyDivisibleExpr(e, mod) and
val = 0 and
b instanceof SemZeroBound
b.(Bounds::SemSsaBound).getAVariable() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
or
exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
ssaModulus(v, bb, b, val, mod) and
e = v.getAUse() and
bb.getAnExpr() = e
)
or
exists(SemExpr mid, int val0, int delta |
semExprModulus(mid, b, val0, mod) and
semValueFlowStep(e, mid, delta) and
exists(SemExpr e, int val0, int delta |
semExprModulus(e, b, val0, mod) and
valueFlowStepSsa(v, pos, e, delta) and
val = remainder(val0 + delta, mod)
)
or
exists(SemConditionalExpr cond, int v1, int v2, int m1, int m2 |
cond = e and
condExprBranchModulus(cond, true, b, v1, m1) and
condExprBranchModulus(cond, false, b, v2, m2) and
mod = m1.gcd(m2).gcd(v1 - v2) and
mod != 1 and
val = remainder(v1, mod)
)
or
exists(SemBound b1, SemBound b2, int v1, int v2, int m1, int m2 |
addModulus(e, true, b1, v1, m1) and
addModulus(e, false, b2, v2, m2) and
mod = m1.gcd(m2) and
mod != 1 and
val = remainder(v1 + v2, mod)
|
b = b1 and b2 instanceof SemZeroBound
moduloGuardedRead(v, pos, val, mod) and b instanceof Bounds::SemZeroBound
}
/**
* Holds if `e` is equal to `b + val` modulo `mod`.
*
* There are two cases for the modulus:
* - `mod = 0`: The equality `e = b + val` is an ordinary equality.
* - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
*/
cached
predicate semExprModulus(SemExpr e, Bounds::SemBound b, int val, int mod) {
not ignoreExprModulus(e) and
(
e = b.getExpr(D::fromInt(val)) and mod = 0
or
b = b2 and b1 instanceof SemZeroBound
evenlyDivisibleExpr(e, mod) and
val = 0 and
b instanceof Bounds::SemZeroBound
or
exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
ssaModulus(v, bb, b, val, mod) and
e = v.getAUse() and
bb.getAnExpr() = e
)
or
exists(SemExpr mid, int val0, int delta |
semExprModulus(mid, b, val0, mod) and
U::semValueFlowStep(e, mid, D::fromInt(delta)) and
val = remainder(val0 + delta, mod)
)
or
exists(SemConditionalExpr cond, int v1, int v2, int m1, int m2 |
cond = e and
condExprBranchModulus(cond, true, b, v1, m1) and
condExprBranchModulus(cond, false, b, v2, m2) and
mod = m1.gcd(m2).gcd(v1 - v2) and
mod != 1 and
val = remainder(v1, mod)
)
or
exists(Bounds::SemBound b1, Bounds::SemBound b2, int v1, int v2, int m1, int m2 |
addModulus(e, true, b1, v1, m1) and
addModulus(e, false, b2, v2, m2) and
mod = m1.gcd(m2) and
mod != 1 and
val = remainder(v1 + v2, mod)
|
b = b1 and b2 instanceof Bounds::SemZeroBound
or
b = b2 and b1 instanceof Bounds::SemZeroBound
)
or
exists(int v1, int v2, int m1, int m2 |
subModulus(e, true, b, v1, m1) and
subModulus(e, false, any(Bounds::SemZeroBound zb), v2, m2) and
mod = m1.gcd(m2) and
mod != 1 and
val = remainder(v1 - v2, mod)
)
)
or
exists(int v1, int v2, int m1, int m2 |
subModulus(e, true, b, v1, m1) and
subModulus(e, false, any(SemZeroBound zb), v2, m2) and
mod = m1.gcd(m2) and
mod != 1 and
val = remainder(v1 - v2, mod)
}
private predicate condExprBranchModulus(
SemConditionalExpr cond, boolean branch, Bounds::SemBound b, int val, int mod
) {
semExprModulus(cond.getBranchExpr(branch), b, val, mod)
}
private predicate addModulus(SemExpr add, boolean isLeft, Bounds::SemBound b, int val, int mod) {
exists(SemExpr larg, SemExpr rarg | nonConstAddition(add, larg, rarg) |
semExprModulus(larg, b, val, mod) and isLeft = true
or
semExprModulus(rarg, b, val, mod) and isLeft = false
)
)
}
}
private predicate condExprBranchModulus(
SemConditionalExpr cond, boolean branch, SemBound b, int val, int mod
) {
semExprModulus(cond.getBranchExpr(branch), b, val, mod)
}
private predicate addModulus(SemExpr add, boolean isLeft, SemBound b, int val, int mod) {
exists(SemExpr larg, SemExpr rarg | nonConstAddition(add, larg, rarg) |
semExprModulus(larg, b, val, mod) and isLeft = true
or
semExprModulus(rarg, b, val, mod) and isLeft = false
)
}
private predicate subModulus(SemExpr sub, boolean isLeft, SemBound b, int val, int mod) {
exists(SemExpr larg, SemExpr rarg | nonConstSubtraction(sub, larg, rarg) |
semExprModulus(larg, b, val, mod) and isLeft = true
or
semExprModulus(rarg, b, val, mod) and isLeft = false
)
}
/**
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
* in an arbitrary 1-based numbering of the input edges to `phi`.
*/
private predicate rankedPhiInput(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
) {
edge.phiInput(phi, inp) and
edge =
rank[r](SemSsaReadPositionPhiInputEdge e |
e.phiInput(phi, _)
|
e order by e.getOrigBlock().getUniqueId()
private predicate subModulus(SemExpr sub, boolean isLeft, Bounds::SemBound b, int val, int mod) {
exists(SemExpr larg, SemExpr rarg | nonConstSubtraction(sub, larg, rarg) |
semExprModulus(larg, b, val, mod) and isLeft = true
or
semExprModulus(rarg, b, val, mod) and isLeft = false
)
}
/**
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
* in an arbitrary 1-based numbering of the input edges to `phi`.
*/
private predicate rankedPhiInput(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
) {
edge.phiInput(phi, inp) and
edge =
rank[r](SemSsaReadPositionPhiInputEdge e |
e.phiInput(phi, _)
|
e order by e.getOrigBlock().getUniqueId()
)
}
}

838
cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll
View File

@@ -1,830 +1,24 @@
/**
* Provides classes and predicates for range analysis.
*
* An inferred bound can either be a specific integer, the abstract value of an
* SSA variable, or the abstract value of an interesting expression. The latter
* category includes array lengths that are not SSA variables.
*
* If an inferred bound relies directly on a condition, then this condition is
* reported as the reason for the bound.
*/
/*
* This library tackles range analysis as a flow problem. Consider e.g.:
* ```
* len = arr.length;
* if (x < len) { ... y = x-1; ... y ... }
* ```
* In this case we would like to infer `y <= arr.length - 2`, and this is
* accomplished by tracking the bound through a sequence of steps:
* ```
* arr.length --> len = .. --> x < len --> x-1 --> y = .. --> y
* ```
*
* In its simplest form the step relation `E1 --> E2` relates two expressions
* such that `E1 <= B` implies `E2 <= B` for any `B` (with a second separate
* step relation handling lower bounds). Examples of such steps include
* assignments `E2 = E1` and conditions `x <= E1` where `E2` is a use of `x`
* guarded by the condition.
*
* In order to handle subtractions and additions with constants, and strict
* comparisons, the step relation is augmented with an integer delta. With this
* generalization `E1 --(delta)--> E2` relates two expressions and an integer
* such that `E1 <= B` implies `E2 <= B + delta` for any `B`. This corresponds
* to the predicate `boundFlowStep`.
*
* The complete range analysis is then implemented as the transitive closure of
* the step relation summing the deltas along the way. If `E1` transitively
* steps to `E2`, `delta` is the sum of deltas along the path, and `B` is an
* interesting bound equal to the value of `E1` then `E2 <= B + delta`. This
* corresponds to the predicate `bounded`.
*
* Phi nodes need a little bit of extra handling. Consider `x0 = phi(x1, x2)`.
* There are essentially two cases:
* - If `x1 <= B + d1` and `x2 <= B + d2` then `x0 <= B + max(d1,d2)`.
* - If `x1 <= B + d1` and `x2 <= x0 + d2` with `d2 <= 0` then `x0 <= B + d1`.
* The first case is for whenever a bound can be proven without taking looping
* into account. The second case is relevant when `x2` comes from a back-edge
* where we can prove that the variable has been non-increasing through the
* loop-iteration as this means that any upper bound that holds prior to the
* loop also holds for the variable during the loop.
* This generalizes to a phi node with `n` inputs, so if
* `x0 = phi(x1, ..., xn)` and `xi <= B + delta` for one of the inputs, then we
* also have `x0 <= B + delta` if we can prove either:
* - `xj <= B + d` with `d <= delta` or
* - `xj <= x0 + d` with `d <= 0`
* for each input `xj`.
*
* As all inferred bounds can be related directly to a path in the source code
* the only source of non-termination is if successive redundant (and thereby
* increasingly worse) bounds are calculated along a loop in the source code.
* We prevent this by weakening the bound to a small finite set of bounds when
* a path follows a second back-edge (we postpone weakening till the second
* back-edge as a precise bound might require traversing a loop once).
*/
private import RangeAnalysisSpecific as Specific
private import RangeAnalysisStage
private import RangeAnalysisSpecific
private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
private import RangeUtils
private import SignAnalysisCommon
private import ModulusAnalysis
private import experimental.semmle.code.cpp.semantic.Semantic
private import ConstantAnalysis
private import experimental.semmle.code.cpp.semantic.SemanticBound as SemanticBound
cached
private module RangeAnalysisCache {
cached
module RangeAnalysisPublic {
/**
* Holds if `b + delta` is a valid bound for `e`.
* - `upper = true` : `e <= b + delta`
* - `upper = false` : `e >= b + delta`
*
* The reason for the bound is given by `reason` and may be either a condition
* or `NoReason` if the bound was proven directly without the use of a bounding
* condition.
*/
cached
predicate semBounded(SemExpr e, SemBound b, int delta, boolean upper, SemReason reason) {
bounded(e, b, delta, upper, _, _, reason) and
bestBound(e, b, delta, upper)
}
module Bounds implements BoundSig<FloatDelta> {
class SemBound instanceof SemanticBound::SemBound {
string toString() { result = super.toString() }
SemExpr getExpr(float delta) { result = super.getExpr(delta) }
}
/**
* Holds if `guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)`.
*/
cached
predicate possibleReason(SemGuard guard) {
guard = boundFlowCond(_, _, _, _, _) or guard = semEqFlowCond(_, _, _, _, _)
class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
}
}
private import RangeAnalysisCache
import RangeAnalysisPublic
private module CppRangeAnalysis =
RangeStage<FloatDelta, Bounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
/**
* Holds if `b + delta` is a valid bound for `e` and this is the best such delta.
* - `upper = true` : `e <= b + delta`
* - `upper = false` : `e >= b + delta`
*/
private predicate bestBound(SemExpr e, SemBound b, int delta, boolean upper) {
delta = min(int d | bounded(e, b, d, upper, _, _, _)) and upper = true
or
delta = max(int d | bounded(e, b, d, upper, _, _, _)) and upper = false
}
/**
* Holds if `comp` corresponds to:
* - `upper = true` : `v <= e + delta` or `v < e + delta`
* - `upper = false` : `v >= e + delta` or `v > e + delta`
*/
private predicate boundCondition(
SemRelationalExpr comp, SemSsaVariable v, SemExpr e, int delta, boolean upper
) {
comp.getLesserOperand() = semSsaRead(v, delta) and e = comp.getGreaterOperand() and upper = true
or
comp.getGreaterOperand() = semSsaRead(v, delta) and e = comp.getLesserOperand() and upper = false
or
exists(SemSubExpr sub, SemConstantIntegerExpr c, int d |
// (v - d) - e < c
comp.getLesserOperand() = sub and
comp.getGreaterOperand() = c and
sub.getLeftOperand() = semSsaRead(v, d) and
sub.getRightOperand() = e and
upper = true and
delta = d + c.getIntValue()
or
// (v - d) - e > c
comp.getGreaterOperand() = sub and
comp.getLesserOperand() = c and
sub.getLeftOperand() = semSsaRead(v, d) and
sub.getRightOperand() = e and
upper = false and
delta = d + c.getIntValue()
or
// e - (v - d) < c
comp.getLesserOperand() = sub and
comp.getGreaterOperand() = c and
sub.getLeftOperand() = e and
sub.getRightOperand() = semSsaRead(v, d) and
upper = false and
delta = d - c.getIntValue()
or
// e - (v - d) > c
comp.getGreaterOperand() = sub and
comp.getLesserOperand() = c and
sub.getLeftOperand() = e and
sub.getRightOperand() = semSsaRead(v, d) and
upper = true and
delta = d - c.getIntValue()
)
}
/**
* Holds if `comp` is a comparison between `x` and `y` for which `y - x` has a
* fixed value modulo some `mod > 1`, such that the comparison can be
* strengthened by `strengthen` when evaluating to `testIsTrue`.
*/
private predicate modulusComparison(SemRelationalExpr comp, boolean testIsTrue, int strengthen) {
exists(
SemBound b, int v1, int v2, int mod1, int mod2, int mod, boolean resultIsStrict, int d, int k
|
// If `x <= y` and `x =(mod) b + v1` and `y =(mod) b + v2` then
// `0 <= y - x =(mod) v2 - v1`. By choosing `k =(mod) v2 - v1` with
// `0 <= k < mod` we get `k <= y - x`. If the resulting comparison is
// strict then the strengthening amount is instead `k - 1` modulo `mod`:
// `x < y` means `0 <= y - x - 1 =(mod) k - 1` so `k - 1 <= y - x - 1` and
// thus `k - 1 < y - x` with `0 <= k - 1 < mod`.
semExprModulus(comp.getLesserOperand(), b, v1, mod1) and
semExprModulus(comp.getGreaterOperand(), b, v2, mod2) and
mod = mod1.gcd(mod2) and
mod != 1 and
(testIsTrue = true or testIsTrue = false) and
(
if comp.isStrict()
then resultIsStrict = testIsTrue
else resultIsStrict = testIsTrue.booleanNot()
) and
(
resultIsStrict = true and d = 1
or
resultIsStrict = false and d = 0
) and
(
testIsTrue = true and k = v2 - v1
or
testIsTrue = false and k = v1 - v2
) and
strengthen = (((k - d) % mod) + mod) % mod
)
}
/**
* Gets a condition that tests whether `v` is bounded by `e + delta`.
*
* If the condition evaluates to `testIsTrue`:
* - `upper = true` : `v <= e + delta`
* - `upper = false` : `v >= e + delta`
*/
private SemGuard boundFlowCond(
SemSsaVariable v, SemExpr e, int delta, boolean upper, boolean testIsTrue
) {
exists(
SemRelationalExpr comp, int d1, int d2, int d3, int strengthen, boolean compIsUpper,
boolean resultIsStrict
|
comp = result.asExpr() and
boundCondition(comp, v, e, d1, compIsUpper) and
(testIsTrue = true or testIsTrue = false) and
upper = compIsUpper.booleanXor(testIsTrue.booleanNot()) and
(
if comp.isStrict()
then resultIsStrict = testIsTrue
else resultIsStrict = testIsTrue.booleanNot()
) and
(
if
getTrackedTypeForSsaVariable(v) instanceof SemIntegerType or
getTrackedTypeForSsaVariable(v) instanceof SemAddressType
then
upper = true and strengthen = -1
or
upper = false and strengthen = 1
else strengthen = 0
) and
(
exists(int k | modulusComparison(comp, testIsTrue, k) and d2 = strengthen * k)
or
not modulusComparison(comp, testIsTrue, _) and d2 = 0
) and
// A strict inequality `x < y` can be strengthened to `x <= y - 1`.
(
resultIsStrict = true and d3 = strengthen
or
resultIsStrict = false and d3 = 0
) and
delta = d1 + d2 + d3
)
or
exists(boolean testIsTrue0 |
semImplies_v2(result, testIsTrue, boundFlowCond(v, e, delta, upper, testIsTrue0), testIsTrue0)
)
or
result = semEqFlowCond(v, e, delta, true, testIsTrue) and
(upper = true or upper = false)
or
// guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
// exists a guard `guardEq` such that `v = v2 - d1 + d2`.
exists(SemSsaVariable v2, SemGuard guardEq, boolean eqIsTrue, int d1, int d2 |
guardEq = semEqFlowCond(v, semSsaRead(v2, d1), d2, true, eqIsTrue) and
result = boundFlowCond(v2, e, delta + d1 - d2, upper, testIsTrue) and
// guardEq needs to control guard
guardEq.directlyControls(result.getBasicBlock(), eqIsTrue)
)
}
private newtype TSemReason =
TSemNoReason() or
TSemCondReason(SemGuard guard) { possibleReason(guard) }
/**
* A reason for an inferred bound. This can either be `CondReason` if the bound
* is due to a specific condition, or `NoReason` if the bound is inferred
* without going through a bounding condition.
*/
abstract class SemReason extends TSemReason {
/** Gets a textual representation of this reason. */
abstract string toString();
}
/**
* A reason for an inferred bound that indicates that the bound is inferred
* without going through a bounding condition.
*/
class SemNoReason extends SemReason, TSemNoReason {
override string toString() { result = "NoReason" }
}
/** A reason for an inferred bound pointing to a condition. */
class SemCondReason extends SemReason, TSemCondReason {
/** Gets the condition that is the reason for the bound. */
SemGuard getCond() { this = TSemCondReason(result) }
override string toString() { result = getCond().toString() }
}
/**
* Holds if `e + delta` is a valid bound for `v` at `pos`.
* - `upper = true` : `v <= e + delta`
* - `upper = false` : `v >= e + delta`
*/
private predicate boundFlowStepSsa(
SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta, boolean upper, SemReason reason
) {
semSsaUpdateStep(v, e, delta) and
pos.hasReadOfVar(v) and
(upper = true or upper = false) and
reason = TSemNoReason()
or
exists(SemGuard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
reason = TSemCondReason(guard)
)
}
/** Holds if `v != e + delta` at `pos` and `v` is of integral type. */
private predicate unequalFlowStepIntegralSsa(
SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta, SemReason reason
) {
getTrackedTypeForSsaVariable(v) instanceof SemIntegerType and
exists(SemGuard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = semEqFlowCond(v, e, delta, false, testIsTrue) and
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
reason = TSemCondReason(guard)
)
}
/**
* An expression that does conversion, boxing, or unboxing
*/
private class ConvertOrBoxExpr extends SemUnaryExpr {
ConvertOrBoxExpr() {
this instanceof SemConvertExpr
or
this instanceof SemBoxExpr
or
this instanceof SemUnboxExpr
}
}
/**
* A cast that can be ignored for the purpose of range analysis.
*/
private class SafeCastExpr extends ConvertOrBoxExpr {
SafeCastExpr() {
conversionCannotOverflow(getTrackedType(pragma[only_bind_into](getOperand())),
getTrackedType(this))
}
}
/**
* Holds if `typ` is a small integral type with the given lower and upper bounds.
*/
private predicate typeBound(SemIntegerType typ, int lowerbound, int upperbound) {
exists(int bitSize | bitSize = typ.getByteSize() * 8 |
bitSize < 32 and
(
if typ.isSigned()
then (
upperbound = 1.bitShiftLeft(bitSize - 1) - 1 and
lowerbound = -upperbound - 1
) else (
lowerbound = 0 and
upperbound = 1.bitShiftLeft(bitSize) - 1
)
)
)
}
/**
* A cast to a small integral type that may overflow or underflow.
*/
private class NarrowingCastExpr extends ConvertOrBoxExpr {
NarrowingCastExpr() {
not this instanceof SafeCastExpr and
typeBound(getTrackedType(this), _, _)
}
/** Gets the lower bound of the resulting type. */
int getLowerBound() { typeBound(getTrackedType(this), result, _) }
/** Gets the upper bound of the resulting type. */
int getUpperBound() { typeBound(getTrackedType(this), _, result) }
}
/** Holds if `e >= 1` as determined by sign analysis. */
private predicate strictlyPositiveIntegralExpr(SemExpr e) {
semStrictlyPositive(e) and getTrackedType(e) instanceof SemIntegerType
}
/** Holds if `e <= -1` as determined by sign analysis. */
private predicate strictlyNegativeIntegralExpr(SemExpr e) {
semStrictlyNegative(e) and getTrackedType(e) instanceof SemIntegerType
}
/**
* Holds if `e1 + delta` is a valid bound for `e2`.
* - `upper = true` : `e2 <= e1 + delta`
* - `upper = false` : `e2 >= e1 + delta`
*/
private predicate boundFlowStep(SemExpr e2, SemExpr e1, int delta, boolean upper) {
semValueFlowStep(e2, e1, delta) and
(upper = true or upper = false)
or
e2.(SafeCastExpr).getOperand() = e1 and
delta = 0 and
(upper = true or upper = false)
or
exists(SemExpr x | e2.(SemAddExpr).hasOperands(e1, x) |
// `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
not x instanceof SemConstantIntegerExpr and
not e1 instanceof SemConstantIntegerExpr and
if strictlyPositiveIntegralExpr(x)
then upper = false and delta = 1
else
if semPositive(x)
then upper = false and delta = 0
else
if strictlyNegativeIntegralExpr(x)
then upper = true and delta = -1
else
if semNegative(x)
then upper = true and delta = 0
else none()
)
or
exists(SemExpr x, SemSubExpr sub |
e2 = sub and
sub.getLeftOperand() = e1 and
sub.getRightOperand() = x
|
// `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
not x instanceof SemConstantIntegerExpr and
if strictlyPositiveIntegralExpr(x)
then upper = true and delta = -1
else
if semPositive(x)
then upper = true and delta = 0
else
if strictlyNegativeIntegralExpr(x)
then upper = false and delta = 1
else
if semNegative(x)
then upper = false and delta = 0
else none()
)
or
e2.(SemRemExpr).getRightOperand() = e1 and
semPositive(e1) and
delta = -1 and
upper = true
or
e2.(SemRemExpr).getLeftOperand() = e1 and semPositive(e1) and delta = 0 and upper = true
or
e2.(SemBitAndExpr).getAnOperand() = e1 and
semPositive(e1) and
delta = 0 and
upper = true
or
e2.(SemBitOrExpr).getAnOperand() = e1 and
semPositive(e2) and
delta = 0 and
upper = false
or
Specific::hasBound(e2, e1, delta, upper)
}
/** Holds if `e2 = e1 * factor` and `factor > 0`. */
private predicate boundFlowStepMul(SemExpr e2, SemExpr e1, int factor) {
exists(SemConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
e2.(SemMulExpr).hasOperands(e1, c) and factor = k
or
exists(SemShiftLeftExpr e |
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
)
)
}
/**
* Holds if `e2 = e1 / factor` and `factor > 0`.
*
* This conflates division, right shift, and unsigned right shift and is
* therefore only valid for non-negative numbers.
*/
private predicate boundFlowStepDiv(SemExpr e2, SemExpr e1, int factor) {
exists(SemConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
exists(SemDivExpr e |
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = k
)
or
exists(SemShiftRightExpr e |
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
)
or
exists(SemShiftRightUnsignedExpr e |
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
)
)
}
/**
* Holds if `b + delta` is a valid bound for `v` at `pos`.
* - `upper = true` : `v <= b + delta`
* - `upper = false` : `v >= b + delta`
*/
private predicate boundedSsa(
SemSsaVariable v, SemSsaReadPosition pos, SemBound b, int delta, boolean upper,
boolean fromBackEdge, int origdelta, SemReason reason
) {
exists(SemExpr mid, int d1, int d2, SemReason r1, SemReason r2 |
boundFlowStepSsa(v, pos, mid, d1, upper, r1) and
bounded(mid, b, d2, upper, fromBackEdge, origdelta, r2) and
// upper = true: v <= mid + d1 <= b + d1 + d2 = b + delta
// upper = false: v >= mid + d1 >= b + d1 + d2 = b + delta
delta = d1 + d2 and
(if r1 instanceof SemNoReason then reason = r2 else reason = r1)
)
or
exists(int d, SemReason r1, SemReason r2 |
boundedSsa(v, pos, b, d, upper, fromBackEdge, origdelta, r2) or
boundedPhi(v, b, d, upper, fromBackEdge, origdelta, r2)
|
unequalIntegralSsa(v, pos, b, d, r1) and
(
upper = true and delta = d - 1
or
upper = false and delta = d + 1
) and
(
reason = r1
or
reason = r2 and not r2 instanceof SemNoReason
)
)
}
/**
* Holds if `v != b + delta` at `pos` and `v` is of integral type.
*/
private predicate unequalIntegralSsa(
SemSsaVariable v, SemSsaReadPosition pos, SemBound b, int delta, SemReason reason
) {
exists(SemExpr e, int d1, int d2 |
unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
boundedUpper(e, b, d1) and
boundedLower(e, b, d2) and
delta = d2 + d1
)
}
/**
* Holds if `b + delta` is an upper bound for `e`.
*
* This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
*/
pragma[nomagic]
private predicate boundedUpper(SemExpr e, SemBound b, int delta) {
bounded(e, b, delta, true, _, _, _)
}
/**
* Holds if `b + delta` is a lower bound for `e`.
*
* This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
*/
pragma[nomagic]
private predicate boundedLower(SemExpr e, SemBound b, int delta) {
bounded(e, b, delta, false, _, _, _)
}
/** Weakens a delta to lie in the range `[-1..1]`. */
bindingset[delta, upper]
private int weakenDelta(boolean upper, int delta) {
delta in [-1 .. 1] and result = delta
or
upper = true and result = -1 and delta < -1
or
upper = false and result = 1 and delta > 1
}
/**
* Holds if `b + delta` is a valid bound for `inp` when used as an input to
* `phi` along `edge`.
* - `upper = true` : `inp <= b + delta`
* - `upper = false` : `inp >= b + delta`
*/
private predicate boundedPhiInp(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, SemBound b, int delta,
boolean upper, boolean fromBackEdge, int origdelta, SemReason reason
) {
edge.phiInput(phi, inp) and
exists(int d, boolean fromBackEdge0 |
boundedSsa(inp, edge, b, d, upper, fromBackEdge0, origdelta, reason)
or
boundedPhi(inp, b, d, upper, fromBackEdge0, origdelta, reason)
or
b.(SemSsaBound).getAVariable() = inp and
d = 0 and
(upper = true or upper = false) and
fromBackEdge0 = false and
origdelta = 0 and
reason = TSemNoReason()
|
if semBackEdge(phi, inp, edge)
then
fromBackEdge = true and
(
fromBackEdge0 = true and delta = weakenDelta(upper, d - origdelta) + origdelta
or
fromBackEdge0 = false and delta = d
)
else (
delta = d and fromBackEdge = fromBackEdge0
)
)
}
/**
* Holds if `b + delta` is a valid bound for `inp` when used as an input to
* `phi` along `edge`.
* - `upper = true` : `inp <= b + delta`
* - `upper = false` : `inp >= b + delta`
*
* Equivalent to `boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)`.
*/
pragma[noinline]
private predicate boundedPhiInp1(
SemSsaPhiNode phi, SemBound b, boolean upper, SemSsaVariable inp,
SemSsaReadPositionPhiInputEdge edge, int delta
) {
boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)
}
/**
* Holds if `phi` is a valid bound for `inp` when used as an input to `phi`
* along `edge`.
* - `upper = true` : `inp <= phi`
* - `upper = false` : `inp >= phi`
*/
private predicate selfBoundedPhiInp(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, boolean upper
) {
exists(int d, SemSsaBound phibound |
phibound.getAVariable() = phi and
boundedPhiInp(phi, inp, edge, phibound, d, upper, _, _, _) and
(
upper = true and d <= 0
or
upper = false and d >= 0
)
)
}
/**
* Holds if `b + delta` is a valid bound for some input, `inp`, to `phi`, and
* thus a candidate bound for `phi`.
* - `upper = true` : `inp <= b + delta`
* - `upper = false` : `inp >= b + delta`
*/
pragma[noinline]
private predicate boundedPhiCand(
SemSsaPhiNode phi, boolean upper, SemBound b, int delta, boolean fromBackEdge, int origdelta,
SemReason reason
) {
boundedPhiInp(phi, _, _, b, delta, upper, fromBackEdge, origdelta, reason)
}
/**
* Holds if the candidate bound `b + delta` for `phi` is valid for the phi input
* `inp` along `edge`.
*/
private predicate boundedPhiCandValidForEdge(
SemSsaPhiNode phi, SemBound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
SemReason reason, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge
) {
boundedPhiCand(phi, upper, b, delta, fromBackEdge, origdelta, reason) and
(
exists(int d | boundedPhiInp1(phi, b, upper, inp, edge, d) | upper = true and d <= delta)
or
exists(int d | boundedPhiInp1(phi, b, upper, inp, edge, d) | upper = false and d >= delta)
or
selfBoundedPhiInp(phi, inp, edge, upper)
)
}
/**
* Holds if `b + delta` is a valid bound for `phi`.
* - `upper = true` : `phi <= b + delta`
* - `upper = false` : `phi >= b + delta`
*/
private predicate boundedPhi(
SemSsaPhiNode phi, SemBound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
SemReason reason
) {
forex(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) |
boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
)
}
/**
* Holds if `e` has an upper (for `upper = true`) or lower
* (for `upper = false`) bound of `b`.
*/
private predicate baseBound(SemExpr e, int b, boolean upper) {
Specific::hasConstantBound(e, b, upper)
or
upper = false and
b = 0 and
semPositive(e.(SemBitAndExpr).getAnOperand()) and
// REVIEW: We let the language opt out here to preserve original results.
not Specific::ignoreZeroLowerBound(e)
}
/**
* Holds if the value being cast has an upper (for `upper = true`) or lower
* (for `upper = false`) bound within the bounds of the resulting type.
* For `upper = true` this means that the cast will not overflow and for
* `upper = false` this means that the cast will not underflow.
*/
private predicate safeNarrowingCast(NarrowingCastExpr cast, boolean upper) {
exists(int bound | bounded(cast.getOperand(), any(SemZeroBound zb), bound, upper, _, _, _) |
upper = true and bound <= cast.getUpperBound()
or
upper = false and bound >= cast.getLowerBound()
)
}
pragma[noinline]
private predicate boundedCastExpr(
NarrowingCastExpr cast, SemBound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
SemReason reason
) {
bounded(cast.getOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
}
/**
* Holds if `b + delta` is a valid bound for `e`.
* - `upper = true` : `e <= b + delta`
* - `upper = false` : `e >= b + delta`
*/
private predicate bounded(
SemExpr e, SemBound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
SemReason reason
) {
not Specific::ignoreExprBound(e) and
(
e = b.getExpr(delta) and
(upper = true or upper = false) and
fromBackEdge = false and
origdelta = delta and
reason = TSemNoReason()
or
baseBound(e, delta, upper) and
b instanceof SemZeroBound and
fromBackEdge = false and
origdelta = delta and
reason = TSemNoReason()
or
exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
boundedSsa(v, bb, b, delta, upper, fromBackEdge, origdelta, reason) and
e = v.getAUse() and
bb.getBlock() = e.getBasicBlock()
)
or
exists(SemExpr mid, int d1, int d2 |
boundFlowStep(e, mid, d1, upper) and
// Constants have easy, base-case bounds, so let's not infer any recursive bounds.
not e instanceof SemConstantIntegerExpr and
bounded(mid, b, d2, upper, fromBackEdge, origdelta, reason) and
// upper = true: e <= mid + d1 <= b + d1 + d2 = b + delta
// upper = false: e >= mid + d1 >= b + d1 + d2 = b + delta
delta = d1 + d2
)
or
exists(SemSsaPhiNode phi |
boundedPhi(phi, b, delta, upper, fromBackEdge, origdelta, reason) and
e = phi.getAUse()
)
or
exists(SemExpr mid, int factor, int d |
boundFlowStepMul(e, mid, factor) and
not e instanceof SemConstantIntegerExpr and
bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
b instanceof SemZeroBound and
delta = d * factor
)
or
exists(SemExpr mid, int factor, int d |
boundFlowStepDiv(e, mid, factor) and
not e instanceof SemConstantIntegerExpr and
bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
b instanceof SemZeroBound and
d >= 0 and
delta = d / factor
)
or
exists(NarrowingCastExpr cast |
cast = e and
safeNarrowingCast(cast, upper.booleanNot()) and
boundedCastExpr(cast, b, delta, upper, fromBackEdge, origdelta, reason)
)
or
exists(
SemConditionalExpr cond, int d1, int d2, boolean fbe1, boolean fbe2, int od1, int od2,
SemReason r1, SemReason r2
|
cond = e and
boundedConditionalExpr(cond, b, upper, true, d1, fbe1, od1, r1) and
boundedConditionalExpr(cond, b, upper, false, d2, fbe2, od2, r2) and
(
delta = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1
or
delta = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2
)
|
upper = true and delta = d1.maximum(d2)
or
upper = false and delta = d1.minimum(d2)
)
)
}
private predicate boundedConditionalExpr(
SemConditionalExpr cond, SemBound b, boolean upper, boolean branch, int delta,
boolean fromBackEdge, int origdelta, SemReason reason
) {
bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason)
}
import CppRangeAnalysis

148
cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisSpecific.qll
View File

@@ -3,86 +3,90 @@
*/
private import experimental.semmle.code.cpp.semantic.Semantic
private import RangeAnalysisStage
private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*
* This predicate is to keep the results identical to the original Java implementation. It should be
* removed once we have the new implementation matching the old results exactly.
*/
predicate ignoreSsaReadCopy(SemExpr e) { none() }
module CppLangImpl implements LangSig<FloatDelta> {
/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*
* This predicate is to keep the results identical to the original Java implementation. It should be
* removed once we have the new implementation matching the old results exactly.
*/
predicate ignoreSsaReadCopy(SemExpr e) { none() }
/**
* Ignore the bound on this expression.
*
* This predicate is to keep the results identical to the original Java implementation. It should be
* removed once we have the new implementation matching the old results exactly.
*/
predicate ignoreExprBound(SemExpr e) { none() }
/**
* Ignore the bound on this expression.
*
* This predicate is to keep the results identical to the original Java implementation. It should be
* removed once we have the new implementation matching the old results exactly.
*/
predicate ignoreExprBound(SemExpr e) { none() }
/**
* Ignore any inferred zero lower bound on this expression.
*
* This predicate is to keep the results identical to the original Java implementation. It should be
* removed once we have the new implementation matching the old results exactly.
*/
predicate ignoreZeroLowerBound(SemExpr e) { none() }
/**
* Ignore any inferred zero lower bound on this expression.
*
* This predicate is to keep the results identical to the original Java implementation. It should be
* removed once we have the new implementation matching the old results exactly.
*/
predicate ignoreZeroLowerBound(SemExpr e) { none() }
/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*
* This predicate is to keep the results identical to the original Java implementation. It should be
* removed once we have the new implementation matching the old results exactly.
*/
predicate ignoreSsaReadArithmeticExpr(SemExpr e) { none() }
/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*
* This predicate is to keep the results identical to the original Java implementation. It should be
* removed once we have the new implementation matching the old results exactly.
*/
predicate ignoreSsaReadArithmeticExpr(SemExpr e) { none() }
/**
* Holds if the specified variable should be excluded from the result of `ssaRead()`.
*
* This predicate is to keep the results identical to the original Java implementation. It should be
* removed once we have the new implementation matching the old results exactly.
*/
predicate ignoreSsaReadAssignment(SemSsaVariable v) { none() }
/**
* Holds if the specified variable should be excluded from the result of `ssaRead()`.
*
* This predicate is to keep the results identical to the original Java implementation. It should be
* removed once we have the new implementation matching the old results exactly.
*/
predicate ignoreSsaReadAssignment(SemSsaVariable v) { none() }
/**
* Adds additional results to `ssaRead()` that are specific to Java.
*
* This predicate handles propagation of offsets for post-increment and post-decrement expressions
* in exactly the same way as the old Java implementation. Once the new implementation matches the
* old one, we should remove this predicate and propagate deltas for all similar patterns, whether
* or not they come from a post-increment/decrement expression.
*/
SemExpr specificSsaRead(SemSsaVariable v, int delta) { none() }
/**
* Adds additional results to `ssaRead()` that are specific to Java.
*
* This predicate handles propagation of offsets for post-increment and post-decrement expressions
* in exactly the same way as the old Java implementation. Once the new implementation matches the
* old one, we should remove this predicate and propagate deltas for all similar patterns, whether
* or not they come from a post-increment/decrement expression.
*/
SemExpr specificSsaRead(SemSsaVariable v, float delta) { none() }
/**
* Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
*/
predicate hasConstantBound(SemExpr e, int bound, boolean upper) { none() }
/**
* Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
*/
predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
/**
* Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).
*/
predicate hasBound(SemExpr e, SemExpr bound, int delta, boolean upper) { none() }
/**
* Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).
*/
predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() }
/**
* Holds if the value of `dest` is known to be `src + delta`.
*/
predicate additionalValueFlowStep(SemExpr dest, SemExpr src, int delta) { none() }
/**
* Holds if the value of `dest` is known to be `src + delta`.
*/
predicate additionalValueFlowStep(SemExpr dest, SemExpr src, float delta) { none() }
/**
* Gets the type that range analysis should use to track the result of the specified expression,
* if a type other than the original type of the expression is to be used.
*
* This predicate is commonly used in languages that support immutable "boxed" types that are
* actually references but whose values can be tracked as the type contained in the box.
*/
SemType getAlternateType(SemExpr e) { none() }
/**
* Gets the type that range analysis should use to track the result of the specified expression,
* if a type other than the original type of the expression is to be used.
*
* This predicate is commonly used in languages that support immutable "boxed" types that are
* actually references but whose values can be tracked as the type contained in the box.
*/
SemType getAlternateType(SemExpr e) { none() }
/**
* Gets the type that range analysis should use to track the result of the specified source
* variable, if a type other than the original type of the expression is to be used.
*
* This predicate is commonly used in languages that support immutable "boxed" types that are
* actually references but whose values can be tracked as the type contained in the box.
*/
SemType getAlternateTypeForSsaVariable(SemSsaVariable var) { none() }
/**
* Gets the type that range analysis should use to track the result of the specified source
* variable, if a type other than the original type of the expression is to be used.
*
* This predicate is commonly used in languages that support immutable "boxed" types that are
* actually references but whose values can be tracked as the type contained in the box.
*/
SemType getAlternateTypeForSsaVariable(SemSsaVariable var) { none() }
}

1032
cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisStage.qll Normal file
View File

File diff suppressed because it is too large Load Diff

245
cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeUtils.qll
View File

@@ -3,133 +3,138 @@
*/
private import experimental.semmle.code.cpp.semantic.Semantic
private import RangeAnalysisSpecific as Specific
private import RangeAnalysisSpecific
private import RangeAnalysisStage as Range
private import ConstantAnalysis
/**
* Gets an expression that equals `v - d`.
*/
SemExpr semSsaRead(SemSsaVariable v, int delta) {
// There are various language-specific extension points that can be removed once we no longer
// expect to match the original Java implementation's results exactly.
result = v.getAUse() and delta = 0
or
exists(int d1, SemConstantIntegerExpr c |
result.(SemAddExpr).hasOperands(semSsaRead(v, d1), c) and
delta = d1 - c.getIntValue() and
not Specific::ignoreSsaReadArithmeticExpr(result)
)
or
exists(SemSubExpr sub, int d1, SemConstantIntegerExpr c |
result = sub and
sub.getLeftOperand() = semSsaRead(v, d1) and
sub.getRightOperand() = c and
delta = d1 + c.getIntValue() and
not Specific::ignoreSsaReadArithmeticExpr(result)
)
or
result = v.(SemSsaExplicitUpdate).getSourceExpr() and
delta = 0 and
not Specific::ignoreSsaReadAssignment(v)
or
result = Specific::specificSsaRead(v, delta)
or
result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta) and
not Specific::ignoreSsaReadCopy(result)
or
result.(SemStoreExpr).getOperand() = semSsaRead(v, delta)
}
/**
* Gets a condition that tests whether `v` equals `e + delta`.
*
* If the condition evaluates to `testIsTrue`:
* - `isEq = true` : `v == e + delta`
* - `isEq = false` : `v != e + delta`
*/
SemGuard semEqFlowCond(SemSsaVariable v, SemExpr e, int delta, boolean isEq, boolean testIsTrue) {
exists(boolean eqpolarity |
result.isEquality(semSsaRead(v, delta), e, eqpolarity) and
(testIsTrue = true or testIsTrue = false) and
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
)
or
exists(boolean testIsTrue0 |
semImplies_v2(result, testIsTrue, semEqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
)
}
/**
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
*/
predicate semSsaUpdateStep(SemSsaExplicitUpdate v, SemExpr e, int delta) {
exists(SemExpr defExpr | defExpr = v.getSourceExpr() |
defExpr.(SemCopyValueExpr).getOperand() = e and delta = 0
module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::UtilSig<D> {
/**
* Gets an expression that equals `v - d`.
*/
SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) {
// There are various language-specific extension points that can be removed once we no longer
// expect to match the original Java implementation's results exactly.
result = v.getAUse() and delta = D::fromInt(0)
or
defExpr.(SemStoreExpr).getOperand() = e and delta = 0
exists(D::Delta d1, SemConstantIntegerExpr c |
result.(SemAddExpr).hasOperands(semSsaRead(v, d1), c) and
delta = D::fromFloat(D::toFloat(d1) - c.getIntValue()) and
not Lang::ignoreSsaReadArithmeticExpr(result)
)
or
defExpr.(SemAddOneExpr).getOperand() = e and delta = 1
exists(SemSubExpr sub, D::Delta d1, SemConstantIntegerExpr c |
result = sub and
sub.getLeftOperand() = semSsaRead(v, d1) and
sub.getRightOperand() = c and
delta = D::fromFloat(D::toFloat(d1) + c.getIntValue()) and
not Lang::ignoreSsaReadArithmeticExpr(result)
)
or
defExpr.(SemSubOneExpr).getOperand() = e and delta = -1
result = v.(SemSsaExplicitUpdate).getSourceExpr() and
delta = D::fromFloat(0) and
not Lang::ignoreSsaReadAssignment(v)
or
e = defExpr and
not (
defExpr instanceof SemCopyValueExpr or
defExpr instanceof SemStoreExpr or
defExpr instanceof SemAddOneExpr or
defExpr instanceof SemSubOneExpr
) and
delta = 0
)
}
result = Lang::specificSsaRead(v, delta)
or
result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta) and
not Lang::ignoreSsaReadCopy(result)
or
result.(SemStoreExpr).getOperand() = semSsaRead(v, delta)
}
/**
* Holds if `e1 + delta` equals `e2`.
*/
predicate semValueFlowStep(SemExpr e2, SemExpr e1, int delta) {
e2.(SemCopyValueExpr).getOperand() = e1 and delta = 0
or
e2.(SemStoreExpr).getOperand() = e1 and delta = 0
or
e2.(SemAddOneExpr).getOperand() = e1 and delta = 1
or
e2.(SemSubOneExpr).getOperand() = e1 and delta = -1
or
Specific::additionalValueFlowStep(e2, e1, delta)
or
exists(SemExpr x | e2.(SemAddExpr).hasOperands(e1, x) |
x.(SemConstantIntegerExpr).getIntValue() = delta
)
or
exists(SemExpr x, SemSubExpr sub |
e2 = sub and
sub.getLeftOperand() = e1 and
sub.getRightOperand() = x
|
x.(SemConstantIntegerExpr).getIntValue() = -delta
)
}
/**
* Gets a condition that tests whether `v` equals `e + delta`.
*
* If the condition evaluates to `testIsTrue`:
* - `isEq = true` : `v == e + delta`
* - `isEq = false` : `v != e + delta`
*/
SemGuard semEqFlowCond(
SemSsaVariable v, SemExpr e, D::Delta delta, boolean isEq, boolean testIsTrue
) {
exists(boolean eqpolarity |
result.isEquality(semSsaRead(v, delta), e, eqpolarity) and
(testIsTrue = true or testIsTrue = false) and
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
)
or
exists(boolean testIsTrue0 |
semImplies_v2(result, testIsTrue, semEqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
)
}
/**
* Gets the type used to track the specified expression's range information.
*
* Usually, this just `e.getSemType()`, but the language can override this to track immutable boxed
* primitive types as the underlying primitive type.
*/
SemType getTrackedType(SemExpr e) {
result = Specific::getAlternateType(e)
or
not exists(Specific::getAlternateType(e)) and result = e.getSemType()
}
/**
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
*/
predicate semSsaUpdateStep(SemSsaExplicitUpdate v, SemExpr e, D::Delta delta) {
exists(SemExpr defExpr | defExpr = v.getSourceExpr() |
defExpr.(SemCopyValueExpr).getOperand() = e and delta = D::fromFloat(0)
or
defExpr.(SemStoreExpr).getOperand() = e and delta = D::fromFloat(0)
or
defExpr.(SemAddOneExpr).getOperand() = e and delta = D::fromFloat(1)
or
defExpr.(SemSubOneExpr).getOperand() = e and delta = D::fromFloat(-1)
or
e = defExpr and
not (
defExpr instanceof SemCopyValueExpr or
defExpr instanceof SemStoreExpr or
defExpr instanceof SemAddOneExpr or
defExpr instanceof SemSubOneExpr
) and
delta = D::fromFloat(0)
)
}
/**
* Gets the type used to track the specified source variable's range information.
*
* Usually, this just `e.getType()`, but the language can override this to track immutable boxed
* primitive types as the underlying primitive type.
*/
SemType getTrackedTypeForSsaVariable(SemSsaVariable var) {
result = Specific::getAlternateTypeForSsaVariable(var)
or
not exists(Specific::getAlternateTypeForSsaVariable(var)) and result = var.getType()
/**
* Holds if `e1 + delta` equals `e2`.
*/
predicate semValueFlowStep(SemExpr e2, SemExpr e1, D::Delta delta) {
e2.(SemCopyValueExpr).getOperand() = e1 and delta = D::fromFloat(0)
or
e2.(SemStoreExpr).getOperand() = e1 and delta = D::fromFloat(0)
or
e2.(SemAddOneExpr).getOperand() = e1 and delta = D::fromFloat(1)
or
e2.(SemSubOneExpr).getOperand() = e1 and delta = D::fromFloat(-1)
or
Lang::additionalValueFlowStep(e2, e1, delta)
or
exists(SemExpr x | e2.(SemAddExpr).hasOperands(e1, x) |
D::fromInt(x.(SemConstantIntegerExpr).getIntValue()) = delta
)
or
exists(SemExpr x, SemSubExpr sub |
e2 = sub and
sub.getLeftOperand() = e1 and
sub.getRightOperand() = x
|
D::fromInt(-x.(SemConstantIntegerExpr).getIntValue()) = delta
)
}
/**
* Gets the type used to track the specified expression's range information.
*
* Usually, this just `e.getSemType()`, but the language can override this to track immutable boxed
* primitive types as the underlying primitive type.
*/
SemType getTrackedType(SemExpr e) {
result = Lang::getAlternateType(e)
or
not exists(Lang::getAlternateType(e)) and result = e.getSemType()
}
/**
* Gets the type used to track the specified source variable's range information.
*
* Usually, this just `e.getType()`, but the language can override this to track immutable boxed
* primitive types as the underlying primitive type.
*/
SemType getTrackedTypeForSsaVariable(SemSsaVariable var) {
result = Lang::getAlternateTypeForSsaVariable(var)
or
not exists(Lang::getAlternateTypeForSsaVariable(var)) and result = var.getType()
}
}

916
cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SignAnalysisCommon.qll
View File

@@ -6,488 +6,494 @@
* three-valued domain `{negative, zero, positive}`.
*/
private import RangeAnalysisStage
private import SignAnalysisSpecific as Specific
private import experimental.semmle.code.cpp.semantic.Semantic
private import ConstantAnalysis
private import RangeUtils
private import Sign
/**
* An SSA definition for which the analysis can compute the sign.
*
* The actual computation of the sign is done in an override of the `getSign()` predicate. The
* charpred of any subclass must _not_ invoke `getSign()`, directly or indirectly. This ensures
* that the charpred does not introduce negative recursion. The `getSign()` predicate may be
* recursive.
*/
abstract private class SignDef instanceof SemSsaVariable {
final string toString() { result = super.toString() }
module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
/**
* An SSA definition for which the analysis can compute the sign.
*
* The actual computation of the sign is done in an override of the `getSign()` predicate. The
* charpred of any subclass must _not_ invoke `getSign()`, directly or indirectly. This ensures
* that the charpred does not introduce negative recursion. The `getSign()` predicate may be
* recursive.
*/
abstract private class SignDef instanceof SemSsaVariable {
final string toString() { result = super.toString() }
/** Gets the possible signs of this SSA definition. */
abstract Sign getSign();
}
/** An SSA definition whose sign is computed based on standard flow. */
abstract private class FlowSignDef extends SignDef {
abstract override Sign getSign();
}
/** An SSA definition whose sign is determined by the sign of that definitions source expression. */
private class ExplicitSignDef extends FlowSignDef instanceof SemSsaExplicitUpdate {
final override Sign getSign() { result = semExprSign(super.getSourceExpr()) }
}
/** An SSA Phi definition, whose sign is the union of the signs of its inputs. */
private class PhiSignDef extends FlowSignDef instanceof SemSsaPhiNode {
final override Sign getSign() {
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
edge.phiInput(this, inp) and
result = semSsaSign(inp, edge)
)
}
}
/** An SSA definition whose sign is computed by a language-specific implementation. */
abstract class CustomSignDef extends SignDef {
abstract override Sign getSign();
}
/**
* An expression for which the analysis can compute the sign.
*
* The actual computation of the sign is done in an override of the `getSign()` predicate. The
* charpred of any subclass must _not_ invoke `getSign()`, directly or indirectly. This ensures
* that the charpred does not introduce negative recursion. The `getSign()` predicate may be
* recursive.
*
* Concrete implementations extend one of the following subclasses:
* - `ConstantSignExpr`, for expressions with a compile-time constant value.
* - `FlowSignExpr`, for expressions whose sign can be computed from the signs of their operands.
* - `CustomsignExpr`, for expressions whose sign can be computed by a language-specific
* implementation.
*
* If the same expression matches more than one of the above subclasses, the sign is computed as
* follows:
* - The sign of a `ConstantSignExpr` is computed solely from `ConstantSignExpr.getSign()`,
* regardless of any other subclasses.
* - If a non-`ConstantSignExpr` expression matches exactly one of `FlowSignExpr` or
* `CustomSignExpr`, the sign is computed by that class' `getSign()` predicate.
* - If a non-`ConstantSignExpr` expression matches both `FlowSignExpr` and `CustomSignExpr`, the
* sign is the _intersection_ of the signs of those two classes' `getSign()` predicates. Thus,
* both classes have the opportunity to _restrict_ the set of possible signs, not to generate new
* possible signs.
* - If an expression does not match any of the three subclasses, then it can have any sign.
*
* Note that the `getSign()` predicate is introduced only in subclasses of `SignExpr`.
*/
abstract class SignExpr instanceof SemExpr {
SignExpr() { not Specific::ignoreExprSign(this) }
final string toString() { result = super.toString() }
abstract Sign getSign();
}
/** An expression whose sign is determined by its constant numeric value. */
private class ConstantSignExpr extends SignExpr {
ConstantSignExpr() {
this instanceof SemConstantIntegerExpr or
exists(this.(SemNumericLiteralExpr).getApproximateFloatValue())
/** Gets the possible signs of this SSA definition. */
abstract Sign getSign();
}
final override Sign getSign() {
exists(int i | this.(SemConstantIntegerExpr).getIntValue() = i |
i < 0 and result = TNeg()
/** An SSA definition whose sign is computed based on standard flow. */
abstract private class FlowSignDef extends SignDef {
abstract override Sign getSign();
}
/** An SSA definition whose sign is determined by the sign of that definitions source expression. */
private class ExplicitSignDef extends FlowSignDef instanceof SemSsaExplicitUpdate {
final override Sign getSign() { result = semExprSign(super.getSourceExpr()) }
}
/** An SSA Phi definition, whose sign is the union of the signs of its inputs. */
private class PhiSignDef extends FlowSignDef instanceof SemSsaPhiNode {
final override Sign getSign() {
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
edge.phiInput(this, inp) and
result = semSsaSign(inp, edge)
)
}
}
/** An SSA definition whose sign is computed by a language-specific implementation. */
abstract class CustomSignDef extends SignDef {
abstract override Sign getSign();
}
/**
* An expression for which the analysis can compute the sign.
*
* The actual computation of the sign is done in an override of the `getSign()` predicate. The
* charpred of any subclass must _not_ invoke `getSign()`, directly or indirectly. This ensures
* that the charpred does not introduce negative recursion. The `getSign()` predicate may be
* recursive.
*
* Concrete implementations extend one of the following subclasses:
* - `ConstantSignExpr`, for expressions with a compile-time constant value.
* - `FlowSignExpr`, for expressions whose sign can be computed from the signs of their operands.
* - `CustomsignExpr`, for expressions whose sign can be computed by a language-specific
* implementation.
*
* If the same expression matches more than one of the above subclasses, the sign is computed as
* follows:
* - The sign of a `ConstantSignExpr` is computed solely from `ConstantSignExpr.getSign()`,
* regardless of any other subclasses.
* - If a non-`ConstantSignExpr` expression matches exactly one of `FlowSignExpr` or
* `CustomSignExpr`, the sign is computed by that class' `getSign()` predicate.
* - If a non-`ConstantSignExpr` expression matches both `FlowSignExpr` and `CustomSignExpr`, the
* sign is the _intersection_ of the signs of those two classes' `getSign()` predicates. Thus,
* both classes have the opportunity to _restrict_ the set of possible signs, not to generate new
* possible signs.
* - If an expression does not match any of the three subclasses, then it can have any sign.
*
* Note that the `getSign()` predicate is introduced only in subclasses of `SignExpr`.
*/
abstract class SignExpr instanceof SemExpr {
SignExpr() { not Specific::ignoreExprSign(this) }
final string toString() { result = super.toString() }
abstract Sign getSign();
}
/** An expression whose sign is determined by its constant numeric value. */
private class ConstantSignExpr extends SignExpr {
ConstantSignExpr() {
this instanceof SemConstantIntegerExpr or
exists(this.(SemNumericLiteralExpr).getApproximateFloatValue())
}
final override Sign getSign() {
exists(int i | this.(SemConstantIntegerExpr).getIntValue() = i |
i < 0 and result = TNeg()
or
i = 0 and result = TZero()
or
i > 0 and result = TPos()
)
or
i = 0 and result = TZero()
or
i > 0 and result = TPos()
)
or
not exists(this.(SemConstantIntegerExpr).getIntValue()) and
exists(float f | f = this.(SemNumericLiteralExpr).getApproximateFloatValue() |
f < 0 and result = TNeg()
or
f = 0 and result = TZero()
or
f > 0 and result = TPos()
)
}
}
abstract private class NonConstantSignExpr extends SignExpr {
NonConstantSignExpr() { not this instanceof ConstantSignExpr }
final override Sign getSign() {
// The result is the _intersection_ of the signs computed from flow and by the language.
(result = this.(FlowSignExpr).getSignRestriction() or not this instanceof FlowSignExpr) and
(result = this.(CustomSignExpr).getSignRestriction() or not this instanceof CustomSignExpr)
}
}
/** An expression whose sign is computed from the signs of its operands. */
abstract private class FlowSignExpr extends NonConstantSignExpr {
abstract Sign getSignRestriction();
}
/** An expression whose sign is computed by a language-specific implementation. */
abstract class CustomSignExpr extends NonConstantSignExpr {
abstract Sign getSignRestriction();
}
/** An expression whose sign is unknown. */
private class UnknownSignExpr extends SignExpr {
UnknownSignExpr() {
not this instanceof FlowSignExpr and
not this instanceof CustomSignExpr and
not this instanceof ConstantSignExpr and
(
// Only track numeric types.
getTrackedType(this) instanceof SemNumericType
or
// Unless the language says to track this expression anyway.
Specific::trackUnknownNonNumericExpr(this)
)
not exists(this.(SemConstantIntegerExpr).getIntValue()) and
exists(float f | f = this.(SemNumericLiteralExpr).getApproximateFloatValue() |
f < 0 and result = TNeg()
or
f = 0 and result = TZero()
or
f > 0 and result = TPos()
)
}
}
final override Sign getSign() { semAnySign(result) }
}
abstract private class NonConstantSignExpr extends SignExpr {
NonConstantSignExpr() { not this instanceof ConstantSignExpr }
/**
* A `Load` expression whose sign is computed from the sign of its SSA definition, restricted by
* inference from any intervening guards.
*/
class UseSignExpr extends FlowSignExpr {
SemSsaVariable v;
UseSignExpr() { v.getAUse() = this }
override Sign getSignRestriction() {
// Propagate via SSA
// Propagate the sign from the def of `v`, incorporating any inference from guards.
result = semSsaSign(v, any(SemSsaReadPositionBlock bb | bb.getAnExpr() = this))
or
// No block for this read. Just use the sign of the def.
// REVIEW: How can this happen?
not exists(SemSsaReadPositionBlock bb | bb.getAnExpr() = this) and
result = semSsaDefSign(v)
final override Sign getSign() {
// The result is the _intersection_ of the signs computed from flow and by the language.
(result = this.(FlowSignExpr).getSignRestriction() or not this instanceof FlowSignExpr) and
(result = this.(CustomSignExpr).getSignRestriction() or not this instanceof CustomSignExpr)
}
}
}
/** A binary expression whose sign is computed from the signs of its operands. */
private class BinarySignExpr extends FlowSignExpr {
SemBinaryExpr binary;
/** An expression whose sign is computed from the signs of its operands. */
abstract private class FlowSignExpr extends NonConstantSignExpr {
abstract Sign getSignRestriction();
}
BinarySignExpr() { binary = this }
/** An expression whose sign is computed by a language-specific implementation. */
abstract class CustomSignExpr extends NonConstantSignExpr {
abstract Sign getSignRestriction();
}
override Sign getSignRestriction() {
exists(SemExpr left, SemExpr right |
binaryExprOperands(binary, left, right) and
/** An expression whose sign is unknown. */
private class UnknownSignExpr extends SignExpr {
UnknownSignExpr() {
not this instanceof FlowSignExpr and
not this instanceof CustomSignExpr and
not this instanceof ConstantSignExpr and
(
// Only track numeric types.
Utils::getTrackedType(this) instanceof SemNumericType
or
// Unless the language says to track this expression anyway.
Specific::trackUnknownNonNumericExpr(this)
)
}
final override Sign getSign() { semAnySign(result) }
}
/**
* A `Load` expression whose sign is computed from the sign of its SSA definition, restricted by
* inference from any intervening guards.
*/
class UseSignExpr extends FlowSignExpr {
SemSsaVariable v;
UseSignExpr() { v.getAUse() = this }
override Sign getSignRestriction() {
// Propagate via SSA
// Propagate the sign from the def of `v`, incorporating any inference from guards.
result = semSsaSign(v, any(SemSsaReadPositionBlock bb | bb.getAnExpr() = this))
or
// No block for this read. Just use the sign of the def.
// REVIEW: How can this happen?
not exists(SemSsaReadPositionBlock bb | bb.getAnExpr() = this) and
result = semSsaDefSign(v)
}
}
/** A binary expression whose sign is computed from the signs of its operands. */
private class BinarySignExpr extends FlowSignExpr {
SemBinaryExpr binary;
BinarySignExpr() { binary = this }
override Sign getSignRestriction() {
exists(SemExpr left, SemExpr right |
binaryExprOperands(binary, left, right) and
result =
semExprSign(pragma[only_bind_out](left))
.applyBinaryOp(semExprSign(pragma[only_bind_out](right)), binary.getOpcode())
)
or
exists(SemDivExpr div | div = binary |
result = semExprSign(div.getLeftOperand()) and
result != TZero() and
div.getRightOperand().(SemFloatingPointLiteralExpr).getFloatValue() = 0
)
}
}
pragma[nomagic]
private predicate binaryExprOperands(SemBinaryExpr binary, SemExpr left, SemExpr right) {
binary.getLeftOperand() = left and binary.getRightOperand() = right
}
/**
* A `Convert`, `Box`, or `Unbox` expression.
*/
private class SemCastExpr instanceof SemUnaryExpr {
string toString() { result = super.toString() }
SemCastExpr() {
this instanceof SemConvertExpr
or
this instanceof SemBoxExpr
or
this instanceof SemUnboxExpr
}
}
/** A unary expression whose sign is computed from the sign of its operand. */
private class UnarySignExpr extends FlowSignExpr {
SemUnaryExpr unary;
UnarySignExpr() { unary = this and not this instanceof SemCastExpr }
override Sign getSignRestriction() {
result =
semExprSign(pragma[only_bind_out](left))
.applyBinaryOp(semExprSign(pragma[only_bind_out](right)), binary.getOpcode())
)
or
exists(SemDivExpr div | div = binary |
result = semExprSign(div.getLeftOperand()) and
result != TZero() and
div.getRightOperand().(SemFloatingPointLiteralExpr).getFloatValue() = 0
semExprSign(pragma[only_bind_out](unary.getOperand())).applyUnaryOp(unary.getOpcode())
}
}
/**
* A `Convert`, `Box`, or `Unbox` expression, whose sign is computed based on
* the sign of its operand and the source and destination types.
*/
abstract private class CastSignExpr extends FlowSignExpr {
SemUnaryExpr cast;
CastSignExpr() { cast = this and cast instanceof SemCastExpr }
override Sign getSignRestriction() { result = semExprSign(cast.getOperand()) }
}
/**
* A `Convert` expression.
*/
private class ConvertSignExpr extends CastSignExpr {
override SemConvertExpr cast;
}
/**
* A `Box` expression.
*/
private class BoxSignExpr extends CastSignExpr {
override SemBoxExpr cast;
}
/**
* An `Unbox` expression.
*/
private class UnboxSignExpr extends CastSignExpr {
override SemUnboxExpr cast;
UnboxSignExpr() {
exists(SemType fromType | fromType = Utils::getTrackedType(cast.getOperand()) |
// Only numeric source types are handled here.
fromType instanceof SemNumericType
)
}
}
private predicate unknownSign(SemExpr e) { e instanceof UnknownSignExpr }
/**
* Holds if `lowerbound` is a lower bound for `v` at `pos`. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate lowerBound(
SemExpr lowerbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
) {
exists(boolean testIsTrue, SemRelationalExpr comp |
pos.hasReadOfVar(v) and
semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
not unknownSign(lowerbound)
|
testIsTrue = true and
comp.getLesserOperand() = lowerbound and
comp.getGreaterOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
(if comp.isStrict() then isStrict = true else isStrict = false)
or
testIsTrue = false and
comp.getGreaterOperand() = lowerbound and
comp.getLesserOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
(if comp.isStrict() then isStrict = false else isStrict = true)
)
}
}
pragma[nomagic]
private predicate binaryExprOperands(SemBinaryExpr binary, SemExpr left, SemExpr right) {
binary.getLeftOperand() = left and binary.getRightOperand() = right
}
/**
* A `Convert`, `Box`, or `Unbox` expression.
*/
private class SemCastExpr extends SemUnaryExpr {
SemCastExpr() {
this instanceof SemConvertExpr
or
this instanceof SemBoxExpr
or
this instanceof SemUnboxExpr
}
}
/** A unary expression whose sign is computed from the sign of its operand. */
private class UnarySignExpr extends FlowSignExpr {
SemUnaryExpr unary;
UnarySignExpr() { unary = this and not this instanceof SemCastExpr }
override Sign getSignRestriction() {
result = semExprSign(pragma[only_bind_out](unary.getOperand())).applyUnaryOp(unary.getOpcode())
}
}
/**
* A `Convert`, `Box`, or `Unbox` expression, whose sign is computed based on
* the sign of its operand and the source and destination types.
*/
abstract private class CastSignExpr extends FlowSignExpr {
SemUnaryExpr cast;
CastSignExpr() { cast = this and cast instanceof SemCastExpr }
override Sign getSignRestriction() { result = semExprSign(cast.getOperand()) }
}
/**
* A `Convert` expression.
*/
private class ConvertSignExpr extends CastSignExpr {
override SemConvertExpr cast;
}
/**
* A `Box` expression.
*/
private class BoxSignExpr extends CastSignExpr {
override SemBoxExpr cast;
}
/**
* An `Unbox` expression.
*/
private class UnboxSignExpr extends CastSignExpr {
override SemUnboxExpr cast;
UnboxSignExpr() {
exists(SemType fromType | fromType = getTrackedType(cast.getOperand()) |
// Only numeric source types are handled here.
fromType instanceof SemNumericType
/**
* Holds if `upperbound` is an upper bound for `v` at `pos`. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate upperBound(
SemExpr upperbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
) {
exists(boolean testIsTrue, SemRelationalExpr comp |
pos.hasReadOfVar(v) and
semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
not unknownSign(upperbound)
|
testIsTrue = true and
comp.getGreaterOperand() = upperbound and
comp.getLesserOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
(if comp.isStrict() then isStrict = true else isStrict = false)
or
testIsTrue = false and
comp.getLesserOperand() = upperbound and
comp.getGreaterOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
(if comp.isStrict() then isStrict = false else isStrict = true)
)
}
}
private predicate unknownSign(SemExpr e) { e instanceof UnknownSignExpr }
/**
* Holds if `eqbound` is an equality/inequality for `v` at `pos`. This is
* restricted to only include bounds for which we might determine a sign. The
* boolean `isEq` gives the polarity:
* - `isEq = true` : `v = eqbound`
* - `isEq = false` : `v != eqbound`
*/
private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
exists(SemGuard guard, boolean testIsTrue, boolean polarity |
pos.hasReadOfVar(v) and
semGuardControlsSsaRead(guard, pos, testIsTrue) and
guard.isEquality(eqbound, Utils::semSsaRead(v, D::fromInt(0)), polarity) and
isEq = polarity.booleanXor(testIsTrue).booleanNot() and
not unknownSign(eqbound)
)
}
/**
* Holds if `lowerbound` is a lower bound for `v` at `pos`. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate lowerBound(
SemExpr lowerbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
) {
exists(boolean testIsTrue, SemRelationalExpr comp |
pos.hasReadOfVar(v) and
semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
not unknownSign(lowerbound)
|
testIsTrue = true and
comp.getLesserOperand() = lowerbound and
comp.getGreaterOperand() = semSsaRead(v, 0) and
(if comp.isStrict() then isStrict = true else isStrict = false)
/**
* Holds if `bound` is a bound for `v` at `pos` that needs to be positive in
* order for `v` to be positive.
*/
private predicate posBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
upperBound(bound, v, pos, _) or
eqBound(bound, v, pos, true)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that needs to be negative in
* order for `v` to be negative.
*/
private predicate negBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
lowerBound(bound, v, pos, _) or
eqBound(bound, v, pos, true)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v`
* can be zero.
*/
private predicate zeroBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
lowerBound(bound, v, pos, _) or
upperBound(bound, v, pos, _) or
eqBound(bound, v, pos, _)
}
/** Holds if `bound` allows `v` to be positive at `pos`. */
private predicate posBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
posBound(bound, v, pos) and TPos() = semExprSign(bound)
}
/** Holds if `bound` allows `v` to be negative at `pos`. */
private predicate negBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
negBound(bound, v, pos) and TNeg() = semExprSign(bound)
}
/** Holds if `bound` allows `v` to be zero at `pos`. */
private predicate zeroBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
lowerBound(bound, v, pos, _) and TNeg() = semExprSign(bound)
or
testIsTrue = false and
comp.getGreaterOperand() = lowerbound and
comp.getLesserOperand() = semSsaRead(v, 0) and
(if comp.isStrict() then isStrict = false else isStrict = true)
)
}
/**
* Holds if `upperbound` is an upper bound for `v` at `pos`. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate upperBound(
SemExpr upperbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
) {
exists(boolean testIsTrue, SemRelationalExpr comp |
pos.hasReadOfVar(v) and
semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
not unknownSign(upperbound)
|
testIsTrue = true and
comp.getGreaterOperand() = upperbound and
comp.getLesserOperand() = semSsaRead(v, 0) and
(if comp.isStrict() then isStrict = true else isStrict = false)
lowerBound(bound, v, pos, false) and TZero() = semExprSign(bound)
or
testIsTrue = false and
comp.getLesserOperand() = upperbound and
comp.getGreaterOperand() = semSsaRead(v, 0) and
(if comp.isStrict() then isStrict = false else isStrict = true)
)
}
upperBound(bound, v, pos, _) and TPos() = semExprSign(bound)
or
upperBound(bound, v, pos, false) and TZero() = semExprSign(bound)
or
eqBound(bound, v, pos, true) and TZero() = semExprSign(bound)
or
eqBound(bound, v, pos, false) and TZero() != semExprSign(bound)
}
/**
* Holds if `eqbound` is an equality/inequality for `v` at `pos`. This is
* restricted to only include bounds for which we might determine a sign. The
* boolean `isEq` gives the polarity:
* - `isEq = true` : `v = eqbound`
* - `isEq = false` : `v != eqbound`
*/
private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
exists(SemGuard guard, boolean testIsTrue, boolean polarity |
/**
* Holds if there is a bound that might restrict whether `v` has the sign `s`
* at `pos`.
*/
private predicate hasGuard(SemSsaVariable v, SemSsaReadPosition pos, Sign s) {
s = TPos() and posBound(_, v, pos)
or
s = TNeg() and negBound(_, v, pos)
or
s = TZero() and zeroBound(_, v, pos)
}
/**
* Gets a possible sign of `v` at `pos` based on its definition, where the sign
* might be ruled out by a guard.
*/
pragma[noinline]
private Sign guardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
result = semSsaDefSign(v) and
pos.hasReadOfVar(v) and
semGuardControlsSsaRead(guard, pos, testIsTrue) and
guard.isEquality(eqbound, semSsaRead(v, 0), polarity) and
isEq = polarity.booleanXor(testIsTrue).booleanNot() and
not unknownSign(eqbound)
)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that needs to be positive in
* order for `v` to be positive.
*/
private predicate posBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
upperBound(bound, v, pos, _) or
eqBound(bound, v, pos, true)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that needs to be negative in
* order for `v` to be negative.
*/
private predicate negBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
lowerBound(bound, v, pos, _) or
eqBound(bound, v, pos, true)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v`
* can be zero.
*/
private predicate zeroBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
lowerBound(bound, v, pos, _) or
upperBound(bound, v, pos, _) or
eqBound(bound, v, pos, _)
}
/** Holds if `bound` allows `v` to be positive at `pos`. */
private predicate posBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
posBound(bound, v, pos) and TPos() = semExprSign(bound)
}
/** Holds if `bound` allows `v` to be negative at `pos`. */
private predicate negBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
negBound(bound, v, pos) and TNeg() = semExprSign(bound)
}
/** Holds if `bound` allows `v` to be zero at `pos`. */
private predicate zeroBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
lowerBound(bound, v, pos, _) and TNeg() = semExprSign(bound)
or
lowerBound(bound, v, pos, false) and TZero() = semExprSign(bound)
or
upperBound(bound, v, pos, _) and TPos() = semExprSign(bound)
or
upperBound(bound, v, pos, false) and TZero() = semExprSign(bound)
or
eqBound(bound, v, pos, true) and TZero() = semExprSign(bound)
or
eqBound(bound, v, pos, false) and TZero() != semExprSign(bound)
}
/**
* Holds if there is a bound that might restrict whether `v` has the sign `s`
* at `pos`.
*/
private predicate hasGuard(SemSsaVariable v, SemSsaReadPosition pos, Sign s) {
s = TPos() and posBound(_, v, pos)
or
s = TNeg() and negBound(_, v, pos)
or
s = TZero() and zeroBound(_, v, pos)
}
/**
* Gets a possible sign of `v` at `pos` based on its definition, where the sign
* might be ruled out by a guard.
*/
pragma[noinline]
private Sign guardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
result = semSsaDefSign(v) and
pos.hasReadOfVar(v) and
hasGuard(v, pos, result)
}
/**
* Gets a possible sign of `v` at `pos` based on its definition, where no guard
* can rule it out.
*/
pragma[noinline]
private Sign unguardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
result = semSsaDefSign(v) and
pos.hasReadOfVar(v) and
not hasGuard(v, pos, result)
}
/**
* Gets a possible sign of `v` at read position `pos`, where a guard could have
* ruled out the sign but does not.
* This does not check that the definition of `v` also allows the sign.
*/
private Sign guardedSsaSignOk(SemSsaVariable v, SemSsaReadPosition pos) {
result = TPos() and
forex(SemExpr bound | posBound(bound, v, pos) | posBoundOk(bound, v, pos))
or
result = TNeg() and
forex(SemExpr bound | negBound(bound, v, pos) | negBoundOk(bound, v, pos))
or
result = TZero() and
forex(SemExpr bound | zeroBound(bound, v, pos) | zeroBoundOk(bound, v, pos))
}
/** Gets a possible sign for `v` at `pos`. */
private Sign semSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
result = unguardedSsaSign(v, pos)
or
result = guardedSsaSign(v, pos) and
result = guardedSsaSignOk(v, pos)
}
/** Gets a possible sign for `v`. */
pragma[nomagic]
Sign semSsaDefSign(SemSsaVariable v) { result = v.(SignDef).getSign() }
/** Gets a possible sign for `e`. */
cached
Sign semExprSign(SemExpr e) {
exists(Sign s | s = e.(SignExpr).getSign() |
if
getTrackedType(e) instanceof SemUnsignedIntegerType and
s = TNeg() and
not Specific::ignoreTypeRestrictions(e)
then result = TPos()
else result = s
)
}
/**
* Dummy predicate that holds for any sign. This is added to improve readability
* of cases where the sign is unrestricted.
*/
predicate semAnySign(Sign s) { any() }
/** Holds if `e` can be positive and cannot be negative. */
predicate semPositive(SemExpr e) {
semExprSign(e) = TPos() and
not semExprSign(e) = TNeg()
}
/** Holds if `e` can be negative and cannot be positive. */
predicate semNegative(SemExpr e) {
semExprSign(e) = TNeg() and
not semExprSign(e) = TPos()
}
/** Holds if `e` is strictly positive. */
predicate semStrictlyPositive(SemExpr e) {
semExprSign(e) = TPos() and
not semExprSign(e) = TNeg() and
not semExprSign(e) = TZero()
}
/** Holds if `e` is strictly negative. */
predicate semStrictlyNegative(SemExpr e) {
semExprSign(e) = TNeg() and
not semExprSign(e) = TPos() and
not semExprSign(e) = TZero()
hasGuard(v, pos, result)
}
/**
* Gets a possible sign of `v` at `pos` based on its definition, where no guard
* can rule it out.
*/
pragma[noinline]
private Sign unguardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
result = semSsaDefSign(v) and
pos.hasReadOfVar(v) and
not hasGuard(v, pos, result)
}
/**
* Gets a possible sign of `v` at read position `pos`, where a guard could have
* ruled out the sign but does not.
* This does not check that the definition of `v` also allows the sign.
*/
private Sign guardedSsaSignOk(SemSsaVariable v, SemSsaReadPosition pos) {
result = TPos() and
forex(SemExpr bound | posBound(bound, v, pos) | posBoundOk(bound, v, pos))
or
result = TNeg() and
forex(SemExpr bound | negBound(bound, v, pos) | negBoundOk(bound, v, pos))
or
result = TZero() and
forex(SemExpr bound | zeroBound(bound, v, pos) | zeroBoundOk(bound, v, pos))
}
/** Gets a possible sign for `v` at `pos`. */
private Sign semSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
result = unguardedSsaSign(v, pos)
or
result = guardedSsaSign(v, pos) and
result = guardedSsaSignOk(v, pos)
}
/** Gets a possible sign for `v`. */
pragma[nomagic]
Sign semSsaDefSign(SemSsaVariable v) { result = v.(SignDef).getSign() }
/** Gets a possible sign for `e`. */
cached
Sign semExprSign(SemExpr e) {
exists(Sign s | s = e.(SignExpr).getSign() |
if
Utils::getTrackedType(e) instanceof SemUnsignedIntegerType and
s = TNeg() and
not Specific::ignoreTypeRestrictions(e)
then result = TPos()
else result = s
)
}
/**
* Dummy predicate that holds for any sign. This is added to improve readability
* of cases where the sign is unrestricted.
*/
predicate semAnySign(Sign s) { any() }
/** Holds if `e` can be positive and cannot be negative. */
predicate semPositive(SemExpr e) {
semExprSign(e) = TPos() and
not semExprSign(e) = TNeg()
}
/** Holds if `e` can be negative and cannot be positive. */
predicate semNegative(SemExpr e) {
semExprSign(e) = TNeg() and
not semExprSign(e) = TPos()
}
/** Holds if `e` is strictly positive. */
predicate semStrictlyPositive(SemExpr e) {
semExprSign(e) = TPos() and
not semExprSign(e) = TNeg() and
not semExprSign(e) = TZero()
}
/** Holds if `e` is strictly negative. */
predicate semStrictlyNegative(SemExpr e) {
semExprSign(e) = TNeg() and
not semExprSign(e) = TPos() and
not semExprSign(e) = TZero()
}
}

2
cpp/ql/lib/qlpack.yml
View File

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

2
cpp/ql/lib/semmle/code/cpp/Location.qll
View File

@@ -10,12 +10,14 @@ import semmle.code.cpp.File
*/
class Location extends @location {
/** Gets the container corresponding to this location. */
pragma[nomagic]
Container getContainer() { this.fullLocationInfo(result, _, _, _, _) }
/** Gets the file corresponding to this location, if any. */
File getFile() { result = this.getContainer() }
/** Gets the 1-based line number (inclusive) where this location starts. */
pragma[nomagic]
int getStartLine() { this.fullLocationInfo(_, result, _, _, _) }
/** Gets the 1-based column number (inclusive) where this location starts. */

12
cpp/ql/lib/semmle/code/cpp/dataflow/old/internal/DataFlowImplConsistency.qll
View File

@@ -45,6 +45,16 @@ module Consistency {
) {
none()
}
/** Holds if `(c, pos, p)` should be excluded from the consistency test `uniqueParameterNodeAtPosition`. */
predicate uniqueParameterNodeAtPositionExclude(DataFlowCallable c, ParameterPosition pos, Node p) {
none()
}
/** Holds if `(c, pos, p)` should be excluded from the consistency test `uniqueParameterNodePosition`. */
predicate uniqueParameterNodePositionExclude(DataFlowCallable c, ParameterPosition pos, Node p) {
none()
}
}
private class RelevantNode extends Node {
@@ -246,6 +256,7 @@ module Consistency {
query predicate uniqueParameterNodeAtPosition(
DataFlowCallable c, ParameterPosition pos, Node p, string msg
) {
not any(ConsistencyConfiguration conf).uniqueParameterNodeAtPositionExclude(c, pos, p) and
isParameterNode(p, c, pos) and
not exists(unique(Node p0 | isParameterNode(p0, c, pos))) and
msg = "Parameters with overlapping positions."
@@ -254,6 +265,7 @@ module Consistency {
query predicate uniqueParameterNodePosition(
DataFlowCallable c, ParameterPosition pos, Node p, string msg
) {
not any(ConsistencyConfiguration conf).uniqueParameterNodePositionExclude(c, pos, p) and
isParameterNode(p, c, pos) and
not exists(unique(ParameterPosition pos0 | isParameterNode(p, c, pos0))) and
msg = "Parameter node with multiple positions."

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

@@ -45,6 +45,16 @@ module Consistency {
) {
none()
}
/** Holds if `(c, pos, p)` should be excluded from the consistency test `uniqueParameterNodeAtPosition`. */
predicate uniqueParameterNodeAtPositionExclude(DataFlowCallable c, ParameterPosition pos, Node p) {
none()
}
/** Holds if `(c, pos, p)` should be excluded from the consistency test `uniqueParameterNodePosition`. */
predicate uniqueParameterNodePositionExclude(DataFlowCallable c, ParameterPosition pos, Node p) {
none()
}
}
private class RelevantNode extends Node {
@@ -246,6 +256,7 @@ module Consistency {
query predicate uniqueParameterNodeAtPosition(
DataFlowCallable c, ParameterPosition pos, Node p, string msg
) {
not any(ConsistencyConfiguration conf).uniqueParameterNodeAtPositionExclude(c, pos, p) and
isParameterNode(p, c, pos) and
not exists(unique(Node p0 | isParameterNode(p0, c, pos))) and
msg = "Parameters with overlapping positions."
@@ -254,6 +265,7 @@ module Consistency {
query predicate uniqueParameterNodePosition(
DataFlowCallable c, ParameterPosition pos, Node p, string msg
) {
not any(ConsistencyConfiguration conf).uniqueParameterNodePositionExclude(c, pos, p) and
isParameterNode(p, c, pos) and
not exists(unique(ParameterPosition pos0 | isParameterNode(p, c, pos0))) and
msg = "Parameter node with multiple positions."

10
cpp/ql/lib/semmle/code/cpp/ir/implementation/Opcode.qll
View File

@@ -30,6 +30,7 @@ private newtype TOpcode =
TNegate() or
TShiftLeft() or
TShiftRight() or
TUnsignedShiftRight() or
TBitAnd() or
TBitOr() or
TBitXor() or
@@ -652,6 +653,15 @@ module Opcode {
final override string toString() { result = "ShiftRight" }
}
/**
* The `Opcode` for a `UnsignedShiftRightInstruction`.
*
* See the `UnsignedShiftRightInstruction` documentation for more details.
*/
class UnsignedShiftRight extends BinaryBitwiseOpcode, TUnsignedShiftRight {
final override string toString() { result = "UnsignedShiftRight" }
}
/**
* The `Opcode` for a `BitAndInstruction`.
*

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

@@ -1204,6 +1204,17 @@ class ShiftRightInstruction extends BinaryBitwiseInstruction {
ShiftRightInstruction() { this.getOpcode() instanceof Opcode::ShiftRight }
}
/**
* An instruction that shifts its left operand to the right by the number of bits specified by its
* right operand.
*
* Both operands must have an integer type. The result has the same type as the left operand.
* The leftmost bits are zero-filled.
*/
class UnsignedShiftRightInstruction extends BinaryBitwiseInstruction {
UnsignedShiftRightInstruction() { this.getOpcode() instanceof Opcode::UnsignedShiftRight }
}
/**
* An instruction that performs a binary arithmetic operation involving at least one pointer
* operand.

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

@@ -1204,6 +1204,17 @@ class ShiftRightInstruction extends BinaryBitwiseInstruction {
ShiftRightInstruction() { this.getOpcode() instanceof Opcode::ShiftRight }
}
/**
* An instruction that shifts its left operand to the right by the number of bits specified by its
* right operand.
*
* Both operands must have an integer type. The result has the same type as the left operand.
* The leftmost bits are zero-filled.
*/
class UnsignedShiftRightInstruction extends BinaryBitwiseInstruction {
UnsignedShiftRightInstruction() { this.getOpcode() instanceof Opcode::UnsignedShiftRight }
}
/**
* An instruction that performs a binary arithmetic operation involving at least one pointer
* operand.

11
cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll
View File

@@ -1204,6 +1204,17 @@ class ShiftRightInstruction extends BinaryBitwiseInstruction {
ShiftRightInstruction() { this.getOpcode() instanceof Opcode::ShiftRight }
}
/**
* An instruction that shifts its left operand to the right by the number of bits specified by its
* right operand.
*
* Both operands must have an integer type. The result has the same type as the left operand.
* The leftmost bits are zero-filled.
*/
class UnsignedShiftRightInstruction extends BinaryBitwiseInstruction {
UnsignedShiftRightInstruction() { this.getOpcode() instanceof Opcode::UnsignedShiftRight }
}
/**
* An instruction that performs a binary arithmetic operation involving at least one pointer
* operand.

6
cpp/ql/src/CHANGELOG.md
View File

@@ -1,3 +1,9 @@
## 0.5.1
### Minor Analysis Improvements
* The `cpp/no-space-for-terminator` and `cpp/uncontrolled-allocation-size` queries have been enhanced with heuristic detection of allocations. These queries now find more results.
## 0.5.0
### Minor Analysis Improvements

258
cpp/ql/src/Critical/MissingCheckScanf.ql
View File

@@ -20,81 +20,190 @@ import semmle.code.cpp.dataflow.DataFlow
import semmle.code.cpp.ir.IR
import semmle.code.cpp.ir.ValueNumbering
/** An expression appearing as an output argument to a `scanf`-like call */
class ScanfOutput extends Expr {
ScanfFunctionCall call;
int varargIndex;
Instruction instr;
ValueNumber valNum;
/**
* Holds if `call` is a `scanf`-like function that may write to `output` at index `index`.
*
* Furthermore, `instr` is the instruction that defines the address of the `index`'th argument
* of `call`, and `vn` is the value number of `instr.`
*/
predicate isSource(ScanfFunctionCall call, int index, Instruction instr, ValueNumber vn, Expr output) {
output = call.getOutputArgument(index).getFullyConverted() and
instr.getConvertedResultExpression() = output and
vn.getAnInstruction() = instr
}
ScanfOutput() {
this = call.getOutputArgument(varargIndex).getFullyConverted() and
instr.getConvertedResultExpression() = this and
valueNumber(instr) = valNum
}
/**
* Holds if `instr` is control-flow reachable in 0 or more steps from
* a call to a `scanf`-like function.
*/
pragma[nomagic]
predicate fwdFlow0(Instruction instr) {
isSource(_, _, instr, _, _)
or
exists(Instruction prev |
fwdFlow0(prev) and
prev.getASuccessor() = instr
)
}
ScanfFunctionCall getCall() { result = call }
/**
* Holds if `instr` is part of the IR translation of `access` that
* is not an expression being deallocated, and `instr` has value
* number `vn`.
*/
predicate isSink(Instruction instr, Access access, ValueNumber vn) {
instr.getAst() = access and
not any(DeallocationExpr dealloc).getFreedExpr() = access and
vn.getAnInstruction() = instr
}
/**
* Returns the smallest possible `scanf` return value that would indicate
* success in writing this output argument.
*/
int getMinimumGuardConstant() {
result =
varargIndex + 1 -
count(ScanfFormatLiteral f, int n |
// Special case: %n writes to an argument without reading any input.
// It does not increase the count returned by `scanf`.
n <= varargIndex and f.getUse() = call and f.getConversionChar(n) = "n"
)
}
predicate hasGuardedAccess(Access e, boolean isGuarded) {
e = this.getAnAccess() and
if
exists(int value, int minGuard | minGuard = this.getMinimumGuardConstant() |
e.getBasicBlock() = blockGuardedBy(value, "==", call) and minGuard <= value
or
e.getBasicBlock() = blockGuardedBy(value, "<", call) and minGuard - 1 <= value
or
e.getBasicBlock() = blockGuardedBy(value, "<=", call) and minGuard <= value
)
then isGuarded = true
else isGuarded = false
}
/**
* Get a subsequent access of the same underlying storage,
* but before it gets reset or reused in another `scanf` call.
*/
Access getAnAccess() {
exists(Instruction dst |
this.bigStep() = dst and
dst.getAst() = result and
valueNumber(dst) = valNum
)
}
private Instruction bigStep() {
result = this.smallStep(instr)
/**
* Holds if `instr` is part of a path from a call to a `scanf`-like function
* to a use of the written variable.
*/
pragma[nomagic]
predicate revFlow0(Instruction instr) {
fwdFlow0(instr) and
(
isSink(instr, _, _)
or
exists(Instruction i | i = this.bigStep() | result = this.smallStep(i))
}
exists(Instruction succ | revFlow0(succ) | instr.getASuccessor() = succ)
)
}
private Instruction smallStep(Instruction i) {
instr.getASuccessor*() = i and
i.getASuccessor() = result and
not this.isBarrier(result)
}
private predicate isBarrier(Instruction i) {
valueNumber(i) = valNum and
exists(Expr e | i.getAst() = e |
i = any(StoreInstruction s).getDestinationAddress()
or
[e, e.getParent().(AddressOfExpr)] instanceof ScanfOutput
/**
* Holds if `instr` is part of a path from a call to a `scanf`-like function
* that writes to a variable with value number `vn`, without passing through
* redefinitions of the variable.
*/
pragma[nomagic]
private predicate fwdFlow(Instruction instr, ValueNumber vn) {
revFlow0(instr) and
(
isSource(_, _, instr, vn, _)
or
exists(Instruction prev |
fwdFlow(prev, vn) and
prev.getASuccessor() = instr and
not isBarrier(instr, vn)
)
}
)
}
/**
* Holds if `instr` is part of a path from a call to a `scanf`-like function
* that writes to a variable with value number `vn`, without passing through
* redefinitions of the variable.
*
* Note: This predicate only holds for the `(intr, vn)` pairs that are also
* control-flow reachable from an argument to a `scanf`-like function call.
*/
pragma[nomagic]
predicate revFlow(Instruction instr, ValueNumber vn) {
fwdFlow(instr, vn) and
(
isSink(instr, _, vn)
or
exists(Instruction succ | revFlow(succ, vn) |
instr.getASuccessor() = succ and
not isBarrier(succ, vn)
)
)
}
/**
* A type that bundles together a reachable instruction with the appropriate
* value number (i.e., the value number that's transferred from the source
* to the sink).
*/
newtype TNode = MkNode(Instruction instr, ValueNumber vn) { revFlow(instr, vn) }
class Node extends MkNode {
ValueNumber vn;
Instruction instr;
Node() { this = MkNode(instr, vn) }
final string toString() { result = instr.toString() }
final Node getASuccessor() { result = MkNode(instr.getASuccessor(), vn) }
final Location getLocation() { result = instr.getLocation() }
}
/**
* Holds if `instr` is an instruction with value number `vn` that is
* used in a store operation, or is overwritten by another call to
* a `scanf`-like function.
*/
private predicate isBarrier(Instruction instr, ValueNumber vn) {
// We only need to compute barriers for instructions that we
// managed to hit during the initial flow stage.
revFlow0(pragma[only_bind_into](instr)) and
valueNumber(instr) = vn and
exists(Expr e | instr.getAst() = e |
instr = any(StoreInstruction s).getDestinationAddress()
or
isSource(_, _, _, _, [e, e.getParent().(AddressOfExpr)])
)
}
/** Holds if `n1` steps to `n2` in a single step. */
predicate isSuccessor(Node n1, Node n2) { n1.getASuccessor() = n2 }
predicate hasFlow(Node n1, Node n2) = fastTC(isSuccessor/2)(n1, n2)
Node getNode(Instruction instr, ValueNumber vn) { result = MkNode(instr, vn) }
/**
* Holds if `source` is the `index`'th argument to the `scanf`-like call `call`, and `sink` is
* an instruction that is part of the translation of `access` which is a transitive
* control-flow successor of `call`.
*
* Furthermore, `source` and `sink` have identical global value numbers.
*/
predicate hasFlow(
Instruction source, ScanfFunctionCall call, int index, Instruction sink, Access access
) {
exists(ValueNumber vn |
isSource(call, index, source, vn, _) and
hasFlow(getNode(source, vn), getNode(sink, vn)) and
isSink(sink, access, vn)
)
}
/**
* Gets the smallest possible `scanf` return value of `call` that would indicate
* success in writing the output argument at index `index`.
*/
int getMinimumGuardConstant(ScanfFunctionCall call, int index) {
isSource(call, index, _, _, _) and
result =
index + 1 -
count(ScanfFormatLiteral f, int n |
// Special case: %n writes to an argument without reading any input.
// It does not increase the count returned by `scanf`.
n <= index and f.getUse() = call and f.getConversionChar(n) = "n"
)
}
/**
* Holds the access to `e` isn't guarded by a check that ensures that `call` returned
* at least `minGuard`.
*/
predicate hasNonGuardedAccess(ScanfFunctionCall call, Access e, int minGuard) {
exists(int index |
hasFlow(_, call, index, _, e) and
minGuard = getMinimumGuardConstant(call, index)
|
not exists(int value |
e.getBasicBlock() = blockGuardedBy(value, "==", call) and minGuard <= value
or
e.getBasicBlock() = blockGuardedBy(value, "<", call) and minGuard - 1 <= value
or
e.getBasicBlock() = blockGuardedBy(value, "<=", call) and minGuard <= value
)
)
}
/** Returns a block guarded by the assertion of `value op call` */
@@ -112,12 +221,9 @@ BasicBlock blockGuardedBy(int value, string op, ScanfFunctionCall call) {
)
}
from ScanfOutput output, ScanfFunctionCall call, Access access
where
output.getCall() = call and
output.hasGuardedAccess(access, false) and
not exists(DeallocationExpr dealloc | dealloc.getFreedExpr() = access)
from ScanfFunctionCall call, Access access, int minGuard
where hasNonGuardedAccess(call, access, minGuard)
select access,
"This variable is read, but may not have been written. " +
"It should be guarded by a check that the $@ returns at least " +
output.getMinimumGuardConstant() + ".", call, call.toString()
"It should be guarded by a check that the $@ returns at least " + minGuard + ".", call,
call.toString()

78
cpp/ql/src/Security/CWE/CWE-290/AuthenticationBypass.ql
View File

@@ -15,76 +15,24 @@
import semmle.code.cpp.ir.dataflow.internal.DefaultTaintTrackingImpl
import TaintedWithPath
string getATopLevelDomain() {
result =
[
"com", "ru", "net", "org", "de", "jp", "uk", "br", "pl", "in", "it", "fr", "au", "info", "nl",
"cn", "ir", "es", "cz", "biz", "ca", "eu", "ua", "kr", "za", "co", "gr", "ro", "se", "tw",
"vn", "mx", "ch", "tr", "at", "be", "hu", "tv", "dk", "me", "ar", "us", "no", "sk", "fi",
"id", "cl", "nz", "by", "xyz", "pt", "ie", "il", "kz", "my", "hk", "lt", "cc", "sg", "io",
"edu", "gov"
]
}
predicate hardCodedAddressOrIP(StringLiteral txt) {
exists(string s | s = txt.getValueText() |
// Hard-coded ip addresses, such as 127.0.0.1
s.regexpMatch("\"[0-9]+[.][0-9]+[.][0-9]+[.][0-9]+\"") or
// Hard-coded addresses such as www.mycompany.com
s.matches("\"www.%\"") or
s.matches("\"http:%\"") or
s.matches("\"https:%\"") or
s.matches("\"%.com\"") or
s.matches("\"%.ru\"") or
s.matches("\"%.net\"") or
s.matches("\"%.org\"") or
s.matches("\"%.de\"") or
s.matches("\"%.jp\"") or
s.matches("\"%.uk\"") or
s.matches("\"%.br\"") or
s.matches("\"%.pl\"") or
s.matches("\"%.in\"") or
s.matches("\"%.it\"") or
s.matches("\"%.fr\"") or
s.matches("\"%.au\"") or
s.matches("\"%.info\"") or
s.matches("\"%.nl\"") or
s.matches("\"%.cn\"") or
s.matches("\"%.ir\"") or
s.matches("\"%.es\"") or
s.matches("\"%.cz\"") or
s.matches("\"%.biz\"") or
s.matches("\"%.ca\"") or
s.matches("\"%.eu\"") or
s.matches("\"%.ua\"") or
s.matches("\"%.kr\"") or
s.matches("\"%.za\"") or
s.matches("\"%.co\"") or
s.matches("\"%.gr\"") or
s.matches("\"%.ro\"") or
s.matches("\"%.se\"") or
s.matches("\"%.tw\"") or
s.matches("\"%.vn\"") or
s.matches("\"%.mx\"") or
s.matches("\"%.ch\"") or
s.matches("\"%.tr\"") or
s.matches("\"%.at\"") or
s.matches("\"%.be\"") or
s.matches("\"%.hu\"") or
s.matches("\"%.tv\"") or
s.matches("\"%.dk\"") or
s.matches("\"%.me\"") or
s.matches("\"%.ar\"") or
s.matches("\"%.us\"") or
s.matches("\"%.no\"") or
s.matches("\"%.sk\"") or
s.matches("\"%.fi\"") or
s.matches("\"%.id\"") or
s.matches("\"%.cl\"") or
s.matches("\"%.nz\"") or
s.matches("\"%.by\"") or
s.matches("\"%.xyz\"") or
s.matches("\"%.pt\"") or
s.matches("\"%.ie\"") or
s.matches("\"%.il\"") or
s.matches("\"%.kz\"") or
s.matches("\"%.my\"") or
s.matches("\"%.hk\"") or
s.matches("\"%.lt\"") or
s.matches("\"%.cc\"") or
s.matches("\"%.sg\"") or
s.matches("\"%.io\"") or
s.matches("\"%.edu\"") or
s.matches("\"%.gov\"")
s.regexpMatch("\"(www\\.|http:|https:).*\"") or
s.regexpMatch("\".*\\.(" + strictconcat(getATopLevelDomain(), "|") + ")\"")
)
}

7
cpp/ql/src/change-notes/2023-01-05-heuristic-allocations.md → cpp/ql/src/change-notes/released/0.5.1.md
View File

@@ -1,4 +1,5 @@
---
category: minorAnalysis
---
## 0.5.1
### Minor Analysis Improvements
* The `cpp/no-space-for-terminator` and `cpp/uncontrolled-allocation-size` queries have been enhanced with heuristic detection of allocations. These queries now find more results.

2
cpp/ql/src/codeql-pack.release.yml
View File

@@ -1,2 +1,2 @@
---
lastReleaseVersion: 0.5.0
lastReleaseVersion: 0.5.1

9
cpp/ql/src/codeql-suites/cpp-security-experimental.qls Normal file
View File

@@ -0,0 +1,9 @@
- description: Extended and experimental security queries for C and C++
- queries: .
- apply: security-experimental-selectors.yml
from: codeql/suite-helpers
- apply: codeql-suites/exclude-slow-queries.yml
# Excluding problematically slow experimental queries
- exclude:
query path:
- experimental/Security/CWE/CWE-266/IncorrectPrivilegeAssignment.ql

1
cpp/ql/src/experimental/Likely Bugs/ArrayAccessProductFlow.ql
View File

@@ -6,6 +6,7 @@
* @id cpp/off-by-one-array-access
* @tags reliability
* security
* experimental
*/
import cpp

1
cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql
View File

@@ -7,6 +7,7 @@
* @id cpp/overrun-write
* @tags reliability
* security
* experimental
* external/cwe/cwe-119
* external/cwe/cwe-131
*/

1
cpp/ql/src/experimental/Likely Bugs/RedundantNullCheckParam.ql
View File

@@ -9,6 +9,7 @@
* @tags reliability
* security
* external/cwe/cwe-476
* experimental
*/
import cpp

1
cpp/ql/src/experimental/Security/CWE/CWE-020/LateCheckOfFunctionArgument.ql
View File

@@ -9,6 +9,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-20
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-020/NoCheckBeforeUnsafePutUser.ql
View File

@@ -11,6 +11,7 @@
* @problem.severity warning
* @security-severity 7.5
* @tags security
* experimental
* external/cwe/cwe-020
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-078/WordexpTainted.ql
View File

@@ -8,6 +8,7 @@
* @precision high
* @id cpp/wordexp-injection
* @tags security
* experimental
* external/cwe/cwe-078
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-1041/FindWrapperFunctions.ql
View File

@@ -8,6 +8,7 @@
* @tags correctness
* maintainability
* security
* experimental
* external/cwe/cwe-1041
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-1126/DeclarationOfVariableWithUnnecessarilyWideScope.ql
View File

@@ -9,6 +9,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-1126
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-120/MemoryUnsafeFunctionScan.ql
View File

@@ -6,6 +6,7 @@
* @id cpp/memory-unsafe-function-scan
* @tags reliability
* security
* experimental
* external/cwe/cwe-120
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-125/DangerousWorksWithMultibyteOrWideCharacters.ql
View File

@@ -7,6 +7,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-125
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-190/AllocMultiplicationOverflow.ql
View File

@@ -6,6 +6,7 @@
* @precision low
* @tags security
* correctness
* experimental
* external/cwe/cwe-190
* external/cwe/cwe-128
* @id cpp/multiplication-overflow-in-alloc

1
cpp/ql/src/experimental/Security/CWE/CWE-190/DangerousUseOfTransformationAfterOperation.ql
View File

@@ -7,6 +7,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-190
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-193/ConstantSizeArrayOffByOne.ql
View File

@@ -7,6 +7,7 @@
* @id cpp/constant-array-overflow
* @tags reliability
* security
* experimental
*/
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis

1
cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql
View File

@@ -8,6 +8,7 @@
* @id cpp/invalid-pointer-deref
* @tags reliability
* security
* experimental
* external/cwe/cwe-119
* external/cwe/cwe-125
* external/cwe/cwe-193

1
cpp/ql/src/experimental/Security/CWE/CWE-200/ExposureSensitiveInformationUnauthorizedActor.ql
View File

@@ -8,6 +8,7 @@
* @tags correctness
* maintainability
* security
* experimental
* external/cwe/cwe-200
* external/cwe/cwe-264
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-243/IncorrectChangingWorkingDirectory.ql
View File

@@ -7,6 +7,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-243
* external/cwe/cwe-252
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-266/IncorrectPrivilegeAssignment.ql
View File

@@ -8,6 +8,7 @@
* @tags correctness
* maintainability
* security
* experimental
* external/cwe/cwe-266
* external/cwe/cwe-264
* external/cwe/cwe-200

1
cpp/ql/src/experimental/Security/CWE/CWE-273/PrivilegeDroppingOutoforder.ql
View File

@@ -8,6 +8,7 @@
* @problem.severity recommendation
* @id cpp/drop-linux-privileges-outoforder
* @tags security
* experimental
* external/cwe/cwe-273
* @precision medium
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-285/PamAuthorization.ql
View File

@@ -5,6 +5,7 @@
* @problem.severity error
* @id cpp/pam-auth-bypass
* @tags security
* experimental
* external/cwe/cwe-285
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-359/PrivateCleartextWrite.ql
View File

@@ -6,6 +6,7 @@
* @problem.severity error
* @id cpp/private-cleartext-write
* @tags security
* experimental
* external/cwe/cwe-359
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-362/double-fetch.ql
View File

@@ -11,6 +11,7 @@
* @problem.severity warning
* @security-severity 7.5
* @tags security
* experimental
* external/cwe/cwe-362
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-377/InsecureTemporaryFile.ql
View File

@@ -7,6 +7,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-377
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-401/MemoryLeakOnFailedCallToRealloc.ql
View File

@@ -8,6 +8,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-401
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-415/DoubleFree.ql
View File

@@ -6,6 +6,7 @@
* @problem.severity warning
* @precision medium
* @tags security
* experimental
* external/cwe/cwe-415
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-476/DangerousUseOfExceptionBlocks.ql
View File

@@ -7,6 +7,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-476
* external/cwe/cwe-415
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-561/FindIncorrectlyUsedSwitch.ql
View File

@@ -8,6 +8,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-561
* external/cwe/cwe-691
* external/cwe/cwe-478

1
cpp/ql/src/experimental/Security/CWE/CWE-670/DangerousUseSSL_shutdown.ql
View File

@@ -7,6 +7,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-670
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-675/DoubleRelease.ql
View File

@@ -6,6 +6,7 @@
* @problem.severity warning
* @precision medium
* @tags security
* experimental
* external/cwe/cwe-675
* external/cwe/cwe-666
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-691/InsufficientControlFlowManagementAfterRefactoringTheCode.ql
View File

@@ -10,6 +10,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-691
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-691/InsufficientControlFlowManagementWhenUsingBitOperations.ql
View File

@@ -8,6 +8,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-691
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-703/FindIncorrectlyUsedExceptions.ql
View File

@@ -7,6 +7,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-703
* external/cwe/cwe-248
* external/cwe/cwe-390

1
cpp/ql/src/experimental/Security/CWE/CWE-754/ImproperCheckReturnValueScanf.ql
View File

@@ -7,6 +7,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-754
* external/cwe/cwe-908
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-758/UndefinedOrImplementationDefinedBehavior.ql
View File

@@ -8,6 +8,7 @@
* @problem.severity warning
* @precision medium
* @tags security
* experimental
* external/cwe/cwe-758
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-783/OperatorPrecedenceLogicErrorWhenUseBitwiseOrLogicalOperations.ql
View File

@@ -8,6 +8,7 @@
* @precision medium
* @tags maintainability
* readability
* experimental
* external/cwe/cwe-783
* external/cwe/cwe-480
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-783/OperatorPrecedenceLogicErrorWhenUseBoolType.ql
View File

@@ -8,6 +8,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-783
* external/cwe/cwe-480
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-787/UnsignedToSignedPointerArith.ql
View File

@@ -6,6 +6,7 @@
* @problem.severity warning
* @tags reliability
* security
* experimental
* external/cwe/cwe-787
*/

1
cpp/ql/src/experimental/Security/CWE/CWE-788/AccessOfMemoryLocationAfterEndOfBufferUsingStrlen.ql
View File

@@ -8,6 +8,7 @@
* @precision medium
* @tags correctness
* security
* experimental
* external/cwe/cwe-788
*/

2
cpp/ql/src/qlpack.yml
View File

@@ -1,5 +1,5 @@
name: codeql/cpp-queries
version: 0.5.1-dev
version: 0.5.2-dev
groups:
- cpp
- queries

3
cpp/ql/test/library-tests/dataflow/dataflow-tests/dataflow-consistency.expected
View File

@@ -99,6 +99,9 @@ postWithInFlow
| test.cpp:526:3:526:4 | * ... [post update] | PostUpdateNode should not be the target of local flow. |
| test.cpp:526:4:526:4 | e [inner post update] | PostUpdateNode should not be the target of local flow. |
| test.cpp:531:40:531:40 | e [inner post update] | PostUpdateNode should not be the target of local flow. |
| test.cpp:537:5:537:6 | * ... [post update] | PostUpdateNode should not be the target of local flow. |
| test.cpp:537:6:537:6 | p [inner post update] | PostUpdateNode should not be the target of local flow. |
| test.cpp:542:23:542:23 | x [inner post update] | PostUpdateNode should not be the target of local flow. |
viableImplInCallContextTooLarge
uniqueParameterNodeAtPosition
uniqueParameterNodePosition

12
cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp
View File

@@ -530,4 +530,14 @@ void test_set_through_const_pointer(int *e)
{
set_through_const_pointer(source(), &e);
sink(*e); // $ ir MISSING: ast
}
}
void sink_then_source(int* p) {
sink(*p);
*p = source(); // $ SPURIOUS: ir=537:10 ir=541:9
}
void test_sink_then_source() {
int x;
sink_then_source(&x);
}

1
cpp/ql/test/library-tests/dataflow/dataflow-tests/uninitialized.expected
View File

@@ -37,3 +37,4 @@
| test.cpp:517:7:517:16 | stackArray | test.cpp:519:3:519:12 | stackArray |
| test.cpp:517:7:517:16 | stackArray | test.cpp:520:3:520:12 | stackArray |
| test.cpp:517:7:517:16 | stackArray | test.cpp:521:8:521:17 | stackArray |
| test.cpp:541:9:541:9 | x | test.cpp:542:23:542:23 | x |

57
cpp/ql/test/library-tests/ir/ir/PrintAST.expected
View File

@@ -207,34 +207,35 @@ bad_asts.cpp:
# 27| Type = [SpecifiedType] const Point
# 27| ValueCategory = lvalue
# 28| getStmt(1): [ReturnStmt] return ...
# 30| [TopLevelFunction] void Bad::errorExpr()
# 30| <params>:
# 30| getEntryPoint(): [BlockStmt] { ... }
# 31| getStmt(0): [DeclStmt] declaration
# 31| getDeclarationEntry(0): [VariableDeclarationEntry] definition of intref
# 31| Type = [LValueReferenceType] int &
# 31| getVariable().getInitializer(): [Initializer] initializer for intref
# 31| getExpr(): [ErrorExpr] <error expr>
# 31| Type = [ErroneousType] error
# 31| ValueCategory = prvalue
# 32| getStmt(1): [DeclStmt] declaration
# 32| getDeclarationEntry(0): [VariableDeclarationEntry] definition of x
# 32| Type = [IntType] int
# 32| getVariable().getInitializer(): [Initializer] initializer for x
# 32| getExpr(): [ErrorExpr] <error expr>
# 32| Type = [ErroneousType] error
# 32| ValueCategory = prvalue
# 33| getStmt(2): [ExprStmt] ExprStmt
# 33| getExpr(): [AssignExpr] ... = ...
# 33| Type = [IntType] int
# 33| ValueCategory = lvalue
# 33| getLValue(): [VariableAccess] x
# 33| Type = [IntType] int
# 33| ValueCategory = lvalue
# 33| getRValue(): [ErrorExpr] <error expr>
# 33| Type = [ErroneousType] error
# 33| ValueCategory = prvalue(load)
# 34| getStmt(3): [ReturnStmt] return ...
bad_stmts.cpp:
# 5| [TopLevelFunction] void Bad::errorExpr()
# 5| <params>:
# 5| getEntryPoint(): [BlockStmt] { ... }
# 6| getStmt(0): [DeclStmt] declaration
# 6| getDeclarationEntry(0): [VariableDeclarationEntry] definition of intref
# 6| Type = [LValueReferenceType] int &
# 6| getVariable().getInitializer(): [Initializer] initializer for intref
# 6| getExpr(): [ErrorExpr] <error expr>
# 6| Type = [ErroneousType] error
# 6| ValueCategory = prvalue
# 7| getStmt(1): [DeclStmt] declaration
# 7| getDeclarationEntry(0): [VariableDeclarationEntry] definition of x
# 7| Type = [IntType] int
# 7| getVariable().getInitializer(): [Initializer] initializer for x
# 7| getExpr(): [ErrorExpr] <error expr>
# 7| Type = [ErroneousType] error
# 7| ValueCategory = prvalue
# 8| getStmt(2): [ExprStmt] ExprStmt
# 8| getExpr(): [AssignExpr] ... = ...
# 8| Type = [IntType] int
# 8| ValueCategory = lvalue
# 8| getLValue(): [VariableAccess] x
# 8| Type = [IntType] int
# 8| ValueCategory = lvalue
# 8| getRValue(): [ErrorExpr] <error expr>
# 8| Type = [ErroneousType] error
# 8| ValueCategory = prvalue(load)
# 9| getStmt(3): [ReturnStmt] return ...
clang.cpp:
# 5| [TopLevelFunction] int* globalIntAddress()
# 5| <params>:

8
cpp/ql/test/library-tests/ir/ir/bad_asts.cpp
View File

@@ -1,4 +1,4 @@
// semmle-extractor-options: -std=c++17 --expect_errors
// semmle-extractor-options: -std=c++17
// Test cases that illustrate known bad ASTs that we have to work around in IR generation.
namespace Bad {
@@ -26,10 +26,4 @@ namespace Bad {
void CallCopyConstructor(const Point& a) {
Point b = a; // Copy constructor contains literal expressions with no values.
}
void errorExpr() {
int &intref = 0;
int x = 0[0];
x = 1[1];
}
}

10
cpp/ql/test/library-tests/ir/ir/bad_stmts.cpp Normal file
View File

@@ -0,0 +1,10 @@
// semmle-extractor-options: -std=c++17 --expect_errors
// Test cases that illustrate known bad ASTs that we have to work around in IR generation.
namespace Bad {
void errorExpr() {
int &intref = 0;
int x = 0[0];
x = 1[1];
}
}

22
cpp/ql/test/library-tests/ir/ir/operand_locations.expected
View File

@@ -98,17 +98,17 @@
| bad_asts.cpp:27:15:27:15 | StoreValue | r27_6 |
| bad_asts.cpp:27:15:27:15 | Unary | r27_3 |
| bad_asts.cpp:27:15:27:15 | Unary | r27_4 |
| bad_asts.cpp:30:8:30:16 | ChiPartial | partial:m30_3 |
| bad_asts.cpp:30:8:30:16 | ChiTotal | total:m30_2 |
| bad_asts.cpp:30:8:30:16 | SideEffect | m30_3 |
| bad_asts.cpp:31:10:31:15 | Address | &:r31_1 |
| bad_asts.cpp:31:18:31:19 | StoreValue | r31_2 |
| bad_asts.cpp:32:9:32:9 | Address | &:r32_1 |
| bad_asts.cpp:32:12:32:16 | StoreValue | r32_2 |
| bad_asts.cpp:33:5:33:5 | Address | &:r33_3 |
| bad_asts.cpp:33:5:33:12 | Address | &:r33_1 |
| bad_asts.cpp:33:5:33:12 | Load | ~m30_4 |
| bad_asts.cpp:33:5:33:12 | StoreValue | r33_2 |
| bad_stmts.cpp:5:8:5:16 | ChiPartial | partial:m5_3 |
| bad_stmts.cpp:5:8:5:16 | ChiTotal | total:m5_2 |
| bad_stmts.cpp:5:8:5:16 | SideEffect | m5_3 |
| bad_stmts.cpp:6:10:6:15 | Address | &:r6_1 |
| bad_stmts.cpp:6:18:6:19 | StoreValue | r6_2 |
| bad_stmts.cpp:7:9:7:9 | Address | &:r7_1 |
| bad_stmts.cpp:7:12:7:16 | StoreValue | r7_2 |
| bad_stmts.cpp:8:5:8:5 | Address | &:r8_3 |
| bad_stmts.cpp:8:5:8:12 | Address | &:r8_1 |
| bad_stmts.cpp:8:5:8:12 | Load | ~m5_4 |
| bad_stmts.cpp:8:5:8:12 | StoreValue | r8_2 |
| clang.cpp:5:6:5:21 | Address | &:r5_5 |
| clang.cpp:5:6:5:21 | ChiPartial | partial:m5_3 |
| clang.cpp:5:6:5:21 | ChiTotal | total:m5_2 |

39
cpp/ql/test/library-tests/ir/ir/raw_ir.expected
View File

@@ -120,25 +120,26 @@ bad_asts.cpp:
# 26| v26_10(void) = AliasedUse : ~m?
# 26| v26_11(void) = ExitFunction :
# 30| void Bad::errorExpr()
# 30| Block 0
# 30| v30_1(void) = EnterFunction :
# 30| mu30_2(unknown) = AliasedDefinition :
# 30| mu30_3(unknown) = InitializeNonLocal :
# 31| r31_1(glval<int &>) = VariableAddress[intref] :
# 31| r31_2(error) = Error :
# 31| mu31_3(int &) = Store[intref] : &:r31_1, r31_2
# 32| r32_1(glval<int>) = VariableAddress[x] :
# 32| r32_2(error) = Error :
# 32| mu32_3(int) = Store[x] : &:r32_1, r32_2
# 33| r33_1(glval<error>) = Error :
# 33| r33_2(error) = Load[?] : &:r33_1, ~m?
# 33| r33_3(glval<int>) = VariableAddress[x] :
# 33| mu33_4(int) = Store[x] : &:r33_3, r33_2
# 34| v34_1(void) = NoOp :
# 30| v30_4(void) = ReturnVoid :
# 30| v30_5(void) = AliasedUse : ~m?
# 30| v30_6(void) = ExitFunction :
bad_stmts.cpp:
# 5| void Bad::errorExpr()
# 5| Block 0
# 5| v5_1(void) = EnterFunction :
# 5| mu5_2(unknown) = AliasedDefinition :
# 5| mu5_3(unknown) = InitializeNonLocal :
# 6| r6_1(glval<int &>) = VariableAddress[intref] :
# 6| r6_2(error) = Error :
# 6| mu6_3(int &) = Store[intref] : &:r6_1, r6_2
# 7| r7_1(glval<int>) = VariableAddress[x] :
# 7| r7_2(error) = Error :
# 7| mu7_3(int) = Store[x] : &:r7_1, r7_2
# 8| r8_1(glval<error>) = Error :
# 8| r8_2(error) = Load[?] : &:r8_1, ~m?
# 8| r8_3(glval<int>) = VariableAddress[x] :
# 8| mu8_4(int) = Store[x] : &:r8_3, r8_2
# 9| v9_1(void) = NoOp :
# 5| v5_4(void) = ReturnVoid :
# 5| v5_5(void) = AliasedUse : ~m?
# 5| v5_6(void) = ExitFunction :
clang.cpp:
# 5| int* globalIntAddress()

9
cpp/ql/test/library-tests/ir/modulus-analysis/ModulusAnalysis.ql
View File

@@ -1,9 +1,16 @@
import cpp
import experimental.semmle.code.cpp.semantic.analysis.ModulusAnalysis
import experimental.semmle.code.cpp.semantic.Semantic
import experimental.semmle.code.cpp.semantic.analysis.RangeUtils
import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisSpecific
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis
import semmle.code.cpp.ir.IR as IR
import TestUtilities.InlineExpectationsTest
module ModulusAnalysisInstantiated =
ModulusAnalysis<FloatDelta, Bounds, RangeUtil<FloatDelta, CppLangImpl>>;
class ModulusAnalysisTest extends InlineExpectationsTest {
ModulusAnalysisTest() { this = "ModulusAnalysisTest" }
@@ -23,7 +30,7 @@ class ModulusAnalysisTest extends InlineExpectationsTest {
private string getAModString(SemExpr e) {
exists(SemBound b, int delta, int mod |
semExprModulus(e, b, delta, mod) and
ModulusAnalysisInstantiated::semExprModulus(e, b, delta, mod) and
result = b.toString() + "," + delta.toString() + "," + mod.toString() and
not (delta = 0 and mod = 0)
)

9
cpp/ql/test/library-tests/ir/sign-analysis/SignAnalysis.ql
View File

@@ -1,9 +1,14 @@
import cpp
import experimental.semmle.code.cpp.semantic.analysis.SignAnalysisCommon
import experimental.semmle.code.cpp.semantic.Semantic
import experimental.semmle.code.cpp.semantic.analysis.RangeUtils
import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisSpecific
import semmle.code.cpp.ir.IR as IR
import TestUtilities.InlineExpectationsTest
module SignAnalysisInstantiated = SignAnalysis<FloatDelta, RangeUtil<FloatDelta, CppLangImpl>>;
class SignAnalysisTest extends InlineExpectationsTest {
SignAnalysisTest() { this = "SignAnalysisTest" }
@@ -21,4 +26,6 @@ class SignAnalysisTest extends InlineExpectationsTest {
}
}
private string getASignString(SemExpr e) { result = strictconcat(semExprSign(e).toString(), "") }
private string getASignString(SemExpr e) {
result = strictconcat(SignAnalysisInstantiated::semExprSign(e).toString(), "")
}

8
cpp/ql/test/library-tests/syntax-zoo/allocators.cpp
View File

@@ -1,7 +1,7 @@
struct Foo
struct Allocators
{
Foo(int x, int y) : m_x(x), m_y(y) {}
~Foo() {m_x = m_y = 0;}
Allocators(int x, int y) : m_x(x), m_y(y) {}
~Allocators() {m_x = m_y = 0;}
// NB: In Microsoft mode, size_t is predeclared.
static void* operator new(size_t sz, int z, int w) { return nullptr; }
@@ -13,7 +13,7 @@ struct Foo
int main()
{
auto foo = new(11, 22) Foo(33, 44);
auto foo = new(11, 22) Allocators(33, 44);
delete foo;
}

6
cpp/ql/test/library-tests/syntax-zoo/array_delete.cpp
View File

@@ -1,7 +1,7 @@
struct Foo {
~Foo();
struct ArrayDelete {
~ArrayDelete();
};
void f() {
delete[] (Foo*)nullptr;
delete[] (ArrayDelete*)nullptr;
}

4
cpp/ql/test/library-tests/syntax-zoo/dataflow-consistency.expected
View File

@@ -74,8 +74,8 @@ argHasPostUpdate
| ir.cpp:625:5:625:5 | s | ArgumentNode is missing PostUpdateNode. |
postWithInFlow
| VacuousDestructorCall.cpp:10:22:10:22 | i [inner post update] | PostUpdateNode should not be the target of local flow. |
| allocators.cpp:4:11:4:13 | m_x [post update] | PostUpdateNode should not be the target of local flow. |
| allocators.cpp:4:17:4:19 | m_y [post update] | PostUpdateNode should not be the target of local flow. |
| allocators.cpp:4:18:4:20 | m_x [post update] | PostUpdateNode should not be the target of local flow. |
| allocators.cpp:4:24:4:26 | m_y [post update] | PostUpdateNode should not be the target of local flow. |
| assignexpr.cpp:9:4:9:4 | i [post update] | PostUpdateNode should not be the target of local flow. |
| builtin.c:34:23:34:31 | staticint [inner post update] | PostUpdateNode should not be the target of local flow. |
| builtin.c:39:37:39:45 | carry_out [inner post update] | PostUpdateNode should not be the target of local flow. |

30
cpp/ql/test/query-tests/Security/CWE/CWE-134/semmle/argv/argvLocal.c
View File

@@ -168,4 +168,34 @@ int main(int argc, char **argv) {
int i10 = (int) argv[1];
printf((char *) i10);
printWrapper((char *) i10);
// BAD: b value comes from argv
{
char b[64];
char *bp = &b[0];
char *t;
if (0) {
t = 0;
} else {
t = bp;
}
memcpy(t, argv[1] + 1, 1);
printf(bp);
printWrapper(bp);
}
// BAD: b value comes from argv
{
char b[64];
char *bp = &b[0];
char *t;
if (1) {
t = ++bp;
} else {
t = 0;
}
memcpy(t, argv[1] + 1, 1);
printf(bp);
printWrapper(bp);
}
}

44
cpp/ql/test/query-tests/Security/CWE/CWE-134/semmle/argv/argvLocal.expected
View File

@@ -147,6 +147,30 @@ edges
| argvLocal.c:168:18:168:21 | argv | argvLocal.c:170:24:170:26 | i10 |
| argvLocal.c:168:18:168:21 | argv | argvLocal.c:170:24:170:26 | i10 |
| argvLocal.c:168:18:168:21 | argv | argvLocal.c:170:24:170:26 | i10 |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:183:10:183:11 | (const char *)... |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:183:10:183:11 | (const char *)... |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:183:10:183:11 | bp |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:183:10:183:11 | bp |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:183:10:183:11 | bp indirection |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:183:10:183:11 | bp indirection |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:184:16:184:17 | bp |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:184:16:184:17 | bp |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:184:16:184:17 | bp |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:184:16:184:17 | bp |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:184:16:184:17 | bp indirection |
| argvLocal.c:182:13:182:16 | argv | argvLocal.c:184:16:184:17 | bp indirection |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:198:10:198:11 | (const char *)... |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:198:10:198:11 | (const char *)... |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:198:10:198:11 | bp |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:198:10:198:11 | bp |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:198:10:198:11 | bp indirection |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:198:10:198:11 | bp indirection |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:199:16:199:17 | bp |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:199:16:199:17 | bp |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:199:16:199:17 | bp |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:199:16:199:17 | bp |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:199:16:199:17 | bp indirection |
| argvLocal.c:197:13:197:16 | argv | argvLocal.c:199:16:199:17 | bp indirection |
subpaths
nodes
| argvLocal.c:95:9:95:12 | argv | semmle.label | argv |
@@ -239,6 +263,22 @@ nodes
| argvLocal.c:170:15:170:26 | i10 | semmle.label | i10 |
| argvLocal.c:170:24:170:26 | i10 | semmle.label | i10 |
| argvLocal.c:170:24:170:26 | i10 | semmle.label | i10 |
| argvLocal.c:182:13:182:16 | argv | semmle.label | argv |
| argvLocal.c:182:13:182:16 | argv | semmle.label | argv |
| argvLocal.c:183:10:183:11 | (const char *)... | semmle.label | (const char *)... |
| argvLocal.c:183:10:183:11 | bp | semmle.label | bp |
| argvLocal.c:183:10:183:11 | bp indirection | semmle.label | bp indirection |
| argvLocal.c:184:16:184:17 | bp | semmle.label | bp |
| argvLocal.c:184:16:184:17 | bp | semmle.label | bp |
| argvLocal.c:184:16:184:17 | bp indirection | semmle.label | bp indirection |
| argvLocal.c:197:13:197:16 | argv | semmle.label | argv |
| argvLocal.c:197:13:197:16 | argv | semmle.label | argv |
| argvLocal.c:198:10:198:11 | (const char *)... | semmle.label | (const char *)... |
| argvLocal.c:198:10:198:11 | bp | semmle.label | bp |
| argvLocal.c:198:10:198:11 | bp indirection | semmle.label | bp indirection |
| argvLocal.c:199:16:199:17 | bp | semmle.label | bp |
| argvLocal.c:199:16:199:17 | bp | semmle.label | bp |
| argvLocal.c:199:16:199:17 | bp indirection | semmle.label | bp indirection |
#select
| argvLocal.c:95:9:95:15 | access to array | argvLocal.c:95:9:95:12 | argv | argvLocal.c:95:9:95:15 | access to array | The value of this argument may come from $@ and is being used as a formatting argument to printf(format). | argvLocal.c:95:9:95:12 | argv | argv |
| argvLocal.c:96:15:96:21 | access to array | argvLocal.c:96:15:96:18 | argv | argvLocal.c:96:15:96:21 | access to array | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format). | argvLocal.c:96:15:96:18 | argv | argv |
@@ -266,3 +306,7 @@ nodes
| argvLocal.c:151:15:151:16 | i8 | argvLocal.c:149:11:149:14 | argv | argvLocal.c:151:15:151:16 | i8 | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format). | argvLocal.c:149:11:149:14 | argv | argv |
| argvLocal.c:169:18:169:20 | i10 | argvLocal.c:168:18:168:21 | argv | argvLocal.c:169:18:169:20 | i10 | The value of this argument may come from $@ and is being used as a formatting argument to printf(format). | argvLocal.c:168:18:168:21 | argv | argv |
| argvLocal.c:170:24:170:26 | i10 | argvLocal.c:168:18:168:21 | argv | argvLocal.c:170:24:170:26 | i10 | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format). | argvLocal.c:168:18:168:21 | argv | argv |
| argvLocal.c:183:10:183:11 | bp | argvLocal.c:182:13:182:16 | argv | argvLocal.c:183:10:183:11 | bp | The value of this argument may come from $@ and is being used as a formatting argument to printf(format). | argvLocal.c:182:13:182:16 | argv | argv |
| argvLocal.c:184:16:184:17 | bp | argvLocal.c:182:13:182:16 | argv | argvLocal.c:184:16:184:17 | bp | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format). | argvLocal.c:182:13:182:16 | argv | argv |
| argvLocal.c:198:10:198:11 | bp | argvLocal.c:197:13:197:16 | argv | argvLocal.c:198:10:198:11 | bp | The value of this argument may come from $@ and is being used as a formatting argument to printf(format). | argvLocal.c:197:13:197:16 | argv | argv |
| argvLocal.c:199:16:199:17 | bp | argvLocal.c:197:13:197:16 | argv | argvLocal.c:199:16:199:17 | bp | The value of this argument may come from $@ and is being used as a formatting argument to printWrapper(correct), which calls printf(format). | argvLocal.c:197:13:197:16 | argv | argv |

23
cpp/ql/test/query-tests/Security/CWE/CWE-290/semmle/AuthenticationBypass/AuthenticationBypass.expected
View File

@@ -11,6 +11,18 @@ edges
| test.cpp:38:25:38:30 | call to getenv | test.cpp:42:14:42:20 | address |
| test.cpp:38:25:38:42 | call to getenv | test.cpp:42:14:42:20 | address |
| test.cpp:38:25:38:42 | call to getenv | test.cpp:42:14:42:20 | address |
| test.cpp:49:25:49:30 | call to getenv | test.cpp:52:14:52:20 | address |
| test.cpp:49:25:49:30 | call to getenv | test.cpp:52:14:52:20 | address |
| test.cpp:49:25:49:30 | call to getenv | test.cpp:56:14:56:20 | address |
| test.cpp:49:25:49:30 | call to getenv | test.cpp:56:14:56:20 | address |
| test.cpp:49:25:49:30 | call to getenv | test.cpp:60:14:60:20 | address |
| test.cpp:49:25:49:30 | call to getenv | test.cpp:60:14:60:20 | address |
| test.cpp:49:25:49:42 | call to getenv | test.cpp:52:14:52:20 | address |
| test.cpp:49:25:49:42 | call to getenv | test.cpp:52:14:52:20 | address |
| test.cpp:49:25:49:42 | call to getenv | test.cpp:56:14:56:20 | address |
| test.cpp:49:25:49:42 | call to getenv | test.cpp:56:14:56:20 | address |
| test.cpp:49:25:49:42 | call to getenv | test.cpp:60:14:60:20 | address |
| test.cpp:49:25:49:42 | call to getenv | test.cpp:60:14:60:20 | address |
subpaths
nodes
| test.cpp:16:25:16:30 | call to getenv | semmle.label | call to getenv |
@@ -25,7 +37,18 @@ nodes
| test.cpp:38:25:38:42 | call to getenv | semmle.label | call to getenv |
| test.cpp:42:14:42:20 | address | semmle.label | address |
| test.cpp:42:14:42:20 | address | semmle.label | address |
| test.cpp:49:25:49:30 | call to getenv | semmle.label | call to getenv |
| test.cpp:49:25:49:42 | call to getenv | semmle.label | call to getenv |
| test.cpp:52:14:52:20 | address | semmle.label | address |
| test.cpp:52:14:52:20 | address | semmle.label | address |
| test.cpp:56:14:56:20 | address | semmle.label | address |
| test.cpp:56:14:56:20 | address | semmle.label | address |
| test.cpp:60:14:60:20 | address | semmle.label | address |
| test.cpp:60:14:60:20 | address | semmle.label | address |
#select
| test.cpp:20:7:20:12 | call to strcmp | test.cpp:16:25:16:30 | call to getenv | test.cpp:20:14:20:20 | address | Untrusted input $@ might be vulnerable to a spoofing attack. | test.cpp:16:25:16:30 | call to getenv | call to getenv |
| test.cpp:31:7:31:12 | call to strcmp | test.cpp:27:25:27:30 | call to getenv | test.cpp:31:14:31:20 | address | Untrusted input $@ might be vulnerable to a spoofing attack. | test.cpp:27:25:27:30 | call to getenv | call to getenv |
| test.cpp:42:7:42:12 | call to strcmp | test.cpp:38:25:38:30 | call to getenv | test.cpp:42:14:42:20 | address | Untrusted input $@ might be vulnerable to a spoofing attack. | test.cpp:38:25:38:30 | call to getenv | call to getenv |
| test.cpp:52:7:52:12 | call to strcmp | test.cpp:49:25:49:30 | call to getenv | test.cpp:52:14:52:20 | address | Untrusted input $@ might be vulnerable to a spoofing attack. | test.cpp:49:25:49:30 | call to getenv | call to getenv |
| test.cpp:56:7:56:12 | call to strcmp | test.cpp:49:25:49:30 | call to getenv | test.cpp:56:14:56:20 | address | Untrusted input $@ might be vulnerable to a spoofing attack. | test.cpp:49:25:49:30 | call to getenv | call to getenv |
| test.cpp:60:7:60:12 | call to strcmp | test.cpp:49:25:49:30 | call to getenv | test.cpp:60:14:60:20 | address | Untrusted input $@ might be vulnerable to a spoofing attack. | test.cpp:49:25:49:30 | call to getenv | call to getenv |

24
cpp/ql/test/query-tests/Security/CWE/CWE-290/semmle/AuthenticationBypass/test.cpp
View File

@@ -43,3 +43,27 @@ void processRequest3()
isServer = 1;
}
}
void processRequest4()
{
const char *address = getenv("SERVERIP");
bool cond = false;
if (strcmp(address, "127.0.0.1")) { cond = true; } // BAD
if (strcmp(address, "127_0_0_1")) { cond = true; } // GOOD (not an IP)
if (strcmp(address, "127.0.0")) { cond = true; } // GOOD (not an IP)
if (strcmp(address, "127.0.0.0.1")) { cond = true; } // GOOD (not an IP)
if (strcmp(address, "http://mycompany")) { cond = true; } // BAD
if (strcmp(address, "http_//mycompany")) { cond = true; } // GOOD (not an address)
if (strcmp(address, "htt://mycompany")) { cond = true; } // GOOD (not an address)
if (strcmp(address, "httpp://mycompany")) { cond = true; } // GOOD (not an address)
if (strcmp(address, "mycompany.com")) { cond = true; } // BAD
if (strcmp(address, "mycompany_com")) { cond = true; } // GOOD (not an address)
if (strcmp(address, "mycompany.c")) { cond = true; } // GOOD (not an address)
if (strcmp(address, "mycompany.comm")) { cond = true; } // GOOD (not an address)
if (cond) {
isServer = 1;
}
}

2069
csharp/downgrades/1136957c0b3c73a7798ae42645c361e813295393/old.dbscheme Normal file
View File

File diff suppressed because it is too large Load Diff

2069
csharp/downgrades/1136957c0b3c73a7798ae42645c361e813295393/semmlecode.csharp.dbscheme Normal file
View File

File diff suppressed because it is too large Load Diff

2
csharp/downgrades/1136957c0b3c73a7798ae42645c361e813295393/upgrade.properties Normal file
View File

@@ -0,0 +1,2 @@
description: Remove operators from the virtualizable type.
compatibility: full

13
csharp/downgrades/d0fba103f7dee477dd7d9f6c038518b3f683b2c7/expressions.ql Normal file
View File

@@ -0,0 +1,13 @@
class Expression extends @expr {
string toString() { none() }
}
class TypeOrRef extends @type_or_ref {
string toString() { none() }
}
from Expression e, int k, int kind, TypeOrRef t
where
expressions(e, k, t) and
if k = [133, 134] then kind = 106 else kind = k
select e, kind, t

2069
csharp/downgrades/d0fba103f7dee477dd7d9f6c038518b3f683b2c7/old.dbscheme Normal file
View File

File diff suppressed because it is too large Load Diff

2067
csharp/downgrades/d0fba103f7dee477dd7d9f6c038518b3f683b2c7/semmlecode.csharp.dbscheme Normal file
View File

File diff suppressed because it is too large Load Diff

3
csharp/downgrades/d0fba103f7dee477dd7d9f6c038518b3f683b2c7/upgrade.properties Normal file
View File

@@ -0,0 +1,3 @@
description: Remove unsigned right shift and unsigned right shift assignment expression kinds.
compatibility: backwards
expressions.rel: run expressions.qlo

6
csharp/extractor/Semmle.Extraction.CIL/Entities/DefinitionMethod.cs
View File

@@ -92,7 +92,8 @@ namespace Semmle.Extraction.CIL.Entities
yield return Tuples.cil_parameter_out(pe);
if (p.Attributes.HasFlag(ParameterAttributes.In))
yield return Tuples.cil_parameter_in(pe);
Attribute.Populate(Context, pe, p.GetCustomAttributes());
foreach (var c in Attribute.Populate(Context, pe, p.GetCustomAttributes()))
yield return c;
}
yield return Tuples.metadata_handle(this, Context.Assembly, MetadataTokens.GetToken(handle));
@@ -205,7 +206,8 @@ namespace Semmle.Extraction.CIL.Entities
yield return Tuples.cil_newslot(this);
// Populate attributes
Attribute.Populate(Context, this, md.GetCustomAttributes());
foreach (var c in Attribute.Populate(Context, this, md.GetCustomAttributes()))
yield return c;
}
}

Some files were not shown because too many files have changed in this diff Show More