Getting Started with Code2Inv

With Docker (the easy way)

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.

Building From Source (the not-so-easy way)

You can visit our GitHub repository here. All the instructions for installing Code2Inv and its front-ends are in the file. Follow those instructions and you should be done with installing Code2Inv in no time!

Customizing Code2Inv

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.

Running Code2Inv

We refer to the Code2Inv repository root as code2inv-repo. Running Code2Inv is straightforward. The script for running Code2Inv called 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
$ ./ ../../benchmarks/C_instances/c_graph/101.c.json ../../benchmarks/C_instances/c_smt2/101.c.smt specs/c_spec