@@ -769,26 +769,32 @@ private float getLowerBoundsImpl(Expr expr) {
769
769
exists ( float x , float y |
770
770
x = getFullyConvertedLowerBounds ( maxExpr .getLeftOperand ( ) ) and
771
771
y = getFullyConvertedLowerBounds ( maxExpr .getRightOperand ( ) ) and
772
- if x >= y then result = x else result = y
772
+ result = x . maximum ( y )
773
773
)
774
774
)
775
775
or
776
- // ConditionalExpr (true branch)
777
- exists ( ConditionalExpr condExpr |
776
+ exists ( ConditionalExpr condExpr , Expr conv , float ub , float lb |
778
777
expr = condExpr and
778
+ conv = condExpr .getCondition ( ) .getFullyConverted ( ) and
779
779
// Use `boolConversionUpperBound` to determine whether the condition
780
780
// might evaluate to `true`.
781
- boolConversionUpperBound ( condExpr .getCondition ( ) .getFullyConverted ( ) ) = 1 and
782
- result = getFullyConvertedLowerBounds ( condExpr .getThen ( ) )
783
- )
784
- or
785
- // ConditionalExpr (false branch)
786
- exists ( ConditionalExpr condExpr |
787
- expr = condExpr and
788
- // Use `boolConversionLowerBound` to determine whether the condition
789
- // might evaluate to `false`.
790
- boolConversionLowerBound ( condExpr .getCondition ( ) .getFullyConverted ( ) ) = 0 and
791
- result = getFullyConvertedLowerBounds ( condExpr .getElse ( ) )
781
+ lb = boolConversionLowerBound ( conv ) and
782
+ ub = boolConversionUpperBound ( conv )
783
+ |
784
+ // Both branches can be taken
785
+ ub = 1 and
786
+ lb = 0 and
787
+ exists ( float thenLb , float elseLb |
788
+ thenLb = getFullyConvertedLowerBounds ( condExpr .getThen ( ) ) and
789
+ elseLb = getFullyConvertedLowerBounds ( condExpr .getElse ( ) ) and
790
+ result = thenLb .minimum ( elseLb )
791
+ )
792
+ or
793
+ // Only the `true` branch can be taken
794
+ ub = 1 and lb != 0 and result = getFullyConvertedLowerBounds ( condExpr .getThen ( ) )
795
+ or
796
+ // Only the `false` branch can be taken
797
+ ub != 1 and lb = 0 and result = getFullyConvertedLowerBounds ( condExpr .getElse ( ) )
792
798
)
793
799
or
794
800
exists ( AddExpr addExpr , float xLow , float yLow |
@@ -973,26 +979,32 @@ private float getUpperBoundsImpl(Expr expr) {
973
979
exists ( float x , float y |
974
980
x = getFullyConvertedUpperBounds ( minExpr .getLeftOperand ( ) ) and
975
981
y = getFullyConvertedUpperBounds ( minExpr .getRightOperand ( ) ) and
976
- if x <= y then result = x else result = y
982
+ result = x . minimum ( y )
977
983
)
978
984
)
979
985
or
980
- // ConditionalExpr (true branch)
981
- exists ( ConditionalExpr condExpr |
986
+ exists ( ConditionalExpr condExpr , Expr conv , float ub , float lb |
982
987
expr = condExpr and
988
+ conv = condExpr .getCondition ( ) .getFullyConverted ( ) and
983
989
// Use `boolConversionUpperBound` to determine whether the condition
984
990
// might evaluate to `true`.
985
- boolConversionUpperBound ( condExpr .getCondition ( ) .getFullyConverted ( ) ) = 1 and
986
- result = getFullyConvertedUpperBounds ( condExpr .getThen ( ) )
987
- )
988
- or
989
- // ConditionalExpr (false branch)
990
- exists ( ConditionalExpr condExpr |
991
- expr = condExpr and
992
- // Use `boolConversionLowerBound` to determine whether the condition
993
- // might evaluate to `false`.
994
- boolConversionLowerBound ( condExpr .getCondition ( ) .getFullyConverted ( ) ) = 0 and
995
- result = getFullyConvertedUpperBounds ( condExpr .getElse ( ) )
991
+ lb = boolConversionLowerBound ( conv ) and
992
+ ub = boolConversionUpperBound ( conv )
993
+ |
994
+ // Both branches can be taken
995
+ ub = 1 and
996
+ lb = 0 and
997
+ exists ( float thenLb , float elseLb |
998
+ thenLb = getFullyConvertedUpperBounds ( condExpr .getThen ( ) ) and
999
+ elseLb = getFullyConvertedUpperBounds ( condExpr .getElse ( ) ) and
1000
+ result = thenLb .maximum ( elseLb )
1001
+ )
1002
+ or
1003
+ // Only the `true` branch can be taken
1004
+ ub = 1 and lb != 0 and result = getFullyConvertedUpperBounds ( condExpr .getThen ( ) )
1005
+ or
1006
+ // Only the `false` branch can be taken
1007
+ ub != 1 and lb = 0 and result = getFullyConvertedUpperBounds ( condExpr .getElse ( ) )
996
1008
)
997
1009
or
998
1010
exists ( AddExpr addExpr , float xHigh , float yHigh |
@@ -1140,10 +1152,7 @@ private float getUpperBoundsImpl(Expr expr) {
1140
1152
not expr instanceof SimpleRangeAnalysisExpr
1141
1153
or
1142
1154
// A modeled expression for range analysis
1143
- exists ( SimpleRangeAnalysisExpr rangeAnalysisExpr |
1144
- rangeAnalysisExpr = expr and
1145
- result = rangeAnalysisExpr .getUpperBounds ( )
1146
- )
1155
+ result = expr .( SimpleRangeAnalysisExpr ) .getUpperBounds ( )
1147
1156
}
1148
1157
1149
1158
/**
@@ -1594,7 +1603,7 @@ private module SimpleRangeAnalysisCached {
1594
1603
* the lower bound of the expression after all the casts have been applied,
1595
1604
* call `lowerBound` like this:
1596
1605
*
1597
- * ` lowerBound(expr.getFullyConverted())`
1606
+ * lowerBound(expr.getFullyConverted())
1598
1607
*/
1599
1608
cached
1600
1609
float lowerBound ( Expr expr ) {
@@ -1613,7 +1622,7 @@ private module SimpleRangeAnalysisCached {
1613
1622
* the upper bound of the expression after all the casts have been applied,
1614
1623
* call `upperBound` like this:
1615
1624
*
1616
- * ` upperBound(expr.getFullyConverted())`
1625
+ * upperBound(expr.getFullyConverted())
1617
1626
*/
1618
1627
cached
1619
1628
float upperBound ( Expr expr ) {
0 commit comments