Internal error during verification

[seebees]

Dafny version

4.8.1

Code to produce this issue

The PR is here: aws/aws-cryptographic-material-providers-library#806

The file that is failing to verify in that PR: https://github.com/aws/aws-cryptographic-material-providers-library/pull/806/files#diff-ed5b8971fe7fff55f2444af19903591bee0b44bc8b78be7bc1b23a37feda0d43

Here is the error: https://github.com/aws/aws-cryptographic-material-providers-library/actions/runs/11173345447/job/31061290595?pr=806#step:9:1403

Command to run and resulting output

dafny verify AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy --function-syntax:3 --unicode-char:false --resource-limit 1000000 --log-format:csv --boogie /trace --verification-time-limit 20

What happened?

Encountered internal compilation exception: Exception of type 'cce+UnreachableException' was thrown.
dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy(129,14): Error: Internal error occurred during verification: Exception of type 'cce+UnreachableException' was thrown.
at Microsoft.Dafny.BoogieGenerator.ExpressionTranslator.TrExpr(Expression expr)
at Microsoft.Dafny.BoogieGenerator.ExpressionTranslator.TrExpr(Expression expr)
at Microsoft.Dafny.BoogieGenerator.ExpressionTranslator.TrExpr(Expression expr)
at Microsoft.Dafny.BoogieGenerator.ExpressionTranslator.TrInSet_Aux(IToken tok, Expr elmt, Expr elmtBox, Expression s, Boolean aggressive, Boolean& performedRewrite)
at Microsoft.Dafny.BoogieGenerator.InRWClause_Aux(IToken tok, Expr o, Expr boxO, Expr f, List1 rw, Boolean usedInUnchanged, ExpressionTranslator etran, Expression receiverReplacement, Dictionary2 substMap)
at Microsoft.Dafny.BoogieGenerator.InRWClause(IToken tok, Expr o, Expr f, List1 rw, Boolean useInUnchanged, ExpressionTranslator etran, Expression receiverReplacement, Dictionary2 substMap)
at Microsoft.Dafny.BoogieGenerator.InRWClause(IToken tok, Expr o, Expr f, List1 rw, ExpressionTranslator etran, Expression receiverReplacement, Dictionary2 substMap)
at Microsoft.Dafny.BoogieGenerator.CheckFrameSubset(IToken tok, List1 calleeFrame, Expression receiverReplacement, Dictionary2 substMap, ExpressionTranslator etran, IdentifierExpr enclosingFrame, Action4 MakeAssert, ProofObligationDescription desc, QKeyValue kv) Unhandled exception. cce+UnreachableException: Exception of type 'cce+UnreachableException' was thrown. at Microsoft.Dafny.BoogieGenerator.ExpressionTranslator.TrExpr(Expression expr) at Microsoft.Dafny.BoogieGenerator.ExpressionTranslator.TrExpr(Expression expr) at Microsoft.Dafny.BoogieGenerator.ExpressionTranslator.TrExpr(Expression expr) at Microsoft.Dafny.BoogieGenerator.ExpressionTranslator.TrInSet_Aux(IToken tok, Expr elmt, Expr elmtBox, Expression s, Boolean aggressive, Boolean& performedRewrite) at Microsoft.Dafny.BoogieGenerator.InRWClause_Aux(IToken tok, Expr o, Expr boxO, Expr f, List1 rw, Boolean usedInUnchanged, ExpressionTranslator etran, Expression receiverReplacement, Dictionary2 substMap) at Microsoft.Dafny.BoogieGenerator.InRWClause(IToken tok, Expr o, Expr f, List1 rw, Boolean useInUnchanged, ExpressionTranslator etran, Expression receiverReplacement, Dictionary2 substMap) at Microsoft.Dafny.BoogieGenerator.InRWClause(IToken tok, Expr o, Expr f, List1 rw, ExpressionTranslator etran, Expression receiverReplacement, Dictionary2 substMap) at Microsoft.Dafny.BoogieGenerator.ProcessCallStmt(CallStmt cs, Dictionary2 tySubst, Expr bReceiver, List1 Lhss, List1 LhsTypes, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) at Microsoft.Dafny.BoogieGenerator.CheckFrameSubset(IToken tok, List1 calleeFrame, Expression receiverReplacement, Dictionary2 substMap, ExpressionTranslator etran, IdentifierExpr enclosingFrame, Action4 MakeAssert, ProofObligationDescription desc, QKeyValue kv)
at Microsoft.Dafny.BoogieGenerator.ProcessCallStmt(CallStmt cs, Dictionary2 tySubst, Expr bReceiver, List1 Lhss, List1 LhsTypes, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran)
at Microsoft.Dafny.BoogieGenerator.TrCallStmt(CallStmt s, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran, IdentifierExpr actualReceiver) at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran)
at Microsoft.Dafny.BoogieGenerator.TrUpdateStmt(BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran, UpdateStmt statement) at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran)
at Microsoft.Dafny.BoogieGenerator.TrStmtList(List1 stmts, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran, RangeToken scopeRange, Boolean processLabels)
at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) at Microsoft.Dafny.BoogieGenerator.TrMethodBody(Method m, BoogieStmtListBuilder builder, List1 localVariables, ExpressionTranslator etran)
at Microsoft.Dafny.BoogieGenerator.AddMethodImpl(Method m, Procedure proc, Boolean wellformednessProc)
at Microsoft.Dafny.BoogieGenerator.AddMethod_Top(Method m, Boolean isByMethod, Boolean includeAllMethods)
at Microsoft.Dafny.BoogieGenerator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType)
at Microsoft.Dafny.BoogieGenerator.AddRevealableTypeDecl(RevealableTypeDecl d)
at Microsoft.Dafny.BoogieGenerator.DoTranslation(Program p, ModuleDefinition forModule)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.<>c__DisplayClass3_0.b__0()
at System.Threading.Tasks.Task1.InnerInvoke() at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj) at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state) --- End of stack trace from previous location --- at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state) at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread) --- End of stack trace from previous location --- at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken) at Microsoft.Dafny.Compilation.<>c__DisplayClass54_0.<<VerifyUnverifiedSymbol>b__1>d.MoveNext() at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed) at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed) at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed) at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed) at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed) at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable1 randomSeed)+System.Threading.Tasks.Sources.IValueTaskSource<System.Boolean>.GetResult()
at System.Linq.AsyncEnumerable.ToObservableObservable1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 50 --- End of stack trace from previous location --- at System.Reactive.PlatformServices.ExceptionServicesImpl.Rethrow(Exception exception) in /_/Rx.NET/Source/src/System.Reactive/Internal/ExceptionServicesImpl.cs:line 16 at System.Reactive.ExceptionHelpers.Throw(Exception exception) in /_/Rx.NET/Source/src/System.Reactive/Internal/ExceptionServices.cs:line 14 at System.Reactive.Stubs.<>c.<.cctor>b__2_1(Exception ex) in /_/Rx.NET/Source/src/System.Reactive/Internal/Stubs.cs:line 16 at System.Reactive.AnonymousObserver1.OnErrorCore(Exception error) in //Rx.NET/Source/src/System.Reactive/AnonymousObserver.cs:line 73
at System.Reactive.ObserverBase1.OnError(Exception error) in /_/Rx.NET/Source/src/System.Reactive/ObserverBase.cs:line 59 at System.Reactive.Subjects.Subject1.OnError(Exception error) in //Rx.NET/Source/src/System.Reactive/Subjects/Subject.cs:line 124
at System.Linq.AsyncEnumerable.ToObservableObservable1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() --- End of stack trace from previous location --- at System.Linq.AsyncEnumerable.ToObservableObservable1.<>c__DisplayClass2_0.<g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 74
--- End of stack trace from previous location ---
at System.Threading.Tasks.Task.<>c.b__128_1(Object state)
at System.Threading.QueueUserWorkItemCallbackDefaultContext.Execute()
at System.Threading.ThreadPoolWorkQueue.Dispatch()
at System.Threading.PortableThreadPool.WorkerThread.WorkerThreadStart()
at System.Threading.Thread.StartCallback()
xargs: dafny: terminated with signal 6; aborting
at Microsoft.Dafny.BoogieGenerator.TrCallStmt(CallStmt s, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran, IdentifierExpr actualReceiver) at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran)
at Microsoft.Dafny.BoogieGenerator.TrUpdateStmt(BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran, UpdateStmt statement) at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran)
at Microsoft.Dafny.BoogieGenerator.TrStmtList(List1 stmts, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran, RangeToken scopeRange, Boolean processLabels)
at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) at Microsoft.Dafny.BoogieGenerator.TrMethodBody(Method m, BoogieStmtListBuilder builder, List1 localVariables, ExpressionTranslator etran)
at Microsoft.Dafny.BoogieGenerator.AddMethodImpl(Method m, Procedure proc, Boolean wellformednessProc)
at Microsoft.Dafny.BoogieGenerator.AddMethod_Top(Method m, Boolean isByMethod, Boolean includeAllMethods)
at Microsoft.Dafny.BoogieGenerator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType)
at Microsoft.Dafny.BoogieGenerator.AddRevealableTypeDecl(RevealableTypeDecl d)
at Microsoft.Dafny.BoogieGenerator.DoTranslation(Program p, ModuleDefinition forModule)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.<>c__DisplayClass3_0.b__0()
at System.Threading.Tasks.Task1.InnerInvoke() at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj) at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state) --- End of stack trace from previous location --- at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state) at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread) --- End of stack trace from previous location --- at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken) at Microsoft.Dafny.Compilation.<>c__DisplayClass54_0.<<VerifyUnverifiedSymbol>b__1>d.MoveNext() at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed) at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed) at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed) at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed) at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed) at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable1 randomSeed)+MoveNext()
|
129 | predicate ValidState()
| ^^^^^^^^^^

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

Linux, Mac

[seebees]

Looks like #5776 is the issue here.

[keyboardDrummer]

I pulled the PR and ran the command this GH issue provides with 4.8.1, but it verified successfully. I've tried to do the same as the failing CI, checking the Dafny version and the commit versions of the main repo and submodules, but I'm not running into the issue. Have you had success reproducing it locally?

[keyboardDrummer]

Note that instead of --boogie /trace, you can use --progress, for a more Dafny centric progress UI

[keyboardDrummer]

Managed to reproduce this, will fix next Monday

[keyboardDrummer]

Smaller reproduction:

abstract module FooM {

  method Foo(x: int) returns (r: int) modifies match x { case 0 => {} case _ => {} } ensures r == 3
}

abstract module BlaM {
  import Bar : FooM

  method Bla(x: int) returns (r: int) {
    r := Bar.Foo(3);
  }
}