Skip to content

Commit 8aaf9f6

Browse files
committed
C++: Factor out widening of bounds
1 parent 7bf677d commit 8aaf9f6

File tree

1 file changed

+16
-26
lines changed

1 file changed

+16
-26
lines changed

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

Lines changed: 16 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,18 @@ private float wideningUpperBounds(ArithmeticType t) {
9393
result = 1.0 / 0.0 // +Inf
9494
}
9595

96+
/** Gets the widened lower bound for a given type and lower bound. */
97+
bindingset[type, lb]
98+
float widenLowerBound(Type type, float lb) {
99+
result = max(float widenLB | widenLB = wideningLowerBounds(type) and widenLB <= lb | widenLB)
100+
}
101+
102+
/** Gets the widened upper bound for a given type and upper bound. */
103+
bindingset[type, ub]
104+
float widenUpperBound(Type type, float ub) {
105+
result = min(float widenUB | widenUB = wideningUpperBounds(type) and widenUB >= ub | widenUB)
106+
}
107+
96108
/**
97109
* Gets the value of the expression `e`, if it is a constant.
98110
* This predicate also handles the case of constant variables initialized in different
@@ -656,12 +668,7 @@ private float getTruncatedLowerBounds(Expr expr) {
656668
then
657669
// Apply widening where we might get a combinatorial explosion.
658670
if isRecursiveBinary(expr)
659-
then
660-
result =
661-
max(float widenLB |
662-
widenLB = wideningLowerBounds(expr.getUnspecifiedType()) and
663-
not widenLB > newLB
664-
)
671+
then result = widenLowerBound(expr.getUnspecifiedType(), newLB)
665672
else result = newLB
666673
else result = exprMinVal(expr)
667674
) and
@@ -715,12 +722,7 @@ private float getTruncatedUpperBounds(Expr expr) {
715722
then
716723
// Apply widening where we might get a combinatorial explosion.
717724
if isRecursiveBinary(expr)
718-
then
719-
result =
720-
min(float widenUB |
721-
widenUB = wideningUpperBounds(expr.getUnspecifiedType()) and
722-
not widenUB < newUB
723-
)
725+
then result = widenUpperBound(expr.getUnspecifiedType(), newUB)
724726
else result = newUB
725727
else result = exprMaxVal(expr)
726728
)
@@ -1815,13 +1817,7 @@ module SimpleRangeAnalysisInternal {
18151817
// The new lower bound is from a recursive source, so we round
18161818
// down to one of a limited set of values to prevent the
18171819
// recursion from exploding.
1818-
result =
1819-
max(float widenLB |
1820-
widenLB = wideningLowerBounds(getVariableRangeType(v)) and
1821-
not widenLB > truncatedLB
1822-
|
1823-
widenLB
1824-
)
1820+
result = widenLowerBound(getVariableRangeType(v), truncatedLB)
18251821
else result = truncatedLB
18261822
)
18271823
or
@@ -1845,13 +1841,7 @@ module SimpleRangeAnalysisInternal {
18451841
// The new upper bound is from a recursive source, so we round
18461842
// up to one of a fixed set of values to prevent the recursion
18471843
// from exploding.
1848-
result =
1849-
min(float widenUB |
1850-
widenUB = wideningUpperBounds(getVariableRangeType(v)) and
1851-
not widenUB < truncatedUB
1852-
|
1853-
widenUB
1854-
)
1844+
result = widenUpperBound(getVariableRangeType(v), truncatedUB)
18551845
else result = truncatedUB
18561846
)
18571847
or

0 commit comments

Comments
 (0)