An easy way to get Code2Inv up and running is to build it using the Dockerfile we have provided.
You can either pull the docker image from our dockerhub repo:
docker pull code2inv/code2inv
or build the docker container yourself by running the following command in the repo's root directory:
$ docker build -t code2inv/code2inv docker/
This should create an image called code2inv/code2inv
. To see all the docker images, run
$ docker images
Create the docker container:
$ docker run -it --name code2inv code2inv/code2inv
This should open a docker container with all code2inv setup completed.
The following are needed for running the basic setup
- python-3.7
- PyTorch 0.4.0
- python library: numpy, tqdm, pyparsing
- gcc/g++ 5.4.0 (or higher)
- clang-7
- make, cmake
code2inv uses the Z3 theorem prover to verify the correctness of generated loop invariants. Follow these steps to build Z3:
- Clone the source code of Z3 from https://github.com/Z3Prover/z3
- Run
git checkout tags/z3-4.8.7; python scripts/mk_make.py --prefix=<installation_prefix> --python --pypkgdir=<python_site_package_directory>; cd build; make; make install
Remember to set environment variables LD_LIBRARY_PATH
and PYTHONPATH
to contain paths for Z3 shared libraries and Z3Py, respectively. These paths will be indicated upon successful installation of Z3.
There are two frontends, one each for the C and CHC instances. The C frontend is called clang-fe and can be found in the clang-fe/
directory. The CHC frontend is called chc-fe and is located in the chc-fe/
directory. These frontends have limited support and are tested with the benchmarks included. Primarily, they can be used with programs containing single loops.
The clang-fe
frontend is used to extract program graphs and verification conditions (VCs) from the input C programs. This will be a necessary step if you wish to run Code2Inv on a C file which isn't in the benchmarks. The program graphs and VCs for our benchmarks are already included in the benchmarks/C_instances
directory and the same for the Non Linear benchmarks are included in the benchmarks/nl-bench/
directory. To build the frontend, follow the instructions in README in clang-fe
.
The chc-fe
frontend is used to extract program graphs from the input CHC programs (the CHC constraints themselves serve as the verification conditions (VCs)). This will be necessary to run Code2Inv for constraints not included in the benchmarks. The graphs and the VCs are already included in the benchmarks/CHC_instances
directory. To run the CHC frontend, follow the instructions in README in chc-fe
.
First, install the dev version of this package. To do this, run the following in the repository root directory:
$ pip install -e .
First change directory as follows:
$ cd code2inv/prog_generator
Directly run the solver script:
$ ./run_solver_file.sh $graph_file $vc_file $specification_file
To assign the output and related logs to a file, you can add the optional -o
argument:
$ ./run_solver_file.sh $graph_file $vc_file $specification_file \
-o output_file
To run code2inv on one of the 133 Linear C instances:
$ ./run_solver_file.sh ../../benchmarks/C_instances/c_graph/101.c.json ../../benchmarks/C_instances/c_smt2/101.c.smt specs/c_spec
Optionally, to store the result and related logs into an output file inv_result.txt
:
$ ./run_solver_file.sh ../../benchmarks/C_instances/c_graph/101.c.json ../../benchmarks/C_instances/c_smt2/101.c.smt specs/c_spec -o inv_result.txt
Some of other benchmarks which give an answer relatively quick include: 102.c, 53.c, 56.c, 65.c, 18.c, 98.c. Just substitute 101.c in the previous command with one of these benchmarks to get the solution for the same.
To run code2inv on one of the 120 Linear CHC instances:
$ ./run_solver_file.sh ../../benchmarks/CHC_instances/sygus-constraints-graphs/sygus-bench-101.c.smt.json ../../benchmarks/CHC_instances/sygus-constraints/sygus-bench-101.c.smt specs/chc_spec
Optionally, to store the result and related logs into an output file inv_result.txt
:
$ ./run_solver_file.sh ../../benchmarks/CHC_instances/sygus-constraints-graphs/sygus-bench-101.c.smt.json ../../benchmarks/CHC_instances/sygus-constraints/sygus-bench-101.c.smt specs/chc_spec -o inv_result.txt
Some of other benchmarks which give an answer relatively quick include: 78.c, 115.c, 45.c, 54.c, 71.c, 77.c. Just substitute 101.c in the previous command with one of these benchmarks to get the solution for the same.
To use a different grammar file for the invariants, refer to the grammar section in the customization guide.
For general customization, check out the customization guide.
To run Code2Inv on your own C programs or CHC instances, you will have to use the frontends provided to generate the program graphs and the verification conditions.
Code2Inv only supports C files with one loop and no external function calls (refer to benchmarks/C_instances/c/
for examples of supported C programs).
We refer to the file as file.c
.
First, we need our input files which are the program graph json file and verification conditions SMT2 file. Follow the README in clang-fe/
and build the front-end. Then perform the following while in the clang-fe/
directory:
$ ./bin/clang-fe -ssa file.c > file.c.json 2>/dev/null
$ ./bin/clang-fe -smt file.c > file.c.smt2 2>/dev/null
Our graph file is now file.c.json
and verification condition file is file.c.smt2
. Now from the repository directory, do the following:
$ cd code2inv/prog_generator
$ ./run_solver_file.sh file.c.json file.c.smt2 specs/c_spec -o file_inv.txt
After the solution is found (if it is found), you will see the solution and its logs printed on the screen (the line begins with Found a solution for 0...
). There will also be a file called file_inv.txt created with this information.
Code2Inv has only been tested on the CHC constraints corresponding to single loop C files obtained from Seahorn (refer to benchmarks/CHC_instances/sygus-constraints
for examples of supported CHC constraints).
We refer to our file as file.chc
.
First, we need our input files which are the program graph json file and the verification conditions file. The CHC file itself will serve as our verification condition file, so we only need to extract a program graph from it:
$ cd chc-fe
$ python graph-gen.py file.chc > file.json
Our graph file is now file.json
and verification condition file is file.chc
. From the repository directory, do the following:
$ cd code2inv/prog_generator
$ ./run_solver_file.sh file.c.json file.c.smt2 specs/c_spec -o file_inv.txt
After the solution is found (if it is found), you will see the solution and its logs printed on the screen (the line begins with Found a solution for 0...
). There will also be a file called file_inv.txt created with this information.
Run:
$ cd code2inv/prog_generator
$ ./pretraining.sh ${dataset} ${prog_idx} ${agg_check} ${grammar_file}
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.
An easier way would be to run
$ cd tests; ./test_learning.sh ${prog_idx}
Run:
$ cd code2inv/prog_generator
$ ./fine_tuning.sh ${dataset} ${prog_idx} ${agg_check} ${init_epoch} ${grammar_file}
where the penultimate argument init_epoch
stands for the model dump of corresponding epoch (latest
for the latest epoch dumped).
An easier way would be to run
$ cd tests; ./test_fine_tuning.sh ${prog_idx}