The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).

Overview

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.

Comments
  • Improved Presentation of Matching Loops

    Improved Presentation of Matching Loops

    Pull request :twisted_rightwards_arrows: created by bitbucket user nilsbecker_ on 2018-01-09 19:48 Last updated on 2018-10-22 21:06 Original Bitbucket pull request id: 3

    Participants:

    • @alexanderjsummers (reviewer) :heavy_check_mark:
    • bitbucket user nilsbecker_

    Source: https://github.com/viperproject/axiom-profiler/commit/f688bd92aab6c44762cf4c02484ef9786dbae4a5 on branch nilsbecker_/axiom-profiler/default Destination: https://github.com/viperproject/axiom-profiler/commit/6a01ca9c6a1108d4df1f8b59bab38e6c591b5ceb on branch master Marge commit: https://github.com/viperproject/axiom-profiler/commit/75414eaee0ea0a0bb992096c4b7af350198e7bf6

    State: MERGED

    • Showing how generalized terms propagate through a single iteration of a matching loop
    • Explaining how matching loop starts over
    • More detailed explanation of how a term is obtained that can be matched by the next quantifier instantiation
    • Small changes to improve usability and direct the users attention

    Logs for the new version of the axiom profiler will have to be generated using the PROOF=true z3 option.

    Note: Quantifiers with the same name and body are unified in the new version of the axiom profiler. The identifiers presented by the axiom profiler may therefore not correspond to the ones used in the log file.

    merged pull request 
    opened by viper-admin 33
  • Exception:

    Exception: "Expected pattern but found Term"

    Created by bitbucket user jonhdotnet on 2018-11-20 22:50 Last updated on 2018-11-21 14:15

    I generated this log with boogie 2.3.0.61016 on Linux:

    mono ~/dafny-base/boogie/Binaries/Boogie.exe /z3exe:/home/jonh/dafny-base/dafny/Binaries/z3/bin/z3 /proc:'Impl$$_6_TwoThreeTree.__default.InsertIntoThreeNodeRight' /tmp/foo.bpl

    I try to feed it to the axiom profiler (fresh hg checkout today), but it throws an exception:

    An exception occurred while parsing the log: Expected pattern but found Term[boolType] Identifier:35, #Children:0.

    I added enough additional printf to determine that this is coming from line 31595 of the log. But I'm too inexperienced with z3 to understand what the log file means, and hence what this exception case means.


    Attachments:

    bug major 
    opened by viper-admin 13
  • Added Ubuntu instructions to README.

    Added Ubuntu instructions to README.

    Pull request :twisted_rightwards_arrows: created by @vakaras on 2016-08-14 19:41 Last updated on 2016-09-05 11:43 Original Bitbucket pull request id: 1

    Participants:

    • @alexanderjsummers (reviewer) :heavy_check_mark:
    • @vakaras

    Source: https://github.com/viperproject/axiom-profiler/commit/a96c99798867a9c1b0c702d588d81f3a20988203 on branch vakaras/axiom-profiler/default Destination: https://github.com/viperproject/axiom-profiler/commit/c18596e461c215dd687e1908bf224ae48ecbaa29 on branch master Marge commit: https://github.com/viperproject/axiom-profiler/commit/a96c99798867a9c1b0c702d588d81f3a20988203

    State: MERGED

    merged pull request 
    opened by viper-admin 3
  • Incorrect usage message/help page: passing a Boogie file to AxiomProfiler does not work

    Incorrect usage message/help page: passing a Boogie file to AxiomProfiler does not work

    Created by bitbucket user mschlaipfer on 2019-06-05 02:24 Last updated on 2019-07-10 13:25

    While I do not know what AxiomProfiler will do with a Boogie file, I have tried to pass one to it as stated in the usage and help pages:

    > $ AxiomProfiler prelude.bpl file.bpl /l:file.log /c:1
    Aborting parsing command line arguments:
    Multiple inputs files specified.
    Usage: AxiomProfiler [options] <prelude-file> <filename>
           prelude-file       : VCC prelude file location
           filename           : Boogie input file
           options
              /f:<function>   : Function name
              /t:<seconds>    : Verification timeout
              /l:<file>       : Log file to process
              /s              : Skip conflicts/decisions (conserves memory)
              /v1             : Start Z3 v1 (default)
              /v2             : Start Z3 v2
    

    Either there’s a bug or the help/usage messages are out-dated or unclear. Note that also the /c: option is not mentioned in the usage message.

    Maybe it is relevant that I am using cygwin.

    bug minor 
    opened by viper-admin 3
  • "Array dimension exceeded" error on loading log file

    Created by @alexanderjsummers on 2019-09-16 10:14 Last updated on 2019-09-30 15:52

    The log file (much truncated) and corresponding smt file are attached.


    Attachments:

    bug major 
    opened by viper-admin 2
  • Version 4.8.6 of z3 not compatible with Axiom Profiler

    Version 4.8.6 of z3 not compatible with Axiom Profiler

    Created by bitbucket user alexandrebinninger on 2019-07-04 13:20 Last updated on 2019-07-11 20:15

    I generated log files with z3 ver 4.8.6 and 4.8.5, but only the version 4.8.5 worked. The version 4.8.6 was compiled on Ubuntu 16.04 from the github (commit : e0a44894cf480908ddc8110b1761e682af4e4644). A .smt2 file is attached (the one I used).


    Attachments:

    bug minor 
    opened by viper-admin 2
  • Issues concerning CLI inputs for boogie and z3.

    Issues concerning CLI inputs for boogie and z3.

    Created by bitbucket user alexandrebinninger on 2019-07-02 10:17 Last updated on 2019-07-11 20:12

    Issues concerning CLI inputs for boogie and z3.

    • The order of the arguments matters for command-line inputs with z3.
    • It does not work on powershell.
    • We have to put an equality between z3 arguments. Sometimes some double quotes ".

    See the attached file for the complete terminal execution.


    Attachments:

    minor proposal 
    opened by viper-admin 2
  • Variable Names for Nested Quantifiers

    Variable Names for Nested Quantifiers

    Created by bitbucket user nilsbecker_ on 2019-02-27 19:27 Last updated on 2019-04-26 15:15

    Z3's internal indices are used to attach names and sorts to quantified variables. However, this does not work for nested quantifiers since z3 assigns the same indices to variables of the outer and inner quantifiers. E.g. in

    #!smt2
    
    forall x. A(x) && forall y. B(x, y)
    

    both x and y are assigned index 0. Loading logs that contain nested quantifiers such as https://bitbucket.org/viperproject/axiom-profiler-test-logs/src/default/civl-example-from-siddharth/test-test_1.smt (also attached) usually raises exceptions which are caught by the fault tolerance mechanisms in release builds resulting in those variable names / sorts being ignored for that quantifier. In practice nested quantifiers are usually rewritten into a single quantifier before being instantiated so the user may not necessarily notice any issues.


    Attachments:

    bug major 
    opened by viper-admin 2
  • Various small fixes

    Various small fixes

    Pull request :twisted_rightwards_arrows: created by bitbucket user moknuese on 2019-08-27 09:29 Last updated on 2019-11-29 18:54 Original Bitbucket pull request id: 7

    Participants:

    • @alexanderjsummers (reviewer)

    Source: https://github.com/viperproject/axiom-profiler/commit/8b65072a4becfafa0d4522ffdd3fd8a9bcf1e759 on branch moknuese/axiom-profiler/default Destination: https://github.com/viperproject/axiom-profiler/commit/964e670adff4e96aa9e0e9e87685015ae040c448 on branch master

    State: OPEN

    Here are quick fixes to various little things I encountered when using the AxiomProfiler on Debian 10, using mono 5.18.
    I didn’t go to deep into what the code does, so please let me know if any of the changes
    could lead to wrong outputs.

    • Avoids a problem with ToArray on mono. When using ToArray no substantial log files could be loaded
    • Print a message rather than crash the program Encountered when a path explanation featured 'arith-axiom'
    • fixes a crash on mono when color visualization is requested
    • fixes a crash when window is brought into focus by clicking in the middle third
    • fixes a problem where sometimes there are no statistics, but Max expects at least one element
    • fixes a crash when requesting quantifier blame visualization
    • fixes a crash when explaining a basic- or arith axiom also improves debugability by printing exception stacktraces to the console
    pull request 
    opened by viper-admin 1
  • Small Features and Adjustments

    Small Features and Adjustments

    Pull request :twisted_rightwards_arrows: created by bitbucket user nilsbecker_ on 2018-10-31 11:50 Last updated on 2018-10-31 11:51 Original Bitbucket pull request id: 5

    Participants:

    • bitbucket user nilsbecker_ :heavy_check_mark:

    Source: https://github.com/viperproject/axiom-profiler/commit/e05dfb1e80cb49fa3aa8a61809032edfbccccb15 on branch nilsbecker_/axiom-profiler/default Destination: https://github.com/viperproject/axiom-profiler/commit/75414eaee0ea0a0bb992096c4b7af350198e7bf6 on branch master Marge commit: https://github.com/viperproject/axiom-profiler/commit/13b6b225b7c8b1aea27399c118783fd9f767225c

    State: MERGED

    merged pull request 
    opened by viper-admin 1
  • Removed the copy task that causes the build to fail on Linux.

    Removed the copy task that causes the build to fail on Linux.

    Pull request :twisted_rightwards_arrows: created by @vakaras on 2017-05-05 10:21 Last updated on 2017-06-06 14:39 Original Bitbucket pull request id: 2

    Participants:

    • @alexanderjsummers (reviewer) :heavy_check_mark:

    Source: https://github.com/viperproject/axiom-profiler/commit/debb0b070e41f160ec13907b367dcb8dc1a8461c on branch vakaras/axiom-profiler/default Destination: https://github.com/viperproject/axiom-profiler/commit/c25401cd9d16dcb060e6ce91864fc1ad5e2c221a on branch master Marge commit: https://github.com/viperproject/axiom-profiler/commit/debb0b070e41f160ec13907b367dcb8dc1a8461c

    State: MERGED

    merged pull request 
    opened by viper-admin 1
  • Show original terms

    Show original terms

    From the presentation today, we saw that quantifier instantiations (rectangles) are shown, as well as theory-derived terms (diamonds). However, terms that come from the program itself, which I would expect to see at the root of the graph, cannot be seen.

    Maybe this could be an option?

    opened by Aurel300 0
  • Does not work on z3 logs generated using Silicon

    Does not work on z3 logs generated using Silicon

    I have a 2gb z3.log file generated using .\silicon --numberOfParallelVerifiers 1 --z3Args """""trace=true proof=true""""" --z3Exe ..\..\STMCors\deps\z3\4.8.6\z3.exe .\temp.sil

    The file temp.sil passes verification:

    Silicon finished verification successfully in 02m:20s.
    

    Yet, axiom-profiler produces a dialog box stating that an array contains no elements, but after clicking OK, it shows a bunch of quantifiers, but the number of instances are all 0.

    I can't upload the log file here because it is over 2gb in size, but I attached the temp.sil silver file that was used as an input for Silicon (renamed as temp.txt, because GitHub won't accept files ending with .sil). temp.txt

    opened by Jankoekenpan 1
  • Out of memory exception on small files

    Out of memory exception on small files

    I have this z3 log file of 3 gigabytes. When I load it into axiom profiler, axiom profiler gives an out of memory exception. If I cut it down to 800kb, it still gives an OOM. In both these cases, the first 8 quantifiers in the list of axiom profiler have about 20 instances total. Since I started with a 3 gigabyte file, I would expect more instances.

    If I cut it down to 500kb, it loads just fine, but contains no quantifier instances.

    I can also post a link to the 3 gigabyte version if needed.

    If I have a look where visual studio reports the exception, I get the following:

    afbeelding

    The "explanations" list seems to get filled up up to the memory limit of the system because of some cycle in the input...?

    I acquired this file by running viper/silicon with --numberOfParallelVerifiers 1 --z3Args '"trace=true proof=true"'. Besides that, I only did truncation on it using truncate -s 800K z3.log.

    Can axiom profiler be made aware of the cycle in these files? Or is the z3 log output of viper somehow wrong? Since the behavior between the 3gig file and 800k file is identical, I'm assuming truncation does not matter.

    opened by bobismijnnaam 1
  • Crash whith Mono when loading large log files

    Crash whith Mono when loading large log files

    When running the axiom profiler with Mono, loading any log file of nontrivial size (more than a few megabytes) seems to cause a crash. Using Mono is currently the only way to run the axiom profiler on non-Windows OSs, so this issue might affect many users that want to try the profiler.

    Probably related to this, the wiki of FStar reports the following:

    Using mono, the profiler seems too slow to process any trace of nontrivial size (with a 15 Mo z3.log, it ran for an hour before I kill it);

    bug 
    opened by fpoli 2
  • Subgraph

    Subgraph

    Changed how the program finds paths and the pattern of the path. Changed 'explain path' to 'explain subgraph'

    • New 'find path' will always include the node selected in the path. Notes here.
    • 'explain subgraph also find common incoming edges in the cycles. Notes here
    opened by TigerThePro 2
  • Missing instantiation of inner/nested quantifier

    Missing instantiation of inner/nested quantifier

    Note: Reducing attached SMT file to its minimum revealed issue #26.

    Running SMT file set_equals_triggers_datatypes.smt2.txt on Z3 4.8.6 on Windows 10 produced z3.log. Loading this into the axiom profiler shows an instantiation of axiom Set_equal_outer, and instantiations of datatype axioms that are triggered by terms that — I believe — have been obtained from instantiating axiom Set_equal_inner. According to the profiler, however, the latter was not instantiated.

    opened by mschwerhoff 0
Owner
Viper Project
Verification Infrastructure for Permission-​based Reasoning
Viper Project
Sampling profiler and tracer for Ruby (CRuby) which runs in BPF

rbperf rbperf is a low-overhead sampling profiler and tracer for Ruby (CRuby) which runs in BPF Build To build rbperf you would need a Linux machine w

Javier Honduvilla Coto 75 Dec 19, 2022
A Rust macro for writing regex pattern matching.

regexm A Rust macro for writing regex pattern matching.

Takayuki Maeda 46 Oct 24, 2022
Malloc frequency profiler

Malloc frequency profiler This malloc frequency profiler helps detect program hotspots that perform a large number of memory allocations.

Leonid Ryzhyk 7 Jan 7, 2022
A tracing profiler for the Sega MegaDrive/Genesis

md-profiler, a tracing profiler for the Sega MegaDrive/Genesis This program, meant to be used with this fork of BlastEm, helps you finding bottlenecks

null 15 Nov 3, 2022
Simple timings profiler

profl Simple timings profiler Example fn main() -> std::io::Result<()> { profl::init("timings.data"); let mut total = 0; for i in 0..1000

Broxus 1 Dec 9, 2021
Py-spy - Sampling profiler for Python programs

py-spy: Sampling profiler for Python programs py-spy is a sampling profiler for Python programs. It lets you visualize what your Python program is spe

Ben Frederickson 9.5k Jan 8, 2023
🐦 Friendly little instrumentation profiler for Rust 🦀

?? puffin The friendly little instrumentation profiler for Rust How to use fn my_function() { puffin::profile_function!(); ... if ... {

Embark 848 Dec 29, 2022
A memory profiler for Linux.

Bytehound - a memory profiler for Linux Features Can be used to analyze memory leaks, see where exactly the memory is being consumed, identify tempora

Koute 3.3k Dec 25, 2022
🐝🦀🔥 An ebpf based CPU profiler written in Rust

profile-bee ?? ?? ?? Profile Bee is an eBPF based CPU profiler written in Rust for performance and efficiency. Aya is used for building the BPF progra

Joshua Koo 5 Dec 16, 2022
Membrane is an opinionated crate that generates a Dart package from a Rust library. Extremely fast performance with strict typing and zero copy returns over the FFI boundary via bincode.

Membrane is an opinionated crate that generates a Dart package from a Rust library. Extremely fast performance with strict typing and zero copy returns over the FFI boundary via bincode.

Jerel Unruh 70 Dec 13, 2022
Code for connecting an RP2040 to a Bosch BNO055 IMU and having the realtime orientation data be sent to the host machine via serial USB

Code for connecting an RP2040 (via Raspberry Pi Pico) to a Bosch BNO055 IMU (via an Adafruit breakout board) and having the realtime orientation data be sent to the host machine via serial USB.

Gerald Nash 3 Nov 4, 2022
Adapter plugin to use Ruff in dprint's CLI and with JavaScript via Wasm

dprint-plugin-ruff Adapter for Ruff for use as a formatting plugin in dprint. Formats .py and .pyi files. Note: For formatting .ipynb files, use the J

null 3 Nov 28, 2023
notify Node.js binding via napi-rs.

@napi-rs/notify notify Node.js binding via napi-rs. Install this package yarn add

LongYinan 9 Jun 6, 2022
Trigger sounds via RFID tags or barcodes

Reads codes via RFID or 1D/2D barcode USB scanners and plays soundfiles mapped to them.

Jochen Kupperschmidt 3 Mar 12, 2022
esp-serial-dbg - debugging of esp-hal based applications via serial

esp-serial-dbg - debugging of esp-hal based applications via serial About This is still work in progress! At least the contained examples should work

Björn Quentin 3 Aug 23, 2022
An RSS feed aggregator that notifies you of new posts via email.

Rss2Email A small program capable of aggregating content from multiple RSS/Atom feeds and mailing them to you in a practical summary email. Keep track

Tony 18 Dec 18, 2022
A Bancho implementation made in Rust for the *cursed* stack.

cu.rs A Bancho implementation made in Rust for the cursed stack. THIS PROJECT IS REALLY UNFINISHED AND IN ITS EARLY STAGES A drag and drop replacement

RealistikOsu! 5 Feb 1, 2022
An annotated string type in Rust, made up of string slices

A string type made up of multiple annotated string slices.

Togglebit 3 Dec 29, 2022
A bundler (mainly for TypeScript projects) made in Rust

TSAR A bundler (mainly for TypeScript projects) made in Rust. Also my first Rust Project! What does TSAR stand for Like phar (PHP Archive) or JAR (Jav

null 2 Mar 19, 2022