Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Patrick LaFontaine, Zhe Zhou, Ashish Mishra, Suresh Jagannathan, Benjamin Delaware

TL;DR

This work tackles the challenge of generating inputs that satisfy sparse preconditions in property-based testing by automatically repairing incomplete input generators. It introduces Cobb, a coverage-type guided enumerative synthesis pipeline that characterizes missing inputs with $ uut{b}{\phi}$ coverage types and patches generators using a bottom-up term enumeration driven by a cost model. The approach combines phase-based missing-coverage abduction, sketch localization with typed holes, and a lattice-based patch extraction to guarantee coverage completeness while preserving existing generator behavior. Empirical results across diverse datatypes (lists, trees, STLC terms) show Cobb can repair incomplete generators to achieve coverage-complete outputs, with varying performance depending on component sets and the chosen repair strategy, and it further demonstrates potential for sketch-based synthesis and static data generation in PBT workflows.

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.

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

TL;DR

This work tackles the challenge of generating inputs that satisfy sparse preconditions in property-based testing by automatically repairing incomplete input generators. It introduces Cobb, a coverage-type guided enumerative synthesis pipeline that characterizes missing inputs with coverage types and patches generators using a bottom-up term enumeration driven by a cost model. The approach combines phase-based missing-coverage abduction, sketch localization with typed holes, and a lattice-based patch extraction to guarantee coverage completeness while preserving existing generator behavior. Empirical results across diverse datatypes (lists, trees, STLC terms) show Cobb can repair incomplete generators to achieve coverage-complete outputs, with varying performance depending on component sets and the chosen repair strategy, and it further demonstrates potential for sketch-based synthesis and static data generation in PBT workflows.

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.

Paper Structure

This paper contains 40 sections, 15 theorems, 41 equations, 17 figures, 3 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Background and Overview
  3. Phase 1: Characterizing Missing Coverage
  4. Phase 2: Synthesis
  5. Language
  6. Type System
  7. Input Generator Repair
  8. Inferring Missing Coverage
  9. Localization
  10. Synthesizing Patches
  11. Enumerate
  12. Filter
  13. Extract a Precise Repair
  14. Extract an Imprecise Repair
  15. Implementation
  16. ...and 25 more sections

Key Result

theorem 1

A well-typed test generator of type $\covervdash f \;:\; \overline{x_i: \nuot{b_i}{\phi_i}} \shortrightarrow \nuut{b}{\phi}$, when applied to well-typed arguments $\overline{\covervdash v_i~:~\nuot{b_i}{\phi_i}}$, can evaluate to every value satisfying $\phi[\overline{x_i\mapsto v_i}]$: $\forall v.\

Figures (17)

  • Figure 1: Overview of our proposed pipeline.
  • Figure 2: Three sized generators for non-empty lists of even numbers, followed by refinement and coverage types for their bodies. The direction of the subtyping relation on the types in each column is included. We use $il$ as an alias for int list.
  • Figure 3: Example sets of enumerated terms; elements of $\Sigma_i$ cost less than elements of $\Sigma_{i+1}$.
  • Figure 4: A subset of the join semi-lattice built for $\hole{}_2$ in , where $\Gamma_2 \equiv \Code{n}:\ot{\;\Code{n}}{\Code{int}}{\Code{n} > 0\;}$ and $\phi(\Code{l}) \equiv \lnot \Code{empty}(\Code{tail(l)}) \land \Code{len}(\Code{tail(l)}) \leq (\Code{n}-1) + 1 \land \Code{all\_evens}(\Code{tail(l)})$.
  • Figure 5: syntax.
  • ...and 12 more figures

Theorems & Definitions (27)

  • theorem 1: Type Soundness poirot
  • theorem 2: is Sound
  • theorem 3: is Sound and Total
  • theorem 4: Type Soundness poirot
  • proof
  • theorem 5: is Sound
  • proof
  • lemma 1: Soundness of $\typeInfer{}$
  • proof
  • lemma 2: Soundness of $\localize{}$
  • ...and 17 more