编译器不应该错误编译。窥视孔优化(对输入程序执行局部重写，以提高生成的代码的效率)是编译器错误的持久来源。我们创建了Alive，这是一种特定于领域的语言，用于编写优化并自动证明它们的正确性或生成反例。此外，Alive还可以被自动转换为适合于LLVM优化过程的c++代码。Alive是基于对可用性和形式化方法的平衡的尝试;例如，它捕获但很大程度上隐藏了各种未定义行为的详细语义。Alive在LLVM编译器中发现了许多bug，并被LLVM开发人员所使用。
回到顶部
编译器优化应该是高效的，有效的，正确的，但满足所有这些目标是困难的。在实践中，效率和效果相对容易量化，但正确性却不容易量化。不正确的编译器优化可能会潜伏很长一段时间;由此产生的问题很微妙，很难诊断，因为错误是在比软件开发人员通常工作的抽象级别更低的层次上引入的。
随机测试7，<一个href="#R20">20.是一种提高编译器正确性的方法;它已经被证明是有效的，但是测试当然会漏掉bug。防止编译器错误的一种更强的保险形式可以通过证明编译器是正确的(编译器验证)或证明某个特定编译是正确的(翻译验证)来提供。编译器验证的艺术状态需要一个全新的编译器实现和许多人-年的证明工程(例如CompCert9)，使得这种方法在大多数生产环境中不切实际。
我们开发了Alive:一种新的语言和工具，用于开发正确的窥视孔优化，如图1所示。LLVM中的窥视孔优化由指令组合器(InstCombine)通道执行。Alive的目标是一个实用和正式的设计点;它允许编译器编写者为LLVM的中间表示(IR)指定窥视孔优化，它会在满足模理论(SMT)解算器的帮助下自动证明它们是正确的(或提供一个反例)，并且它会自动生成类似于在指令组合器中发现的手写窥视孔优化的c++代码。Alive的主要贡献在于识别了一个可以自动验证的窥视孔优化子集，并基于LLVM IR的语义提供了一个可用的形式化方法工具，支持在LLVM未定义行为存在时的自动正确性证明，以及支持代码生成。
图1。活着的概述。在Alive中表达的优化是使用Z3 SMT求解器自动验证的。经过验证的优化被转换为c++实现，用于LLVM。
InstCombine转换执行大量代数简化，从而提高效率、启用其他优化并规范化LLVM代码。InstCombine优化一直是LLVM bug的一个持久来源。7，<一个href="#R20">20.
InstCombine转换的一个例子是(x1) +C并把它变成(C1）x在哪里x是变量，是排他的还是，和C任意常数的宽度是x。如果C是3333，这个InstCombine转换的LLVM输入看起来像这样:
%1 = xor i32 %x, 1%2 =添加i32 % 1,3333
优化后的代码:
%2 = sub i32 3332， %x
在Alive中，同样的优化是:
%1 = xor %x, 1%2 =添加%1,C= >%2 = sub C-1， %x
Alive规范在语法和语义上都与它所描述的LLVM转换相似。它比等价的c++实现简洁得多，不使用LLVM的内部数据结构和控制流来表示，并且可以由Alive工具包自动验证。这种转换说明了Alive支持的两种抽象形式:选择编译时常量的抽象和位宽的抽象。
到目前为止，Alive已经帮助我们在LLVM InstCombine转换中发现了23个以前未知的bug。此外，我们还通过监控各种InstCombine补丁提交到LLVM subversion存储库，防止了数十个bug进入LLVM。一些LLVM开发人员目前正在使用Alive原型来检查他们的InstCombine转换。Alive是开源的，也可以在<一个href="http://rise4fun.com/Alive">http://rise4fun.com/Alive．
我们设计Alive来模拟LLVM IR，因为我们的用户LLVM开发者已经是这方面的专家了。Alive最重要的特性包括对常量选择的抽象，对操作数位宽的抽象(章节2.2)，以及对LLVM控制未定义行为的指令属性的抽象(章节2.4)。
2.1.语法
Alive转换具有形式一个B,在那里一个是源模板(非代码)B是目标模板(优化代码)。此外，转换可以包括前提条件。因为像LLVM一样，Alive的表示是基于静态单分配(SSA)形式指令的有向图，所以非依赖指令的顺序是不相关的。
Alive实现了LLVM整数和指针指令的一个子集。它对分支的支持也很有限:为了避免循环，分支不允许向后跳转。活着支持LLVM的新南威尔士、nuw,确切的指令属性，通过添加未定义的行为来削弱整型指令的行为。
新南威尔士、nuw
确切的
范围。源模板和目标模板必须有一个公共的根变量这是对应图形的根。其余的变量要么是转换的输入，要么是由源模板或目标模板中的指令产生的临时变量。输入在源和目标模板中都是可见的。在源模板中定义的临时变量在前提条件、目标和从定义点开始的源剩余部分的范围内。在目标中声明的临时对象在目标剩余部分的范围内。为了帮助捕获错误，源模板中的每个临时指令都必须在以后的源指令中使用或在目标指令中覆盖，而且所有的目标指令都必须在以后的目标指令中使用或覆盖源指令。
常数表达式。为了实现代数简化和常量折叠，Alive包含了一种用于常量表达式的语言。常量表达式可以是一个字面量，一个抽象常量(例如，上页示例中的C)，或者应用于1或2个常量表达式的一元或二元运算符。操作符包括有符号和无符号算术操作符以及按位逻辑操作符。Alive还支持常量表达式的函数。内置函数包括类型转换以及数学和位向量实用程序(例如abs()， umax()， width())。
2.2.类型系统
Alive支持LLVM类型的一个子集，比如整数和指针。LLVM使用任意大小的整数，对每个宽度使用单独的类型(例如i8或i57)。Alive对LLVM的指针和数组类型支持有限，不支持结构体和向量。最近的工作随后扩展了Alive，支持浮点类型。14，<一个href="#R16">16
与LLVM不同，Alive允许省略类型注释，并且不要求值具有唯一的类型。这支持在Alive中对优化进行简洁的规范，因为许多窥视孔优化不是特定于类型的。为每个隐式类型值推断一组可能的类型，并检查每个类型赋值的优化正确性。因为LLVM有无限多的整数类型，所以我们为隐式类型的整型值设置了64位的上限。
2.3.内置的谓词
一些窥视孔优化使用数据流分析的结果。Alive使用一组内置谓词(如isPowerOf2()、MaskedValueIsZero()和WillNotOverflowSignedAdd())使这些结果可用。产生这些结果的分析是可信的:验证它们的正确性不在Alive的范围内。谓词可以与通常的逻辑连接词组合在一起。图2显示了一个示例转换，该转换在其先决条件中包含一个内置谓词。
图2。这是一个生动的例子。((BV）C1) (BC2)可转换为(BV) (C1C2)当C1C2 = 0时为谓词MaskedValueIsZero（V,¬C1)为真，表明LLVM数据流分析得出结论V¬C1 = 0。％B和%V输入变量。C1,C2是常数。％t0, %t1, %t2是临时变量。这个转换的根是%R。
2.4.LLVM中未定义的行为
为了积极优化良好定义的程序，LLVM有3种不同的未定义行为。它们一起支持许多理想的优化，LLVM积极地利用这些机会。
未定义的行为LLVM类似于C和c++中未定义的行为:执行它的程序可能发生任何事情。编译器可以简单地假设没有发生未定义的行为;这种假设给程序开发人员(或编译器和语言运行时，当一个安全的语言被编译为LLVM时)施加了相应的义务，以确保不执行未定义的操作。执行未定义行为的指令可以用任意指令序列替换。当一条指令执行未定义的行为时，所有后续指令也可以被视为未定义。
表1显示了根据LLVM IR规范，Alive的算术指令何时定义了行为。例如,udiv指令只在被除数非零时定义。除了内存访问指令(在原始论文中讨论过)10)，表1中未列出的指令总是被定义。
udiv
表1。定义算术指令的约束条件。<u是无符号的小于。INT_MIN给定位宽的最小带符号整数值。
的未定义的值（undef在IR中)是一种有限形式的未定义行为，它模仿了一个自由浮动的硬件寄存器，每次读取它都可以返回任何值。从语义上说,undef表示某一特定类型的所有可能位模式的集合;的每次使用，编译器都可以随意选择一个方便的值undef启用主动优化。例如，一个1位未定义的值，符号扩展为32位，将生成一个包含所有0或所有1的变量。
undef
毒的价值观，它与未定义的值不同，用于指示无副作用指令具有产生未定义行为的条件。当有毒值被带有副作用的指令使用时，程序将显示真正的未定义行为。因此，有毒值是延迟未定义的行为:它们旨在支持可能未定义操作的投机执行。毒物值污染后续的依赖指令;不像undef，有毒值无法通过后续操作清除。语义的微妙之处undef目前正在研究有害值及其对启用或禁用优化的影响。8
转移指令,shl、ashr,lshr，在它们的第二个参数时产生一个有害值改变数量，大于或等于操作的位宽。
shl、ashr
lshr
指令属性修改一些LLVM指令的行为。的新南威尔士州属性("无符号换行")使符号溢出未定义。例如，Alive转换是有效的，它等价于C和c++中的(x+1) >x到1的优化，其中x是一个有符号整数:
新南威尔士州
%1 =添加NSW %x, 1%2 = icmp SGT %1， %x= >% 2 = true
一个类似的nuw属性的存在是为了排除无符号换行。的加、减、乘或左移操作新南威尔士州或nuw属性溢出，结果是毒药。此外，LLVM的右移和除法指令有一个确切的要求操作不可损耗的属性。表2提供了指令必须无毒的约束条件。编写Alive模式的开发人员可以忽略指令属性，在这种情况下，Alive会推断它们可以安全放置在哪里。
nuw
表2。算术指令的约束是无毒的。>>u和÷u是无符号移位和除法运算。B是操作数的位宽。午时经（一个n) sign-extends一个通过n位;ZExt（一个n) zero-extends一个通过n位。
Alive解释器通过将源和目标、它们的定义条件和整体正确性标准自动编码到SMT查询来验证转换。Alive变换是对所有集合的参数化可行的类型:满足LLVM类型系统约束且不超过默认64位限制的具体类型。
如果Alive转换的源或目标中没有未定义的行为，我们可以使用直接的等价性检查来检查正确性:对于输入变量的每个值，源和目标中出现的任何变量的值必须是相同的。然而，对于2.4节中描述的3种未定义行为中的任何一种，等价性检查都不足以证明其正确性。我们使用细化来推断存在未定义行为时的优化。活体转化的目标改进源模板，如果目标的所有行为都包含在源的行为集中。也就是说，转换可以删除未定义的行为，但不会添加它们。
当一个优化包含或可能产生undef值时，我们需要确保目标永远不会产生源不产生的值。也就是说，anundef源中表示一组值，目标可以将其提炼为任何特定的值，但是undef在目标中表示一组必须的值所有为人精细化之源。毒性值的处理方法是确保当源指令没有产生毒性值时，目标模板中的指令不会产生毒性值，对于任何特定的输入值选择。总之，我们通过检查(1)源定义时目标是定义的，(2)源无毒时目标是无毒的，(3)源定义且无毒时目标生成源产生的值的子集来检查正确性。
为了确定这些条件是否成立，我们要求SMT求解器找出违反这些条件的情况。当找到这些反示例时，将向用户报告这些反示例，如图3所示。相反，如果SMT求解器能够证明不存在反例，那么条件必须成立，优化是有效的。
图3。Alive的错误转换反例报告为LLVM PR21245。
3.1.验证条件代
Alive验证条件生成器(VC Gen)利用位向量理论将值、指令和表达式编码成SMT表达式。LLVM操作和位向量逻辑之间的对应关系非常密切，这使得编码非常直观。对于每条指令，解释器计算3个SMT表达式:(1)表示指令结果的表达式，(2)表示表达式l指示该指令是否已定义，以及(3)一个表达式表明结果是否无毒。第一个类型对应于指令的返回类型。其他是布尔谓词。所有3个可能包含自由变量，对应于优化中未解释的输入变量和符号常量。
通常，指令的结果是通过对其参数的编码应用相应的位向量操作来编码的。它的定义性和无毒条件是定义性和无毒条件的结合，分别是它的论点，以及该指令的任何特定要求。
例如，考虑指令精确的%a， %b，编码如下:
精确的%a， %b
在÷u是无符号位向量除法。无符号除法要求第二个参数非零，而确切的属性要求%的能被整除的% b。
%的
% b。
编码undefvalues。Undefvalues表示可能值的集合。VC Gen将它们编码为新的SMT变量，这些变量被收集到一个集合中
没有发现记录
