Skip to content

Commit b57243e

Browse files
authored
Merge pull request #20579 from aschackmull/shared/rangeanalysis-joinorder
Rangeanalysis: Fix a bad join-order in boundedPhiRankStep.
2 parents e65f8ea + 2e9e357 commit b57243e

File tree

1 file changed

+27
-29
lines changed

1 file changed

+27
-29
lines changed

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

Lines changed: 27 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -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

Comments
 (0)