Axiom Profiler 2.0

Runs online

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. 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.

This tool reimplements Axiom Profiler 1.0 and aims to eventually add new features while still delivering on 3 improvements:

• OS agnostic (runs in the browser)
• Better performance (about 10x faster parsing)
• Does not crash

More details of the tool's features can be found in the README of the old tool.

Note: not all features of the old tool are currently implemented: you may still find it useful to use the old tool.

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 /proverOpt:O:trace=true /proverOpt:O:proof=true ./file.bpl

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.vpr

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

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

on Unix-like systems or:

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

in Windows command prompt.

Carbon

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

carbon --print ./file.bpl ./file.vpr
boogie /vcsCores:1 /proverOpt:O:trace=true /proverOpt:O: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.