（计算机软件与理论专业论文）类型化低级语言的扩展.pdf

中国科学技术大学硕士学位论文 摘要 摘要 由于i n t e m e t 的爆发式增长和广泛应用，移动计算吸引了越来越多的关注， 在这个领域中程序的安全问题显得至关重要。当用户从网上下载一段代码( 浏览 器插件，j a v a 小程序) 到主机上，总是希望它的运行不会危害主机。检验并执行 从网络获得的移动代码的j a v a 虚拟机正是一个典型的例子。用形式化的方法在软 件开发过程中进行严格推理是提高软件质量的根本途径。在众多的形式化方法中， 近十年来从程序设计语言的角度来支持软件开发的研究引起了广泛的关注。基于 语言方法的优点在于从程序基础出发考虑软件安全，有利于减小运算系统的需信 任计算基础、描述较小粒度的安全策略。 本文的工作基于i n t e l 的开放式运行平台( o p e nr u n t i m ep l a t f o r m ，简称o r p ) 。 提出了对类型化低级语言语言( t y p e dl o w l e v e l l a n g u a g e ，简称t l l ) 的扩展， 将利用类型信息所带来的类型安全性带到接近于汇编语言的一层。前期的工作支 持了j a v a 虚拟机语言( j a v av i r t u a lm a c h i n el a n g u a g e ，简称j v m l ) 的一些基本特 性：单类继承，数据和方法类成员描述符，数组操作等。本文的工作将完成对j v m l 如下特性的扩展；静态成员，接口多继承，动态下溯( d y n a m i c a ld o w n c a s t ) 。 首先，在实现t l l 的过程中，发现从j a v a 到字节码( b y t e c o d e ) 的翻译过程中 丢弃了部分类型信息。在设计中，不仅要保持字节码中现有的类型信息，而且要 从中推导出丢失的类型信息。本文针对些难解问题提出了重建算法。 在研究工作中发现，j a v a 对象的接口方法调用中包含了一种特殊类型调度 ( t y p ed i s p a t c h ) 过程。本文还提出了个对接口多继承的新编码方案。类型调 度是高层语言中常见的动态类型分析机制。当涉及到类型调度结构的翻译时，从 j v m l 到t l l 的翻译变得更复杂。t l l 中引入了一种新型的标签类型，这种类型 的值能够用来标注一类具有相同结构的类型的值。利用这种标签类型t l l 能够有 效地实现j a v a 字节码中接口多继承翻译， 最后，在j a v a 虚拟机的实现中，经常需要调用一些用本地代码编写的例程用 以进行某些底层的操作，这种方法不仅扩大了需信任计算基础( t r u s t e dc o m p u t i n ! 里型兰垫查查兰堕圭堂生丝苎 塑萋 b a s e ，简称t c b ) ，而且语言间的差异造成了优化上的一些困难，为此，本文的 t 作中应用了一种新的解决方法，构造m a g i cc l a s s ，直接用t l l 代码实现某些 例程，使之能通过t l l 类型检查器的检查，缩小了t c b 。 本课题得到国家自然科学基金项目( 6 0 1 7 3 0 4 9 ) 和i n t e l 中国研究中心资助。 关键词：软件安全，程序验证，需信任计算基础，类型安全，类型安全语言，j a v a 虚拟机，类型保持翻译，对象编码，类型调度 i i 中国科学技术大学硕士学位论文 a b s t r a c t a b s t r a c t t h ee x p l o s i v eg r o w t ho fi n t e r n e th a si n d u c e di n t e r e s ti nm o b i l ec o m p u t a t i o nf o r p r o g r a m m i n gt h ew e b ”i nt h i sd o m a i n ，t h es a f e t ya n ds e c u r i t yp r o p e r t i e so f p r o g r a m s a r em o r ec r u c i a lt h a ne v e rb e f o r ew h e nu s e r so b t a i nap i e c eo fs o f t w a r ef r o mn e t w o r k ， t h e ym i g h tl i k et oa s c e r t a i nt h a ti t i ss a f et oe x e c u t eas a f em o b i l eh o s ti so n et h a t p e r m i t su n t r u s t e ds o f t w a r et o r u nw h i l eg u a r a n t e e i n gt h e s eu n t r u s t e dc o d e so b e ya g i v e ns e c u r i t yp o l i c y a n dj a v av i r t u a lm a c h i n ej u s ti sa l l e x a m p l eo fas a f e h o s t a m o n gv a r i o u sf o r m a lm e t h o d s ，l a n g u a g e b a s e da p p r o a c ht o s o f t w a r es e c u r i t yh a s a t t r a c t e dw i d e s p r e a da t t e n t i o ni nt h ep a s td e c a d e l a n g u a g e b a s e da p p r o a c h e ss t a r t f r o mt h eb a s eo fs o f t w a r e ，t h a t i s ，p r o g r a m m i n gl a n g u a g e a n d c o m p i l e r t h e s e a p p r o a c h e sh e l pr e d u c et h et r u s t e dc o m p u t i n g b a s eo fs o f t w a r es y s t e m s ，a n dd e s c r i b e f i n e g r a i n e ds a f e t yp o l i c i e s o u rw o r kb a s e do nt h ei a t e lo p e nr u n t i m ep l a t f o r m ( o r p ) a n dp r o p o s e dt h e e x t e n s i o n st ot y p e dl o w l e v e ll a n g u a g e ( 叫，d e s i g n e dt ob r i n gt y p es a f e t yt o a l e v e lc l o s et oa s s e m b l el a n g u a g et h ef o r m e rw o r ks u p p o r t ss o m ef e a t u r e so fj a v a v i r t u a lm a c h i n e l a n g u a g e ：c l a s s e s ，i n h e r i t a n c e ，d a t a a n dm e t h o dc l a s sm e m b e r d e s c r i p t o r s ，a r r a ym a n i p u l a t i o na n ds oo n t h ew o r ko ft h i st h e s i sw i l lf i n i s ht h e s u p p o r t t ot h e f o l l o w i n g f e a t u r e ：s t a t i c m e m b e r s ，m u l t i - i n h e r i t a n c e ，d y n a m i c a l d o w n c a s t w h e ni m p l e m e n t i n g t l l ，af a c t w a sf o u n dt h a ts o m e t y p e i n f o r m a t i o nh a v e b e e n a b a n d o n e da f t e rt r a n s l a t i o nf r o mj a v at o h y t e c o d e i nt h i si m p l e m e n t a t i o n ，n o to n l yt h et y p e i n f o r m a t i o nk e p ti nb y t e c o d ew a sm s e r v e d ，b u ta l s ot h o s et h a th a db e e na b a n d o n e dw e r ei n f e r r e d t h i st h e s i sd e s c r i b e ss o m eb a s i c q u e s t i o n s a b o u tt y p e r e e u n s t r u e t i o n , a n dp r o p o s e ss o m c a l g o r i t h m s w ef o u n dt h a tt h e r ew a sas p e c i a lt y p ed i s p a t c hw h e na ni n t e r f a c em e t h o dw a s i n v o k e dt h i st h e s i sp r o p o s e dan e we f f i c i e n te n c o d i n gm e t h o do f m u l t i i n h e r i t a n c eo f m ! 里型堂垫查查堂婴主兰篁笙兰 垒! ! 竺! 竺 i n t e r f a c e t y p ed i s p a t c h i n gi s ac o m m o nm e c h a n i s mu s e di nh i g h - l e v e ll a n g u a g et o a n a l y z et y p e sd y n a m i c a l l yt h e t r a n s l a t i o nf r o mj v m lt ot l lb e c o m e sm o r ec o m p l e x w h e n t y p ed i s p a t c h c o n s t r l l e t sa r e i n v o l v e dw h i c ha r e i m p l e m e n t e d w i t h t a g m e c h a n i s man e w t a gt y p ei si n t r o d u c e di n t ot l lat a go f t h e s et y p e sc a n b eu s e dt o a t t a c h et oak i n do fv a l u e sh a v i n gt h es a m et y p es t r u c t u r et l l c o n t a i n i n gt h i st y p ei s a b l et oe f f i c i e n t l yi m p l e m e n ti n t e r f a c ei n v o k a t i o ni nj a v aw i t ht h et a gt y p et l l st y p e s y s t e mi sa b l e t oa s s u r et y p ed i s p a t c h i n gi sr e l i a b l eb y c h e c k i n g w i t h t y p i n gr u l e s i nt h ei m p l e m e n t a t i o no fj a v av i r t u a lm a c h i n e ，s o m ep r o g r a m sw r i t t e ni nn a t i v e c o d ea r en e e d e dt od os o m eo p e r a t i o n so nt h el o wl e v e lh a r d w a r e st h i sm e t h o dn o t o n l ye n l a r g e dt h e t r u s t e dc o d eb a s e ( t c b ) ，b u ta l s oc a u s e dal o to ft r o u b l et o o p t i m i z a t i o n t h i st h e s i sp r o p o s e d an e wm e t h o d ，w i t ha m a g i cc l a s s t h o s ep r o g r a m s w i l lb ew r i t t e ni nt l l d i r e c t l ya n dc h e c k e db y t l l t y p ec h e c k e f t h i sr e s e a r c h p r o j e c t i s s u p p o r t e db y n m i o n a ln a t u r a ls c i e n c ef o u n d a t i o n ( 6 0 17 3 0 4 9 ) a n di n t e lc o r pc h i n ar e s e a r c hc e n t e r k e y w o r d ：s o f t w a r es a f e t y , p r o g r a mv e r i f i c a t i o n ，t r u s t e dc o m p u t i n gb a s e ，t y p es a f e t y , t y p e - s a f el a n g u a g e ，j a v a v m u a l m a c h i n e ，t y p e - p r e s e r v i n gc o m p i l a t i o n ，o b j e c t e n c o d i n g ，t y p ed i s p a t c h 中国科学技术大学硕士学位论文 第一蕈绪论 1 1 研究背景和意义 第一章绪论 由1 二i n t e r n e t 的爆发式增长和广泛应用，移动计算吸弓f 了越来越多的关注， 在这个领域中程序的安全问题显得至关重要。当用户从网上下载一段代码( 浏览 器插件，j a v a 小程序) 到主机上，总是希望它的运行不会危害主机。一一个安全主 机( s a f eh o s t ) 应该能够拒绝可能会破坏主机的代码，而允许那些符合一定的安 全策略的不信任方代码在其上运行。检验并执行从嚼络获得的移动代码的j a v a 虚 拟机正是一个典型的例子。这样的安全主机一方面要对外来的代码进行检验，以 保护自己；另方面它对安全与否的判断又依赖于对某些代码( 代码检验程序) 的信任。蔫信任计算基础( t c b ) 这个概念通常被用来评价一个系统的易被攻击 性。t c b 指的是实现系统的代码中不能证明为安全而不得不给予信任的那些部 分。这就意味着t c b 中可能含有安全漏洞系统的安全依赖于t c b 中代码的正 确性。一个系统的t c b 包含的代码越多，可能存在的安全闻题就越多，因而被击 破的可能性就越大。一个j a v a 虚拟机的实现通常包含了大量的代码，它的各个部 分，例如即时编译器( j u s t i n t i m ec o m p i l e r ，简称j i t ) ，垃圾收集器通常部含 有近万行代码。在大多数j a v a 虚拟机的实现中，这些代码都包含在t c b 之内。 在过去的十年中。出现了许多利用基于语言的技术来确保低级语言代码安全 性的研究。其中较具影响的研究包括携带证明代码( p r o o f - c a r r y i n gc o d e ，简称 p c c ) n e c u l a 9 7 ，类型化汇编语言( 母p e da s s e m b l yl a n g u a g e ，简称t a l ) f m o r r i s e t t 9 9 ，和商阶类型化语言f l i n t s h a 0 9 7 。它们表明了利用类型和逻辑能 够有效地验证代码的安全性质。p c c 使用种通用逻辑来表示机器代码的安全属 性及其证明，通过对证明的验证来确保对应的机器代码是满足代码消费者定义的 安全策略的。t a l 的类型系统保证那些通过类型检查的良类型的汇编程序不会出 现意想不到的错误彳亍为。基于p c c 思想构造的一个j a v a 程序运行系统的t c b 只 包含了不到2 7 0 0 行代码 a p p e l 0 2 ，而t a l 也将编译器排除出t c b 。这些工作的 中国科学技术大学硕士学位论文 第一章绪论 共同之处是：通过验证编译器将从源程序获得的有用信息以不同的表示形式( 逻 辑谓词、类型注释) 保持到目标代码中，这些信息将被用于目标代码安全属性的 验证。 出于同样目的，我们设计了一种用于j a v a 虚拟机的类型化低级语言( t y p e d l o w - l e v e ll a n g u a g e ，简称t l l ) ，作为j i t 编译器的中间语言。在现有的j a v a 虚 拟机上，将j a v a 虚拟机语言( 简称p c m l ，又称j v m 字节码) 程序翻译成本地 机器代码在字节码验证之后，它并不能保证经过验证的属性在翻译过程中能够得 到保持，因此j i t 在j a v a 虚拟机系统的t c b 中。使用t l l 可以降低代码验证的 层次，同时也减小了虚拟机的t c b ，因为j i t 的前端可以排除出t c b 。我们基于 i n t e l 的j a v a 虚拟机实现，开放运行平台( o p e nr u m i m ep l a t f o r m ，简称 o r p i n t e l o r p l ) ，构建了一个用t l l 作为验证语言的t 编译器。由于t l l 的低 级和通用性，使o r p 有可能成为支持多种语言程序验证和运行的平台。 在第一期的工作中，我们的实现基于j v m l 的一个精简子集，j v m l 。，支持 若干基本特性，如数组，单继承等。在即将介绍的扩展版本的实现中，我们将增 加对静态成员，接口多继承，动态下溯( d y n a m i c a ld o w n c a s t ) 的支持。 在下一节我们将介绍目前在这个领域的研究现状。 1 2 研究现状 为了实现对t l l 的扩展，首先的问题就是从j a v a 到字节码的转换中编译器丢 失了一些方法内部的局部类型信息，而在我们设计的t l l 指令中，每一个操作数 都有确定的类型信息。t l l 不仅保持了字节码中现有的类型信息，而且还包括了 从字节码中推导出的被丢弃的类型信息，比如局部变量和操作数栈的类型。在建 立类型化的中间表示时，就是要通过数据滤分析，由动态类型重建这些源代码中 的静态类型信息。 为了实现对类型转换和多继承的支持，动态类型分析是非常重要的，g l e w 提 出的标签机制对我们项目组的工作有重要启发作用。 2 中国科学技术大学硕士学位论文 第一章绪论 1 2 1 类型重建 为j a v a 虚拟机平台设计一种类型化的、更底层的中间语言吸引了很多研究兴 趣。例如y a l ef l i n t 项目，c o r n e l lt a l x 8 6 ，以及m i c r o s o f tm a r m o t 。为了建立i r 的类型信息，这些中间语言的前端设计都涉及到t b y t e c o d e 的类型重建。如 【c h i t s 0 1 ，【g h 0 0 ，【m a r m o t 9 9 。这些重建过程基本上都是先将栈式的b y t e c o d e 转换为传统i r ( 五t ! j i m p l e ，m a r m o t 中的j i r ，f l i n t 中的2 j v m l ) ，然后通过数据 流分祈收集类型约束，最后类型重建。但是它们在类型表示，类型约束表示以及 重建算法上都有所不同。 【g h 0 0 】为y v m l 中的局部变量推导静态类型。它们以有向图的形式表示类型 约束关系，并通过三步算法为局部变量推导静态类型。它不使用特定的s s a ，所 以他们也必须要分离变量的每次赋值。由于不支持集合类型，为了解决接口的多 继承闯题，必须插入显式的类型转换。 f l i n t 项目 c h r i s 0 1 中，将b y t e c o d e 转换为函数式j v m ，经过了：基本块划分， 为每个程序点推导局部变量以及栈位置的类型，最后转换成a j v m l 。这种方法引 入厂集合类型 i n t p t ，c o o r p t l ，通过符号执行传播类型信息。为类的初始化使用 r 一一个额外类型c o 。但这种方法没有为小整型重建类型。 m a r m o t 9 9 的类型重建过程如下：对省略的类型收集类型约束，得到了对于二 方法所有类型变量的类型f l o w 约束系统。这个系统将约束分解成强关联的元素， 并接深度优先的顺序解决每个成员。这样得到的类型化中间语言所有的变量都是 有类型的，所有的c o e r c i o n 和转换都是显式的，所有的操作符的重载都被解析过。 但是这种类型重建建立在特定的s s a 上，也就是说先要把b y t e c o d e 转换成一般的、 带有临时变量的瓜，然后再转换成s s a 的形式才能做类型重建。并且由于在类 型重建中使用了子定型完全( s u b t y p ec o m p l e t i o n ) 的技术，有时为了使类型偏序 集合形成类型格( t v p el a t t i c e ) 、每两个接口都有l u b 和g l b ，会加入新类型并 改变接口的继承关系。所以这种类型重建不适合用在有动态代码优化的v m 上。 中国科学技术大学硕土学位论文 第一章绪论 1 2 2 动态类型分析 在文章( ( t y p ed i s p a t c hf o rn a m e d h i e r a r c h i c a lt y p e s ) ) 中，g l e w 总结了在不 同语言中的各种类型调度实现，并提出了标签机制。g l e w 的标签语言能够很好地 实现各种具有层次结构的类型调度结构。用于类造型中的标签就是典型的具有层 次结构的标签：与标签( 类) 联系的是该标签相应类型及其子类型( 类及它的子 类) ；进行标签比较时则不仅仅是比较值的标签与已知标签是否相等，而是还比较 值的标签是否是己知标签的子标签。g l e w 的标签类型形如t a 酽0 ， ； ) 。它具有 三种不同的标志：若中= + ，该类型的值可以作为r 子类型的值的标签；若中= ， 则该类型的值可以作为r 父类型的值的标签；若( p 一，那么只能作为r 类型的标 签。这些标签类型能够有效地实现对象的类标签。他的解决方案还被用于t a l 对 面向对象语言的类型保持翻译 g l e w 0 0 。我们的低级语言t l l 也引入了这种标 签来实现j a v a 的向下造型表达式。 除了g l e w 的工作之外，c r a r y 和w e i r c h 也为动态类型分析作出了重要的贡 献。他们设计的语言h 【c r a r y 9 9 及在后继工作中设计的l x c r a r y 0 2 能够将运行 时类型信息表示成一般的项。在类型制导的编译中( t y p e d i r e c t e dc o m p i l a t i o n ) 这些语言可以用于分析上下文中静态无法确定的类型信息( 包括实现本文中提到 的基于标签机制的类型分析) ，并把这些信息用于代码的优化和转换。他们的语言 具有一般性，但是也相对复杂，每一种类型和每一种类型构造符都有唯一的项对 应。与他们的工作相比，g l e w 的工作更具有针对性。标签语言和标签类型针对具 有明显特征并且广泛用于各种高级语言的类型调度结构提出。而本文在他的工作 基础上对标签的表现能力上作了补充，使标签能够标注具有一类相同结构的类型 的值。 l e a g u e 用f l i n t 实现的j a v a 编译器 l e a g u e 0 2 是一个具有相当影响的类型保 持编译器。在他的工作中对接口方法调用的处理和本文中提到的并不相同。一个 类实例被当作接1 2 1 实例时，例如第2 节程序中r e c t a n g l e 类对象被传给形参为 s c a l a b l e 的函数s c a l es h a p e ，这个实例被重新包装为具有唯一接口方法表的接口 4 中国科学技术大学硕士学位论文 第一章绪论 实例。这种处理方法事实上是生成了一个新实例，它的实例数据和原实例丰h 同， 不同的是提取了相应方法形成接口方法表。因此在调用接口方法时，同一接口实 例的接口方法表的位置是固定的。这种处理方法将会产生大量的临时对象耗费空 间。 另一种处理方法就是把类的所有接口方法表都放到一个无顺序元组中。无顺 序元组的域选择和顺序元组中的相应操作类似，但是需要编译器来实现运行时查 找。这仍然是一个较高级的语言抽象，与验证编译器希望在较低级层次上翻译高 级语言程序的目的不符合。 1 3 本文主要工作和创新点 本文研究工作的重点是扩展设计类型化低级语言做为即时编译器的中间语 言，并实现相应的编译器前端。涉及的内容包括类型安全的概念、类型化方法的 目的和意义、类型化方法的应用、类型化低级语言的形式化描述、对象编码、从 j a v a 虚拟机语言到类型化低级语言的翻译环境、对方法的翻译、类型表达式的表 示法和类型操作等。在研究过程中，笔者对大量相关研究文献进行了分析理解， 为类型化低级语言的设计提出若干设想，负责其中的标签类型的设计，对象编码 的修改，对相关函数的翻译等工作。并做为主要人员参与了扩展以t l l 为中间语 言的即时编译器的前端实现工作。 本文的章节安排、具体工作和创新点如下： 第一章介绍了类型化方法的背景，类型化方法的特性以及它的研究手段和意 义。简要介绍我们即将对t l l 所作的扩展，以及目前相关领域的研究现状。做为 本文研究工作的基础。 第二章介绍了t l l 项目的前期工作，给出t l l 的形式化描述，包括语法形 式，操作语义规则和静态语义规则。文中对组成1 1 工程序的四个要素，堆，变量 表，寄存器文件和全局变量声明和指令序列都进行了详细的描述；解释t l l 的类 型系统，包括堆值类型，类型强制和复杂类型等。 第三章在实现t l l 的过程中，我们发现从j a v a 到字节码( b y t e c o d e ) 的翻译过 中国科学技术大学硕士学位论文 第一章绪论 程中丢弃了部分类型信息。在我们的设计中，不仅要保持字节码中现有的类型信 息，而且要从中推导出丢失的类型信息。因此我们针对一些难解问题提出了重建 算法。 第四章在研究工作中发现，j a v a 对象的接口方法调用中包含了一种特殊类型 调度( t y p ed i s p a t c h ) 过程，为此，我们设计了一种新的标签类型及相应的编码 方案用以解决带有接口的对象编码问题。 第五章在j a v a 虚拟机的实现中，经常需要调用一些用本地代码编写的例程 用来进行某些底层的操作，这种方法不仅扩大了t c b ，而且语言间的差异造成了 优化上的一些困难，为此，我们提出了一种新的解决方法，构造m a g i cc l a s s ，直 接用t l l 代码实现某些例程，在本章中将对这种方法有详细地描述。 中国科学技术大学硕士学位论文 第二章类型化低级语言介绍 第二章类型化低级语言介绍 2 1t l l 的提出 因为类型化方法的各种优点，所以考虑将类型化技术应用到现存的某个具体 的j a v a 虚拟机实现上，整合类型化中间语言技术到该虚拟机的即时编译器 ( j u s t i n t i m ec o m p i l e r ) ，以获得类型化技术给我们带来的种种好处。根据这个 想法，本项目组提出了类型化低级语言( t y p e dl o w l e v e ll a n g u a g e ) ，一个接近 汇编语言层的低级语言。我们探索使用t l l 作为该虚拟机的通用中间语言的可能 性，目的是为了支持多种高层语言，并尽量缩小它的可信任计算基。 我们的工作实现了对j a v a 虚拟机语言( 简称j v m l ，又称j v m 字节码) 的 一个精简子集j v m l o 的支持。本章首先将简要的介绍j v m l o ；并将形式地描述 目标语言t l l 的语法、操作语义和定型规贝a ( t y p i n gr u l e ) ；最后简要介绍从j v m l o 到t l l 翻译过程中使用的方法。 2 2 源语言j v m l o c l a s sc i d s u p e r c l a s s ：c l a s ss c ； 【f i e ld i ：t y p e i 【m e t h o d t ： a r g j ：t y p e j - t y p e a ：b o d y ：】 1 f i e l d d e s c r i p t o r s j , m e t h e o d d e s c r i p t o r s ， 耐p e ：2 c l a s s d i i n t i l o n g i f l o a t ld o u b l e fb o o l | 【b p e b o d y ：= l l n s t + i n s t ：2 p o pj p o p 2 p u s h fd u p i t _ m o p i t _ l o a da i lts t o r e 托jl d c l i i n c i 图21j v m l o 的语法图 7 中国科学技术大学碗士学位论文第二章类型化低级语百介绍 我们选择了j v m l 的一个子集作为t l l 的源语言，称之为j v m l o 。它包含 了j a v a 虚拟机语言的基本特征：类，继承关系，类成员描述符( 包括普通数据成 员和方法成员) ，由j v m l 的指令序列组成的方法体等。在j v m l o 中没有得到支 持的j a v a 虚拟机语言的特征主要有：静态成员，访问控制，接口，动态下溯 ( d y n a m i c a ld o w n c a s t ) ，异常等。它们中的大多数在可预见的将来是可以得到支 持的。比如实现对静态成员的支持，只需要在现有的t l l 框架上做一个简单的扩 展。然而，有些语言特征，如异常，就比较难以在t l l 中实现。目前并没有合适 的想法去实现它们，这些都是将来需要进行努力的的方向。图中列出了源语言 j v m l o 的语法形式。 2 3 类型化低级语言t l l 胁n d s t y p e s 1 ( ：2 t ir o w fn u mjk i k 2 t ：= 口l c i f f 1 1 il n l v 群：r 兰t lt2 l m 口：r t i3 c t ：茁t 1 t 2 s m a l lv a l u et y p e sc ：= i n t1 1 c l x c | l c ir e f t ( ? ) + ln u l ll s i n t ( t ) l a r r a y ( t ，c 1 r e g i s t e r f i l et y p e sr ：= v 三? = 誊。c ) + ) h e a p v a l u e t y p ef ( p = + | - c o e r c i o n s 8 ：= t 】ir o l l 。lu n r o l l 。le p a c k 。 t ，v 】 g l o b a l v a r i a b l e s g ：2 xc = w ix = f n l a l ( c l c 。) ：c i ) i n s t r u c t i o ns e q u e n c e ：1 ：= 旺：r ) + l ；i 1h a l tir e t u r nr i 2b o p r l ，v l ，v 2 a s s i g n v l ，v 2l j m p t 弘lb _ c o nr ，三【t 】 l c a l lr ，v t 】，v 1 ，v n le o p e n a ，r ，v | h a l l o c r ，v ，t f h r e a dr ，v i ，v 2 ih w r i t e v l ，r ，v 2 ja r r l o a dr l ， v ，i 2 a n s t o r e l 1 ，v ，r 2l s a f e s u br 1 ，r 2 ，l l o p e r a n d sv ：。w ir ix i6 v 】 w = c o n s t l ，j6 w l n s t ：= o f f r = r l ir 2 卜 r e g i s t e r b l e sr ：2 。l w 】， ，r n w 。) v a r i a b l e st a b l e se ：= x x w l ， ，x n w n1 图22t l l 的语法图 t l l 语言比j v m l 语言更接近机器代码，但为了兼顾表示的简洁性及j i t 编 中国科学技术大学硕士学位论文 第二章类型化低级语言介绍 译模式的需要，它又保持了某些高级语言的特征。一个t l l 程序大致可以描绘为： 若干个全局变量声明了函数和静态分配的数据；函数由指令序列构成，t l l 指令 类似用于大多数编译器的三地址中间指令；全局变量、函数以及函数内跳转目标 标签有显式的类型标注。些j i t 编译器中间语言也保留了部分j a v a 源程序类型 信息。与它们不同，t l l 的类型系统采用了从系统f ( s y s t e m f ) 演化而来的高阶类 型系统。这样的高阶类型系统更具有一般形式，能够表示多种高级数据抽象和安 全属性，为使t l l 能够面向多种源语言提供了基础。本节余下内容将形式地描述 t l l 。 一个t l l 程序是一个四元组，包括堆h ，变量表e ，寄存器文件r ，以及 个全局变量声明和指令序列( g ；i ) 。程序中函数的定义是全局性的，所以它们也 可以被看做是全局变量。 堆珏由标签h 到堆值( 数据块和代码块) 的映射来表示。其中数据块被划分 为数个以偏移量z 做索引的堆槽( s l o t ) 。每个堆槽含有一个字值w 或者一组连续 的具有相同类型的字值 w t ，w n 。我们使用w 来表示一个字节，字和双字的 值。变量表e 由变量x 到字值w 的映射来表示。一个声明g 将给e 增加一个新 的全局变量，同时给这个新的全局变量赋以初值w 。如果这个全局变量是一个函 数，那么映射对应的值就是相应指令序列的代码入口。寄存器文件r 由虚拟寄存 器r 到字值的映射来表示。局部变量定义和t l l 指令序列构成了函数体。局部变 量通常是寄存器分配的，所以也称它们为虚拟寄存器。在t l l 抽象机中，寄存器 的数目假定是无限的。我们使用寄存器来存储计算的中间结果，它们也是物理寄 存器的候选者。 t l l 指令集包括基本的赋值指令，二二元算术指令和分支指令。一个t l l 指令 包含一个操作码，指定这个指令要执行的操作。操作码后面跟数个操作数，是操 作执行的载体。操作数由单值v ( s m a l lv a l u e ) 表示。单值包括字值，寄存器，全 局变量或者个被强制的值。单值的对立面就是堆值，它是单值的元组，占据了 堆上的一块内存空间。 t l l 指令比j v m l 的指令更接近本地代码。例如，在t l l 指令集中，有堆值 操作指令b a l l o c ，h r e a d 等等，它们代替了j v m l 中的对象n e w 和成员访问指令。 9 生望型兰垫查盔堂堡圭兰堡堕茎 兰三皇鲞型些堡丝堕亘! ! 塑 用通用的c a l l 指令代替了j v m l 中各种各样的方法调用指令。因此t l l 指令也比 j v m l 指令更加通用一些，用t l l 指令实现不同源语言的基本操作是很方便的。 同时，t l l 指令比汇编指令要高层一些。有些高层的抽象，如函数，数组还是保 留下来了。 指令c a l l 后面跟着一个参数列表，在本地代码中，它将被扩展为一系列p u s h 操作和一个跟具体编译器的调用惯例一致的调用指令。分支指令，也叫作控制流 指令，i m p ，bc o n ，等等是用来转换函数运行路径的。这些指令的操作数是函数 内标签，它是一个指令序列的入口位置，这个指令序列以i m p 或者r e t u r n 终止。 函数内标签用标签类型标识，这个类型是一系列( 寄存器，类型) 对。一个标签 函数被看做是后续指令序列的前条件。a r r l o a d ，a r r s t o r 是数组访问指令。s a f e s u b 指令则被用来执行数组越界检查。另外，t l l 指令集中还有一些指令跟类型操作 有关，例如e o p e n 指令就是用来打开一个存在包( e x i s t e n t i a lp a c k a g e ) 的。 2 4j v m l o t l l 翻译器 2 4 1 类和对象的布局( o b j e c tl a y o u t ) 图23 类和对象的布局 在t l l 的翻译中，类和对象具有如图这样的布局，比起o r p 现有的类和对 象的布局，主要的区别在方法表和类布局上。为了不影响其它不在j v m l 。中代码 ( c l a s s 库文件) 的执行，我们在o r p 原有的布局上安排我们的数据结构。 类存放了相同对象公共数据，也为创建类实例提供了一个模板。在我们的数 据布局中方法表v t a b l e 的指针以及静态数据体现了类的前一个特征，而n e w 和 闺圉 j 月 一 嘶 一萤 中国科学技术大学硕士学位论文 第二章类型化低级语i 介绍 函数则实现了类的后一种功能。在源程序中类还记录了类各种属性：继承信 息，域的访问控制，以及成员的类型。因此我们把类的信息分成两类；一类是“静 态”的信息，它们是编译器需要关心和操作的信息，用来进行些编译前的静态 判断和识别，例如类型继承关系；而另外一类则是运行时数据，在程序运行时访 问操作的数据和代码，例如方法表指针以及通过它对方法代码入口的访问。在t l l 的翻译思想中，对这两类数据加以区分。类的继承关系以及一些静态的信息保存 到低层的类型信息当中。在理想的情况下，这部分信息表达的属性和限制能够完 全由低层的类型来翻译，而低层语言的类型检查则能够检查是否保持了高层语言 的属性和满足高层语言的限制。而”动态”的部分则用低层语言的指令和数据表示 来翻译，这些指令和数据的操作则受到类型系统的约束，使数据的访问总是合法 的。我们的类布局中数据包括的就是这一部分。 o r p 原有的c l a s s 结构包括了上面所说的两部分信息，我们把如上图所示的 类数据提取出来构造了结构x c t y p e d e f s t r u c tx c v t a b l e + m t b ； v o i d4 cn e w ；n e w 方法的入口地址 v o i d + c _ i n i t 1 ； 方法的入口地址数组 ) x c ； 而c l a s s 结构增加了一个域，也就是x c 的指针，另外还有对x c 的t l l 类 型标注。对类数据的访问也就是对x c 中数据的访问则要满足所标注类型的限制。 原有的c l a s s 结构的其它域仍然保留下来，对于那些不在j v m l 。子集当中的类库 文件，我们还要依赖o r p 原有的装载编译过程，将它们转换为n a t i v e 代码。此 外，在把j w m l o 字节码翻译成t l l 的过程中，我们也需要c l a s s 这样收集字节码 中类以及其中成员所有源程序信息的结构来起到抽象语法树作用。 n e w 函数入口是一段n a t i v e 代码的地址。这段代码调用g c 模块分配新的类 实例需要的空间，类似于原有o r p 中提供的运行时支持代码。我们为它标注t l l 类型信息。这段n a t i v e 代码也在t c b 当中，它是否符合标注的t l l 类型信息是 需要我们信任的。 ! 里型堂垫查查堂堡圭兰垡丝苎兰= 童鲞型些堡笙堕墨坌型 函数和方法表中的其它方法一样，初始的入f _ 代码也是 c o m p i l em es t u b 。我们把x c 中一个 函数对应的域的地址记录在它的方法旬 柄m e t h o d 的a b l 9 _ p a t c h 中，当 编译为n a t i v e 代码，则将x c 中的相应表 项更新。 2 4 2 字节码到t l l 指令内部表示的翻译 下面详细描述