Import an abstract module without a default exportset causes Dafny to crash

[EkanshdeepGupta]

Dafny version

4.1.0

Code to produce this issue

module A {
  export E
    provides f

  function f() : bool { true }
}

abstract module B {
  import A0: A
}

Command to run and resulting output

$ ./Binaries/Dafny verify ~/test/scratch.dfy
    |
130 |   import A0: A
    |              ^

/Users/ekanshdg/test/scratch.dfy(130,13): Error: no default export set declared in module: A
Unhandled exception. System.AggregateException: One or more errors occurred. (One or more errors occurred. (One or more errors occurred. (Object reference not set to an instance of an object.)))
 ---> System.AggregateException: One or more errors occurred. (One or more errors occurred. (Object reference not set to an instance of an object.))
 ---> System.AggregateException: One or more errors occurred. (Object reference not set to an instance of an object.)
 ---> System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, Boolean isAnExport) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyCore/AST/Modules/ModuleDefinition.cs:line 393
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs:line 122
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyCore/Resolver/ModuleResolver.cs:line 184
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyCore/Resolver/ProgramResolver.cs:line 161
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyCore/Resolver/ProgramResolver.cs:line 66
   at Microsoft.Dafny.DafnyMain.<>c__DisplayClass5_0.<Resolve>b__0() in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyCore/DafnyMain.cs:line 89
   at System.Threading.Tasks.Task.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 inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task.Wait(Int32 millisecondsTimeout, CancellationToken cancellationToken)
   at System.Threading.Tasks.Task.Wait()
   at Microsoft.Dafny.DafnyMain.Resolve(Program program) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyCore/DafnyMain.cs:line 89
   at Microsoft.Dafny.DafnyMain.ParseCheck(TextReader stdIn, IReadOnlyList`1 files, String programName, DafnyOptions options, Program& program) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyCore/DafnyMain.cs:line 54
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IReadOnlyList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, DafnyOptions options, Boolean lookForSnapshots, String programId) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyDriver/DafnyDriver.cs:line 439
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, String[] args) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyDriver/DafnyDriver.cs:line 142
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass11_0.<MainWithWriters>b__0() in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyDriver/DafnyDriver.cs:line 119
   at System.Threading.Tasks.Task`1.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj)
   at System.Threading.ExecutionContext.RunFromThreadPoolDispatchLoop(Thread threadPoolThread, ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
   at System.Threading.ExecutionContext.RunFromThreadPoolDispatchLoop(Thread threadPoolThread, ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.MainWithWriters(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, String[] args) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyDriver/DafnyDriver.cs:line 119
   at Microsoft.Dafny.DafnyDriver.Main(String[] args) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/DafnyDriver/DafnyDriver.cs:line 106
   at Dafny.Dafny.Main(String[] args) in /Users/ekanshdg/git_dafny/dafny_mainline/Source/Dafny/Dafny.cs:line 7
fish: Job 1, './Binaries/Dafny verify ~/test/…' terminated by signal SIGABRT (Abort)

What happened?

When importing an abstract module without a default export set, Dafny reports the error, but then subsequently crashes.

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

Mac