Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving

# Bit-Vector CHC Solving for Binary Analysis and Vice Versa This is the (unofficial) artifact for the NFM'26 paper "Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving" by Aaron Bembenek and Toby Murray. For the purposes of reproducibility and evaluation, this artifact includes benchmarks from [CHC-COMP 2025](https://github.com/chc-comp/chc-comp25-benchmarks) and [LinearArbitrary-SeaHorn](https://github.com/GaloisInc/LinearArbitrary-SeaHorn). ## Docker Images Running the pipeline (to convert a binary to CHCs) or running an experiment (on CHCs) requires loading a Docker image.We have provided two images, one built for ARM64/AArch64, the other for AMD64/x86-64.Download the appropriate Docker image for your architecture and load it like so: ```shelldocker load -i binary-chc-[arm/amd]64.tar.gz``` Theta and UAutomizer will work on only the AMD64/x86-64 image. ## Binary-to-CHC Pipeline The `pipeline` directory contains the material relevant to the binary-to-CHC pipeline. The subdirectory `pipeline/chc-encoder/` includes the source code for the part of the pipeline we wrote---i.e., the component that encodes the Boogie file output by Basil as CHCs. To run the pipeline on an AArch64 Linux binary `[binary]` and write the result to file `[chcs.smt2]`, use this command from the artifact root directory: ```shellpipeline/encode [binary] [chcs.smt2]``` ## Benchmarks The benchmarks we used are in the `benchmarks/` subdirectory. The benchmarks in the `benchmarks/chc-comp/` subdirectory are those from the bit-vector track of CHC-COMP 2025. The benchmarks in the `benchmarks/test/` subdirectory are the ones we generate using our pipeline.Each leaf directory corresponds to a single benchmark.A directory of the form `benchmarks/text/X/Y/Z` will have the following content: - `Z.c`: the LinearArbitrary-SeaHorn benchmark (perhaps slightly adapted)- `Z.ultimate.c`: the version of the benchmark we run UAutomizer on- `Z.-O0.smt2`: the CHC constraints for the -O0 binary- `Z.-O2.smt2`: the CHC constraints for the -O2 binary- `verification.h`: used to build the benchmark- `seahorn/seahorn.h`: used to build the benchmark- `Makefile`: makefile for rebuilding the benchmark To use the makefile, you need to set these variables, either as environment variables or `make` configuration variables: - `ENCODE_SCRIPT`: should point to the script `pipeline/encode`- `ENCODE_CC`: should be set to a C compiler for producing AArch64 Linux binaries (e.g., something like `aarch64-unknown-linux-gnu-gcc` on Mac) Rebuilding the benchmarks also requires that the Docker image has been loaded. ## Experiments Our experimental scripts are located in the `experiments/scripts` directory. To evaluate a solver `[solver]` on CHC/C file `[input_file]` given a timeout `[timeout]` seconds, and store the results in directory `[results_dir]`, run this command: ```shellexperiments/evaluate [input_file] [solver] [timeout] [results_dir]``` The results will be a JSON file with a hash for a name.Because this script goes through docker, the "file" attribute of the JSON file will always be "/input/input_file.c", no matter what the actually input file is.Thus, to run experiments on many files and be able to identify which file each JSON report corresponds to, you could use a different result directory for each input file. The options for the solver argument are: `eldarica`, `spacer`, `theta`, and `uautomizer`.Theta and UAutomizer will only work on an AMD64/x86-64 architecture.The version of Eldarica we include (v2.2.1) is slightly newer than the version used in our experiments (commit 92860f1); we were unable to rebuild that particular commit in the Docker image. ## Analysis The `analysis` directory holds the results from the experiments reported in the paper and our analysis scripts.All following directions will be relative to this directory. To run the data processing and analysis scripts in this directory, you will want to create a Python virtual environment (with Conda, venv, etc.; we use Python 3.14.2), and then install the required dependencies: ```shellpip install -r requirements.txt``` The raw results are stored as JSON files (one per solver-benchmark pair) in `results/`; we have post-processed them into the CSV file `results.csv`.We have extracted the features from the CHC files in the `../benchmarks/` directory and stored them in the CSV file `chc_data.csv`.These CSV files can be recreated by running the `scripts/assemble_data.sh` script. Subdirectories `section4/` and `section5/` each have a Jupyter Notebook performing the analysis discussed in Sections 4 and 5, respectively. ## Acknowledgments This research was supported by The University of Melbourne’s Research Computing Services and the Petascale Campus Initiative.This research is supported by the Commonwealth of Australia as represented by the Defence Science and Technology Group of the Department of Defence.See paper for additional acknowledgments.