Java字节码的非终止性分析实验及有效终止测试技术

理论计算机科学电子笔记253（2009）83-96www.elsevier.com/locate/entcsJava字节码的非终止性分析实验E'tiennePayet1IREMIAUniversit'edeLaR'eunionFranceFausto Spoto2维罗纳大学信息学系意大利摘要非终止性分析证明程序或程序的一部分不会终止。这一点很重要，因为非终止性通常是计算机程序的意外行为，并暴露了代码中的错误。虽然研究已经找到了证明逻辑程序和项重写系统的非终止性的方法，但对于命令式程序来说，这几乎是不可能的。在本文中，我们描述和实验的技术证明非终止的命令，字节码程序的非终止性，一个（约束）逻辑程序。 此外，我们表明，我们的非终止性测试有效地帮助终止测试，通过避免昂贵的搜索那些部分的代码的终止证明，这种证明不存在。关键词：Java，Java字节码，静态分析，终止，非终止1介绍Java字节码[8]是Java和其他编程语言编译的结果。它是一种低级的、面向对象的、类型安全的语言，以独立于机器的格式分发，因此可以在不同的体系结构上执行。它是编译必须从网络下载到客户端计算机或移动电话中的应用程序的首选目标。近期1电子邮件地址：epayet@univ-reunion.fr2电子邮件：fausto. univr.it1571-0661 © 2009 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.11.01684- 是的Payet，F.Spoto/Electronic Notes in Theoretical Computer Science 253（2009）Google的Android系统[1]使用Java字节码作为Android程序的编译目标，然后将其转换为以机器为中心的低级字节码。由于Java字节码的广泛使用，研究越来越多地集中在检查，以自动的方式，Java字节码应用程序是无害的。这包括证明，例如，他们没有过度使用系统的资源。这样的资源之一就是时间。特别是，Java字节码程序的终止性证明保证它们实际上会终止。这样的证明对于软件开发者来说是重要的，因为它们支持他的产品的质量标准然而，计算机程序的终止性是一个不可判定的属性，许多方法的终止性仍然没有得到证明，因此这些方法可能是潜在的非终止性。一个直接的证明其非终止性变得可取，因为它展示了一个实际的，典型的意外行为的程序，往往意味着非终止性的方法包含一个错误。目前，还没有系统来证明Java字节码方法的非终止性，因为研究主要集中在逻辑程序的非终止性证明[4，11，10，2，16，15]和项重写系统[21，5，24，22，23，9]。在最近的论文[7]中，作者考虑了C程序的非终止性，并[6，14]提供了一些测试C程序的技术，这些技术可以检测程序崩溃，断言违反和非终止性等错误在[20]中，介绍了一种自动检查命令式程序的非终止性的方法;它基于生成用于证明某些潜在循环永远不会退出的不变量;该技术在一组用Java片段编写的程序上进行了实验，并且没有考虑堆数据结构。在本文中，我们提供了一个例子，我们的方法成功地证明了一个程序的非终止性，其中定义了一个数据结构。本文提供了第一个实验与Java字节码程序的非终止性证明的自动推导。我们从我们以前的Julia+BinTerm工具工作开始，用于Java字节码的终止分析[19]。在那里，我们将原始的Java字节码程序P翻译成约束逻辑程序P CLP，其终止需要P的终止。在这里，我们展示了如何，在这些情况下，当近似的字节码是准确的，非终止的P CLP需要的P。因此，我们使用与[ 19 ]中相同的工具来证明Java字节码程序的非终止性，这是通过利用逻辑程序的非终止性分析[10]的先前结果来实现的;即，我们证明了P CLP的非终止性，因此在可能的情况下推断出P的非终止性。虽然这些结果远不是Java字节码程序的非终止性分析问题的一个明确的解决方案，但它们代表了朝着这个方向迈出的第一步，并突出了当前方法的弱点，如果非终止性分析必须应用于真正的Java和Java字节码软件，那么必须解决这些弱点请注意，虽然在[7]中考虑了C的存在非终止性概念，但我们在这里考虑了从Java字节码程序派生的CLP程序的通用非终止性概念本文还表明，我们的非终止性测试有效地帮助了[19]中定义的终止性测试也就是说，我们使用我们的非终止性测试来向- 是的Payet，F.Spoto/Electronic Notes in Theoretical Computer Science 253（2009）85在[19]中，终止证明人指出，PCLP中的某些条款是不同的，因此为它们寻找（通常是昂贵的）终止证明是无用的请注意，这种技术适用于所有Java字节码程序，也适用于字节码的近似不精确或所有方法实际终止的情况。我们的终止测试是适用于，事实上，CLP程序，其条款可能不会终止，因为从P到PCLP抽象诱导的近似。2Java字节码编译成约束逻辑程序Java字节码是一种低级的面向对象的类型安全语言。 其静态分析复杂的是，它没有明确的结构，不同于高，它使用一个临时变量堆栈。因此，变量的数量和类型在同一方法中的不同程序点上是不同的。我们最近开发了一个Java字节码程序（以及Java程序）的静态分析，它证明了程序的大多数方法的终止性[19]。这个想法是，Java字节码程序首先被翻译成它的通过使用不同的抽象分析域，应用基本块和基于这些块上的指称语义的抽象解释[3]。后者提供了对程序所使用的数字或数据结构的数值和结构约束的保守近似：第一个域，用于共享[13]，确定绑定到程序变量的数据结构何时可以共享堆上的位置，以便一个变量的更新也可能影响其他变量。这个信息在第二个域中被利用，用于循环性[12]，它确定绑定到程序变量的数据结构何时可能包含位置循环，因此该数据结构上的迭代可能不一定终止。然后，这两种信息都用于路径长度域[17，19]，该域计算字节码中每个指令执行之前和之后程序变量大小之间的关系：绑定到数据结构的变量的大小或路径长度是可以从该变量跟随的指针的最大长度;绑定到数组的变量的路径长度是数组的长度;数值变量的路径长度是它的值;布尔变量的路径长度是0表示false，1表示true。路径长度的结果最终用于表示程序的每个基本块的开始和结束处的变量大小之间的关系。这是根据线性约束上的约束逻辑程序PCLP来编写的，其谓词b（vars）对应于P的每个基本块b，并且vars是b执行开始时的变量。这些近似建立约束，稍后用于推导程序中变量值的界限，这对于终止和非终止分析的工作至关重要。文[19]证明了主要结果。 终止分析如下：定理2.1设P是Java字节码程序，b是P的基本块. 如果86- 是的Payet，F.Spoto/Electronic Notes in Theoretical Computer Science 253（2009）查询b（vars）在P CLP中只有终止计算，对于vars的所有固定整数值，则Java虚拟机的 所 有 执 行 都在b终止。Q然而，相反的情况一般不成立：我们可以找到程序P和P的基本块b，使得在翻译PCLP中，谓词b（vars）对于vars的某些固定的初始整数值不终止，尽管从b开始的P的所有执行都终止。 这是由于在将P转换为P CLP的过程中所做的近似：共享和循环分析都是近似的，因此，例如，分析者可能不一定证明非循环列表实际上是非循环的。此外，一些字节码具有固有的非线性行为，例如乘法和除法，因此不能通过使用可用于路径长度的线性约束来近似。从Java或Java字节码到CLP的转换使其统一了对任何类型循环的处理：for、while循环、递归、具有取决于数值、引用或布尔变量的退出条件的循环、退出break语句的循环，所有这些都成为P CLP块图中的循环。因此，P CLP的终止可以以统一的方式建立，也可以在if语句内赋值的布尔变量存在的情况下建立，从而使循环退出。关于程序PCLP的一个重要点是，其终止仅对接地输入有意义，其中所有变量都已绑定到其整数路径长度（定理2.1）。此外，PCLP的分句是二元的，即它们具有形式p（X）<$c，q（Y），在形式ht上只有一个谓词。F. Mesnard，它在PCLP中的大多数循环的迭代中找到递减的度量。该工具的计算成本通过减少PCLP中的子句的数量而降低：即，仅考虑循环中的子句，因为它们对应于原始程序P中的循环或递归，并且是确定程序的终止或非终止的那些子句此外，它的成本也减少了减少的谓词的arity，当很明显，删除的参数是无关的谓词的终止。这些优化在[18]中被定义并证明是正确的。因此，在我们所有的例子中，CLP程序将只表达程序循环的路径长度关系。虽然定理2.1的逆命题一般不成立，但在许多情况下，原始程序P到路径长度的近似是精确的，在这个意义上，P CLP程序表示的所有表示都是表示P的真实、具体执行的实际表示。例如，这是处理整数值的指令的近似值的情况，乘法和除法的无表例外;以及处理已被循环性分析成功证明为非循环的数据结构的指令的情况。 在这些常见的情况下，CLP程序的非终止性证明会导致原始Java字节码程序的非终止性证明。在下文中，我们将讨论如何构造CLP程序的非终止性证明，并讨论在许多情况下我们可以得出结论（或不）原始Java字节码程序也不会终止。- 是的Payet，F.Spoto/Electronic Notes in Theoretical Computer Science 253（2009）87⟨|∃⟩⟨|∃⟩⊆⟨|∃⟩⟨|∃⟩X|我的宝贝←3约束逻辑程序的非终止性证明在[10]中为约束逻辑编程的标准操作语义提供了一个非终止性准则，其中自由变量可能出现在对谓词的调用中。我们在本文中考虑的语义的这个标准的专门化（在对谓词的调用中不允许自由变量）在本节中简要描述。我们考虑路径长度多面体上的约束逻辑程序（CLP（PL））。W elett表示项的序列，X和Y表示不同变量的序列，p和q表示谓词符号，c表示路径长度约束。一个原子有p（t）的形式，其中t的长度等于p的长度。查询具有以下形式p（X|c. 一个小句有形式p（X）<$c，q（Y），其中X和Y是不相交的，并且在c中发生的变量必然在XY 中 发 生 。CLP（PL）计划是一套有限的条款。 我们使用Xboxc作为Xbox1的快捷方式。 . 其中X1， . ，Xn：=Xn.con到序列Xn的概率用ynXnc表示，并且是约束其中Var （c）是在c中发生的变量的集合。集合描述bed通过查询Q：=p（X）|c表示为ySet（Q）;它由所有的原子组成，形式p（v（X1）， . ，v（Xn）），其中X1， . ，Xn：=X∈，v是c的基解。我们说Set（Q）是非终止的 wrt。 CLP（PL）程序P，当对于所有p（v（X1），.，v（Xn））∈ Set（Q），查询X1，.，Xn）|X1= v（X1），.，Xn= v（Xn）是非终止的WRT。P的约束逻辑程序的标准语义。这意味着可以在程序P中为该查询构建无限计算。请注意，我们不考虑P的子句之间的任何优先级，也就是说，我们假设一个谓词与定义该谓词的所有子句的非确定性归结下面的结果为约束逻辑程序提供了简单的非终止条件。定理3.1（[10]）Letp（X∈）c，p（Y）是CLP（PL）p ro-gramP中的一个反行书分句。如果设置（p（Y） ）（c）集合（p（X） ）X<$c）thenSet（p（X<$c）Xc）是非终止wrt。 P.Q定理3.1是指如果由c的所有解赋予Y的值的集合包含在由c的所有解赋予X的值的集合中，则由c的一个解赋予X的值提供一个n-终止基查询。事实上，在tuitively，该约 束条件是该子句的保护，并且Set（p（Y）c）Set（p（X）Xc）意味着该子句的每个输出值都满足该保护。因此，如果一个值满足守卫，那么它就进入子句和相应的输出满足了保护，所以这个输出也可以进入子句，下一个输出满足了保护，依此类推。 注意，定理3.1中蕴涵的逆命题并不总是成立：例如考虑递归子句p（X）← X≥3，p（Y）;我们有Set（n）p（X）|X≥3 <$），即集合（Xp（X）|X≥3 π），是非终止wrt. 尽管Set（Bp（Y）|X ≥ 3 X），即 设置（p（Y）|真值x），不包含在Set（x p（X））中|X≥ 3 μ m）。88- 是的Payet，F.Spoto/Electronic Notes in Theoretical Computer Science 253（2009）⟨|∃⟩⟨|∃⟩ ⊆⟨|∃⟩X定理3.2（[10]）Let q（X）←c，p（Y）e是一个CLP（PL）程序P中的子句，Q是一个查询，使得Set（Q）是非终止的wrt. P. 如果设置（p（Y）|Y|X P.Q定理3.2的推论是，集合（q（X）Xc）中的任意y值q（x）满足子句的保护符，并且相应的输出p（y_c）包含在Set（p（Y_c ））中。（c）。 设定值（p（Y） ）（c）Set（Q）和Set（Q）是非终止wrt。 P，则p（y_n）不终止wrt。 P，soq（xn）d oes也不终止。这些定理提供了一个简单的机制来推断基础非终止查询：首先，使用定理3.1从程序的递归子句中推断出一组非终止查询，然后在定理3.2的帮助下完成这个集合。4Java字节码程序在本节中，我们给出了几个例子，我们可以从CLP程序的非终止性中得出原始程序的非终止性，以及不可能的4.1迭代精确逼近当分析中的Java字节码程序P的路径长度约束的近似是精确的时，PCLP的非终止性的证明也是P的非终止性的证明。精确的形式定义要求字节码具有与其数值抽象完全匹配的具体行为，也就是说，满足字节码的输入/输出抽象的每对状态必须对应于字节码的实际具体行为注意，抽象的正确性必须始终保持相反的情况定义4.1 [精确抽象]让ins是一个字节码指令，形式化为具体JVM状态的输入/输出映射，如[ 19 ]所示，并让insPL是其最佳状态的正确估计，即。a约束输入变量v和输出变量s。 这个近似是精确的当且仅当，对于所有满足ins处的静态信息（局部变量和stac k eleme n ts的numb er和ty pe）的输入状态σ n和输出变量σn，当ver{vn> →pathn t h（σn（v））}{vn> →pathn t h（σn（v））}|=在sPL中，则σ（σ）=σ。Q例如，考虑程序Add1：public classUncategorized {publicstatic void main（String args[]）{intk= 3;inti= 2;i = 0; i = 1; i = 1;<}}对应于Add1的字节码程序的近似是精确的：- 是的Payet，F.Spoto/Electronic Notes in Theoretical Computer Science 253（2009）89Q- --≥ −≥-≥ − −≥ −循环保护涉及添加字节码指令，如[19]中所提供的，其近似值为addPL=Unchanged q（#l，#s−2）<${s<$#s−2+s<$#s−1=s<$#s−2}其中#l和#s是在指令发生的程序点q处的局部变量和堆栈元素的数量;我们区分在执行字节码的开始处的变量v（写为v_i）和在其结束处的变量v（写为v_i）。 对于a bove意味着addd oes不修改任何局部变量，也不修改任何不参与加法的堆栈元素;此外，stack（s#s−2 ）的新顶部持有一个值，该值等于前两个最顶部stackelements（s#s−2和s#s−1）的相加。这个近似是精确的，因为对于每一对满足该字节码处的静态信息和上述近似的输入状态σ和输出状态σ，我们必须使局部变量在σ和σ中具有相同的值，并且σ 的 stack的顶部是σ的stack顶部的最顶部两个值的和，使得这些状态满足ad d q（σ）=σ。相应的CLP（PL）程序Add1CLP为：entry（IL2）<${IL2−OL2 = −1， −IL2 ≥ −4，IL2 ≥ 2}，entry（OL2）谓词条目表示程序循环的入口点;局部变量2实现i，而变量k被删除，因为它与程序的终止无关。这个CLP程序是通过使用引言中引用的抽象解释推导出来的。也就是说，我们已经使用了路径长度抽象分析，其已经导出了约束IL2OL2=1（即，局部变量2，即i，随着循环的迭代而减小）和约束IL2_4、IL2_2，其提供了循环内该变量的可能值的界限.CLP程序终止。根据定理2.1，我们得出结论：Add1也终止如果我们把Add1变成非终止程序：public classUncategorized {publicstatic void main（String args[]）{intk= 3;inti= 2;i<= 0; i = 0;}}我们得到CLP（PL）程序Add2CLP：entry（IL2）<${IL2−OL2 = 1， −IL2 ≥ −2}，entry（OL2）根据定理3.1，它不会终止，因为约束的投影 将其独特的子句添加到IL2上（分别为OL2）是IL22（分别）OL2（1）和我们有设置（输入（OL2）|− OL2 ≥ −1）设置（输入（IL2）|− IL2 ≥ −2μ m）。在这里，我们可以从Add2CLP的非终止性安全地得出Add2的非终止性的结论。我们的技术也能够处理更复杂的情况。比如说，如果我们将程序Add2的非终止循环嵌套到终止循环中，90- 是的Payet，F.Spoto/Electronic Notes in Theoretical Computer Science 253（2009）≥⟨|⟩⟨·· ·|···⟩获取：public classUncategorized {publicstatic void main（String args[]）{intk= 3;for（intj= 0;j 10; j++）

下载后可阅读完整内容，剩余1页未读，立即下载