Kleene代数与Java字节码验证的数据流分析方法

理论计算机科学电子笔记141（2005）221-236www.elsevier.com/locate/entcsKleene代数和字节码验证L-ucjaKot1DexterKozen2康奈尔大学计算机科学系美国纽约州伊萨卡市，邮编：14853-7501摘要大多数程序静态分析的标准方法，如流行的工作列表方法，都是一阶方法，用抽象值归纳地注释程序点。在[6]中，我们介绍了一种基于Kleene代数的二阶方法。在这种方法中，感兴趣的主要对象不是抽象数据值，而是操纵它们的传递函数。这些元素构成一个左手Kleene代数。数据流标记不是通过用抽象值归纳地标记程序来实现的，而是通过计算传递函数矩阵的星形（Kleene闭包）来实现的。在本文中，我们将展示这个通用框架如何应用于Java字节码验证问题。我们展示了如何指定在Java字节码验证中出现的传递函数，以便可以有效地计算Kleene代数操作（连接，组合，星形）。我们还给出了一个混合数据流分析算法，该算法计算控制流图的割集上的矩阵的闭包，从而避免了当图中有圈时数据流信息的重新计算。 当可以找到小割集时，该方法可以潜在地提高标准工作列表算法的性能关键词：Java，字节码，验证，静态分析，抽象解释，Kleene代数1引言数据流分析和抽象解释涉及程序中各个点的执行状态信息的静态推导。通常存在类型或抽象值的半格L，每个描述更大的运行时间值集合。每个指令都有一个或多个相关的传递函数f：L→L，描述了指令如何转换抽象状态。1电子邮件：lucja@cs.cornell.edu2电子邮件：kozen@cs.cornell.edu1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.028222- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）用于数据流分析的工作列表算法是计算具有L元素的控制流图G的节点的最小定点标记的标准方法[5]。从起始节点处的初始信息开始，通过将传输函数应用于节点处的当前数据流信息并更新后继节点直到达到固定点，数据流信息在前向方向上传播工作列表方法的一个缺点是图中的节点可能会被分析多次。例如，如果节点s被标记为l∈L，然后稍后被重新访问并重新标记为lJ> l，则可以再次遍历s运行时间可能与dn一样糟糕，其中n是大小d是半格的深度，尽管在实践中这种最坏情况的界限可能很少达到。因此，工作列表算法仍然是许多实际程序分析任务的流行方法。工作表方法是一个一阶方法，因为主要感兴趣的对象是半格L的元素。文[6]介绍了一种基于Kleene代数的二阶泛函方法。在这种方法中，感兴趣的主要对象不是抽象数据值，而是操纵它们的传递函数这些元素构成一个（左手）Kleene代数.Kleene代数是一个著名的代数结构家族，在计算机科学中有着丰富的理论和许多应用在二阶方法中，最小定点标记不是通过用抽象值对程序进行归纳标记来实现的，而是通过计算传递函数矩阵的星（Kleene闭包）来实现的在本文中，我们将演示如何将这个通用框架应用于字节码验证问题。具体来说，我们主要关注Java。本文的贡献是双重的：（i）我们给出了传递函数的显式指定机制，允许有效地计算Kleene代数运算（连接，组合，星形）（第3节）;（ii）我们提出了一种数据流算法，该算法计算控制流图割集上传递函数矩阵的闭包，从而避免了数据流信息的重新计算（第4节）。当可以找到小割集时，该方法可以潜在地提高标准工作列表算法的性能2背景2.1上半格我们的抽象数据值将形成一个上半格L，其中join +和底部元素。运算+是结合的、交换的和幂等的（x+x=x）.半格的偏序为x≤y惠x+y=y。- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）223元素是半格的最小元素，并且是+. 我们还假设上升链条件（ACC）：没有无限上升，在L.这是确保数据流计算收敛的标准假设。从这个假设可以得出，存在一个最大元素T。直觉上，半格中的较低元素表示更具体的-形成，并且连接操作表示信息的分离例如，在Java类层次结构中，String和StringBuffer的联接是Object，这是它们在层次结构中最小的共同祖先元素T表示类型错误。在实践中，数据流分析计算试图形成没有意义的连接x+y的指示致命类型错误，分析将中止。我们用x+y=T来表示这种情况。元素“”表示“未标记”。例如，工作列表算法中的初始标记是映射w0：V→L，其中V是控制流图的顶点集合，使得w0（s0）是在起始节点s0处可用的初始数据流信息，并且对于所有其他节点u∈V，w0（u）=n。2.2Kleene代数Kle enealgebra（KA）是一个结构（K，+，·，0，1），(i) （K，+，·，0，1）是恒等式环，(ii) ba是最小的x，使得b+xa≤x，并且(iii) a≠b是最小的x，使得b+ax≤x。这里的在本文中，我们使用[6]中的一个较弱的公理化。我们将假定该代数是左分配的，但不一定是右分配的。然而，我们将假设它是右预分配的。也就是说，我们不假定ac+bc=（a+b）c，而仅假定ac+bc≤（a+b）c。此外，我们不会假设上述（iii），而只假设（ii）。这样的代数称为左手Kleene代数。运算+给出关于≤的上确界。可以证明所有的运算都是关于≤单调的。乘法单调性的证明不需要分配性，只需要预分配性。一个重要的事实是，（左手）Kleene代数上的n×n矩阵在适当的定义下再次形成（左手）Kleene代数运营商的建议。我们建议读者参考[7，6]以获得更完整的处理。224- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）2.3半格上的严格单调函数在我们的应用中，我们将传递函数建模为严格单调函数f：L→L，其中L是满足升链条件的上半格。映射f必须满足f（x）=f（y）（1）f（λ）= λ。（二）有特殊的严格单调函数0 = λx。λ1 = λ x.x。f的定义域是domf ={x ∈ L |f（x）/= T}。性质（1）意味着domf在≤下是向下闭的。设K表示L上的严格单调函数族。我们可以在K上强加一个左手Kleene代数结构如下。首先，逐点定义函数加法（f+g）（x）=f（x）+g（x）f ≤ g惠f+g= g。在这个定义下，K构成一个具有最少元素0的上半格K的元素可以用普通的函数组合来组合。算子记为·，f和g的合成记为fg;因此（fg）（x）=g（f（x））。注意x∈domfgi <$x∈domf和f（x）∈domg。函数1是复合的双侧恒等式，0是双侧恒等式。歼灭者成分分布在左边+，但不一定在右边。然而，由于单调性，它是右次分配的 因此K在运算+，·，0，1下构成一个左幂等元环.元素f被定义为在输入x上给出最小值的函数。使得x+f（y）≤y。在符号中，f（x）= μy. （x+f（y）≤y），其中μ是通常的最小定点算子。存在最小固定点，因为f是单调的，ACC成立，所以单调序列x，x + f（x），x + f（x + f（x）），.在有限步后收敛，但不一定在x中一致有界;一个反例由N∞{∞}组成的半格给出，其中min作为连接，并且在输入x上的严格单调函数f给出∞，如果x=∞，如果x≥1，则为x−1，如果x= 0，则为0。- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）225定理2.1（[6]）真图（K，+，·，λ，0，1）是一个左手Klene代数.3应用到JavaJava字节码验证算法，如Java虚拟机（JVM）规范[9]所述，是一种工作列表算法。[9]中算法的官方说明是可操作的，但在更数学的处理上有许多尝试[1，2，3，8，10]。在这个应用程序中，L的元素描述了局部变量和操作数堆栈的当前状态，它们包括当前执行方法的堆栈框架L的顶元素T和底元素T是人造的元素，分别表示类型错误和未标记状态每L的其他元素包括(i) 从半格L0到局部变量数组的类型赋值，如下所述，以及(ii) 包含来自L0的值的有界深度操作数堆栈。这些赋值必须满足某些约束，如下所述。半格L0描述了局部变量和操作数栈元素的类型在JVM中，局部变量没有固定的类型，但允许在程序的不同点包含不同的类型半格L0的顶元素Useless表示未初始化或不可用值（不要与L的顶部元素T混淆）。当在两个或多个控制流路径的连接处合并局部变量数组和操作数堆栈的状态时，所得到的状态是由不同路径产生的状态在L中的各国必须满足某些兼容性条件，或者它们不能合并;在这种情况下，L中的联接是T，表示类型错误。例如，堆栈深度必须相同，并且对应堆栈条目的L0中的联接可能不是Useless。然而，相应的局部变量的连接很可能是无用的。L0中的Useless下面是几个不可比较的类型层次结构. 第一个是Java类层次结构，顶部元素Object表示所有引用值，包括接口和数组。Object下面的数组类型由维度和组件类型信息组成。 有一个最小的引用类型，表示空引用。类型是所有其他引用类型的子类型在Useless的正下方还有Int、Float、Long和Double类型。类型Int表示Java基本类型int、byte、char、short和226- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）布尔值。 在JVM中，所有这些值都表示为整数。最后，有一个不可比的类型层次结构的集合，代表Java try-catch-finally结构实现中使用的嵌入式jsr子例程的返回地址众所周知，这些子程序会导致字节码验证的特殊问题[2，3，8，10]。考虑到jsr/ret引入的额外复杂性的程度，并且考虑到它们是Java特有的特性，而不是一般的字节码，我们选择在本文中放弃它们的处理对于p，q∈L，连接p+q被定义为：• p和q的当前堆叠深度相同，• 定义了p和q中相应局部变量数组元素在L0中的连接，• p和q中相应栈元素在L0中的连接被定义，并且不是无用的。如果p+q被定义，它的值是通过将p和q中相应的局部变量数组元素在L0中连接起来，并与p和q中的栈相同。如果p+q是未知的，我们取p+q=T。3.1传递函数传递函数f：L→L可以根据其前提条件和影响来指定。前提条件是一组指定f的域的约束，而结果描述f如何改变抽象状态。前提条件和结果可以用三元组编码P=（oldD，oldS，olddL）E= （ newD ， newS ，newL），其中：• oldS是断言α≤t的数组，其中α是一个变量，t∈L0，或者只是一个无约束变量α。每个α在oldS中至多出现一次。这些指定的抽象值预计将占据在执行之前的堆栈，并构成类型安全执行的先决条件例如，iadd（整数加法）指令将具有oldS=[α≤Int，β≤Int]，表示该指令期望堆栈顶部有两个整数。astore3指令（在局部变量3中存储引用值）将具有oldS=[α≤Object]，指示指令期望在堆栈顶部的引用值。swap指令将具有oldS=[α，β]，指示指令期望堆栈顶部的任意类型的两个- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）227数组oldS通常不指定整个堆栈，只指定最上面的几个项。我们将oldS的大小表示为|孩子|.• oldD是oldS之下堆栈的最大允许深度。这指定了有多少可用的堆栈空间可以在没有堆栈的情况下执行f例如，如果f需要5个空闲堆栈位置，|孩子|是3，那么oldD=maxS− 8，表示最多可能有maxS −8栈中oldS指定的元素下面的其他元素。数量oldD可以是0和maxS之间的任何数，包括0和maxS。• oldL是断言α≤t的数组，其中α是一个变量，t∈L0，或者只是一个无约束变量α，指定了对局部变量的类型约束，这些约束是类型安全执行f所必需的。每个α都发生在在olddL中最多一次，并且oldS和olddL中的变量必须不相交。例如，aload3指令的oldL数组（从局部变量3加载引用类型）将包含局部变量3的α ≤Object。• newS是一个包含类型值和变量的表达式数组，这些变量表示f在堆栈上执行的结果。例如，iadd指令将具有newS =[Int]，指示指令返回一个位于堆栈顶部的整数如果swap指令[1]，故有[1]，故有[2]，故有[3]。如果aload3指令的局部变量3具有α≤Object，则它将具有newS=[α]。我们将newS的大小表示为：|新闻|.• newD是一个与oldD相同或为0的数字。在大多数情况下，它与oldD相同，表示oldS下面的堆栈未被指令修改。一个例外是athrow指令，它在压入异常对象之前清空堆栈。对于这个指令，或者对于任何由其他方式抛出的异常，newD将为0。• newL描述了f对局部变量的显式影响例如，istore2指令的newL数组（整数存储到局部变量2）将指定局部变量2在执行f之后包含α，其中oldS=[α ≤ Int]。等价地，newL的局部变量2也可以包含常数Int，因为Int在L0中是最小的，因此α ≤ Int <$α = Int。此外，newL包含由f不确定的oldL的约束。例如，对于指令aload 3，如果oldL数组指定局部变量3的α ≤ Object，则newL数组将包含局部变量3的α。数组newL和newS可以包含抽象类型和类型变量的符号连接这些性质将适用于所有的传递函数，228- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）字节码指令，我们对连接和组合的定义将保留它们。因此，我们可以期望它们对我们分析中的所有函数都成立。3.2由P，E在本节中，我们将展示一个规范P，E如何唯一地描述一个传递函数f：L→L。f的定义域是p∈L的集合，使得下面的（i）(i) 对于每一个最高的|孩子|p中栈的元素，如果oldS的相应元素是α≤t，则该元素必须小于或等于t。如果oldS的对应元素是变量α，则类型不受约束。(ii) 对于每个局部变量x，如果oldL的第x个元素是α≤t，则p的第x个局部变量必须小于或等于t。如果oldL的第x个元素是变量α，则p的第x个局部变量不受约束。(iii) p处的堆栈深度不大于oldD+|孩子|.最后，我们指定f（p）的值，其中p∈domf。对于每个局部变量x，如果oldL的第x个元素是α≤t或α，则将α与p的第x个元素统一。 类似地，对于oldS的每个元素，如果该元素是α≤t或α，则将α与p的栈的相应元素统一。现在，对于每个局部变量x，计算newL的第x个元素，它是一个符号在这种替换下，L0中变量和常数的连接这将是f（p）的局部变量数组的第x个元素类似地获得对应于newS的f（p）的栈的值如果oldD=newD，栈中f（p）处的否则，如果newD= 0，则f（p）处的堆栈内容将只是newS。3.3传递函数在本节中，我们描述了传递函数的具体化的Kleene代数运算。然而，在此之前，我们提出了一个辅助操作，当比较具有不同oldS或newS长度的两个规范时，该操作很有用。3.3.1延长给定一个指定值P，E，使得oldD=newD≥ 1，我们可以通过在oldS和newS上直接在已经表示的元素下添加一个新的无约束变量α，并将oldD和newD减1来延长堆栈由此产生的规格PJ，EJ表示相同- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）229传递函数f作为P，E，具有附加的限制，即栈被约束为具有在oldS和newS之下的至少一个附加元素。在oldD≥1但newD= 0的情况下，例如使用athrow指令，我们可以通过将新的无约束变量α添加到oldS，直接在已经表示的元素下，并递减，老D 1结果指定PJ，EJ表示与P，E相同的传递函数f，但增加了一个限制，即oldS必须至少比以前多一个元素。3.3.2加入给定分别定义传递函数f和g的规范Pf，Ef和Pg，Eg，我们希望定义Pf+ g和Ef+g。直觉上，我们希望Pf+ g是暗示Pf和Pg的最弱约束集，并且我们希望Ef+ g是Ef和Eg的连接。Pf和Pg对堆栈深度的约束不能太强，以免阻止堆栈的合并。因此，必须保持以下所有属性：旧Df+|旧Sf| ≥|旧Sg|旧Dg+|旧Sg| ≥|旧Sf|新Df+|新Sf| ≥|新Sg|新Dg+|新Sg| ≥|新Sf|.冷杉，如果|旧Sf|=/|旧Sg|，say|旧Sf|<|旧Sg|，如第3.3.1节中所述，我们将旧的Sf放大，直到它们具有相同的长度。如果这是不可能的，因为oldDf= 0，这是一个类型错误。因此，我们可以不损失一般性地假设，|旧Sf|=的|旧Sg|.为了定义Pf+g，我们首先设置oldDdefoldD ，oldD）。f+g= min（fg这将oldDf+g设置为由oldDf施加的两个约束中较严格的一个，并且旧湾数组oldSf+g的内容是暗示oldSf和oldSg施加的约束的最弱约束。要在oldSf+g中定义元素i，从栈顶开始查找oldSf和oldSg中相应的元素称这些项为if和ig。在oldSf+g中元素i的值定义如下。• 如果if，ig中的一个是α≤s，另一个是β≤t且s≤t或仅是β，则旧Sf+g中对应的约束是α≤s，因为它是更严格的统一Pf，Ef，Pg，Eg中的α和β。230- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）F• 如果if是α，ig是β，则统一Pf，Ef，Pg，Eg中的两个变量。旧Sf+g的对应元素为α。• 如果if是α≤s且ig是β≤t，其中s≤t也不是t≤s，则它是一个类型错误。我们从oldLf和oldLg类似地定义oldLf+g。如果两个数组中的变量都是受约束的，比如s和t，且s≤t，则将两个变量统一在Pf，Ef，Pg，Eg中，并在oldLf+g中用s约束它。如果其中元素是无约束的，取另一个约束，统一两个变量。对于Ef+g，我们使用了|newSf|=的|新Sg|否则，这是一个错误。设置newDdef01 - 02 -2013刘晓波（新Df，newDg）。这背后的直觉与oldDf+g相同。定义newLf+g为newLf和newLg的并。 也就是说，为了获得newLf+g中的特定元素，取newLf和newLg中对应元素在L0中的连接。如果需要的话，可以使用结合性、交换性和恒等式来简化得到的表达式。如果此过程中两个类型值的任何联接都是Useless，则不是类型错误。类似地，定义newSf+g为newSf和newSg的连接，除了a无用值是类型错误。3.3.3组合物假设我们给出传递函数f和g的具体值Pf，Pg，Ef，Eg。我们希望定义Pfg和Efg。要使组成合法，必须满足以下条件：新Df+|新Sf| ≥|旧Sg|旧Dg+|旧Sg| ≥|新Sf|.If|新Sf||，我们将首先介 绍|, wefirstlengthentheshorteroneasdescribedin第3.3.1节。如果因为oldDg或newDf中的一个为0而不可能，则这是一个类型错误。 这样我们就可以在没有损失的情况下，|新Sf|=的|.|.首先，我们定义oldDfg。有两种情况，取决于f：⎧oldDdefmin（newDf，oldDg），如果oldDf=newDffg=oldD，否则，请执行以下操作。为了构造oldLfg，我们从oldLf开始，并按如下方式修改它。如果newLf的局部变量x包含类型为constant的表达式es∈L0和一个或多个类型变量，并且如果oldLg的局部变量x是- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）231defformα≤t，我们必须有s≤t，否则这是一个类型错误。直觉上，f在该位置产生的类型至少可以是s，因此g不能对该元素施加更强的约束。此外，对于e中的所有变量β，如果约束β≤u出现在oldLf或oldSf中且t≤u，或者如果β在oldLf或oldSf中出现无约束，则将约束β≤u或β在oldLf或oldSf中的无约束出现替换为β≤t。直觉上，由oldLg施加的较强约束β≤t通过f向后传播。如果u≤t，我们不改变约束β≤u。如果u不≤t，t也不≤u，则是类型错误。当对所有局部变量x都这样做时，得到的数组为奥尔德尔湾类似的构造适用于oldSfg。我们从老F开始。如果newSf的任何元素是一个表达式e，其类型常数s∈L0和一个或多个类型变量，并且如果oldSg的相应元素具有形式α≤t，则我们必须有s≤t，否则它是一个类型错误。此外，如上所述，对于e中的所有变量β，如果需要，我们通过f向后传播约束β≤t定义Efg如下。同样，newDfg有两种情况，取决于f：newD⎧defmin（newDf，oldDg），如果oldDg=newDgfg=新D，g否则。我们计算newLfg和newSfg如下。分别从newLg和newSg对于oldLg中每个α或α≤t的局部变量，将α与newLf中相应位置的表达式统一起来，并应用如果需要的话，这个替换为newLg和newSg，评估和简化类似地，对于oldSg中的每个堆栈条目α或α≤t，将α与newSf中相应位置的表达式统一起来，并应用如果需要的话，对newLg和newSg进行这种替换，进行评估和简化如果Useless出现在newSg中表达式的求值中，则表示类型错误。生成的数组分别为newLfg和newSfg3.3.4身份def恒等函数1 =λp.p由下式指定：P1，E1=（maxS，[]，A），其中[]表示空堆栈，A是maxL个不同的未约束变量的数组232- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）3.3.5明星给定一个传递函数f的指定值P，E，f的指定值可以通过取f的许多有限次幂的并来计算。为了不造成类似的错误，我们最好|旧Sf|=的|newSf|：if|old|新S>| 新 Sf| ， 则 f 的 S o m e o w r 将 在 下 面 的 对 话 框 中 产 生 。 |, th ensomepoweroffwillresultinastackunderflow.需要将p个wersf k的连接进行到k=|旧Sf|这是在旧Sf或旧L f中的任何变量或常数应用传播到新S f或新L f中的新xpr esion所 需 的 步 数 的上 限。Thusf=（1+f）k，其中k=|旧Sf|+最大L，其中，通过保留可实现压缩以logk步进行平方例3.1考虑Java片段如果（b）x = y+1;否则x =z;(i) 赋值x = z可能被编译为字节码序列iload 5iStore 3其中局部变量x和z分别占据局部变量数组中的位置3和5指令iload5<在oldL中有局部变量5的α int（或者只是int，因为α≤int意味着α=int），oldS=[]，oldD = maxS− 1，表明至少有一个空闲堆栈位置。iload5的结果有newS =[int]，表明一个int已经被压入栈中，int在newL的位置5。istore3指令有oldS =[int]和newS =[]，oldD =maxS− 1，并且在newL的位置3有int。 这两条指令的组成是：对于oldL中的局部变量5，int;对于newL中的局部变量3和5，oldS = newS =[]，oldD = newD = maxS − 1。(ii) 赋值x = y+1可能被编译为字节码序列iload 4iconst 1iaddistore 3其中局部变量y占据局部变量数组中的位置4这四条指令的组成是int，对 于 oldL 中 的 局 部 变 量 4 ， 对 于 newL 中 的 局 部 变 量 3 和 4 ，oldS=newS=[]，oldD=newD=maxS- 2，因为序列需要两个空闲堆栈位置。- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）233(iii) 整个条件语句将涉及计算（i）和（ii）中两个字节码序列的和这两个序列对于oldL中的局部变量4和5，以及newL中的局部变量3、4和5，oldS=newS=[]，oldD=newD=maxS− 2。4的算法在本节中，我们提出了一个混合算法的数据流分析，可以提供一个改进的性能在标准的工作列表算法时，可以找到一个小割集。该算法利用了在如上定义的传递函数上计算Kleene代数运算我们给出一个有n条指令的程序，我们希望用半格的元素来标记程序的底层控制流程图GL.设E是n×n矩阵，其行和列由G的顶点索引，使得如果（s，t）是G的一条边，则E[s，t]是标记边（s，t）的传递函数，如果（s，t）不是G的一条边，则E[s，t]= 0.这个矩阵很容易在一个单一的通过程序构造。回想2.2节，左手Kleene代数上的n×n矩阵因此，我们可以说矩阵E。 中间E[u，v]是传递的组成的连接沿着从u到v的所有路径运行。 如果我们能计算E，那么我们可以通过估计E∈[s0，u]（l0），得到G中任意节点u上所需的定点数据流标号，其中l0∈L是该节点s0的初始标号.标签l0由一个空堆栈组成，方法（包括对象本身，如果它是一个实例方法）在前几个局部变量中，对于其余的局部变量无用。 由其在元素l∈L上的指定P，E给出的传递函数的值可以通过将oldS和oldL中的变量与l中的相应值统一来计算，检查oldS和oldL中的所有约束α ≤ t是否满足，然后在此替换下评估newS和newL中的表达式。在[6]中显示，该方法的抽象版本和标准工作列表算法在所有类型正确的程序上产生相同的定点标记4.1小割集我们不直接计算E，因为它太大了。相反，我们提出了以下混合方法，该方法将上述思想与工作列表算法结合使用，以避免重新计算数据流信息。设M是G中的割集（也称为反馈点集），即G的每个有向圈至少包含一个节点的节点234- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）⎣∗∗inM.我们还将起始节点s0包含在M中，即使s0可能不是一个割点。设m =|M|.寻找最小割集是NP-完全的，但对于可约图来说是多项式时间可解的[4]。流程图从Java源代码编译的字节码程序通常是可约的。在实践中，简单地将M作为后边缘的所有目标的集合应该给出非常小的割集。设A、B、C和D为M×M、M×（V-M）、（V-M）×M，E的（V-M）×（V-M）个子矩阵分别为：⎡ ⎤A BE=100。C Ddef设F A+定义=(see[6]），BD C和G=D+CAB. 左手Kleene代数⎡ ⎤FFBD∗ ⎣ ⎦E=吉尔卡.（三）GM是割集的事实在代数上由性质Dn−m= 0反映。 这是因为Dn−m描述了长度为n-m到V-M;但根据鸽子洞原理，任何这样的路径都有一个重复的节点，因此将包含一个必须与M相交的圈。因此，不可能存在这样的道路可以证明，如果P和Q是矩阵，使得对于所有i，j，不是Pij和Qij都是非零的，则P和Q满足关于任何其他矩阵R的右分配性;即，（P+Q）R=PR+QR。这适用于I和D，因为I只有对角线上的非零元素，而D只有零元素今天，其他人都认为这是一个错误。 我不明白（I+D）k=kDi.从这个事实和左手Kleene公理i=0时代数，我们有D=（I+D）n−m−1因此，F = A + BD<$C = A + B（I + D）n−m−1C。m×m矩阵F描述了从一个割点到另一个割点的不经过中间割点的路径的标号由于V-M上的子图是非循环的，所以F可以使用传统的工作列表算法从每个割点开始在时间O（mn在每个这样的计算中，V-M的每个顶点最多被访问一次。或者，我们可以对子图进行拓扑排序，并按排序顺序计算组合作为这种计算的副产品，我们还获得了矩阵defHn−m−1= BD=B（I+D），它描述了从一个割点到一个非割点的路径的标签，- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）235000 0 00而不是通过任何其他切入点。现在我们需要计算F的星，但这个矩阵通常比E小得多。我们可以通过使用矩阵的星的递归定义的分治方法来做到这一点（3）。时间复杂度为O（m3）。现在，为了实现最终的数据流标记，我们观察到第s行是传递函数F_n[s0，u]的向量，对于u中的任意一个，当将其应用于l0时，产生u的最终数据流标记。类似地，FH的s流是针对非割点v的传递函数FH[s0，v]的向量，当应用于l0时，产生v. 对函数F[s0，u]（l0）的计算可以在一段时间内完成，或者O（m）在所有。一旦我们有了这个值向量，我们就可以计算FH[s，v]（l） =FH[u，v]（F[s，u]（l）），u∈ M时间复杂度为O（m），也就是O（nm）。4.2复杂性该算法的最坏情况复杂度为O（nm+m3）。与工作表算法的最坏情况复杂度O（nd）（d为半格L的深度）相比，当m较小时，我们的算法可以得到改进二阶方法的另一个优点是它易于并行化。工作表方法本质上是顺序的，因为传递函数的每个应用都需要知道其输入，而组合可以在不知道其输入的情况下计算这些问题有待于今后的调查。确认感谢Stephen Chong、Andrew Myers和Radu Rugina提供的宝贵讨论。这项工作得到了NSF资助CCR-0105586和ONR资助N 00014 -01-1-0968的部分支持。本文所载的观点和结论是作者的观点和结论，不应被解释为必然代表这些组织或美国政府的官方政策或认可，无论是明示还是暗示。236- 是的Kot，D.Kozen/Electronic Notes in Theoretical Computer Science 141（2005）引用[1] Abadi，M.和R. Stata，Java字节码子例程的类型系统，在：Proc.25th Symp。《程序设计语言原理》，ACM SIGPLAN/SIGACT，1998年。149比160[2] Coglio，A.，Java字节码子程序的简单验证技术，并发和计算：实践和经验16（2004），pp。647-670[3] Freund ， S.N. 和 j.C. Mitchell ， A type system for the Java bytecode language and verifier，J. Automated Reasoning30（2003），pp.271-321.[4] Garey，M.R. 和D.S. 约翰逊，NP-完整性，弗里曼1979年[5] Kildall，G.一、 A unified approach to global program optimization，in：Proc. Conf. 程序设计语言原理（POPL'73），ACM，1973年，pp。194-206.[6] Kot，L-。和D. 王文，张文，张文，等.计算机科学与工程.北京：清华大学出版社，2004.URLhttp://www.cs.cornell.edu/kozen/papers/KADataflow.pdf[7] Kozen，D.，Kleene代数和正则事件代数的完备性定理。的Comput。110（1994），pp. 366-390.URLhttp://www.cs.cornell.edu/kozen/papers/ka.ps[8] Leroy，X.，Java字节码验证：概述，在：G。贝里，H。Comon和A. Finkel，editors，Proc.Conference on Computer Aided Verification （ CAV 2001 ） ， Lect. Notes in ComputerScience2102（2001），pp.265-285[9] Lindholm，T.和F.Yellin，[10] 钱 志 ， Java 字 节 码 验 证 的 标 准 定 点 迭 代 ， Transactions on Programming Languages andSystems22（2000），pp.638-672.