paperbot · PL 论文追踪

全部论文 待读 收藏

P2 We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators

全覆盖:不完整输入生成器的类型引导修复
OOPSLA 9(OOPSLA2)2025匹配度 2/10 · 该论文属于程序合成/修复与属性测试领域,虽涉及类型引导合成,但未涉及用户核心关注的LLM/Agent、ML系统静态分析、浮点程序分析或贝叶斯程序分析,与研究方向匹配度低。引用 1 inbox
Patrick LaFontaine, Zhe Zhou, Ashish Mishra, Suresh Jagannathan, Benjamin Delaware
crossref: 2026-09-10

AI 速览

一句话:提出基于覆盖类型的枚举合成算法,自动修复不完整的属性测试输入生成器,使其能生成所有满足前置条件的输入。

基于属性的测试(PBT)通过前置/后置条件描述程序语义性质,其有效性依赖于快速生成满足前置条件的输入。当前置条件语义丰富时,纯随机生成难以产生有效输入,用户不得不手写专门的输入生成器,而手写生成器常常是不完整的——无法生成某些满足前置条件的值。本文提出一种新的程序修复技术,能够修补不完整的生成器,使其值域覆盖所有合法输入。其核心是新颖的枚举式合成算法,利用近期提出的「覆盖类型(coverage types)」概念,同时刻画缺失测试值集合以及候选修复所提供的覆盖范围。作者实现了面向 OCaml 生成器的修复工具 Cobb,并在取自 PBT 文献的基准测试集上验证了其修复能力。

问题
手写的属性测试输入生成器往往不完整,无法生成部分满足前置条件的值,导致随机测试无法充分探测程序行为,而用户难以自行发现并补全这些遗漏。
方法
提出一种类型引导的程序修复技术:用覆盖类型刻画合法输入空间中缺失的测试值以及候选修复的覆盖范围,并据此设计枚举式合成算法,搜索能补全生成器值域的修复补丁。
评估
实现 OCaml 生成器修复工具 Cobb,并在来自属性测试文献的一组基准上评估其修复不完整生成器的效果。
原文摘要(Abstract)

Property-based testing (PBT) is a popular technique for automatically testing semantic properties of a program, specified as a pair of pre- and post-conditions. The efficacy of this approach depends on being able to quickly generate inputs that meet the precondition, in order to maximize the set of program behaviors that are probed. For semantically rich preconditions, purely random generation is unlikely to produce many valid inputs; when this occurs, users are forced to manually write their own specialized input generators. One common problem with handwritten generators is that they may be incomplete , i.e., they are unable to generate some values meeting the target precondition. This paper presents a novel program repair technique that patches an incomplete generator so that its range includes every valid input. Our approach uses a novel enumerative synthesis algorithm that leverages the recently developed notion of coverage types to characterize the set of missing test values as well as the coverage provided by candidate repairs. We have implemented a repair tool for OCaml generators, called Cobb, and used it to repair a suite of benchmarks drawn from the PBT literature.

链接与引用

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

BibTeX
@article{paperbot2898,
  title = {We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators},
  author = {Patrick LaFontaine and Zhe Zhou and Ashish Mishra and Suresh Jagannathan and Benjamin Delaware},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA2},
  year = {2025},
  doi = {10.1145/3763158}
}