For more details, please refer to our:

PLDI26 paper: https://connglli.github.io/pdfs/reify_pldi26.pdf

GitHub repository: https://github.com/connglli/Reify

RefractIR (by-product): https://github.com/connglli/RefractIR

Muiltiple techniques exist to implement semantic reification.

Our implementation Reify separates leaf function generation from whole program generation, via a lightweight symbolic execution and EMI-based peephole rewrite.

Till now, Reify found more than 60 bugs in GCC & LLVM.

This brings new possibilities due to its natural support for *arbitrary* control flow:

The CFG can be in any shape (eg nested unbounded loops or irreducible regions), but we only reify one terminating well-defined execution path.

Unexecuted blocks can have any legitimate code.

Given any CFG and a selected execution path on top of it, semantic reification constructs

- a CFG-matching program,
- an input, and
- an expected output,

such that execution

- follows that path,
- avoids UB,
- terminates, and
- produces the known output.

We consider program semantics at two dimensions:

- at compile time, a CFG describes what a program *can* do;

- at runtime, an execution path determines what it *actually* does.