Towards a Dereversibilizer: Fewer Asserts, Statically

Reversible programming is an unconventional paradigm that offers new ways to construct software. When programs have inherent inverse counterparts, such as compression/decompression, the invertibility of reversible implementations enables a “write once, verify once” approach. The nature of today’s computers is, however, irreversible. This work-in-progress contribution explores the dereversibilization of reversible source programs into irreversible target programs. As a first step into this space, we explore the use of state-of-the-art Satisfiability-Modulo-Theories (SMT) solvers to statically remove redundant assertions. We divide the problem space into two parts: High-level dereversibilization of Janus-like source programs and classical compilation to machine code. In this contribution, we focus on the semantics-preserving removal of assertions from reversible control-flow statements. Our prototype reduces the size of the assembly code and marks the first step towards automatic dereversibilization and new opportunities of using reversible programs.