search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.92k stars 262 forks source link

Support for debugging compiled Dafny code? #1782

Open robin-aws opened 2 years ago

robin-aws commented 2 years ago

Several different options here:

  1. Emitting code comments with the Dafny source that generated sections of target language code.
  2. External metadata mapping output back to Dafny source (a.k.a. "source maps").
  3. (Expensive) Implementing debugging tools for Dafny in each supported target language.
  4. (Expensive) Targeting bytecode rather than source, as bytecode often has direct support for debugging symbols and metadata.
keyboardDrummer commented 2 years ago

Could you elaborate on what (2) means? Suppose you generate C# from Dafny, then I don't see an external metadata mapping to generate. I'd think that you can't generate C# and a .pdb file, since the .pdb file only maps CIL back to source code.

I think the solution for providing Dafny debugging is to have a proxy debug server that wraps around the target language debug server and transforms each request using a source map generated by the Dafny compiler, that map the generated target language code back to the original Dafny program.