達到定義數據流問題的特殊情況

Question

達到定義的問題是數據流分析中最根本的問題之一。給定一個包含變量定義和用途的控制流程圖，問題導致計算出哪些變量定義可能達到特定用途。

例如，考慮流圖：

    ____________ 
       1:| x <- ... | 
        ------------ 
        |   \ 
        |    __________ 
        |   2:| x <- ... | 
        |    ----------- 
        |   /
        ____________  
       3:| ... <- x | 
        ------------ 

在塊3的用途變量x可從任一定義在塊1或到達方框2.

該算法用於計算其定義可以達到使用是經典的數據流問題。使用從龍書編譯的符號（新版）的到達定義數據流的問題如下：

域：定義設置（例如{X < - ...，...}）
方向：正向傳遞函數：fb（x）= gen（B）U（x-kill（B））其中gen（B）是塊B生成和殺死的定義的集合（B）阻止B殺死的定義的集合
邊界：OUT [ENTRY] = {}即沒有定義流程用於輸入函數
符合運算符：U（聯合），即流入塊的定義是定義中的前一個塊的聯合。
方程：OUT [B] = FB（IN [B]），IN [B] = U（在PRED P）OUT [P]
初始化：OUT [B] = {}

然而，並非所有的定義都是一樣的。例如，塊1中的定義可能永遠達不到塊3中的使用，因爲它可能被塊2中的定義所殺死。另一方面，塊2中的定義（如果被執行的話）將保留其值直到其在塊中的使用3.

我想找到在定義和使用情況的任何路徑上沒有查殺定義的用法的擴展定義。我的問題是是否存在類似的數據流問題（可能是傳播等）。在數據流分析方面如何解決它。

我確實有一個可能的解決方案，但如果解決方案已經存在，我不想重新發明輪子。

Answer 1

更改問題定義如下：

滿足運營：∩（相交），即該流至一個塊的定義是定義的交集出前身塊。

方程：OUT [B] = FB（IN [B]）， IN [B] =∩（在PRED P）OUT [P]

Answer 2

這裏是我解決了這個問題。這可能不是最有效的方式，但我相信它是有效的。我將把這個問題稱爲保留定義的問題。首先，我計算達到的定義。我在由位集合表示的定義集上使用迭代數據流算法。

爲了做到這一點，我需要首先計算每個塊的gen（B）和kill（B）。這些是分別由每個街區生成和殺死的定義。注意這裏kill（B）是實際kill（B）的一個超集，因爲我不知道什麼定義和哪些塊真的被殺死了，因爲在這一點上我沒有考慮數據流。

應用到達定義後，我在控制流程圖中爲每個塊設置了REACH_IN（B）和REACH_OUT（B）集。我知道保留的定義是到達定義的一個子集。爲了計算它們，我需要找出哪些定義永遠不會從程序進入每個塊時被殺死。我將調用這些集合，不設置kill集合，我將提供一個算法來計算圖中每個塊的NO_KILL_IN（B）和NO_KILL_OUT（B）。這裏是數據流分析的算法。

域：的定義集合（例如{X < - ..，...}）
方向：向前
傳遞函數：FB（X）= X - （殺滅（B）∩REACH_IN（B） ）其中殺滅（B）是阻止B殺死的定義的集合並且REACH_IN（B）流入B的定義的集合。
邊界：NO_KILL_OUT [ENTRY] = U（通用集）即所有定義不被殺死從函數的輸入
符合運算符：∩（交點），即如果某個定義在任何前導塊中未被殺死，則該定義不會被終止。
方程：NO_KILL_OUT [B] = FB（IN [B]），NO_KILL_IN [B] =∩（在PRED P）NO_KILL_OUT [P]
初始化：NO_KILL_OUT [B] = ü

注在傳輸函數中，我們計算殺死（B）∩REACH_IN（B），它是在塊B中被殺死的實際定義的集合。如果我們不使用它，我們將會過於持久。該算法計算哪些定義在每個塊前後都不會被殺死，而不考慮它們是否已經生成。爲了計算所保存的定義，我們簡單地預成型件的交叉點：

PRESERVE_IN（B）= REACH_IN（B）∩NO_KILL_IN（B）
PRESERVE_OUT（B）= REACH_OUT（B）∩NO_KILL_OUT（B）

Answer 3

您可能希望查看時態邏輯，而計算樹邏輯非常適合在控制流圖中定義路徑上的屬性。在CTL數據流性能的一些示例示於本文：

Proving correctness of compiler optimizations by temporal logic