指針程序的分析以及循環(huán)不變形狀圖的推斷.pdf

1、近年來，計算機軟件系統(tǒng)在日常生活和工作中的地位越來越重要，而計算機軟件規(guī)模也日漸龐大，其安全問題也因此而受到更多的重視。在一些安全攸關(guān)的領(lǐng)域，軟件的高可信已經(jīng)變得十分必要。提高軟件可信程度的一個重要方法就是形式程序驗證。在典型的形式程序驗證過程中，程序員通常需要手工書寫函數(shù)前后條件以及循環(huán)不變式，給程序員帶來了極大的不便。同時，循環(huán)不變式的自動推斷問題又遲遲沒有解決。這都是形式程序驗證在工業(yè)界的應(yīng)用進展緩慢的原因。
　　 研究自

2、動推斷循環(huán)不變式的方法，不僅對程序驗證，而且對程序分析等領(lǐng)域也具有重要的意義。對指針程序而言，數(shù)據(jù)結(jié)構(gòu)的形狀分析給循環(huán)不變式的推斷乃至程序驗證提供很多有用的信息。
　　 本文使用一種新的方式來解決指針程序分析驗證中的困難及循環(huán)不變式的自動推斷問題。我們設(shè)計了一個形狀系統(tǒng)，要求程序員聲明各種遞歸結(jié)構(gòu)類型參與構(gòu)建的數(shù)據(jù)結(jié)構(gòu)的形狀，并聲明指針變量所指向的形狀，以換取編譯器或其他軟件工具檢查程序是否有形狀錯誤，幫助排除所構(gòu)建的形狀偏離程

3、序員期望的程序。與此同時，我們還設(shè)計了一種基于形狀圖邏輯的形狀分析方法，為程序驗證提供指針相關(guān)的循環(huán)不變形狀圖和函數(shù)前后條件形狀圖。
　　 形狀圖是表達程序所操作的聲明指針和動態(tài)分配的結(jié)構(gòu)體中域指針的指向的一種圖形，它不僅準(zhǔn)確地表達了指針之間的相等關(guān)系，還能提供其他有用信息，例如可用來查詢訪問路徑的別名。循環(huán)不變形狀圖是循環(huán)不變式中關(guān)于指針部分的形狀圖表示，描述了循環(huán)不變式中指針之間的相等關(guān)系等信息。形狀圖邏輯把形狀圖看作程序中

4、指針信息斷言的一種圖形表示，并在此基礎(chǔ)上對Hoare 邏輯進行擴展，可用于對操作易變數(shù)據(jù)結(jié)構(gòu)的指針程序的分析和驗證。
　　 基于形狀圖邏輯，采用先形狀分析，后程序驗證的方法，我們實現(xiàn)了一個程序驗證器。該驗證器能夠驗證本文所定義的各種形狀的程序，并且不需要程序員提供有關(guān)數(shù)據(jù)結(jié)構(gòu)形狀的函數(shù)前后條件和循環(huán)不變式，但需要程序員提供非指針型數(shù)據(jù)的函數(shù)前后條件和循環(huán)不變式。本文所設(shè)計實現(xiàn)的方法在一定程度上解決了循環(huán)不變式自動推斷的難題，為程