mirror of
https://github.com/github/codeql.git
synced 2026-02-12 13:11:20 +01:00
2c5dd2dfa3
This PR separates the core cpp packs into `codeql/cpp-queries` and `codeql/cpp-all`. There are very few lines of code changed. Almost all changes are moving files around.
479 lines
16 KiB
Plaintext
479 lines
16 KiB
Plaintext
import cpp
|
|
|
|
/**
|
|
* Describes whether a relation is 'strict' (that is, a `<` or `>`
|
|
* relation) or 'non-strict' (a `<=` or `>=` relation).
|
|
*/
|
|
newtype RelationStrictness =
|
|
/**
|
|
* Represents that a relation is 'strict' (that is, a `<` or `>` relation).
|
|
*/
|
|
Strict() or
|
|
/**
|
|
* Represents that a relation is 'non-strict' (that is, a `<=` or `>=` relation)
|
|
*/
|
|
Nonstrict()
|
|
|
|
/**
|
|
* Describes whether a relation is 'greater' (that is, a `>` or `>=`
|
|
* relation) or 'lesser' (a `<` or `<=` relation).
|
|
*/
|
|
newtype RelationDirection =
|
|
/**
|
|
* Represents that a relation is 'greater' (that is, a `>` or `>=` relation).
|
|
*/
|
|
Greater() or
|
|
/**
|
|
* Represents that a relation is 'lesser' (that is, a `<` or `<=` relation).
|
|
*/
|
|
Lesser()
|
|
|
|
private RelationStrictness negateStrictness(RelationStrictness strict) {
|
|
strict = Strict() and result = Nonstrict()
|
|
or
|
|
strict = Nonstrict() and result = Strict()
|
|
}
|
|
|
|
private RelationDirection negateDirection(RelationDirection dir) {
|
|
dir = Greater() and result = Lesser()
|
|
or
|
|
dir = Lesser() and result = Greater()
|
|
}
|
|
|
|
/**
|
|
* Holds if `dir` is `Greater` (that is, a `>` or `>=` relation)
|
|
*/
|
|
boolean directionIsGreater(RelationDirection dir) {
|
|
dir = Greater() and result = true
|
|
or
|
|
dir = Lesser() and result = false
|
|
}
|
|
|
|
/**
|
|
* Holds if `dir` is `Lesser` (that is, a `<` or `<=` relation)
|
|
*/
|
|
boolean directionIsLesser(RelationDirection dir) {
|
|
dir = Greater() and result = false
|
|
or
|
|
dir = Lesser() and result = true
|
|
}
|
|
|
|
/**
|
|
* Holds if `rel` is a relational operation (`<`, `>`, `<=` or `>=`)
|
|
* with fully-converted children `lhs` and `rhs`, described by
|
|
* `dir` and `strict`.
|
|
*
|
|
* For example, if `rel` is `x < 5` then
|
|
* `relOp(rel, x, 5, Lesser(), Strict())` holds.
|
|
*/
|
|
private predicate relOp(
|
|
RelationalOperation rel, Expr lhs, Expr rhs, RelationDirection dir, RelationStrictness strict
|
|
) {
|
|
lhs = rel.getLeftOperand().getFullyConverted() and
|
|
rhs = rel.getRightOperand().getFullyConverted() and
|
|
(
|
|
rel instanceof LTExpr and dir = Lesser() and strict = Strict()
|
|
or
|
|
rel instanceof LEExpr and dir = Lesser() and strict = Nonstrict()
|
|
or
|
|
rel instanceof GTExpr and dir = Greater() and strict = Strict()
|
|
or
|
|
rel instanceof GEExpr and dir = Greater() and strict = Nonstrict()
|
|
)
|
|
}
|
|
|
|
/**
|
|
* Holds if `rel` is a relational operation (`<`, `>`, `<=` or `>=`)
|
|
* with fully-converted children `a` and `b`, described by `dir` and `strict`.
|
|
*
|
|
* This allows for the relation to be either as written, or with its
|
|
* arguments reversed; for example, if `rel` is `x < 5` then both
|
|
* `relOpWithSwap(rel, x, 5, Lesser(), Strict())` and
|
|
* `relOpWithSwap(rel, 5, x, Greater(), Strict())` hold.
|
|
*/
|
|
predicate relOpWithSwap(
|
|
RelationalOperation rel, Expr a, Expr b, RelationDirection dir, RelationStrictness strict
|
|
) {
|
|
relOp(rel, a, b, dir, strict) or
|
|
relOp(rel, b, a, negateDirection(dir), strict)
|
|
}
|
|
|
|
/**
|
|
* Holds if `rel` is a comparison operation (`<`, `>`, `<=` or `>=`)
|
|
* with fully-converted children `a` and `b`, described by `dir` and `strict`, with
|
|
* result `branch`.
|
|
*
|
|
* This allows for the relation to be either as written, or with its
|
|
* arguments reversed; for example, if `rel` is `x < 5` then
|
|
* `relOpWithSwapAndNegate(rel, x, 5, Lesser(), Strict(), true)`,
|
|
* `relOpWithSwapAndNegate(rel, 5, x, Greater(), Strict(), true)`,
|
|
* `relOpWithSwapAndNegate(rel, x, 5, Greater(), Nonstrict(), false)` and
|
|
* `relOpWithSwapAndNegate(rel, 5, x, Lesser(), Nonstrict(), false)` hold.
|
|
*/
|
|
predicate relOpWithSwapAndNegate(
|
|
RelationalOperation rel, Expr a, Expr b, RelationDirection dir, RelationStrictness strict,
|
|
boolean branch
|
|
) {
|
|
relOpWithSwap(rel, a, b, dir, strict) and branch = true
|
|
or
|
|
relOpWithSwap(rel, a, b, negateDirection(dir), negateStrictness(strict)) and
|
|
branch = false
|
|
}
|
|
|
|
/**
|
|
* Holds if `cmp` is an equality operation (`==` or `!=`) with fully-converted
|
|
* children `lhs` and `rhs`, and `isEQ` is true if `cmp` is an
|
|
* `==` operation and false if it is an `!=` operation.
|
|
*
|
|
* For example, if `rel` is `x == 5` then
|
|
* `eqOpWithSwap(cmp, x, 5, true)` holds.
|
|
*/
|
|
private predicate eqOp(EqualityOperation cmp, Expr lhs, Expr rhs, boolean isEQ) {
|
|
lhs = cmp.getLeftOperand().getFullyConverted() and
|
|
rhs = cmp.getRightOperand().getFullyConverted() and
|
|
(
|
|
cmp instanceof EQExpr and isEQ = true
|
|
or
|
|
cmp instanceof NEExpr and isEQ = false
|
|
)
|
|
}
|
|
|
|
/**
|
|
* Holds if `cmp` is an equality operation (`==` or `!=`) with fully-converted
|
|
* operands `a` and `b`, and `isEQ` is true if `cmp` is an `==` operation and
|
|
* false if it is an `!=` operation.
|
|
*
|
|
* This allows for the equality to be either as written, or with its
|
|
* arguments reversed; for example, if `cmp` is `x == 5` then both
|
|
* `eqOpWithSwap(cmp, x, 5, true)` and
|
|
* `eqOpWithSwap(cmp, 5, x, true)` hold.
|
|
*/
|
|
private predicate eqOpWithSwap(EqualityOperation cmp, Expr a, Expr b, boolean isEQ) {
|
|
eqOp(cmp, a, b, isEQ) or
|
|
eqOp(cmp, b, a, isEQ)
|
|
}
|
|
|
|
/**
|
|
* Holds if `cmp` is an equality operation (`==` or `!=`) with fully-converted
|
|
* children `a` and `b`, `isEQ` is true if `cmp` is an `==` operation and
|
|
* false if it is an `!=` operation, and the result is `branch`.
|
|
*
|
|
* This allows for the comparison to be either as written, or with its
|
|
* arguments reversed; for example, if `cmp` is `x == 5` then
|
|
* `eqOpWithSwapAndNegate(cmp, x, 5, true, true)`,
|
|
* `eqOpWithSwapAndNegate(cmp, 5, x, true, true)`,
|
|
* `eqOpWithSwapAndNegate(cmp, x, 5, false, false)` and
|
|
* `eqOpWithSwapAndNegate(cmp, 5, x, false, false)` hold.
|
|
*/
|
|
predicate eqOpWithSwapAndNegate(EqualityOperation cmp, Expr a, Expr b, boolean isEQ, boolean branch) {
|
|
eqOpWithSwap(cmp, a, b, branch) and isEQ = true
|
|
or
|
|
eqOpWithSwap(cmp, a, b, branch.booleanNot()) and isEQ = false
|
|
}
|
|
|
|
/**
|
|
* Holds if `cmp` is an unconverted conversion of `a` to a Boolean that
|
|
* evalutes to `isEQ` iff `a` is 0.
|
|
*
|
|
* Note that `a` can be `cmp` itself or a conversion thereof.
|
|
*/
|
|
private predicate eqZero(Expr cmp, Expr a, boolean isEQ) {
|
|
// The `!a` expression tests `a` equal to zero when `a` is a number converted
|
|
// to a Boolean.
|
|
isEQ = true and
|
|
exists(Expr notOperand | notOperand = cmp.(NotExpr).getOperand().getFullyConverted() |
|
|
// In C++ code there will be a BoolConversion in `!myInt`
|
|
a = notOperand.(BoolConversion).getExpr()
|
|
or
|
|
// In C code there is no conversion since there was no bool type before C99
|
|
a = notOperand and
|
|
not a instanceof BoolConversion // avoid overlap with the case above
|
|
)
|
|
or
|
|
// The `(bool)a` expression tests `a` NOT equal to zero when `a` is a number
|
|
// converted to a Boolean. To avoid overlap with the case above, this case
|
|
// excludes conversions that are right below a `!`.
|
|
isEQ = false and
|
|
linearAccess(cmp, _, _, _) and
|
|
// This test for `isCondition` implies that `cmp` is unconverted and that the
|
|
// parent of `cfg` is not a `NotExpr` -- the CFG doesn't do branching from
|
|
// inside `NotExpr`.
|
|
cmp.isCondition() and
|
|
// The GNU two-operand conditional expression is not supported for the
|
|
// purpose of guards, but the value of the conditional expression itself is
|
|
// modeled in the range analysis.
|
|
not exists(ConditionalExpr cond | cmp = cond.getCondition() and cond.isTwoOperand()) and
|
|
(
|
|
// In C++ code there will be a BoolConversion in `if (myInt)`
|
|
a = cmp.getFullyConverted().(BoolConversion).getExpr()
|
|
or
|
|
// In C code there is no conversion since there was no bool type before C99
|
|
a = cmp.getFullyConverted() and
|
|
not a instanceof BoolConversion // avoid overlap with the case above
|
|
)
|
|
}
|
|
|
|
/**
|
|
* Holds if `branch` of `cmp` is taken when `a` compares `isEQ` to zero.
|
|
*
|
|
* Note that `a` can be `cmp` itself or a conversion thereof.
|
|
*/
|
|
predicate eqZeroWithNegate(Expr cmp, Expr a, boolean isEQ, boolean branch) {
|
|
// The comparison for _equality_ to zero is on the `true` branch when `cmp`
|
|
// compares equal to zero and on the `false` branch when `cmp` compares not
|
|
// equal to zero.
|
|
eqZero(cmp, a, branch) and isEQ = true
|
|
or
|
|
// The comparison for _inequality_ to zero is on the `false` branch when
|
|
// `cmp` compares equal to zero and on the `true` branch when `cmp` compares
|
|
// not equal to zero.
|
|
eqZero(cmp, a, branch.booleanNot()) and isEQ = false
|
|
}
|
|
|
|
/**
|
|
* Holds if `expr` is equivalent to `p*v + q`, where `p` is a non-zero
|
|
* number. This takes into account the associativity, commutativity and
|
|
* distributivity of arithmetic operations.
|
|
*/
|
|
predicate linearAccess(Expr expr, VariableAccess v, float p, float q) {
|
|
// Exclude 0 and NaN.
|
|
(p < 0 or p > 0) and
|
|
linearAccessImpl(expr, v, p, q)
|
|
}
|
|
|
|
/**
|
|
* Holds if `expr` is equivalent to `p*v + q`.
|
|
* This takes into account the associativity, commutativity and
|
|
* distributivity of arithmetic operations.
|
|
*/
|
|
private predicate linearAccessImpl(Expr expr, VariableAccess v, float p, float q) {
|
|
// Base case
|
|
expr = v and p = 1.0 and q = 0.0
|
|
or
|
|
expr.(ReferenceDereferenceExpr).getExpr() = v and p = 1.0 and q = 0.0
|
|
or
|
|
// a+(p*v+b) == p*v + (a+b)
|
|
exists(AddExpr addExpr, float a, float b |
|
|
addExpr.getLeftOperand().isConstant() and
|
|
a = addExpr.getLeftOperand().getFullyConverted().getValue().toFloat() and
|
|
linearAccess(addExpr.getRightOperand(), v, p, b) and
|
|
expr = addExpr and
|
|
q = a + b
|
|
)
|
|
or
|
|
// (p*v+a)+b == p*v + (a+b)
|
|
exists(AddExpr addExpr, float a, float b |
|
|
addExpr.getRightOperand().isConstant() and
|
|
b = addExpr.getRightOperand().getFullyConverted().getValue().toFloat() and
|
|
linearAccess(addExpr.getLeftOperand(), v, p, a) and
|
|
expr = addExpr and
|
|
q = a + b
|
|
)
|
|
or
|
|
// a-(m*v+b) == -m*v + (a-b)
|
|
exists(SubExpr subExpr, float a, float b, float m |
|
|
subExpr.getLeftOperand().isConstant() and
|
|
a = subExpr.getLeftOperand().getFullyConverted().getValue().toFloat() and
|
|
linearAccess(subExpr.getRightOperand(), v, m, b) and
|
|
expr = subExpr and
|
|
p = -m and
|
|
q = a - b
|
|
)
|
|
or
|
|
// (p*v+a)-b == p*v + (a-b)
|
|
exists(SubExpr subExpr, float a, float b |
|
|
subExpr.getRightOperand().isConstant() and
|
|
b = subExpr.getRightOperand().getFullyConverted().getValue().toFloat() and
|
|
linearAccess(subExpr.getLeftOperand(), v, p, a) and
|
|
expr = subExpr and
|
|
q = a - b
|
|
)
|
|
or
|
|
// +(p*v+q) == p*v + q
|
|
exists(UnaryPlusExpr unaryPlusExpr |
|
|
linearAccess(unaryPlusExpr.getOperand().getFullyConverted(), v, p, q) and
|
|
expr = unaryPlusExpr
|
|
)
|
|
or
|
|
// (larger_type)(p*v+q) == p*v + q
|
|
exists(Cast cast, ArithmeticType sourceType, ArithmeticType targetType |
|
|
linearAccess(cast.getExpr(), v, p, q) and
|
|
sourceType = cast.getExpr().getUnspecifiedType() and
|
|
targetType = cast.getUnspecifiedType() and
|
|
// This allows conversion between signed and unsigned, which is technically
|
|
// lossy but common enough that we'll just have to assume the user knows
|
|
// what they're doing.
|
|
targetType.getSize() >= sourceType.getSize() and
|
|
expr = cast
|
|
)
|
|
or
|
|
// (p*v+q) == p*v + q
|
|
exists(ParenthesisExpr paren |
|
|
linearAccess(paren.getExpr(), v, p, q) and
|
|
expr = paren
|
|
)
|
|
or
|
|
// -(a*v+b) == -a*v + (-b)
|
|
exists(UnaryMinusExpr unaryMinusExpr, float a, float b |
|
|
linearAccess(unaryMinusExpr.getOperand().getFullyConverted(), v, a, b) and
|
|
expr = unaryMinusExpr and
|
|
p = -a and
|
|
q = -b
|
|
)
|
|
or
|
|
// m*(a*v+b) == (m*a)*v + (m*b)
|
|
exists(MulExpr mulExpr, float a, float b, float m |
|
|
mulExpr.getLeftOperand().isConstant() and
|
|
m = mulExpr.getLeftOperand().getFullyConverted().getValue().toFloat() and
|
|
linearAccess(mulExpr.getRightOperand(), v, a, b) and
|
|
expr = mulExpr and
|
|
p = m * a and
|
|
q = m * b
|
|
)
|
|
or
|
|
// (a*v+b)*m == (m*a)*v + (m*b)
|
|
exists(MulExpr mulExpr, float a, float b, float m |
|
|
mulExpr.getRightOperand().isConstant() and
|
|
m = mulExpr.getRightOperand().getFullyConverted().getValue().toFloat() and
|
|
linearAccess(mulExpr.getLeftOperand(), v, a, b) and
|
|
expr = mulExpr and
|
|
p = m * a and
|
|
q = m * b
|
|
)
|
|
}
|
|
|
|
/**
|
|
* Holds if `guard` is a comparison operation (`<`, `<=`, `>`, `>=`,
|
|
* `==` or `!=`), one of its arguments is equivalent (up to
|
|
* associativity, commutativity and distributivity or the simple
|
|
* arithmetic operations) to `p*v + q` (for some `p` and `q`),
|
|
* `direction` describes whether `guard` give an upper or lower bound
|
|
* on `v`, and `branch` indicates which control-flow branch this
|
|
* bound is valid on.
|
|
*
|
|
* For example, if `guard` is `2*v + 3 > 10` then
|
|
* `cmpWithLinearBound(guard, v, Greater(), true)` and
|
|
* `cmpWithLinearBound(guard, v, Lesser(), false)` hold.
|
|
* If `guard` is `4 - v > 5` then
|
|
* `cmpWithLinearBound(guard, v, Lesser(), false)` and
|
|
* `cmpWithLinearBound(guard, v, Greater(), true)` hold.
|
|
*
|
|
* A more sophisticated predicate, such as `boundFromGuard`, is needed
|
|
* to compute an actual bound for `v`. This predicate can be used if
|
|
* you just want to check whether a variable is bounded, or to restrict
|
|
* a more expensive analysis to just guards that bound a variable.
|
|
*/
|
|
predicate cmpWithLinearBound(
|
|
ComparisonOperation guard, VariableAccess v,
|
|
RelationDirection direction, // Is this a lower or an upper bound?
|
|
boolean branch // Which control-flow branch is this bound valid on?
|
|
) {
|
|
exists(Expr lhs, float p, RelationDirection dir |
|
|
linearAccess(lhs, v, p, _) and
|
|
relOpWithSwapAndNegate(guard, lhs, _, dir, _, branch) and
|
|
(
|
|
p > 0 and direction = dir
|
|
or
|
|
p < 0 and direction = negateDirection(dir)
|
|
)
|
|
)
|
|
or
|
|
exists(Expr lhs |
|
|
linearAccess(lhs, v, _, _) and
|
|
eqOpWithSwap(guard, lhs, _, branch)
|
|
)
|
|
}
|
|
|
|
/**
|
|
* Holds if `lb` and `ub` are the lower and upper bounds of the unspecified
|
|
* type `t`.
|
|
*
|
|
* For example, if `t` is a signed 32-bit type then holds if `lb` is
|
|
* `-2^31` and `ub` is `2^31 - 1`.
|
|
*/
|
|
private predicate typeBounds(ArithmeticType t, float lb, float ub) {
|
|
exists(IntegralType integralType, float limit |
|
|
integralType = t and limit = 2.pow(8 * integralType.getSize())
|
|
|
|
|
if integralType instanceof BoolType
|
|
then lb = 0 and ub = 1
|
|
else
|
|
if integralType.isSigned()
|
|
then (
|
|
lb = -(limit / 2) and ub = (limit / 2) - 1
|
|
) else (
|
|
lb = 0 and ub = limit - 1
|
|
)
|
|
)
|
|
or
|
|
// This covers all floating point types. The range is (-Inf, +Inf).
|
|
t instanceof FloatingPointType and lb = -(1.0 / 0.0) and ub = 1.0 / 0.0
|
|
}
|
|
|
|
private Type stripReference(Type t) {
|
|
if t instanceof ReferenceType then result = t.(ReferenceType).getBaseType() else result = t
|
|
}
|
|
|
|
/** Gets the type used by range analysis for the given `StackVariable`. */
|
|
Type getVariableRangeType(StackVariable v) { result = stripReference(v.getUnspecifiedType()) }
|
|
|
|
/**
|
|
* Gets the lower bound for the unspecified type `t`.
|
|
*
|
|
* For example, if `t` is a signed 32-bit type then the result is
|
|
* `-2^31`.
|
|
*/
|
|
float typeLowerBound(Type t) { typeBounds(stripReference(t), result, _) }
|
|
|
|
/**
|
|
* Gets the upper bound for the unspecified type `t`.
|
|
*
|
|
* For example, if `t` is a signed 32-bit type then the result is
|
|
* `2^31 - 1`.
|
|
*/
|
|
float typeUpperBound(Type t) { typeBounds(stripReference(t), _, result) }
|
|
|
|
/**
|
|
* Gets the minimum value that this expression could represent, based on
|
|
* its type.
|
|
*
|
|
* For example, if `expr` has a signed 32-bit type then the result is
|
|
* `-2^31`.
|
|
*
|
|
* Note: Due to the way casts are represented, rather than calling
|
|
* `exprMinVal(expr)` you will normally want to call
|
|
* `exprMinVal(expr.getFullyConverted())`.
|
|
*/
|
|
float exprMinVal(Expr expr) { result = typeLowerBound(expr.getUnspecifiedType()) }
|
|
|
|
/**
|
|
* Gets the maximum value that this expression could represent, based on
|
|
* its type.
|
|
*
|
|
* For example, if `expr` has a signed 32-bit type then the result is
|
|
* `2^31 - 1`.
|
|
*
|
|
* Note: Due to the way casts are represented, rather than calling
|
|
* `exprMaxVal(expr)` you will normally want to call
|
|
* `exprMaxVal(expr.getFullyConverted())`.
|
|
*/
|
|
float exprMaxVal(Expr expr) { result = typeUpperBound(expr.getUnspecifiedType()) }
|
|
|
|
/**
|
|
* Gets the minimum value that this variable could represent, based on
|
|
* its type.
|
|
*
|
|
* For example, if `v` has a signed 32-bit type then the result is
|
|
* `-2^31`.
|
|
*/
|
|
float varMinVal(Variable v) { result = typeLowerBound(v.getUnspecifiedType()) }
|
|
|
|
/**
|
|
* Gets the maximum value that this variable could represent, based on
|
|
* its type.
|
|
*
|
|
* For example, if `v` has a signed 32-bit type then the result is
|
|
* `2^31 - 1`.
|
|
*/
|
|
float varMaxVal(Variable v) { result = typeUpperBound(v.getUnspecifiedType()) }
|