Boogie's new testing infrastructure

Developer
May 11, 2014 at 5:22 PM
Hi All,

Boogie's new testing infrastructure (lit) is now in Boogie's default branch. I plan to remove the old testing infrastructure VERY soon but I'd like to give a little time for Boogie users to try out the new infrastructure and fix a few remaining issues.

I've written a little documentation on the new infrastructure. The new infrastructure is vastly superior to the old batch file infrastructure. Please try it out.

I've kept the old batch file testing scripts functioning (for now) so that it is possible to run either infrastructure on Windows. However both infrastructures use the same name (Output) for their temporary output which causes problems if you run one infrastructure and then try to run the other. To work around this please run the Tests\clean.py script before switching between the testing infrastructures. This issue will go away as soon as we kill the old testing infrastructure

The following tests currently fail for the lit testing infrastructure
Failing Tests (10):
    Boogie :: og/DeviceCacheSimplified.bpl
    Boogie :: og/DeviceCacheWithBuffer.bpl
    Boogie :: og/async.bpl
    Boogie :: og/houd1.bpl
    Boogie :: og/lock-introduced.bpl
    Boogie :: og/termination.bpl
    Boogie :: og/treiber-stack.bpl
    Boogie :: test15/CaptureState.bpl
    Boogie :: test21/Maps2.bpl
    Boogie :: test21/test3_AddMethod_conv.bpl
The test15/CaptureState.bpl does not fail on Windows using Z3 4.1 (http://research.microsoft.com/en-us/downloads/0a7db466-c2d7-4c51-8246-07e25900c7e7/). I tried using Z3 4.1.1 on Linux (https://github.com/delcypher/z3/tree/4.1.1-fixed) and it's still broken. I'm not convinced they are actually the same version because the reported version of the Z3 build on linux is 4.2 rather than 4.1 despite me taking this from the v4.1.1 git tag. Basically we need to agree on a common version of Z3 available to all users and fix this test.

All other tests listed above basically fail because someone left them in the repository but they were not being run in the old infrastructure! So I've left these tests partially implemented until we decide what to do with these.

There are also a bunch of test directories (AbsHoudini, doomed, z3api and test17) that are currently disabled because they were broken (as far as could tell) in the old infrastructure. lit is aware of these tests but I've instructed it to treat these directories as unsupported tests for now. If these tests are of no use they should be removed.
Developer
May 12, 2014 at 3:19 PM
It has been requested that I provide examples of OutputCheck style tests that are now supported in the new testing infrastructure. Here are two I just added.

https://boogie.codeplex.com/SourceControl/latest#Test/test0/Arrays1.bpl
https://boogie.codeplex.com/SourceControl/latest#Test/houdini/houd12.bpl

The OutputCheck style tests have the advantage that you write what you expect as comments near the relevant code (this is great for tool error messages) and also make the test stable to file name and line number changes. Unfortunately right now it not possible to specify that the CHECK directives can be in any order which might be necessary for some tests in the Boogie test suite. This could be implemented in the OutputCheck tool but right now I do not have time to do so, there is an issue open on this though.
Developer
May 27, 2014 at 8:08 PM
I believe the new infrastructure is now in a state where it can successfully replace the old infrastructure so I am going to make the switch tomorrow. I will be removing all of the old test infrastructure so if you don't want this to happen you need to object now!

There are a still a few niggling issues.
  • test15/CaptureState.bpl still fails for me under Linux because of Z3 differences. We need to move to a common version of Z3 that is available both on Linux/OSX and Windows.
  • Many tests have been marked as xfail because someone left them lying around in the test suite but they weren't being executed! I've marked them as xfail for now so they don't generate a warning when lit is executed but we should really decide what do with these test cases because they aren't useful in their current form.
  • Several test folders have been disabled because (e.g. AbsHoundini) because they were disabled in the old infrastructure. This needs fixing! I partially fixed up the AbsHoudini tests (modify Test/AbsHoudini/lit.local.cfg to allow lit to run the tests in this directory) but more work is needed and I don't know anything about Abstract Houdini so someone who actually does needs to fix this.
Developer
May 28, 2014 at 3:48 PM
Okay. The old testing infrastructure has been removed. I've left a few remnants of it in folders that were not converted to lit. There are still a few issues left to resolve (discussed in my previous post) but hopefully those can be fixed.

Have fun with a faster and more flexible testing infrastructure!