Stack overflow with long-ish seq #5471
Comments
hmijail
added
the
kind: bug
|
Same issue, albeit with different information: boogie-org/boogie#711 |
|
This issue is difficult to solve. We'll solve it at some point but I'd rather deprioritize it for now. How pressing is it for you? |
|
Well... quite. This bug seems to lock us into using Dafny <=4.4 for a project, and unfortunately 4.4 seems to have trouble with --resource-limit and with resource usage logging (i.e., "valid" outcomes with resource count -1, either with or without isolated assertions). This kills the tools I've been building to diagnose slow/brittle verification, which is currently a huge pain point. I'll check if earlier versions have better resource accounting. |
|
Can you work around the issue by doing something like: ? I can also add a hidden option to Dafny that allows customizing the used stack size, which would allow you to raise the length limit of the sequence. |
|
That works! I don't get it. I DID try with But that causes the same stack overflow. Happy to push forward with your version, but if there is some insight I'm missing here, I'd love to know! |
MikaelMayer
added
the
part: verifier
Dafny version4.7 Code to produce this issuemain.dfy: module M {
/* Given a list of numbers, check if any two sums to 0. */
method {:testEntry} two_sum(numbers: seq<real>) returns (b: bool)
{
b := false;
var n := |numbers|;
if n > 1 {
var i, j := 0, 1;
while i < n - 1
decreases n - i
{
while j < n
decreases n - j
{
var sum := numbers[j] + numbers[i];
if sum == 0.0 || sum == 0.0 {
b := true;
return;
}
j := j + 1;
}
i := i + 1;
}
}
}
}Command to run and resulting outputdafny generate-tests InlinedBlock main.dfy > main_test.dfy
dafny run main_test.dfyWhat happened?
When What type of operating system are you experiencing the problem on?Mac |
|
Execution might be more related to compilation, and then that'd be #3759? ... or maybe all go together...? |
|
I believe verification is attempted before both execution and compilation, which seems to be the underlying cause here |
Your bug report didn't provide a stack trace, but I'm guessing you're saying the stack overflow occurs in Boogie, just like @hmijail 's, which is why you're saying this relates to verification. |
Dafny version
4.6
Code to produce this issue
Command to run and resulting output
What happened?
The given code verifies correctly up to dafny 4.4.
Since then, up to today's nightly (4.6+), verification fails with a Stack Overflow.
Beware, the behavior is very confusing.
dafny verify example.dfymight fail a number of times, and then start working correctly for a good number of times.dafny measure-complexity --iterations 10fails much more reliably (as soon as the 2nd iteration).The exact contents of the stack overflow trace kept changing as I reduced the code for this issue. The last case was this one:
What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered: