Semantic Reification: A New Paradigm for Random Program Generation
This program is tentative and subject to change.
We introduce semantic reification, a novel paradigm for random program generation that centers on program semantics rather than syntax. Our key insight is to reformulate random program generation to capture two types of program semantics: (1) compile-time semantics (what a program can do), represented by the control flow graph (CFG), and (2) runtime semantics (what a program actually does), represented by execution paths within the CFG. For any CFG and any execution path on it, semantic reification constructs a program guaranteed to be well-behaved with respect to a specific input and output. This means that when executed with this input, the program deterministically follows the designated execution path to produce the expected output. This paradigm differs from existing work by supporting arbitrary control flow such as unbounded loops and irreducible regions, while still ensuring that the generated programs are semantically correct and terminating. We develop a practical realization of this paradigm. First, we introduce symbolic function reification that integrates a lightweight form of symbolic execution into the generation process to generate an individual, leaf function (i.e., a function that is free of function calls). Each leaf function satisfies the constraints of a given CFG and a selected execution path. Second, we compose multiple leaf functions into a larger, more complex program via semantics-preserving peephole rewriting, guided by an arbitrary call graph. Over five months, our implementation for C compilers, Reify, has uncovered 59 bugs in GCC and LLVM (57 confirmed, 27 fixed), 24 of which are long-latent. Among them, 36 are wrong-code bugs, many are high-priority issues, and most of them involve semantic characteristics overlooked by existing tools. We believe semantic reification opens new directions for research beyond compilers, such as validating debuggers, analyzers, and verifiers.
This program is tentative and subject to change.
Thu 18 JunDisplayed time zone: Mountain Time (US & Canada) change
14:00 - 15:20 | |||
14:00 20mTalk | [SIGPLAN] Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing PLDI Research Papers Yile Gu University of Washington, Ian Neal University of Michigan and Veridise, Jiexiao Xu University of Washington, Shaun Christopher Lee University of Washington, Ayman Said University of Michigan, Musa Haydar University of Michigan, Jacob Van Geffen , Andrew Quinn University of California at Santa Cruz, Baris Kasikci University of Washington | ||
14:20 20mTalk | Trace-Guided Synthesis of Effectful Test Generators PLDI Research Papers Zhe Zhou Purdue University, Ankush Desai Snowflake, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University DOI | ||
14:40 20mTalk | Semantic Reification: A New Paradigm for Random Program Generation PLDI Research Papers Kavya Chopra ETH Zurich, Cong Li ETH Zurich, Thodoris Sotiropoulos ETH Zurich, Zhendong Su ETH Zurich DOI Pre-print | ||
15:00 20mTalk | The Search for Constrained Random Generators PLDI Research Papers Harrison Goldstein SUNY Buffalo, Hila Peleg Technion, Cassia Torczon University of Pennsylvania, Daniel Sainati University of Pennsylvania, Leonidas Lampropoulos University of Maryland at College Park, Benjamin C. Pierce University of Pennsylvania DOI | ||