基于抽象解釋的帶指針?biāo)阈g(shù)程序的分析方法.pdf

1、指針作為 C語言的基本語法元素，使用時具有高度的靈活性，這種靈活性雖然為 C語言程序的編寫帶來了極大的便利，卻同時也使得指針使用不當(dāng)成為引發(fā)空指針解引用、數(shù)組越界等非法內(nèi)存訪問的源泉之一。指針?biāo)阈g(shù)是出現(xiàn)在嵌入式程序中常見的一類指針用法。研究帶指針?biāo)阈g(shù)程序的分析對提高航空航天等安全攸關(guān)領(lǐng)域的軟件可信性具有重大意義。
　　抽象解釋為靜態(tài)分析提供了一個通用理論框架?；诔橄蠼忉尩某绦驍?shù)值性質(zhì)分析能有效地分析程序變量的值范圍信息。指針分析

2、技術(shù)能夠有效分析程序中指針變量的指向信息及別名信息。但是單純的數(shù)值分析技術(shù)和指針分析技術(shù)都無法有效處理指針?biāo)阈g(shù)。為此，本文在抽象解釋框架下提出了將數(shù)值分析與指向分析相結(jié)合的面向帶指針?biāo)阈g(shù)程序的分析方法。
　　本文首先設(shè)計了一個精確刻畫指針變量指向信息的內(nèi)存模型，提出了相應(yīng)的用于指針?biāo)阈g(shù)分析的抽象內(nèi)存模型。然后基于該抽象內(nèi)存模型設(shè)計并實現(xiàn)了一個針對指向關(guān)系分析的指向抽象域。在此基礎(chǔ)上，把數(shù)值分析和指向分析結(jié)合起來以通過靜態(tài)分析獲取帶

3、指針?biāo)阈g(shù)程序的數(shù)值不變式和指向不變式，并基于這些不變式結(jié)果實現(xiàn)了帶指針?biāo)阈g(shù)程序運行時錯誤的查找。
　　本文利用開源的數(shù)值抽象域庫 Apron和本文設(shè)計的指向抽象域，基于抽象解釋實現(xiàn)了面向帶指針?biāo)阈g(shù)程序的靜態(tài)分析工具原型。該工具主要分為四個部分：前端預(yù)處理模塊、抽象域庫模塊、不動點求解模塊以及報警模塊。本文實現(xiàn)的工具原型已經(jīng)支持部分帶指針?biāo)阈g(shù) C程序的有效分析，并在其上開展了部分實驗。實現(xiàn)結(jié)果表明，該工具能夠有效地分析指針程序的指向