DIADEM: debugging made dependable and measurable

软件质量对大多数人来说越来越重要。软件中的漏洞每年都会造成巨大的经济损失，甚至是生命损失。为了消除错误，开发人员主要依赖于他们的工具。交互式调试工具是至关重要的。它们单独提供了运行（二进制）程序的高级（源代码）视图，使程序员能够“看到”在他们面前运行的程序中出现的错误。然而，调试基础设施是出了名的不可靠，因为它只有在各种元数据完整和正确的情况下才能工作。如果没有，程序员看到的是部分或不正确的视图，这可能是无用的或积极误导。由于可调试性和优化之间的紧张关系，这些问题经常出现在流行语言中（例如C， c++, Rust, Go）。在这些语言中，调试通过编译器生成/元数据/描述二进制（可执行）代码与源代码（人工编写）代码之间的关系来进行。元数据生成是“尽最大努力”，而优化经常会引入缺陷——但简单地禁用优化很少是一种选择。程序员依靠优化来减轻他们大量的手工调整。没有它们，代码的运行速度可能会慢几十倍。此外，由于源语言中未定义的行为（未规范），一些bug只出现在优化的代码中。这个问题极具挑战性。它的核心是，编写编译器优化以保持可调试性需要额外的努力，在已经复杂的代码转换（“传递”）上。在实践中，省略了一些边角，使输出元数据保持近似。为了让作者能够接受，改进必须在不增加任务基线复杂性的情况下重塑工作/奖励曲线。与性能不同，到目前为止，调试缺乏定量的基准测试，因此编译器作者没有优先考虑可调试性或在可调试性上进行竞争。现有的技术相当于基于交互的调试测试，通常具有缩小引入缺陷的通道的功能。这是偶然的，因为探索所有元数据包括实现全覆盖测试（在所有程序位置“驱动”调试器）这个已经很困难的问题。相反，我们建议将元数据作为其本身的工件来分析。这意味着，我们必须设计一种自定义的系统的、符号的方法，以探索编译后的代码，以数学的方式评估元数据的正确性，而不是通过调试器与单个具体执行交互的测试。与随意的测试不同，这保证了对丢失的覆盖率和正确性的系统测量；后者可以（我们假设）使用源语言的正式规范的最新进展来自动化，即/可执行语义/，作为当前手工实践的替代。这种并行源级和二进制级探索的思想还提出了一种激进的方法：对元数据进行事后合成，从而使编译器完全不必生成元数据。这里的思想建立在相邻问题（翻译验证和反编译）的成功工作之上。该项目将通过实际方法进行，在真实的生产编译器（LLVM）上进行实验。它将构建可嵌入现有编译器测试工作流程的新工具，既可以诊断编译器错误，又可以量化修复错误后的改进。它将经验地探索编译器内部使用的抽象和帮助器，以设计出使它们更易于维护调试的设计。最后，它将构建一个新颖的工具，探索在编译器之外以即时方式合成高质量元数据的激进思想。它将制定指标，允许与传统方法进行定量比较。受益者有很多层次：编译器作者、软件开发人员，以及使用或依赖受影响软件的一般公众。

Software quality is increasingly critical to most of humanity. Bugs in software claim a huge annual toll, financially and even in human life. To eliminate bugs, developers depend crucially on their tools. Tools for interactive debugging are vital. They alone provide a high- (source-) level view of a running (binary) program, enabling programmers to 'see the bug' as it occurs in the program running in front of them. However, debugging infrastructure is notoriously unreliable, as it works only if various metadata is complete and correct. If not, the programmer sees a partial or incorrect view, which may be useless or actively misleading.These problems occur often in popular languages (e.g. C, C++, Rust, Go), owing to a tension between debuggability and optimisation. Debugging in these languages works by compiler-generated /metadata/ describing how binary (executable) code relates to source (human-written) code. Metadata generation is 'best-effort', and optimisation frequently introduces flaws -- but simply disabling optimisations is seldom an option. Programmers rely on optimisations to relieve them of much hand-tuning. Without them, code may run tens of times slower. Furthermore, some bugs appear only in optimised code, owing to undefined behaviour (underspecification) in the source language.This problem is extremely challenging. The heart of it is that writing compiler optimisations that preserve debuggability demands extra effort, on what are already intricate code transformations ('passes'). In practice corners are cut, leaving the output metadata approximate. To be acceptable to pass authors, improvements must reshape the effort/reward curve without increasing the task's baseline complexity. Unlike performance, debugging so far lacks quantitative benchmarks, so compiler authors have not prioritised or competed on debuggability.Existing techniques amount to interaction-based testing of debugging, often with features for narrowing down which passes introduced a flaw. This is haphazard, since exploring all metadata includes the already-hard problem of achieving full-coverage tests (to 'drive' the debugger over all program locations). We propose instead to analyse metadata as an artifact in its own right. This means instead of tests that interact with a single concrete execution through a debugger, we must devise a custom systematic, symbolic method for exploring the compiled code, evaluating the correctness of metadata in a mathematical manner. Unlike haphazard testing, this promises systematic measurement of lost coverage and correctness; the latter can (we hypothesise) be automated using recent advances in formal specification of source languages, namely /executable semantics/, as a replacement for the current manual practices. This idea of parallel source- and binary-level exploration also suggests a radical approach: post-hoc synthesis of metadata, relieving the compiler of generating it at all. The idea here builds on successful work on neighbouring problems (translation validation and decompilation).The project will proceed by practical methods, experimenting on a real production compiler (LLVM). It will build novel tools embeddable into existing compiler-testing workflows, both to diagnose compiler bugs and to quantify the improvement from fixing them. It will empirically explore abstractions and helpers used internally in compilers, to devise designs making them measurably more debug-preserving. Finally it will build a novel tool exploring the radical idea of synthesising high-quality metadata in post-hoc fashion, outside the compiler. It will develop metrics allowing quantitative comparison against traditional approaches. The beneficiaries are on many levels: compiler authors, software developers at large, and the general public who use or depend on the affected software.