Bonsai：类型系统的基于综合的推理

我们描述了关于类型系统可执行模型的符号推理算法，支持面向类型系统设计者的三种查询。首先，我们检查类型可靠性缺陷，并在发现此类缺陷时综合出一个反例程序。其次，我们比较类型系统的两个版本，综合出一个被其中一个接受而被另一个拒绝的程序。第三，我们最小化综合出的反例程序的大小。这些算法对类型检查器和解释器进行符号求值，生成公式来刻画在类型检查器和解释器中失败或成功的程序集合。然而，对解释器进行符号求值带来了效率挑战，这是由于必须合并各种可能输入程序的执行路径。我们的主要贡献是 Bonsai 树，这是一种新颖的程序和程序状态的符号表示，解决了这些挑战。Bonsai 树以逻辑约束的形式编码复杂的语法信息，从而实现更高效的合并。我们在 Bonsai 工具中实现了这些算法，该工具是类型系统设计者的助手。我们进行了案例研究，探讨 Bonsai 如何帮助测试和探索各种类型系统。Bonsai 高效地综合出了自动工具此前无法触及的可靠性缺陷的反例，并且是首个发现最近报告的 Scala 可靠性缺陷 SI-9633 反例的自动化工具。