hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-25 08:45:14 +02:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'main' into no-dtt-in-unbounded-write

Browse Source
This commit is contained in:
Mathias Vorreiter Pedersen
2023-11-10 12:57:42 +00:00
parent 7048190929 340b20f93d
commit 4f6b6b4a6f
1406 changed files with 52150 additions and 28757 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
cpp/ql/lib/change-notes/2023-11-08-strsafe-models.md Normal file
View File

@@ -0,0 +1,4 @@
---
category: minorAnalysis
---
* Added models for the `sprintf` variants from the `StrSafe.h` header.

23
cpp/ql/lib/semmle/code/cpp/models/implementations/Printf.qll
View File

@@ -147,19 +147,32 @@ private class SnprintfImpl extends Snprintf {
/**
* The Microsoft `StringCchPrintf` function and variants.
* See: https://learn.microsoft.com/en-us/windows/win32/api/strsafe/
* and
* https://learn.microsoft.com/en-us/previous-versions/windows/embedded/ms860435(v=msdn.10)
*/
private class StringCchPrintf extends FormattingFunction {
StringCchPrintf() {
this instanceof TopLevelFunction and
this.hasGlobalName([
"StringCchPrintf", "StringCchPrintfEx", "StringCchPrintf_l", "StringCchPrintf_lEx",
"StringCbPrintf", "StringCbPrintfEx", "StringCbPrintf_l", "StringCbPrintf_lEx"
]) and
exists(string baseName |
baseName in [
"StringCchPrintf", //StringCchPrintf(pszDest, cchDest, pszFormat, ...)
"StringCchPrintfEx", //StringCchPrintfEx(pszDest,cchDest, ppszDestEnd, pcchRemaining, dwFlags, pszFormat, ...)
"StringCchPrintf_l", //StringCchPrintf_l(pszDest, cbDest, pszFormat, locale, ...)
"StringCchPrintf_lEx", //StringCchPrintf_lEx(pszDest, cchDest, ppszDestEnd, pcchRemaining, dwFlags, pszFormat, locale, ...)
"StringCbPrintf", //StringCbPrintf(pszDest, cbDest, pszFormat, ...)
"StringCbPrintfEx", //StringCbPrintfEx(pszDest, cbDest, ppszDestEnd, pcbRemaining, dwFlags, pszFormat, ...)
"StringCbPrintf_l", //StringCbPrintf_l(pszDest, cbDest, pszFormat, locale, ...)
"StringCbPrintf_lEx" //StringCbPrintf_lEx(pszDest, cbDest, ppszDestEnd, pcbRemaining, dwFlags, pszFormat, locale, ...)
]
|
this.hasGlobalName(baseName + ["", "A", "W"])
) and
not exists(this.getDefinition().getFile().getRelativePath())
}
override int getFormatParameterIndex() {
if this.getName().matches("%Ex") then result = 5 else result = 2
if this.getName().matches("%Ex" + ["", "A", "W"]) then result = 5 else result = 2
}
override int getOutputParameterIndex(boolean isStream) { result = 0 and isStream = false }

82
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll
View File

@@ -130,7 +130,7 @@ module SemanticExprConfig {
newtype TSsaVariable =
TSsaInstruction(IR::Instruction instr) { instr.hasMemoryResult() } or
TSsaOperand(IR::Operand op) { op.isDefinitionInexact() }
TSsaOperand(IR::PhiInputOperand op) { op.isDefinitionInexact() }
class SsaVariable extends TSsaVariable {
string toString() { none() }
@@ -139,7 +139,7 @@ module SemanticExprConfig {
IR::Instruction asInstruction() { none() }
IR::Operand asOperand() { none() }
IR::PhiInputOperand asOperand() { none() }
}
class SsaInstructionVariable extends SsaVariable, TSsaInstruction {
@@ -155,7 +155,7 @@ module SemanticExprConfig {
}
class SsaOperand extends SsaVariable, TSsaOperand {
IR::Operand op;
IR::PhiInputOperand op;
SsaOperand() { this = TSsaOperand(op) }
@@ -163,7 +163,7 @@ module SemanticExprConfig {
final override Location getLocation() { result = op.getLocation() }
final override IR::Operand asOperand() { result = op }
final override IR::PhiInputOperand asOperand() { result = op }
}
predicate explicitUpdate(SsaVariable v, Expr sourceExpr) {
@@ -190,83 +190,25 @@ module SemanticExprConfig {
SemType getSsaVariableType(SsaVariable v) {
result = getSemanticType(v.asInstruction().getResultIRType())
or
result = getSemanticType(v.asOperand().getUse().getResultIRType())
}
BasicBlock getSsaVariableBasicBlock(SsaVariable v) {
result = v.asInstruction().getBlock()
or
result = v.asOperand().getUse().getBlock()
result = v.asOperand().getAnyDef().getBlock()
}
private newtype TReadPosition =
TReadPositionBlock(IR::IRBlock block) or
TReadPositionPhiInputEdge(IR::IRBlock pred, IR::IRBlock succ) {
exists(IR::PhiInputOperand input |
pred = input.getPredecessorBlock() and
succ = input.getUse().getBlock()
)
}
class SsaReadPosition extends TReadPosition {
string toString() { none() }
Location getLocation() { none() }
predicate hasRead(SsaVariable v) { none() }
}
private class SsaReadPositionBlock extends SsaReadPosition, TReadPositionBlock {
IR::IRBlock block;
SsaReadPositionBlock() { this = TReadPositionBlock(block) }
final override string toString() { result = block.toString() }
final override Location getLocation() { result = block.getLocation() }
final override predicate hasRead(SsaVariable v) {
exists(IR::Operand operand | operand.getDef() = v.asInstruction() |
not operand instanceof IR::PhiInputOperand and
operand.getUse().getBlock() = block
)
}
}
private class SsaReadPositionPhiInputEdge extends SsaReadPosition, TReadPositionPhiInputEdge {
IR::IRBlock pred;
IR::IRBlock succ;
SsaReadPositionPhiInputEdge() { this = TReadPositionPhiInputEdge(pred, succ) }
final override string toString() { result = pred.toString() + "->" + succ.toString() }
final override Location getLocation() { result = succ.getLocation() }
final override predicate hasRead(SsaVariable v) {
exists(IR::PhiInputOperand operand | operand.getDef() = v.asInstruction() |
operand.getPredecessorBlock() = pred and
operand.getUse().getBlock() = succ
)
}
}
predicate hasReadOfSsaVariable(SsaReadPosition pos, SsaVariable v) { pos.hasRead(v) }
predicate readBlock(SsaReadPosition pos, BasicBlock block) { pos = TReadPositionBlock(block) }
predicate phiInputEdge(SsaReadPosition pos, BasicBlock origBlock, BasicBlock phiBlock) {
pos = TReadPositionPhiInputEdge(origBlock, phiBlock)
}
predicate phiInput(SsaReadPosition pos, SsaVariable phi, SsaVariable input) {
/** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
predicate phiInputFromBlock(SsaVariable phi, SsaVariable inp, BasicBlock bb) {
exists(IR::PhiInputOperand operand |
pos = TReadPositionPhiInputEdge(operand.getPredecessorBlock(), operand.getUse().getBlock())
|
bb = operand.getPredecessorBlock() and
phi.asInstruction() = operand.getUse() and
(
input.asInstruction() = operand.getDef()
inp.asInstruction() = operand.getDef()
or
input.asOperand() = operand
inp.asOperand() = operand
)
)
}

35
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll
View File

@@ -31,35 +31,8 @@ class SemSsaPhiNode extends SemSsaVariable {
SemSsaPhiNode() { Specific::phi(this) }
final SemSsaVariable getAPhiInput() { result = Specific::getAPhiInput(this) }
}
class SemSsaReadPosition instanceof Specific::SsaReadPosition {
final string toString() { result = super.toString() }
final Specific::Location getLocation() { result = super.getLocation() }
final predicate hasReadOfVar(SemSsaVariable var) { Specific::hasReadOfSsaVariable(this, var) }
}
class SemSsaReadPositionPhiInputEdge extends SemSsaReadPosition {
SemBasicBlock origBlock;
SemBasicBlock phiBlock;
SemSsaReadPositionPhiInputEdge() { Specific::phiInputEdge(this, origBlock, phiBlock) }
predicate phiInput(SemSsaPhiNode phi, SemSsaVariable inp) { Specific::phiInput(this, phi, inp) }
SemBasicBlock getOrigBlock() { result = origBlock }
SemBasicBlock getPhiBlock() { result = phiBlock }
}
class SemSsaReadPositionBlock extends SemSsaReadPosition {
SemBasicBlock block;
SemSsaReadPositionBlock() { Specific::readBlock(this, block) }
SemBasicBlock getBlock() { result = block }
SemExpr getAnExpr() { result = this.getBlock().getAnExpr() }
final predicate hasInputFromBlock(SemSsaVariable inp, SemBasicBlock bb) {
Specific::phiInputFromBlock(this, inp, bb)
}
}

8
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
View File

@@ -74,6 +74,8 @@ module Sem implements Semantic {
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
int getBlockId1(BasicBlock bb) { result = bb.getUniqueId() }
class Guard = SemGuard;
predicate implies_v2 = semImplies_v2/4;
@@ -92,12 +94,6 @@ module Sem implements Semantic {
class SsaExplicitUpdate = SemSsaExplicitUpdate;
class SsaReadPosition = SemSsaReadPosition;
class SsaReadPositionPhiInputEdge = SemSsaReadPositionPhiInputEdge;
class SsaReadPositionBlock = SemSsaReadPositionBlock;
predicate conversionCannotOverflow(Type fromType, Type toType) {
SemanticType::conversionCannotOverflow(fromType, toType)
}

29
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll
View File

@@ -133,33 +133,4 @@ module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
or
not exists(Lang::getAlternateTypeForSsaVariable(var)) and result = var.getType()
}
import Ranking
}
import Ranking
module Ranking {
/**
* Holds if `rix` is the number of input edges to `phi`.
*/
predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
rix = max(int r | rankedPhiInput(phi, _, _, r))
}
/**
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
* in an arbitrary 1-based numbering of the input edges to `phi`.
*/
predicate rankedPhiInput(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
) {
edge.phiInput(phi, inp) and
edge =
rank[r](SemSsaReadPositionPhiInputEdge e |
e.phiInput(phi, _)
|
e order by e.getOrigBlock().getUniqueId()
)
}
}

34
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
View File

@@ -45,7 +45,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
/** An SSA Phi definition, whose sign is the union of the signs of its inputs. */
private class PhiSignDef extends FlowSignDef instanceof SemSsaPhiNode {
final override Sign getSign() {
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
exists(SemSsaVariable inp, SsaReadPositionPhiInputEdge edge |
edge.phiInput(this, inp) and
result = semSsaSign(inp, edge)
)
@@ -170,11 +170,11 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
override Sign getSignRestriction() {
// Propagate via SSA
// Propagate the sign from the def of `v`, incorporating any inference from guards.
result = semSsaSign(v, any(SemSsaReadPositionBlock bb | bb.getAnExpr() = this))
result = semSsaSign(v, any(SsaReadPositionBlock bb | bb.getBlock().getAnExpr() = this))
or
// No block for this read. Just use the sign of the def.
// REVIEW: How can this happen?
not exists(SemSsaReadPositionBlock bb | bb.getAnExpr() = this) and
not exists(SsaReadPositionBlock bb | bb.getBlock().getAnExpr() = this) and
result = semSsaDefSign(v)
}
}
@@ -290,7 +290,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
* to only include bounds for which we might determine a sign.
*/
private predicate lowerBound(
SemExpr lowerbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
SemExpr lowerbound, SemSsaVariable v, SsaReadPosition pos, boolean isStrict
) {
exists(boolean testIsTrue, SemRelationalExpr comp |
pos.hasReadOfVar(v) and
@@ -314,7 +314,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
* to only include bounds for which we might determine a sign.
*/
private predicate upperBound(
SemExpr upperbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
SemExpr upperbound, SemSsaVariable v, SsaReadPosition pos, boolean isStrict
) {
exists(boolean testIsTrue, SemRelationalExpr comp |
pos.hasReadOfVar(v) and
@@ -340,7 +340,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
* - `isEq = true` : `v = eqbound`
* - `isEq = false` : `v != eqbound`
*/
private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SsaReadPosition pos, boolean isEq) {
exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
pos.hasReadOfVar(pragma[only_bind_into](v)) and
guardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
@@ -355,7 +355,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
* Holds if `bound` is a bound for `v` at `pos` that needs to be positive in
* order for `v` to be positive.
*/
private predicate posBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
private predicate posBound(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
upperBound(bound, v, pos, _) or
eqBound(bound, v, pos, true)
}
@@ -364,7 +364,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
* Holds if `bound` is a bound for `v` at `pos` that needs to be negative in
* order for `v` to be negative.
*/
private predicate negBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
private predicate negBound(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
lowerBound(bound, v, pos, _) or
eqBound(bound, v, pos, true)
}
@@ -373,24 +373,24 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
* Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v`
* can be zero.
*/
private predicate zeroBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
private predicate zeroBound(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
lowerBound(bound, v, pos, _) or
upperBound(bound, v, pos, _) or
eqBound(bound, v, pos, _)
}
/** Holds if `bound` allows `v` to be positive at `pos`. */
private predicate posBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
private predicate posBoundOk(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
posBound(bound, v, pos) and TPos() = semExprSign(bound)
}
/** Holds if `bound` allows `v` to be negative at `pos`. */
private predicate negBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
private predicate negBoundOk(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
negBound(bound, v, pos) and TNeg() = semExprSign(bound)
}
/** Holds if `bound` allows `v` to be zero at `pos`. */
private predicate zeroBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
private predicate zeroBoundOk(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
lowerBound(bound, v, pos, _) and TNeg() = semExprSign(bound)
or
lowerBound(bound, v, pos, false) and TZero() = semExprSign(bound)
@@ -408,7 +408,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
* Holds if there is a bound that might restrict whether `v` has the sign `s`
* at `pos`.
*/
private predicate hasGuard(SemSsaVariable v, SemSsaReadPosition pos, Sign s) {
private predicate hasGuard(SemSsaVariable v, SsaReadPosition pos, Sign s) {
s = TPos() and posBound(_, v, pos)
or
s = TNeg() and negBound(_, v, pos)
@@ -421,7 +421,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
* might be ruled out by a guard.
*/
pragma[noinline]
private Sign guardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
private Sign guardedSsaSign(SemSsaVariable v, SsaReadPosition pos) {
result = semSsaDefSign(v) and
pos.hasReadOfVar(v) and
hasGuard(v, pos, result)
@@ -432,7 +432,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
* can rule it out.
*/
pragma[noinline]
private Sign unguardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
private Sign unguardedSsaSign(SemSsaVariable v, SsaReadPosition pos) {
result = semSsaDefSign(v) and
pos.hasReadOfVar(v) and
not hasGuard(v, pos, result)
@@ -443,7 +443,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
* ruled out the sign but does not.
* This does not check that the definition of `v` also allows the sign.
*/
private Sign guardedSsaSignOk(SemSsaVariable v, SemSsaReadPosition pos) {
private Sign guardedSsaSignOk(SemSsaVariable v, SsaReadPosition pos) {
result = TPos() and
forex(SemExpr bound | posBound(bound, v, pos) | posBoundOk(bound, v, pos))
or
@@ -455,7 +455,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
}
/** Gets a possible sign for `v` at `pos`. */
private Sign semSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
private Sign semSsaSign(SemSsaVariable v, SsaReadPosition pos) {
result = unguardedSsaSign(v, pos)
or
result = guardedSsaSign(v, pos) and