Hang with dafny verify on Std

[atomb]

Dafny version

5cf477a

Code to produce this issue

dafny/Source/DafnyStandardLibraries/src/Std/Strings.dfy

Lines 84 to 93 in 73fcdf3

	function {:vcs_split_on_every_assert} ToNat(str: String) : (n: nat)
	requires forall c <- str :: IsDigitChar(c)
	{
	if str == [] then 0
	else
	LemmaMulNonnegativeAuto();
	var c := str[|str| - 1];
	assert IsDigitChar(c);
	ToNat(str[..|str| - 1]) * base + charToDigit[c]
	}

Command to run and resulting output

(In Source/DafnyStandardLibraries/src/Std)

$ dafny verify dfyconfig.toml --boogie-filter "*Strings.ParametricConversion*ToNat*"

(hangs with 0% CPU use after a minute or so)

$ dafny /compile:0 /readsClausesOnMethods:1 /proc:"*Strings.ParametricConversion*ToNat*" `find . -name "*.dfy" | grep -v TargetSpecific`

Dafny program verifier finished with 7 verified, 0 errors
$

What happened?

Even with --cores 1, dafny verify hangs, but the old-style CLI works correctly.

What type of operating system are you experiencing the problem on?

Mac

[keyboardDrummer]

I think I have a partial understanding of why this bug occurs. It occurs when using dafny verify with --boogie-filter and --isolate-assertions (or equivalent), and was introduced in #5031

Dafny is waiting for all the assertion batches to complete, but Boogie is skipping some of them, without telling Dafny, so Dafny keeps waiting.

If you set a verification time limit and wait for that to pass, does it return an internal error? If yes that would confirm the above.

I'm inclined to remove support for --boogie-filter from dafny verify since we have --filter-symbol now, which does the skipping on the Dafny level, and it's not easy to fix --boogie-filter here. PR: #5090

[atomb]

Yep, I think you're right. I do get an internal error when adding a time limit.

I like the ability to use wildcards to limit to everything in a given module, or even a subset of definitions in a module. Do you have any plans for a filtering option that allows that, using Dafny-centric names?

[atomb]

When running dafny verify dfyconfig.toml --filter-symbol "Strings.ParametricConversion", I still get a hang. Is filtering by module expected to work? And, if not, we should have an error message instead of a hang.

[atomb]

For context, this came about when trying to verify the standard libraries with --warn-{redundant,contradictory}-assumptions. The process was hanging, which it doesn't when using old-style options. I used --boogie-filter to try to identify which definition was leading to the hang, under the hypothesis that this might be occurring due to a Z3 crash.

I just double-checked, and can confirm that this hang is still happening with dafny verify (even with --cores 1), but not with old-style options (even with multiple cores).

[keyboardDrummer]

When running dafny verify dfyconfig.toml --filter-symbol "Strings.ParametricConversion", I still get a hang. Is filtering by module expected to work? And, if not, we should have an error message instead of a hang.

Should work yes. Did you add a timelimit when doing this to check whether it's a bug instead of a verification taking long problem?

I like the ability to use wildcards to limit to everything in a given module, or even a subset of definitions in a module. Do you have any plans for a filtering option that allows that, using Dafny-centric names?

Can you not already do that with --filter-symbol ? It doesn't accept wildcards but it uses Contains, so there's an implicit wildcard to the left and right.

[keyboardDrummer]

Closing because we've removed support for --boogie-filter