Handle `--coverage-report` with `dafny translate` (or legacy compilation option)

[codyroux]

Summary

Currently there is no way to generate coverage report with separately compiled Dafny.

Background and Motivation

To compile tests, I call (legacy) dafny -spillTargetCode:3 -out:/some/runtime/folder -runAllTests:1 ...

and run it with dotnet run ...

This does not enable passing in the option --coverage-report. Calling dafny test DafnyFile.dfy is difficult since the {:extern} functions need to be linked via some fiddly C# compilation configuration.

Proposed Feature

We propose adding the ability for dafny -spillTargetCode:3 or dafny translate cs (ideally the former for now) to handle the --coverage-report flag, which would behave as if one called dafny test --coverage-report:some-folder directly, when running the emitted code with dotnet run.

Alternatives

I'm not sure what the alternative is, possibly enabling linking C# externs more easily in the dafny test configuration.

[robin-aws]

I'm not sure what the alternative is, possibly enabling linking C# externs more easily in the dafny test configuration.

Correct me if I'm wrong, but this is particularly tricky because you don't just have a few C# files to pass into dafny test (which isn't currently possible since only dafny run takes the --input option, but that could be fixed easily), but you also have a dependency on a Nuget package you'd have to fetch the DLL for and pass in, which is even more awkward.

[codyroux]

That's correct, yes.

[keyboardDrummer]

@codyroux It sounds like you're saying there's an option --coverage-report that can be used with dafny test, but you can't use it because you're not using dafny test directly. However, there is no --coverage-report option for dafny test. There is one for dafny generate-tests, but I don't see how the semantics of that option could translate to dafny test or dafny translate, since they relate to verification based test generation.

[codyroux]

I'm referring to this feature: https://github.com/dafny-lang/dafny/commit/4d7bdf582e6a9c1b05063dac6130f65f196001a0

I think it's referenced here: http://dafny.org/dafny/DafnyRef/DafnyRef#sec-dafny-test

[keyboardDrummer]

Ah, I see. Sorry for my mistake! I was looking at Dafny 4.3 options.

[keyboardDrummer]

I think what we can do is change dafny translate --include-test-runner --coverage-report=<file> so that when the translated code is run, using non-Dafny implementations of externs and other configuration you provide to it, the resulting binary will write a code coverage report that follows some standard, like the Cobertura coverage format, to the <file> location that was specified when running dafny translate