POPL17-Artifact-Paper238

Artifact

We provide our artifact in the form of a virtual machine which can be downloaded here.

Paper #238
Fast Polyhedra Abstract Domain

Paper

System Requirements

  1. Make sure you have 64-bit VirtualBox from Oracle.
  2. The SeaHorn framework has a number of dependencies which require around 10GB of disk space. We recommended allocating at least 20GB of disk space to the virtual machine.
  3. The analysis with newpolka requires large amount of RAM memory (as reported in the paper). Allocate at least 10GB to the virtual machine for analyzing larger benchmarks.

Instructions

  1. Extract the virtual machine from the zip file and open in VirtualBox.
  2. The login credentials for the Virtual Machine are:
      username: POPL2017
      password: popl2017
  3. The source code for our library (optpoly) and newpolka can be found in "apron/optpoly" and "apron/newpolka" directories respectively.
  4. To install optpoly, go to "apron/optpoly" and type "make" and then "sudo make install".
  5. To install newpolka, go to "apron/newpolka" and type "make allRll" and then "sudo make install".
  6. The benchmarks used in the paper can be found in "POPLBenchmarks" directory. We also provide smaller benchmarks in "loops" directory for correctness testing.
  7. As the Virtual machine is already large, we did not include all benchmarks from SV-COMP. However, these benchmarks are publicly available here.

Correctness testing

  1. The analysis is intra-procedural and produces invariants in the form of polyhedra constraints for each basic block in the function. The variables correspond to llvm bitcode and thus they have unusual names in the invariants.
  2. As there is no canonical form for polyhedra, the invariants computed by optpoly may be syntactically different from those produced by newpolka, although they represent the same polyhedron (unless either newpolka or optpoly produces integer overflow). For example, {x-y=2, z-y=3} and {x-y=2, z-x=1} are syntactically different but represent the same polyhedra.
  3. Since the analysis with newpolka does not finish on most benchmarks reported in the paper, we provide smaller benchmarks in the "loops" directory. The script "verify.sh" in "scripts" directory runs the analysis with both optpoly and newpolka on these small benchmarks and collects results in "Verify/optpoly" and "Verify/newpolka" directories.
  4. The generated invariants are small and it is possible to manually compare them.
  5. In the case of integer overflow with either library, the corresponding file will contain "exception" string.

Reproducing results

  1. For reproducing results reported in the paper, run "measurement.sh" in "scripts" directory. It runs the analysis on all benchmarks with optpoly first and then with newpolka.
  2. The invariants are collected in "Results/optpoly" and "Results/newpolka" directories.
  3. Unix's "time" command is used to display memory consumption (as maximum resident set size) on the terminal. Note that it can also report the total time used by the process which includes time for preprocessing and parsing with llvm which is not part of the Polyhedra analysis. We report the time for the Polyhedra analysis separately on the terminal. (it is also present in the generated files)
  4. We set a default timeout limit of 6000 sec per benchmark, it is trivial to change this limit as per convenience in "measurement.sh".

Caveats

  1. The analysis runs slower on the virtual machine and the timings vary considerably. We measured timings from 71 sec to 120 sec during separate runs for "usb_core_main0" benchmark with optpoly. The "net_ppp" benchmark is also around three times slower with optpoly.
  2. For some benchmarks, seahorn crashes after the Polyhedra analysis completes. However, this is not due to optpoly or newpolka.
  3. There is typo in table 2, for the mtd-ubi benchmark, the analysis time with optpoly should be 4 sec instead of 23.

Compilation

All libraries can be compiled by running "compile.sh" in "scripts" directory.

Precision testing

  1. The analysis is intra-procedural and produces invariants in the form of sub-polyhedra constraints for each basic block in the function. The variables correspond to LLVM bitcode and thus they have unusual names in the invariants. LLVM can also produce different variable names for the same file on different runs.
  2. Since the analysis on larger benchmarks produce very large invariants, we provide smaller benchmarks in the "loops" directory. Running "sudo compare.sh" in "scripts" directory runs the Polyhedra, Octagon and Zones analysis with all libraries on these small benchmarks and collects results in "Compare" directory.
  3. The generated invariants are small and it is possible to manually compare them.

Reproducing results

  1. For reproducing results reported in the paper, run "sudo measurement.sh" in "scripts" directory. It runs the Zones analysis with all libraries on all benchmarks followed by Octagon and Polyhedra.
  2. The invariants are collected in "Results" directory.
  3. Unix's "time" command is used to display memory consumption (as maximum resident set size) on the terminal. Note that it can also report the total time used by the process which includes time for preprocessing and parsing with LLVM which is not part of the Sub-Polyhedra analysis. We report the time for the Sub-Polyhedra analysis separately on the terminal. (it is also present in the generated files) along with the invariants.
  4. We set a default timeout limit of 6000 sec per benchmark, it is trivial to change this limit as per convenience in "measurement.sh".

Caveats

  1. The analysis runs slower on the virtual machine and the timings vary considerably. On our machine, we observed that the slower libraries (e.g., PPL) run upto 10x slower on the virtual machines. The slowdown for our implementation was upto 2x.
  2. For some benchmarks, seahorn crashes after the Sub-Polyhedra analysis completes. However, this is not due to Sub-Polyhedra analysis.
  3. The "mtd_ubi" benchmarks runs longer with Octagon analysis than with Polyhedra. This is because the Octagon widening takes longer to converge on this benchmark than Polyhedra widening.

Additional statistics

We performed additional experiments to gather more statistics which were not reported earlier, but will be included in the final version of the paper. For each join point during analysis with optpoly, we measured the total number of variables (|X|), the number of variables in the largest block in the output (|S|) and the number of blocks in the output partition (nb). In the table below, we report the max and the average of these. We also report the fraction of times the output partition was trivial.

Benchmark Max(|X|)Avg(|X|)Max(|S|) Avg(|S|) Max(nb) Avg(nb) trivial/total
firewire_firedtv 159 80 24 5 31 6 10/577
net_fddi_skfp 589111 89 24 89 15 76/5163
mtd_ubi 528 60 111 10 57 12 27/2518
usb_core_main0 365 72 267 29 61 15 80/14594
tty_synclinkmp 332 47 48 8 34 10 23/3862
scsi_advansys 282 67 117 11 82 19 11/2315
staging_vt6656 675 53 204 10 62 6 35/1330
net_ppp 218 59 112 33 19 5 1/2350
p10_l00 303 184 234 59 38 29 0/601
p16_l40 188 125 86 39 53 38 4/186
p12_l57 921 371 461 110 68 28 4/914
p13_l53 1631 458 617 149 78 28 5/1325
p19_l59 1272 476 867 250 65 21 9/1754
ddv_all 45 22 7 2 14 8 5/124