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