Boogie not Terminating with Prune on

[yizhou7]

I am exporting some boogie files from some Dafny code.
I noticed that for some of them (attached in the zip file):
they terminate properly if /prune is not turned on,
but they do not seem to terminate if /prune is turned on.

For example, this would stop after about 11 seconds on my machine:

dotnet tool run boogie /timeLimit:1 /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 boogies/Impl-HandleWriteResponseImpl.i.dfy.bpl

But this would run for more than a minute so I have to kill it:

dotnet tool run boogie /timeLimit:1 /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 boogies/Impl-HandleWriteResponseImpl.i.dfy.bpl /prune

I am running Ubuntu 20.04, boogie 3.0.4.0, .NET SDK 6.0.412.

My unsubstantiated guess is that it might be a problem with how Booige is interacting with Z3,
since both the dotnet and the z3 process are in interruptable sleep after a while,
neither using any CPU, but also not terminating.

nonterminating.zip

[shazqadeer]

You are better off asking this question in the Dafny forum. /prune is an experimental feature in Boogie currently used only in Dafny.

cc: @atomb , @RustanLeino , @keyboardDrummer

[keyboardDrummer]

I'm guessing that your program is missing pruning annotations, so pruning causes it be incorrect and this causes the SMT solver to hang and Boogie to wait indefinitely for an answer from the solver.

[yizhou7]

@keyboardDrummer could you provide some context on the pruning annotations? Are there special assumptions made by Boogie for /prune to be used?

These boogie files were generated by an older version of Dafny on an old project (Veribetrkv https://github.com/secure-foundations/veribetrkv-osdi2020). Is it unreasonable to expect the boogie to work on these? (They actually mostly verify without the /prune option on, but run into issues with /prune).

[keyboardDrummer]

These boogie files were generated by an older version of Dafny on an old project (Veribetrkv https://github.com/secure-foundations/veribetrkv-osdi2020). Is it unreasonable to expect the boogie to work on these?

I think the upcoming version of Dafny may correct print uses annotations when printing Boogie files, but older versions will not.

Could you check if this change to the /prune help answers your remaining questions? https://github.com/boogie-org/boogie/pull/793/files

[zafer-esen]

I think the upcoming version of Dafny may correct print uses annotations when printing Boogie files, but older versions will not.

This was fixed by Boogie #765, it should work with nightly Dafny (or any version of Dafny that uses Boogie >= 3.0.1).

Another thing about running Boogie directly on the printed file: the default type encoding in Boogie is currently \typeEncoding:m (monomorphic). Dafny until recently used \typeEncoding:p (predicates) and now it uses \typeEncoding:a (arguments). You might want to specify a type encoding other than m for the following reasons.

• If you use m it might be a good idea to also use the Boogie option \useArrayAxioms, since otherwise the array functions become interpreted and this might cause issues in the axiomatization of Dafny types, where those functions are used in triggers (for instance the axiomatization of heaps).

• If you are using an older version of Dafny and if you plan on using the monomorphic encoding, in addition to what is written in the documentation provided by @keyboardDrummer , you should also put axioms that only quantify over the polymorphic type inside uses clauses, such as this one. One such axiom (maybe the one I linked) was not inside a uses clause in older versions of Dafny. This is not an issue in other type encodings.

[yizhou7]

Could you check if this change to the /prune help answers your remaining questions? https://github.com/boogie-org/boogie/pull/793/files

Thank you @keyboardDrummer for the pointer, I think that clarifies things quite a bit,
and thank you @zafer-esen for detailed tips on the type encoding options.

I am trying to evaluate how well pruning works in reducing instability.

From the responses above, I have the following impression:

1. If I intend to use prune, there needs to be special care in declaring the dependencies (along with the type encoding) when generating the boogie code, otherwise Boogie might be too aggressive in reducing the context.
2. These annotations are not emitted by older versions of Dafny.
3. It is therefore unreasonable to use boogie files exported from projects written in older versions of Dafny, and expect the newest Booige can show the effectiveness of prune.
4. What might be more useful is a project written in a the up-to-date version of Dafny.

Are these the correct impression? I have ran some experiments, which shows that 3 might be true.

[zafer-esen]

1 is correct - basically you need to move all axioms without triggers into uses clauses of functions and constants, where you want these axioms to be available. This also includes axioms that only quantify over a polymorphic type when using \typeEncoding:m, because those axioms lose their quantifiers during monomorphization.

For 3, I think you can still add the {:include_dep} attribute to axioms without triggers (+ those that only quantify over polymorphic types if using monomorphization), if that is feasible to do, and pruning should work correctly on your exported Boogie files. That would be equivalent to adding those axioms to the uses clauses of all symbols appearing in that axiom. Here is an example.

If you want to dive into Boogie to automate this, you can remove the if condition here, but just doing this would affect axioms with triggers too and weaken pruning. You can also update the logic here to only do this automatically in axioms without triggers.