boogie does not terminate

[rahxephon89]

Hi, when I tried to verify the following program boogie.bpl using the command:

boogie -doModSetAnalysis -printVerifiedProceduresCount:0 -printModel:1 -enhancedErrorMessages:1 -proverOpt:O:model_validate=true -proverOpt:PROVER_PATH=~/z3 -useArrayAxioms -proverOpt:O:smt.QI.EAGER_THRESHOLD=100 -proverOpt:O:smt.QI.LAZY_THRESHOLD=100 -vcsCores:4 -proverOpt:O:trace=true -proverOpt:O:trace_file_name=z3.trace -proverLog:@PROC@.smt boogie.bpl

boogie got stuck without terminating. Any hints on why it happens and/or how to debug it further? Thanks!

System spec:

Arch: Arm64
OS: Mac OS 15.1.1 
boogie version: tried both 3.2.4 and latest on main
z3 version: tried both 4.11.2 and 4.13.4

[wrwg]

It appears the problem here also manifests by ever growing memory (Boogie grows over 100g in some cases). Any idea what could cause this, and a possible option to turn off/on to prevent the memory growth?

[rahxephon89]

cc @shazqadeer

[shazqadeer]

The file is large. There is no magic. If I were to debug this problem, I would start by trying to minimize the size while not losing the issue. Can you try to do a bit of this? Then I will also try to help.

How many verification problems are present in the file?

Is there any non-linear arithmetic? If not, most likely the problem is due to quantifiers.

[wrwg]

The problem is not z3 here, with quantifiers and the like, but Boogie. We are observing that boogies memory grows unbounded (100GB and growing). Wondering what could cause this? Is there an algorithm inside Boogie which does constant rewriting of the VC such that it grows without bounds? We are used to this from Z3 but not from Boogie.

We also seeing no active z3 instance running and still Boogie using compute.

[shazqadeer]

Thanks for that clarification. Very interesting! I will take a look.

[wrwg]

Here is another boogie.bpl (1).txt which should clearly show the memory explosion, run as:

 boogie -doModSetAnalysis -printVerifiedProceduresCount:0 -printModel:1 -enhancedErrorMessages:0 -proverOpt:O:model_validate=true -proverOpt:PROVER_PATH=/Users/wrwg/bin/z3 -useArrayAxioms -proverOpt:O:smt.QI.EAGER_THRESHOLD=100 -proverOpt:O:smt.QI.LAZY_THRESHOLD=100 -vcsCores:4 boogie.bpl

[wrwg]

This thing actually verifies sometimes but othertimes finishes with SIGKILL, I guess because out of memory. It may pass on your machine, but on my Mac I can see with Activity Monitor how it goes over 100GB

[shazqadeer]

I tried the first file @rahxephon89 supplied. Boogie has been running on my Mac for about 12 minutes now and the memory consumption of Boogie appears to be holding steady at 2GB.

[wrwg]

To summarize our observation:

1. In the first example we see Boogie endlessly running with constant memory but no z3 instances. We never saw it terminating.
2. In the second example, we see Boogie starting to grow after a couple of minutes for over 100GB and then sometimes terminate with success, sometimes via SIGKILL (I guess .Net kills it because of memory use, or perhaps MacOS).

Perhaps these two issues are separate, perhaps have some related cause?

Thank you for any help. Unfortunately it is pretty hard to reproduce which of the tons of formulas causes it and which feature interaction contributes.

[rahxephon89]

@shazqadeer Here is a smaller example: boogie-bug.bpl.txt. It seems that procedure $c0de_emojicoin_dot_fun_register_market_inner$verify leads to hanging.

[shazqadeer]

In the first file that @rahxephon89 provided (titled boogie.bpl), line 58806 has a very large expression (more than 1700 nested occurrences of ConcatVec). It appears that you are trying to translate a very large constant vector. When I stepped through the debugger, I noticed a "hang" in Boogie VC generation at the place where this expression is being translated. This is even before the VC is being sent to the SMT solver. You should be able to replicate this problem by running boogie with the following options:

-doModSetAnalysis -trace boogie.bpl -proc:"\$c0de_emojicoin_dot_fun_init_module\$verify"

The -proc option verifies only the argument procedure. I stripped out all the other options you were using because they are relevant to SMT solving and model generation. The problem we are debugging is at the Boogie level.

This behavior is surprising to me. Even though the expression is large, I expect expression translation to have linear complexity. So it should not appear to "hang".

[shazqadeer]

If you would like to help debug the issue further, you could do the following:

1. Check that you are able to reproduce the problem according to my instructions
2. Try to isolate the large expression in a file by itself and see if the problem continues

Otherwise, I will try to make progress as I find time.

Are you blocked on this issue? You could consider getting unblocked for now by replacing the large constant vector with an uninterpreted constant. Perhaps the correctness of your program does not depend on the constant vector value.

[wrwg]

Shaz, thanks for looking into this. The first example is actually not blocking us right now, but the 2nd example I provided, where Boogie's memory goes over 100GB, brings us close to the point where we need to turn the Move prover off. We have worked around it by sharding verification in multiple Boogie files (so it only goes up to 80GB and passes on CI), but that seems fragile until a further butterfly.

As a background, we are creating large Boogie files with huge constants since years and never run into problems. Given the automatic generation of Boogie from Move, we can't just turn a constant easily into an uninterpreted function. But we will take a look for other solutions.

Could you confirm that in the internal architecture of Boogie, such large memory growth is something which could even happen outside of a bug? My understanding until now was there is no non-linear term rewriting or similar happening in Boogie.

[rahxephon89]

Hi @shazqadeer, the memory issue has been mitigated by making specs more opaque. I will try to debug the first issue and get back to you once there is anything interesting found. Thanks!

Update: confirmed that removing all large vector constants makes verification go through.