Skip to content

Commit c14d917

Browse files
committed
Rangeanalysis: Prune range calculation.
1 parent 58d463d commit c14d917

File tree

1 file changed

+50
-0
lines changed

1 file changed

+50
-0
lines changed

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1132,6 +1132,50 @@ module RangeStage<
11321132
bindingset[x, y]
11331133
private float truncatingDiv(float x, float y) { result = (x - (x % y)) / y }
11341134

1135+
/**
1136+
* Holds if `b + delta` is a valid bound for `e` that can be found using only
1137+
* simple forward-flowing steps and disregarding phi-nodes.
1138+
* - `upper = true` : `e <= b + delta`
1139+
* - `upper = false` : `e >= b + delta`
1140+
*
1141+
* This predicate is used as a fast approximation for `bounded` to avoid
1142+
* excessive computation in certain cases. In particular, this applies to
1143+
* loop-unrolled code like
1144+
* ```
1145+
* if (..) x+=1; else x+=100;
1146+
* x &= 7;
1147+
* if (..) x+=1; else x+=100;
1148+
* x &= 7;
1149+
* if (..) x+=1; else x+=100;
1150+
* x &= 7;
1151+
* ...
1152+
* ```
1153+
*/
1154+
private predicate preBounded(Sem::Expr e, SemBound b, D::Delta delta, boolean upper) {
1155+
baseBound(e, b, delta, upper)
1156+
or
1157+
exists(Sem::Expr mid, D::Delta d1, D::Delta d2 |
1158+
boundFlowStep(e, mid, d1, upper) and
1159+
preBounded(mid, b, d2, upper) and
1160+
delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2))
1161+
)
1162+
or
1163+
exists(Sem::SsaVariable v, SsaReadPositionBlock bb, Sem::Expr mid, D::Delta d1, D::Delta d2 |
1164+
boundFlowStepSsa(v, bb, mid, d1, upper, _) and
1165+
preBounded(mid, b, d2, upper) and
1166+
delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2)) and
1167+
bb.getAnSsaRead(v) = e
1168+
)
1169+
}
1170+
1171+
private predicate bestPreBound(Sem::Expr e, SemBound b, D::Delta delta, boolean upper) {
1172+
delta = min(D::Delta d | preBounded(e, b, d, upper) | d order by D::toFloat(d)) and
1173+
upper = true
1174+
or
1175+
delta = max(D::Delta d | preBounded(e, b, d, upper) | d order by D::toFloat(d)) and
1176+
upper = false
1177+
}
1178+
11351179
/**
11361180
* Holds if `b + delta` is a valid bound for `e`.
11371181
* - `upper = true` : `e <= b + delta`
@@ -1142,6 +1186,12 @@ module RangeStage<
11421186
D::Delta origdelta, SemReason reason
11431187
) {
11441188
not ignoreExprBound(e) and
1189+
// ignore poor bounds
1190+
not exists(D::Delta d | bestPreBound(e, b, d, upper) |
1191+
D::toFloat(delta) > D::toFloat(d) and upper = true
1192+
or
1193+
D::toFloat(delta) < D::toFloat(d) and upper = false
1194+
) and
11451195
(
11461196
baseBound(e, b, delta, upper) and
11471197
fromBackEdge = false and

0 commit comments

Comments
 (0)