Φ-指令的功能消除：静态单赋值形式与寄存器分配的类型系统

理论计算机科学电子笔记176（2007）3-20www.elsevier.com/locate/entcsΦ-指令的功能消除Lennart Beringer1慕尼黑路德维希-马克西米利安大学信息学研究所Oettingenstrasse67，80538慕尼黑，德国摘要我们提出了一个功能模拟消除Φ-指令静态单分配（SSA）代码。扩展以前的工作SSA和函数语言之间的关系，我们表明，从A-范式（ANF）到一个更严格的形式称为GNF的转换需要相同的补偿指令插入，通常插入在翻译过程中从SSA到机器代码。 将翻译从语法级别提升到类型级别，我们引入类型系统其调解从ANF代码到正确寄存器分配的机器代码的转换，并允许在类型化功能设置中执行代码优化和转换关键词：编译，函数中间表示，静态单赋值形式，Phi消除，寄存器分配的类型系统1介绍静态单赋值（SSA）形式[10]是中间代码的一种流行的命令式表示，并且已经证明了几个程序分析任务可以从SSA的使用中受益[25，18，16]。为了保持要求每个变量具有单个定义点的定义属性，引入了Φ-指令，其在基本块的开始处合并变量的内容。在从SSA到机器码的转换过程中，Φ-指令被控制流前置器中的寄存器移动所取代。这种补偿代码的插入需要尊重基本块中Φ指令的并发解释，即使应用于破坏SSA的一些隐式结构的中间程序优化的结果[8]。Appel和Kelsey观察到SSA和函数式编程语言的受限形式之间的密切对应[4，15]。这种对应的特点是：（1）相互尾递归的一阶函数1电子邮件：beringer@tcs.ifi.lmu.de1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.06.0034L. Beringer/Electronic Notes in Theoretical Computer Science 176（2007）3SSA阿佩尔-凯尔西ANFGNF转换进出口圣杯语义重合功能圣杯Fig. 1. 语法圣杯转换和Φ-指令和标记的基本块，（2）这样一个函数的每个形式参数的事实， f相当于标记为f的基本块的开始处的一个Φ指令，以及（3）语法（嵌套）范围与支配Φ指令被放置在何处的支配性概念之间的对应关系。事实上，有可能定义一种语言，其具有作用域导向静态绑定的函数（按值调用）语义与具有解释Φ函数的命令式语义相一致。正如Chakravarty等人[9]所证明的那样，这种对应关系也可以用来表达使用函数语言中的概念和术语由于转换成机器代码破坏了对应的结构，因此无法在SSA级别执行的优化（变量合并，寄存器分配，.. . ）不能直接建模为适当的功能操作的对应物实际上，消除Φ指令可能会引入额外的指令，变量和基本块[8，27]。在以前的工作[7]中，我们介绍了函数代码的语法规则，该规则在没有Φ函数的情况下恢复对应关系。我们提出了一种语言（Grail），它不包含Φ-指令，并且可以给出重合的函数（按值调用）和命令式语义，这两种语义都在一个完全标准的方式。此外，（1）函数（let-bound）变量与命令式变量（寄存器）是双射的，（2）变量的自由出现对应于命令式活性，以及（3）每个函数调用相当于单个（跳转）指令。特别地，“寄存器移位”是显式的，并且在函数调用之前的补偿指令中执行。同样，这种对应关系可以用于关联程序分析框架：我们表明，用于检测寄存器内容何时被访问一次的低级分析可以无论是强制性的还是功能性的。适当的数据流方程的解与某类系统中的导子双射对应。在本文中，我们表明，在语言水平的对应关系延伸到水平之间的转换（图1）。从A-范式（ANF，[14]）开始，我们定义了一系列转换步骤，这些步骤产生Grail范式（缩写为GNF）的代码，这是ANF的一种限制形式，体现了本质圣杯的句法限制为了证明转换对应于Φ-指令的消除，我们考虑SSA上每个单独步骤的效果。这种转换并不要求程序是边分裂的形式，但涉及一种称为分支规范化的L. Beringer/Electronic Notes in Theoretical Computer Science 176（2007）35这是作为转换的最后一步执行的。因此，函数标识符在应用我们的算法之前和之后与基本块标签作为一种语法代码表示，GNF违反了函数抽象原则，因为它没有观察到α-转换，而且在β-归约下可接受程序的类不是封闭的. 在这两个问题中，后一个问题似乎不那么重要，与其他需要函数参数为变量的函数中间语言共享[3，28]。违反α-等价性更为严重，因为它排除了等式推理。因此，在本文的第二部分中，我们介绍了一系列类型系统，它们捕获了转换的不同方面。这些类型系统中限制最严格的类型系统可用于发出满足GNF条件，同时提升强语法条件。 考虑到Grail在命令寄存器和函数变量之间的双向性，这种类型系统以适当的寄存器分配来表征程序就不足为奇了。因此，它可以被用作任意寄存器分配算法的目标，我们表明，语法GNF转换实际上可以提升为类型系统之间的转换。在Grail中，寄存器对程序变量的分配相当于函数表示的语法转换。这对应于大多数命令式编译器的结构，在消除Φ指令后，在低级别执行寄存器分配[21]。相比之下，我们的框架允许人们研究SSA和机器级优化之间的相互作用，在Φ消除期间插入补偿代码，以及组合的低级寄存器分配。总结本文的贡献，我们• 提出了从ANF到GNF的语法翻译，其正确性是根据功能操作语义来说明的（第2节），• 证明了这种转换对应于从SSA程序中消除Φ-函数，使用文献中的一个众所周知的例子作为我们的指导例子（第3节），• 提出了一个类型系统族，其中可以强制映射到同一寄存器的变量可以驻留在同一类型中，并引入了一个正式的代码提取函数，其正确性被声明为操作行为的保存结果（第4节）。我们在第5节结束时讨论了未来和相关的工作。这篇论文的扩展版本可以从作者的主页上获得2语法转换为GNF2.1ANF和SSA我们对SSA和ANF的表示与[9]中的表示类似，但我们将注意力限制在一个过程上：ANF中的函数应用作为尾调用发生。给定相互不相交的常数集Const（包括特殊常数tt和tt，范围为c，d）。. . ）和变量的方差（范围由6L. Beringer/Electronic Notes in Theoretical Computer Science 176（2007）31N1E Eb：：= e |b; f：e |b; f：{b}e：：= rett; |gotof;| x ← t; e| x ← Φ（p1，.，pn）; e| ifttheneelse ea∈ ANF：：= t|f（t1，.， t n）| 设x = t，| iftthena1else a2| recf1（x1，.，x1）= a1：f（xn，.，x n）= ap：：= f：t|start：tt ∈ Term：：=c|Xn1中nnn图二、 掸邦军和胜利阵线f，g，...，x，y。. . ），SSA和ANF的语法如图2所示。ANF表达式可以是术语，函数调用（参数必须是术语），术语的let绑定，条件和命名函数的定义（可能相互递归）。作为标准实践，我们将始终假设函数名f1，...，f n在声明中联合出现是不同的，并且在每个声明中，形式参数是不同的，并且不同于f i。此外，我们只考虑一阶规划。类似的假设也适用于SSA代码：联合定义的基本块的标签是唯一的，并且块f中的Φ指令对于f的每个控制流前导g只携带一个参数g：t。每个ANF函数声明中的形式参数必须是不同的，这在SSA中意味着，基本块中的所有Φ指令具有不同的左侧。 该条件函数式语言中的一个常见要求，并且是基本块中所有Φ指令的并发解释所必需的。 我们建议读者参考[9]， 从SSA程序到ANF表达式的翻译的正式定义，一个正确性参数的程序是正确嵌套的，即程序中的Φ函数的存在服从优势关系（也见[3]和[15]）。我们的ANF操作语义是由一个大步求值关系a v给出的，其中v是一个环境，即从变量到值的有限映射。值可以是常量或闭包（表示为形式参数的三元组环境和功能体）：C=[x1，.， x n]，E，a∈ Clos = Var list × Env ×ANFv∈Val =Const+ClosE ∈Env=Var ›→finVal正如Milner和Tofte [ 19 ]所指出的那样，Aczel的非良基集理论可以用来证明这种设置，因为它保证了三个（相互递归定义的）语义范畴的存在，特别是满足无限恒等式的对象的存在，如F = E[ x → n [ x 1，...，x n]，F，a n]. E的定义域用domE表示，E[x<$→v]表示环境x到v的映射，在其他地方的作用类似于E图3中给出了定义Eav的规则。L. Beringer/Electronic Notes in Theoretical Computer Science 176（2007）37我E11nnCONST埃克塞特VARx∈dom EE x E（x）LETEtwE[x <$→w] avEletx=tinavCALLEf[x1， . ，xn]，F，ai。我 的爱F[xi<$→vi]i=1，...，纳贾季夫E f（t1，.，t n）TRUEE ttE -1000Eiftthena1elsea2vFALSEEE -2002年Eiftthena1elsea2v费加诺夫F=E[fi→E[xi， . ，xi]，F，aii i]i=1，.，nREC1ni埃 厄雷克 f1（x1， . . . ，x1）=a1吉夫1N1：f n（x n，.，Xn ）=an1nn中图三.ANF的操作语义我们省略了SSA程序语义的正式定义，但回顾了Φ函数的标准解释：当控制流从块f传递到块g时，所有Φ指令x1← Φ（f1：t1，...，f1：t1）1 1n n：x k← Φ（f k：t k，...，f k：t k）在g中被解释为并发赋值xk←tk，其中i是唯一指数f i= f。2.2圣杯范式与GNF-转换为了本文的目的，ANF程序被称为Grail范式(GNF)如果它满足以下条件，其中（iii）是可选的。(i) 所有函数都被完全λ提升。(ii) 对于所有函数f，调用f的所有实际参数都是变量，并且在语法上（在每个参数位置）与f的定义中的形式参数一致。(iii) 条件句的两个分支a1和a2iftthena1elsea2是以下形式之一t或f（t1，...，t n）。第二个条件也被称为圣杯的“调用约定”。在[7]中，我们表明，对于满足调用约定的程序，与v密切相关的函数语义与标准的命令式语义一致。后者在没有Φ-指令的情况下与SSA语义一致。第三个条件相当于要求ANF表达式是基本块而不是扩展基本块[21]。一个普通的ANF程序到GNF的转换可以通过以下四个步骤来实现：(i) α-全局转换变量，使得没有变量被绑定超过一次-8L. Beringer/Electronic Notes in Theoretical Computer Science 176（2007）3G-I（f（t，.，t），[x，...，x]，x）Qf（x，.，x）xi= ti1n1n1nG = II（f（t1， . ，ti−1，xi，ti+1， . ，tn），[x1， . ，xn]，x）Qa∈j. X/=tI j（f（t1， . ，tn），[x1， . ，xn]，x）Qletxi=tiinaG-III（f（t1， . ，tn）[x/xi]，[xi，. ，xn]，x）Qa （xi/=ti（f（t1， . ，tn），[x1， . ，xn]，x）Q令x=xiin ak. 你好xk=tj见图4。定义G的规则(ii) λ-提升所有函数，即将函数体的自由变量转换为形式参数，相应地更新函数调用，然后将所有函数声明移动到顶层。结果程序在最外面的位置最多包含一个rec语句。(iii) 将每个调用转换为满足调用约定的代码，即， 确保对由f（x1，...， x n）=a是字面上 的 f（x1，.， x n）。(iv) （可选）通过插入新的函数声明来规范化分支前两个步骤是众所周知的，步骤（ii）中的两个任务通常被称为参数提升和块重构（例如参见Danvy et[11]）。由于我们的语言是一阶的，我们认为λ-提升是指整篇论文中基类型参数的λ第三步的目的是实现（假设的）并行赋值let（x1，.，x n）=（t1，...，t n）在f（x1，.， x n）通过一个一元let绑定序列，后面跟着相同的调用f（x1，...，xn），其中x1，...，xn是f的形式参数。原则上，这可以通过发射让y1= t1在. 让y n= t n进入设x1= y1在... 设x n= y n在f（x1，...， x n），其中临时变量y1，...，y n是不同的和新鲜的。相反，我们提出了以下算法G，它只使用一个临时变量。我们定义了将G（f（t1，...，t n），x）是一个if（f（t1，.，t n），[x1，.，x n]，x） Da可以使用图4中给出的规则导出。同样，xi是f结果a包含k+m令-其中k是位置i的数量，其中ti xi和m是数量循环的序列（即序列[x i0，...，从{x1，.，xn}使得xij= tij+1modl，其中0 ≤ rec[f（α（ρi）， . ，α（ρi））n=n[fi→（ρi， . ，ρi）→ρi]i=1，.，n：inAα（D0）见图12。 寄存器分配：重写步骤例4.4对于分配α，其中α（ρn）= α（ρm）= n，α（ρa）= α（ρb）= a，α（ρtest）=test，应用Aα（. ）t0fac2是rec fac2J（ n， a）=let test= n 1in F <$A α（D）<$v。这个主张来自于一个更一般的结果，对于自由变量的表达式，其证明采用了环境上的等价关系，遵循米尔纳和托夫特的演绎证明技术详情见[6]。4.3证明变换类型中寄存器信息的可用性允许我们将GNF转换重新表述为类型系统之间的转换在图►ai：ρi1niΣ一16L. Beringer/Electronic Notes in Theoretical Computer Science 176（2007）313中，我们给出了一个定义L. Beringer/Electronic Notes in Theoretical Computer Science 176（2007）317f（y，.，y−，x，y我我 我Γ，x：ω1我r，x：ρ我 Σ1我1一期+1，...，yn）：ρifj。ρj=σj：Difj。 ρiσj和x∈/{yj.|j我Σ我 我ωi} dom！D ：y：σΦi. Dcj：Γ， x：ρiyj：σjΓ，x：ρi令x=yiinf（y1， . ，yi−1，x，yi+1， . ，yn）：ρifρiσi和σk。你好ρk=.σj，且x∈/{yj|{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}你是谁？{\fnarialblack\fs12\bord1\shad0\4aH00\fscx90\fscy110}I'm sorry.D ：y：σΦ萨伊体育会yJyi：Dcj：Γ， x：ωyj：σjΓ， x：ωx：ωΣ f（y，.，yn）[x/y]：ρ令x=yiinf（y1， . ，yn）[x/yi]：ρ图十三.证明了将D ∈ Tx变换为Φω（D）∈ Tx，ρ的变换Φ ω。从Tx到Tx的这种转换，ρ，由三个子句定义。该算法将形状调用Dj：Γyj：σj（f）=（ρ1， . ，ρn）→ρr =1，...，y n）：ρ其中ω是新寄存器。这三条规则中关于语域类型的附加条件反映了早期规则G-I的语法附加条件到G-III。 在规则第二子句中，所有导数D^j都是有效的，因为Γ！yj=σjρi对于所有jI. 规则G-III中的单个附加变量的作用是在第三个句子中更正式地，与算法G的关系可以陈述如下：定理4.6设D：Γf（y1，…，y n）：ρ和π（f）=（ρ1，...，ρ n）→ ρ。 设α对于D和dω∈f{ρ1， . . . ，ρn}m。Then（A α（D），[α（ρ1），...，α（ρ n）]，α（ω））DA α（Φ ω（D））.证据 关于Φω（D）的高度的归纳。 详情见[6]。Q这一结果与定理2.1和4.5一起，证明了使用Φ时基于类型的寄存器分配的在命令式编译器中，与寄存器分配交互的低级优化需要在Φ指令被消除之后执行，因此不能利用SSA结构。类型化设置允许我们在功能设置中对这种窥视孔优化进行短语化，并使用ANF结构对其进行合理化。 在非寄存器分配ANF一级，Chakravarty等人重新表述了一种基于SSA的算法，用于执行常数传播和不可达代码消除作为函数操作，并指出这种方法用于证明分析正确性的好处[9]。虽然我们还没有进行详细的研究窥视孔优化，这是不难证明，►Σω18L. Beringer/Electronic Notes in Theoretical Computer Science 176（2007）3t/=x，t/=y，x/=y21简单变换的可靠性，例如令x=t1in令y=t2ina：ρ− →Γlety=t2inletx=t1ina：ρ或者代码发射函数A α（. ）A（设Γy：ρ1D：Γ，x：ρ2a：ρ）ρ1=ρ2α（D）在a：ρ中的Γπ令x=y−−−−→Aα它避免了平凡的分配让α（ρ1）= α（ρ1）在. 由t=y和ρ= ρ1的Let规则的实例化产生。5讨论在本文中，我们证明了消除Φ-指令从SSA形式的代码对应于转换的函数程序从ANF到更严格的GNF格式。我们首先介绍了转换作为一个纯粹的语法转换，结合了众所周知的转换步骤，如λ提升与GNF转换和分支规范化。然后，我们介绍了一个家庭的类型系统，模型中间程序表示和相关的证明转换。使用简单的代码提取函数建立了操作可靠性，如果将其应用于最严格的演算，则生成可以按功能或命令解释的代码，而不需要Φ指令。一些作者最近提出了基于类型的演算用于寄存器分配，通常使用类似ANF的语言[28，1，2，24]。虽然我们已经将注意力限制在具有尾递归调用的一阶语言上，但显然需要将其推广到高阶函数，其中调用者和被调用者需要就特定的寄存器分配原则达成一致。事实上，[28]，[1]和[2]采用了引用系统来记录更一般的函数调用对寄存器的影响，并且类似的注释记录在TAL中的代码指针类型中[20]。Ohori代码是命令式表示的，证明树是线性的。返回指令被建模为公理，顺序程序组合被建模为语法指导的证明规则的应用。结构规则对变量活性进行建模，管理分配过程，并以一种将我们的寄存器变量上下文查找规则泛化的方式在基于寄存器的机器和基于堆栈的机器之间进行区分。虽然与SSA的关系被简单地讨论过，但在[24]中没有给出细节，但[22]探索了各种证明系统和编译成ANF之间的关系。因此，对我们的翻译进行更详细的证明理论分析将补充Ohori的工作，同时在符号上比SSC更接近函数类型系统是.同样基于ANF的是Thiemann的类型系统，其中，再次，上下文的结构规则对寄存器内容的阴影进行建模[28]。L. Beringer/Electronic Notes in Theoretical Computer Science 176（2007）319Agat [1]提出了一种类型系统，用于具有（有限）寄存器文件和（原则上无界）堆栈的机器的低级显式寄存器注释函数形式。从未分配程序到已分配程序的转换是通过两种操作语义实现的，第一种操作语义忽略寄存器注释并使用函数解释，第二种操作语义对寄存器文件建模命令式语义。与我们的设置相反，程序变量不直接对应于寄存器，并且引入了明确的指令，可以在不同的位置之间移动值。类型系统的可靠性结果表明，对于良好类型的程序，这两种语义是一致的，并且使用进一步的操作语义来证明，该操作语义统一了前面的两种语义。类型系统包括闭包的有效注释，确保函数期望它们的参数在正确的寄存器中，并且不干扰活动位置。与这些正式系统类似，我们的类型系统