Reproduction Package for TOSEM Submission "Precise Error Conditions"

Résumé fourni par la source

Reproduction Package for the Paper “Precise Error Conditions” Abstract This artifact is a reproduction package for the paper “Precise Error Conditions” which has been submitted to TOSEM. It consists of all executables, input data and results required to reproduce the experiments. In particular, it also contains the original results of the paper and a way to generate the plots in the paper from it. We run the experiments using 8 cores and a limit of 28 GB of memory and 60 minutes of CPU time per task. In the artifact we reduce the limits to 4 cores and 8GB of memory. While the reduction of cores will only affect the results related to the Wall Time (RQ1, RQ2), the reduced memory limit might lead to more out-of-memory exceptions in this artifact affecting all results. A full reproduction of the experiments requires roughly 2 years of CPU time. For demonstration purposes, a subset of tasks has been selected which takes about one hour. To check that everything is working as intended, make smoketest runs a small instance of all three parts of the artifact, including the case study on LLM-based program repair (cf. Section ‘Smoke Test’). The reproduction package can be found in Zenodo. Contents This artifact contains the following items: README.md: This file. setup_vm.sh: Prepares a clean Ubuntu machine, for example the CAV 2026 VM, for this artifact (cf. Section ‘Environment’). This is the first thing to run. config.sh, config_clean_vm.sh: The two environments for BenchExec, one of which has to be sourced in every shell before an experiment (cf. Section ‘TL;DR’). check_configured.sh checks that it was. benchmark-defs/*.xml.template: Templates to generate benchmark definition files for running the experiments using BenchExec. benchmark-defs/set_tasks.py: Script to change the tasks to be run in the xml files. benchmark-defs/tasks*.txt: Sets of tasks benchmark-defs/tasks-all.txt: All tasks used to produce the results in the paper. benchmark-defs/tasks-subset.txt: Subset of the tasks of the paper that runs in about an hour, generated by scripts/select_subset.py. benchmark-defs/tasks-one.txt: Two tasks used only for the smoke test of the Artifact. case-study: Programs and error conditions of the case study on LLM-based program repair (cf. Section ‘Case Study’). case-study/tasks: The C programs and their precise error conditions, which are the input of the case study. case-study/output: Written by make case-study, and holds the generated fixes, the classifications, and the result table. The classifications are judgements, so re-running the case study produces the labels of whoever runs it. case-study/output-paper: The same, as recorded for the paper: the fixes the model produced, the verdicts of CPAchecker on them, and the labels of the two authors that RQ5 reports. It is separate from case-study/output, so that re-running the case study compares against it instead of overwriting it (cf. Section ‘Case Study’). data-analysis: Scripts and definitions to produce the CSV files used to generate the plots in the paper. data-analysis/requirements.txt: Python packages required for the plots. data-analysis/wheels: Those packages as prebuilt wheels for Python 3.12, so that setup_vm.sh needs no package index. scripts: Scripts of the case study (cf. Section ‘Case Study’) and helpers for packaging the artifact. scripts/requirements.txt: Python packages required for the case study. scripts/wheels: Those packages as prebuilt wheels for Python 3.12, so that setting up the case study needs no package index. scripts/models: The weights of the model of the case study (about 5 GB). Makefile: Makefile to run the experiments. results-paper: Raw results of the experiments presented in the paper. License.txt: License information for the artifact. sv-benchmarks: The SV-COMP26 benchmarks, without tasks and programs which were not used in the experiments in order to make the artifact smaller. Tools DescribErr: DescribErr, revision 7aeedbdf, in the folder describerr, together with the tools it calls (CPAchecker, UAutomizer, CBMC) and TransVer revision ecd35a59, which rewrites the specifications no-overflow and termination into a reachability property. This is the revision that produced the results of the paper, and it is the one that make describerr checks out, so a rebuild reproduces the shipped tool rather than the current state of its repository. Its Python packages in describerr/lib/pip contain compiled extensions and are built for Python 3.12, the version of the CAV 2026 VM (cf. Section ‘Environment’). BenchExec: BenchExec version 3.32 in the folder benchexec. This Readme contains the following sections to help the user to reproduce the experiments: TL;DR: A quick guide to reproduce the experiments and analyze the data. Environment: Describes the environment in which the artifact was tested and can be run. Smoke Test: Describes how to check in about ten minutes that every part of the artifact works. Paper Example: Describes how to run DescribErr on the example of the introduction of the paper, which takes 12 to 15 minutes. Experiments: Describes how to execute the experiments and generate the results. Results: Describes where the results can be found and how to analyze them. Case Study: Describes how to run and label the case study on LLM-based program repair. Known Issues: Describes known issues when executing the artifact. TL;DR We tested the artifact inside the CAV 2026 VM (Ubuntu 24.04) with username and password being cav. The artifact needs about 45 GB of free disk space, which is more than that VM provides, so its disk has to be enlarged before it is used (cf. Section ‘Environment’). To run DescribErr on single examples, 4 cores and 8GB of RAM are sufficient. Give the VM 4 cores and 8 GB of memory and enlarge its disk to at least 70 GB (cf. Section ‘Environment’), then extract the files in the provided ZIP archive to an arbitrary directory and open a terminal inside it. Setup the environment of the VM using ./setup_vm.sh (requires root and will reboot your system). Set the environment variables (needed once per terminal): source config_clean_vm.sh: if full read/write access for all tools to /home is fine (recommended in the CAV VM) source config.sh: if you have a overlayfs in version 1.10 or newer installed Run make smoketest to check that all three parts of the artifact work: the analyses, the case study and the data analysis (cf. Section ‘Smoke Test’). Choose one of the following sets of tasks to run make setup-benchmark: Reproduce all results in our paper on your machine (takes about 2 years of CPU time, requires 8 cores and 31GB of RAM). We strongly discourage from running this inside the VM. make setup-benchmark-vm: Reproduce all results in our paper on your machine (takes about 2 years of CPU time, requires 4 cores and 8GB of RAM; final results might differ because of reduced resources). make setup-subset: Run a representative subset of our tasks (takes about 20 minutes, and at most an hour, and requires only 8 GB of RAM). make setup-testing: Run the two tasks of the smoke test only (takes about a minute and requires only 8 GB of RAM). Run make experiments to run the experiments for DescribErr. If you do not want to re-run the experiments of the paper, but continue the pipeline with our results, run make use-paper-results instead. Run make process-results to generate the results as HTML tables, raw CSV and plots used in the paper. Find them here: results/tables, and results/analysis. On the full results of the paper this takes several hours (cf. Section ‘Results’). Run make case-study LABELER= RUN_ARGS="--context-size 8192" to perform the case study on LLM-based program repair (cf. Section ‘Case Study’). This sets up a local LLM, queries it once per program and prompt, and asks you to classify the resulting fixes; it takes a bit over an hour. Find the result table here: case-study/output. The RUN_ARGS are what makes the model fit into the 8 GB of the VM (cf. Section ‘Me

Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.