Skip to content

Commit 4e6707f

Browse files
MathiasVPMathiasVP
committed
Fix joins.
Before: ``` Pipeline standard for boundedSsa#8#ffffffff@d4d576wg was evaluated in 651 iterations totaling 39789ms (delta sizes total: 235714). 3482 ~0% {8} r1 = JOIN unequalIntegralSsa#5#fffff#prev_delta WITH boundedSsa#8#ffffffff#prev ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.4, Rhs.4, Rhs.5, Rhs.6 1747 ~0% {8} r2 = SELECT r1 ON In.5 = false 1747 ~3% {8} r3 = SCAN r2 OUTPUT In.0, In.1, In.2, (In.3 + i2f(1)), false, In.6, In.7, In.4 1735 ~4% {8} r4 = SELECT r1 ON In.5 = true 1735 ~6% {8} r5 = SCAN r4 OUTPUT In.0, In.1, In.2, (In.3 - i2f(1)), true, In.6, In.7, In.4 1843 ~97% {8} r6 = JOIN unequalIntegralSsa#5#fffff#prev WITH boundedSsa#8#ffffffff#prev_delta ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.4, Rhs.4, Rhs.5, Rhs.6 907 ~99% {8} r7 = SELECT r6 ON In.5 = false 907 ~108% {8} r8 = SCAN r7 OUTPUT In.0, In.1, In.2, (In.3 + i2f(1)), false, In.6, In.7, In.4 2642 ~41% {8} r9 = r5 UNION r8 4389 ~22% {8} r10 = r3 UNION r9 936 ~99% {8} r11 = SELECT r6 ON In.5 = true 936 ~100% {8} r12 = SCAN r11 OUTPUT In.0, In.1, In.2, (In.3 - i2f(1)), true, In.6, In.7, In.4 512745 ~2% {6} r13 = SCAN bounded#7#fffffff#prev_delta OUTPUT In.0, In.3, In.1, In.2, In.4, In.5 229218 ~0% {9} r14 = JOIN r13 WITH boundFlowStepSsa#6#ffffff_240135#join_rhs ON FIRST 2 OUTPUT Rhs.5, Rhs.2, Rhs.3, Lhs.2, Rhs.4, Lhs.3, Lhs.1, Lhs.4, Lhs.5 229218 ~0% {8} r15 = SCAN r14 OUTPUT In.0, In.1, In.2, In.3, (In.4 + In.5), In.6, In.7, In.8 {8} r16 = r15 AND NOT num#TSemNoReason#f(Lhs.0) 5397 ~0% {8} r17 = SCAN r16 OUTPUT In.1, In.2, In.3, In.4, In.5, In.6, In.7, In.0 557965 ~0% {5} r18 = SCAN unequalIntegralSsa#5#fffff#prev_delta OUTPUT In.0, In.2, In.3, In.1, In.4 0 ~0% {8} r19 = JOIN r18 WITH boundedPhi#7#fffffff#prev ON FIRST 3 OUTPUT Lhs.0, Lhs.3, Lhs.1, Lhs.2, Lhs.4, Rhs.3, Rhs.4, Rhs.5 0 ~0% {8} r20 = SELECT r19 ON In.5 = false 0 ~0% {8} r21 = SCAN r20 OUTPUT In.0, In.1, In.2, (In.3 + i2f(1)), false, In.6, In.7, In.4 5397 ~0% {8} r22 = r17 UNION r21 6333 ~12% {8} r23 = r12 UNION r22 10722 ~16% {8} r24 = r10 UNION r23 0 ~0% {8} r25 = SELECT r19 ON In.5 = true 0 ~0% {8} r26 = SCAN r25 OUTPUT In.0, In.1, In.2, (In.3 - i2f(1)), true, In.6, In.7, In.4 362119282 ~1% {5} r27 = SCAN unequalIntegralSsa#5#fffff#prev OUTPUT In.0, In.2, In.3, In.1, In.4 41 ~8% {8} r28 = JOIN r27 WITH boundedPhi#7#fffffff#prev_delta ON FIRST 3 OUTPUT Lhs.0, Lhs.3, Lhs.1, Lhs.2, Lhs.4, Rhs.3, Rhs.4, Rhs.5 27 ~0% {8} r29 = SELECT r28 ON In.5 = false 27 ~4% {8} r30 = SCAN r29 OUTPUT In.0, In.1, In.2, (In.3 + i2f(1)), false, In.6, In.7, In.4 14 ~42% {8} r31 = SELECT r28 ON In.5 = true 14 ~42% {8} r32 = SCAN r31 OUTPUT In.0, In.1, In.2, (In.3 - i2f(1)), true, In.6, In.7, In.4 41 ~12% {8} r33 = r30 UNION r32 41 ~12% {8} r34 = r26 UNION r33 512745 ~0% {7} r35 = SCAN bounded#7#fffffff#prev_delta OUTPUT In.0, In.3, In.1, In.2, In.4, In.5, In.6 229272 ~0% {10} r36 = JOIN r35 WITH boundFlowStepSsa#6#ffffff_240135#join_rhs ON FIRST 2 OUTPUT Rhs.5, Lhs.2, Lhs.1, Lhs.4, Lhs.5, Lhs.6, Rhs.2, Rhs.3, Rhs.4, Lhs.3 229272 ~0% {9} r37 = SCAN r36 OUTPUT In.0, In.1, In.2, In.3, In.4, In.5, In.6, In.7, (In.8 + In.9) 223867 ~0% {8} r38 = JOIN r37 WITH num#TSemNoReason#f ON FIRST 1 OUTPUT Lhs.6, Lhs.7, Lhs.1, Lhs.8, Lhs.2, Lhs.3, Lhs.4, Lhs.5 3482 ~1% {8} r39 = JOIN unequalIntegralSsa#5#fffff#prev_delta WITH boundedSsa#8#ffffffff#prev ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Rhs.4, Rhs.5, Rhs.6, Rhs.7 1747 ~0% {8} r40 = SELECT r39 ON In.4 = false 1747 ~0% {8} r41 = SCAN r40 OUTPUT In.7, In.0, In.1, In.2, (In.3 + i2f(1)), false, In.5, In.6 1735 ~0% {8} r42 = SELECT r39 ON In.4 = true 1735 ~0% {8} r43 = SCAN r42 OUTPUT In.7, In.0, In.1, In.2, (In.3 - i2f(1)), true, In.5, In.6 3482 ~0% {8} r44 = r41 UNION r43 557965 ~0% {4} r45 = SCAN unequalIntegralSsa#5#fffff#prev_delta OUTPUT In.0, In.2, In.3, In.1 0 ~0% {8} r46 = JOIN r45 WITH boundedPhi#7#fffffff#prev ON FIRST 3 OUTPUT Lhs.0, Lhs.3, Lhs.1, Lhs.2, Rhs.3, Rhs.4, Rhs.5, Rhs.6 0 ~0% {8} r47 = SELECT r46 ON In.4 = false 0 ~0% {8} r48 = SCAN r47 OUTPUT In.7, In.0, In.1, In.2, (In.3 + i2f(1)), false, In.5, In.6 0 ~0% {8} r49 = SELECT r46 ON In.4 = true 0 ~0% {8} r50 = SCAN r49 OUTPUT In.7, In.0, In.1, In.2, (In.3 - i2f(1)), true, In.5, In.6 0 ~0% {8} r51 = r48 UNION r50 3482 ~0% {8} r52 = r44 UNION r51 {8} r53 = r52 AND NOT num#TSemNoReason#f(Lhs.0) 20 ~0% {8} r54 = SCAN r53 OUTPUT In.1, In.2, In.3, In.4, In.5, In.6, In.7, In.0 1843 ~0% {8} r55 = JOIN unequalIntegralSsa#5#fffff#prev WITH boundedSsa#8#ffffffff#prev_delta ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Rhs.4, Rhs.5, Rhs.6, Rhs.7 907 ~0% {8} r56 = SELECT r55 ON In.4 = false 907 ~1% {8} r57 = SCAN r56 OUTPUT In.7, In.0, In.1, In.2, (In.3 + i2f(1)), false, In.5, In.6 936 ~0% {8} r58 = SELECT r55 ON In.4 = true 936 ~1% {8} r59 = SCAN r58 OUTPUT In.7, In.0, In.1, In.2, (In.3 - i2f(1)), true, In.5, In.6 1843 ~3% {8} r60 = r57 UNION r59 362119282 ~0% {4} r61 = SCAN unequalIntegralSsa#5#fffff#prev OUTPUT In.0, In.2, In.3, In.1 41 ~0% {8} r62 = JOIN r61 WITH boundedPhi#7#fffffff#prev_delta ON FIRST 3 OUTPUT Lhs.0, Lhs.3, Lhs.1, Lhs.2, Rhs.3, Rhs.4, Rhs.5, Rhs.6 27 ~0% {8} r63 = SELECT r62 ON In.4 = false 27 ~0% {8} r64 = SCAN r63 OUTPUT In.7, In.0, In.1, In.2, (In.3 + i2f(1)), false, In.5, In.6 14 ~0% {8} r65 = SELECT r62 ON In.4 = true 14 ~0% {8} r66 = SCAN r65 OUTPUT In.7, In.0, In.1, In.2, (In.3 - i2f(1)), true, In.5, In.6 41 ~0% {8} r67 = r64 UNION r66 1884 ~3% {8} r68 = r60 UNION r67 {8} r69 = r68 AND NOT num#TSemNoReason#f(Lhs.0) 1853 ~0% {8} r70 = SCAN r69 OUTPUT In.1, In.2, In.3, In.4, In.5, In.6, In.7, In.0 1873 ~0% {8} r71 = r54 UNION r70 225740 ~0% {8} r72 = r38 UNION r71 225781 ~0% {8} r73 = r34 UNION r72 236503 ~2% {8} r74 = r24 UNION r73 235722 ~1% {8} r75 = r74 AND NOT boundedSsa#8#ffffffff#prev(Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.4, Lhs.5, Lhs.6, Lhs.7) return r75 ``` After: ``` Pipeline standard for boundedSsa#8#ffffffff@2122e6w8 was evaluated in 651 iterations totaling 343ms (delta sizes total: 235815). 0 ~0% {8} r1 = JOIN unequalIntegralSsa#5#fffff#prev_delta WITH boundedPhi#7#fffffff#prev ON FIRST 3 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.4, Rhs.3, Rhs.4, Rhs.5 0 ~0% {8} r2 = SELECT r1 ON In.5 = false 0 ~0% {8} r3 = SCAN r2 OUTPUT In.0, In.1, (In.2 + i2f(1)), In.3, false, In.6, In.7, In.4 0 ~0% {8} r4 = SELECT r1 ON In.5 = true 0 ~0% {8} r5 = SCAN r4 OUTPUT In.0, In.1, (In.2 - i2f(1)), In.3, true, In.6, In.7, In.4 41 ~8% {8} r6 = JOIN unequalIntegralSsa#5#fffff#prev WITH boundedPhi#7#fffffff#prev_delta ON FIRST 3 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.4, Rhs.3, Rhs.4, Rhs.5 27 ~0% {8} r7 = SELECT r6 ON In.5 = false 27 ~0% {8} r8 = SCAN r7 OUTPUT In.0, In.1, (In.2 + i2f(1)), In.3, false, In.6, In.7, In.4 27 ~0% {8} r9 = r5 UNION r8 27 ~0% {8} r10 = r3 UNION r9 14 ~42% {8} r11 = SELECT r6 ON In.5 = true 14 ~42% {8} r12 = SCAN r11 OUTPUT In.0, In.1, (In.2 - i2f(1)), In.3, true, In.6, In.7, In.4 3482 ~0% {8} r13 = JOIN unequalIntegralSsa#5#fffff#prev_delta WITH boundedSsa#8#ffffffff#prev ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.4, Rhs.4, Rhs.5, Rhs.6 1747 ~0% {8} r14 = SELECT r13 ON In.5 = false 1747 ~3% {8} r15 = SCAN r14 OUTPUT In.0, In.1, (In.2 + i2f(1)), In.3, false, In.6, In.7, In.4 1735 ~3% {8} r16 = SELECT r13 ON In.5 = true 1735 ~3% {8} r17 = SCAN r16 OUTPUT In.0, In.1, (In.2 - i2f(1)), In.3, true, In.6, In.7, In.4 3482 ~0% {8} r18 = r15 UNION r17 3496 ~0% {8} r19 = r12 UNION r18 3523 ~0% {8} r20 = r10 UNION r19 1843 ~103% {8} r21 = JOIN unequalIntegralSsa#5#fffff#prev WITH boundedSsa#8#ffffffff#prev_delta ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.4, Rhs.4, Rhs.5, Rhs.6 907 ~105% {8} r22 = SELECT r21 ON In.5 = false 907 ~108% {8} r23 = SCAN r22 OUTPUT In.0, In.1, (In.2 + i2f(1)), In.3, false, In.6, In.7, In.4 936 ~101% {8} r24 = SELECT r21 ON In.5 = true 936 ~109% {8} r25 = SCAN r24 OUTPUT In.0, In.1, (In.2 - i2f(1)), In.3, true, In.6, In.7, In.4 512745 ~4% {6} r26 = SCAN bounded#7#fffffff#prev_delta OUTPUT In.0, In.3, In.1, In.2, In.4, In.5 229313 ~0% {9} r27 = JOIN r26 WITH boundFlowStepSsa#6#ffffff_240135#join_rhs ON FIRST 2 OUTPUT Rhs.5, Rhs.2, Lhs.2, Rhs.4, Lhs.3, Rhs.3, Lhs.1, Lhs.4, Lhs.5 229313 ~0% {8} r28 = SCAN r27 OUTPUT In.0, In.1, In.2, (In.3 + In.4), In.5, In.6, In.7, In.8 {8} r29 = r28 AND NOT num#TSemNoReason#f(Lhs.0) 5492 ~2% {8} r30 = SCAN r29 OUTPUT In.1, In.2, In.3, In.4, In.5, In.6, In.7, In.0 6428 ~15% {8} r31 = r25 UNION r30 7335 ~27% {8} r32 = r23 UNION r31 512745 ~0% {7} r33 = SCAN bounded#7#fffffff#prev_delta OUTPUT In.0, In.3, In.1, In.2, In.4, In.5, In.6 229367 ~0% {10} r34 = JOIN r33 WITH boundFlowStepSsa#6#ffffff_240135#join_rhs ON FIRST 2 OUTPUT Rhs.5, Lhs.2, Lhs.1, Lhs.4, Lhs.5, Lhs.6, Rhs.2, Rhs.3, Rhs.4, Lhs.3 229367 ~0% {9} r35 = SCAN r34 OUTPUT In.0, In.1, In.2, In.3, In.4, In.5, In.6, In.7, (In.8 + In.9) 223867 ~0% {8} r36 = JOIN r35 WITH num#TSemNoReason#f ON FIRST 1 OUTPUT Lhs.6, Lhs.1, Lhs.8, Lhs.7, Lhs.2, Lhs.3, Lhs.4, Lhs.5 0 ~0% {8} r37 = JOIN unequalIntegralSsa#5#fffff#prev_delta WITH boundedPhi#7#fffffff#prev ON FIRST 3 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Rhs.3, Rhs.4, Rhs.5, Rhs.6 0 ~0% {8} r38 = SELECT r37 ON In.4 = false 0 ~0% {8} r39 = SCAN r38 OUTPUT In.7, In.0, In.1, (In.2 + i2f(1)), In.3, false, In.5, In.6 0 ~0% {8} r40 = SELECT r37 ON In.4 = true 0 ~0% {8} r41 = SCAN r40 OUTPUT In.7, In.0, In.1, (In.2 - i2f(1)), In.3, true, In.5, In.6 0 ~0% {8} r42 = r39 UNION r41 3482 ~0% {8} r43 = JOIN unequalIntegralSsa#5#fffff#prev_delta WITH boundedSsa#8#ffffffff#prev ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Rhs.4, Rhs.5, Rhs.6, Rhs.7 1747 ~0% {8} r44 = SELECT r43 ON In.4 = false 1747 ~0% {8} r45 = SCAN r44 OUTPUT In.7, In.0, In.1, (In.2 + i2f(1)), In.3, false, In.5, In.6 1735 ~1% {8} r46 = SELECT r43 ON In.4 = true 1735 ~2% {8} r47 = SCAN r46 OUTPUT In.7, In.0, In.1, (In.2 - i2f(1)), In.3, true, In.5, In.6 3482 ~2% {8} r48 = r45 UNION r47 3482 ~2% {8} r49 = r42 UNION r48 {8} r50 = r49 AND NOT num#TSemNoReason#f(Lhs.0) 20 ~0% {8} r51 = SCAN r50 OUTPUT In.1, In.2, In.3, In.4, In.5, In.6, In.7, In.0 41 ~2% {8} r52 = JOIN unequalIntegralSsa#5#fffff#prev WITH boundedPhi#7#fffffff#prev_delta ON FIRST 3 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Rhs.3, Rhs.4, Rhs.5, Rhs.6 27 ~0% {8} r53 = SELECT r52 ON In.4 = false 27 ~0% {8} r54 = SCAN r53 OUTPUT In.7, In.0, In.1, (In.2 + i2f(1)), In.3, false, In.5, In.6 14 ~0% {8} r55 = SELECT r52 ON In.4 = true 14 ~0% {8} r56 = SCAN r55 OUTPUT In.7, In.0, In.1, (In.2 - i2f(1)), In.3, true, In.5, In.6 41 ~0% {8} r57 = r54 UNION r56 1843 ~1% {8} r58 = JOIN unequalIntegralSsa#5#fffff#prev WITH boundedSsa#8#ffffffff#prev_delta ON FIRST 4 OUTPUT Lhs.0, Lhs.1, Lhs.2, Lhs.3, Rhs.4, Rhs.5, Rhs.6, Rhs.7 907 ~0% {8} r59 = SELECT r58 ON In.4 = false 907 ~1% {8} r60 = SCAN r59 OUTPUT In.7, In.0, In.1, (In.2 + i2f(1)), In.3, false, In.5, In.6 936 ~0% {8} r61 = SELECT r58 ON In.4 = true 936 ~0% {8} r62 = SCAN r61 OUTPUT In.7, In.0, In.1, (In.2 - i2f(1)), In.3, true, In.5, In.6 1843 ~0% {8} r63 = r60 UNION r62 1884 ~0% {8} r64 = r57 UNION r63 {8} r65 = r64 AND NOT num#TSemNoReason#f(Lhs.0) 1853 ~1% {8} r66 = SCAN r65 OUTPUT In.1, In.2, In.3, In.4, In.5, In.6, In.7, In.0 1873 ~1% {8} r67 = r51 UNION r66 225740 ~0% {8} r68 = r36 UNION r67 233075 ~0% {8} r69 = r32 UNION r68 236598 ~0% {8} r70 = r20 UNION r69 235817 ~0% {8} r71 = r70 AND NOT boundedSsa#8#ffffffff#prev(Lhs.0, Lhs.1, Lhs.2, Lhs.3, Lhs.4, Lhs.5, Lhs.6, Lhs.7) return r71 ```
1 parent 123e587 commit 4e6707f

File tree

1 file changed

+10
-7
lines changed

1 file changed

+10
-7
lines changed

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -660,7 +660,7 @@ module RangeStage<
660660
* - `upper = false` : `v >= b + delta`
661661
*/
662662
private predicate boundedSsa(
663-
SemSsaVariable v, SemSsaReadPosition pos, SemBound b, D::Delta delta, boolean upper,
663+
SemSsaVariable v, SemBound b, D::Delta delta, SemSsaReadPosition pos, boolean upper,
664664
boolean fromBackEdge, D::Delta origdelta, SemReason reason
665665
) {
666666
exists(SemExpr mid, D::Delta d1, D::Delta d2, SemReason r1, SemReason r2 |
@@ -673,10 +673,13 @@ module RangeStage<
673673
)
674674
or
675675
exists(D::Delta d, SemReason r1, SemReason r2 |
676-
boundedSsa(v, pos, b, d, upper, fromBackEdge, origdelta, r2) or
677-
boundedPhi(v, b, d, upper, fromBackEdge, origdelta, r2)
676+
boundedSsa(pragma[only_bind_into](v), pragma[only_bind_into](b), pragma[only_bind_into](d),
677+
pragma[only_bind_into](pos), upper, fromBackEdge, origdelta, r2)
678+
or
679+
boundedPhi(pragma[only_bind_into](v), pragma[only_bind_into](b), pragma[only_bind_into](d),
680+
upper, fromBackEdge, origdelta, r2)
678681
|
679-
unequalIntegralSsa(v, pos, b, d, r1) and
682+
unequalIntegralSsa(v, b, d, pos, r1) and
680683
(
681684
upper = true and delta = D::fromFloat(D::toFloat(d) - 1)
682685
or
@@ -694,7 +697,7 @@ module RangeStage<
694697
* Holds if `v != b + delta` at `pos` and `v` is of integral type.
695698
*/
696699
private predicate unequalIntegralSsa(
697-
SemSsaVariable v, SemSsaReadPosition pos, SemBound b, D::Delta delta, SemReason reason
700+
SemSsaVariable v, SemBound b, D::Delta delta, SemSsaReadPosition pos, SemReason reason
698701
) {
699702
exists(SemExpr e, D::Delta d1, D::Delta d2 |
700703
unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
@@ -746,7 +749,7 @@ module RangeStage<
746749
) {
747750
edge.phiInput(phi, inp) and
748751
exists(D::Delta d, boolean fromBackEdge0 |
749-
boundedSsa(inp, edge, b, d, upper, fromBackEdge0, origdelta, reason)
752+
boundedSsa(inp, b, d, edge, upper, fromBackEdge0, origdelta, reason)
750753
or
751754
boundedPhi(inp, b, d, upper, fromBackEdge0, origdelta, reason)
752755
or
@@ -1022,7 +1025,7 @@ module RangeStage<
10221025
reason = TSemNoReason()
10231026
or
10241027
exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
1025-
boundedSsa(v, bb, b, delta, upper, fromBackEdge, origdelta, reason) and
1028+
boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and
10261029
e = v.getAUse() and
10271030
bb.getBlock() = e.getBasicBlock()
10281031
)

0 commit comments

Comments
 (0)