基于CTL的循环优化变换描述方法摘要：TRANS是基于CTL的优化变换描述语言，对TRANS语言作了宏扩展，给出了循环嵌套、循环归纳变量、循环依赖及方向向量的时序逻辑描述。从依赖分析的角度对重排序循环优化变换加以考查，并以循环逆转和循环交换为例阐述了其形式化描述方法。关键词：循环优化变换；分支时序逻辑；依赖分析：TP311．5文献标志码：A：1001－3695(2007)07－0049－030引言??优化变换是程序的等价性变换，其目的是提高目标程序的执行性能，或缩短目标程序的代码规模、降低程序的运行功耗等。通常，程序大多数的执行时间都耗费在循环上，旨在发掘和提高循环并发度的优化是现代高性能体系结构下的主要编译优化方法之一。如果变换后的程序与变换前的程序语义等价，则程序变换是正确的。软件测试是保证程序变换正确性的方法之一。JTT是一种编译优化自动化测试工具，用于嵌入式环境下的C++优化编译器的系统测试和回归测试[1]。JTT工具的使用能较大地提高被测编译器系统中优化功能模块的语句覆盖率，使得系统的可靠性得到较大改善。然而JTT工具并没有对优化变换作出精确刻画，难以生成有针对性的测试用例，从而导致测试冗余。??文献[2]提出了一种基于CTL的程序变换语义等价性的证明方法。它通过归纳法证明程序??π和变换后的程序π′的计算序列之间存在互模拟关系R，从而证明程序π与程序π′??之间的语义等价。证明程序变换的正确性需要对变换作出准确的形式化描述。文献[2]给出了优化变换描述语言TRANS，采用带条件的重写规则??I→I??′ifconditions描述变换，变换条件用CTL公式表示。文献[2]对A.V.Aho等人[3]概括的古典优化变换从数据流和控制流的角度加以考查，并应用TRANS语言进行描述，但对文献[4]中概括的循环分布、循环逆转、循环交换等基于依赖分析的循环优化变换难以适用。??1基于CTL的优化变换描述语言TRANS??TRANS是一种基于CTL的优化变换描述语言[2]，其描述变换的通用形式依赖于某些条件的一系列动作：??3基于依赖分析的循环优化形式化描述??在现代编译器中，循环优化变换通常被用来增强并行性和存储访问局部性。许多优化变换包括循环分布、循环合并、循环逆转、循环交换、循环分片等都是重排序变换，它仅改变代码的执行次序而不增加或减少任何语句的执行。任何一种重排序变换如果维持程序中每一个依赖，那么此变换将维持该程序的含义。绝大多数的重排序循环优化变换只改变循环嵌套中某一层或某几层循环的迭代顺序，因而它仅需维持部分依赖就可维持程序的含义。该章从依赖保持的角度出发给出了重排序循环优化变换的形式化描述，并以循环逆转、循环交换为例阐述了该方法。此外，本章关注迭代步长为1的For循环，其他循环可以通过循环规范化转换为该类型的循环[4]。??3．1循环逆转??循环逆转是在循环迭代范围内改变循环遍历的方向。下面的代码：??通过循环逆转变换为??图2给出了上面代码在逆转前和逆转后的控制流图。??为描述循环逆转，必须从循环嵌套中识别出需要逆转的循环。假设对??n层循环嵌套中的第k??层循环作逆转，那么根据本文2．1节中循环和循环嵌套的宏定义有??4结束语??本文对基于CTL的优化变换描述语言TRANS进行了宏扩展，以宏的形式给出了循环嵌套、循环归纳变量、循环依赖以方向向量的时序逻辑描述，扩展了TRANS语言的描述能力。从依赖保持的角度出发，用时序逻辑公式对重排序循环优化变换的条件进行描述，从而对该类优化变换作出了精确和简洁的形式化刻画。今后的工作包括：①由于存在相当一部份的循环优化变换依赖于特定的机器特性，希望将来引入对机器特性的描述，从而对这类优化变换给出刻画方法；②将这一描述结果用于指导针对编译优化的测试用例生成，提升JTT工具的测试能力；③在这一描述结果的基础上，从依赖保持的角度出发，给出循环优化变换正确性的证明。??参考文献：[1]朱丹枫.一种用于测试编译优化的程序控制结构生成算法[D].北京:中国科学院软件研究所,2005.[2]LACEYD.Programtransformationusingtemporallogicspecification[D].Oxford:OxfordUniversityComputingLaboratory,2003.[3]AHOAV,SETHIR,ULLMANJDpilers:principles,techniques,...