@@ -1144,6 +1144,17 @@ private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
11441144 if guardLB > defLB then result = guardLB else result = defLB
11451145 )
11461146 or
1147+ exists ( VariableAccess access , float neConstant , float lower |
1148+ isNEPhi ( v , phi , access , neConstant ) and
1149+ lower = getFullyConvertedLowerBounds ( access ) and
1150+ if lower = neConstant then result = lower + 1 else result = lower
1151+ )
1152+ or
1153+ exists ( VariableAccess access |
1154+ isUnsupportedGuardPhi ( v , phi , access ) and
1155+ result = getFullyConvertedLowerBounds ( access )
1156+ )
1157+ or
11471158 result = getDefLowerBounds ( phi .getAPhiInput ( v ) , v )
11481159}
11491160
@@ -1161,6 +1172,17 @@ private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
11611172 if guardUB < defUB then result = guardUB else result = defUB
11621173 )
11631174 or
1175+ exists ( VariableAccess access , float neConstant , float upper |
1176+ isNEPhi ( v , phi , access , neConstant ) and
1177+ upper = getFullyConvertedUpperBounds ( access ) and
1178+ if upper = neConstant then result = upper - 1 else result = upper
1179+ )
1180+ or
1181+ exists ( VariableAccess access |
1182+ isUnsupportedGuardPhi ( v , phi , access ) and
1183+ result = getFullyConvertedUpperBounds ( access )
1184+ )
1185+ or
11641186 result = getDefUpperBounds ( phi .getAPhiInput ( v ) , v )
11651187}
11661188
@@ -1423,22 +1445,13 @@ private predicate linearBoundFromGuard(
14231445 // 1. x <= upperbound(RHS)
14241446 // 2. x >= lowerbound(RHS)
14251447 //
1426- // For x != RHS, we create trivial bounds:
1427- //
1428- // 1. x <= typeUpperBound(RHS.getUnspecifiedType())
1429- // 2. x >= typeLowerBound(RHS.getUnspecifiedType())
1430- //
1431- exists ( Expr lhs , Expr rhs , boolean isEQ |
1448+ exists ( Expr lhs , Expr rhs |
14321449 linearAccess ( lhs , v , p , q ) and
1433- eqOpWithSwapAndNegate ( guard , lhs , rhs , isEQ , branch ) and
1450+ eqOpWithSwapAndNegate ( guard , lhs , rhs , true , branch ) and
1451+ getBounds ( rhs , boundValue , isLowerBound ) and
14341452 strictness = Nonstrict ( )
1435- |
1436- // True branch
1437- isEQ = true and getBounds ( rhs , boundValue , isLowerBound )
1438- or
1439- // False branch: set the bounds to the min/max for the type.
1440- isEQ = false and exprTypeBounds ( rhs , boundValue , isLowerBound )
14411453 )
1454+ // x != RHS and !x are handled elsewhere
14421455}
14431456
14441457/** Utility for `linearBoundFromGuard`. */
@@ -1455,6 +1468,42 @@ private predicate exprTypeBounds(Expr expr, float boundValue, boolean isLowerBou
14551468 isLowerBound = false and boundValue = exprMaxVal ( expr .getFullyConverted ( ) )
14561469}
14571470
1471+ /**
1472+ * Holds if `(v, phi)` ensures that `access` is not equal to `neConstant`. For
1473+ * example, the condition `if (x + 1 != 3)` ensures that `x` is not equal to 2.
1474+ * Only integral types are supported.
1475+ */
1476+ private predicate isNEPhi (
1477+ Variable v , RangeSsaDefinition phi , VariableAccess access , float neConstant
1478+ ) {
1479+ exists (
1480+ ComparisonOperation cmp , boolean branch , Expr linearExpr , Expr rExpr , float p , float q , float r
1481+ |
1482+ access .getTarget ( ) = v and
1483+ phi .isGuardPhi ( access , cmp , branch ) and
1484+ eqOpWithSwapAndNegate ( cmp , linearExpr , rExpr , false , branch ) and
1485+ v .getUnspecifiedType ( ) instanceof IntegralOrEnumType and // Float `!=` is too imprecise
1486+ r = getValue ( rExpr ) .toFloat ( ) and
1487+ linearAccess ( linearExpr , access , p , q ) and
1488+ neConstant = ( r - q ) / p
1489+ )
1490+ }
1491+
1492+ /**
1493+ * Holds if `(v, phi)` constrains the value of `access` but in a way that
1494+ * doesn't allow this library to constrain the upper or lower bounds of
1495+ * `access`. An example is `if (x != y)` if neither `x` nor `y` is a
1496+ * compile-time constant.
1497+ */
1498+ private predicate isUnsupportedGuardPhi ( Variable v , RangeSsaDefinition phi , VariableAccess access ) {
1499+ exists ( ComparisonOperation cmp , boolean branch |
1500+ access .getTarget ( ) = v and
1501+ phi .isGuardPhi ( access , cmp , branch ) and
1502+ eqOpWithSwapAndNegate ( cmp , _, _, false , branch ) and
1503+ not isNEPhi ( v , phi , access , _)
1504+ )
1505+ }
1506+
14581507cached
14591508private module SimpleRangeAnalysisCached {
14601509 /**
0 commit comments