Learning Abstraction Selection for Bayesian ProgramAnalysis

學習貝葉斯程序分析的抽象選擇

https://dl.acm.org/doi/pdf/10.1145/3649845

摘要

我們提出了一種基于學習的方法，用于選擇適用于貝葉斯程序分析的抽象。貝葉斯程序分析通過為分析規(guī)則附加概率，將程序分析轉(zhuǎn)化為貝葉斯模型。它能夠計算分析結(jié)果的概率，并可以通過從用戶反饋、測試運行及其他信息中學習來更新這些概率。其使用的抽象方式極大地影響了它從這些信息中學習的效果。已有大量關(guān)于為傳統(tǒng)程序分析選擇抽象的研究，但這些方法在貝葉斯程序分析中并不有效，因為它們沒有優(yōu)化泛化能力。我們提出了一種數(shù)據(jù)驅(qū)動的框架，通過從帶標簽的程序中學習來解決這個問題。該框架從一個抽象出發(fā)，根據(jù)分析推導(dǎo)決定如何改變該抽象。為了具備泛化能力，它考慮了分析推導(dǎo)的圖屬性；為了具備有效性，它還考慮了更改抽象前后所產(chǎn)生的推導(dǎo)結(jié)果。我們通過數(shù)據(jù)競爭分析和線程逃逸分析展示了我們方法的有效性。

CCS 概念：? 軟件及其工程 → 自動靜態(tài)分析。
附加關(guān)鍵詞和短語：靜態(tài)分析、貝葉斯網(wǎng)絡(luò)、告警排序、面向程序分析的機器學習、抽象解釋。

1 引言

基于抽象解釋的程序分析 [Cousot 1996] 通常采用過近似（over-approximation）方法，并常常以邏輯規(guī)則形式表達。這可能導(dǎo)致其結(jié)果中出現(xiàn)大量誤報（false alarms），從而嚴重影響用戶的使用體驗。

近年來，一種新的范式被提出用于解決這一問題：將傳統(tǒng)分析轉(zhuǎn)化為貝葉斯模型 [Mangal 等人 2015]。我們在本文中將其稱為貝葉斯程序分析（Bayesian program analysis）。在該范式中，通過為分析規(guī)則附加概率來量化其近似程度。生成的報告也帶有相應(yīng)的概率值，可用于對告警進行排序。這樣一來，分析就成為一個貝葉斯模型，并可以通過從各種后驗信息中學習來不斷改進其結(jié)果。這些后驗信息可以來自用戶反饋 [Mangal 等人 2015; Raghothaman 等人 2018]、舊版本的程序 [Heo 等人 2019b]，以及測試運行 [Chen 等人 2021]。

眾所周知，在平衡傳統(tǒng)程序分析的精確性與可擴展性之間，抽象的選擇至關(guān)重要。同樣的問題也適用于貝葉斯程序分析。然而，由于貝葉斯程序分析本質(zhì)上也是一個學習系統(tǒng)，抽象的選擇還會影響它從后驗信息中泛化的能力。

如果使用的抽象過于精細，可能會阻礙后驗信息有效傳播到相關(guān)的分析結(jié)果；而如果使用的抽象過于粗糙，則可能導(dǎo)致后驗信息錯誤地傳播到不相關(guān)的分析結(jié)果中。由于像用戶標注這樣的后驗信息獲取成本較高，因此在選擇抽象時，優(yōu)化其泛化能力往往比優(yōu)化精確性和可擴展性更為重要。換句話說，我們希望選擇一個能夠在給定數(shù)量的后驗信息下產(chǎn)生良好告警排序的抽象。

在本文中，我們旨在解決這一挑戰(zhàn)。具體來說，以從用戶反饋中學習為例，我們的目標是在相同數(shù)量的用戶反饋下優(yōu)化告警排序的質(zhì)量。然而，要解決這個問題，我們面臨兩大主要挑戰(zhàn)：

1. 有效性（Effectiveness）
   盡管已有大量關(guān)于如何為傳統(tǒng)分析選擇合適抽象的研究 [Bielik 等人 2017; Grigore 和 Yang 2016; Hassanshahi 等人 2017; He 等人 2020; Heo 等人 2016, 2019a, 2017; Jeon 等人 2019, 2018, 2020; Jeon 和 Oh 2022; Jeong 等人 2017; Kastrinis 和 Smaragdakis 2013; Li 等人 2022, 2018a,b, 2020; Liang 和 Naik 2011; Liang 等人 2011; Lu 和 Xue 2019; Oh 等人 2014, 2015; Peleg 等人 2016; Singh 等人 2018; Smaragdakis 等人 2014; Tan 等人 2021, 2016, 2017; Wei 和 Ryder 2015; Zhang 等人 2014, 2013]，但它們無法直接應(yīng)用于貝葉斯程序分析的場景。這些方法通常依賴于一個關(guān)鍵假設(shè)：在資源無限的情況下，抽象越細，分析結(jié)果越好。然而，由于存在后驗信息泛化的問題，這一假設(shè)不再成立。

2. 通用性（Generality）
   雖然可以為特定的分析實例開發(fā)有效的解決方案，但我們的目標是開發(fā)一種適用于廣泛貝葉斯分析的方法論。

為了應(yīng)對這兩個挑戰(zhàn)，我們提出了一種數(shù)據(jù)驅(qū)動的方法——BinGraph，它基于分析推導(dǎo)的一般特征來選擇程序抽象。對于某一特定程序分析任務(wù)，在給定一組已知真實告警的訓(xùn)練程序的前提下，BinGraph 會識別出對泛化最有利的抽象，并嘗試根據(jù)分析推導(dǎo)的特征學習出選擇這類抽象的策略。

當面對一個新的待分析程序時，BinGraph 首先使用某個抽象（通常是粗粒度的）運行分析。通過觀察分析推導(dǎo)過程，決定如何修改分析所用的抽象。與現(xiàn)有的面向傳統(tǒng)分析的數(shù)據(jù)驅(qū)動方法 [Jeon 等人 2019, 2018, 2020; Jeon 和 Oh 2022; Jeong 等人 2017; Oh 等人 2015] 相比，BinGraph 還會考慮應(yīng)用候選抽象修改后的分析推導(dǎo)結(jié)果，以最大化其有效性。這樣，我們的方法能夠更準確地預(yù)測使用某一抽象所帶來的影響。

我們的評估表明，這種基于分析推導(dǎo)變化的學習方法在優(yōu)化泛化能力方面是有效的。在應(yīng)對通用性挑戰(zhàn)方面，BinGraph 所考慮的特征是分析無關(guān)的推導(dǎo)圖屬性（graph properties）。只要我們可以提取某一分析的推導(dǎo)圖，BinGraph 就可以適用。這一點對于所有現(xiàn)有的貝葉斯程序分析都成立，因為它們都依賴推導(dǎo)圖來進行概率推理。

我們已在貝葉斯程序分析框架 Bingo [Raghothaman 等人 2018] 中實現(xiàn)了 BinGraph，并使用兩個代表性分析進行了評估：

• 一個具有 4^ 種可能抽象的數(shù)據(jù)競爭分析；

• 一個具有 2^ 種可能抽象的線程逃逸分析；

測試對象是一組包含 13 個 Java 程序的套件，代碼規(guī)模在 55–529 KLOC 之間，其中 表示兩種分析中對象分配語句的數(shù)量。

我們將 BinGraph 與三種基線方法進行了比較：

• Base-C

  ：使用最粗粒度的抽象；

• Base-P

  ：使用最精確的抽象；

• Base-R

  ：隨機選擇粒度的抽象。

平均而言，與這些基線方法相比，BinGraph 的倒序數(shù)量（inversion count，即用戶在看到一個真實告警之前所檢查的虛假告警對的數(shù)量）分別降低了45.36%、23.38% 和 45.64%。

貢獻

本文做出了以下貢獻：

1. 我們提出了一種用于貝葉斯程序分析中學習抽象選擇的框架BinGraph。
   BinGraph 對泛化能力具有直接的優(yōu)化作用，并且可以通用地應(yīng)用于具有不同邏輯規(guī)則的貝葉斯程序分析。

2. 我們展示了 BinGraph 在多個實際程序上的多樣化分析中的有效性。
   與基線方法相比，BinGraph 顯著提升了貝葉斯程序分析的泛化能力。

2 激勵性示例

本節(jié)將以圖1中的Java代碼片段為例，進行線程逃逸分析（thread-escape analysis），以解釋我們的問題和核心思想。這是一個用于說明的合成代碼，這些類的具體成員并不重要，請關(guān)注字段與對象之間的指向關(guān)系。

這段代碼中有兩個繼承自Thread的子類。Thread1的run方法分配了多個對象，并且Thread1的靜態(tài)字段指向其中一些對象。而Thread2的run方法則操作Thread1的一個靜態(tài)字段，并輸出相關(guān)信息。

用戶關(guān)心的是共有9條語句，這些語句在注釋中標記為 E1 到 E9。用戶想知道這些語句所操作的目標是否被多個線程訪問。由于Thread2僅操作靜態(tài)字段global2，所以在程序?qū)嶋H執(zhí)行過程中，只有語句 E7 的操作目標是被多個線程訪問的。

我們將展示貝葉斯參數(shù)化線程逃逸分析如何幫助用戶找出語句 E7。

2.1 一種參數(shù)化線程逃逸分析

用 Datalog 表達的分析如圖2所示，為了說明目的，它比實際分析做了簡化。該分析是流不敏感（flow-insensitive）和上下文不敏感（context-insensitive）的。

許多分析都具有參數(shù)化特性，以允許調(diào)整其抽象方式，從而在精確性與可擴展性之間取得平衡。本例中的分析也是如此。這些參數(shù)決定了如何在抽象中建模各種程序事實，我們將其稱為對這些事實的建模策略。

例如，在基于克隆的指針分析中，比如-對象敏感指針分析（-object-sensitive pointer analysis）[Milanova et al. 2005]，每個調(diào)用點都可以通過一個 值進行參數(shù)化，以決定如何建模與其相關(guān)的調(diào)用上下文。

就當前的線程逃逸分析而言，它的參數(shù)化方式體現(xiàn)在如何對每個堆對象進行建模上。有兩種策略可以用來建模一個對象：

1. 它被視為與同一類、且采用相同建模策略的其他對象相同的抽象對象；

2. 它被視為與在同一行創(chuàng)建（分配站點）、并采用相同建模策略的其他對象相同的抽象對象。

如果兩個對象采用了不同的建模策略，則它們不會被視作同一個抽象對象。

代碼中有11個與分析相關(guān)的分配站點，在注釋中標記為 H1 到 H11。它們的類類型包括 T1 到 T7。對于每一個分配站點，我們可以選擇使用上述兩種策略之一來對其所分配的對象進行建模。

如果某個分配站點采用的是第一種策略，我們說它的抽象級別（abstraction level）為 0；否則為 1。這里的抽象級別是一個特定參數(shù)，用于配置該分配站點下所有對象的建模策略。

在其他分析中，抽象級別可能與不同的程序元素相關(guān)聯(lián)。在這個例子中，為了簡化起見，我們通過一個布爾向量對整個分析中使用的抽象進行參數(shù)化，該向量的長度等于程序中分配站點的數(shù)量。向量的第個元素表示第個分配站點的抽象級別。

當一個分配站點采用更高的抽象級別時，抽象會更加精確，但也可能導(dǎo)致可擴展性下降。這種參數(shù)化設(shè)置在傳統(tǒng)分析中常用于權(quán)衡精度與性能之間的關(guān)系。

具體來說：

• 關(guān)系HL編碼了抽象信息；

• HX

  編碼了一個分配站點上的對象被建模成哪個抽象對象。

規(guī)則 R1 和 R2 描述了如何從 HL 推導(dǎo)出 HX。

除了 HL 外，其他輸入關(guān)系編碼了由基于分配站點的指針分析計算出的指向信息（points-to information）。規(guī)則 R3、R4 和 R5 將這些信息提升為基于 HX 的適當抽象對象。

最后，規(guī)則 R6、R7 和 R8 描述了分析的主要邏輯：

1. 如果一個對象被賦值給靜態(tài)字段，那么它“逃逸”（escapes）；

2. 如果一個已逃逸對象的字段指向另一個對象，那么后者也逃逸。

Datalog 推理引擎接收這些規(guī)則和輸入關(guān)系（來自對 Java 代碼片段早期分析的結(jié)果），并不斷推導(dǎo)輸出元組（tuples），直到無法再推導(dǎo)出新的元組為止。

這些規(guī)則是過近似（over-approximation）的，可能會產(chǎn)生誤報（false alarms）。近似的來源包括：

1. 堆抽象

   ：運行時多個具體的對象被抽象為一個抽象對象；

2. 一個對象只要能從靜態(tài)字段可達，并不一定真的會被多個線程訪問（例如程序可能是單線程的）。

我們通過一個例子更詳細地解釋（1）：假設(shè)有一個抽象對象 O，它包含兩個具體對象 o? 和 o?。假設(shè) o? 被一個靜態(tài)字段指向，而 o? 并未逃逸。根據(jù) R6，O 逃逸了，其中也包含了 o?，這就是過近似。假設(shè)指令 e 只訪問 o?，根據(jù) R8，e 訪問了一個逃逸對象，這又是一次過近似。同樣的推理適用于 R7。

當抽象確定后，我們可以將所有的輸入元組、派生元組以及參與推導(dǎo)這些元組的基本子句（ground clauses）可視化為一個有向圖。我們將這些元組和規(guī)則實例稱為一次分析運行的分析推導(dǎo)（analysis derivation），對應(yīng)的圖稱為推導(dǎo)圖（derivation graph）。

圖3展示了在三種不同抽象下的推導(dǎo)圖。在這些圖中，沒有被框起來的頂點表示相關(guān)的基本子句。例如，“R7(H1, H2)”表示涉及 H1 和 H2 的規(guī)則 R7 的一個實例。被框起來的頂點表示元組。白色背景的表示派生元組，灰色背景的表示輸入元組。特別地，雙邊框的頂點表示警報元組（alarm tuples）。

對于每種抽象，分析分別給出了 7、9 和 8 個警報，其中只有 escE(E7) 是真正的警報。抽象越精確，基于它的分析所產(chǎn)生的誤報就越少。然而，即使使用最精確的抽象，用戶也很難快速找到真正的警報。

接下來我們將展示貝葉斯程序分析如何幫助用戶更快地找到真正的警報。

2.2 一種參數(shù)化貝葉斯程序分析與抽象選擇問題

我們首先簡要介紹貝葉斯程序分析。它將分析推導(dǎo)轉(zhuǎn)換為一個概率模型，結(jié)合后驗信息，計算每個警報為真的概率，并向用戶展示概率最高的那個警報。用戶檢查該警報是否為真，并將結(jié)果反饋回去。然后，利用該反饋作為新的后驗信息，重新計算概率，如此繼續(xù)交互過程。

我們將基于后驗信息更新警報概率的過程稱為泛化（generalization），并將給定一定量后驗信息時能夠生成良好警報排序的能力稱為貝葉斯程序分析的泛化能力。在交互式警報解決的場景中，泛化能力越強，在相同數(shù)量的用戶反饋下排在前列的真實警報就越多，或者識別所有真實警報所需的用戶反饋就越少。

為了評估本文中貝葉斯程序分析的泛化能力，我們假設(shè)交互過程會持續(xù)到所有真實警報都被檢查為止；而在實際中，用戶可以隨時停止。在本例中，我們使用在最壞情況下（因為可能存在概率相同的警報）用戶檢查完所有真實警報所需的輪次數(shù)量作為一個評估指標。數(shù)值越低，表示泛化能力越好。

回到示例來看，規(guī)則是過近似（over-approximation）的，可能會推導(dǎo)出虛假的程序事實。我們可以通過為這些規(guī)則附加概率來量化它們的不精確性。為了簡化起見，我們將這些概率統(tǒng)一設(shè)為0.95。在實踐中，這些概率可以從有標注的程序中學習得到。

在此基礎(chǔ)上，一個推導(dǎo)圖可以被轉(zhuǎn)化為一個貝葉斯網(wǎng)絡(luò)。具體來說，推導(dǎo)圖中的每個元組和相關(guān)基本子句都被視為一個伯努利隨機變量（Bernoulli random variable），表示該元組或相關(guān)基本子句是否成立。推導(dǎo)圖中相鄰頂點之間的關(guān)系通過條件概率進行建模。

以相關(guān)的基本子句
R7(H1, H2) : escX(H2) :- escX(H1), XFX(H1, H2)
為例，其對應(yīng)的條件概率如下所示：

推導(dǎo)圖中每個相關(guān)基本子句及其相鄰頂點都使用類似的條件概率。

每個警報為真的概率可以通過對貝葉斯網(wǎng)絡(luò)進行邊緣推理（marginal inference）來計算 [Murphy et al. 1999]。這些概率用于對警報進行排序。

我們以最精確的抽象 為例。每個警報為真的概率如表1a所示。分析系統(tǒng)向用戶展示最可能為真的警報escE(E1)。用戶發(fā)現(xiàn)這個警報是假的，并給出負面反饋。系統(tǒng)將此反饋作為后驗信息，更新每個警報的概率，如表1b所示。交互過程根據(jù)用戶的意愿繼續(xù)進行。

如表2所示，在第4輪時，用戶收到了真正的警報。請注意，即使每一輪中可能存在多個概率相同的最可能警報，無論系統(tǒng)選擇哪一個進行提示，用戶最多只需檢查4個警報即可找到真正警報。相比之下，使用傳統(tǒng)分析方法，在最壞情況下用戶需要檢查全部7個警報。

通過使用更合適的抽象，貝葉斯分析的性能還可以進一步提升。考慮抽象 S3，其中只有與真實警報直接相關(guān)的分配站點 H7 被設(shè)置為抽象級別 1。使用這種抽象，傳統(tǒng)分析的性能下降了，因為它現(xiàn)在會生成8個警報。然而，在貝葉斯分析中，用戶只需檢查兩個警報就能找到真正警報。

其原因是：一個更粗粒度的抽象有時可以將更多的假警報關(guān)聯(lián)在一起。因此，對一個假警報提供反饋可以泛化到更多假警報。讓我們仔細看一下圖3c中在抽象 S3 下的推導(dǎo)圖。在這個圖中，所有假警報彼此相連，但與唯一的真正警報斷開連接。因此，對任何一個假警報提供負面反饋都會降低其他所有假警報的概率。而真正警報的概率不受影響，因此它的排名得到提升。

而在抽象 S1 的推導(dǎo)圖中，大多數(shù)假警報之間是相互斷開的。

使用過于粗糙的抽象也可能帶來負面影響。我們來看最“便宜”的抽象 S2。在其推導(dǎo)圖（見圖3b）中，所有警報都被連接在一起。因此，對負警報的反饋也會影響真正警報的概率。結(jié)果是，它的性能比 S3 更差。

從上述觀察中，我們可以得出兩個關(guān)鍵見解：

1. 抽象的選擇對貝葉斯程序分析的性能有重大影響

2. 由于泛化問題的存在，貝葉斯程序分析的性能并不總是與傳統(tǒng)分析一致。

對于傳統(tǒng)分析來說，在不考慮效率的前提下，更精確的抽象不會導(dǎo)致更差的結(jié)果。然而，在本例中，S3 是一種在精度上處于中間位置的抽象，卻是在所有 211 種可能抽象中，貝葉斯分析表現(xiàn)最優(yōu)的抽象。

這表明，貝葉斯程序分析的抽象選擇問題本質(zhì)上不同于傳統(tǒng)分析的抽象選擇問題，我們需要新的技術(shù)來解決這一問題。

2.3 我們的方法

圖4展示了我們解決這個問題的工作流程，稱為BinGraph。它是一種基于學習的方法。我們先關(guān)注它的在線部分。

從最粗糙的抽象（在示例中為 S2）開始，BinGraph 試圖迭代地細化抽象。雖然在本例中抽象級別只能是布爾值（0 或 1），但在一般情況下，它可以是一個自然數(shù)。此外，在其他分析中，參數(shù)化可能并不與分配站點相關(guān)，而是與程序元素如方法或變量相關(guān)。我們將這些程序元素統(tǒng)稱為抽象點（abstraction points）。

提高某個抽象點的抽象級別會使抽象變得更精確。這在傳統(tǒng)分析中是非常常見的設(shè)定。例如，在參數(shù)化的 k-對象敏感指針分析 [Milanova et al. 2005] 中，抽象級別就是每個調(diào)用點的上下文敏感度。

此外，對于每個具有特定抽象級別的抽象點，都會有一個對應(yīng)的參數(shù)元組（parameter tuple）作為輸入。例如，如果 H1 的抽象級別是 0，則參數(shù)元組為HL(H1, 0)；如果是 1，則為HL(H1, 1)。

在每一次迭代中，BinGraph 決定是否將每個抽象點的抽象級別提升一級，或者保持不變。迭代次數(shù)等于最大抽象級別（在本例中為1）。作為一種基于學習的方法，BinGraph 會評估提升每個抽象點級別的影響，并根據(jù)學到的策略決定是否進行提升。

為了獲得有效性（Effectiveness），BinGraph 在刻畫一個參數(shù)時考慮了兩個推導(dǎo)圖：

1. 第一個是當前抽象下的推導(dǎo)圖（在本例中為 S2 ）；

2. 第二個是整體提升后的抽象下的推導(dǎo)圖（即將每個抽象點的抽象級別提升一級，對應(yīng)于 S1 ）。

在傳統(tǒng)分析中，使用較粗粒度抽象下分析的信息可以反映更精確抽象下的相關(guān)屬性，主要是因為抽象越精細，分析結(jié)果越好。然而這一假設(shè)在貝葉斯分析中并不成立，因此僅使用粗粒度抽象下的信息無法準確預(yù)測更精確抽象下的分析效果。因此，同時使用這兩個抽象下的推導(dǎo)圖可以確保每次迭代中所做的抽象改進對分析結(jié)果更有利。

為了獲得通用性（Generality），BinGraph 僅考慮與參數(shù)元組（如HL(x, y)）相關(guān)的推導(dǎo)圖屬性。雖然 BinGraph 可以配置不同的圖屬性，但在實驗中，給定一個參數(shù)元組，它使用三種屬性類型：

1. 可到達頂點的數(shù)量 ；

2. 到可到達頂點的最短距離的平均值 ；

3. 最短距離 ≤ 的頂點數(shù)量 。

請注意，這些屬性只與推導(dǎo)圖有關(guān)，而與分析的語義無關(guān)，因此它們可以應(yīng)用于任何類型的貝葉斯程序分析。此外，BinGraph 也支持添加其他類型的屬性。

選擇這三類特征背后的直覺是：它們反映了細化參數(shù)元組對貝葉斯網(wǎng)絡(luò)中信息傳播的潛在影響：

1. 可到達頂點的數(shù)量 ：

   表示可能受某個參數(shù)元組細化影響的頂點數(shù)量。換句話說，它反映了該元組對整個貝葉斯網(wǎng)絡(luò)的整體影響。

2. 到可到達頂點的最短距離的平均值 ：

   由于在貝葉斯網(wǎng)絡(luò)中，某個頂點距離參數(shù)元組越遠，其受影響的程度就越弱，因此該特征反映了參數(shù)元組細化對可到達頂點的平均影響。

3. 最短距離 ≤ 的頂點數(shù)量 ：

   該特征反映了對某一子圖的潛在影響，即在一定距離范圍內(nèi)受影響的頂點數(shù)量。此外，與信息傳播無關(guān)的是，該特征還可以捕捉給定半徑內(nèi)的不同子圖模式，從而可用于識別需要細化的參數(shù)元組。

在我們的實驗中，這類特征共有九種，其中 k=2,3,…,10。

我們并沒有為本文中的分析專門設(shè)計這些特征，但我們相信它們是一些通用特征，能夠反映信息傳播的影響。然而，針對特定分析精心設(shè)計特征仍有提升空間，以實現(xiàn)更優(yōu)的性能。

我們以與 H1 相關(guān)的部分為例來解釋 BinGraph。BinGraph 會計算在抽象 S2下推導(dǎo)圖中HL(H1, 0)的屬性，以及在抽象 S1 下推導(dǎo)圖中HL(H1, 1)的屬性。

在這里，我們考慮三種屬性，如表3所示，為了簡化起見，第三種屬性只考慮了一個距離閾值。圖5展示了用于計算這些屬性的相關(guān)子圖。

實際的特征向量是一個三維實數(shù)向量，其中每個元素是原始圖上某屬性與其在細化圖上對應(yīng)屬性的比值。表3展示了 H1 的這些值。

按照這種方法，H3 和 H5 具有與 H1 相同的特征值（0.371, 1.085, 0.444），而 H7 則具有不同的特征值（0.882, 0.940, 0.778）。

BinGraph 所學到的策略被表示為一組三維立方體：只有特征值落入這些立方體內(nèi)的參數(shù)元組才會被細化。

例如，假設(shè)通過在類似程序上的訓(xùn)練，BinGraph 學到了一個由立方體[0.8, 1] × [0.9, 1] × [0.7, 1]表示的策略。使用該策略，BinGraph 能夠?qū)?H7 與其他分配站點區(qū)分開來。而正是這個分配站點是我們需要提升抽象級別以獲得最優(yōu)抽象 S3 的關(guān)鍵所在。

我們將在第4節(jié)中進一步詳細介紹 BinGraph 的在線部分和離線部分。

3 前提知識3.1 Datalog 語法與語義

3.2 參數(shù)化 Datalog 程序分析

我們現(xiàn)在轉(zhuǎn)向?qū)崿F(xiàn)參數(shù)化程序分析的 Datalog 程序。

與標準的 Datalog 程序相比，它的輸入現(xiàn)在分為兩個部分：

3.3 參數(shù)化貝葉斯程序分析

在本節(jié)中，我們僅介紹使用用戶反饋作為后驗信息的貝葉斯程序分析。

一個參數(shù)化貝葉斯程序分析是基于一個參數(shù)化 Datalog 程序分析

用戶可以在任何時間終止交互過程。

為了在實驗中評估貝葉斯程序分析的泛化能力（generalization ability），我們假設(shè)用戶會在所有警報都被檢查完之后才終止交互。

這一設(shè)定遵循了近期關(guān)于貝葉斯程序分析的研究 [Chen et al. 2021; Heo et al. 2019b; Kim et al. 2022; Raghothaman et al. 2018]。

而在實際中，用戶可能采用其他終止條件。例如，用戶可能決定在連續(xù) n 個警報都是假警報后停止。

在我們的實驗中，通常只有在檢查了大量假警報之后，才能發(fā)現(xiàn)一小部分真實警報。

4 BinGraph 框架

一個抽象點的特征值表示基于某個特定抽象的分析推導(dǎo)特征。這些特征值將在 BinGraph 的整個過程中被使用。

所學到的策略（Learned）是一組在離線部分計算出的特征值。如果某個抽象點的特征值包含在 Learned 中，則其抽象級別將被提升。

實驗中所使用的屬性類型將在第5節(jié)中展示。

4.2 BinGraph 的離線部分

BinGraph 的離線部分包括一個標注算法（labeling algorithm）和一個學習算法（learning algorithm）。

對于每一個訓(xùn)練程序，我們預(yù)先獲得其真實警報，并在不同抽象下自動模擬整個交互過程，以計算逆序數(shù)（inversion count）。

算法2展示了標注算法，它生成兩個帶標簽的特征值集合：

• Labeled0

  ：表示不應(yīng)該提升抽象級別的抽象點；

• Labeled1

  ：表示應(yīng)該提升抽象級別的抽象點。

BinGraph 的學習算法受到 Graphick [Jeon et al. 2020] 的啟發(fā)。其核心思想是：找到一個實數(shù)范圍，使得它盡可能多地覆蓋適合提升抽象級別的特征值（即 Labeled1），同時盡可能少地覆蓋不適合提升的特征值（即 Labeled0）。這樣，當某個抽象點的特征值落在這個范圍內(nèi)時，提升它的抽象級別很可能對分析有幫助。

FeatureScore描述了立方體中屬于 L1 的特征值所占的比例。
如果 FeatureScore不低于一個超參數(shù) θ，或者劃分過程超過了時間限制，則劃分過程將終止。最終的立方體會被返回。

例 4.4。考慮 N = 3，Labeled0 = {(3, 3, 3), (4, 4, 4), (5, 5, 5)}，Labeled1 = {(1, 1, 1), (2, 2, 2), (4, 4, 4), (6, 6, 6)}，超參數(shù) = 0.6。最初，我們設(shè)定 0 = Labeled0，1 = Labeled1。第一個立方體從包含1 中每個特征值的最小立方體 [1, 6] × [1, 6] × [1, 6] 開始。尋找立方體的過程如下所示，索引是隨機選擇的。

5 實驗評估

我們的評估旨在回答以下問題：

RQ1：BinGraph 在提升貝葉斯程序分析的泛化能力方面有多大的效果？

RQ2：BinGraph 對超參數(shù)和訓(xùn)練基準程序的敏感度如何？

RQ3：為了刻畫抽象點，是否有必要計算整體細化后的推導(dǎo)圖？

RQ4：使用 BinGraph 所選擇抽象的貝葉斯程序分析在可擴展性方面表現(xiàn)如何？

RQ5：現(xiàn)有的、用于傳統(tǒng)程序分析的抽象選擇方法能否替代我們的方法？
在傳統(tǒng)分析中具有較好精度/可擴展性平衡的抽象，是否恰好在其對應(yīng)的貝葉斯分析中也具有良好的泛化能力？

我們在第5.1 節(jié)中描述實驗設(shè)置，然后在第5.2 至 5.6 節(jié)中依次討論上述問題的回答。

5.1 實驗設(shè)置

我們在配備 2.6 GHz 處理器和 256 GB 內(nèi)存、運行 Oracle HotSpot JVM 1.6 的 Linux 機器上完成了所有實驗。

我們使用Chord 框架[Naik et al. 2006] 進行 Datalog 程序分析，使用Bingo 框架[Raghothaman et al. 2018] 進行貝葉斯推理。

我們?yōu)橥茖?dǎo)圖設(shè)置了40GB 的大小限制，并為每次貝葉斯網(wǎng)絡(luò)推理設(shè)置了2小時的時間限制。若超出任一限制，則將此次運行標記為失敗并終止。

實例分析（Instance Analyses）我們在表4中總結(jié)了兩個實例分析的統(tǒng)計信息：

(1)第一個是數(shù)據(jù)競爭分析（datarace analysis）[Naik et al. 2006]，它用于找出可能同時訪問相同堆對象且至少有一次是寫操作的所有語句對。

該分析包含一個參數(shù)化的、流不敏感但上下文敏感的 k-對象敏感指針分析 [Milanova et al. 2005]。

• 抽象點是 k -對象敏感分析中的分配站點；

• 每個分配站點的抽象級別（即 k 值）取值范圍為 {0, 1, 2, 3}；

• 抽象級別表示上下文敏感的程度；當對應(yīng)級別為 0 時，表示該站點采用上下文不敏感的處理方式。

(2)為了展示 BinGraph 的通用性，我們也考慮了一個線程逃逸分析（thread-escape analysis）[Naik et al. 2012]，它用于找出所有其操作目標可能被多個線程訪問的語句。

• 該分析是流不敏感和上下文不敏感的；

• 分析通過如何建模堆對象進行參數(shù)化；

• 抽象點仍然是分配站點；

• 每個分配站點的抽象級別取值為 {0, 1}；

• • 對于抽象級別為 0 的分配站點，在分析過程中，其所有對象被視為一個整體；

  • 對于抽象級別為 1 的分配站點，會為其創(chuàng)建一個獨立的抽象對象，該站點下所有對象都視為這個抽象對象。

對于每個基準程序，我們預(yù)先檢查了每個警報是否為真，并自動模擬整個交互過程以計算相關(guān)指標。

• 對于數(shù)據(jù)競爭分析，我們通過人工檢查獲取真實警報 [Raghothaman et al. 2018]；

• 對于線程逃逸分析，我們將基于 CEGAR 的流敏感與上下文敏感分析[Zhang et al. 2013] 的結(jié)果作為真實警報。

由于以下原因，部分程序未納入最終評估：

• 在數(shù)據(jù)競爭分析中，有4個程序未生成任何警報，因此被排除；

• 在線程逃逸分析中，有另外4個程序因參考分析未能終止而被排除。

基準抽象（Baseline Abstractions）

我們將 BinGraph 生成的抽象與三種基準抽象進行比較：

• Base-C

  ：最粗糙的抽象 S0 ；

• Base-P

  ：最精確的抽象，其中對所有抽象點 x∈AS ，都有 SP(x)=AL ；

• Base-R

  ：隨機抽象 SR(x) ，其抽象級別在 {0, 1, ..., AL} 中均勻分布。

對于 Base-R，我們展示了三次運行結(jié)果的平均值。

我們通過與這些基準的比較來說明：
BinGraph 在提升抽象精度時所選擇的方向?qū)Ψ夯芰κ怯幸娴摹炔贿^于粗糙、也不過于精細，也不會退化為隨機選擇。

我們將在第5.6節(jié)中評估那些在傳統(tǒng)程序分析中具有良好精度/可擴展性平衡的抽象。

特征類型（Features）

我們在表6中展示了實驗中使用的屬性類型（即 βi(G,v) 的含義）。

在第2.3節(jié)中我們已經(jīng)介紹了選擇這些屬性類型的直覺動機。

由于這些屬性在優(yōu)化效果上表現(xiàn)良好，我們建議在使用 BinGraph 時采用這些屬性。

為了避免除以零的情況，在計算特征值時，所有屬性值都會加一。

評估指標（Metrics）

主要評估指標是第3.3節(jié)中介紹的逆序數(shù)（inversion count），它反映了用戶在整個交互過程中的體驗，并進一步體現(xiàn)了貝葉斯程序分析的泛化能力。

此外，我們還展示了以往研究 [Raghothaman et al. 2018] 中使用的兩個補充指標：

• Rank-100%-T

  ：用戶檢查完所有真實警報所需的輪次；

• Rank-90%-T

  ：用戶檢查完90%的真實警報（向上取整）所需的輪次。

我們將基準程序劃分為訓(xùn)練集、驗證集和測試集。
驗證集用于確定第4.2節(jié)中介紹的超參數(shù) θ。

• 對于數(shù)據(jù)競爭分析，我們使用{jspider, hedc}進行訓(xùn)練，使用{weblech}進行驗證；

• 對于線程逃逸分析，我們使用{ftp, javasrc-p}進行訓(xùn)練，使用{weblech}進行驗證。

我們之所以選擇這些基準程序，是因為它們在字節(jié)碼規(guī)模上相對較小；而使用大規(guī)模程序進行訓(xùn)練和驗證的時間成本過高，難以接受。

其余基準程序則用于最終測試。

5.2 有效性

我們在表7中展示了有效性結(jié)果的主要指標匯總。

與基準方法相比，BinGraph 在大多數(shù)基準程序上的逆序數(shù)（inversion count）顯著更少。

• BinGraph 在12個基準程序中的10個上優(yōu)于 Base-C，平均減少比例分別為31.52%和53.59%（對應(yīng)兩種分析）。

• • 這表明 BinGraph 通過提升抽象精度有效增強了泛化能力。

• BinGraph 在12個基準程序中的11個上優(yōu)于 Base-P，平均減少比例分別為27.81%和20.42%。

• • 這表明 BinGraph 所選擇的抽象雖然不如 Base-P 精確，但具有更強的泛化能力。

  • 原因在于 BinGraph 只提升那些對泛化有益的抽象點。一個典型例子是luindex，Base-P 的逆序數(shù)是 BinGraph 的29倍，因為在高精度抽象下假警報之間的關(guān)聯(lián)被切斷了。

• BinGraph 在所有12個基準程序上都優(yōu)于 Base-R，平均減少比例分別為42.55%和48.22%。

• • 這表明 BinGraph 學到的策略與隨機選擇有明顯差異。

  • 此外，其他兩個指標也顯示出類似的改進。

我們在圖8中繪制了數(shù)據(jù)競爭分析的ROC曲線[Fawcett 2006]，在圖9中繪制了線程逃逸分析的 ROC 曲線。

• 一個點 (x,y) 表示用戶在交互了 x+y 輪后檢查了 x 個假警報和 y 個真警報；

• 相關(guān)指標 AUC 是 ROC 曲線下面積的歸一化值，在以往研究 [Raghothaman et al. 2018] 中也有使用；

• 逆序數(shù)與 AUC 的關(guān)系為： Inversion(S)=NTNF(1?AUC) 其中 NT 、 NF 分別是真實警報和假警報的數(shù)量；

• 由于不同抽象可能導(dǎo)致假警報數(shù)量不同，因此我們主要使用逆序數(shù)而非 AUC 作為評估指標；

• AUC 越大，逆序數(shù)越小；

• 因此，AUC 可以直觀展示不同抽象之間泛化能力的差異；

• 與其它基線方法相比，BinGraph 明顯具有更高的 AUC，這形象地說明了 BinGraph 所選抽象具有強大的泛化能力。

有兩個異常情況值得注意：

1. 在數(shù)據(jù)競爭分析實驗中，對于基準程序avrora，Base-C 的逆序數(shù)低于其它方法，但其 Rank-100%-T 和 Rank-90%-T 更高。

• 主要原因是 Base-C 僅用 130 輪就找到了 25 個真實警報（而 BinGraph、Base-P 和 Base-R 分別用了 363、391 和 414 輪），但在接下來尋找剩余 4 個真實警報時卻花了 808 輪；

• 這表明 Base-C 在交互初期表現(xiàn)良好，但隨后效果極差；

• 因此，雖然 Base-C 的逆序數(shù)很低，但這并不意味著它的泛化能力更強。

在數(shù)據(jù)競爭分析中，對于基準程序xalan，除最粗糙的抽象（0-CFA）外，幾乎所有有價值的抽象（包括 1-object-sensitivity 和 2-object-sensitivity，即抽象中對所有抽象點 x 有 S(x)=1 或 S(x)=2）都被標記為失敗。

• 主要原因是現(xiàn)有的貝葉斯程序分析框架在使用精確抽象處理大規(guī)模程序時可擴展性較差。

總結(jié)：

BinGraph 確實在優(yōu)化貝葉斯程序分析的泛化能力方面非常有效，并且有望在交互過程中提升用戶體驗。

5.3 敏感性研究

我們評估了 BinGraph 對超參數(shù)和訓(xùn)練基準程序的敏感程度。

對超參數(shù)的敏感性

我們在圖10中展示了在不同超參數(shù) θ 值（見算法4）下，BinGraph 在訓(xùn)練集和驗證集上的表現(xiàn)。

我們以 0.05 為步長，將 θ 從 0 到 1 進行遍歷，并使用相對于 Base-R 的逆序數(shù)平均減少比例來評估其影響。

BinGraph 的表現(xiàn)會隨著 θ 的變化而變化。例如：

• 當 θ 接近 1 時，在訓(xùn)練集上的表現(xiàn)顯著優(yōu)于驗證集；

• 主要原因是當 θ 較高時，算法4會產(chǎn)生覆蓋范圍較小的立方體，從而導(dǎo)致過擬合。

為了應(yīng)對 BinGraph 對超參數(shù)的敏感性問題，我們選擇在訓(xùn)練集和驗證集上綜合平均減少比例最高的 θ 值作為最終設(shè)置：

• 對于線程逃逸分析，選用了 θ=0.35

• 對于數(shù)據(jù)競爭分析，選用了 θ=0.45

為了測量 BinGraph 對訓(xùn)練基準程序的敏感性，我們進行了留一交叉驗證（leave-one-out cross-validation）。

由于一些用于數(shù)據(jù)競爭分析的基準程序規(guī)模過大，無法用于訓(xùn)練，因此我們只針對線程逃逸分析在全部9個基準程序上進行了實驗。

設(shè)BinGraphC是交叉驗證下的設(shè)置，我們在表8中展示了指標匯總結(jié)果。

可以看出，BinGraph 和 BinGraphC 相對于 Base-R 的提升效果相似，三類指標的差異分別為：

• 7.46%
• 1.50%
• 2.41%

總結(jié)：BinGraph 對訓(xùn)練基準程序的選擇并不敏感。

5.4 使用兩個推導(dǎo)圖的必要性

請注意，BinGraph 使用了兩個推導(dǎo)圖來刻畫每個抽象點。

然而，在進行整體細化后的推導(dǎo)圖 G′ 上的計算成本，要顯著高于在整體細化前的推導(dǎo)圖 G。

為了驗證計算 G′ 的必要性，我們進行了一項消融實驗（ablation experiment），即僅使用 G來刻畫每個抽象點。

形式上，我們將第4.1節(jié)中的特征值重新定義為：

其他設(shè)置保持不變，包括訓(xùn)練集、驗證集以及選擇超參數(shù) θ 的標準。

設(shè)BinGraphA為該消融實驗的設(shè)置，我們在表9中展示了指標匯總結(jié)果。

可以看出，與 Base-R 相比，BinGraphA 的變化趨勢與 BinGraph 完全不同，且在大多數(shù)指標上甚至不如 Base-R。

主要原因在于：

• 推導(dǎo)圖 G 僅基于當前抽象的信息來刻畫抽象點，而沒有考慮潛在細化后的情況；

• 這導(dǎo)致學到的策略無法有效幫助找到合適的抽象。

總體而言，使用推導(dǎo)圖 G′ 是有必要的，也是有價值的。

5.5 可擴展性

我們分別評估了 BinGraph 兩個部分的可擴展性：

• 離線部分

  ：評估 BinGraph 的訓(xùn)練成本；

• 在線部分

  ：評估在 BinGraph 所選抽象下貝葉斯程序分析的運行成本。

由于 Datalog 引擎的運行時間在整個過程中可以忽略不計（不到1%），我們僅展示貝葉斯推理的評估結(jié)果。

訓(xùn)練成本 為了加快訓(xùn)練過程，我們在以下兩個方面實現(xiàn)了并行化：

1. 用于標注的模擬退火算法（Simulated Annealing）；

2. 用于獲取超參數(shù)的驗證過程。

對于數(shù)據(jù)競爭分析：

• 標注過程耗時4天；

• 學習過程（包括驗證）耗時1天。

對于線程逃逸分析：

• 標注過程耗時2天；

• 學習過程（包括驗證）耗時8小時。

總體而言，BinGraph 的訓(xùn)練成本是可以接受的。

貝葉斯推理成本 貝葉斯推理的計算成本主要取決于推導(dǎo)圖在簡化后的規(guī)模

由于線程逃逸分析的平均迭代時間可以忽略不計（小于1秒），我們未展示其相關(guān)數(shù)據(jù)。

我們在表10中展示了數(shù)據(jù)競爭分析在可擴展性方面的指標匯總。

一個反直覺的現(xiàn)象是：

• 在某些基準程序（如ftp）中，最精確的抽象 Base-P 所生成的推導(dǎo)圖比其它抽象更小；

• 然而，在簡化前，Base-P 的推導(dǎo)圖是最大的；

• 主要原因是用于去除環(huán)結(jié)構(gòu)的算法是啟發(fā)式的，其效果依賴于圖的結(jié)構(gòu)。

結(jié)論：

在現(xiàn)有的貝葉斯程序分析框架下，與其它方法相比，BinGraph 的可擴展性是可以接受的。

5.6 傳統(tǒng)方法的無效性

傳統(tǒng)方法的目標是找到在精度與可擴展性之間取得良好平衡的抽象。

那么，這些抽象是否也具有良好的泛化能力？我們能否使用傳統(tǒng)方法來替代我們的方法？

為了回答這些問題，我們首先進行了一項控制變量實驗（controlled variable experiment），修改了 BinGraph 的學習目標，使其專門學習這類抽象。

具體來說，對于一個訓(xùn)練程序，我們使用 BinGraph 來學習這樣一個抽象：它是所有生成最少警報的抽象中成本最低的那個。

我們將這類抽象稱為最小抽象（minimal abstractions），并通過系統(tǒng)搜索方法LearnMinimalAbstraction[Jeon et al. 2020] 來識別它們。

此外，由于我們的方法最初并非為學習此類抽象而設(shè)計，為了消除學習過程帶來的噪聲影響，我們在測試程序上也使用該系統(tǒng)搜索方法來識別最小抽象，并評估其泛化效果。

我們僅研究了線程逃逸分析的結(jié)果，因為當使用測試程序時，系統(tǒng)搜索方法在數(shù)據(jù)競爭分析中無法擴展。

表11展示了在這兩種設(shè)置下所識別出的抽象，在用于貝葉斯程序分析時，相較于最廉價抽象所帶來的提升程度。其中：

• BinGraphM

  表示在訓(xùn)練集上通過修改后的 BinGraph 所學到的抽象；

• Minimal

  表示在測試程序上通過系統(tǒng)搜索得到的抽象。

結(jié)果顯示：

• 在線程逃逸分析中，BinGraphM 相比我們原始的方法表現(xiàn)相當不錯；

• 但在數(shù)據(jù)競爭分析中，BinGraphM 的表現(xiàn)極差。

原因如下：

• 對于線程逃逸數(shù)據(jù)集，一些在精度和可擴展性之間取得平衡的抽象，恰好也具有較好的泛化能力；

• 但在數(shù)據(jù)競爭分析中并非如此。

此外：

• Minimal

  的表現(xiàn)顯著劣于 BinGraph 和 BinGraphM；

• 這表明，線程逃逸分析測試程序上的“最小抽象”實際上在泛化能力方面更差。

結(jié)論：

傳統(tǒng)方法無法可靠地找到適用于貝葉斯程序分析的、具有良好泛化能力的抽象。

6 相關(guān)工作

我們的方法與以下兩個方向的研究相關(guān)：

1. 貝葉斯程序分析
2. 傳統(tǒng)分析中的數(shù)據(jù)驅(qū)動抽象選擇技術(shù)

我們在下面對這些相關(guān)研究進行總結(jié)。

貝葉斯程序分析

貝葉斯程序分析工具基于邏輯規(guī)則構(gòu)建概率模型，融合各種后驗信息，并計算每個警報為真的概率。

• Eugene

  [Mangal et al. 2015] 和Bingo[Raghothaman et al. 2018] 使用用戶反饋作為后驗信息；

• Drake

  [Heo et al. 2019b] 利用舊版本程序的信息；

• DynaBoost

  [Chen et al. 2021] 則使用動態(tài)分析結(jié)果。

由于使用不同的抽象等價于使用不同的邏輯規(guī)則，并且不會導(dǎo)致后續(xù)流程（如構(gòu)建概率模型和泛化后驗信息）的不兼容性，因此我們的方法可以直接與這些工具結(jié)合使用。

BayeSmith[Kim et al. 2022] 利用語法信息從現(xiàn)有規(guī)則中學習新的推導(dǎo)規(guī)則及其概率。

例如，對于現(xiàn)有規(guī)則

R1:A(x) :- B(x)

BayeSmith 可能將其細化為兩條規(guī)則：

• R11:A(x) :- B(x),Loop(x)
• R12:A(x) :- B(x),?Loop(x)

并為它們分配不同的概率。
每條關(guān)于 R1 的基本子句都會被替換為 R11 或 R12 中的一條。

生成的貝葉斯網(wǎng)絡(luò)中唯一的區(qū)別是新增了輸入元組Loop(x)和?Loop(x)，以及基本子句的新概率。

由于輸入元組的概率為1，它們不會影響貝葉斯推理過程。

因此，BayeSmith 并未實質(zhì)改變貝葉斯網(wǎng)絡(luò)的結(jié)構(gòu)，它本質(zhì)上是一種學習基本子句概率的方法。

相比之下，我們的方法改變了貝葉斯網(wǎng)絡(luò)的結(jié)構(gòu)，而不是基本子句的概率，因此我們提出的方法與 BayeSmith 是互補關(guān)系。

傳統(tǒng)分析中的數(shù)據(jù)驅(qū)動抽象選擇

傳統(tǒng)程序分析中的抽象選擇問題已被廣泛研究 [Bielik et al. 2017; Grigore and Yang 2016; He et al. 2020; Heo et al. 2016, 2019a, 2017; Jeon et al. 2019, 2018, 2020; Jeon and Oh 2022; Jeong et al. 2017; Liang et al. 2011; Oh et al. 2015; Peleg et al. 2016; Singh et al. 2018; Wei and Ryder 2015]。

盡管這些方法在優(yōu)化泛化能力方面效果不佳，但其中一些思路值得借鑒。

我們的方法借鑒了其中一些研究 [Jeon et al. 2019, 2018, 2020; Jeon and Oh 2022; Jeong et al. 2017; Oh et al. 2015]，它們使用特征來獨立表達每個抽象點的特性。

在這些方法中，所選特征通常與：

• 程序本身有關(guān)

  （例如某個方法是否包含一個分配站點）；

• 或與分析本身有關(guān)（例如對象分配圖中頂點的度數(shù)）[Li et al. 2018b; Tan et al. 2016]。

為了在貝葉斯程序分析的背景下實現(xiàn)通用性與有效性，我們的方法使用基于整體細化前后推導(dǎo)圖差異的屬性。

7 結(jié)論

我們提出了BinGraph，這是一個用于學習貝葉斯程序分析中抽象選擇的通用框架。BinGraph 的核心思想是：通過多輪迭代細化抽象，并利用推導(dǎo)圖的差異來刻畫每個抽象點。在基于兩個實例分析和13個 Java 程序的實驗中，我們展示了 BinGraph 在增強貝葉斯程序分析的泛化能力方面的有效性。

原文鏈接： https://dl.acm.org/doi/pdf/10.1145/3649845