Generating Conforming Programs With Xsmith
summary
Xsmith is a Racket DSL and library that generates conforming programs — syntactically, statically and dynamically valid tests that avoid undefined or nondeterministic behavior — by composing reusable properties and canned components. It reduces generator size from the scale of 39,000 LOC vs few hundred lines, emits test cases via a choice-based AST builder, and powers generators for Racket, Dafny, Standard ML and WebAssembly. Evaluation finds 46 deep semantic bugs across four implementations, demonstrating the approach works.
AI-written summary · about
chapters (16)
- 0:00Xsmith and conforming programs
- 1:25Random testing needs conforming programs
- 3:53Challenge of program generators
- 4:57Xsmith simplifies generator creation
- 6:45Writing Xsmith specifications
- 8:12Generating ASTs step by step
- 10:21Customizing with properties
- 12:08Encoding types and rules
- 13:56WebAssembly generator example
- 14:37Reusing language components
- 15:41Evaluating Xsmith’s effectiveness
- 16:41Comparing generator sizes
- 17:22Bug categories found
- 18:23Real-world bugs discovered
- 20:28Xsmith conclusions and future
- 21:36Q&A
related talks
38mLiving with Spec
22mBoosting Compiler Testing by Injecting Real-World Code
45mLanguage-Oriented Programming with Racket
28mLanguage Support for Property-Based Testing
16mRandomised Testing of the Dafny Compiler
24mSeamless Code Generator Synchronization in the Composition of Heterogeneous Modeli...
15mGrammar-Based Testing for Little Languages: An Experience Report with Student Compilers
22mDSLs in Racket: You Want It How, Now?