@@ -682,60 +682,65 @@ module RangeStage<
682682 * - `upper = false` : `e2 >= e1 + delta`
683683 */
684684 private predicate boundFlowStep ( Sem:: Expr e2 , Sem:: Expr e1 , D:: Delta delta , boolean upper ) {
685- valueFlowStep ( e2 , e1 , delta ) and
686- ( upper = true or upper = false )
687- or
688- e2 . ( SafeCastExpr ) . getOperand ( ) = e1 and
689- delta = D :: fromInt ( 0 ) and
690- ( upper = true or upper = false )
691- or
692- javaCompatibility ( ) and
693- exists ( Sem :: Expr x , Sem :: SubExpr sub |
694- e2 = sub and
695- sub . getLeftOperand ( ) = e1 and
696- sub . getRightOperand ( ) = x
697- |
698- // `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
699- not x instanceof Sem :: ConstantIntegerExpr and
700- if strictlyPositiveIntegralExpr ( x )
701- then upper = true and delta = D :: fromInt ( - 1 )
702- else
703- if semPositive ( x )
704- then upper = true and delta = D:: fromInt ( 0 )
685+ // Constants have easy, base-case bounds, so let's not infer any recursive bounds.
686+ not e2 instanceof Sem :: ConstantIntegerExpr and
687+ (
688+ valueFlowStep ( e2 , e1 , delta ) and
689+ upper = [ true , false ]
690+ or
691+ e2 . ( SafeCastExpr ) . getOperand ( ) = e1 and
692+ delta = D :: fromInt ( 0 ) and
693+ upper = [ true , false ]
694+ or
695+ javaCompatibility ( ) and
696+ exists ( Sem :: Expr x , Sem :: SubExpr sub |
697+ e2 = sub and
698+ sub . getLeftOperand ( ) = e1 and
699+ sub . getRightOperand ( ) = x
700+ |
701+ // `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
702+ not x instanceof Sem :: ConstantIntegerExpr and
703+ if strictlyPositiveIntegralExpr ( x )
704+ then upper = true and delta = D:: fromInt ( - 1 )
705705 else
706- if strictlyNegativeIntegralExpr ( x )
707- then upper = false and delta = D:: fromInt ( 1 )
706+ if semPositive ( x )
707+ then upper = true and delta = D:: fromInt ( 0 )
708708 else
709- if semNegative ( x )
710- then upper = false and delta = D:: fromInt ( 0 )
711- else none ( )
709+ if strictlyNegativeIntegralExpr ( x )
710+ then upper = false and delta = D:: fromInt ( 1 )
711+ else
712+ if semNegative ( x )
713+ then upper = false and delta = D:: fromInt ( 0 )
714+ else none ( )
715+ )
716+ or
717+ e2 .( Sem:: RemExpr ) .getRightOperand ( ) = e1 and
718+ semPositive ( e1 ) and
719+ delta = D:: fromInt ( - 1 ) and
720+ upper = true
721+ or
722+ e2 .( Sem:: RemExpr ) .getLeftOperand ( ) = e1 and
723+ semPositive ( e1 ) and
724+ delta = D:: fromInt ( 0 ) and
725+ upper = true
726+ or
727+ e2 .( Sem:: BitAndExpr ) .getAnOperand ( ) = e1 and
728+ semPositive ( e1 ) and
729+ delta = D:: fromInt ( 0 ) and
730+ upper = true
731+ or
732+ e2 .( Sem:: BitOrExpr ) .getAnOperand ( ) = e1 and
733+ semPositive ( e2 ) and
734+ delta = D:: fromInt ( 0 ) and
735+ upper = false
736+ or
737+ additionalBoundFlowStep ( e2 , e1 , delta , upper )
712738 )
713- or
714- e2 .( Sem:: RemExpr ) .getRightOperand ( ) = e1 and
715- semPositive ( e1 ) and
716- delta = D:: fromInt ( - 1 ) and
717- upper = true
718- or
719- e2 .( Sem:: RemExpr ) .getLeftOperand ( ) = e1 and
720- semPositive ( e1 ) and
721- delta = D:: fromInt ( 0 ) and
722- upper = true
723- or
724- e2 .( Sem:: BitAndExpr ) .getAnOperand ( ) = e1 and
725- semPositive ( e1 ) and
726- delta = D:: fromInt ( 0 ) and
727- upper = true
728- or
729- e2 .( Sem:: BitOrExpr ) .getAnOperand ( ) = e1 and
730- semPositive ( e2 ) and
731- delta = D:: fromInt ( 0 ) and
732- upper = false
733- or
734- additionalBoundFlowStep ( e2 , e1 , delta , upper )
735739 }
736740
737741 /** Holds if `e2 = e1 * factor` and `factor > 0`. */
738742 private predicate boundFlowStepMul ( Sem:: Expr e2 , Sem:: Expr e1 , D:: Delta factor ) {
743+ not e2 instanceof Sem:: ConstantIntegerExpr and
739744 exists ( Sem:: ConstantIntegerExpr c , int k | k = c .getIntValue ( ) and k > 0 |
740745 e2 .( Sem:: MulExpr ) .hasOperands ( e1 , c ) and factor = D:: fromInt ( k )
741746 or
@@ -755,6 +760,7 @@ module RangeStage<
755760 * therefore only valid for non-negative numbers.
756761 */
757762 private predicate boundFlowStepDiv ( Sem:: Expr e2 , Sem:: Expr e1 , D:: Delta factor ) {
763+ not e2 instanceof Sem:: ConstantIntegerExpr and
758764 Sem:: getExprType ( e2 ) instanceof Sem:: IntegerType and
759765 exists ( Sem:: ConstantIntegerExpr c , D:: Delta k |
760766 k = D:: fromInt ( c .getIntValue ( ) ) and D:: toFloat ( k ) > 0
@@ -1149,8 +1155,6 @@ module RangeStage<
11491155 or
11501156 exists ( Sem:: Expr mid , D:: Delta d1 , D:: Delta d2 |
11511157 boundFlowStep ( e , mid , d1 , upper ) and
1152- // Constants have easy, base-case bounds, so let's not infer any recursive bounds.
1153- not e instanceof Sem:: ConstantIntegerExpr and
11541158 bounded ( mid , b , d2 , upper , fromBackEdge , origdelta , reason ) and
11551159 // upper = true: e <= mid + d1 <= b + d1 + d2 = b + delta
11561160 // upper = false: e >= mid + d1 >= b + d1 + d2 = b + delta
@@ -1164,15 +1168,13 @@ module RangeStage<
11641168 or
11651169 exists ( Sem:: Expr mid , D:: Delta factor , D:: Delta d |
11661170 boundFlowStepMul ( e , mid , factor ) and
1167- not e instanceof Sem:: ConstantIntegerExpr and
11681171 bounded ( mid , b , d , upper , fromBackEdge , origdelta , reason ) and
11691172 b instanceof SemZeroBound and
11701173 delta = D:: fromFloat ( D:: toFloat ( d ) * D:: toFloat ( factor ) )
11711174 )
11721175 or
11731176 exists ( Sem:: Expr mid , D:: Delta factor , D:: Delta d |
11741177 boundFlowStepDiv ( e , mid , factor ) and
1175- not e instanceof Sem:: ConstantIntegerExpr and
11761178 bounded ( mid , b , d , upper , fromBackEdge , origdelta , reason ) and
11771179 b instanceof SemZeroBound and
11781180 D:: toFloat ( d ) >= 0 and
0 commit comments