@@ -322,6 +322,8 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
322322 * actually references but whose values can be tracked as the type contained in the box.
323323 */
324324 Sem:: Type getAlternateTypeForSsaVariable ( Sem:: SsaVariable var ) ;
325+
326+ default predicate javaCompatibility ( ) { none ( ) }
325327}
326328
327329signature module UtilSig< Semantic Sem, DeltaSig DeltaParam> {
@@ -736,6 +738,16 @@ module RangeStage<
736738 )
737739 }
738740
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+
739751 /**
740752 * Holds if `e1 + delta` is a valid bound for `e2`.
741753 * - `upper = true` : `e2 <= e1 + delta`
@@ -749,6 +761,28 @@ module RangeStage<
749761 delta = D:: fromInt ( 0 ) and
750762 ( upper = true or upper = false )
751763 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
752786 e2 .( Sem:: RemExpr ) .getRightOperand ( ) = e1 and
753787 semPositive ( e1 ) and
754788 delta = D:: fromInt ( - 1 ) and
@@ -1254,6 +1288,7 @@ module RangeStage<
12541288 upper = false and delta = D:: fromFloat ( D:: toFloat ( d1 ) .minimum ( D:: toFloat ( d2 ) ) )
12551289 )
12561290 or
1291+ not javaCompatibility ( ) and
12571292 exists ( Sem:: Expr mid , D:: Delta d , float f |
12581293 e .( Sem:: NegateExpr ) .getOperand ( ) = mid and
12591294 b instanceof SemZeroBound and
@@ -1277,6 +1312,7 @@ module RangeStage<
12771312 b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
12781313 )
12791314 or
1315+ not javaCompatibility ( ) and
12801316 exists ( D:: Delta dLeft , D:: Delta dRight , boolean fbeLeft , boolean fbeRight |
12811317 boundedSubOperandLeft ( e , upper , b , dLeft , fbeLeft , origdelta , reason ) and
12821318 boundedSubOperandRight ( e , upper , dRight , fbeRight ) and
@@ -1294,6 +1330,7 @@ module RangeStage<
12941330 fromBackEdge = fbeLeft .booleanOr ( fbeRight )
12951331 )
12961332 or
1333+ not javaCompatibility ( ) and
12971334 exists (
12981335 Sem:: RemExpr rem , D:: Delta d_max , D:: Delta d1 , D:: Delta d2 , boolean fbe1 , boolean fbe2 ,
12991336 D:: Delta od1 , D:: Delta od2 , SemReason r1 , SemReason r2
@@ -1318,6 +1355,7 @@ module RangeStage<
13181355 upper = false and delta = D:: fromFloat ( - D:: toFloat ( d_max ) .abs ( ) + 1 )
13191356 )
13201357 or
1358+ not javaCompatibility ( ) and
13211359 exists (
13221360 D:: Delta dLeft , D:: Delta dRight , boolean fbeLeft , boolean fbeRight , D:: Delta odLeft ,
13231361 D:: Delta odRight , SemReason rLeft , SemReason rRight
0 commit comments