Ghost inference for decreases-to causes crash

[RustanLeino]

Dafny version

master branch, 2 Nov 2024

Code to produce this issue

method InferredGhost(x: int) returns (c: bool) {
  var b := x - 1 decreases to x; // expected: b is inferred to be ghost
  c := b; // expected error: cannot assign ghost to non-ghost
}

Command to run and resulting output

% dafny verify test.dfy
Process terminated. Assertion failed.
   at Microsoft.Dafny.ExpressionTester.UsesSpecFeatures(Expression expr) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/ExpressionTester.cs:line 652
   at Microsoft.Dafny.GhostInterestVisitor.CheckAssignStmt(SingleAssignStmt s, Boolean mustBeErasable, String proofContext) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/GhostInterestVisitor.cs:line 545
   at Microsoft.Dafny.GhostInterestVisitor.Visit(Statement stmt, Boolean mustBeErasable, String proofContext) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/GhostInterestVisitor.cs:line 220
   at Microsoft.Dafny.GhostInterestVisitor.<>c__DisplayClass9_0.<Visit>b__3(Statement ss) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/GhostInterestVisitor.cs:line 153
   at System.Collections.Generic.List`1.ForEach(Action`1 action)
   at Microsoft.Dafny.GhostInterestVisitor.Visit(Statement stmt, Boolean mustBeErasable, String proofContext) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/GhostInterestVisitor.cs:line 153
   at Microsoft.Dafny.GhostInterestVisitor.Visit(Statement stmt, Boolean mustBeErasable, String proofContext) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/GhostInterestVisitor.cs:line 172
   at Microsoft.Dafny.GhostInterestVisitor.<>c__DisplayClass9_0.<Visit>b__9(Statement ss) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/GhostInterestVisitor.cs:line 287
   at System.Collections.Generic.List`1.ForEach(Action`1 action)
   at Microsoft.Dafny.GhostInterestVisitor.Visit(Statement stmt, Boolean mustBeErasable, String proofContext) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/GhostInterestVisitor.cs:line 287
   at Microsoft.Dafny.ModuleResolver.ComputeGhostInterest(Statement stmt, Boolean mustBeErasable, String proofContext, ICodeContext codeContext) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/ModuleResolver.cs:line 2036
   at Microsoft.Dafny.ModuleResolver.ResolveClassMembers_Pass1(TopLevelDeclWithMembers cl) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/ModuleResolver.cs:line 1853
   at Microsoft.Dafny.ModuleResolver.ComputeGhostInterestAndMisc(List`1 declarations) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/ModuleResolver.cs:line 1660
   at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, String moduleDescription, Boolean isAnExport) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/ModuleResolver.cs:line 1242
   at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, String exportSetName) in $DAFNY/Source/dafny/Source/DafnyCore/AST/Modules/ModuleDefinition.cs:line 499
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation) in $DAFNY/Source/dafny/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs:line 129
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/ModuleResolver.cs:line 184
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/ProgramResolver.cs:line 177
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) in $DAFNY/Source/dafny/Source/DafnyCore/Resolver/ProgramResolver.cs:line 70
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken) in $DAFNY/Source/dafny/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs:line 54
   at System.Runtime.CompilerServices.AsyncMethodBuilderCore.Start[TStateMachine](TStateMachine& stateMachine)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken) in $DAFNY/Source/dafny/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs:line 41
   at System.Runtime.CompilerServices.AsyncMethodBuilderCore.Start[TStateMachine](TStateMachine& stateMachine)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken) in $DAFNY/Source/dafny/Source/DafnyCore/Pipeline/TextDocumentLoader.cs:line 53
   at System.Runtime.CompilerServices.AsyncMethodBuilderCore.Start[TStateMachine](TStateMachine& stateMachine)
   at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.TextDocumentLoader.<>c__DisplayClass5_0.<ResolveAsync>b__0() in $DAFNY/Source/dafny/Source/DafnyCore/Pipeline/TextDocumentLoader.cs:line 44
   at System.Threading.Tasks.Task`1.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
   at System.Threading.Tasks.Task.ExecuteEntry()
   at System.Threading.Tasks.TaskScheduler.TryExecuteTask(Task task)
   at Microsoft.Boogie.CustomStackSizePoolTaskScheduler.RunItem()
   at Microsoft.Boogie.CustomStackSizePoolTaskScheduler.WorkLoop()
   at System.Threading.Thread.StartCallback()

What happened?

Dafny crashes. I didn't look int the details, but I suspect the error is that CheckIsCompilable and UsesSpecFeatures are not both equipped to handle decreases to expressions, see the source comments by those methods.

In PR #5891, I added the repro above as a commented-out test in dafny0/DecreasesTo5.dfy.

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

Mac