部分冗余删除的证明变换研究

Proof Transformation for Partial Redundancy Elimination

部分冗余删除优化是一个同时包含有公共子表达式删除和表达式提升的复杂优化,但是对基于部分冗余删除优化的证明变换研究,还停留在对一些简单情况的处理和讨论上.本文在实验室前期优化对证明调整的研究基础上,总结简单优化行为对证明变换的调整过程,通过将部分冗余删除优化细分为简单的PRE、复杂的PRE、复制代码的PRE、前瞻的PRE,给出了不仅是简单的优化调整证明方法,而是包含有基于复杂的部分冗余删除优化的证明变换的方法.

Partiai redundancy elimination, aka PRE,is a subtle optimization that performs common sub-expression elimination and ex- pression motion at the same time. But the research on proof transformation based on PILE,is also remain in some simple situations. In our previous work, we demonstrate the mechanism for proof transformation, a process where a program＇s proof is automatically trans- formed into one for the optimized program alongside the sirnplc optimizing transformation of the program and based on the same data- flow analysis result. In this paper, PRE is broken down into simple PRE, complex PRE and speculative PRE, so that we can give the mechanism for transforming a given program＇s proof to match the optimized program applied PRE,not only sirnplc PRE,but also com- plex optirnizations.