Verifiable SSA program representation for aggressive compiler optimization

摘要

We present a verifiable low-level program representation to embed, propagate, and preserve safety information in high performance compilers for safe languages such as Java and C#. Our representation precisely encodes safety information via static single-assignment (SSA) [11, 3] proof variables that are first-class constructs in the program.