- How to run the virtual machine. 1. Download the virtual machine archive (vm.zip) 2. Extract it. A new directory, pldi-vm, is created. 3. Enter the pldi-vm directory. 4. If you are using VMWare, then you can directly use debian-7.0.0-i386-minimal.vmx Otherwise (e.g. VirtualBox), create a new PAE-enabled virtual machine and use debian-7.0.0-i386-minimal.vmdk as the initial disk. 5. Login: pldi 6. Password: pldi NOTE: If you are using VirtualBox and if you want to connect to the VM through the network, then you may have to configure the network device as Host-Only network (Machine > Settings > Network > Adapter 1 > Attached to > Host-only adapter). You may need to first add a host-only adapter from the host side (File > Preferences > Network > Host-only Networks > Add). - Quick Start! Go in the tests directory, it contains a small C file which you can compile with our quantitative compiler. The compiler will generate a '.bnd' file which contains automatically derived bounds for all the functions in the file! It also produces a '.s' assembly file which is the x86 compiled code. To compile, do: $ make You can run the test program and observe its output: $ ./t0 $ echo $? Check out the bounds in 't0.bnd'. $ cat t0.bnd If you want to see what stack space the program actually consumes on the real machine, use our 'stackmon' program: $ stackmon ./t0 And see that our tool is sound! The 'stackmon' program can monitor one specific function of your C program, just use the -f option: $ stackmon -f g ./t0 - The Good Old CompCert Still Works (and is now aware that the x86 stack is finite!) In the above example, the C file is compiled with 'qccomp' which derives bounds automatically for simple code. In case you have more complex code with recursive functions you will have to do proofs by hand but you can still compile it using the Quantitative CompCert without automatic bound derivation. To invoke the regular stack aware CompCert: $ ccomp - More details! We have the complete development available in the veristack directory. It features a very detailed README file which we recommend you to read in details. It also includes most of the examples described in the PLDI 2014 paper. Take note that everything is already compiled! - In case you lost it in history Here is the motd. * --- Welcome, reviewers --- * * This virtual machine contains a working Debian system * with both Coq and OCaml installed. The most convenient * way to play with this plateform is to connect to the VM * using ssh. Direct usage is of course possible. * * Run 'ip addr show dev eth0', to get the IP address of * the VM. Connect to it (on your local computer) with * 'ssh pldi@IPADDR'. * * When you are ready, read the INSTRUCTIONS file. * * If you need it (you should not), the root password * is 'p'.