Generation and verification of COINS compiler optimizers using temporal logic and high-level extensions of optimizers

点击翻译按钮获取中文摘要

We generated a C language compiler optimizers using the low-level intermediate form of the COINS compiler. We specify patterns and transformations of optimizers in CTL-FV, which is a bi-directional temporal logic, and performed model checking.On the other hand, a generic algorithm is made, which converts partial redundancy elimination (PRE) in the normal form into one in the static single assignment form. In addition to the generalization, we have improved the effectiveness and the efficiency of the PRE and the partial dead code elimination which is another code optimization technique similar to PRE. As a new code optimization, we also have proposed atechnique that increases cache-hit ratio.