Skip to content

Commit

Permalink
Rangeanalysis: Prune range calculation.
Browse files Browse the repository at this point in the history
  • Loading branch information
aschackmull committed Dec 7, 2023
1 parent eb150cc commit 3b8e180
Showing 1 changed file with 50 additions and 0 deletions.
50 changes: 50 additions & 0 deletions shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
Original file line number Diff line number Diff line change
Expand Up @@ -1132,6 +1132,50 @@ module RangeStage<
bindingset[x, y]
private float truncatingDiv(float x, float y) { result = (x - (x % y)) / y }

/**
* 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 |
boundFlowStep(e, mid, d1, upper) and
preBounded(mid, b, d2, upper) and
delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2))
)
or
exists(Sem::SsaVariable v, SsaReadPositionBlock bb, Sem::Expr mid, D::Delta d1, D::Delta d2 |
boundFlowStepSsa(v, bb, mid, d1, upper, _) and
preBounded(mid, b, d2, upper) and
delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2)) and
bb.getAnSsaRead(v) = e
)
}

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`
Expand All @@ -1142,6 +1186,12 @@ module RangeStage<
D::Delta origdelta, SemReason reason
) {
not ignoreExprBound(e) and
// ignore poor bounds
not exists(D::Delta d | bestPreBound(e, b, d, upper) |
D::toFloat(delta) > D::toFloat(d) and upper = true
or
D::toFloat(delta) < D::toFloat(d) and upper = false
) and
(
baseBound(e, b, delta, upper) and
fromBackEdge = false and
Expand Down

0 comments on commit 3b8e180

Please sign in to comment.