NullReferenceException in the C++ compiler when using unbounded integers

[fpoli]

The C++ compiler crashes with a NullReferenceException when using unbounded integers.

Command: dafny /compile:4 /spillTargetCode:2 /compileTarget:cpp Program.dfy

Program:

method Test(x: (int, int)) {}

Output:

Dafny program verifier finished with 0 verified, 0 errors
Unhandled exception. System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.CppCompiler.Warn(String msg, IToken tok) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler-cpp.cs:line 859
   at Microsoft.Dafny.CppCompiler.TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl member, Boolean class_name) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler-cpp.cs:line 880
   at Microsoft.Dafny.CppCompiler.<ActualTypeArgs>b__61_0(Type tp) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler-cpp.cs:line 1070
   at Microsoft.Dafny.Util.Comma[T](String comma, IEnumerable`1 l, Func`2 f) in /Users/fpoli/projects/dafny-original/Source/Dafny/Util.cs:line 29
   at Microsoft.Dafny.Util.Comma[T](IEnumerable`1 l, Func`2 f) in /Users/fpoli/projects/dafny-original/Source/Dafny/Util.cs:line 21
   at Microsoft.Dafny.CppCompiler.ActualTypeArgs(List`1 typeArgs) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler-cpp.cs:line 1069
   at Microsoft.Dafny.CppCompiler.TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl member, Boolean class_name) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler-cpp.cs:line 914
   at Microsoft.Dafny.CppCompiler.DeclareFormalString(String prefix, String name, Type type, IToken tok, Boolean isInParam) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler-cpp.cs:line 1108
   at Microsoft.Dafny.CppCompiler.DeclareFormal(String prefix, String name, Type type, IToken tok, Boolean isInParam, ConcreteSyntaxTree wr) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler-cpp.cs:line 1115
   at Microsoft.Dafny.Compiler.WriteFormals(String sep, List`1 formals, ConcreteSyntaxTree wr, List`1 useTheseNamesForFormals) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler.cs:line 1318
   at Microsoft.Dafny.CppCompiler.CreateMethod(Method m, List`1 typeArgs, Boolean createBody, ConcreteSyntaxTree wdr, ConcreteSyntaxTree wr, Boolean lookasideBody) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler-cpp.cs:line 751
   at Microsoft.Dafny.CppCompiler.ClassWriter.CreateMethod(Method m, List`1 typeArgs, Boolean createBody, Boolean forBodyInheritance, Boolean lookasideBody) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler-cpp.cs:line 690
   at Microsoft.Dafny.Compiler.CompileMethod(Program program, Method m, IClassWriter cw, Boolean lookasideBody) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler.cs:line 2176
   at Microsoft.Dafny.Compiler.CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWriter classWriter) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler.cs:line 1763
   at Microsoft.Dafny.Compiler.Compile(Program program, ConcreteSyntaxTree wrx) in /Users/fpoli/projects/dafny-original/Source/Dafny/Compiler.cs:line 1204
   at Microsoft.Dafny.DafnyDriver.CompileDafnyProgram(Program dafnyProgram, String dafnyProgramName, ReadOnlyCollection`1 otherFileNames, Boolean invokeCompiler, TextWriter outputWriter) in /Users/fpoli/projects/dafny-original/Source/DafnyDriver/DafnyDriver.cs:line 666
   at Microsoft.Dafny.DafnyDriver.Compile(String fileName, ReadOnlyCollection`1 otherFileNames, Program dafnyProgram, PipelineOutcome oc, Dictionary`2 statss, Boolean verified) in /Users/fpoli/projects/dafny-original/Source/DafnyDriver/DafnyDriver.cs:line 441
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in /Users/fpoli/projects/dafny-original/Source/DafnyDriver/DafnyDriver.cs:line 281
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /Users/fpoli/projects/dafny-original/Source/DafnyDriver/DafnyDriver.cs:line 60
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass1_0.<Main>b__0() in /Users/fpoli/projects/dafny-original/Source/DafnyDriver/DafnyDriver.cs:line 36
   at System.Threading.ThreadHelper.ThreadStart_Context(Object state)
   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.ThreadHelper.ThreadStart()

The reason seems here:

dafny/Source/Dafny/Compiler-cpp.cs

Lines 1069 to 1072 in b066352

	private string ActualTypeArgs(List<Type> typeArgs) {
	return typeArgs.Count > 0
	? String.Format(" <{0}> ", Util.Comma(typeArgs, tp => TypeName(tp, null, null))) : "";
	}

A null is passed to the tok parameter of TypeName, but TypeName tries to use tok to report a warning.

[parno]

Thanks for the report. As mentioned here (https://github.com/dafny-lang/dafny/blob/master/docs/Compilation/Cpp.md), the C++ backend does not currently support the int type. It's good to know this is a place that will need fixing, however, when/if we eventually add that support.

[robin-aws]

Assigning this to myself as the UnsupportedFeatureError method I added recently is going to hit this a lot too.