理论计算机科学：从公共语言到Java虚拟机的转换比较研究

理论计算机科学电子笔记141（2005）35-52www.elsevier.com/locate/entcs通用语言Java与Java虚拟机Sam Shiel萨姆·希尔1，2伊恩·贝利3牛津布鲁克斯大学计算机系Oxford OX33 1HX，U.K.摘要我们描述了如何将程序从公共语言转换为Java虚拟机，基于我们编写应用程序的经验我们还叙述了这一经验告诉我们这两种架构之间的差异。关键词：字节码语义，字节码转换，字节码验证1介绍目 前 使 用 的 两 个 最 著 名 的 基 于 堆 栈 的 虚 拟 机 是 公 共 语 言 虚 拟 机（Common Language Virtual Machine，JVM）和Java虚拟机（Java VirtualMachine，JVM）。两者之间有许多明显的相似之处。两者都是静态类型的，提供自动内存管理（垃圾收集），1感谢审稿人提供了额外的想法并指出了原始草案2 电子邮件：sam. gmail.com3电子邮件：ibayley@brookes.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.03936S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）35多线程能力，并在指令级支持面向对象的模型。再进一步，这两个都使用单继承对象模型，具有多接口实现。两者都包含了类、抽象类、接口、方法（虚的和静态的）和字段（实例和静态的）的概念。因此，了解JVM和JVM在多大程度上是等价的是一个学术兴趣的问题。虽然Gough已经比较了这两者[3]，但我们认为最好的比较方法是编写一个应用程序，将最初编译为在JVM上运行的程序转换为在JVM上这将迫使对能力方面的任何差异进行审查。因此， 我们中的一个人（Shiel）写了这样一份申请。正如预期的那样，在这个应用程序的设计和实现中出现的问题反映了JVM和JVM之间的差异和相似之处此外，《公约》还支持核查的概念。有趣的是，在过去的几年里，JVM一直是深入研究的主题[10]，但几乎没有发表关于JVM的文章，尽管事实上这两个虚拟机之间存在许多重要的差异。两者之间的详细比较将使研究人员能够应用他们为JVM获得的结果。第一个小小的障碍是在Java中使用不同的术语来表示其他熟悉的JVM概念。代表应用程序的类集合被捆绑在一起作为一个程序集，这是一个包或文件的等价物。程序集由两种类型的数据组成：方法体（指令序列）和元数据。元数据包含的信息比JVM“.class”文件中的信息多，对于可编程逻辑器件本身的体系结构，程序计数器被重命名为指令指针，操作数栈被重命名为计算栈。局部变量数组没有被重命名，但这可能会引起误解，因为它不包括调用方法时使用的参数;它们单独保存在一个参数数组中。对Android的一个要求是它是语言中立的，可以开发多语言应用程序。为了帮助这种互操作性，公共类型系统（CTS）与公共语言规范（CLS）一起定义了一组规则，应用程序的每个组件都必须遵守。最后，用于编写指令的语言被称为通用中间语言（CIL）。本文件的结构是沿着这一类型的系统。 部分2考虑了单独使用基元类型时可能遇到的问题。第3节描述了值类型，它们是最大的S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）3537CLR类型JVM类型描述布尔›→布尔True或FalseSByte›→字节带符号8位字节Int16›→做空带符号16位整数Char›→char无符号16位字符，Unicode格式Int32›→int符号32位整数Int64›→长带符号64位整数单个›→燕麦单精度示波器，IEEE 754格式双›→双双精度示波器，IEEE 754格式字节›→无无符号8位字节UInt16›→无无符号16位整数UInt32›→无无符号32位整数UInt64›→无无符号64位整数表1将JVM值类型映射到JVM原语。在Java和JVM之间进行数据交换。第4节讨论数组。第5节介绍了对象，并由第6节扩展，第6节考虑了继承和类层次结构。第7节提到了其他特性，如指针和异常。最后，第8节结束。2基元类型如表1所示，在JVM值类型和JVM基元类型之间存在相当密切的对应关系。例外的是没有签名的类型，它们没有JVM等价物。2.1定加载数值常量使用ldc系列指令加载到堆栈中，而字符串引用使用ldstr指令加载所有这些指令都是使用ldcJVM指令转换的，该指令将常量池中的常量加载到堆栈上。然而，更有效的解决方案是在可能的情况下使用指令bipush（或sipush）将有符号字节（或有符号短）字面量加载到堆栈上。38S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）35也有专门的CIL指令来推送范围为-1到32位整数。8个，每个都占用一个字节。这些指令中的大多数都可以转换为相应的单字节JVM指令，例如iconst 1，它将整数常量1推送到堆栈上。2.2普通指令许多JVM指令将类型信息编码为前缀。例如，iadd将两个整数相加，fmul将两个整数相乘。结合指令操作数（对于更通用的指令，如ldc），总是可以推断出被操作的类型。转换数字常量加载是直接的，因为CIL指令的ldc家族对于可能被推送到堆栈上的每种类型的值（整数，长，双精度或双精度）都有不同的指令。然而，大多数CIL指令是通用的，并且不包含可以从中推断类型的信息（例如，对于乘法和加法，只有一个mul指令和一个add指令）。这是因为CIL总是被编译而不是解释[5]。为了正确地将CIL指令转换为JVM指令，因此有必要为每个被转换的方法维护一个JVM计算堆栈的类型模型2.3算术和逻辑要将JVM中的算术和逻辑指令转换为它们的JVM等价物，我们只需要识别计算堆栈顶部的类型JVM还支持无符号整数（尽管这不符合CLS）和过流检查算法，这两个都是JVM中缺乏的。将这些特性转换到JVM中是可能的，但很笨拙。为了模拟UInt 32，我们可以使用一个long类型的数据类型不变式，即前32位总是清除的;因此，这些位在每次操作后都会被屏蔽。类似的方法适用于Byte或UInt16，但对于UInt64，我们需要使用辅助变量来存储最高有效位（MSB）。额外的指令将被插入以在每个操作之后根据结果和操作数的MSB来设置或清除该位。为了转换过流检查，我们将再次使用超大的工作空间（足够大，不会发生真正的过流），测试结果，如果结果太大，则抛出定制的异常S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）3539值类型CLRJVM整数beq目的地如果ICMPEQ目地参考beq目的地如果ACMPEQ目地长beq目的地lcmp如果EQ目的地浮子beq目的地fcmpl如果EQ目的地双beq目的地dcmpl如果EQ目的地2.4分支表2比较条件分支指令。有两个复杂的翻译周围的流控制指令。 首先，JVM方法的大小限制为65，535字节。 因此，只能直接转换将导致JVM方法大小小于或等于此限制的其次，JVM比较分支指令只直接操作整数和引用，而更通用的分支指令也操作整数、long和double。这就要求转换器在比较双精度浮点数、双精度浮点数或长整型时生成两条JVM指令。作为示例，表2显示了在计算堆栈顶部的两个值相等的情况下，用于分支到给定目的地的等效的JVM和JVM指令。类似的翻译适用于bne、bge、bgt、ble和bltCIL指令。该指令也有条件分支指令，其中整数值是无符号比较的，但这些指令可以以类似于无符号算术指令的方式进行转换。3值类型也许JVM中缺少的由Java语言提供的最重要的特性是值类型。值类型满足JVM中原始类型和用户定义的结构和枚举（如C编程语言中的结构和枚举）的角色。与JVM中的基元类型一样，值类型通过值传递，并存储在堆栈中，而不是堆中（值类型除外40S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）35是引用类型的成员）。但是，与JVM基本类型不同，值类型可以有关联的方法。这些方法不存储在堆栈上，因此值类型只占用表示其实际值所需的堆栈空间。将值类型的语义从JVM转换到JVM是有问题的。一种方法是将表示基元类型的JVM值类型转换为它们的JVM基元类型等价物，然后创建一个JVM盒类，复制每个这样的JVM值类型的功能和接口。然后，可以通过将基元类型装箱到相应box类的实例中，调用适当的方法，然后从对象实例中取消装箱基元类型，来模拟对值类型的方法调用。更详细地说，装箱值类型涉及将其从计算堆栈中移除，在堆上创建引用类型并将值存储在引用类型内，然后将对装箱值的引用放置在计算堆栈上。取消装箱将从堆栈中移除引用类型，并从其中检索值类型，然后将值类型放置在计算堆栈上。当然，这需要实例化和垃圾收集box对象的所有开销，因此远非理想。在我们描述另一种方法之前，请注意，需要装箱和拆箱来转换特定的指令框，并将该框拆箱，并将值类型拆箱到引用。每个JVM box类将被赋予额外的get和set方法，以便box指令可以通过实例化适当的box类并调用set方法来转换，而unbox指令可以通过调用get方法来转换。第7.1节给出了装箱和拆箱的一个示例。另一种方法利用了这样一个事实，即赋值类型必须是final的，具有固定数量的方法。这允许我们提供一组JVM类，这些类与那些表示原始类型的值类型相同，但有一个关键的区别：所有方法都被定义为静态的，添加了一个额外的参数，其目的是将值类型的值因此，我们可以将一个对Java值类型的虚方法调用转换为一个JVM静态方法调用，其值为参数。这种静态方法调用不需要对基元类型进行装箱和拆箱的开销，因此开销要小得多在这两种方法中，结构值类型都必须被转换为引用类型，并提供深度克隆复制方法来模拟值类型语义（因为结构可能包含其他值类型，这些值类型本身使用引用类型进行模拟当顶部的项目S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）3541如果计算栈是结构，则将通过调用其复制方法来翻译重复指令，该复制方法将递归地调用其所有结构成员上的复制这些问题和周围的并发症已经由Gough [2]进行了探讨，他使用了术语4阵列该函数提供了两种类型的数组：一维数组（也称为向量）和多维数组。向量可以包含对其他向量的引用，从而启用（可能是不规则的）数组的数组，这就是多维数组在JVM中的实现方式，因为它没有直接等效的多维数组。数组向量是System.Array抽象类的子类型，因此对于每个数组类型，都有一个从System.Array派生的对应向量类型。有一些特定的CIL指令用于创建向量，操作（加载和存储）其中的元素并获得向量的长度。幸运的是，它们中的每一个都有一个直接的JVM对应物， 很容易.下一个问题是如何处理在向量类型实例上调用的方法。这可能最容易通过创建一系列JVM类（每个CLS类型一个）来处理，这些类实现由System.Array抽象类定义的接口。System.Array类中定义的非静态方法需要更改为静态方法，并添加一个额外的参数来传递数组实例引用。然后，转换将涉及将CIL源代码中的任何向量实例方法调用替换为相应的JVM静态方法。数组中的多维数组也表示为System.Array抽象类的子类型。但是，没有专门的CIL指令来处理多维数组。相反，它们被视为任何其他引用类型。因此，将XML多维数组转换为JVM将是一个创建JVM类的问题，这些类复制了XML多维数组类的接口和功能最后一个复杂的问题是数组的初始化方式。与生成一系列指令来初始化数组的元素不同（就像在JVM上所做的那样），JavaScript使用一个特殊的帮助器方法，该方法接受要初始化的数组和一个表示初始元素值的结构作为参数。这个结构需要被转换成适当的JVM指令序列。42S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）355对象5.1性能与JVM不同的是，JVM有属性作为类型成员的概念。然而，属性实际上是作为常规访问器方法实现的，在元数据中被特别标识为属性。CIL代码中对属性的所有引用都是通过调用访问器方法来实现的，这使得属性的转换完全透明。5.2会员访问Modifierspublic和private修饰符与JVM public和private修饰符具有相同的含义，并按此翻译。此外，JVM提供了比JVM更细粒度的成员访问修改器像往常一样，所有类成员都可以由封闭类访问。修饰符修饰符“As-socket”意味着类成员可以被同一个程序集中的类访问（请记住，这此外，当族访问和 （ 分 别 包 含 或 ） 程 序 集 访 问 的 条 件 都 成 立 时 ， 调 制 器 因 此 ，'FamOrAssem'转换为受保护，'Assembly'转换为包可见性，默认情况下，通过缺少修改器来表示。JVM没有与'FamAndAssem'或'Family'访问修改器等效的访问修改器5.3方法参数和局部变量在JVM中，每个方法都可以访问一组32位隐式寄存器，这些寄存器用于存储其参数和局部变量。由于每个寄存器只能存储一个32位值，长和双倍大小的参数和局部变量占用两个相邻的寄存器。 在静态方法的情况下，方法的参数将驻留在寄存器{0，.，N + D}，其中N是参数的总数，D是长参数或双倍大小参数（消耗两个寄存器）的数量。 在非静态的方法时，实例引用隐式放置在寄存器{0}中，因此方法参数将驻留在寄存器{1，.，N + D}，其中N和D如上定义。属于该方法的任何局部变量占用后续寄存器，长和双局部变量再次需要两个相邻的寄存器。由于方法参数和局部变量放在同一组寄存器中，因此可以使用适当类型的load和storeS. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）3543指令请注意，当加载或存储double或long时，加载和存储指令始终引用存储值的两个寄存器中较低的寄存器，但它们仍然将两个寄存器的内容作为单个值加载到计算堆栈上。在MySQL中，方法参数和局部变量使用两组不同的寄存器，并使用不同的指令进行访问。与JVM不同，寄存器的大小是可变的，因此每个参数和局部变量只消耗一个寄存器，而不管它的大小。方法的参数通过ldarg和starg指令访问（对于实例方法，参数寄存器{0}包含实例引用，与JVM一样）。局部变量使用通用的ldloc和stloc指令访问。因此，将方法参数和局部变量从JVM转换到JVM需要将JVM中的两组寄存器映射到JVM中的单组寄存器，同时考虑到需要为每个长且双倍大小的参数或局部变量分配两个相邻的寄存器。5.4访问字段字段在JVM和JVM上的访问方式非常相似。JVM分别使用ldfield和stfld指令来加载和存储实例字段，而JVM使用直接等效的getfield和putfield指令。对于静态字段，JVM使用ldsfld和stsfld指令，它们在getstatic和putstatic指令中也有直接的JVM对应物。6继承6.1类Java 类 最 终 必 须 从 System.Object 派 生 ， 而 JVM 类 必 须 从java.lang.Object派生。在这两种情况下，一个类只能从一个超类继承，但可以实现多个接口。忽略嵌套类的特殊情况，类在两个平台上的默认可见性都是私有的（这意味着它只能从声明它的程序集或包中访问），但它也可以指定为公共的。System.Object提供了与java.lang.Object类似的功能。将Java类转换为JVM类的最完整的解决方案是创建一个JVM类，它的直接超类是java.lang.Object，但它模仿System.Object的接口。然后，所有转换后的JavaScript类都将从System.Object类的JVM版本派生，44S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）35本身将从java.lang.Object派生。一种更简单但有限的方法（只能在没有访问System.Object类的成员时使用）是将直接超类为System.Object的JVM类为直接超类为java.lang.Object的6.2接口在这两种情况下，接口只是一个标记为接口的纯抽象类在Java和JVM中，接口不能从任何类型派生，但它可以有一个或多个超接口。因此，一个JVM接口可以直接转换成JVM接口。6.3方法调用JVM和JVM都支持静态方法和实例方法。 在JVM上，所有的实例方法都是虚拟的，但JVM同时具有虚拟和非虚拟实例方法。此外，该方法允许使用newslot指令定义虚方法，这意味着该方法将占用v表中的新槽，而不是覆盖任何继承的方法。由于JVM没有非虚实例方法和newslot指令的概念，因此不能在所有情况下直接转换这些方法，尽管名称修改可能是一种解决方案。在这两个平台上，方法参数都是从左到右推送的，从而简化了翻译。CIL调用指令执行早期绑定调用，通常用于调用静态方法和超类中的方法[8]。因此，它完成了JVMinvokestatic和invokespecial指令的角色。CILcallvirt指令执行后期绑定调用[8]，并用于调用虚拟方法。它相当于JVMinvokevirtual和invokeinterface指令。6.4构造函数调用Java和JVM都支持静态构造函数和实例构造函数的概念。静态构造函数（也称为类构造函数）通常用于初始化属于类的静态字段，并在创建类的任何实例或访问任何静态成员之前隐式调用实例构造函数用于创建和初始化类实例，并在实例化类时显式调用。这个函数将所有静态构造函数命名为.cctor，将所有实例构造函数命名为.ctor，而在JVM上，它们被命名为clinit>和init>，S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）3545CLRJVMldc.i4.3新的多边形newobj void Polygon：：.ctor（int32）DUP图标3invokespecialPolygon/init>（I）V表3在JVM和JVM上调用构造函数。- 是的静态构造函数在两个平台上的行为方式相同，并且很容易转换。然而，实例构造函数的调用会使翻译变得非常复杂。考虑一个表示多边形的类，其构造函数接受指定多边形实例的边数的单个整数参数。表3比较了实例化一个表示三角形的多边形对象可以看出，在单个CIL指令newobj创建新实例并调用其实例构造函数之前，该版本将实例构造函数的参数推送到计算堆栈相反，JVM版本创建一个新的引用，复制它，加载操作数堆栈，然后显式调用实例构造函数。为了在被调用的构造函数采用单个参数的情况下转换CILnewobj指令，转换器将需要在加载单个参数之前插入new和dupJVM指令（或者对于任何N元构造函数，在N个参数被N个连续加载压入之前）。这当然假定所有参数都是显式的计算而不是计算。如果参数3是推的结果并且例如将ints 1和2相加，则new和dup指令将必须在这两个压入之前插入。更一般地说，我们需要执行数据流分析，以在指令序列中找到正确的位置来推送对象引用。一个更简单的（虽然不太有效）首先将堆栈顶部的N个构造函数参数存储到局部变量中，然后实例化对象并复制其引用的指令在将构造函数参数加载回堆栈并最终调用构造函数之前，先在堆栈上调用构造函数。46S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）357其他问题7.1参考参数JVM允许通过引用和值传递值类型，而JVM原语类型只能通过值传递。局部变量或方法参数的地址可以作为托管指针加载到使用ldloca和ldargaCIL指令重新加载的SQL计算堆栈上。CIL指令的stind家族从堆栈中获取值和托管指针，并将该值存储在托管指针所引用的位置中，而ldind指令从堆栈中获取托管指针，并将在堆栈上的托管指针所引用的位置处找到的值放置在堆栈上。下面的CIL代码提供了使用引用参数的原型swap方法的实现（类似C的伪代码已添加到注释中）：.method static void swap（int32 X，int32 Y）ldarg.0// load address of X // temp = *x;.ldind.i4//间接加载X的值stloc.0//临时保存X的值ldarg.0//加载X的地址// *x=*y;. ldarg.1//加载Yldind.i4 //间接加载Y的值stind.i4 //将Y的值存储到Xldarg.1//加载Y的地址// *y = temp;. ldloc.0//加载Xstind.i4 //将X的原始值存储到Y的地址ret//从方法为了使用上面的代码交换两个局部变量，我们必须首先使用ldloca指令将它们的地址加载到计算堆栈上，然后调用swap方法：...ldloca 0 // load address of Xldloca 1 // load address of Y callvoid swap（int32，int32）...可验证性约束禁止托管指针指向指针，因此引用参数传递可以使用装箱和拆箱转换到JVM（该技术是Gough [1]提出的几种技术之一）。对于每一个基本类型，一个合适的盒子类必须用get和set方法定义，如第3节所述。S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）3547在我们下面对JVM的翻译中，我们假设了一个合适的int box类，它配备了get和set方法。注意，CLI指令ldind是通过调用get方法转换的，stind是通过调用set方法转换的下面是swap的JVM版本：aload_0// load reference to boxed X invokevirtual Box.get：（）I//从box istore_2中检索X的值//临时保存X的值aload_0//加载对盒装X的aload_1// load reference to boxed Y invokevirtual Box.get：（）I// retrieve value of Y from box invokevirtual Box.set：（I）V // set value of boxed X to Y aload_1// load referenceto boxed Yiload_2// load临时保存的X值invokevirtual Box.set：（I）V//将装箱的Y值设置为Xreturn//返回方法ldloca和ldarga指令的每次出现都被转换为JVM指令序列，以实例化适当的box对象，并以局部变量或参数作为参数调用set方法。...new Box//创建X dup的box调用专用框。“init>"：（）Vastore_2//保存对X框的aload_2//加载X框的iload_0//X的加载值invokevirtual Box.set：（I）V//X new Box的box值//为Y dup创建box调用专用框。“init>"：（）Vastore_3//保存对Y框的aload_3//加载对Y框的iload_1//Y的负载值invokevirtual Box.set：（I）V// box value of Yaload_2//加载装箱的X引用aload_3// load boxed Y reference invokestatic swap：（LBox;LBox;）Vaload_2//加载装箱X的地址invokevirtual Box.get：（）I//取消装箱X的值istore_0//存储X48S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）35aload_3//加载装箱Y的地址invokevirtual Box.get：（）I//取消装箱Y的值istore_1//存储Y...虽然也可以获得指向实例或静态字段的托管指针（分别使用ldflda和ldsflda指令）和数组元素（使用ldelema指令），但我们还没有考虑如何将这些功能转换到JVM中。7.2异常处理乍看之下，Java和JVM上的异常处理非常相似，都支持熟悉的然而，他们在几个方面有所不同。首先，JVM允许抛出System.Object的任何实例或子类，但JVM只允许抛出java.lang.Throwable的实例或子类。除了镜像JVM中的catch和finally子句之外，JavaScript还支持fault和filter子句。fault子句与finally子句的不同之处在于，只有在关联的try块中抛出异常时，它才会执行。过滤器子句实际上是一个谓词，可以决定是否应该处理或忽略异常此外，在处理最后条款的方式上也有不同。看下面的例子（摘自[7]）：public void onDestiny（）{Destiny {return（）;}最后{return（）;}}上面代码对应的JVM指令如下：00 负载_001 invoketrypticaltryItOut（）V04jsr 1407 返回08 astore_109 JSR 1412 负载_113 阿斯洛S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）354914 astore_215 负载_016 invokevirtual wrapItUp（）V19个ret 2try块，在0和7之间，调用tryitOut（），然后调用finally块作为子例程，并随后返回。位于操作集14和19之间的finally块将返回地址存储在寄存器{2}中，调用wrapitUp（），然后使用存储在寄存器{2}中的位置返回。令人惊讶的是，在o_sets 8和13之间还有一个catch块，它存储抛出的异常，调用finally块，检索异常，然后再次抛出。如果你考虑到仅仅存储和检索异常和返回地址的指令的数量，那么毫不奇怪，Python中的同一个例子更简洁：00 ldarg.0//开始尝试01 call instance void tryItOut（）06 leave.s 15 //try结束08 ldarg.0//finally 09调用实例void wrapItUp（）14 最后15 ret专用指令leave和endfinally分别退出try块和finally块。请注意，我们不需要翻译未捕获异常的重抛出。7.3未检查的有几个我们根本没有研究过的特征。这些包括尾调用（Schinz和Odersky[11]详细讨论了尾调用和JVM），线程，委托，强制，枚举和事件。8结论和进一步工作开发的翻译应用程序能够将CIL的结构和功能的重要子集翻译到JVM，包括近一半的CIL指令集。它可以翻译：(i) 类、抽象类和接口定义。(ii) 静态和实例（空值）构造函数调用。50S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）35(iii) 虚方法和静态方法的定义和调用。(iv) 字段定义和访问。(v) 对应于JVM基元类型的值类型。(vi) 流量控制指令。(vii) 算术（不包括无符号和过流检查）和逻辑指令。(viii) 对应于JVM基元类型的值类型数组这项调查在Java和JVM之间产生了许多分歧。我们特别感兴趣的是与任何形式化的验证研究相关的类型化规则和操作语义。(i) CIL指令是通用的，因此键入规则的条件将更加复杂。(ii) 由于以下额外的限制，验证可以在单次通过中完成，而不需要定点迭代：无条件跳转后的操作数堆栈被假设为空，除非该位置本身是向前跳转的目标（[9]，章节6.1.7.5）。仅仅因为这个特性，我们就很想看看定理证明者检验验证的可靠性会容易得多(iii) 数据类型系统更丰富，因为数据项可以是值或引用，并且几乎在每个类型规则中都必须参考这些信息。指令框和取消框必须区分值和引用，它们的位置也将不同。(iv) CLS不需要一个对象在使用之前被初始化的规则，因为它不能在没有初始化的情况下被创建然而，它确实像JVM一样要求没有对象被初始化两次，但这也必须相对容易确保，因为构造函数方法之外的每个对象都已经初始化了。(v) 而不是使用一个子程序的通用概念，在ESTA有特殊的异常处理和使用 普 通 的 控 制 流 程 指 令 的 cialised 结 构 受 到 限 制 。 例 如 ， 只 有throw、leave、endfilter、endfinally和rethrow可以用于离开受保护的块，而不是任何常规的分支指令。JVM使用返回地址作为第一个类值，因此需要进行数据流分析对受保护块的大多数限制完全是词法的，易于检查。我们现在计划使用这些见解来形式化XML的语义，类似于许多人对JVM所做的事情[10]。那么我们打算S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）3551导出本文中概述的转换作为数据细化。更准确地说，我们将定义一个从命令行状态到JVM状态的函数，并为每个CLI指令导出等价物，以及定义其适用性的保护措施。我们还将从另一个方向派生一个数据类型细化，从JVM到Java。我们选择了另一个方向进行研究，只是因为后者被认为更有表现力。本文中受益于形式推理的方面包括动态方法分派、过流算法和寄存器。特别是，我们所提倡的对象初始化的处理，可以证明是正确的，通过推导出我们还打算构建一个正式的异常处理的模型，作为一种方式来阐明的OSPECIFICATION。这将使我们能够检查JVM和JVM异常处理的相对表达能力看到如何管理托管指针的正式规范，以及没有非法内存被访问的证明，也会很有趣。我们希望这篇介绍能启发其他研究者更仔细地研究CIL的语义和验证进一步的调查可能会发现验证是否过于宽松，过于限制，两者兼而有之或两者兼而有之，并可能对未来虚拟机的设计做出很大贡献。引用[1] Gough，J，Java虚拟机的参数传递（1998）。URLciteseer.ist.psu.edu/gough98parameter.html[2] Gough，J，“Compiling for the .NET Common Language Runtime,” Prentice-Hall,[3] Gough，K.J.，Stacking them up：a comparison of virtual machines，in：ACSAC55比61[4] Gough，K. J.和D. Corney，在Java虚拟机上实现Java以外的语言。网址citeseer.ist.psu.edu/499197.html[5] Hamilton，J.，公共语言运行库中的语言集成。38（2003），pp. 19-28岁。[6] Lidin，S.，“Inside Microsoft .NET[7] Lindholm，T.和F. Yellin，“Java虚拟机规范”，Addison-Wesley Longman Publishing Co.，股份有限公司、1999.[8] Meijer，E. 和j. Gough，公共语言运行时的技术概述（2000）。URLciteseer.ist.psu.edu/meijer00technical.html[9] 米勒，J.S.和S. Ragsdale，52S. 谢尔岛Bayley/Electronic Notes in Theoretical Computer Science 141（2005）35[10] 钱志，“A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and[11] Schinz，M.和M.奥德斯基，尾巴呼叫消除对的Java虚拟机器，在：Proc.ACM SIGPLAN BABEL'01 多 语 言 基 础 设 施 和 互 操 作 性 研 讨 会 。 ， Electronic Notes inTheoretical Computer Science59（2001），pp. 155 http://www.elsevier.com/locate/entcs/。