search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.91k stars 261 forks source link

Stack overflow occurs when running dafny, resulting in crash #3803

Closed TonyZhangND closed 1 year ago

TonyZhangND commented 1 year ago

Dafny version

4.0, 3.13, 3.12, 3.11, 3.10

Code to produce this issue

No response

Command to run and resulting output

command is

dafny /timeLimit:20 /compile:0  /allowGlobals /vcsCores:2 applicationProof.dfy

Output is 

Stack overflow.
   at Microsoft.Boogie.VCExprAST.VCExprNAry.get_Arguments()
   at Microsoft.Boogie.TypeErasure.OpTypeEraserPremisses.VisitBoogieFunctionOp(Microsoft.Boogie.VCExprAST.VCExprNAry, Microsoft.Boogie.TypeErasure.VariableBindings)
   at Microsoft.Boogie.VCExprAST.VCExprBoogieFunctionOp.Accept[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](Microsoft.Boogie.VCExprAST.VCExprNAry, Microsoft.Boogie.VCExprAST.IVCExprOpVisitor`2<System.__Canon,System.__Canon>, System.__Canon)
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](Microsoft.Boogie.VCExprAST.IVCExprOpVisitor`2<System.__Canon,System.__Canon>, System.__Canon)
   at Microsoft.Boogie.TypeErasure.TypeEraser.Visit(Microsoft.Boogie.VCExprAST.VCExprNAry, Microsoft.Boogie.TypeErasure.VariableBindings)
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](Microsoft.Boogie.VCExprAST.IVCExprVisitor`2<System.__Canon,System.__Canon>, System.__Canon)
   at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].Visit(Microsoft.Boogie.VCExprAST.VCExprNAry, System.__Canon)
   at Microsoft.Boogie.TypeErasure.TypeEraser.Visit(Microsoft.Boogie.VCExprAST.VCExprNAry, Microsoft.Boogie.TypeErasure.VariableBindings)
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](Microsoft.Boogie.VCExprAST.IVCExprVisitor`2<System.__Canon,System.__Canon>, System.__Canon)
   at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].Mutate(Microsoft.Boogie.VCExprAST.VCExpr, System.__Canon)
   at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitImpliesOp(Microsoft.Boogie.VCExprAST.VCExprNAry, Microsoft.Boogie.TypeErasure.VariableBindings)
   at Microsoft.Boogie.VCExprAST.VCExprOp.Accept[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](Microsoft.Boogie.VCExprAST.VCExprNAry, Microsoft.Boogie.VCExprAST.IVCExprOpVisitor`2<System.__Canon,System.__Canon>, System.__Canon)
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](Microsoft.Boogie.VCExprAST.IVCExprOpVisitor`2<System.__Canon,System.__Canon>, System.__Canon)
   at Microsoft.Boogie.TypeErasure.TypeEraser.Visit(Microsoft.Boogie.VCExprAST.VCExprNAry, Microsoft.Boogie.TypeErasure.VariableBindings)

    ...

   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[System.Threading.Tasks.VoidTaskResult, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].ExecutionContextCallback(System.Object)
   at System.Threading.ExecutionContext.RunInternal(System.Threading.ExecutionContext, System.Threading.ContextCallback, System.Object)
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[System.Threading.Tasks.VoidTaskResult, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].MoveNext(System.Threading.Thread)
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[System.Threading.Tasks.VoidTaskResult, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].MoveNext()
   at System.Threading.Tasks.AwaitTaskContinuation.RunOrScheduleAction(System.Runtime.CompilerServices.IAsyncStateMachineBox, Boolean)
   at System.Threading.Tasks.Task.RunContinuations(System.Object)
   at System.Threading.Tasks.Task.FinishContinuations()
   at System.Threading.Tasks.Task`1[[System.Char, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].TrySetResult(Char)
   at SMTLib.SExprParser+<SkipWs>d__8.MoveNext()
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[System.Char, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[SMTLib.SExprParser+<SkipWs>d__8, Boogie.Provers.SMTLib, Version=2.16.0.0, Culture=neutral, PublicKeyToken=null]].ExecutionContextCallback(System.Object)
   at System.Threading.ExecutionContext.RunFromThreadPoolDispatchLoop(System.Threading.Thread, System.Threading.ExecutionContext, System.Threading.ContextCallback, System.Object)
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[System.Char, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[SMTLib.SExprParser+<SkipWs>d__8, Boogie.Provers.SMTLib, Version=2.16.0.0, Culture=neutral, PublicKeyToken=null]].MoveNext(System.Threading.Thread)
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[System.Char, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[SMTLib.SExprParser+<SkipWs>d__8, Boogie.Provers.SMTLib, Version=2.16.0.0, Culture=neutral, PublicKeyToken=null]].ExecuteFromThreadPool(System.Threading.Thread)
   at System.Threading.ThreadPoolWorkQueue.Dispatch()
   at System.Threading.PortableThreadPool+WorkerThread.WorkerThreadStart()
   at System.Threading.Thread.StartCallback()


### What happened?

Stack overflow occurs in multiple dafny versions on both Intel and M2 macs. 
I can only make the error occur on large dafny projects of a couple thousand lines.
Error occurs more readily (smaller projects) with vcsCores >1, but also happens on 1 core when more lines of code are present. 

Here is the project in which the error occurs.

[paxos.zip](https://github.com/dafny-lang/dafny/files/11081524/paxos.zip)

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

Mac
TonyZhangND commented 1 year ago

I suspect it is PR 524 in Boogie that reduced the stack size, making it susceptible to stack overflows.

I verified that this bug is triggered in all versions of Dafny >= 3.6, and is not triggered in 3.5.0.

kumom commented 1 year ago

Did you get the same result if you run the code in VS Code? Because VS Code shows Verification succeeded while calling Dafny from terminal results stack overflow, outputting the exact same message that you produced here. My code is only around 300 lines.