Unlocking C++ for C verifiers using ClangIR (accompanying artifact)

Artifact - Unlocking C++ for C verifiers using ClangIR (ICSE 2027) This artifact accompanies our ICSE 2027 paper. It contains everything needed to reproduce all results, tables, heatmaps, and plots in the paper, plus the reusable translation tool itself. The core idea: take C++ (or hard-to-verify C), lower it through ClangIR, and emit verifier-friendly C with verification intrinsics. C-only software verifiers can then handle C++, and patchy C support is worked around - all while preserving high-level structure (loops, records, exception scopes, virtual dispatch) for traceability. Requirements A Linux x86-64 host. The shipped binaries (cir2c, clang, cir-opt) need glibc ≥ 2.38 and a libstdc++ providing GLIBCXX_3.4.32 (GCC ≥ 13.2). Recommended: Ubuntu 24.04 LTS (glibc 2.39, GCC 14) or newer. Nothing else is needed just to inspect the shipped results; the tools below are only required for the regeneration steps that use them. cgroup v2 is required for the verification runs (make smoke-test / make full-test): BenchExec uses it to enforce and measure each run's CPU, memory and time limits. Set it up following BenchExec's guide — the Setting up Cgroups section, in particular Setting up Cgroups v2 on Machines with systemd. This is not needed for make rq1 / make figures / make tables / make sources. Command-line tools (PATH) Tool Needed by Notes bash, GNU coreutils (sed, nproc, timeout, …) all scripts / Makefiles GNU make ≥ 4.3 top-level + harness Makefiles grouped targets (&:) need ≥ 4.3 python3 ≥ 3.8 every analysis/generation script GNU parallel make rq1 / rq1-rerun (cir2c test suite) pdflatex (TeX Live / TeX distribution) make rq1 (renders the table PDFs) needs the standalone, booktabs, xspace packages git, curl, unzip, patch verification runs fetch/clone/install verifiers, BenchExec, fm-tools various ubuntu packages verification runs C verifiers' declared dependencies, same as on SV-COMP The LLVM/Clang + ClangIR toolchain (clang, clang++, cir-opt) and the built cir2c are shipped in llvm-install/ and cir2c/build/ — no separate install. Python packages The following third-party packages are used (everything else is the standard library): pip install PyYAML matplotlib numpy pandas matplotlib, numpy, pandas — make figures (gen_figures.py). PyYAML — the verification harness (make smoke-test / full-test, XML/task generation). Contents of the Artifact Path What it is cir2c/ the translator (C/C++ -> verifier-friendly C via ClangIR). See cir2c/README.md for reuse on your own code. llvm-install/ the prebuilt LLVM/Clang + ClangIR toolchain cir2c runs on verification_analysis/ the SV-COMP verifier evaluation harness (sources, results, tables, figures). See its README. Makefile top-level orchestrator - every reproduction step below is a target Included LLVM version LLVM/Clang 23.0.0 (23.0.0git) with ClangIR, built from llvm/llvm-project commit 9f578bc595ca7c1a5ce35b17c483fd6c557d11ef, shipped prebuilt in llvm-install/ (clang, clang++, cir-opt, MLIR/LLVM libraries, and the bundled libc++ headers). cir2c is already built against it at cir2c/build/cir2c. What you can reproduce Everything the paper reports: RQ1 - the cir2c test-suite tables: how cir2c fares on the LLVM test suite (compile + link + run + output match) and the ESBMC-eval suite (compile completeness). RQ2 - the verifier comparison tables (ESBMC baseline vs. each C verifier across the mapped suites), the dual-majority heatmaps (Fig. 5), and the shared-task quantile / cactus plots (Fig. 6). Reproduction process All results and data are already in the artifact - the pre-computed verification results live in verification_analysis/results/, the comparison tables in verification_analysis/tables/, and the four mapped source sets in verification_analysis/sources/. You can inspect the paper's numbers without running anything. Everything can also be regenerated from scratch via the Makefile. Each step is a single target: Step Command Time RQ1 tables (LLVM + ESBMC), reusing shipped results.txt make rq1 seconds RQ1, re-running the cir2c test suite first make rq1-rerun ~30 min RQ2 figures (heatmaps + plots) make figures seconds RQ2 comparison tables make tables ~1–2 min Regenerate the 4 derived source sets make sources ~1 h Smoke verification run make smoke-test ~15–30 min Full verification run make full-test ~155 CPU-days (see below) Clean generated artifacts make clean - (regen is slow!) Times are approximate and hardware-dependent (measured on an 8-core machine; tune parallelism with JOBS=N). RQ1 - cir2c LLVM + ESBMC test tables (make rq1) The artifact ships the two test-suite summaries (cir2c/test/{llvm,esbmc}/results.txt), so the default reproduction reuses them and just rebuilds the tables - no slow re-run needed: make rq1 # reuse shipped results.txt -> tables (seconds) This: runs generate.sh -> results2tex.py on the shipped results.txt to emit the LaTeX number macros cir2c/test/{llvm,esbmc}/numbers.tex (with built-in sub-total consistency checks); renders rq1-tables.tex - a minimal, self-contained re-derivation of the paper's RQ1 tables - once per table, as cropped PDFs next to this README: table4a.pdf - ESBMC suite completeness (does cir2c emit C that compiles?) table4b.pdf - LLVM SingleSource completeness table5.pdf - LLVM SingleSource output equivalence (compiled C runs and matches the reference output) Time: seconds. To regenerate the results.txt from scratch - re-running cir2c's own test suite (cir2c/test/run_tests.sh) over the LLVM test suite (RUN_LLVM=1: compile, link, run, diff against .reference_output) and the ESBMC-eval suite (RUN_ESBMC=1: compile completeness): make rq1-rerun # discard shipped results.txt, re-run the suite, rebuild tables Time: ~10 min (LLVM) + ~15–30 min (ESBMC) on an 8-core machine; the table build is then a few seconds. (make rq1 also falls back to this automatically if a results.txt is missing, e.g. after make clean.) RQ2 - figures from the included data (make figures) Regenerates the four paper figures from the included normalized results (no verification run needed) and writes them next to this README: make figures Produces, in this directory: fig5a.pdf, fig5b.pdf - dual-majority heatmaps (C++ vs. mapped C). fig6a.pdf, fig6b.pdf - shared-task quantile (cactus) plots. Time: seconds. (Script: verification_analysis/scripts/gen_figures.py.) The per-tool comparison tables are rebuilt with make tables (delegates to the harness's table-generator, ~1–2 min). Regenerate the 4 derived source sets (make sources) Rebuilds cpp-baseline, c-havoc_std, c-exact_std, and c-nohavoc_std under verification_analysis/sources/ by running cir2c over the original C++ suite (sources/esbmc-eval/, the input, is left untouched): make sources # or: make sources JOBS=16 Time: ~1 h on an 8-core machine (cir2c runs once per task, per variant). Script: verification_analysis/scripts/setup-sources.py. Smoke verification run (make smoke-test) A fast end-to-end check: 10 tasks per suite, every detected verifier, then tables. Validates the whole pipeline (download tool -> run -> normalize -> table). make smoke-test # local BenchExec (default) make smoke-test RUNNER=vcloud # BenchCloud / BenchCloud To run on BenchCloud with custom scheduler/heap flags, edit VCLOUD_FLAGS in verification_analysis/Makefile. Time: ~15–30 min, dominated by first-use tool-archive downloads. Full verification run (make full-test) The complete campaign - every task, every verifier, every config - i.e. exactly what produced the results already shipped here. Same runner options as the smoke test (RUNNER=benchexec|vcloud; custom vcloud flags via VCLOUD_FLAGS in verification_analysis/Makefile): make full-test RUNNER=vcloud FORCE=1 This takes around ≈ 13.4 million CPU-seconds ≈ 155 CPU-days. In practice this is run with heavy parallelism (locally with -jN, or distributed on BenchCloud), so wall-clock is far lower - but the raw compute cost is as above. Clean (make clean) Removes the generated artifacts: the 4 derived source sets (cpp-baseline, c-havoc_std, c-exact_std, c-nohavoc_std - sources/esbmc-eval is kept as it is the input); the entire results/ directory; the RQ1 outputs: the shipped cir2c/test/{llvm,esbmc}/results.txt, the derived numbers.tex, and the rendered table*.pdf / fig*.pdf next to this README. make clean # asks for confirmation Regeneration is expensive: the sources take around 1 h to rebuild (make sources), the results take ~155 CPU-days to recompute (make full-test), and the RQ1 results.txt take ~1 h to re-measure (make rq1-rerun). The figures and tables shipped in the artifact derive from results/ and the results.txt, so cleaning discards the primary data.