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

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

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

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