Bad inference of default calc operator causes crash

[RustanLeino]

Dafny version

4.0.0

Code to produce this issue

method Issues(a: bool, s: set) {
  // Any one of the following 8 lines causes a crash

  calc { a; <== false; }
  calc { true; <== a; }
  calc { a; ==> true; }
  calc { false; ==> a; }

  calc { s; >= ({}); }
  calc { s; > ({}); }
  calc { {}; <= s; }
  calc { {}; < s; }
}

Command to run and resulting output

% dafny verify test.dfy
Unhandled exception. 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.Resolver.ResolveStatement(Statement stmt, ResolutionContext resolutionContext)
   at Microsoft.Dafny.Resolver.ResolveStatementWithLabels(Statement stmt, ResolutionContext resolutionContext)
   at Microsoft.Dafny.Resolver.ResolveBlockStatement(BlockStmt blockStmt, ResolutionContext resolutionContext)
   at Microsoft.Dafny.Resolver.ResolveMethod(Method m)
   at Microsoft.Dafny.Resolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl)
   at Microsoft.Dafny.Resolver.ResolveNamesAndInferTypesForOneDeclaration(TopLevelDecl topd)
   at Microsoft.Dafny.Resolver.ResolveNamesAndInferTypes(List`1 declarations, Boolean initialRound)
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport)
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport)
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog)
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter)
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId)
   --- 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(String[] args)
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0()
   at System.Threading.Thread.StartCallback()

What happened?

When a calc statement does not explicitly give a default operator, Dafny picks one. It usually picks ==, but in the 8 cases shown above (which start or end with the literal false, true, or {}), Dafny considers the candidate ==> for the first two, <== for the next two, <= for the next two, and >= for the final two.

Dafny 4.0 then picks that candidate operator as the calc statement's default operator. In the examples above, the candidate operator is in conflict with the given step operators (for example, ==> is not allowed to be chained with <==), which causes a crash.

The right thing to do is to discard the candidate operator if it would lead to such conflicts (and instead pick == as usual in those cases).

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

Mac