Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Stack overflow at Microsoft.Boogie.Type.GetHashCode() #4098

Open
muchang opened this issue May 29, 2023 · 2 comments
Open

Stack overflow at Microsoft.Boogie.Type.GetHashCode() #4098

muchang opened this issue May 29, 2023 · 2 comments
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: boogie Happens after passing the program to Boogie priority: not yet Will reconsider working on this when we're looking for work

Comments

@muchang
Copy link

muchang commented May 29, 2023

Dafny version

4.1.0

Code to produce this issue

No response

Command to run and resulting output

$ ./dafny/Binaries/Dafny /compile:0 main.dfy
Stack overflow.
   at Microsoft.Boogie.Type.GetHashCode()
   at System.Collections.Generic.Dictionary`2[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[Microsoft.Boogie.TypeErasure.MapTypeAbstractionBuilder+MapTypeClassRepresentation, Boogie.VCExpr, Version=2.16.4.0, Culture=neutral, PublicKeyToken=null]].FindValue(System.__Canon)
   at System.Collections.Generic.Dictionary`2[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[Microsoft.Boogie.TypeErasure.MapTypeAbstractionBuilder+MapTypeClassRepresentation, Boogie.VCExpr, Version=2.16.4.0, Culture=neutral, PublicKeyToken=null]].TryGetValue(System.__Canon, MapTypeClassRepresentation ByRef)
   at Microsoft.Boogie.TypeErasure.MapTypeAbstractionBuilder.GetClassRepresentation(Microsoft.Boogie.MapType)
   at Microsoft.Boogie.TypeErasure.MapTypeAbstractionBuilder.AbstractMapType(Microsoft.Boogie.MapType)
   at Microsoft.Boogie.TypeErasure.TypeAxiomBuilder.Type2Term(Microsoft.Boogie.Type, System.Collections.Generic.IDictionary`2<Microsoft.Boogie.TypeVariable,Microsoft.Boogie.VCExprAST.VCExpr>)
   at Microsoft.Boogie.TypeErasure.TypeAxiomBuilderPremisses.GenVarTypeAxiom(Microsoft.Boogie.VCExprAST.VCExprVar, Microsoft.Boogie.Type, System.Collections.Generic.IDictionary`2<Microsoft.Boogie.TypeVariable,Microsoft.Boogie.VCExprAST.VCExpr>)
   at Microsoft.Boogie.TypeErasure.TypeAxiomBuilderPremisses.AddVarTypeAxiom(Microsoft.Boogie.VCExprAST.VCExprVar, Microsoft.Boogie.Type)
   at Microsoft.Boogie.TypeErasure.TypeAxiomBuilder.Typed2Untyped(Microsoft.Boogie.VCExprAST.VCExprVar)
   at Microsoft.Boogie.TypeErasure.TypeEraser.Visit(Microsoft.Boogie.VCExprAST.VCExprVar, Microsoft.Boogie.TypeErasure.VariableBindings)
   at Microsoft.Boogie.VCExprAST.VCExprVar.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]].MutateSeq(System.Collections.Generic.IEnumerable`1<Microsoft.Boogie.VCExprAST.VCExpr>, System.__Canon)
   at Microsoft.Boogie.TypeErasure.OpTypeEraser.MutateSeq(Microsoft.Boogie.VCExprAST.VCExprNAry, Microsoft.Boogie.TypeErasure.VariableBindings, Int32)
   at Microsoft.Boogie.TypeErasure.OpTypeEraser.CastArgumentsToOldType(Microsoft.Boogie.VCExprAST.VCExprNAry, Microsoft.Boogie.TypeErasure.VariableBindings, Int32)
   at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitEqOp(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 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 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 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)
....

What happened?

Dafny throws out a stack overflow when verifying this program. It seems to be a Boogie crash. The bug trigger is hard to reduce further, but it would be okay to investigate the crash.

The trigger and the output log are too large to paste above. The complete files are attached here.
dafny_crash.zip

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

Linux
@muchang muchang added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label May 29, 2023
@keyboardDrummer
Copy link
Member

The root cause is this Boogie issue: boogie-org/boogie#711

@keyboardDrummer keyboardDrummer added the part: boogie Happens after passing the program to Boogie label May 30, 2023
@keyboardDrummer
Copy link
Member

keyboardDrummer commented May 30, 2023 •
edited
Loading

Through debugger I verified that this stack overflow occurs despite the thread using a 16 MB stack. This is the same stack size as was used in Boogie versions such as 2.8.6: https://github.com/boogie-org/boogie/blob/v2.8.6/Source/ExecutionEngine/ExecutionEngine.cs#L439

@keyboardDrummer keyboardDrummer added the crash Dafny crashes on this input, or generates malformed code that can not be executed label Dec 18, 2023
@keyboardDrummer keyboardDrummer added the during 2: compilation of correct program Dafny rejects a valid program during compilation label Feb 7, 2024
@keyboardDrummer keyboardDrummer added the priority: not yet Will reconsider working on this when we're looking for work label Apr 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: boogie Happens after passing the program to Boogie priority: not yet Will reconsider working on this when we're looking for work
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@keyboardDrummer @muchang