@@ -995,15 +995,23 @@ module RangeStage<
995
995
}
996
996
997
997
/**
998
- * Holds if `e` has an upper (for `upper = true`) or lower
999
- * (for `upper = false`) bound of `b` .
998
+ * Holds if `e` has an intrinsic upper (for `upper = true`) or lower
999
+ * (for `upper = false`) bound of `b + delta` as a base case for range analysis .
1000
1000
*/
1001
- private predicate baseBound ( Sem:: Expr e , D:: Delta b , boolean upper ) {
1002
- hasConstantBound ( e , b , upper )
1003
- or
1004
- upper = false and
1005
- b = D:: fromInt ( 0 ) and
1006
- semPositive ( e .( Sem:: BitAndExpr ) .getAnOperand ( ) )
1001
+ private predicate baseBound ( Sem:: Expr e , SemBound b , D:: Delta delta , boolean upper ) {
1002
+ includeBound ( b ) and
1003
+ (
1004
+ e = b .getExpr ( delta ) and
1005
+ upper = [ true , false ]
1006
+ or
1007
+ hasConstantBound ( e , delta , upper ) and
1008
+ b instanceof SemZeroBound
1009
+ or
1010
+ upper = false and
1011
+ delta = D:: fromInt ( 0 ) and
1012
+ semPositive ( e .( Sem:: BitAndExpr ) .getAnOperand ( ) ) and
1013
+ b instanceof SemZeroBound
1014
+ )
1007
1015
}
1008
1016
1009
1017
/**
@@ -1129,19 +1137,10 @@ module RangeStage<
1129
1137
) {
1130
1138
not ignoreExprBound ( e ) and
1131
1139
(
1132
- e = b .getExpr ( delta ) and
1133
- ( upper = true or upper = false ) and
1134
- fromBackEdge = false and
1135
- origdelta = delta and
1136
- reason = TSemNoReason ( ) and
1137
- includeBound ( b )
1138
- or
1139
- baseBound ( e , delta , upper ) and
1140
- b instanceof SemZeroBound and
1140
+ baseBound ( e , b , delta , upper ) and
1141
1141
fromBackEdge = false and
1142
1142
origdelta = delta and
1143
- reason = TSemNoReason ( ) and
1144
- includeBound ( b )
1143
+ reason = TSemNoReason ( )
1145
1144
or
1146
1145
exists ( Sem:: SsaVariable v , SsaReadPositionBlock bb |
1147
1146
boundedSsa ( v , b , delta , bb , upper , fromBackEdge , origdelta , reason ) and
0 commit comments