mirror of
https://github.com/github/codeql.git
synced 2025-12-16 16:53:25 +01:00
Merge rc/3.12 into main
This commit is contained in:
Aditya Sharad
@@ -289,6 +289,10 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
|
||||
predicate ignoreExprBound(Sem::Expr e);
|
||||
|
||||
default predicate javaCompatibility() { none() }
|
||||
|
||||
default predicate includeConstantBounds() { any() }
|
||||
|
||||
default predicate includeRelativeBounds() { any() }
|
||||
}
|
||||
|
||||
signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> {
|
||||
@@ -678,60 +682,65 @@ module RangeStage<
|
||||
* - `upper = false` : `e2 >= e1 + delta`
|
||||
*/
|
||||
private predicate boundFlowStep(Sem::Expr e2, Sem::Expr e1, D::Delta delta, boolean upper) {
|
||||
valueFlowStep(e2, e1, delta) and
|
||||
(upper = true or upper = false)
|
||||
or
|
||||
e2.(SafeCastExpr).getOperand() = e1 and
|
||||
delta = D::fromInt(0) and
|
||||
(upper = true or upper = false)
|
||||
or
|
||||
javaCompatibility() and
|
||||
exists(Sem::Expr x, Sem::SubExpr sub |
|
||||
e2 = sub and
|
||||
sub.getLeftOperand() = e1 and
|
||||
sub.getRightOperand() = x
|
||||
|
|
||||
// `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
|
||||
not x instanceof Sem::ConstantIntegerExpr and
|
||||
if strictlyPositiveIntegralExpr(x)
|
||||
then upper = true and delta = D::fromInt(-1)
|
||||
else
|
||||
if semPositive(x)
|
||||
then upper = true and delta = D::fromInt(0)
|
||||
// Constants have easy, base-case bounds, so let's not infer any recursive bounds.
|
||||
not e2 instanceof Sem::ConstantIntegerExpr and
|
||||
(
|
||||
valueFlowStep(e2, e1, delta) and
|
||||
upper = [true, false]
|
||||
or
|
||||
e2.(SafeCastExpr).getOperand() = e1 and
|
||||
delta = D::fromInt(0) and
|
||||
upper = [true, false]
|
||||
or
|
||||
javaCompatibility() and
|
||||
exists(Sem::Expr x, Sem::SubExpr sub |
|
||||
e2 = sub and
|
||||
sub.getLeftOperand() = e1 and
|
||||
sub.getRightOperand() = x
|
||||
|
|
||||
// `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
|
||||
not x instanceof Sem::ConstantIntegerExpr and
|
||||
if strictlyPositiveIntegralExpr(x)
|
||||
then upper = true and delta = D::fromInt(-1)
|
||||
else
|
||||
if strictlyNegativeIntegralExpr(x)
|
||||
then upper = false and delta = D::fromInt(1)
|
||||
if semPositive(x)
|
||||
then upper = true and delta = D::fromInt(0)
|
||||
else
|
||||
if semNegative(x)
|
||||
then upper = false and delta = D::fromInt(0)
|
||||
else none()
|
||||
if strictlyNegativeIntegralExpr(x)
|
||||
then upper = false and delta = D::fromInt(1)
|
||||
else
|
||||
if semNegative(x)
|
||||
then upper = false and delta = D::fromInt(0)
|
||||
else none()
|
||||
)
|
||||
or
|
||||
e2.(Sem::RemExpr).getRightOperand() = e1 and
|
||||
semPositive(e1) and
|
||||
delta = D::fromInt(-1) and
|
||||
upper = true
|
||||
or
|
||||
e2.(Sem::RemExpr).getLeftOperand() = e1 and
|
||||
semPositive(e1) and
|
||||
delta = D::fromInt(0) and
|
||||
upper = true
|
||||
or
|
||||
e2.(Sem::BitAndExpr).getAnOperand() = e1 and
|
||||
semPositive(e1) and
|
||||
delta = D::fromInt(0) and
|
||||
upper = true
|
||||
or
|
||||
e2.(Sem::BitOrExpr).getAnOperand() = e1 and
|
||||
semPositive(e2) and
|
||||
delta = D::fromInt(0) and
|
||||
upper = false
|
||||
or
|
||||
additionalBoundFlowStep(e2, e1, delta, upper)
|
||||
)
|
||||
or
|
||||
e2.(Sem::RemExpr).getRightOperand() = e1 and
|
||||
semPositive(e1) and
|
||||
delta = D::fromInt(-1) and
|
||||
upper = true
|
||||
or
|
||||
e2.(Sem::RemExpr).getLeftOperand() = e1 and
|
||||
semPositive(e1) and
|
||||
delta = D::fromInt(0) and
|
||||
upper = true
|
||||
or
|
||||
e2.(Sem::BitAndExpr).getAnOperand() = e1 and
|
||||
semPositive(e1) and
|
||||
delta = D::fromInt(0) and
|
||||
upper = true
|
||||
or
|
||||
e2.(Sem::BitOrExpr).getAnOperand() = e1 and
|
||||
semPositive(e2) and
|
||||
delta = D::fromInt(0) and
|
||||
upper = false
|
||||
or
|
||||
additionalBoundFlowStep(e2, e1, delta, upper)
|
||||
}
|
||||
|
||||
/** Holds if `e2 = e1 * factor` and `factor > 0`. */
|
||||
private predicate boundFlowStepMul(Sem::Expr e2, Sem::Expr e1, D::Delta factor) {
|
||||
not e2 instanceof Sem::ConstantIntegerExpr and
|
||||
exists(Sem::ConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
|
||||
e2.(Sem::MulExpr).hasOperands(e1, c) and factor = D::fromInt(k)
|
||||
or
|
||||
@@ -751,6 +760,7 @@ module RangeStage<
|
||||
* therefore only valid for non-negative numbers.
|
||||
*/
|
||||
private predicate boundFlowStepDiv(Sem::Expr e2, Sem::Expr e1, D::Delta factor) {
|
||||
not e2 instanceof Sem::ConstantIntegerExpr and
|
||||
Sem::getExprType(e2) instanceof Sem::IntegerType and
|
||||
exists(Sem::ConstantIntegerExpr c, D::Delta k |
|
||||
k = D::fromInt(c.getIntValue()) and D::toFloat(k) > 0
|
||||
@@ -983,16 +993,31 @@ module RangeStage<
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e` has an upper (for `upper = true`) or lower
|
||||
* (for `upper = false`) bound of `b`.
|
||||
*/
|
||||
private predicate baseBound(Sem::Expr e, D::Delta b, boolean upper) {
|
||||
hasConstantBound(e, b, upper)
|
||||
private predicate includeBound(SemBound b) {
|
||||
// always include phi bounds
|
||||
b.(SemSsaBound).getVariable() instanceof Sem::SsaPhiNode
|
||||
or
|
||||
upper = false and
|
||||
b = D::fromInt(0) and
|
||||
semPositive(e.(Sem::BitAndExpr).getAnOperand())
|
||||
if b instanceof SemZeroBound then includeConstantBounds() else includeRelativeBounds()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e` has an intrinsic upper (for `upper = true`) or lower
|
||||
* (for `upper = false`) bound of `b + delta` as a base case for range analysis.
|
||||
*/
|
||||
private predicate baseBound(Sem::Expr e, SemBound b, D::Delta delta, boolean upper) {
|
||||
includeBound(b) and
|
||||
(
|
||||
e = b.getExpr(delta) and
|
||||
upper = [true, false]
|
||||
or
|
||||
hasConstantBound(e, delta, upper) and
|
||||
b instanceof SemZeroBound
|
||||
or
|
||||
upper = false and
|
||||
delta = D::fromInt(0) and
|
||||
semPositive(e.(Sem::BitAndExpr).getAnOperand()) and
|
||||
b instanceof SemZeroBound
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1107,6 +1132,84 @@ module RangeStage<
|
||||
bindingset[x, y]
|
||||
private float truncatingDiv(float x, float y) { result = (x - (x % y)) / y }
|
||||
|
||||
/**
|
||||
* Holds if `e1 + delta` is a valid bound for `e2`.
|
||||
* - `upper = true` : `e2 <= e1 + delta`
|
||||
* - `upper = false` : `e2 >= e1 + delta`
|
||||
*
|
||||
* This is restricted to simple forward-flowing steps and disregards phi-nodes.
|
||||
*/
|
||||
private predicate preBoundStep(Sem::Expr e2, Sem::Expr e1, D::Delta delta, boolean upper) {
|
||||
boundFlowStep(e2, e1, delta, upper)
|
||||
or
|
||||
exists(Sem::SsaVariable v, SsaReadPositionBlock bb |
|
||||
boundFlowStepSsa(v, bb, e1, delta, upper, _) and
|
||||
bb.getAnSsaRead(v) = e2
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if simple forward-flowing steps from `e` can reach an expression that
|
||||
* has multiple incoming bound-flow edges, that is, it has multiple ways to
|
||||
* get a valid bound.
|
||||
*/
|
||||
private predicate reachesBoundMergepoint(Sem::Expr e, boolean upper) {
|
||||
2 <= strictcount(Sem::Expr mid | preBoundStep(e, mid, _, upper))
|
||||
or
|
||||
exists(Sem::SsaPhiNode v, SsaReadPositionBlock bb |
|
||||
boundFlowStepSsa(v, bb, _, _, upper, _) and
|
||||
bb.getAnSsaRead(v) = e
|
||||
)
|
||||
or
|
||||
exists(Sem::Expr e2 |
|
||||
preBoundStep(e2, e, _, upper) and
|
||||
reachesBoundMergepoint(e2, upper)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate relevantPreBoundStep(Sem::Expr e2, Sem::Expr e1, D::Delta delta, boolean upper) {
|
||||
preBoundStep(e2, e1, delta, upper) and
|
||||
reachesBoundMergepoint(e2, upper)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `e` that can be found using only
|
||||
* simple forward-flowing steps and disregarding phi-nodes.
|
||||
* - `upper = true` : `e <= b + delta`
|
||||
* - `upper = false` : `e >= b + delta`
|
||||
*
|
||||
* This predicate is used as a fast approximation for `bounded` to avoid
|
||||
* excessive computation in certain cases. In particular, this applies to
|
||||
* loop-unrolled code like
|
||||
* ```
|
||||
* if (..) x+=1; else x+=100;
|
||||
* x &= 7;
|
||||
* if (..) x+=1; else x+=100;
|
||||
* x &= 7;
|
||||
* if (..) x+=1; else x+=100;
|
||||
* x &= 7;
|
||||
* ...
|
||||
* ```
|
||||
*/
|
||||
private predicate preBounded(Sem::Expr e, SemBound b, D::Delta delta, boolean upper) {
|
||||
baseBound(e, b, delta, upper)
|
||||
or
|
||||
exists(Sem::Expr mid, D::Delta d1, D::Delta d2 |
|
||||
relevantPreBoundStep(e, mid, d1, upper) and
|
||||
preBounded(mid, b, d2, upper) and
|
||||
delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2))
|
||||
)
|
||||
}
|
||||
|
||||
private predicate bestPreBound(Sem::Expr e, SemBound b, D::Delta delta, boolean upper) {
|
||||
delta = min(D::Delta d | preBounded(e, b, d, upper) | d order by D::toFloat(d)) and
|
||||
upper = true
|
||||
or
|
||||
delta = max(D::Delta d | preBounded(e, b, d, upper) | d order by D::toFloat(d)) and
|
||||
upper = false
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `e`.
|
||||
* - `upper = true` : `e <= b + delta`
|
||||
@@ -1117,15 +1220,14 @@ module RangeStage<
|
||||
D::Delta origdelta, SemReason reason
|
||||
) {
|
||||
not ignoreExprBound(e) and
|
||||
(
|
||||
e = b.getExpr(delta) and
|
||||
(upper = true or upper = false) and
|
||||
fromBackEdge = false and
|
||||
origdelta = delta and
|
||||
reason = TSemNoReason()
|
||||
// ignore poor bounds
|
||||
not exists(D::Delta d | bestPreBound(e, b, d, upper) |
|
||||
D::toFloat(delta) > D::toFloat(d) and upper = true
|
||||
or
|
||||
baseBound(e, delta, upper) and
|
||||
b instanceof SemZeroBound and
|
||||
D::toFloat(delta) < D::toFloat(d) and upper = false
|
||||
) and
|
||||
(
|
||||
baseBound(e, b, delta, upper) and
|
||||
fromBackEdge = false and
|
||||
origdelta = delta and
|
||||
reason = TSemNoReason()
|
||||
@@ -1137,8 +1239,6 @@ module RangeStage<
|
||||
or
|
||||
exists(Sem::Expr mid, D::Delta d1, D::Delta d2 |
|
||||
boundFlowStep(e, mid, d1, upper) and
|
||||
// Constants have easy, base-case bounds, so let's not infer any recursive bounds.
|
||||
not e instanceof Sem::ConstantIntegerExpr and
|
||||
bounded(mid, b, d2, upper, fromBackEdge, origdelta, reason) and
|
||||
// upper = true: e <= mid + d1 <= b + d1 + d2 = b + delta
|
||||
// upper = false: e >= mid + d1 >= b + d1 + d2 = b + delta
|
||||
@@ -1152,7 +1252,6 @@ module RangeStage<
|
||||
or
|
||||
exists(Sem::Expr mid, D::Delta factor, D::Delta d |
|
||||
boundFlowStepMul(e, mid, factor) and
|
||||
not e instanceof Sem::ConstantIntegerExpr and
|
||||
bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
|
||||
b instanceof SemZeroBound and
|
||||
delta = D::fromFloat(D::toFloat(d) * D::toFloat(factor))
|
||||
@@ -1160,7 +1259,6 @@ module RangeStage<
|
||||
or
|
||||
exists(Sem::Expr mid, D::Delta factor, D::Delta d |
|
||||
boundFlowStepDiv(e, mid, factor) and
|
||||
not e instanceof Sem::ConstantIntegerExpr and
|
||||
bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
|
||||
b instanceof SemZeroBound and
|
||||
D::toFloat(d) >= 0 and
|
||||
|
||||
Reference in New Issue
Block a user