PLDI '25 Artifact Description

Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses

This is the artifact description for our PLDI '25 paper "Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses" by F. Stemmler, M. Schwarz, J. Erhard, S. Tilscher, and H. Seidl.

The artifact is available on Zenodo.

The description here is provided for convenience and not maintained. The artifact contains Goblint at pldi25_eval_runtime and pldi25_eval_stats git tags.

For convenience, this file is also included in the VM (at ~/precision-recovery-mixed-flowsens-benchmarks/README.md) to be able to copy commands.

Overview

The artifact is a virtual machine packaged for Oracle VirtualBox 6.1, which is available from Oracle and through the package manager of most distributions. The operating system is Ubuntu 24.04 LTS.

The folder structure of this artifact (~/precision-recovery-mixed-flowsens-benchmarks) is as follows:

  • analyzer: the Goblint analyzer
  • helper-scripts: Some helper scripts
  • rq1-3-benchmarks: Contains the instructions to reproduce the evaluation for RQ1-RQ3
  • rq4-results: Contains the raw data for RQ4
  • rq5-benchmarks: Contains the instructions to reproduce the evaluation for RQ5
  • README.md: top-level readme
  • CODE.md: A description of the changes made to Goblint.
  • EXAMPLE.md: An example program highlighting precision differences

There are two branches of the analyzer repository of relevance here:

  • pldi25_eval_runtime used to measure runtimes.
  • pldi25_eval_stats collects additional statistics but is slower.

In the artifact, analyzer is already checked out and dependencies are installed. If recreating the artifact from scratch proceed to General setup of the analyzer at the bottom.

Getting Started

  • For help importing the virtual machine, see https://docs.oracle.com/cd/E26217_01/E26796/html/qs-import-vm.html
  • The login is goblint:goblint.
  • Users not using EN-US keyboard: Switch the keyboard layout to match yours by
    • Clicking en in the right upper corner and
    • Choosing your layout if suggested or clicking on Keyboard Settings to set up another.

  • Verify the analyzer works by

    • Navigating to the folder of the artifact (~/precision-recovery-mixed-flowsens-benchmarks)
    • cd analyzer
    • make sanitytest (it may run a few minutes)
    • Expected output:

    Excellent: ignored check on tests/regression/03-practical/21-pfscan_combine_minimal.c:21 is now passing! Excellent: ignored check on tests/regression/03-practical/21-pfscan_combine_minimal.c:29 is now passing! No errors :)

Step-by-Step Reproduction

The steps for reproduction and claims are split by RQs, as is the evaluation section:

  • For RQ1-3, follow the instructions below and in ./rq1-3-benchmarks/README.md
  • For RQ4, see below and ./rq4-results/README.md
  • For RQ5, follow the instructions below and in ./rq5-benchmarks/README.md

Reproduction of Experiments for RQ1-3

The folder structure for this RQ (~/precision-recovery-mixed-flowsens-benchmarks/rq1-3-benchmarks) is as follows:

  • paper-runs: Folder containing the raw data of the runs underlying the plots in the paper
  • plots: Tex files with pgplots plots for plotting results
  • bench.txt: Specifies the full list of benchmark programs
  • reduced.txt: Specifies the reduced list of benchmark programs recommended for reproduction
  • Various Ruby / Python / Shell scripts

There are several levels of reproduction possible here:

  • A: The folder paper-runs contains the data produced by the runs we used for the paper. This allows reproducing the plots and data from our raw results. (Recommended)
  • B: We provide a subset of the benchmarks (including the ones used for Plot 3) for which results can realistically be reproduced inside the VM (Recommended)
  • C: We provide the scripts for a full reproduction (all 11k SV-COMP programs). This requires a machine with a considerable number N of cores so runtime is acceptable, e.g., 40 for the config and at least 15GB*N of RAM and a runtime of several days (assuming N=48 cores). (Not Recommended)

In the artifact, sv-comp is already checked out at the correct path. If recreating the artifact from scratch proceed to General setup of SV-COMP at the bottom.

Step 1: Producing the raw data

First step: Change into the analyzer repo cd .., run git checkout pldi25_eval_runtime, and make release. Then, change back to this directory.

The raw data here takes the form of a text file svcomp-raw.txt. The folder paper-runs contains the version of this raw data corresponding to the run in the paper.

Option A

As our raw data is used, nothing is to be done.

Option B

From this directory, run ./run-sv-comp.rb --pin --clean --reduced > svcomp-raw.txt 2> progress.txt

Expected Runtime: Around 1h40min

If you want to keep track of the progress you can open an additional terminal tail -f progress.txt.

Option C

From this directory, run ./run-sv-comp.rb --pin --clean -j 40 > svcomp-raw.txt 2> progress.txt

The -j parameter provides the number of concurrent runs to execute.

(The runtime here is on the magnitude of days with N=48 cores)

Step 2: Producing the plots

(For Option A: pass --paper as an additional argument to the scripts)

  • For plot 2
    • Run ./plot2.sh (Should this fail to the correct output check the individual steps listed in that file)
    • The resulting plot is located in plots/2/plot2.pdf
  • For plot 3
    • Run ./plot3.sh (Should this fail to the correct output check the individual steps listed in that file)
    • The resulting plot is located in plots/3/plot3.pdf

A list of claims from the paper supported by the artifact, and how/why

  • Total number of tasks and terminating task

    • plots/2/timeout-counts.tex

  • Fig. 2 (by reproducing the plot)

  • Fig. 3 (by reproducing the plot)

  • RQ1

    Concerning (RQ1), we find a net precision improvement in about 52% of tasks when using the new update rule with the number of W/N switches limited to either 3 (ours3) or 20 (ours20). 13% (ours3) and 20% (ours20) of tasks show substantial improvements. Conversely, ours loses precision compared to the baseline on about 1% of tasks, where almost all show substantial losses in precision.

    • Run ./compare.py --compare ours3 and ./compare.py --compare ours20
    • (For Option A: adding --paper)

    The subcategory ReachSafety-Recursive benefits particularly from update rule ours (see fig. 3). Both analyses provide substantial improvements in about 43% of cases. Interestingly, the share of degraded cases is also greater with about 4%.

    • Run ./compare.py --compare ours3 --rec and ./compare.py --compare ours20 --rec
    • (For Option A: adding --paper)

  • RQ2

    W.r.t. (RQ2), the update rule apinis produces an improvement only in about 40% of tasks, which are substantial only in 7% of tasks. At the same time, 18% of the tasks have a net precision loss and 11% a substantial loss.

    • Run ./compare.py --compare apinis
    • (For Option A: adding --paper)

    On the subset of ReachSafety-Recursive the update rule apinis achieves substantial precision improvements only in about 21% of cases, whereas it is 43% for the new update rule.

    • Run ./compare.py --compare apinis --rec
    • (For Option A: adding --paper)

  • RQ3:

    Regarding (RQ3), the update rule ours yields an improvement on 52% of tasks, regardless of whether the widening limit was set to 3 or 20. However, with a W/N limit of 20, 20% of tasks show substantial improvements, instead of 13% with the limit of 3. On ReachSafety-Recursive, with both limits to the number of W/N switches, an equal amount of precision is recovered (43%).

    • See RQ1.

Expected Output for Option B

By necessity, the results on this set do not fully coincide with the results on the full set. The subset for B was constructed to contain all the cases needed for full reproduction of the recursive subset, and by then subsequently adding categories while making sure the overall runtime inside the artifact remains acceptable. Unfortunately, a subset showing all effects but still having a reasonable runtime remained elusive.

SV-COMP has large groups of benchmarks that share similar characteristics, and the choice of whether these are included into the subset or not makes a huge difference for the observed numbers on the subset. A detailed investigation of what separates those tasks where effects can be observed from those where no or only small effects can be observed is certainly interesting. However, we think it is a topic for future work, and deem it to be out of scope for the artifact evaluation.

Nevertheless, we expect that these experiments, together with the extraction from the logs (Option A) and the fact that the recursive set is fully reproduced, inspire confidence in our overall experimental setup and results without having to take on the burden of a full reproduction involving multiple days of runtime on highly parallel machines.

  • Plots: See directory plots/b_{2,3}

  • Total number of tasks and terminating task:

    • plots/b_2/timeout-counts.tex
    • The subset was chosen to not include any tasks where the 15min timeout is hit to avoid excessive runtimes

  • Expected output for ./compare.py --compare ours3

Total entries: 992
improved (> 0%) : 172 (17.34%)
improved significantly (>= 5%) : 162 (16.33%)
worsened (< 0%) : 55 (5.54%)
worsened significantly (<= -5%) : 42 (4.23%)
  • Expected output for ./compare.py --compare ours20
Total entries: 992
improved (> 0%) : 172 (17.34%)
improved significantly (>= 5%) : 162 (16.33%)
worsened (< 0%) : 55 (5.54%)
worsened significantly (<= -5%) : 42 (4.23%)
  • Expected output for ./compare.py --compare ours3 --rec
Total entries: 156
improved (> 0%) : 67 (42.95%)
improved significantly (>= 5%) : 66 (42.31%)
worsened (< 0%) : 8 (5.13%)
worsened significantly (<= -5%) : 8 (5.13%)
  • Expected output for ./compare.py --compare ours20 --rec
Total entries: 156
improved (> 0%) : 67 (42.95%)
improved significantly (>= 5%) : 66 (42.31%)
worsened (< 0%) : 8 (5.13%)
worsened significantly (<= -5%) : 8 (5.13%)
  • Expected output for ./compare.py --compare apinis
Total entries: 992
improved (> 0%) : 90 (9.07%)
improved significantly (>= 5%) : 71 (7.16%)
worsened (< 0%) : 293 (29.54%)
worsened significantly (<= -5%) : 291 (29.33%)
  • Expected output for ./compare.py --compare apinis --rec
Total entries: 156
improved (> 0%) : 37 (23.72%)
improved significantly (>= 5%) : 34 (21.79%)
worsened (< 0%) : 22 (14.10%)
worsened significantly (<= -5%) : 20 (12.82%)

To further understand why these numbers differ from the ones observed in the overall set, one may additionally run ./compare_per_cat.py --compare ours20 --paper where ours20 can be replaced with any of the other options. One can observe that the impact of our update rules varies widely within these suites as provided by SV-COMP. Our hypothesis is that programs placed in the same category are roughly similar, though we have not yet investigated how program properties relate to precision gains.

General setup of SV-COMP

  • Clone sv-benchmarks at specific tag svcomp24 into the parent directory git clone --branch svcomp24-final --depth 1 https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.git

Data for Experiments for RQ4

In this folder (~/precision-recovery-mixed-flowsens-benchmarks/rq4-results), we provide the resulting tables from runs on SV-COMP controlled under Benchexec.

A list of claims from the paper supported by the artifact, and how/why

Overall, the analyses have almost identical runtimes on the tasks when they terminate. An exception is the configuration apinis, for which quite a few outliers with high runtime overheads are observed.

  • Open table-generator.table.html and navigate to the tab titled Scatter Plot.
  • Change Correct only for Results: to All.
  • Change X-Axis to cputime for base.
  • Change Y-Axis to cputime for one of ours3, ours20, or apinis.

The resulting plot shows runtimes of the base approach vs. the other. Each point is one program. For points on the diagonal, both approaches took the same time. For points below it, the other approach was faster; for those above it, base was faster.

The analyses with WizWoz's default update rule (972) and the update rule ours with a limit of 3 (975) and 20 (974) to the number of W/N switches, fail to complete in a similar number of cases, whereas the analysis with the update rule extracted from Apinis et al. (1003) fails to complete slightly more often

  • Open table-generator.table.html and navigate to the tab titled Table.
  • Then in the column Goblint [...] base (last one), select Category -> Error.

  • The number at the top right Showing 972 of 11222 tasks gives the number of failures.

  • Repeat for ours3, ours20, and apinis.

The majority of timeouts and other failures are shared between all considered analyses.

Open table-generator.diff.html. This lists all tasks where the type of failure differs or one of the analysis produced a timeout and the other did not. Observe that it is only 42/11222 tasks where this is the case.

A list of claims from the paper not supported by the artifact, and how/why

Our motivation for (RQ4) is producing reliable performance measurements by using benchexec which uses cgroups and other mechanisms to ensure that runtimes are reliable. Given the virtualization which occurs by using VirtualBox, the results of such a run would be no more representative than runs conducted with the setup we used for (RQ1-3). While the configurations for (RQ1-3) incur some overhead for marshaling, it is the same for all update rules. Thus, the results from that run can stand in to inspire confidence in the numbers for (RQ4) but cannot directly reproduce them.

Reproduction of Experiments for RQ5

The folder structure for this RQ (~/precision-recovery-mixed-flowsens-benchmarks/rq5-benchmarks) is as follows:

  • concrat: The benchmark programs assembled by [Hong and Ryu 2023]
  • pthread: The pthread benchmark programs from [Schwarz et al. 2021, 2023b]
  • svcomp: The device driver benchmark programs from [Schwarz et al. 2021, 2023b]
  • paper-runs: Folder containing the raw data of the runs underlying the plots in the paper
  • plots: Tex files with pgplots plots for plotting results
  • bench.txt: Specifies the full list of benchmark programs
  • reduced.txt: Specifies the reduced list of benchmark programs recommended for reproduction
  • Various Ruby / Python / Shell scripts

There are several levels of reproduction possible here:

  • A: The folder paper-runs contains the data produced by the runs we used for the paper. This allows reproducing the plots and data from our raw results. (Recommended)
  • B: We provide a subset of the benchmarks which can realistically be reproduced inside the VM (Recommended)
  • C: We provide the scripts for a full reproduction. The runtime for this is several days. (Not Recommended)

Producing the raw data

The raw data here takes the form of two text files plot4-7-raw.txt and plot5-6-raw.txt. The folder paper-runs contains the version of this raw data corresponding to the run in the paper.

Option A

As our raw data is used, nothing is to be done.

Option B
  1. Change into the analyzer repo, run git checkout pldi25_eval_runtime and make release

  2. From the rq5-benchmarks, run ./update_bench_propertimings.rb --i 1 --reduced &> plot5-6-raw.txt (By modifying the number supplied after i, you can specify that the average of more runs should be taken. To reduce runtimes, we recommend against it when reproducing results)

    Expected Runtime: Around 20min

  3. Change into the analyzer repo, run git checkout pldi25_eval_stats and make release

  4. From the rq5-benchmarks, run ./update_bench_fullpreccmp.rb --idead --priv-only --reduced &> plot4-7-raw.txt

    Expected Runtime: Around 25min

Note: Those with more patience may add programs from bench.txt back to reduced.txt to increase the subset of considered programs.

Option C
  1. Change into the analyzer repo, run git checkout pldi25_eval_runtime and make release

  2. From the rq5-benchmarks, run ./update_bench_propertimings.rb --i 1 &> plot5-6-raw.txt (By modifying the number supplied after i, you can specify that the average of more runs should be taken. To reduce runtimes, we recommend against it when reproducing results)

  3. Change into the analyzer repo, run git checkout pldi25_eval_stats and make release

  4. From the rq5-benchmarks, run ./update_bench_fullpreccmp.rb --idead --priv-only &> plot4-7-raw.txt

Producing the plots

(For Option A: pass --paper as an additional argument to the scripts)

  • Steps for reproducing plots 5 & 6:

    • For plot 5
      • Run ./plot5.sh (Should this fail to the correct output check the individual steps listed in that file)
      • The resulting plot is located in plots/5/plot5.pdf
    • For plot 6
      • Run ./plot6.sh (Should this fail to the correct output check the individual steps listed in that file)
      • The resulting plot is located in plots/6/plot6.pdf

  • Steps for reproducing plots 4 & 7:

    • For plot 4:
      • Run ./plot4.sh (Should this fail to the correct output check the individual steps listed in that file)
      • The resulting plot is located in plots/4/plot4.pdf
    • For plot 7:
      • Run ./plot7.sh (Should this fail to the correct output check the individual steps listed in that file)
      • The resulting plot is located in plots/7/plot7.pdf

Depending on the runtimes observed in the VM, the pgfplot options may need to be modified a little, see the *.tex file in the folder ./plots/N.

A list of claims from the paper supported by the artifact, and how/why

Plots 4-7: By reproducing them as outlined above

N.B.: Runtimes in the VM were observed to be quite a lot slower overall, though the relationship between configurations should still roughly be the same.

Specific claims:

  • When turning to net precision changes by aggregating precision losses and gains per program, we find that the update rule ours improves precision in 24 out of 38 cases, with 12 of these improvements being substantial. ours-bot improves precision for 32 programs, with 15 substantial improvements.

ours and ours-bot worsen net precision in only three and two cases, respectively, with two cases showing substantial losses for both approaches.

- Run `./compare.py --compare ours` and `./compare.py --compare ours-bot`
- (For **Option A:** adding `--paper`)

  • ours-bot always improves at least as many unknowns as ours and often more.

    • From Plot 4

  • The update rule apinis, on the other hand, improves net precision in only 11 cases, with six of these being substantial. Conversely, it worsens net precision in 18 cases, with 11 of these precision losses being substantial.

    • Run ./compare.py --compare apinis
    • (For Option A: adding --paper)

  • Abstract garbage collection generally comes with a moderate slowdown, but causes a slowdown by a factor of 2.72 in the extreme.

    • From Plot 5 and Running ./overhead.py
    • (For Option A: adding --paper)

  • For 18 out of 38 cases, over 40% of contexts are identified as dead.

    • Run ./dead-contexts.py
    • (For Option A: adding --paper)

We find that ours-bot increases memory usage by 15% for two programs, while it yields a reduction for 18 programs. At the extremes, the magnitude of the reduction is considerable. For ypbind and smtprc, e.g., the heap memory footprint is roughly halved.

- Run `./garbage.py`
- (For **Option A:** adding `--paper`)

Expected Output for Option B

  • Plots: See directory plots/b_{4,5,6,7}

  • Expected output for ./compare.py --compare ours

Total entries: 11
improved (> 0%) : 4 (36.36%)
improved significantly (>= 5%) : 1 (9.09%)
worsened (< 0%) : 1 (9.09%)
worsened significantly (<= -5%) : 0 (0.00%)
  • Expected output for ./compare.py --compare ours-bot
Total entries: 11
improved (> 0%) : 10 (90.91%)
improved significantly (>= 5%) : 3 (27.27%)
worsened (< 0%) : 0 (0.00%)
worsened significantly (<= -5%) : 0 (0.00%)
  • Expected output for ./compare.py --compare apinis
Total entries: 11
improved (> 0%) : 3 (27.27%)
improved significantly (>= 5%) : 2 (18.18%)
worsened (< 0%) : 2 (18.18%)
worsened significantly (<= -5%) : 1 (9.09%)
  • Expected output for ./overhead.py
Maximal overhead of 'ours-bot' over 'ours': 1.79
Corresponding row: {'suite': 'SV-COMP (ordered by logical LoC within this group)', 'file': 'marvell2', 'coordindex': '11', 'ours': '33.537565', 'ours-memory': '132.0', 'apinis': '39.773272', 'apinis-memory': '114.78', 'ours-bot': '60.106936', 'ours-bot-memory': '114.78', 'base': '39.964723', 'base-memory': '132.0'}
  • Expected output for ./dead-contexts.py
Total entries: 11
40% or more identified : 4
  • Expected output for ./garbage.py
Memory usage of ours-bot as fraction of ours for tegra20 : 0.76
Memory usage of ours-bot as fraction of ours for marvell1 : 0.76
Memory usage of ours-bot as fraction of ours for marvell2 : 0.87
Memory usage of ours-bot as fraction of ours for nsc : 0.76
Memory usage of ours-bot as fraction of ours for adutux : 1.00
Memory usage of ours-bot as fraction of ours for iowarrior : 0.87
Memory usage of ours-bot as fraction of ours for w83977af : 1.00
Memory usage of ours-bot as fraction of ours for ctrace : 1.00
Memory usage of ours-bot as fraction of ours for pfscan : 0.87
Memory usage of ours-bot as fraction of ours for knot : 1.00
Memory usage of ours-bot as fraction of ours for aget : 0.87
Gain: 3
Loss: 0

Reusability

There are several axes along which other researchers can build on this work; we briefly sketch two of these here:

Re-use the analyzer

The Goblint analyzer comes with extensive documentation (see analyzer/docs) or (perhaps more conveniently) the rendered online version. Of particular relevance here are:

Thus, the framework can serve as a testbed for new ideas for static analysis, allowing researchers to focus on the aspect of the system they are interested in while relying on the framework for everything else. The changes made to Goblint to implement the update rules are outlined in the external repository's CODE.md.

Example

An example program example.c is provided in the top folder of analyzer to highlight precision differences between configurations. For details see the external repository's EXAMPLE.md.

Experiment with further programs within this VM

All scripts are written in a way where it is easy to add further programs to the setup, or experiment with different settings and analyses. To this end, it suffices to modify the respective bench.txt files by, e.g.,

  • a) adding additional programs on which to experiment to the end or
  • b) specifying additional configurations which to run at the beginning of the file.

General setup of analyzer

  • Clone analyzer into top-level directory git clone git@github.com:goblint/analyzer.git
  • cd analyzer
  • git checkout pldi25_eval_stats (pldi25_eval_runtime will do too, dependencies are identical)
  • make setup
  • make dev
  • make release

Acknowledgments

We would like to thank the anonymous reviewers for their valuable feedback, which was instrumental in polishing the paper. DeepSeek was used to help with the creation of scripts for extracting precision data from logfiles. This work was supported in part by Deutsche Forschungsgemeinschaft (DFG) -- 378803395/2428 ConVeY.