Reify es una herramienta de generación aleatoria de programas basada en reificación semántica, diseñada para poner a prueba compiladores de C y, potencialmente, otras máquinas virtuales. Su propósito es producir funciones y programas en C libres de comportamientos indefinidos (UB), de modo que cualquier discrepancia detectada al ejecutarlos pueda atribuirse con alta probabilidad a un fallo del compilador y no a una peculiaridad del estándar.
El proyecto, publicado en GitHub bajo licencia MIT, se acompaña de un artículo científico aceptado en PLDI'26 (ACM SIGPLAN Conference on Programming Language Design and Implementation). Según la documentación, con Reify se han descubierto y reportado 59 errores en los compiladores GCC y LLVM, lo que ilustra el valor práctico del enfoque. En la actualidad, la herramienta admite únicamente tipos i32, arreglos de i32 y estructuras de i32, aunque los autores trabajan en ampliar el soporte a otros tipos primitivos y agregados, además de experimentar con la generación de bytecode de Java y de eBPF. Estas líneas experimentales ya han destapado un error en el compilador JIT de OpenJ9 y dos errores en el runtime de eBPF del núcleo Linux.
El flujo de uso parte de la compilación con un compilador compatible con C++20 (GCC 10+ o Clang 10+) y de la instalación de Bitwuzla, un solucionador SMT. A partir de ahí, el script fuzz.py permite lanzar baterías de pruebas contra GCC o Clang con parámetros concretos, mientras que rysmith genera funciones individuales y rylink compone programas completos a partir de un conjunto de funciones. Cada función generada se acompaña de su código en C, un archivo con mapeos de entrada y salida que garantiza la ausencia de UB, su representación en S-expression y un programa principal para compilarla y ejecutarla. Existe además un modo experimental que extrae grafos de control de flujo de herramientas como Csmith o YARPGen para reutilizarlos como punto de partida.
Los autores también desarrollan un lenguaje simbólico experimental llamado symlang, sobre el cual existe una reimplementación de Reify con soporte enriquecido para punteros, vectores e intrínsecos. Entre las limitaciones reconocidas destacan la posibilidad de que la generación de funciones individuales tarde mucho o falle por restricciones insatisfacibles —motivo por el que los comandos se invocan con un timeout de tres segundos— y el hecho de que la generación de bytecode de Java y eBPF todavía es inestable y se considera experimental.