viperproject / axiom-profiler Goto Github PK

View Code? Open in Web Editor NEW

27.0 27.0 4.0 58.39 MB

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

License: Other

SMT 0.51% PowerShell 0.34% TeX 7.70% C# 89.42% Makefile 0.01% CSS 0.19% JavaScript 1.18% HTML 0.57% Dockerfile 0.10%

axiom-profiler's People

Stargazers

Watchers

Forkers

hermetique tigerthepro ksqsf

axiom-profiler's Issues

Enabled sending bug reports for confidential files by adding the ability to obfuscate z3 smtlib files to the SMT-COMP scrambler

Created by bitbucket user mschlaipfer on 2019-07-23 03:37
Last updated on 2019-10-14 20:04

Maybe this is interesting to the axiom profiler team.

I have implemented functionality to the SMT-COMP scrambler that allows to obfuscate smtlib files that have z3-specific features. The PR is currently pending here: https://github.com/SMT-COMP/scrambler/pull/2/files
I don’t know if the team behind the scrambler will merge it, though. If not, the fork is on my github profile at https://github.com/mschlaipfer/scrambler/tree/z3-specific.

Support for Theory Solvers, MBQI

Pull request 🔀 created by bitbucket user nilsbecker_ on 2019-02-23 13:48
Last updated on 2019-02-27 18:38
Original Bitbucket pull request id: 6

Participants:

@alexanderjsummers (reviewer)

Source: 0bd9b4e on branch nilsbecker_/axiom-profiler/default
Destination: d25a3e8 on branch master
Marge commit: 0bd9b4e

State: MERGED

The corresponding z3 pull request is: Z3Prover/z3#2150.

Handling of Rewrite Steps

Created by bitbucket user nilsbecker_ on 2019-02-27 19:51
Last updated on 2019-09-30 15:50

For simple loops as shown in the attached file where we have some term f(x) and add 1 to x each time around the loop the integer arithmetic solver (or any other solver in different examples) may rewrite some terms. In the attached example we bind x to a then a+1 then a+2 etc. In order to correctly generalize these terms we would need to have a+1+1 as the third term.

Note that we end up with something looking very similar to what we would want the generalization to be due to the generalization going wrong in just the right way: we first anti-unify the terms shown above to obtain T then essentially ignore the first term (a) for the results since it was not produced by any instantiation in the loop. Anti-unifying a+1, a+2, etc. then gives us a+Int() (it is even possible to obtain T+Int() in other examples), however, the identifier of the Int constant is prefixed with a "g" indicating that the constant changes in each iteration of the loop.

Attachments:

Improved Presentation of Matching Loops

Pull request 🔀 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) ✔️

bitbucket user nilsbecker_

Source: f688bd9 on branch nilsbecker_/axiom-profiler/default
Destination: 6a01ca9 on branch master
Marge commit: 75414ea

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.

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:

"in this draft paper" pdf link update

found at
https://pm.inf.ethz.ch/publications/BeckerMuellerSummers19.pdf

Small Features and Adjustments

Pull request 🔀 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_ ✔️

Source: e05dfb1 on branch nilsbecker_/axiom-profiler/default
Destination: 75414ea on branch master
Marge commit: 13b6b22

State: MERGED

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:

Crash, potentially related to incremental solving (push-pop blocks)

Created by @mschwerhoff on 2016-09-26 12:53

The axiom profiler crashes (on Win 10 x64) if the second trace recorded in the zipped Z3 logfile is inspected, i.e. if invoked as follows:

AxiomProfiler.exe /c:2 logfile-0208-z3.log

Screenshots of the reported error messages are attached.

Attachments:

"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:

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

Pull request 🔀 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) ✔️

Source: debb0b0 on branch vakaras/axiom-profiler/default
Destination: c25401c on branch master
Marge commit: debb0b0

State: MERGED

Exception: Cycle in causality graph

A recent nightly of the axiom profiler crashes with Found cycle in causality graph!. The exception occurs regardless of whether or not Only show instantiations from single check is ticked while loading the Z3 logfile.

Z3 logfile

z3.log

Created by Z3 4.8.6 on Windows 10.

Source SMT file

set_equals_triggers_datatypes.smt2.txt

Exception details

See the end of this message for details on invoking 
just-in-time (JIT) debugging instead of this dialog box.

************** Exception Text **************
System.Exception: Found cycle in causality graph!
   at AxiomProfiler.QuantifierModel.Instantiation.get_Depth() in C:\Program Files (x86)\Jenkins\jobs\axiom-profiler-win\workspace\source\QuantifierModel\Instantiation.cs:line 125
   at AxiomProfiler.DAGView.<drawGraphNoFilterQuestion>b__11_0(Instantiation inst) in C:\Program Files (x86)\Jenkins\jobs\axiom-profiler-win\workspace\source\DAGView.cs:line 77
   at System.Linq.Enumerable.WhereListIterator`1.MoveNext()
   at System.Linq.Buffer`1..ctor(IEnumerable`1 source)
   at System.Linq.OrderedEnumerable`1.<GetEnumerator>d__1.MoveNext()
   at System.Linq.Enumerable.<TakeIterator>d__25`1.MoveNext()
   at System.Collections.Generic.List`1..ctor(IEnumerable`1 collection)
   at System.Linq.Enumerable.ToList[TSource](IEnumerable`1 source)
   at AxiomProfiler.DAGView.drawGraphNoFilterQuestion() in C:\Program Files (x86)\Jenkins\jobs\axiom-profiler-win\workspace\source\DAGView.cs:line 76
   at AxiomProfiler.AxiomProfiler.loadModel(ParameterConfiguration config) in C:\Program Files (x86)\Jenkins\jobs\axiom-profiler-win\workspace\source\AxiomProfiler.cs:line 264
   at AxiomProfiler.AxiomProfiler.loadModelFromZ3Logfile() in C:\Program Files (x86)\Jenkins\jobs\axiom-profiler-win\workspace\source\AxiomProfiler.cs:line 250
   at AxiomProfiler.AxiomProfiler.LoadZ3Logfile_Click(Object sender, EventArgs e) in C:\Program Files (x86)\Jenkins\jobs\axiom-profiler-win\workspace\source\AxiomProfiler.cs:line 85
   at System.Windows.Forms.ToolStripItem.RaiseEvent(Object key, EventArgs e)
   at System.Windows.Forms.ToolStripMenuItem.OnClick(EventArgs e)
   at System.Windows.Forms.ToolStripItem.HandleClick(EventArgs e)
   at System.Windows.Forms.ToolStripItem.HandleMouseUp(MouseEventArgs e)
   at System.Windows.Forms.ToolStrip.OnMouseUp(MouseEventArgs mea)
   at System.Windows.Forms.ToolStripDropDown.OnMouseUp(MouseEventArgs mea)
   at System.Windows.Forms.Control.WmMouseUp(Message& m, MouseButtons button, Int32 clicks)
   at System.Windows.Forms.Control.WndProc(Message& m)
   at System.Windows.Forms.ToolStrip.WndProc(Message& m)
   at System.Windows.Forms.ToolStripDropDown.WndProc(Message& m)
   at System.Windows.Forms.NativeWindow.Callback(IntPtr hWnd, Int32 msg, IntPtr wparam, IntPtr lparam)


************** Loaded Assemblies **************
mscorlib
    Assembly Version: 4.0.0.0
    Win32 Version: 4.7.3620.0 built by: NET472REL1LAST_B
    CodeBase: file:///C:/Windows/Microsoft.NET/Framework64/v4.0.30319/mscorlib.dll
----------------------------------------
AxiomProfiler
    Assembly Version: 2.0.0.0
    Win32 Version: 2.0.0.0
    CodeBase: file:///F:/Downloads/Axiom-Profiler-Win/Debug/AxiomProfiler.exe
----------------------------------------
System.Windows.Forms
    Assembly Version: 4.0.0.0
    Win32 Version: 4.7.3580.0 built by: NET472REL1LAST_C
    CodeBase: file:///C:/WINDOWS/Microsoft.Net/assembly/GAC_MSIL/System.Windows.Forms/v4.0_4.0.0.0__b77a5c561934e089/System.Windows.Forms.dll
----------------------------------------
System
    Assembly Version: 4.0.0.0
    Win32 Version: 4.7.3451.0 built by: NET472REL1LAST_C
    CodeBase: file:///C:/WINDOWS/Microsoft.Net/assembly/GAC_MSIL/System/v4.0_4.0.0.0__b77a5c561934e089/System.dll
----------------------------------------
System.Drawing
    Assembly Version: 4.0.0.0
    Win32 Version: 4.7.3056.0 built by: NET472REL1
    CodeBase: file:///C:/WINDOWS/Microsoft.Net/assembly/GAC_MSIL/System.Drawing/v4.0_4.0.0.0__b03f5f7f11d50a3a/System.Drawing.dll
----------------------------------------
Microsoft.Msagl.Drawing
    Assembly Version: 3.0.0.0
    Win32 Version: 3.0.0.0
    CodeBase: file:///F:/Downloads/Axiom-Profiler-Win/Debug/Microsoft.Msagl.Drawing.DLL
----------------------------------------
System.Configuration
    Assembly Version: 4.0.0.0
    Win32 Version: 4.7.3056.0 built by: NET472REL1
    CodeBase: file:///C:/WINDOWS/Microsoft.Net/assembly/GAC_MSIL/System.Configuration/v4.0_4.0.0.0__b03f5f7f11d50a3a/System.Configuration.dll
----------------------------------------
System.Core
    Assembly Version: 4.0.0.0
    Win32 Version: 4.7.3620.0 built by: NET472REL1LAST_B
    CodeBase: file:///C:/WINDOWS/Microsoft.Net/assembly/GAC_MSIL/System.Core/v4.0_4.0.0.0__b77a5c561934e089/System.Core.dll
----------------------------------------
System.Xml
    Assembly Version: 4.0.0.0
    Win32 Version: 4.7.3056.0 built by: NET472REL1
    CodeBase: file:///C:/WINDOWS/Microsoft.Net/assembly/GAC_MSIL/System.Xml/v4.0_4.0.0.0__b77a5c561934e089/System.Xml.dll
----------------------------------------
Microsoft.Msagl
    Assembly Version: 1.0.0.0
    Win32 Version: 1.0.0.0
    CodeBase: file:///F:/Downloads/Axiom-Profiler-Win/Debug/Microsoft.Msagl.DLL
----------------------------------------
Microsoft.Msagl.GraphViewerGdi
    Assembly Version: 3.0.0.0
    Win32 Version: 3.0.0.0
    CodeBase: file:///F:/Downloads/Axiom-Profiler-Win/Debug/Microsoft.Msagl.GraphViewerGdi.DLL
----------------------------------------

************** JIT Debugging **************
To enable just-in-time (JIT) debugging, the .config file for this
application or computer (machine.config) must have the
jitDebugging value set in the system.windows.forms section.
The application must also be compiled with debugging
enabled.

For example:

<configuration>
    <system.windows.forms jitDebugging="true" />
</configuration>

When JIT debugging is enabled, any unhandled exception
will be sent to the JIT debugger registered on the computer
rather than be handled by this dialog box.

Added Ubuntu instructions to README.

Pull request 🔀 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) ✔️

@vakaras

Source: a96c997 on branch vakaras/axiom-profiler/default
Destination: c18596e on branch master
Marge commit: a96c997

State: MERGED

Connecting Inner and Outer Quantifiers (Nesting)

Created by bitbucket user nilsbecker_ on 2019-02-27 20:21

In some cases, when z3 doesn't rewrite nested quantifiers into a single quantifier, it may be useful to be able to tell which instantiation of the outer quantifier lead to the creation of the inner quantifier.

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.

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:

sequence.smt2

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.

800kb file that causes a crash and has only a handful of quantifier instances: z3_smaller.log
500kb file that doesn't crash but has no quantifier instances: z3_smaller_no_quant.log

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:

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.

Hiding Term Identifiers doesn't always work in a matching loop explanation

Created by @alexanderjsummers on 2019-11-18 13:29

For example, loading the log file attached to this issue, selecting the topmost node and clicking Explain Path yields an explanation in which the term identifiers can't be removed.

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:

issues.txt

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.

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);

Large Text font size isn't always applied

Created by @alexanderjsummers on 2019-11-18 15:00

For example, loading the log file attached to this issue, selecting the topmost node and clicking Explain Path yields an explanation in which some term structure is displayed in small font. Similarly, selecting a diamond node, the theory-solver-related text is small.

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

AxiomProfiler should emit a version number with Usage message

Created by bitbucket user jonhdotnet on 2018-11-20 22:54
Last updated on 2019-09-16 10:32

I filed a bug report, and realized I didn't have a way to learn the version number of the AxiomProfiler that I used. In my case that's probably okay; it was a recent hg checkout. But it would probably help with future reports to provide a version number.

Failure inside the docker

When I tried to execute the command: docker build . --tag=axiom-profiler, I got the following error:

[+] Building 4.1s (16/17)                                                                                         docker:desktop-linux
 => [internal] load .dockerignore                                                                                                 0.0s
 => => transferring context: 2B                                                                                                   0.0s
 => [internal] load build definition from Dockerfile                                                                              0.0s
 => => transferring dockerfile: 768B                                                                                              0.0s
 => [internal] load metadata for docker.io/x11vnc/desktop:20.04                                                                   1.3s
 => [ 1/12] FROM docker.io/x11vnc/desktop:20.04@sha256:d1b18f3cbcc5f741341e9b257b7f509119d4a25ba0eb2cfc9e66c5a594195d18           0.0s
 => https://nuget.org/nuget.exe                                                                                                   1.1s
 => [internal] load build context                                                                                                 0.0s
 => => transferring context: 7.79kB                                                                                               0.0s
 => CACHED [ 2/12] RUN apt update                                                                                                 0.0s
 => CACHED [ 3/12] RUN apt install -y gnupg ca-certificates                                                                       0.0s
 => CACHED [ 4/12] RUN apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831E  0.0s
 => CACHED [ 5/12] RUN echo "deb https://download.mono-project.com/repo/ubuntu stable-focal main" > /etc/apt/sources.list.d/mono  0.0s
 => CACHED [ 6/12] RUN apt update                                                                                                 0.0s
 => CACHED [ 7/12] RUN DEBIAN_FRONTEND=noninteractive apt install -y mono-devel                                                   0.0s
 => CACHED [ 8/12] COPY --chown=ubuntu:ubuntu . /home/ubuntu/axiom-profiler                                                       0.0s
 => CACHED [ 9/12] WORKDIR /home/ubuntu/axiom-profiler                                                                            0.0s
 => CACHED [10/12] ADD --chown=ubuntu:ubuntu https://nuget.org/nuget.exe nuget.exe                                                0.0s
 => ERROR [11/12] RUN mono ./nuget.exe install Microsoft.Net.Compilers                                                            1.6s
------                                                                                                                                 
 > [11/12] RUN mono ./nuget.exe install Microsoft.Net.Compilers:                                                                       
0.514 TYPE: 6                                                                                                                          
0.514 V: mono_helper_ldstr_mscorlib                                                                                                    
0.514 * Assertion at ../../mono/arch/amd64/../x86/x86-codegen.h:410, condition `offset == (gint32)offset' not met                      
0.514                                                                                                                                  
0.515 
0.515 =================================================================
0.515 	Native Crash Reporting
0.515 =================================================================
0.515 Got a SIGABRT while executing native code. This usually indicates
0.515 a fatal error in the mono runtime or one of the native libraries 
0.515 used by your application.
0.515 =================================================================
0.518 
0.518 =================================================================
0.518 	Native stacktrace:
0.518 =================================================================
0.518 	0x40000c004b - mono : 
0.518 	0x40000c03dd - mono : 
0.518 	0x400006d087 - mono : 
0.518 	0x40000bf5cc - mono : 
0.518 	0x4001d2a3c0 - /lib/x86_64-linux-gnu/libpthread.so.0 : 
0.518 	0x40020cb18b - /lib/x86_64-linux-gnu/libc.so.6 : gsignal
0.518 	0x40020aa859 - /lib/x86_64-linux-gnu/libc.so.6 : abort
0.518 	0x400002f3c4 - mono : 
0.518 	0x4000314135 - mono : 
0.518 	0x40003315be - mono : 
0.518 	0x4000331c73 - mono : monoeg_assertion_message
0.518 	0x4000331cb0 - mono : mono_assertion_message_disabled
0.519 	0x4000095bb8 - mono : 
0.519 	0x40000c329b - mono : 
0.519 	0x40000c683b - mono : 
0.519 	0x40000c6b96 - mono : 
0.519 	0x40000381e2 - mono : 
0.519 	0x40000709c6 - mono : 
0.519 	0x4000071524 - mono : 
0.519 	0x4002806393 - Unknown
0.519 
0.519 =================================================================
0.519 	Telemetry Dumper:
0.519 =================================================================
0.522 Pkilling 0x274969323264x from 0x274914048960x
0.525 Entering thread summarizer pause from 0x274914048960x
0.525 Finished thread summarizer pause from 0x274914048960x.
0.525 Failed to create breadcrumb file (null)/crash_hash_0x384ca2be0
0.558 
0.558 Waiting for dumping threads to resume
1.567 
1.567 =================================================================
1.567 	External Debugger Dump:
1.567 =================================================================
1.571 mono_gdb_render_native_backtraces not supported on this platform, unable to find gdb or lldb
1.582 
1.582 =================================================================
1.582 	Basic Fault Address Reporting
1.582 =================================================================
1.582 Memory around native instruction pointer (0x40020cb18b):0x40020cb17b  d2 4c 89 ce bf 02 00 00 00 b8 0e 00 00 00 0f 05  .L..............
1.584 0x40020cb18b  48 8b 84 24 08 01 00 00 64 48 33 04 25 28 00 00  H..$....dH3.%(..
1.584 0x40020cb19b  00 75 26 44 89 c0 48 81 c4 18 01 00 00 c3 0f 1f  .u&D..H.........
1.584 0x40020cb1ab  80 00 00 00 00 48 8b 15 b9 4c 1a 00 f7 d8 41 b8  .....H...L....A.
1.585 
1.585 =================================================================
1.585 	Managed Stacktrace:
1.585 =================================================================
1.585 	  at <unknown> <0xffffffff>
1.585 	  at System.IO.UnexceptionalStreamWriter:.ctor <0x00053>
1.585 	  at System.IO.UnexceptionalStreamWriter:.ctor <0x0006f>
1.585 	  at System.Console:SetupStreams <0x00287>
1.585 	  at System.Console:.cctor <0x001bf>
1.585 	  at System.Object:runtime_invoke_void <0x0009d>
1.585 	  at <unknown> <0xffffffff>
1.586 	  at NuGet.Program:Main <0x000b3>
1.586 	  at <Module>:runtime_invoke_int_object <0x000a8>
1.586 =================================================================
1.586 qemu: uncaught target signal 6 (Aborted) - core dumped
1.592 Aborted
------
Dockerfile:16
--------------------
  14 |     WORKDIR /home/ubuntu/axiom-profiler
  15 |     ADD --chown=ubuntu:ubuntu https://nuget.org/nuget.exe nuget.exe
  16 | >>> RUN mono ./nuget.exe install Microsoft.Net.Compilers
  17 |     RUN xbuild /p:Configuration=Release source/AxiomProfiler.sln
  18 |     
--------------------
ERROR: failed to solve: process "/bin/sh -c mono ./nuget.exe install Microsoft.Net.Compilers" did not complete successfully: exit code: 134

Tracking of Backtracking During SMT Run

Created by bitbucket user nilsbecker_ on 2019-02-27 20:17

Log files generated by z3 already contain information on decisions and corresponding backtracking during the model search. It may be useful to display that information, e.g. when looking at high-branching behavior.

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?

Mono Interface Issues

Created by bitbucket user nilsbecker_ on 2019-02-27 19:55

When running the Axiom Profiler on Linux using Mono some of the text on the buttons on the right-hand-side ("Show Longest Path", etc.) is clipped and the highlighting in the panel left-hand-side is sometimes offset by a few characters.

Prefix Loading

Created by bitbucket user nilsbecker_ on 2019-02-27 20:12

It is currently possible to only load a prefix of a file by clicking "Cancel" while the file is loading. It would be nice to specify the number of lines to load from the beginning.

Smart Printing

Created by bitbucket user nilsbecker_ on 2019-02-27 20:10
Last updated on 2019-02-27 20:22

It is not uncommon that the bodies of quantifiers contain a number of implications which z3 rewrites into a big or clause. Oftentimes a user is only interested in one of the disjucts. At least when looking at paths or generalizations the tool should be able to tell which disjuncts are interesting based on which terms are used to trigger the next instantiation in the path (these terms are highlighted in yellow and blue). It may, therefore, be useful to be able to set a different printing depth for "interesting" terms than for other ones. This would especially be useful to reduce clutter when exploring deep term structures. The resulting representation may then look similar to:

#!

or(..., ..., >...<, >...<, ...,
    f(g(T+1, h(...))),
    >...<, >...<, >...<)

It may also be worth considering applying a similar technique to additional triggers of a quantifier that were not used to produce this instantiation.

Explain Path feature sometimes chooses a very small subset of the "obvious" path

Created by @alexanderjsummers on 2019-11-18 13:27

For example, loading the attached log file and clicking on the topmost node displayed yields a path of only length three; there are two reasonable choices available, and both should be longer.

Attachments:

heaps-simpler2.log

viperproject / axiom-profiler Goto Github PK

axiom-profiler's People

Stargazers

Watchers

Forkers

axiom-profiler's Issues

Z3 logfile

Source SMT file

Exception details

Recommend Projects

Recommend Topics

Recommend Org