面向RISC-V的匯編程序語義等價性自動化測試系統①

徐學政, 王 濤, 方 健, 張光達

(軍事科學院 國防科技創新研究院, 北京 100097)

1 引言

1.1 研究背景

RISC-V是一個基于精簡指令集(RISC)原則的開源指令集架構, 因其精簡、開放、模塊化的設計和高可定制的特點在工業界和教育界廣受歡迎.隨著面向RISC-V的處理器接連問世, 圍繞RISC-V建設完善的軟件生態系統將會大大提高系統和應用軟件的設計開發效率, 并降低其維護成本.

在面向RISC-V的軟件開發過程中, 尤其是基于擴展指令 (例如向量擴展指令或用戶自定義指令) 進行程序開發時, 很難避免以手寫匯編的方式為程序編寫高效的匯編代碼.例如, 為標準的C函數庫編寫相應的向量版本函數.與編譯器自動生成的代碼不同, 手工開發的匯編代碼雖然可以最大限度地提高程序的效率, 但繞過了編譯時對程序的約束 (如類型檢查[1]、寄存器分配[2]等), 因而對開發者提出了更高的要求.如果開發者經驗不足或對指令的理解有誤, 將會為代碼的正確性和安全性埋下隱患.以向量擴展指令為例, 為常用函數(如strlen、memcpy等) 的標準版本開發相應的向量版本后, 能否快速地、自動化地測試向量版本與標準版本的函數在語義上是否等價, 將大大影響代碼的正確性和軟件開發和調試的效率.

1.2 研究現狀

國內外學者已提出多種程序測試方法[3-5], 主要分為靜態和動態兩種測試思路: (1) 靜態測試利用形式化的方法[6](如符號執行[7]等), 通過對程序語句的語義建模, 模擬程序的執行, 從而達到對程序正確性的驗證.該方法不依賴指令的軟硬件運行環境, 能夠對程序的分支進行全覆蓋從而達到嚴格的驗證結果, 但隨著程序規模的擴大, 靜態方法的運算量呈現指數級增長.因別名、分支條件不可解等因素而被迫對程序采取保守的建模方式, 也會為靜態分析帶來大量誤報[8]; (2) 動態測試 (如模糊測試[9]等) 給定程序的輸入值, 運行測試程序以觸發程序中的錯誤.雖有效避免了誤報, 但在程序分支的覆蓋率上往往很難匹及靜態方法.此外, 學術界也利用靜態和動態相結合的方式[10,11]對軟件測試提供新的思路.CASM-Verify[11]結合隨機測試和符號執行驗證密碼算法在X86_64和SSE的匯編實現上的等價性, 但缺乏針對RISC-V的支持.

目前, 面向RISC-V的指令或系統級軟件模擬器(如Spike、Qemu[12]、Ovpsim等) 可以為程序提供動態測試環境.針對某段待測試的匯編程序, 并給定輸入值和期望的輸出值, 開發者能夠在模擬器上對匯編程序進行功能級測試.例如, Ovpsim提供了以測試用例為主導的測試腳本, 開發者可以通過將程序的運行結果 (某些寄存器或內存的值) 與參考值進行比對, 以達到測試的目的.然而, 這種方式并無法滿足語義等價性測試的需求, 因為: (1) 現有框架只針對單一測試程序,缺乏對多個程序語義等價性測試的框架; (2) 比對程序的實際輸出值與參考值, 并不足以支持語義等價性測試, 指令運行過程中產生的副作用 (如是否更改了其他寄存器和內存的值) 并未納入考慮, 將為程序的正確性和安全性埋下隱患.

本研究基于模擬器的動態測試環境, 聚焦于設計并實現一套面向RISC-V的匯編程序語義等價性自動化測試系統, 旨在提高RISC-V匯編程序的開發與測試效率.針對已有框架的不足, 本文設計并實現了針對多個RISC-V匯編程序語義等價性的測試框架.系統可通過跟蹤機器狀態, 捕獲程序執行的副作用, 并結合用戶定義的測試目標生成測試報告.實驗表明, 本系統相比已有的測試系統, 能夠有效地對RISC-V匯編程序的語義等價性進行測試.

本文結構如下: 第2節簡要介紹了RISC-V的應用程序二進制接口; 第3節對本文研究的問題進行形式化描述; 第4節和第5節分別對系統設計和系統實現進行詳細介紹; 第6節介紹了實驗設計及結果并進行了案例分析; 第7節進行了總結和展望.

2 RISC-V的應用程序二進制接口

本節以RV64G默認的LP64D規范為例, 簡要介紹RISC-V的應用程序二進制接口 (Application Binary Interface, ABI).ABI規定了RISC-V二進制的寄存器規范、運行時棧的空間分布、函數調用規范、C語言類型細節、ELF文件格式、尋址方式等, 影響了編譯工具鏈中指令生成、寄存器分配、ELF文件生成等諸多方面.了解ABI規范對于匯編程序的測試至關重要,例如返回值的傳遞規范將影響程序的觀測值的選定.本節簡要介紹其中寄存器規范、運行時棧分布和函數調用規范3個方面.

2.1 寄存器規范

依照LP64D規范, RISC-V的通用寄存器包含32個整型寄存器, 32個浮點寄存器和32個向量寄存器.

32 個整型寄存器中, 0號寄存器x0恒為全0; 16個為調用者負責保存 (caller-saved) , 寄存器值在函數調用之后的值可能被修改; 16個為被調用者負責保存 (calleesaved) , 寄存器值在函數調用之后不會更改.其中x10-x17共8個寄存器為參數寄存器 (即a0-a7寄存器);32個浮點寄存器中, 20個為caller-saved, 12個為callersaved, 同樣具有8個參數寄存器; 32個向量寄存器 (以及vl、vtype等) 均為caller-saved.

2.2 運行時棧的空間分布

運行時棧負責維護函數執行時傳遞的參數、臨時變量、callee-saved寄存器等.依照LP64D規范, 運行時棧空間從高地址向低地址生長, 以16字節對齊.具體的空間分布如圖1所示.

圖1 RISC-V運行時棧的空間分布示意圖

2.3 函數調用規范

函數調用規范 (calling convention) 主要規定函數調用時參數和返回值如何傳遞, 本節依照LP64D, 主要分為5部分進行介紹: 整型參數、浮點參數、結構體參數、變長參數和返回值.

整型參數傳遞的主要原則是: 對于大小不超過64 bit的參數, 使用單個整型參數寄存器; 對于大小在64 bit和128 bit之間的參數, 使用連續的兩個整型參數寄存器, 低64 bit和高64 bit分別放在寄存器x(n)和x(n+1)中, 若僅剩一個整型參數寄存器, 低位使用寄存器, 高位則使用棧傳遞; 若無可用的整型參數寄存器, 使用棧傳遞, 參數自右向左依次壓棧.

浮點參數傳遞的主要原則是: 對于大小不超過64 bit的參數, 使用單個浮點參數寄存器, 不足64 bit的浮點數進行1擴展; 若無可用的浮點參數寄存器, 使用整型參數寄存器代替; 若無可用的整型參數寄存器, 將參數自右向左壓棧.

結構體參數傳遞的主要原則是: 若結構體無浮點數成員, 可看作1個整型參數, 依照整型參數傳遞原則處理, 結構體內存分布不變; 若僅包含1個(或2個)成員, 均為浮點數且均為超過64 bit, 則使用1個(或2個)浮點參數寄存器傳遞; 若僅包含1個整型成員和1個浮點成員, 均不超過64 bit, 則分別使用1個整型和1個浮點參數寄存器傳遞; 其余情況均參照整型參數傳遞原則.

C語言中的變長參數分為有名和無名參數, 無名參數以省略號代替, 其類型和個數編譯時未知, 由調用者通知被調用者本次調用的參數類型和個數(例如printf以格式化字符串的形式), 并默認執行參數的類型提升(例如將float提升為double).變長參數傳遞的不同之處在于: 使用連續的兩個寄存器傳遞64 bit至128 bit的參數時, 第1個寄存器必須為偶數號; 被調用者先將所有使用寄存器傳遞的無名參數進行壓棧, 并計算首個無名參數在棧中的地址.

返回值可看作被調用者向調用者傳遞的參數, 以前兩個參數寄存器傳遞返回值.如果返回值超過128 bit(需要以指針的方式間接傳遞), 調用者負責為返回值在棧中分配空間, 并隱式地將其在棧中的地址作為第1個參數傳遞, 實際的參數依次后移.

3 問題描述

3.1 機器狀態模型

一個簡單的機器狀態模型可將機器狀態m用一系列的“鍵-值”對 (k,v)來描述.即:

同時, 值v可由下式表示:

其中, 鍵k可由寄存器名稱或內存地址構成, 值v可由十六進制數字表示.例如, 可將值為0xffff的寄存器x1表示為 (x1, 0xffff), 值為0x17的內存地址0x7f7e9b18表示為(0x7f7e9b18, 0x17).

給定程序p和初始 (輸入) 機器狀態mI, 機器可通過運行p得到新的 (輸出) 機器狀態mO, 該過程可用p(mI)=mO表示.

3.2 一般的程序測試模型

我們將一般的基于測試用例的程序測試 (簡稱一般測試) 模型描述為: 對程序p輸入一組初始機器狀態,并設置相對應的期望輸出的機器狀態, 通過判斷以下關系是否成立以測試程序p的正確性:

實踐中, 輸入的機器狀態可由測試的運行環境 (初始化程序、輸入參數等) 給定, 而期望的輸出狀態卻難以完整描述, 一般只通過某個 (或多個) 變量的值描述.例如, 針對某個輸出狀態mO, 期望的函數的返回值為1, 可記為mO={(a0, 0x1)}.顯然, 不完整的機器狀態描述為測試帶來諸多隱患.例如, 程序滿足期望的輸出值并通過測試, 但其間可能修改了預期之外的內存值或callee-saved寄存器值從而引發安全問題.

3.3 語義等價性測試模型

對于兩段程序p0和p1和任意的機器狀態m, 嚴格的語義等價可描述為:

該定義需對比任意輸入狀態下的完整輸出機器狀態以確保語義的等價, 相比一般測試模型具有更為嚴格的定義以確保捕獲程序的副作用.顯然, 我們無法負擔對任意機器狀態的窮舉.另外, 完整地描述機器狀態通常是沒有必要的.例如, 在第2節介紹的ABI中, RISC-V的32個整型寄存器中有16個屬于調用者維護, 允許用戶程序進行修改而無須恢復現場, 若兩個待測程序對某些調用者維護的寄存器進行了不同的修改, 仍可認為其語義等價.實際上, 在調用者維護的寄存器中,除用于存放返回值的寄存器外, 大部分寄存器無須在測試中進行描述.

我們將語義等價性測試模型描述為三元組(P,M,K), 包括一組待測程序P={p0,p1,p2,···}, 一組作為輸入的機器狀態M={m0,m1,m2,···}以及一組作為測試標準的鍵K={k0,k1,k2,···}.當滿足以下條件時, 程序通過語義等價性測試:

與一般的測試模型不同的是, 語義等價性測試模型: (1) 規定了一組鍵作為測試標準, 通常包括返回值寄存器a0, 被調用者維護的寄存器、某些內存值等, 遠遠多于一般測試的某幾個觀測值; (2) 無須給定輸入機器狀態對應的輸出機器狀態, 即無須由用戶為相應鍵k計算值v.

4 系統設計

基于第3.3節介紹的語義等價性測試模型, 我們設計了面向RISC-V的匯編程序語義等價性自動化測試系統.本節介紹總體框架(4.1節)以及其中的系統配置(4.2節)、測試運行(4.3節)和結果分析(4.4節)3個環節.

4.1 總體框架

測試系統的整體流程如圖2所示.其中, 系統配置環節準備了測試所需的測試用例和一組待測程序, 并由用戶配置測試目標.之后, 系統分別運行各個待測程序并同時追蹤機器的狀態變化, 記錄下在運行過程中被更改的機器狀態.最后, 通過比對各個待測程序更改的機器狀態, 結合測試目標, 生成語義等價性測試的測試報告.

圖2 語義等價性測試系統整體流程圖

4.2 系統配置

4.2.1 生成測試用例

測試用例的生成[13,14]與本系統相對獨立, 可以采用手工編寫或在給定約束下自動生成兩種方法.與傳統的“輸入-輸出”模式的測試用例不同, 語義等價性測試并不要求用戶給定期望的輸出值, 只需要比對待測程序的運行結果是否一致即可, 這大大減少了生成測試用例的工作量.本系統采用測試用例的自動生成, 以函數int add(inta, intb)為例, 在給定參數的數據類型int的前提下, 系統隨機生成一系列測試用例, 如a=1,b=2;a=99,b=-99等.

4.2.2 準備待測程序

為保持待測程序運行前機器狀態的一致性, 系統分別對每個待測程序進行“匯編-鏈接”, 生成可執行文件 (見圖3).其中測試用例負責準備輸入參數并調用相應的待測程序, 為提示模擬器待測程序運行的開始和結束, 系統在待測程序的開始和結束插入兩條指示性的自定義指令test_start和test_end, 并同時在匯編器和模擬器中添加支持.另一個可行的實現思路是: 通過保存模擬器的狀態, 實現在同一狀態下分別調用不同的待測程序.

圖3 待測程序生成可執行文件流程圖

4.2.3 配置測試目標

用戶的測試目標, 即第3.3節中的集合K, 在本系統中是可配置的, 覆蓋寄存器及內存的值.具體地, 用戶需要配置: (1) 觀測目標, 包括反映程序功能正確性的寄存器或內存的值 (如作為返回值的a0寄存器); (2) 約束條件, 包括是否允許待測程序修改被調用者維護的寄存器或其他內存值.

4.3 測試運行

單個待測程序的測試運行流程如圖4所示.系統基于RISC-V軟件模擬器對輸入的可執行文件進行譯碼和執行, 在識別自定義的test_start后, 記錄初始的機器狀態, 運行待測程序, 并同時跟蹤機器狀態的變化,直至運行test_end后, 記錄最終所有被更改的機器狀態.

圖4 單個待測程序測試運行流程圖

4.4 結果分析

圖5給出了系統針對一組待測程序的測試運行和結果分析流程圖.系統通過將多個更改的機器狀態進行比對, 結合用戶配置的測試目標, 形成最終的測試報告.若所有待測程序在觀測目標上產生了相同的結果并滿足其他約束條件, 則測試通過.

圖5 一組待測程序測試運行及結果分析流程圖

5 系統實現

本系統基于Spike模擬器實現.支持擴充的指示性指令 (test_start和test_end) 所需的匯編器基于LLVM[15]后端實現, 鏈接器使用RISC-V的gcc工具鏈(C庫使用newlib).向量擴展指令的指令編碼及Spike模擬器功能實現遵循RVV-0.9規范.

系統利用偽隨機數實現了支持常用數據類型的測試用例隨機自動生成的函數庫, 包括整型、浮點型、字符型、字符串型等.用戶通過提供參數類型, 取值范圍等信息可自動生成隨機的測試用例.

系統支持通過JSON文件配置測試目標 (示例見圖6).其中, 決定程序正確性的觀測目標可用戶根據ABI和程序的具體功能手動設置, 默認觀測目標為a0寄存器.另外, 如圖6所示, 用戶可直接配置是否允許修改調用者維護的寄存器和其他內存值.

圖6 測試目標配置文件config.json示例

系統在運行test_end指令時輸出寄存器文件以對比寄存器值.對于內存值, 系統采取在模擬器插樁的方式監測內存變化.具體地, 在運行test_start指令后, 所有store類指令會額外記錄目標內存地址, 并在執行test_end是輸出記錄的內存地址及內存值.

圖7展示了針對某個測試用例的測試報告模板,分為測試結果、觀測目標、內存及被調用者維護的寄存器和其他.

圖7 測試報告模板

6 實驗與結果

本實驗旨在驗證語義等價性測試系統的有效性,并以一般的測試系統為基準, 評估其測試效果和時間開銷.實驗運行于Intel Core i7-9700 CPU以及32 GB內存的機器, 使用Ubuntu 20.04操作系統, 實驗結果均為運行5次的平均值.

6.1 測試集構造

我們選取5個常用C函數 (見表1) 作為系統的測試集, 每個函數具有一個標準版本、一個基于RVV的向量版本以及兩個變異版本.為充分驗證系統的測試有效性, 我們基于每個向量版本, 為程序引入副作用:(1) 將程序中某個被調用者維護的寄存器更改為調用者維護的寄存器形成變異版1; (2) 在程序中插入一條store指令更改某個指針參數對應的內存中的值形成變異版 2.表1 中, “9、11”表示 memcpy 的兩個變異版本的代碼量分別是9和11.

表1 常用C函數組成的匯編程序測試集

6.2 系統有效性驗證及時間開銷評估

為驗證本系統的有效性, 實驗采取隨機生成的1000個測試用例分別對 “標準-向量”“標準-變異1”和“標準-變異2”共3組程序進行語義等價性測試 (簡稱等價測試), 并同時運行一般測試 (僅比較函數觀測目標) 作為對比.

表2給出了測試結果和時間開銷.語義等價的 “標準&向量”組通過了一般測試及等價測試.但面對具有副作用的兩個變異版本, 一般測試依然顯示通過, 而等價測試通過更加嚴格的機器狀態對比, 有效地捕獲到副作用, 并報告測試未通過.

表2 基于1000個測試用例的一般測試和等價測試的有效性和時間對比

時間開銷方面, 等價測試由于追蹤、記錄、對比機器狀態而相比一般測試平均帶來約350%的額外時間開銷.但由于等價測試通常針對函數級的程序, 時間開銷通常是可接受的.例如向量計算函數saxpy在1000個測試用例下僅用時0.14 s左右.

6.3 案例分析

本節以函數strlen為例, 分析系統的測試有效性.表3給出了strlen的函數聲明、某測試用例、正確的返回值以及測試目標.該函數運行結束后, 由標準版函數計算觀測得出, 觀測目標a0應為0x20, 即整數32.另外, 用戶規定被調用者維護的寄存器和運行時棧以外的內存值在函數運行后不允許修改.

表3 函數strlen的測試用例及測試目標

函數strlen的向量版本及相應的兩個變異版本的生成方式見圖8.其中, 變異版1修改了被調用者維護的寄存器, 而變異版2修改了內存值, 二者均不滿足測試目標.傳統的基于返回值對比的測試方法因無 法捕獲此類副作用而通過了測試.基于語義等價性測試系統, 我們分別對“標準-向量”“標準-變異 1”和“標準-變異2”這3組程序進行測試.三者的測試報告見圖9.其中, 正確的向量版函數產生了與標準版相同的觀測值(a0) , 并未引入任何違反測試目標的副作用, 成功通過測試.變異版1修改了被調用者維護的寄存器s1, 變異版2修改了內存地址0x23f00的值, 均違反了測試目標而未通過測試.

圖8 函數strlen向量及變異版本

圖9 函數strlen的測試報告

此案例表明, 本系統能夠通過跟蹤機器狀態, 結合測試目標, 有效地捕獲程序產生的副作用, 提供嚴格有效的語義等價性測試.

7 總結與展望

本研究基于Spike模擬器, 設計并實現一套面向RISC-V的匯編程序語義等價性自動化測試系統, 通過比對不同程序運行后的全機器狀態 (寄存器、內存等) ,結合用戶配置的測試目標, 自動完成測試并生成測試報告.實驗表明, 本系統可成功捕獲程序運行的副作用,為語義等價性有效地提供了更為嚴格的測試環境.

基于本系統, 未來可通過以下3方面繼續提高語義等價性測試的有效性和易用性: (1) 結合模糊測試技術, 更為有效地生成測試用例, 提高測試的分支覆蓋率和有效性; (2) 結合缺陷定位技術[16,17], 為語句進行可疑性排序, 提高系統的易用性; (3) 采用動靜結合的方式[11]對匯編語義等價性進行更為嚴格的測試.