Compiling Xen with CBMC: docker file "expensive regression test"

[polgreen]

Compilation of Xen with goto-cc currently fails, although at some point in the past it has worked. I would obviously like the compilation to work again (and for that separate issues are being filed), but I would also like some kind of "expensive" regression test to prevent this kind of degradation happening in future.

This PR adds scripts to create a docker container that compiles Xen with goto-cc. In effect, everything we need the regression test to do. I don't know how it would be best to have this set up as an actual regression test though.

To create the docker file, on a machine with docker installed, run the following script from the cbmc top directory

./make_xen_docker_container.sh

This creates a docker container based on the Dockerfile. The docker container runs the script "scrpts/docker_compile_xen.sh", which:

• adds the soft links required from goto-cc to goto-ld, goto-gcc and goto-diff
• downloads https://github.com/awslabs/one-line-scan.git
• downloads Xen
• attempts to compile Xen with goto-cc
• shows an error message, and paths to the build log if the compilation fails

[allredj]

Passed Diffblue compatibility checks (cbmc commit: 70a0fde).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77823134

[kroening]

Looks good -- may I suggest to move this from the root directory to regression/goto-cc-xen?
Then add a readme in that directory with the information that the comment above contains.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 8f842ec).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92262009

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 507766e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102261536

[tautschnig]

Calling everyone with opinions about testing and infrastructure: this PR now adds a new directory integration, with a first xen entry. The idea being that we can start building out integration tests. In theory, and if Docker is installed, cd integration/xen && make does the trick. Unfortunately I ran into some local technical issues so I couldn't fully run this on my box, hoping to get those resolved very soon. Meanwhile everyone is invited to take a look. (It's a very small PR, don't be scared!)

[smowton]

So it currently doesn't actually use cbmc but just goto-cc's Xen? Do you intend it to do some analysis or just serve as a stress test for goto-cc?

[tautschnig]

Do you intend it to do some analysis or just serve as a stress test for goto-cc?

We could of course add some analysis, but before doing so we might have to address issues such as function-pointer removal (#2620). I'd say:

1. Have the ability to reliably build Xen. That's pending some other PRs (goto-ld: handle EFI binaries gracefully #2557, Enable goto-cc to build and link Xen #1357).
2. Test that and experiment with analyses (which @polgreen has already done a lot).
3. Fix bugs found in 2).
4. Add 2) to the integration test.