到达定义数据流问题的特例

Question

定义达成问题是数据流分析中最基本的问题之一。给定一个包含变量定义和用途的控制流图，问题会导致计算哪些变量定义可以达到特定用途。

例如，考虑流程图：

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

块 3 中变量 x 的使用可以从块 1 或块 2 中的定义实现。

计算哪些定义可以实现使用的算法是经典的数据流问题。使用龙编译器书（新版）中的符号，到达定义数据流问题如下：

域：定义集（例如 {x <- .., ...}）
方向：前进
传递函数：fb(x) = gen(B) U (x - Kill(B)) 其中 gen(B) 是块 B 生成的定义集，kill(B) 是块 B 杀死的定义集
边界：OUT[ENTRY] = {} 即没有定义流进入函数
满足运算符：U(union)，即流向块的定义是前驱块中的定义的并集。
方程：OUT[B] = fb(IN[B]), IN[B] = U(P in pred)OUT[P]
初始化： OUT[B] = {}

但是，并非所有定义都是相同的。例如，块 1 中的定义可能永远不会在块 3 中使用，因为它可能会被块 2 中的定义杀死。另一方面，块 2 中的定义如果被执行，将保留其值，直到在块中使用为止3.

我想找到一个用法的到达定义，该用法在从定义到用法的任何路径上都没有终止定义。我的问题是是否存在类似的数据流问题（可能是传播等）。从数据流分析的角度如何解决。

我确实有一个可能的解决方案来解决这个问题，但如果解决方案已经存在，我不想重新发明轮子。

Answer 1

像这样更改问题定义：

满足运算符：∩（相交），即流向块的定义是前驱块的定义的交集。

方程：OUT[B] = fb(IN[B]),
IN[B] = ∩(P in pred)OUT[P]

Answer 2

这是我解决问题的方法。这可能不是最有效的方法，但我相信它有效。我将把这个问题称为保留定义的问题。首先我计算到达的定义。我正在对位集表示的定义集使用迭代数据流算法。

为了做到这一点，我需要首先计算每个块的 gen(B) 和kill(B)。这些是分别由每个块生成和终止的定义。请注意，这里的kill（B）是实际kill（B）的超集，因为我不知道真正被杀死的定义和块，因为我此时没有考虑数据流。

应用到达定义后，我为控制流图中的每个块设置了 REACH_IN(B) 和 REACH_OUT(B)。我知道保留的定义是到达定义的子集。为了计算它们，我需要找出从程序入口到每个块的哪些定义永远不会被删除。我将这些集合称为“无终止集合”，并且我将提供一种算法来计算图中每个块的 NO_KILL_IN(B) 和 NO_KILL_OUT(B)。这是数据流分析方面的算法。

域：定义集（例如 {x <- .., ...}）
方向：前进
传递函数：fb(x) = x - (kill(B) ∩ REACH_IN(B)) 其中kill(B) 是阻止B 杀死的定义集，REACH_IN(B) 是流入B 的定义集。
边界：NO_KILL_OUT[ENTRY] = U（通用集），即所有定义都不会从函数的入口处终止
相遇运算符：∩(交集)，即如果定义没有在任何前驱块中被杀死，则该定义不会被杀死。
方程：NO_KILL_OUT[B] = fb(IN[B]), NO_KILL_IN[B] = ∩(P in pred)NO_KILL_OUT[P]
初始化：NO_KILL_OUT[B] = U

请注意，在转移函数中，我们计算kill(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 中数据流属性的一些示例：

证明通过时序逻辑优化编译器的正确性