This clang-fe branch uses Clang compiler as the front-end, which is still under development by Aaditya Naik.

• python-2.7
• PyTorch 0.4.0
• python library: numpy, tqdm, pyparsing
• gcc/g++ 5.4.0 (or higher)
• make, cmake

code2inv uses the Z3 theorem prover to verify the correctness of generated loop invariants. Follow these steps to build Z3:

1. Clone the source code of Z3 from https://github.com/Z3Prover/z3
2. Run python scripts/mk_make.py --prefix /usr/local/; cd build; make -j16; make install

Remember to set environment variables DYLD_LIBRARY_PATH and PYTHONPATH to contain paths for Z3 shared libraries and Z3Py, respectively. These paths will be indicated upon successful installation of Z3.

The frontend is used to extract program graphs and verification conditions (VCs) from the input C programs. The program graphs and VCs for our benchmarks are already included in the benchmarks directory. To build the frontend, follow the instructions in README in code2inv-fe.

Install the dev version of this package:

pip install -e .

cd code2inv/prog_generator, then directly run the script ./run_solver.sh

To modify the script run_solver.sh:

1. Set the data_folder option to the code folder that contains folders graph/ and smt2/ which are created by the front-end pre-processor
2. Set the file_list option to the file that contains a list of code names. See code2inv/benchmarks/names.txt as an example.
3. Set the single_sample option to be the index of code where you want to find the loopinv for.
4. Adjust other parameters if necessary. Make sure to change parameters like max_and, max_or, max_depth, list_op to make sure the loopinv space is large enough (but not too large).

cd code2inv/prog_generator Then run: ./pretraining.sh ${dataset} ${prog_idx} ${agg_check} where dataset is the data name, prog_idx stands for the set of random perturbed programs, and agg_check can be 0 or 1, denoting whether more aggressive checker should be used.

cd code2inv/prog_generator Then run: ./fine_tuning.sh ${dataset} ${prog_idx} ${agg_check} ${init_epoch} where the last argument init_epoch stands for the model dump of corresponding epoch.