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
```
This commit is contained in:
Mathias Vorreiter Pedersen
2023-08-24 10:29:04 +01:00
parent 123e58767b
commit 4e6707fee5

View File

@@ -660,7 +660,7 @@ module RangeStage<
* - `upper = false` : `v >= b + delta`
*/
private predicate boundedSsa(
SemSsaVariable v, SemSsaReadPosition pos, SemBound b, D::Delta delta, boolean upper,
SemSsaVariable v, SemBound b, D::Delta delta, SemSsaReadPosition pos, boolean upper,
boolean fromBackEdge, D::Delta origdelta, SemReason reason
) {
exists(SemExpr mid, D::Delta d1, D::Delta d2, SemReason r1, SemReason r2 |
@@ -673,10 +673,13 @@ module RangeStage<
)
or
exists(D::Delta d, SemReason r1, SemReason r2 |
boundedSsa(v, pos, b, d, upper, fromBackEdge, origdelta, r2) or
boundedPhi(v, b, d, upper, fromBackEdge, origdelta, r2)
boundedSsa(pragma[only_bind_into](v), pragma[only_bind_into](b), pragma[only_bind_into](d),
pragma[only_bind_into](pos), upper, fromBackEdge, origdelta, r2)
or
boundedPhi(pragma[only_bind_into](v), pragma[only_bind_into](b), pragma[only_bind_into](d),
upper, fromBackEdge, origdelta, r2)
|
unequalIntegralSsa(v, pos, b, d, r1) and
unequalIntegralSsa(v, b, d, pos, r1) and
(
upper = true and delta = D::fromFloat(D::toFloat(d) - 1)
or
@@ -694,7 +697,7 @@ module RangeStage<
* Holds if `v != b + delta` at `pos` and `v` is of integral type.
*/
private predicate unequalIntegralSsa(
SemSsaVariable v, SemSsaReadPosition pos, SemBound b, D::Delta delta, SemReason reason
SemSsaVariable v, SemBound b, D::Delta delta, SemSsaReadPosition pos, SemReason reason
) {
exists(SemExpr e, D::Delta d1, D::Delta d2 |
unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
@@ -746,7 +749,7 @@ module RangeStage<
) {
edge.phiInput(phi, inp) and
exists(D::Delta d, boolean fromBackEdge0 |
boundedSsa(inp, edge, b, d, upper, fromBackEdge0, origdelta, reason)
boundedSsa(inp, b, d, edge, upper, fromBackEdge0, origdelta, reason)
or
boundedPhi(inp, b, d, upper, fromBackEdge0, origdelta, reason)
or
@@ -1022,7 +1025,7 @@ module RangeStage<
reason = TSemNoReason()
or
exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
boundedSsa(v, bb, b, delta, upper, fromBackEdge, origdelta, reason) and
boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and
e = v.getAUse() and
bb.getBlock() = e.getBasicBlock()
)