一種驗(yàn)證指針程序的方法

隨著國(guó)家、社會(huì)和日常生活對(duì)軟件系統(tǒng)的依賴(lài)程度日益增長(zhǎng)，安全攸關(guān)軟件的高可信成為保障國(guó)家安全、保持經(jīng)濟(jì)可持續(xù)發(fā)展和維護(hù)社會(huì)穩(wěn)定的必要條件。
　形式驗(yàn)證是提高軟件可信程度的重要方法。粗略地說(shuō)，軟件的形式驗(yàn)證有兩種途徑，第一種是模型檢測(cè)，它通過(guò)遍歷系統(tǒng)所有狀態(tài)空間，能夠?qū)τ懈F狀態(tài)系統(tǒng)進(jìn)行自動(dòng)驗(yàn)證，并自動(dòng)構(gòu)造不滿足驗(yàn)證性質(zhì)的反例。這種方法在工業(yè)界較流行。第二種是邏輯推理，它利用某種程序邏輯進(jìn)行演算，對(duì)程序性質(zhì)進(jìn)行嚴(yán)格的推理，產(chǎn)生驗(yàn)證條件，再利用定理證明器進(jìn)行證明。本文所討論的方法是基于邏輯推理的方式。
　對(duì)于指針程序的推理，關(guān)鍵在于別名的判斷和處理。通常所采用的Hoare邏輯的一個(gè)重要限制是程序中不同的名字代表不同的程序?qū)ο?，即不允許出現(xiàn)別名。
　對(duì)于指針別名判斷的一種解決辦法是采用分離邏輯。使用分離邏輯的一個(gè)問(wèn)題是，通常的自動(dòng)定理證明器都不能證明帶分離合取連接詞（*，Separating Conjunction）的驗(yàn)證條件，必須為分離邏輯設(shè)計(jì)專(zhuān)用的自動(dòng)定理證明工具。
　本文提出一種利用形狀圖信息來(lái)消除訪問(wèn)路徑別名，使得指針程序仍然可以用Hoare邏輯來(lái)進(jìn)行驗(yàn)證的方法。
1 PointerC語(yǔ)言和形狀圖邏輯
1.1 PointerC語(yǔ)言
　PointerC是一個(gè)強(qiáng)調(diào)指針類(lèi)型并增加形狀聲明的類(lèi)C小語(yǔ)言，詳細(xì)的語(yǔ)法信息請(qǐng)見(jiàn)參考文獻(xiàn)[1]。在結(jié)構(gòu)體聲明中，通過(guò)指針域指向形狀的聲明來(lái)確定這種結(jié)構(gòu)體用來(lái)構(gòu)造什么形狀的數(shù)據(jù)結(jié)構(gòu)，同時(shí)也限定了該結(jié)構(gòu)體類(lèi)型的指針?biāo)苤赶虻男螤?。這是對(duì)應(yīng)形狀分析的需求所做的語(yǔ)言擴(kuò)展，所允許的形狀有單鏈表、循環(huán)單鏈表、雙向鏈表、循環(huán)雙向鏈表。
1.2 形狀圖和形狀邏輯
　程序驗(yàn)證之前，首先基于形狀圖邏輯對(duì)程序進(jìn)行形狀分析，形狀分析為每個(gè)程序點(diǎn)構(gòu)建形狀圖，這些形狀圖構(gòu)成程序驗(yàn)證所需要的指針信息。在此通過(guò)舉例來(lái)介紹形狀圖[1]。
　以圖1（參考文獻(xiàn)[1]中有序鏈表節(jié)點(diǎn)插入函數(shù)循環(huán)不變式的形狀圖）為例說(shuō)明形狀圖和程序點(diǎn)指針等信息的聯(lián)系。在圖1中，圓節(jié)點(diǎn)表示指針類(lèi)型的聲明變量；虛邊框的矩形節(jié)點(diǎn)不代表任何程序元素；矩形節(jié)點(diǎn)表示由malloc生成的結(jié)構(gòu)體變量；灰色矩形節(jié)點(diǎn)是濃縮節(jié)點(diǎn)，表示若干個(gè)（可以是0個(gè)）相鄰的、屬于同一數(shù)據(jù)結(jié)構(gòu)的、同類(lèi)型的結(jié)構(gòu)體變量，下側(cè)可以有無(wú)代表被濃縮節(jié)點(diǎn)個(gè)數(shù)的整型表達(dá)式以及約束該表達(dá)式的斷言。若沒(méi)有，則表示被濃縮節(jié)點(diǎn)個(gè)數(shù)是某個(gè)自然數(shù)，但和任何變量或常數(shù)聯(lián)系不起來(lái)。由圖1可知，head == ptr1，ptr == ptr1->next，head指向鏈表的長(zhǎng)度是m，ptr指向濃縮節(jié)點(diǎn)代表m-1個(gè)節(jié)點(diǎn)，可用head(->next)m-1上角標(biāo)的方式來(lái)表示。

可見(jiàn)，形狀圖可以作為程序斷言，它是該圖所能表達(dá)的指針相等、不相等和別名斷言等的合取，包括其中謂詞節(jié)點(diǎn)和濃縮節(jié)點(diǎn)下側(cè)有關(guān)表長(zhǎng)或被濃縮節(jié)點(diǎn)個(gè)數(shù)的整型數(shù)據(jù)斷言。
　　形狀圖邏輯就是基于上面觀點(diǎn)來(lái)設(shè)計(jì)的Hoare邏輯的一種擴(kuò)展。程序規(guī)范的形式是{G∧Q}S{G′∧Q′}，其中G是形狀圖，Q是表達(dá)程序其他性質(zhì)的符號(hào)斷言，兩部分的合取G∧Q作為程序點(diǎn)完整的斷言。本文程序驗(yàn)證器的第一步工作，在無(wú)需程序員提供有關(guān)形狀的函數(shù)前后條件和循環(huán)不變式的情況下，利用形狀圖邏輯對(duì)程序進(jìn)行形狀分析。由于從一個(gè)語(yǔ)句前的G推導(dǎo)該語(yǔ)句后的G′不受Q的影響，因此形狀分析時(shí)，把程序規(guī)范簡(jiǎn)化為{G}S{G′}，以此來(lái)使用形狀圖邏輯的推理規(guī)則，建立各程序點(diǎn)的形狀圖G。在形狀分析的過(guò)程中，還利用循環(huán)不變式推斷算法得出各循環(huán)的循環(huán)不變形狀圖[2]。
　在完成形狀分析后，程序驗(yàn)證器進(jìn)行程序其他性質(zhì)Q的驗(yàn)證。在{G∧Q}S{G′∧Q′}中，若S不是指針操作語(yǔ)句，則G′和G一樣，但Q′可能不同于Q。若S是指針操作語(yǔ)句（指針賦值、分配空間和釋放空間等），則除了G′和G可能不同外，Q′和Q可能也有一些細(xì)微的區(qū)別。下面是本文關(guān)注的部分。
2 指針程序的驗(yàn)證方法
　程序點(diǎn)數(shù)據(jù)結(jié)構(gòu)構(gòu)成的形狀有多種可能時(shí)，則G表示為G1∨G2∨…∨Gn。同樣，Q也可能是Q1∨Q2∨…∨Qm的析取形式。完整的斷言可以整理成析取范式（Disjunctive Normal Form）G1∧Q1∨G2∧Q2∨…∨Gk∧Qk的形式。根據(jù)形狀圖邏輯，可以用析取范式的一種情況為例來(lái)討論，寫(xiě)成G∧Q，G和Q分別都是合取形式。
程序驗(yàn)證器基于形狀圖邏輯[2]進(jìn)行最強(qiáng)后條件演算并產(chǎn)生驗(yàn)證條件，驗(yàn)證條件由證明器Z3[3]自動(dòng)證明。
2.1 形狀圖和符號(hào)斷言之間的聯(lián)系
　符號(hào)斷言Q中允許出現(xiàn)指針是否等于NULL或兩個(gè)指針是否相等的斷言。即使函數(shù)前后條件和循環(huán)不變式中沒(méi)有這樣的斷言，它們也會(huì)因?yàn)槌霈F(xiàn)在條件語(yǔ)句或循環(huán)語(yǔ)句的布爾表達(dá)式中，而在最強(qiáng)后條件演算過(guò)程中被加到Q中。
　Q中指針等于NULL或兩個(gè)指針相等的斷言會(huì)因?yàn)楹虶中的信息重復(fù)而被吸收，或因有矛盾而使得G∧Q為假。
　Q中訪問(wèn)路徑的合法性依賴(lài)于G。例如，在Q中若出現(xiàn)非指針型的訪問(wèn)路徑p -> … -> data，則忽略->data所剩下的前綴應(yīng)該是G上到達(dá)某個(gè)結(jié)構(gòu)節(jié)點(diǎn)的一條訪問(wèn)路徑，若是到達(dá)懸空節(jié)點(diǎn)、null節(jié)點(diǎn)或不存在這樣的路徑則都非法的，若是到達(dá)謂詞節(jié)點(diǎn)則視謂詞節(jié)點(diǎn)展開(kāi)后的情況決定。
　Q中的訪問(wèn)路徑之間是否有別名，Q中的訪問(wèn)路徑和下一條語(yǔ)句S中的訪問(wèn)路徑之間,以及S中的訪問(wèn)路徑之間是否有別名都依賴(lài)于G，即利用G可以判斷。
　在指針操作語(yǔ)句中，在對(duì)指針u賦值時(shí)可能會(huì)影響符號(hào)斷言：符號(hào)斷言中若有以u(píng)或u為前綴的訪問(wèn)路徑，則要用和u相等但不是別名的u′來(lái)代換u。另一個(gè)影響符號(hào)斷言的場(chǎng)合是，在free語(yǔ)句之后應(yīng)該刪除涉及被釋放節(jié)點(diǎn)上數(shù)據(jù)的原子斷言。
　G中也會(huì)有符號(hào)斷言，附加在濃縮節(jié)點(diǎn)上，用來(lái)限制它代表結(jié)構(gòu)節(jié)點(diǎn)的個(gè)數(shù)。G的符號(hào)斷言和Q的符號(hào)斷言不會(huì)有矛盾，但前者有時(shí)會(huì)給出更準(zhǔn)確的信息。

2.2 程序推理規(guī)則的擴(kuò)展
　在使用推理規(guī)則從語(yǔ)句S的前條件G∧Q產(chǎn)生后條件G′∧Q′時(shí)，要保證Q合法、Q和G無(wú)重復(fù)與矛盾。
　先考慮S是指針操作語(yǔ)句。修改指針型數(shù)據(jù)的簡(jiǎn)單語(yǔ)句會(huì)引起指針值的變化，或者是存儲(chǔ)堆塊的增減，因而導(dǎo)致形狀圖的變化。根據(jù)2.1節(jié)的介紹知道，對(duì)Q的影響是訪問(wèn)路徑的替換或者刪除部分?jǐn)嘌?。先假定Q和S無(wú)別名，有別名的情況在考慮非指針操作語(yǔ)句時(shí)介紹。下面給出各種語(yǔ)句規(guī)則。
　(1)指針型賦值語(yǔ)句u=v
　若u既不是null指針也不是懸空指針，則按下面規(guī)則得到后斷言。
　{G∧Q} u = v {G′∧Q[u′/u]}
其中G′是由形狀分析得到的形狀圖，Q[u′/u]表示Q中作為訪問(wèn)路徑（包括作為前綴情況）的u和其相等且不互為別名的訪問(wèn)路徑u′代換。
　(2)對(duì)指針賦值的其他語(yǔ)句
　分配空間語(yǔ)句u=malloc(t)和函數(shù)調(diào)用語(yǔ)句ret=f(act)有關(guān)Q的處理同上面賦值語(yǔ)句的規(guī)則一樣。
　(3)釋放空間語(yǔ)句free(u)
　釋放u指向的節(jié)點(diǎn)后，Q中含u或u的別名的原子斷言不應(yīng)再存在，因此規(guī)則如下：
{G∧Q} free(u) {G′∧Q′}
其中Q′由把Q中含u或u的別名的原子斷言都刪除而得到。
　很容易明白，若Q無(wú)別名，則這些語(yǔ)句的規(guī)則不會(huì)導(dǎo)致Q′出現(xiàn)別名，因?yàn)樗鼈儗?duì)Q做的小修改都不會(huì)引入別名。
　再考慮非指針操作語(yǔ)句。只要前斷言Q和語(yǔ)句S中無(wú)別名，則使用Hoare的賦值公理就是可靠的。若有別名，則可以先用G的信息來(lái)消除別名（把互為別名的訪問(wèn)路徑改成都用其中同一條訪問(wèn)路徑），然后再用賦值公理。定義eliminate_aliases函數(shù)為(S′,Q′)=eliminate_aliases(G, S, Q),它根據(jù)G消除S和Q中的別名，得到S′和Q′。
　把Hoare邏輯的賦值公理限定為無(wú)別名時(shí)才能使用，并增加下面的消除別名推理規(guī)則，就可以對(duì)含訪問(wèn)路徑別名的程序進(jìn)行推理。
對(duì)于修改指針型數(shù)據(jù)的語(yǔ)句，其前斷言Q可能是程序員提供的，例如不排除循環(huán)不變式中 Q存在別名，因此有時(shí)也需要這條規(guī)則。
　復(fù)合、條件和循環(huán)語(yǔ)句的規(guī)則以及推論規(guī)則的形式和Hoare邏輯相應(yīng)規(guī)則的形式一致。

3 系統(tǒng)原型
　基于形狀圖邏輯，實(shí)現(xiàn)了PointerC語(yǔ)言的一個(gè)程序驗(yàn)證器[1]，它能夠驗(yàn)證使用圖1所定義的各種形狀的程序。除了驗(yàn)證形狀外，還能驗(yàn)證節(jié)點(diǎn)上數(shù)據(jù)的一些性質(zhì)。本文對(duì)有序鏈表插入節(jié)點(diǎn)的函數(shù)進(jìn)行了驗(yàn)證。
　該驗(yàn)證器分成下面幾個(gè)模塊，按所列次序順序執(zhí)行：
　(1)普通編譯器的前端。對(duì)源程序進(jìn)行詞法分析、語(yǔ)法分析和靜態(tài)語(yǔ)義檢查后，生成抽象語(yǔ)法樹(shù)。
　(2)形狀分析。遍歷抽象語(yǔ)法樹(shù)，根據(jù)形狀聲明和形狀圖邏輯來(lái)生成各程序點(diǎn)的形狀圖。
　(3)驗(yàn)證條件的生成。遍歷抽象語(yǔ)法樹(shù)，根據(jù)程序員提供的函數(shù)前后條件和循環(huán)不變式，按最強(qiáng)后條件演算方式為各函數(shù)生成驗(yàn)證條件。
　(4)驗(yàn)證條件的證明。將生成的各驗(yàn)證條件G∧Q?圯Q′，按照上一節(jié)所介紹的方法翻譯成P∧Q?圯Q′的形式，逐個(gè)交給證明器進(jìn)行證明。
本文提出一種利用形狀圖信息來(lái)消除訪問(wèn)路徑別名，使得指針程序仍然可以用Hoare邏輯來(lái)進(jìn)行驗(yàn)證的方法，并利用可自動(dòng)定理證明器的支持，開(kāi)發(fā)了一個(gè)PointerC語(yǔ)言的程序驗(yàn)證器原型，展示了該方法的可行性。
參考文獻(xiàn)
[1] ZHANG Y, LI Z P, CHEN Y Y, et al. Shape graph logic and A shape system (Extended Verison).URL:http://ssg.ustcsz.edu.cn/content/shape-graph-logic.2010(11).
[2] NECULA G. Proof-carrying code,In Proc.24th ACM Symp.On Principles of Prog.Lang. New York, 1997(1):106-119.
[3] MOURA L D, BJORNER N. Z3: An Efficient SMT solver, conference on tools and algorithms for the construction and analysis of Systems(TACAS). Budapest, Hungary, volume 4963 of LNCS, 2008:337-340.