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.

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:

• nils-z3.log.gz
• foo.bpl
• z3.log

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

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.

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:

• z3-shortened2.log
• with-wands.smt2-11.smt2

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

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

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:

• nested.log
• test-test_1.smt

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

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

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?

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

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.

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

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

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.