正式构建控制流图

Question

我正在为大学项目编写编译器，我想将我的抽象语法树转换为控制流图 (CFG)。

我认为 CFG 中的节点（V）应该是来自 AST 的节点。我在算法上知道如何构造边缘集 (G=(V,E))，但我很难更正式地编写过程

我已经创建了这个 scala 样式模式匹配（伪）：

def edges(n:Node)(nestedin_next: Node) : List[(Node,Node)] = 
    n match {
       case (c_1 :: c_2::tl) => (c1,c2) :: edges(c2::tl)(nestedin_next)++
                                   edges(c_1)(c_2)//recurse
       case c_1 :: Nil => (c_1,nestedin_next)::Nil
       case  i@ IF(_,c1,c2) => (i,c1)::(i,c2)::edges(c1)(nestedin_next)++
                                edges(c2)(nestedin_next)
       case _ => Nil
     }

应该匹配 AST 结构，例如：

( IF(1,
       ASSIGN(x,1), // ia1
       ASSIGN(x,2) // ia2
     ) ::  // i1
  ASSIGN(y,2) ::  // a1
  ASSIGN(z,ADD(x,y)) :: //a2 
  IF(z, 
       RET(z), //i2r1
         assign(z,0):: // i2a1
         ret(z) // i2r2
  ) :://i2
   Nil
)

并提供如下边集：

{ i1 -> ia1,
   i1 -> ia2,
   ia1 -> a1,
   ia2 -> a1,
   a1 -> a2,
   a2 -> i2,
   i2 -> i2r1
   i2-> i2a1
   i2a1 -> i2r2
   i2r2 -> _|_
   i2r1 -> _|_ 
}

DotSrc

有人知道如何比scala“伪代码”更正式地做到这一点吗？

我在想一些归纳的东西，比如：

e[[ IF(_,b1,b2) ]] = (if -> b1) + (if -> b2) \cup e[[ b1 ]] \cup e[[ b2 ]]
e[[ b1, b2 ]] = e[[b1]] \cup e[[b2]]

（虽然上面只给出一棵树而不是一个图。例如，从分支的边缘到下一条语句没有边缘）

编辑：

我一直在阅读 kiama and dataflows 上的 scala，我喜欢他们使用的“succ”和“following”方法。不过，我很难将其归结为更正式的描述，主要是因为漂亮的childAttr、s.next 隐藏了一些在我尝试正式指定时变得丑陋的细节。

编辑2：

我已经阅读了 Dragon Book 和“ML 中的现代编译器实现”以及来自 Learning to write a compiler 的一些其他材料，其中一些/大部分提到了数据流和控制流，但从未过多地涉及如何创建任何正式的 CFG。

EDIT3：

通过Kiama作者，Associate Professor Dr. Tony Sloane我收到了一些additional book references to look up。

据我所知，这些书籍的“实现方式”是基于程序的“每个语句”而不是 AST，并且基于基本块。尽管如此，伟大的投入！

Answer 1

Google's Closure Compiler 实现了Control-Flow Analysis，它将 JavaScript 的 AST 转换为控制流图。此实现的想法灵感来自论文：Declarative Intraprocedural Flow Analysis of Java Source Code。

Answer 2

如果您的意图是简单地创建一些看起来更正式的东西，那么您可以使用standard notation 将这些匹配操作表示为推理规则。你应该用一个单一的减少步骤来表达它，而不是递归的，因为这样就足够了，简单地继续应用这些规则，直到不能再应用。

也就是说，这个定义本质上与你的 scala 代码完全相同。如果你真的想做任何“正式”的事情，你需要证明的属性是：

• 您的 CFG 转换算法总是终止
• 相对于给定的 AST 输入，您的 CFG 是否最小
• 对于给定的 AST 输入，您的算法是否有唯一的 CFG 可导出（即，它产生的 CFG 不是不确定的）。

我也不认为您的基本块方法（而不是每个语句方法）一定是一个坏主意。如果你可以匹配一个基本块，你可以编写一个规则，根据这个匹配的存在来断言集合成员资格，这似乎是完全合理的。看起来你开始草拟的归纳定义可以正常工作。

其他有趣的事情可能是尝试（正式地）将structured operational semantics 和您的 CFG 构造联系起来。这方面可能已经有工作了，但我只是粗略地谷歌搜索了一下，并没有发现两者之间有任何明确的关系，但直觉上似乎应该存在。