search

dafny-lang / dafny

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

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

Open muchang opened 1 year ago

muchang commented 1 year ago

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

keyboardDrummer commented 1 year ago

The root cause is this Boogie issue: https://github.com/boogie-org/boogie/issues/711

keyboardDrummer commented 1 year ago

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