Incorrect programId passed to Boogie causes memory leak in LSP server

[cpitclaudel]

Boogie accepts a programId along with each program in ExecutionEngine.InferAndVerify. This ID is used as a key to partition a cache of recent parses:

https://github.com/boogie-org/boogie/blob/ce03249fa06a7442df96352bb55e1bfba3e30365/Source/ExecutionEngine/ExecutionEngine.cs#L253-L257

A reasonable choice of key, for example, is the path of the current program. Alternatively, if there is only one program being verified, using null is also reasonable; in that case Boogie uses a default string (https://github.com/boogie-org/boogie/blob/ce03249fa06a7442df96352bb55e1bfba3e30365/Source/ExecutionEngine/ExecutionEngine.cs#L318-L321). This is what the Dafny CLI does:

dafny/Source/DafnyDriver/DafnyDriver.cs

Line 263 in 38be532

var ev = ProcessFiles(new List<DafnyFile> { f }, new List<string>().AsReadOnly(), reporter, lookForSnapshots, f.FilePath);

dafny/Source/Dafny/DafnyMain.cs

Lines 236 to 239 in b6d7ae8

	if (programId == null) {
	programId = "main_program_id";
	}
	programId += "_" + moduleName;

The legacy DafnyServer used by Emacs uses just a module name, because it can't operate on more than one file at a time, so the file name part isn't needed:

dafny/Source/DafnyServer/DafnyHelper.cs

Line 85 in 495e7d2

switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram_" + moduleName, null, DateTime.UtcNow.Ticks.ToString())) {

The LSP server does something different:

dafny/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs

Lines 103 to 107 in 5becffa

	var uniqueId = Guid.NewGuid().ToString();
	using (cancellationToken.Register(() => CancelVerification(uniqueId))) {
	try {
	var statistics = new PipelineStatistics();
	var outcome = ExecutionEngine.InferAndVerify(program, statistics, uniqueId, null, uniqueId);

The test generator does the same thing, which is equally wrong, I think:

dafny/Source/DafnyTestGeneration/ProgramModification.cs

Lines 85 to 88 in b6d7ae8

	var log = Utils.CaptureConsoleOutput(
	() => ExecutionEngine.InferAndVerify(program,
	new PipelineStatistics(), uniqueId,
	_ => { }, uniqueId));

In both cases one new program entry is created in the cache every time Boogie is queries. The cache's default expiration policy is a 10-minutes window, so for 10 minutes memory usage just grows.

The fix is to pass the program name instead of a freshly created unique string as the programId. I will open a PR soon.