Cycle in type declaration causes crash

[RustanLeino]

Dafny version

current master (post 4.2.0)

Code to produce this issue

trait YT<W> {
  const f: W
}

class Y extends YT<Y -> nat> {
}

Command to run and resulting output

% dafny verify test.dfy

Unhandled exception. System.AggregateException: One or more errors occurred. (One or more errors occurred. (One or more errors occurred. (Unable to cast object of type 'Microsoft.Dafny.ClassDecl' to type 'Microsoft.Dafny.ICallable'.)))
 ---> System.AggregateException: One or more errors occurred. (One or more errors occurred. (Unable to cast object of type 'Microsoft.Dafny.ClassDecl' to type 'Microsoft.Dafny.ICallable'.))
 ---> System.AggregateException: One or more errors occurred. (Unable to cast object of type 'Microsoft.Dafny.ClassDecl' to type 'Microsoft.Dafny.ICallable'.)
 ---> System.InvalidCastException: Unable to cast object of type 'Microsoft.Dafny.ClassDecl' to type 'Microsoft.Dafny.ICallable'.
   at Microsoft.Dafny.ModuleResolver.CheckVariance(Type type, TopLevelDecl enclosingTypeDefinition, TPVariance context, Boolean lax) in DAFNY/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 5093
   at Microsoft.Dafny.ModuleResolver.CheckVariance(Type type, TopLevelDecl enclosingTypeDefinition, TPVariance context, Boolean lax) in DAFNY/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 5100
   at Microsoft.Dafny.ModuleResolver.CheckVariance(Type type, TopLevelDecl enclosingTypeDefinition, TPVariance context, Boolean lax) in DAFNY/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 5100
   at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, String moduleName, Boolean isAnExport) in DAFNY/Source/DafnyCore/Resolver/ModuleResolver.cs:line 1487
   at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, Boolean isAnExport) in DAFNY/Source/DafnyCore/AST/Modules/ModuleDefinition.cs:line 428
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation) in DAFNY/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs:line 122
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in DAFNY/Source/DafnyCore/Resolver/ModuleResolver.cs:line 184
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in DAFNY/Source/DafnyCore/Resolver/ProgramResolver.cs:line 171
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) in DAFNY/Source/DafnyCore/Resolver/ProgramResolver.cs:line 66
   at Microsoft.Dafny.DafnyMain.<>c__DisplayClass5_0.<Resolve>b__0() in DAFNY/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 DAFNY/Source/DafnyCore/DafnyMain.cs:line 89
   at Microsoft.Dafny.DafnyMain.ParseCheck(TextReader stdIn, IReadOnlyList`1 files, String programName, DafnyOptions options, Program& program) in DAFNY/Source/DafnyCore/DafnyMain.cs:line 54
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IReadOnlyList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, DafnyOptions options, Boolean lookForSnapshots, String programId) in DAFNY/Source/DafnyDriver/DafnyDriver.cs:line 451
   --- 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 DAFNY/Source/DafnyDriver/DafnyDriver.cs:line 149
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass11_0.<MainWithWriters>b__0() in DAFNY/Source/DafnyDriver/DafnyDriver.cs:line 120
   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 DAFNY/Source/DafnyDriver/DafnyDriver.cs:line 120
   at Microsoft.Dafny.DafnyDriver.Main(String[] args) in DAFNY/Source/DafnyDriver/DafnyDriver.cs:line 107
   at Dafny.Dafny.Main(String[] args) in DAFNY/Source/Dafny/Dafny.cs:line 7

What happened?

The use of Y in the type argument to the class Y itself causes Dafny to crash.

Note, this crash is rather recent, because the program does not crash with Dafny 4.2.0.

Also note, if this program were accepted (not just without crashing, but without causing any other error), then it is possible that the following program would also be accepted and verified:

trait YT<W> {
  const f: W
}

class Y extends YT<Y -> nat> {
  constructor(f: Y -> nat)
    ensures this.f == f
  {
    this.f := f;
  }
}

method Main()
  ensures false
{
  // error: knot.f calls itself without decreasing
  var arrow := (x: Y) => 1 + x.f(x);
  var knot := new Y(arrow);
  var a := knot.f(knot);
}

This is a variation of Test/Landin/Knot4.dfy.

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

Mac

[ssomayyajula]

git bisect says this was introduced in #4240, will take a look.

[ssomayyajula]

Offending file here.

Looks like the issue is that the precondition for CheckVariance() -- !lax || enclosingTypeDefinition is ICallable -- is not actually satisfied so line 5062 in the same file errors out (weirdly, the trace does not report this contract violation). @RustanLeino both enclosingTypeDefinition and t0 at line 5062 are ClassDecls, which is not ICallable. Yet, it looks like you want to use the call graph to detect a circular reference, which requires you to pass in ICallables. Is there another way to do that?

[ssomayyajula]

In the commit before fix #4240, CheckVariance() looks like this:

public void CheckVariance(Type type, ICallable enclosingTypeDefinition, ...) {
  ...
  } else if (type is UserDefinedType) {
    var t = (UserDefinedType)type;
    ...
    } else {
      var resolvedClass = t.ResolvedClass;
      ...
      if (lax) {
        var cg = enclosingTypeDefinition.EnclosingModule.CallGraph;
        var t0 = resolvedClass as ICallable;
        if (t0 != null && cg.GetSCCRepresentative(t0) == cg.GetSCCRepresentative(enclosingTypeDefinition)) {
          ...
        }
      }
    }
  }
}

Note that enclosingTypeDefinition is always ICallable, so the innermost if is fine regardless if resolvedClass is ICallable (referring to an iterator or datatype declaration) or not. Post fix, the signature looks like this:

public void CheckVariance(Type type, TopLevelDecl enclosingTypeDefinition, ...)

And the innermost if looks like this:

if (t0 != null && cg.GetSCCRepresentative(t0) == cg.GetSCCRepresentative((ICallable)enclosingTypeDefinition))

enclosingTypeDefinition is not necessarily ICallable --- in the example above, it's a ClassDecl. So, the cast fails. It's sufficient to just add another type test for enclosingTypeDefinition:

• Circular references to iterators and datatypes in a negative position will still be caught, as desired, and...
• Such references to class types is stopped by HigherOrderHeapAllocationCheckerConstructor.cs as in Landin's knot-style cases