Modeling Erlang Compiler IR as SMT Formulas
John Högberg · 2024
Erlang is an unorthodox language that has fault-tolerance and observability (tracing) baked into the language. This allows users to debug production systems without the maintenance overhead of adding these features manually, but comes at the cost of adding a side effect to almost every operation. Because the design choices around tracing err on the side of maximum observability, the compiler does not have much freedom to perform common optimizations, and requires sophisticated analysis to safely apply all but the simplest transformations. Each individual optimization also implements its own bespoke analysis, which is error-prone and difficult to maintain. This report describes an ongoing experiment on translating one of the compiler's intermediate representations (IR) to formulas, enabling the use of a satisfiability modulo theories (SMT) solver to drive analysis as well as prove the semantics-preserving nature of optimizations.