Axiom Profiler

A tool for visualising, analysing and understanding quantifier instantiations made via E-matching in a run of an SMT solver (at present, only Z3 has been modified to provide the necessary log files). The tool takes a log file (which can be generated by Z3 by passing additional command-line options; see below) and presents information visually, primarily using a graph representation of the quantifier instantiations made and their causal connections. This graph can be filtered and explored in a variety of ways, and detailed explanations of individual quantifier instantiations are assembled and displayed in the left-hand panel. A range of customisations are available for aiding the presentation and understanding of this information, including explanations of equalities used to justify a quantifier instantiation. The Explain Path feature in the graph also produces automatically explanations of matching loops occurring in the SMT run. More details of the tool's features can be found in this draft paper

Our tool was originally based on a tool called the VCC Axiom Profiler, and was since developed via Frederik Rothenberger's MSc project: Integration and Analysis of Alternative SMT Solvers for Software Verification and by substantial work by Nils Becker, both supervised by Alexander J. Summers who can be contacted with questions about the current version of the tool. We welcome bug reports and pull requests.

Using on Windows

1. Clone this repository:

   git clone https://github.com/viperproject/axiom-profiler.git
   

2. Build from Visual Studio (also possible on the command-line): open source/AxiomProfiler.sln solution, and run the release build. Requires C# 6.0 features, .Net >= 4.5 (and a version of Visual Studio which supports this, e.g. >= 2017).

3. Run the tool (either via Visual Studio, or by executing bin/Release/AxiomProfiler.exe)

Using on Ubuntu

(Note that the GUI of the tool currently suffers from some glitches when running under mono.)

1. Clone this repository:

   git clone https://github.com/viperproject/axiom-profiler.git
   cd axiom-profiler
   

2. Install Mono from https://www.mono-project.com/download/stable/

3. Download NuGet:

   wget https://nuget.org/nuget.exe
   

4. Install C# 6.0 compiler:

   mono ./nuget.exe install Microsoft.Net.Compilers
   

5. Compile project:

   xbuild /p:Configuration=Release source/AxiomProfiler.sln
   

6. Run Axiom Profiler:

   mono bin/Release/AxiomProfiler.exe
   

Using on Mac/Ubuntu (via Docker)

1. Install Docker.

2. Clone this repository:

    git clone https://github.com/viperproject/axiom-profiler.git
    cd axiom-profiler
   

3. Build the Docker image:

    docker build . --tag=axiom-profiler
   

4. Start the Docker image, replacing <path> with the absolute path of the folder containing the Z3 logs:

    docker run -t -p 6080:6080 -v<path>:/home/ubuntu/data axiom-profiler
   

5. Follow the instructions printed in the terminal to open a remote desktop of the Docker image.

6. In the remote desktop, open a terminal and start the axiom profiler:

    mono /home/ubuntu/axiom-profiler/bin/Release/AxiomProfiler.exe
   

7. In the axiom profiler, the logs can be loaded from the "Personal > data" location.

Obtaining logs from Z3

NOTE: The Axiom Profiler requires at least version 4.8.5 of z3. To build the latest version of z3 from source follow the instructions at https://github.com/Z3Prover/z3.

Run Z3 with two extra command-line options:

z3 trace=true proof=true ./input.smt2

This will produce a log file called ./z3.log. If you want to specify the target filename, you can pass a third option:

z3 trace=true proof=true trace-file-name=foo.log ./input.smt2

NOTE: if this takes too long, it is possible to run the Axiom Profiler with a prefix of a valid log file - you could potentially kill the z3 process and obtain the corresponding partial log. Some users (especially on Windows) have reported that killing z3 can cause a lot of the file contents to disappear; if you observe this problem, it's recommended to copy the log file before killing the process.

Similarly, if you have a log file which takes too long to load into the Axiom Profiler, hitting Cancel will cause the tool to work with the portion loaded so far.

Obtaining Z3 logs from various verification tools that use Z3 (feel free to add more)

Boogie

To obtain a Z3 log with Boogie, use e.g:

boogie /vcsCores:1 /z3opt:trace=true /z3opt:PROOF=true ./file.bpl

Note that you may also want to pass the /vcsCores:1 option to disable concurrency (since otherwise many Z3 instances may write to the same file)

Silicon

To obtain a Z3 log with the Viper symbolic execution verifier (Silicon), use e.g:

silicon --numberOfParallelVerifiers 1 --z3Args "trace=true proof=true" ./file.sil

If it complains about an unrecognized argument, try escaping the double-quotes. E.g.:

silicon --numberOfParallelVerifiers 1 --z3Args '"trace=true proof=true"' ./file.sil

on Unix-like systems or:

silicon --numberOfParallelVerifiers 1 --z3Args """trace=true proof=true""" ./file.sil

in Windows command prompt or:

silicon --numberOfParallelVerifiers 1 --z3Args """""trace=true proof=true""""" ./file.sil

in Windows PowerShell.

Carbon

To obtain a Z3 log with the Viper verification condition generation verifier (Carbon), use e.g:

carbon --print ./file.bpl ./file.sil
boogie /vcsCores:1 /z3opt:trace=true /z3opt:proof=true ./file.bpl

In all cases, the Z3 log should be stored in ./z3.log (this can also be altered by correspondingly passing z3 the trace-file-name option described above)

Dafny

See these instructions in Dafny's wiki: Investigating slow verification performance.

FStar

See these instructions in FStar's wiki: Profiling Z3 queries.