Documentation: hard to figure out how to run Boogie manually

[tchajed]

For debugging particularly tricky problems I think at some point you need to drop down to the Boogie level. Currently it's kind of tricky to run the same version of Boogie that Dafny is using, because it seems to call it via a DLL. Would it be possible to expose it? Or at least point to Boogie installation instructions?

When I did go and follow the Boogie installation instructions I also had to get the .NET 3.1 runtime because Dafny is using .NET 5 and Boogie wasn't compatible with it - that might just be a separate Boogie issue.

[RustanLeino]

I do this all the time when debugging Dafny itself. It is doable and simple--once you know how. :/ It would be good to document this. Here is a start to that documentation:

• The version of Boogie that Dafny depends on is listed in the Directory.Build.props file. Currently, this is Boogie version 2.8.26. You can download the Boogie binaries from https://github.com/boogie-org/boogie/releases.

• Currently, Boogie uses .NET Core 3.1, so you need to install it. (Dafny is a .NET 5.0 program. As it turns out, with only .NET 5.0 installed on your machine, a .NET 5.0 program like Dafny can still call into a .NET Core 3.1 library like Boogie. But to invoke a .NET Core 3.1 program an an executable, you need to install .NET Core 3.1.)

• You'll need to use the same version of Z3 for Boogie as you use for Dafny. The version of Z3 that Dafny depends on is listed in package.py. Currently, this is Z3 version 4.8.5. If you're running Dafny on your machine, you should already have Z3 in the z3/bin subdirectory of the Dafny binaries directory. Boogie will pick up Z3 from your PATH.

• Dafny calls Boogie with certain options. You'll find these in the ApplyDefaultOptions() and SetZ3Options() methods in DafnyOptions.cs. They are:

  • /infer:j
  • /proverOpt:O:auto_config=false
  • /proverOpt:O:type_check=true
  • /proverOpt:O:smt.case_split=3
  • /proverOpt:O:smt.qi.eager_threshold=100
  • /proverOpt:O:smt.delay_units=true
  • /proverOpt:O:smt.arith.solver=2

• To output the Boogie program that Dafny generates, use the /print option. For example:

  dafny MyProgram.dfy /print:d.bpl

  You can now run Boogie directly on the resulting file, d.bpl. This allows you to read and edit d.bpl. If you have a multi-module Dafny program (or especially if a Dafny bug produces malformed Boogie), the output file may have some name like d__MyModule.bpl (this can sometimes be confusing, especially if there's also a d.bpl file, because Boogie still uses the name d.bpl in its diagnostic messages).

• When doing this kind of debugging, I find that the Boogie options /timeLimit and /proc are helpful. (These options are also available from the Dafny command line.) For example,

  boogie d.bpl /timeLimit:10 /proc:"*MyProc"

[tchajed]

This documentation looks great to me, thanks Rustan! I didn't know about the default Boogie options but that does seem important.

[hmijail]

I'm looking into using Axiom Profiler to try to help improve verification times. Given the changing Dafny / Boogie interface, plus functionalities like Dafny's --isolate-assertions, --random-seed, it'd be great to have more clarity on how to get insight into a reproducible end-to-end verification - from Dafny code to Z3 proof log.

Or even, would it be possible to have an option for the toolchain to dump the proper intermediate products it generated?

Currently I'm making do with dafny's --bprint (marked as internal), and then trying various boogie / z3 options until something seems to work. But I think that in this way I am losing most of the work already done by dafny itself, plus possibly butchering the whole thing, let alone getting something reproducible.

[keyboardDrummer]

I'm looking into using Axiom Profiler to try to help improve verification times. Given the changing Dafny / Boogie interface, plus functionalities like Dafny's --isolate-assertions, --random-seed, it'd be great to have more clarity on how to get insight into a reproducible end-to-end verification - from Dafny code to Z3 proof log.

Or even, would it be possible to have an option for the toolchain to dump the proper intermediate products it generated?

Currently I'm making do with dafny's --bprint (marked as internal), and then trying various boogie / z3 options until something seems to work. But I think that in this way I am losing most of the work already done by dafny itself, plus possibly butchering the whole thing, let alone getting something reproducible.

How far do you get with the information @RustanLeino provided above?

Or even, would it be possible to have an option for the toolchain to dump the proper intermediate products it generated?

Next step could be that --bprint also prints out a boogie CLI invocation that uses the correct arguments, although that is somewhat surprising not too easy to generate from Dafny's programmatic use of Boogie :-)

[hmijail]

How far do you get with the information @RustanLeino provided above?

As it is, I think the only information that still kinda-works is the /print / --bprint.

As for boogie options, I already have a set of options that "generate something" after experimenting with the (even more outdated) info at AxiomProfiler Dafny wiki page. Then I found this issue, but realized that the mentioned ApplyDefaultOptions() and SetZ3Options() links are dead in the current tree, so I thought better to ask instead of keeping blindly trying even more options.

For a concrete example: I couldn't find a difference between what is --bprinted with and without --isolate-assertions - nor any other option to carry forward those isolated assertions down the chain. For example, would it be similar to using the @PROC@ boogie macros, as in /proverOpt:LOG_FILE=input-@PROC@.log? Looks like it might, but feels wrong to be reverse-engineering this kind of thing.

[keyboardDrummer]

For a concrete example: I couldn't find a difference between what is --bprinted with and without --isolate-assertions - nor any other option to carry forward those isolated assertions down the chain.

--isolate-assertions becomes /vcsSplitOnEveryAssert in Boogie.

[hmijail]

My use case is that I have an interesting run of e.g. dafny measure-complexity [--isolate-assertions] --random-seed X --iterations 10 --log json myfile.dfy , where one specific function (or Assertion Batch) with a specific Random Seed failed to verify. Let's say I want to examine what's going on in Axiom Profiler. How can one drill into that function (or AB) and RS down to the z3 proof log?

I can see /vcsSplitOnEveryAssert being one piece of the puzzle, but is that all? For example, the Dafny reference manual mentions that the randomness is automatically implemented by modifying details of the source code. Does that happen in Dafny (and then I need a bpl file specific to the RS), or does that happen in Boogie (and then I only need to pass the RS to Boogie together with the generic bpl)?

My basic assumption is that by narrowing down the scope at the dafny level I will have an easier time in Axiom Profiler. The mentions of boogie's /proc imply the same. But maybe AP really requires good understanding of the whole dafny-boogie-z3 transformations, and then asking for help at the dafny level makes no sense?

[keyboardDrummer]

My use case is that I have an interesting run of e.g. dafny measure-complexity [--isolate-assertions] --random-seed X --iterations 10 --log json myfile.dfy , where one specific function (or Assertion Batch) with a specific Random Seed failed to verify

Our advice is to debug such problems at the Dafny level. Here's a piece of documentation that can help with that: https://dafny.org/dafny/DafnyRef/DafnyRef#sec-brittle-verification It links to two other pages that contain most of the information, so be sure to check those out.

I can see /vcsSplitOnEveryAssert being one piece of the puzzle, but is that all? For example, the Dafny reference manual mentions that the randomness is automatically implemented by modifying details of the source code. Does that happen in Dafny (and then I need a bpl file specific to the RS), or does that happen in Boogie (and then I only need to pass the RS to Boogie together with the generic bpl)?

That happens in Boogie, although I'm only 50% sure that passing the RS to Boogie will give the same results.