王 豐，張 俊

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

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

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

1 引言

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

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

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

2 Rust特性介紹

2.1 所有權(quán)

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

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

2.2 借用

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

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

2.3 生命周期

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

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

3 KRust:使用K定義的Rust形式化語(yǔ)義

3.1 K框架

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

語(yǔ)義規(guī)則是基于程序狀態(tài)來(lái)描述，實(shí)現(xiàn)語(yǔ)義規(guī)則首先需要刻畫(huà)程序狀態(tài)。K 提供了“結(jié)構(gòu)”的概念來(lái)描述程序狀態(tài)，其中包含了自定義的標(biāo)簽和映射關(guān)系。為了方便閱讀，本文中語(yǔ)義規(guī)則的書(shū)寫(xiě)沒(méi)有完全遵循K 的語(yǔ)法。圖1是一個(gè)簡(jiǎn)單的語(yǔ)義規(guī)則的示例，其規(guī)則用來(lái)查找一個(gè)變量對(duì)應(yīng)的值。規(guī)則中涉及到了三個(gè)標(biāo)簽。第一個(gè)標(biāo)簽k 用來(lái)存儲(chǔ)需要被執(zhí)行的程序語(yǔ)句。第二個(gè)標(biāo)簽env 存儲(chǔ)的是映射關(guān)系集合，記錄變量名和地址之間的對(duì)應(yīng)關(guān)系。第三個(gè)標(biāo)簽store 也是映射關(guān)系的集合，和env 不同，store記錄的是地址和值之間的映射關(guān)系。這個(gè)規(guī)則表示的意思是，X會(huì)被替換為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 用來(lái)描述Rust 程序狀態(tài)所使用的15個(gè)標(biāo)簽。T標(biāo)簽是K提供的頂層標(biāo)簽，用來(lái)包含其他自定義的標(biāo)簽。k 里面記錄的是所有的程序語(yǔ)句。env 記錄變量到地址的映射的集合。control和fstack 用來(lái)實(shí)現(xiàn)函數(shù)調(diào)用，fstack 包含的是一個(gè)列表，列表里每個(gè)元素包含的是一個(gè)局部的env 標(biāo)簽、程序語(yǔ)句和返回值類(lèi)型。genv 是全局的映射關(guān)系。typeEnv記錄的是變量對(duì)應(yīng)的類(lèi)型。變量對(duì)應(yīng)的值存儲(chǔ)在store 標(biāo)簽中。mutType 用來(lái)記錄一個(gè)變量是否是可變的。nextLoc 用來(lái)為新申明的變量分配地址，其中僅包含一個(gè)整型值，表示下一個(gè)可用的地址。borrow 記錄對(duì)象是否被其他變量引用了，以及是被可變引用了，還是被不可變引用了。ref 記錄一個(gè)變量引用的另一個(gè)變量的地址，引用的類(lèi)型是可變引用還是不可變引用記錄在了refType中。moved記錄對(duì)象是否被清理了。mType 記錄成員函數(shù)的類(lèi)型。methods保存了Trait中定義的函數(shù)接口（Rust的Trait類(lèi)似于Java 的接口概念）。enumElements 記錄了枚舉類(lèi)型中的元素。

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

3.3 語(yǔ)義規(guī)則

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

3.3.1 變量聲明

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

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

3.3.2 借用和生命周期

圖4給出的是可變借用語(yǔ)義規(guī)則。如需要把一個(gè)變量Y借用給另一個(gè)變量X，需要滿(mǎn)足X存活的時(shí)間比Y長(zhǎng)的條件。L1＞L2限制了X必須在Y之后被定義，即X的生命周期是包含于Y的。moved標(biāo)簽中兩個(gè)映射對(duì)必須存在，確保X和Y此時(shí)沒(méi)有被清理。另外，在把Y的可變引用賦值給X之前，Y必須滿(mǎn)足沒(méi)有被其他變量所引用，無(wú)論是可變引用還是不可變引用。因此，在borrow 標(biāo)簽中，Y的地址L2對(duì)應(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定義的語(yǔ)義規(guī)則中，S是一個(gè)已經(jīng)定義的結(jié)構(gòu)體。X被聲明為可變變量，并且初值為一個(gè)結(jié)構(gòu)體實(shí)例，此時(shí)X的類(lèi)型被更新為S。F1是語(yǔ)義規(guī)則中定義的輔助函數(shù)，用來(lái)存儲(chǔ)結(jié)構(gòu)體中的字段。TIDs表示的是函數(shù)參數(shù)的類(lèi)型。在這條規(guī)則中，store 標(biāo)簽中的映射對(duì)確保了S的確是一個(gè)結(jié)構(gòu)體，否則這條語(yǔ)義不會(huì)被執(zhí)行。Vs中存儲(chǔ)的是結(jié)構(gòu)體實(shí)例中字段具體的值。F2是另一個(gè)自定義的輔助函數(shù)，用來(lái)完成具體的賦值工作，即把Vs賦值給X中的字段，此后可以通過(guò)X來(lái)獲取這個(gè)結(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類(lèi)型，即結(jié)構(gòu)體變量。把Y賦值給X后，X變?yōu)閅對(duì)應(yīng)的結(jié)構(gòu)體實(shí)例的擁有者。F3輔助函數(shù)會(huì)將Y中的字段的值，賦值給X中對(duì)應(yīng)的字段的值。然后F4輔助函數(shù)會(huì)將moved 標(biāo)簽中Y對(duì)應(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這條語(yǔ)義將impl 中的成員函數(shù)依次進(jìn)行處理。env 和store 中的映射對(duì)用來(lái)確保S是一個(gè)結(jié)構(gòu)體。針對(duì)每個(gè)成員函數(shù)，這條語(yǔ)義會(huì)把其轉(zhuǎn)化為全局函數(shù)，函數(shù)名改為“S∷X”，并且更新形參列表，然后遞歸進(jìn)行處理。由于成員函數(shù)的第一個(gè)參數(shù)為self，將會(huì)占有調(diào)用次函數(shù)的變量的所有權(quán)，因此在mType標(biāo)簽中，將函數(shù)名對(duì)應(yīng)的值賦值為自定義的標(biāo)識(shí)符“take”，在此成員函數(shù)調(diào)用的時(shí)候會(huì)被使用，用來(lái)轉(zhuǎn)移調(diào)用者的所有權(quán)。

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

4 測(cè)試和應(yīng)用

4.1 一致性測(cè)試

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

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

4.2 應(yīng)用

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

4.2.1調(diào)試器

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

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

1.krun sample.rs--debugger

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

4.2.2 驗(yàn)證工具

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

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

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

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

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