@@ -322,6 +322,8 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
322
322
* actually references but whose values can be tracked as the type contained in the box.
323
323
*/
324
324
Sem:: Type getAlternateTypeForSsaVariable ( Sem:: SsaVariable var ) ;
325
+
326
+ default predicate javaCompatibility ( ) { none ( ) }
325
327
}
326
328
327
329
signature module UtilSig< Semantic Sem, DeltaSig DeltaParam> {
@@ -736,6 +738,16 @@ module RangeStage<
736
738
)
737
739
}
738
740
741
+ /** Holds if `e >= 1` as determined by sign analysis. */
742
+ private predicate strictlyPositiveIntegralExpr ( Sem:: Expr e ) {
743
+ semStrictlyPositive ( e ) and getTrackedType ( e ) instanceof Sem:: IntegerType
744
+ }
745
+
746
+ /** Holds if `e <= -1` as determined by sign analysis. */
747
+ private predicate strictlyNegativeIntegralExpr ( Sem:: Expr e ) {
748
+ semStrictlyNegative ( e ) and getTrackedType ( e ) instanceof Sem:: IntegerType
749
+ }
750
+
739
751
/**
740
752
* Holds if `e1 + delta` is a valid bound for `e2`.
741
753
* - `upper = true` : `e2 <= e1 + delta`
@@ -749,6 +761,28 @@ module RangeStage<
749
761
delta = D:: fromInt ( 0 ) and
750
762
( upper = true or upper = false )
751
763
or
764
+ javaCompatibility ( ) and
765
+ exists ( Sem:: Expr x , Sem:: SubExpr sub |
766
+ e2 = sub and
767
+ sub .getLeftOperand ( ) = e1 and
768
+ sub .getRightOperand ( ) = x
769
+ |
770
+ // `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
771
+ not x instanceof Sem:: ConstantIntegerExpr and
772
+ if strictlyPositiveIntegralExpr ( x )
773
+ then upper = true and delta = D:: fromInt ( - 1 )
774
+ else
775
+ if semPositive ( x )
776
+ then upper = true and delta = D:: fromInt ( 0 )
777
+ else
778
+ if strictlyNegativeIntegralExpr ( x )
779
+ then upper = false and delta = D:: fromInt ( 1 )
780
+ else
781
+ if semNegative ( x )
782
+ then upper = false and delta = D:: fromInt ( 0 )
783
+ else none ( )
784
+ )
785
+ or
752
786
e2 .( Sem:: RemExpr ) .getRightOperand ( ) = e1 and
753
787
semPositive ( e1 ) and
754
788
delta = D:: fromInt ( - 1 ) and
@@ -1254,6 +1288,7 @@ module RangeStage<
1254
1288
upper = false and delta = D:: fromFloat ( D:: toFloat ( d1 ) .minimum ( D:: toFloat ( d2 ) ) )
1255
1289
)
1256
1290
or
1291
+ not javaCompatibility ( ) and
1257
1292
exists ( Sem:: Expr mid , D:: Delta d , float f |
1258
1293
e .( Sem:: NegateExpr ) .getOperand ( ) = mid and
1259
1294
b instanceof SemZeroBound and
@@ -1277,6 +1312,7 @@ module RangeStage<
1277
1312
b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
1278
1313
)
1279
1314
or
1315
+ not javaCompatibility ( ) and
1280
1316
exists ( D:: Delta dLeft , D:: Delta dRight , boolean fbeLeft , boolean fbeRight |
1281
1317
boundedSubOperandLeft ( e , upper , b , dLeft , fbeLeft , origdelta , reason ) and
1282
1318
boundedSubOperandRight ( e , upper , dRight , fbeRight ) and
@@ -1294,6 +1330,7 @@ module RangeStage<
1294
1330
fromBackEdge = fbeLeft .booleanOr ( fbeRight )
1295
1331
)
1296
1332
or
1333
+ not javaCompatibility ( ) and
1297
1334
exists (
1298
1335
Sem:: RemExpr rem , D:: Delta d_max , D:: Delta d1 , D:: Delta d2 , boolean fbe1 , boolean fbe2 ,
1299
1336
D:: Delta od1 , D:: Delta od2 , SemReason r1 , SemReason r2
@@ -1318,6 +1355,7 @@ module RangeStage<
1318
1355
upper = false and delta = D:: fromFloat ( - D:: toFloat ( d_max ) .abs ( ) + 1 )
1319
1356
)
1320
1357
or
1358
+ not javaCompatibility ( ) and
1321
1359
exists (
1322
1360
D:: Delta dLeft , D:: Delta dRight , boolean fbeLeft , boolean fbeRight , D:: Delta odLeft ,
1323
1361
D:: Delta odRight , SemReason rLeft , SemReason rRight
0 commit comments