理论计算机科学电子笔记：部分求值的应用和优化技术

理论计算机科学电子笔记190（2007）85-101www.elsevier.com/locate/entcs用部分求值MiguelG'omez-Zamalloa1ElviraAlbert1Germ'anPuebla21DSIC，CompluttenseUniversityofMadrid，{mzamalloa，elvira}@ fdi.ucm.es2马德里技术大学，fi.upm.es摘要编译的解释性方法允许通过部分地评估解释器来w.r.t.源程序。 这种方法虽然在原则上很有吸引力，但在实践中并没有得到广泛应用，主要是因为很难找到一种总是获得“质量”编译程序的部分评估策略。尽管如此，在最近的工作中，我们已经进行了概念证明，至少对于一些例子，这种方法可以应用于将Java字节码反编译为Prolog。这允许应用现有的高级工具来分析逻辑程序，以验证Java字节码。然而，成功的部分评估的解释器（一个现实的子集）Java字节码是一个相当具有挑战性的问题。这项工作的目的是提高性能的反编译过程在两个方面。首先，我们希望获得高质量的反编译程序，即，简单而小巧。我们称之为反编译的效率。 其次，我们希望反编译过程在时间和内存使用方面尽可能高效，以便在实践中扩展。 我们称之为反编译的效率。有了这个目标，我们提出了一些技术，以改善部分评估策略。我们认为，我们的实验结果表明，我们能够显着提高反编译过程的效率和有效性。保留字：Java字节码，反编译，部分求值1介绍部分求值[12]是一种基于语义的程序转换技术，其主要目的是通过将程序进行特殊化来优化程序。部分输入（静态数据）-因此它也被称为程序专门化。本质上，给定一个程序P和一个静态数据s，部分求值器返回一个剩余程序Ps，它是Pw.r.t.的一个特殊版本静态数据s使得对于所有动态（即，非静态）数据d.部分评估技术[12]的发展导致了所谓的“解释性方法”的编制，也被称为第一个在这种方法中，从源语言LS到目标语言LO的源程序P的编译原则上可以通过专门化以LOw.r. t编写的用于LS的解释器Int来P. 的1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.06286M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）85SS这样获得的程序IntP可以类似于使用编译器CompO从LS到LO直接编译P的结果CompO（P）。当LS是Java字节码，LO是Prolog时，我们理论上得到了获得Java字节码的高级逻辑表示的动机是明确的：我们可以将为高级语言开发的高级工具应用于结果程序，而不必处理字节码的复杂的非结构化控制流程，堆栈的使用，异常处理及其面向对象的特性等。特别是，对于逻辑编程，我们有可用的通用分析工具，这些工具是增量的[10]和模块化的[4]，我们将能够直接使用[1]。使用解释性方法进行反编译而不是实现从Java字节码到LP的编译器的动机包括：1）可扩展性，在这个意义上，它很容易修改解释器，以观察新的利益属性，2）容易信任，在这个意义上，它是相当困难的证明（或信任）编译器保留程序语义，并且，显式地指定所使用的语义是什么也是复杂的，3）更容易维护，JVM语义中的新变化可以很容易地在解释器中反映出来，4）更容易实现，只要有一个强大的LP部分求值器就可以了。解释性方法的成功高度依赖于消除解析程序、获取指令等的开销从而获得类似于由传统编译器获得的程序的程序 当LS和LO语言都相同时，完全摆脱解释层被称为“琼斯最优性”[11，12]，并且直观地意味着将解释器Int特殊化为程序P的结果应该基本上与P相同，即，IntP P. 专业化解释器已经是多年来的研究主题，特别是在逻辑编程社区中（参见，例如，[22，23，15]和他们的参考）。然而，尽管有这些努力，以系统的方式实现琼斯最优性并不简单，因为给定一个程序P，可以获得无限数量的剩余程序IntP，其中只有一小部分类似于直接编译的结果。因此，迄今为止只取得了部分成功，例如在简单Vanilla解释器的专门化中，用调试器扩展的同一解释器和lambda解释器[15]。实现有效反编译的第一个要求是拥有一个足够强大（或部分求值术语中的“积极”）的部分求值器，以便从剩余程序中消除解释级别的开销。 从某种意义上说，[1]中的工作表明，我们的部分求值器[20，2]足够激进，可以用于解释方法。接下来的两个问题，我们需要回答，这是在这项工作中解决的是：是控制策略使用过于积极在某些情况下？如果是这样的话，有可能解决这个问题吗？请注意，过于激进的策略的后果可能是相当消极的：它可能会在反编译过程中引入非终止性，即使过程终止，也可能导致无效的反编译（在时间和内存方面）和不必要的大型剩余程序。应当注意M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）8587n类课堂阅读器1类jvml程序....类文件图1.一、无注释在线PE反编译Java字节码为Prolog反编译过程的存储器效率是非常重要的，因为可能发生由于部分求值器耗尽存储器而导致反编译器无法生成剩余程序的情况2反编译过程图1显示了最初在[1]中提出并在本文中遵循的解释性反编译过程的概述。 首先，给定一组.class文件{class1，.. . ，classn}，一个名为class reader的程序，返回[3]《易经》云：“君子之道，焉可诬也？”我们使用稍微修改过的JVM语言，其中一些字节码指令被分解，并包含一些其他的小简化（参见[1]）。然后，我们有一个用Ciao编写的JVML解释器，它捕获JVM语义。反编译过程包括专门化JVML解释器w.r.t.类的LP表示。在这项工作中，我们将通过引入两个新元素（出现在图中的虚线框中）来改进反编译：部分求值器中改进的多方差控制和过滤器注释，以细化部分求值器的控制。2.1字节码的LP表示类读取器生成的LP（Ciao）程序包含{class 1，. . ，classn}。它们被表示为一组事实字节码;也是通过将.class文件中可用的所有其他信息（类名、方法和字段签名等）放在一起而获得的单个事实类每个字节码事实都是字节码（PC，MethodID，Class，Inst，Size）的形式，其中Class和MethodID分别标识指令Inst所属的类和PC对应于程序计数器，Size对应于指令的字节数，以便能够计算程序计数器的下一个值。事实类的形式与本文无关，但可以在[1]中观察到示例2.1[LP表示]我们的运行示例由单个Java类LinearSearch组成，如图2所示。在右边，我们显示了与用数字“0”标识的方法搜索相对应的字节码剩余程序jvml（LP）过滤器部分求值器多花的控制88M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）85class LinearSearch{public int findDuplicate（int[]nums）{ int size=nums.length;int i=0; inti= 0;while（（i size））（！））{if（xs[i]==x）found =true;else i++;}返回i;}bytecode（0，'0 '，1，aload（0），1）. bytecode（1，'0 '，1，arraylength，1）. bytecode（2，'0'，1，istore（2），1）. bytecode（3，'0'，1，const（（int i，int j）. bytecode（4，'0 '，1，istore（3），1）. bytecode（5，'0 '，1，const（（int i，int j）. bytecode（6，'0'，1，istore（4），2）.bytecode（8，'0 '，1，iload（4），2）.bytecode（10，'0 '，1，iload（2），1）.bytecode（11，'0 '，1，if_icmp（geInt，26），3）.bytecode（14，'0 '，1，iload（3），1）.bytecode（15，'0 '，1，if0（neInt，22），3）.bytecode（18，'0 '，1，aload（0），1）.bytecode（19，'0 '，1，iload（4），2）.bytecode（21，'0'，1，iaload，1）.bytecode（22，'0 '，1，iload（1），1）.bytecode（23，'0 '，1，if_icmp（neInt，8），3）. 2016- 05 - 13 01：01：02（（int i，int j）. bytecode（27，'0'，1，istore（3），1）.bytecode（28，'0 '，1，goto（-20，3）.bytecode（31，'0 '，1，iinc（4，1），3）.bytecode（34，'0 '，1，goto（-26，3）.bytecode（37，'0 '，1，iload（4），2）.bytecode（39，'0 '，1，irereturn，1）.图二. 运行示例的Java代码和LP类号“1”的（第三个标记为0到6的字节码（第一个参数）对应于Java程序中的前三个初始化指令。然后，如果while条件中的第一个合取不成立（字节码8-11），PC将向下移动26个位置（即，字节码37）。否则，检查第二个合取，并且类似地，PC可以在22个位置中增加字节码37）。if指令中的条件对应于字节码18-23，then分支到26-28，else分支到31-34。最后，字节码37-39代表回归。2.2JVML解释器JVML解释器遵循Bicolano [19]中的正式规范，在Ciao在我们的规范中，状态由st（Heap，Frame，StackFrame）形式的项建模每个帧的形式为fr（Method，PC，OperandStack，LocalV ar），包含操作数堆栈OperandStack和局部变量LocalV在方法的程序点PC处。注意，每当我们处于异常状态时，状态和帧将相应地分别表示为stE和frE项，使用与其同源st和fr相同的参数，除了OperandStack将是引用堆中相应异常对象的位置号（而不是列表）。图3显示了CiaoJVML解释器的一个片段。 给定程序和当前状态，其主谓词execute first调用谓词step，后者在执行相应的字节码后产生状态。该过程迭代M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）8589execute（Program，State，FinalState）：-step（_，Program，State，NextState），execute（Program，NextState，FinalState）.execute（_P，State，State）：-check_return（State）.execute（Program，State，NextState）：-State=stE（Heap，frE（Method，PC，Loc，_），[]），NextState=st（Heap，fr（Method，PC，[ref（Loc）]，_），[]），not_handled_exception（Program，State）.check_return（st（_H，fr（Method，PC，_Stack，_L），[]））：-parametionAt（Method，PC，return）.check_return（st（_H，fr（Method，PC，[num（int（_I）|_Stack]，_L），[]））：-parallelationAt（Method，PC，irereturn）.check_return（st（_H，fr（方法，PC，[ref（loc（_I）|_Stack]，_L），[]））：-reconstitutionAt（Method，PC，areturn）.step（goto_step_ok，_P，st（H，fr（M，PC，S，L），SF），st（H，fr（M，PCb，S，L），SF））：-predictionAt（M，PC，goto（O）），PCb= PC+O。...图三. JVML解释器的片段通过递归调用，谓词执行新的状态，直到以下条件之一成立：1）我们到达返回指令（即return、irereturn或areturn），JVM调用栈为空，2）我们处于异常状态，没有找到合适的异常处理程序，JVM调用栈为空，3）在当前PC上没有字节码指令。对于一个有效的字节码程序，后者完整的解释器，以及一系列的例子，可以在www.example.com上找到http://cliplab.org/Systems/jvm-by-pe。3逻辑程序在线部分求值基础我们假设熟悉逻辑编程的基本概念[18]。 执行 用于原子A的逻辑程序P包括为P{A}构建所谓的SLD树，然后从该树的每个非失败分支提取计算的答案替换。在线部分评估建立在逻辑程序的执行方法之上，具有两个主要的挑战：• 为了保证展开过程的终止，在构建SLD树时，可以选择不进一步展开目标，而是在树中留下具有非空、可能非失败的目标的叶子。生成的SLD称为部分SLD树。请注意，即使所有可能查询的SLD树都是有限的，在部分评估期间要构建的SLD也可能是有限的。其原因是，由于动态值在专门化时是未知的，因此专门化SLD树在运行时可以比实际SLD树拥有更多的分支（特别是无限分支）。从每个预解式中选择哪个原子以及何时停止解折叠由解折叠规则决定。• 部分求值器可能必须构建几个SLD树，以确保叶子中剩下的所有原子都被某棵所谓的抽象运算符对必须部分评估的原子执行当90M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）85输入：一个程序P和一组原子S输出：一组原子T：i：=0;S0：=S重复1.T：=unfold（Si，P）;2.Si+1：= abstract（Si，Tcalls）; 3.i：=i+ 1;直到Si=Si−1（模重命名）返回T：=Si见图4。 部分求值算法如果所有原子都被覆盖，那么就不需要建造更多的树和过程完成。关于抽象运算符的细节在第4节中出现。逻辑程序的联机部分求值的大多数算法的本质（见例如[8]）可以在图4所示的算法中查看，该算法是参数化的w.r.t.展开规则unfold和抽象运算符abstract。它从一个程序P和一组初始原子S开始。在每一次迭代中，局部控制由展开规则执行，展开规则取当前原子集Si和程序，并为Si中的原子构造部分SLD树。 在全局控制中，当树的叶子中的一些调用（在算法中被命名为T调用）没有被适当地覆盖时，操作符抽象将它们添加到新的原子集合中，以适当的“一般化”形式部分地评估，使得确保终止（即，条件Si=Si−1）。因此，基本上，该算法迭代地构造部分SLD树，直到它们的所有叶子被根节点覆盖对Pw.r.t.然后，S可以系统地从所得到的原子集合T中提取出来。结式的概念用于生成与最终原子集T的SLD树的每个根到叶推导相关联的程序规则。特别地，给定P<${A}的一个SLD导子，其中A∈T以B结尾，θ是导子步骤中MGU的合成部分求值被定义为与构造的部分SLD树的导子相关联的结果序列，对于所有P∈ {A}，A∈T。4JVM解释器为了实现有效的反编译，关键要求之一是具有可用的控制策略（即，展开和抽象运算符），这些运算符足够强大，可以消除解释器开销。因此，[1]中的实验是通过使用基于同胚嵌入的“积极”控制策略进行的在局部控制中，我们所说的积极性是指展开规则，只要没有终止问题，它就尽可能长地计算推导。在全局控制中，它表示在尽可能少的情况下泛化而不危及终止的抽象运算符。M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）85914.1一个成功的例子图5中的例子有助于说明在2.2节中JVM解释器的专门化中出现的挑战。专门化过程通过运行第3节的PE算法开始，初始程序P是JVM解释器和以下初始原子：execute（Prog，st（heap（[array（locationArray（_，integer Type（int）），_）]），fr（method LinearSearch.search0，[]，[ref（1），_，0，0，0]），[]），_）其中，让我们注意到，这个初始状态是根据“方法调用规范”构建的（MIS），即，一个高级描述，指定我们要反编译的方法及其参数值。在我们的例子中，我们想反编译一个方法，用于计算任何整数数组和任何值作为参数的线性搜索因此，我们使用LinearSearch.search“intwww.example.com（int[]，int）“作为MIS。在图中，我们描绘了一个SLD树（的简化版本），该树导致我们运行的例子的有效反编译为了只关注相关参数，execute（Program，st（Heap，fr（Method，PC，Stack，LocalVar），CallStack），FinalState）形式的每个原子在图中表示为execute（PC，LocalVar），以仅显示其两个关键参数。实际上，参数Program和Method始终是常量，堆栈不相关，本例中未使用堆。CallStack总是空列表，因为所考虑的方法不调用任何其他方法（也不调用它自己），并且FinalState总是一个新变量。图中的另一个简化是每个箭头涉及应用几个展开步骤。特别地，步骤谓词的执行可以被认为是展开期间的黑盒，在这个意义上，它执行所有操作（即，多个展开步骤）并返回相应的状态。因此，我们可以忽略产生为了展开对步骤的调用，并将每个派生查看为执行、步骤、执行、步骤......的形式的序列。（在图中，我们实际上只显示了一个步骤）。每个步骤操作的主体中的一些语句在涉及到在专门化时未知的数据时可以保留为剩余语句时间展开期间的计算规则能够剩余化未充分实例化的调用，并以安全的方式选择非最左边的原子[2]，特别是执行进一步的调用。4.2基于嵌入的感兴趣的读者可以参考Leuschel92M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）85execute（0，[ref，0，0]）Jstep（.. . ），.Jexecute（1，[ref，0，0]）J.J- -，，_..Jexecute（11，[ref，0，0]）”他说..execute（39，[ref，0，0]）execute（15，[ref，0，0]），o，，z......，，J真Jexecute（23，[ref，0，0]）执行（34，[ref，，，0，1]）执行（28，[ref，，，1，0]），o，，zJ J- -.........，，。∞J_execute（8，[ref，0，0]）execute（8，[ref，0，1]）execute（8，[ref，1，0]）图五. JVM解释器s（s（U+ W）×（U+s（V）表示s（U× （U+ V））。根据上述定义，可以定义以下策略（它们对应于[1]中使用的策略4.2.1本地控制基于同胚嵌入的展开算子，表示为展开算子，允许导出的扩展，直到到达在其覆盖祖先序列中嵌入一些先前原子的原子（参见例如，[20]）。直觉是，在相同的推导中达到更大（或相等）的原子可能会危及终止，因此必须停止计算。此外，为了达到所需的侵略性水平，还需要能够适应精心处理内置谓词，并安全地执行非最左展开[2]。然而，在无限签名的情况下（例如，整数），这种展开规则可能导致非终止计算。对于一个应用程序，可以使用以下格式的数组：execute（8，[ref，0，0]），execute（8，[ref，0，1]），execute（8，[ref，0，2]）. . ，whhichcangrowinitely并且同胚嵌入不会将其标记为潜在危险。结果，通过考虑通常的同胚嵌入关系，图5中的部分SLD的第二分支不被标记为危险的，并且展开不终止。这在图中由∞符号表示为第二分支的延续。一个可能的相对简单的解决方案，以避免这种非终止的展开行为是使用轻微的适应的原始同胚关系，其中任何数嵌入任何其他数-ber，denotednu m。在执行（8，[ref，0，1 ]）的过程中，执行（8，[ref，0，0]）（以及副作用）。对于一个电话来说，M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）8593同胚嵌入关系虽然保证了局部求值过程的终止，但它是一种过于粗糙的近似，并导致过多的精度损失。它被证明不是我们的解释器的专门化的可接受的替代方案，因为在几乎所有情况下，剩余程序包含完整的解释器，即，我们无法消除解释层。4.2.2全局控制同胚嵌入排序也可以在抽象算子抽象矩阵内的全局控制级使用，以便决定何时进行泛化（即，应用最具体的概括），然后继续构建（可能是部分）SLD树基本上，对于每个新原子A，它检查它是否大于（即，它嵌入）集合Si中的任何原子（其包含已经构建的部分树 如果A没有嵌入Si中的任何原子，则将其添加到集合中;否则，通过使用msg操作符将两个原子泛化。在此之前，如果在Siandw中执行（8，[ref，0，0]），要执行（8，[ref，1，0]），请使用所有的内存嵌入关系，没有危险被标记。因此，为了保证在全局控制级别终止，我们还需要修改在有限时签名（数字）。 通过使用修改后的嵌入关系与h_numb_r_s_numm，在引入Si之前，将后者实现为执行（8，[ref，X，0]）。关于PE过程的效率，应该注意的是，基于嵌入的控制策略的使用引入了显著的开销，因为我们需要跟踪祖先（参见，例如，[20]），并对每个原子参数执行昂贵的嵌入检查。5用于反编译的正如我们在前一节中所看到的，在存在无限签名的情况下，比如整数，无论是整数还是整数都不能单独实现有效和高效的反编译。特别是，使用“警告”可能过于咄咄逼人，因为它会导致太长的派生（甚至危及终止），这会阻止质量反编译相比之下，使用“num“显然太保守了，因为它过早地停止了派生，导致丢失了获得高质量反编译程序所必需的信息。在本节中，我们建议使用[9]的部分求值类型，以便为PE过程提供额外的信息，并改进基于上述嵌入顺序使用先前技术所获得的结果。这种附加信息是程序相关的，因此，当我们对重复地部分评估一个程序感兴趣时，计算它是有意义的。这在我们的反编译方法中显然是这样的，因为我们反复地专门化解释器w.r.t.。不同的字节码程序。此信息通过[9]中定义的可选部分求值类型提供。它们将允许我们在体育课上对论点进行有选择的、上下文相关的处理。特别是，区分了以下基本类型94M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）85• dyn：动态的意思。这种类型用于避免过于激进的策略。它表示用户认为，一旦发现w.r.t.的差异，就丢失存储在相应参数中的信息是一个好主意另一个“相似”的原子。请注意，除非此类信息丢失，否则需要增加多元方差，以便使用差异信息的相应值维护单独的调用模式这导致更高的专业化成本和更大的剩余程序。可以标记为动态参数的一个例子是我们运行示例中的Loc• f sig：代表有限签名。从字面上看，这意味着可能出现的函子和常量名称的数量是有限的。因此，对于这种类型的参数，保证终止。考虑这种类型的动机是，它避免了对可能包含数字的参数使用numnum的需要用户可以将此类型用于那些保证只包含有限个数字集的参数。例如，在我们的例子中，参数PC虽然使用数字来表示程序计数器是很自然的，但这是一个关键这是获得本文所述结果所需的观察。• const：constant的意思。引入这种类型的动机只是专业化过程的效率。当然，它应该只应用于我们知道在专门化期间总是被实例化为相同值的参数。它的使用根本不会影响控制策略，但它允许避免在永远不会改变的参数上反复测试嵌入关系例如，这是程序论证的情况。它在整个反编译过程中保持不变。• term：表示期限。 这是最常见的类型，包括所有可能的术语，包括部分实例化的术语。这是默认类型，除非用户显式提供更精确的pe类型。对于包含算术的程序（比如我们的JVM解释器），我们使用的默认嵌入关系是numnum，因为否则不能保证终止为了允许在参数中的任何深度使用上述基本类型，并且允许具有不同函子的析取类型的可能性，我们可以为其声明不同的类型，部分求值类型的概念，pe类型，被定义为[9]与上述基本类型相结合的常规类型[6]让我们解释一下上述pe类型execute的第一个参数是Program，它显然是常数，因为在每个部分求值期间，只有一个固定的程序，并且不需要泛化这个参数。第三个参数是final（输出）State，它在调用之前总是一个变量，因此它可以被赋予类型项。第二个参数中当前State的类型是析取的，我们通过两个规则声明它，每个函子一个。 第一个对应于正常状态st，第二个对应于异常状态stE。最相关的要点是：1）堆和调用栈的类型被声明为dyn，因为我们不介意M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）8595如果需要的话，在反编译方法时的部分计算过程中，所有关于它们的信息。直观地说，这就是说，我们不希望根据堆或调用堆栈的状态生成一个方法的多个反编译版本。相反，正如在标准编译中发生的那样，方法的反编译应该独立于调用它的上下文（因此应该忽略此信息2）再次，我们区分两种类型的帧对于正常（fr）和异常行为（frE）。重要的是，PC和Method都只能被实例化为有限个值，因为给定一个固定的程序，方法的数量和不同程序计数器的数量因此，它们可以安全地声明为f sig，从而防止重要信息丢失。最后，我们声明局部变量Loc的集合和堆栈位置堆栈作为dyn，因为他们威胁终止，因为我们已经看到在example.请注意，部分计算的终止要求提供的pe类型为此，要求任何标记为f sig的sub（参数）实际上具有有限签名。pe类型声明的重要性在于，它们可以在PE时用于忽略、过滤或保持每个参数中的信息可用，如上所述。使用pe类型声明的嵌入关系称为带pe类型的 作为传统的嵌入关系，它分别通过相应的展开映射和抽象映射算子，在局部和全局控制下引导PE过程。6减少全局控制中的多变量在上一节中，我们已经看到了如何使用合适的部分求值类型，在局部和全局控制级别上都保持了对Reynnum的终止保证，同时又足够积极，从而摆脱了解释层。然而，虽然这样得到的反编译程序是可以接受的，仔细检查这些残留的程序表明，相对经常，无用的专业化已经执行。在局部控制级别，执行比必要的更多的展开通常会导致由许多子句定义的剩余谓词在全局控制级别，试图太精确会导致在剩余程序中产生太多的谓词。问题是，在全局控制下抽象原子时，是否有任何方法可以考虑以前的泛化历史。直觉是要跟踪我们被迫忘记的信息，的部分评估过程，并继续忘记它直接为所有新的原子，这是类似于以前处理的一些标准。这样做的动机是，由于我们很可能最终会被迫忘记这些信息，所以我们越早忘记这些信息越好，无论是在专业化时间还是剩余程序的大小我们现建议96M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）85一种基于上述思想的技术，其可以通过改进的抽象运算符被包括在标准部分求值算法内。为了做到这一点，首先，我们需要给出一些初步的定义。项T是S的推广（或S是T的实例），记为T≤S，如果<$σ。Tσ= S。两个项T和TJ是变体，记为T<$TJ，如果T≤TJ且TJ≤T。如果T和TJ是变体，则存在重命名ρ使得Tρ=TJ。一组项{T1，.，Tn}是另一项T，使得，σn，其中Ti= Tσi，i = 1，.，n.泛化T是{T1，.，Tn}，如果对于每隔一项TJs. t. TJ是{T1，. ，Tn}，TJ≤ T. 我们也说两个原 子 是 同 系 的 ， 记 作 A<$B ， 如 果 filter （ A ， pe typeA ） <$filter （ B ， petypeB）。定义6.1[HINTSTABLE]我们将HINTSTABLE定义为一组成对的原子A.A.，G.，s.t.G≤A（即，G是A的推广）。我们将这些原子对称为提示，因为它们提供了在全局控制级别执行抽象期间如何忘记无用信息的建议。接下来，我们需要定义一组对HINTT表的操作，这些操作将在后面的部分求值算法中用于添加和恢复表中的信息。• addHint：HINTSTABLE×Atoms，Atoms →HINTSTABLEaddHint（HT，A，G）=HTA，G• applyHint提示：提示表×原子→原子applyHint（HT，A）=msg（GsA）其中Gs ={G |<$B，G <$∈ H INT T ABLE，A <$B}• applyHint提示：提示表×原子→原子applyHint（HT，A）=msg（GsA）其中Gs ={G |<$B，G <$∈ H INT T ABLE，A <$B}现在，我们可以通过依赖上面给出的定义和运算符来定义抽象的xpt+genxpt定义6.2[abstractpt+gen]抽象运算符abstractpt+gen根据抽象pt运算符定义如下：abstractcallback+gencallback（Si，Tcalls，HT）=abstractcallback（Si，ATcalls）其中，AT呼叫={H|H = applyHint<$（HT，A），<$A∈ T调用，<$∈ {<$，<$}}让我们注意到，抽象的“pt+ gen”算子定义是参数化的。“" ， 它 表 示 两 个 不同 的 抽 象 运 算 符 ， 即 抽 象 提 示 + 生 成 提 示 和 抽 象 提 示 + 生 成 提 示 ，具 体 取 决 于 使 用 哪 个 a p p l y H i n t 运 算 符 。在讨论了如何在全局控制期间利用hints-tables之后，主要问题是我们如何准确地用所需的条目填充这样的表。我们建议在部分评估期间以这样的方式简单地仪器化测试，即每当它标记两个原子A和B之间的可能问题时，即，如果M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）8597main（[[ref（loc（1）），num（int（_））]，heap（[array（B，A）]）]，[num（int（0））]）：-0>=B.main（[ref（loc（1）），num（int（A））]，heap（[array（B，[num（int（D）|C]）]）]，[E]）：-0< B，D\=A，execute（[num（int（D））|C]、B、A、0、1、F、E）。main（[ref（loc（1）），num（int（A））]，heap（[array（B，[num（int（A）|C]）]，[D]）：-0< B，execute（[num（int（A））|C]、B、A、1、0、E、D）。main（[[null，num（int（_））]，heap（[]）]，[ref（loc（1））]）.execute（A，B，C，D，E，heap（[array（B，A）]），num（int（E）：-E>=B.execute（A，B，C，D，E，heap（[array（B，A）]），num（int（E）：- E B，D\ =0. 执行（A，B，C，0，D，E，J）：-D B，0= D，L是D+1，nth（L，A，num（int（M），M1=C，N是D+1，执行（A，B，C，0，N，E，J）。执行（A，B，C，0，D，E，J）：-D B，0= D，L是 D+1，nth（L，A，num（int（C），执行（A，B，C，1，D，E，J）。见图6。 线性搜索程序如果关系A和B都成立，除了返回值true之外，它还存储对A，msg（A，B）插入提示表。例6.3现在，让我们再次考虑图5中的SLD树。我们从一个空的提示表HT={}开始。首先，在中间分支中，一旦我们到达e_bed_dd_a_m_execute（8，[ref，0，1]），就可以通过调用addHint运算符来实现。同样，另一个提示将被添加到右分支中。因此，在构建第一个展开树之后，该表具有以下两个条目：HT=.Σexecute（8， [ref，0， 1]），execute（8， [ref，0，Y]）execute（8， [ref，1， 0]），execute（8， [ref，X，0]）一旦展开过程完成（参见第3节中的部分求值算法），将对抽象运算符进行以下调用：abstract抽象操作符+gen抽象操作符（{}，{execute（8， [ref，0， 1]），execute（8，[ref，1， 0]）}，HT）现在，让我们解释每个不同抽象操作符的应用效果：• 使用abstract+ gen。applyHint 函数操作符简单地返回每个原子的相应的广义版本。因此，标准的ab操作符将被抽象的abstract（{}，{execute（8，[ref，0，Y]）调用，execute（8， [ref，，X，0]）}）。注意，虽然我们保持了相同数量的不同原子，但由于我们推广了一个数值参数，因此可能会减少多变量，避免了在相应的参数中出现具有不同数值的相同原子的新不同版本的可能性。• 使用abstract+gen。在这种情况下，多变量将立即减少，因为正如我们将看到的，两个原子将坍缩成相同的一般化版本。这是由于同系原子在applyHint操作符内部执行，这将引起对标准抽象操作符abstract_opt（{}，{execute（8， [ref，X，Y]），execute（8， [ref，X，Y]）}）的以下调用在图6中，我们可以看到我们利用新引入的技术获得的剩余代码，通过部分评估JVML解释器w.r.t. 的98M. Gómez-Zamalloa等人/理论计算机科学电子笔记190（2007）85基准一的pt收益名称大小TM Mem UNF/Eval大小 TM Mem UNF/Eval大小 TM大小exp0.331.567121393/2270.960.635471092/1870.782.49 1.23GCD0.271.195661118/1440.790.48329837/1100.622.48 1.26LCM0.614.159693211/3672.501.394712509/2972.282.98 1.09combNR0.333.3413322179/2872.000.927291623/2161.473.64 1.36combR0.395.8217332750/2852.451.4712032131/2271.783.95 1.38染0.281.525621099/1480.850.60321818/1140.682.53 1.25添加0.80 29.7559809083/111523.15 7.0338236757/83018.18 4.23 1.27exp0.418.4420273570/5594.571.2210792444/3823.166.92 1.45简化0.7014.6030766205/8978.702.8719174774/6977.265.08 1.20二元Srch0.42 38.809867 10740/1571 29.91 6.0033614837/72711.53 6.46 2.59向前0.6062.87410614714/2256 16.30 9.20410814714/2256 16.30 6.83 1.00菲布0.28---/--0.643381421/1911.10∞∞线性0.32---/--1.804782610/39416.09∞∞迹象0.33---/--3.9810524401/70211.40∞∞表1测量PE类型的效果我们运行的例子的字节码程序（见图1）。2）的情况。因此，我们已经使用了xpt作为嵌入关系（当嵌入被标记时添加提示）和抽象xpt+ genxpt运算符。注意，入口调用是main（In，Out），其中In将被实例化到为方法指定的参数值列表