代数库规范下的程序合成 1引用BenjaminMariano,JoshReese,Siyu

文章插图
1 引用Benjamin Mariano, Josh Reese, Siyuan Xu, ThanhVu Nguyen, Xiaokang Qiu, Jeffrey S. Foster, Armando Solar-Lezama, "Program Synthesis with Algebraic Library Specifications", In Proceedings of the 2019 Program Synthesis with Algebraic Library Specifications. ACM, 132:1-132:25.
2 摘要程序合成领域的一个极具挑战性的任务是合成使用库的程序。目前，主流软件在开发过程中或多或少会调用到第三方库。该领域的最新研究进展是通过模拟库实现对库进行建模，以更简单的方式执行相同的功能。但是，模拟库可能仍然庞大而复杂，并且必须包含许多实现细节。这两个因素都会限制程序合成的性能。为了解决这个问题，我们引入了 JLibSketch ，这是一个 Java 程序合成工具，允许使用代数规范来描述库行为，这些规范是方法调用序列的重写规则，例如，加密后再解密（使用相同的密钥）就是标识。 JLibSketch 通过将 JLibSketch 问题编译为 Sketch 程序合成工具的问题来实现重写规则。更具体地说，在编译后，我们使用抽象数据类型（ADT）表示库调用，并通过重写规则修改对这些 ADT 进行操作。如果重写规则是有序且不可统一的，我们将对形式进行规范化并证明其合理且完整。我们通过使用 JLibSketch 合成了九个程序，并使用来自三个领域的库对这些程序进行了评估：数据结构，密码学和文件系统。通过实验发现，我们提出的方法在代数规范的平均大小方面约为模拟库方法的一半。我们还发现，代数规范在 9 个程序中的 7 个上的表现要优于模拟方法，并且在最后两个程序上展现出相同的性能。基于以上，我们认为 JLibSketch 在使用库的程序合成方面迈出了重要的一步。
3 概述近年来，基于 Sketch 的程序合成取得了巨大进步，给定包含某些未知数的部分程序，它可以解决这些未知数，因此合成的程序可以满足其断言。剩下的主要挑战是合成使用库的程序，这在大多数软件中很常见。一种可能的方法是将库源代码内联到 Sketch 中，但这在实践中是站不住脚的：库代码很大且很复杂。相反，一种更有效的方法是开发以 Sketch 语言编写的模拟库（或仅模拟），以更简单的方式实现基本的库功能。但是，在实践中，模拟可能是相当大的，并且它们包括合成器必须依据的许多实现细节，所以很难通过模拟获得良好的合成性能。
JLibSketch 建立在 JSketch 之上，将基于 Sketch 的程序合成带入 Java 。图 1 说明了 JSketch 的一些关键功能，它们模仿了相应的 Sketch 功能。每个 JSketch 程序包含一个或多个线束，它们是可以包含三种未知数的部分程序：漏洞，用??表示，代表整数或布尔常数；表达式合成器，用{| e1, e2, ... |}表示；和函数合成器。 JSketch 的目标是找到未知的实例，以便对于参数的所有选择都满足其断言。例如，图 1 显示了一个示例 JSketch 问题。
文章插图
图 1 简单的 JSketch 问题
尽管 JSketch 很有前途，但很难使用它来合成使用库的程序。作为运行示例，我们将考虑我们的基准测试之一 SuffixArray 。该基准测试的一部分是合成方法 lrs ，如图 2d 所示。我们将在短期内讨论该图的细节。现在，我们仅观察到代码使用 TreeSet（图中用 TS 表示），它是 Java 标准库中的数据结构。因此，合成器需要了解 TreeSet 方法的语义才能解决此问题。
文章插图
图 2 来自 SuffixArray 的 JLibSketch 示例
最直接的解决方案是将 TreeSet 源代码连接到 Sketch ，但是不幸的是，该方法不起作用。标准的 TreeSet 实现基于 TreeMap 库构建，这会使问题太大而无法解决。相反，我们需要构建一个更小，更简单且易于合成的表示模型。一种建模方法是编写 TreeSet 的模拟实现，该实现可避免使用本机代码并且具有较少的依赖性。尽管这可能是有效的，但模拟也可能很长，降低了合成性能，编写模拟需要选择可能会带来意想不到的后果的一系列实现选择。
JLibSketch 旨在通过扩展 JSketch 来支持代数规范，以建立模型库来解决这个问题。例如，图 2a 提供了部分规范，描述了在@rewriteClass（第 1 行）中分组的 TreeSet 的几种方法（缩写为 TS）之间的关系。
要了解这些规则在实践中是如何工作的，请考虑图 2b 中的 Sketch ，用于前面提到的 lrs 方法。此方法（第 30 行）返回包含最长重复子字符串的 TreeSet 。