search

dafny-lang / ide-vscode

VSCode IDE Integration for Dafny
https://marketplace.visualstudio.com/items?itemName=dafny-lang.ide-vscode
MIT License
21 stars 18 forks source link

Dafny IDE bombs on long string #313

Open sarsko opened 1 year ago

sarsko commented 1 year ago

Failing code

method Main()
{
    var i := 3;
    var inp := "123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890";
    while i < |inp| {
        i := i + 1;
    }

}

Steps to reproduce the issue

Expected behavior

No crash.

Actual behavior

Crash.

I get the following output:

Stack overflow.
Repeat 1010 times:
--------------------------------
   at Microsoft.Boogie.AbstractInterpretation.ThresholdFinder.VisitNAryExpr(Microsoft.Boogie.NAryExpr)
   at Microsoft.Boogie.NAryExpr.StdDispatch(Microsoft.Boogie.StandardVisitor)
   at Microsoft.Boogie.ReadOnlyVisitor.Visit(Microsoft.Boogie.Absy)
   at Microsoft.Boogie.ReadOnlyVisitor.VisitExpr(Microsoft.Boogie.Expr)
   at Microsoft.Boogie.ReadOnlyVisitor.VisitExprSeq(System.Collections.Generic.IList`1<Microsoft.Boogie.Expr>)
--------------------------------
   at Microsoft.Boogie.AbstractInterpretation.ThresholdFinder.VisitNAryExpr(Microsoft.Boogie.NAryExpr)
   at Microsoft.Boogie.NAryExpr.StdDispatch(Microsoft.Boogie.StandardVisitor)
   at Microsoft.Boogie.ReadOnlyVisitor.Visit(Microsoft.Boogie.Absy)
   at Microsoft.Boogie.ReadOnlyVisitor.VisitExpr(Microsoft.Boogie.Expr)
   at Microsoft.Boogie.ReadOnlyVisitor.VisitAssignCmd(Microsoft.Boogie.AssignCmd)
   at Microsoft.Boogie.AssignCmd.StdDispatch(Microsoft.Boogie.StandardVisitor)
   at Microsoft.Boogie.ReadOnlyVisitor.Visit(Microsoft.Boogie.Absy)
   at Microsoft.Boogie.AbstractInterpretation.ThresholdFinder.Find(System.Collections.Generic.List`1<System.Numerics.BigInteger> ByRef, System.Collections.Generic.List`1<System.Numerics.BigInteger> ByRef)
   at Microsoft.Boogie.AbstractInterpretation.NativeIntervalDomain.Specialize(Microsoft.Boogie.Implementation)
   at Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.ComputeProgramInvariants(Microsoft.Boogie.Program, System.Collections.Generic.Dictionary`2<Microsoft.Boogie.Procedure,Microsoft.Boogie.Implementation[]>, Microsoft.Boogie.AbstractInterpretation.NativeLattice)
   at Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(Microsoft.Boogie.Program)
   at Microsoft.Boogie.ExecutionEngine.PreProcessProgramVerification(Microsoft.Boogie.Program)
   at Microsoft.Boogie.ExecutionEngine.GetImplementationTasks(Microsoft.Boogie.Program)
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier+<>c__DisplayClass9_0.<GetVerificationTasksAsync>b__0(System.Tuple`2<System.String,Microsoft.Boogie.Program>)
   at System.Linq.Enumerable+SelectManySingleSelectorIterator`2[[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]].ToList()
   at System.Linq.Enumerable.ToList[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](System.Collections.Generic.IEnumerable`1<System.__Canon>)
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier+<GetVerificationTasksAsync>d__9.MoveNext()
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[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]].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.__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]].MoveNext(System.Threading.Thread)
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[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]].ExecuteFromThreadPool(System.Threading.Thread)
   at System.Threading.ThreadPoolWorkQueue.Dispatch()
   at System.Threading.PortableThreadPool+WorkerThread.WorkerThreadStart()
   at System.Threading.Thread.StartCallback()
[Info  - 11:40:14 PM] Connection to server got closed. Server will restart.

The following popup also comes up:

The Dafny Language Server server crashed 5 times in the last 3 minutes. The server will not be restarted.

(I am writing long strings because I wanted to do Advent of Code, and did not want to bother with figuring out how to parse stuff. Sorry.)

keyboardDrummer commented 1 year ago

One action item is changing the language server so it doesn't crash if an exception occurs in Microsoft.Boogie.ExecutionEngine.GetImplementationTasks