SSA优化算法：基于lambda演算和ANF的形式化映射

理论计算机科学电子笔记82第二次（2003年）网址：http://www.elsevier.nl/locate/entcs/volume82.html15页SSA优化算法曼努埃尔·M T. Chakravarty1，Gabriele Keller1和Patryk Zadarnowski1新南威尔士大学计算机科学与工程学院澳大利亚悉尼摘要静态单赋值（SSA）形式是依赖于数据流信息的一系列优化算法的核心，因此，对采用这些算法的编译器的正确性至关重要。众所周知，SSA形式与lambda项密切相关（即，函数程序），并且考虑到在lambda演算中用于形式推理的理论和框架上花费的大量精力，利用这种联系来提高我们推理编译器优化的能力似乎是很自然的。在本文中，我们讨论了一个新的形式化的映射从SSA程序的限制形式的lambda条款，称为管理范式（ANF）。我们推测，这种连接提高了我们推理基于SSA的优化算法的能力，并通过提出一个众所周知的基于SSA的条件常数传播算法的ANF变体来提供第一个数据点。1介绍静态单赋值（SSA）形式是编译器优化的流行中间表示[7]，因此，在推理这些优化的正确性时具有相当大的意义不幸的是，由于所谓的φ函数，SSA程序和基于SSA的优化算法的语义的形式化处理是复杂的，φ函数控制进入代码块的数据流边缘的合并[4]。Kelsey [12]和Appel [3，2]指出了SSA形式的程序和lambda术语之间的对应关系功能程序）。我们相信，这种对应关系可以用来简化迄今为止基于SSA形式的我们尤其1电邮地址：{chak，keller，patrykz}@ cse.unsw.edu.au2003年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。CHAKRAVARTY，凯勒和ZADARNOWSKI2建议基于lambda演算的中间形式导致更清晰的算法，我们期望这些算法对具体实现的正确性产生积极影响，即使它们没有被正式验证。在本文中，我们专注于lambda项的限制形式，称为管理范式（ANF）[8]，因为它们比一般的lambda项具有更明确的操作Kelsey [12]将SSA形式与受限lambda项的不同形式联系起来，称为连续传递样式（CPS）。然而，Flanagan等人。[8，17]表明，对于数据流分析，使用CPS比直接风格表示（如ANF）没有真正的优势。事实上，CPS需要额外的转换，如果没有特殊的措施，CPS中的非分布式流程因此，我们不使用Kelsey第3节通过改写Weg- man和Zadeck的[22]稀疏条件常数算法来利用SSA和ANF的对应关系在下文中，我们将Wegman和Zadeck新的基于ANF的算法SccANF.我们用一个符号表示Scc和F，定义良好的语义，与Wegman和Zadeck使用的非正式符号相反我们相信，我们的符号的语义严谨性与我们的中间语言（即ANF）的定义良好的语义相结合，意味着SccANF更适合于形式分析。总之，本文做出了以下技术贡献：• 我们将SSA形式的程序映射到ANF形式的程序（第2.3节）。• 我们介绍的算法SccANF，其中我们声称，它实现了相同的分析ANF程序的SccSSA做SSA程序（第3节）。然而，SccANF的定义更为严格• 我们确定SccANF是保守的;即， 标记为常数的变量确实是常数（第4节）。然而，我们实际上并没有证明SccANF和SccSSA实现了相同的分析。事实上，由于Wegman和Zadeck [22]相当非正式的介绍，这将很难实现。我们做的，但是，目前正式声明我们的映射SSA计划ANF计划的合理性和SCC ANF的合理性。我们喜欢把本文中的结果看作是朝着在传统语言的编译器中获得类型化、函数式中间语言的良好优势迈出的一步。这些好处包括简化了编译器优化正确性的推理，在编译时对优化代码进行基于类型的验证，以及支持生成经过认证的二进制文件[9，20，16，14，18]。此外，ANF自然地将过程内分析与过程间分析集成在一起。CHAKRAVARTY，凯勒和ZADARNOWSKI32使数据流显式在本节中，我们为SSA和ANF定义了一个具体的符号。此外，我们还通过一个将SSA形式的程序转换为ANF形式的等价程序的转换过程来证明这两种中间形式之间的关系2.1静态单一分配表单静态单赋值（SSA）形式[1]是程序的一种命令式表示，它通过要求每个变量只有一个赋值来显式地编码数据流信息。图2显示了SSA形式的阶乘函数。除了两个φ函数，程序类似于标准的三地址代码：为了简洁起见，我们允许在construct语句的分支中内联块;实际上，if语句中的两个赋值应该放在一个单独的块中，这样，if确实表示一个条件跳转。变量x和r的值在“fac”中的三个位置更新。为了实现单一赋值属性，我们为每次更新创建一个新变量，将x分为x、x0和x1，r也是如此。由于可以从起始块或从L1本身到达块L1，因此在L1的开始处，我们必须使用所谓的φ函数合并x和r的两个值源，该函数基于跳转的源块选择值注意，在SSA中，单赋值属性是纯语法的，因为在循环L1中，变量在每次迭代的运行时仍然会更新一个过程可以通过将基本块排列成支配者树来以SSA形式放置，其中每个节点的父节点支配其子节点。如果从过程开始到表达式的每个路径都包含该赋值，则该赋值支配表达式。SSA形式已由Cytron等人推广。[7]，他们描述了一种用于在线性时间内计算优势信息的算法，并演示了SSA如何增加许多需要数据流分析的优化的能力图1给出了结构化SSA形式的抽象语法;即， 我们的变体SSA中的支配树是显式编码的块结构。每个过程的主体由一系列标记表达式组成，这些表达式被构造成支配树（每个花括号组中的第一个块直观地说，大括号为块标签提供了传统的作用域层次结构此外，我们没有将变量打包到CFG中，而是遵循Kelsey [12]，用计算相应值的基本块的标签将每个参数注释到φ函数中，或者在过程的未标记条目块中计算值时开始一个完整的SSA程序p由一组（可能递归的）过程和一个入口点e组成。SSA表达式由以下序列组成：CHAKRAVARTY，凯勒和ZADARNOWSKI4p：：=procx（x）{b}p|eb：：=e|b;x：e|b1;x：{b2}e：：=x←φ（g）;e|x← v; |x ← v（v）;e|goto x;|retv;|return（v）;|ifvthene1elsee2g：：=l：vl：：= x|开始v：：= x|Cx：：=x，x|ϵv：：=v，v|ϵg：：= g，gϵ|x：：=变量或标签c：：=常数e：：=v|v（v）|设x=v在e中|设x = v（v）在e中|letrecfineS|ifvthene1elsee2f：：=x（x）=ev：：= x|Cx：：=x，x|ϵv：：=v，v|ϵf：：= f; f |ϵx：：=变量c：：=常数（非洲民族阵线）图1.静态单赋值与A-正规型以跳跃结尾的作业为了讨论的目的，我们不指定常数集;一般来说，它将包括整数，浮点数和机器操作码（原语）。为了简单起见，我们假设程序中的所有变量和标签都是唯一的。2.2管理范式图1的右侧以管理范式（ANF）[8]呈现了程序的抽象语法，这是一种如图2中的ANF代码示例所示，函数是使用letrec表达式引入的，它对应于完整的程序和SSA形式的特定过程的CFG结构。尾调用通过它们在let表达式中的位置显式表示：出现在变量绑定右侧的函数应用程序表示正常调用，而出现在主体中的函数应用程序表示尾调用（跳转）。像SSA形式一样，ANF通过命名程序中的所有子表达式来显式地编码数据流，并且只允许对任何特定变量进行单一定义。然而，在ANF中，这种限制是动态的，因为在运行时，每次调用函数都会创建一个新的作用域这使得ANF语义的公式化直接和直观。此外，它将用于表达数据流的机制的数量从两个（φ函数和过程参数）减少到一个（仅参数），简化了程序分析并消除了SSA中过程内和过程间数据流之间的人为区别最后，定义的语法清晰的范围简化了许多有效和有用的优化的制定，这些优化涉及跨基本块的代码运动在SSA中，这些算法的设计受到保持程序优势属性的需要的阻碍[2]。SSA和ANF程序的形式化操作语义在CHAKRAVARTY，凯勒和ZADARNOWSKI5FFFFprocfac（x）{r←1;gotoL1;;L1 ： r0<$φ （ start ：r，L1：r1）;x0<$φ（start：x，L1：x1）;ifx0thenr1←mul（r0，x0）;x1←sub（x0，1）;gotoL1;其他intn =0;}return（10）;莱特雷克fac（x）=letrecfac′（x0，r0）=ifx0then设r1=mul（r0，x0）x1=sub（x0，1）infac′（x1，r1）elser10的infac′（x，1）infac（10）（非洲民族阵线）图2. 阶乘函数本文的完整版本[5]。ANF的变体在许多函数式语言的编译器中用作中间表示，包括Haskell的GHC[11，21]和ML的TIL [20]2.3从SSA到ANF阶乘函数的SSA和ANF形式之间的相似性在图2中的例子是显而易见的：SSA块被转换成ANF函数，其中参数列表来自块中的φ表达式在图3中，我们定义了一个函数，该函数将格式良好的结构化SSA程序形式化为ANF。翻译遵循SSA形式的程序结构。完整的程序被F和Fp翻译成一个包罗万象的最外层的字母。 在每个程序中，b和l生成ANF函数 对于每个SSA块，支配者树的每一层都被转换成一个单独的嵌套letrec。这使得沿着支配路径定义的变量通过嵌套过程的常用作用域规则可见，同时通过转换的SSA块为每次迭代构造新的动态作用域。选择组的支配者作为letrec的主体表达式。此外，由于支配者树的叶子除了通过它们的直接支配者之外不能到达，ANF的作用域规则强制SSA形式的支配属性。如果需要的话，结果程序中的嵌套letrec结构可以使用标准的lambda提升[10]转换来处理每个SSA块被转换为单独的ANF函数。跳转被转换为对相应函数的尾调用，其中参数列表由Fg从目标块中的φ当将块转换为函数时，使用φ计算相应的形式参数列表。由于在SSA中，必须通过φ节点访问未沿支配路径定义的变量，因此这强制执行结果程序的格式良好CHAKRAVARTY，凯勒和ZADARNOWSKI6翻译功能：F（p））=letrec Fp（p）in Fe（ Sp（p），start，start）收集SSA程序的外部letrec：Fp（p））=startFp（<$procx（x）{b}p））=x（x）=Fb（b，start，B（b，start））;Fp（p）从dominator树构造内部的letrec结构：Fb（<$e），l，B）=letrec Fl（b，B）in Fe（ Sb（b），l，B）将SSA块收集到内部letrec列表中： Fl（<$e），B）=Fl（b;x：e），B）=x（Fφ（e，b））=Fe（e，x，B）;Fl（b，B）F1（<$b1;x：{b2}），B）=x（Fφ（Sb（b2），λ））=Fb（b2，x，B（b2，B））;F1（b1，B）将SSA块转换为ANF表达式：Fe（<$x <$φ（g）;e），l，B）=Fe（e，l，B）Fe（<$x ←v;e），l，B）=令x=v在 Fe（e，l，B）中Fe（<$x←v（v）;e），l，B）=设x=v（v）inFe（e，l，B）Fe（<$retv;），l，B）=vFe（<$retv（v）;），l，B）=v（v）Fe（<$ifvthene1elsee2），l，B）=ifvthenFe（e1，l，B）elseFe（e2，l，B）Fe（<$gotox;），l，B）=x（Fg（β（B，x），l，B））从φ节点构造函数参数列表Fφ（<$x←φ（g）;e），x）=x，Fφ（e，x）Fφ（<$x<$v;e），x）=Fφ（e，x）Fφ（<$x<$v（v）;e），x）=Fφ（e，x）Fφ（φifvthene1elsee2），x）=Fφ（e1，Fφ（e2，x））Fφ（φe），x）=x为一个已翻译的跳转构造一个参数列表Fg（<$x←φ（g）;e），l，x）=κ（g，l），Fg（e，l，x）Fg（<$x←v;e），l，x）=Fg（e，l，x）Fg（<$x←v（v）;e），l，x）=Fg（e，l，x）Fg（如果v则e1elsee2），l，x）=Fg（e1，l，Fg（e2，l，x））Fg（<$e），l，x）=x查找程序的入口表达式：Sp（<$e））=eSp（<$procx（x）{b}p））=Sp（p）查找过程的入口块：Sb（<$e））=eSb（<$bx：e））= Sb（b）Sb（<$b1;x：{b2}））=Sb（b1）为程序构建标签列表B（e），B）=BB（<$b;x：e），B）=B（b，B），x<$→eB（<$b1;x：{b2}），B）=B（b1，B），x<$→Sb（b2）搜索标签的φ参数列表：κ（<$x1：v，g），x2）=ifx1=x2thenvelseκ（g，x2）查找标签环境：β（B，x1<$→e），x2）=ifx1=x2theneelseβ（B，x2）标签环境的辅助语法：B：：= |B，x → eCHAKRAVARTY，凯勒和ZADARNOWSKI7图3. SSA翻译成ANFCHAKRAVARTY，凯勒和ZADARNOWSKI8F⊥±→∈ H±电子邮件电子邮件∈T{T}∈⊂定理2.1对于任何良构SSA程序p，（p）生成良构ANF程序。定理2.1的证明依赖于SSA和ANF的良构性，这在本文的未删节版本[5]中给出3函数形式为了证明ANF优于SSA的优点，我们引入了基于SSA的稀疏条件常数算法SccSSA的ANF变量。由于空间限制，我们无法在本文中呈现原始算法;请参考Wegman &Zadeck [22]的文章进行比较。本节的其余部分定义了SccANF，我们声称它发现了与SccSSA相同的常数，并删除了相同的不可达代码，给定ANF项，使用图3中的函数F从SSA程序计算。3.1先决条件我们假设被分析的程序是ANF（如图1所定义），它是一阶的，所有变量名都是唯一的，并且包含在Var集合中。（我们将在3.5节讨论高阶程序。）此外，集合 Prim Var 包含所有原始函数的名称。分析在抽象域 Abs=，Const，其中cConst是具体值域的常数值。在Abs上定义了一个偏序，它的最小元素和最大元素都是它的。2更准确地说，对于每个常数cConst，我们有<$c<$。此外，我们定义，对于x，y绝对值，z = x y是绝对值中的最小值，使得x z和y z。这个抽象域背后的直觉是，每当一个变量或函数映射到，它永远不会收到一个具体的值;每当它映射到一个常数，这是它曾经假设的唯一值;每当它映射到T，它是非常数。我们需要一个函数E，它实现了对Prim中原语的求值;即，对p∈Prim，ci∈Const，E <$p（c1，.，cn））计算将p应用于ci的结果。此外，EAbs将E扩展到抽象域Abs-即，如果该原语的任何参数是或T，则它分别产生或T;否则，它的行为与E相同。除了输入程序之外，算法的中央数据结构是一个环境Γ：Var Abs，它将变量名映射到抽象域的值。环境包括值和函数变量的条目，后者确定函数的结果值我们写2.我们使用抽象解释约定，它不表示结果，只表示有冲突的值。这与数据流分析文献中使用相同符号的情况相反。3请注意，这包括非终止函数;因此，这不是一个充分的条件这是一个错误的结论，这个函数是死代码。CHAKRAVARTY，凯勒和ZADARNOWSKI9›→∈S一AS一一联系我们Γx表示在环境Γ中查找与x相关联的值，并且Γ[x a]表示将与x相关联的值更新为a。此外，Dom Γ表示在Γ中有条目的变量。最后，我们将x的项的细化定义为：ΓH[x <$→a]|x∈/DomΓ=Γ [x <$→a]| otherwise= Γ[x<$→（ΓxHa）]该方程的初值为ΓPrim=[p <$→T|p∈Prim]。我们使用FV f来表示函数f体中的所有自由变量;注意，这包括所有参数变量，在递归函数的情况下，包括函数名本身。相反，Occx表示程序中所有函数f，对于x FVf。该算法维护一个工作列表，其中包含需要处理的函数名称;工作列表最初为空。3.2该算法该算法分两个阶段计算程序的优化形式：第一阶段，通过计算变量环境Γ来分析程序，第二阶段，基于Γ计算优化版本。两个阶段都是语法导向的（即，根据来自图1的ANF语法进行）注意，在和的定义中，元变量v可以是常数c，也可以是值变量x。我们假设Γ的正则扩张为常数值，使得Γc =c。我们使用一种符号来表示A和S，这种符号可以理解为纯函数式编程语言Haskell的LATEX增强版本[15]。因此，我们算法的语义是由Haskell的语言定义准确定义的。3.2.1第一阶段：程序分析图4中显示的函数（见下一页）有三个参数：（1）递归遍历的ANF表达式e(2)当前变量环境r，以及（3）当前工作列表r。它返回一个三元组，包含（a）e的抽象值，（b）更新的变量环境，以及（c）新的工作列表。 后者包含的函数 使用，但没有在e中定义，并且其使用增加了有关调用函数的参数值范围计算成本最高的情况是letrec表达式，其中我们需要搜索，直到Γ没有收集到任何新信息。给定ANF中的一个程序e，如果A∈）ΓPrim =a，Γ，，我们可以区分三种情况：• 如果a= 0，程序不会终止。• 如果a=c，对于一个常数c，程序总是得到c。• 如果a=T，则环境Γ表征了CHAKRAVARTY，凯勒和ZADARNOWSKI10⟨ ⟩AH›→∃H ›→ › →→哪里A <$v）Γ = Γv，Γ，A<$f（v1，. 。，vn））| f∈Prim=EAb s¢f(Γv1,.. 。，Vn））| otherwise= ⟨ΓJf , Γ J, if changed then Ω ∪ {f } else Ω⟩f被定义为f（x1，... 。，xn）=er J= r[f，x1，rv1，.。。 ，xnr vn]变了=i rxi< $rvi--表示r是否改变<$letx=e1ine2）a，ΓJ，J=<$e1） ΓΓJJ= ΓJ[xa]changed = Γxи Γatransected =Occx Dom Γin-- dom Dom r删除尚未使用的函数A<$ifvthene1elsee2）ΓA2）ΓJJ（如果改变，则不考虑其他情况）| Γ v == ⊥= ⟨⊥, Γ, Ω⟩| Γ v == True= A¢e1) ΓΩ| Γ v == False= A¢e2) ΓΩ| Γ v == T= leta1，r1，a2，r2，f1，. fnine）让a，rJ，在a1Ha2，Γ2，rJJ，。。 ，fn）Γ J（f n，f N）在如果Γ J== Γ JJ，则λa，Γ J，λ JJ不等于λletrecf1，.。。，fnine）Γ JJ<$JJAfixfunn1，.. 。，funn）|$i. fi∈=r，r| otherwise =让a，rJ，ΓJJ= ΓJH [fi <$→a]JJ=在一个固定的乐趣1，。。。 ，funn）Γ JJ（if Γ fi<$r a then <$JJ<$（Occ fi<$Dom Γ）else <$JJ）哪里（fi（x1，. 。，xm） =e）=funi一一CHAKRAVARTY，凯勒和ZADARNOWSKI11图4. SccANF的分析功能CHAKRAVARTY，凯勒和ZADARNOWSKI12一EH一›→⊥SS⊥程序. 特别地，映射到常数值的所有变量可以是被所述常数取代此外，所有函数f无法访问的代码。∈/DomΓ构成的各种等式的操作如下。 如果被分析的表达式只是一个常量或变量，我们用Γ来确定它的抽象值。在应用素数p（v1，. 。 ，vn），我们使用T来获得自变量Vi的抽象值，并应用抽象求值函数Abs。 更有趣的是应用用户定义函数f（v1，. 。 ，vn）。通过用Γvi（调用f的具体值）来精化每个xi（到f的形式参数）的映射，可以将元素tΓ精化为ΓJ如果Γ在这个细化过程中实际上发生了变化，那么f就被添加到工作列表中，因为我们需要根据新的环境来（重新）处理它的定义精化f对于确保f出现在Γ中是重要的;即，它被标记为可访问代码。如果被分析的表达式的形式为letx=e1ine2，我们根据e1的抽象值来精化x在Γ中的映射;如果这个精化改变了Γ，所有包含x作为自由变量的函数都被添加到工作列表中，因为它们的抽象值可能因此而改变注意，我们需要将Occx与Dom Γ相交，以确保只有保证可达的函数才被添加到工作列表中如果分析的表达式是一个常数，如果条件变量v是非常数的，我们形成两个分支的抽象值的交a1a2;否则，我们选择由v确定的分支。最后，对于表达式letrecf1，..，fnine，我们首先遍历body表达式e，从相互递归的绑定集合f1，...，fn在修改后的工作列表j中;然后，我们使用辅助函数Afix分析f i。后者是一个递归函数，在每次调用时，它都会选择当前工作列表中出现的函数fi它使用结果来细化Γ中的fi条目;与普通let绑定的情况一样，如果Γ发生变化，工作列表将扩展Occfi。函数fix终止，如果fi不再出现在工作列表中。这并不意味着函数必须为空;它仍然可能包含在封闭的letrec表达式中定义的函数。3.2.2第二阶段：专业化在将抽象值赋给Γ中的变量的基础上，该函数将原始程序转换为具有常量变量和不可达代码的优化程序。该函数在程序中进行单次扫描，并利用以下属性：当-every r将变量（函数）映射到常量c时，该变量（函数）将在使用该变量（调用该函数）的程序的任何可能运行中包含（返回）c 此外，表示函数不会终止。因此，这样一个函数的任何出现都可以被一个任意的发散计算所取代，我们再次用来表示。CHAKRAVARTY，凯勒和ZADARNOWSKI13一不不任何不在Dom Γ中的函数都是死代码。将原始程序与由A计算的环境Γ结合为优化程序的专门化函数定义如下：第五节）|Γv∈/{T，τ}=Γv-常数t| otherwise= v--non-constantS<$f（v1，. 。，vn））|Γf/=T=Γf| eval=E¢f(w1,.. 。，wn））| otherwise=f(w1,.. 。，wn）哪里wi= S <$vi），i∈{1，.， n}eval = f∈Prim且i∈ {1，.，n}。wi∈ConstS<$letx=e1ine2）|Γx∈/{T，ε}=S<$e2）--x是常数| otherwise= 设x=S <$e1）inS <$e2）S<$ifvthene1elsee2）| Γ v == True= S¢e1)| Γ v == False= S¢e2)| otherwise= if v then S¢e1) else S¢e2)S<$f（x1，. 。，xn）=e）|f∈/DomΓ=π-u nusedc ode| Γ f /= T= ϵ-- constant function| otherwise=f(x1,.. 。，xn） =S<$e）Sletrecf1，.，f2ine）=letrecS？f1），. 。。，S <$f2）in S <$e）3.3侧-E截面到目前为止，我们还没有讨论SccANF如何处理侧边引用原语（例如I/O操作）。他们需要一些额外的照顾，但不构成任何基本的精神问题。每当遇到一个侧射基元p（图4中的第二个方程）时，假设p的应用的评估结果为。此外，任何函数体中包含一个侧面连接原语的函数在Γ中。 后者的基本原理是，即使函数是常量，也不能删除它，因为它的调用带有一个结果。注意，侧终止原语的存在是我们需要区分死代码函数和非终止函数的唯一原因。如果一个非终止函数有一个输出，我们不能用任意的发散计算来代替它。换句话说，unfined（）=unfined（）ones（）=letx=write char需要区别对待;虽然，A会将A分配给两者。CHAKRAVARTY，凯勒和ZADARNOWSKI14∈ EE∈AS不H →T→T3.4内联由于ANF已经包含了函数抽象的概念，它适合于一组函数或过程的统一表示，这为过程间分析开辟了一条道路，在我们的例子中，是过程间常量传播。众所周知，将内联或过程集成与常数传播相结合可以改善结果。对于非递归函数（不包含边引用原语），SccANF，将它们视为A和S中的原语。更确切地说，在定义和的第二个等式中，我们用一个更自由的条件“fPrim或f是非递归的”来代替条件fPrim。此外，我们扩展和Abs的能力，评估非递归函数。3.5高阶函数SccANF需要一阶程序，因为它不显式处理高阶变量。然而，高阶变量的处理对于现代面向对象语言和函数式语言是有多种不同复杂程度的方法可以扩展SccANF给出最不精确结果的最简单方案是将Γ精化为Γ[x1，...，Xn对于所有函数f（x1，...，xn）= e，它们被分配给一个变量（而不是被调用）。这反映了我们无法获得关于f被调用的参数值范围的任何知识。此外，A需要针对任何高阶调用站点x（x1，...， xn），其中x是未知函数值。虽然上面的xi到的映射是正确的，但它太保守了，因为我们可以静态地推断出一些分配给变量的函数的调用位置。特别是，我们改进的基本方案，使用常数传播，以确定高阶调用网站，所有可能的执行程序，调用相同的功能。为了做到这一点，它必须扩展包含在抽象域Abs中的常数集，并使用表示用作值的各种函数的每当A得到对于呼叫站点x（x1，...，xn），我们可以将该调用位置视为f（x1，...，xn）。然而，通过注意到SccANF和抽象解释的相似性[6]，以及SccANF对应于所谓的0CFA分析的事实ysis [19]，我们可以使用抽象闭包的幂集作为高阶变量的抽象域。对所得到的算法的详细描述超出了本文的范围，但它与Sabry和Felleisen [17]研究4新算法为了确定可靠性，我们需要三个辅助定义。第一个问题涉及环境，表达式的自由变量。它是健忘的CHAKRAVARTY，凯勒和ZADARNOWSKI15≤与绑定变量相关的条目。定义4.1Γ0≤FV（e） Γ1惠x∈ FVe Dom Γ0， Γ0x = Γ1x。接下来的两个定义涵盖了算法A及其辅助函数Afix对于一个特定表达式的有效性。定义4.2A对表达式e（记为A <$e））i ∈ F对任意两个环境Γ0和ΓJ都有效，其中Γ0≤FV （e ） ΓJ，A <$e）Γ0{}= F_a， Γ， F_a意味着E_Abs<$e）ΓJ=E_Abs<$S_e） ΓJ;此外，如果F_a ={}，则E_Abs<$e）ΓJ =a。定义4.3对于任意两个环境Γ 0和Γ j，Afix对一组函数绑定fs和一个工作列表f（0）（记为Afix <$fs）i是有效的，其中Γ 0≤FV（fs）Γ J，对于每个绑定f（x1，...，xn）=e，Afix<$fs）<$0 <$0=<$<$r，< $r对f∈<$0时EAbs<$e）<$J=EAbs <$Se<$）<$j进行了积分.由于关系FV（e）不注意约束变量，有效性意味着即使输入环境中的约束变量与分配给变量的实际值不同，算法也会产生合适的环境。 这个属性很重要，因为算法是乐观的，即，在算法执行期间构造的中间环境可能对某些变量的值作出不正确的假设然而，除非所有这些绑定都被T替换，否则算法不会终止。定理4.4（A的合理性）A对所有ANF表达式e成立。证明过程是通过归纳表达式中letrecs的嵌套深度进行的，并包含以下三个主要步骤：(i) 基本情况（A（0））：我们断言对于每个不包含letrec表达式的ANF表达式e，我们有A（e）。(ii) 辅助步骤（A（n）<$A fix（n））：给定一个函数绑定fs和一个工作列表fs，我们断言A fix<$fs）<$仅当对于所有绑定f（x1，.， xn）=efromfs，A <$e）成立。(iii) 归纳步骤（A（n）<$A（n+ 1））：给定函数绑定fs的列表和ANF表达式e，我们断言A <$e）和A fix<$fs）一起隐含A <$letrecfsin e）。我们在本文的未删节版中详细介绍了这三个步骤[5]。5结论本文将SSA形式的程序映射到ANF，并给出了Wegman Zadeck的条件常数传播算法的ANF版本&，我们称之为SCC ANF。此外，我们已经概述了如何基于ANF的算法可以扩展到包括内联和高阶函数。我们感兴趣的是在传统语言的编译器中评估类型化的函数式中间语言的有用性。该算法CHAKRAVARTY，凯勒和ZADARNOWSKI16ASSccANF的定义比Wegman Zadeck的原始算法更严格，因为首先，ANF具有定义良好的语义，其次，我们的符号本质上是编程语言Haskell的一个很好的这种语义清晰性是任何关于编译器优化的严格形式化推理的先决条件此外，这是一个先决条件，认真比较工作的抽象解释与经典的数据流分析文献。Lerner等人介绍了一种在基于图的框架[13]第10段。然而，他们的重点是数据流分析的模块组成。致谢。 我们感谢裁判的有益的意见。引用[1] Alpern，B.，M. N. Wegman和F. K. Zadeck，Detecting equity of variables inprograms ， 第 15 届 ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages（1998）。1比11[2] Appel ， A. W. ， “Modern Compiler Implementation in ML,” CambridgeUniversity Press,[3] Appel，A. W.，SSA是函数式编程，ACM SIGPLAN Notices33（1998），pp. 17比20[4] 巴兰斯河一、A. B. Maccabe和K. J.Ottero，程序依赖网络：一种支持命令式语言的控制、数据和需求驱动解释的表示，在：程序设计语言设计和实现（1990），pp.257-271。[5] Chakravarty，M. M. T.，G. Keller和P. Zadarnowski，关于SSA优化算法的功能观点-未删节，技术报告0217，新南威尔士大学（2003）。[6] Cousot，P. and R. Cousot，Abstract interpretation：a unified lattice modelfor static analysis of programs by construction or approximation offixpoints，in：Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium onPrinciples of Programming Languages（1977），pp. 238-252。[7] 塞隆河，J.Ferrante，B. K.罗森，M。N. Wegman和F. K. Zadeck，E. C. C.计算静态单赋值形式和控制依赖图，ACM程序设计语言与系统学报13（1991），pp.451-490[8] 弗拉纳根角，A.萨布里湾F. Duba和M. Felleisen，The essence of compilingwithcontinuations ， in ： ProceedingsACMSIGPLAN1993Conf.onProgramming Language Design and Implementation，PLDI'93（1993），pp.237-2474两个功能的具体实现在Haskell中，http://www.cse.unsw.edu.au/~patrykz/ssa-lambda/。CHAKRAVARTY，凯勒和ZADARNOWSKI17[9] 哈 珀 河 和 G. Morrisett ， Compiling polymorphism using intensionaltypeanalysis，第22届ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages（1995），pp. 130-141。[10] Johnsson ， T. ， Lambda lifting ： Transforming programs to recursiveequations ， in ： Jouannaud ， editor ， Proceedings of the InternationalConference on Functional Programming and Computer Architecture，number201 in Lecture Notes in Computer Science（1985）.[11] 琼 斯 ， S 。 P. 和 A. L. M. Santos ， A transformation-based optimiser forHaskell，Science of Computer Programming32（1998），pp.3-47[12] 凯 尔 西 河 一 、 A correspondence between continuation passing style andstatic single assignment form，ACM SIGPLAN Notices30（1995），pp.13比22[13] Lerner，S.， D. Grove和C. Chambers，组成数据流分析第29届ACMSIGACT-SIGPLAN程序设计语言原理研讨会论文集（2002年），pp. 270-282。[14] Morrisett ， G. ， D. 沃 克 ， K. Crary 和 N. Glew ， From System F toTypedAssembly Language ， ACM Transactions on Programming Languagesand Systems21（1999），pp. 528-569.[15] Peyton Jones，S.例如，Haskell 98：一种非严格的纯函数式语言（1999年）。URL http://haskell.org/definition/[16] Peyton Jones，S. L.，通过程序转换编译Haskell：来自战壕的报告，在：H。R.Nielson，editor，Proceedings of the European Symposium on Programming，Lecture Notes in Computer Science1058（1996），pp.18比44[17] Sabry，A. 和M. 费莱森，是连续传递有用为数据流量分析？ACMSIGPLAN'94 Programming Language Design and Implementation（PLDI）会议论文集（1994年1-12号。[18] Schneider，F. B、G. Morrisett和R. Harper，A language-based approach tosecurity，in：Informatics：10 Years Back，10 Years Ahead，Lecture Notes inComputer Science2000（2000），pp.86比101[19] 颤抖，O.，Scheme中的控制流分析，见：SIGPLAN '88编程语言设计与实现会议论文集[20] Tarditi，D.，G. Morrisett，P. Cheng，C. 斯通河，巴西-地 Harper和P.Lee，TIL：ML的类型导向优化编译器，在：SIGPLAN编程语言设计和实现，1996年，第100页。181-192.[21] Tolmach，A.例如， GHC核心语言（2001年）的第10页。C