一句话：提出 Ikaros，用生成器与 SMT 预言机系统验证 Scala、Java、Haskell 模式匹配覆盖分析器的可靠性与完备性。
模式匹配已成为函数式与非函数式语言中的常见特性，语言实现通常借助模式匹配覆盖分析器静态检查穷尽性与冗余性。然而，这些分析器可能存在可靠性（漏报不安全模式）与完备性（误报合法模式）缺陷。本文提出一种系统化验证方法：设计代数数据类型与模式匹配语句生成器，支持广义代数数据类型等复杂特性；为避免从头构建参考实现，通过构造方式或 SMT 编码生成穷尽与非穷尽用例，形成通用测试预言，将分析结果与约束求解器交叉检查，从而暴露可靠性与完备性缺陷。该方法在 Ikaros 中实现，并在 Scala、Java、Haskell 三个主流编译器上评估，共发现 16 个缺陷，其中 12 个已修复，7 个为可能导致运行时错误的重要可靠性缺陷。Ikaros 还提供了可扩展框架，可推广至任何具有 ML 风格模式匹配的语言。
Pattern matching is a powerful mechanism for writing safe and expressive conditional logic. Once primarily associated with functional programming, it has become a common paradigm even in non-functional languages, such as Java. Languages that support pattern matching include specific analyzers, known as pattern-match coverage analyzers, to ensure its correct and efficient use by statically verifying properties such as exhaustiveness and redundancy. However, these analyzers can suffer from soundness and completeness issues, leading to false negatives (unsafe patterns mistakenly accepted) or false positives (valid patterns incorrectly rejected). In this work, we present a systematic approach for validating soundness and completeness in pattern-match coverage analyzers. The approach consists of a novel generator for algebraic data types and pattern-matching statements, supporting features that increase the complexity of coverage analysis, such as generalized algebraic data types. To establish the test oracle without building a reference implementation from scratch, the approach generates both exhaustive and inexhaustive pattern-matching cases, either by construction or by encoding them as SMT formulas. The latter leads to a universal test oracle that cross-checks coverage analysis results against a constraint solver, exposing soundness and completeness bugs in case of inconsistencies. We implement this approach in Ikaros , which we evaluate on three major compilers: Scala, Java, and Haskell. Despite pattern-match coverage analyzers being only a small part of these compilers, Ikaros has uncovered 16 bugs, of which 12 have been fixed. Notably, 7 instances were important soundness bugs that could lead to unexpected runtime errors. Additionally, Ikaros provides a scalable framework for extending it to any language with ML-like pattern matching.
@article{paperbot2954,
title = {Validating Soundness and Completeness in Pattern-Match Coverage Analyzers},
author = {Cyril Flurin Moser and Thodoris Sotiropoulos and Chengyu Zhang and Zhendong Su},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763171}
}