從今天開始，我們會介紹system software verification，compiler toolchain是build verification的必要工具，所以我們會先驗證compiler toolchain correctness。因為verification需要運行在kernel之上，所以需要驗證kernel booting flow。當kernel booting完成後，會對hardware做DVT、對device driver做device driver test、對kernel做kernel test，最後則是敘述方便進行驗證的test framework。
Compiler toolchain會將source code轉換成executable file，compiler toolchain correctness verification會確認compiler toolchain是否依照語言標準與source code的邏輯進行正確轉換。
Compiler toolchain是build system software的tools，因此它是一切的源頭，所以我們需要進行compiler toolchain的正確性測試，提早檢測出隱藏的bugs。
Compiler toolchain correctness verification由數值運算組成而不需要控制hardware，所以能利用CPU simuator執行。
每種語言都有自己的語法語義規範 (specification) ，compiler需要依照程式語言的規範處理輸入的source code，標準測試目的在驗證compiler是否遵循標準對程式進行解讀。 例如: GCC在執行時，可以指定遵循的C語言標準(C90, C99, C11, …)，所以對GCC做標準測試時會依照指定的標準給予對應的測項，以確定GCC可以正確支援每一種宣稱支援的標準。
Compiler toolchain會針對程式做最佳化，讓程式的執行時間或容量減少。而compiler的最佳化有很多技術，也有讓user手動開啟的最佳化選項，但compiler需要確保最佳化開啟後除了有效果，也不能影響software的正確性。 例如: 我們可以在在gcc開啟-Os最佳化軟體容量，再加上-flto開啟連結時的最佳化，但編譯出來的軟體，最終的執行結果上還是必須和沒有開啟任何最佳化相同。
Compiler toolchain需要保證同樣一份source code在同一個compiler toolchain上面要build兩次要得到完全相同的結果。例如: 同樣的hello world程式，用同一套compiler toolchain來build兩次，使用binary diff工具比較會發現兩次build得到的執行檔binary一模一樣。
Compiler toolchain正確性驗證的測項種類驗種項目、種類、組合繁多，可以透過工具產生programs來驗證compiler的正確性。
Csmith
Csmith是一個可以隨機產生C programs的工具，他主要目的是利用差異測試作為測試預言，使用隨機C programs查找compiler錯誤。
SuperTest
進階的工具可以配合C語言的標準生成或提供人工事先設計好的C programs作為測試的對象。
驗證方法
測項的最尾端可以將執行結果輸出(例如文字檔)，C source使用多套compiler toolchain編譯同一份source code，再把執行的結果做對比。
驗證平台
Compiler toolchain正確性驗證可以使用CPU模擬器執行，不需要完整硬體平台。
iThome鐵人賽
看影片追技術