Repository files navigation

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 calledcode2inv/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:

1. Clone the source code of Z3 fromhttps://github.com/Z3Prover/z3
2. Rungit 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 variablesLD_LIBRARY_PATH andPYTHONPATH 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 theclang-fe/ directory. The CHC frontend is called chc-fe and is located in thechc-fe/ directory. These frontends have limited support and are tested with the benchmarks included. Primarily, they can be used with programs containing single loops.

Theclang-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 thebenchmarks/C_instances directory and the same for the Non Linear benchmarks are included in thebenchmarks/nl-bench/ directory. To build the frontend, follow the instructions inREADME inclang-fe.

Thechc-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 thebenchmarks/CHC_instances directory. To run the CHC frontend, follow the instructions inREADME inchc-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 fileinv_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 fileinv_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 thecustomization guide.

For general customization, check out thecustomization 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 tobenchmarks/C_instances/c/ for examples of supported C programs).

We refer to the file asfile.c.

First, we need our input files which are the program graph json file and verification conditions SMT2 file. Follow the README inclang-fe/ and build the front-end. Then perform the following while in theclang-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 nowfile.c.json and verification condition file isfile.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 withFound 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 tobenchmarks/CHC_instances/sygus-constraints for examples of supported CHC constraints).

We refer to our file asfile.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 nowfile.json and verification condition file isfile.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 withFound 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}

wheredataset is the data name,prog_idx stands for the set of random perturbed programs, andagg_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 argumentinit_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}