电子学报
電子學報
전자학보
ACTA ELECTRONICA SINICA
2012年
11期
2171-2176
,共6页
徐超%何炎祥%吴伟%陈勇%刘健博
徐超%何炎祥%吳偉%陳勇%劉健博
서초%하염상%오위%진용%류건박
编译优化%正确性%模拟关系%定理证明
編譯優化%正確性%模擬關繫%定理證明
편역우화%정학성%모의관계%정리증명
编译器中通常采用各种优化方法来提高目标代码的质量,为了实现较好的效果,一些编译优化算法通常十分复杂,很容易给可靠性和安全性带来隐患.现有的编译器缺陷大部分是由优化阶段引起的.传统的编译优化正确性研究大部分只关注优化算法的正确性,但是只有该算法被正确的实现了才能确保实际运行的优化过程是正确的.本文提出一种基于模拟关系的方法来验证编译优化实现的正确性.在每次优化结束后,我们通过建立优化前代码和优化后代码之间的模拟关系生成优化正确应满足的逻辑条件,然后验证逻辑条件是否成立从而判定编译优化的实现是否正确性.以优化编译中的常量折叠优化和变量替换的验证作为示例显示了本方法的有效性和可靠性.
編譯器中通常採用各種優化方法來提高目標代碼的質量,為瞭實現較好的效果,一些編譯優化算法通常十分複雜,很容易給可靠性和安全性帶來隱患.現有的編譯器缺陷大部分是由優化階段引起的.傳統的編譯優化正確性研究大部分隻關註優化算法的正確性,但是隻有該算法被正確的實現瞭纔能確保實際運行的優化過程是正確的.本文提齣一種基于模擬關繫的方法來驗證編譯優化實現的正確性.在每次優化結束後,我們通過建立優化前代碼和優化後代碼之間的模擬關繫生成優化正確應滿足的邏輯條件,然後驗證邏輯條件是否成立從而判定編譯優化的實現是否正確性.以優化編譯中的常量摺疊優化和變量替換的驗證作為示例顯示瞭本方法的有效性和可靠性.
편역기중통상채용각충우화방법래제고목표대마적질량,위료실현교호적효과,일사편역우화산법통상십분복잡,흔용역급가고성화안전성대래은환.현유적편역기결함대부분시유우화계단인기적.전통적편역우화정학성연구대부분지관주우화산법적정학성,단시지유해산법피정학적실현료재능학보실제운행적우화과정시정학적.본문제출일충기우모의관계적방법래험증편역우화실현적정학성.재매차우화결속후,아문통과건립우화전대마화우화후대마지간적모의관계생성우화정학응만족적라집조건,연후험증라집조건시부성립종이판정편역우화적실현시부정학성.이우화편역중적상량절첩우화화변량체환적험증작위시례현시료본방법적유효성화가고성.
