一種基于棧區(qū)內(nèi)存模型的C程序別名判斷算法

常 歡，羅奇鳴，李薛劍，陳意云

(中國(guó)科學(xué)技術(shù)大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，合肥 230026) (中國(guó)科大先進(jìn)技術(shù)研究院 中國(guó)科大國(guó)創(chuàng)高可信軟件工程中心，合肥 231283)

1 引 言

C語(yǔ)言因靈活高效的特性廣泛應(yīng)用于系統(tǒng)軟件的開(kāi)發(fā)中.C語(yǔ)言的指針操作沒(méi)有任何保護(hù)，這給C語(yǔ)言帶來(lái)很多不安全因素，導(dǎo)致C語(yǔ)言程序容易出現(xiàn)缺陷.在軍事、航天、醫(yī)療設(shè)備、交通、能源、金融等安全攸關(guān)的應(yīng)用領(lǐng)域, 任何軟件缺陷都可能導(dǎo)致災(zāi)難性的后果，軟件工程的歷史上多次出現(xiàn)了這樣的案例.對(duì)于這些領(lǐng)域用C語(yǔ)言開(kāi)發(fā)的軟件系統(tǒng)，保障其質(zhì)量(尤其是正確性和安全性)是至關(guān)重要的.

目前在軟件產(chǎn)業(yè)界，主要的質(zhì)量保障方法包括軟件測(cè)試、靜態(tài)分析和形式化驗(yàn)證.軟件測(cè)試和靜態(tài)分析只能發(fā)現(xiàn)軟件中存在的錯(cuò)誤而無(wú)法驗(yàn)證程序功能的正確性.在靜態(tài)分析中，指針?lè)治鍪且粋€(gè)不可判定問(wèn)題[1,2].形式化驗(yàn)證可以驗(yàn)證程序的正確性，主要包括兩種方法：模型檢測(cè)[3]和演繹推理[4].模型檢測(cè)的應(yīng)用被限制在狀態(tài)空間有窮的系統(tǒng).在演繹推理中，通常用斷言表示程序中每條語(yǔ)句處的狀態(tài)，由斷言根據(jù)Hoare邏輯[5]、分離邏輯[6]等規(guī)則推理得到驗(yàn)證條件交由Z3[7]等自動(dòng)定理證明器進(jìn)行證明.演繹推理的優(yōu)點(diǎn)是無(wú)誤報(bào)，不要求狀態(tài)空間有窮，并且可以模塊化地進(jìn)行驗(yàn)證.

C語(yǔ)言采用相對(duì)底層的內(nèi)存模型，指針可以指向內(nèi)存的任意位置，并可以在不同類(lèi)型之間自由轉(zhuǎn)換.C語(yǔ)言提供多種內(nèi)存操作，如多級(jí)指針間接訪問(wèn)、任意指針?biāo)阈g(shù)、數(shù)組和結(jié)構(gòu)體數(shù)據(jù)類(lèi)型.因此C語(yǔ)言程序可能發(fā)生空指針、 野指針、數(shù)組越界等多種內(nèi)存安全問(wèn)題.上述原因使得在驗(yàn)證工具內(nèi)建立C的內(nèi)存模型較為困難.

我們之前實(shí)現(xiàn)了一個(gè)PointerC[8]語(yǔ)言程序驗(yàn)證工具，該工具基于形狀圖邏輯[9]對(duì)堆指針程序進(jìn)行驗(yàn)證.目前我們正在研發(fā)一個(gè)基于Hoare邏輯和形狀圖邏輯的安全C語(yǔ)言(以下簡(jiǎn)稱(chēng)為Safe-C)程序驗(yàn)證工具. Safe-C是C99的一個(gè)子集，是在C99的基礎(chǔ)上所設(shè)計(jì)的面向驗(yàn)證的C語(yǔ)言.

Hoare邏輯的核心是Hoare三元組，其形式如下：

{P} C {Q}

(1)

這里的P和Q是斷言而C是命令.P稱(chēng)為前斷言，Q稱(chēng)為后斷言.斷言中不同的左值表達(dá)式代表不同的存儲(chǔ)對(duì)象，而C的編程語(yǔ)言的語(yǔ)義允許存在別名，即不同的左值表達(dá)式可以代表同一個(gè)存儲(chǔ)對(duì)象.在使用Hoare邏輯的賦值規(guī)則前必須消除斷言中的別名，否則會(huì)得到錯(cuò)誤的推理結(jié)果.動(dòng)態(tài)檢測(cè)[10-11]可以通過(guò)編譯和運(yùn)行程序來(lái)獲取內(nèi)存對(duì)象的運(yùn)行時(shí)地址，但在程序驗(yàn)證中無(wú)法做到.如何在驗(yàn)證工具中消除斷言中的別名是一個(gè)技術(shù)挑戰(zhàn).

本文的貢獻(xiàn)在于：第一，根據(jù)C語(yǔ)言的語(yǔ)義提出了一種棧區(qū)內(nèi)存模型，使程序驗(yàn)證工具能夠精確地跟蹤棧區(qū)的多種類(lèi)型的表達(dá)式，包括取地址、多級(jí)解引用、指針關(guān)系運(yùn)算、結(jié)構(gòu)體和數(shù)組等；第二，基于上述內(nèi)存模型，本文提出了一種判斷別名的算法，使得驗(yàn)證條件生成器在應(yīng)用Hoare賦值規(guī)則前準(zhǔn)確完成別名替換.

2 Safe-C驗(yàn)證工具

2.1 安全C語(yǔ)言與程序標(biāo)注

Safe-C在不犧牲C語(yǔ)言靈活性的前提下，對(duì)C語(yǔ)言的各種類(lèi)型增加一些編程約束，使得程序?qū)@些類(lèi)型的變量的操作表現(xiàn)得較為規(guī)矩.約束大都針對(duì)指針類(lèi)型，要點(diǎn)如下：

1) 把堆分配類(lèi)型及其指針和非堆分配類(lèi)型及其指針進(jìn)行區(qū)分，盡量不出現(xiàn)可同為兩者的類(lèi)型和指針.

2) 簡(jiǎn)化堆和其他數(shù)據(jù)區(qū)的關(guān)系，盡量避免出現(xiàn)從堆指向其他數(shù)據(jù)區(qū)的指針，不濫用從其他數(shù)據(jù)區(qū)指向堆的指針.

3) 禁止對(duì)不是指在數(shù)組區(qū)間(包括動(dòng)態(tài)分配的某類(lèi)型的若干個(gè)元素構(gòu)成的區(qū)間)的指針使用指針?biāo)阈g(shù)運(yùn)算.

被驗(yàn)證的程序由安全C語(yǔ)言源代碼和寫(xiě)在注釋中的程序標(biāo)注兩部分組成.程序標(biāo)注是對(duì)于程序行為的形式化說(shuō)明，可用來(lái)生成驗(yàn)證條件.程序標(biāo)注需要符合形式化的語(yǔ)法和語(yǔ)義規(guī)范，為此我們參考ACSL[12]設(shè)計(jì)了面向程序驗(yàn)證的Safe-C語(yǔ)言的程序標(biāo)注規(guī)范SCSL.

2.2 驗(yàn)證工具的主要模塊與驗(yàn)證流程

圖1顯示了驗(yàn)證工具的主要模塊和驗(yàn)證流程見(jiàn)圖1：

圖1 驗(yàn)證工具的主要模塊和驗(yàn)證流程 Fig.1 Modules and procedures of the Safe-C verifier

1) 前端檢查源程序中的代碼和標(biāo)注是否符合Safe-C的要求，同時(shí)收集一些必要的全局信息，然后生成語(yǔ)法樹(shù).

2) 驗(yàn)證條件生成器遍歷語(yǔ)法樹(shù)，首先根據(jù)程序入口處的標(biāo)注產(chǎn)生入口處的斷言，隨后根據(jù)每條語(yǔ)句的演算規(guī)則進(jìn)行演算，產(chǎn)生當(dāng)前程序點(diǎn)的斷言.遇到有程序標(biāo)注的地方，會(huì)產(chǎn)生驗(yàn)證條件驗(yàn)證當(dāng)前程序點(diǎn)斷言是否滿(mǎn)足程序標(biāo)注.另外在每條語(yǔ)句的演算規(guī)則內(nèi)，驗(yàn)證工具還會(huì)適時(shí)檢查程序是否可能出現(xiàn)內(nèi)存泄漏、空指針解引用、越界訪問(wèn)、運(yùn)算溢出等C語(yǔ)言程序中常見(jiàn)錯(cuò)誤.對(duì)于棧區(qū)變量與棧區(qū)指針的操作在驗(yàn)證條件生成器中處理，而將堆指針相關(guān)的操作交由形狀分析模塊處理，并將驗(yàn)證結(jié)果返回給驗(yàn)證條件生成器模塊.

3) 驗(yàn)證條件生成器模塊產(chǎn)生的驗(yàn)證條件由斷言翻譯器模塊翻譯為定理證明器Z3可以識(shí)別的smt2文件，最終交由Z3驗(yàn)證得到驗(yàn)證結(jié)果. ·

3 棧區(qū)內(nèi)存模型

3.1 Hoare邏輯賦值規(guī)則與別名

在使用Hoare邏輯對(duì)高級(jí)語(yǔ)言程序進(jìn)行演繹推理的過(guò)程中，每當(dāng)使用賦值規(guī)則

{Q[E/x]}x=E{Q}

(2)

時(shí)必須保證后斷言Q和賦值語(yǔ)句x=E(E是表達(dá)式)中沒(méi)有潛在的別名，否則Q[E/x]是最弱前斷言的結(jié)論不可靠.例如，對(duì)于賦值語(yǔ)句p→data=3和后斷言p→data+q→data== 6使用Hoare邏輯的賦值公理，可得到該語(yǔ)句前斷言q→data== 3；但該語(yǔ)句的最弱前斷言是p== q‖p!= q&&q→data== 3.在此用賦值規(guī)則未能得到最弱前斷言的原因是，訪問(wèn)路徑p→data和q→data被認(rèn)為是代表不同的程序?qū)ο?，而?shí)際上若p等于q時(shí)，訪問(wèn)路徑p→data和q→data互為別名，它們代表同一個(gè)程序?qū)ο?當(dāng)對(duì)p→data賦值時(shí)，q→data的值也被修改了.由此可見(jiàn)，程序中出現(xiàn)別名增加了程序驗(yàn)證的難度，跟蹤每個(gè)程序點(diǎn)的別名信息對(duì)基于演繹推理的程序驗(yàn)證是重要的.考慮如下的C語(yǔ)言代碼：

int a[3]={1,2,3};

int *p=a;

a[2]=4;

*(p+2)=5;

在這段代碼中，指針p指向了數(shù)組a的首地址.指針導(dǎo)致了別名的出現(xiàn)，也就是兩個(gè)左值表達(dá)式可以代表同一個(gè)內(nèi)存地址.這里*(p+2)與a[2]互為別名.

3.2 棧區(qū)內(nèi)存模型

堆分配和堆指針的處理采用形狀圖邏輯處理[9]，本文僅討論棧區(qū)分配的變量與指針.在編程語(yǔ)言的語(yǔ)義中，通常用環(huán)境和狀態(tài)來(lái)表示變量名稱(chēng)到值的映射.環(huán)境表示將名字映射到存儲(chǔ)單元的函數(shù)，

Env=Var→loc

(3)

而狀態(tài)表示將存儲(chǔ)單元映射到它所保存值的函數(shù).

Store=Loc→Value

(4)

C語(yǔ)言標(biāo)準(zhǔn) 將表達(dá)式分為左值表達(dá)式和右值表達(dá)式.代表內(nèi)存對(duì)象的表達(dá)式是左值表達(dá)式，其余的是右值表達(dá)式.左值相同的表達(dá)式在內(nèi)存中的存儲(chǔ)位置相同，即互為別名.因此消除別名的關(guān)鍵是精確記錄內(nèi)存對(duì)象的左值，從而判斷表達(dá)式的左值是否相同.

根據(jù)以上思路，我們對(duì)式(3)和式(4)分別進(jìn)行擴(kuò)展，用如下兩個(gè)映射定義Safe-C的棧區(qū)內(nèi)存模型.第一個(gè)映射

Env=LExpr→LValue

(5)

表示將左值表達(dá)式映射到左值的函數(shù)，LExpr表示代表內(nèi)存對(duì)象的左值表達(dá)式的集合，LValue表示左值的集合.在驗(yàn)證工具內(nèi)，左值不僅表示抽象的內(nèi)存地址，也包含了左值表達(dá)式的類(lèi)型(type)和長(zhǎng)度(length)信息.第二個(gè)映射

Store=LValue→RValue

(6)

表示左值所代表的存儲(chǔ)單元到右值的映射，RValue表示右值的集合.這里的右值和C語(yǔ)言中的右值含義相同，在驗(yàn)證工具內(nèi)用斷言表示.

我們用一張表來(lái)表示內(nèi)存模型所表示的映射關(guān)系，稱(chēng)作內(nèi)存表.在驗(yàn)證工具內(nèi)部，非指針的右值和指針的右值通常分開(kāi)存放，這樣方便將棧區(qū)變量的賦值與棧區(qū)指針的關(guān)系運(yùn)算分開(kāi)處理.非指針的斷言用符號(hào)斷言Q來(lái)表示，內(nèi)存表用M來(lái)表示.我們?cè)诰哂凶笾档谋磉_(dá)式名字前面加上@作為對(duì)應(yīng)表達(dá)式的左值的名稱(chēng).非數(shù)組類(lèi)型左值@x的長(zhǎng)度默認(rèn)為1，表示在內(nèi)存中占據(jù)1個(gè)x類(lèi)型的長(zhǎng)度.對(duì)于不同的左值表達(dá)式，其左值和右值有不同的產(chǎn)生規(guī)則，以下分別舉例說(shuō)明：

1) 對(duì)于非指針類(lèi)型的變量x，為其產(chǎn)生左值@x，@x保存有x的類(lèi)型信息和長(zhǎng)度(默認(rèn)是1)，x的右值保存在符號(hào)斷言Q中，不出現(xiàn)在內(nèi)存表M中.

2) 如果是一個(gè)指針類(lèi)型變量p，則除了為其產(chǎn)生其左值@p外，還會(huì)根據(jù)其指向產(chǎn)生不同的右值.如果p是空指針或野指針，則其右值為 ull.如果p指向某個(gè)存儲(chǔ)對(duì)象，則指針的右值為存儲(chǔ)對(duì)象的左值，用函數(shù)形式的三元屬性來(lái)表示.三元屬性的定義是

pointer(name,length,offset)

(7)

在前期工作[13]基礎(chǔ)上進(jìn)行改進(jìn)，name不再是程序變量的名字或者是任意的虛擬名字，而是指針?biāo)赶蜃兞康淖笾?，length表示該左值的長(zhǎng)度，offset表示指針的偏移.這樣可以更清晰地記錄指針的指向信息和層級(jí)關(guān)系，從而支持多級(jí)指針間接訪問(wèn).另外，在對(duì)指針的處理中有兩種特殊的情況：

1) 將數(shù)組名看成指向自身所在內(nèi)存區(qū)間首地址的指針.數(shù)組名本身并不是左值，不能出現(xiàn)在賦值表達(dá)式的左邊.但可以被用于取地址操作符&，所以這里將其視作特殊的左值表達(dá)式，產(chǎn)生的左值表示數(shù)組所占的內(nèi)存區(qū)間，其長(zhǎng)度是數(shù)組長(zhǎng)度.另外數(shù)組名可以像指針一樣出現(xiàn)在指針關(guān)系運(yùn)算中，為處理方便，設(shè)置數(shù)組名右值為三元屬性.其三元屬性所對(duì)應(yīng)的name是其自身對(duì)應(yīng)的左值，length為數(shù)組長(zhǎng)度，由于數(shù)組名代表數(shù)據(jù)塊首地址，故offset固定為0.

2) 為函數(shù)入口處的形參指針額外產(chǎn)生一個(gè)特殊的左值表示其指向的存儲(chǔ)單元.這是因?yàn)轵?yàn)證工具以函數(shù)為模塊進(jìn)行驗(yàn)證，實(shí)參并不出現(xiàn)在函數(shù)內(nèi)，實(shí)參所指向的存儲(chǔ)單元也不在本函數(shù)棧內(nèi).即需要為位于函數(shù)棧外的形參所指向的存儲(chǔ)單元產(chǎn)生一個(gè)特殊的左值，以避免信息的丟失.在本文中，在@和形參名之間加上符號(hào)#來(lái)表示形參指針?biāo)赶虻拇鎯?chǔ)單元.特別的，如果有多個(gè)形參指針指向相同的存儲(chǔ)單元，需要在函數(shù)的前條件中加以說(shuō)明，以確保相同的存儲(chǔ)單元只產(chǎn)生一個(gè)左值.

3) 對(duì)于結(jié)構(gòu)體變量賦值需要將結(jié)構(gòu)體展開(kāi)，看作對(duì)其每一個(gè)域的賦值.因此除了為結(jié)構(gòu)體變量產(chǎn)生左值外，還會(huì)根據(jù)每一個(gè)域的類(lèi)型，遞歸地為其每一個(gè)域產(chǎn)生左值和右值.

4) 對(duì)于數(shù)組下標(biāo)表達(dá)式如a[i]產(chǎn)生數(shù)組名a的左值和右值信息，但并不會(huì)為a中的每一個(gè)元素產(chǎn)生左值和右值.這里我們采用一種延遲插入的方式，僅當(dāng)a中的某一元素出現(xiàn)在斷言中，我們才為其產(chǎn)生左值.這樣可以減少驗(yàn)證工具內(nèi)插入和查詢(xún)的開(kāi)銷(xiāo).

5) 對(duì)于解引用表達(dá)式，可以將其轉(zhuǎn)化為上述的某一種左值表達(dá)式，故不再單獨(dú)討論.

考慮如下的代碼片段：

int x=5;

int a[100];

int* p=a;

int* q;

struct {

int d

} s;

則為其產(chǎn)生的符號(hào)斷言Q和內(nèi)存表M如下：

Q:x== 5

M:

LExprLValueRValuex@xa@apointer(@a,100,0)p@ppointer(@a,100,0)q@q ulls@s s.d@s.d

3.3 驗(yàn)證點(diǎn)斷言與內(nèi)存表的構(gòu)造

驗(yàn)證點(diǎn)是程序代碼中函數(shù)入口處、循環(huán)入口處以及其他有程序標(biāo)注的地方.當(dāng)驗(yàn)證工具演算到驗(yàn)證點(diǎn)時(shí)，需要驗(yàn)證當(dāng)前程序斷言是否滿(mǎn)足驗(yàn)證點(diǎn)的標(biāo)注，然后根據(jù)標(biāo)注產(chǎn)生驗(yàn)證點(diǎn)的內(nèi)存表和程序當(dāng)前點(diǎn)的新斷言.函數(shù)入口、循環(huán)入口與其他驗(yàn)證點(diǎn)略有區(qū)別.

3.3.1 函數(shù)入口處內(nèi)存狀態(tài)的構(gòu)造

函數(shù)入口處的協(xié)議稱(chēng)為requires斷言，其經(jīng)過(guò)范式化后可以表示為：

R1‖R2‖…‖Rn

(8)

其中每個(gè)Ri(1≤i≤n)稱(chēng)為析取子式，每一個(gè)析取子式對(duì)應(yīng)于演算過(guò)程中的一個(gè)分支，分支的程序狀態(tài)構(gòu)造如下：

1) 將所有全局變量，函數(shù)形參變量依次填入內(nèi)存表中，并初始化所有變量的左值信息(包括變量類(lèi)型，所在數(shù)據(jù)塊大小等).

2) 非指針變量的右值信息不需要填入表中，仍然保存在斷言中.需要修改時(shí)，直接遍歷斷言語(yǔ)法樹(shù)修改即可.對(duì)于棧指針變量，需要找出程序標(biāo)注中與其相關(guān)的斷言，產(chǎn)生對(duì)應(yīng)的三元屬性，并填入內(nèi)存表中.

我們將每一個(gè)分支的符號(hào)斷言稱(chēng)作Qi，對(duì)應(yīng)的內(nèi)存表稱(chēng)作Mi，則入口處的程序狀態(tài)可以用如下形式表示：

(Q1&&M1)‖(Q2&&M2)‖…‖(Qn&&Mn)

(9)

3.3.2 循環(huán)入口處內(nèi)存狀態(tài)的構(gòu)造

在進(jìn)入循環(huán)之前，首先要驗(yàn)證當(dāng)前斷言是否滿(mǎn)足循環(huán)不變式.即對(duì)斷言的每一個(gè)分支，產(chǎn)生如下的驗(yàn)證條件：

Qi&&GetAssert(Mi)== >Ii‖I2‖…‖In

(10)

其中GetAssert()函數(shù)獲取表中的棧指針相關(guān)斷言，I1‖I2‖…‖In是范式化后的循環(huán)不變式.

根據(jù)循環(huán)不變式生成循環(huán)入口處斷言和內(nèi)存表的方法與函數(shù)入口處的方法類(lèi)似.不同的是在循環(huán)入口處需要將局部變量也考慮進(jìn)去.其他驗(yàn)證點(diǎn)的構(gòu)造和循環(huán)入口處類(lèi)似，不同的是循環(huán)出口處需要再驗(yàn)證一次是否滿(mǎn)足循環(huán)不變式，而其他驗(yàn)證點(diǎn)通常只需要驗(yàn)證一次.

3.4 棧區(qū)賦值語(yǔ)句規(guī)則

3.4.1 取地址和解引用操作

為了支持多級(jí)指針操作，需要根據(jù)內(nèi)存模型和C的語(yǔ)義定義取地址和解引用的操作規(guī)則，規(guī)則定義如下：

LValueRValue&exprN/ALValue(expr)*exprRValue(expr)Store(RValue(expr))

&expr是一個(gè)右值表達(dá)式，不可作為左值表達(dá)式，計(jì)算該表達(dá)式的值得到的是expr的地址(左值).

*expr既可以是左值表達(dá)式，也可以是右值表達(dá)式，作為左值時(shí)其含義是獲取expr指針?biāo)赶虻拇鎯?chǔ)對(duì)象，作為右值時(shí)其含義是獲取指針?biāo)赶虻拇鎯?chǔ)對(duì)象所保存的值.在計(jì)算*expr表達(dá)式的值時(shí)，首先需要查詢(xún)判斷expr指針是否是空指針或野指針，若是則報(bào)錯(cuò).其次需要判斷訪問(wèn)是否越界.例如對(duì)于賦值語(yǔ)句int i=*(q+j); 而言，指針q的右值為pointer(@a,100,k)，表示q指向數(shù)組a的第k個(gè)位置上.則需要產(chǎn)生如下驗(yàn)證條件：

Q&&GetAssert(M)== >0≤(k+j)<100

如果上述蘊(yùn)含式成立，則表示訪問(wèn)合法；如果不成立，則表示訪問(wèn)越界.

3.4.2 棧區(qū)變量賦值

對(duì)棧區(qū)變量賦值，首先需要消除別名.需要消除別名的地方有三處，分別是保存符號(hào)斷言的Qi、內(nèi)存表中Mi中的length字段和offset字段以及賦值表達(dá)式的右子式.遍歷上述三處的每一個(gè)表達(dá)式，根據(jù)本文第4節(jié)提出的判斷別名的算法，將與被賦值表達(dá)式互為別名的表達(dá)式替換為被賦值表達(dá)式.隨后對(duì)賦值語(yǔ)句使用Hoare邏輯賦值規(guī)則在每一個(gè)分支上進(jìn)行演算，演算規(guī)則為：

{Qi&&Mi}
x=E
{(Qi′&&Mi′)[x′/x]&&x== E′[x′/x]}

(11)

其中，Qi′、Mi′和E′分別表示消除別名后的符號(hào)斷言、內(nèi)存表和賦值表達(dá)式的右子式.x′是和x同類(lèi)型的虛擬變量, [x′/x]表示將x替換為x′.如果被賦值的表達(dá)式是結(jié)構(gòu)體變量，那么需要遞歸的對(duì)每一個(gè)域做別名替換操作.

3.4.3 指針關(guān)系運(yùn)算

指針關(guān)系運(yùn)算可以統(tǒng)一表示為以下形式：

p=q+e;

其中p和q是有左值的指針類(lèi)型訪問(wèn)路徑，e是整型表達(dá)式，"+"泛指加減運(yùn)算符.把p=q看成p=q+0的特例.

在演算過(guò)程中，我們將指針的狀態(tài)保存在內(nèi)存表M中，符號(hào)斷言中Q不出現(xiàn)指針相關(guān)的斷言，從而簡(jiǎn)化指針賦值的處理.只需要將右表達(dá)式中的棧指針p的三元屬性的前兩個(gè)屬性復(fù)制并替換左表達(dá)式q中對(duì)應(yīng)的屬性，將右表達(dá)式指針指向的偏移與表達(dá)式e的計(jì)算結(jié)果填入左邊指針的偏移中.推理規(guī)則是：

{Mi={…p== pointer(@v1,length1,offset1),

q== pointer(@v2,length2,offset2)…}}

p=q+e

{Mi′={…p== pointer(@v2,length2,offset2+e),

q== pointer(@v2,length2,offset2)…}}

(12)

其中Mi和Mi′表示賦值前后的內(nèi)存表狀態(tài)，@v1和@v2分別表示語(yǔ)句執(zhí)行前p和q指向的內(nèi)存對(duì)象的左值.

4 判斷別名的算法

3.1節(jié)指出在使用Hoare邏輯的賦值規(guī)則前必須消除斷言中潛在的別名，否則可能導(dǎo)致推理的結(jié)果不正確.要正確的消除別名，首先要判斷兩個(gè)表達(dá)式是否為別名，即判斷兩個(gè)表達(dá)式的左值是否相同.但是內(nèi)存表中并非存有所有的左值表達(dá)式的左值，所以我們基于3.2 節(jié)的棧區(qū)內(nèi)存模型提出一種判斷兩個(gè)左值表達(dá)式是否別名的算法，如圖2 所示.

圖2 判斷別名的算法Fig.2 Algorithm for judging aliases

1) 復(fù)雜訪問(wèn)路徑是含多個(gè)域訪問(wèn)符的表達(dá)式，如p→a.b.其中域訪問(wèn)符包括.和→兩種.但其實(shí)p→a是(*p).a的語(yǔ)法美化，所以可以將→表示成.來(lái)統(tǒng)一處理.若兩個(gè)復(fù)雜訪問(wèn)路徑的最后一個(gè)域相同，則判斷兩個(gè)訪問(wèn)路徑的前綴是否別名.如p→a.b和q.c.b這兩個(gè)表達(dá)式的最后一個(gè)域皆為b，則判斷(*p).a和q.c的左值是否相同，若不相同則兩個(gè)表達(dá)式不為別名.

2) 如果兩個(gè)表達(dá)式是分別是解引用和數(shù)組表達(dá)式，可以將二者統(tǒng)一為數(shù)組表達(dá)式，通過(guò)比較數(shù)組名、數(shù)組表達(dá)式的維數(shù)以及每一維的索引來(lái)判斷兩個(gè)表達(dá)式是否別名.假設(shè)p和q是棧指針，a是數(shù)組，需要比較兩個(gè)表達(dá)式*(p+3)與q[4]是否別名.內(nèi)存表中有斷言p== pointer(@a,10,1)、q== pointer(@a,10,0)和a== pointer(@a,10,0)，此時(shí)可以將兩個(gè)表達(dá)式統(tǒng)一成數(shù)組表達(dá)式均為a[4].通過(guò)比較數(shù)組名稱(chēng)以及第一維的索引，可以判斷出兩個(gè)表達(dá)式互為別名.

3) 如果兩個(gè)表達(dá)式都是簡(jiǎn)單變量，則直接比較二者左值是否相等.簡(jiǎn)單變量在此處包括全局變量、函數(shù)形參變量、局部變量、以及結(jié)構(gòu)體變量的域等.在每個(gè)程序點(diǎn)處構(gòu)造內(nèi)存模型時(shí)已經(jīng)將其加入內(nèi)存表，故可以直接通過(guò)查表判斷二者左值是否相同.

4) 如果兩個(gè)表達(dá)式是其他類(lèi)型，則不會(huì)互為別名.

5 驗(yàn)證實(shí)例

我們以一個(gè)含有結(jié)構(gòu)體和二重指針等復(fù)雜數(shù)據(jù)結(jié)構(gòu)的函數(shù)為例介紹本文提出的棧區(qū)內(nèi)存模型.該函數(shù)的功能是查找一個(gè)數(shù)組中的最大值和最小值并返回，代碼顯示在圖3.我們將重點(diǎn)放在介紹內(nèi)存表的創(chuàng)建、賦值語(yǔ)句的規(guī)則以及如何利用內(nèi)存表來(lái)實(shí)現(xiàn)多級(jí)指針的訪問(wèn)和別名消除.

圖3 包含二重指針和結(jié)構(gòu)體的函數(shù)Fig.3 Function with double pointer and structure

在第8行函數(shù)入口處，根據(jù)函數(shù)前條件構(gòu)造函數(shù)入口處的斷言Q和內(nèi)存表M.本例中函數(shù)前條件(requires)中的標(biāo)注為size > 0 && length(a) == size.根據(jù)3.3.1小節(jié)中的規(guī)則，得到函數(shù)入口處斷言和內(nèi)存表：

Q:size>0

M:

LEx-prLValueRValuea@apointer(@#a,size,0)size@size

第9行處理變量s的聲明，對(duì)其左值進(jìn)行初始化.第10行首先聲明一個(gè)指向結(jié)構(gòu)體的指針p，并用s的地址來(lái)初始化p.第11行聲明一個(gè)二重指針q，并對(duì)數(shù)組名a取地址來(lái)初始化q.帶有初始化的聲明語(yǔ)句可以首先處理聲明，再按賦值語(yǔ)句規(guī)則處理.對(duì)于取地址表達(dá)式，利用3.4節(jié)提出的規(guī)則獲得表達(dá)式左值信息并產(chǎn)生三元屬性作為被賦值指針的右值.

第12行和13行是兩條棧區(qū)變量的賦值語(yǔ)句，第14行是帶有初始化的聲明語(yǔ)句.對(duì)于被賦值的表達(dá)式，如果沒(méi)有出現(xiàn)在內(nèi)存表中且內(nèi)存表中有與之別名的表達(dá)式，則產(chǎn)生的符號(hào)斷言用該別名表達(dá)式；如果沒(méi)有出現(xiàn)在內(nèi)存表且沒(méi)有與之別名的表達(dá)式，則加入內(nèi)存表中.

上述語(yǔ)句執(zhí)行結(jié)束后，得到的斷言和內(nèi)存表如下：

Q: size>0&&s.min== (*q)[0] &&s.max== (*q)[0]&&i== 0

M:

LExprLValueRValuea@apointer(@#a,size,0)size@sizes@ss.max@s.maxs.min@s.minp@ppointer(@s,1,0)q@qpointer(@a,1,0)i@i

對(duì)應(yīng)的函數(shù)的棧區(qū)狀態(tài)可以如圖4所示.

圖4 棧區(qū)狀態(tài)Fig.4 State of the stack area

驗(yàn)證到第17行循環(huán)入口處，我們將棧區(qū)的所有非指針變量和指針變量的斷言合并，并將斷言中的解引用表達(dá)式替換成數(shù)組表達(dá)式，驗(yàn)證是否滿(mǎn)足循環(huán)不變式.在循環(huán)入口合并后的斷言如下：

Q：size>0 &&s.min== a[0] &&s.max== a[0] && i== 0 && a== pointer(@#a,size,0) && p== pointer(@s,1,0) && q== pointer(@a,1,0)

當(dāng)驗(yàn)證完成后，依據(jù)循環(huán)不變式產(chǎn)生循環(huán)后的斷言和內(nèi)存表，此時(shí)的斷言已經(jīng)存在分支.在此我們以第一個(gè)分支為例繼續(xù)向下演算，這里不再展示此處的斷言和內(nèi)存表.

第18行是一個(gè)條件語(yǔ)句，這里將產(chǎn)生分支.符合條件語(yǔ)句的分支將會(huì)在斷言中加入s.max < (*q)[i]這個(gè)斷言.在第19行賦值語(yǔ)句前，首先找出斷言中與被賦值表達(dá)式p→max別名的表達(dá)式.利用第4節(jié)提出的判斷別名算法可以判斷出s.max和p→max是別名，產(chǎn)生虛擬變量@v1替換斷言中所有的s.max.因?yàn)閟.max與p→max左值相同，且s.max已經(jīng)出現(xiàn)在內(nèi)存表中(內(nèi)存表中不會(huì)出現(xiàn)兩個(gè)互為別名的左值表達(dá)式)，故用s.max替換賦值語(yǔ)句中的p→max.隨后執(zhí)行賦值語(yǔ)句.執(zhí)行完后的本分支的符號(hào)斷言和內(nèi)存表為：

Q: size >0 && i

M:

LExprLValueRValuea@apointer(@#a,size,0)size@sizes@ss.max@s.maxs.min@s.minp@ppointer(@s,1,0)q@qpointer(@a,1,0)i@i

第20行的條件語(yǔ)句會(huì)再產(chǎn)生兩個(gè)分支.執(zhí)行完第22行的賦值語(yǔ)句后，驗(yàn)證各個(gè)分支的斷言是否滿(mǎn)足循環(huán)不變式.然后以循環(huán)不變式作為程序斷言繼續(xù)演算.第24行是return語(yǔ)句，驗(yàn)證函數(shù)的返回值是否滿(mǎn)足函數(shù)的后條件.

6 相關(guān)工作對(duì)比

因?yàn)轵?yàn)證C語(yǔ)言相對(duì)困難，所以國(guó)際上成熟的的C語(yǔ)言驗(yàn)證工具也相對(duì)較少.在學(xué)術(shù)界，相對(duì)有影響力的研究成果有VCC[14]、Toccata[15]和VeriFast[16]等.VCC專(zhuān)注于發(fā)現(xiàn)C并發(fā)程序的中的問(wèn)題，而Toccata則將重點(diǎn)放在了精度驗(yàn)證上，二者對(duì)C的數(shù)據(jù)類(lèi)型的支持不夠完善.VeriFast相對(duì)成熟，該工具基于分離邏輯，支持豐富的斷言數(shù)據(jù)類(lèi)型和用戶(hù)自定義謂詞.而我們的驗(yàn)證工具基于Hoare邏輯和形狀圖邏輯，理論路線與之不同.有些比較有影響的驗(yàn)證工具如Spec#[17]只支持驗(yàn)證C#等沒(méi)有指針的面向?qū)ο笳Z(yǔ)言.

如何消除C語(yǔ)言中的別名以及支持C語(yǔ)言中種類(lèi)眾多的表達(dá)式是驗(yàn)證C程序的困難之一.文獻(xiàn)[13]提出了一種三元屬性的棧指針表示方法，支持帶有一級(jí)棧指針程序的驗(yàn)證，但其對(duì)多級(jí)指針間接訪問(wèn)以及復(fù)雜數(shù)據(jù)結(jié)構(gòu)沒(méi)有支持.本文與[13]的區(qū)別在于提出了一種適用于C程序驗(yàn)證工具的棧區(qū)內(nèi)存模型，使程序驗(yàn)證工具能夠精確地跟蹤棧區(qū)多種類(lèi)型的表達(dá)式，包括取地址、多級(jí)解引用、指針關(guān)系運(yùn)算、結(jié)構(gòu)體和數(shù)組等.另外本文還給出了基于該內(nèi)存模型的別名判斷算法，使得驗(yàn)證條件生成器在應(yīng)用Hoare賦值公理前準(zhǔn)確完成別名替換.

7 結(jié)束語(yǔ)

目前該內(nèi)存模型已經(jīng)在Safe-C驗(yàn)證工具內(nèi)實(shí)現(xiàn).限于篇幅，本文只介紹了一個(gè)驗(yàn)證實(shí)例.Safe-C驗(yàn)證工具已經(jīng)驗(yàn)證通過(guò)了一維數(shù)組、二維數(shù)組、二重指針、易變數(shù)據(jù)結(jié)構(gòu)、棧指針、字符串等77個(gè)經(jīng)典C程序，其中包括快速排序、冒泡排序、字符串匹配等經(jīng)典算法.這些程序已經(jīng)上傳至以下網(wǎng)址：https:.github.com/huanGG/Safe-C.