编程语言设计与实现(PLDI)2020论文集

表示不变量是保存模块产生的抽象类型的所有值的属性。表示不变量在软件工程和程序验证中发挥着重要作用。在这篇文章中，我们开发了一个反例驱动的算法，用于推导足以隐含模块所需规范的表示不变量。关键的新颖性是类型导向的可视归纳概念，它确保算法在减弱和加强候选不变量之间交替时朝着其目标前进。该算法由一个基于实例的综合引擎和一个验证器参数化，并证明了它对于有限类型上的一阶模块是可靠和完备的，假设合成器和验证器也是如此。我们在一个名为Hanoi的工具中实现这些想法，该工具合成递归数据类型的表示不变量。河内不仅处理一阶码的不变量，还处理高阶码的不变量。在后端，河内使用一个名为Myth的枚举合成器和一个枚举测试工具作为验证器。因为河内使用测试来验证，所以它是不可靠的，尽管我们的经验评估表明，在我们调查的基准上它是成功的。

我们介绍了Analytic Program Repair，这是一种数据驱动的策略，用于通过修复错误的程序来提供对类型错误的反馈。我们的策略是基于这样的洞察力，即类似的错误也有类似的修复。因此，我们展示了如何使用不良类型程序对及其固定版本的训练数据集来：(1)通过将训练集中所做的编辑抽象和划分成具有代表性的模板集来学习候选修复模板的集合；(2)通过在训练集中使用的修复模板上训练多类分类器，从给定的错误中预测合适的模板；(3)通过枚举和排序与预测模板匹配的正确(例如，类型良好的)术语来从模板合成具体的修复。我们已经在Rite中实现了我们的方法：OCaml程序的类型错误报告工具。我们在4500个错误类型的Ocaml程序语料库上对Rite的准确性和效率进行了评估，这些程序来自入门编程课程的两个实例，并对生成的错误消息的质量进行了用户研究，显示出错误消息的位置和最终修复质量在统计意义上优于最先进的工具。

最近的程序合成技术通过将低级三角形网格反编译成构造性实体几何(CSG)表达式来帮助用户定制CAD模型(例如，用于3D打印)。在没有循环或函数的情况下，编辑CSG可能需要许多协调的更改，而现有的网格反编译器使用的启发式算法可能会混淆高级结构。

本文提出了第二个反编译阶段，以稳健地将非结构化CSG表达式收缩为具有MAP和Fold运算符的更具可编辑性的程序。我们提出了一个工具Szalinski，它使用相等饱和和保持语义的CAD重写来高效地搜索较小的等价程序。Szalinski依赖于逆变换，这是求解者推测性地将等价项添加到E图中的一种新方法。我们在案例研究中对Szalinski进行了定性评估，展示了它如何与现有的网格反编译器组合在一起，并演示了Szalinski可以在几秒钟内缩小大型模型。

连续标记启用语言中的动态绑定和上下文检查，并正确处理尾部调用和一流的、多提示的、带分隔符的延续。延续标记最简单、最直接的用法是实现动态作用域的变量，如当前输出流或当前异常处理程序。其他用途包括用于调试或安全检查的堆栈检查、正在进行的计算的序列化以及冗余检查的运行时省略。通过向编程语言的用户公开连续标记，可以将更多类型的语言扩展实现为库，而无需进一步更改编译器。同时，编译器和运行时系统必须提供连续标记的有效实现，以确保库实现的语言扩展与更改编译器一样有效。我们实现的CHEZ方案的延续标记(支持球拍)使得动态绑定和查找变得恒定和快速，保留了CHEZ方案的一流延续的性能，并且对不使用一流延续或标记的程序片断施加了可以忽略不计的开销。(=。

字节可寻址永久存储器(如Intel/Micron 3D XPoint)是一种新兴的技术，它在易失性存储器和永久存储之间架起了一座桥梁。永久内存中的数据在崩溃和重新启动后仍然存在；但是，要确保这些数据在故障后保持一致是一件具有挑战性的事情。现有

具有高级控制功能的高级语言的实现者可能会问这样一个问题：“我的实现的最佳选择是什么？不幸的是，目前的文献没有提供太多指导，因为以前的研究在方法论上存在各种缺陷，对于现代硬件来说已经过时了。”在缺乏最近良好标准化的衡量标准和对其实施细节的整体概述的情况下，选择战略时阻力最小的路径是信任民俗，但民俗也是值得怀疑的。

本文试图通过对实现调用堆栈和延续的六种不同方法进行“苹果对苹果”的比较来纠正这种情况。这种比较使用相同的源语言、编译器流水线、LLVM后端和运行时系统，唯一的区别是实现策略的不同。我们比较了不同方法的实现挑战、它们的顺序性能，以及它们支持高级控制机制(包括支持大量线程代码)的适用性。除了实现策略的比较，论文的贡献还包括一些有用的实现技术，我们在此过程中发现。

在动态类型语言中，在部分上下文上进行类型推断是具有挑战性的。在这项工作中，我们提出了一个图神经网络模型，它通过对程序的结构、名称和模式进行概率推理来预测类型。该网络使用深度相似性学习来学习类型空间-类型离散空间的连续松弛-以及如何将符号(即标识符)的类型属性嵌入其中。重要的是，我们的模型可以使用一次性学习来预测类型的开放词汇表，包括稀有类型和用户定义的类型。我们在Typilus for Python中实现了我们的方法，它将TypeSpace与可选的类型检查器相结合。我们证明了锥虫能准确地预测类型。Typilus自信地预测70%的可注释符号的类型；当它预测一个类型时，该类型选择性地检查95%的时间。Typilus还可以发现不正确的类型注释；两个重要且流行的开源库，airseq和allennlp，接受了我们的Pull请求，修复了Typilus发现的注释错误。

验证真实世界的程序通常需要推断具有非线性约束的循环不变量。这在执行许多数值操作的程序中尤其如此，例如航空电子设备或工业工厂的控制系统。最近，数据驱动的循环不变量推理方法显示出很好的应用前景，特别是在线性循环不变量方面。然而，将数据驱动推理应用于非线性循环不变量是具有挑战性的，因为高阶项的数量和幅度都很大，在少量样本上存在过拟合的可能性，以及可能存在的非线性不等式界的大空间。

本文介绍了一种新的用于一般SMT学习的神经结构--门控连续逻辑网络(G-CLN)，并将其应用于非线性回路不变学习。G-CLN扩展了连续逻辑网络(CLN)的结构，增加了门控单元和丢弃，使模型能够稳健地学习大量项上的一般不变量。为了解决有限程序采样引起的过拟合问题，我们引入了分数采样-循环语义对连续函数的一种合理放松，有助于在实域上进行无界采样。此外，我们还设计了一个新的CLN激活函数-分段有偏二次单位(PBQU)，用于自然地学习紧不等式界。

我们将这些方法结合到一个非线性循环不变量推理系统中，该系统可以学习一般的非线性循环不变量。我们在非线性循环不变量的基准上对我们的系统进行了评估，结果表明它解决了27个问题中的26个，比以前的工作多了3个，平均运行时间为53.3秒。通过解决线性Code2Inv基准测试中的所有124个问题，进一步证明了G-CLN的泛型学习能力。我们还进行了定量的稳定性评估，结果表明G-CLN在二次问题上的收敛速度为97.5%，比CLN模型提高了39.2%。

学习神经程序嵌入是在程序语言研究中利用深度神经网络的关键-精确而有效的程序表示使深层模型能够应用于广泛的程序分析任务。现有的方法主要是从源代码中学习嵌入程序，因此，它们不能捕获深入、精确的程序语义。另一方面，从运行时信息中学习的模型在很大程度上依赖于程序执行的质量，从而导致训练后的模型具有高度不同的质量。本文通过引入一种新的深度神经网络来克服现有方法的这些固有缺陷。

静态二进制重写在软件安全和系统中有许多重要的应用，如硬化、修复、修补、插装和调试。虽然已经提出了许多不同的静态二进制重写工具，但大多数都依赖于从输入二进制文件中恢复控制流信息。恢复步骤是必要的，因为重写过程可能会移动指令，这意味着需要相应地调整重写的二进制文件中的跳转目标集。由于控制流信息的静态恢复通常是一个难题，因此大多数工具依赖于一组简化的试探法或假设，例如特定的编译器、特定的源语言或二进制文件元信息。然而，依赖于假设或启发式方法在实践中往往伸缩性很差，而且大多数最先进的静态二进制重写工具无法处理非常大/复杂的程序，如Web浏览器。

在本文中，我们介绍了E9Patch，这是一个可以静态重写x86_64二进制文件的工具，它不需要任何控制流信息。为此，E9Patch开发了一套二进制重写方法，例如指令双关、填充和驱逐，它们可以在不需要移动其他指令的情况下向蹦床插入跳转。由于这保留了跳转目标集，因此消除了对控制流恢复和相关试探法的需要。因此，E9Patch在设计上是健壮的，可以扩展到非常大的(>；100MB)剥离的二进制文件，包括Google Chrome和Firefox Web浏览器。我们还评估了E9Patch在实际应用中的有效性，例如二进制检测、强化和修复。

现代软件系统广泛使用从C和C++派生的库。然而，由于这些语言缺乏内存安全，这些库可能会受到漏洞的影响，这可能会使应用程序面临潜在的攻击。例如，glibc中存在大量面向返回的编程小工具，它们允许将语义有效但恶意的图灵完整和不完整程序拼接在一起。虽然CVE会被发现，而且通常会打补丁和补救，但这样的小工具会成为未来未被发现的攻击的基础，为生成恶意程序打开了越来越多的可能性。因此，图书馆的此类小工具的数量和表现力(效用)的显著减少是一个重要的问题。

在这项工作中，我们提出了一种新的方法来处理应用程序的库函数，该方法侧重于“只获得您想要的”原则。这与目前侧重于“削减不需要的东西”的做法有很大不同。我们的方法侧重于根据需要激活/去激活库函数，以减少动态链接的代码面，从而大大降低构建恶意程序的可能性。其关键思想是仅加载将在运行时在应用程序内的每个库调用点使用的库函数集。这种需求驱动加载方法依赖于一个输入感知的Oracle，它可以预测执行期间给定调用点所需的一组近乎精确的库函数。预测的函数被及时加载，并在返回时卸载。

我们提出了一个基于决策树的预测器，它起到了预言机的作用，以及一个优化的运行时系统，它直接与GNU libc和libstdc++等库二进制文件一起工作。结果表明，平均而言，该方案减少了97.2%的库暴露代码表面，减少了97.9%的链接库中的ROP小工具，在大多数情况下实现了至少97%的预测准确率，并且在SPEC 2006的所有基准测试中，所有库的运行开销增加了18%(Glibc为16%，其他库为2%)。此外，我们在两个实际应用程序(sshd和nginx)上演示了BlankIt，它们具有高消胀和低开销。

并发分离逻辑对并发数据结构的推理已经取得了很大的成功。这一成功源于他们在多个层次上的模块化应用，导致根据程序结构、程序状态和单个线程进行分解的证明。尽管有这些进步，但要实现跨不同数据结构实现的证明重用仍然很困难。对于大类搜索结构，我们演示了如何通过将线程安全证明与结构完整性证明解耦来实现进一步的证明模块性。我们的工作基于Shasha和Goodman的模板算法，它们规定了线程如何交互，但从内存中节点的具体布局中抽象出来。在最近提出的组合抽象流框架和分离逻辑IRIS的基础上，我们展示了如何证明模板算法的正确性，以及如何实例化它们以获得多个经过验证的实现。

我们通过将程序机械化来演示我们的方法

因果一致性是弱于顺序一致性的最基本、应用最广泛的一致性模型之一。本文研究了在因果一致共享内存模型下运行的有限状态并发程序的安全性质验证问题。对于因果一致性的标准模型(也称为因果收敛和强释放获取)，我们建立了这个问题的可判断性。我们的证明基于线程潜力的概念，通过开发一种替代的操作语义进行证明，该语义等价于现有的声明性语义，并构成了一个结构良好的转换系统。特别地，我们的结果允许对C/C++11(RA)的发布/获取片段中的一大类程序进行验证。事实上，虽然最近显示RA下的验证对于一般程序是不可确定的，但是由于RA与我们在这里研究的写/写无竞争程序的模型一致，所以对于这类广泛使用的程序，RA下的验证的可判断性从我们的结果得出。新的操作语义也可以独立用于弱一致性共享存储模型的研究和验证。

异步程序是出了名的难以推理，因为它们会产生以不确定方式异步生效的计算任务。公式的归纳不变量的设计。

..