一句话：提出错误枚举方法，通过构造性地注入类型不匹配生成非法类型程序，系统性地发现类型分析器中的可靠性缺陷。
类型分析器的可靠性缺陷往往只在特定条件下才被触发，现有测试技术难以系统性地构造出能暴露问题的非法类型程序。本文提出错误枚举（error enumeration）：给定一个良类型程序 P，在所有可能的程序位置注入类型不匹配，将表达式替换为类型不兼容的表达式，从而探索与 P 仅差一处的非法类型程序。其核心挑战有二：一是在存在类型推断与 refinement 时可靠地注入类型错误——类型推断可能通过调整上下文推断类型而静默“修复”注入的错误；二是让大种子程序的探索在实践中可行。为此作者提出基于使用点的轻量推理技术，利用各元素使用点处已有的类型标注恢复缺失类型，从而保证在使用点产生真正的类型不兼容；并通过只枚举那些最终导致形状特征不同的类型之间比较的错误来剪枝搜索空间。作者实现了工具 Eris，在 Kotlin、Scala、Groovy 编译器中的三个类型分析器以及广泛用于 Java 空指针错误检测的 Checker Framework 上进行评估，共发现 64 个由非法类型程序引起的缺陷，其中 51 个导致不可靠性（unsoundness），13 个导致编译期崩溃；进一步分析表明多数可靠性缺陷只在高度复杂的条件下被触发，超出已有工作的能力范围。
We propose error enumeration, a method that aims to discover soundness defects in type analyzers by generating ill-typed programs by construction. Given a well-typed program P , it systematically injects type mismatches at all possible program locations to explore ill-typed programs that differ from P by replacing one expression with incompatible ones. The core contributions of our work are: (1) soundly injecting type mismatches even in the presence of type inference and refinements, and (2) enabling practical exploration of large seed programs by pruning the search space. Incomplete type information complicates the injection of type mismatches, as type inference can silently ”repair” the injected error by adjusting inferred types in the surrounding context so that the program still type-checks. We address this by introducing a lightweight, usage-based reasoning technique that recovers missing types of program elements by leveraging the existing type annotations at each element’s use site. This enables the injection of errors that guarantee type incompatibilities at the use sites of variables and other expressions. Finally, to prune the search space, we enumerate only those errors that ultimately lead to comparisons between types with distinct shape characteristics. We evaluated our implementation, Eris, on (1) three type analyzers integrated into the compilers of Kotlin, Scala, and Groovy, and (2) the Checker Framework, widely used to identify null-related errors in Java programs. Eris has uncovered 64 bugs caused by ill-typed programs: 51 leading to unsoundness, and 13 to compile-time crashes. Further investigation reveals that the majority of the soundness bugs discovered by Eris are triggered under highly complex conditions, where error injection requires (1) specific combinations of actual vs. expected type pairs at deeply-nested program locations, or (2) reasoning about control flow and missing type information, capabilities that lie beyond the scope of existing work.
@article{SotiropoulosS26,
title = {Enumerating Ill-Typed Programs for Testing Type Analyzers},
author = {Thodoris Sotiropoulos and Zhendong Su},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808320}
}