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

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

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

3 系統(tǒng)原型
　基于形狀圖邏輯，實現(xiàn)了PointerC語言的一個程序驗證器[1]，它能夠驗證使用圖1所定義的各種形狀的程序。除了驗證形狀外，還能驗證節(jié)點上數(shù)據(jù)的一些性質(zhì)。本文對有序鏈表插入節(jié)點的函數(shù)進行了驗證。
　該驗證器分成下面幾個模塊，按所列次序順序執(zhí)行：
　(1)普通編譯器的前端。對源程序進行詞法分析、語法分析和靜態(tài)語義檢查后，生成抽象語法樹。
　(2)形狀分析。遍歷抽象語法樹，根據(jù)形狀聲明和形狀圖邏輯來生成各程序點的形狀圖。
　(3)驗證條件的生成。遍歷抽象語法樹，根據(jù)程序員提供的函數(shù)前后條件和循環(huán)不變式，按最強后條件演算方式為各函數(shù)生成驗證條件。
　(4)驗證條件的證明。將生成的各驗證條件G∧Q?圯Q′，按照上一節(jié)所介紹的方法翻譯成P∧Q?圯Q′的形式，逐個交給證明器進行證明。
本文提出一種利用形狀圖信息來消除訪問路徑別名，使得指針程序仍然可以用Hoare邏輯來進行驗證的方法，并利用可自動定理證明器的支持，開發(fā)了一個PointerC語言的程序驗證器原型，展示了該方法的可行性。
參考文獻
[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.