論文閲讀

Jubi Taneja, Zhengyang Liu, and John Regehr. 2020. Testing static analyses for precision and soundness. In Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization (CGO 2020). Association for Computing Machinery, New York, NY, USA, 81–93. https://doi.org/10.1145/3368826.3377927

Introduction

作者的目的是開發 formal-method-based（基於形式化的）算法，靜態分析中的 imprecisions 和 unsoundnesses 。

作者的貢獻是設計並評估了數種算法來分析編譯器靜態分析結果的 soundnesses 和 precisions，他們在 LLVM 並上沒有找到新 soundness bugs ，但是可以發現以前修復的 soundness bug。他們在 LLVM 中發現了比較多的 imprecisions 問題，并且部分被修復了。主要的分析目標是 LLVM 的重要數據流分析 Known bits , Demanded bit, Integer ranges, 以及一些前向分析布爾值的 sound 與 precise。

工作内容上，作者通過自己的算法計算代碼片段的 sound and maximally precise ，與 LLVM 自己產生的數據流信息相比較。當 LLVM 比自己的 more precise 時，可能 LLVM 的 soundnesses 就會存在問題。當 LLVM 比自己 less precise 時，他們的 precision 可能就會有問題。~~（有點奇怪）~~

Backround

作者的研究基於 Souper: A Synthesizing Superoptimizer

Dataflow Analysis

數據流分析用於計算程序執行過程中的正確性。數據流分析應該是 sound ，但是它也允許 imprecision，即允許 false positive。

Static Analysis in LLVM

LLVM 對於靜態分析是一個非常好的基石，高級語言的 tricky 和 implicit 的一些特性比如類型轉換，表達式的順序等在 LLVM IR 中就不會出現這種妨礙分析的特性。它的 SSA 使得對函數的數據流分析變得高效且簡單。由於 LLVM 中已經實現了非常多的優化器，比如 dead code optimization，減少了工作的一些小阻礙。~~畢竟是爲了分析 soundnesses 與 precisions，最後還要看看有沒有提升優化器能力~~。

Known Bits

用於判斷執行過程中 bit 是 0 或 1，使得算數運算中可以表現的更高效。

Number of Sign Bits

符號位的高位，可能會有和符號位相同的值，可以用來節約空間。

由於 Number of Sign Bits 的分析準則和 Known Bits 分析准測比較相似，所以作者忽略了這一部分。

~~不太懂這是怎麽優化的~~

Single-bit Analyses

判斷值非0，負，非負，2冪。同 Number of Sign Bits。

如果輸入要麽是 0 或 1，輸出對應了 0 或 1。那麽這個分析就是 sound。如果輸出為 0 或1 對應了輸入為 0 或 1，則分析是 maximally precise。

Integer Range Analysis

優化 away comparisons ，比如 [0, 100) < [200, 205) 可以被簡化爲 true。LLVM 的 Correlated Value Propagation pass 就是以這種方式優化程序的優化器。

Lazy Value Info（LVI）是 LLVM 的經典的 integer range analysis。LVI 中的 constant range 有四種形式：

Empty set: 空的 concretization set
Full set: 包含所有整形的 concretization set
Regular range [a, b) with a <u b: 包含所有大於等於 a 且小於 b 的 concretization set
Wrapped range [a, b) with a >u b: 包含所以要麽大於等於a 要麽小於 b 的 concretization set

a=b=0 和 a=b=UNIT_MAX 表示empty 和 full sets。

~~（這裏怎樣是 sound 怎樣是 precise 看不懂，以後再補充）~~

Demanded Bits

與前面的分析不同，demanded bits 是 backword program analysis，尋找那些沒用的 bits，比如説某個 32bit 整數被裁剪為 8bit 的證書，那麽前面 24bits 就會被 demanded bits 標記為 not demanded。

如果 not demanded bits 被任意設置為 0 或 1 而不影響結果，那麽這個分析就是 sound。

如果 demanded bits 被任意設置為 0 或 1，導致了結果的改變，那麽這個分析就是 maximally precise。

如果分析完發現全都是 not demanded bits，那麽 f 就可以直接被移除了。~~似乎這種思想可以用在 d算數混淆中~~。如果只是部分 not demanded bits ，可能我們可以用更簡單的表達式去表示。~~看上去是一種非常好用的優化器。~~

Reasoning about LLVM using Souper

Souper 是一個開源的 “super optimizer”，運行在 LLVM middle-end optimization pass，把 LLVM IR 轉換爲它自己的 IR，并將發現的優化應用於正在編譯過程中的優化器。~~怎麽一股 JIT 的味道~~

作者重用了 Souper 部分計算 precise 的 dataflow facts，因爲他們也要把 LLVM IR 轉換爲用於 SMT solvers 查詢的 IR。之後用於分析的每一部分代碼片段被稱之爲 “Souper expression”，表示了 LLVM instructions 的一個有向無環圖。

但是 Souper 也有一些缺陷，它無法看到内存引用，函數調用，循環迭代等。

Souper 在作者的工作中大部分都沒有用到。在 integer range 計算中存在一些特殊情況，後文會講到。

Testing Dataflow Analyses for Soundness and Precision

這一節講了作者的工作，需要將解決一些 sub-problems

用典型的 LLVM IR 去測試編譯器的 dataflow analyses
保證 LLVM 和作者的算法分析的是同樣的代碼，也就是之前提到的 peace of code，這樣方便比較
用 SMT 計算 precise dataflow 結果。

Finding Test Inputs

作者使用 SPEC CPU 2017 中的 C C++ benchmarks，關閉 Souper 的 syntjesos，最後他們產生了 269113 的 Souper expressions，71.6% 重複不止一次， 11.4% 重複超過 10次，1.6% 超過 100次。~~（這有什麽意義嗎，感覺和文章想做的事情沒什麽關係，後面再看看）~~

Enabling Comparable Reslts

他們不能輕易的獲得 precise dataflow results，也就很難進行比較，比如 LLVM integer analysis 存在過程閒的分析，而他們處理不了。作者的思路是再把 Souper IR 轉換成 LLVM IR 進行比較。~~實在難以理解，爲什麽會分析不了，因爲 Souper 本身就不支持過程閒分析嗎，最後居然要再轉換成 LLVM IR 來比較二者的精度~~