@@ -682,60 +682,65 @@ module RangeStage<
682
682
* - `upper = false` : `e2 >= e1 + delta`
683
683
*/
684
684
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 )
705
705
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 )
708
708
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 )
712
738
)
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 )
735
739
}
736
740
737
741
/** Holds if `e2 = e1 * factor` and `factor > 0`. */
738
742
private predicate boundFlowStepMul ( Sem:: Expr e2 , Sem:: Expr e1 , D:: Delta factor ) {
743
+ not e2 instanceof Sem:: ConstantIntegerExpr and
739
744
exists ( Sem:: ConstantIntegerExpr c , int k | k = c .getIntValue ( ) and k > 0 |
740
745
e2 .( Sem:: MulExpr ) .hasOperands ( e1 , c ) and factor = D:: fromInt ( k )
741
746
or
@@ -755,6 +760,7 @@ module RangeStage<
755
760
* therefore only valid for non-negative numbers.
756
761
*/
757
762
private predicate boundFlowStepDiv ( Sem:: Expr e2 , Sem:: Expr e1 , D:: Delta factor ) {
763
+ not e2 instanceof Sem:: ConstantIntegerExpr and
758
764
Sem:: getExprType ( e2 ) instanceof Sem:: IntegerType and
759
765
exists ( Sem:: ConstantIntegerExpr c , D:: Delta k |
760
766
k = D:: fromInt ( c .getIntValue ( ) ) and D:: toFloat ( k ) > 0
@@ -1149,8 +1155,6 @@ module RangeStage<
1149
1155
or
1150
1156
exists ( Sem:: Expr mid , D:: Delta d1 , D:: Delta d2 |
1151
1157
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
1154
1158
bounded ( mid , b , d2 , upper , fromBackEdge , origdelta , reason ) and
1155
1159
// upper = true: e <= mid + d1 <= b + d1 + d2 = b + delta
1156
1160
// upper = false: e >= mid + d1 >= b + d1 + d2 = b + delta
@@ -1164,15 +1168,13 @@ module RangeStage<
1164
1168
or
1165
1169
exists ( Sem:: Expr mid , D:: Delta factor , D:: Delta d |
1166
1170
boundFlowStepMul ( e , mid , factor ) and
1167
- not e instanceof Sem:: ConstantIntegerExpr and
1168
1171
bounded ( mid , b , d , upper , fromBackEdge , origdelta , reason ) and
1169
1172
b instanceof SemZeroBound and
1170
1173
delta = D:: fromFloat ( D:: toFloat ( d ) * D:: toFloat ( factor ) )
1171
1174
)
1172
1175
or
1173
1176
exists ( Sem:: Expr mid , D:: Delta factor , D:: Delta d |
1174
1177
boundFlowStepDiv ( e , mid , factor ) and
1175
- not e instanceof Sem:: ConstantIntegerExpr and
1176
1178
bounded ( mid , b , d , upper , fromBackEdge , origdelta , reason ) and
1177
1179
b instanceof SemZeroBound and
1178
1180
D:: toFloat ( d ) >= 0 and
0 commit comments