《理论计算机科学电子札记》2003年第网址：http://www.elsevier.nl/locate/entcs/volume82.html17页分类与形式上的不变折叠Sabine Glesner1德国卡尔斯鲁厄信息大学Jan Olaf Blech2德国卡尔斯鲁厄信息大学摘要常量折叠是一种众所周知的编译器优化，它在编译时就已经计算常量表达式。只有当编译器计算出的结果与目标机器在运行时计算出的结果完全相同时，常量折叠才有效。我们分类不同的算术推导出一个一般条件下，目标机的算术可以被替换为编译器的算术。此外，我们认为整数arithmetics作为一个特殊情况。它们可以用剩余类算术来描述。我们表明，这些算术形成一个格。利用这个格上的序关系，我们建立了一个充要条件，在这个条件下，一个与目标机不同的剩余类算法可以进行常数折叠.关于形式验证，我们已经在Is-abelle/HOL系统中形式化了我们的证明。作为例子，我们讨论了Java和C的整数运算，并显示编译器运算是有效的常数折叠。这个讨论也揭示了C编译器错误行为的潜在来源关键词：整数和剩余类算术，常数折叠，形式正确性，Isabelle/HOL形式化，Java和C整数算术。1电邮地址： glesner@ipd.info.uni-karlsruhe.de2电邮地址： blech@ipd.info.uni-karlsruhe.de2003年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。萨宾·格勒斯纳和J·安·奥拉夫·布莱赫21介绍大多数编程语言没有明确规定如何执行算术计算。相反，它们隐含地引用目标机器处理器的内置算法。 优点是源程序的可移植性更好。特别是整数运算主要用于在小范围内对任务进行计数，其精确表现为整数环Z。同样的源程序可以翻译成16位、32位甚至64位处理器的机器代码。这种情况对编译器中允许的优化有影响。常量折叠是编译器的中间表示中的一种众所周知的优化，它在编译时已经计算常量表达式只有当编译器计算出的结果与目标机器在运行时计算出的结果完全相同时，常量折叠才有效本文在一个一般的框架内对整数运算和浮点运算进行了特别是，我们陈述了一个充分的标准下，目标机的算术可以被替换为编译器的算术。此外，我们描述的充分必要条件下，一个给定的整数算术可以安全地取代其他一些整数算术。这些条件是有效可判定的。我们讨论了Java和C整数算术和允许的编译器算术方面的影响，我们的标准的可替代性。此外，我们提出了一个正式的证明我们的标准，在伊莎贝尔/HOL系统的正确性。作为一个相当有趣的动机的重要性，编译器arith- metic考虑以下可能是真实的故事[Poo 94]。1994年，英国的一家主要城市银行想要找出他们的奔腾处理器中有哪些是奔腾错误的。他们编写了一个测试程序，用它检查了所有的奔腾机器，令人惊讶的是，所有的奔腾机器都有这个错误。为了进一步检查，他们还测试了其他机器，更令人惊讶的是，他们发现这些机器也存在Pentium bug。在困惑之后，他们得出了这样的解释。编译器进行常量折叠，计算表达式，以在编译时揭示Pentium错误这个编译处理器是一个有缺陷的奔腾处理器，它把错误的结果硬连接到翻译的机器程序中。因此，反过来，错误出现在程序的每次运行中，与执行处理器的算法无关这个故事表明，编译器的算法是重要的，需要完全像目标机器的算法，以保证优化的目标程序的行为完全像未优化的目标程序将做的。利用本文的结果，我们给出了算术之间可替代关系的一般框架。我们专门为整数算术的一般设置，得到一个有效的可判定的标准之间的不同的整数算术的可替换性在第二节中，我们回顾了泛代数和抽象代数中的一些符号和结果在第3节中，我们萨宾·格勒斯纳和J·安·奥拉夫·布莱赫3一|∈ F提出了人工智能替代关系的一般框架。在第4节中我们考虑整数算术，并证明它们可以排列在一个格中。这个格同构于整数环Z的同余关系这种分类给了我们一个必要的和充分的标准之间的替代整数arithmetics，表达了某些直观的除数性质。我们在第5节讨论了Java和C的整数运算，并展示了如何用我们的模式对它们进行这个讨论特别揭示了Java和C算术之间的根本区别。在Java中，算术表达式的结果由Java语义决定。在C程序中，算术表达式的结果是根据目标机器算术来定义的。在第6节中，我们描述了我们的Isabelle/HOL形式化。我们将在第7节讨论相关工作。在第8节中，我们总结了未来工作的各个方面。2基础理想情况下，人们可以认为程序设计语言中的整数和浮点运算等于整数环Z或实数域R然而，现实是不同的，因为几乎所有编程语言中的算术都是由目标处理器的可用算术运算来实现的这些操作仅针对有限个可能的输入值定义，因此与Z或R不同。我们描述这些处理器算术以及Z和R作为通用代数。这种一般性的设置使我们能够在一个统一的框架中看待所有这些算术。在这一节中，我们回顾一些标准的符号和结果，从经典和泛代数。有关更多详情或证明，请参阅。[Lan79，Ihr88，BS00]。2.1泛代数定义2.1[运算]对于每个chn∈IN<${0}和每个ch非空集合A，一个映射f：An−→A称为A上的n元运算. n称为f的arity。 A上所有n元运算的集合记为Opn（A）.⬦定义2.2 [代数的类型]一类代数是函数符号的集合F，使得一个非线性整数n∈IN<${0}被分配给一个函数符号f∈ F。 n是f的元数，f是n元函数符号。⬦定义2.3[泛代数] F型泛代数A是有序对 = （A，F）其中A是非空集且F =（fAF）是A上的一族有限运算。由此，给每个n元函数符号f ∈ F赋予一个n元运算fA∈ Opn（A）. A称为A=（A，F）的宇宙F中的元素是A的基本运算。 如果F ={f1，...， f k}是有限的，我们记为（A，f1，.， f k）对于（A，F）.⬦在本文中，只要这种简化是明确的，我们就写f而不是fA萨宾·格勒斯纳和J·安·奥拉夫·布莱赫4-----−→- -例2.4 [群和环]代数的经典例子是群和环。群是一个代数G =（G，·，− 1，1），其中下列恒等式为真：（阿贝尔群也满足交换性：x·y= y·x）。x·（y·z）=（x·y）·z（结合性）e·x=x·e=x（中性元素）x·x−1=x−1·x=e（逆元素）环是一个代数（R，+，，0，），其中+和是二元运算，是一元运算，0是零元运算。一个环满足以下条件：（R，+，，0）是阿贝尔群。是一个结合运算，满足两个分配律：x·（y+z）=（x·y）+（x·z）和（x+y）·z=（x·z）+（y·z）□给定一个变量集合V和一类代数F，项集合T（F，V）像往常一样归纳定义：所有变量v∈V都是项。 如果f是一个n元的函数符号并且t1，...， t n是项，则f（t1，...， n）是一个术语。定义2.5设F是一类代数，V是一组变量。变量集V上的F型项代数T（V）是代数T（V）=（T（F，V），F）使得对每个f∈F，fT（V）（t1，.，t n）= f（t1，.，t n）。⬦2.2同态定义2.6【同态】设A和B是两个相同类型F的代数。一个映射α：A−→B称为从A到B的同态，如果α（fA（a1，...，a n））= fB（α（a1），.，α（an））。α的核ker（α）定义为yker（α）={（a，aJ）|a，AJ∈A<$α（a）=α（AJ）}.⬦定理2.7（级联）设α：A−→B和β：B−→C是从A到B和从B到C的同态。则α和β的级联，β<$α，其中β <$α（a）= β（α（a）），对a ∈ A，也是同态。 ⬦例2.8 [Z的模算术Zn]考虑Z中的模算术Zn，Zn={0，1， . . . ， n−1}。 加法定义如下：x+Zny=（x + Zy）mod n。如果x∈Zn，则−x=n−Zx。 x−Zny是x+Zn（Zny）的缩写。乘法的定义类似。（+Z和Z 分别表示Z中的加法和减法） 很容易证明f：ZZn满足f（x）= xmodn是Z到Zn的同态。□2.3同余关系与商代数定义2.9代数A =（A，F）上的一个同余关系θ是A上的一个等价关系，使得对所有f ∈ F，如果f是 n元的且（ ti ，tJi）∈ θ，1≤i≤n ，则 当（f（t1， . ，tn）， f（tJ1， . ，tJn））∈θ. 所有同余类的集合记为A/θ，包含a的同余类记为a/θ。⬦定理2.10设α：A−→B是从A到B的同态。然后ker（α）是A上的一个同余关系。⬦萨宾·格勒斯纳和J·安·奥拉夫·布莱赫5A Aa一·−∈ ∈ ⇒·∈∈ ∈ ⇒∈--定义2.11[商代数]让 =（A，F）是一个代数，θ是上的同余关系 . 的商代数以θ表示， /θ，是 论域为A/θ且基本运算满足：fA/θ（a1/θ，...，a n/θ）=fA（a1，.， a n）/θ。⬦例2.12[Z的剩余类]Zn={0，1， . ， n−1}可以看作是剩余类nZ+r的标准表示，0≤r≤标准代表n个等价类Fig. 1. Z的剩余类n-1，Z，cf.图1. 剩余类定义如下（对于任意但固定的n≥ 1和所有r，其中0≤r≤n−1）：nZ + r ={x∈Z|x mod n = r}。这些剩余类是同余关系θn在Z：xθn yi ∈x modn =y modn上的同余类。显然，θn是Z上的等价关系，因为它是自反的、对称的和传递的。此外，它是一个同余关系，因为它在运算+Zn，Zn和Zn.因此，我们得出结论：Z/θn=Zn是一个具有定义良好的运算的代数，如定义2.11所示。人们可以证明Zn是一个环（由Birkho环（R，+，，0，）的理想J是R的子集。在交换环中，它们由三个性质定义：J; x，yJx + yJ;以及x J，aRa xJ. 每个理想都是同态的核，反之亦然，同态的每个核都是理想。此外，在Z中，理想恰是同余类nZ，其中n∈N+.□一个重要的结果从泛代数国家的同余关系的代数是一个格（参见。[BS00]）。我们在第4节中对整数算术进行分类时使用了这个结果。定理2.13设A是一个代数，Con A是A的所有同余关系的集合。A的同余格，记为ConA，是其论域为Con A的格，并且满足和连接计算如下：• θ1<$θ2=θ1<$θ2nZ nZ+1 nZ+2.nZ+（n−2）nZ+（n−1）..................−2n −2n+1-2n +2...−n−2 −n−1- n-n+1-n+2.−2−101二......n−2n−1n n+1 n+2...2n−2 2n−12n 2n+1 2n+2...3n−2 3n−1.....................萨宾·格勒斯纳和J·安·奥拉夫·布莱赫6·A ≥ B AB• θ1<$θ2= θ1<$（θ1<$θ2）<$（θ1<$θ2<$θ1）<$（θ1<$θ2<$θ1<$θ2）<$···或者等价地，（a，b）∈θ1<$θ2i <$有一个元素序列a = c1，c2，..，c n= b使得（ci，ci+1）∈θ1或（ci，ci+1）∈θ2，其中1≤i≤n−1。⬦3算术的一般分类乍一看，人们可能会认为编程语言中的整数和浮点运算分别是环和场。对于整数的模运算，这是真的。但是对于饱和整数算术，我们不再有环上的算术。类似地，只有在没有舍入误差或过流的情况下，浮点运算的行为才像域中的运算。在本节中，我们定义了算术的概念，并导出了代数之间的可替换性的概念。此外，我们定义了关于一个特定常数表达式的可替换性定义3.1[算术]算术是F型代数A，使得F中包含以下函数符号：+，−，·，0。+和·是二元函数符号，−是一元函数符号，0是零元函数符号。⬦这个定义涵盖了经典的算术，如Z和R以及Zn，饱和整数或浮点运算在微处理器中实现我们不需要代数的基本运算的任何性质，例如0x = 0。任何正确类型的代数都被接受为算术我们需要能够比较算术。因此，我们定义一个关系 用类型（A）表示由代数A的基本运算解释的函数符号。如果Op≠ Type（A），则我们用A表示|Op如下代数（A，{f A|f∈Type（A）<$Op}），它只有A的基本运算的子集，即Op中包含的运算。定义3.2[更精确≥]一个代数A=（A，FA）更精确比代数B=（B，FB），记为A ≥ B，i ≠• （B）类型（A），如果• 存在一个满射同态f：A|Op（B）→ B。⬦If，then可以用来代替计算常量表达式。为了形式化这一点，我们需要代数A=（A，F）的常数表达式的形式定义我们将它们定义为在“变量”集合A上的相同类型的项代数 如果f：A −→ B是定义在A上的函数，那么我们可以将这个函数提升到f：T（A）−→ T（B）通过将每个a ∈ A映射到f（a）和每个项gA（t1，...， tn）到gB（f（t1），.，f（t n））。此外，我们需要一个赋值函数evalA，它为每个项t∈T（Type（A），A）分配一个A的元素。evalA：T（A）−→ A归纳定义如下：如果t=a，对于某个a∈A，则evalA（a）=a。 如果t = h（t1，...，t n），则evalA（t）= hA（evalA（t1），...，evalA（tn））。萨宾·格勒斯纳和J·安·奥拉夫·布莱赫7∈ABA ≥ B/∈∈B−→ A{|}B −→BB −→ A|定理3.3（可替换性）设A =（A，FA），B =（B，FB）是代数，A ≥ B.令f：A|Op （B ）→ B是A的相应同态|Op （B ）至B。则存在一个函数f−1：T（Type（B），B）→T（Type（B），A），其中f（eval A（f −1（t）=eval B（t），对所有t ∈ T（Type（B），B）。⬦证据 首先我们定义一个函数f −1：Op（B），它可以提升为f−1：T（Type（），B）T（Type（），A）。然后我们证明f−1具有所需的性质。定义f−1：suc hthatf−1（b）=a f（a）=b。 因为f是满射的（cf. 定义3.2），f−1=对于所有bB。 Letf−1（b）f−1（b）（任意但固定）。 则f（f−1（b））=b独立于f−1（b）∈f−1（b）的选择成立（直接从f−1的定义开始）。设t∈T（Type（B），B）.我们证明了f（evalA（f−1（t）））=evalB（t）对于所有通过对t的期限结构的归纳，证明了t∈T（Type（B），B）.BaseCase：t=bforsomebB. f（evalA（f−1（b）=f（evalA（aJ））=f（aJ）=f（f−1（b））=b（其中aJ=f−1（b））。归纳情况：f（eval A（f −1（h（t1，...，t n）== f（eval A（h（f −1（t1），.，f−1（t n）（提升f −1到项）=f（h（eval A（f−1（t1）），.， eval A（f −1（t n ）（eval A的定义）= h（f（eval A（f −1（t1），.，f（eval A（f −1（t n）（f是同态）=h（eval B（t1），.， eval B（t n））（归纳假设）=eval B（h（t1，.， t n））（eval B的定义）定理3.3直接指出，无论何时，我们都可以计算常数表达式in而不是in，因为我们有A和B之间的传递函数。定义3.2和定理3.3描述了编程语言中的算术和目标处理器之间的可替换性的一般情况。它们不仅模拟了数学运算Z和R，而且模拟了标准的模整数运算以及饱和运算和浮点运算。关于常数折叠，也有罕见的情况：考虑例如。一个用浮点运算计算常量整数表达式的编译器如果我们可以陈述传递函数f和f−1，我们可以使用浮点运算来计算整数表情在实践中，人们经常面临的情况是，一个不断的inte-ger表达式将在一个目标模运算中进行计算，但编译器只有一个不同的模运算。定理3.3定义了需要验证的证明义务。有时，确保任意表达式的两个算术之间的可替换性并不重要，但仅对一个特定的常数项。这种情况在以下定义中描述：定义3.4设A=（A，FA）和B=（B，FB）是代数，使得类型（B）等于类型（A）。设t∈T（Type（B），B）.关于t，A比B更精确，记为A ≥tB，如果存在传递函数f：A −→ B和f−1：B −→ A使得f（evalA（f−1（t）=evalB（t）。⬦如果代数A比代数B更精确一个常数项t，那么我们可以用传递函数f和f−1在A而不是B中计算t。萨宾·格勒斯纳和J·安·奥拉夫·布莱赫8∈{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy110}{−}{−{−}{−}∈{−}≤ ≤ −∈{−}··−→4算术格在这一节中，我们集中讨论剩余类算术，即Zn，n中的模算术N+。这些算术包含在编程语言中，通常有两种变体，即有符号整数和无符号无符号整数直接对应于集合Zn= 0，1，. n 1 . 无符号整数上的算术运算与Zn上的定义完全相同。有符号整数表示n/2，...，1，0，1，... （n/2）1，假设n是偶数，否则在范围内（n1）/2，.，1，0，1，... （n1）/2。如果以二进制补码表示进行二进制编码我们可以用统一的方法来处理有符号算术和无符号算术这两种变体。 因此，我们将n个节点{0，1， . ， n−1}作为Z的同余类nZ+r的标准表示，0≤r≤n−1。 此外，我们观察到，数{−n/2，...，-1，0，1，...，（n/2）−1}3表示相同的同余类，其中nZ + r对于r∈ {（n/2），.，n-1}不是由它的标准代表r表示，而是由代表r-n表示，参见。 也 是图1。Eachmodulo-arithmeticZn ，n∈N+，是一个算术：我是m4。1 Z的每一 个二元算术Zn，n∈N+，是F={+，−，·，0}的算术.⬦证据 直接从定义3.1开始。✷定理4.2（剩余类算术的可替换性）设m，n∈N+. 若n整除m，则Zm比Zn 更精确，Zm≥Zn.⬦证据我们需要证明定义3.2的两个要求都得到了满足。第一个，Type（Zn）→Type（Zm），平凡地成立为了验证第二个要求，我们定义一个函数f：ZmZn，并证明它是一个满射同态。设m=pZn（p存在是因为n能整除m）。 每个x0，...，M1可以表示为x = r + ZlZn，对于某些l0，...，p1和0Rn1. 定义f（x）=r。 显然，f是满射的，因为对于x0，...，n1，f（x）=x平凡成立。 因此，我们认为，Zn中的每个元素是Zm中至少一个元素的像。 为了证明f是同态，我们需要证明以下四个等式：1. f（0Zm）= 0Zn3.f（−Zmx）=−Znf（x）2. f（x+Zmy）=f（x）+Znf（y）4.f（x·Zmy）=f（x）·Znf（y）第一个方程成立，其余的方程在下面证明。因此，我们假设x = r + Zl·Zn和y= rJ+ ZlJ·Zn，其中0 ≤r，rJ≤ n−1且l，lJ∈{0， . ， p−1}。2. 证明f（x+Zmy）=f（x）+Znf（y）：f（x+Zmy）=f（（r+Zl·Zn）+Zm（rJ+ZlJ·Zn））=[3]为了简化符号，我们只给出n为偶数的情况萨宾·格勒斯纳和J·安·奥拉夫·布莱赫9≥≥∈≥≥∈}{1}|}≤ ≤ −联系我们|=f（（r+Zml·Zmn）+Zm（rJ+ZmlJ·Zmn））（因为0≤x，ym）<=f（r+ZmrJ+Zml·Zmn+ZmlJ·Zmn）r+ZmrJ如果r+ZmrJ≤n−1=r+ZmrJ−Zmn，否则n= r + Znrj = f（x）+Znf（y）.3. 证明f（−Zmx）=−Znf（x）：f（−Zmx）=f（m−Zx）=f（m−Z（r+Zl·Zn））=f（m−Z（l·Zn）−Zr）=f（m−Zr）==f（p·Zn−Zr）=f（（p−Z1）·Zn+Zn−Zr）=n−Zr=−Znr=−Znf（x）.4. 证明f（x·Zmy）=f（x）·Znf（y）：一方面，我们有f（x）·Znf（y）=r·ZNRJ=（r·ZRJ）modn.另一方面，我们有f（x·Zmy）=f（（r+Zl·Zn）·Zm（rJ+ZlJ·Zn））=f（r·ZmrJ）。r·ZmrJ=rJJ，其中r·ZrJ=lJJ·Zm+ZrJJ且0≤rJJ≤m−1，且（r·ZrJ）modn =rJJJ，其中r·ZrJ=lJJJ·Zn+ZrJJJ且0≤rJJJ≤n− 1。因为n整除m，所以存在q使得q·ZlJJ=lJJJ和rJJmodn =rJJJ，这完成了证明。我是m4。3Z比每个Zn更精确，其中n∈N+，Z≥Zn。证据直接从例2.8和2.12中所述的关于Z✷定理4.4（n-算术格）剩余类代数Zn，n∈N+，与偏序≥的Z构成一个LatitiIntArith=（{Z }<${Zn|n∈N+}，≥）.⬦证据我们根据上面定理4.3的陈述定义inf（Zn，Z）=Zn和sup（Zn，Z）=Z此外，还需要证明对任意两个算术Zn和Zn，存在inf（Zn，Zn）和sup（Zn，Zn）.因此，我们证明了以下，其中inf（Zn，Zm）=Zgcd（n，m） 和 sup（Zn，Zm）=Zlcm（n，m）我们只证明了inf（Zn，Zm）的情况，因为上确界的情况显然，ZnZgcd（n，m）和ZmZgcd（n，m）。此外，不存在另一个Zk满足k>gcd（m，n）使得ZnZk和ZmZk，因为这样k不能整除n和m。✷格Int Arith的顶部元素是Z，底部元素是Z1.格Int Arith是完备格，因为对于ZZnnN+的每个子集A，存在Inf（A）和Sup（A）。下一个定理陈述了Int Arith与Z上的同余关系格ConZ的联系。这个定理是由这样一个事实得出的：对于n N+，剩余类nZ恰好是Z上的理想，如例2.12所解释的。每个理想定义一个同余关系θn，其同余类为nZ+r，0r n1，参见。图1，其中nZ+r=x x modn =r。反之亦然，Z上的每一个同余关系定义了一个理想，这个理想是包含0的同余类定理4.5格Int Arith同构于格的对偶上的同余关系的ConZ。萨宾·格勒斯纳和J·安·奥拉夫·布莱赫10−→∈/∈⊆≥−→{|∈ }⇐ ⊆≥证据设θ n={（x，y）|x mod n = y modn}。我们定义函数f：IntArith锥Z，其中f（Zn）=θn且f（Z）=（z，z）zZ=：θ∞（即只有全同整数等价的同余关系）和函数f−1：ConZIntArith，其中f−1（θn）=Zn且f−1（θ∞）=Z。显然，f和f −1是满射函数，f −1是f的反函数。我们需要证明f是一个同构，即，Zm≥Zni <$θm<$θn。“设Zm≥Zn。然后有一个满射同态f：Zm−→Zn。此外，满射同态g：Z−→Zm和h：Z−→Zn 存 在，因为Z≥Zn和Z≥Zm。h=fg成立。此外，ker（g）=θm，ker（h）=θn。设（x，y）θm= ker（g）存在，但（x，y）θn= ker（h）.这是一个矛盾，因为所有被g映射到同一图像的元素也必须被fg=h映射到同一图像。 因此，θm<$θn必须成立。““：假设θ mθ n和显示ZmZn：假设θ mθ n。为了证明Zm我们证明了n整除M. 为了证明这一点，我们假设相反，n不整除m，并证明这导致矛盾：（m，0）∈θm但（m，0）/∈θn，因为n不整除m。但这与θm<$θn的假设相矛盾。因此，我们得出结论，n整除m，Zm≥Zn。✷从定理4.5可以直接得出，定理4.54.2不仅是一个充分的标准，而且是一个必要的标准：推论4.6Letm，n∈N+. n整除mi <$Zm≥Zn。⬦有人可能会问，为什么我们在陈述定理4.1时没有将整数运算“mod”和“div”（在许多编程语言中都可以使用）包括到下面的反例表明，在这个假设下，我们将不能证明类似于推论4.6中的可替换性准则：（4+Z85）mod Z87 =1，（4 +Z16 5）modZ16 7 = 2，（4 +Z8 5）divZ8 2 = 0，但（4 +Z16 5）divZ16 2 = 4。推论4.6给出了目标处理器中的整数运算可被编译器中的整数运算替换的有效判定准则整数算术Zn的常数表达式可以在整数算术Zmin除以m中计算。在现代处理器体系结构中，n和m始终是2的幂。对于他们来说，这个标准规定，如果编译器算术中的数字表示等于或大于目标处理器中的数字表示，并且如果两者都根据模算术计算值（这并不像看起来那么清楚，参见。我们将在下一节讨论在下面的部分中，我们将讨论C和Java整数算法，并展示如何应用此标准来分类编译器中的有效常量折叠优化这些考虑也揭示了C语言标准[ISO99]包含一些关于整数算术的危险定义萨宾·格勒斯纳和J·安·奥拉夫·布莱赫11−Java整数签名未签名long（64位）int（32位）短（16位）字符（16位）字C整数签名未签名long long int unsigned long long intunsigned long intint unsigned intshort int unsigned short int signedchar unsigned char图二. Java和C语言数据类型5Java和C语言中的算术Java语言规范精确地定义了如何表示整数这是Java的一个重要属性，因为这种编程语言已被设计用于Internet上的分布式应用程序。Java程序需要独立于目标机器执行它而产生相同的结果。相比之下，C（以及大多数广泛使用的命令式和面向对象的编程语言）更加草率，并且留下了许多重要的特性。这种不准确的语言规范背后的意图是明确的。同样的C程序应该运行在16位，32位，甚至64位的体系结构，通过实例化的整数算术的源程序与算术运算内置在目标处理器cessor。这导致了更高效的代码，因为它可以直接使用可用的只要整数计算只处理“足够小”的数字，就不会出现不一致。从这个意义上说，C整数算法是一个占位符，它并没有被编程语言规范精确定义，而是只有通过确定目标机器才能完全实例化。在本节中，我们将讨论C和Java的整数运算。因此，我们表明，C整数算术承担不正确的算术行为的潜在来源Java精确地定义了如何表示整数以及如何计算整数所有有符号整数的值都是长度的2的补码表示，如图2所示。Char是唯一的无符号整数类型。它的值表示Unicode字符，从如果一个整数运算符有一个long类型的操作数，那么另一个操作数也被转换为long类型否则，操作将在int类型的操作数上执行，如果需要，较短的操作数将转换为int。转换规则是精确指定的，参见。[ESGB00].Java整数运算的精确规范精确地确定了由编译的萨宾·格勒斯纳和J·安·奥拉夫·布莱赫12≥−−- − −−程序，独立于执行它们的目标机器。如果是对长整数的运算，则在算术Z 64中计算它们，否则在Z32中计算。回想一下，Z 2 n中的2我们在第四节开始时的解释根据推论4.6，我们可以在编译时就计算Java程序中的常量整数表达式，只要满足以下两个条件之一(i) 该表达式将在Z64中计算，编译器使用算术Zn·64，n∈N+，或(ii) 该表达式在Z32中求值，编译器使用算术Zn·32，n∈N+。C语言规范[ISO99]没有像Java规范那样精确地定义整数值和整数运算。我们不给这里的所有细节，但只讨论最重要的特点和他们的implications上编译算法。C有两种整数值，有符号的和无符号的，参见。图2. C语言规范定义了一个头文件limits. h>，它确定了相应整数类型中一个给定的编译器应该提供这个文件，使得它的特定整数值范围包含C规范中确定的范围C规范要求对于每个有符号整数类型，都有一个对应但不同的相同大小的无符号整数类型整数类型的值具有[ISO99]第6.2.5条无 符号整数表示0，...，2 N1其中N是表示的长度。头文件将无符号整数的最小范围确定为0，.，2N1，其中N是 8表示char，16表示short和int，32表示long int，64表示long long int。对于有符号整数，范围（2 N-11），.，2N−1 1是指定的，N定 义 为 无 符 号 整 数 。 例 如 ， GNU C 编 译 器 [Pro02] 将 范 围 重 新 定 义 为−2N−1，...， 2 N−1− 1根据Z2N，其中对于int，N = 32。C规范中的这些定义，特别是limits. h>中的定义，如果进行恒定折叠，则具有两个潜在的意外行为来源第一个问题涉及目标算法的不完全指定 如果目标体系结构严格遵守中的范围，则不会根据Z2N计算算术，因为元素2 N−1不存在。目前尚不清楚C规范是否打算要求Z2N−1或Z2N算术。因此，编译器算法不能在编译时计算任意整数表达式。只有定义3.4中所述的要求能够被验证的那些才能被计算。例如，如果常数表达式中的整数非常小，使得Z2N−1和Z2N之间的区别无关紧要，则表达式可以被求值。第二个来源的不正确的常数折叠出现萨宾·格勒斯纳和J·安·奥拉夫·布莱赫13|||因为整数范围可以由目标机器任意扩展。例如，它将与C规范相一致，以扩展范围，从而包含比正数更多的负数。虽然这个或类似的扩展仍然适合剩余类设置（我们可以任意选择等价类的代表），但可能会出现一个实际问题：整数的二进制表示不再具有众所周知的解释，即以“1”开头的数字更专业的程序员可能不会期望整数的非标准解释因此，这些被允许的非常规解释是错误的潜在来源6在Isabelle/HOL我们已经正式我们的主要结果关于整数算术的Isabelle/HOL [NPW 02]系统内的替代。Isabelle是一个通用的定理证明者。它可以用不同的逻辑来实例化，而Is-abelle/HOL，简单类型的高阶逻辑，是最广泛使用的一种。我们的主要结果在定理4.2中陈述，并且说如果n整除m，则Zm比Zn更精确。如果想要正式验证编译器进行integer常量折叠，那么我们的Isabelle证明可以成为这个整体正确性证明的一部分我们的Isabelle证明是通用的，因为它没有实例化数字n和m。在本节中，我们将解释我们的Isabelle形式化的主要数据结构和证明步骤。Isabelle证明文档包含数据类型定义、函数和常数定义以及引理。一个引理可以通过应用某些证明技巧来验证，例如归纳法，区分格，或者应用已经验证过的引理。我们将常量表达式建模为树：数据类型Etree=Leaf int节点运算符Etree Etree数据类型运算符=Add Sub M ult我们定义了计算常量表达式树的函数。函数calc计算整数环Z内的树。calcm在Zm的运算中求值，calmn在Zm·n中求值。这里我们只给出calc和calcm的定义。calcmn的定义类似。calcm：：′′Etree intint′′普里姆雷克′′calcm（叶a）m=amodm′′′′calcm（Nodeoxab）m=（caseoxof加上m（计算a m）+（计算b m））mod m）|子图（计算a m）-（计算b m））mod m）|Mult（calcma m）（calcm b m））mod m））′′常数calc：：′′Etreeint′′普里姆雷克′′calc（叶a）=a′′′′ca lc（Nodeoxab）=（Addx（calc a）+（calc b）的情况ox）|子表（计算a）−（计算b）|Mult（ca lca）（ca常数萨宾·格勒斯纳和J·安·奥拉夫·布莱赫14||/|⇒|我们的第一个引理指出，Zmodm中的运算结果与取操作数modm然后计算Zm中的结果相同。引理JJ（calc a）mod m=（calcm a（m：：int））JJ这个引理可以通过对a，JJapply（induct tac a）JJ的归纳来验证。Isabelle创建了这些证明义务：1. int. calc（Leaf int）mod m=calcm（Leaf int）2.操作符Etree 1 Etree 2.[计算Etree1mod m =计算Etree 1m;计算Etree 2mod m =计算Etree 2m]calc（Node operator Etree1Etree 2）mod m=calcm（Node operator Etree1Etree 2）m归纳法的基本情况可以直接使用calc和calcm的定义来验证。Isabelle通过使用策略JJapply autoJJ自动完成这一步。其余的证明义务可以通过对可能的操作者进行个案区分来验证。首先，我们选择Add-操作符并开始区分大小写，JJapply（case tacJJoperator =AddJJ）JJ。Isabelle产生这个结果（由于空间原因，我们省略了另一个情况JJ运算符=AddJJ2.第二章[计算Etree1mod m =计算Etree 1m;计算Etree 2mod m =计算Etree 2m]=（计算Etree1+计算Etree 2）mod m=（计算Etree1m +计算Etree 2m）mod m下面的引理（在Isabelle中可用）用于下一个证明步骤：引理JJ（a+b）mod m=（a mod m+b mod m）mod（m：：int）JJ伊莎贝尔可以完全自动证明这一剩余的证明义务。另外两种情况稍微复杂一些，因为上面使用的引理需要在之前证明。我们还证实了calcm可以被calmn取代。7相关工作编译器的正确性已经在许多研究项目中进行了研究然而，就作者所知，还没有研究对不同的算术进行描述和分类，以确定它们的考虑编译算术正确性的一个非常早期的研究是[MP67]，它验证了算术表达式到机器代码的翻译，但没有注意到源和目标算术可能不同的事实。德国Verifix项目[GZ99]的目标是构建正确的编译器。这个项目已经取得了进展，建立索赔，这是可能的编译器构造的标准框架内建立可证明正确的编译器。在[Nec00]中，展示了如何验证GCC的携带证明代码[NL98]是萨宾·格勒斯纳和J·安·奥拉夫·布莱赫15构造正确编译器的另一种较弱的方法，其保证生成的代码完全满足某些必要的正确性条件。Pnueli [PSS98，ZPL01]还解决了构造正确编译器的问题[GGB02]研究嵌入式处理器专用编译器优化的验证这些作品都没有解决在编程语言及其编译器中处理不同算术的问题。特别是，这些作品都没有建立一个不同的算术之间的一般可替代性8结论本文给出了算术可替代性的一个一般充分判据。因此，我们将算术定义为某些类型的泛代数。我们的可替换性准则定义了算术上的一个序关系。关于整数算术，我们证明了剩余类算术构成一个格，它同构于Z的同余关系的对偶格。这一特征为可替代性提供了一个充分而必要的标准对Java和C语言中的整数运算进行了讨论和比较它们的特点显示了使用Java或C作为实现语言的不同意图和目的Java是为互联网上的分布式应用程序而设计的。Java程序行为必须独立于执行机器而唯一确定。相比之下，C通常用于接近机器代码级别的系统实现。这些C程序必须尽可能高效，因此使用了可用的机器算法.因此，在C语言中，算术运算并没有被完全指定，而是作为各种机器算术的占位符我们认为，这种不完整的C整数运算规范是错误编译器行为的潜在来源尽管如此，我们的研究结果状态的可替换性的一个简单的标准，并可能有助于减少编译错误。我们已经正式的Isabelle/HOL系统，一个互动的高阶定理证明器的整数算术的可替代性我们的标准。这个证明是通用的，因为它没有指定所涉及的整数arith- metics的绝对大小该形式证明可以成为执行常量折叠的编译器的正确性的形式证明的一部分。在未来的工作中，我们希望进一步研究算术，例如。饱和整数运算。饱和算术不再是环，而仍然是我们形式化意义上我们还想考虑一下浮点运算.是否存在不同的可替换点算术是一个悬而未决的问题。很可能，我们需要扩大我们对可替代性的定义，并用舍入误差的相对大小来参数化它，以便对浮点运算进行充分的分类。萨宾·格勒斯纳和J·安·奥拉夫·布莱赫16引用[BS00] Stanley Burris和H.P. Sankappanavar。泛代数课程，2000年。千禧版。最初由Springer于1981年出版[E
我的内容管理
展开
