# Create a LoopInvGen container with 4GB memory, no swap and 1 CPU
$ docker run -it --memory=4g --memory-swap=4g --cpus=1 padhi/loopinvgen

See the official Docker guide for more details on applying resource constraints.

0. Get the required packages for your OS.

Please see the Dockerfile for the complete list of required packages for building LoopInvGen and its dependencies.
Most of these packages are already installed on standard installations of most *nix distributions, except, may be, these: aspcud libgmp-dev libomp-dev m4.

1. Install ocaml >= 4.04.2.

We recommend using an OCaml compiler with flambda optimizations enabled. For example, with opam, you could:

• run opam switch 4.07.1+flambda for opam 1.x
• run opam switch create 4.07.1+flambda for opam 2.x

2. opam install the dependencies.

$ opam install alcotest.0.8.5 core.v0.11.3 core_extended.v0.11.0 dune.1.7.0

3. Get the Z3 project.

We have tested LoopInvGen with the latest stable version of Z3 (4.8.4). You could either:

• git checkout https://github.com/Z3Prover/z3.git for the bleeding edge version, or
• wget https://github.com/Z3Prover/z3/archive/z3-4.8.4.zip && unzip z3-4.8.4.zip for the stable version

4. git clone this project, and build everything.

$ ./build_all.sh -z /PATH/TO/z3_dir

The build_all.sh script would build Z3, copy it to ./_dep/, and then build LoopInvGen. Alternatively, you can copy a precompiled version of Z3 to ./_dep/, and simply run ./build_all.sh.

For debug builds, use the -D or --debug switch when invoking ./build_all.sh.

For future builds after any changes to the source code, you only need to run dune build. You can configure the build profile to either debug or optimize (default), using: dune build --profile <profile>.

Verifying Generated Invariants

The -v switch makes LoopInvGen verify the benchmark with the generated invariant:

$ ./loopinvgen.sh -v benchmarks/LIA/2016.SyGuS-COMP/array.sl
PASS

It gives one of the following verdicts:

PASS                : The generated invariant successfully verifies the benchmark.
PASS (NO SOLUTION)  : The benchmark is invalid (no invariant can verify it),
                      and no invariant was generated.
FAIL {<vc1>;...}    : The generated invariant fails to verify the VCs: vc1, vc2 etc.
                      where each VC is one of {pre, post, trans}.
FAIL (NO SOLUTION)  : The benchmark is invalid (no invariant can verify it),
                      but an invariant (that is not empty/false) was generated.
[TIMEOUT] <verdict> : Invariant inference timed out.
                      With an empty (false) invariant, <verdict> is one of the verdicts above.

Try ./loopinvgen.sh -h for other options that allow more control over the inference process.

For each benchmark, the test_all.sh script generates one of the verdicts mentioned above, or:

[SKIPPED] <verdict> : Invariant inference was skipped for an already passing benchmark.
                      <verdict> is one of the PASS verdicts above.

Caching of Results

Since test_all.sh caches results from previous runs, it skips benchmarks that are known to be passing.
This may be disabled by:

• using the -r or --rerun-passed switch with test_all.sh, or
• deleting the previous log directory (default: _log), or
• specifying a new log directory (-l _new_log).

Benchmarking with Other Inference Tools

test_all.sh is a generic benchmarking script that may run any invariant inference tool. which accepts the SyGuS format. This makes it easier for us to compare various tools easily.
To use an invariant inference tool other than LoopInvGen, invoke it as: test_all.sh -b <path/to/benchmarks> -T <path/to/tool> [-- -tool -specific -options]

Limiting Execution Time

Just like loopinvgen.sh, the test_all.sh script allows users to limit the execution time for the invariant inference tools using the -t flag.

$ ./test_all.sh -b benchmarks/LIA -t 10

Try ./test_all.sh -h for more options.