@@ -923,17 +923,18 @@ module RangeStage<
923923 }
924924
925925 /**
926- * Holds if `b + delta` is a valid bound for `inp` when used as an input to
927- * `phi` along `edge `.
926+ * Holds if `b + delta` is a valid bound for the input `inp` to `phi` along
927+ * the edge with rank `rix `.
928928 * - `upper = true` : `inp <= b + delta`
929929 * - `upper = false` : `inp >= b + delta`
930930 */
931931 private predicate boundedPhiInp (
932- Sem:: SsaPhiNode phi , Sem :: SsaVariable inp , SsaReadPositionPhiInputEdge edge , SemBound b ,
933- D:: Delta delta , boolean upper , boolean fromBackEdge , D :: Delta origdelta , SemReason reason
932+ Sem:: SsaPhiNode phi , int rix , SemBound b , D :: Delta delta , boolean upper , boolean fromBackEdge ,
933+ D:: Delta origdelta , SemReason reason
934934 ) {
935- edge .phiInput ( phi , inp ) and
936- exists ( D:: Delta d , boolean fromBackEdge0 |
935+ exists (
936+ D:: Delta d , boolean fromBackEdge0 , Sem:: SsaVariable inp , SsaReadPositionPhiInputEdge edge
937+ |
937938 boundedSsa ( inp , b , d , edge , upper , fromBackEdge0 , origdelta , reason )
938939 or
939940 boundedPhi ( inp , b , d , upper , fromBackEdge0 , origdelta , reason )
@@ -945,6 +946,7 @@ module RangeStage<
945946 origdelta = D:: fromFloat ( 0 ) and
946947 reason = TSemNoReason ( )
947948 |
949+ rankedPhiInput ( phi , inp , edge , rix ) and
948950 if backEdge ( phi , inp , edge )
949951 then
950952 fromBackEdge = true and
@@ -963,33 +965,30 @@ module RangeStage<
963965 }
964966
965967 /**
966- * Holds if `b + delta` is a valid bound for `inp` when used as an input to
967- * `phi` along `edge `.
968+ * Holds if `b + delta` is a valid bound for the input `inp` to `phi` along
969+ * the edge with rank `rix `.
968970 * - `upper = true` : `inp <= b + delta`
969971 * - `upper = false` : `inp >= b + delta`
970972 *
971- * Equivalent to `boundedPhiInp(phi, inp, edge , b, delta, upper, _, _, _)`.
973+ * Equivalent to `boundedPhiInp(phi, rix , b, delta, upper, _, _, _)`.
972974 */
973975 pragma [ noinline]
974976 private predicate boundedPhiInp1 (
975- Sem:: SsaPhiNode phi , SemBound b , boolean upper , Sem:: SsaVariable inp ,
976- SsaReadPositionPhiInputEdge edge , D:: Delta delta
977+ Sem:: SsaPhiNode phi , SemBound b , boolean upper , int rix , D:: Delta delta
977978 ) {
978- boundedPhiInp ( phi , inp , edge , b , delta , upper , _, _, _)
979+ boundedPhiInp ( phi , rix , b , delta , upper , _, _, _)
979980 }
980981
981982 /**
982- * Holds if `phi` is a valid bound for `inp` when used as an input to `phi`
983- * along `edge `.
983+ * Holds if `phi` is a valid bound for the input `inp` to `phi` along the
984+ * edge with rank `rix `.
984985 * - `upper = true` : `inp <= phi`
985986 * - `upper = false` : `inp >= phi`
986987 */
987- private predicate selfBoundedPhiInp (
988- Sem:: SsaPhiNode phi , Sem:: SsaVariable inp , SsaReadPositionPhiInputEdge edge , boolean upper
989- ) {
988+ private predicate selfBoundedPhiInp ( Sem:: SsaPhiNode phi , int rix , boolean upper ) {
990989 exists ( D:: Delta d , SemSsaBound phibound |
991990 phibound .getVariable ( ) = phi and
992- boundedPhiInp ( phi , inp , edge , phibound , d , upper , _, _, _) and
991+ boundedPhiInp ( phi , rix , phibound , d , upper , _, _, _) and
993992 (
994993 upper = true and D:: toFloat ( d ) <= 0
995994 or
@@ -1009,33 +1008,34 @@ module RangeStage<
10091008 Sem:: SsaPhiNode phi , boolean upper , SemBound b , D:: Delta delta , boolean fromBackEdge ,
10101009 D:: Delta origdelta , SemReason reason
10111010 ) {
1012- boundedPhiInp ( phi , _, _ , b , delta , upper , fromBackEdge , origdelta , reason )
1011+ boundedPhiInp ( phi , _, b , delta , upper , fromBackEdge , origdelta , reason )
10131012 }
10141013
10151014 /**
10161015 * Holds if the candidate bound `b + delta` for `phi` is valid for the phi input
1017- * `inp` along ` edge`.
1016+ * along the edge with rank `rix `.
10181017 */
10191018 private predicate boundedPhiCandValidForEdge (
10201019 Sem:: SsaPhiNode phi , SemBound b , D:: Delta delta , boolean upper , boolean fromBackEdge ,
1021- D:: Delta origdelta , SemReason reason , Sem :: SsaVariable inp , SsaReadPositionPhiInputEdge edge
1020+ D:: Delta origdelta , SemReason reason , int rix
10221021 ) {
10231022 boundedPhiCand ( phi , upper , b , delta , fromBackEdge , origdelta , reason ) and
10241023 (
1025- exists ( D:: Delta d | boundedPhiInp1 ( phi , b , upper , inp , edge , d ) |
1024+ exists ( D:: Delta d | boundedPhiInp1 ( phi , b , upper , rix , d ) |
10261025 upper = true and D:: toFloat ( d ) <= D:: toFloat ( delta )
10271026 )
10281027 or
1029- exists ( D:: Delta d | boundedPhiInp1 ( phi , b , upper , inp , edge , d ) |
1028+ exists ( D:: Delta d | boundedPhiInp1 ( phi , b , upper , rix , d ) |
10301029 upper = false and D:: toFloat ( d ) >= D:: toFloat ( delta )
10311030 )
10321031 or
1033- selfBoundedPhiInp ( phi , inp , edge , upper )
1032+ selfBoundedPhiInp ( phi , rix , upper )
10341033 )
10351034 }
10361035
10371036 /**
1038- * Holds if `b + delta` is a valid bound for `phi`'s `rix`th input edge.
1037+ * Holds if `b + delta` is a valid bound for `phi` when accounting for the
1038+ * input edges ranked 1 through `rix`.
10391039 * - `upper = true` : `phi <= b + delta`
10401040 * - `upper = false` : `phi >= b + delta`
10411041 */
@@ -1044,10 +1044,8 @@ module RangeStage<
10441044 Sem:: SsaPhiNode phi , SemBound b , D:: Delta delta , boolean upper , boolean fromBackEdge ,
10451045 D:: Delta origdelta , SemReason reason , int rix
10461046 ) {
1047- exists ( Sem:: SsaVariable inp , SsaReadPositionPhiInputEdge edge |
1048- rankedPhiInput ( phi , inp , edge , rix ) and
1049- boundedPhiCandValidForEdge ( phi , b , delta , upper , fromBackEdge , origdelta , reason , inp , edge )
1050- |
1047+ boundedPhiCandValidForEdge ( phi , b , delta , upper , fromBackEdge , origdelta , reason , rix ) and
1048+ (
10511049 rix = 1
10521050 or
10531051 boundedPhiRankStep ( phi , b , delta , upper , fromBackEdge , origdelta , reason , rix - 1 )
0 commit comments