An extension of ConSORT with the support of pointer arithmetic.

Building

Dependencies

The tool is written in OCaml, and it is known to work with OCaml 4.14.1. It also depends on the following OCaml libraries:

• ocamllex
• ocamlyacc

The following are additional (optional) dependencies that are used to solve the constraints generated by our tool:

• z3 (tested with 4.11.2)
• hoice (tested with 1.10.0)

Compilation

We use OCamlMakefile for compilation. The following command should build the executable main.

cd src && make

To clean the object files and the executable, you simply need to execute

make clean

while you are in /src.

Running

The simplest way to run the tool is to use the script test.sh provided that z3 and hoice are installed. For example

./test.sh examples/non-alias/init.imp

will checks the absence of assertion failure of init.imp. If you see ownership:sat and refinement:sat it means that the ownership and refinement inference have succeeded, respectively.

Manual execution is slightly more complicated.

Our tool has three modes. The first mode ./src/main int <filename> k does the first phase of the ownership inference against the program <filename>. The tool calculates the ownership constraints \forall ~x \exists ~y . phi(~x, ~y) and instantiates the universal quantifiers with n_1, ..., n_k and generates the formula \exists ~y . phi(n_1, ~y) /\ ... /\ phi(n_k, ~y). The formula in the SMT-LIB format is generated in experimet/out_int (currently the name of the output file is hard coded.) and the validity of this formula can be checked using z3. If the formula is valid, we let z3 generate the model, i.e. the assignments for ~y and use it in the next phase.

Now the second mode ./src/main fv <filename> 0does the second step of the ownership inference. It reads the SMT-LIB file generated by z3 (assuming that it is name experiment/result_int) in the previous phase and generates a SMTLIB file, named experiment/out_fv, corresponding to \forall ~x phi(~x, ~a), where ~a is the witness for \exist ~y obtained in the first phase. The validity of this formula can be checked by z3, and if the formula is valid we let z3 generate the ownerships (as a model).

The last mode ./src/main chc <filename> 0 calculates the constraints for the refinement inference against the program <filename>. It reads the ownerships (assuming that it is stored in experiment/result) and generates an SMT-LIB file containing the set of CHCs. The satisfiability of the set of CHCs can be checked by a CHC solver such as hoice.