mirror of
https://github.com/github/codeql.git
synced 2025-12-23 20:26:32 +01:00
Merge branch 'main' into rdmarsh2/range-analysis-overflow
This commit is contained in:
1
.github/workflows/check-change-note.yml
vendored
1
.github/workflows/check-change-note.yml
vendored
@@ -8,6 +8,7 @@ on:
|
|||||||
- "*/ql/src/**/*.qll"
|
- "*/ql/src/**/*.qll"
|
||||||
- "*/ql/lib/**/*.ql"
|
- "*/ql/lib/**/*.ql"
|
||||||
- "*/ql/lib/**/*.qll"
|
- "*/ql/lib/**/*.qll"
|
||||||
|
- "*/ql/lib/**/*.yml"
|
||||||
- "!**/experimental/**"
|
- "!**/experimental/**"
|
||||||
- "!ql/**"
|
- "!ql/**"
|
||||||
- "!swift/**"
|
- "!swift/**"
|
||||||
|
|||||||
2
.github/workflows/close-stale.yml
vendored
2
.github/workflows/close-stale.yml
vendored
@@ -12,7 +12,7 @@ jobs:
|
|||||||
runs-on: ubuntu-latest
|
runs-on: ubuntu-latest
|
||||||
|
|
||||||
steps:
|
steps:
|
||||||
- uses: actions/stale@v7
|
- uses: actions/stale@v8
|
||||||
with:
|
with:
|
||||||
repo-token: ${{ secrets.GITHUB_TOKEN }}
|
repo-token: ${{ secrets.GITHUB_TOKEN }}
|
||||||
stale-issue-message: 'This issue is stale because it has been open 14 days with no activity. Comment or remove the `Stale` label in order to avoid having this issue closed in 7 days.'
|
stale-issue-message: 'This issue is stale because it has been open 14 days with no activity. Comment or remove the `Stale` label in order to avoid having this issue closed in 7 days.'
|
||||||
|
|||||||
68
.github/workflows/ruby-build.yml
vendored
68
.github/workflows/ruby-build.yml
vendored
@@ -48,6 +48,9 @@ jobs:
|
|||||||
run: |
|
run: |
|
||||||
brew install gnu-tar
|
brew install gnu-tar
|
||||||
echo "/usr/local/opt/gnu-tar/libexec/gnubin" >> $GITHUB_PATH
|
echo "/usr/local/opt/gnu-tar/libexec/gnubin" >> $GITHUB_PATH
|
||||||
|
- name: Install cargo-cross
|
||||||
|
if: runner.os == 'Linux'
|
||||||
|
run: cargo install cross --version 0.2.5
|
||||||
- uses: ./.github/actions/os-version
|
- uses: ./.github/actions/os-version
|
||||||
id: os_version
|
id: os_version
|
||||||
- name: Cache entire extractor
|
- name: Cache entire extractor
|
||||||
@@ -78,8 +81,18 @@ jobs:
|
|||||||
- name: Run tests
|
- name: Run tests
|
||||||
if: steps.cache-extractor.outputs.cache-hit != 'true'
|
if: steps.cache-extractor.outputs.cache-hit != 'true'
|
||||||
run: cd extractor && cargo test --verbose
|
run: cd extractor && cargo test --verbose
|
||||||
- name: Release build
|
# On linux, build the extractor via cross in a centos7 container.
|
||||||
if: steps.cache-extractor.outputs.cache-hit != 'true'
|
# This ensures we don't depend on glibc > 2.17.
|
||||||
|
- name: Release build (linux)
|
||||||
|
if: steps.cache-extractor.outputs.cache-hit != 'true' && runner.os == 'Linux'
|
||||||
|
run: |
|
||||||
|
cd extractor
|
||||||
|
cross build --release
|
||||||
|
mv target/x86_64-unknown-linux-gnu/release/extractor target/release/
|
||||||
|
mv target/x86_64-unknown-linux-gnu/release/autobuilder target/release/
|
||||||
|
mv target/x86_64-unknown-linux-gnu/release/generator target/release/
|
||||||
|
- name: Release build (windows and macos)
|
||||||
|
if: steps.cache-extractor.outputs.cache-hit != 'true' && runner.os != 'Linux'
|
||||||
run: cd extractor && cargo build --release
|
run: cd extractor && cargo build --release
|
||||||
- name: Generate dbscheme
|
- name: Generate dbscheme
|
||||||
if: ${{ matrix.os == 'ubuntu-latest' && steps.cache-extractor.outputs.cache-hit != 'true'}}
|
if: ${{ matrix.os == 'ubuntu-latest' && steps.cache-extractor.outputs.cache-hit != 'true'}}
|
||||||
@@ -227,3 +240,54 @@ jobs:
|
|||||||
shell: bash
|
shell: bash
|
||||||
run: |
|
run: |
|
||||||
codeql database analyze --search-path "${{ runner.temp }}/ruby-bundle" --format=sarifv2.1.0 --output=out.sarif ../database ruby-code-scanning.qls
|
codeql database analyze --search-path "${{ runner.temp }}/ruby-bundle" --format=sarifv2.1.0 --output=out.sarif ../database ruby-code-scanning.qls
|
||||||
|
|
||||||
|
# This is a copy of the 'test' job that runs in a centos7 container.
|
||||||
|
# This tests that the extractor works correctly on systems with an old glibc.
|
||||||
|
test-centos7:
|
||||||
|
defaults:
|
||||||
|
run:
|
||||||
|
working-directory: ${{ github.workspace }}
|
||||||
|
strategy:
|
||||||
|
fail-fast: false
|
||||||
|
runs-on: ubuntu-latest
|
||||||
|
container:
|
||||||
|
image: centos:centos7
|
||||||
|
env:
|
||||||
|
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
|
||||||
|
needs: [package]
|
||||||
|
steps:
|
||||||
|
- name: Install gh cli
|
||||||
|
run: |
|
||||||
|
yum-config-manager --add-repo https://cli.github.com/packages/rpm/gh-cli.repo
|
||||||
|
# fetch-codeql requires unzip and jq
|
||||||
|
# jq is available in epel-release (https://docs.fedoraproject.org/en-US/epel/)
|
||||||
|
yum install -y gh unzip epel-release
|
||||||
|
yum install -y jq
|
||||||
|
- uses: actions/checkout@v3
|
||||||
|
- name: Fetch CodeQL
|
||||||
|
uses: ./.github/actions/fetch-codeql
|
||||||
|
|
||||||
|
# Due to a bug in Actions, we can't use runner.temp in the run blocks here.
|
||||||
|
# https://github.com/actions/runner/issues/2185
|
||||||
|
|
||||||
|
- name: Download Ruby bundle
|
||||||
|
uses: actions/download-artifact@v3
|
||||||
|
with:
|
||||||
|
name: codeql-ruby-bundle
|
||||||
|
path: ${{ runner.temp }}
|
||||||
|
- name: Unzip Ruby bundle
|
||||||
|
shell: bash
|
||||||
|
run: unzip -q -d "$RUNNER_TEMP"/ruby-bundle "$RUNNER_TEMP"/codeql-ruby-bundle.zip
|
||||||
|
|
||||||
|
- name: Run QL test
|
||||||
|
shell: bash
|
||||||
|
run: |
|
||||||
|
codeql test run --search-path "$RUNNER_TEMP"/ruby-bundle --additional-packs "$RUNNER_TEMP"/ruby-bundle ruby/ql/test/library-tests/ast/constants/
|
||||||
|
- name: Create database
|
||||||
|
shell: bash
|
||||||
|
run: |
|
||||||
|
codeql database create --search-path "$RUNNER_TEMP"/ruby-bundle --language ruby --source-root ruby/ql/test/library-tests/ast/constants/ ../database
|
||||||
|
- name: Analyze database
|
||||||
|
shell: bash
|
||||||
|
run: |
|
||||||
|
codeql database analyze --search-path "$RUNNER_TEMP"/ruby-bundle --format=sarifv2.1.0 --output=out.sarif ../database ruby-code-scanning.qls
|
||||||
|
|||||||
1
.github/workflows/ruby-qltest.yml
vendored
1
.github/workflows/ruby-qltest.yml
vendored
@@ -4,6 +4,7 @@ on:
|
|||||||
push:
|
push:
|
||||||
paths:
|
paths:
|
||||||
- "ruby/**"
|
- "ruby/**"
|
||||||
|
- "shared/**"
|
||||||
- .github/workflows/ruby-build.yml
|
- .github/workflows/ruby-build.yml
|
||||||
- .github/actions/fetch-codeql/action.yml
|
- .github/actions/fetch-codeql/action.yml
|
||||||
- codeql-workspace.yml
|
- codeql-workspace.yml
|
||||||
|
|||||||
@@ -1,4 +1,4 @@
|
|||||||
---
|
---
|
||||||
category: deprecated
|
category: deprecated
|
||||||
---
|
---
|
||||||
* The `SslContextCallAbstractConfig`, `SslContextCallConfig`, `SslContextCallBannedProtocolConfig`, `SslContextCallTls12ProtocolConfig`, `SslContextCallTls13ProtocolConfig`, `SslContextCallTlsProtocolConfig`, `SslContextFlowsToSetOptionConfig`, `SslOptionConfig` dataflow configurations from `BoostorgAsio` have been deprecated. Please use `SslContextCallConfigSig`, `SslContextCallMake`, `SslContextCallFlow`, `SslContextCallBannedProtocolFlow`, `SslContextCallTls12ProtocolFlow`, `SslContextCallTls13ProtocolFlow`, `SslContextCallTlsProtocolFlow`, `SslContextFlowsToSetOptionFlow`.
|
* The `SslContextCallAbstractConfig`, `SslContextCallConfig`, `SslContextCallBannedProtocolConfig`, `SslContextCallTls12ProtocolConfig`, `SslContextCallTls13ProtocolConfig`, `SslContextCallTlsProtocolConfig`, `SslContextFlowsToSetOptionConfig`, `SslOptionConfig` dataflow configurations from `BoostorgAsio` have been deprecated. Please use `SslContextCallConfigSig`, `SslContextCallGlobal`, `SslContextCallFlow`, `SslContextCallBannedProtocolFlow`, `SslContextCallTls12ProtocolFlow`, `SslContextCallTls13ProtocolFlow`, `SslContextCallTlsProtocolFlow`, `SslContextFlowsToSetOptionFlow`.
|
||||||
|
|||||||
6
cpp/ql/lib/change-notes/2023-03-23-dataflow-renaming.md
Normal file
6
cpp/ql/lib/change-notes/2023-03-23-dataflow-renaming.md
Normal file
@@ -0,0 +1,6 @@
|
|||||||
|
---
|
||||||
|
category: deprecated
|
||||||
|
---
|
||||||
|
* The recently introduced new data flow and taint tracking APIs have had a
|
||||||
|
number of module and predicate renamings. The old APIs remain in place for
|
||||||
|
now.
|
||||||
@@ -0,0 +1,4 @@
|
|||||||
|
---
|
||||||
|
category: fix
|
||||||
|
---
|
||||||
|
* Fixed some accidental predicate visibility in the backwards-compatible wrapper for data flow configurations. In particular `DataFlow::hasFlowPath`, `DataFlow::hasFlow`, `DataFlow::hasFlowTo`, and `DataFlow::hasFlowToExpr` were accidentally exposed in a single version.
|
||||||
4
cpp/ql/lib/change-notes/2023-03-30-bufferaccess.md
Normal file
4
cpp/ql/lib/change-notes/2023-03-30-bufferaccess.md
Normal file
@@ -0,0 +1,4 @@
|
|||||||
|
---
|
||||||
|
category: feature
|
||||||
|
---
|
||||||
|
* Added overridable predicates `getSizeExpr` and `getSizeMult` to the `BufferAccess` class (`semmle.code.cpp.security.BufferAccess.qll`). This makes it possible to model a larger class of buffer reads and writes using the library.
|
||||||
@@ -3,3 +3,4 @@ import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
|
|||||||
// Import each extension we want to enable
|
// Import each extension we want to enable
|
||||||
import extensions.SubtractSelf
|
import extensions.SubtractSelf
|
||||||
import extensions.ConstantBitwiseAndExprRange
|
import extensions.ConstantBitwiseAndExprRange
|
||||||
|
import extensions.StrlenLiteralRangeExpr
|
||||||
|
|||||||
@@ -0,0 +1,18 @@
|
|||||||
|
private import cpp
|
||||||
|
private import experimental.semmle.code.cpp.models.interfaces.SimpleRangeAnalysisExpr
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Provides range analysis information for calls to `strlen` on literal strings.
|
||||||
|
* For example, the range of `strlen("literal")` will be 7.
|
||||||
|
*/
|
||||||
|
class StrlenLiteralRangeExpr extends SimpleRangeAnalysisExpr, FunctionCall {
|
||||||
|
StrlenLiteralRangeExpr() {
|
||||||
|
getTarget().hasGlobalOrStdName("strlen") and getArgument(0).isConstant()
|
||||||
|
}
|
||||||
|
|
||||||
|
override int getLowerBounds() { result = getArgument(0).getValue().length() }
|
||||||
|
|
||||||
|
override int getUpperBounds() { result = getArgument(0).getValue().length() }
|
||||||
|
|
||||||
|
override predicate dependsOnChild(Expr e) { none() }
|
||||||
|
}
|
||||||
@@ -54,7 +54,7 @@ module PrivateCleartextWrite {
|
|||||||
predicate isBarrier(DataFlow::Node node) { node instanceof Sanitizer }
|
predicate isBarrier(DataFlow::Node node) { node instanceof Sanitizer }
|
||||||
}
|
}
|
||||||
|
|
||||||
module WriteFlow = TaintTracking::Make<WriteConfig>;
|
module WriteFlow = TaintTracking::Global<WriteConfig>;
|
||||||
|
|
||||||
class PrivateDataSource extends Source {
|
class PrivateDataSource extends Source {
|
||||||
PrivateDataSource() { this.getExpr() instanceof PrivateDataExpr }
|
PrivateDataSource() { this.getExpr() instanceof PrivateDataExpr }
|
||||||
|
|||||||
@@ -12,12 +12,92 @@ private import semmle.code.cpp.ir.ValueNumbering
|
|||||||
module SemanticExprConfig {
|
module SemanticExprConfig {
|
||||||
class Location = Cpp::Location;
|
class Location = Cpp::Location;
|
||||||
|
|
||||||
class Expr = IR::Instruction;
|
/** A `ConvertInstruction` or a `CopyValueInstruction`. */
|
||||||
|
private class Conversion extends IR::UnaryInstruction {
|
||||||
|
Conversion() {
|
||||||
|
this instanceof IR::CopyValueInstruction
|
||||||
|
or
|
||||||
|
this instanceof IR::ConvertInstruction
|
||||||
|
}
|
||||||
|
|
||||||
|
/** Holds if this instruction converts a value of type `tFrom` to a value of type `tTo`. */
|
||||||
|
predicate converts(SemType tFrom, SemType tTo) {
|
||||||
|
tFrom = getSemanticType(this.getUnary().getResultIRType()) and
|
||||||
|
tTo = getSemanticType(this.getResultIRType())
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Gets a conversion-like instruction that consumes `op`, and
|
||||||
|
* which is guaranteed to not overflow.
|
||||||
|
*/
|
||||||
|
private IR::Instruction safeConversion(IR::Operand op) {
|
||||||
|
exists(Conversion conv, SemType tFrom, SemType tTo |
|
||||||
|
conv.converts(tFrom, tTo) and
|
||||||
|
conversionCannotOverflow(tFrom, tTo) and
|
||||||
|
conv.getUnaryOperand() = op and
|
||||||
|
result = conv
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
/** Holds if `i1 = i2` or if `i2` is a safe conversion that consumes `i1`. */
|
||||||
|
private predicate idOrSafeConversion(IR::Instruction i1, IR::Instruction i2) {
|
||||||
|
not i1.getResultIRType() instanceof IR::IRVoidType and
|
||||||
|
(
|
||||||
|
i1 = i2
|
||||||
|
or
|
||||||
|
i2 = safeConversion(i1.getAUse()) and
|
||||||
|
i1.getBlock() = i2.getBlock()
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
module Equiv = QlBuiltins::EquivalenceRelation<IR::Instruction, idOrSafeConversion/2>;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* The expressions on which we perform range analysis.
|
||||||
|
*/
|
||||||
|
class Expr extends Equiv::EquivalenceClass {
|
||||||
|
/** Gets the n'th instruction in this equivalence class. */
|
||||||
|
private IR::Instruction getInstruction(int n) {
|
||||||
|
result =
|
||||||
|
rank[n + 1](IR::Instruction instr, int i, IR::IRBlock block |
|
||||||
|
this = Equiv::getEquivalenceClass(instr) and block.getInstruction(i) = instr
|
||||||
|
|
|
||||||
|
instr order by i
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
/** Gets a textual representation of this element. */
|
||||||
|
string toString() { result = this.getUnconverted().toString() }
|
||||||
|
|
||||||
|
/** Gets the basic block of this expression. */
|
||||||
|
IR::IRBlock getBlock() { result = this.getUnconverted().getBlock() }
|
||||||
|
|
||||||
|
/** Gets the unconverted instruction associated with this expression. */
|
||||||
|
IR::Instruction getUnconverted() { result = this.getInstruction(0) }
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Gets the final instruction associated with this expression. This
|
||||||
|
* represents the result after applying all the safe conversions.
|
||||||
|
*/
|
||||||
|
IR::Instruction getConverted() {
|
||||||
|
exists(int n |
|
||||||
|
result = this.getInstruction(n) and
|
||||||
|
not exists(this.getInstruction(n + 1))
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
/** Gets the type of the result produced by this instruction. */
|
||||||
|
IR::IRType getResultIRType() { result = this.getConverted().getResultIRType() }
|
||||||
|
|
||||||
|
/** Gets the location of the source code for this expression. */
|
||||||
|
Location getLocation() { result = this.getUnconverted().getLocation() }
|
||||||
|
}
|
||||||
|
|
||||||
SemBasicBlock getExprBasicBlock(Expr e) { result = getSemanticBasicBlock(e.getBlock()) }
|
SemBasicBlock getExprBasicBlock(Expr e) { result = getSemanticBasicBlock(e.getBlock()) }
|
||||||
|
|
||||||
private predicate anyConstantExpr(Expr expr, SemType type, string value) {
|
private predicate anyConstantExpr(Expr expr, SemType type, string value) {
|
||||||
exists(IR::ConstantInstruction instr | instr = expr |
|
exists(IR::ConstantInstruction instr | getSemanticExpr(instr) = expr |
|
||||||
type = getSemanticType(instr.getResultIRType()) and
|
type = getSemanticType(instr.getResultIRType()) and
|
||||||
value = instr.getValue()
|
value = instr.getValue()
|
||||||
)
|
)
|
||||||
@@ -58,41 +138,46 @@ module SemanticExprConfig {
|
|||||||
predicate nullLiteral(Expr expr, SemAddressType type) { anyConstantExpr(expr, type, _) }
|
predicate nullLiteral(Expr expr, SemAddressType type) { anyConstantExpr(expr, type, _) }
|
||||||
|
|
||||||
predicate stringLiteral(Expr expr, SemType type, string value) {
|
predicate stringLiteral(Expr expr, SemType type, string value) {
|
||||||
anyConstantExpr(expr, type, value) and expr instanceof IR::StringConstantInstruction
|
anyConstantExpr(expr, type, value) and
|
||||||
|
expr.getUnconverted() instanceof IR::StringConstantInstruction
|
||||||
}
|
}
|
||||||
|
|
||||||
predicate binaryExpr(Expr expr, Opcode opcode, SemType type, Expr leftOperand, Expr rightOperand) {
|
predicate binaryExpr(Expr expr, Opcode opcode, SemType type, Expr leftOperand, Expr rightOperand) {
|
||||||
exists(IR::BinaryInstruction instr | instr = expr |
|
exists(IR::BinaryInstruction instr |
|
||||||
|
instr = expr.getUnconverted() and
|
||||||
type = getSemanticType(instr.getResultIRType()) and
|
type = getSemanticType(instr.getResultIRType()) and
|
||||||
leftOperand = instr.getLeft() and
|
leftOperand = getSemanticExpr(instr.getLeft()) and
|
||||||
rightOperand = instr.getRight() and
|
rightOperand = getSemanticExpr(instr.getRight()) and
|
||||||
// REVIEW: Merge the two `Opcode` types.
|
// REVIEW: Merge the two `Opcode` types.
|
||||||
opcode.toString() = instr.getOpcode().toString()
|
opcode.toString() = instr.getOpcode().toString()
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
predicate unaryExpr(Expr expr, Opcode opcode, SemType type, Expr operand) {
|
predicate unaryExpr(Expr expr, Opcode opcode, SemType type, Expr operand) {
|
||||||
type = getSemanticType(expr.getResultIRType()) and
|
exists(IR::UnaryInstruction instr | instr = expr.getUnconverted() |
|
||||||
(
|
type = getSemanticType(instr.getResultIRType()) and
|
||||||
exists(IR::UnaryInstruction instr | instr = expr |
|
operand = getSemanticExpr(instr.getUnary()) and
|
||||||
operand = instr.getUnary() and
|
// REVIEW: Merge the two operand types.
|
||||||
// REVIEW: Merge the two operand types.
|
opcode.toString() = instr.getOpcode().toString()
|
||||||
opcode.toString() = instr.getOpcode().toString()
|
)
|
||||||
)
|
or
|
||||||
or
|
exists(IR::StoreInstruction instr | instr = expr.getUnconverted() |
|
||||||
exists(IR::StoreInstruction instr | instr = expr |
|
type = getSemanticType(instr.getResultIRType()) and
|
||||||
operand = instr.getSourceValue() and
|
operand = getSemanticExpr(instr.getSourceValue()) and
|
||||||
opcode instanceof Opcode::Store
|
opcode instanceof Opcode::Store
|
||||||
)
|
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
predicate nullaryExpr(Expr expr, Opcode opcode, SemType type) {
|
predicate nullaryExpr(Expr expr, Opcode opcode, SemType type) {
|
||||||
type = getSemanticType(expr.getResultIRType()) and
|
exists(IR::LoadInstruction load |
|
||||||
(
|
load = expr.getUnconverted() and
|
||||||
expr instanceof IR::LoadInstruction and opcode instanceof Opcode::Load
|
type = getSemanticType(load.getResultIRType()) and
|
||||||
or
|
opcode instanceof Opcode::Load
|
||||||
expr instanceof IR::InitializeParameterInstruction and
|
)
|
||||||
|
or
|
||||||
|
exists(IR::InitializeParameterInstruction init |
|
||||||
|
init = expr.getUnconverted() and
|
||||||
|
type = getSemanticType(init.getResultIRType()) and
|
||||||
opcode instanceof Opcode::InitializeParameter
|
opcode instanceof Opcode::InitializeParameter
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
@@ -122,8 +207,10 @@ module SemanticExprConfig {
|
|||||||
newtype TSsaVariable =
|
newtype TSsaVariable =
|
||||||
TSsaInstruction(IR::Instruction instr) { instr.hasMemoryResult() } or
|
TSsaInstruction(IR::Instruction instr) { instr.hasMemoryResult() } or
|
||||||
TSsaOperand(IR::Operand op) { op.isDefinitionInexact() } or
|
TSsaOperand(IR::Operand op) { op.isDefinitionInexact() } or
|
||||||
TSsaPointerArithmeticGuard(IR::PointerArithmeticInstruction instr) {
|
TSsaPointerArithmeticGuard(ValueNumber instr) {
|
||||||
exists(Guard g, IR::Operand use | use = instr.getAUse() |
|
exists(Guard g, IR::Operand use |
|
||||||
|
use = instr.getAUse() and use.getIRType() instanceof IR::IRAddressType
|
||||||
|
|
|
||||||
g.comparesLt(use, _, _, _, _) or
|
g.comparesLt(use, _, _, _, _) or
|
||||||
g.comparesLt(_, use, _, _, _) or
|
g.comparesLt(_, use, _, _, _) or
|
||||||
g.comparesEq(use, _, _, _, _) or
|
g.comparesEq(use, _, _, _, _) or
|
||||||
@@ -138,7 +225,7 @@ module SemanticExprConfig {
|
|||||||
|
|
||||||
IR::Instruction asInstruction() { none() }
|
IR::Instruction asInstruction() { none() }
|
||||||
|
|
||||||
IR::PointerArithmeticInstruction asPointerArithGuard() { none() }
|
ValueNumber asPointerArithGuard() { none() }
|
||||||
|
|
||||||
IR::Operand asOperand() { none() }
|
IR::Operand asOperand() { none() }
|
||||||
}
|
}
|
||||||
@@ -156,15 +243,15 @@ module SemanticExprConfig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
class SsaPointerArithmeticGuard extends SsaVariable, TSsaPointerArithmeticGuard {
|
class SsaPointerArithmeticGuard extends SsaVariable, TSsaPointerArithmeticGuard {
|
||||||
IR::PointerArithmeticInstruction instr;
|
ValueNumber vn;
|
||||||
|
|
||||||
SsaPointerArithmeticGuard() { this = TSsaPointerArithmeticGuard(instr) }
|
SsaPointerArithmeticGuard() { this = TSsaPointerArithmeticGuard(vn) }
|
||||||
|
|
||||||
final override string toString() { result = instr.toString() }
|
final override string toString() { result = vn.toString() }
|
||||||
|
|
||||||
final override Location getLocation() { result = instr.getLocation() }
|
final override Location getLocation() { result = vn.getLocation() }
|
||||||
|
|
||||||
final override IR::PointerArithmeticInstruction asPointerArithGuard() { result = instr }
|
final override ValueNumber asPointerArithGuard() { result = vn }
|
||||||
}
|
}
|
||||||
|
|
||||||
class SsaOperand extends SsaVariable, TSsaOperand {
|
class SsaOperand extends SsaVariable, TSsaOperand {
|
||||||
@@ -179,7 +266,9 @@ module SemanticExprConfig {
|
|||||||
final override IR::Operand asOperand() { result = op }
|
final override IR::Operand asOperand() { result = op }
|
||||||
}
|
}
|
||||||
|
|
||||||
predicate explicitUpdate(SsaVariable v, Expr sourceExpr) { v.asInstruction() = sourceExpr }
|
predicate explicitUpdate(SsaVariable v, Expr sourceExpr) {
|
||||||
|
getSemanticExpr(v.asInstruction()) = sourceExpr
|
||||||
|
}
|
||||||
|
|
||||||
predicate phi(SsaVariable v) { v.asInstruction() instanceof IR::PhiInstruction }
|
predicate phi(SsaVariable v) { v.asInstruction() instanceof IR::PhiInstruction }
|
||||||
|
|
||||||
@@ -192,9 +281,9 @@ module SemanticExprConfig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
Expr getAUse(SsaVariable v) {
|
Expr getAUse(SsaVariable v) {
|
||||||
result.(IR::LoadInstruction).getSourceValue() = v.asInstruction()
|
result.getUnconverted().(IR::LoadInstruction).getSourceValue() = v.asInstruction()
|
||||||
or
|
or
|
||||||
result = valueNumber(v.asPointerArithGuard()).getAnInstruction()
|
result.getUnconverted() = v.asPointerArithGuard().getAnInstruction()
|
||||||
}
|
}
|
||||||
|
|
||||||
SemType getSsaVariableType(SsaVariable v) {
|
SemType getSsaVariableType(SsaVariable v) {
|
||||||
@@ -236,7 +325,7 @@ module SemanticExprConfig {
|
|||||||
final override predicate hasRead(SsaVariable v) {
|
final override predicate hasRead(SsaVariable v) {
|
||||||
exists(IR::Operand operand |
|
exists(IR::Operand operand |
|
||||||
operand.getDef() = v.asInstruction() or
|
operand.getDef() = v.asInstruction() or
|
||||||
operand.getDef() = valueNumber(v.asPointerArithGuard()).getAnInstruction()
|
operand.getDef() = v.asPointerArithGuard().getAnInstruction()
|
||||||
|
|
|
|
||||||
not operand instanceof IR::PhiInputOperand and
|
not operand instanceof IR::PhiInputOperand and
|
||||||
operand.getUse().getBlock() = block
|
operand.getUse().getBlock() = block
|
||||||
@@ -257,7 +346,7 @@ module SemanticExprConfig {
|
|||||||
final override predicate hasRead(SsaVariable v) {
|
final override predicate hasRead(SsaVariable v) {
|
||||||
exists(IR::PhiInputOperand operand |
|
exists(IR::PhiInputOperand operand |
|
||||||
operand.getDef() = v.asInstruction() or
|
operand.getDef() = v.asInstruction() or
|
||||||
operand.getDef() = valueNumber(v.asPointerArithGuard()).getAnInstruction()
|
operand.getDef() = v.asPointerArithGuard().getAnInstruction()
|
||||||
|
|
|
|
||||||
operand.getPredecessorBlock() = pred and
|
operand.getPredecessorBlock() = pred and
|
||||||
operand.getUse().getBlock() = succ
|
operand.getUse().getBlock() = succ
|
||||||
@@ -303,17 +392,21 @@ module SemanticExprConfig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
Expr getBoundExpr(Bound bound, int delta) {
|
Expr getBoundExpr(Bound bound, int delta) {
|
||||||
result = bound.(IRBound::Bound).getInstruction(delta)
|
result = getSemanticExpr(bound.(IRBound::Bound).getInstruction(delta))
|
||||||
}
|
}
|
||||||
|
|
||||||
class Guard = IRGuards::IRGuardCondition;
|
class Guard = IRGuards::IRGuardCondition;
|
||||||
|
|
||||||
predicate guard(Guard guard, BasicBlock block) { block = guard.getBlock() }
|
predicate guard(Guard guard, BasicBlock block) { block = guard.getBlock() }
|
||||||
|
|
||||||
Expr getGuardAsExpr(Guard guard) { result = guard }
|
Expr getGuardAsExpr(Guard guard) { result = getSemanticExpr(guard) }
|
||||||
|
|
||||||
predicate equalityGuard(Guard guard, Expr e1, Expr e2, boolean polarity) {
|
predicate equalityGuard(Guard guard, Expr e1, Expr e2, boolean polarity) {
|
||||||
guard.comparesEq(e1.getAUse(), e2.getAUse(), 0, true, polarity)
|
exists(IR::Instruction left, IR::Instruction right |
|
||||||
|
getSemanticExpr(left) = e1 and
|
||||||
|
getSemanticExpr(right) = e2 and
|
||||||
|
guard.comparesEq(left.getAUse(), right.getAUse(), 0, true, polarity)
|
||||||
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock controlled, boolean branch) {
|
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock controlled, boolean branch) {
|
||||||
@@ -324,16 +417,17 @@ module SemanticExprConfig {
|
|||||||
guard.controlsEdge(bb1, bb2, branch)
|
guard.controlsEdge(bb1, bb2, branch)
|
||||||
}
|
}
|
||||||
|
|
||||||
Guard comparisonGuard(Expr e) { result = e }
|
Guard comparisonGuard(Expr e) { getSemanticExpr(result) = e }
|
||||||
|
|
||||||
predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
|
predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
|
||||||
none() // TODO
|
none() // TODO
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** Gets the expression associated with `instr`. */
|
||||||
|
SemExpr getSemanticExpr(IR::Instruction instr) { result = Equiv::getEquivalenceClass(instr) }
|
||||||
}
|
}
|
||||||
|
|
||||||
SemExpr getSemanticExpr(IR::Instruction instr) { result = instr }
|
predicate getSemanticExpr = SemanticExprConfig::getSemanticExpr/1;
|
||||||
|
|
||||||
IR::Instruction getCppInstruction(SemExpr e) { e = result }
|
|
||||||
|
|
||||||
SemBasicBlock getSemanticBasicBlock(IR::IRBlock block) { result = block }
|
SemBasicBlock getSemanticBasicBlock(IR::IRBlock block) { result = block }
|
||||||
|
|
||||||
|
|||||||
@@ -250,16 +250,26 @@ SemType getSemanticType(Specific::Type type) {
|
|||||||
Specific::unknownType(type) and result = TSemUnknownType()
|
Specific::unknownType(type) and result = TSemUnknownType()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
private class SemNumericOrBooleanType extends SemSizedType {
|
||||||
|
SemNumericOrBooleanType() {
|
||||||
|
this instanceof SemNumericType
|
||||||
|
or
|
||||||
|
this instanceof SemBooleanType
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if the conversion from `fromType` to `toType` can never overflow or underflow.
|
* Holds if the conversion from `fromType` to `toType` can never overflow or underflow.
|
||||||
*/
|
*/
|
||||||
predicate conversionCannotOverflow(SemNumericType fromType, SemNumericType toType) {
|
predicate conversionCannotOverflow(SemNumericOrBooleanType fromType, SemNumericOrBooleanType toType) {
|
||||||
// Identity cast
|
// Identity cast
|
||||||
fromType = toType
|
fromType = toType
|
||||||
or
|
or
|
||||||
// Treat any cast to an FP type as safe. It can lose precision, but not overflow.
|
// Treat any cast to an FP type as safe. It can lose precision, but not overflow.
|
||||||
toType instanceof SemFloatingPointType and fromType = any(SemNumericType n)
|
toType instanceof SemFloatingPointType and fromType = any(SemNumericType n)
|
||||||
or
|
or
|
||||||
|
fromType instanceof SemBooleanType and toType instanceof SemIntegerType
|
||||||
|
or
|
||||||
exists(SemIntegerType fromInteger, SemIntegerType toInteger, int fromSize, int toSize |
|
exists(SemIntegerType fromInteger, SemIntegerType toInteger, int fromSize, int toSize |
|
||||||
fromInteger = fromType and
|
fromInteger = fromType and
|
||||||
toInteger = toType and
|
toInteger = toType and
|
||||||
|
|||||||
@@ -17,16 +17,7 @@ module FloatDelta implements DeltaSig {
|
|||||||
Delta fromInt(int n) { result = n }
|
Delta fromInt(int n) { result = n }
|
||||||
|
|
||||||
bindingset[f]
|
bindingset[f]
|
||||||
Delta fromFloat(float f) {
|
Delta fromFloat(float f) { result = 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
|
|
||||||
)
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
module FloatOverflow implements OverflowSig<FloatDelta> {
|
module FloatOverflow implements OverflowSig<FloatDelta> {
|
||||||
|
|||||||
@@ -502,7 +502,7 @@ UtilSig<D> UtilParam> {
|
|||||||
SemSsaVariable v2, SemGuard guardEq, boolean eqIsTrue, D::Delta d1, D::Delta d2,
|
SemSsaVariable v2, SemGuard guardEq, boolean eqIsTrue, D::Delta d1, D::Delta d2,
|
||||||
D::Delta oldDelta
|
D::Delta oldDelta
|
||||||
|
|
|
|
||||||
guardEq = semEqFlowCond(v, semSsaRead(v2, d1), d2, true, eqIsTrue) and
|
guardEq = semEqFlowCond(v, semSsaRead(pragma[only_bind_into](v2), d1), d2, true, eqIsTrue) and
|
||||||
result = boundFlowCond(v2, e, oldDelta, upper, testIsTrue) and
|
result = boundFlowCond(v2, e, oldDelta, upper, testIsTrue) and
|
||||||
// guardEq needs to control guard
|
// guardEq needs to control guard
|
||||||
guardEq.directlyControls(result.getBasicBlock(), eqIsTrue) and
|
guardEq.directlyControls(result.getBasicBlock(), eqIsTrue) and
|
||||||
@@ -598,24 +598,6 @@ UtilSig<D> UtilParam> {
|
|||||||
delta = D::fromInt(0) and
|
delta = D::fromInt(0) and
|
||||||
(upper = true or upper = false)
|
(upper = true or upper = false)
|
||||||
or
|
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 = D::fromInt(1)
|
|
||||||
else
|
|
||||||
if semPositive(x)
|
|
||||||
then upper = false and delta = D::fromInt(0)
|
|
||||||
else
|
|
||||||
if strictlyNegativeIntegralExpr(x)
|
|
||||||
then upper = true and delta = D::fromInt(-1)
|
|
||||||
else
|
|
||||||
if semNegative(x)
|
|
||||||
then upper = true and delta = D::fromInt(0)
|
|
||||||
else none()
|
|
||||||
)
|
|
||||||
or
|
|
||||||
exists(SemExpr x, SemSubExpr sub |
|
exists(SemExpr x, SemSubExpr sub |
|
||||||
e2 = sub and
|
e2 = sub and
|
||||||
sub.getLeftOperand() = e1 and
|
sub.getLeftOperand() = e1 and
|
||||||
@@ -1085,13 +1067,196 @@ UtilSig<D> UtilParam> {
|
|||||||
delta = D::fromFloat(f) and
|
delta = D::fromFloat(f) and
|
||||||
if semPositive(e) then f >= 0 else any()
|
if semPositive(e) then f >= 0 else any()
|
||||||
)
|
)
|
||||||
|
or
|
||||||
|
exists(
|
||||||
|
SemBound bLeft, SemBound bRight, D::Delta dLeft, D::Delta dRight, boolean fbeLeft,
|
||||||
|
boolean fbeRight, D::Delta odLeft, D::Delta odRight, SemReason rLeft, SemReason rRight
|
||||||
|
|
|
||||||
|
boundedAddOperand(e, upper, bLeft, false, dLeft, fbeLeft, odLeft, rLeft) and
|
||||||
|
boundedAddOperand(e, upper, bRight, true, dRight, fbeRight, odRight, rRight) and
|
||||||
|
delta = D::fromFloat(D::toFloat(dLeft) + D::toFloat(dRight)) and
|
||||||
|
fromBackEdge = fbeLeft.booleanOr(fbeRight)
|
||||||
|
|
|
||||||
|
b = bLeft and origdelta = odLeft and reason = rLeft and bRight instanceof SemZeroBound
|
||||||
|
or
|
||||||
|
b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
|
||||||
|
)
|
||||||
|
or
|
||||||
|
exists(
|
||||||
|
SemRemExpr rem, D::Delta d_max, D::Delta d1, D::Delta d2, boolean fbe1, boolean fbe2,
|
||||||
|
D::Delta od1, D::Delta od2, SemReason r1, SemReason r2
|
||||||
|
|
|
||||||
|
rem = e and
|
||||||
|
b instanceof SemZeroBound and
|
||||||
|
not (upper = true and semPositive(rem.getRightOperand())) and
|
||||||
|
not (upper = true and semPositive(rem.getLeftOperand())) and
|
||||||
|
boundedRemExpr(rem, true, d1, fbe1, od1, r1) and
|
||||||
|
boundedRemExpr(rem, false, d2, fbe2, od2, r2) and
|
||||||
|
(
|
||||||
|
if D::toFloat(d1).abs() > D::toFloat(d2).abs()
|
||||||
|
then (
|
||||||
|
d_max = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1
|
||||||
|
) else (
|
||||||
|
d_max = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2
|
||||||
|
)
|
||||||
|
)
|
||||||
|
|
|
||||||
|
upper = true and delta = D::fromFloat(D::toFloat(d_max).abs() - 1)
|
||||||
|
or
|
||||||
|
upper = false and delta = D::fromFloat(-D::toFloat(d_max).abs() + 1)
|
||||||
|
)
|
||||||
|
or
|
||||||
|
exists(
|
||||||
|
D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight, D::Delta odLeft,
|
||||||
|
D::Delta odRight, SemReason rLeft, SemReason rRight
|
||||||
|
|
|
||||||
|
boundedMulOperand(e, upper, true, dLeft, fbeLeft, odLeft, rLeft) and
|
||||||
|
boundedMulOperand(e, upper, false, dRight, fbeRight, odRight, rRight) and
|
||||||
|
delta = D::fromFloat(D::toFloat(dLeft) * D::toFloat(dRight)) and
|
||||||
|
fromBackEdge = fbeLeft.booleanOr(fbeRight)
|
||||||
|
|
|
||||||
|
b instanceof SemZeroBound and origdelta = odLeft and reason = rLeft
|
||||||
|
or
|
||||||
|
b instanceof SemZeroBound and origdelta = odRight and reason = rRight
|
||||||
|
)
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[nomagic]
|
||||||
private predicate boundedConditionalExpr(
|
private predicate boundedConditionalExpr(
|
||||||
SemConditionalExpr cond, SemBound b, boolean upper, boolean branch, D::Delta delta,
|
SemConditionalExpr cond, SemBound b, boolean upper, boolean branch, D::Delta delta,
|
||||||
boolean fromBackEdge, D::Delta origdelta, SemReason reason
|
boolean fromBackEdge, D::Delta origdelta, SemReason reason
|
||||||
) {
|
) {
|
||||||
bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason)
|
bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[nomagic]
|
||||||
|
private predicate boundedAddOperand(
|
||||||
|
SemAddExpr add, boolean upper, SemBound b, boolean isLeft, D::Delta delta, boolean fromBackEdge,
|
||||||
|
D::Delta origdelta, SemReason reason
|
||||||
|
) {
|
||||||
|
// `semValueFlowStep` already handles the case where one of the operands is a constant.
|
||||||
|
not semValueFlowStep(add, _, _) and
|
||||||
|
(
|
||||||
|
isLeft = true and
|
||||||
|
bounded(add.getLeftOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
|
||||||
|
or
|
||||||
|
isLeft = false and
|
||||||
|
bounded(add.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
pragma[nomagic]
|
||||||
|
private predicate boundedRemExpr(
|
||||||
|
SemRemExpr rem, boolean upper, D::Delta delta, boolean fromBackEdge, D::Delta origdelta,
|
||||||
|
SemReason reason
|
||||||
|
) {
|
||||||
|
bounded(rem.getRightOperand(), any(SemZeroBound zb), delta, upper, fromBackEdge, origdelta,
|
||||||
|
reason)
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Define `cmp(true) = <=` and `cmp(false) = >=`.
|
||||||
|
*
|
||||||
|
* Holds if `mul = left * right`, and in order to know if `mul cmp(upper) 0 + k` (for
|
||||||
|
* some `k`) we need to know that `left cmp(upperLeft) 0 + k1` and
|
||||||
|
* `right cmp(upperRight) 0 + k2` (for some `k1` and `k2`).
|
||||||
|
*/
|
||||||
|
pragma[nomagic]
|
||||||
|
private predicate boundedMulOperandCand(
|
||||||
|
SemMulExpr mul, SemExpr left, SemExpr right, boolean upper, boolean upperLeft,
|
||||||
|
boolean upperRight
|
||||||
|
) {
|
||||||
|
not boundFlowStepMul(mul, _, _) and
|
||||||
|
mul.getLeftOperand() = left and
|
||||||
|
mul.getRightOperand() = right and
|
||||||
|
(
|
||||||
|
semPositive(left) and
|
||||||
|
(
|
||||||
|
// left, right >= 0
|
||||||
|
semPositive(right) and
|
||||||
|
(
|
||||||
|
// max(left * right) = max(left) * max(right)
|
||||||
|
upper = true and
|
||||||
|
upperLeft = true and
|
||||||
|
upperRight = true
|
||||||
|
or
|
||||||
|
// min(left * right) = min(left) * min(right)
|
||||||
|
upper = false and
|
||||||
|
upperLeft = false and
|
||||||
|
upperRight = false
|
||||||
|
)
|
||||||
|
or
|
||||||
|
// left >= 0, right <= 0
|
||||||
|
semNegative(right) and
|
||||||
|
(
|
||||||
|
// max(left * right) = min(left) * max(right)
|
||||||
|
upper = true and
|
||||||
|
upperLeft = false and
|
||||||
|
upperRight = true
|
||||||
|
or
|
||||||
|
// min(left * right) = max(left) * min(right)
|
||||||
|
upper = false and
|
||||||
|
upperLeft = true and
|
||||||
|
upperRight = false
|
||||||
|
)
|
||||||
|
)
|
||||||
|
or
|
||||||
|
semNegative(left) and
|
||||||
|
(
|
||||||
|
// left <= 0, right >= 0
|
||||||
|
semPositive(right) and
|
||||||
|
(
|
||||||
|
// max(left * right) = max(left) * min(right)
|
||||||
|
upper = true and
|
||||||
|
upperLeft = true and
|
||||||
|
upperRight = false
|
||||||
|
or
|
||||||
|
// min(left * right) = min(left) * max(right)
|
||||||
|
upper = false and
|
||||||
|
upperLeft = false and
|
||||||
|
upperRight = true
|
||||||
|
)
|
||||||
|
or
|
||||||
|
// left, right <= 0
|
||||||
|
semNegative(right) and
|
||||||
|
(
|
||||||
|
// max(left * right) = min(left) * min(right)
|
||||||
|
upper = true and
|
||||||
|
upperLeft = false and
|
||||||
|
upperRight = false
|
||||||
|
or
|
||||||
|
// min(left * right) = max(left) * max(right)
|
||||||
|
upper = false and
|
||||||
|
upperLeft = true and
|
||||||
|
upperRight = true
|
||||||
|
)
|
||||||
|
)
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Holds if `isLeft = true` and `mul`'s left operand is bounded by `delta`,
|
||||||
|
* or if `isLeft = false` and `mul`'s right operand is bounded by `delta`.
|
||||||
|
*
|
||||||
|
* If `upper = true` the computed bound contributes to an upper bound of `mul`,
|
||||||
|
* and if `upper = false` it contributes to a lower bound.
|
||||||
|
* The `fromBackEdge`, `origdelta`, `reason` triple are defined by the recursive
|
||||||
|
* call to `bounded`.
|
||||||
|
*/
|
||||||
|
pragma[nomagic]
|
||||||
|
private predicate boundedMulOperand(
|
||||||
|
SemMulExpr mul, boolean upper, boolean isLeft, D::Delta delta, boolean fromBackEdge,
|
||||||
|
D::Delta origdelta, SemReason reason
|
||||||
|
) {
|
||||||
|
exists(boolean upperLeft, boolean upperRight, SemExpr left, SemExpr right |
|
||||||
|
boundedMulOperandCand(mul, left, right, upper, upperLeft, upperRight)
|
||||||
|
|
|
||||||
|
isLeft = true and
|
||||||
|
bounded(left, any(SemZeroBound zb), delta, upperLeft, fromBackEdge, origdelta, reason)
|
||||||
|
or
|
||||||
|
isLeft = false and
|
||||||
|
bounded(right, any(SemZeroBound zb), delta, upperRight, fromBackEdge, origdelta, reason)
|
||||||
|
)
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -198,6 +198,16 @@ module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** An expression of an unsigned type. */
|
||||||
|
private class UnsignedExpr extends FlowSignExpr {
|
||||||
|
UnsignedExpr() { Utils::getTrackedType(this) instanceof SemUnsignedIntegerType }
|
||||||
|
|
||||||
|
override Sign getSignRestriction() {
|
||||||
|
result = TPos() or
|
||||||
|
result = TZero()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private predicate binaryExprOperands(SemBinaryExpr binary, SemExpr left, SemExpr right) {
|
private predicate binaryExprOperands(SemBinaryExpr binary, SemExpr left, SemExpr right) {
|
||||||
binary.getLeftOperand() = left and binary.getRightOperand() = right
|
binary.getLeftOperand() = left and binary.getRightOperand() = right
|
||||||
@@ -328,10 +338,11 @@ module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
|
|||||||
* - `isEq = false` : `v != eqbound`
|
* - `isEq = false` : `v != eqbound`
|
||||||
*/
|
*/
|
||||||
private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
|
private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
|
||||||
exists(SemGuard guard, boolean testIsTrue, boolean polarity |
|
exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
|
||||||
pos.hasReadOfVar(v) and
|
pos.hasReadOfVar(pragma[only_bind_into](v)) and
|
||||||
semGuardControlsSsaRead(guard, pos, testIsTrue) and
|
semGuardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
|
||||||
guard.isEquality(eqbound, Utils::semSsaRead(v, D::fromInt(0)), polarity) and
|
e = Utils::semSsaRead(pragma[only_bind_into](v), D::fromInt(0)) and
|
||||||
|
guard.isEquality(eqbound, e, polarity) and
|
||||||
isEq = polarity.booleanXor(testIsTrue).booleanNot() and
|
isEq = polarity.booleanXor(testIsTrue).booleanNot() and
|
||||||
not unknownSign(eqbound)
|
not unknownSign(eqbound)
|
||||||
)
|
)
|
||||||
|
|||||||
@@ -8,3 +8,4 @@ upgrades: upgrades
|
|||||||
dependencies:
|
dependencies:
|
||||||
codeql/ssa: ${workspace}
|
codeql/ssa: ${workspace}
|
||||||
codeql/tutorial: ${workspace}
|
codeql/tutorial: ${workspace}
|
||||||
|
codeql/util: ${workspace}
|
||||||
|
|||||||
@@ -2,7 +2,7 @@
|
|||||||
* Provides an implementation of global (interprocedural) data flow. This file
|
* Provides an implementation of global (interprocedural) data flow. This file
|
||||||
* re-exports the local (intraprocedural) data flow analysis from
|
* re-exports the local (intraprocedural) data flow analysis from
|
||||||
* `DataFlowImplSpecific::Public` and adds a global analysis, mainly exposed
|
* `DataFlowImplSpecific::Public` and adds a global analysis, mainly exposed
|
||||||
* through the `Make` and `MakeWithState` modules.
|
* through the `Global` and `GlobalWithState` modules.
|
||||||
*/
|
*/
|
||||||
|
|
||||||
private import DataFlowImplCommon
|
private import DataFlowImplCommon
|
||||||
@@ -73,10 +73,10 @@ signature module ConfigSig {
|
|||||||
*/
|
*/
|
||||||
default FlowFeature getAFeature() { none() }
|
default FlowFeature getAFeature() { none() }
|
||||||
|
|
||||||
/** Holds if sources should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sources should be grouped in the result of `flowPath`. */
|
||||||
default predicate sourceGrouping(Node source, string sourceGroup) { none() }
|
default predicate sourceGrouping(Node source, string sourceGroup) { none() }
|
||||||
|
|
||||||
/** Holds if sinks should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sinks should be grouped in the result of `flowPath`. */
|
||||||
default predicate sinkGrouping(Node sink, string sinkGroup) { none() }
|
default predicate sinkGrouping(Node sink, string sinkGroup) { none() }
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -166,10 +166,10 @@ signature module StateConfigSig {
|
|||||||
*/
|
*/
|
||||||
default FlowFeature getAFeature() { none() }
|
default FlowFeature getAFeature() { none() }
|
||||||
|
|
||||||
/** Holds if sources should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sources should be grouped in the result of `flowPath`. */
|
||||||
default predicate sourceGrouping(Node source, string sourceGroup) { none() }
|
default predicate sourceGrouping(Node source, string sourceGroup) { none() }
|
||||||
|
|
||||||
/** Holds if sinks should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sinks should be grouped in the result of `flowPath`. */
|
||||||
default predicate sinkGrouping(Node sink, string sinkGroup) { none() }
|
default predicate sinkGrouping(Node sink, string sinkGroup) { none() }
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -182,15 +182,15 @@ signature module StateConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Gets the exploration limit for `hasPartialFlow` and `hasPartialFlowRev`
|
* Gets the exploration limit for `partialFlow` and `partialFlowRev`
|
||||||
* measured in approximate number of interprocedural steps.
|
* measured in approximate number of interprocedural steps.
|
||||||
*/
|
*/
|
||||||
signature int explorationLimitSig();
|
signature int explorationLimitSig();
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* The output of a data flow computation.
|
* The output of a global data flow computation.
|
||||||
*/
|
*/
|
||||||
signature module DataFlowSig {
|
signature module GlobalFlowSig {
|
||||||
/**
|
/**
|
||||||
* A `Node` augmented with a call context (except for sinks) and an access path.
|
* A `Node` augmented with a call context (except for sinks) and an access path.
|
||||||
* Only those `PathNode`s that are reachable from a source, and which can reach a sink, are generated.
|
* Only those `PathNode`s that are reachable from a source, and which can reach a sink, are generated.
|
||||||
@@ -203,28 +203,28 @@ signature module DataFlowSig {
|
|||||||
* The corresponding paths are generated from the end-points and the graph
|
* The corresponding paths are generated from the end-points and the graph
|
||||||
* included in the module `PathGraph`.
|
* included in the module `PathGraph`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowPath(PathNode source, PathNode sink);
|
predicate flowPath(PathNode source, PathNode sink);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if data can flow from `source` to `sink`.
|
* Holds if data can flow from `source` to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlow(Node source, Node sink);
|
predicate flow(Node source, Node sink);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if data can flow from some source to `sink`.
|
* Holds if data can flow from some source to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowTo(Node sink);
|
predicate flowTo(Node sink);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if data can flow from some source to `sink`.
|
* Holds if data can flow from some source to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowToExpr(DataFlowExpr sink);
|
predicate flowToExpr(DataFlowExpr sink);
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Constructs a standard data flow computation.
|
* Constructs a global data flow computation.
|
||||||
*/
|
*/
|
||||||
module Make<ConfigSig Config> implements DataFlowSig {
|
module Global<ConfigSig Config> implements GlobalFlowSig {
|
||||||
private module C implements FullStateConfigSig {
|
private module C implements FullStateConfigSig {
|
||||||
import DefaultState<Config>
|
import DefaultState<Config>
|
||||||
import Config
|
import Config
|
||||||
@@ -233,10 +233,15 @@ module Make<ConfigSig Config> implements DataFlowSig {
|
|||||||
import Impl<C>
|
import Impl<C>
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `Global` instead. */
|
||||||
|
deprecated module Make<ConfigSig Config> implements GlobalFlowSig {
|
||||||
|
import Global<Config>
|
||||||
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Constructs a data flow computation using flow state.
|
* Constructs a global data flow computation using flow state.
|
||||||
*/
|
*/
|
||||||
module MakeWithState<StateConfigSig Config> implements DataFlowSig {
|
module GlobalWithState<StateConfigSig Config> implements GlobalFlowSig {
|
||||||
private module C implements FullStateConfigSig {
|
private module C implements FullStateConfigSig {
|
||||||
import Config
|
import Config
|
||||||
}
|
}
|
||||||
@@ -244,6 +249,11 @@ module MakeWithState<StateConfigSig Config> implements DataFlowSig {
|
|||||||
import Impl<C>
|
import Impl<C>
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `GlobalWithState` instead. */
|
||||||
|
deprecated module MakeWithState<StateConfigSig Config> implements GlobalFlowSig {
|
||||||
|
import GlobalWithState<Config>
|
||||||
|
}
|
||||||
|
|
||||||
signature class PathNodeSig {
|
signature class PathNodeSig {
|
||||||
/** Gets a textual representation of this element. */
|
/** Gets a textual representation of this element. */
|
||||||
string toString();
|
string toString();
|
||||||
|
|||||||
@@ -8,6 +8,7 @@ private import DataFlowImplCommon
|
|||||||
private import DataFlowImplSpecific::Private
|
private import DataFlowImplSpecific::Private
|
||||||
private import DataFlowImplSpecific::Public
|
private import DataFlowImplSpecific::Public
|
||||||
private import DataFlowImplCommonPublic
|
private import DataFlowImplCommonPublic
|
||||||
|
private import codeql.util.Unit
|
||||||
import DataFlow
|
import DataFlow
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -91,10 +92,10 @@ signature module FullStateConfigSig {
|
|||||||
*/
|
*/
|
||||||
FlowFeature getAFeature();
|
FlowFeature getAFeature();
|
||||||
|
|
||||||
/** Holds if sources should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sources should be grouped in the result of `flowPath`. */
|
||||||
predicate sourceGrouping(Node source, string sourceGroup);
|
predicate sourceGrouping(Node source, string sourceGroup);
|
||||||
|
|
||||||
/** Holds if sinks should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sinks should be grouped in the result of `flowPath`. */
|
||||||
predicate sinkGrouping(Node sink, string sinkGroup);
|
predicate sinkGrouping(Node sink, string sinkGroup);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -445,11 +446,7 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private module Stage1 implements StageSig {
|
private module Stage1 implements StageSig {
|
||||||
class Ap extends int {
|
class Ap = Unit;
|
||||||
// workaround for bad functionality-induced joins (happens when using `Unit`)
|
|
||||||
pragma[nomagic]
|
|
||||||
Ap() { this in [0 .. 1] and this < 1 }
|
|
||||||
}
|
|
||||||
|
|
||||||
private class Cc = boolean;
|
private class Cc = boolean;
|
||||||
|
|
||||||
@@ -3633,7 +3630,7 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
* The corresponding paths are generated from the end-points and the graph
|
* The corresponding paths are generated from the end-points and the graph
|
||||||
* included in the module `PathGraph`.
|
* included in the module `PathGraph`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowPath(PathNode source, PathNode sink) {
|
predicate flowPath(PathNode source, PathNode sink) {
|
||||||
exists(PathNodeImpl flowsource, PathNodeImpl flowsink |
|
exists(PathNodeImpl flowsource, PathNodeImpl flowsink |
|
||||||
source = flowsource and sink = flowsink
|
source = flowsource and sink = flowsink
|
||||||
|
|
|
|
||||||
@@ -3643,6 +3640,9 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `flowPath` instead. */
|
||||||
|
deprecated predicate hasFlowPath = flowPath/2;
|
||||||
|
|
||||||
private predicate flowsTo(PathNodeImpl flowsource, PathNodeSink flowsink, Node source, Node sink) {
|
private predicate flowsTo(PathNodeImpl flowsource, PathNodeSink flowsink, Node source, Node sink) {
|
||||||
flowsource.isSource() and
|
flowsource.isSource() and
|
||||||
flowsource.getNodeEx().asNode() = source and
|
flowsource.getNodeEx().asNode() = source and
|
||||||
@@ -3653,17 +3653,26 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
/**
|
/**
|
||||||
* Holds if data can flow from `source` to `sink`.
|
* Holds if data can flow from `source` to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlow(Node source, Node sink) { flowsTo(_, _, source, sink) }
|
predicate flow(Node source, Node sink) { flowsTo(_, _, source, sink) }
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `flow` instead. */
|
||||||
|
deprecated predicate hasFlow = flow/2;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if data can flow from some source to `sink`.
|
* Holds if data can flow from some source to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowTo(Node sink) { sink = any(PathNodeSink n).getNodeEx().asNode() }
|
predicate flowTo(Node sink) { sink = any(PathNodeSink n).getNodeEx().asNode() }
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `flowTo` instead. */
|
||||||
|
deprecated predicate hasFlowTo = flowTo/1;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if data can flow from some source to `sink`.
|
* Holds if data can flow from some source to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowToExpr(DataFlowExpr sink) { hasFlowTo(exprNode(sink)) }
|
predicate flowToExpr(DataFlowExpr sink) { flowTo(exprNode(sink)) }
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `flowToExpr` instead. */
|
||||||
|
deprecated predicate hasFlowToExpr = flowToExpr/1;
|
||||||
|
|
||||||
private predicate finalStats(
|
private predicate finalStats(
|
||||||
boolean fwd, int nodes, int fields, int conscand, int states, int tuples
|
boolean fwd, int nodes, int fields, int conscand, int states, int tuples
|
||||||
@@ -4574,7 +4583,7 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
*
|
*
|
||||||
* To use this in a `path-problem` query, import the module `PartialPathGraph`.
|
* To use this in a `path-problem` query, import the module `PartialPathGraph`.
|
||||||
*/
|
*/
|
||||||
predicate hasPartialFlow(PartialPathNode source, PartialPathNode node, int dist) {
|
predicate partialFlow(PartialPathNode source, PartialPathNode node, int dist) {
|
||||||
partialFlow(source, node) and
|
partialFlow(source, node) and
|
||||||
dist = node.getSourceDistance()
|
dist = node.getSourceDistance()
|
||||||
}
|
}
|
||||||
@@ -4594,7 +4603,7 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
* Note that reverse flow has slightly lower precision than the corresponding
|
* Note that reverse flow has slightly lower precision than the corresponding
|
||||||
* forward flow, as reverse flow disregards type pruning among other features.
|
* forward flow, as reverse flow disregards type pruning among other features.
|
||||||
*/
|
*/
|
||||||
predicate hasPartialFlowRev(PartialPathNode node, PartialPathNode sink, int dist) {
|
predicate partialFlowRev(PartialPathNode node, PartialPathNode sink, int dist) {
|
||||||
revPartialFlow(node, sink) and
|
revPartialFlow(node, sink) and
|
||||||
dist = node.getSinkDistance()
|
dist = node.getSinkDistance()
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
/**
|
/**
|
||||||
* DEPRECATED: Use `Make` and `MakeWithState` instead.
|
* DEPRECATED: Use `Global` and `GlobalWithState` instead.
|
||||||
*
|
*
|
||||||
* Provides a `Configuration` class backwards-compatible interface to the data
|
* Provides a `Configuration` class backwards-compatible interface to the data
|
||||||
* flow library.
|
* flow library.
|
||||||
@@ -11,6 +11,7 @@ import DataFlowImplSpecific::Public
|
|||||||
private import DataFlowImpl
|
private import DataFlowImpl
|
||||||
import DataFlowImplCommonPublic
|
import DataFlowImplCommonPublic
|
||||||
import FlowStateString
|
import FlowStateString
|
||||||
|
private import codeql.util.Unit
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A configuration of interprocedural data flow analysis. This defines
|
* A configuration of interprocedural data flow analysis. This defines
|
||||||
@@ -328,7 +329,6 @@ private module Config implements FullStateConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private import Impl<Config> as I
|
private import Impl<Config> as I
|
||||||
import I
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
||||||
@@ -379,6 +379,8 @@ class PathNode instanceof I::PathNode {
|
|||||||
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
module PathGraph = I::PathGraph;
|
||||||
|
|
||||||
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
||||||
exists(PathNode source0, PathNode sink0 |
|
exists(PathNode source0, PathNode sink0 |
|
||||||
hasFlowPath(source0, sink0, config) and
|
hasFlowPath(source0, sink0, config) and
|
||||||
@@ -388,7 +390,7 @@ private predicate hasFlow(Node source, Node sink, Configuration config) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
||||||
hasFlowPath(source, sink) and source.getConfiguration() = config
|
I::flowPath(source, sink) and source.getConfiguration() = config
|
||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
/**
|
/**
|
||||||
* DEPRECATED: Use `Make` and `MakeWithState` instead.
|
* DEPRECATED: Use `Global` and `GlobalWithState` instead.
|
||||||
*
|
*
|
||||||
* Provides a `Configuration` class backwards-compatible interface to the data
|
* Provides a `Configuration` class backwards-compatible interface to the data
|
||||||
* flow library.
|
* flow library.
|
||||||
@@ -11,6 +11,7 @@ import DataFlowImplSpecific::Public
|
|||||||
private import DataFlowImpl
|
private import DataFlowImpl
|
||||||
import DataFlowImplCommonPublic
|
import DataFlowImplCommonPublic
|
||||||
import FlowStateString
|
import FlowStateString
|
||||||
|
private import codeql.util.Unit
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A configuration of interprocedural data flow analysis. This defines
|
* A configuration of interprocedural data flow analysis. This defines
|
||||||
@@ -328,7 +329,6 @@ private module Config implements FullStateConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private import Impl<Config> as I
|
private import Impl<Config> as I
|
||||||
import I
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
||||||
@@ -379,6 +379,8 @@ class PathNode instanceof I::PathNode {
|
|||||||
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
module PathGraph = I::PathGraph;
|
||||||
|
|
||||||
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
||||||
exists(PathNode source0, PathNode sink0 |
|
exists(PathNode source0, PathNode sink0 |
|
||||||
hasFlowPath(source0, sink0, config) and
|
hasFlowPath(source0, sink0, config) and
|
||||||
@@ -388,7 +390,7 @@ private predicate hasFlow(Node source, Node sink, Configuration config) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
||||||
hasFlowPath(source, sink) and source.getConfiguration() = config
|
I::flowPath(source, sink) and source.getConfiguration() = config
|
||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
/**
|
/**
|
||||||
* DEPRECATED: Use `Make` and `MakeWithState` instead.
|
* DEPRECATED: Use `Global` and `GlobalWithState` instead.
|
||||||
*
|
*
|
||||||
* Provides a `Configuration` class backwards-compatible interface to the data
|
* Provides a `Configuration` class backwards-compatible interface to the data
|
||||||
* flow library.
|
* flow library.
|
||||||
@@ -11,6 +11,7 @@ import DataFlowImplSpecific::Public
|
|||||||
private import DataFlowImpl
|
private import DataFlowImpl
|
||||||
import DataFlowImplCommonPublic
|
import DataFlowImplCommonPublic
|
||||||
import FlowStateString
|
import FlowStateString
|
||||||
|
private import codeql.util.Unit
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A configuration of interprocedural data flow analysis. This defines
|
* A configuration of interprocedural data flow analysis. This defines
|
||||||
@@ -328,7 +329,6 @@ private module Config implements FullStateConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private import Impl<Config> as I
|
private import Impl<Config> as I
|
||||||
import I
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
||||||
@@ -379,6 +379,8 @@ class PathNode instanceof I::PathNode {
|
|||||||
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
module PathGraph = I::PathGraph;
|
||||||
|
|
||||||
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
||||||
exists(PathNode source0, PathNode sink0 |
|
exists(PathNode source0, PathNode sink0 |
|
||||||
hasFlowPath(source0, sink0, config) and
|
hasFlowPath(source0, sink0, config) and
|
||||||
@@ -388,7 +390,7 @@ private predicate hasFlow(Node source, Node sink, Configuration config) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
||||||
hasFlowPath(source, sink) and source.getConfiguration() = config
|
I::flowPath(source, sink) and source.getConfiguration() = config
|
||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
/**
|
/**
|
||||||
* DEPRECATED: Use `Make` and `MakeWithState` instead.
|
* DEPRECATED: Use `Global` and `GlobalWithState` instead.
|
||||||
*
|
*
|
||||||
* Provides a `Configuration` class backwards-compatible interface to the data
|
* Provides a `Configuration` class backwards-compatible interface to the data
|
||||||
* flow library.
|
* flow library.
|
||||||
@@ -11,6 +11,7 @@ import DataFlowImplSpecific::Public
|
|||||||
private import DataFlowImpl
|
private import DataFlowImpl
|
||||||
import DataFlowImplCommonPublic
|
import DataFlowImplCommonPublic
|
||||||
import FlowStateString
|
import FlowStateString
|
||||||
|
private import codeql.util.Unit
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A configuration of interprocedural data flow analysis. This defines
|
* A configuration of interprocedural data flow analysis. This defines
|
||||||
@@ -328,7 +329,6 @@ private module Config implements FullStateConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private import Impl<Config> as I
|
private import Impl<Config> as I
|
||||||
import I
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
||||||
@@ -379,6 +379,8 @@ class PathNode instanceof I::PathNode {
|
|||||||
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
module PathGraph = I::PathGraph;
|
||||||
|
|
||||||
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
||||||
exists(PathNode source0, PathNode sink0 |
|
exists(PathNode source0, PathNode sink0 |
|
||||||
hasFlowPath(source0, sink0, config) and
|
hasFlowPath(source0, sink0, config) and
|
||||||
@@ -388,7 +390,7 @@ private predicate hasFlow(Node source, Node sink, Configuration config) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
||||||
hasFlowPath(source, sink) and source.getConfiguration() = config
|
I::flowPath(source, sink) and source.getConfiguration() = config
|
||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
||||||
|
|||||||
@@ -140,10 +140,8 @@ private module LambdaFlow {
|
|||||||
}
|
}
|
||||||
|
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private TReturnPositionSimple viableReturnPosLambda(
|
private TReturnPositionSimple viableReturnPosLambda(DataFlowCall call, ReturnKind kind) {
|
||||||
DataFlowCall call, DataFlowCallOption lastCall, ReturnKind kind
|
result = TReturnPositionSimple0(viableCallableLambda(call, _), kind)
|
||||||
) {
|
|
||||||
result = TReturnPositionSimple0(viableCallableLambda(call, lastCall), kind)
|
|
||||||
}
|
}
|
||||||
|
|
||||||
private predicate viableReturnPosOutNonLambda(
|
private predicate viableReturnPosOutNonLambda(
|
||||||
@@ -155,11 +153,12 @@ private module LambdaFlow {
|
|||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[nomagic]
|
||||||
private predicate viableReturnPosOutLambda(
|
private predicate viableReturnPosOutLambda(
|
||||||
DataFlowCall call, DataFlowCallOption lastCall, TReturnPositionSimple pos, OutNode out
|
DataFlowCall call, TReturnPositionSimple pos, OutNode out
|
||||||
) {
|
) {
|
||||||
exists(ReturnKind kind |
|
exists(ReturnKind kind |
|
||||||
pos = viableReturnPosLambda(call, lastCall, kind) and
|
pos = viableReturnPosLambda(call, kind) and
|
||||||
out = getAnOutNode(call, kind)
|
out = getAnOutNode(call, kind)
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
@@ -188,6 +187,7 @@ private module LambdaFlow {
|
|||||||
else any()
|
else any()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
predicate revLambdaFlow0(
|
predicate revLambdaFlow0(
|
||||||
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
|
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
|
||||||
@@ -274,6 +274,7 @@ private module LambdaFlow {
|
|||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
predicate revLambdaFlowOut(
|
predicate revLambdaFlowOut(
|
||||||
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
|
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
|
||||||
@@ -285,7 +286,7 @@ private module LambdaFlow {
|
|||||||
or
|
or
|
||||||
// non-linear recursion
|
// non-linear recursion
|
||||||
revLambdaFlowOutLambdaCall(lambdaCall, kind, out, t, toJump, call, lastCall) and
|
revLambdaFlowOutLambdaCall(lambdaCall, kind, out, t, toJump, call, lastCall) and
|
||||||
viableReturnPosOutLambda(call, _, pos, out)
|
viableReturnPosOutLambda(call, pos, out)
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
/**
|
/**
|
||||||
* DEPRECATED: Use `Make` and `MakeWithState` instead.
|
* DEPRECATED: Use `Global` and `GlobalWithState` instead.
|
||||||
*
|
*
|
||||||
* Provides a `Configuration` class backwards-compatible interface to the data
|
* Provides a `Configuration` class backwards-compatible interface to the data
|
||||||
* flow library.
|
* flow library.
|
||||||
@@ -11,6 +11,7 @@ import DataFlowImplSpecific::Public
|
|||||||
private import DataFlowImpl
|
private import DataFlowImpl
|
||||||
import DataFlowImplCommonPublic
|
import DataFlowImplCommonPublic
|
||||||
import FlowStateString
|
import FlowStateString
|
||||||
|
private import codeql.util.Unit
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A configuration of interprocedural data flow analysis. This defines
|
* A configuration of interprocedural data flow analysis. This defines
|
||||||
@@ -328,7 +329,6 @@ private module Config implements FullStateConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private import Impl<Config> as I
|
private import Impl<Config> as I
|
||||||
import I
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
||||||
@@ -379,6 +379,8 @@ class PathNode instanceof I::PathNode {
|
|||||||
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
module PathGraph = I::PathGraph;
|
||||||
|
|
||||||
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
||||||
exists(PathNode source0, PathNode sink0 |
|
exists(PathNode source0, PathNode sink0 |
|
||||||
hasFlowPath(source0, sink0, config) and
|
hasFlowPath(source0, sink0, config) and
|
||||||
@@ -388,7 +390,7 @@ private predicate hasFlow(Node source, Node sink, Configuration config) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
||||||
hasFlowPath(source, sink) and source.getConfiguration() = config
|
I::flowPath(source, sink) and source.getConfiguration() = config
|
||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
||||||
|
|||||||
@@ -3,6 +3,7 @@ private import DataFlowUtil
|
|||||||
private import DataFlowDispatch
|
private import DataFlowDispatch
|
||||||
private import FlowVar
|
private import FlowVar
|
||||||
private import DataFlowImplConsistency
|
private import DataFlowImplConsistency
|
||||||
|
private import codeql.util.Unit
|
||||||
|
|
||||||
/** Gets the callable in which this node occurs. */
|
/** Gets the callable in which this node occurs. */
|
||||||
DataFlowCallable nodeGetEnclosingCallable(Node n) { result = n.getEnclosingCallable() }
|
DataFlowCallable nodeGetEnclosingCallable(Node n) { result = n.getEnclosingCallable() }
|
||||||
@@ -264,15 +265,6 @@ int accessPathLimit() { result = 5 }
|
|||||||
*/
|
*/
|
||||||
predicate forceHighPrecision(Content c) { none() }
|
predicate forceHighPrecision(Content c) { none() }
|
||||||
|
|
||||||
/** The unit type. */
|
|
||||||
private newtype TUnit = TMkUnit()
|
|
||||||
|
|
||||||
/** The trivial type with a single element. */
|
|
||||||
class Unit extends TUnit {
|
|
||||||
/** Gets a textual representation of this element. */
|
|
||||||
string toString() { result = "unit" }
|
|
||||||
}
|
|
||||||
|
|
||||||
/** Holds if `n` should be hidden from path explanations. */
|
/** Holds if `n` should be hidden from path explanations. */
|
||||||
predicate nodeIsHidden(Node n) { none() }
|
predicate nodeIsHidden(Node n) { none() }
|
||||||
|
|
||||||
|
|||||||
@@ -33,9 +33,9 @@ private module AddTaintDefaults<DataFlowInternal::FullStateConfigSig Config> imp
|
|||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Constructs a standard taint tracking computation.
|
* Constructs a global taint tracking computation.
|
||||||
*/
|
*/
|
||||||
module Make<DataFlow::ConfigSig Config> implements DataFlow::DataFlowSig {
|
module Global<DataFlow::ConfigSig Config> implements DataFlow::GlobalFlowSig {
|
||||||
private module Config0 implements DataFlowInternal::FullStateConfigSig {
|
private module Config0 implements DataFlowInternal::FullStateConfigSig {
|
||||||
import DataFlowInternal::DefaultState<Config>
|
import DataFlowInternal::DefaultState<Config>
|
||||||
import Config
|
import Config
|
||||||
@@ -48,10 +48,15 @@ module Make<DataFlow::ConfigSig Config> implements DataFlow::DataFlowSig {
|
|||||||
import DataFlowInternal::Impl<C>
|
import DataFlowInternal::Impl<C>
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `Global` instead. */
|
||||||
|
deprecated module Make<DataFlow::ConfigSig Config> implements DataFlow::GlobalFlowSig {
|
||||||
|
import Global<Config>
|
||||||
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Constructs a taint tracking computation using flow state.
|
* Constructs a global taint tracking computation using flow state.
|
||||||
*/
|
*/
|
||||||
module MakeWithState<DataFlow::StateConfigSig Config> implements DataFlow::DataFlowSig {
|
module GlobalWithState<DataFlow::StateConfigSig Config> implements DataFlow::GlobalFlowSig {
|
||||||
private module Config0 implements DataFlowInternal::FullStateConfigSig {
|
private module Config0 implements DataFlowInternal::FullStateConfigSig {
|
||||||
import Config
|
import Config
|
||||||
}
|
}
|
||||||
@@ -62,3 +67,8 @@ module MakeWithState<DataFlow::StateConfigSig Config> implements DataFlow::DataF
|
|||||||
|
|
||||||
import DataFlowInternal::Impl<C>
|
import DataFlowInternal::Impl<C>
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `GlobalWithState` instead. */
|
||||||
|
deprecated module MakeWithState<DataFlow::StateConfigSig Config> implements DataFlow::GlobalFlowSig {
|
||||||
|
import GlobalWithState<Config>
|
||||||
|
}
|
||||||
|
|||||||
@@ -2,7 +2,7 @@
|
|||||||
* Provides an implementation of global (interprocedural) data flow. This file
|
* Provides an implementation of global (interprocedural) data flow. This file
|
||||||
* re-exports the local (intraprocedural) data flow analysis from
|
* re-exports the local (intraprocedural) data flow analysis from
|
||||||
* `DataFlowImplSpecific::Public` and adds a global analysis, mainly exposed
|
* `DataFlowImplSpecific::Public` and adds a global analysis, mainly exposed
|
||||||
* through the `Make` and `MakeWithState` modules.
|
* through the `Global` and `GlobalWithState` modules.
|
||||||
*/
|
*/
|
||||||
|
|
||||||
private import DataFlowImplCommon
|
private import DataFlowImplCommon
|
||||||
@@ -73,10 +73,10 @@ signature module ConfigSig {
|
|||||||
*/
|
*/
|
||||||
default FlowFeature getAFeature() { none() }
|
default FlowFeature getAFeature() { none() }
|
||||||
|
|
||||||
/** Holds if sources should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sources should be grouped in the result of `flowPath`. */
|
||||||
default predicate sourceGrouping(Node source, string sourceGroup) { none() }
|
default predicate sourceGrouping(Node source, string sourceGroup) { none() }
|
||||||
|
|
||||||
/** Holds if sinks should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sinks should be grouped in the result of `flowPath`. */
|
||||||
default predicate sinkGrouping(Node sink, string sinkGroup) { none() }
|
default predicate sinkGrouping(Node sink, string sinkGroup) { none() }
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -166,10 +166,10 @@ signature module StateConfigSig {
|
|||||||
*/
|
*/
|
||||||
default FlowFeature getAFeature() { none() }
|
default FlowFeature getAFeature() { none() }
|
||||||
|
|
||||||
/** Holds if sources should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sources should be grouped in the result of `flowPath`. */
|
||||||
default predicate sourceGrouping(Node source, string sourceGroup) { none() }
|
default predicate sourceGrouping(Node source, string sourceGroup) { none() }
|
||||||
|
|
||||||
/** Holds if sinks should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sinks should be grouped in the result of `flowPath`. */
|
||||||
default predicate sinkGrouping(Node sink, string sinkGroup) { none() }
|
default predicate sinkGrouping(Node sink, string sinkGroup) { none() }
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -182,15 +182,15 @@ signature module StateConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Gets the exploration limit for `hasPartialFlow` and `hasPartialFlowRev`
|
* Gets the exploration limit for `partialFlow` and `partialFlowRev`
|
||||||
* measured in approximate number of interprocedural steps.
|
* measured in approximate number of interprocedural steps.
|
||||||
*/
|
*/
|
||||||
signature int explorationLimitSig();
|
signature int explorationLimitSig();
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* The output of a data flow computation.
|
* The output of a global data flow computation.
|
||||||
*/
|
*/
|
||||||
signature module DataFlowSig {
|
signature module GlobalFlowSig {
|
||||||
/**
|
/**
|
||||||
* A `Node` augmented with a call context (except for sinks) and an access path.
|
* A `Node` augmented with a call context (except for sinks) and an access path.
|
||||||
* Only those `PathNode`s that are reachable from a source, and which can reach a sink, are generated.
|
* Only those `PathNode`s that are reachable from a source, and which can reach a sink, are generated.
|
||||||
@@ -203,28 +203,28 @@ signature module DataFlowSig {
|
|||||||
* The corresponding paths are generated from the end-points and the graph
|
* The corresponding paths are generated from the end-points and the graph
|
||||||
* included in the module `PathGraph`.
|
* included in the module `PathGraph`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowPath(PathNode source, PathNode sink);
|
predicate flowPath(PathNode source, PathNode sink);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if data can flow from `source` to `sink`.
|
* Holds if data can flow from `source` to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlow(Node source, Node sink);
|
predicate flow(Node source, Node sink);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if data can flow from some source to `sink`.
|
* Holds if data can flow from some source to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowTo(Node sink);
|
predicate flowTo(Node sink);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if data can flow from some source to `sink`.
|
* Holds if data can flow from some source to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowToExpr(DataFlowExpr sink);
|
predicate flowToExpr(DataFlowExpr sink);
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Constructs a standard data flow computation.
|
* Constructs a global data flow computation.
|
||||||
*/
|
*/
|
||||||
module Make<ConfigSig Config> implements DataFlowSig {
|
module Global<ConfigSig Config> implements GlobalFlowSig {
|
||||||
private module C implements FullStateConfigSig {
|
private module C implements FullStateConfigSig {
|
||||||
import DefaultState<Config>
|
import DefaultState<Config>
|
||||||
import Config
|
import Config
|
||||||
@@ -233,10 +233,15 @@ module Make<ConfigSig Config> implements DataFlowSig {
|
|||||||
import Impl<C>
|
import Impl<C>
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `Global` instead. */
|
||||||
|
deprecated module Make<ConfigSig Config> implements GlobalFlowSig {
|
||||||
|
import Global<Config>
|
||||||
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Constructs a data flow computation using flow state.
|
* Constructs a global data flow computation using flow state.
|
||||||
*/
|
*/
|
||||||
module MakeWithState<StateConfigSig Config> implements DataFlowSig {
|
module GlobalWithState<StateConfigSig Config> implements GlobalFlowSig {
|
||||||
private module C implements FullStateConfigSig {
|
private module C implements FullStateConfigSig {
|
||||||
import Config
|
import Config
|
||||||
}
|
}
|
||||||
@@ -244,6 +249,11 @@ module MakeWithState<StateConfigSig Config> implements DataFlowSig {
|
|||||||
import Impl<C>
|
import Impl<C>
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `GlobalWithState` instead. */
|
||||||
|
deprecated module MakeWithState<StateConfigSig Config> implements GlobalFlowSig {
|
||||||
|
import GlobalWithState<Config>
|
||||||
|
}
|
||||||
|
|
||||||
signature class PathNodeSig {
|
signature class PathNodeSig {
|
||||||
/** Gets a textual representation of this element. */
|
/** Gets a textual representation of this element. */
|
||||||
string toString();
|
string toString();
|
||||||
|
|||||||
@@ -8,6 +8,7 @@ private import DataFlowImplCommon
|
|||||||
private import DataFlowImplSpecific::Private
|
private import DataFlowImplSpecific::Private
|
||||||
private import DataFlowImplSpecific::Public
|
private import DataFlowImplSpecific::Public
|
||||||
private import DataFlowImplCommonPublic
|
private import DataFlowImplCommonPublic
|
||||||
|
private import codeql.util.Unit
|
||||||
import DataFlow
|
import DataFlow
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -91,10 +92,10 @@ signature module FullStateConfigSig {
|
|||||||
*/
|
*/
|
||||||
FlowFeature getAFeature();
|
FlowFeature getAFeature();
|
||||||
|
|
||||||
/** Holds if sources should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sources should be grouped in the result of `flowPath`. */
|
||||||
predicate sourceGrouping(Node source, string sourceGroup);
|
predicate sourceGrouping(Node source, string sourceGroup);
|
||||||
|
|
||||||
/** Holds if sinks should be grouped in the result of `hasFlowPath`. */
|
/** Holds if sinks should be grouped in the result of `flowPath`. */
|
||||||
predicate sinkGrouping(Node sink, string sinkGroup);
|
predicate sinkGrouping(Node sink, string sinkGroup);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -445,11 +446,7 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private module Stage1 implements StageSig {
|
private module Stage1 implements StageSig {
|
||||||
class Ap extends int {
|
class Ap = Unit;
|
||||||
// workaround for bad functionality-induced joins (happens when using `Unit`)
|
|
||||||
pragma[nomagic]
|
|
||||||
Ap() { this in [0 .. 1] and this < 1 }
|
|
||||||
}
|
|
||||||
|
|
||||||
private class Cc = boolean;
|
private class Cc = boolean;
|
||||||
|
|
||||||
@@ -3633,7 +3630,7 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
* The corresponding paths are generated from the end-points and the graph
|
* The corresponding paths are generated from the end-points and the graph
|
||||||
* included in the module `PathGraph`.
|
* included in the module `PathGraph`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowPath(PathNode source, PathNode sink) {
|
predicate flowPath(PathNode source, PathNode sink) {
|
||||||
exists(PathNodeImpl flowsource, PathNodeImpl flowsink |
|
exists(PathNodeImpl flowsource, PathNodeImpl flowsink |
|
||||||
source = flowsource and sink = flowsink
|
source = flowsource and sink = flowsink
|
||||||
|
|
|
|
||||||
@@ -3643,6 +3640,9 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `flowPath` instead. */
|
||||||
|
deprecated predicate hasFlowPath = flowPath/2;
|
||||||
|
|
||||||
private predicate flowsTo(PathNodeImpl flowsource, PathNodeSink flowsink, Node source, Node sink) {
|
private predicate flowsTo(PathNodeImpl flowsource, PathNodeSink flowsink, Node source, Node sink) {
|
||||||
flowsource.isSource() and
|
flowsource.isSource() and
|
||||||
flowsource.getNodeEx().asNode() = source and
|
flowsource.getNodeEx().asNode() = source and
|
||||||
@@ -3653,17 +3653,26 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
/**
|
/**
|
||||||
* Holds if data can flow from `source` to `sink`.
|
* Holds if data can flow from `source` to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlow(Node source, Node sink) { flowsTo(_, _, source, sink) }
|
predicate flow(Node source, Node sink) { flowsTo(_, _, source, sink) }
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `flow` instead. */
|
||||||
|
deprecated predicate hasFlow = flow/2;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if data can flow from some source to `sink`.
|
* Holds if data can flow from some source to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowTo(Node sink) { sink = any(PathNodeSink n).getNodeEx().asNode() }
|
predicate flowTo(Node sink) { sink = any(PathNodeSink n).getNodeEx().asNode() }
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `flowTo` instead. */
|
||||||
|
deprecated predicate hasFlowTo = flowTo/1;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if data can flow from some source to `sink`.
|
* Holds if data can flow from some source to `sink`.
|
||||||
*/
|
*/
|
||||||
predicate hasFlowToExpr(DataFlowExpr sink) { hasFlowTo(exprNode(sink)) }
|
predicate flowToExpr(DataFlowExpr sink) { flowTo(exprNode(sink)) }
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `flowToExpr` instead. */
|
||||||
|
deprecated predicate hasFlowToExpr = flowToExpr/1;
|
||||||
|
|
||||||
private predicate finalStats(
|
private predicate finalStats(
|
||||||
boolean fwd, int nodes, int fields, int conscand, int states, int tuples
|
boolean fwd, int nodes, int fields, int conscand, int states, int tuples
|
||||||
@@ -4574,7 +4583,7 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
*
|
*
|
||||||
* To use this in a `path-problem` query, import the module `PartialPathGraph`.
|
* To use this in a `path-problem` query, import the module `PartialPathGraph`.
|
||||||
*/
|
*/
|
||||||
predicate hasPartialFlow(PartialPathNode source, PartialPathNode node, int dist) {
|
predicate partialFlow(PartialPathNode source, PartialPathNode node, int dist) {
|
||||||
partialFlow(source, node) and
|
partialFlow(source, node) and
|
||||||
dist = node.getSourceDistance()
|
dist = node.getSourceDistance()
|
||||||
}
|
}
|
||||||
@@ -4594,7 +4603,7 @@ module Impl<FullStateConfigSig Config> {
|
|||||||
* Note that reverse flow has slightly lower precision than the corresponding
|
* Note that reverse flow has slightly lower precision than the corresponding
|
||||||
* forward flow, as reverse flow disregards type pruning among other features.
|
* forward flow, as reverse flow disregards type pruning among other features.
|
||||||
*/
|
*/
|
||||||
predicate hasPartialFlowRev(PartialPathNode node, PartialPathNode sink, int dist) {
|
predicate partialFlowRev(PartialPathNode node, PartialPathNode sink, int dist) {
|
||||||
revPartialFlow(node, sink) and
|
revPartialFlow(node, sink) and
|
||||||
dist = node.getSinkDistance()
|
dist = node.getSinkDistance()
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
/**
|
/**
|
||||||
* DEPRECATED: Use `Make` and `MakeWithState` instead.
|
* DEPRECATED: Use `Global` and `GlobalWithState` instead.
|
||||||
*
|
*
|
||||||
* Provides a `Configuration` class backwards-compatible interface to the data
|
* Provides a `Configuration` class backwards-compatible interface to the data
|
||||||
* flow library.
|
* flow library.
|
||||||
@@ -11,6 +11,7 @@ import DataFlowImplSpecific::Public
|
|||||||
private import DataFlowImpl
|
private import DataFlowImpl
|
||||||
import DataFlowImplCommonPublic
|
import DataFlowImplCommonPublic
|
||||||
import FlowStateString
|
import FlowStateString
|
||||||
|
private import codeql.util.Unit
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A configuration of interprocedural data flow analysis. This defines
|
* A configuration of interprocedural data flow analysis. This defines
|
||||||
@@ -328,7 +329,6 @@ private module Config implements FullStateConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private import Impl<Config> as I
|
private import Impl<Config> as I
|
||||||
import I
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
||||||
@@ -379,6 +379,8 @@ class PathNode instanceof I::PathNode {
|
|||||||
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
module PathGraph = I::PathGraph;
|
||||||
|
|
||||||
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
||||||
exists(PathNode source0, PathNode sink0 |
|
exists(PathNode source0, PathNode sink0 |
|
||||||
hasFlowPath(source0, sink0, config) and
|
hasFlowPath(source0, sink0, config) and
|
||||||
@@ -388,7 +390,7 @@ private predicate hasFlow(Node source, Node sink, Configuration config) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
||||||
hasFlowPath(source, sink) and source.getConfiguration() = config
|
I::flowPath(source, sink) and source.getConfiguration() = config
|
||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
/**
|
/**
|
||||||
* DEPRECATED: Use `Make` and `MakeWithState` instead.
|
* DEPRECATED: Use `Global` and `GlobalWithState` instead.
|
||||||
*
|
*
|
||||||
* Provides a `Configuration` class backwards-compatible interface to the data
|
* Provides a `Configuration` class backwards-compatible interface to the data
|
||||||
* flow library.
|
* flow library.
|
||||||
@@ -11,6 +11,7 @@ import DataFlowImplSpecific::Public
|
|||||||
private import DataFlowImpl
|
private import DataFlowImpl
|
||||||
import DataFlowImplCommonPublic
|
import DataFlowImplCommonPublic
|
||||||
import FlowStateString
|
import FlowStateString
|
||||||
|
private import codeql.util.Unit
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A configuration of interprocedural data flow analysis. This defines
|
* A configuration of interprocedural data flow analysis. This defines
|
||||||
@@ -328,7 +329,6 @@ private module Config implements FullStateConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private import Impl<Config> as I
|
private import Impl<Config> as I
|
||||||
import I
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
||||||
@@ -379,6 +379,8 @@ class PathNode instanceof I::PathNode {
|
|||||||
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
module PathGraph = I::PathGraph;
|
||||||
|
|
||||||
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
||||||
exists(PathNode source0, PathNode sink0 |
|
exists(PathNode source0, PathNode sink0 |
|
||||||
hasFlowPath(source0, sink0, config) and
|
hasFlowPath(source0, sink0, config) and
|
||||||
@@ -388,7 +390,7 @@ private predicate hasFlow(Node source, Node sink, Configuration config) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
||||||
hasFlowPath(source, sink) and source.getConfiguration() = config
|
I::flowPath(source, sink) and source.getConfiguration() = config
|
||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
/**
|
/**
|
||||||
* DEPRECATED: Use `Make` and `MakeWithState` instead.
|
* DEPRECATED: Use `Global` and `GlobalWithState` instead.
|
||||||
*
|
*
|
||||||
* Provides a `Configuration` class backwards-compatible interface to the data
|
* Provides a `Configuration` class backwards-compatible interface to the data
|
||||||
* flow library.
|
* flow library.
|
||||||
@@ -11,6 +11,7 @@ import DataFlowImplSpecific::Public
|
|||||||
private import DataFlowImpl
|
private import DataFlowImpl
|
||||||
import DataFlowImplCommonPublic
|
import DataFlowImplCommonPublic
|
||||||
import FlowStateString
|
import FlowStateString
|
||||||
|
private import codeql.util.Unit
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A configuration of interprocedural data flow analysis. This defines
|
* A configuration of interprocedural data flow analysis. This defines
|
||||||
@@ -328,7 +329,6 @@ private module Config implements FullStateConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private import Impl<Config> as I
|
private import Impl<Config> as I
|
||||||
import I
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
||||||
@@ -379,6 +379,8 @@ class PathNode instanceof I::PathNode {
|
|||||||
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
module PathGraph = I::PathGraph;
|
||||||
|
|
||||||
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
||||||
exists(PathNode source0, PathNode sink0 |
|
exists(PathNode source0, PathNode sink0 |
|
||||||
hasFlowPath(source0, sink0, config) and
|
hasFlowPath(source0, sink0, config) and
|
||||||
@@ -388,7 +390,7 @@ private predicate hasFlow(Node source, Node sink, Configuration config) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
||||||
hasFlowPath(source, sink) and source.getConfiguration() = config
|
I::flowPath(source, sink) and source.getConfiguration() = config
|
||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
/**
|
/**
|
||||||
* DEPRECATED: Use `Make` and `MakeWithState` instead.
|
* DEPRECATED: Use `Global` and `GlobalWithState` instead.
|
||||||
*
|
*
|
||||||
* Provides a `Configuration` class backwards-compatible interface to the data
|
* Provides a `Configuration` class backwards-compatible interface to the data
|
||||||
* flow library.
|
* flow library.
|
||||||
@@ -11,6 +11,7 @@ import DataFlowImplSpecific::Public
|
|||||||
private import DataFlowImpl
|
private import DataFlowImpl
|
||||||
import DataFlowImplCommonPublic
|
import DataFlowImplCommonPublic
|
||||||
import FlowStateString
|
import FlowStateString
|
||||||
|
private import codeql.util.Unit
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A configuration of interprocedural data flow analysis. This defines
|
* A configuration of interprocedural data flow analysis. This defines
|
||||||
@@ -328,7 +329,6 @@ private module Config implements FullStateConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private import Impl<Config> as I
|
private import Impl<Config> as I
|
||||||
import I
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
* A `Node` augmented with a call context (except for sinks), an access path, and a configuration.
|
||||||
@@ -379,6 +379,8 @@ class PathNode instanceof I::PathNode {
|
|||||||
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
final predicate isSinkGroup(string group) { super.isSinkGroup(group) }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
module PathGraph = I::PathGraph;
|
||||||
|
|
||||||
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
private predicate hasFlow(Node source, Node sink, Configuration config) {
|
||||||
exists(PathNode source0, PathNode sink0 |
|
exists(PathNode source0, PathNode sink0 |
|
||||||
hasFlowPath(source0, sink0, config) and
|
hasFlowPath(source0, sink0, config) and
|
||||||
@@ -388,7 +390,7 @@ private predicate hasFlow(Node source, Node sink, Configuration config) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
private predicate hasFlowPath(PathNode source, PathNode sink, Configuration config) {
|
||||||
hasFlowPath(source, sink) and source.getConfiguration() = config
|
I::flowPath(source, sink) and source.getConfiguration() = config
|
||||||
}
|
}
|
||||||
|
|
||||||
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
private predicate hasFlowTo(Node sink, Configuration config) { hasFlow(_, sink, config) }
|
||||||
|
|||||||
@@ -140,10 +140,8 @@ private module LambdaFlow {
|
|||||||
}
|
}
|
||||||
|
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
private TReturnPositionSimple viableReturnPosLambda(
|
private TReturnPositionSimple viableReturnPosLambda(DataFlowCall call, ReturnKind kind) {
|
||||||
DataFlowCall call, DataFlowCallOption lastCall, ReturnKind kind
|
result = TReturnPositionSimple0(viableCallableLambda(call, _), kind)
|
||||||
) {
|
|
||||||
result = TReturnPositionSimple0(viableCallableLambda(call, lastCall), kind)
|
|
||||||
}
|
}
|
||||||
|
|
||||||
private predicate viableReturnPosOutNonLambda(
|
private predicate viableReturnPosOutNonLambda(
|
||||||
@@ -155,11 +153,12 @@ private module LambdaFlow {
|
|||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[nomagic]
|
||||||
private predicate viableReturnPosOutLambda(
|
private predicate viableReturnPosOutLambda(
|
||||||
DataFlowCall call, DataFlowCallOption lastCall, TReturnPositionSimple pos, OutNode out
|
DataFlowCall call, TReturnPositionSimple pos, OutNode out
|
||||||
) {
|
) {
|
||||||
exists(ReturnKind kind |
|
exists(ReturnKind kind |
|
||||||
pos = viableReturnPosLambda(call, lastCall, kind) and
|
pos = viableReturnPosLambda(call, kind) and
|
||||||
out = getAnOutNode(call, kind)
|
out = getAnOutNode(call, kind)
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
@@ -188,6 +187,7 @@ private module LambdaFlow {
|
|||||||
else any()
|
else any()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
predicate revLambdaFlow0(
|
predicate revLambdaFlow0(
|
||||||
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
|
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
|
||||||
@@ -274,6 +274,7 @@ private module LambdaFlow {
|
|||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pragma[assume_small_delta]
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
predicate revLambdaFlowOut(
|
predicate revLambdaFlowOut(
|
||||||
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
|
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
|
||||||
@@ -285,7 +286,7 @@ private module LambdaFlow {
|
|||||||
or
|
or
|
||||||
// non-linear recursion
|
// non-linear recursion
|
||||||
revLambdaFlowOutLambdaCall(lambdaCall, kind, out, t, toJump, call, lastCall) and
|
revLambdaFlowOutLambdaCall(lambdaCall, kind, out, t, toJump, call, lastCall) and
|
||||||
viableReturnPosOutLambda(call, _, pos, out)
|
viableReturnPosOutLambda(call, pos, out)
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@@ -6,6 +6,7 @@ private import DataFlowImplConsistency
|
|||||||
private import semmle.code.cpp.ir.internal.IRCppLanguage
|
private import semmle.code.cpp.ir.internal.IRCppLanguage
|
||||||
private import SsaInternals as Ssa
|
private import SsaInternals as Ssa
|
||||||
private import DataFlowImplCommon as DataFlowImplCommon
|
private import DataFlowImplCommon as DataFlowImplCommon
|
||||||
|
private import codeql.util.Unit
|
||||||
|
|
||||||
cached
|
cached
|
||||||
private module Cached {
|
private module Cached {
|
||||||
@@ -799,15 +800,6 @@ int accessPathLimit() { result = 5 }
|
|||||||
*/
|
*/
|
||||||
predicate forceHighPrecision(Content c) { none() }
|
predicate forceHighPrecision(Content c) { none() }
|
||||||
|
|
||||||
/** The unit type. */
|
|
||||||
private newtype TUnit = TMkUnit()
|
|
||||||
|
|
||||||
/** The trivial type with a single element. */
|
|
||||||
class Unit extends TUnit {
|
|
||||||
/** Gets a textual representation of this element. */
|
|
||||||
string toString() { result = "unit" }
|
|
||||||
}
|
|
||||||
|
|
||||||
/** Holds if `n` should be hidden from path explanations. */
|
/** Holds if `n` should be hidden from path explanations. */
|
||||||
predicate nodeIsHidden(Node n) {
|
predicate nodeIsHidden(Node n) {
|
||||||
n instanceof OperandNode and
|
n instanceof OperandNode and
|
||||||
|
|||||||
@@ -103,7 +103,7 @@ private module DefaultTaintTrackingConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
private module DefaultTaintTrackingFlow = TaintTracking::Make<DefaultTaintTrackingConfig>;
|
private module DefaultTaintTrackingFlow = TaintTracking::Global<DefaultTaintTrackingConfig>;
|
||||||
|
|
||||||
private module ToGlobalVarTaintTrackingConfig implements DataFlow::ConfigSig {
|
private module ToGlobalVarTaintTrackingConfig implements DataFlow::ConfigSig {
|
||||||
predicate isSource(DataFlow::Node source) { source = getNodeForSource(_) }
|
predicate isSource(DataFlow::Node source) { source = getNodeForSource(_) }
|
||||||
@@ -121,13 +121,13 @@ private module ToGlobalVarTaintTrackingConfig implements DataFlow::ConfigSig {
|
|||||||
predicate isBarrierIn(DataFlow::Node node) { nodeIsBarrierIn(node) }
|
predicate isBarrierIn(DataFlow::Node node) { nodeIsBarrierIn(node) }
|
||||||
}
|
}
|
||||||
|
|
||||||
private module ToGlobalVarTaintTrackingFlow = TaintTracking::Make<ToGlobalVarTaintTrackingConfig>;
|
private module ToGlobalVarTaintTrackingFlow = TaintTracking::Global<ToGlobalVarTaintTrackingConfig>;
|
||||||
|
|
||||||
private module FromGlobalVarTaintTrackingConfig implements DataFlow::ConfigSig {
|
private module FromGlobalVarTaintTrackingConfig implements DataFlow::ConfigSig {
|
||||||
predicate isSource(DataFlow::Node source) {
|
predicate isSource(DataFlow::Node source) {
|
||||||
// This set of sources should be reasonably small, which is good for
|
// This set of sources should be reasonably small, which is good for
|
||||||
// performance since the set of sinks is very large.
|
// performance since the set of sinks is very large.
|
||||||
ToGlobalVarTaintTrackingFlow::hasFlowTo(source)
|
ToGlobalVarTaintTrackingFlow::flowTo(source)
|
||||||
}
|
}
|
||||||
|
|
||||||
predicate isSink(DataFlow::Node sink) { exists(adjustedSink(sink)) }
|
predicate isSink(DataFlow::Node sink) { exists(adjustedSink(sink)) }
|
||||||
@@ -145,7 +145,7 @@ private module FromGlobalVarTaintTrackingConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private module FromGlobalVarTaintTrackingFlow =
|
private module FromGlobalVarTaintTrackingFlow =
|
||||||
TaintTracking::Make<FromGlobalVarTaintTrackingConfig>;
|
TaintTracking::Global<FromGlobalVarTaintTrackingConfig>;
|
||||||
|
|
||||||
private predicate readsVariable(LoadInstruction load, Variable var) {
|
private predicate readsVariable(LoadInstruction load, Variable var) {
|
||||||
load.getSourceAddress().(VariableAddressInstruction).getAstVariable() = var
|
load.getSourceAddress().(VariableAddressInstruction).getAstVariable() = var
|
||||||
@@ -331,7 +331,7 @@ private import Cached
|
|||||||
cached
|
cached
|
||||||
predicate tainted(Expr source, Element tainted) {
|
predicate tainted(Expr source, Element tainted) {
|
||||||
exists(DataFlow::Node sink |
|
exists(DataFlow::Node sink |
|
||||||
DefaultTaintTrackingFlow::hasFlow(getNodeForSource(source), sink) and
|
DefaultTaintTrackingFlow::flow(getNodeForSource(source), sink) and
|
||||||
tainted = adjustedSink(sink)
|
tainted = adjustedSink(sink)
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
@@ -360,8 +360,8 @@ predicate taintedIncludingGlobalVars(Expr source, Element tainted, string global
|
|||||||
DataFlow::VariableNode variableNode, GlobalOrNamespaceVariable global, DataFlow::Node sink
|
DataFlow::VariableNode variableNode, GlobalOrNamespaceVariable global, DataFlow::Node sink
|
||||||
|
|
|
|
||||||
global = variableNode.getVariable() and
|
global = variableNode.getVariable() and
|
||||||
ToGlobalVarTaintTrackingFlow::hasFlow(getNodeForSource(source), variableNode) and
|
ToGlobalVarTaintTrackingFlow::flow(getNodeForSource(source), variableNode) and
|
||||||
FromGlobalVarTaintTrackingFlow::hasFlow(variableNode, sink) and
|
FromGlobalVarTaintTrackingFlow::flow(variableNode, sink) and
|
||||||
tainted = adjustedSink(sink) and
|
tainted = adjustedSink(sink) and
|
||||||
global = globalVarFromId(globalVar)
|
global = globalVarFromId(globalVar)
|
||||||
)
|
)
|
||||||
@@ -450,7 +450,7 @@ module TaintedWithPath {
|
|||||||
predicate isBarrierIn(DataFlow::Node node) { nodeIsBarrierIn(node) }
|
predicate isBarrierIn(DataFlow::Node node) { nodeIsBarrierIn(node) }
|
||||||
}
|
}
|
||||||
|
|
||||||
private module AdjustedFlow = TaintTracking::Make<AdjustedConfig>;
|
private module AdjustedFlow = TaintTracking::Global<AdjustedConfig>;
|
||||||
|
|
||||||
/*
|
/*
|
||||||
* A sink `Element` may map to multiple `DataFlowX::PathNode`s via (the
|
* A sink `Element` may map to multiple `DataFlowX::PathNode`s via (the
|
||||||
@@ -472,7 +472,7 @@ module TaintedWithPath {
|
|||||||
// that makes it easiest to deal with the case where source = sink.
|
// that makes it easiest to deal with the case where source = sink.
|
||||||
TEndpointPathNode(Element e) {
|
TEndpointPathNode(Element e) {
|
||||||
exists(DataFlow::Node sourceNode, DataFlow::Node sinkNode |
|
exists(DataFlow::Node sourceNode, DataFlow::Node sinkNode |
|
||||||
AdjustedFlow::hasFlow(sourceNode, sinkNode)
|
AdjustedFlow::flow(sourceNode, sinkNode)
|
||||||
|
|
|
|
||||||
sourceNode = getNodeForExpr(e) and
|
sourceNode = getNodeForExpr(e) and
|
||||||
exists(TaintTrackingConfiguration ttCfg | ttCfg.isSource(e))
|
exists(TaintTrackingConfiguration ttCfg | ttCfg.isSource(e))
|
||||||
@@ -634,7 +634,7 @@ module TaintedWithPath {
|
|||||||
exists(DataFlow::Node flowSource, DataFlow::Node flowSink |
|
exists(DataFlow::Node flowSource, DataFlow::Node flowSink |
|
||||||
source = sourceNode.(InitialPathNode).inner() and
|
source = sourceNode.(InitialPathNode).inner() and
|
||||||
flowSource = getNodeForExpr(source) and
|
flowSource = getNodeForExpr(source) and
|
||||||
AdjustedFlow::hasFlow(flowSource, flowSink) and
|
AdjustedFlow::flow(flowSource, flowSink) and
|
||||||
tainted = adjustedSink(flowSink) and
|
tainted = adjustedSink(flowSink) and
|
||||||
tainted = sinkNode.(FinalPathNode).inner()
|
tainted = sinkNode.(FinalPathNode).inner()
|
||||||
)
|
)
|
||||||
|
|||||||
@@ -33,9 +33,9 @@ private module AddTaintDefaults<DataFlowInternal::FullStateConfigSig Config> imp
|
|||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Constructs a standard taint tracking computation.
|
* Constructs a global taint tracking computation.
|
||||||
*/
|
*/
|
||||||
module Make<DataFlow::ConfigSig Config> implements DataFlow::DataFlowSig {
|
module Global<DataFlow::ConfigSig Config> implements DataFlow::GlobalFlowSig {
|
||||||
private module Config0 implements DataFlowInternal::FullStateConfigSig {
|
private module Config0 implements DataFlowInternal::FullStateConfigSig {
|
||||||
import DataFlowInternal::DefaultState<Config>
|
import DataFlowInternal::DefaultState<Config>
|
||||||
import Config
|
import Config
|
||||||
@@ -48,10 +48,15 @@ module Make<DataFlow::ConfigSig Config> implements DataFlow::DataFlowSig {
|
|||||||
import DataFlowInternal::Impl<C>
|
import DataFlowInternal::Impl<C>
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `Global` instead. */
|
||||||
|
deprecated module Make<DataFlow::ConfigSig Config> implements DataFlow::GlobalFlowSig {
|
||||||
|
import Global<Config>
|
||||||
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Constructs a taint tracking computation using flow state.
|
* Constructs a global taint tracking computation using flow state.
|
||||||
*/
|
*/
|
||||||
module MakeWithState<DataFlow::StateConfigSig Config> implements DataFlow::DataFlowSig {
|
module GlobalWithState<DataFlow::StateConfigSig Config> implements DataFlow::GlobalFlowSig {
|
||||||
private module Config0 implements DataFlowInternal::FullStateConfigSig {
|
private module Config0 implements DataFlowInternal::FullStateConfigSig {
|
||||||
import Config
|
import Config
|
||||||
}
|
}
|
||||||
@@ -62,3 +67,8 @@ module MakeWithState<DataFlow::StateConfigSig Config> implements DataFlow::DataF
|
|||||||
|
|
||||||
import DataFlowInternal::Impl<C>
|
import DataFlowInternal::Impl<C>
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/** DEPRECATED: Use `GlobalWithState` instead. */
|
||||||
|
deprecated module MakeWithState<DataFlow::StateConfigSig Config> implements DataFlow::GlobalFlowSig {
|
||||||
|
import GlobalWithState<Config>
|
||||||
|
}
|
||||||
|
|||||||
@@ -1105,3 +1105,49 @@ class TranslatedAsmStmt extends TranslatedStmt {
|
|||||||
)
|
)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
class TranslatedVlaDimensionStmt extends TranslatedStmt {
|
||||||
|
override VlaDimensionStmt stmt;
|
||||||
|
|
||||||
|
override TranslatedExpr getChild(int id) {
|
||||||
|
id = 0 and
|
||||||
|
result = getTranslatedExpr(stmt.getDimensionExpr().getFullyConverted())
|
||||||
|
}
|
||||||
|
|
||||||
|
override Instruction getFirstInstruction() { result = this.getChild(0).getFirstInstruction() }
|
||||||
|
|
||||||
|
override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
|
||||||
|
none()
|
||||||
|
}
|
||||||
|
|
||||||
|
override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
|
||||||
|
|
||||||
|
override Instruction getChildSuccessor(TranslatedElement child) {
|
||||||
|
child = this.getChild(0) and
|
||||||
|
result = this.getParent().getChildSuccessor(this)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
class TranslatedVlaDeclarationStmt extends TranslatedStmt {
|
||||||
|
override VlaDeclStmt stmt;
|
||||||
|
|
||||||
|
override TranslatedExpr getChild(int id) { none() }
|
||||||
|
|
||||||
|
override Instruction getFirstInstruction() { result = this.getInstruction(OnlyInstructionTag()) }
|
||||||
|
|
||||||
|
override predicate hasInstruction(Opcode opcode, InstructionTag tag, CppType resultType) {
|
||||||
|
// TODO: This needs a new kind of instruction that represents initialization of a VLA.
|
||||||
|
// For now we just emit a `NoOp` instruction so that the CFG isn't incomplete.
|
||||||
|
tag = OnlyInstructionTag() and
|
||||||
|
opcode instanceof Opcode::NoOp and
|
||||||
|
resultType = getVoidType()
|
||||||
|
}
|
||||||
|
|
||||||
|
override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
|
||||||
|
tag = OnlyInstructionTag() and
|
||||||
|
result = this.getParent().getChildSuccessor(this) and
|
||||||
|
kind instanceof GotoEdge
|
||||||
|
}
|
||||||
|
|
||||||
|
override Instruction getChildSuccessor(TranslatedElement child) { none() }
|
||||||
|
}
|
||||||
|
|||||||
@@ -29,7 +29,23 @@ abstract class BufferAccess extends Expr {
|
|||||||
*/
|
*/
|
||||||
abstract Expr getBuffer(string bufferDesc, int accessType);
|
abstract Expr getBuffer(string bufferDesc, int accessType);
|
||||||
|
|
||||||
abstract int getSize();
|
/**
|
||||||
|
* Gets the expression that represents the size of the buffer access. The
|
||||||
|
* actual size is typically the value of this expression multiplied by the
|
||||||
|
* result of `getSizeMult()`, in bytes.
|
||||||
|
*/
|
||||||
|
Expr getSizeExpr() { none() }
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Gets a constant multiplier for the buffer access size given by
|
||||||
|
* `getSizeExpr`, in bytes.
|
||||||
|
*/
|
||||||
|
int getSizeMult() { none() }
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Gets the buffer access size in bytes.
|
||||||
|
*/
|
||||||
|
int getSize() { result = this.getSizeExpr().getValue().toInt() * this.getSizeMult() }
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -63,10 +79,10 @@ class MemcpyBA extends BufferAccess {
|
|||||||
accessType = 1
|
accessType = 1
|
||||||
}
|
}
|
||||||
|
|
||||||
override int getSize() {
|
override Expr getSizeExpr() { result = this.(FunctionCall).getArgument(2) }
|
||||||
result =
|
|
||||||
this.(FunctionCall).getArgument(2).getValue().toInt() *
|
override int getSizeMult() {
|
||||||
getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
result = getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -89,10 +105,10 @@ class BCopyBA extends BufferAccess {
|
|||||||
accessType = 1
|
accessType = 1
|
||||||
}
|
}
|
||||||
|
|
||||||
override int getSize() {
|
override Expr getSizeExpr() { result = this.(FunctionCall).getArgument(2) }
|
||||||
result =
|
|
||||||
this.(FunctionCall).getArgument(2).getValue().toInt() *
|
override int getSizeMult() {
|
||||||
getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
result = getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -115,10 +131,10 @@ class StrncpyBA extends BufferAccess {
|
|||||||
accessType = 2
|
accessType = 2
|
||||||
}
|
}
|
||||||
|
|
||||||
override int getSize() {
|
override Expr getSizeExpr() { result = this.(FunctionCall).getArgument(2) }
|
||||||
result =
|
|
||||||
this.(FunctionCall).getArgument(2).getValue().toInt() *
|
override int getSizeMult() {
|
||||||
getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
result = getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -141,10 +157,10 @@ class MemccpyBA extends BufferAccess {
|
|||||||
accessType = 2
|
accessType = 2
|
||||||
}
|
}
|
||||||
|
|
||||||
override int getSize() {
|
override Expr getSizeExpr() { result = this.(FunctionCall).getArgument(3) }
|
||||||
result =
|
|
||||||
this.(FunctionCall).getArgument(3).getValue().toInt() *
|
override int getSizeMult() {
|
||||||
getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
result = getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -172,10 +188,10 @@ class MemcmpBA extends BufferAccess {
|
|||||||
accessType = 2
|
accessType = 2
|
||||||
}
|
}
|
||||||
|
|
||||||
override int getSize() {
|
override Expr getSizeExpr() { result = this.(FunctionCall).getArgument(2) }
|
||||||
result =
|
|
||||||
this.(FunctionCall).getArgument(2).getValue().toInt() *
|
override int getSizeMult() {
|
||||||
getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
result = getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -199,10 +215,10 @@ class SwabBA extends BufferAccess {
|
|||||||
accessType = 1
|
accessType = 1
|
||||||
}
|
}
|
||||||
|
|
||||||
override int getSize() {
|
override Expr getSizeExpr() { result = this.(FunctionCall).getArgument(2) }
|
||||||
result =
|
|
||||||
this.(FunctionCall).getArgument(2).getValue().toInt() *
|
override int getSizeMult() {
|
||||||
getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
result = getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -222,10 +238,10 @@ class MemsetBA extends BufferAccess {
|
|||||||
accessType = 1
|
accessType = 1
|
||||||
}
|
}
|
||||||
|
|
||||||
override int getSize() {
|
override Expr getSizeExpr() { result = this.(FunctionCall).getArgument(2) }
|
||||||
result =
|
|
||||||
this.(FunctionCall).getArgument(2).getValue().toInt() *
|
override int getSizeMult() {
|
||||||
getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
result = getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -244,7 +260,9 @@ class ZeroMemoryBA extends BufferAccess {
|
|||||||
accessType = 1
|
accessType = 1
|
||||||
}
|
}
|
||||||
|
|
||||||
override int getSize() { result = this.(FunctionCall).getArgument(1).getValue().toInt() }
|
override Expr getSizeExpr() { result = this.(FunctionCall).getArgument(1) }
|
||||||
|
|
||||||
|
override int getSizeMult() { result = 1 }
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -263,10 +281,10 @@ class MemchrBA extends BufferAccess {
|
|||||||
accessType = 2
|
accessType = 2
|
||||||
}
|
}
|
||||||
|
|
||||||
override int getSize() {
|
override Expr getSizeExpr() { result = this.(FunctionCall).getArgument(2) }
|
||||||
result =
|
|
||||||
this.(FunctionCall).getArgument(2).getValue().toInt() *
|
override int getSizeMult() {
|
||||||
getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
result = getPointedSize(this.(FunctionCall).getTarget().getParameter(0).getType())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -285,11 +303,9 @@ class FreadBA extends BufferAccess {
|
|||||||
accessType = 2
|
accessType = 2
|
||||||
}
|
}
|
||||||
|
|
||||||
override int getSize() {
|
override Expr getSizeExpr() { result = this.(FunctionCall).getArgument(1) }
|
||||||
result =
|
|
||||||
this.(FunctionCall).getArgument(1).getValue().toInt() *
|
override int getSizeMult() { result = this.(FunctionCall).getArgument(2).getValue().toInt() }
|
||||||
this.(FunctionCall).getArgument(2).getValue().toInt()
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -318,11 +334,13 @@ class ArrayExprBA extends BufferAccess {
|
|||||||
accessType = 3
|
accessType = 3
|
||||||
}
|
}
|
||||||
|
|
||||||
|
override Expr getSizeExpr() { result = this.(ArrayExpr).getArrayOffset() }
|
||||||
|
|
||||||
override int getSize() {
|
override int getSize() {
|
||||||
// byte size of the buffer that would be required to support this
|
// byte size of the buffer that would be required to support this
|
||||||
// access
|
// access
|
||||||
result =
|
result = (1 + this.getSizeExpr().getValue().toInt()) * this.getSizeMult()
|
||||||
(1 + this.(ArrayExpr).getArrayOffset().getValue().toInt()) *
|
|
||||||
this.(ArrayExpr).getType().getSize()
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
override int getSizeMult() { result = this.(ArrayExpr).getType().getSize() }
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -394,12 +394,12 @@ module BoostorgAsio {
|
|||||||
* Constructs a standard data flow computation for protocol values to the first argument
|
* Constructs a standard data flow computation for protocol values to the first argument
|
||||||
* of a context constructor.
|
* of a context constructor.
|
||||||
*/
|
*/
|
||||||
module SslContextCallMake<SslContextCallConfigSig Config> {
|
module SslContextCallGlobal<SslContextCallConfigSig Config> {
|
||||||
private module C implements DataFlow::ConfigSig {
|
private module C implements DataFlow::ConfigSig {
|
||||||
import Config
|
import Config
|
||||||
}
|
}
|
||||||
|
|
||||||
import DataFlow::Make<C>
|
import DataFlow::Global<C>
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
@@ -428,7 +428,7 @@ module BoostorgAsio {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module SslContextCallFlow = SslContextCallMake<SslContextCallConfig>;
|
module SslContextCallFlow = SslContextCallGlobal<SslContextCallConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A banned protocol value that flows to the first argument of a context constructor.
|
* A banned protocol value that flows to the first argument of a context constructor.
|
||||||
@@ -458,7 +458,8 @@ module BoostorgAsio {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module SslContextCallBannedProtocolFlow = SslContextCallMake<SslContextCallBannedProtocolConfig>;
|
module SslContextCallBannedProtocolFlow =
|
||||||
|
SslContextCallGlobal<SslContextCallBannedProtocolConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A TLS 1.2 protocol value that flows to the first argument of a context constructor.
|
* A TLS 1.2 protocol value that flows to the first argument of a context constructor.
|
||||||
@@ -488,7 +489,7 @@ module BoostorgAsio {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module SslContextCallTls12ProtocolFlow = SslContextCallMake<SslContextCallTls12ProtocolConfig>;
|
module SslContextCallTls12ProtocolFlow = SslContextCallGlobal<SslContextCallTls12ProtocolConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A TLS 1.3 protocol value that flows to the first argument of a context constructor.
|
* A TLS 1.3 protocol value that flows to the first argument of a context constructor.
|
||||||
@@ -518,7 +519,7 @@ module BoostorgAsio {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module SslContextCallTls13ProtocolFlow = SslContextCallMake<SslContextCallTls13ProtocolConfig>;
|
module SslContextCallTls13ProtocolFlow = SslContextCallGlobal<SslContextCallTls13ProtocolConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A generic TLS protocol value that flows to the first argument of a context constructor.
|
* A generic TLS protocol value that flows to the first argument of a context constructor.
|
||||||
@@ -548,7 +549,7 @@ module BoostorgAsio {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module SslContextCallTlsProtocolFlow = SslContextCallMake<SslContextCallTlsProtocolConfig>;
|
module SslContextCallTlsProtocolFlow = SslContextCallGlobal<SslContextCallTlsProtocolConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A context constructor call that flows to a call to `SetOptions()`.
|
* A context constructor call that flows to a call to `SetOptions()`.
|
||||||
@@ -596,7 +597,7 @@ module BoostorgAsio {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module SslContextFlowsToSetOptionFlow = DataFlow::Make<SslContextFlowsToSetOptionConfig>;
|
module SslContextFlowsToSetOptionFlow = DataFlow::Global<SslContextFlowsToSetOptionConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* An option value that flows to the first parameter of a call to `SetOptions()`.
|
* An option value that flows to the first parameter of a call to `SetOptions()`.
|
||||||
@@ -640,5 +641,5 @@ module BoostorgAsio {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module SslOptionFlow = DataFlow::Make<SslOptionConfig>;
|
module SslOptionFlow = DataFlow::Global<SslOptionConfig>;
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -84,11 +84,11 @@ module OverflowDestinationConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module OverflowDestination = TaintTracking::Make<OverflowDestinationConfig>;
|
module OverflowDestination = TaintTracking::Global<OverflowDestinationConfig>;
|
||||||
|
|
||||||
from FunctionCall fc, OverflowDestination::PathNode source, OverflowDestination::PathNode sink
|
from FunctionCall fc, OverflowDestination::PathNode source, OverflowDestination::PathNode sink
|
||||||
where
|
where
|
||||||
OverflowDestination::hasFlowPath(source, sink) and
|
OverflowDestination::flowPath(source, sink) and
|
||||||
sourceSized(fc, sink.getNode().asIndirectConvertedExpr())
|
sourceSized(fc, sink.getNode().asIndirectConvertedExpr())
|
||||||
select fc, source, sink,
|
select fc, source, sink,
|
||||||
"To avoid overflow, this operation should be bounded by destination-buffer size, not source-buffer size."
|
"To avoid overflow, this operation should be bounded by destination-buffer size, not source-buffer size."
|
||||||
|
|||||||
@@ -80,9 +80,9 @@ predicate introducesNewField(Class derived, Class base) {
|
|||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
module CastToPointerArithFlow = DataFlow::MakeWithState<CastToPointerArithFlowConfig>;
|
module CastToPointerArithFlow = DataFlow::GlobalWithState<CastToPointerArithFlowConfig>;
|
||||||
|
|
||||||
from CastToPointerArithFlow::PathNode source, CastToPointerArithFlow::PathNode sink
|
from CastToPointerArithFlow::PathNode source, CastToPointerArithFlow::PathNode sink
|
||||||
where CastToPointerArithFlow::hasFlowPath(source, sink)
|
where CastToPointerArithFlow::flowPath(source, sink)
|
||||||
select sink, source, sink, "This pointer arithmetic may be done with the wrong type because of $@.",
|
select sink, source, sink, "This pointer arithmetic may be done with the wrong type because of $@.",
|
||||||
source, "this cast"
|
source, "this cast"
|
||||||
|
|||||||
@@ -146,13 +146,13 @@ module NonConstFlowConfig implements DataFlow::ConfigSig {
|
|||||||
predicate isBarrier(DataFlow::Node node) { isBarrierNode(node) }
|
predicate isBarrier(DataFlow::Node node) { isBarrierNode(node) }
|
||||||
}
|
}
|
||||||
|
|
||||||
module NonConstFlow = TaintTracking::Make<NonConstFlowConfig>;
|
module NonConstFlow = TaintTracking::Global<NonConstFlowConfig>;
|
||||||
|
|
||||||
from FormattingFunctionCall call, Expr formatString
|
from FormattingFunctionCall call, Expr formatString
|
||||||
where
|
where
|
||||||
call.getArgument(call.getFormatParameterIndex()) = formatString and
|
call.getArgument(call.getFormatParameterIndex()) = formatString and
|
||||||
exists(DataFlow::Node sink |
|
exists(DataFlow::Node sink |
|
||||||
NonConstFlow::hasFlowTo(sink) and
|
NonConstFlow::flowTo(sink) and
|
||||||
isSinkImpl(sink, formatString)
|
isSinkImpl(sink, formatString)
|
||||||
)
|
)
|
||||||
select formatString,
|
select formatString,
|
||||||
|
|||||||
@@ -16,7 +16,7 @@ import LeapYear
|
|||||||
|
|
||||||
from Expr source, Expr sink
|
from Expr source, Expr sink
|
||||||
where
|
where
|
||||||
PossibleYearArithmeticOperationCheckFlow::hasFlow(DataFlow::exprNode(source),
|
PossibleYearArithmeticOperationCheckFlow::flow(DataFlow::exprNode(source),
|
||||||
DataFlow::exprNode(sink))
|
DataFlow::exprNode(sink))
|
||||||
select sink,
|
select sink,
|
||||||
"An arithmetic operation $@ that uses a constant value of 365 ends up modifying this date/time, without considering leap year scenarios.",
|
"An arithmetic operation $@ that uses a constant value of 365 ends up modifying this date/time, without considering leap year scenarios.",
|
||||||
|
|||||||
@@ -231,7 +231,7 @@ private module LeapYearCheckConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module LeapYearCheckFlow = DataFlow::Make<LeapYearCheckConfig>;
|
module LeapYearCheckFlow = DataFlow::Global<LeapYearCheckConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Data flow configuration for finding an operation with hardcoded 365 that will flow into
|
* Data flow configuration for finding an operation with hardcoded 365 that will flow into
|
||||||
@@ -284,7 +284,7 @@ private module FiletimeYearArithmeticOperationCheckConfig implements DataFlow::C
|
|||||||
}
|
}
|
||||||
|
|
||||||
module FiletimeYearArithmeticOperationCheckFlow =
|
module FiletimeYearArithmeticOperationCheckFlow =
|
||||||
DataFlow::Make<FiletimeYearArithmeticOperationCheckConfig>;
|
DataFlow::Global<FiletimeYearArithmeticOperationCheckConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Taint configuration for finding an operation with hardcoded 365 that will flow into any known date/time field.
|
* Taint configuration for finding an operation with hardcoded 365 that will flow into any known date/time field.
|
||||||
@@ -372,4 +372,4 @@ private module PossibleYearArithmeticOperationCheckConfig implements DataFlow::C
|
|||||||
}
|
}
|
||||||
|
|
||||||
module PossibleYearArithmeticOperationCheckFlow =
|
module PossibleYearArithmeticOperationCheckFlow =
|
||||||
TaintTracking::Make<PossibleYearArithmeticOperationCheckConfig>;
|
TaintTracking::Global<PossibleYearArithmeticOperationCheckConfig>;
|
||||||
|
|||||||
@@ -31,16 +31,14 @@ where
|
|||||||
// If there is a data flow from the variable that was modified to a function that seems to check for leap year
|
// If there is a data flow from the variable that was modified to a function that seems to check for leap year
|
||||||
exists(VariableAccess source, ChecksForLeapYearFunctionCall fc |
|
exists(VariableAccess source, ChecksForLeapYearFunctionCall fc |
|
||||||
source = var.getAnAccess() and
|
source = var.getAnAccess() and
|
||||||
LeapYearCheckFlow::hasFlow(DataFlow::exprNode(source),
|
LeapYearCheckFlow::flow(DataFlow::exprNode(source), DataFlow::exprNode(fc.getAnArgument()))
|
||||||
DataFlow::exprNode(fc.getAnArgument()))
|
|
||||||
)
|
)
|
||||||
or
|
or
|
||||||
// If there is a data flow from the field that was modified to a function that seems to check for leap year
|
// If there is a data flow from the field that was modified to a function that seems to check for leap year
|
||||||
exists(VariableAccess vacheck, YearFieldAccess yfacheck, ChecksForLeapYearFunctionCall fc |
|
exists(VariableAccess vacheck, YearFieldAccess yfacheck, ChecksForLeapYearFunctionCall fc |
|
||||||
vacheck = var.getAnAccess() and
|
vacheck = var.getAnAccess() and
|
||||||
yfacheck.getQualifier() = vacheck and
|
yfacheck.getQualifier() = vacheck and
|
||||||
LeapYearCheckFlow::hasFlow(DataFlow::exprNode(yfacheck),
|
LeapYearCheckFlow::flow(DataFlow::exprNode(yfacheck), DataFlow::exprNode(fc.getAnArgument()))
|
||||||
DataFlow::exprNode(fc.getAnArgument()))
|
|
||||||
)
|
)
|
||||||
or
|
or
|
||||||
// If there is a successor or predecessor that sets the month = 1
|
// If there is a successor or predecessor that sets the month = 1
|
||||||
|
|||||||
@@ -12,5 +12,5 @@ import cpp
|
|||||||
import NtohlArrayNoBound
|
import NtohlArrayNoBound
|
||||||
|
|
||||||
from DataFlow::Node source, DataFlow::Node sink
|
from DataFlow::Node source, DataFlow::Node sink
|
||||||
where NetworkToBufferSizeFlow::hasFlow(source, sink)
|
where NetworkToBufferSizeFlow::flow(source, sink)
|
||||||
select sink, "Unchecked use of data from network function $@.", source, source.toString()
|
select sink, "Unchecked use of data from network function $@.", source, source.toString()
|
||||||
|
|||||||
@@ -161,4 +161,4 @@ private module NetworkToBufferSizeConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module NetworkToBufferSizeFlow = DataFlow::Make<NetworkToBufferSizeConfig>;
|
module NetworkToBufferSizeFlow = DataFlow::Global<NetworkToBufferSizeConfig>;
|
||||||
|
|||||||
@@ -25,17 +25,17 @@ module ExistsAnyFlowConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module ExistsAnyFlow = DataFlow::Make<ExistsAnyFlowConfig>;
|
module ExistsAnyFlow = DataFlow::Global<ExistsAnyFlowConfig>;
|
||||||
|
|
||||||
bindingset[flag]
|
bindingset[flag]
|
||||||
predicate isOptionSet(ConstructorCall cc, int flag, FunctionCall fcSetOptions) {
|
predicate isOptionSet(ConstructorCall cc, int flag, FunctionCall fcSetOptions) {
|
||||||
exists(VariableAccess contextSetOptions |
|
exists(VariableAccess contextSetOptions |
|
||||||
ExistsAnyFlow::hasFlow(DataFlow::exprNode(cc), DataFlow::exprNode(contextSetOptions)) and
|
ExistsAnyFlow::flow(DataFlow::exprNode(cc), DataFlow::exprNode(contextSetOptions)) and
|
||||||
exists(BoostorgAsio::SslSetOptionsFunction f | f.getACallToThisFunction() = fcSetOptions |
|
exists(BoostorgAsio::SslSetOptionsFunction f | f.getACallToThisFunction() = fcSetOptions |
|
||||||
contextSetOptions = fcSetOptions.getQualifier() and
|
contextSetOptions = fcSetOptions.getQualifier() and
|
||||||
forall(Expr optionArgument, Expr optionArgumentSource |
|
forall(Expr optionArgument, Expr optionArgumentSource |
|
||||||
optionArgument = fcSetOptions.getArgument(0) and
|
optionArgument = fcSetOptions.getArgument(0) and
|
||||||
BoostorgAsio::SslOptionFlow::hasFlow(DataFlow::exprNode(optionArgumentSource),
|
BoostorgAsio::SslOptionFlow::flow(DataFlow::exprNode(optionArgumentSource),
|
||||||
DataFlow::exprNode(optionArgument))
|
DataFlow::exprNode(optionArgument))
|
||||||
|
|
|
|
||||||
optionArgument.getValue().toInt().bitShiftRight(16).bitAnd(flag) = flag
|
optionArgument.getValue().toInt().bitShiftRight(16).bitAnd(flag) = flag
|
||||||
@@ -49,7 +49,7 @@ predicate isOptionNotSet(ConstructorCall cc, int flag) { not isOptionSet(cc, fla
|
|||||||
|
|
||||||
from Expr protocolSource, Expr protocolSink, ConstructorCall cc, Expr e, string msg
|
from Expr protocolSource, Expr protocolSink, ConstructorCall cc, Expr e, string msg
|
||||||
where
|
where
|
||||||
BoostorgAsio::SslContextCallTlsProtocolFlow::hasFlow(DataFlow::exprNode(protocolSource),
|
BoostorgAsio::SslContextCallTlsProtocolFlow::flow(DataFlow::exprNode(protocolSource),
|
||||||
DataFlow::exprNode(protocolSink)) and
|
DataFlow::exprNode(protocolSink)) and
|
||||||
cc.getArgument(0) = protocolSink and
|
cc.getArgument(0) = protocolSink and
|
||||||
(
|
(
|
||||||
|
|||||||
@@ -14,12 +14,12 @@ import semmle.code.cpp.security.boostorg.asio.protocols
|
|||||||
|
|
||||||
from Expr protocolSource, Expr protocolSink, ConstructorCall cc
|
from Expr protocolSource, Expr protocolSink, ConstructorCall cc
|
||||||
where
|
where
|
||||||
BoostorgAsio::SslContextCallFlow::hasFlow(DataFlow::exprNode(protocolSource),
|
BoostorgAsio::SslContextCallFlow::flow(DataFlow::exprNode(protocolSource),
|
||||||
DataFlow::exprNode(protocolSink)) and
|
DataFlow::exprNode(protocolSink)) and
|
||||||
not BoostorgAsio::SslContextCallTlsProtocolFlow::hasFlow(DataFlow::exprNode(protocolSource),
|
not BoostorgAsio::SslContextCallTlsProtocolFlow::flow(DataFlow::exprNode(protocolSource),
|
||||||
DataFlow::exprNode(protocolSink)) and
|
DataFlow::exprNode(protocolSink)) and
|
||||||
cc.getArgument(0) = protocolSink and
|
cc.getArgument(0) = protocolSink and
|
||||||
BoostorgAsio::SslContextCallBannedProtocolFlow::hasFlow(DataFlow::exprNode(protocolSource),
|
BoostorgAsio::SslContextCallBannedProtocolFlow::flow(DataFlow::exprNode(protocolSource),
|
||||||
DataFlow::exprNode(protocolSink))
|
DataFlow::exprNode(protocolSink))
|
||||||
select protocolSink, "Usage of $@ specifying a deprecated hardcoded protocol $@ in function $@.",
|
select protocolSink, "Usage of $@ specifying a deprecated hardcoded protocol $@ in function $@.",
|
||||||
cc, "boost::asio::ssl::context::context", protocolSource, protocolSource.toString(),
|
cc, "boost::asio::ssl::context::context", protocolSource, protocolSource.toString(),
|
||||||
|
|||||||
@@ -10,10 +10,10 @@ import ExternalAPIsSpecific
|
|||||||
|
|
||||||
/** A node representing untrusted data being passed to an external API. */
|
/** A node representing untrusted data being passed to an external API. */
|
||||||
class UntrustedExternalApiDataNode extends ExternalApiDataNode {
|
class UntrustedExternalApiDataNode extends ExternalApiDataNode {
|
||||||
UntrustedExternalApiDataNode() { UntrustedDataToExternalApiFlow::hasFlow(_, this) }
|
UntrustedExternalApiDataNode() { UntrustedDataToExternalApiFlow::flow(_, this) }
|
||||||
|
|
||||||
/** Gets a source of untrusted data which is passed to this external API data node. */
|
/** Gets a source of untrusted data which is passed to this external API data node. */
|
||||||
DataFlow::Node getAnUntrustedSource() { UntrustedDataToExternalApiFlow::hasFlow(result, this) }
|
DataFlow::Node getAnUntrustedSource() { UntrustedDataToExternalApiFlow::flow(result, this) }
|
||||||
}
|
}
|
||||||
|
|
||||||
/** DEPRECATED: Alias for UntrustedExternalApiDataNode */
|
/** DEPRECATED: Alias for UntrustedExternalApiDataNode */
|
||||||
|
|||||||
@@ -73,4 +73,4 @@ private module UntrustedDataToExternalApiConfig implements DataFlow::ConfigSig {
|
|||||||
predicate isSink(DataFlow::Node sink) { sink instanceof ExternalApiDataNode }
|
predicate isSink(DataFlow::Node sink) { sink instanceof ExternalApiDataNode }
|
||||||
}
|
}
|
||||||
|
|
||||||
module UntrustedDataToExternalApiFlow = TaintTracking::Make<UntrustedDataToExternalApiConfig>;
|
module UntrustedDataToExternalApiFlow = TaintTracking::Global<UntrustedDataToExternalApiConfig>;
|
||||||
|
|||||||
@@ -16,7 +16,7 @@ import semmle.code.cpp.security.FlowSources
|
|||||||
import UntrustedDataToExternalApiFlow::PathGraph
|
import UntrustedDataToExternalApiFlow::PathGraph
|
||||||
|
|
||||||
from UntrustedDataToExternalApiFlow::PathNode source, UntrustedDataToExternalApiFlow::PathNode sink
|
from UntrustedDataToExternalApiFlow::PathNode source, UntrustedDataToExternalApiFlow::PathNode sink
|
||||||
where UntrustedDataToExternalApiFlow::hasFlowPath(source, sink)
|
where UntrustedDataToExternalApiFlow::flowPath(source, sink)
|
||||||
select sink, source, sink,
|
select sink, source, sink,
|
||||||
"Call to " + sink.getNode().(ExternalApiDataNode).getExternalFunction().toString() +
|
"Call to " + sink.getNode().(ExternalApiDataNode).getExternalFunction().toString() +
|
||||||
" with untrusted data from $@.", source, source.getNode().(RemoteFlowSource).getSourceType()
|
" with untrusted data from $@.", source, source.getNode().(RemoteFlowSource).getSourceType()
|
||||||
|
|||||||
@@ -15,7 +15,7 @@ import ExternalAPIs
|
|||||||
import UntrustedDataToExternalApiFlow::PathGraph
|
import UntrustedDataToExternalApiFlow::PathGraph
|
||||||
|
|
||||||
from UntrustedDataToExternalApiFlow::PathNode source, UntrustedDataToExternalApiFlow::PathNode sink
|
from UntrustedDataToExternalApiFlow::PathNode source, UntrustedDataToExternalApiFlow::PathNode sink
|
||||||
where UntrustedDataToExternalApiFlow::hasFlowPath(source, sink)
|
where UntrustedDataToExternalApiFlow::flowPath(source, sink)
|
||||||
select sink, source, sink,
|
select sink, source, sink,
|
||||||
"Call to " + sink.getNode().(ExternalApiDataNode).getExternalFunction().toString() +
|
"Call to " + sink.getNode().(ExternalApiDataNode).getExternalFunction().toString() +
|
||||||
" with untrusted data from $@.", source, source.toString()
|
" with untrusted data from $@.", source, source.toString()
|
||||||
|
|||||||
@@ -10,10 +10,10 @@ import ExternalAPIsSpecific
|
|||||||
|
|
||||||
/** A node representing untrusted data being passed to an external API. */
|
/** A node representing untrusted data being passed to an external API. */
|
||||||
class UntrustedExternalApiDataNode extends ExternalApiDataNode {
|
class UntrustedExternalApiDataNode extends ExternalApiDataNode {
|
||||||
UntrustedExternalApiDataNode() { UntrustedDataToExternalApiFlow::hasFlow(_, this) }
|
UntrustedExternalApiDataNode() { UntrustedDataToExternalApiFlow::flow(_, this) }
|
||||||
|
|
||||||
/** Gets a source of untrusted data which is passed to this external API data node. */
|
/** Gets a source of untrusted data which is passed to this external API data node. */
|
||||||
DataFlow::Node getAnUntrustedSource() { UntrustedDataToExternalApiFlow::hasFlow(result, this) }
|
DataFlow::Node getAnUntrustedSource() { UntrustedDataToExternalApiFlow::flow(result, this) }
|
||||||
}
|
}
|
||||||
|
|
||||||
/** DEPRECATED: Alias for UntrustedExternalApiDataNode */
|
/** DEPRECATED: Alias for UntrustedExternalApiDataNode */
|
||||||
|
|||||||
@@ -63,4 +63,4 @@ private module UntrustedDataToExternalApiConfig implements DataFlow::ConfigSig {
|
|||||||
predicate isSink(DataFlow::Node sink) { sink instanceof ExternalApiDataNode }
|
predicate isSink(DataFlow::Node sink) { sink instanceof ExternalApiDataNode }
|
||||||
}
|
}
|
||||||
|
|
||||||
module UntrustedDataToExternalApiFlow = TaintTracking::Make<UntrustedDataToExternalApiConfig>;
|
module UntrustedDataToExternalApiFlow = TaintTracking::Global<UntrustedDataToExternalApiConfig>;
|
||||||
|
|||||||
@@ -90,7 +90,7 @@ module TaintedPathConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module TaintedPath = TaintTracking::Make<TaintedPathConfig>;
|
module TaintedPath = TaintTracking::Global<TaintedPathConfig>;
|
||||||
|
|
||||||
from
|
from
|
||||||
FileFunction fileFunction, Expr taintedArg, FlowSource taintSource,
|
FileFunction fileFunction, Expr taintedArg, FlowSource taintSource,
|
||||||
@@ -98,7 +98,7 @@ from
|
|||||||
where
|
where
|
||||||
taintedArg = sinkNode.getNode().asIndirectArgument() and
|
taintedArg = sinkNode.getNode().asIndirectArgument() and
|
||||||
fileFunction.outermostWrapperFunctionCall(taintedArg, callChain) and
|
fileFunction.outermostWrapperFunctionCall(taintedArg, callChain) and
|
||||||
TaintedPath::hasFlowPath(sourceNode, sinkNode) and
|
TaintedPath::flowPath(sourceNode, sinkNode) and
|
||||||
taintSource = sourceNode.getNode()
|
taintSource = sourceNode.getNode()
|
||||||
select taintedArg, sourceNode, sinkNode,
|
select taintedArg, sourceNode, sinkNode,
|
||||||
"This argument to a file access function is derived from $@ and then passed to " + callChain + ".",
|
"This argument to a file access function is derived from $@ and then passed to " + callChain + ".",
|
||||||
|
|||||||
@@ -76,7 +76,7 @@ class ExecState extends TExecState {
|
|||||||
DataFlow::Node getOutgoingNode() { result = outgoing }
|
DataFlow::Node getOutgoingNode() { result = outgoing }
|
||||||
|
|
||||||
/** Holds if this is a possible `ExecState` for `sink`. */
|
/** Holds if this is a possible `ExecState` for `sink`. */
|
||||||
predicate isFeasibleForSink(DataFlow::Node sink) { ExecState::hasFlow(outgoing, sink) }
|
predicate isFeasibleForSink(DataFlow::Node sink) { ExecState::flow(outgoing, sink) }
|
||||||
|
|
||||||
string toString() { result = "ExecState" }
|
string toString() { result = "ExecState" }
|
||||||
}
|
}
|
||||||
@@ -109,7 +109,7 @@ module ExecStateConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module ExecState = TaintTracking::Make<ExecStateConfig>;
|
module ExecState = TaintTracking::Global<ExecStateConfig>;
|
||||||
|
|
||||||
module ExecTaintConfig implements DataFlow::StateConfigSig {
|
module ExecTaintConfig implements DataFlow::StateConfigSig {
|
||||||
class FlowState = TState;
|
class FlowState = TState;
|
||||||
@@ -141,13 +141,13 @@ module ExecTaintConfig implements DataFlow::StateConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module ExecTaint = TaintTracking::MakeWithState<ExecTaintConfig>;
|
module ExecTaint = TaintTracking::GlobalWithState<ExecTaintConfig>;
|
||||||
|
|
||||||
from
|
from
|
||||||
ExecTaint::PathNode sourceNode, ExecTaint::PathNode sinkNode, string taintCause, string callChain,
|
ExecTaint::PathNode sourceNode, ExecTaint::PathNode sinkNode, string taintCause, string callChain,
|
||||||
DataFlow::Node concatResult, Expr command
|
DataFlow::Node concatResult, Expr command
|
||||||
where
|
where
|
||||||
ExecTaint::hasFlowPath(sourceNode, sinkNode) and
|
ExecTaint::flowPath(sourceNode, sinkNode) and
|
||||||
taintCause = sourceNode.getNode().(FlowSource).getSourceType() and
|
taintCause = sourceNode.getNode().(FlowSource).getSourceType() and
|
||||||
isSinkImpl(sinkNode.getNode(), command, callChain) and
|
isSinkImpl(sinkNode.getNode(), command, callChain) and
|
||||||
concatResult = sinkNode.getState().(ExecState).getOutgoingNode()
|
concatResult = sinkNode.getState().(ExecState).getOutgoingNode()
|
||||||
|
|||||||
@@ -114,13 +114,13 @@ module ImproperArrayIndexValidationConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module ImproperArrayIndexValidation = TaintTracking::Make<ImproperArrayIndexValidationConfig>;
|
module ImproperArrayIndexValidation = TaintTracking::Global<ImproperArrayIndexValidationConfig>;
|
||||||
|
|
||||||
from
|
from
|
||||||
ImproperArrayIndexValidation::PathNode source, ImproperArrayIndexValidation::PathNode sink,
|
ImproperArrayIndexValidation::PathNode source, ImproperArrayIndexValidation::PathNode sink,
|
||||||
string sourceType
|
string sourceType
|
||||||
where
|
where
|
||||||
ImproperArrayIndexValidation::hasFlowPath(source, sink) and
|
ImproperArrayIndexValidation::flowPath(source, sink) and
|
||||||
isFlowSource(source.getNode(), sourceType)
|
isFlowSource(source.getNode(), sourceType)
|
||||||
select sink.getNode(), source, sink,
|
select sink.getNode(), source, sink,
|
||||||
"An array indexing expression depends on $@ that might be outside the bounds of the array.",
|
"An array indexing expression depends on $@ that might be outside the bounds of the array.",
|
||||||
|
|||||||
@@ -122,7 +122,7 @@ module UncontrolledArithConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module UncontrolledArith = TaintTracking::Make<UncontrolledArithConfig>;
|
module UncontrolledArith = TaintTracking::Global<UncontrolledArithConfig>;
|
||||||
|
|
||||||
/** Gets the expression that corresponds to `node`, if any. */
|
/** Gets the expression that corresponds to `node`, if any. */
|
||||||
Expr getExpr(DataFlow::Node node) { result = [node.asExpr(), node.asDefiningArgument()] }
|
Expr getExpr(DataFlow::Node node) { result = [node.asExpr(), node.asDefiningArgument()] }
|
||||||
@@ -131,7 +131,7 @@ from
|
|||||||
UncontrolledArith::PathNode source, UncontrolledArith::PathNode sink, VariableAccess va,
|
UncontrolledArith::PathNode source, UncontrolledArith::PathNode sink, VariableAccess va,
|
||||||
string effect
|
string effect
|
||||||
where
|
where
|
||||||
UncontrolledArith::hasFlowPath(source, sink) and
|
UncontrolledArith::flowPath(source, sink) and
|
||||||
sink.getNode().asExpr() = va and
|
sink.getNode().asExpr() = va and
|
||||||
missingGuard(va, effect)
|
missingGuard(va, effect)
|
||||||
select sink.getNode(), source, sink,
|
select sink.getNode(), source, sink,
|
||||||
|
|||||||
@@ -95,14 +95,14 @@ module TaintedAllocationSizeConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module TaintedAllocationSize = TaintTracking::Make<TaintedAllocationSizeConfig>;
|
module TaintedAllocationSize = TaintTracking::Global<TaintedAllocationSizeConfig>;
|
||||||
|
|
||||||
from
|
from
|
||||||
Expr alloc, TaintedAllocationSize::PathNode source, TaintedAllocationSize::PathNode sink,
|
Expr alloc, TaintedAllocationSize::PathNode source, TaintedAllocationSize::PathNode sink,
|
||||||
string taintCause
|
string taintCause
|
||||||
where
|
where
|
||||||
isFlowSource(source.getNode(), taintCause) and
|
isFlowSource(source.getNode(), taintCause) and
|
||||||
TaintedAllocationSize::hasFlowPath(source, sink) and
|
TaintedAllocationSize::flowPath(source, sink) and
|
||||||
allocSink(alloc, sink.getNode())
|
allocSink(alloc, sink.getNode())
|
||||||
select alloc, source, sink, "This allocation size is derived from $@ and might overflow.",
|
select alloc, source, sink, "This allocation size is derived from $@ and might overflow.",
|
||||||
source.getNode(), "user input (" + taintCause + ")"
|
source.getNode(), "user input (" + taintCause + ")"
|
||||||
|
|||||||
@@ -33,14 +33,14 @@ module VerifyResultConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module VerifyResult = DataFlow::Make<VerifyResultConfig>;
|
module VerifyResult = DataFlow::Global<VerifyResultConfig>;
|
||||||
|
|
||||||
from
|
from
|
||||||
DataFlow::Node source, DataFlow::Node sink1, DataFlow::Node sink2, GuardCondition guard, Expr c1,
|
DataFlow::Node source, DataFlow::Node sink1, DataFlow::Node sink2, GuardCondition guard, Expr c1,
|
||||||
Expr c2, boolean testIsTrue
|
Expr c2, boolean testIsTrue
|
||||||
where
|
where
|
||||||
VerifyResult::hasFlow(source, sink1) and
|
VerifyResult::flow(source, sink1) and
|
||||||
VerifyResult::hasFlow(source, sink2) and
|
VerifyResult::flow(source, sink2) and
|
||||||
guard.comparesEq(sink1.asExpr(), c1, 0, false, testIsTrue) and // (value != c1) => testIsTrue
|
guard.comparesEq(sink1.asExpr(), c1, 0, false, testIsTrue) and // (value != c1) => testIsTrue
|
||||||
guard.comparesEq(sink2.asExpr(), c2, 0, false, testIsTrue) and // (value != c2) => testIsTrue
|
guard.comparesEq(sink2.asExpr(), c2, 0, false, testIsTrue) and // (value != c2) => testIsTrue
|
||||||
c1.getValue().toInt() = 0 and
|
c1.getValue().toInt() = 0 and
|
||||||
|
|||||||
@@ -49,7 +49,7 @@ module ToBufferConfig implements DataFlow::ConfigSig {
|
|||||||
predicate isSink(DataFlow::Node sink) { isSinkImpl(sink, _) }
|
predicate isSink(DataFlow::Node sink) { isSinkImpl(sink, _) }
|
||||||
}
|
}
|
||||||
|
|
||||||
module ToBufferFlow = TaintTracking::Make<ToBufferConfig>;
|
module ToBufferFlow = TaintTracking::Global<ToBufferConfig>;
|
||||||
|
|
||||||
predicate isSinkImpl(DataFlow::Node sink, SensitiveBufferWrite w) {
|
predicate isSinkImpl(DataFlow::Node sink, SensitiveBufferWrite w) {
|
||||||
w.getASource() = sink.asIndirectExpr()
|
w.getASource() = sink.asIndirectExpr()
|
||||||
@@ -59,7 +59,7 @@ from
|
|||||||
SensitiveBufferWrite w, ToBufferFlow::PathNode sourceNode, ToBufferFlow::PathNode sinkNode,
|
SensitiveBufferWrite w, ToBufferFlow::PathNode sourceNode, ToBufferFlow::PathNode sinkNode,
|
||||||
FlowSource source
|
FlowSource source
|
||||||
where
|
where
|
||||||
ToBufferFlow::hasFlowPath(sourceNode, sinkNode) and
|
ToBufferFlow::flowPath(sourceNode, sinkNode) and
|
||||||
sourceNode.getNode() = source and
|
sourceNode.getNode() = source and
|
||||||
isSinkImpl(sinkNode.getNode(), w)
|
isSinkImpl(sinkNode.getNode(), w)
|
||||||
select w, sourceNode, sinkNode,
|
select w, sourceNode, sinkNode,
|
||||||
|
|||||||
@@ -33,7 +33,7 @@ module FromSensitiveConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module FromSensitiveFlow = TaintTracking::Make<FromSensitiveConfig>;
|
module FromSensitiveFlow = TaintTracking::Global<FromSensitiveConfig>;
|
||||||
|
|
||||||
predicate isSinkImpl(DataFlow::Node sink, FileWrite w, Expr dest) {
|
predicate isSinkImpl(DataFlow::Node sink, FileWrite w, Expr dest) {
|
||||||
exists(Expr e |
|
exists(Expr e |
|
||||||
@@ -81,7 +81,7 @@ from
|
|||||||
SensitiveExpr source, FromSensitiveFlow::PathNode sourceNode, FromSensitiveFlow::PathNode midNode,
|
SensitiveExpr source, FromSensitiveFlow::PathNode sourceNode, FromSensitiveFlow::PathNode midNode,
|
||||||
FileWrite w, Expr dest
|
FileWrite w, Expr dest
|
||||||
where
|
where
|
||||||
FromSensitiveFlow::hasFlowPath(sourceNode, midNode) and
|
FromSensitiveFlow::flowPath(sourceNode, midNode) and
|
||||||
isSourceImpl(sourceNode.getNode(), source) and
|
isSourceImpl(sourceNode.getNode(), source) and
|
||||||
isSinkImpl(midNode.getNode(), w, dest)
|
isSinkImpl(midNode.getNode(), w, dest)
|
||||||
select w, sourceNode, midNode,
|
select w, sourceNode, midNode,
|
||||||
|
|||||||
@@ -250,13 +250,13 @@ module FromSensitiveConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module FromSensitiveFlow = TaintTracking::Make<FromSensitiveConfig>;
|
module FromSensitiveFlow = TaintTracking::Global<FromSensitiveConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A taint flow configuration for flow from a sensitive expression to an encryption operation.
|
* A taint flow configuration for flow from a sensitive expression to an encryption operation.
|
||||||
*/
|
*/
|
||||||
module ToEncryptionConfig implements DataFlow::ConfigSig {
|
module ToEncryptionConfig implements DataFlow::ConfigSig {
|
||||||
predicate isSource(DataFlow::Node source) { FromSensitiveFlow::hasFlow(source, _) }
|
predicate isSource(DataFlow::Node source) { FromSensitiveFlow::flow(source, _) }
|
||||||
|
|
||||||
predicate isSink(DataFlow::Node sink) { isSinkEncrypt(sink, _) }
|
predicate isSink(DataFlow::Node sink) { isSinkEncrypt(sink, _) }
|
||||||
|
|
||||||
@@ -271,7 +271,7 @@ module ToEncryptionConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module ToEncryptionFlow = TaintTracking::Make<ToEncryptionConfig>;
|
module ToEncryptionFlow = TaintTracking::Global<ToEncryptionConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A taint flow configuration for flow from an encryption operation to a network operation.
|
* A taint flow configuration for flow from an encryption operation to a network operation.
|
||||||
@@ -279,25 +279,25 @@ module ToEncryptionFlow = TaintTracking::Make<ToEncryptionConfig>;
|
|||||||
module FromEncryptionConfig implements DataFlow::ConfigSig {
|
module FromEncryptionConfig implements DataFlow::ConfigSig {
|
||||||
predicate isSource(DataFlow::Node source) { isSinkEncrypt(source, _) }
|
predicate isSource(DataFlow::Node source) { isSinkEncrypt(source, _) }
|
||||||
|
|
||||||
predicate isSink(DataFlow::Node sink) { FromSensitiveFlow::hasFlowTo(sink) }
|
predicate isSink(DataFlow::Node sink) { FromSensitiveFlow::flowTo(sink) }
|
||||||
|
|
||||||
predicate isBarrier(DataFlow::Node node) {
|
predicate isBarrier(DataFlow::Node node) {
|
||||||
node.asExpr().getUnspecifiedType() instanceof IntegralType
|
node.asExpr().getUnspecifiedType() instanceof IntegralType
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module FromEncryptionFlow = TaintTracking::Make<FromEncryptionConfig>;
|
module FromEncryptionFlow = TaintTracking::Global<FromEncryptionConfig>;
|
||||||
|
|
||||||
from
|
from
|
||||||
FromSensitiveFlow::PathNode source, FromSensitiveFlow::PathNode sink,
|
FromSensitiveFlow::PathNode source, FromSensitiveFlow::PathNode sink,
|
||||||
NetworkSendRecv networkSendRecv, string msg
|
NetworkSendRecv networkSendRecv, string msg
|
||||||
where
|
where
|
||||||
// flow from sensitive -> network data
|
// flow from sensitive -> network data
|
||||||
FromSensitiveFlow::hasFlowPath(source, sink) and
|
FromSensitiveFlow::flowPath(source, sink) and
|
||||||
isSinkSendRecv(sink.getNode(), networkSendRecv) and
|
isSinkSendRecv(sink.getNode(), networkSendRecv) and
|
||||||
// no flow from sensitive -> evidence of encryption
|
// no flow from sensitive -> evidence of encryption
|
||||||
not ToEncryptionFlow::hasFlow(source.getNode(), _) and
|
not ToEncryptionFlow::flow(source.getNode(), _) and
|
||||||
not FromEncryptionFlow::hasFlowTo(sink.getNode()) and
|
not FromEncryptionFlow::flowTo(sink.getNode()) and
|
||||||
// construct result
|
// construct result
|
||||||
if networkSendRecv instanceof NetworkSend
|
if networkSendRecv instanceof NetworkSend
|
||||||
then
|
then
|
||||||
|
|||||||
@@ -125,13 +125,13 @@ module FromSensitiveConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module FromSensitiveFlow = TaintTracking::Make<FromSensitiveConfig>;
|
module FromSensitiveFlow = TaintTracking::Global<FromSensitiveConfig>;
|
||||||
|
|
||||||
from
|
from
|
||||||
SensitiveExpr sensitive, FromSensitiveFlow::PathNode source, FromSensitiveFlow::PathNode sink,
|
SensitiveExpr sensitive, FromSensitiveFlow::PathNode source, FromSensitiveFlow::PathNode sink,
|
||||||
SqliteFunctionCall sqliteCall
|
SqliteFunctionCall sqliteCall
|
||||||
where
|
where
|
||||||
FromSensitiveFlow::hasFlowPath(source, sink) and
|
FromSensitiveFlow::flowPath(source, sink) and
|
||||||
isSourceImpl(source.getNode(), sensitive) and
|
isSourceImpl(source.getNode(), sensitive) and
|
||||||
isSinkImpl(sink.getNode(), sqliteCall, _)
|
isSinkImpl(sink.getNode(), sqliteCall, _)
|
||||||
select sqliteCall, source, sink,
|
select sqliteCall, source, sink,
|
||||||
|
|||||||
@@ -89,10 +89,10 @@ module HttpStringToUrlOpenConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module HttpStringToUrlOpen = TaintTracking::Make<HttpStringToUrlOpenConfig>;
|
module HttpStringToUrlOpen = TaintTracking::Global<HttpStringToUrlOpenConfig>;
|
||||||
|
|
||||||
from HttpStringToUrlOpen::PathNode source, HttpStringToUrlOpen::PathNode sink, HttpStringLiteral str
|
from HttpStringToUrlOpen::PathNode source, HttpStringToUrlOpen::PathNode sink, HttpStringLiteral str
|
||||||
where
|
where
|
||||||
HttpStringToUrlOpen::hasFlowPath(source, sink) and
|
HttpStringToUrlOpen::flowPath(source, sink) and
|
||||||
str = source.getNode().asIndirectExpr()
|
str = source.getNode().asIndirectExpr()
|
||||||
select str, source, sink, "This URL may be constructed with the HTTP protocol."
|
select str, source, sink, "This URL may be constructed with the HTTP protocol."
|
||||||
|
|||||||
@@ -46,13 +46,13 @@ module KeyStrengthFlowConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module KeyStrengthFlow = DataFlow::Make<KeyStrengthFlowConfig>;
|
module KeyStrengthFlow = DataFlow::Global<KeyStrengthFlowConfig>;
|
||||||
|
|
||||||
from
|
from
|
||||||
KeyStrengthFlow::PathNode source, KeyStrengthFlow::PathNode sink, FunctionCall fc, int param,
|
KeyStrengthFlow::PathNode source, KeyStrengthFlow::PathNode sink, FunctionCall fc, int param,
|
||||||
string name, int minimumBits, int bits
|
string name, int minimumBits, int bits
|
||||||
where
|
where
|
||||||
KeyStrengthFlow::hasFlowPath(source, sink) and
|
KeyStrengthFlow::flowPath(source, sink) and
|
||||||
sink.getNode().asExpr() = fc.getArgument(param) and
|
sink.getNode().asExpr() = fc.getArgument(param) and
|
||||||
fc.getTarget().hasGlobalName(name) and
|
fc.getTarget().hasGlobalName(name) and
|
||||||
minimumBits = getMinimumKeyStrength(name, param) and
|
minimumBits = getMinimumKeyStrength(name, param) and
|
||||||
|
|||||||
@@ -64,7 +64,7 @@ module NullAppNameCreateProcessFunctionConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module NullAppNameCreateProcessFunction = DataFlow::Make<NullAppNameCreateProcessFunctionConfig>;
|
module NullAppNameCreateProcessFunction = DataFlow::Global<NullAppNameCreateProcessFunctionConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Dataflow that detects a call to CreateProcess with an unquoted commandLine argument
|
* Dataflow that detects a call to CreateProcess with an unquoted commandLine argument
|
||||||
@@ -85,7 +85,7 @@ module QuotedCommandInCreateProcessFunctionConfig implements DataFlow::ConfigSig
|
|||||||
}
|
}
|
||||||
|
|
||||||
module QuotedCommandInCreateProcessFunction =
|
module QuotedCommandInCreateProcessFunction =
|
||||||
DataFlow::Make<QuotedCommandInCreateProcessFunctionConfig>;
|
DataFlow::Global<QuotedCommandInCreateProcessFunctionConfig>;
|
||||||
|
|
||||||
bindingset[s]
|
bindingset[s]
|
||||||
predicate isQuotedOrNoSpaceApplicationNameOnCmd(string s) {
|
predicate isQuotedOrNoSpaceApplicationNameOnCmd(string s) {
|
||||||
@@ -98,12 +98,12 @@ from CreateProcessFunctionCall call, string msg1, string msg2
|
|||||||
where
|
where
|
||||||
exists(Expr appName |
|
exists(Expr appName |
|
||||||
appName = call.getArgument(call.getApplicationNameArgumentId()) and
|
appName = call.getArgument(call.getApplicationNameArgumentId()) and
|
||||||
NullAppNameCreateProcessFunction::hasFlowToExpr(appName) and
|
NullAppNameCreateProcessFunction::flowToExpr(appName) and
|
||||||
msg1 = call.toString() + " with lpApplicationName == NULL (" + appName + ")"
|
msg1 = call.toString() + " with lpApplicationName == NULL (" + appName + ")"
|
||||||
) and
|
) and
|
||||||
exists(Expr cmd |
|
exists(Expr cmd |
|
||||||
cmd = call.getArgument(call.getCommandLineArgumentId()) and
|
cmd = call.getArgument(call.getCommandLineArgumentId()) and
|
||||||
QuotedCommandInCreateProcessFunction::hasFlowToExpr(cmd) and
|
QuotedCommandInCreateProcessFunction::flowToExpr(cmd) and
|
||||||
msg2 =
|
msg2 =
|
||||||
" and with an unquoted lpCommandLine (" + cmd +
|
" and with an unquoted lpCommandLine (" + cmd +
|
||||||
") introduces a security vulnerability if the path contains spaces."
|
") introduces a security vulnerability if the path contains spaces."
|
||||||
|
|||||||
@@ -30,15 +30,15 @@ module ExposedSystemDataConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module ExposedSystemData = TaintTracking::Make<ExposedSystemDataConfig>;
|
module ExposedSystemData = TaintTracking::Global<ExposedSystemDataConfig>;
|
||||||
|
|
||||||
from ExposedSystemData::PathNode source, ExposedSystemData::PathNode sink
|
from ExposedSystemData::PathNode source, ExposedSystemData::PathNode sink
|
||||||
where
|
where
|
||||||
ExposedSystemData::hasFlowPath(source, sink) and
|
ExposedSystemData::flowPath(source, sink) and
|
||||||
not exists(
|
not exists(
|
||||||
DataFlow::Node alt // remove duplicate results on conversions
|
DataFlow::Node alt // remove duplicate results on conversions
|
||||||
|
|
|
|
||||||
ExposedSystemData::hasFlow(source.getNode(), alt) and
|
ExposedSystemData::flow(source.getNode(), alt) and
|
||||||
alt.asConvertedExpr() = sink.getNode().asIndirectExpr() and
|
alt.asConvertedExpr() = sink.getNode().asIndirectExpr() and
|
||||||
alt != sink.getNode()
|
alt != sink.getNode()
|
||||||
)
|
)
|
||||||
|
|||||||
@@ -51,9 +51,9 @@ module PotentiallyExposedSystemDataConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module PotentiallyExposedSystemData = TaintTracking::Make<PotentiallyExposedSystemDataConfig>;
|
module PotentiallyExposedSystemData = TaintTracking::Global<PotentiallyExposedSystemDataConfig>;
|
||||||
|
|
||||||
from PotentiallyExposedSystemData::PathNode source, PotentiallyExposedSystemData::PathNode sink
|
from PotentiallyExposedSystemData::PathNode source, PotentiallyExposedSystemData::PathNode sink
|
||||||
where PotentiallyExposedSystemData::hasFlowPath(source, sink)
|
where PotentiallyExposedSystemData::flowPath(source, sink)
|
||||||
select sink, source, sink, "This operation potentially exposes sensitive system data from $@.",
|
select sink, source, sink, "This operation potentially exposes sensitive system data from $@.",
|
||||||
source, source.getNode().toString()
|
source, source.getNode().toString()
|
||||||
|
|||||||
@@ -45,9 +45,9 @@ module XxeConfig implements DataFlow::StateConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module XxeFlow = DataFlow::MakeWithState<XxeConfig>;
|
module XxeFlow = DataFlow::GlobalWithState<XxeConfig>;
|
||||||
|
|
||||||
from XxeFlow::PathNode source, XxeFlow::PathNode sink
|
from XxeFlow::PathNode source, XxeFlow::PathNode sink
|
||||||
where XxeFlow::hasFlowPath(source, sink)
|
where XxeFlow::flowPath(source, sink)
|
||||||
select sink, source, sink,
|
select sink, source, sink,
|
||||||
"This $@ is not configured to prevent an XML external entity (XXE) attack.", source, "XML parser"
|
"This $@ is not configured to prevent an XML external entity (XXE) attack.", source, "XML parser"
|
||||||
|
|||||||
@@ -39,7 +39,7 @@ module NullDaclConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module NullDaclFlow = DataFlow::Make<NullDaclConfig>;
|
module NullDaclFlow = DataFlow::Global<NullDaclConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Dataflow that detects a call to SetSecurityDescriptorDacl with a pDacl
|
* Dataflow that detects a call to SetSecurityDescriptorDacl with a pDacl
|
||||||
@@ -70,7 +70,7 @@ module NonNullDaclConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module NonNullDaclFlow = DataFlow::Make<NonNullDaclConfig>;
|
module NonNullDaclFlow = DataFlow::Global<NonNullDaclConfig>;
|
||||||
|
|
||||||
from SetSecurityDescriptorDaclFunctionCall call, string message
|
from SetSecurityDescriptorDaclFunctionCall call, string message
|
||||||
where
|
where
|
||||||
@@ -88,7 +88,7 @@ where
|
|||||||
" that is set to NULL will result in an unprotected object."
|
" that is set to NULL will result in an unprotected object."
|
||||||
|
|
|
|
||||||
var = call.getArgument(2) and
|
var = call.getArgument(2) and
|
||||||
NullDaclFlow::hasFlowToExpr(var) and
|
NullDaclFlow::flowToExpr(var) and
|
||||||
not NonNullDaclFlow::hasFlowToExpr(var)
|
not NonNullDaclFlow::flowToExpr(var)
|
||||||
)
|
)
|
||||||
select call, message
|
select call, message
|
||||||
|
|||||||
@@ -24,7 +24,7 @@ import DataFlow::PathGraph
|
|||||||
|
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
Instruction getABoundIn(SemBound b, IRFunction func) {
|
Instruction getABoundIn(SemBound b, IRFunction func) {
|
||||||
result = b.getExpr(0) and
|
getSemanticExpr(result) = b.getExpr(0) and
|
||||||
result.getEnclosingIRFunction() = func
|
result.getEnclosingIRFunction() = func
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -62,11 +62,16 @@ predicate hasSize(AllocationExpr alloc, DataFlow::Node n, string state) {
|
|||||||
predicate isSinkPairImpl(
|
predicate isSinkPairImpl(
|
||||||
CallInstruction c, DataFlow::Node bufSink, DataFlow::Node sizeSink, int delta, Expr eBuf
|
CallInstruction c, DataFlow::Node bufSink, DataFlow::Node sizeSink, int delta, Expr eBuf
|
||||||
) {
|
) {
|
||||||
exists(int bufIndex, int sizeIndex, Instruction sizeInstr, Instruction bufInstr |
|
exists(
|
||||||
|
int bufIndex, int sizeIndex, Instruction sizeInstr, Instruction bufInstr, ArrayFunction func
|
||||||
|
|
|
||||||
bufInstr = bufSink.asInstruction() and
|
bufInstr = bufSink.asInstruction() and
|
||||||
c.getArgument(bufIndex) = bufInstr and
|
c.getArgument(bufIndex) = bufInstr and
|
||||||
sizeInstr = sizeSink.asInstruction() and
|
sizeInstr = sizeSink.asInstruction() and
|
||||||
c.getStaticCallTarget().(ArrayFunction).hasArrayWithVariableSize(bufIndex, sizeIndex) and
|
c.getStaticCallTarget() = func and
|
||||||
|
pragma[only_bind_into](func)
|
||||||
|
.hasArrayWithVariableSize(pragma[only_bind_into](bufIndex),
|
||||||
|
pragma[only_bind_into](sizeIndex)) and
|
||||||
bounded(c.getArgument(sizeIndex), sizeInstr, delta) and
|
bounded(c.getArgument(sizeIndex), sizeInstr, delta) and
|
||||||
eBuf = bufInstr.getUnconvertedResultExpression()
|
eBuf = bufInstr.getUnconvertedResultExpression()
|
||||||
)
|
)
|
||||||
@@ -110,7 +115,7 @@ class StringSizeConfiguration extends ProductFlow::Configuration {
|
|||||||
state1 = s1.toString() and
|
state1 = s1.toString() and
|
||||||
state2 = s2.toString() and
|
state2 = s2.toString() and
|
||||||
add.hasOperands(node1.asOperand(), op) and
|
add.hasOperands(node1.asOperand(), op) and
|
||||||
semBounded(op.getDef(), any(SemZeroBound zero), delta, true, _) and
|
semBounded(getSemanticExpr(op.getDef()), any(SemZeroBound zero), delta, true, _) and
|
||||||
node2.asInstruction() = add and
|
node2.asInstruction() = add and
|
||||||
s1 = s2 + delta
|
s1 = s2 + delta
|
||||||
)
|
)
|
||||||
|
|||||||
@@ -50,9 +50,9 @@ module WordexpTaintConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module WordexpTaint = TaintTracking::Make<WordexpTaintConfig>;
|
module WordexpTaint = TaintTracking::Global<WordexpTaintConfig>;
|
||||||
|
|
||||||
from WordexpTaint::PathNode sourceNode, WordexpTaint::PathNode sinkNode
|
from WordexpTaint::PathNode sourceNode, WordexpTaint::PathNode sinkNode
|
||||||
where WordexpTaint::hasFlowPath(sourceNode, sinkNode)
|
where WordexpTaint::flowPath(sourceNode, sinkNode)
|
||||||
select sinkNode.getNode(), sourceNode, sinkNode,
|
select sinkNode.getNode(), sourceNode, sinkNode,
|
||||||
"Using user-supplied data in a `wordexp` command, without disabling command substitution, can make code vulnerable to command injection."
|
"Using user-supplied data in a `wordexp` command, without disabling command substitution, can make code vulnerable to command injection."
|
||||||
|
|||||||
@@ -32,10 +32,10 @@ module MultToAllocConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module MultToAlloc = DataFlow::Make<MultToAllocConfig>;
|
module MultToAlloc = DataFlow::Global<MultToAllocConfig>;
|
||||||
|
|
||||||
from MultToAlloc::PathNode source, MultToAlloc::PathNode sink
|
from MultToAlloc::PathNode source, MultToAlloc::PathNode sink
|
||||||
where MultToAlloc::hasFlowPath(source, sink)
|
where MultToAlloc::flowPath(source, sink)
|
||||||
select sink, source, sink,
|
select sink, source, sink,
|
||||||
"Potentially overflowing value from $@ is used in the size of this allocation.", source,
|
"Potentially overflowing value from $@ is used in the size of this allocation.", source,
|
||||||
"multiplication"
|
"multiplication"
|
||||||
|
|||||||
@@ -19,7 +19,7 @@ import PointerArithmeticToDerefFlow::PathGraph
|
|||||||
|
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
Instruction getABoundIn(SemBound b, IRFunction func) {
|
Instruction getABoundIn(SemBound b, IRFunction func) {
|
||||||
result = b.getExpr(0) and
|
getSemanticExpr(result) = b.getExpr(0) and
|
||||||
result.getEnclosingIRFunction() = func
|
result.getEnclosingIRFunction() = func
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -43,7 +43,8 @@ module FieldAddressToPointerArithmeticConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module FieldAddressToPointerArithmeticFlow = DataFlow::Make<FieldAddressToPointerArithmeticConfig>;
|
module FieldAddressToPointerArithmeticFlow =
|
||||||
|
DataFlow::Global<FieldAddressToPointerArithmeticConfig>;
|
||||||
|
|
||||||
predicate isFieldAddressSource(Field f, DataFlow::Node source) {
|
predicate isFieldAddressSource(Field f, DataFlow::Node source) {
|
||||||
source.asInstruction().(FieldAddressInstruction).getField() = f
|
source.asInstruction().(FieldAddressInstruction).getField() = f
|
||||||
@@ -70,7 +71,7 @@ predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string o
|
|||||||
|
|
||||||
predicate isConstantSizeOverflowSource(Field f, PointerAddInstruction pai, int delta) {
|
predicate isConstantSizeOverflowSource(Field f, PointerAddInstruction pai, int delta) {
|
||||||
exists(int size, int bound, DataFlow::Node source, DataFlow::InstructionNode sink |
|
exists(int size, int bound, DataFlow::Node source, DataFlow::InstructionNode sink |
|
||||||
FieldAddressToPointerArithmeticFlow::hasFlow(source, sink) and
|
FieldAddressToPointerArithmeticFlow::flow(source, sink) and
|
||||||
isFieldAddressSource(f, source) and
|
isFieldAddressSource(f, source) and
|
||||||
pai.getLeft() = sink.asInstruction() and
|
pai.getLeft() = sink.asInstruction() and
|
||||||
f.getUnspecifiedType().(ArrayType).getArraySize() = size and
|
f.getUnspecifiedType().(ArrayType).getArraySize() = size and
|
||||||
@@ -90,13 +91,13 @@ module PointerArithmeticToDerefConfig implements DataFlow::ConfigSig {
|
|||||||
predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink(sink, _, _) }
|
predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink(sink, _, _) }
|
||||||
}
|
}
|
||||||
|
|
||||||
module PointerArithmeticToDerefFlow = DataFlow::Make<PointerArithmeticToDerefConfig>;
|
module PointerArithmeticToDerefFlow = DataFlow::Global<PointerArithmeticToDerefConfig>;
|
||||||
|
|
||||||
from
|
from
|
||||||
Field f, PointerArithmeticToDerefFlow::PathNode source,
|
Field f, PointerArithmeticToDerefFlow::PathNode source,
|
||||||
PointerArithmeticToDerefFlow::PathNode sink, Instruction deref, string operation, int delta
|
PointerArithmeticToDerefFlow::PathNode sink, Instruction deref, string operation, int delta
|
||||||
where
|
where
|
||||||
PointerArithmeticToDerefFlow::hasFlowPath(source, sink) and
|
PointerArithmeticToDerefFlow::flowPath(source, sink) and
|
||||||
isInvalidPointerDerefSink(sink.getNode(), deref, operation) and
|
isInvalidPointerDerefSink(sink.getNode(), deref, operation) and
|
||||||
isConstantSizeOverflowSource(f, source.getNode().asInstruction(), delta)
|
isConstantSizeOverflowSource(f, source.getNode().asInstruction(), delta)
|
||||||
select source, source, sink,
|
select source, source, sink,
|
||||||
|
|||||||
@@ -24,7 +24,7 @@ import semmle.code.cpp.ir.IR
|
|||||||
|
|
||||||
pragma[nomagic]
|
pragma[nomagic]
|
||||||
Instruction getABoundIn(SemBound b, IRFunction func) {
|
Instruction getABoundIn(SemBound b, IRFunction func) {
|
||||||
result = b.getExpr(0) and
|
getSemanticExpr(result) = b.getExpr(0) and
|
||||||
result.getEnclosingIRFunction() = func
|
result.getEnclosingIRFunction() = func
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -209,7 +209,7 @@ module InvalidPointerToDerefConfig implements DataFlow::ConfigSig {
|
|||||||
predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink(sink, _, _) }
|
predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink(sink, _, _) }
|
||||||
}
|
}
|
||||||
|
|
||||||
module InvalidPointerToDerefFlow = DataFlow::Make<InvalidPointerToDerefConfig>;
|
module InvalidPointerToDerefFlow = DataFlow::Global<InvalidPointerToDerefConfig>;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Holds if `pai` is a pointer-arithmetic operation and `source` is a dataflow node with a
|
* Holds if `pai` is a pointer-arithmetic operation and `source` is a dataflow node with a
|
||||||
@@ -241,7 +241,7 @@ newtype TMergedPathNode =
|
|||||||
// pointer, but we want to raise an alert at the dereference.
|
// pointer, but we want to raise an alert at the dereference.
|
||||||
TPathNodeSink(Instruction i) {
|
TPathNodeSink(Instruction i) {
|
||||||
exists(DataFlow::Node n |
|
exists(DataFlow::Node n |
|
||||||
InvalidPointerToDerefFlow::hasFlow(_, n) and
|
InvalidPointerToDerefFlow::flow(_, n) and
|
||||||
isInvalidPointerDerefSink(n, i, _)
|
isInvalidPointerDerefSink(n, i, _)
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
@@ -349,7 +349,7 @@ predicate hasFlowPath(
|
|||||||
|
|
|
|
||||||
conf1.hasFlowPath(source1.asPathNode1(), _, sink1, _) and
|
conf1.hasFlowPath(source1.asPathNode1(), _, sink1, _) and
|
||||||
joinOn1(pai, sink1, source3) and
|
joinOn1(pai, sink1, source3) and
|
||||||
InvalidPointerToDerefFlow::hasFlowPath(source3, sink3) and
|
InvalidPointerToDerefFlow::flowPath(source3, sink3) and
|
||||||
joinOn2(sink3, sink.asSinkNode(), operation)
|
joinOn2(sink3, sink.asSinkNode(), operation)
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -16,7 +16,7 @@ import experimental.semmle.code.cpp.security.PrivateCleartextWrite::PrivateClear
|
|||||||
import WriteFlow::PathGraph
|
import WriteFlow::PathGraph
|
||||||
|
|
||||||
from WriteFlow::PathNode source, WriteFlow::PathNode sink
|
from WriteFlow::PathNode source, WriteFlow::PathNode sink
|
||||||
where WriteFlow::hasFlowPath(source, sink)
|
where WriteFlow::flowPath(source, sink)
|
||||||
select sink.getNode(), source, sink,
|
select sink.getNode(), source, sink,
|
||||||
"This write into the external location '" + sink.getNode() +
|
"This write into the external location '" + sink.getNode() +
|
||||||
"' may contain unencrypted data from $@.", source, "this source of private data."
|
"' may contain unencrypted data from $@.", source, "this source of private data."
|
||||||
|
|||||||
@@ -12,11 +12,11 @@ module LiteralToGethostbynameConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module LiteralToGethostbynameFlow = DataFlow::Make<LiteralToGethostbynameConfig>;
|
module LiteralToGethostbynameFlow = DataFlow::Global<LiteralToGethostbynameConfig>;
|
||||||
|
|
||||||
from StringLiteral sl, FunctionCall fc, DataFlow::Node source, DataFlow::Node sink
|
from StringLiteral sl, FunctionCall fc, DataFlow::Node source, DataFlow::Node sink
|
||||||
where
|
where
|
||||||
source.asIndirectExpr(1) = sl and
|
source.asIndirectExpr(1) = sl and
|
||||||
sink.asIndirectExpr(1) = fc.getArgument(0) and
|
sink.asIndirectExpr(1) = fc.getArgument(0) and
|
||||||
LiteralToGethostbynameFlow::hasFlow(source, sink)
|
LiteralToGethostbynameFlow::flow(source, sink)
|
||||||
select sl, fc
|
select sl, fc
|
||||||
|
|||||||
@@ -16,11 +16,11 @@ module GetenvToGethostbynameConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module GetenvToGethostbynameFlow = DataFlow::Make<GetenvToGethostbynameConfig>;
|
module GetenvToGethostbynameFlow = DataFlow::Global<GetenvToGethostbynameConfig>;
|
||||||
|
|
||||||
from Expr getenv, FunctionCall fc, DataFlow::Node source, DataFlow::Node sink
|
from Expr getenv, FunctionCall fc, DataFlow::Node source, DataFlow::Node sink
|
||||||
where
|
where
|
||||||
source.asIndirectExpr(1) = getenv and
|
source.asIndirectExpr(1) = getenv and
|
||||||
sink.asIndirectExpr(1) = fc.getArgument(0) and
|
sink.asIndirectExpr(1) = fc.getArgument(0) and
|
||||||
GetenvToGethostbynameFlow::hasFlow(source, sink)
|
GetenvToGethostbynameFlow::flow(source, sink)
|
||||||
select getenv, fc
|
select getenv, fc
|
||||||
|
|||||||
@@ -17,11 +17,11 @@ module EnvironmentToFileConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module EnvironmentToFileFlow = DataFlow::Make<EnvironmentToFileConfig>;
|
module EnvironmentToFileFlow = DataFlow::Global<EnvironmentToFileConfig>;
|
||||||
|
|
||||||
from Expr getenv, Expr fopen, DataFlow::Node source, DataFlow::Node sink
|
from Expr getenv, Expr fopen, DataFlow::Node source, DataFlow::Node sink
|
||||||
where
|
where
|
||||||
source.asIndirectExpr(1) = getenv and
|
source.asIndirectExpr(1) = getenv and
|
||||||
sink.asIndirectExpr(1) = fopen and
|
sink.asIndirectExpr(1) = fopen and
|
||||||
EnvironmentToFileFlow::hasFlow(source, sink)
|
EnvironmentToFileFlow::flow(source, sink)
|
||||||
select fopen, "This 'fopen' uses data from $@.", getenv, "call to 'getenv'"
|
select fopen, "This 'fopen' uses data from $@.", getenv, "call to 'getenv'"
|
||||||
|
|||||||
@@ -30,9 +30,9 @@ module NetworkToBufferSizeConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module NetworkToBufferSizeFlow = TaintTracking::Make<NetworkToBufferSizeConfig>;
|
module NetworkToBufferSizeFlow = TaintTracking::Global<NetworkToBufferSizeConfig>;
|
||||||
|
|
||||||
from DataFlow::Node ntohl, DataFlow::Node offset
|
from DataFlow::Node ntohl, DataFlow::Node offset
|
||||||
where NetworkToBufferSizeFlow::hasFlow(ntohl, offset)
|
where NetworkToBufferSizeFlow::flow(ntohl, offset)
|
||||||
select offset, "This array offset may be influenced by $@.", ntohl,
|
select offset, "This array offset may be influenced by $@.", ntohl,
|
||||||
"converted data from the network"
|
"converted data from the network"
|
||||||
|
|||||||
@@ -0,0 +1,2 @@
|
|||||||
|
| test.cpp:4:3:4:8 | call to strlen | 7.0 | 7.0 |
|
||||||
|
| test.cpp:5:3:5:8 | call to strlen | 1.8446744073709552E19 | 0.0 |
|
||||||
@@ -0,0 +1,6 @@
|
|||||||
|
import cpp
|
||||||
|
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
|
||||||
|
import experimental.semmle.code.cpp.rangeanalysis.extensions.StrlenLiteralRangeExpr
|
||||||
|
|
||||||
|
from FunctionCall fc
|
||||||
|
select fc, upperBound(fc), lowerBound(fc)
|
||||||
@@ -0,0 +1,6 @@
|
|||||||
|
unsigned long strlen(const char *);
|
||||||
|
|
||||||
|
void func(const char *s) {
|
||||||
|
strlen("literal");
|
||||||
|
strlen(s);
|
||||||
|
}
|
||||||
@@ -1,35 +1,21 @@
|
|||||||
| CPP-205.cpp:0:0:0:0 | CPP-205.cpp | |
|
| CPP-205.cpp:2:5:2:5 | definition of fn | function declaration entry for int fn<int>(int), isFromTemplateInstantiation(fn) |
|
||||||
| CPP-205.cpp:1:20:1:20 | T | |
|
| CPP-205.cpp:2:5:2:5 | fn | function int fn<int>(int), isFromTemplateInstantiation(fn) |
|
||||||
| CPP-205.cpp:1:20:1:20 | definition of T | |
|
| CPP-205.cpp:2:5:2:6 | definition of fn | function declaration entry for int fn<T>(T), isFromUninstantiatedTemplate(fn) |
|
||||||
| CPP-205.cpp:2:5:2:5 | definition of fn | function declaration entry for int fn<int>(int) |
|
| CPP-205.cpp:2:5:2:6 | fn | function int fn<T>(T), isFromUninstantiatedTemplate(fn) |
|
||||||
| CPP-205.cpp:2:5:2:5 | fn | function int fn<int>(int) |
|
| CPP-205.cpp:2:10:2:12 | definition of out | isFromTemplateInstantiation(fn), parameter declaration entry for int fn<int>(int) |
|
||||||
| CPP-205.cpp:2:5:2:6 | definition of fn | function declaration entry for int fn<T>(T) |
|
| CPP-205.cpp:2:10:2:12 | definition of out | isFromUninstantiatedTemplate(fn), parameter declaration entry for int fn<T>(T) |
|
||||||
| CPP-205.cpp:2:5:2:6 | fn | function int fn<T>(T) |
|
| CPP-205.cpp:2:10:2:12 | out | isFromTemplateInstantiation(fn), parameter for int fn<int>(int) |
|
||||||
| CPP-205.cpp:2:10:2:12 | definition of out | parameter declaration entry for int fn<T>(T) |
|
| CPP-205.cpp:2:10:2:12 | out | isFromUninstantiatedTemplate(fn), parameter for int fn<T>(T) |
|
||||||
| CPP-205.cpp:2:10:2:12 | definition of out | parameter declaration entry for int fn<int>(int) |
|
| CPP-205.cpp:2:15:5:1 | { ... } | isFromTemplateInstantiation(fn) |
|
||||||
| CPP-205.cpp:2:10:2:12 | out | parameter for int fn<T>(T) |
|
| CPP-205.cpp:2:15:5:1 | { ... } | isFromUninstantiatedTemplate(fn) |
|
||||||
| CPP-205.cpp:2:10:2:12 | out | parameter for int fn<int>(int) |
|
| CPP-205.cpp:3:3:3:33 | declaration | isFromTemplateInstantiation(fn) |
|
||||||
| CPP-205.cpp:2:15:5:1 | { ... } | |
|
| CPP-205.cpp:3:3:3:33 | declaration | isFromUninstantiatedTemplate(fn) |
|
||||||
| CPP-205.cpp:2:15:5:1 | { ... } | |
|
| CPP-205.cpp:3:15:3:15 | declaration of y | isFromUninstantiatedTemplate(fn) |
|
||||||
| CPP-205.cpp:3:3:3:33 | declaration | |
|
| CPP-205.cpp:3:15:3:15 | y | isFromUninstantiatedTemplate(fn) |
|
||||||
| CPP-205.cpp:3:3:3:33 | declaration | |
|
| CPP-205.cpp:3:17:3:31 | 5 | isFromTemplateInstantiation(fn) |
|
||||||
| CPP-205.cpp:3:15:3:15 | declaration of y | |
|
| CPP-205.cpp:4:3:4:11 | return ... | isFromTemplateInstantiation(fn) |
|
||||||
| CPP-205.cpp:3:15:3:15 | y | |
|
| CPP-205.cpp:4:3:4:11 | return ... | isFromUninstantiatedTemplate(fn) |
|
||||||
| CPP-205.cpp:3:17:3:31 | 5 | |
|
| CPP-205.cpp:4:10:4:10 | 0 | isFromTemplateInstantiation(fn) |
|
||||||
| CPP-205.cpp:4:3:4:11 | return ... | |
|
| CPP-205.cpp:4:10:4:10 | 0 | isFromUninstantiatedTemplate(fn) |
|
||||||
| CPP-205.cpp:4:3:4:11 | return ... | |
|
|
||||||
| CPP-205.cpp:4:10:4:10 | 0 | |
|
|
||||||
| CPP-205.cpp:4:10:4:10 | 0 | |
|
|
||||||
| CPP-205.cpp:7:5:7:8 | definition of main | function declaration entry for int main() |
|
| CPP-205.cpp:7:5:7:8 | definition of main | function declaration entry for int main() |
|
||||||
| CPP-205.cpp:7:5:7:8 | main | function int main() |
|
| CPP-205.cpp:7:5:7:8 | main | function int main() |
|
||||||
| CPP-205.cpp:7:12:9:1 | { ... } | |
|
|
||||||
| CPP-205.cpp:8:3:8:15 | return ... | |
|
|
||||||
| CPP-205.cpp:8:10:8:11 | call to fn | |
|
|
||||||
| CPP-205.cpp:8:13:8:13 | 0 | |
|
|
||||||
| file://:0:0:0:0 | (unnamed parameter 0) | parameter for __va_list_tag& __va_list_tag::operator=(__va_list_tag const&) |
|
|
||||||
| file://:0:0:0:0 | (unnamed parameter 0) | parameter for __va_list_tag& __va_list_tag::operator=(__va_list_tag&&) |
|
|
||||||
| file://:0:0:0:0 | __super | |
|
|
||||||
| file://:0:0:0:0 | __va_list_tag | |
|
|
||||||
| file://:0:0:0:0 | operator= | function __va_list_tag& __va_list_tag::operator=(__va_list_tag const&) |
|
|
||||||
| file://:0:0:0:0 | operator= | function __va_list_tag& __va_list_tag::operator=(__va_list_tag&&) |
|
|
||||||
| file://:0:0:0:0 | y | |
|
|
||||||
|
|||||||
@@ -14,10 +14,20 @@ string describe(Element e) {
|
|||||||
result =
|
result =
|
||||||
"parameter declaration entry for " +
|
"parameter declaration entry for " +
|
||||||
getIdentityString(e.(ParameterDeclarationEntry).getFunctionDeclarationEntry().getFunction())
|
getIdentityString(e.(ParameterDeclarationEntry).getFunctionDeclarationEntry().getFunction())
|
||||||
|
or
|
||||||
|
exists(Element template |
|
||||||
|
e.isFromTemplateInstantiation(template) and
|
||||||
|
result = "isFromTemplateInstantiation(" + template.toString() + ")"
|
||||||
|
)
|
||||||
|
or
|
||||||
|
exists(Element template |
|
||||||
|
e.isFromUninstantiatedTemplate(template) and
|
||||||
|
result = "isFromUninstantiatedTemplate(" + template.toString() + ")"
|
||||||
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
from Element e
|
from Element e
|
||||||
where
|
where
|
||||||
not e.getLocation() instanceof UnknownLocation and
|
e.getLocation().getFile().getBaseName() != "" and
|
||||||
not e instanceof Folder
|
not e instanceof Folder
|
||||||
select e, concat(describe(e), ", ")
|
select e, strictconcat(describe(e), ", ")
|
||||||
|
|||||||
@@ -14,8 +14,8 @@ module TestConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module TestFlow = DataFlow::Make<TestConfig>;
|
module TestFlow = DataFlow::Global<TestConfig>;
|
||||||
|
|
||||||
from DataFlow::Node sink, DataFlow::Node source
|
from DataFlow::Node sink, DataFlow::Node source
|
||||||
where TestFlow::hasFlow(source, sink)
|
where TestFlow::flow(source, sink)
|
||||||
select sink, source
|
select sink, source
|
||||||
|
|||||||
@@ -25,8 +25,8 @@ module TestConfig implements DataFlow::ConfigSig {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
module TestFlow = DataFlow::Make<TestConfig>;
|
module TestFlow = DataFlow::Global<TestConfig>;
|
||||||
|
|
||||||
from DataFlow::Node sink, DataFlow::Node source
|
from DataFlow::Node sink, DataFlow::Node source
|
||||||
where TestFlow::hasFlow(source, sink)
|
where TestFlow::flow(source, sink)
|
||||||
select sink, source
|
select sink, source
|
||||||
|
|||||||
@@ -7,8 +7,8 @@ module Cfg implements DataFlow::ConfigSig {
|
|||||||
predicate isSink(DataFlow::Node sink) { sink.asExpr() instanceof VariableAccess }
|
predicate isSink(DataFlow::Node sink) { sink.asExpr() instanceof VariableAccess }
|
||||||
}
|
}
|
||||||
|
|
||||||
module Flow = DataFlow::Make<Cfg>;
|
module Flow = DataFlow::Global<Cfg>;
|
||||||
|
|
||||||
from Expr sink
|
from Expr sink
|
||||||
where Flow::hasFlowToExpr(sink)
|
where Flow::flowToExpr(sink)
|
||||||
select sink
|
select sink
|
||||||
|
|||||||
@@ -5,6 +5,7 @@ import experimental.semmle.code.cpp.semantic.analysis.RangeUtils
|
|||||||
import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
|
import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
|
||||||
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisSpecific
|
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisSpecific
|
||||||
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisImpl
|
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisImpl
|
||||||
|
import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
|
||||||
import semmle.code.cpp.ir.IR as IR
|
import semmle.code.cpp.ir.IR as IR
|
||||||
import TestUtilities.InlineExpectationsTest
|
import TestUtilities.InlineExpectationsTest
|
||||||
|
|
||||||
@@ -18,7 +19,7 @@ class ModulusAnalysisTest extends InlineExpectationsTest {
|
|||||||
|
|
||||||
override predicate hasActualResult(Location location, string element, string tag, string value) {
|
override predicate hasActualResult(Location location, string element, string tag, string value) {
|
||||||
exists(SemExpr e, IR::CallInstruction call |
|
exists(SemExpr e, IR::CallInstruction call |
|
||||||
call.getArgument(0) = e and
|
getSemanticExpr(call.getArgument(0)) = e and
|
||||||
call.getStaticCallTarget().hasName("mod") and
|
call.getStaticCallTarget().hasName("mod") and
|
||||||
tag = "mod" and
|
tag = "mod" and
|
||||||
element = e.toString() and
|
element = e.toString() and
|
||||||
|
|||||||
@@ -12,7 +12,7 @@ class RangeAnalysisTest extends InlineExpectationsTest {
|
|||||||
|
|
||||||
override predicate hasActualResult(Location location, string element, string tag, string value) {
|
override predicate hasActualResult(Location location, string element, string tag, string value) {
|
||||||
exists(SemExpr e, IR::CallInstruction call |
|
exists(SemExpr e, IR::CallInstruction call |
|
||||||
call.getArgument(0) = e and
|
getSemanticExpr(call.getArgument(0)) = e and
|
||||||
call.getStaticCallTarget().hasName("range") and
|
call.getStaticCallTarget().hasName("range") and
|
||||||
tag = "range" and
|
tag = "range" and
|
||||||
element = e.toString() and
|
element = e.toString() and
|
||||||
@@ -29,7 +29,7 @@ private string getDirectionString(boolean d) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
bindingset[value]
|
bindingset[value]
|
||||||
private string getOffsetString(int value) {
|
private string getOffsetString(float value) {
|
||||||
if value >= 0 then result = "+" + value.toString() else result = value.toString()
|
if value >= 0 then result = "+" + value.toString() else result = value.toString()
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -37,7 +37,7 @@ bindingset[s]
|
|||||||
string quote(string s) { if s.matches("% %") then result = "\"" + s + "\"" else result = s }
|
string quote(string s) { if s.matches("% %") then result = "\"" + s + "\"" else result = s }
|
||||||
|
|
||||||
bindingset[delta]
|
bindingset[delta]
|
||||||
private string getBoundString(SemBound b, int delta) {
|
private string getBoundString(SemBound b, float delta) {
|
||||||
b instanceof SemZeroBound and result = delta.toString()
|
b instanceof SemZeroBound and result = delta.toString()
|
||||||
or
|
or
|
||||||
result =
|
result =
|
||||||
@@ -51,7 +51,7 @@ private string getBoundString(SemBound b, int delta) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
private string getARangeString(SemExpr e) {
|
private string getARangeString(SemExpr e) {
|
||||||
exists(SemBound b, int delta, boolean upper |
|
exists(SemBound b, float delta, boolean upper |
|
||||||
semBounded(e, b, delta, upper, _) and
|
semBounded(e, b, delta, upper, _) and
|
||||||
if semBounded(e, b, delta, upper.booleanNot(), _)
|
if semBounded(e, b, delta, upper.booleanNot(), _)
|
||||||
then delta != 0 and result = "==" + getBoundString(b, delta)
|
then delta != 0 and result = "==" + getBoundString(b, delta)
|
||||||
|
|||||||
@@ -18,20 +18,20 @@ int test2(struct List* p) {
|
|||||||
int count = 0;
|
int count = 0;
|
||||||
for (; p; p = p->next) {
|
for (; p; p = p->next) {
|
||||||
count = (count+1) % 10;
|
count = (count+1) % 10;
|
||||||
range(count); // $ range=<=9
|
range(count); // $ range=<=9 range=>=-9 range=<=count:p+1
|
||||||
}
|
}
|
||||||
range(count); // $ range=<=9
|
range(count); // $ range=>=-9 range=<=9
|
||||||
return count;
|
return count;
|
||||||
}
|
}
|
||||||
|
|
||||||
int test3(struct List* p) {
|
int test3(struct List* p) {
|
||||||
int count = 0;
|
int count = 0;
|
||||||
for (; p; p = p->next) {
|
for (; p; p = p->next) {
|
||||||
range(count++); // $ range=<=9
|
range(count++); // $ range=>=-9 range=<=9
|
||||||
count = count % 10;
|
count = count % 10;
|
||||||
range(count); // $ range=<=9
|
range(count); // $ range=<=9 range=>=-9 range="<=... +++0" range=<=count:p+1
|
||||||
}
|
}
|
||||||
range(count); // $ range=<=9
|
range(count); // $ range=>=-9 range=<=9
|
||||||
return count;
|
return count;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -42,11 +42,11 @@ int test4() {
|
|||||||
range(i); // $ range=<=1 MISSING: range=>=0
|
range(i); // $ range=<=1 MISSING: range=>=0
|
||||||
range(total);
|
range(total);
|
||||||
total += i;
|
total += i;
|
||||||
range(total);
|
range(total); // $ range=<=i+1 range=<=i+1 range=>=0 range=>=i+0
|
||||||
}
|
}
|
||||||
range(total);
|
range(total); // $ range=>=0
|
||||||
range(i); // $ range===2
|
range(i); // $ range===2
|
||||||
range(total + i); // $ MISSING:range=>=i+1
|
range(total + i); // $ range===i+2 range=>=2 range=>=i+0
|
||||||
return total + i;
|
return total + i;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -54,14 +54,14 @@ int test5() {
|
|||||||
int i = 0;
|
int i = 0;
|
||||||
int total = 0;
|
int total = 0;
|
||||||
for (i = 0; i < 2; i++) {
|
for (i = 0; i < 2; i++) {
|
||||||
range(i); // $ range=<=1 MISSING:range=>=0
|
range(i); // $ range=<=1 range=>=0
|
||||||
range(total);
|
range(total); // $ range=>=0
|
||||||
total += i;
|
total += i;
|
||||||
range(total);
|
range(total); // $ range=<=i+1 range=>=0 range=>=i+0
|
||||||
}
|
}
|
||||||
range(total);
|
range(total); // $ range=>=0
|
||||||
range(i); // $ range===2
|
range(i); // $ range===2
|
||||||
range(total + i); // $ MISSING:range=>=i+1
|
range(total + i); // $ range===i+2 range=>=2 range=>=i+0
|
||||||
return total + i;
|
return total + i;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -69,10 +69,10 @@ int test6() {
|
|||||||
int i = 0;
|
int i = 0;
|
||||||
int total = 0;
|
int total = 0;
|
||||||
for (i = 0; i+2 < 4; i = i+1) {
|
for (i = 0; i+2 < 4; i = i+1) {
|
||||||
range(i); // $ range=<=1 MISSING:range=>=0
|
range(i); // $ range=<=1 range=>=0
|
||||||
range(total);
|
range(total); // $ range=>=0
|
||||||
total += i;
|
total += i;
|
||||||
range(total);
|
range(total); // $ range=<=i+1 range=>=0 range=>=i+0
|
||||||
}
|
}
|
||||||
return total + i;
|
return total + i;
|
||||||
}
|
}
|
||||||
@@ -149,7 +149,7 @@ int test11(char *p) {
|
|||||||
range(*p);
|
range(*p);
|
||||||
}
|
}
|
||||||
if (c == ':') {
|
if (c == ':') {
|
||||||
range(c);
|
range(c); // $ range===58
|
||||||
c = *p;
|
c = *p;
|
||||||
range(*p);
|
range(*p);
|
||||||
if (c != '\0') {
|
if (c != '\0') {
|
||||||
@@ -233,9 +233,9 @@ int test_unary(int a) {
|
|||||||
range(b); // $ range=<=11 range=>=3
|
range(b); // $ range=<=11 range=>=3
|
||||||
int c = -a;
|
int c = -a;
|
||||||
range(c); // $ range=<=-3 range=>=-11
|
range(c); // $ range=<=-3 range=>=-11
|
||||||
range(b+c); // $ range=<=10 range="<=+ ...:a-1" range=">=- ...+1" range=>=-10
|
range(b+c); // $ range=<=8 range=>=-8
|
||||||
total += b+c;
|
total += b+c;
|
||||||
range(total);
|
range(total); // $ range=<=8 range=>=-8
|
||||||
}
|
}
|
||||||
if (0 <= a && a <= 11) {
|
if (0 <= a && a <= 11) {
|
||||||
range(a); // $ range=<=11 range=>=0
|
range(a); // $ range=<=11 range=>=0
|
||||||
@@ -245,7 +245,7 @@ int test_unary(int a) {
|
|||||||
range(c);
|
range(c);
|
||||||
range(b+c); // $ range=<=11 range="<=+ ...:a+0" MISSING:range=">=- ...+0"
|
range(b+c); // $ range=<=11 range="<=+ ...:a+0" MISSING:range=">=- ...+0"
|
||||||
total += b+c;
|
total += b+c;
|
||||||
range(total);
|
range(total); // $ range=<=0+11 range=<=19 range=>=0-11 range=>=-19
|
||||||
}
|
}
|
||||||
if (-7 <= a && a <= 11) {
|
if (-7 <= a && a <= 11) {
|
||||||
range(a); // $ range=<=11 range=>=-7
|
range(a); // $ range=<=11 range=>=-7
|
||||||
@@ -253,9 +253,9 @@ int test_unary(int a) {
|
|||||||
range(b); // $ range=<=11 range=>=-7
|
range(b); // $ range=<=11 range=>=-7
|
||||||
int c = -a;
|
int c = -a;
|
||||||
range(c); // $ range=<=7 range=>=-11
|
range(c); // $ range=<=7 range=>=-11
|
||||||
range(b+c);
|
range(b+c); // $ range=<=18 range=>=-18
|
||||||
total += b+c;
|
total += b+c;
|
||||||
range(total);
|
range(total); // $ range="<=- ...+18" range=">=- ...-18" range=<=0+29 range=<=37 range=>=0-29 range=>=-37
|
||||||
}
|
}
|
||||||
if (-7 <= a && a <= 1) {
|
if (-7 <= a && a <= 1) {
|
||||||
range(a); // $ range=<=1 range=>=-7
|
range(a); // $ range=<=1 range=>=-7
|
||||||
@@ -263,9 +263,9 @@ int test_unary(int a) {
|
|||||||
range(b); // $ range=<=1 range=>=-7
|
range(b); // $ range=<=1 range=>=-7
|
||||||
int c = -a;
|
int c = -a;
|
||||||
range(c); // $ range=<=7 range=>=-1
|
range(c); // $ range=<=7 range=>=-1
|
||||||
range(b+c);
|
range(b+c); // $ range=<=8 range=>=-8
|
||||||
total += b+c;
|
total += b+c;
|
||||||
range(total);
|
range(total); // $ range="<=- ...+8" range="<=- ...+26" range=">=- ...-8" range=">=- ...-26" range=<=0+37 range=<=45 range=>=0-37 range=>=-45
|
||||||
}
|
}
|
||||||
if (-7 <= a && a <= 0) {
|
if (-7 <= a && a <= 0) {
|
||||||
range(a); // $ range=<=0 range=>=-7
|
range(a); // $ range=<=0 range=>=-7
|
||||||
@@ -275,7 +275,7 @@ int test_unary(int a) {
|
|||||||
range(c);
|
range(c);
|
||||||
range(b+c); // $ range=">=+ ...:a+0" range=>=-7 MISSING:range="<=- ...+0"
|
range(b+c); // $ range=">=+ ...:a+0" range=>=-7 MISSING:range="<=- ...+0"
|
||||||
total += b+c;
|
total += b+c;
|
||||||
range(total);
|
range(total); // $ range="<=- ...+7" range="<=- ...+15" range="<=- ...+33" range=">=- ...-7" range=">=- ...-15" range=">=- ...-33" range=<=0+44 range=<=52 range=>=0-44 range=>=-52
|
||||||
}
|
}
|
||||||
if (-7 <= a && a <= -2) {
|
if (-7 <= a && a <= -2) {
|
||||||
range(a); // $ range=<=-2 range=>=-7
|
range(a); // $ range=<=-2 range=>=-7
|
||||||
@@ -283,10 +283,12 @@ int test_unary(int a) {
|
|||||||
range(b); // $ range=<=-2 range=>=-7
|
range(b); // $ range=<=-2 range=>=-7
|
||||||
int c = -a;
|
int c = -a;
|
||||||
range(c); // $ range=<=7 range=>=2
|
range(c); // $ range=<=7 range=>=2
|
||||||
range(b+c); // $ range="<=- ...-1" range=">=+ ...:a+1" range=>=-6 range=<=6
|
range(b+c); // $ range=<=5 range=>=-5
|
||||||
range(c);
|
total += b+c;
|
||||||
|
range(total); // $ range="<=- ...+5" range="<=- ...+12" range="<=- ...+20" range="<=- ...+38" range=">=- ...-5" range=">=- ...-12" range=">=- ...-20" range=">=- ...-38" range=<=0+49 range=<=57 range=>=0-49 range=>=-57
|
||||||
}
|
}
|
||||||
range(total);
|
range(total); // $ range="<=- ...+5" range="<=- ...+12" range="<=- ...+20" range="<=- ...+38" range=">=- ...-5" range=">=- ...-12" range=">=- ...-20" range=">=- ...-38" range=<=0+49 range=<=57 range=>=0-49 range=>=-57
|
||||||
|
return total;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
@@ -298,17 +300,17 @@ int test_mult01(int a, int b) {
|
|||||||
range(a); // $ range=<=11 range=>=3
|
range(a); // $ range=<=11 range=>=3
|
||||||
range(b); // $ range=<=23 range=>=5
|
range(b); // $ range=<=23 range=>=5
|
||||||
int r = a*b; // 15 .. 253
|
int r = a*b; // 15 .. 253
|
||||||
range(r);
|
range(r); // $ range=<=253 range=>=15
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=>=1
|
range(total); // $ range=<=253 range=>=15
|
||||||
}
|
}
|
||||||
if (3 <= a && a <= 11 && 0 <= b && b <= 23) {
|
if (3 <= a && a <= 11 && 0 <= b && b <= 23) {
|
||||||
range(a); // $ range=<=11 range=>=3
|
range(a); // $ range=<=11 range=>=3
|
||||||
range(b); // $ range=<=23 range=>=0
|
range(b); // $ range=<=23 range=>=0
|
||||||
int r = a*b; // 0 .. 253
|
int r = a*b; // 0 .. 253
|
||||||
range(r);
|
range(r); // $ range=<=253 range=>=0
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=>=0 range=>=3+0
|
range(total); // $ range=<=3+253 range=<=506 range=>=0 range=>=3+0
|
||||||
}
|
}
|
||||||
if (3 <= a && a <= 11 && -13 <= b && b <= 23) {
|
if (3 <= a && a <= 11 && -13 <= b && b <= 23) {
|
||||||
range(a); // $ range=<=11 range=>=3
|
range(a); // $ range=<=11 range=>=3
|
||||||
@@ -316,25 +318,25 @@ int test_mult01(int a, int b) {
|
|||||||
int r = a*b; // -143 .. 253
|
int r = a*b; // -143 .. 253
|
||||||
range(r);
|
range(r);
|
||||||
total += r;
|
total += r;
|
||||||
range(total);
|
range(total); // $ MISSING: range=">=... * ...+0"
|
||||||
}
|
}
|
||||||
if (3 <= a && a <= 11 && -13 <= b && b <= 0) {
|
if (3 <= a && a <= 11 && -13 <= b && b <= 0) {
|
||||||
range(a); // $ range=<=11 range=>=3
|
range(a); // $ range=<=11 range=>=3
|
||||||
range(b); // $ range=<=0 range=>=-13
|
range(b); // $ range=<=0 range=>=-13
|
||||||
int r = a*b; // -143 .. 0
|
int r = a*b; // -143 .. 0
|
||||||
range(r);
|
range(r); // $ range=<=0 range=>=-143
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ MISSING:range=<=3+0
|
range(total); // $ range=<=3+0 range=>=3-143
|
||||||
}
|
}
|
||||||
if (3 <= a && a <= 11 && -13 <= b && b <= -7) {
|
if (3 <= a && a <= 11 && -13 <= b && b <= -7) {
|
||||||
range(a); // $ range=<=11 range=>=3
|
range(a); // $ range=<=11 range=>=3
|
||||||
range(b); // $ range=<=-7 range=>=-13
|
range(b); // $ range=<=-7 range=>=-13
|
||||||
int r = a*b; // -143 .. -21
|
int r = a*b; // -143 .. -21
|
||||||
range(r);
|
range(r); // $ range=<=-21 range=>=-143
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ MISSING:range=<=3-1
|
range(total); // $ range=<=3-21 range=>=3-143 range=>=3-286
|
||||||
}
|
}
|
||||||
range(total); // $ MISSING:range=<=3+0
|
range(total); // $ range=<=3+0 range=>=3-143 range=>=3-286
|
||||||
return total;
|
return total;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -346,17 +348,17 @@ int test_mult02(int a, int b) {
|
|||||||
range(a); // $ range=<=11 range=>=0
|
range(a); // $ range=<=11 range=>=0
|
||||||
range(b); // $ range=<=23 range=>=5
|
range(b); // $ range=<=23 range=>=5
|
||||||
int r = a*b; // 0 .. 253
|
int r = a*b; // 0 .. 253
|
||||||
range(r);
|
range(r); // $ range=<=253 range=>=0
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=>=0
|
range(total); // $ range=>=0 range=<=253
|
||||||
}
|
}
|
||||||
if (0 <= a && a <= 11 && 0 <= b && b <= 23) {
|
if (0 <= a && a <= 11 && 0 <= b && b <= 23) {
|
||||||
range(a); // $ range=<=11 range=>=0
|
range(a); // $ range=<=11 range=>=0
|
||||||
range(b); // $ range=<=23 range=>=0
|
range(b); // $ range=<=23 range=>=0
|
||||||
int r = a*b; // 0 .. 253
|
int r = a*b; // 0 .. 253
|
||||||
range(r);
|
range(r); // $ range=<=253 range=>=0
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=>=0 range=>=0+0
|
range(total); // $ range=>=0 range=>=0+0 range=<=0+253 range=<=506
|
||||||
}
|
}
|
||||||
if (0 <= a && a <= 11 && -13 <= b && b <= 23) {
|
if (0 <= a && a <= 11 && -13 <= b && b <= 23) {
|
||||||
range(a); // $ range=<=11 range=>=0
|
range(a); // $ range=<=11 range=>=0
|
||||||
@@ -364,25 +366,25 @@ int test_mult02(int a, int b) {
|
|||||||
int r = a*b; // -143 .. 253
|
int r = a*b; // -143 .. 253
|
||||||
range(r);
|
range(r);
|
||||||
total += r;
|
total += r;
|
||||||
range(total);
|
range(total); // $ MISSING: range=">=... * ...+0"
|
||||||
}
|
}
|
||||||
if (0 <= a && a <= 11 && -13 <= b && b <= 0) {
|
if (0 <= a && a <= 11 && -13 <= b && b <= 0) {
|
||||||
range(a); // $ range=<=11 range=>=0
|
range(a); // $ range=<=11 range=>=0
|
||||||
range(b); // $ range=<=0 range=>=-13
|
range(b); // $ range=<=0 range=>=-13
|
||||||
int r = a*b; // -143 .. 0
|
int r = a*b; // -143 .. 0
|
||||||
range(r);
|
range(r); // $ range=<=0 range=>=-143
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ MISSING:range=<=0+0
|
range(total); // $ range=<=0+0 range=>=0-143
|
||||||
}
|
}
|
||||||
if (0 <= a && a <= 11 && -13 <= b && b <= -7) {
|
if (0 <= a && a <= 11 && -13 <= b && b <= -7) {
|
||||||
range(a); // $ range=<=11 range=>=0
|
range(a); // $ range=<=11 range=>=0
|
||||||
range(b); // $ range=<=-7 range=>=-13
|
range(b); // $ range=<=-7 range=>=-13
|
||||||
int r = a*b; // -143 .. 0
|
int r = a*b; // -143 .. 0
|
||||||
range(r);
|
range(r); // $ range=<=0 range=>=-143
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ MISSING:range=<=0+0
|
range(total); // $ range=<=0+0 range=>=0-143 range=>=0-286
|
||||||
}
|
}
|
||||||
range(total); // $ MISSING:range=<=0+0
|
range(total); // $ range=<=0+0 range=>=0-143 range=>=0-286
|
||||||
return total;
|
return total;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -443,15 +445,15 @@ int test_mult04(int a, int b) {
|
|||||||
range(b); // $ range=<=23 range=>=5
|
range(b); // $ range=<=23 range=>=5
|
||||||
int r = a*b; // -391 .. 0
|
int r = a*b; // -391 .. 0
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=<=0
|
range(total); // $ range=<=0 range=>=-391
|
||||||
}
|
}
|
||||||
if (-17 <= a && a <= 0 && 0 <= b && b <= 23) {
|
if (-17 <= a && a <= 0 && 0 <= b && b <= 23) {
|
||||||
range(a); // $ range=<=0 range=>=-17
|
range(a); // $ range=<=0 range=>=-17
|
||||||
range(b); // $ range=<=23 range=>=0
|
range(b); // $ range=<=23 range=>=0
|
||||||
int r = a*b; // -391 .. 0
|
int r = a*b; // -391 .. 0
|
||||||
range(r);
|
range(r); // $ range=<=0 range=>=-391
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range="<=- ...+0" range=<=0
|
range(total); // $ range="<=- ...+0" range=<=0 range=">=- ...-391" range=>=-782
|
||||||
}
|
}
|
||||||
if (-17 <= a && a <= 0 && -13 <= b && b <= 23) {
|
if (-17 <= a && a <= 0 && -13 <= b && b <= 23) {
|
||||||
range(a); // $ range=<=0 range=>=-17
|
range(a); // $ range=<=0 range=>=-17
|
||||||
@@ -459,25 +461,25 @@ int test_mult04(int a, int b) {
|
|||||||
int r = a*b; // -391 .. 221
|
int r = a*b; // -391 .. 221
|
||||||
range(r);
|
range(r);
|
||||||
total += r;
|
total += r;
|
||||||
range(total);
|
range(total); // $ MISSING: range="<=... * ...+0"
|
||||||
}
|
}
|
||||||
if (-17 <= a && a <= 0 && -13 <= b && b <= 0) {
|
if (-17 <= a && a <= 0 && -13 <= b && b <= 0) {
|
||||||
range(a); // $ range=<=0 range=>=-17
|
range(a); // $ range=<=0 range=>=-17
|
||||||
range(b); // $ range=<=0 range=>=-13
|
range(b); // $ range=<=0 range=>=-13
|
||||||
int r = a*b; // 0 .. 221
|
int r = a*b; // 0 .. 221
|
||||||
range(r);
|
range(r); // $ range=<=221 range=>=0
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ MISSING:range=">=- ...+0"
|
range(total); // $ range="<=- ...+221" range=">=- ...+0"
|
||||||
}
|
}
|
||||||
if (-17 <= a && a <= 0 && -13 <= b && b <= -7) {
|
if (-17 <= a && a <= 0 && -13 <= b && b <= -7) {
|
||||||
range(a); // $ range=<=0 range=>=-17
|
range(a); // $ range=<=0 range=>=-17
|
||||||
range(b); // $ range=<=-7 range=>=-13
|
range(b); // $ range=<=-7 range=>=-13
|
||||||
int r = a*b; // 0 .. 221
|
int r = a*b; // 0 .. 221
|
||||||
range(r);
|
range(r); // $ range=<=221 range=>=0
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ MISSING:range=">=- ...+0"
|
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
|
||||||
}
|
}
|
||||||
range(total); // $ MISSING:range=">=- ...+0"
|
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
|
||||||
return total;
|
return total;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -489,17 +491,17 @@ int test_mult05(int a, int b) {
|
|||||||
range(a); // $ range=<=-2 range=>=-17
|
range(a); // $ range=<=-2 range=>=-17
|
||||||
range(b); // $ range=<=23 range=>=5
|
range(b); // $ range=<=23 range=>=5
|
||||||
int r = a*b; // -391 .. -10
|
int r = a*b; // -391 .. -10
|
||||||
range(r);
|
range(r); // $ range=<=-10 range=>=-391
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=<=-1
|
range(total); // $ range=<=-10 range=>=-391
|
||||||
}
|
}
|
||||||
if (-17 <= a && a <= -2 && 0 <= b && b <= 23) {
|
if (-17 <= a && a <= -2 && 0 <= b && b <= 23) {
|
||||||
range(a); // $ range=<=-2 range=>=-17
|
range(a); // $ range=<=-2 range=>=-17
|
||||||
range(b); // $ range=<=23 range=>=0
|
range(b); // $ range=<=23 range=>=0
|
||||||
int r = a*b; // -391 .. 0
|
int r = a*b; // -391 .. 0
|
||||||
range(r);
|
range(r); // $ range=<=0 range=>=-391
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range="<=- ...+0" range=<=0
|
range(total); // $ range="<=- ...+0" range=<=0 range=">=- ...-391" range=>=-782
|
||||||
}
|
}
|
||||||
if (-17 <= a && a <= -2 && -13 <= b && b <= 23) {
|
if (-17 <= a && a <= -2 && -13 <= b && b <= 23) {
|
||||||
range(a); // $ range=<=-2 range=>=-17
|
range(a); // $ range=<=-2 range=>=-17
|
||||||
@@ -507,25 +509,25 @@ int test_mult05(int a, int b) {
|
|||||||
int r = a*b; // -391 .. 221
|
int r = a*b; // -391 .. 221
|
||||||
range(r);
|
range(r);
|
||||||
total += r;
|
total += r;
|
||||||
range(total);
|
range(total); // $ MISSING: range="<=... * ...+0"
|
||||||
}
|
}
|
||||||
if (-17 <= a && a <= -2 && -13 <= b && b <= 0) {
|
if (-17 <= a && a <= -2 && -13 <= b && b <= 0) {
|
||||||
range(a); // $ range=<=-2 range=>=-17
|
range(a); // $ range=<=-2 range=>=-17
|
||||||
range(b); // $ range=<=0 range=>=-13
|
range(b); // $ range=<=0 range=>=-13
|
||||||
int r = a*b; // 0 .. 221
|
int r = a*b; // 0 .. 221
|
||||||
range(r);
|
range(r); // $ range=<=221 range=>=0
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ MISSING:range=">=- ...+0"
|
range(total); // $ range="<=- ...+221" range=">=- ...+0"
|
||||||
}
|
}
|
||||||
if (-17 <= a && a <= -2 && -13 <= b && b <= -7) {
|
if (-17 <= a && a <= -2 && -13 <= b && b <= -7) {
|
||||||
range(a); // $ range=<=-2 range=>=-17
|
range(a); // $ range=<=-2 range=>=-17
|
||||||
range(b); // $ range=<=-7 range=>=-13
|
range(b); // $ range=<=-7 range=>=-13
|
||||||
int r = a*b; // 14 .. 221
|
int r = a*b; // 14 .. 221
|
||||||
range(r);
|
range(r); // $ range=<=221 range=>=14
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ MISSING:range=">=- ...+1"
|
range(total); // $ range="<=- ...+221" range="<=- ...+442" range=">=- ...+14"
|
||||||
}
|
}
|
||||||
range(total); // $ MISSING:range=">=- ...+0"
|
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
|
||||||
return total;
|
return total;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -596,7 +598,7 @@ unsigned int test_ternary01(unsigned int x) {
|
|||||||
(range(x), 500); // $ range=<=299
|
(range(x), 500); // $ range=<=299
|
||||||
range(y8); // y8 <= 300
|
range(y8); // y8 <= 300
|
||||||
}
|
}
|
||||||
range(y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8); // $ MISSING:range=">=... = ...:... ? ... : ...+0" MISSING:range=">=call to range+0"
|
range(y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8); // $ MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
|
||||||
return y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8;
|
return y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -626,7 +628,7 @@ unsigned int test_ternary02(unsigned int x) {
|
|||||||
(range(x), 5); // $ range=>=300
|
(range(x), 5); // $ range=>=300
|
||||||
range(y5); // y6 >= 0
|
range(y5); // y6 >= 0
|
||||||
}
|
}
|
||||||
range(y1 + y2 + y3 + y4 + y5); // $ MISSING:range=">=... = ...:... ? ... : ...+0" MISSING:range=">=call to range+0"
|
range(y1 + y2 + y3 + y4 + y5); // $ MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
|
||||||
return y1 + y2 + y3 + y4 + y5;
|
return y1 + y2 + y3 + y4 + y5;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -644,8 +646,8 @@ unsigned int test_comma01(unsigned int x) {
|
|||||||
y += 3,
|
y += 3,
|
||||||
range(y), // $ MISSING:range="==++ ...:... = ...+4" MISSING:range="==... +++3" range="==... ? ... : ...+5"
|
range(y), // $ MISSING:range="==++ ...:... = ...+4" MISSING:range="==... +++3" range="==... ? ... : ...+5"
|
||||||
y);
|
y);
|
||||||
range(y2); // $ MISSING:range="==++ ...:... = ...+4" MISSING:range="==... +++3" MISSING:range="==... ? ... : ...+5"
|
range(y2); // $ range="==++ ...:... = ...+4" range="==... +++3" range="==... ? ... : ...+5"
|
||||||
range(y1 + y2); // $ MISSING:range=">=++ ...:... = ...+5" MISSING:range=">=... +++4" MISSING:range=">=... += ...:... = ...+1" MISSING:range=">=... ? ... : ...+6"
|
range(y1 + y2); // $ MISSING: range=">=++ ...:... = ...+5" range=">=... +++4" range=">=... += ...:... = ...+1" range=">=... ? ... : ...+6"
|
||||||
return y1 + y2;
|
return y1 + y2;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -683,7 +685,7 @@ int test_unsigned_mult01(unsigned int a, unsigned b) {
|
|||||||
int r = a*b; // 15 .. 253
|
int r = a*b; // 15 .. 253
|
||||||
range(r);
|
range(r);
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=>=1
|
range(total); // $ MISSING: range=>=1
|
||||||
}
|
}
|
||||||
if (3 <= a && a <= 11 && 0 <= b && b <= 23) {
|
if (3 <= a && a <= 11 && 0 <= b && b <= 23) {
|
||||||
range(a); // $ range=<=11 range=>=3
|
range(a); // $ range=<=11 range=>=3
|
||||||
@@ -691,7 +693,7 @@ int test_unsigned_mult01(unsigned int a, unsigned b) {
|
|||||||
int r = a*b; // 0 .. 253
|
int r = a*b; // 0 .. 253
|
||||||
range(r);
|
range(r);
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=">=(unsigned int)...+0" range=>=0
|
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
|
||||||
}
|
}
|
||||||
if (3 <= a && a <= 11 && 13 <= b && b <= 23) {
|
if (3 <= a && a <= 11 && 13 <= b && b <= 23) {
|
||||||
range(a); // $ range=<=11 range=>=3
|
range(a); // $ range=<=11 range=>=3
|
||||||
@@ -699,9 +701,9 @@ int test_unsigned_mult01(unsigned int a, unsigned b) {
|
|||||||
int r = a*b; // 39 .. 253
|
int r = a*b; // 39 .. 253
|
||||||
range(r);
|
range(r);
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=">=(unsigned int)...+1" range=>=1
|
range(total); // $ MISSING: range=">=(unsigned int)...+1" range=>=1
|
||||||
}
|
}
|
||||||
range(total); // $ range=">=(unsigned int)...+0" range=>=0
|
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
|
||||||
return total;
|
return total;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -713,23 +715,23 @@ int test_unsigned_mult02(unsigned b) {
|
|||||||
int r = 11*b; // 55 .. 253
|
int r = 11*b; // 55 .. 253
|
||||||
range(r);
|
range(r);
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=>=1
|
range(total); // $ MISSING: range=>=1
|
||||||
}
|
}
|
||||||
if (0 <= b && b <= 23) {
|
if (0 <= b && b <= 23) {
|
||||||
range(b); // $ range=<=23 range=>=0
|
range(b); // $ range=<=23 range=>=0
|
||||||
int r = 11*b; // 0 .. 253
|
int r = 11*b; // 0 .. 253
|
||||||
range(r);
|
range(r);
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=">=(unsigned int)...+0" range=>=0
|
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
|
||||||
}
|
}
|
||||||
if (13 <= b && b <= 23) {
|
if (13 <= b && b <= 23) {
|
||||||
range(b); // $ range=<=23 range=>=13
|
range(b); // $ range=<=23 range=>=13
|
||||||
int r = 11*b; // 143 .. 253
|
int r = 11*b; // 143 .. 253
|
||||||
range(r);
|
range(r);
|
||||||
total += r;
|
total += r;
|
||||||
range(total); // $ range=">=(unsigned int)...+1" range=>=1
|
range(total); // $ MISSING: range=">=(unsigned int)...+1" range=>=1
|
||||||
}
|
}
|
||||||
range(total); // $ range=">=(unsigned int)...+0" range=>=0
|
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
|
||||||
return total;
|
return total;
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -739,7 +741,7 @@ unsigned long mult_rounding() {
|
|||||||
range(y); // $ range===1000000003
|
range(y); // $ range===1000000003
|
||||||
range(x); // $ range===1000000003
|
range(x); // $ range===1000000003
|
||||||
xy = x * y;
|
xy = x * y;
|
||||||
range(xy);
|
range(xy); // $ range===1000000006000000000
|
||||||
return xy; // BUG: upper bound should be >= 1000000006000000009UL
|
return xy; // BUG: upper bound should be >= 1000000006000000009UL
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -759,13 +761,13 @@ unsigned long mult_lower_bound(unsigned int ui, unsigned long ul) {
|
|||||||
range(ui); // $ range=>=10
|
range(ui); // $ range=>=10
|
||||||
range((unsigned long)ui); // $ range=>=10
|
range((unsigned long)ui); // $ range=>=10
|
||||||
unsigned long result = (unsigned long)ui * ui;
|
unsigned long result = (unsigned long)ui * ui;
|
||||||
range(result);
|
range(result); // $ range=>=100 range=>=100
|
||||||
return result; // BUG: upper bound should be >= 18446744065119617025
|
return result; // BUG: upper bound should be >= 18446744065119617025
|
||||||
}
|
}
|
||||||
if (ul >= 10) {
|
if (ul >= 10) {
|
||||||
range(ul); // $ range=>=10
|
range(ul); // $ range=>=10
|
||||||
unsigned long result = ul * ul;
|
unsigned long result = ul * ul;
|
||||||
range(result);
|
range(result); // $ range=>=100
|
||||||
return result; // BUG: lower bound should be 0 (overflow is possible)
|
return result; // BUG: lower bound should be 0 (overflow is possible)
|
||||||
}
|
}
|
||||||
return 0;
|
return 0;
|
||||||
@@ -775,7 +777,7 @@ unsigned long mul_assign(unsigned int ui) {
|
|||||||
if (ui <= 10 && ui >= 2) {
|
if (ui <= 10 && ui >= 2) {
|
||||||
range(ui); // $ range=<=10 range=>=2
|
range(ui); // $ range=<=10 range=>=2
|
||||||
ui *= ui + 0;
|
ui *= ui + 0;
|
||||||
range(ui);
|
range(ui); // $ range=<=100 range=>=4
|
||||||
return ui; // 4 .. 100
|
return ui; // 4 .. 100
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -788,7 +790,7 @@ unsigned long mul_assign(unsigned int ui) {
|
|||||||
range(ulconst); // $ range===10
|
range(ulconst); // $ range===10
|
||||||
ulconst *= 4;
|
ulconst *= 4;
|
||||||
range(ulconst); // $ range===40
|
range(ulconst); // $ range===40
|
||||||
range(uiconst + ulconst); // $ range=">=... *= ...+1" range=">=... + ...+0" range=>=41
|
range(uiconst + ulconst); // $ range===80
|
||||||
return uiconst + ulconst; // 40 .. 40 for both
|
return uiconst + ulconst; // 40 .. 40 for both
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -811,7 +813,7 @@ int mul_by_constant(int i, int j) {
|
|||||||
range(i); // $ range===-1
|
range(i); // $ range===-1
|
||||||
range((int)0xffFFffFF); // $ range===-1
|
range((int)0xffFFffFF); // $ range===-1
|
||||||
i = i * (int)0xffFFffFF; // fully converted literal is -1
|
i = i * (int)0xffFFffFF; // fully converted literal is -1
|
||||||
range(i); // 1 .. 1
|
range(i); // $ range===1
|
||||||
}
|
}
|
||||||
i = i * -1;
|
i = i * -1;
|
||||||
range( i); // -2^31 .. 2^31-1
|
range( i); // -2^31 .. 2^31-1
|
||||||
@@ -854,18 +856,18 @@ int notequal_type_endpoint(unsigned n) {
|
|||||||
|
|
||||||
void notequal_refinement(short n) {
|
void notequal_refinement(short n) {
|
||||||
if (n < 0) {
|
if (n < 0) {
|
||||||
range(n);
|
range(n); // $ range=<=-1
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
if (n == 0) {
|
if (n == 0) {
|
||||||
range(n); // 0 .. 0
|
range(n); // 0 .. 0
|
||||||
} else {
|
} else {
|
||||||
range(n); // 1 ..
|
range(n); // $ range=>=1
|
||||||
}
|
}
|
||||||
|
|
||||||
if (n) {
|
if (n) {
|
||||||
range(n); // 1 ..
|
range(n); // $ range=>=1
|
||||||
} else {
|
} else {
|
||||||
range(n); // 0 .. 0
|
range(n); // 0 .. 0
|
||||||
}
|
}
|
||||||
@@ -881,16 +883,16 @@ void notequal_refinement(short n) {
|
|||||||
void notequal_variations(short n, float f) {
|
void notequal_variations(short n, float f) {
|
||||||
if (n != 0) {
|
if (n != 0) {
|
||||||
if (n >= 0) {
|
if (n >= 0) {
|
||||||
range(n); // 1 .. [BUG: we can't handle `!=` coming first]
|
range(n); // $ range=>=1
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (n >= 5) {
|
if (n >= 5) {
|
||||||
if (2 * n - 10 == 0) { // Same as `n == 10/2` (modulo overflow)
|
if (2 * n - 10 == 0) { // Same as `n == 10/2` (modulo overflow)
|
||||||
range(n);
|
range(n); // $ range=>=5 MISSING: range===5
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
range(n); // 6 ..
|
range(n); // $ range=>=5 MISSING: range=>=6
|
||||||
}
|
}
|
||||||
|
|
||||||
if (n != -32768 && n != -32767) {
|
if (n != -32768 && n != -32767) {
|
||||||
@@ -898,8 +900,12 @@ void notequal_variations(short n, float f) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
if (n >= 0) {
|
if (n >= 0) {
|
||||||
n ? (range(n), n) : (range(n), n); // ? 1.. : 0..0
|
n ?
|
||||||
!n ? (range(n), n) : (range(n), n); // ? 0..0 : 1..
|
(range(n), n) // $ range=>=1
|
||||||
|
: (range(n), n); // $ MISSING: range===0
|
||||||
|
!n ?
|
||||||
|
(range(n), n) // $ MISSING: range===0
|
||||||
|
: (range(n), n); // $ range=>=1
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -915,7 +921,7 @@ void two_bounds_from_one_test(short ss, unsigned short us) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
if (ss < 0x8001) { // Lower bound removed in `getDefLowerBounds`
|
if (ss < 0x8001) { // Lower bound removed in `getDefLowerBounds`
|
||||||
range(ss); // -32768 .. 32767
|
range(ss); // $ range=<=32768 MISSING: range=>=-32768
|
||||||
}
|
}
|
||||||
|
|
||||||
if ((short)us >= 0) {
|
if ((short)us >= 0) {
|
||||||
@@ -940,7 +946,7 @@ void widen_recursive_expr() {
|
|||||||
for (s = 0; s < 10; s++) {
|
for (s = 0; s < 10; s++) {
|
||||||
range(s); // $ range=<=9 MISSING:range=>=0
|
range(s); // $ range=<=9 MISSING:range=>=0
|
||||||
int result = s + s;
|
int result = s + s;
|
||||||
range(result); // 0 .. 18
|
range(result); // $ range=<=18 range=<=s+9 range=>=0 range=>=s+0
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -958,7 +964,22 @@ void guard_bound_out_of_range(void) {
|
|||||||
|
|
||||||
void test_mod(int s) {
|
void test_mod(int s) {
|
||||||
int s2 = s % 5;
|
int s2 = s % 5;
|
||||||
range(s2); // $ range=<=4 // -4 .. 4
|
range(s2); // $ range=>=-4 range=<=4
|
||||||
|
}
|
||||||
|
|
||||||
|
void test_mod_neg(int s) {
|
||||||
|
int s2 = s % -5;
|
||||||
|
range(s2); // $ range=>=-4 range=<=4
|
||||||
|
}
|
||||||
|
|
||||||
|
void test_mod_ternary(int s, bool b) {
|
||||||
|
int s2 = s % (b ? 5 : 500);
|
||||||
|
range(s2); // $ range=>=-499 range=<=499 range="<=... ? ... : ...-1"
|
||||||
|
}
|
||||||
|
|
||||||
|
void test_mod_ternary2(int s, bool b1, bool b2) {
|
||||||
|
int s2 = s % (b1 ? (b2 ? 5 : -5000) : -500000);
|
||||||
|
range(s2); // $ range=>=-499999 range=<=499999
|
||||||
}
|
}
|
||||||
|
|
||||||
void exit(int);
|
void exit(int);
|
||||||
|
|||||||
@@ -7,7 +7,7 @@
|
|||||||
}
|
}
|
||||||
|
|
||||||
if (y - 2 == x && y > 300) {
|
if (y - 2 == x && y > 300) {
|
||||||
range(x + y); // $ range=>=300 range=>=x+1 range=>=y-1
|
range(x + y); // $ range=<=802 range=>=600
|
||||||
return x + y;
|
return x + y;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@@ -4,6 +4,7 @@ import experimental.semmle.code.cpp.semantic.Semantic
|
|||||||
import experimental.semmle.code.cpp.semantic.analysis.RangeUtils
|
import experimental.semmle.code.cpp.semantic.analysis.RangeUtils
|
||||||
import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
|
import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
|
||||||
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisSpecific
|
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisSpecific
|
||||||
|
import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
|
||||||
import semmle.code.cpp.ir.IR as IR
|
import semmle.code.cpp.ir.IR as IR
|
||||||
import TestUtilities.InlineExpectationsTest
|
import TestUtilities.InlineExpectationsTest
|
||||||
|
|
||||||
@@ -16,7 +17,7 @@ class SignAnalysisTest extends InlineExpectationsTest {
|
|||||||
|
|
||||||
override predicate hasActualResult(Location location, string element, string tag, string value) {
|
override predicate hasActualResult(Location location, string element, string tag, string value) {
|
||||||
exists(SemExpr e, IR::CallInstruction call |
|
exists(SemExpr e, IR::CallInstruction call |
|
||||||
call.getArgument(0) = e and
|
getSemanticExpr(call.getArgument(0)) = e and
|
||||||
call.getStaticCallTarget().hasName("sign") and
|
call.getStaticCallTarget().hasName("sign") and
|
||||||
tag = "sign" and
|
tag = "sign" and
|
||||||
element = e.toString() and
|
element = e.toString() and
|
||||||
|
|||||||
@@ -1814,3 +1814,81 @@ ssa.cpp:
|
|||||||
|
|
||||||
# 383| Block 5
|
# 383| Block 5
|
||||||
# 383| v383_17(void) = Unreached :
|
# 383| v383_17(void) = Unreached :
|
||||||
|
|
||||||
|
# 401| void vla(int, int, int, bool)
|
||||||
|
# 401| Block 0
|
||||||
|
# 401| v401_1(void) = EnterFunction :
|
||||||
|
# 401| m401_2(unknown) = AliasedDefinition :
|
||||||
|
# 401| m401_3(unknown) = InitializeNonLocal :
|
||||||
|
# 401| m401_4(unknown) = Chi : total:m401_2, partial:m401_3
|
||||||
|
# 401| r401_5(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 401| m401_6(int) = InitializeParameter[n1] : &:r401_5
|
||||||
|
# 401| r401_7(glval<int>) = VariableAddress[n2] :
|
||||||
|
# 401| m401_8(int) = InitializeParameter[n2] : &:r401_7
|
||||||
|
# 401| r401_9(glval<int>) = VariableAddress[n3] :
|
||||||
|
# 401| m401_10(int) = InitializeParameter[n3] : &:r401_9
|
||||||
|
# 401| r401_11(glval<bool>) = VariableAddress[b1] :
|
||||||
|
# 401| m401_12(bool) = InitializeParameter[b1] : &:r401_11
|
||||||
|
# 402| r402_1(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 402| m402_2(int[]) = Uninitialized[b] : &:r402_1
|
||||||
|
# 402| r402_3(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 402| r402_4(int) = Load[n1] : &:r402_3, m401_6
|
||||||
|
# 402| v402_5(void) = NoOp :
|
||||||
|
# 403| r403_1(glval<int[][]>) = VariableAddress[c] :
|
||||||
|
# 403| m403_2(int[][]) = Uninitialized[c] : &:r403_1
|
||||||
|
# 403| m403_3(unknown) = Chi : total:m401_4, partial:m403_2
|
||||||
|
# 403| r403_4(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 403| r403_5(int) = Load[n1] : &:r403_4, m401_6
|
||||||
|
# 403| r403_6(glval<int>) = VariableAddress[n2] :
|
||||||
|
# 403| r403_7(int) = Load[n2] : &:r403_6, m401_8
|
||||||
|
# 403| v403_8(void) = NoOp :
|
||||||
|
# 405| r405_1(int) = Constant[0] :
|
||||||
|
# 405| r405_2(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 405| r405_3(int *) = Convert : r405_2
|
||||||
|
# 405| r405_4(glval<int>) = CopyValue : r405_3
|
||||||
|
# 405| m405_5(int) = Store[?] : &:r405_4, r405_1
|
||||||
|
# 405| m405_6(int[]) = Chi : total:m402_2, partial:m405_5
|
||||||
|
# 406| r406_1(int) = Constant[1] :
|
||||||
|
# 406| r406_2(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 406| r406_3(int *) = Convert : r406_2
|
||||||
|
# 406| r406_4(int) = Constant[0] :
|
||||||
|
# 406| r406_5(glval<int>) = PointerAdd[4] : r406_3, r406_4
|
||||||
|
# 406| m406_6(int) = Store[?] : &:r406_5, r406_1
|
||||||
|
# 406| m406_7(int[]) = Chi : total:m405_6, partial:m406_6
|
||||||
|
# 408| r408_1(int) = Constant[0] :
|
||||||
|
# 408| r408_2(glval<int[][]>) = VariableAddress[c] :
|
||||||
|
# 408| r408_3(int(*)[]) = Convert : r408_2
|
||||||
|
# 408| r408_4(int) = Constant[1] :
|
||||||
|
# 408| r408_5(int(*)[]) = PointerAdd : r408_3, r408_4
|
||||||
|
# 408| r408_6(glval<int[]>) = CopyValue : r408_5
|
||||||
|
# 408| r408_7(int *) = Convert : r408_6
|
||||||
|
# 408| r408_8(glval<int>) = CopyValue : r408_7
|
||||||
|
# 408| m408_9(int) = Store[?] : &:r408_8, r408_1
|
||||||
|
# 408| m408_10(unknown) = Chi : total:m403_3, partial:m408_9
|
||||||
|
# 410| r410_1(glval<bool>) = VariableAddress[b1] :
|
||||||
|
# 410| r410_2(bool) = Load[b1] : &:r410_1, m401_12
|
||||||
|
# 410| v410_3(void) = ConditionalBranch : r410_2
|
||||||
|
#-----| False -> Block 2
|
||||||
|
#-----| True -> Block 1
|
||||||
|
|
||||||
|
# 411| Block 1
|
||||||
|
# 411| r411_1(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 411| m411_2(int[]) = Uninitialized[b] : &:r411_1
|
||||||
|
# 411| r411_3(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 411| r411_4(int) = Load[n1] : &:r411_3, m401_6
|
||||||
|
# 411| v411_5(void) = NoOp :
|
||||||
|
#-----| Goto -> Block 3
|
||||||
|
|
||||||
|
# 413| Block 2
|
||||||
|
# 413| r413_1(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 413| m413_2(int[]) = Uninitialized[b] : &:r413_1
|
||||||
|
# 413| r413_3(glval<int>) = VariableAddress[n2] :
|
||||||
|
# 413| r413_4(int) = Load[n2] : &:r413_3, m401_8
|
||||||
|
# 413| v413_5(void) = NoOp :
|
||||||
|
#-----| Goto -> Block 3
|
||||||
|
|
||||||
|
# 415| Block 3
|
||||||
|
# 415| v415_1(void) = NoOp :
|
||||||
|
# 401| v401_13(void) = ReturnVoid :
|
||||||
|
# 401| v401_14(void) = AliasedUse : ~m408_10
|
||||||
|
# 401| v401_15(void) = ExitFunction :
|
||||||
|
|||||||
@@ -1804,3 +1804,80 @@ ssa.cpp:
|
|||||||
|
|
||||||
# 383| Block 5
|
# 383| Block 5
|
||||||
# 383| v383_17(void) = Unreached :
|
# 383| v383_17(void) = Unreached :
|
||||||
|
|
||||||
|
# 401| void vla(int, int, int, bool)
|
||||||
|
# 401| Block 0
|
||||||
|
# 401| v401_1(void) = EnterFunction :
|
||||||
|
# 401| m401_2(unknown) = AliasedDefinition :
|
||||||
|
# 401| m401_3(unknown) = InitializeNonLocal :
|
||||||
|
# 401| m401_4(unknown) = Chi : total:m401_2, partial:m401_3
|
||||||
|
# 401| r401_5(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 401| m401_6(int) = InitializeParameter[n1] : &:r401_5
|
||||||
|
# 401| r401_7(glval<int>) = VariableAddress[n2] :
|
||||||
|
# 401| m401_8(int) = InitializeParameter[n2] : &:r401_7
|
||||||
|
# 401| r401_9(glval<int>) = VariableAddress[n3] :
|
||||||
|
# 401| m401_10(int) = InitializeParameter[n3] : &:r401_9
|
||||||
|
# 401| r401_11(glval<bool>) = VariableAddress[b1] :
|
||||||
|
# 401| m401_12(bool) = InitializeParameter[b1] : &:r401_11
|
||||||
|
# 402| r402_1(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 402| m402_2(int[]) = Uninitialized[b] : &:r402_1
|
||||||
|
# 402| r402_3(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 402| r402_4(int) = Load[n1] : &:r402_3, m401_6
|
||||||
|
# 402| v402_5(void) = NoOp :
|
||||||
|
# 403| r403_1(glval<int[][]>) = VariableAddress[c] :
|
||||||
|
# 403| m403_2(int[][]) = Uninitialized[c] : &:r403_1
|
||||||
|
# 403| r403_3(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 403| r403_4(int) = Load[n1] : &:r403_3, m401_6
|
||||||
|
# 403| r403_5(glval<int>) = VariableAddress[n2] :
|
||||||
|
# 403| r403_6(int) = Load[n2] : &:r403_5, m401_8
|
||||||
|
# 403| v403_7(void) = NoOp :
|
||||||
|
# 405| r405_1(int) = Constant[0] :
|
||||||
|
# 405| r405_2(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 405| r405_3(int *) = Convert : r405_2
|
||||||
|
# 405| r405_4(glval<int>) = CopyValue : r405_3
|
||||||
|
# 405| m405_5(int) = Store[?] : &:r405_4, r405_1
|
||||||
|
# 405| m405_6(int[]) = Chi : total:m402_2, partial:m405_5
|
||||||
|
# 406| r406_1(int) = Constant[1] :
|
||||||
|
# 406| r406_2(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 406| r406_3(int *) = Convert : r406_2
|
||||||
|
# 406| r406_4(int) = Constant[0] :
|
||||||
|
# 406| r406_5(glval<int>) = PointerAdd[4] : r406_3, r406_4
|
||||||
|
# 406| m406_6(int) = Store[?] : &:r406_5, r406_1
|
||||||
|
# 406| m406_7(int[]) = Chi : total:m405_6, partial:m406_6
|
||||||
|
# 408| r408_1(int) = Constant[0] :
|
||||||
|
# 408| r408_2(glval<int[][]>) = VariableAddress[c] :
|
||||||
|
# 408| r408_3(int(*)[]) = Convert : r408_2
|
||||||
|
# 408| r408_4(int) = Constant[1] :
|
||||||
|
# 408| r408_5(int(*)[]) = PointerAdd : r408_3, r408_4
|
||||||
|
# 408| r408_6(glval<int[]>) = CopyValue : r408_5
|
||||||
|
# 408| r408_7(int *) = Convert : r408_6
|
||||||
|
# 408| r408_8(glval<int>) = CopyValue : r408_7
|
||||||
|
# 408| m408_9(int) = Store[?] : &:r408_8, r408_1
|
||||||
|
# 408| m408_10(unknown) = Chi : total:m401_4, partial:m408_9
|
||||||
|
# 410| r410_1(glval<bool>) = VariableAddress[b1] :
|
||||||
|
# 410| r410_2(bool) = Load[b1] : &:r410_1, m401_12
|
||||||
|
# 410| v410_3(void) = ConditionalBranch : r410_2
|
||||||
|
#-----| False -> Block 2
|
||||||
|
#-----| True -> Block 1
|
||||||
|
|
||||||
|
# 411| Block 1
|
||||||
|
# 411| r411_1(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 411| m411_2(int[]) = Uninitialized[b] : &:r411_1
|
||||||
|
# 411| r411_3(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 411| r411_4(int) = Load[n1] : &:r411_3, m401_6
|
||||||
|
# 411| v411_5(void) = NoOp :
|
||||||
|
#-----| Goto -> Block 3
|
||||||
|
|
||||||
|
# 413| Block 2
|
||||||
|
# 413| r413_1(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 413| m413_2(int[]) = Uninitialized[b] : &:r413_1
|
||||||
|
# 413| r413_3(glval<int>) = VariableAddress[n2] :
|
||||||
|
# 413| r413_4(int) = Load[n2] : &:r413_3, m401_8
|
||||||
|
# 413| v413_5(void) = NoOp :
|
||||||
|
#-----| Goto -> Block 3
|
||||||
|
|
||||||
|
# 415| Block 3
|
||||||
|
# 415| v415_1(void) = NoOp :
|
||||||
|
# 401| v401_13(void) = ReturnVoid :
|
||||||
|
# 401| v401_14(void) = AliasedUse : ~m408_10
|
||||||
|
# 401| v401_15(void) = ExitFunction :
|
||||||
|
|||||||
@@ -396,4 +396,20 @@ int FusedBlockPhiOperand(int x, int y, int z, bool b1) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
return ret;
|
return ret;
|
||||||
|
}
|
||||||
|
|
||||||
|
void vla(int n1, int n2, int n3, bool b1) {
|
||||||
|
int b[n1];
|
||||||
|
int c[n1][n2];
|
||||||
|
|
||||||
|
*b = 0;
|
||||||
|
b[0] = 1;
|
||||||
|
|
||||||
|
**(c + 1) = 0;
|
||||||
|
|
||||||
|
if(b1) {
|
||||||
|
int b[n1];
|
||||||
|
} else {
|
||||||
|
int b[n2];
|
||||||
|
}
|
||||||
}
|
}
|
||||||
@@ -1695,3 +1695,76 @@ ssa.cpp:
|
|||||||
# 383| v383_13(void) = ReturnValue : &:r383_12, m398_5
|
# 383| v383_13(void) = ReturnValue : &:r383_12, m398_5
|
||||||
# 383| v383_14(void) = AliasedUse : ~m?
|
# 383| v383_14(void) = AliasedUse : ~m?
|
||||||
# 383| v383_15(void) = ExitFunction :
|
# 383| v383_15(void) = ExitFunction :
|
||||||
|
|
||||||
|
# 401| void vla(int, int, int, bool)
|
||||||
|
# 401| Block 0
|
||||||
|
# 401| v401_1(void) = EnterFunction :
|
||||||
|
# 401| mu401_2(unknown) = AliasedDefinition :
|
||||||
|
# 401| mu401_3(unknown) = InitializeNonLocal :
|
||||||
|
# 401| r401_4(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 401| m401_5(int) = InitializeParameter[n1] : &:r401_4
|
||||||
|
# 401| r401_6(glval<int>) = VariableAddress[n2] :
|
||||||
|
# 401| m401_7(int) = InitializeParameter[n2] : &:r401_6
|
||||||
|
# 401| r401_8(glval<int>) = VariableAddress[n3] :
|
||||||
|
# 401| m401_9(int) = InitializeParameter[n3] : &:r401_8
|
||||||
|
# 401| r401_10(glval<bool>) = VariableAddress[b1] :
|
||||||
|
# 401| m401_11(bool) = InitializeParameter[b1] : &:r401_10
|
||||||
|
# 402| r402_1(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 402| mu402_2(int[]) = Uninitialized[b] : &:r402_1
|
||||||
|
# 402| r402_3(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 402| r402_4(int) = Load[n1] : &:r402_3, m401_5
|
||||||
|
# 402| v402_5(void) = NoOp :
|
||||||
|
# 403| r403_1(glval<int[][]>) = VariableAddress[c] :
|
||||||
|
# 403| mu403_2(int[][]) = Uninitialized[c] : &:r403_1
|
||||||
|
# 403| r403_3(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 403| r403_4(int) = Load[n1] : &:r403_3, m401_5
|
||||||
|
# 403| r403_5(glval<int>) = VariableAddress[n2] :
|
||||||
|
# 403| r403_6(int) = Load[n2] : &:r403_5, m401_7
|
||||||
|
# 403| v403_7(void) = NoOp :
|
||||||
|
# 405| r405_1(int) = Constant[0] :
|
||||||
|
# 405| r405_2(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 405| r405_3(int *) = Convert : r405_2
|
||||||
|
# 405| r405_4(glval<int>) = CopyValue : r405_3
|
||||||
|
# 405| mu405_5(int) = Store[?] : &:r405_4, r405_1
|
||||||
|
# 406| r406_1(int) = Constant[1] :
|
||||||
|
# 406| r406_2(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 406| r406_3(int *) = Convert : r406_2
|
||||||
|
# 406| r406_4(int) = Constant[0] :
|
||||||
|
# 406| r406_5(glval<int>) = PointerAdd[4] : r406_3, r406_4
|
||||||
|
# 406| mu406_6(int) = Store[?] : &:r406_5, r406_1
|
||||||
|
# 408| r408_1(int) = Constant[0] :
|
||||||
|
# 408| r408_2(glval<int[][]>) = VariableAddress[c] :
|
||||||
|
# 408| r408_3(int(*)[]) = Convert : r408_2
|
||||||
|
# 408| r408_4(int) = Constant[1] :
|
||||||
|
# 408| r408_5(int(*)[]) = PointerAdd : r408_3, r408_4
|
||||||
|
# 408| r408_6(glval<int[]>) = CopyValue : r408_5
|
||||||
|
# 408| r408_7(int *) = Convert : r408_6
|
||||||
|
# 408| r408_8(glval<int>) = CopyValue : r408_7
|
||||||
|
# 408| mu408_9(int) = Store[?] : &:r408_8, r408_1
|
||||||
|
# 410| r410_1(glval<bool>) = VariableAddress[b1] :
|
||||||
|
# 410| r410_2(bool) = Load[b1] : &:r410_1, m401_11
|
||||||
|
# 410| v410_3(void) = ConditionalBranch : r410_2
|
||||||
|
#-----| False -> Block 2
|
||||||
|
#-----| True -> Block 1
|
||||||
|
|
||||||
|
# 411| Block 1
|
||||||
|
# 411| r411_1(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 411| m411_2(int[]) = Uninitialized[b] : &:r411_1
|
||||||
|
# 411| r411_3(glval<int>) = VariableAddress[n1] :
|
||||||
|
# 411| r411_4(int) = Load[n1] : &:r411_3, m401_5
|
||||||
|
# 411| v411_5(void) = NoOp :
|
||||||
|
#-----| Goto -> Block 3
|
||||||
|
|
||||||
|
# 413| Block 2
|
||||||
|
# 413| r413_1(glval<int[]>) = VariableAddress[b] :
|
||||||
|
# 413| m413_2(int[]) = Uninitialized[b] : &:r413_1
|
||||||
|
# 413| r413_3(glval<int>) = VariableAddress[n2] :
|
||||||
|
# 413| r413_4(int) = Load[n2] : &:r413_3, m401_7
|
||||||
|
# 413| v413_5(void) = NoOp :
|
||||||
|
#-----| Goto -> Block 3
|
||||||
|
|
||||||
|
# 415| Block 3
|
||||||
|
# 415| v415_1(void) = NoOp :
|
||||||
|
# 401| v401_12(void) = ReturnVoid :
|
||||||
|
# 401| v401_13(void) = AliasedUse : ~m?
|
||||||
|
# 401| v401_14(void) = ExitFunction :
|
||||||
|
|||||||
Some files were not shown because too many files have changed in this diff Show More
Reference in New Issue
Block a user