paperbot · PL 论文追踪

全部论文 待读 收藏

P2 API-Driven Program Synthesis for Testing Static Typing Implementations

API 驱动的程序合成:面向静态类型检查实现的测试
POPL 8(POPL)2024匹配度 2/10 · 该论文属于程序合成与编译器测试方向(生成良类型程序以发现类型检查器缺陷),既不涉及将静态分析应用于 ML/Agentic 程序,也不涉及用 LLM/Agent 改进静态分析,与浮点程序分析和贝叶斯程序分析亦无交集。虽属 PL 范畴且偏工程落地,但未命中研究画像中的任何核心问题。引用 15 inbox
Thodoris Sotiropoulos, Stefanos Chaliasos, Zhendong Su
crossref: 2026-09-10

AI 速览

一句话:提出 API 驱动的程序合成方法,复用已有库 API 生成小型良类型程序,以检测静态类型检查实现中的缺陷。

本文研究如何有效测试编译器的静态类型检查实现。作者观察到,许多真实的类型检查缺陷由使用标准库 API 的小型测试用例触发,因为这些 API 往往涉及参数多态、重载和高阶函数等复杂类型特性。为此,论文提出 API 驱动的程序合成:从现有软件库中提取 API 并组合,合成类型密集但规模小且良类型的客户端程序,从而避免从头生成完整 API 定义,同时提升类型特性覆盖。为检验类型检查的健全性与类型推断精度,方法还引入故障注入与语义保持模式及相应的测试预言。作者实现工具 thalia,并在 Scala、Kotlin 和 Groovy 三种流行语言的编译器静态类型检查实现上进行评估,共发现 84 个类型相关缺陷(77 个已确认,22 个已修复),多数由依赖参数多态、重载和高阶函数的 API 测试用例触发;与现有最优方法相比,thalia 生成的测试程序具有不同特征并带来互补收益。

问题
如何自动生成能有效暴露静态类型检查实现缺陷的测试程序,尤其是覆盖标准库 API 所涉及的复杂类型特性。
方法
提出 API 驱动的程序合成,从现有库中提取并组合 API,生成小型良类型客户端程序,并加入故障注入与语义保持模式及测试预言来检验健全性和类型推断精度。
评估
实现 thalia 工具,在 Scala、Kotlin、Groovy 编译器上测试静态类型检查实现,发现 84 个类型缺陷(77 确认、22 修复),并与当前最优方法比较测试程序特征与互补性。
原文摘要(Abstract)

We introduce a novel approach for testing static typing implementations based on the concept of API-driven program synthesis . The idea is to synthesize type-intensive but small and well-typed programs by leveraging and combining application programming interfaces (APIs) derived from existing software libraries. Our primary insight is backed up by real-world evidence: a significant number of compiler typing bugs are caused by small test cases that employ APIs from the standard library of the language under test. This is attributed to the inherent complexity of the majority of these APIs, which often exercise a wide range of sophisticated type-related features. The main contribution of our approach is the ability to produce small client programs with increased feature coverage, without bearing the burden of generating the corresponding well-formed API definitions from scratch. To validate diverse aspects of static typing procedures (i.e., soundness, precision of type inference), we also enrich our API-driven approach with fault-injection and semantics-preserving modes, along with their corresponding test oracles. We evaluate our implemented tool, thalia , on testing the static typing implementations of the compilers for three popular languages, namely, Scala, Kotlin, and Groovy. thalia has uncovered 84 typing bugs (77 confirmed and 22 fixed), most of which are triggered by test cases featuring APIs that rely on parametric polymorphism, overloading, and higher-order functions. Our comparison with state-of-the-art shows that thalia yields test programs with distinct characteristics, offering additional and complementary benefits.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2664,
  title = {API-Driven Program Synthesis for Testing Static Typing Implementations},
  author = {Thodoris Sotiropoulos and Stefanos Chaliasos and Zhendong Su},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {POPL},
  year = {2024},
  doi = {10.1145/3632904}
}