ProveNFix

ProveNFix is a program analysis and repair tool for temporal properties for C language. ProveNFix is written in OCaml, and built on top of the Meta Infer tool.

Infer is a static analysis tool for Java, C++, Objective-C, and C. Infer is written in OCaml. Read Infer's Getting Started page for details on how to install packaged versions of Infer.

The repository provides the artifact for the FSE24 paper: ProveNFix: Temporal Property guided Program Repair. Our Benchmarks are available from Zenodo. The Source Code of the tool is available from GitHub. The final version of the Paper and the Appendix are publicly accessible.

Build ProveNFix

We have a docker image to try out our tool, which is detailed in the Artifact Evaluation Doc.

docker pull yahuuuuui/fse24-prove_n_fix:ubuntu
docker run -i -t yahuuuuui/fse24-prove_n_fix:ubuntu /bin/bash

The source code repository is placed in "/home/", called "infer_TempFix". The benchmarks are also summarized in the docker env. Alternatively, one could build \toolName from scratch using a Linux system (tested on Ubuntu 22.04.4 LTS), with the following dependencies:

apt install menhir 
apt install cmake 
apt install z3 
apt install sqlite3
apt install opam 
opam init
opam switch create 4.14.0
eval $(opam env)  
git clone https://github.com/songyahui/infer_TempFix.git
cd infer_TempFix
./compile

Run ProveNFix on the projects in experiments 1 and 2

Step 1: Put the default spec in the file "spec.c".

Step 2: Run ProveNFix

../../git/infer_TempFix/infer/bin/tempFix

Step 3: Check out the analysis/repair results in the file "TempFix-out/detail.txt"

Here lists the pre-required commands for the benchmark projects

Swoole

phpize
./configure

lxc, WavPack, p11-kit, flex, x264, recutils-1.8, inetutils-1.9.4, snort-2.9.13, grub

./autogen.sh 
./configure

Experiment 3: Automatically detect double free errors

Step1: Checkout the ProveNFix branch and re-build

git checkout doubleFreeClose
./compile

Step 2: Put the default spec ("spec_Temp_grub.c", "spec_Temp_lxc.c", "spec_Temp_p11.c") in the file "spec.c", and run ProveNFix on the projects Grub, lex, and p11-kit respectively.

../../git/infer_TempFix/infer/bin/tempFix

Step 3: Check out the analysis/repair results in the file "TempFix-out/detail.txt"

Experiment 4: generating specs for the OpenSSL project

Step1: Checkout the ProveNFix branch and re-build

git checkout Infer_OpenSSL
./compile

Get the source code and unzip OpenSSL

cd openssl-3.1.2
./Configure --prefix=/usr/local/ssl --openssldir=/usr/local/ssl \
    '-Wl,-rpath,$(LIBRPATH)'

Add the first two specs in the file "spec.c".

#define SW_CHANNEL_MIN_MEM (1024*64)

/*@ return(arg):
    Post (TRUE, return(arg))@*/

/*@ ERR_new():
    Post (TRUE, ERR_new())@*/

Run the ProveNFix

../../git/infer_TempFix/infer/bin/tempFix

Check out generated specs in the file "spec.c".

---

Thanks for trying out ProveNFix. In case there are any issues, please contact Yahui Song (yahui_s@nus.edu.s)