Finding Typing Compiler Bugs
summary
Ephesus builds a program generator that emits large (500–1000 line) polymorphic programs and two transformation tests: type erasure mutation removes optional type annotations to expose inference failures and type-of-writing mutation injects subtle incompatible types to expose unsoundness. The framework tests Java, Kotlin and Groovy compilers and finds 130+ confirmed bugs (86 fixed by developers), including 22 soundness errors; roughly half of bugs come from the generator and half from mutations. Test cases often require manual minimization, and most failures involve parametric polymorphism and generic APIs.
AI-written summary · about
chapters (13)
- 0:00Start
- 0:53Example bug: Rejecting a well-typed program
- 2:13Example bug: Accepting an III-typed program
- 3:08Automated Testing of Compilers
- 6:00Program generation (supported features)
- 7:08Type graph
- 7:43Type erasure mutation (challenges)
- 8:42Type overwriting mutation
- 9:17Evaluation: bug finding results
- 9:47Evaluation: bug and test case characteristics
- 10:47Evaluation: generator and mutations
- 11:00Future work
- 11:55Conclusion
related talks
15mWell-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers
14mFinding Compiler Bugs through Cross-Language Code Generator and Differential Testing
53mLocknote: How Badly Do We Want Correct Compilers?
14mFuzzing C++ Compilers via Type-Driven Mutation
16mGradually Typing Strategies
27mTowards Type Debugging using Partial Evaluation
12mGenerative Type-Aware Mutation for Testing SMT Solvers
56mOn Type-Based Techniques for Program Manipulation