@@ -1011,6 +1011,27 @@ module RangeStage<
10111011 boundedPhiInp ( phi , _, b , delta , upper , fromBackEdge , origdelta , reason )
10121012 }
10131013
1014+ /**
1015+ * Holds if `inp <= delta` where `inp` is the input to `phi` along the edge
1016+ * with rank `rix`.
1017+ *
1018+ * Equivalent to `boundedPhiInp(phi, rix, any(SemZeroBound zb), delta, true, _, _, _)`.
1019+ */
1020+ private predicate zeroUpperBoundedPhiInp1 ( Sem:: SsaPhiNode phi , int rix , D:: Delta delta ) {
1021+ boundedPhiInp1 ( phi , any ( SemZeroBound zb ) , true , rix , delta )
1022+ }
1023+
1024+ /**
1025+ * Holds if `inp <= b + delta` for some input, `inp`, to `phi` and `b >= 0`.
1026+ */
1027+ private predicate upperBoundedPhiCand (
1028+ Sem:: SsaPhiNode phi , SemSsaBound b , D:: Delta delta , boolean fromBackEdge , D:: Delta origdelta ,
1029+ SemReason reason
1030+ ) {
1031+ boundedPhiCand ( phi , true , b , delta , fromBackEdge , origdelta , reason ) and
1032+ typeBound ( Sem:: getSsaType ( b .getVariable ( ) ) , any ( float f | f >= 0 ) , _)
1033+ }
1034+
10141035 /**
10151036 * Holds if the candidate bound `b + delta` for `phi` is valid for the phi input
10161037 * along the edge with rank `rix`.
@@ -1031,6 +1052,12 @@ module RangeStage<
10311052 or
10321053 selfBoundedPhiInp ( phi , rix , upper )
10331054 )
1055+ or
1056+ upperBoundedPhiCand ( phi , b , delta , fromBackEdge , origdelta , reason ) and
1057+ exists ( D:: Delta d1 | zeroUpperBoundedPhiInp1 ( phi , rix , d1 ) |
1058+ upper = true and
1059+ D:: toFloat ( d1 ) <= D:: toFloat ( delta )
1060+ )
10341061 }
10351062
10361063 /**
0 commit comments