Java字节码指令集的形式化：系统和严格的指令数量减少方法

理论计算机科学电子笔记264（4）（2011）19-34www.elsevier.com/locate/entcs一打指令使Java字节码1Patryk Czarnik3 Aleksy Schubert4华沙大学信息学研究所。Banacha 202-097华沙波兰摘要Java字节码形式化的最大障碍之一是语言由200条指令然而，在程序验证和错误检测的上下文中对编程语言的严格处理需要尺寸紧凑的形式主义。因此，实际的Java字节码指令集永远不会在上下文中使用。相反，现有的形式化通常涵盖一组“代表性”的指令。本文描述了如何以系统和严格的方式将指令数量减少到一组可管理的更通用的操作，这些操作涵盖了Java字节码的全部功能指令集的因式分解基于运行时结构的使用，例如操作数堆栈，堆等。这是通过表示Java虚拟机的正式语义来实现的保留字：字节码，语义1介绍程序从一方传输到另一方，在接收方一方提出了程序执行的安全问题。因此，期望提供保证代码从开发者行进到消费者的形式的代码的某些计算属性的手段。 Java字节码语言（简称JVML）是在互联网上传播的最流行的代码格式和安全性它的执行已经引起了实际问题（见[5，8]），这些问题超出了通过Java沙箱控制执行的能力。解决这一问题的一个可能途径是为语言提供一个精确的数学模型，然后利用该模型证明程序的性质，并提供1这项工作得到了波兰政府拨款N N206 493138的部分支持2电子邮件：chrzaszcz@mimuw.edu.pl3电子邮件：czarnik@mimuw.edu.pl4电子邮件：alx@mimuw.edu.pl1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.02.00320J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）19该移动程序具有附加信息，该附加信息将使得有可能在代码消费者侧高效地重构证明JVML提出了几种形式语义，包括最著名的语义：[1，7，11，13，14，15，16]。这些公式来自两个问题之一-要么它们提供（几乎）所有200个字节码指令的形式语义，要么它们选择代表大多数有趣功能的指令子集。前一种选择的缺点是，在这种情况下，形式化是非常困难的操作，因为大多数的证明必须通过归纳程序的结构来因此，后一种选择更经常被研究人员遵循，但是指令代表的特定选择通常与字节码的实际指令无关，并且很少讨论实际指令与模型中的指令的对应关系当前的文章提供了缺少的讨论，并将指令划分为遵循相同模式访问JVM运行时结构（如堆，操作数堆栈等）的组例如，所有的加载指令都被分组在一起，所有的跳转，包括子例程（jsr和ret），还有*aload ，getfield，checkcast和instanceof形成一个单独的组，因为它们都访问堆，（可能）在操作数堆栈上放置一些东西或引发异常。通过这种方式，我们获得了整组JVML指令的因子分解为12项。实际的指令列表可以在[3]中找到我们认为，提出一种基于少量指令的形式化是至关重要的，因为这样更容易证明语言本身的属性-这种语言的许多证明都是通过对可能程序结构的归纳来完成的。如果指令的数量是有限的，那么在这样的证明中要考虑的情况的数量就很小。这就是为什么像EML [10]这样的企业，语义规则的数量达到几百条，未能开发出元理论属性，而Coq模块系统[2]在这方面取得了成功的主要原因。此外，它是一个标准的编译器设计技术，建立一个小的语言，使优化技术的设计很容易。Java及其字节码的此类语言的例子包括BAF，Jimple和Grimp [17]以及BIR [6]。此外，我们的严格考虑提供了一个机会，可以展示真正涵盖整个字节码行为范围的指令。我们知道，对于JVML的某些属性，稍微不同的一组指令会更方便（例如，区间静态分析的证明需要访问实际的算术运算，然后期望显式地考虑然而，仍然有一条路径可以到达JVML中的所有操作，因为它们在我们的语义中的特定行为可以通过访问与我们的一般化操作相关联的适当表来获得我们希望这个解决方案在JVML的所有元证明中都是有用的，因为它允许为许多分析构建一个通用框架，这在为真正的JVML程序构建验证平台时非常重要。当然，本文并没有提供JVML的完整语义，[5]当我们把宽指令看作是独立的指令时，这个数字甚至更大J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）1921×联系我们···非常复杂。事实上，在一些地方，我们故意简化了语义，以便在表达中保持全面2语义域和符号我们在这里给出了Java字节码的一小步语义。语义步骤的一般形式是：P×h，ts →hJ，tsJ（2.1）其中P是程序，h，hJ是堆，ts，tsJ是线程的状态。这些值的语义域定义如下。首先，我们提供程序的描述：Prog=[Cnames~ finCDesc]。程序是具有有限域的部分函数，它将CDesc中的类描述与Cnames中的类名相关联。类名只是适当定义的标识符，类描述被定义为CDesc=[Mnames~finMDesc]，即具有有限域的部分函数，将方法描述MDesc与方法名称相关联。同样，方法名只是适当的标识符，而方法描述则稍微复杂一些，定义为MDesc=[PC~finnInstr]×ExTableExTable=[PC ×Cnames~finnPC]其中Instr是JVM指令集，ExTable是方法的异常表。目的是[PC~finInstr]中的函数提供从指令标签到标签下的指令的映射。 ExTable返回给定异常源地址和类的处理程序地址而《易经》中的《易经》，则是一部经典。堆=[Loc×ThreadId~finn（Cnames ×Monitor ×[Fnames~finnVal]）]其中Loc是具有可区分的位置空的位置（例如，当前体系结构中的自然数或指针）的集合（集合Loc空将被表示为ThreadId是线程标识符的集合（例如自然数），Monitor是将控制给定对象的锁计数器的监视器的集合，这将在后面精确定义。Fnames是字段名称的集合，Val是期望字段值的集合，即Val= int longLoc。ThreadId是堆的一个参数，因为每个线程都有自己的堆状态视图。Java内存模型[9，第17节]描述了不同视图同步线程状态集被定义为线程描述的所有有限集合的集合，Pfinn（线程）历史与状态信息历史相结合，状态信息历史包含线程调度器确定性地选择要执行的线程所需的信息。线程描述是线程=ThreadId×ThreadStatus ×EvalState ×FrameStack其中ThreadStatus表示线程的当前状态，即休眠、阻塞、22J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）19××··×→⟨⟩ts运行、终止等。最后，FrameStack=MethodFrame堆栈包含一系列形式为MethodFrame=Cnames×Mnames ×LVals ×OpStack ×PC其中LVals是定义为[Vars~finType×Val]的局部变量表，局部变量索引集Vars=N，Type是给定条目中的值的类型，Val是局部变量表中包含的值;OpStack是定义为（StackKind（Val PC））的操作数堆栈，其中StackKind表示堆栈的当前单元格中的值的类型，注意我们必须添加PC类型以确保我们可以放置子例程命令使用的字节码指令的标签;相同的集合PC用作MethodFrame的最终复合，并且值指向当前执行的字节码指令;EvalState是一个表示异常被抛出的信息的集合。我们可以假设EvalState=Loc。特殊位置null用于标记没有抛出异常的情况。我们还假设某些异常，如NullPointerException，ClassCastException等，在堆上预先分配。这极大地简化了语义，否则需要大量的语义规则来在堆栈上分配异常并在实际抛出它之前调用它的构造函数。由于简化不涉及使用的定义异常，我们决定不使语义复杂化6值得一提的是，我们在这里提供的语义是所谓的防御风格，即我们提供类型标识以及操作数堆栈和局部变量表条目，以检查存储在那里的值是否具有正确的类型。我们现在可以将监视器Monitor的集合定义为产品ThreadIdN。集合中的一对表示持有锁的线程的标识符，线程进入监视器的次数。 我们假设集合ThreadId包含一个可区分的常量none，它用于表示没有线程持有监视器的情况。对操作数栈o的一个自然操作是压入元素e。它被写为e o。检查栈的顶部是通过模式匹配完成的，并且o=e oJ意味着栈o在顶部包含e，后面是oJ中的其余部分。描述虚拟机状态的数据结构是复杂的。因此，我们需要进一步的符号来检索它们的信息。首先，我们必须介绍选择特定线程的调度程序，被执行：：P finn（Thread）历史线程。我们没有为History提供一个特定的定义，因为它依赖于实现。我们只假设调度程序从它的第一个参数返回任何元素。为了使符号更简洁，我们写ts来表示（ts）。当前线程的组成部分表示为tfsts=tidts，tstatusts，estts，tfsts。由于tfsts也是一个复合值，我们引入了进一步的表示法tfsts=tcnmts，mnmts，lvts，ostckts，pcts·tfstail（二、二）在Bicolano [13] JVM语义中，堆上的空间被分配，但构造函数没有被调用。J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）1923ts←←∈ ∈∈∈ ∈ ∈∈其中cnmts是类名，mnmts是当前执行方法的方法名，lvts是当前方法的局部变量表，ostckts是当前操作数栈PCTS是当前执行的指令的标签。值tfstail表示帧堆栈上剩余方法帧的序列（可能为空）。2.1修改和查找表示法我们经常稍微修改一个给定的线程状态以获得一个新的线程状态。使用符号变更项[替换部件新部件]描述修改。这些可以精确地定义为一个新价值的构造，其中除了被替换的部分之外，所有的成分都是不变的，后者被新的部分所替换。例如，tfs[lvlvJ]是一个线程状态tfs，它被修改，使得它在最顶层方法框架中的局部变量表lvts被新的表lvJ替换。特定指令的查找使用符号P@pc完成。嗯。其中PProg，pcPC，mnmmnames和cnm名字。 这个操作从程序P中提取类声明cnm，然后它使用Java方法查找方案来检索名为mnm的方法（我们假设方法名考虑了方法的签名，因此唯一地确定了类中的方法）。然后pc指示应该从方法的代码中检索哪个字节码指令同样，P @etable。嗯。cnm表示P中cnm类中名为mnm的方法的例外表。对h堆，sLoc，我ThreadId我们写h（s，i）来表示在从线程i在堆h中可见位置s。 在大多数情况下，i在上下文中是清楚的，所以我们省略它并写h（s）。由于h（s）是一个复合值，我们定义h（s）@cnm =π1（h（s））h（s）@monitor =π2（h（s））h（s）@obj=π3（h（s））h（s）@tid =π1（π2（h（s）h（s）@lcount =π2（π2（h（s）在s= null或s/∈ dom（h）的情况下，上面的符号的值为。2.2辅助定义在下面的语义描述中，我们使用了许多次要的符号。本节收集了对其含义的描述这里使用的诸如int之类的名称有两种含义，作为Java类型的原生整数中元素集合的名称，以及作为用于引用集合的语法标识符64位值分为两半。符号long（m1，m2）（分别double（m1，m2））表示long类型的64位值（分别为double）由两个32位字m1和m2构成。对于64位值，没有区分哪一半和哪种类型（长或双精度）的一半的类型表示为一半。Java虚拟机以一种特殊的方式处理64位类型。 因此，Java计算类型根据[12，第3.11.1节]进行划分，24J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）19×→∈∈两个类别：Cat 1={int，float，ref，returnAddr}用于32位类型，Cat 2={long，double}用于64位类型。我们还将使用标记Cat1·来表示类别1\{returnAddr}。一旦选择了当前线程，我们就可以最终确定当前执行的方法。该方法表示为cmthdMDesc。 我们还使用了一个函数next：MDescPC PC来获取方法中下一条指令的标签，使用指令出现的顺序。2.3补充说明我们下面给出的语义实际上更多的是交叉语义的解释，而不是实际的Java内存模型。然而，我们在这里提供了一种处理Java内存模型的方法，因为我们的堆是定义的，所以它可以为每个线程提供不同语义的其他功能，如类加载，类初始化，finalisation，本地和同步方法等，也没有处理。然而，对上面的定义稍加改变，就可以使下面的规则具有可以考虑它们的意义添加反射会更有问题，因为它需要我们改变语义步骤的形式。3指令语义语义规则反映了由指令执行引起的运行时结构的演化。大多数规则直接由当前方法的当前指令控制，但处理异常的规则则不是。在语义转换的过程中，调度程序会在ts中选择一个特定的线程来执行。 我们在2.1节介绍的符号都依赖于线程是固定的假设。因此，我们在每个特定的规则中固定了一个单一的选择。然而，选择可能会改变我们的语义的不同步骤。我们还假设堆的状态可以在每个规则之后改变，以便其内容的可见性在线程之间部分同步。如果我们对每一步进行完全同步，我们就获得了交织语义。3.1指令加载此指令概括了所有读取局部变量并将值推送到操作数堆栈的JVM指令。它的参数描述了要写入堆栈的值的类型和来源，指令的一般形式是load（k，n），其中k∈Cat1· nCat2是一个kind，n是一个局部变量index。在最简单的情况下，当k是32位类型kCat1·时，指令从索引n所指向的局部变量读取值，并将该值放在顶部J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）1925►→ ←←操作数堆栈的它要求值是k类的。lvts（n）=（k，m）ostckJ=（k，m）·ostcktspcJ=next（cmthd，pcts）P@pcts. 孟湾cnmts=load（k，n）k∈Cat1·estts= nullP h，ts h，ts[ostck ostckJ][pc pcJ]ncat1-load（3.1）如果k表示第2类（long或double），则要压入堆栈的值是从两个变量的值中获得的，索引为n和n+1。这是因为category-2值占据了局部变量数组中的两个后续单元格。我们为这样的一对变量中的第二个变量提供了一个人工类型的一半。按照JVM的描述[12，Section 3.6.2]，我们使用单个操作数堆栈元素来表示类别2值。lvts（n）=（k，m1）lvts（n+1）=（half，m2）ostckJ=（k，k（m1，m2））·ostckts pcJ=next（cmthd，pcts）P@pcts. 孟湾cnmts=load（k，n）k∈Cat2 estts= nullncat2-loadP×h，ts →h，ts[ostck <$ostckJ][pc<$pcJ]（3.2）3.2指令存储装置此指令概括了所有从操作数堆栈中弹出值并将其放入局部变量表的JVM指令。它的参数是弹出值的类型和目的地，指令的一般形式是store（k，n），其中k∈Cat1· <$Cat2是一种，n是局部变量指数。在类别1类型的情况下，存储指令从操作数堆栈中弹出最顶层的值，并将其存储在索引为n的局部变量中。lvJ=lvts[n←（k，m）]Ostck_ts=（k，m）·Ostck_J_pc_J=next（cmthd，pc_ts）P@pcts. 孟湾cnmts=store（k，n）k∈Cat1·estts=nullncat 1-商店P×h，ts →h，ts[ostck <$ostckJ][pc<$pcJ][lv<$lvJ]（3.3）如果k∈Cat2，则修改两个后续变量n和n+1现规定26J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）19→||第一个变量是k类的，第二个是半类的。lvJ=lvts[n<$（k，m1）][n+1<$（half，m2）]ostckJ=（k，k（m1，m2））·ostckts pcJ=next（cmthd，pcts）P@pcts. 孟湾cnmts=store（k，n）k∈Cat2estts=nullP×h，ts →h，ts[ostck <$ostckJ][pc<$pcJ]ncat2-store（3.4）3.3指令堆栈指令stackop（op）概括了所有只使用操作数堆栈的JVM指令。应该注意的是，所有这些指令都对固定数量的顶部元素进行操作，而堆栈的底部部分既不读取也不修改。参数op表示要执行的堆栈操作op的含义是通过kindsstackop（op）获得的，它是一组三元组，每个三元组包括：一个输入种类列表l，一个函数f，和一个输出种类列表lJ。列表l定义了操作对操作数栈的要求。堆栈元素的数量必须不小于l的长度，并且对于所有i，堆栈的第i个元素必须是类型为li的。这由check（s，l）表示。函数f：OpStack OpStack是实际的堆栈操作。l个元素从堆栈中弹出并成为f的输入，然后f的结果被推送在堆栈上; lJ描述了f的结果的保证类型。 在某种意义上f：l → lJ。（l，f，lJ）∈ kindsstackop（op）ostckts=s·rcheck（s，l） ostckJ=f（s）·rpcJ= next（cmthd，pcts）P @pcts. 孟湾cnmts=stackop（op）estts= nullP×h，ts →h，ts[ostck ←ostckJ][pc ←pcJ]n-stackop（3.5）例如，JVM指令iadd被映射到stackop（iadd），并且{（[int，int]，fiadd，[int]）}其中fiadd执行两个32位整数的加法多态指令， 例如交换或双工， 有一个以上的项目在kindsstackop，例如kindsstackop（dup2）等于{（[k1，k2]，fdup2，[k1，k2，k1，k2]）} k1，k2∈ Cat1n {（[k]，fdup，[k，k]）} k∈ Cat23.4指令条件该指令概括了所有JVM指令，这些指令可以在当前方法内检查程序控制流，但不J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）1927修 改 方 法 帧 堆 栈 ， 即 所 有 无 条 件 和 有 条 件 跳 转 ， 包 括 tableswitch ，lookupswitch，28J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）19∈►→ ←←jsr和ret。该指令读取并修改操作数堆栈和程序计数器（PC）。指令的一般形式是cond（op，d），其中op标识运行时结构上的实际操作，d D cond，Dcond=[N ~ finnPC]表示指令的静态参数，由地址索引表组成。 kindscond（op）的形 式 和 作 用 类 似 于 kinds stackop 的 作 用 。 这 里 的 区 别 是 f 的 类 型 ： Dcond×OpStack×PC→ OpStack× PC。f的参数是操作数集的表、操作数栈的相关部分和下一个PC。函数f返回操作数栈相关部分的新值和PC的新值只有一条JVM跳转指令jsr将某些值放入操作数堆栈：当前PC;ret是唯一一条从操作数堆栈中弹出PC新值的指令（l，f，lJ）=kindscond（op）ostckts=s·rcheck（s，l）（sJ，pcJ）= f（d，s，next（cmthd，pcts））ostckJ=sJ·rP @pcts.孟湾cnmts=cond（op，d）estts= nullP×h，ts →h，ts[ostck <$ostckJ][pc<$pcJ]n-cond（3.6）例如，JVM指令ifeq（o），如果栈顶的值是整数0，则执行跳转，被映射到cond（ifeq，[0<$→pc+o]），并将cond（ifeq）=（[int]，fifeq，[]）排序，如果s=[（int，0）]，则fifeq（g，s，pc）返回（[]，g（0）），否则返回（[]，pc）。对于lookupswitch，g是一个将键值映射到相应地址的函数3.5指令IINC操作码iinc是唯一一条只使用局部变量数组的JVM指令。在我们的形式化中对应的指令是iinc（n，c），其中n是局部变量索引，c是整数值。如果局部变量n是int类型的，根据Javaint算法，它的值增加clvts（n）=（int，m）lvJ=lvts[n←（int，m+intc）]pcJ= next（cmthd，pcts）P @pcts。孟湾cnmts=iinc（n，c）estts= nullP h，ts h，ts[lv lvJ][pc pcJ]n-iinc（3.7）3.6指令get此指令读取堆并修改操作数堆栈。 一般形式get（op，d），其中op是运算符，d包含一个可选的静态参数-一个限定字段名。与前面的规则一样，kindsget（op，d）提供了堆栈上预期的参数类型，要放入堆栈的值类型列表，以及J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）1929× × →►→ ←←× × →typeDgetOpStack Heap OpStack Loc·.函数f试图从堆中读取指定的对象字段或数组单元。 如果它存在，f返回堆栈的修改部分，这是堆中的值。（l，f，lJ）=kindsget（op，d）ostckts=s·rcheck（s，l）sJ=f（d，s，h）sJ∈OpStackostckJ=sJ·rpcJ= next（cmthd，pcts）P @pcts。孟湾cnmts=get（op，d）estts= nullP h，ts h，ts[ostck ostckJ][pc pcJ]n-get（3.8）如果无法获得请求的值，则必须抛出异常（例如， NullPointerException），f返回异常在堆中的位置e，结果求值状态为异常状态。（l，f，lJ）=kindsget（op，d）ostckts=s·rcheck（s，l）e= f（d，s，h）e ∈ Loc·P @pcts. 孟湾cnmts=get（op，d）estts= nullP×h，ts →h，ts[est ←e]exn-get（3.9）3.7指令放置这条指令读取和修改操作数堆栈和堆，而不创建新的位置。指令的一般形式是put（op，d），其中op是运算符，d包含一个可选的静态参数-一个限定字段名。类 型 put （ op ， d） 的 作 用 类 似 于 前 面 的 类 型 ， 具 有 类 型 D put 的 函 数 fOpStack堆堆洛克。 函数f试图修改堆中指定的字段或数组单元。如果指定的项存在并且可能被修改，f返回修改后的堆。请注意，put写入的值不需要立即被其他线程访问事实上，堆的任何部分都可以在程序执行的任何时候与线程缓存同步，并保留Java内存模型约束特别地，类别2值的两个半值可以独立地同步（l，f，lJ）∈kinds（op，d）ostckts=s·rcheck（s，l）ostckJ=r hJ=f（d，s，h）hJ∈HeappcJ=next（cmthd，pcts）P@pc ts. 孟湾cnmts =put（op，d）estts= nulln-放P×h，ts →hJ，ts[ostck ←ostckJ][pc ←pcJ]（3.1030J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）19）J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）1931►→ ←←如果请求的对象不存在，则引发异常（l，f，lJ）∈kinds（op，d）ostckts=s·rcheck（s，l）ostckJ=r e=f（d，s，h）e∈Loc·P@pc ts. 孟湾cnmts =put（op，d）estts= nullP×h，ts →h，ts[est ←e]支出（3.11）3.8新指令这个指令通过创建一个新的位置来修改操作数栈和堆。指令的一般形式是new（op，d），其中op是运算符，d是其参数（整数和类名）的列表该指令的精确含义由函数f给出，该函数f从kindsnew（op，d）中获得，连同堆栈上的预期参数类型和要存储在操作数堆栈上的预期值类型，其实际上总是一个ref类型的值。函数f本身操作堆，分配所请求的结构并返回已分配结构的位置和 新堆的情况下成功，和异常否则.请注意，此指令及其规则与put非常相似。我们更倾向于将两者分开，因为new向堆添加新位置，而put只修改现有位置。（l，f，lJ）=kindsnew（op，d）ostckts=s·rcheck（s，l）ostckJ=sJ·r（sJ，hJ）=f（d，s，h）sJ∈OpStackhJ∈HeappcJ= next（cmthd，pcts）P @pcts。孟湾cnmts=new（op，d）estts= nullP h，ts hJ，ts[ostck ostckJ][pc pcJ]n-新（3.12）（l，f，l，J）=新种类（op，d）ostckts=s·rcheck（s，l）e = f（d，s，h）e∈ Loc·P @pcts. 孟湾cnmts=new（op，d）estts= nullP×h，ts →h，ts[est ←e]3.9指令监视器exn-new（3.13）此指令可以通过尝试获取或释放监视器来修改线程的状态。操作本身是通过修改堆上的对象来完成的。monitor指令期望在操作数堆栈上有一个位置：与所讨论的监视器相关联的对象。指令的一般形式是monitor（op），其中op是enter或exit。32J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）19× × × ×∪−//打开/关闭►→ ←←指令的两种变体都由相同的两条规则处理-一条用于正确操作，一条用于引发 异 常 。这 些 规 则 由 从 kinds monitor （ op ） 获 得 的 部 分 函 数 f ：ThreadIdLocThreadIdN~ThreadIdNLoc 管 理 。 如 果 op = enter ， 则 f（tidJ，s，tid，c）只有在s = null或tid =none或tid=tidJ时才被定义。在第一种情况下，f返回NullPointerException，在第二个（tidJ，1），第三个（tidJ，c+1）。因为f在s时没有定义null并且tidJ=tid=none，即监视器由不同的线程拥有，则在监视器被释放之前不能触发规则。如果op=exit，f在tid =tidJ时返回异常IllegalPointerorStateException，否则返回NullPointerException或（none，0）或（tid，c1），这取决于s和c的值。由于篇幅有限，我们没有正式说明与synchronized方法相关的其他同步操作。然而，请注意，从语法上将一个同步方法转换为一个在开始时具有monitor（enter）并在每个退出点具有monitor（exit）的方法f=kindsmonitor（op）ostckts=s·r s∈Loc(tidJ，lcountJ）=f（tidts，s，h（s）@tid，h（s）@lcount）tidJ∈ThreadIdlcountJ ∈NpcJ=next（cmthd，pcts）ostckJ=rhJ=h[s <$h（s）[tid <$tidJ][lcount<$lcountJ]]P@pc ts. 孟湾cnmts =monitor（op）estts= nullP h，ts hJ，ts[pc pcJ][ostck ostckJ]n-监视器（3.14）f=kindsmonitor（op）ostckts=s·r s∈Loce=f（tidts，s，h（s）@tid，h（s）@lcount）e∈LocP@pc ts. 孟湾cnmts =monitor（op）estts= nullP×h，ts →h，ts[est <$e]exn-监视器（3.15）3.10指令调用该指令修改操作数堆栈、方法帧堆栈并读取堆。指令的一般格式是invoke（mode，cnm，mnm），其中mode是接口、特殊、静态或虚拟中的一种，cnm和mnm是应该被调用的方法的类和方法名这个指令的主要动作是找到方法代码，准备新的方法框架，并将执行传递给新的方法实例。 为此，从kindsinvoke（mode，cnm，mnm）读取堆栈上预期值的类型l以及方法lJJ. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）1933►→←►→←然 后 从 方 法 签 名 中 读 取 它 们 。列 表 lJ 的 长 度 最 多 为 1 。接 下 来 ， 执 行dispatchdispatch函数也可以返回异常。n-invoke规则的其余部分用于准备新方法框架：函数initlv在拆分long和double类型的值并执行必要的浮点值集转换后，将来自堆栈的参数放入新框架的局部变量表中[12，Section 3.8.3]。最后，新的方法框架被放到方法框架栈上，初始操作数栈为空，pc=0。这里不处理同步方法，但请参见第3.9节结束（l，lJ）=kindsofinvoke（mode，cnm，mnm）ostckts=s·rcheck（s，l）cnmJ=dispatch（mode，cnm，mnm，s，h）tfsJ=tfsts[ostck←r]lvJ= initlv（lvlength（P @mnm.cnm），s）tfsJJ=cnmJ，mnm，lvJ，[ ]，0·tfsJP@pc ts. 孟湾cnmts=invoke（mode，cnm， mnm）estts= nullP h，ts h，ts[tfs tfsJJ]n-调用（3.16）（l，lJ）=kindsofinvoke（mode，cnm，mnm）ostckts=s·r check（s，l）e=dispatch（mode，cnm，mnm，s，h）e∈LocP@pc ts. 孟湾cnmts=invoke（mode，cnm， mnm）estts= nullP h，ts h，ts[este]exn-调用（3.17）3.11指令返回此指令从当前方法返回。它读取操作数堆栈，并通过删除当前帧和更新前一帧来修改方法帧堆栈：将pc移动到下一个指令（通常在调用指令上），并在转换后通过推送返回值来更新操作数堆栈。该指令的一般形式是return（l），其中l是长度最多为1的类型列表尽管[12]没有明确说明这一点，但我们决定添加规则n-term-return，处理终止对应的方法34J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）19►→←帧堆栈上的最后一帧这些规则不处理退出同步方法时释放监视器的问题。但是，这可以通过在每个返回语句之前放置一个monitor（exit）指令请参见第3.9节的讨论。ostckts=s·rcheck（s，l）tfsts= f1·OstckJ，mnmJ，lvJ，ostckJ，pcJ，tfstailf1∈MethodFrametfsJ= Ostck J，mnmJ，lvJ，vsc（s）·ostckJ，next（P @mnmJ. cnmJ，pcJ）n·tfs尾P @pcts. 孟湾cnmts=return（l）estts= nullP h，ts h，ts[tfs tfsJ]n-返回（3.18）ostckts=s·rcheck（s，l）tfsts=[f] f∈MethodFrametfsJ=[] tstatusJ=已删除P@pc ts. 孟湾cnmts =return（l）estts= nulln项收益P×h，ts→h，ts[tfs <$tfsJ][tstatus<$tstatusJ]（3.19）3.12指令抛出此指令不带参数，它从堆栈中读取并删除异常的位置，并更改当前线程的求值状态（规则ex-throw）。在我们的语义中处理异常的方式如下。 每个线程的求值状态（est）组件表示当est= null时执行是否处于正常状态，否则处于异常处理状态。请注意，切换到后一种状态不仅可以通过执行throw指令来完成，还可以通过抛出异常（例如， NullPointerException）。 如果est = e是一个有效异常的位置，那么剩余的规则ex-in-handle、ex-out-handle或ex-term-handle都可以被触发，这取决于异常是在当前方法中处理还是引起它的突然终止。在后一种情况下，ex-term-handle规则处理当前方法是方法帧堆栈上最后一个方法的特殊情况。 这个规则在[ 12]中没有直接的对应关系，就像规则n-term-return一样。没有处理的特性是当一个同步方法被异常突然终止时释放监视器。但是请注意，这可以通过添加一个捕获所有异常处理程序来模拟，该处理程序将执行指令监视器（退出），然后重新抛出异常。 另见结尾处的讨论第3.9节。J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）1935►→ ← ←←tsostckts=e·r e∈Loc·P@pc ts. 孟湾cnmts =throwestts= nullP×h，ts →h，ts[est <$e]ex-throw（3.20）ostckJ=[e]（pcts，h（e）@cnm）∈ dom（P @etable.孟湾cnmts）pcJ= P @etable. 孟湾cnmts（pcts，h（e）@cnm）estts=e∈Loc·P h，ts h，ts[ostck ostckJ][pc pcJ][estnull]ex-in-handle（3.21）（pcts，h（e）@cnm） /∈dom（P @etable. 孟湾cnmts）tfsts=f1·f2·tfstailf1，f2∈MethodFrameestts=e∈Loc·P×h，ts→h，ts[tfs ←f2尾伸出柄·tfsts]（pcts，h（e）@cnm）/∈ dom（P @etable. 孟湾cnmts）tfsts=[f]f∈MethodFrameestts=e∈Loc·（3.22）P×h，ts →h，ts[tfs <$[ ] ][tstatus<$ATED]ex-term-handle（3.23）3.13无语义一些指令的功能不能通过运行时结构的语义转换来表达，因为它们的含义在JVM规范中没有描述[12]。它们是断点、impdep1、impdep2和带有操作码186的指令。7因此，本文将其省略。操作码宽度与非宽度操作一起考虑4结论我们已经提出了一个简洁的形式化的JVML，原来是factoris-能够到12指令助记符。这是可能的，因为我们分离了许多指令的通用操作，并将单个操作码的特定行为列表化通过这种方式，我们严格地降低了整个语言的整体复杂性，而没有显著牺牲其功能。引用[1] 阿特基河，CoqJVM：Java虚拟机的可执行规范，使用依赖类型，在：M。米库兰岛Scagnetto和F.36J. Chrza Beszcz等人理论计算机科学电子笔记264（4）（2011）19Honsell，editors，Types for Proofs and Programs，International Conference，TYPES 2007，Cividaledes Friuli ， Italy ， May 2-5 ， 2007 ， Revised Selected Papers ， Lecture Notes in Compu