浮点比较操作兼容性检查的静态分析

可在www.sciencedirect.com在线获取理论计算机科学电子笔记288（2012）15-23www.elsevier.com/locate/entcs浮点比较操作中位大小的兼容性检查ManuelFüahndrich1FrancescoLogozzo2微软研究院，雷德蒙德摘要我们激励、定义并设计了一个简单的静态分析，以检查浮动点值的比较使用兼容的位宽，从而使用兼容的精度范围。由于处理器内部浮点寄存器（通常为80或64位）的位宽不同，当存储在存储器中时对应的宽度（64或32位）。该分析保证了来自内存（即数组元素、实例和静态字段）的浮点值不会与寄存器（即 参数或局部变量）。没有这样的分析，静态符号验证是不可靠的，因此可能会报告假阴性。静态分析在Clousot中完全实现，Clousot是我们基于抽象解释的静态合同检查器。关键词：抽象解释，契约设计，浮点数，数值抽象域，静态分析，. NET。1引言由于比较值的精度不匹配，在程序中比较浮动点值可能会引入细微的精度失配是由于将通常较大的寄存器内部浮动点宽度（80或64位）截断为将值存储到主存储器中时使用的浮动点宽度（64或32位）而产生的。这种不匹配可能会产生意外的程序行为，导致程序员混淆，如果出现错误，则会导致不可靠的静态程序分析。我们用图1中的代码片段来介绍这个问题，它是从带有合同注释的“经典”银行账户示例中提取的在本文中，我们使用C#作为我们的语言和.NET运行时。然而，本文所讨论的一般问题在许多编程语言和运行时中都存在我们解决这些其他方面的节。五、1电子邮件：maf@microsoft.com2电子邮件：logozzo@microsoft.com1571-0661 © 2012 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.10.00416M. Fähndrich，F.Logozzo/Electronic Notes in Theoretical Computer Science 288（2012）15public class String{私人浮动余额;公共账户（浮动初始）{合同。要求（初始>= 0.0f）;returninitial;}public void Deposit（float amount）{合约.Requires（amount >= 0.0）;合同。保证（余额==合约.OldValue（余额）+ 金额）;余额=余额+金额;}//其他方法}图1.一、经典银行账户示例的C#代码片段 合同要求指定先决条件，合同。确保指定后置条件，合同。OldValue表示入口点处参数表达式的值（在C#中不可直接表示事实证明，后置条件是不正确的，并且它可能在运行时为合适的amount值失败。Account类表示一个银行帐户。Deposit方法通过给定的非负数金额更新余额。Deposit的后置条件声明在方法退出时，余额已正确更新。 当前余额存储在float类型的实例字段中。ECMA标准要求。NET实现，以遵循IEC：60559：1989标准。乍一看，人们期望后置条件成立，任何静态分析器都可以轻松证明它。事实上，通过符号传播的简单推理（balance0表示方法入口处的字段balance值）可以是：assert balance==余额0+金额余额{按分配：余额=余额0+金额}断言余额0+金额==余额 0+金额平等（equality）真不幸的是，一个静态分析器。NET执行此推理将是不健全的！例如，下面两行C#代码：var account = new Account（6.28318548f）; account.Deposit（3.14159274f）;在方法Deposit中导致后置条件违反（参见 图2）。这是怎么了让• 可以排除过低，因为浮动点数不能过低（在最坏的情况下，操作会导致特殊值±∞或NaN）。• IEEE754标准和示例中的代码是单线程的事实排除了非确定性。• 也要排除抵消：例如，数值量是正的，并且具有相同的数量级• 浮点加法是可交换的，所以这不是问题的原因M. Fähndrich，F.Logozzo/Electronic Notes in Theoretical Computer Science 288（2012）1517图二、Deposit的后置条件在运行时失败。要么.• 加法不一定是结合的，但我们在这里不需要结合性（我们只加两个数）。真正的罪魁祸首是平等测试。一般来说，所有对浮动点值的比较都然而，乍看起来，为什么这种比较会成为问题的根源还不清楚：毕竟，我们是把同样的两个量加起来，然后比较它们是否相等。如果发生了一些舍入误差，那么在两次加法中应该发生同样的误差，或者意外行为的原因是要找到更深层次的规范的共同语言（分区I，节。[1]的12.1.3浮点数（静态数据、数组元素和类的字段）的存储位置是固定大小的。支持的存储大小为float32和float64。 其他地方（在计算堆栈上，作为参数、作为返回类型和作为局部变量）使用内部浮点类型来。在每一个这样的实例中，变量或表达式的名义类型是float 32或float 64，但它的值可以在内部以额外的范围和/或精度表示。内部浮动点表示的大小取决于实现，可以变化，并且精度至少应与所表示的变量或表达式的精度一样大。当从存储器加载这些类型时，执行从float32或float64到【...】当内部表示形式为具有比其标称类型更大的范围和/或精度，则将其自动强制为存储位置的类型。该标准允许利用最大精度从浮点硬件可用的寄存器中的值的操作，而不管其标称类型，只要在内存存储的内部值被截断到标称大小。现在很容易理解为什么我们在运行时会遇到后置条件冲突对表达式this的求值结果。balance+amount以硬件可用的最大精度进行内部存储（在Intel处理器上为80位寄存器，在ARM架构上为64位）。在该示例中，18M. Fähndrich，F.Logozzo/Electronic Notes in Theoretical Computer Science 288（2012）15L=k(loadconst）l=l1l=l 1 opl 2l= o. F（副本）（二进制运算）（负载场）l=（类型）l1O. f=L（演员）（storefield）l=a[li](load数组）a[li]=l（storearray）图3.第三章。我们考虑用于分析的简化字节码语言常数k只能是属于float32或float64范围的只允许类型转换为∈{float 32，float 64}。相加的结果是9。42477822，无法精确表示的值 32比特的连续字段存储强制将值截断为32位，从而更改值。例如，9。42477822被强制为浮点数，导致精度损失，从而导致value9。424778是在这个领域中被发现的。平衡当计算后置条件时，平衡的截断值被重新计算。从内存中加载，但后置条件中的加法是用内部精度重新计算的。比较这两个值会导致后置条件失败，因为9。424778/= 9. 42477822.贡献我们提出了一个简单的静态分析来检查，迭代点比较（等式，不等式）使用兼容类型的操作数当它们不兼容时，分析向用户报告警告消息，以便所有连续的验证都应被理解为有条件的。我们在Clousot中完全实现了分析，Clousot是我们基于.NET抽象解释的静态合约检查器[2]。我们通过在.NET的基类库上运行它来验证分析，它发出了5个真正的警告。2语言我们说明了我们的分析上的最低限度的字节码语言。我们做一些简单的假设。 有两 种 变 量 ： 存 储 变 量 （ f ， a∈S ） 和 局 部 变 量 （ l ， p∈L ） 。Storevariablesareinstancefields，staticfieldsandsquares. 局部变量是局部变量、参数和返回值。变量属于集合Vars=SL。不允许出现别名。该语言只有两个名义浮点类型（float32，float64∈TN）和一个内部浮点类型（floatX），使得64≤X。 在x86上，floatX是float80，允许扩展浮点精度。请注意. NET标准不像C [3]那样包括长双精度型，因此应用程序员无法访问floatX类型。所有变量都有一个名义型的浮动点类型。在运行时，局部变量的名义引用点类型可能会扩大，但存储变量的类型不会扩大。我们说“可能被加宽”，因为它取决于编译器的寄存器分配选择。我们认为，强制代码独立于浮动点寄存器分配选择来计算值是合理的。简化的字节码语言如图所示3 .第三章。浮点常量M. Fähndrich，F.Logozzo/Electronic Notes in Theoretical Computer Science 288（2012）1519第0章：L1=这个平衡一曰：L2=金额+l1第二章：这个平衡=L2第三节：L1=这个平衡第四章：lcomp=l1==l 2图四、在我们的简单字节码指令集中运行示例的（部分）编译加载到局部变量中（load const）。允许的常量值仅为标称类型所允许的值，即32或64位的浮点常量，包括±∞和NaN（非数字）等特殊值。值可以复制到局部变量，保留其内部值（复制）。只允许对名义型类型进行强制转换，并根据需要缩小或扩大值（强制转换）。一般来说，如果l1和l具有相同的名义类型，那么（cast）在语义上等同于（copy），因为它们的内部类型可能不同。二进制运算是通常的浮点算术运算（+，−，，/）和（无序）比较运算（==，≤，）（二进制运算）。计算的结果是0。如果比较结果为假，则为0;如果比较结果为假，则为1。0否则。值从字段（[load/store]字段）加载并存储到字段。我们不区分静态和实例字段。字段仅包含名义类型的值：因此，当将局部存储到字段中时，其值自动缩小到字段名义类型值。如果l的值太大或太小，则它近似于±∞或0。类似地，从数组读取的值具有名义类型值，而写入数组的值被缩小为数组类型的名义数组是由局部值索引的，除了通常的越界检查外，我们假设当li是一个具有非零小数部分的浮点数或它是NaN时，计算也会停止。例2.1图1的方法deposit（没有合约）的主体的简化字节码的编译在图4中。 请注意，商店和 加载字段操作现在在字节码中变得显式3抽象语义学3.1抽象域我们使用的抽象域T捕获变量可能具有的潜在运行时重定位点宽度，这可能比其名义类型更精确。因此，T的元素属于集合Vars−→TX，其中64≤X，TX是抽象域：T，，浮动3，，2floa，，t6420M. Fähndrich，F.Logozzo/Electronic Notes in Theoretical Computer Science 288（2012）15floatX⊥M. Fähndrich，F.Logozzo/Electronic Notes in Theoretical Computer Science 288（2012）152110. f=l）（τ）=τ<$l=l）（τ）=τ[l<$→τ（l）]11<$a[l]=l）（τ）=τi<$l=lopl）（τ）=τ[l<$→floatX]12（Ⅲ）（Ⅲ）<$l=k）（τ）=τ[l<$→η（l）]<$l=（type）l1）（τ） =τ[l<$→type]l=o。f）（τ）=τ[l] →η（o. （f）]→η（a[·]）图五、抽象的语义。函数η返回变量的名义类型如果X= 64，即硬件不提供任何更宽的浮点寄存器，则float64和floatX重合。这是ARM架构的情况，但 而不用于提供额外精度寄存器的x86体系结构抽象域T的运算（order，join，meet）是上面格上的运算的逐点扩展。不需要加宽，因为网格具有有限的高度。3.2抽象语义抽象语义·∈P×T−→T在每个程序点静态确定每个局部变量的内部类型。根据ECMA标准，已知悬挂物变量的名义类型与内部类型一致抽象传递函数的定义见图5。唯一可以显式表示的常量值是那些可接受的float32或float64值：在负载常数之后的局部的内部类型是其标称类型。变量副本保留内部类型。ECMA标准保证将值v强制转换为类型会将值v截断为类型范围中的1。如果v对于类型来说太大或太小，那么它将四舍五入到±∞或0。二进制运算的结果是最大硬件精度的值，我们用floatX表示。从字段或数组位置读取提供标称类型的值（字段中不能存储额外的精度）。写入字段或数组位置会导致将值截断为相应的名义类型。例3.1对于图4中的字节码，τ0=[amount<$→floatX]，每个程序点后面的推断内部类型是：0：τ1=τ0[l1float32]1：τ2=τ1[l2<$→floatX]2：τ3=τ23：τ4=τ3[l1→›4：τ5=τ4[1comp浮动32]floatX]3.3检查现在检查程序P在浮动点比较中的精度不匹配是相当容易的。首先运行分析P，为每个程序点收集内部类型的过度近似。对于P中的每个（二元运算），pp：l=l1opl222M. Fähndrich，F.Logozzo/Electronic Notes in Theoretical Computer Science 288（2012）15见图6。 克劳索发出的警告使得op是==，≤， getτpp之一，这是pp的抽象预状态。若τpp（l1）或τpp（l2）与T不同，且τpp（l1）=τpp（l2），则对于具有相同内部类型的变量否则，比较可能发生在不同宽度的浮动点值上，因此应向用户发出警告。例3.2在我们的运行示例中，τ5（l2）=floatX，τ5（l1）=float32。 因此，向用户发出警告（参见。图6）。3.4修复警告当分析不能证明比较的操作数是同一类型时，用户可以通过添加显式转换来修复它。例如，在我们运行的示例中，正确的后置条件是显式的类型强制合同。保证（余额==（float）Contract.OldValue（balance）+ 金额）;从程序员的角度来看，这种强制似乎是多余的，因为表达式契约。OldValue（balance）+amount已经具有名义型float32。他/她可能期望到float 32的显式强制转换将是无操作。但由于本文所解释的原因，演员阵容可能是一个截断。4实施和实验我们已经在Clousot中实现了本文中描述的分析，Clousot是我们的CodeContracts静态分析器[2]。分析器首先从磁盘读取IL，然后为每个方法构建控制流程图，在必要的点插入合同。然后，它通过摆脱计算堆栈和堆来简化程序，重建在编译过程中丢失的表达式，并最终生成标量程序。在标量程序的顶部运行几个分析，即：非空、数字、数组或算术。我们在算法分析中增加了本文所述的定位点比较中的精度失配检测的核心库上的分析是快速和准确的。NET框架工作，mscorlib. dll，由25089个方法组成，总时间增加不到10秒，它报告了5个警告。我们手动检查了它们，它们都代表了类似于以下示例的真实警告：public boolean isNonZero（） {M. Fähndrich，F.Logozzo/Electronic Notes in Theoretical Computer Science 288（2012）1523return f！= 0.0F;}根据ECMA标准，调用者的参数f可以在寄存器中传递，因此在内存中使用比float32更多的位因此 ，与0相比，不平等。0F可能导致true，即使f被截断为float32等于0。是的。作为这可能导致问题的示例，请考虑：classC {float a;//不应该是0.0Fpublic booleancompute（booleancompute，booleancompute）{this.a= f;}...在上面的代码中，程序员希望保护对字段的赋值确保存储在字段中的值永远不为0。是的。然而，由于f的寄存器分配，使用超过32位表示的值接近于0。0F但不等于0。0F可以通过测试并被截断为0。当存储在这个。a.5讨论一些语言和编译器已经使用其他方法解决了本文中描述的问题。C编译器通常使用编译时开关来控制编译器是否应该发出严格遵守类型中定义的位宽的代码，或者是否允许在寄存器中使用额外的精度进行计算。使用严格遵守声明的类型要求编译器在每个可能导致更高精度的截断点操作之后发出截断强制转换，或者将截断点单元置于自动执行截断的模式[10]。Java标准提供了strictfp关键字来强制执行这种trun行为，从而完全避免了本文中描述的问题，精确度和速度的代价。我们决定只在比较浮动点数时检测精度不匹配的问题另一种观点是编写一个分析，每当某个更高精度的指针隐式转换为标称类型宽度时（例如，每当结果存储到内存中时），该分析都会警告用户。这种替代分析的问题我们发现，关于比较的警告以更可操作的方式解决了问题。6相关工作以前在这方面的工作主要集中在增强静态分析技术，以合理地分析程序的浮动点。例如，[4，6，5]提出了静态分析，以找出在计算浮动点时不精确的原因[9]提出了一些想法，24M. Fähndrich，F.Logozzo/Electronic Notes in Theoretical Computer Science 288（2012）15将数值抽象域扩展到IEEE 754兼容的迭代点值的分析，并[7]引入程序转换技术以减少迭代点计算中的错误。我们的工作是正交的，因为我们对计算的实际值不感兴趣，而只对检测可能导致意外比较结果的情况感兴趣。这种检测的需要对于避免那些看起来已经通过符号执行验证过的合约的运行时失败是特别重要的。7结论我们描述了一个简单的静态分析，以检测不存在“令人惊讶的”行为的分析的动机是我们的代码契约工具的用户反馈。他们报告的假阴性与引言中描述的例子类似。我们在代码契约的静态检查工具中集成了分析，经验表明它足够准确。确认非常感谢Matthias Jauernig，他是第一个报告这里展示的Clousot的不健全的人。也感谢Juan Chen对ARM架构中的停靠点子系统引用[1] ECMA。 通用语言规范。[2] M. Füahndrich和F. 洛格佐 静态压缩与抽象解释。 在Fo V eOOS'10，LNCS。Springer-Verlag，2010.[3] 美国国家编程语言标准C语言规范，1990年。[4] E. Goubault和S.该死有限精度计算的静态分析。在VMCAI，第232-247页，2011中。[5] M. 马特尔有限精度计算中舍入误差的传播：一种语义学方法。在ESOP，第194-208页[6] M. 马特尔回路数值稳定性的静态分析SAS，第133-150页，2002年[7] M. 马特尔数值精度的程序转换在PEPM，第101[8] B.迈耶。Ei Eel：语言。普伦蒂斯·霍尔1991年[9] A. 我的女儿 用于检测运行时错误的关系抽象域。在04年的员工持股计划中。[10] D.蒙尼奥验证浮动点计算的陷阱。ACM翻译计划。Lang.系统，30（3），2008.