如何理解基於CFL-reachability的過程間分析？

01-28

過程間分析是如何轉化為CFL-reachability問題的？CFL-reachability問題又是如何求解的？
能否結合實際問題給出些淺顯的例子？

那位Hao Fu同學已經答出關鍵了，context-free languages因為有那個棧，所以可以用來識別括弧匹配的問題。說得更具體一點就是能配對。程序分析中有許多問題需要解決這個配對的問題，比如interprocedural analysis需要call和return配對，指針分析需要load和store配對。這些需要配對的問題就可以描述成CFL-reachability problem。

關於CFL-Reachability問題本身，Thomas Reps寫有一篇文章：Program Analysis via Graph Reachability。該文包含CFL-Reachability的定義、性質、例子、解法。還給出4個能描述成CFL-reachability problem的程序分析問題（interprocedural data-flow analysis, slicing, shape analysis, flow-insensitive points-to analysis）。題主想要的答案就在裡邊。

把interprocedural analysis轉化成CFL-reachability problem的一個好處是，可以使一部分滿足特定性質的interprocedural data-flow problem，以不那麼高的成本獲得full context-sensitivity。詳情請見Reps等人95年發表於POPL的經典論文Precise Interprocedural Dataflow Analysis via Graph Reachability。

前面的回答已經解釋了CFL-Reachability問題以及如何用它來解決過程間分析，我再補充一下如何求解CFL-Reachability。

傳統的 $O(n^3)$ 演算法基於動態規劃，其中 $n$ 是圖中頂點數，並假設文法的大小是常數。對文法先進行正則化處理，通常是轉化成2NF，即每個rule右端的長度不超過2。這個過程只會讓文法大小線性增長。令 $langle u,v,A angle$ 表示 $u$ 到 $v$ 存在一條路徑，這條路徑所表示的串可以被非終結符 $A$ 生成。可見狀態空間為 $O(n^2)$ 。狀態轉移則是枚舉rule進行。以 $A ightarrow BC$ 為例，設當前有一個未轉移的狀態 $langle u,v,B angle$ ，那麼枚舉已轉移的狀態 $langle v,w,C angle$ ，得到新狀態 $langle u,w,A angle$ 。一次狀態轉移的複雜度為 $O(n)$ ，從而整個演算法是三次方級別的。

一些過程間分析中會產生規模很大的圖，三次方的演算法在效率上比較吃力，於是有一些工作想要優化CFL-Reachability的演算法，或者在實踐中通過一些heuristic提升效率。POPL08有一篇Subcubic Algorithms for Recursive State Machines，大致是用四個毛子演算法優化到了 $O(frac{n^3}{log n})$ 。CC15有一篇Towards a Scalable Framework for Context-Free Language Reachability，大致是借用Datalog（也是一種被用來描述程序分析的語言，表達能力是包含CFL的）裡面的技巧，並使用了四分樹來優化一些矩陣操作。

另外，還有一些工作在挖掘CFL-Reachability的潛力。POPL15有一篇Specification Inference Using Context-Free Language Reachability，想要在代碼片段缺失的情形下做分析，通過帶權的CFL-Reachability（要求路徑的邊權和最小），並給未知的部分添上帶權值的邊，儘可能的對未知程序的行為做較少假設，並將這些假設反饋給用戶，用戶告知這些邊是否實際存在，進而完成分析。POPL15還有一篇Summary-based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks，同樣是想要在一些信息缺失的情況下做分析（例如在callback未知的情況下分析JDK），大致是基於Dyck Language（只匹配括弧的CFL），對圖中邊與邊的依賴建模：圖中兩頂點間的可達性可能依賴於另外一些邊存在。論文中提出的TAL可以認為是對CFL的擴展。

因為題主已經搞懂了，而且有專家現身，我就不繼續班門弄斧了。

取匿了，歡迎搞程序分析的同學私信交流學習。

/***********************************************************************************************************/

正在學這塊, 先談談自己的理解.

context-free grammar 相比regular更強大的原因在於它的自動機(push-down automata)多了一個棧, 因此可以識別括弧匹配這類原本RL識別無能的語言(證明參見pumping lemma). CFL的識別語言問題又可以通過轉化成解圖可達性的問題並用相關演算法來解決.

現在需要把一個函數的調用和它的返回配對起來, 那麼可以把這個函數調用看成(, 返回看成). 因此它也就能用CFL描述, 也就可以用圖可達性來解了.

具體的例子以後上.