@@ -995,15 +995,23 @@ module RangeStage<
995995 }
996996
997997 /**
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 .
10001000 */
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+ )
10071015 }
10081016
10091017 /**
@@ -1129,19 +1137,10 @@ module RangeStage<
11291137 ) {
11301138 not ignoreExprBound ( e ) and
11311139 (
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
11411141 fromBackEdge = false and
11421142 origdelta = delta and
1143- reason = TSemNoReason ( ) and
1144- includeBound ( b )
1143+ reason = TSemNoReason ( )
11451144 or
11461145 exists ( Sem:: SsaVariable v , SsaReadPositionBlock bb |
11471146 boundedSsa ( v , b , delta , bb , upper , fromBackEdge , origdelta , reason ) and
0 commit comments