3 tests fail in test-relate?

[yilongli]

I run the regression tests out-of-the-box and get three failures from p-loop-unrollx2, p-loop-unrollx2-temp and p-sp-reorder. Are they supposed to pass? I am using z3 4.4.0. Thanks!

Complete test result:

Test                           Check Lns Sec ATP
------------------------------------------------
n-branch-fold                   PASS  18   0   1
n-branch-spec-copy-prop-01      PASS  35   1  14
n-branch-spec-copy-prop-02      PASS  36   0  11
n-branch-spec                   PASS  27   0  11
n-copy-prop-01                  PASS  20   0   1
n-cse-01                        PASS  25   0   1
n-diff                          PASS  13   0   1
n-loop-peel-01                  PASS  23   1  12
n-loop-peel-02                  PASS  23   0  12
n-loop-split-01                 PASS  26   0  18
n-loop-split-02                 PASS  28   1   3
n-loop-unswitch-01              PASS  31   0  36
n-loop-unswitch-02              PASS  31   0  20
n-loop-unswitch-03              PASS  31   1   2
n-soft-pipe-01                  PASS  24   0  17
n-soft-pipe-02                  PASS  24   0  12
n-soft-pipe-03                  PASS  30   2  17
n-soft-pipe-04                  PASS  31   0   1
n-soft-pipe-05                  PASS  30   0   1
n-trail-blaze-01                PASS  27   0   1
n-trail-blaze-02                PASS  27   0  12
p-assign-consts-swap            PASS  15   0   1
p-branch-fold                   PASS  17   0   3
p-branch-spec-copy-prop-01      PASS  34   1   9
p-branch-spec-copy-prop-02      PASS  35   0   9
p-branch-spec                   PASS  26   0  10
p-common-subexpr-elim-01        PASS  21   0   1
p-copy-prop-01                  PASS  19   0   1
p-cse-01                        PASS  22   0   1
p-cse-02                        PASS  19   0   1
p-loop-inv-lift                 PASS  21   0   8
p-loop-peel-01                  PASS  22   0  10
p-loop-peel-02                  PASS  21   0  10
p-loop-split                    PASS  28   1  16
p-loop-unroll-inf               PASS  17   0  10
p-loop-unrollx2                 FAIL  22   0  12
p-loop-unrollx2-temp            FAIL  21   1  17
p-loop-unswitch-01              PASS  29   1  36
p-loop-unswitch-02              PASS  30   0  36
p-nop                           PASS  11   0   1
p-same                          PASS  12   1   1
p-shift-loop-index              FAIL  20   0  10
p-soft-pipe-01                  PASS  23   0  10
p-soft-pipe-02                  PASS  29   0  10
p-soft-pipe-03                  PASS  29   1  10
p-sp-reorder                    FAIL  18   0   1
p-temp-intermediate             PASS  15   0   1
p-temp-lift                     PASS  18   0   1
p-temp                          PASS  14   0   1
p-trail-blaze                   PASS  27   0  10

[ztatlock]

It looks like there are 4 failed tests actually!

I'm not sure how long these have been failing. After the camera-ready 6 years ago we rewrote the tool, so it may be that we never got these working again before moving on to other things.

I'll try to find some time to dig into this more, but in the meantime, you can get Graphviz representations of the simulation relation by running pec directly.

  $ ./bin/pec test/relate/p-shift-loop-index.rwr
  $ dot -Tpng /tmp/pec-rwr.dot > i.png

Should produce something like:

Which is very useful for debugging. The logs also contain all the intermediate SMT queries.

Keep me posted and I'll try to help out as much as possible!

[yilongli]

Thanks for the advice! I am personally more interested in how they are supposed to work instead of why they aren't working. It's really helpful to see the simulation relation in graph.