出具證明編譯器中驗(yàn)證條件化簡(jiǎn)和編譯優(yōu)化的研究.pdf

1、程序驗(yàn)證用邏輯證明的方法證明程序滿足其規(guī)范，是實(shí)現(xiàn)安全性的重要方法。出具證明編譯器(Certifying Compiler)是編譯器與驗(yàn)證器的結(jié)合。本文描述的出具證明編譯器項(xiàng)目CComp讓用戶(hù)給出描述程序正確性的規(guī)范，并在源代碼使用霍爾邏輯風(fēng)格的推理規(guī)則產(chǎn)生驗(yàn)證條件(Verification Condition，VC)，經(jīng)由證明器證明后產(chǎn)生證明項(xiàng)。然后將源代碼和規(guī)范轉(zhuǎn)化成底層的匯編代碼和其上的規(guī)范，并利用源級(jí)證明項(xiàng)生成匯編代碼級(jí)證明，最

2、終生成攜帶證明代碼。
　　 CComp由多人協(xié)作完成，本人承擔(dān)項(xiàng)目中的斷言語(yǔ)言設(shè)計(jì)以及驗(yàn)證條件生成和化簡(jiǎn)工作。實(shí)驗(yàn)室先前的項(xiàng)目PointerC[4]，過(guò)大的驗(yàn)證條件規(guī)模成為系統(tǒng)性能的瓶頸。因此CComp采用一系列的措施來(lái)化簡(jiǎn)VC，刪除其中的冗余。
　　 實(shí)用的編譯器會(huì)包含眾多優(yōu)化，以提高程序執(zhí)行的效率。編譯優(yōu)化是一系列程序變換，對(duì)于出具證明編譯中包含規(guī)范的程序，變換前的程序的規(guī)范可能無(wú)法正確或充分地描述變換后的程序，為

3、此程序規(guī)范也應(yīng)該隨著代碼優(yōu)化一起轉(zhuǎn)換。目前關(guān)于出具證明編譯器的項(xiàng)目較少研究編譯優(yōu)化的影響，但編譯優(yōu)化是決定出具證明編譯器是否能走向應(yīng)用的關(guān)鍵因素之一。
　　 本文通過(guò)分析研究，針對(duì)以上兩個(gè)重要問(wèn)題分別提出了相應(yīng)的解決方案，并實(shí)現(xiàn)了原型系統(tǒng)驗(yàn)證方法的合理性。本文的主要貢獻(xiàn)為：
　　 1.為CComp項(xiàng)目設(shè)計(jì)了使用分離邏輯描述的斷言語(yǔ)言和其推理規(guī)則，實(shí)現(xiàn)了相應(yīng)的驗(yàn)證條件生成器；設(shè)計(jì)并實(shí)現(xiàn)了一個(gè)重寫(xiě)系統(tǒng)，實(shí)現(xiàn)了驗(yàn)證條件的化簡(jiǎn)，