王 豐，張 俊

1.中國科學(xué)院 上海微系統(tǒng)與信息技術(shù)研究所，上海 200050

2.上?？萍即髮W(xué) 信息科學(xué)與技術(shù)學(xué)院，上海 201210

3.中國科學(xué)院大學(xué)，北京 100049

1 引言

Rust是近年來興起的系統(tǒng)級編程語言，由火狐瀏覽器的開發(fā)商Mozilla[1]研發(fā)和維護(hù)。Rust 旨在不犧牲性能的情況下，實(shí)現(xiàn)內(nèi)存安全和對內(nèi)存的精細(xì)化控制。Rust 目前已經(jīng)被應(yīng)用到大型系統(tǒng)級軟件的開發(fā)中，例如操作系統(tǒng)、設(shè)備驅(qū)動、游戲引擎和網(wǎng)絡(luò)瀏覽器等。和Rust不同，C/C++雖然提供了對內(nèi)存的精細(xì)化控制，但是由于沒有垃圾回收機(jī)制，需要程序員自己手動釋放申請的動態(tài)內(nèi)存，這將會導(dǎo)致大量的內(nèi)存安全問題，例如野指針等等。Java等語言提供了垃圾回收功能，但是程序員對內(nèi)存的控制方面不如C/C++高效。另一方面，垃圾回收運(yùn)行的時候會影響整個程序的運(yùn)行，對程序的性能會產(chǎn)生影響。

Rust 有三個主要特性：所有權(quán)、借用和生命周期。這些特性使得Rust和主流系統(tǒng)級的編程語言有著本質(zhì)的不同。在Rust 中，資源的所有權(quán)是一個變量綁定。當(dāng)一個變量離開它的作用域的時候，Rust會自動釋放這個變量所綁定的資源。資源的所有權(quán)可以被轉(zhuǎn)移。這個特性保證了對任意一個資源，只有唯一的一個所有者。Rust提供了借用機(jī)制，可以讓一個資源被多個變量共享。借用機(jī)制的實(shí)現(xiàn)需要使用引用類型。在Rust中，有兩種引用類型：可變引用和不可變引用?？勺円每梢杂脕硇薷馁Y源，而不可變引用只能用來讀取資源，不能用來修改。Rust的借用機(jī)制有兩條規(guī)則：一個資源如果有多個引用，那么這些引用都必須是不可變引用；可變引用最多只能有一個。Rust 的生命周期機(jī)制用來規(guī)避不安全的借用。任何的借用都必須比資源所有者有更小的作用域。這個機(jī)制消除了很多內(nèi)存問題，例如“野指針”和“釋放后使用”等。

形式化語義是構(gòu)建程序分析和驗(yàn)證工具，例如模型檢查等，和協(xié)助開發(fā)安全可靠的編譯器的基礎(chǔ)。目前來說，Rust 的形式化語義還沒有被充分研究，也沒有一個完備的語義，對程序分析和驗(yàn)證工具的開發(fā)造成了很大的困難。在這篇文章中，提出了針對Rust 語言的形式化可執(zhí)行操作語義KRust。KRust 是第一個刻畫Rust 的形式化可執(zhí)行操作語義。“可執(zhí)行”表示KRust 可以根據(jù)語義，直接運(yùn)行Rust 程序。目前，實(shí)現(xiàn)的語義規(guī)則涉及了Rust 的核心特性：所有權(quán)、借用和生命周期。使用了K 框架[2](以下簡稱K)來開發(fā)。K是專門用來刻畫編程語言語義的工具。使用K 定義的形式化語義有很多好處。首先，K 能自動生成一個解釋器，因此用K 實(shí)現(xiàn)的語義是可執(zhí)行的。另外，K提供了模型檢查和符號執(zhí)行等形式化工具，因此定義好語義規(guī)則后，可以直接使用K提供的工具對Rust程序進(jìn)行形式化分析。

2 Rust特性介紹

2.1 所有權(quán)

所有權(quán)是Rust 最重要的特性，確保了程序中的資源有且僅有一個所有者。

在上面的程序中，第2行定義了一個字符串類型的變量s。此時，s擁有了一個字符串“Hello”。在程序的第3行，s被賦值給了新的變量v。Rust的所有權(quán)機(jī)制導(dǎo)致了s將失去原有字符串的所有權(quán)，v成為了字符串“Hello”的所有者。此后，不能再通過s訪問原來的字符串，因此第4行輸出s內(nèi)容的語句會報錯。

2.2 借用

Rust 提供了借用機(jī)制，通過使用引用類型（&和&mut），可以臨時把資源的所有權(quán)借用給其他變量。

在上面的例子中，第2行和第5行分別使用了mut 關(guān)鍵詞定義了一個可變的變量。在第3行，變量a被借用給了x，但這個借用是不可變借用，因此第4行嘗試通過x來修改a的值會報錯。第6行的借用是可變借用，可以通過y來修改b的值。

2.3 生命周期

Rust 的借用機(jī)制賦予了變量對一個資源臨時的讀寫權(quán)限，而生命周期機(jī)制是用來檢查借用是否有效的手段。

上面的程序首先定義了一個可變變量x。第3行到第6行中間的代碼塊中定義了一個變量y，初始值為2，然后把對y的可變借用賦值給了x。x是在代碼塊之前定義的，x的生命周期一直到程序的最后一行，而y的生命周期在第6行就結(jié)束了。如果x想要借用y的值，Rust 的生命周期機(jī)制則會要求x的生命周期必須包含于y的生命周期。而此時x的生命周期是包含y的，因此第5行的借用和第7行的賦值都無效，并報錯。如果沒有生命周期機(jī)制，x在第6行之后就是一個“空指針”，造成內(nèi)存安全問題。

3 KRust:使用K定義的Rust形式化語義

3.1 K框架

K是一個可執(zhí)行的語義框架，提供了程序狀態(tài)空間和語義規(guī)則的表示方法，可以方便用來定義一門語言的操作語義。K可以自動生成解釋器，來執(zhí)行真實(shí)的代碼。除此以外，K 提供了很多靜態(tài)分析工具，比如模型檢查、符號執(zhí)行和定理證明等。目前，已經(jīng)有很多語言使用K 定義了形式化語義，例如C[3-4]、Python[5]、PHP[6]、Java[7]和JavaScript[8]等。

語義規(guī)則是基于程序狀態(tài)來描述，實(shí)現(xiàn)語義規(guī)則首先需要刻畫程序狀態(tài)。K 提供了“結(jié)構(gòu)”的概念來描述程序狀態(tài)，其中包含了自定義的標(biāo)簽和映射關(guān)系。為了方便閱讀，本文中語義規(guī)則的書寫沒有完全遵循K 的語法。圖1是一個簡單的語義規(guī)則的示例，其規(guī)則用來查找一個變量對應(yīng)的值。規(guī)則中涉及到了三個標(biāo)簽。第一個標(biāo)簽k 用來存儲需要被執(zhí)行的程序語句。第二個標(biāo)簽env 存儲的是映射關(guān)系集合，記錄變量名和地址之間的對應(yīng)關(guān)系。第三個標(biāo)簽store 也是映射關(guān)系的集合，和env 不同，store記錄的是地址和值之間的映射關(guān)系。這個規(guī)則表示的意思是，X會被替換為V，當(dāng)且僅當(dāng)env標(biāo)簽中存在從X到L的映射，并且store中存在從L到V的映射。

Fig.1 Rule for lookup圖1 變量替換規(guī)則

3.2 KRust結(jié)構(gòu)

圖2展示了KRust 用來描述Rust 程序狀態(tài)所使用的15個標(biāo)簽。T標(biāo)簽是K提供的頂層標(biāo)簽，用來包含其他自定義的標(biāo)簽。k 里面記錄的是所有的程序語句。env 記錄變量到地址的映射的集合。control和fstack 用來實(shí)現(xiàn)函數(shù)調(diào)用，fstack 包含的是一個列表，列表里每個元素包含的是一個局部的env 標(biāo)簽、程序語句和返回值類型。genv 是全局的映射關(guān)系。typeEnv記錄的是變量對應(yīng)的類型。變量對應(yīng)的值存儲在store 標(biāo)簽中。mutType 用來記錄一個變量是否是可變的。nextLoc 用來為新申明的變量分配地址，其中僅包含一個整型值，表示下一個可用的地址。borrow 記錄對象是否被其他變量引用了，以及是被可變引用了，還是被不可變引用了。ref 記錄一個變量引用的另一個變量的地址，引用的類型是可變引用還是不可變引用記錄在了refType中。moved記錄對象是否被清理了。mType 記錄成員函數(shù)的類型。methods保存了Trait中定義的函數(shù)接口（Rust的Trait類似于Java 的接口概念）。enumElements 記錄了枚舉類型中的元素。

Fig.2 Configuration of KRust圖2 KRust結(jié)構(gòu)

3.3 語義規(guī)則

KRust 目前已經(jīng)實(shí)現(xiàn)了405條語義，包括了變量的聲明和賦值、變量之間的借用、解引用、函數(shù)（包括結(jié)構(gòu)體中成員函數(shù)）的定義及調(diào)用、結(jié)構(gòu)體、Trait 和模式匹配等。KRust 語義中包含的類型有基本數(shù)據(jù)類型、引用類型、結(jié)構(gòu)體類型、枚舉類型、靜態(tài)數(shù)組和動態(tài)數(shù)組等。KRust也實(shí)現(xiàn)了基本的控制流語義，包括分支判斷和循環(huán)操作等。KRust 實(shí)現(xiàn)了Rust 最重要的3個特性，即所有權(quán)、借用和生命周期。由于篇幅所限，下面僅列舉了5條語義規(guī)則，全部語義詳見KRust源代碼(https://bitbucket.org/jerrywang304/krustcode)。在這些語義規(guī)則中，“?”表示存在一對映射?！?”用來新增加一對映射?！?⊥”表示未定義的值?！癆?(B?C)”表示將原來的映射對“A?B”替換為“A?C”。一條程序語句被K執(zhí)行成功之后，會被替換為K中的特殊符號“·”，然后再繼續(xù)執(zhí)行下一條。

3.3.1 變量聲明

圖3給出的是變量聲明語義規(guī)則。在定義一個不可變且有顯式類型的變量后，首先需要給變量分配一個地址L，并且在env標(biāo)簽中增加從X到L的映射關(guān)系。X并沒有初始化值，因此store 標(biāo)簽中的值為“⊥”。typeEnv中記錄了X的類型為T。mutType中，0代表不可變。moved中，0表示沒有被清理，因?yàn)榇藭r只是定義X。nextLoc中保存的是下一個可用的地址，L已經(jīng)被使用了，則下一個可用地址為L+1。在其他標(biāo)簽中，由于X還未被使用，值都為“⊥”。

Fig.3 Rule for declaration圖3 變量聲明規(guī)則

3.3.2 借用和生命周期

圖4給出的是可變借用語義規(guī)則。如需要把一個變量Y借用給另一個變量X，需要滿足X存活的時間比Y長的條件。L1＞L2限制了X必須在Y之后被定義，即X的生命周期是包含于Y的。moved標(biāo)簽中兩個映射對必須存在，確保X和Y此時沒有被清理。另外，在把Y的可變引用賦值給X之前，Y必須滿足沒有被其他變量所引用，無論是可變引用還是不可變引用。因此，在borrow 標(biāo)簽中，Y的地址L2對應(yīng)的值之前必須是“⊥”，然后需要改成1。在borrow標(biāo)簽中，1表示已經(jīng)被可變引用，0表示已經(jīng)被不可變引用。

Fig.4 Rule for mutable borrowing圖4 可變借用規(guī)則

3.3.3 結(jié)構(gòu)體和所有權(quán)轉(zhuǎn)移

在圖5定義的語義規(guī)則中，S是一個已經(jīng)定義的結(jié)構(gòu)體。X被聲明為可變變量，并且初值為一個結(jié)構(gòu)體實(shí)例，此時X的類型被更新為S。F1是語義規(guī)則中定義的輔助函數(shù)，用來存儲結(jié)構(gòu)體中的字段。TIDs表示的是函數(shù)參數(shù)的類型。在這條規(guī)則中，store 標(biāo)簽中的映射對確保了S的確是一個結(jié)構(gòu)體，否則這條語義不會被執(zhí)行。Vs中存儲的是結(jié)構(gòu)體實(shí)例中字段具體的值。F2是另一個自定義的輔助函數(shù)，用來完成具體的賦值工作，即把Vs賦值給X中的字段，此后可以通過X來獲取這個結(jié)構(gòu)體實(shí)例中的值。

Fig.5 Rule for declaration of struct instance圖5 結(jié)構(gòu)體實(shí)例聲明規(guī)則

圖6定義了結(jié)構(gòu)體變量所有權(quán)轉(zhuǎn)移的規(guī)則。X和Y都是S類型，即結(jié)構(gòu)體變量。把Y賦值給X后，X變?yōu)閅對應(yīng)的結(jié)構(gòu)體實(shí)例的擁有者。F3輔助函數(shù)會將Y中的字段的值，賦值給X中對應(yīng)的字段的值。然后F4輔助函數(shù)會將moved 標(biāo)簽中Y對應(yīng)的值由0改為1，即清理掉Y的結(jié)構(gòu)體實(shí)例。

Fig.6 Rule for ownership move of struct圖6 結(jié)構(gòu)體所有權(quán)轉(zhuǎn)移規(guī)則

3.3.4 結(jié)構(gòu)體成員函數(shù)實(shí)現(xiàn)

圖7這條語義將impl 中的成員函數(shù)依次進(jìn)行處理。env 和store 中的映射對用來確保S是一個結(jié)構(gòu)體。針對每個成員函數(shù)，這條語義會把其轉(zhuǎn)化為全局函數(shù)，函數(shù)名改為“S∷X”，并且更新形參列表，然后遞歸進(jìn)行處理。由于成員函數(shù)的第一個參數(shù)為self，將會占有調(diào)用次函數(shù)的變量的所有權(quán)，因此在mType標(biāo)簽中，將函數(shù)名對應(yīng)的值賦值為自定義的標(biāo)識符“take”，在此成員函數(shù)調(diào)用的時候會被使用，用來轉(zhuǎn)移調(diào)用者的所有權(quán)。

Fig.7 Rule for struct methods圖7 結(jié)構(gòu)體成員函數(shù)規(guī)則

4 測試和應(yīng)用

4.1 一致性測試

和先前文獻(xiàn)中的工作一樣[3-8]，KRust也使用了測試集來測試語義實(shí)現(xiàn)的和Rust 編譯器是否一致，即給定相同的代碼，比較KRust和Rust官方編譯器編譯執(zhí)行后的輸出結(jié)果。采用的測試集包括了Rust編譯器官方測試集和針對每個語義規(guī)則寫的Rust 代碼。Rust 官方提供了針對編譯器的測試集。官方測試集中的大量代碼有調(diào)用庫函數(shù)，調(diào)用外部C 程序代碼，沒有主函數(shù)，只針對Rust 某個版本和只適用于特定操作系統(tǒng)等問題，不完全適合用來做語義對比測試。從官方測試集中選取了157個合適的測試樣例。在這些代碼中，KRust和Rust編譯器表現(xiàn)出了一致的行為。由于這157個測試樣例沒有涵蓋KRust支持的全部語法和語義，在實(shí)驗(yàn)過程中使用了另外34個真實(shí)有效的Rust 代碼。在這部分測試代碼中，KRust 沒有表現(xiàn)出和Rust 編譯器完全相同的行為。在測試結(jié)構(gòu)體成員函數(shù)的語義規(guī)則中，實(shí)驗(yàn)發(fā)現(xiàn)了Rust編譯器的bug。

在上面的例子中，第1行定義了一個結(jié)構(gòu)體，第2行至第6行為結(jié)構(gòu)體實(shí)現(xiàn)了一個成員函數(shù)。這個成員函數(shù)的參數(shù)是self，不是引用，一旦被調(diào)用會導(dǎo)致結(jié)構(gòu)體實(shí)例的所有權(quán)轉(zhuǎn)移。第8行定義了一個結(jié)構(gòu)體實(shí)例。第9行將結(jié)構(gòu)體實(shí)例所有權(quán)進(jìn)行轉(zhuǎn)移。第10行的調(diào)用會導(dǎo)致q被清理掉。但是依然可以在第11行使用q嘗試修改結(jié)構(gòu)體實(shí)例。編譯器沒有在第11行做出警告和報錯。根據(jù)Rust官方文檔的介紹，q對應(yīng)的結(jié)構(gòu)體實(shí)例此時已經(jīng)被清理，不能再被訪問。KRust不會成功執(zhí)行第11行的代碼，因?yàn)樗`反了KRust中定義好的語義規(guī)則，而Rust編譯器沒有在第11行發(fā)出任何警告或者報錯信息。把這個問題報給了Rust社區(qū)。Rust編譯器已經(jīng)對這個問題進(jìn)行了更新，最新版本(1.33.0)對這類操作會給出警告，未來Rust編譯器更加完善后，會直接給出報錯信息。

4.2 應(yīng)用

K 提供的形式化工具，可以用來進(jìn)行模型檢查、可達(dá)性分析、符號執(zhí)行和驗(yàn)證等。

4.2.1調(diào)試器

K自帶的調(diào)試工具可以方便用來查看程序狀態(tài)。

假設(shè)上面的程序名為sample.rs，可以使用如下命令來調(diào)試查看每一條語義規(guī)則執(zhí)行后的程序狀態(tài)。

1.krun sample.rs--debugger

在第4行代碼第一次被執(zhí)行后，調(diào)試器會顯示出如下的程序狀態(tài)。

4.2.2 驗(yàn)證工具

下面是一個具體的驗(yàn)證算法復(fù)雜度的例子。

上面的Rust代碼使用了輾轉(zhuǎn)相減法來計算最大公約數(shù)。K提供了一個配置文件，用來做驗(yàn)證。為了證明算法的復(fù)雜度為O(max(a,b))，需要在配置文件中添加以下內(nèi)容。

time 標(biāo)簽中保存的是一個整數(shù)，函數(shù)每調(diào)用一次，這個數(shù)加1。T1和T2分別代表了函數(shù)調(diào)用前后time標(biāo)簽里的值，T2-T1代表了函數(shù)執(zhí)行的次數(shù)。K的驗(yàn)證工具輸出為“true”，證明了T2-T1 ≤maxInt(X,Y)，即復(fù)雜度為O(max(a,b))。

5 相關(guān)工作

K已經(jīng)成功地被用來定義了多種語言的語義，例如C[3-4]、Java 1.4[7]、JavaScript[8]、PHP[6]、Python3.3[5]、Verilog[9]和Scheme[10]。Rust 和這些語言有著本質(zhì)的不同，不能簡單模仿這些工作，需要重新定義程序狀態(tài)和語義規(guī)則。Rust 的出現(xiàn)吸引了很多研究者的關(guān)注，目前已經(jīng)有一些關(guān)于Rust 測試和語義等方面的工作。Reed 也發(fā)表了Rust 語義相關(guān)的工作，主要針對的是Rust的借用檢查器（borrow checker）。但是這份語義支持的Rust 的語法過于陳舊，并且沒有被實(shí)現(xiàn)，更不能被執(zhí)行[11]。Jung等人使用Coq定義了新的語言λRust和這門語言的語義[12]。這份工作主要研究的是Rust 的所有權(quán)機(jī)制。λRust和Rust 的中間表示（mid-level intermediate representation，MIR）非常相似，但不是真實(shí)Rust語言。并且，λRust定義了比Rust語言本身還多的語義。Dewey等人針對Rust的類型檢查開發(fā)了一款模糊測試工具，并且發(fā)現(xiàn)了Rust 編譯器的問題[13]，這項研究也說明了在開發(fā)安全可靠的編譯器的過程中是需要形式化語義的。目前已有研究人員針對Rust開發(fā)了程序分析工具[14-15]，但是這兩個工作都把Rust轉(zhuǎn)到其他的編程語言，例如C語言，然后應(yīng)用針對這個語言的程序分析工具進(jìn)行分析。但是，把編程語言轉(zhuǎn)換的過程很容易出現(xiàn)不一致的情況，會丟失語言的特性，也很難保證轉(zhuǎn)換的正確性。KRust描述的就是Rust的語義，沒有做任何轉(zhuǎn)變。

6 結(jié)束語

本文給出了第一個針對Rust語言的形式化可執(zhí)行語義KRust。KRust目前涵蓋了Rust中所有的基本類型和基本運(yùn)算；復(fù)合數(shù)據(jù)類型，例如結(jié)構(gòu)體、數(shù)組和動態(tài)數(shù)組，以及枚舉類型；基本的控制流和分支判斷；函數(shù)，包括成員函數(shù)的定義和調(diào)用；Trait；模式匹配等。KRust 實(shí)現(xiàn)的語義規(guī)則涵蓋了Rust 最重要的三個特性，即所有權(quán)、借用和生命周期。為了測試KRust的語義和Rust語義的一致性，使用了真實(shí)有效的Rust 代碼作為測試集，其中包括了Rust 官方編譯器測試樣例。同時，通過一致性對比測試，發(fā)現(xiàn)了Rust編譯器的問題。另外，還介紹了KRust在Rust程序分析和驗(yàn)證上的潛在應(yīng)用。本文主要的工作是實(shí)現(xiàn)Rust 核心語義，未來工作包括實(shí)現(xiàn)更多的語義規(guī)則，使KRust 更加完備，以及把KRust 應(yīng)用到開發(fā)Rust程序分析工具中。