This is the easiest way to get started with Code2Inv. All you need is a machine with Docker installed and you are set!
Once you have Docker installed, you simply need to pull the Docker image from our Dockerhub repository. Fair warning, though, the image is a bit big.
$ docker pull code2inv/code2inv
Once the download is complete, you can run it as follows:
$ docker run -it --name code2inv code2inv/code2inv
This should run the image in a Docker container called code2inv. You can now play around with Code2Inv! Refer to the Experiments section in our README (available in our GitHub Repository) to know how to run Code2Inv.
You can visit our GitHub repository here. All the instructions for installing Code2Inv and its front-ends are in the README.md file. Follow those instructions and you should be done with installing Code2Inv in no time!
Code2Inv takes as input a graph file, a verification condition file and a specification file. We have included example inputs in our GitHub repository in the benchmarks directory.
The graph file is a file containing a single JSON object, with a list of nodes and the control flows between these nodes. These nodes include statements and expressions with details of these statements, including the variables, constants and operators used. This graph is indicative of the structural representation of the program. We include details about constructing the graph file here in our GitHub repository.
The verification condition file is a file containing the verification conditions used to check the correctness of the predicted invariant candidate. This may be in any format provided that the checker is able to process them and extract the counter examples when needed. We include further details about the verification condition file here in our GitHub repository.
The specification file is a file which contains the relative path to the grammar file, the name
of the checker module and the variable format which occurs in both the graph and the
verification condition files. The grammar file contains the grammar used to construct the invariant.
The checker module is used for checking the proposed invariant candidate against the verification
condition file and returning any counter examples. The variable format is to be specified as
ssa only if the SSA format of variables is used in the input graph and the
verification condition file. We include more details about the specification file
here in our GitHub repository.
We refer to the Code2Inv repository root as code2inv-repo. Running Code2Inv is straightforward.
The script for running Code2Inv called run_solver_file.sh is located in the
code2inv-repo/code2inv/prog_generator directory. It takes the three inputs as mentioned
earlier as well as an option to specify the output file. We show running Code2Inv on one of the C
programs we provide in the benchmarks directory.
$ cd code2inv-repo/code2inv/prog_generator
$ ./run_solver_file.sh ../../benchmarks/C_instances/c_graph/101.c.json ../../benchmarks/C_instances/c_smt2/101.c.smt specs/c_spec