Skip to content

Commit a78756f

Browse files
committed
Merge branch 'main' into splitoff
2 parents 479c58b + c28062a commit a78756f

File tree

178 files changed

+37037
-34329
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

178 files changed

+37037
-34329
lines changed

cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll

Lines changed: 40 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -158,22 +158,6 @@ private class UnsignedBitwiseAndExpr extends BitwiseAndExpr {
158158
}
159159
}
160160

161-
/**
162-
* Gets the floor of `v`, with additional logic to work around issues with
163-
* large numbers.
164-
*/
165-
bindingset[v]
166-
float safeFloor(float v) {
167-
// return the floor of v
168-
v.abs() < 2.pow(31) and
169-
result = v.floor()
170-
or
171-
// `floor()` doesn't work correctly on large numbers (since it returns an integer),
172-
// so fall back to unrounded numbers at this scale.
173-
not v.abs() < 2.pow(31) and
174-
result = v
175-
}
176-
177161
/** A `MulExpr` where exactly one operand is constant. */
178162
private class MulByConstantExpr extends MulExpr {
179163
float constant;
@@ -1266,7 +1250,7 @@ private float getLowerBoundsImpl(Expr expr) {
12661250
rsExpr = expr and
12671251
left = getFullyConvertedLowerBounds(rsExpr.getLeftOperand()) and
12681252
right = getValue(rsExpr.getRightOperand().getFullyConverted()).toInt() and
1269-
result = safeFloor(left / 2.pow(right))
1253+
result = (left / 2.pow(right)).floorFloat()
12701254
)
12711255
// Not explicitly modeled by a SimpleRangeAnalysisExpr
12721256
) and
@@ -1475,7 +1459,7 @@ private float getUpperBoundsImpl(Expr expr) {
14751459
rsExpr = expr and
14761460
left = getFullyConvertedUpperBounds(rsExpr.getLeftOperand()) and
14771461
right = getValue(rsExpr.getRightOperand().getFullyConverted()).toInt() and
1478-
result = safeFloor(left / 2.pow(right))
1462+
result = (left / 2.pow(right)).floorFloat()
14791463
)
14801464
// Not explicitly modeled by a SimpleRangeAnalysisExpr
14811465
) and
@@ -1725,6 +1709,22 @@ predicate nonNanGuardedVariable(Expr guard, VariableAccess v, boolean branch) {
17251709
nanExcludingComparison(guard, branch)
17261710
}
17271711

1712+
/**
1713+
* Adjusts a lower bound to its meaning for integral types.
1714+
*
1715+
* Examples:
1716+
* `>= 3.0` becomes `3.0`
1717+
* ` > 3.0` becomes `4.0`
1718+
* `>= 3.5` becomes `4.0`
1719+
* ` > 3.5` becomes `4.0`
1720+
*/
1721+
bindingset[strictness, lb]
1722+
private float adjustLowerBoundIntegral(RelationStrictness strictness, float lb) {
1723+
if strictness = Nonstrict() and lb.floorFloat() = lb
1724+
then result = lb
1725+
else result = lb.floorFloat() + 1
1726+
}
1727+
17281728
/**
17291729
* If the guard is a comparison of the form `p*v + q <CMP> r`, then this
17301730
* predicate uses the bounds information for `r` to compute a lower bound
@@ -1736,15 +1736,29 @@ private predicate lowerBoundFromGuard(Expr guard, VariableAccess v, float lb, bo
17361736
|
17371737
if nonNanGuardedVariable(guard, v, branch)
17381738
then
1739-
if
1740-
strictness = Nonstrict() or
1741-
not getVariableRangeType(v.getTarget()) instanceof IntegralType
1742-
then lb = childLB
1743-
else lb = childLB + 1
1739+
if getVariableRangeType(v.getTarget()) instanceof IntegralType
1740+
then lb = adjustLowerBoundIntegral(strictness, childLB)
1741+
else lb = childLB
17441742
else lb = varMinVal(v.getTarget())
17451743
)
17461744
}
17471745

1746+
/**
1747+
* Adjusts an upper bound to its meaning for integral types.
1748+
*
1749+
* Examples:
1750+
* `<= 3.0` becomes `3.0`
1751+
* ` < 3.0` becomes `2.0`
1752+
* `<= 3.5` becomes `3.0`
1753+
* ` < 3.5` becomes `3.0`
1754+
*/
1755+
bindingset[strictness, ub]
1756+
private float adjustUpperBoundIntegral(RelationStrictness strictness, float ub) {
1757+
if strictness = Nonstrict() and ub.ceilFloat() = ub
1758+
then result = ub
1759+
else result = ub.ceilFloat() - 1
1760+
}
1761+
17481762
/**
17491763
* If the guard is a comparison of the form `p*v + q <CMP> r`, then this
17501764
* predicate uses the bounds information for `r` to compute a upper bound
@@ -1756,11 +1770,9 @@ private predicate upperBoundFromGuard(Expr guard, VariableAccess v, float ub, bo
17561770
|
17571771
if nonNanGuardedVariable(guard, v, branch)
17581772
then
1759-
if
1760-
strictness = Nonstrict() or
1761-
not getVariableRangeType(v.getTarget()) instanceof IntegralType
1762-
then ub = childUB
1763-
else ub = childUB - 1
1773+
if getVariableRangeType(v.getTarget()) instanceof IntegralType
1774+
then ub = adjustUpperBoundIntegral(strictness, childUB)
1775+
else ub = childUB
17641776
else ub = varMaxVal(v.getTarget())
17651777
)
17661778
}

0 commit comments

Comments
 (0)