• 4.48 MB
  • 2022-06-17 14:58:31 发布

浅论aspectj程序分析及编织优化相关技术研究

  • 85页
  • 当前文档由用户上传发布,收益归属用户
  1. 1、本文档共5页,可阅读全部内容。
  2. 2、本文档内容版权归属内容提供方,所产生的收益全部归内容提供方所有。如果您对本文有版权争议,可选择认领,认领后既往收益都归您。
  3. 3、本文档由用户上传,本站不保证质量和数量令人满意,可能有诸多瑕疵,付费之前,请仔细先通过免费阅读内容等途径辨别内容交易风险。如存在严重挂羊头卖狗肉之情形,可联系本站下载客服投诉处理。
  4. 文档侵权举报电话:19940600175。
东南大学博士学位论文AspectJ程序分析及编织优化相关技术研究姓名:曹璟申请学位级别:博士专业:计算机软件与理论指导教师:徐宝文20090106 摘要AspectJ是--1"7新的程序设计语言,它是在Java语言的基础上扩充了AOP系统而来的。AspectJ语言的面向方面程序设计方法能够弥补传统面向对象技术在模块化软件中横切关注点方面的不足,因此它不仅是人们研究AOP语言的主要平台,在现实中也有着广泛的应用。AspectJ语言既对程序分析领域提出了新问题,也对传统的分析提出了新的挑战。我们对AspectJ程序的面向方面调用图及其构造,以及动态通知的编织优化进行了深入的研究,并按照新的需求重新考虑了Java程序类型分析和指向分析等问题。‘论文的主要研究成果包括:(1)提出了基于SAT求解的Java程序类型分析的新方法,该方法是流敏感、属性敏感以及上下文敏感的,能够在复杂度可接受的情况下构造出更加精确的程序调用图。方法的基本思想是将程序抽象为命题逻辑公式,然后利用SAT求解器求解来完成分析。我们以方法为单位进行抽象,首先将方法转换成SSA扩展形式,然后将变量和属性抽象为布尔向量.类型被编码为具体的向量,相关语句的公式通过联结符“^”联结成方法的公式。我们通过求取方法抽象的概要进一步缩小方法公式的规模并化简推导过程。对于方法概要公式,既可以单独求解(过程内分析),也可以按照上下文不敏感或敏感的方式联结起来求解(过程间分析)。(2)提出了基于SAT求解的Java程序指向分析的新方法,该方法同样是流敏感、属性敏感以及上下文敏感的,能够有效缓解传统方法精确分析时的状态空间爆炸问题。方法的基本思想和主要分析流程与基于SAT求解的Java程序类型分析方法相同。主要区别在于指向分析方法是一个反复迭代、逐步求精的过程,它利用已有的分析结果精化当前的方法公式,再次组成程序的公式并求解,从而获得更加精确的分析结果,如此反复直至达到稳定。(3)提出了适合AspectJ程序分析的面向方面调用图,该调用图能够表示AspectJ语言定义的多种程序执行事件,并且能够在上下文不敏感的情况下间接表示出与节点相关的部分对象的动态类型,解决了传统上下文不敏感调用图的缺陷。我们在传统调用图的基础上增加了节点的种类,定义了节点的类型并区分静态节点类型和动态节点类型,另外还定义了边的种类。我们将基于SAT求解的Java程序类型分析方法用于上下文不敏感面向方面调用图的构造。对于基程序和方面程序中的通知,我们采用基于SAT的方法分析。对于通知在程序中的织入点,我们通过对切点做快速的解析来估计。对于静态通知,我们能够准确的估计通知的织入点,但对于动态通知,我们只能估计出所有可能的织入点。要想进一步提高动态通知织入点的估计精度,可以运用我们提出的动态通知编织优化方法。‘(4)提出了基于上下文不敏感面向方面调用图的AspectJ程序动态通知编织优化方法,相比较其它优化方法,该方法考虑了具有分别与对象的动态类型和程序运行时调用栈有关的两类动态性的通知的编织优化。我们的方法在上下文不敏感面向方面凋用图上求解程序运行到可能织入点时的调用栈表达式,并利用面向方面调用图的动态类型推导能力推导调用栈表达式中节点的所有可能的类型,然后将该表达式与切点匹配,若切点包含表达式中的所有模式,则将通知调用无条件织入该节点;若切点不包含其中任一种模式,则通知调用不织入;至于其它情况,通知调用仍需条件织入。关键词:Java语言、调用图、类型分析、指针分析、面向方面程序设计、AspectJ语言、编织、优化、SAT AbstractAspectJisanewprogramminglanguagewhichextendsJavawithAOP(aspect-orientedprogramming)system.Theaspect-orientedprogrammingmechanismincorporatedinAspectJcanovercomeshortcomingsofthetraditionalobject-orientedprogrammingtechniquewhichfailstomodularizecrosscuttingconcernsinsoftware.Therefore,AspectJwillnotonlybeamajorplatformforpeopletoresearchAOPlanguages,butalsohavemanyapplicationsinrealworld.AspectJproposesnewquestionsinprogramminganalysis;meanwhileitchallengessometraditionalanalysis.Wemakeadeepresearchontheconstructionofaspect-orientedcallgraphofAspecUprograms,andtheweavingoptimizationofdynamicadvices.Basedonnewrequirements,wereviewedsometraditionalanalysissuchastypeanalysisandpoints-toanalysisofJavaprograms.Themaincontributionsofthispaperarelistedasfollows.(1)Weproposedanewmethod,whichisflow-,field—andcontext-sensitive,fortypeanalysisofJavaprogramsbasedonSATsolver,itcallconstructamoreprecisecallgraphofprogramunderanacceptablecomplexitylevel.Inshort,themethodabstractsapropositionalformulafromaJavaprogram,andthensolvestheformulatocompletetheanalysisbyusingSATsolver.TakingeveryJavamethodasanabstractionunit,wefirstlychangetheformofthemethodfromitsoriginalformtoextendedSSAform.ThenBooleanvectorsareabstractedfromvariablesfindfields,realtypesareencodedtovectorvalues,andformulasofstatementsarelinkedsoastoconstimtetheformulaofthemethodusinglogicalconjunctionsymbol”^”.Afterthat,wepartiallyevaluatemethodabstractiontoreducethesizeoftheoriginalformulaofthemethodandsimplifythedeductioninsolvingtheformula.Fortheformulainmethodsummary,notonlycanwesolveitdependentlyforintra-proceduralanalysis,butalsolinkseveralformulasandsolvethemforinter-proceduralanalysisasawhole.(2)Weproposedanewmethod,whichisalsoflow-,field—andcontext-sensitive,forpoints-toanalysisofJavaprogramsbasedonSATsolver,itcanrelievethestatespaceexplosionproblemintheprecisepoints—toanalysisusingtraditionalmethods.ThebasicprincipleandthemajorpartofitsframeworkarethesameaSthemethodfortypeanalysismentionedinthepreviousparagraph.Themaindifferenceisthatthemethodforpoints-toanalysisdoesalliterativeanalysis;thatis,itimprovesexitingformulasofmethodsbasedoncurrentresults,linksthemtoconstitutethe.program’sformula,andthensolvestheformulaagaintoproduceamorepreciseresult.Werepeattheiterativeanalysistimeandagainuntilafixed-pointisreached.(3)WeproposedanewkindofcallgraphnamedAspect—OrientedCallGraph(ACGforshort)forAspectJprogramanalysis.ACGcallexpressalmostallkindsofprogramexecutioneventsdefinedinAspecU’sJoinPointmodel,andcanindirectlydescribethedynamictypeofsomerelatedobjects.ACGisregarded丛anextensionofthetraditionalcallgraphforthefollowingreasons;1)thenodeisextended;2)thetypeofanodewhichconsistsoftherelatedtype‘ofcurrentobjectandthatoftargetobjectisdefined;and3)edgesofACGaredividedintodependentandindependentedges.WeusesuchanextensionofthemethodfortypeanalysisofJavaprograms,aimingatconstructingthecontext-insensitiveACGofAspectJprograms.Inourmethod,weusethetypeanalysismethodtoanalyzebaseprogramsandadvices,andestimatethewovenpointsofadvicesinprogramsthroughrapidpointcutparsing.Thewovenpointsofstaticadvicescanbepreciselyestimated,butthosefordynamicadvicesCallonlyrecieveallthepossibleestimations.Toimprovetheprecision,thedynamicadvicesweavingoptimizingmethodwillbediscussedinthenextparagraph.(4)WeproposedanAspecUdynamicadvicesweavingoptimizingmethodbasedonthecontext-insensitiveACGofAspecUprograms.Comparedwithothermethods,ourmethodcallhandletwokindsofdynamicadviceswhichcorrelatewithobject’sdynamictypeandruntimecallstackrespectively.Ourmethodfirstlysolvesthecallstackexpressionofthepossiblewovenpointsofdynamicadvicesonthecontext-insensitiveACQandthen deducesallthepossibletypesofthenodesintheexpression.Afterthatwematchesthecallstackexpressionwiththepointcutofadynamicadvice,anddecideshowtoweavetheadvicebasedontheresultofmatching:1)ifthepointcutcontainstheentireexpression,thenitiswovendefinitely;2)ifthepointcutdoesnotincludeanypa:ttemoftheexpression,thenitisnotwoven;3)ifneitherofthetwosituationshappens,theadviceiswovenwitharesidueprogram.Keywords:Javalanguage,callgraph,typeanalysis,pointsanalysis,aspect—orientedprogramming,AspectJlanguage,weaving,optimizing,SAT 东南大学学位论文独创性声明本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知,除了文中特别加以标注和致谢的地方外,论文中不包含其他人已经发表或撰写过的研究成果,也不包含为获得东南大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意,研究生签名:东南大学学位论文使用授权声明东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位论文的复印件和电子文档,可以采用影印、缩印或其他复制手段保存论文。本人电子文档的内容和纸质:论文的内容相一致。除在保密期内的保密论文外,允许论文被查阅和借阅,可以公布(包括以电子信息形式刊登)论文的全部内容或中、英文摘要等部分内容。论文的公布(包括以电子信息形式刊登)授权东南大学研究生院办理。研究生签名:—夔生导师签名:崾霹研究生签名:丛!:!:导师签名:划.12.驴 东南大学博士学位论文1.1选题依据第一章引言软件的模块化是软件工程领域中的一个重要研究课题。模块化的软件具有更好的可重用性、可维护性、可扩展性和可验证性,是实现软件工厂的必经之路【l-3】。随着软件规模的日益庞大,人们对软件模块化程度的要求也越来越高。软件的模块化不仅需要程序员具备良好的模块化程序设计思想,更离不开程序设计语言的支持,不同设计范式的程序设计语言具有不同的模块化能力。过程式程序设计语言(例如C、Pascal、Algol60等等)支持函数级别的封装,而面向对象程序设计语言(例如Java、C++、Smalltalkl4J、Rubyl51等等)则支持对象级别的封装,其模块化能力强于前者。虽然面向对象程序设计方法仍然是当前软件设计方法的主流,但其在模块化能力上的不足逐渐暴露出来。KiczalesG等人指出软件中存在一些具有横越多个模块的行为,使用传统的软件开发方法不能够达到有效模块化的特殊关注点,他们将这些特殊关注点称为横切关注点(crosscutconcern)[6-81.例如,图1.1是一横切关注点示例,FigureElement是抽象类,Point和Line是两个具体的类。DisplayUpdating是一个关注点,其功能是当图形元素改变坐标后即时更新在视图上的显示,这通过在设置坐标值后紧接着调用Display.update0方法实现。如果利用传统程序开发技术,我们必须在setX(in0、setY(int)、moveBy(int,inO、setPl(Poin0、setP2(Point)以及moveBy(int,in0等6个方法中都添加Display.update0方法调用语句。因此,关注点DisplayUpdating是一个横切关注点,其横越了Point和Line两个类共6个方法。图I.1横切关注点示例为了能够有效的封装横切关注点,KiczaleSG等人提出了面向方面的程序设计思想⋯¨,并且通过对Java语言扩充AOP系统设计出了AspectJ语割12-15】。其它面向方面程序设计语言还有AspectWerkztl6-18】、JBossAOPll9"201以及SpringAOPl2u2](AspectJ项目和AspectWerkz项目于2005年合并【1司),它们都是对Java语言的面向方面扩充。在众多的AOP语言中,AspectJ最为典型,是研究AOP语言及其应用的主要平台。AspectJ语言AOP系统的核心是预定义的连接点模型(joinpointmodel),以及增加的切点(pointcut)、类型间声明(intertypedeclaration)、通知(advice)和方面(aspect)等新的语言设施【13】。AspectJ语言将横切关注点封装为方面。例如,我们可以将图1.1所示的横切关注点封装为如下的方面程序。aspectap{pointcutpcl:call(voidFigureElement+.set搴(一));pointcutpc2:call(voidFigureElement.moveBy(int,int));after():pclIlpc2{Display.update0;)}1 东南大学博士学位论文其中,pcl和pc2是切点,pcl通过通配符选定了FigureElement子类的所有以“set”开头的方法,即Point类的setX和setY方法以及Line类的setPl和setP2方法,pc2选定了FigureElement类的moveBy方法(由于Point和Line是FigureElement的子类,因此也包括它们的moveBy方法),紧接着的通知指定当调用完pcl和pc2选定的方法后执行语句“Display.update0;”。这样我们就把原先需要在6处插入的语句封装到了一处。待到编译时,AspectJ语言的编译程序将方面织入到程序中。方面被编译成普通的类,通知被编译成普通的方法,通知的调用插入到由切点指定的程序点处,编织后的AspectJ程序是一个普通的Java字节码程序[23,241。这种织入方式将编织代价转移到编译时,并且使得程序执行不需要修改Java虚拟机。但它对动态通知的编织效果不好,会留下大量的滞留程序,用于程序运行时做检查,满足条件则执行通知,不满足则跳过通知继续执行。目前,AspectJ编译程序没有采用任何优化技术消除滞留程序,从而造成编织后程序执行效率的低下。这就给AspectJ程序分析提出了具体的问题,即我们如何通过分析来优化对动态通知的编织,提高编织后程序的执行效率。动态通知的编织优化离不开AspectJ程序的调用图,但AspectJ语言引入的新的语言设施给传统程序调用图及其构造带来了新的挑战。一方面,节点种类单一的传统程序调用图已经无法表示AspectJ连接点模型中定义的丰富的程序事件。因此,需要研究适合AspectJ程序分析的调用图。另一方面,构造调用图的传统方法达到了构造精度的瓶颈,在复杂度可接受的情况下无法构造出较为精确的调用图,不能满足优化的需求。因此,需要研究构造程序调用图的新方法。由于AspectJ是Java语言的AOP扩展,因此我们首先研究Java程序调用图的构造,然后将构造方法扩展到AspectJ程序中。构造Java程序调用图的实质是进行类型分析。而别名关系对包括类型分析在内的面向对象程序分析的精度有着较大的影响。现有的指向分析方法大都是流不敏感且上下文不敏感的,因此分析出的别名关系不够精确,从而造成其它程序分析精度的低下。为此,研究一种实用的更加精确的Java程序指向分析方法非常有现实意义。综上所述,本课题研究的目的旨在通过对AspectJ程序分析及编织优化相关技术的研究,提出一种Java程序调用图构造和指向分析的新方法;提出一种适合AspectJ程序分析的调用图,并研究其构造方法;研究动态通知编织的优化问题,分析通知织入的确定性,减少滞留程序,改善程序运行效率。1.2国内外研究现状(1)Java程序调用图的构造面向对象程序调用图构造是面向对象程序分析中的经典问题,自九十年代以来,人们对其进行了广泛而深入的研究,提出了从简单剑复杂的多种构造方法,主要包括CHAl25,26J、RTA[2刀、XTA系列(包括CTA、FTA、MTA和XTA)[2s1、VTA系列(包括DTA和VTA)[29l、以及k-CFA(k≥0)[30,31】。这些方法都是流不敏感的,并且除k-CFA(k≥1)以外的方法也是上下文不敏感的,因此虽然它们的构造速度较快,但精度低。而精度稍高的k-CFA(k≥1)的空间复杂度难以被人们接受。因而目前的程序分析仍然大都采用快速但粗糙的方法构造程序的调用图。(2)Java程序指向分析指向分析的目的是分析变量的指向集,从中可以归纳出变量间的别名关系,而准确的别名关系能够提高大多数程序分析的精度,因而指向分析一直是程序分析中的热点和难点之一。人们在指向分析方面做了大量的研究工作,提出了不少分析方法13}卯J。文献[32-36]的方法是基于数据流方程的流敏感方法。这类方法精度较高,但复杂度也很高,因而只适用于小规模的程序。文献[37-40]的方法是基于合一(unification.based)的流不敏感方法。这类方法复杂度低,能够适用于大规模的程序,但其精度也很低,无法满足人们的需求。文献[41.55】的方法是基于包含(inclusion.based)的流不敏感方法。这类方法的精度和复杂度介于前两类方法之间,是人们研究的重点。AndersenLO最先提出基于包含的分析方法1411,他将程序中变量间指向集的包含关系抽象为一个约束系统,原问题转换为该系统的求解。FaehndrichM利用图来表示包含关系,将原问题转换为计算图上的动态传递闭包1421。文献[43,44】将FaehndrichM的方法推广到上下文敏感的分析。文献[45-491I),lIJ针对动态传递2 东南大学博士学位论文闭包的计算提出了一些改进的算法。SridharanM将指向分析转换为图的上下文无关语言可达性(CFL-reachability)问题【5们。为了进一步降低方法的空间复杂度以提高适用性,BemdlM等人利用二元决策表(BDD)来表示包含关系与指向信息【51‘53】。Whale),J则将BemdlM的方法推广到上下文敏感的分析I川。另外,ZhuJ提出了基于BDD的符号指向分析方法15”n。虽然BDD的使用能够降低指向分析的空间复杂度.但它只能在一定程度上缓解状态空间爆炸,却无法避免它,并且BryantRE曾经指出,对于有些公式。无论变量顺序怎样,其OBDD都是指数爆炸的,没有优化的空间[SSl。指向分析面临的主要问题始终是精度与效率的平衡问题15%21,寻找既具有令人满意的精度又能够适用于大规模程序的分析方法是人们探求的目标。(3)AspectJ程序调用图及其构造由于AspectJ语言是对Java语言的扩展,因此人们试图将面向对象程序调用图以及构造方法应用于AspcctJ程序。但AspectJ语言引入的新的语言设施给应用造成了一定的阻碍。其中,最主要的两个问题是如何在调用图中表示AspectJ连接点模型中的程序事件?以及如何在调用图中确定通知的调用点?目前,详细讨论AspectJ程序调用图及其构造的文献很少,在现有的研究成果中,AvgustinovP等人针对编织后的AspectJ程.序构造调用图【631,此时与构造普通Java字节码程序调用图无异,因而可以直接使用面向对象程序的调用图及其构造方法,这样就直接绕过了第二个问题。但构造出的程序调用图反映的是编织后的程序,与AspectJ源程序还是有区别的。并且该方法仍然没有解决第一个问题。HayashidaR等人104J以及TakashiI等人165埴接将面向对象程序调用图用于AspectJ程序的表示,将通知也看做普通的方法,因而调用图只表示了方法执行和通知执行这两种程序事件,他们利用已有的面向对象程序调用图的构造方法分别构造基程序和方面程序的调用图,然后通过文本匹配确定通知的调用点,但他们仅仅考虑了静态切点。李楠等人将面向对象程序调用图中的节点扩展为两类,分别表示“方法调用”和“方法执行”事件,并且也将通知看做普通的方法,他们将RA、RTA、VTA方法扩展至lJAspectJ程序中,也通过文本匹配确定通知的调用点,但他们考虑Tcflow切点的匹配166,671。由此可知,现有的AspectJ程序调用图只能表示连接点模型中少数的程序事件,并且调用图构造方法大都基于传统方法,因而不可避免的存在传统方法精度低的缺陷。“)AspectJ动态通知的编织优化动态通知是指包含动态切点的通知。动态切点可分为三类:第一类只考察调用栈中的调用信息(通过cflow或cflowbelow切点指定);第二类只考察对象的运行时类型(通过this、target或args切点指定);第三类则兼具前两类动态特性,既考察调用栈的状态,又考察运行时类型。通常,方面程序中第三类动态切点屠多。人们已提出的优化方法较少,其中,MasuharaH等人使用部分求值技术(partialevaluation),利用编译时获得的静态信息确定织入点,该方法对静态切点有效,但对动态切点的优化效果不好,匹配cflow时需要遍历调用栈1681。AspectJ编译程序针对cflow的匹配做了优化,它通过构造自动机,使得匹配时只需查看栈顶元素,无需对调用栈进行遍历[69】。上述两种方法都没有尝试确定动态切点的织入点。AvgustinovP等人提出的方法只考虑了cflow的优化,忽略了对象运行时类型的分析,因此该方法不适用于优化具有此类动态性的切点,而在所有的动态切点中又以这种切点居多163,70】。1.3主要研究内容根据国内外在程序分析及编译优化技术方面的研究现状,以及最新发展动态,我们拟在AspectJ程序分析及编织优化方面展开深入研究。具体而言,本课题将在以下几个方面展开研究。(1)基于SAT求解的Java程序调用图构造研究构造精确的Java程序调用图需要对程序做属性敏感、流敏感以及上下文敏感的类型分析,传统分析方法皆因复杂度太高难以胜任,为此,需要研究新的构造方法。命题逻辑的可满足性SAT问题(SATisfjabiIity,简称sAT)是第一个被证明的NP完全问题【7l】,近年来,随着SAT求解器能力的提高,SAT问题广泛应用于数字电子电路的自动设计和验证(verification),集成3 东南大学博士学位论文电路的等价检测(equivalencechecking)以及人工智能中的自动定理证明等等【72。791。在程序分析和验证领域,由于SAT问题的应用能够克服传统方法存在的状态空间爆炸问题,因此它同样受到人们越来越多的重视。ClarkeEM等人利用SAT求解器进行谓词抽象过程中状态空间的搜索,提高了搜索的速度和精度瞄U"引J。XieY等人提出了一种基于SAT的c程序缺陷侦测方法182,83]。DennisG等人利用SAT验证Java程序的方法是否满足其规格说吲341。SAT问题的应用使得他们的方法能够适用于大规模的程序。鉴于SAT问题应用的优势,我们将它应用于Java程序类型分析以构造程序调用图。我们要求新的方法是流敏感、属性敏感的,并且可以进行上下文敏感的分析。(2)基于SAT求解的Java程序指向分析研究指向分析的空间复杂度比类型分析更高,利用现有分析方法做流敏感、上下文敏感的分析时存在状态空间爆炸问题,因此精确的分析很难适用于大规模的程序分析。虽然BDD在一定程度上能够降低分析的空间复杂度,但当变量的个数成千上万时,BDD需要的存储空间就会变得很大【5引,因此鉴于SAT应用在空间复杂度方面的优势,我们拟继续利用SAT问题做Java程序的指向分析。同样的,我们要求指向分析新方法是流敏感、属性敏感的,并且可以进行上下文敏感的分析。(3)AspectJ程序面向方面程序调用图及其构造研究AspectJ语言的连接点模型定义了包括方法调用事件、方法执行事件在内的11种事件Il引。如果能够在调用图上直接表示出这些事件则大大便于AspectJ程序的分析和优化。另外,上下文不敏感的传统调用图虽然构造便捷,但却无法表示程序执行到节点时相关对象(执行对象和目标对象)的动态类型。为此,我们对传统调用图进行扩充,提出一种面向方面的调用图,该图能够表示AspectJ语言定义的大部分程序执行事件,并且节点具有类型属性,能够在上下文不敏感的情况下推导出相关对象的动态类型。我们仅仅讨论上下文不敏感面向方面调用图的构造,因为这类图使用得最为广泛。我们将(1)中研究的类型分析新方法加以扩展,用于其构造。构造的一个主要难点在于通知调用点的确定。对此,我们采用保守估计的方法,找出所有可能的调用点。(4)AspectJ程序动态通知编织优化研究优化动态通知编织的关键是明确其在可能织入点上的织入情况:若一定织入,则删除滞留程序,直接织入通知调用语句;若一定不织入,则一并删除滞留程序与通知调用语句。由于动态通知关注运行时由预定义事件构成的调用栈以及相关对象的动态类型,因此我们利用AspectJ程序的上下文不敏感面向方面调用图分析运行时调用栈及对象的动态类型,如果分析结果被切点完全切中则通知一定被织入,如果分析结果没有被切点切中则通知一定不被织入。1.4论文主要成果论文工作的主要成果如下:·提出了基于SAT求解的Java程序类型分析的新方法,该方法是流敏感、属性敏感以及上下文敏感的,能够在复杂度可接受的情况下构造出更加精确的程序调用图。·提出了基于SAT求解的Java程序指向分析的新方法,该方法同样是流敏感、属性敏感以及上下文敏感的,能够有效缓解传统方法精确分析时的状态空间爆炸问题。·提出了适合AspectJ程序分析的面向方面调用图,该调用图能够表示AspectJ语言定义的多种程序执行事件,并且能够在上下文不敏感的情况下间接表示出与节点相关的部分对象的动态类型,解决了传统上下文不敏感调用图的缺陷。·提出了AspectJ程序上下文不敏感面向方面调用图的构造方法,该方法能够构造出较为精确的面向方面调用图,为AspectJ程序分析提供了可靠的参考。·提出了基于上下文不敏感面向方面调用图的AspectJ程序动态通知编织优化方法,相比较其它优化方法,该方法考虑了具有分别与对象的动态类型和程序运行时调用栈有关的两类动态性的通知的编织优化。4 东南大学博士学位论文1.5论文结构论文各章节摘要如下:·第一章作为整个论文的绪论,通过对软件中的横切关注点以及AspectJ的简单介绍引出待研究的问题,介绍现有的解决方案和仍存在的不足;描述论文的研究方案,在给出研究内容和方法后,简要地介绍研究成果和论文结构。·第二章讨论基于SAT求解的Java程序调用图构造方法。方法的基本思想是将程序抽象为命题逻辑公式,然后利用SAT求解器求解来完成分析。我们以方法为单位进行抽象,首先将方法转换成SSA扩展形式,然后将变量和属性抽象为布尔向量,类型被编码为具体的向量,相关语句的公式通过联结符“^”联结成方法的公式。我们通过求取方法抽象的概要进一步缩小方法公式的规模并化简推导过程。对于方法概要公式,既可以单独求解(过程内分析),也可以按照上下文不敏感或敏感的方式联结起来求解(过程间分析)。·第三章讨论基于SAT求解的Java程序指向分析方法。方法的基本思想和主要分析流程与基于SAT求解的Java程序类型分析方法相同。主要区别在于指向分析方法是一个反复迭代、逐步求精的过程,它利用已有的分析结果精化当前的方法公式,再次组成程序的公式并求解,从而获得更加精确的分析结果,如此反复直至达到稳定。·第四章介绍AspectJ程序面向方面调用图ACG,并讨论上下文不敏感ACG的构造方法。我们在传统调用图的基础上增加了节点的种类,定义了节点的类型并区分静态节点类型和动态节点类型,另外还定义了边的种类。我们将基于SAT求解的Java程序类型分析方法用于上下文不敏感面向方面调用图的构造。对于基程序和方面程序中的通知,我们采用基于SAT的方法分析。对于通知在程序中的织入点,我们通过对切点做快速的解析来估计。对于静态通知,我们能够准确的估计通知的织入点,但对于动态通知,我们只能估计出所有可能的织入点。要想进一步提高动态通知织入点的估计精度,可以运用我们提出的动态通知编织优化方法。·第五章讨论AspectJ程序动态通知编织的优化。我们的方法在上下文不敏感面向方面调用图上求解程序运行到可能织入点时的调用栈表达式,并利用面向方面调用图的动态类型推导能力推导调用栈表达式中节点的所有可能的类型,然后将该表达式与切点匹配,若切点包含表达式中的所有模式,则将通知调用无条件织入该节点;若切点不包含其中任一种模式,则通知调用不织入;至于其它情况,通知调用仍需条件织入。·第六章对整个论文研究和实践工作进行了总结,同时指出我们现有工作的局限性有待提高和改进的方面,简单阐述我们正在进行或将要进行的研究工作。5 东南大学博士学位论文第二章基于SAT求解的Java程序调用图构造程序调用图是一种描述函数(或方法)问调用关系的有向多图,图中节点表示函数(或方法)(通常用一元组<函数名(或方法名)>表示),有向边表示调用关系(通常用三元组<头节点,尾节点,调用行号>表示),节点间的有向边可以不止一条以表示不同程序点上的调用。调用图是关于程序的非常重要的信息,大多数程序分析需要依赖调用图进行过程间分析。按照上下文是否敏感,调用图可分为上下文不敏感的和上下文敏感的两类。上下文不敏感调用图在构造时不区分调用发生时的上下文,一个方法只用一个节点表示。例如,图2.1(a)所示是一程序实例,图2.1(”是其上下文不敏感调用图;而上下文敏感调用图在构造时区分调用发生时的上下文,即使是相同的方法,在不同的上下文下调用也用不同的节点表示。很多信息可以作为上下文,比较常见的两种上下文是调用路径和参数类型的笛卡尔积。例如,图2.Kc)所示是图2.Ka)程序的以调用路径为上下文的上下文敏感调用图。publicimerfaceiF{15publicvoidmlO;16)17publicclassAimplementsIF{18publicvoidmlO{⋯}19}20publicclassBimplementsIF(21publicvoidmlO{⋯}22)23publicclassC(24publicvoidnO-O{25Aa=newAO;26m4(a);27})(b)(c)圈2.1程序调用图示例对于过程式语言程序,例如不含函数指针的C程序,由于被调函数名静态绑定到具体的函数,因此只需通过简单的语法分析即可构造出程序的调用图(构造包含函数指针的C程序的调用图需要进行指向分析)。而对于面向对象语言程序,例如Java程序,由于被调方法名动态绑定到具体的方法,因此需要通过类型分析获得被调对象的所有可能的运行时类型,才能构造出完备的程序调用图。Java语言的类型分为基本类型和引用类型,只有引用类型才能创建对象,因此Java类型分析只需分析声明为引用类型的变量的运行时类型。具体的,Java类型分析需要考虑六类语句:对象创建语句、简单赋值语句、对象属性引用语句、对象属性定义语句、强制类型转换语句和方法调用语句(如图2.2所示)。6订B饵吣a删州删一吣一一咄一愀.:藿一锨锨.忙b似.忙m.忙c喊,札一一吣一一一一一一●23456789m¨他BM 东南大学博士学位论文(1)V=11CWType;(2)Vl=v2(3)VI=V2.E(4)VI.f=v2;(5)Vl=(Type)v2;(6)VI2V2.m(al,...,an);图2.2Java类型分析考虑的六类语句分析出被调对象的所有可能的运行时类型后,只需根据被调方法名在这些类型的声明中查找与之匹配的方法即可得到实际调用的所有方法,从而构造出调用图。2.1研究现状现有的面向对象程序调用图构造方法主要有CHA方法【25矧、RTA方法【271、XTA系列方法(包括CTA方法、MTA方法、FTA方法和XTA方法)1281、VTA系列方法(包括VTA方法和DTA方法)129】以及k-CFA(k≥O)方法【30"311。CHA(ClassHierarchyAnalysis)方法只考虑了方法调用语句。该方法首先统计程序中定义的类型,接着从入口方法开始分析,当遇到方法调用语句时,则在被调变量v的声明类型及其子类型中查找与被调方法m匹配的方法,匹配上的方法都是被调的实际方法,然后依次进入每个实际方法递归分析。RTA(RapidTypeAnalysis)方法是对CHA方法的改进,它考虑了对象创建语句和方法调用语句。该方法的基本思想是只有创建了实例对象的类型,其定义的方法才会被调用。因此该方法首先统计程序中定义的类型,并且根据程序中所有对象创建语句从中筛选掉没有创建实例的类型,剩下的类型作为全局类型搜索集,接着从入口方法开始分析,当遇到方法调用语句时,根据被调变量V的声明类型在全局类型搜索集中寻找该类型及其子类型,然后在寻找出的类型中查找与被调方法m匹配的方法,匹配上的方法都是被调的实际方法,然后依次进入每个实际方法递归分析。RTA方法只有一个全局类型搜索集,无论分析哪个方法时针对遇到的方法调用都在全局类型搜索集中搜索。XTA系列方法对此进行了改进,它们同样考虑了对象创建语句和方法调用语句,但通过建立多个独立的类型搜索集,缩小每个方法调用的搜索空间,进一步提高分析精度。其中,XTA方法的类型搜索集共有nm。个(nf为所有属性的个数,nm为所有方法的个数),搜索集之间按照一定的规则传播类型,当遇到方法调用语句时,在其所处方法对应的搜索集中查找。CTA方法、FTA方法以及MTA方法是XTA方法的简化,‘CTA方法的类型搜索集为nc个(nc为类的个数),VIA方法的类型搜索集为nc+n。个,MTA方法的类型搜索集为nc+nf个。VTA系列方法利用类型传播图做类型分析,它们考虑了全部六类语句。类型传播图是一种有向图,图中节点表示程序中的变量,节点上附加有类型集表示变量可能的运行时类型,从第二至第六类语句中抽象出的有向边表示类型传播关系。分析的基本方法是首先由程序中的对象创建语句获得节点的初始类型集,然后依据有向边不断的传播类型使得节点上的类型集达到稳定状态,从而获得分析结果。VTA方法和DTA方法的区别在对对象属性的处理上,VTA方法是基于属性的,而DTA方法是属性不敏感的,因此VTA方法比DTA方法更加精确。k-CFA(k≥0)方法起源于函数式语言Scheme程序的控制流分析。该方法的基本思想是将程序中的这六类语句转换成类型不等式,从而将整个程序抽象为一个类型约束系统,然后求解该系统完成对程序的分析。当k≥l时,k-CFA方法区分不同上下文下的类型不等式。总的来说,影响面向对象程序调用图构造方法精度的因素主要有以下三个:·控制流敏感性(contr01.flow-sensitivity,简称流敏感性)。控制流不敏感(control,flow-insensitive)的方法仅按照程序的行文顺序分析程序,而不遵循语句间的控制流关系:而控制流敏感(contr01.flow-sensitive)的方法则依据程序的控制流图,按照语句间的控制流顺序分析程序。控制流敏感的方法比不敏感的方法更精确。。上下文敏感性(context-sensitivity)。7 东南大学博士学位论文上下文不敏感(context.insensitive)的方法不区分调用上下文,在所有调用上下文下分析的都是同一个方法;而上下文敏感(context.sensitive)的方法则区分调用上下文,在不同调用上下文下分析的是方法的不同副本。上下文敏感的方法比不敏感的方法更精确。·对象属性敏感性(field.sensitivity)。对象属性敏感性分为属性不敏感(field.insensitive)、基于属性(field-based)以及属性敏感(field—sensitive)三类。属性不敏感的方法不区分对象的不同属性,它将所有属性用同一个变量表示:基于属性(field.based)的方法区分不同的属性,但忽略不同的对象,它将所有对象的同名属性用同一个变量表示;属性敏感(field.sensitive)的方法则对每个对象的每个属性都单独表示。属性敏感的方法精度最高,基于属性的方法次之,属性不敏感的方法精度最低。表2.1针对上述三个因素列出了现有方法各自的特点。表2.1现有构造方法的特点\、磁CHARTAXTA系列VTA系列CFA系列因兮\CTAFTAMT^XTADTAVTAOCFAkCFA流敏感否上下文敏感否是属性敏感不敏感基于属性不敏感基于属性图2.3给出了现有方法间代价和精度关系[28,96,971。在该图中,从左向右,精度逐渐提高,同时构造代价也逐渐增加。图2.3现有构造方法间的关系要构造出精确的程序调用图,必须进行流敏感的类型分析,而传统的数据流分析方法需要在程序的控制流图上进行迭代,分析时需要为不同的程序点保存当前的分析结果,在上下文敏感的情况下将会占有大量的存储空间,分析会因内存耗尽而终止[971。因此,在绝大多数程序分析中,人们大都采用流不敏感、上下文不敏感的构造方法,但高效的同时降低了调用图的精度,影响了后继分析的效果。随着计算技术的进步,我们认为研究实用的精确的面向对象程序调用图构造的新方法是十分必要的,并且新的方法应当是流敏感、上下文敏感、以及属性敏感的。本文我们介绍基于SAT求解的Java程序调用图构造的新方法:2.2节介绍新方法的基本思想;2.3节介绍语句及结构抽象;2.4节介绍方法抽象;2.5节介绍过程内分析;2.6节介绍过程间分析:2.7节介绍我们开发的原型系统SATTAS;2.8节总结。需要说明的是,下文在没有特别说明的情况下,所提类型是指引用类型,所提变量是指声明为引用类型的变量,所提属性也仅仅指声明为引用类型的属性。2.2基本思想命题逻辑的可满足性问题是第一个被证明的NP完全问题1711,它在理论和实际应用中都有许多非常重要的应用。理论上由于它是个NP完全问题,因此只要找到它的P时间算法,或者证明不存在这样的算法,8 东南大学博士学位论文那么P=?NP就可以解决。在实际应用中,计算领域中广泛存在的NP问题,如数字电子电路的自动设计和验证(verification)问题,集成电路的等价检测问题(equivalencechecking),人工智能中的自动定理证明等等,都可以直接转化成为SATIh-J题处理17卜仃J。在模型检查和程序验证领域,SAT问题的应用也受到人们越来越多的重视。BiereA等人利用SAT来做符号模型检查【7Sl。McMillanKL等人将SAT用于无界符号模型检查【79】。ClarkeEM等人利用SAT进行程序的谓词抽象【∞,8¨。XieY等人提出了一种基于SAT的C程序缺陷侦测方法182’831。DennisG等人利用SAlr验:证JaVa程序的方法是否满足其规格说吲洲。sAT问题的应用能够解决状态空间爆炸问题,使得他们的方法能够适用于大规模的程序。传统验证方法利用状态转移规则从初始状态开始逐个验证所有可达的状态,由于需要验证的状态往往随着问题的规模呈指数级增长,而传统方法又需要直接存储这些状态数据,因此很容易产生状态空间爆炸问题。利用BDD来存储状态虽然能够利用状态间的共性对存储空间进行压缩,但它只能缓解状态空间爆炸问题,当验证问题规模很大时,BDD需要的内存空间就会变得很大【581。而SAT问题的应用则将状态转移规则以及需要验证的条件抽象为命题逻辑公式,然后利用求解工具对满足条件的状态空间进行穷举,从而得到验证结果。不同于传统方法和{BDD直接存储状态的策略,SAT问题应用存储的是状态转移规则,因此它能够解决状态空间爆炸问题。具体的,SAT问题包含以下三种成分:·布尔变量,我们用x1,X2,X3,⋯米表示。·文字,我们用QI,Q,Q3,⋯来表示,一个文字是一个布尔变量(Q=工),或者布尔变量取反(Q=—霄)。·子句,我们用Cl,Q,c3,⋯来表示,一个子旬是若干文字的析取式(C=QlvQ2v⋯v岛)。SAT问题的目标是判定是否存在布尔变量的一组赋值,使得下面的合取范式(ConjunctiveNormalForm,简称CNF)成真:CtAC2A⋯^G求解SAT问题的算法研究是一个非常热门的领域。近年来,随着各种逻辑和组合优化技术,如回跳、冲突学习、重启搜索等;各种优良的数据结构如观察变量表、头尾表等;以及各种智能启发式搜索技术,如变量无关性递减和启发算法、最大动态独立和启发算法等等[85-8s1的引入,现在的SAT求解器(SATsolver),如GRASP[901,Chaff[911,zChafft921,GSAT[931,BerkMin[941,SATO[951等等,已经可以达到工业级的应用。为了便于CNF范式的输入,SAT求解器大多采用一种与其等价的DIMACS数据格式。一个CNF公式的DIMACS格式的模式为:e注释Pcnf布尔变量个数予句个数子旬编码部分(一个子句的编码占一行,并以“0”结尾)例如,a师公式(xlVX3V",X4)A(X4)A(x2v--,x3)的DIMACS公式为cThisisanexampleofacommentline.Pcnf43l3-4O402.30由于SAT问题的应用在空间复杂度方面有着显著的优势,因此我们研究如何将其应用到Java程序的调用图构造中去,也就是研究利用SAT问题进行Java程序类型分析的方法。研究的核心问题是如何将Java程序抽象成命题逻辑公式。我们方法的基本思想是将程序中的变量编码成布尔向量,其取值表示该变量的类型,用逻辑等价关系抽象变量间的类型传递,通过逻辑与(“A”)和逻辑或(“V”)将程序联结成一个命题公式,最后将其转换成CNF形式,利用SAT求解器求出所有可满足解。例如,对于下面的程序片段,1a=newTIO;9 东南大学博士学位论文2b2a;我们将它抽象成如下的公式(为了便于论述,下文对于具体类型赋值的表述均采用下面公式(1)的形式),(口=五)(1)^(6付口)(2)其中,变量a抽象为布尔向量二,变量b抽象为布尔向量舌,符号H表示逻辑等价。假设布尔向量的长度为2,类型Tl的布尔向量值为订,则程序片段的命题公式为(口=五)^(6H口).营aoAolA(bo卜ao)A(bo_ao)^(61.1.--q)A(6I专a1)§aoA口I^(60V一口o)^(一60Vao)A(6lV---,a1)^(.16lV口1)将其转化为CNF形式,并按照D1MACS格式输入后,求解得如下结果alao。ll岛60=11将上述结果解码即得变量a和b的类型都是Tl。从该示例中可以总结出三项基本抽象规则分别如规则2.1、规则2.2以及规则2.3所示。规则2.1(变量抽象规则):变量抽象成唯一的布尔向量,向量值表示变量的类型。规则2.2(赋值抽象规则):变量间的类型赋值抽象成逻辑等价关系。规则2.3(顺序语句公式联结规则):顺序语句公式间用“A”联结。上述示例十分简单,真正的抽象过程远比这复杂,涉及到变量的抽象、数组的抽象、属性的抽象、语句的抽象、结构的抽象以及方法的抽象等等,还需考虑数组元素访问的不确定性以及变量间可能存在的别名关系,并且需要体现山流敏感性以及属性敏感性。图2.4基于SAT求解的Java程序类型分析的流程lO 东南大学博士学位论文图2.4给出了基于SAT求解进行Java程序类型分析的具体流程。如图所示,分析的主要步骤是程序的抽象。抽象以方法为基本单位,在进行过程内(或过程间)分析前,Java程序的每个方法被独立的抽象为一组命题逻辑公式,抽象前需将方法转换为SSA扩展表示形式,抽象后我们通过求解方法抽象的概要(methodsummary)对方法原始公式进行化简。过程内和过程间分析都是利用方法概要公式获得程序的公式。过程内分析通过保守估计为每个方法概要公式补充入口锚点的初始值,然后对其单独求解。过程间分析则根据程序规模及上下文敏感性选择合适的方式(整体分析或分部分析)将存在调用关系的方法概要公式通过入口及出口锚点联结起来求解。最后将求解结果解码,并与方法概要中的变量常值信息综合,获得最终的分析结果。下文我们将对程序的抽象过程进行详细讨论。由于方法抽象较为复杂,因此我们首先在2.3节介绍图2.4中方法抽象步骤二,然后在2.4节介绍方法抽象步骤一和步骤三,最后分别在2.5和2.6节介绍过程内程序分析和过程间程序分析。为了便于抽象,我们假定Java源程序中属性或方法的访问路径不超过两位,即:·类属性(或静态属性)访问形如Tf,其中T是类型名,f是属性名。·对象属性访问形如v.f,其中v是简单变量,f是属性名。·方法调用形如v.m(pl,...),其中V是简单变量,m是方法名,参数Pi只能是简单变量、类属性或对象属性,不能是其它的方法调用。另外,我们不允许返回语句直接返回新创建的对象。若源程序不满足以上条件,则可以利用临时变量对程序进行化简,化简不会影响最终分析结果。例如,对于图2.5(a)所示的程序片段,其化简后的形式如图2.5(b)所示。Tifoo(T2p){T3V2a【2】.eTIs2v.吕bar(p);returnIicwT10,}Tifoo(T2p){1"4tmp=a【2】;LV=tmp卜£T5tmp2=v.g;TIS=tmp2.bar(p);Titmp3=newTl();returntmp3;"(a)(b)图2.5Java源程序化简示例2.3程序抽象初步:语句及结构抽象抽象语句及程序结构面临的首要问题是赋值副作用的影响以及控制流的抽象。在程序设计语言中,将变量与值关联的方式有两种:一种是绑定(binding)方式,该方式的特点是只能绑定一次,不能重复绑定,也就是说,一旦绑定变量的值将不再变化;另一种是赋值(assignment)方式,该方式允许变量多次赋值,从而造成变量值的不断改变,这通常被称为赋值的副作用pK鲫J。Java语言采用赋值方式,其副作用给抽象造成了一定的困难。例如,对于下面的程序片段,1v=newTl;2V=newT2;按照规则2.1~规则2.3,我们将其抽象为(-=正)A(-=互),但此公式永假。~种解决方法是用“V”联结顺序语句公式,但其缺点是无法利用顺序语句间的强更新(strongupdate)来提高分析精度,失去了流敏感分析的意义,因此该方法不可行。相对于流不敏感的分析,流敏感的分析具有以下优势:第一,它能够进行顺序结构语句间的强更新;第二,它能够区别分析分支结构的各个分支,而不是将所有分支的语句混合在一起分析;第三,它能够区分出循环结构,从而针对循环体内和体外的程序片段采用不同的分析方法。综上所述,我们希望类型分析方法是流敏感的,因此程序抽象方法必须能够抽象出程序的控制流。经过深入研究,我们发现在以SSA形式表示的程序上进行抽象能够有效解决上述两个问题。 东南大学博士学位论文2.3.1静态单赋值形式静态单赋值(StaticSingleAssignment,简称SSA)形式是一种程序表示形式,主要用于程序的编译优化,能够显著提高优化的效率‘m1041,被诸如gcc、LLVM(LowLevelVirtualMachine)【1051、ORC(OpenResearchCompiler)[1061以及Java编译程序等多数现代编译程序广泛采用Il们J。SSA形式的主要优点是将程序中的数据流和控制流都显式的表示了出来,它通过以下两个措施实现了这一点:1)通过重命名使得程序中的每个变量只被赋值一次,因而对于变量的引用,只有一个定义点可达;2)增加了a函数,用以表示控制流汇合点处变量的值可能从不同的控制流上流入。图2.6是程序SSA形式示例。其中,图2.6(a)是一程序片段;图2.6(c)是该程序片段的控制流图CFG(ControlFlowGraph)[ios,109】,图2.6(b)是该程序片段的SSA形式。如图所示,变换后的程序中的变量通过添加下标来区分不同的定义点,并且对每次变量的引用都明确指出其定义点。另外,在控制流的每一处汇合点,针对每一个从不同分支流入的相同变量都会添加一个O函数,通过它将不同分支上流入的值赋给新的变量,例如,语句“j2=004,j1);”表示变量j2的值来自基本块8中的j4或者来自基本块l中的jl。i=newTl():j=newT2();k=lleWT3();whiic(T){.f(P){J2I:if(Q)k=j;elsek=i;}elsek。newTs();(a)il=newTl0;jI=newT2();kl=newT3();while(T){j2。44,j1);k22o(ks,kJ;if(P)(J3=iI;if(Q)k32j3:elsek4=il;ks=0(k3,kd;"elsel(4=newT5();j42003,j2):l‘6=o(k2,k5);)(b)(C)图2.6程序SSA形式示例SSA形式解决了赋值副作用以及控制流给抽象带来的困难。首先,该形式确保变量只被赋值一次,因此抽象没有了赋值副作用的影响。其次,该形式将程序的控制流用语句显式的表示了出来,因此抽象相关语句也就抽象出了控制流。CytmnR等人提出了一种高效的程序SSA形式构造方法,其时间复杂度为O(E+T+DF),其中,E是程序控制流图CFG的边数,r是程序中赋值语句和。函数的总数,DF是支配边界节点(DominanceFrontier)的总数,实验表明该方法时间复杂度与程序的规模近似成线性关系[HOJll】。。2.3.2语句抽象传统的SSA形式只考虑了普通变量,没有考虑数组和属性的表示,不能用于Java程序,因此我们的抽象并非基于传统的SSA形式,需要对该形式进行扩展。另外,为了方便抽象,我们修改了SSA形式中某些语句的表示。由于SSA形式的扩展较为复杂,我们留待2.4节再详细讨论。本节的下文重点讨论基于SSA扩展形式的语句抽象以及结构抽象。Java程序的SSA扩展形式包含普通变量、数组变量、对象属性和类属性。抽象时,我们对它们采取相同的处理方式,都编码成唯一的布尔向量,因此为了表述的方便,下文我们把它们统一用变量表示。程序中需要抽象的语句可归为三类,分别是取值语句、赋值语句以及a函数语句(如图2.7所示)。其中,取值语句表示变量取具体的值u,U可以是某个类型T也可以是null。取值语句由源程序中的对象创建语句和强制类型转换语句转换而来,或者是因需要添加的。与传统形式不同的是,在SSA扩展形式中D函数的参12、,、,、,、,、,、,、,、,、,、,、,、;、;0UQ0OH够∞∞仃@@@ 东南大学博士学位论文数可以是变量,也可以是具体的值U。Y)J"I-,需要指出的是,我们将源程序中的方法调用语句转换成了其它语句,因而被抽象的语句不包括方法调用语句。(I)V2U;(2)V2w;(3)V2毗⋯,U91s$w);图2.7被抽象的三类语句下面我们介绍如何抽象这三类语句。假设程序中声明了CNum个类,根据规则2.1,我们将变量抽象为长度为lo&“M”+1’(包含null)的布尔向量,每个类编码为lo&(cⅣ删+1’位的具体向量。我们用瓦表示变量v对应的布尔向量。假设石和瓦是长度为n的布尔向量,bli和b2i分别表示瓦和乏的第i个分量,记(6l专62)=(6I。一%)^⋯A(612专622)^(6ll_62I)三类语句的抽象规则分别如规则2.4、规则2.5以及规则2.6所示,其中,《u】,表示值u的编码的第i位,t·H,,是命题逻辑中的相等联结符。如该图所示,取值语句的公式是由变量v的布尔向量瓦的所有位组成的合取式,并且每一位需根据值编码对应位的值决定取正还是取反。变量赋值语句的公式的含义是赋值符号两边变量的布尔向量的取值相同。a函数语句的公式可看作是由多个取值语句或赋值语句的公式组成的析取式,表示有多种可能的取值。规则2.4(取值语句抽象规则):Formula(”u≥m咖I“={羔黜曼规则2.5(赋值语句抽象规则):Formula(“V=w;’,)=(巩<--9,钆)2(钆卜丸)^(钆一bw)规则2.6(a函数语句抽象规则):Formula(“v=D化⋯U,...,w);”)=(Formula(“V=t;”)v⋯vFonnula(“V=U;”)v⋯vFormula(“V2w;”))图2.8是三类语句抽象的简单示例。图2.8(b)是程序片段的类继承结构以及类的编码(包含null)。图2.8(a)包含3条语句,其中,每个变量都被抽象成一个两位的布尔向量,例如变量a的布尔向量为瓯,每条语句右边是其抽象成的命题公式。Ia=C;2c=b:3d=“a,B);(6口:^6口1)(玩H玩)锄付6口)V伤2A"n乃1)(a)Anull:00一lIA:0l/\B:10BCC:1i(b)圈2.8语句抽象示例为了下文论述的方便,我们用伪公式“(变量名=值)”作为取值语句的简化表示,用伪公式“(变量名付变量名)”作为赋值语句公式的简化表示,并且我们仍然将公式中的向量称为变量。例如,对于图2.8(a)中的语句1,我们用“(a≈)”代替“(吃:A6口I)”,对于语句2,我们用“(cob)”代替“(包H%)”。2.3.3结构抽象本小节讨论程序结构的抽象,我们首先介绍三种基本结构(顺【序结构、分支结构和循环结构)的抽象,然后介绍它们相互嵌套时的抽象,最后再扩展到任意程序结构上。本节的讨论不涉及过程间的抽象。1)顺序结构抽象顺序结构非常简单,只需将结构中有关语句的公式取交(用“A”联结)即可。结合SSA扩展形13 东南大学博士学位论文式的优点,该抽象方式能够达到强更新的分析效果。例如,图2.9是顺序结构抽象示例,在示例中,左边是源程序,中间是相应的SSA扩展形式,右边是每条语句的公式。求解该结构的公式可获知语句5处变量d的类型是T2,而不是Tl或T2,体现了强更新的精度优势。a;newTl();b;BOWI"20;C5a;C=b;d=c;al;Tl;bt=T2;CI二aI;c2=bfidl=c2;(al=T0(bl=.T2)(cl<->a0(cq<-}b1)(dl<-"c2)结构抽象:(al=T1)A(bl=T2)^(cl=a1)A(C2=b1)A(dl-c2)求解结果:Types(a0={Tl",Types(b,产{T2),Types(c1):{T1),Types(c2)={T2),TypeS(d1)={T2}图2.9顺序结构抽象示例2)分支结构抽象分支结构与抽象顺序结构相同,也是将结构中有关语句的公式取交。得益于SSA扩展形式,我们能够仍然用“A”而非“v’’联结各分支的公式,不用于文献【821的方法,这样做的好处是,当抽象多重分支结构时,能够有效避免公式中“A”与“v”相互嵌套的情况,从而大大降低了分支结构公式转换成CNF形式的复杂度。图2.10给出了分支结构抽象的示例。a=newTl();b=newT2();if(P)C2a;elscc=b:al=Tl;bl=T2;if(P)C12aj;elsec2=bl;c3=o(c1,c2);(al=Ti)(hi=T2)(cI÷"a1)(e20b3(c3÷’cI)v(c3”c9结构抽象:(al=Ti)/,(bl=T2)A(Clg-"a,)^(e20b1)^((c3付cI)v(c3付c2))求解结果:Types(ax)2{TI},Types(bt)={T2},Types(c0={TI},Types(c2)={T2),Types(c3)={Tin,T2)图2.10分支结构抽象示例3)循环结构循环结构的抽象相对复杂一些。首先,我们仍然将结构中有关语句的公式取交作为原始公式,但该公式并不能直接用于结构的分析。在进一步分析原因之前,我们首先给出若干定义。定义2.1赋值图是一个有向图G=<ⅣI州∥o正>,其中:(1)节点集为%u‰。G包含两类节点,一类是表示具体值的节点,我们称这类节点为值节点,用‰表示值节点集:另一类是表示变量的节点,我们称这类节点为变量节点,用M计表示变量节点集。(2)边集D虬,XM。广}M研.。G包含两类边,一类是变量节点到变量节点的有向边,另一类是值节点到变量节点的有向边。定义2.2我们称赋值图上节点1"1,到节点砌的路径为赋值路径,两点间的赋值路径可能不只一条,我们用AssPath(n,"n2)表示节点聆,到节点坳的所有赋值路径的集合。我们用赋值路径表示,程序执行过程中,值经过若干中间变量流入目标变量的过程,因此一个合法的赋值路径应该包含值节点。而由定义2.1可知,值节点只有出边,没有入边,因而值节点不可能是赋值路14 东南大学博士学位论文径的中间节点,从而我们可以得出这样的结论,即合法赋值路径的起始节点一定是值节点。如果我们用值节点表示类型(或null),变量节点表示变量,那么类型(或null)在变量间的传播可以用赋值图和赋值路径表示出来(图中,我们用大写字母表示值节点,小写字母表示变量节点)。由程序抽象出的命题公式可以构造出赋值图,构造方法非常简单,只要首先为公式中的每个变量(或值)构造单独的节点,然后由形如“(变量名=值)”的子式构造“值一变量名”的有向边,由形如“(变量名H变量名)”的子式构造“变量名专变量名”的有向边。赋值路径则从赋值图中抽取。例如,图2.11是赋值图及赋值路径的示例。图2.11(a)上方是一程序片段的公式,图2.11(b)是由该公式构造出的赋值图,图2.1l(a)下方是从该赋值图上抽取的合法赋值路径。命题公式:(aI-T)^(cI付aI)^((c3付c1)V(c3HaI))赋值路径:Path(T,al产{T.啪l}Path(T,C3)={T—蛆l—*I_c3,10aI—c3)(a)图2.11赋值图及赋值路径示例循环结构SSA扩展形式在结构中添加的a函数语句会导致由该结构原始公式构造出的赋值图含有带环的赋值路径。例如,如图2.12(a)所示,循环结构体的原始公式是由语句5至语句ll的公式组成的合取式,由该原始公式构造出的赋值图(见图2.12∞)中含有的带环赋值路径为a2—}b3—争b2—手c3—手c2—》t1—÷a3—}a2实际上,这些带环赋值路径都是结构原始公式中的某些合取子式(原始公式转换成析取范式后其中的某些析取项)引入的,例如上述路径就包含在子式(a2<-÷a3)A(b2付b3)^(c2壬专c3)^(tl÷坳)^(c3Hb2)^(b3÷}a2)人(a30t1)的赋值图中。la=⋯:2b=newT0;3c=⋯:4while(P)(5678t=c:9C=b:10b=a二lIa=t:12,al。⋯;bl=LCt2⋯;while(P){a2=o(aI’a3);b2=“bl,b3);c2=0(cI,c3);tt2c2;C3=b2;b3=az;a32tI;)(al=⋯)(bl=T)(cl=⋯)(a#->a1)v(a2/,-}a3)(b2Hbt)v(b2÷}b3)(c20eov(c2Hc3)(tlHc2)(c30b2)(b3<-}a2)(a3<->tD结构的原始抽象:((a2付a1)V(a2Ha3))^((b2壬÷b1)“k付b3))^((c2钟cI)V(c2Hc3))A(tl<-"}02)A(c3《-*b2)^(b3t÷a2)^(码付t1)验证后的结构抽象:((a2÷÷a1)^(b2Hbl)^(c2Hcl)^(tl÷屹)^(c3÷÷b2)^(b3<-->a2)A(a3<--}tI))v((a2<-->a=)^(b2<-}bi)^(c2付c3)^(tI付02)^(c30b2)A(b3<--}a2)A(a3<-->t1))V...v((a2<---》a1)A(b2÷岫3)^(02Hc3)^(tl毗)^(c3付b2)A(b3<-->a2)A(a3<-->t!))(a)图2.12循环结构抽象示例由原始公式构造出的赋值图:a1a3L/a21blb3\▲cl\■这些赋值图中含有带环赋值路径的子式妨碍了循环结构原始公式的直接求解。因为从语义上它们可满足当且仅当包含的变量的取值相同,由于我们无法限定SAT求解器求解它们时所尝试的类型范围,因此变15 东南大学博士学位论文量类型的求解结果将是源程序中声明的所有类,这显然是错误的。因此循环结构的原始公式不能作为结构的最终抽象,需要将其中此类子式剔除。又由于这类子式蕴含的带环赋值路径是不合法的(不含值节点,即类型节点),因此它们并非程序执行过程中类型传播的正确描述,因而剔除它们不会影响循环结构分析结果的正确性。从循环结构原始公式中剔除蕴含带环赋值路径的合取子式的方法步骤是:(1)将原始公式转换成析取范式:(2)由每个析取项(是一个合取子式)构造赋值图,若赋值图中含有强连通分量,则舍弃该项;(3)将所有剩下的项重新组成析取范式,作为循环结构的抽象。我们称这一过程为对原始公式的循环验证。·可以计算出,循环验证需要验证的子式的个数是丌m。局,其中m是循环结构SSA扩展形式中a函数的个数,岛是第f个。函数参数的个数。验证一个子式的复杂度由构造赋值图的复杂度和求强连通分量的复杂度组成,前者的复杂度是O(时P)(其中刀是节点个数,e是边的个数),后者的复杂度也是O(时P),因此总的复杂度是旷.O(以+e)(七通常等于2)。由此可知,循环验证的时间复杂度是指数级的,但是当m不大时(我们将在下一小节介绍减小m的方法),上述循环结构的抽象方法是可行的。虽然抽象循环结构比较复杂,但相比循环结构的传统分析方法(反复迭代分析直至达到不动点),我们的方法具有如定理2.1所述的显著优势。定理2.1基于循环结构抽象公式求解的分析方法无需反复迭代。证明:对于循环结构体内的任一变量,我们考查类型第一次流入它的最短赋值路径。遍历该路径相当于按照一定的顺序执行了结构体内的某些语句,这些语句的执行顺序不同于行文顺序,并且结构体内不同的语句最多被执行一次。传统分析方法要遍历该路径可能需要对结构体迭代分析多次。而由于结构抽象出的公式含有控制流信息,囚此经过循环验证后的公式蕴含了该最短路径,对结构公式求解一次即可遍历该路径,因而无需反复迭代。例如,对于图2.12的程序示例,赋值路径T.专b_◆c—争t.÷a是源程序Path(T,口)中的一条最短路径,传统分析方法需要对结构体迭代两次才能遍历该路径。而赋值路径T._"bl—岫2—}c3—"c2—争tl—"a3是源程序SSA扩展形式Path(B,a3)中的一条最短路径,该路径蕴含在循环结构的公式中,对公式求解一次即可遍历该路径。4)结构嵌套以上我们介绍了三种基本程序结构的抽象方法,下面我们讨论基本结构相互嵌套时的抽象,然后再将抽象方法推广到一般结构上。我们运用递归分析方法讨论嵌套结构的抽象。基本结构的嵌套可分为顺序结构、分支结构以及循环结构分别嵌套其它结构(可以是任意一种基本结构,也可以是嵌套结构)等三种嵌套结构(分别如图2.13(a)、图2.13(b)和图2.13(e)所示)。对于每种嵌套结构,我们将它分解成多个部分,假设每个部分已经过抽象并且经过循环验证(即图中的公式乃、乃、乃、F4)。对于前两种嵌套结构(图2.13(a)幂11图2.13(b)所示),它们的公式是各部分公式直接取交,由于联结不会产生新的带环赋值路径,因此无需对复合公式进行循环验证。对于第三种嵌套结构(图2.13(c)所示),它的公式也是各部分公式的交,但由于联结后的复合公式可能会产生新的带环赋值路径,因此需要对它进行循环验证后才能作为该结构的公式。由于每种嵌套结构的公式都是将各部分的公式取交,这意味着,我们也可以对这些嵌套结构进行直接的抽象,也就是说直接将结构中有关语句的公式取交并循环验证,而无需采用上述的先逐渐往下分解成基本结构后抽象,再逐渐往上复合的递归抽象方法。16 东南大学博士学位论文》⋯需凡{曲乃函囱凡、~l:::::一L:二=::rF’}裔要对。n^如^,,,重新验证[圈一凡I◆乃J陬网一图2.13结构嵌套抽象示例F’八F2入Fs心l但另一方面,递归抽象方法的优势是能够降低对较大规模程序的公式进行循环验证的复杂度。例如,如果一个程序片段具有多层循环结构,或者是若干个循环结构顺序组织在一起,那么若对该程序片段的原始公式进行整体循环验证,则由于0函数个数较多,验证复杂度较高;而若采用递归抽象方法,则可以对程序片段进行逐层验证或分部验证,这将大大降低验证的复杂度。因而,递归抽象方法使得我们对循环结构的抽象过程是可行的。.由上述讨论我们发现结构抽象具有两个特点:其一,结构的公式是结构内有关语句公式的交;其二,只有循环结构内的公式才需要进行循环验证。鉴于此,我们将抽象方法进一步推广到一般程序结构上。算法2.1给出了适用于任意结构的通用抽象方法,其中计算图G的极大强连通分支集合公式的函数caIStrConComForm如算法2.2所示。由于该算法基于程序的控制流图CFG,因此它适用于抽象任意结构的Java程序(例如程序中包含异常处理语句、带标号的continue或break语句等)。输入:SSA扩展形式表示的程序片段输出:抽象jlj的命题逻辑公式算法:begin构造程序片段的控制流图吕ifg是强连通图then取消g最外层的回边;endif求g中极大强连通分支的集合SCGSs;calStrConComForm(Szs);将各分支公式及g包含的其它有关语句的公式取交组成复合公式£ifg是强连通图then对f做循环验证:endifreturn£end算法2.1通用抽象方法输入:强连通分支集合SCGS。输出:每个分支的命题逻辑公式算法:beginifSCGSg_锄then严程序不包含循环结构·,return该程序片段中有关语句公式的交:else产程序包含循环结构·/for每个极大强连通分支g’SCGSgdoifg’规模不大或者其内部不包含子循环结构then将g’作为一个整体进行抽象并做循环验证;retum验证后的公式:else取消g’最外层的回边;求g’的极人强连通分支的集合Sg·;calStrConForm(Ss,);将各分支公式及g’包含的其它有关语句的公式取交组成复合公式£对f再次做循环验证:return£endifendforendifend17算法2.2强连通分支集合公式求解算法calStrConComForm军一囹◆圃◆圃◆圃一◆一◆一◆一◆一 东南大学博士学位论文2.4程序抽象进阶:方法抽象本节我们详细讨论方法的SSA扩展表示形式、方法抽象以及方法概要(即图2.4流程中方法抽象步骤一和步骤三)。我们以方法为单位进行抽象,程序的抽象是由方法抽象生成的。抽象方法时需要方法以SSA形式表示,但传统SSA形式并不适合Java方法,因此我们对其进行扩展。扩展不仅涉及增加数组与属性的表示,还涉及方法锚点的设置。为了进一步缩小方法公式的规模,我们对方法原始抽象进行部分求解,获得方法概要。下文我们首先介绍数组和属性的表示,然后介绍方法锚点,接着讨论方法SSA扩展形式的构造,最后介绍方法抽象以及方法概要。2.4.1数组和属性的表示数组和属性的静态分析存在不确定性,抽象它们的难处在于要使得求解结果是对真实情况的安全估计(safeapproximation),因此如何在SSA扩展表示形式中涵盖所有可能性就显得极为关键。1)数组的表示数组静态分析时,由于元素索引很难静态求值,因此被访问数组元素的判定是不确定的,这使得数组元素难以被准确的表示出来。例如,如图2.14(a)所示,假设T2是Tl的子类型,语句5处变量b的实际类型与变量i的值有关,若i为0,则b的类型为Tl;若i为l,则b的类型为T2。由于i的值无法静态获取,因此无法确定元素a[il应该表示为a【l】还是a【21。为保证分析是安全的,我们对数组元素的引用做保守的估计,也就是说,当引用任意的数组元素时,获取的是当前所有元素的值。因而对于图2.14(a)而言,语句5处变量b的类型是Tl或T2。TIBa=newTl【2】;a[O】=newTl();a[1J=rlcwT2();i=EXP;Ttb=a【i】;(a)图2.14数组表示示例al=null;a2=双al,TI);a3=以a2,T2);il=EXP;Tlbl=a3;(b)为此,我们在SSA扩展形式中对Java源程序做如下变换:·将形如“类型名口数组名=new类型名[长度】;”的数组创建语句替换为形如“数组名=null;”的取值语句。·将形如“数组名【索弓11=表达式;”的数组元素赋值语句替换为形如“数组名=D(数组名,表达式);”的0函数语句。·将形如“/hs=数组名[索引】;”的数组元素引用语句替换为形如“lhs=数组名;”的数组名引用语句,其中lhs(1efthandside)表示语句的赋值符号左边部分。上述程序变换的含义是利用0函数来收集所有赋给数组元素的值,并将这些值赋给数组变量,通过把对数组元素的引用修改为对数组变量的引用获取当前所有元素的值,数组变量的初始值为null。2)属性的表示Java语言的属性分为静态属性和非静态属性:静态属性也称为类属性,是指在类中声明的具有static修饰符的变量,或者是在接口中声明的变量(无论是否具有static修饰符),该属性具有全局可见性:非静态属性也称为对象属性,是指在类中声明的不具有static修饰符的变量⋯引。对象属性静态分析的不确定性是由别名关系引起的。当多个变量指向相同的对象时,它们之问就存在别名关系,通常称这些变量互为别名。别名关系使得我们不能按照字面上来表示对象属性的引用。例如,在图2.15(a)的程序片段中,若语句1处变量v和和语句3处变量W不是别名,则语句6处变量s的类型是T1;若它们是别名,则变量S的类型是T3。因而语句6处对象属性v.f的表示就难以选择,若还是表示为v.f贝O得出前者的分析结果,若修改为w.f则得出后者的分析结果。18 东南大学博士学位论文对象属性的表示不仅受到不同变量间别名关系的印象,还会受到同一变量在不同程序点处别名关系的影响。同样在图2.15(a),假设语句1处变量v与语句3处变量W不是别名,那么若语句8处变量v与语句1处变量V是别名,则语句9处变量t的类型为Tl,否则不是Tl。由此可见,表示对象属性不像表示普通变量那样简单。V。⋯;v.f=ncwTlO;w2⋯:w.f=new聪);w.f=newL();s=v.£U=w.£V2⋯:t=v.£(a)IVl5⋯:2vi.6=TI;3w1.fl=o(null,VI-f1):4v2.fl=o(null,v1.f1);5wl=⋯;6W1.易=T2;7v卜乞=o(v1.矗,W1.fg;8V2.乞=畎V2.fl,WI.B);9Wl。6=T3;10VI.6=o(v1.丘,W1.B);1V2.f3=o(V2.最,W1.6);128l=V卜£;13Ul=W1.f3;14V2=⋯;15tl=v2.fi;(b)图2.15对象属性表示示例如果我们能够预先获知变量间的别名关系,那么就可以精确的表示程序中的对象属性。例如,对于图2.15(a),著语句1处变量v和语句3处变量W不是别名,则无需修改语句4:若它们是别名,则可将语句4修改为“S=w.f;”,同理可对语句9做相应的改动。但要获知变量间的别名关系需要对程序进行指向分析(或别名分析),一来这给类型分析带来了较大的代价;二来指向分析(或别名分析)离不开程序调用图,因而它们之间存在相互依赖的关系。因此,前人大都采取基于属性的分析策略,将所有变量的同名属性用同一个变量表示,换句话说,该策略认为拥有相同属性的变量都互为别名。我们在别名关系上也做同样的假设,但我们采取属性敏感的策略,即区分不同变量的同名属性,将它们表示为不同的变量。我们通过添加D函数语句来处理别名关系带来的不确定性:对于每一个形如“变量名.属性名”的对象属性引用,我们在控制流上位于该引用点前的每一条不同变量上同名属性的定义语句后添加。函数语句。另外,我们通过添加下标的方式重命名对象属性的变量名和属性名,并且变量名的下标与最接近的前向(控制流上位于前面的)同名变量的下标保持一致,换句话说,如果之后该变量被重新定义,那么其下标加l,则后向(控制流上位于后面的)对象属性的变量名的下标也相应的加1。这种对象属性重命名方式的优点是既能够区分不同对象的同名属性,又不失对同一对象属性的强更新能力。对于顺序结构中两条对象属性定义语句:·若属性的变量名下标相同,则说明它们是同一个对象上的属性,那么后一条语句就能够强更新前一条语句;。·若属性的变量名下标不同,则说明它们可能是不同对象上的属性,那么就不能强更新,并且还需要在语句后添加痧函数语句。图2.1sO)是图2.15(妙陧序示例的SSA扩展形式。图中,语句6处W1.f2以及语句9处W1.f3的变量名下标与语句5处Wl保持一致。需要指出的是,W1.fl定义语句(语句3)反而在Wl定义语句(语句5)前,这是由在语句2后添加W1.f的D函数语句导致的,添加。函数语句是因为语句5处变量W1可能与语句l处变量vl是别名。在该图中,由于假定vl和Wl是别名,我们添加了语句3、语句7和语句lO,由于假定vl和V2是别名,我们添加了语句4、语句8和语句1l。对基于该图抽象得到的公式进行求解可分析出变量Sl和tl的类型为Tl、T2或T3,变量Ul的类型为T3,而如果采用基于属性的策略分析则变量S和u的类型都是T卜T2或T3。由此可见,屙眭敏感策略比基于属性的策略更加精确。对象属性表示形式转换的具体过程分为五步:19 东南大学博士学位论文(1)添加普通变量的控制流a函数语句;(2)对方法中的普通变量以及属性的变量名重命名;(3)添加对象属性O函数语句;(4)添加对象属性的控制流O函数语句;(5)对对象属性的属性名重命名。这里我们给出第三步的算法如算法2.3所示,其它步骤将在2.4.3节中介绍。输入:Java方法的控制流图CFG算法:beginworklist=O:for方法中的每个形如”V;.f"’的属性引用dofor由该属性所在基本块的第一条语句至该属性引用语句的每一条语句doif该语句足对形如”wi.f’的属性的定义,13t(v≠w)或(v==W且i≠j)then在该语句后添加形如”Vi.f=以vi.ewj.f)”的语句;endifendfor将该基本块的前驱节点加入worklist;whileworklist≠Odo从worklist中取;{{一个基本块节点:if该基本块没有被处理过thenfor基本块中的每一条语句doif该语句是对形如”wi.f’’的属性的定义,f1.(v≠w)或(v—W且i≠j)then在该语句后添加形如”vi.f=o(vi.£wj.o,’的语句;’endifendfor将该基本块标记为已处理过,并将该基本块的前驱节点加入worklist;endifendwhileendforend算法2.3对象属性。函数语句添加算法类属性的表示则不受别名关系的影响,因为虽然类属性可以通过不同的变量来访问,但访问的都是同一个物理空间。因此,我们对类属性直接采用“类型名.属性名”的形式表示,并且只对属性名重命名。图2.16给出了类属性表示的示例。C.f=newTl();v=C.£C.f=new1"2();C.f=newT3();W=C.£(a)C.fl=TI;v1=C.fi;C.f2=T2:C.6=L;Wl=C.6;(b)图2.16类属性表示示例2.4.2方法锚点方法锚点是方法公式中特殊的变量,方法公式通过它们与外界进行值的传递。进行过程间分析时,存在调用关系的方法的公式是通过方法锚点联结在一起的。伴随着每个方法公式,都有一份方法锚点表,联结两个方法的公式时需对照各自的表将对应的锚点用逻辑等价关系联结起来。方法锚点是在构造方法SSA扩展形式时设置的,抽象方法时则从形式中整理山方法锚点表。方法锚点分为入口锚点和出口锚点,方法公式通过入口锚点接受外界传递进来的值,通过出口锚点将方法内部的值传递出去。方法的入口锚点共有五类,分别与形参、类属性、调用方法返同值、从调用方法返回的类属性、以及从调用方法返回的实参有关。方法的出口锚点共有三类,分别与方法返回值、方法返回的类属性、以及方法返回的形参有关。下面我们详细介绍每一类锚点及其设置方法。20 东南大学博士学位论文1)形参锚点当调用方法时,Java通过传值方式将实参的值传递给形参ll12J,此时形参和实参是一对别名。方法不仅可以引用形参本身,还可以引用形参的属性以及属性的属性等等。在形参被重新定义前,方法对形参的属性以及属性的属性等的定义会间接影响到实参,而当形参被重新定义后,其与实参就有可能不再是别名,那么对形参的任何改变不一定会影响到实参。需要指出的是,方法的形参不仅包括声明的变量,还包括隐含的this伪变量。我们在方法入口设置形参入口锚点以接收实参传递的值,在方法出口设置形参出口锚点以将方法内部影响实参的赋值传递出去。形参入口锚点集包括形参变量本身、形参的属性、形参属性的属性等(以此类推直至属性是Java预定义的类型,为了方便论述,下文我们将变量韵属性、属性的属性等所有属性称为由该变量衍生出的属性)。形参出口锚点集包括由形参衍生出的属性,但不包括形参变量本身,因为对形参本身的定义不会对实参产生影响。我们结合实例说明如何在方法的SSA扩展形式中设置形参锚点。图2.17是方法形参锚点的示例,其中,图2.17(a)是一程序片段,方法foo拥有类型为A的形参a,类型A声明了一个类型为T1的属性f’类型Tl声明了一个类型为他的属性g。图2.17(b)是方法foo的SSA扩展形式(只包含了形参锚点),其中,al,a1.fl以及tmpl.91是形参入口锚点,分别接受实参本身的值、实参的属性f的值,以及实参属性f的属性g的值。由于我们假定方法中属性或者方法的访问路径不超过两位,因此我们通过临时变量tmpI来访问实参属性f的属性。语句2、3、4和6是不完整的a函数语句,不被抽象为命题公式,它们的作用是方便SSA扩展形式的转换。语句后的注释标识入口锚点的身份,用于抽象方法时识别这些锚点。例如,语句4的注释说明aI.£是第二个形参a的属性f的入口锚点(第一个形参是this)。a1.f3以及tmp2.&是形参出口锚点,语句17和19用于定位出口锚点,它们也不被抽象为命题公式。我们通过语句左边变量的取名标识右边出13锚点的身份。例如,语句17表明a1.6传递第二个形参的属性f的值,语句19表明tmp2.92传递第二个形参属性f的属性g的值。需要指出的是出口锚点a1.6中变量名a的下标为l,表示该属性是入口锚点al的属性,因为al与实参才是一对别名。我fI、J称语句2、3、4、6、17和19这类语句为锚点标识语句,入口锚点的标识模式为“inparai.fieldAccessPath”,出口锚点的标识模式为“outparai.field_AccessPath”,其中f是形参的序号,fieldAccessPath是属性的访问路径(标识中我们不限制访问路径的长度)。1publicclassTi(2publicT2g;3)4publicclassA(5publicTi£6)7publicclassB(8publicvoidfoo(Aa){9AU=a:10TlV=乱E11a.f=flewTI();12a2newA0;13a.f=newT30;14TlW=乱£15w.92newl"20;16)17}(a)publicvoidfoo(Aa)fthisl=o();//in_.para0aI=00;//inparalal。‘=00;//inparal.ftmpl=a卜fl;trapl.蜀200;//in_paral.f.gtmp2.gl=e(null,tmp卜gO;AUl=aftTIVl=a1.fi;a1.如=IlCWTl0;a2=A;a2.fl=T3;aj.f3=D(a卜£,a2.f1);TIW1=a2.fl;w1.gl=T2;trap2.922o(tmp2.gl,w".gO;out..paral.f=a1.f3;trap2=8.I.f3;out__paral.f.g;tmp2.92;图2.17方法形参锚点示例算法2.4给出了形参锚点标识语句添加算法,其中“Smark”表示取mark的字符串值,对属性进行处理的函数fieldAdd()女[I算法2.5所示。2l●23456789m¨挖B¨搭M"幅侈加 东南大学博士学位论文输入:Java方法CFG算法:beginfor方法的第i个形参vdo输入:属性v.f"标识mark算法:beginifv.f具有属性thenmark=“para"+i-l:令tmp足随机生成的变量名;在方法入口添加形如“V=oO;in在方法入口添加形如“=v.£”的语句;.tmp$mark”的语句:ifv是形参thenif形参v具有属性then在方法出口添加形如“tmp=v1.f;”的语句;for形参v的每个属性fdoelse在方法出口添加形如‘‘tmp=v.fi”的语句;endifmark+=“.f’’;forv.f的每个属性gdo在方法入口添加形如“v.f=00;//in—mark=mark+“.g’;‘Smark"的语句;在方法入口添加形如“tmp.g=00;//in一在方法出口添加形如“ontSmark=-$mark”的语句;v卜f”的语句;在方法出口添加形如“out$mark=fieldAdd(v.f,mark);trap.g;”的语句;endforfieldAdd(tmp.g,mark);endifendforendifend算法2.4形参锚点标识语句添加算法算法2.5处理属性的函数fieidAdd2)类属性锚点Java语言的类属性具有全局可见性【ll21,方法内部可以直接访问类属性从而和外界相互影响。类属性入口锚点集设置在方法入口处,包括类属性本身以及由类属性衍生出的属性;类属性出口锚点集设置在方法出口处,包括类属性本身以及由类属性衍生出的属性。图2.18给出了类属性锚点的示例,其中,图2.18(a)是源程序,图2.18(b)是方法foo的SSA扩展形式(只包含了类属性锚点)。图2.18(b)中,类属性入口锚点为A.fl和tmp卜91,出口锚点为A.最和trap2.92,语句2,4,13,15是锚点标识语句。入口锚点的标识模式为“in”,出口锚点的标_staticField.fieldAccessPath识模式为“outstaticField.fieldAccessPath”。1publicclassTI{2publicl29;3}4publicclassA{5publicTlE6}7publicclassB{8publicvoidf000{9TlV=A.£10T2W;v.g;11A.f=newTl0;12V=A.e13v.g=flewl20;14)15,(a)Ipublicvoidf000{2A.fj=00;//in_A.f3tmpl=A.fl;4tmp=.gI=o();Hin—Af:g5V1.gl=o(null,tmp卜gI);6tmp2.gl=o(null,tmpt.gD;7vl=A.fl;8w12VI.gt;9A.丘=TI;10V2=A.如;11V2.gl=亿:12trap2.922o(tmp2.gl,V2.91);13OUt-A.f=A.f2;14tmp2=A.疋;15ont』.f.g2tmp2.92;16’(b)图2.18类属性锚点示例类属性锚点标识语句添加算法如算法2.6所示。31方法返回值锚点若方法具有引用类型返回值,则还需在方法出口设置返回值出口锚点。返回值出口锚点集包括返回的变量以及由该变量衍生出的属性。由于Java方法可以拥有多条返回语句,因而可能有多个返回变量,如果我们为每个返回变量单独设置锚点则显得较为繁琐,为此我们增加一个中间变量ret,并通过a函数收集所有返回变量,然后以ret变量以及由它衍生出的属性作为返回值出口锚点。22 东南大学博士学位论文输入:Java方法CFG算法:beginfor程序的每个类属性A.fdomark=“A.if;在方法入口添加形如“A.f=00;//in_$mark"’的语句;if类属性A.f具有属性thenfor类属性A.f的每个属性gdomark+=“.g’;在方法入口添加形如“.g=00;//in_$mark"的语句;在方法出121添加形如“out_$mark=A.f.g’的语句;fieldAdd(A.£&mark);endforendifendforend算法2.6类属性锚点标识语句添加算法图2.19给出了方法返回值锚点的示例,其中,图2.19(a)是源程序,图2.19(b)是方法foo的SSA扩展形式(只包含了返回值锚点)。如图所示,方法foo有两条返回语句,分别返回变量S和变量u指向的对象,假设类型T1不再含有引用类型属性,则方法foo返回值出口锚点是retl和retI.f4,语句12和13是锚点标识语句,出口锚点的标识模式为“outretfieldAccessPath”。1publicclassA{2publicstaticTI£3)4publicclassB{5publicAf000{6if【P){7AS2newA0;8s.f=newTl0;9returns:10)else(1IAU=newA0;12U.f2newT2C);13retumu:14’15)16}(a)1publicAfooO{2if【P)(3ASI=A;4SI.£=TI;5retl.G=烈null,SI.f0;6)else{7AUl=A;8U1.fI=佗;9retI.£=o(null,U1.f1);lO)11reh=“SI,u1);12retl.f4=o(reh.f2,reh.G);13out_ret2rch;14out—ret.f=reh.f:l;15}(b)图2.19返回值锚点示例返回值锚点标识语句添加算法如算法2.7所示。输入:Java方法CFG算法:begin//假设方法有i(1,其中:(1)Form是方法的命题逻辑公式,该公式由方法SSA扩展形式中如图2.7所示的三类语句的公式通过“^”联结而成。 东南大学博士学位论文输入:CFG节点代表的基本块B,标记tag算法:beginforB中的每一条赋值语句或取值语句Adoif【ta乎一NoltMAL)then,/变量V可以是普通变量,数组变量或类属性forRHS(A)中的每一个变量V或RHS(A)qb的每一个对象属性v.f或LHS(A)@的对象属性v.fdo将v替换为vi,其中i=Top(Stack(v));endforitlLHS(A)为变量v)theni=Count(v);将V替换为vi;pushiontoStack(v);Count(v)=i+1;endifelse//铲FIELDforRHS(A)中的每个对象属性Vk.fdo将vk.f替换为Vk-fl,其中i=Top(Stack(vk.f));endforitlLHS(A)为Vk.0theni=Count(vk.f);将vk.f替换为vk.f;;pushiontoStack(vk.f);Count(vk.f产件l;endifendforfor每个B’∈Suce(B)doj=WhichPred(B’,B);forB’中的每个D函数语句Fdoif【tag—.NORMAL)then,/假设F的第j个操作数是变量V将v替换为vi,其中i=Top(Stack(v));else,/假设F的第j个操作数是对象属性vk.fif((i=Top(Stack(Vk.D))!=0)then将vk.f替换为Vk.fi,其中i=Top(Stack(vk.f));else将vk.f替换为null;endifendforfor每个B’∈Children(B)dorename(B’);endforforB中的每一条赋值语句或取值语句AdopopStack(oldLHS(A));endforend算法2.12变量和属性重命名函数rename(2)APList是方法锚点表,该表记录了方法每个锚点的信息。锚点信息是一个三元组,kindE{in,out}表示锚点的类型,in表示入口锚点,out表示出口锚点,identity表示锚点的身份,其模式为相应锚点标识中去掉“in”或“out_”前缀后剩下的部分,variable是具体的变量或属性。例如,图2.21(a)是方法m的SSA扩展形式,其中sf是类型A的静态属性,该方法的抽象如图2.21(b)所示,方法锚点表中的项“(in,A.s£A.sfi)”表明该方法关于类属性A.sf的入口锚点为A.sfl。publicm0{A.sfi200;//in—A.sfml=C;Vl=A.sfi;out_A.sf2A.sfi;}方法公式:(ml=C)^(v12A.sfi)方法锚点表:(in,A.sf,A.sfi)(out,A.sf;A.sfi)(a)(b)图2.2l方法抽象示例在SSA扩展形式的基础上获取方法抽象的过程分为两步:1)抽象三类语句并提取锚点信息。这一步只需从前往后遍历一遍方法,针对每一条语句s:·若S形如“v=U;”,则将它抽象为“(v=U)”;·若S形如“v=w:”,则将它抽象为“(vHw)”;·若S形如“v=.a(t"⋯,U,...,w);”,则将它抽象为“(VHt)v⋯v(v=U)v⋯v(v<-->w)”;·若s形如“/hs=a();//inarchor-identity”,则构造锚点信息(in,archor-identity,lhs)力n入方法锚点表;·若S形如“out=则构造锚点信息,入方法锚点表;_archor-identiO,rhs;999(outarchor-identity,rhs)力n2)调用通用抽象算法(算法2.1)由语句的公式获得方法的公式。27 东南大学博士学位论文2.4.5方法概要属性敏感的对象属性表示方式以及方法锚点的设置大大增加了方法公式的规模,可能导致生成的程序公式达到或超出SAT求解器的求解能力,从而急剧的降低分析的效率,因此需要想办法缩减方法原始公式的规模。仔细分析方法的公式,我们可以发现这样的规律:第一,除入口锚点外,其它变量最终的取值要么是常量,要么依赖于入口锚点,或者前两种可能性都存在:第二,如果变量的取值不依赖于入口锚点,那么它必定取常值。基于此,我们认为可以从两方面简化方法公式:在变量通过其它变量间接依赖于入口锚点的情况下,如果能够确定它们间的依赖关系,那么可以将该变量的公式整体替换为该变量与入口锚点间的公式,从而将间接依赖关系简化为直接依赖关系;在变量取常值的情况下,由于变量的值不会随着调用环境的不同而改变,因此如果能够求出其值并记录下来,那么就可以把相关的子式删除以简化公式。例如,在下面的方法公式中(其中i卜i2是入口锚点,01是出口锚点,vl、v2是局部变量,T卜T2是具体类型),(VI付il)v(vlHi2)Vm÷w1)V(V2_T1)V(01-T2)V(v3付VI)变量v2既通过变量vl依赖于il和i2,又取常值Tl,变量v3仅通过变量Vl依赖于i1和i2。因此,针对变量V2,我们可以将子式“(V2付v1)”替换为“(V2付il)v(V2付i2)”,并删除子式“(v2=TI)”,同时记录下V2的值可以是Tl:针对变量v3,则将子式“(V3Hvl)”替换为“(v3Hil)v(V3Hi2)”。需要指出的是,变量与入口锚点依赖关系的化简可能会增加关于该变量的予式的个数,例如上述示例中v3子式的个数由1个增加到了2个。但这只会发生在变量同时依赖于多个入口锚点的情况下,现实中这种情况并不多见。一般的,变量只依赖于一个入口锚点,此时化简虽然没有改变该变量的子式个数,但简化了该变量类型的推导过程。定义2.4方法概要(methodsummary)是一个三元组,其中:(1)Form是方法的命题逻辑公式,该公式是方法抽象中公式的化简。(2)APList是方法锚点表,该表与方法抽象的锚点列表一致。(3)VCList是变量常值表,该表记录了方法原始公式中的变量及其常值。变量常值信息结构是一个二元组,其中,variable表示变量(包括属性),values是该变量的常值表,记录了变量的所有常值。假设原始方法抽象为<尸4list>,P为方法公式。Alist为锚点列表,其中入口锚点为ik(1妯),非入口锚点为vi(1匀9),我们通过对尸进行部分求解获取方法概要,具体步骤如下:首先,求户中非入口锚点变量vi的常值。方法是判断公式’P^1代Hil)^⋯^-1(VjHim)是否可满足,若公式不可满足则表示变量vi的值不是常量,反之则表示变量vi的值可以是常量。在可满足的情况下,通过求出公式的所有可满足解可获得变量vi的所有常值。其次,求尸中非入口锚点变量vj与入口锚点间的依赖关系。变量vi可能依赖于一个或多个入口锚点,我们逐个求vj与每个入El锚点间的依赖。对于入I:1锚点ik,判断vj是否依赖于ik的方法是判断公式P^-1(Vi÷÷il)^⋯八](Vj÷}.k_1)^.1(Vj+-">ik+1)A⋯^一(Vj÷争im)A—COnst(vj)是否可满足,若公式可满足则表示变量vj依赖于ik,反之则表示vj不依赖ik。其中,Const(vj)]壬表示Vi取常值的子式,假设vi的常值为Cl、C2,则Const(vj)y9((vj=COv(vj=C2))。最后,生成方法概要。假设对尸中所有非入E1锚点变量运用上述两步后得到变量vi(1匀aaI.f2)A(UI《--)tmp2.gn)分析结果如表2.2的第三列所示(我们只给出源程序中变量的类型集)。类似可分析方法bar和main,这里不再给出分析过程,只给出分析结果如表2.2的第三列所示。表2.2分析结果SSA扩展形式中类型集源程序中的变量的表示(基于RTA)(基于拓扑排序)方法foo第15行变量aa。(A}{A)第16行变量缸aal{A)第17行属性a.fa1.fl{C}第18行属性aa.f勰卜fl{Cl}第19行变量VVl{C,CI,C2){C2’第20行伪变量thisthisI{Main}(Main}第20行变量VV2{C,cl,c2}{el}第2l行,叟量WWI{C,Cl,C2}{C2}第22行变量uUl{D}方法bar第25行属性扎fa卜厶fC2){C2}第26行属性a.Cgtmp2.gl{D}第27行属性A.sfA.sf2{BI)第28行返叫值rch{CI}{Ci}方法main第3l行变量mml{Main}第32行变量mml{Main}{Main)第33行变量VVl{B,B1){B1)根据分析结果构造出的初始调用图如图2.26所示。根据该调用图,我们确定下一步的分析顺序是方法bar、方法foo和方法main。首先分析方法bar,仍然通过RTA方法估计它的入口锚点,分析结果如表2.2第四列所示。其次分析方法foo,其入口锚点v2、v2.gl、aal.丘、tmp2.91、A.sf2的初始值由方法bar的分析结果获得,分别为{c1)、{D)、{C2}、{D}和{B1),分析结果如表2.2第四列所示。最后分析方法main,其入口锚点A.s如的初始值由方法foo的分析结果获得,为{B1},分析结果如表2.2第四列所示。对比表2.2的最后两列可知,基于拓扑排序的分析比基于RTA的分析更加精确。Ipublicstaticvoidmain(){2八娟=null;3ml=Main;4out_cp32—A.sf=A.sfl;5out_cp32_ar90=ml;6A.sf2200;//in_cp32_—A.sf7V12A.sfi;8)(a)方法main的原始公式:(mI=Main)A(Vl<---}A.sfi)方法锚点表:(in,cp32_A.seA.sf2),(out,cp32_ar90,m1)(out,cp32.A.seA.sfi)简化后的公式:(VI÷}A.st2)常量列表:(mI"Main),(A.sfi,null)(b)图2.25方法main的抽象30图2.26程序调用图甲暑 东南大学博士学位论文1publicvoidf000{方法foo的原始公式:2A.嫡=o()://in—A.sf(trapl.gl--null)A(al=A)^(aal--A)3thisl=0();llinpara0A(a1.fl=C)A(aal.fl=C1)^((a1.如Ha卜fOv(a1.fjH豫I.f1))4tmpl.gl=null;^(VI.÷÷a卜f2)A(tmpj*-"aal.f1)A(tmp3.目付v2.91)5aI=A;A(tmp2<-->aaI.f2)^((tmp3.g_2<->tmp2.gt)v(tmp3.92+->tmps.91))68al=A;A(Wl《---)aaI.6)^(tmps<->aal.6)A(Ul<--}tmp3.92);:ii翼l;方法锚点表:91。孙妾咖:胁融盏in,Acp.s2f峨,A.sfl圳),(in,nr:acpra20啊,this。1k91),VlOl=a,.f2;【1n,cpzuJet’v2J,‘1n,cpzu』cIr吕V2·glJ’1outcp‘20:强l;,..£·丘),,·k·91),_argl(incp20_arglanI(incp20_argltmp21123蠹2囊Lf=a”a^;盟in,cp印220_0_鹕A.sf,㈨A.sf2),’(ou(ou删t,cp2恤0arg∽0,thisaaaal)p2aall.毛|13臼IIpI=1.f1:【out"印2虹a唱l,,‘out,。u—鹕1·t,1J㈡14西谜1.f.g=mtmpl.91.嬲out,cp.s£20_圳ar91.龟呻1.gA∞岬雌舭两’outc15p20A.sf=A.sfl:(o咄A·3f’A·s埘16out_cp20_ar902this|;简化后的公式:l7V22o();//in--印2(_(trap2付勰1.f2)A(tmp3.gl付v2.91)l8V2·gl2o();//in._cp20mt.gA((tmp3.92<-->tmp2.91)v(tmp3.92Hv2.91))19trap3·gl2o(null,v2.91);^(wlH瑟1.f2)^(tmps<->aal.垃)人(uI付tmp2.91)20aal.疋20();//incp20_argI.f21tmp2=嬲卜丘;变量常值表:22tmp2.gl=0();//incp20_ar91.f.g(tmp|.蜀,null),(al,A)23trap3.92=a(tmps.gl,tmp2.91):(缸l,A),(a卜6,C)24A.啦=00;//in_cp20_A.sf(aa|.fI,CI),(a1.乞C)25Wl=觚1.£;(a1.乞C1),(VI,C)26缸np3=aal.乞;(VI,C1),(tmpl,C1)27ul2tmp3.92;28out_A.sf=A.s£;29}(a)IpublicCbar(Aa){2this|=00;//in_para03al=以);//in_paral4a1.£=00;//in__paral.f5tmp|=a1.fl;6tmpl.gl=麒);//in__paral.f.g7tmp3.gl2o(null,tmpl.gO;8ret|.gf=o(null,trap|.飘);9A.s£=o();HiLA.sflOa1.£=C2;11蜘np2=a1.岛;12tmp2.gm2D:13tmp3.925o(tmp3.91,tmpz.gI);14ret|.92。o(reh.gl,trap2.gI);15A.sf2=BI;16tmpp|=C1:17retl=trnpp|;18out_ret=retl;19out_ret.g2ret|.92;20out_paraI.f=a卜丘;21tmp3=a1.如;22out__paral.f.g=tmp3.ga;23outA.sf2A.s6;24}(a)图2.23方法foo的抽象(b)方法bar的原始公式:(tmpl付a卜f1)A(tmp3.91付tnlp卜91)^(rnl.gl<-->tmp|.91)^(a1.f2=C2)A(trnp2<-->a1.6)^(tmp:.912D)^((trap3.92<-->tmp3.gDv(tmp3.92<-->tmp2.91))A((reh.92<->ret|.g|)v(reh.92<-->tmp2.91))^(As分:B1)^(tmpp|=C1)^(tmp3e->a|.6)方法锚点表:(in,A.s£A.sfO,(in,paral,at)(in,paral.£a1.f1),(in。paral.f.g,trap|,gO(in,para0,this0,(out,ret,rot|)(out,ret.g,ret卜92),(out,paral.£a1.丘)(out,para!,£吕trap3.&),(out,A.sf,A.sf2)简化后的公式:(tmpl付a卜f0A(tmps.g|<-}tmp|.91)^(retl.gl付tmpl.91)^(trap3.92<->tmp|.gD^(ret|.&Htmpl.gm)变量常值表:(a卜丘,c2),(trap2,C2)(tmp2.gl,D),(tmp3.92,D)(A.s如,BI),(tmppl,C1)(tmm,c2),(retl,CI)(rot.&,D)图2.24方法bar的抽象(b) 东南大学博士学位论文2.6程序抽象高级ll:过程间分析过程间分析是根据初始调用图(通过RTA分析或上述过程内分析方法构造)将存在调用关系的方法的概要的公式通过方法锚点联结起来求解,然后将求解结果与方法概要中变量常值信息进行综合从而获得类型分析结果.过程间分析又分为上下文不敏感的分析和上下文敏感的分析。直观上,上下文不敏感的分析最多把方法公式联结一次,而上下文敏感的分析则可能把方法公式联结多次。上下文敏感的分析比不敏感的分析更加精确,但分析的复杂度也更高。对于大型程序,上下文敏感下获得的程序抽象可能会超出现有SAT求解器的能力,从而急剧降低分析的效率和精度。为此,我们提出分部分析方法,即将一定长度内调用路径中的若干方法公式联结在一起求解。相对的,我们称将所有方法公式联结起来求解的方法为整体分析方法。理论上,在相同的上下文敏感性下,整体分析比分部分析精确。当然,过程间分析是否上下文敏感与分析采用整体分析还是分部分析是相互独立的。在SAT求解器能力允许的情况下,上下文敏感的整体分析最为精确,上下文敏感的分部分析或上下文不敏感的整体分析(两者间的精度不好比较)次之,上下文不敏感的分部分析则相对最粗糙。下面我们首先给出方法公式的联结规则,然后介绍整体分析方法和分部分析方法,最后讨论以调用路径为上下文的上下文不敏感以及上下文敏感的分析。2.6.1方法公式的联结程序调用图上方法间调用关系的一般模式可归纳为如图2.27所示的多对多模式。该模式表示施调方法calleri(1§9)在某调用点可能调用多个方法calleel、⋯、callee。,并且被调方法calleej可能被多个方法callerl、⋯、eallern调用。一对一、一对多以及多对一模式都是多对多模式的特例。图2.27方法问调用模式我们讨论多对多模式下方法公式的联结。假设在该模式下:1)施调方法calleri(199)的公式为Formula(calleri),调用方法calleej(1匀蜘)的调用点为cp(calleri),调用点实参的出口锚点为ARGout(cp(calleri)),调用点类属性的出口锚点为SFD。ul(cp(calleri)),调用点返回值的入口锚点为RETi。(cp(calleri)),调用点类属性的入口锚点为SFDi。(cp(calleri)),调用点实参的入口锚点为ARGi。(cp(calleri))i2)被调方法calleej(1匀蜘)的公式为Formula(calleej),形参的入口锚点为PARAi。(calleej),形参的出El锚点为PARA。ul(calleej),类属性的入口锚点为SFDin(calleej),类属性的出口锚点为SFDI咖(calleej),返回值的出I=1锚点为REToIIl(calleej)。3)对于出口锚点OV,谓词ConstValue(ov)表示在变量常值表中查找OV所有的常值并返回。则多对多模式下方法公式的联结规则如下述规则2.8所示。规则2.8(多对多模式下方法公式联结规则):numberofconsttm.valtueso,fovFormula(ov—}iv)::=(\/(iv=ConstValuei(ov)))V(iv七÷ov)(1);l。Formula(ARGout(cp(callerl)⋯cp(caller.))-9"PARAin(calleei))::=A(VFormula(ARG删(cp(callerk))---}PARAjnj(calleei)))j=Ok=l(2) 东南大学博士学位论文Formula(SFDo眦(cp(callerl)⋯cp(callern))jSFDi。(calleei))numberofstnticfieldsn:#/\(Vk册比(sFD删(cp(callerk))-}SFD岫(calleei)))j=1Ir=lFormula(RETotl‘(calleeI...calleem)一REk(cp(calleei)))numberofm咖valuesm:≥/\(\/名确u/a(RET,。tj(calleek)_RE‰(cp(calle毛))))j=1k=lFormula(SFD。m(calleel⋯ealleem)一SFDilI(cp(calleri)))numberofstaticfieldsnl:;/\(V7如硎ula(SFD删(calleek)-}SFD呵(cp(calle£))))户lk=lFormula(PARA咖(calleel...calleem)一ARGi。(cp(calleri)))numberoflmramentsIn:≥/\(\∥砌ula(PARA。嘶(cafleek)--}ARGinj(cp(calleIi))))j-Ik=lFormula(calleri⋯callern—calleei)::-Formula(ARGout(cp(callerl)⋯cp(callern))寸PARAin(calleei))AFormula(SFDom(cp(callerI)⋯cp(caller.))专SFDin(calleei))Formula(calleel...calleem哼calleri)::=Formula(RETo眦(calleel...calleem)一RETin(cp(calleri)))AFormula(SFDom(calleel...cailee。)一SFDi。(cp(calleri)))AFormula(PARAom(calleel...calleem)一ARGilI(cp(calleri)))Formula(callerI⋯callern斗calleel...calleem)::=(/\p朋甜la(calleri))A(AForm甜la(cailel⋯caIIek—calleek))iffilk=lA(AFormula(calleej))A(AFormula(calleeI...calleemcall%”(3)(4)(6)规则2.8(9)表明复合公式由四个部分组成,它们分别是所有施调方法的公式、所有被调方法的公式、施调方法向被调方法传值的公式以及被调方法向施调方法传值的公式。其中,多个施调方法向单个被调方法传值的公式包括实参到形参的传递公式以及类属性的传递公式(见规则2.8(7)),多个被调方法向单个施调方法传值的公式包括形参到实参的传递公式、返回值的传递公式以及类属性的传递公式(见规则2:8(8))。规则2.8(2)与规则2.8(3)分别描述了多个施调方法调用点实参和类属性的出口锚点向单个被调方法形参和类属性的入口锚点传值的公式(伪变量this是第零个形参)。规则2.8(4)、规则2.8(5)与规则2.8(6)贝JJ分别描述了多个被调方法返回值、类属性以及形参的出口锚点向单个施调方法调用点返回值、调用点类属性以及调用点实参的入口锚点传值的公式。规则2.8(1)给出了出口锚点OV向入口锚点iv传值的公式的一般形式。由于在方法概要中,OV有可能不仅取多个常值,同时还依赖于若干入口锚点(即OV出现在方法概要的公式中),因此iv与OV的联结包括iv与OV所有常值的联结以及iv与OV直接联结两部分。如果OV不取常值,则前一部分为空,若OV不出现在方法概要的公式中,则后一部分为空。当n等于1时,规则2.8退化为一对多模式下方法公式的联结规则;当m等于1时,退化为多对一模式下方法公式的联结规则;当m和n都等于1时,则进一步退化为一对一模式下方法公式的联结规则。33 东南大学博士学位论文2.6.2整体分析与分部分析整体分析方法的指导思想是利用规则2.8按照初始调用图所示的调用关系,将方法概要的公式全部联结在一起构成程序的完整公式统一求解。分部分析方法的指导思想则是将初始调用图划分为若干子图,然后针对每一块子图,利用规则2.8按照该子图所示的调用关系将方法概要的公式联结起来求解。划分会造成一些调用边的丢失,对于发出这些调用边的节点表示的方法,需要估计出相关调用点返回值、类属性以及实参的入口锚点的初始值,而对于这些调用边指向的节点代表的方法,需要估计出形参以及类属性的入口锚点的初始值。图2.28分部分析方法示例例如,如图2.28所示,我们将原程序调用图划分为三个子图,我们对每个子图单独求解。对于子图l,实际上是方法m2的过程内分析。对于子图2,求解公式是方法m3、方法m4以及方法m5公式的复合,其中方法m3形参及类属性的入1:3锚点的初始值来自估计,而方法m5形参及类属性的入口锚点的初始值来自两方面:一方面是从方法m4传递进来;另一方面来自估计。同理可以获得子图3的求解公式。分部分析过程中方法入口锚点初始值的估计同样有基于RTA的估计以及基于拓扑排序的估计两种。后者的具体过程为:将每个子图压缩为一个节点,则由原图得到子图间的调用图,对新图进行拓扑排序,然后按照排序顺序分析子图,用前驱节点的分析结果来代替对后继节点代表的子图中丢失调用边的方法中方法调用的入口锚点的估计,对于其它入口锚点的初始值仍然采用RTA方法估计。例如,对于上述示例,我们用子图l和子图2的分析结果米代替方法ml中,用子图2的分析结果来代替方法m7中。另外,这两种分析方法都只联结一次递归方法的公式,对方法递归调用点有关入口锚点的初始值使用RTA方法估计。理论上,整体分析的精度优于分部分析,因此,当SAT求解器求解能力比较强,或者程序公式的规模适中时,应当采片j整体分析,否则采用分部分析,并且当进行分部分析时,应当尽可能将子图划分的大一些,使其包含更多的节点。2.6.3上下文不敏感分析与上下文敏感分析上下文不敏感分析和上下文敏感分析的基本方法非常简单:不敏感分析根据程序的上下文不敏感调用图由方法公式构成程序公式并求解,而敏感分析则根据程序的上下文敏感调用图获得程序公式并求解。我们以方法调用路径为上下文,按照调用路径的长短,上下文敏感分析又可分为调用路径氏度有限的分析和调用路径长度无限的分析。理论上,前者的精度低于后者,但是其效率高于后者,而且随着长度逐渐增大,前者的精度将逐渐逼近后者,因此,下文我们重点介绍前者。调用路径长度有限的上下文敏感分析参照以有限长度调用路径为上下文的上下文敏感调用图联结方法公式。我们由上下文不敏感调用图构造所需的上下文敏感调用图。首先定义有向图上节点的分裂操作如定义2.5所示。定义2.5设G是一有向图,刀是G上入度大于1的节点,令刀的入度为,,则节点行的分裂过程如下:首先将"复制卜l份,然后将聆上的Z条入射边平均分配到,个节点(力加厶1个副本)上,使得每个节点34 东南大学博士学位论文的入度为l,最后将刀上的所有出射边复制厶l份分配到厶1个副本上,使得每个副本与n指向相同的后继节点。假设上下文不敏感调用图为G,设定的调用路径长度为k,我们通过对G中的节点进行分裂构造上下文敏感调用图G,,具体步骤为:(I)利用Dijkstra算法求上下文不敏感调用图上从起点到入度大于1的所有节点的最短路径;(2)对那些最短路径小于等于k的节点按照它们的拓扑排序进行分裂;(3)对展开后的调用图再次求从起点到入度大于l的所有节点的最短路径,并对其中最短路径小于等于k的所有节点进行分裂;(4)重复第(3)步直至图上入度大于l的节点的最短路径都大于k。例如,图2.29(a)所示是一上下文不敏感调用图,由该调用图运用上述方法构造出的长度为l的上下文敏感调用图如图2.29(b)所示。(a)(”(c)图2.29由上下文不敏感调用图构造上下文敏感调用图示例通过上述步骤构造出的G,并非传统意义上的以k长度路径为上下文的上下文敏感调用图(设为G”),但G,更优于G”,因为G上从起始节点到某个入度大于l的节点(设为玎)的每条路径长度不一定都小于等于k,按照传统含义,只有那些长度小于等于k的路径才需要复制出一个单独的节点厅的副本,而我们的构造方法则针对每条路径都复制一个副本,因此在G,7中被区分开的方法的不同副本在G7中也被区分开,而在G,中被区分开的方法的不同副本在G,’中却不一定被区分开,从而参照G7获得的程序公式更加精确。例如,图2.29(c)是传统意义上长度为1的上下文敏感调用图,其中方法m4有两个副本,方法m2和m3共享一个副本。而在图2.29(b)中方法ml、m2以及m3都独享方法m4的副本。另外,需要说明的是,基于上下文敏感调用图联结方法公式时,由于同一个方法公式可能会被联结多次,因此需要注意避免重名冲突。本节的最后,我们对图2.22的程序实例进行上下文不敏感的分析。图2.26是其上下文不敏感调用图,参照该图获得的程序公式为(变量加上了方法名前缀)Formula(program)::=Formula(Main.main)AFormula(Main.main--÷Main.foo)AFormula(Main.foo)AFormula(Mmn.foo)AFormula(Main.foo-}Main.bar)AFormula(Main.bar)AFormula(Main.bar---}Main.foo)AFormula(Main.foo-+Main.main)2(main_m15Main)A(main_Vl÷}mairLA.sG)^(foojhisl÷÷main—m1)A(f00_A.sfi--nuli)^(foo_tmp24-ffoo_aal.f2)A(foo_tmp3.gl÷}fooLv2.91)A(f00__W1(==)fooaal.f2)A((footmp3.92÷÷f09jmp2.g,)v(foo_.tmp3.&Hfo虻V2.gD)A(foo_tmp“-)foo_aal.丘)^(fbo.-ul付fIo0.jmp2.gI)^(baohisl付f.oo..thisl).A(bar_A.s毛付矗)o_A.sfl)A(bar_al=A)A(bar__a1.fl=C1)A(bar_tmpl.gl=null)A(bar_tmpt4-}bara1.f0A(bartmp3.gl七÷baljmp卜90A(bar_reh.gl÷÷b2Lrjmp卜90A(bar_tmp3.&HbaI:tmpl.91)^(baUmp3H砚1.f2)A(barreh.&付tmp2.91)A(foo__v2=C!)r,(foo_v2.gl=D)A(foo._aal.f2=C2)A((footmp2.gl=D)A(f00_.tmp2.勖÷÷b可tlnp3.92)A(fOo._A.sf2=BI)A(mainA.sf2<--}foo_A.sf2)分析结果如表2.3所示(我们只给出源程序中变量的类型集)。35 东南大学博士学位论文表2.3分析结果SSA扩展形式中源程序中的变量类型集的表示方法foo第15行变量aal{Al第16行变量砚aal{A}第17行属性a.faj.fl{C}第18行属性aa.f缸卜fl{CI)第19行变量VVl{C2}第20行伪变量thisthisI{Main)第20行变量VV2{C1}第21行变量WWl{C2}第22行变量UUl{D}方法bar第25行属性a.fa1.£(C2}第26行属性a.Egtmp2.gl{D}第27行属性A.sfA.s龟{B1}第28行返回值ret{Ci}方法main第31行变量mml{Main)第32行变量mml·{Main)第33行变量VVI{BI}SATTAS(SAT-basedTypeAnalysisSystem)是我们采用Java语言开发的基于SAT求解的Java程序类型分析原型系统。该系统的设计目标是能够对任意的Java程序进行过程内或过程间的流敏感以及属性敏感的分析,获得每个变量的类型集并构造出程序的调用图。由于时间和精力所限,我们只实现出了过程内分析的功能,并且要求输入的程序满足我们在2.2节提出的要求,输出的结果也只是以文本形式表示的变量的类型集,但是我们在系统设计时预留了相应的功能和数据接口,今后能够方便的对本系统进行完善和进一步的扩充。2.7.1系统框架’如图2.30所示,SATTAS系统主要由词法语法分析模块、SSA扩展形式转换模块以及程序抽象模块组成。其中,词法语法分析模块调用eclipseJDT(JavaDevelopmentTools)[113,114】提供的的API对Java源程,<~~’?、?7:~‘;,.,’i一。::。、j一源代码uJ\狒弋’荔、N一∥/,,’巴,,一∈];厂、‘-二)I:\、一一/程序ASTI?方法SSA扩程序抽象库、一—/,■■-一—_一、,~~,,-一.-●,,展形式库、、、~.一一一,,,词法语法分新糙操\/图2.30SATTAS总体框架36 东南大学博士学位论文序进行词法和语法分析,生成程序的抽象语法树AST。SSA扩展形式转换模块利用程序AST构造每个方法的SSA扩展形式,生成以对象方式表示的方法SSA扩展形式库。程序抽象模块则基于SSA扩展形式库中的信息进行方法的抽象并求取方法概要,生成同样以对象方式表示的程序抽象库,然后根据分析策略(目前仅实现了过程内的分析策略)联结方法概要的公式构成程序的公式,将程序公式转换成DIMACS格式后利用SAT求解器zChaff【92]求解。将求解结果解码,并与方法概要中的变量常值信息进行综合后,即可获得最终的分析结果。我们将上述三个模块实现为三个Java包(package),由于词法语法分析模块调用第三方的API进行词法、语法分析,因此我们重点介绍SSA扩展形式转换模块和程序抽象模块。sattas.sM::S∞ne-methodsMap+addMethod(innait)oSmng.inmethod:ConuolRowGral^)+contmnsMeihod(mnan"le:Smng)booleansattas.ssa::GraphNode+gelMethod(mna/Td!Smng)ControlFIowOrelda-blockBaslcBlock+remo’eMethod(mnero:Smng)-chddrenListl.p"ⅢGraphNode-prevNod8List∞ttas.ssa::ControlPlo“;r@h-stlc.cNod∞List,nodes:M印+addChlld“nc:GraphNede)enid"NodeGrat-aNoae+adflPrevNedeOnnGra曲Noae)-exllNode.GnphNede+addSuceNodelinnGraDIINode).dominalorTreeRcotGraphNode+getBIocL()BaslcBlock+bmldCFGFromMelhod(irtmethod:or8.edipse.jdt.core.domMethodDedanUim)+getChddren0:LISt+bmldDomTreeO。咤elParcmOGr@hNode+binIdExlSSAO+BeIPrevNodesOLm+calculateDF(mn:Gr@hNode’:tim+getSuccNed嚣(JList+getDomTreeRootOGraphNode+setBlod,(inbBasxBloek)+gelEntD"NodeOGr@hNodo+setParem(inPGfa时lNode)+getExttNodeOG删幽Nodesatl85.s轴::【IlIslelllocksatt醑.ssa::StatelentPaIr-sJlenlenlpmrsLIsl-jdlStalemeittorgechpsejdlcoredomStatement+addStaiementPmrAt(insp:Stalem∞lPait,inindex:inl"-始aSbalemeqllSSASlalemenl+gelSlatemenlPalrs()List1-geOdlStalemenlOorgechpsejdtcor‘dontStalement+getstatementPmrAl(inindex:int):S“llemmtPair+getSsoSlatement0:SSAStatement+removeStalemeI"ttPmrAt(inindexinl)+seudtstalemcnt(1It3orgeclipse)drcoleaom.$U帅arent)+se6saSiatemelltfiItsSSAStatement)satta.s.SSfl::SSAInnorAnchorgarkStatment<<接n>)sattfir.s舳::SSAOuter^nchorMarkStatment4hsName痧船tlas.s期::SSAStateawnt≈-IhsNamc,dent=.wSiring’l$S,YdlnnerAm:horMarlaqta/ementO:boo/canI一_·rhsName+geddeitutyOSmug+ts.S:(,"AOuterAnchorMarl_S"tatememO,b∞lean懈Lh“)Nm*+IgiSAl’htStatementOboolean+geildemiiyOStfin8十lsl姗竹^ndmndaASl脚ana’l()bool翻n+is,t,:"CAValAsstgnS/atementOboolean——+geiRhsONane竹sOuterAnchorMarkStalemeitK):boolean+lsS:;^Var^’sI"Ro|emcntoboolean+isSSAh-merAnc出orMarkSla/emml0:bodean+lsSSAPhiStalemeitt(1booleanZ∑2\Z∑+lsSSAOuterAnchorMa;kStaiemenl0:bool硼+lsSSAPhiStatemenl(Jboolean+isSSAValAsslgnStalemeni{)boolean+IsSSAValASslgnSlale㈣t()boolean+,sSSAVarAssl肼Stalernent():boolean+IsSSAVarAsslglStalmenl(1:boolⅫ,t-Jelldelllll).(n"lIdSmng)+sei|dentlly(midSmn8)+setLhs(mbName)+selRhs(mbName)sRttas.Bsa::sskValAssIgnStatc囊entSlitt聃.s8R::SSAPhiStatcuentsatiRs.sgH::SSAVar^ssJgnStateacotJhsName·Ihs:Nam-IhsNam.disValue·rhsLISt-rhsNarne+geIL嚼JName+geiLhs(JName+gelLhsOName+0dRh“)Value+geiRhsOList+EeiRhsONa哪+tsSSAlnnerAnchorMarkSlalemmt().boolean+lsSSAInnerAnchorMarkStatemellt0boolean+lsSSAlnnerAnchorMarkSlatement0:boole曩l+lssSAOuIerAnchorMarLS垭cm∞“)boolean+isSSAOuterAnchorMarkSlatement():bodeaa+IsSSAOulerAncho;MarkStatement():boolean+lasSAPhlStalementl)boolean+IsSSAPhiSialementOboolean+lassAPhiStatememOboolean+IdSAValAss,gnStatemenIO:boolean+lsSSAValAsslgnSlalemenIOboolean+IsSSAValASslgnStalemenl0boolean+IssSAVarA骆ignstaI蛐I酬()boolean+JssSAVa,As自删SIaI肼舶螂:bool翻n+lsSSAVatAsslgitSlalem脚10:bool枷+setLhs(mbName)+selLhs(JnbName)+sellhs(inbName’+selP.hs(mbVaJueltselRhs(mbV=due)+s“RhsonbName)LfIfsatt8s.s鞠::‘~altfIedtueme<(接门>>。Htt“8,S躲::;..NmreII-narrmSimpleNamesattas.ssB::Value+tsTypeOboo/can+getFully(.)ua/dledNameOStringN-quahfierNameZ∑+#sOuahl?edNome(Jboolean+ts菏mpleNameO&^olean+getFull)QuahliedNilme():String+getName()SlmpleName△+gelQuahfierOName+isQuahfledName()booleansatta墨s5B::TypeSattasls船j:Si|pJeKale+tasimPJeNnme0bool啪-idStung·idSinng竹eINanleflnnameSimpleNarue)+geiVaheOStnnS+geiFull)Qua]lfiedNameO:String+tetOuehfiev(mauaIln盯Nanvel+ISType(’boolean+gelNameOSiring+selValue(invalueString)+lsOualtfiedName0boolean+isSimpleName()boolean+setName(iitnmStnn曲图2.3l形式转换模块类结构图37 东南大学博士学位论文2.7.2SSA扩展形式转换模块SSA扩展形式转换模块的静态类结构如图2.31所示。其中,ControlFlowGmph是该模块的核心类,我们用它的实例表示转换前后的Java方法。ControlFlowGmph中的节点表示Java方法的基本块(BasicBlock),基本块由顺序语句对(StatementPair)组成,而一个StatementPair实例则包含了一条AST中的语句和一条SSA扩展形式语句。我们将SSAStatement实现为接口,并具体定义了五种SSA扩展形式语句,其中的SSAValAssignStatement、SSAVarAssignStatement以及SSAPhiStatement分别对应图2.7中的三类语句,SSAlnnerAnchorMarkStatement和SSAOuterAnchorMarkStatement则分别是入口锚点标识语句以及出口锚点标识语句。我们将SSA扩展形式库实现为一个单件类Scene的实例,所有的方法记录在该实例的methods属性中。‘SSA扩展形式转换的大致流程如下:首先我们创建一个Scene的实例,然后针对前一阶段生成的每个方法的AST,创建ControlFlowGraph的实例,调用实例的buildCFGFromMethodO方法构造控制流图,构造时我们直接在StatementPair实例的idtStatement属性中记录AST中的语句,然后再调用ControiFlowGraph实例的buildExtSSA0方法构造SSA扩展形式,该方法是对算法2.9的实现,构造填充StatementPair实例的ssaStatement属性,并插入新的语句对。2.7.3程序抽象模块程序抽象模块的静态类结构如图2.32所示。我们将方法抽象以及经过部分求解后获得的方法概要封装为MethodAbstraction的实例。该实例包含三个属性,属性anchors记录了方法锚点,属性constants记录了变量的常值,属性formula则记录了方法的公式。接口Formula派生出了四个类,其中Factor的实例表示单个的布尔变量。为了能够方便的得到以DIMACS格式表示的公式,在Factor实例中,我们用长整型数来命名布尔变量,变量及属性名与布尔向量间的映射关系则记录在Scene实例的num2var属性中。所有方法抽象也记录在Scene实例的methods属性中,该实例即是程序抽象库。我们通过创建Intraprocedural的实例进行过程内分析,属性program记录了补充了入口锚点初始值之后的方法公式,我们将此类公式封装为SolvableAbstraction的实例,可以通过调用实例的solveO方法进行公式的求解。程序抽象的大致流程为:我们首先创建一个Scene的实例,然后针对每个SSA扩展形式库中的方法(即图2.33程序抽象库类结构图38 东南大学博士学位论文ControlFIowGraph实例)创建一个MethodAbstraction的实例,调用该实例的parse0方法进行方法的抽象,parse0方法通过2.4.4节介绍的步骤首先抽象出文本形式的方法公式,然后再将变量和属性名编码,生成Fomula的实例。在抽象过程中,我们利用JGraph[]提供的API对公式进行循环验证。获得方法原始抽象之后,我们再调用MethodAbstraction实例的panialEvaluate0求解方法概要。最后,我们创建Intraprocedural的实例并通过调用buildProgramAbstractionO方法从程序抽象库中(即Scene实例)构造出可直接求解的公式,然后调用solveO方法求解。2.7.4公式的求解我们使用zChafd921求解SAT公式,该求解器接受DIMACS格式的输入,其中命题逻辑公式以CNF的形式表示,而从程序中抽象出的公式并非CNF形式,这就涉及到命题逻辑公式由一般形式到CNF形式的转换。我们使用第三方工具sat2cntil”1来做形式转换。该工具接受SAT格式的输入,输出DIMACS格式【1161。SAT格式中命题逻辑公式的表示更接近一般形式,例如,公式(x,vx3v-1xO^(x4)^(x2V_1X3)的SAT格式为cSampleSATformatCPsat4(幸(+(13-4)+(4)+(2—3)))SAT格式的公式可通过调用SolvableAbstraction实例或MethodAbstraction实例的writelnSATformat0方法获得。缺省情况下,zChaff在求出公式的一个可满足解后即终止。为了求出所有的可满足解,我们修改zChaff源代码中的sat_solver.cpp文件:首先我们添加my_handleresultOi函数如下voidmy_handle_result(SAT--Managermng){intvarNum=num—indep_var;int宰newClause=newint[varNum];for(inti=1;i<_varNum;i++){intassign=SAT-鼻etVarAsgnment(mng,i);if(assign一0)newClause[i-1】=2宰i;elsenewClause[i一1】=2幸i+l;)SAT-』ddClause(mng,newClause,varNum);SA£Reset(mng);}该函数的功能是将当前求得的可满足解取反后交上原命题逻辑公式,并重置求解器。然后我们在main()i函数中每求出一个可满足解时就调用一下my_handle_result0,然后再次求解直至没有可满足解为止,即intmain(intargo,char··argv){while(1){intresult=SATSolve(rang);if(result:==SATISFIABLE){verify_solution(mng);my_handle_result(mng);continue;}else{break;)}求解后,我们依据sa“as.109ic.Scene实例中记录的映射关系解码,并将求解结果与方法概要中记录的变量常值进行综合,得到最终的分析结果。39 东南大学博士学位论文2.8本章小结本章我们提出了基于SAT求解的Java程序类型分析方法,相比较其它方法,我们方法的优势主要有:·该方法是流敏感的,但无需在控制流图上进行迭代。·该方法是属性敏感的,能够区分不同变量的同名属性。·该方法既可以进行上下文不敏感的分析,也可以进行上下文敏感的分析。·该方法求解公式时利用了SAT求解器包含的多种高效的启发式搜索技术,有利于加快类型的推导。·该方法利用了SAT问题应用在空间复杂度方面的优势,能够有效降低精确分析带来的高复杂度。我们还考虑过另一种程序抽象模型,即状态转移系统。状态转移系统可定义为一个三元组锱球,sO>,其中,S是程序状态集,程序状态是由程序中所有变量及属性组成的向量;R是状态转移规则集,状态转移规则规定了程序状态的变化方式,对象创建语句、类型转换语句以及赋值语句等等都对应一条状态转移规则;s0是程序初始状态,由程序入口处变量的类型决定。例如,建模成状态转移系统后,语句“6=c;”被抽象成“&l(6声跗c)”,其中S表示程序第f个状态,“文c)”表示S状态时变量C的值。相比较基于SSA扩展形式的抽象方法,状态转移系统模型存在以下缺点:1)程序状态包含程序中的所有变量,这将大大增加程序公式的规模;2)如果要做流敏感的分析,则需要按照程序的控制流逐条抽象语句,且对结构的抽象存在‘V’、‘‘人,’相互嵌套,增加了转换成CNF形式的复杂度;3)对循环结构需要迭代分析。 东南大学博士学位论文第三章基于SAT求解的Java程序指向分析Java程序指向分析研究程序中引用类型变量和属性指向的堆对象集,这些堆对象是虚拟的抽象空间,并非程序运行时创建的对象实例。指向分析研究的一个重要意义在于从变量指向集信息中可以推导出变量间的别名关系【117,118】,从而有助于提高大多数程序分析的精度。人们在指向分析方面做了大量的研究工作,提出了不少分析方法p玉川J。文献[32.36】的方法是基于数据流方程的流敏感方法。这类方法的基本思想是首先将语句抽象成一个描述流入该语句前变量指向集与流出该语句后变量指向集间关系的方程,然后从程序的入口方法开始按照控制流的顺序逐条求解语句的方程。这类方法精度较高,但时间和空间复杂度也很高,因而只适用于小规模的程序。文献[37.401的方法是基于合一的流不敏感方法。这类方法的中心思想是认为赋值符号两边变量的指向集是相同的,因此分析时能够通过合并变量指向集加快推导速度并减少存储空间。这类方法时间和空间复杂度相对都较低,能够适用于大规模的程序,但分析结果非常粗糙,无法满足人们的需求。文献[41.55]的方法是基于包含的流不敏感方法。这类方法的中心思想是认为赋值符号左边变量的指向集包含右边变量的指向集,因此这类方法的精度要优于基于合~的方法,但要劣于基于数据流方程的流敏感方法。另外,该类方法的复杂度也介于前两类方法之间,成为人们研究的重点。AndersonLO最先提出基于包含的分析方法f4ll,他将相关语句抽象为一个个的约束,约束描述了变量间指向集的包含关系,这样由整个程序就获得了一个约束系统,通过求解该约束系统就能得到源程序的一个合理分析结果。FaehndrichM利用约束图进行分析,约束图是一个有向图,图中节点表示变量,节点上附加了变量的指向集,有向边表示变量间指向集的包含关系,原问题则转换为计算约束图的动态传递闭包【4引。文献[43,44】将FaehndrichM的方法推广到上下文敏感的分析。文献[45—49]贝JJ针对动态传递闭包的计算提出了一些改进的算法。SridharanM将指向分析转换为有向图的上下文无关语言可达性问题,图中节点表示变量和抽象空间,有向边表示指向关系或包含关系,边上附加了语言中的文字反映了该边的具体含义【5⋯。为了进一步降低方法的空间复杂度,BemdlM利用二元决策表BDD来表示包含关系与指向信息,将指向集的推导转换为BDD上的操作【5I"52l,WhaleyJ则将BemdlM的方法推广到上下文敏感的分析中p4。。另外,ZhuJ也独立的提出了基于BDD的符号指向分析方法155-57J。他们方法都是利用BDD对布尔函数真值表的压缩表示能力减少变量指向集表示需要的存储空间。虽然BDD能在一定程度上降低空间复杂度,但当需要表示的变量很多时,BDD需要的内存空间仍然会变得很大【5引。基于包含的分析方法虽然流行,但它终究是个流不敏感的方法,在分析精度上始终不如流敏感的方法。而基于数据流方程的流敏感分析方法存在空间复杂度过高的问题,对较大规模程序进行上下文敏感分析时会因内存耗尽而终止。我们认为,这和传统方法的分析策略有关。传统流敏感分析方法需针对不同的程序点存储变量的指向集,并根据语句的数据流方程对这些指向集进行操作,因此当变量很多时需要的存储空间就会很大,特别是进行上下文敏感分析时,在不同的上下文上需要对同一个方法进行重复分析,而上下文的个数随着程序规模的变大增长很快,因而所需鲍存储空间会加速膨胀。本章我们介绍基于SAT求解的Java程序指向分析方法。不同于传统方法,我们的方法并不直接存储变量的指向集,而是存储程序抽象出的命题公式,然后利用求解器对命题公式进行求解,相当于从程序中推导出变量的指向集。后续章节安排如下:3.1节介绍基于SAT求解的Java程序指向分析方法的基本思想、分析流程,并详细讨论与第三章类型分析方法的差异;3.2节是实例研究,我们对一程序实例分别做上下文不敏感和上下文敏感的分析13.3节讨论类型分析与指向分析的综合;3.4节是本章小结。3.1分析方法本节我们首先介绍方法的基本思想,然后介绍方法的主要分析流程,最后详细讨论与第三章类型分析方法的差异。41 东南大学博士学位论文3.1.1基本思想对于Java程序而言,流敏感的类型分析与流敏感的指向分析之间存在相似性:前者研究类型在变量或属性间的传播,而后者研究抽象堆对象在变量或属性间的传播。因此,如果改变布尔向量代表的意义,那么基于SAT求解的Java程序类型分析方法的基本思想也同样适用于Java程序指向分析,即将程序中的变量编码成布尔向量,其取值表示该变量指向的抽象对象,用逻辑等价关系抽象变量间指向对象的传递,通过逻辑与(“A”)和逻辑或(“v”)将程序联结成一个命题公式,最后将其转换成CNF形式,利用SAT求解器求出所有可满足解。1V=new00;2W=new00;3v.f=w;4V=nc,w00;5v.f=new00;(a)图3.1程序示例vl=0-I;Wl=Oa;v1.fl=wl;v2=O“:v2.fl=015;(b)例如,如图3.1(a)所示的程序片段,我们首先将它转换成图3.1(b)所示的SSA扩展形式。在该形式中,具体的值不是类型而是抽象对象,我们用相应对象创建语句的行号命名抽象对象。然后,我们从该形式中抽象出公式(Vl=Osl)^(Wl-=-Os2)A(V1.fi<"">WI)A(v2=Os4)A(V2.fl=035)求解可得p捃(V1)={o。I),pts(w1)2{Os2,,pts(v1.f1)={O。2),pts(v2)={o“),pts(v2.fi)2{O。5)由p船(V1)与pts(v1.fi)可得pts(O。1.f1)={O。2)由p括(v2)与pts(v2.fi)可得pts(Os4.f1)={O。5}3.1.2分析流程指向分析是一个反复求解、逐步求精的过程:我们首先确定分析的上下文敏感性并构造初始调用图,其次将所有方法都转换成SSA扩展形式,然后对方法进行抽象并求解方法概要,接着根据初始调用图将方法概要公式联结为程序公式并由SAT求解器求解,根据求解结果推导出变量的别名关系,并以此改进方法现有的SSA扩展形式,然后再次进行方法抽象、公式联结、公式求解、形式改进等等,直至方法的SSA扩展形式不再改变为止。指向分析的具体流程如图3.2所示。3.1.3与类型分析方法的差异在具体的分析过程中,指向分析方法与类型分析方法在值的命名以及抽象精化等两方面存在差异。对于其它方面,我们可以直接将类型分析中的处理方法用于指向分析。1)值的命名类型分析研究的是类型,类型只需以类型名来命名,类型的命名不受上下文敏感性的影响,也就是说,不同上下文下类型名相同的两个类型是同一个类型。指向分析研究的是抽象对象,但抽象对象不能仅仅以对象创建语句的行号来命名(假设程序所有语句统一编号),因为命名还受到上下文敏感性的影响,在不同上下文下,同一条语句创建出的是不同的抽象对象。因此,指向分析需首先确定分析策略,然后再命名抽象对象。42 东南大学博士学位论文图3.2基于SAT求解的Java程序指向分析流程具体的,我们首先构造程序的上下文不敏感调用图,若进行的是以有限长度调用路径为上下文的上下文敏感分析,则通过2.6.3节介绍的方法由上下文不敏感调用图获取相应的上下文敏感调用图。调用图上,每个节点都代表了不同的方法(或同一个方法的不同副本),每个方法(或方法副本)中不同语句创建的对象都是不同的抽象对象,我们对这些抽象对象进行统一的命名(可通过上下文加行号的方式)。然后我们将方法转换成SSA扩展形式,这只需对算法2.9做以下少许的改动即可:1)将算法中的值由类型替换成统一命名的抽象对象:2)将源程序中的强制类型转换语句转换成赋值语句,而非取值语句。(1)V=U;(2)vI=v2;(3)Vm3o(vi,...,U,⋯,vk);图3.3被抽象的三类语句指向分析需要抽象的语句同样是取值语句、赋值语句以及D函数语句等三类(如图3.3所示),只是语句中值U的含义不同。我们把变量和属性也都抽象成唯一的布尔向量,布尔向量的取值代表了相应变量的指向,其长度由抽象对象的个数决定,因而2.3.2节的抽象规则2.4、2.5、2.6仍然适用。我们逐一抽象调用图上节点代表的方法,方法抽象及求解方法概要的过程也与类型分析一致。需要说明的是,由于上下文敏感调用图上多个节点可能代表了同一个方法的多个副本,这些方法副本的SSA扩展形式的区别仅仅是创建的抽象对象不同以及变量或属性不同,因而没有必要对每个方法副本都进行抽象及求解方法概要,只需对此类方法抽象一次,求出方法概要后,针对不同的方法副本,拷贝一份方法概要并稍作修改即可。43 东南大学博士学位论文2)抽象精化类型分析时,由于无法预知别名信息,在对象属性的表示上我们只能采取保守的策略,从而降低了方法公式的精度。指向分析时,我们可以从当前的分析结果中获得别名信息,然后利用该信息优化现有方法的SSA扩展形式,再次抽象得到更加精确的方法公式,求解该公式就能获得更好的分析结果。方法SSA扩展形式的优化对象是因对象属性的表示而添加的a函数语句。由2.4.1节的介绍可知,因无法预知变量间的别名关系,为确保分析的安全性,需针对对象属性的引用在不同变量的同名属性定义点后添加a函数语句。例如,图3.4(a)是一程序片段,图3.4(b)是其SSA扩展形式。该形式中,语句6引用了变量v的属性f,由于不确定v和W的别名关系,因此在语句4变量W的属性f的定义点后添加了。函数语句,以确保语句6处变量S的值包含os2和O“。在获知v和W的指向集后,该。函数语句是可以被优化的:1)若V和W的指向集不存在交集,则它们不是别名,语句4对W属性f的定义不会影响到变量v,因此可以直接将a函数语句删除(如图3.4(d)所示),此时变量S的指向集为{os2}:2)若V和W都唯一指向相同的对象,则它们是确定别名(mustalias),语句4对W属性f的定义一定会影响到变量v,因此可以将a函数语句修改为赋值语句(如图3.4(c)的语句5所示),此时变量S的指向集为{Os4};3)若v和W指向多个对象且指向集的交集不为空,则它们是可能别名(mayalias),语句4对W属性f的定义可能会影响到变量V,此时D函数语句不能被优化。V2⋯:v.f=aewTl();W2⋯:w.f=newT2();S=v.£V14⋯;VI.ft=012;w12⋯;WI.fl=O“;V1.£=o(v1.fl,WI.f1);3l。V1.£;V12⋯;V1.fl=0吐;W12⋯;WI.fl=0s4;VI.I"2=W卜fi;8I=V1.最;V12⋯;VI.fl=Oa;W12⋯:WI.£=O“;Sl=VI.fl;(a)(b)(c)(d)图3.4SSA扩展形式优化示例基于上述分析,我们给出对象属性D函数语句优化规则如下述规则3.1所述。规则3.1(对象属性D函数语句优化规则):对于形如“Vi.f=o(u,wj.f);”的语句,其中U可以是Vi.f或null,令vi的指向集为pts(vi),wj的指向集为pts(wi),“lI’,表示集合元素的个数,则优化规则为(1)若pts(vi)np缸(Wi)一lzI,则删除该语句;(2)若Ipts(vi)l>1,pts(wj)l>1,且pts(vONpts(wj)≠O,则不改变该语句;(3)若∞妇(vi)l—p括(Wj)I—ltRpts(vO==pts(wj),则将该语句替换为形如“Vi.f=wj.f”的语句;指向分析过程是一种白顶向下、逐步求精的过程:分析初始,第一次将方法转换成SSA扩展形式时,我们对别名关系采取同类型分析一样的保守估计,抽象出的方法公式较为粗糙;随着分析的深入,方法SSA扩展形式的逐步优化,方法公式也越来越精确,求解的结果也越米越准确;如此反复分析直至达到不动点,我们就可以获得精确的指向分析结果。publicclassA{⋯’publicclassB{publicA£)publicclassC(publicvoidml(){BV2newB0;AW2m3Cv,v);}publicvoidha0(Bs2newB0;Bt。newB0;}AU2m3(s,t);}publicAm3(BP,Bq){p.f2newA0;q.f2rlfWA0;returnp.t}publicstaticvoidmain(){Ca2newC0;&ml();丑m2();}图3.5指向分析程序实例44 东南大学博士学位论文3.2实例研究图3.5是一程序实例,该程序包含A、B、C三个类,B类声明了类型为A的属性CC类包含ml、m2、m3和main等四个方法,我们对该程序实例分别进行上下文不敏感和上下文敏感的指向分析。3.2.1上下文不敏感分析图3.6程序实例的上下文不敏感调用图图3.6是程序实例的上下文不敏感调用图,根据它我们利用源程序中对象创建语句的行号给抽象对象命名(我们对源程序语句统一编号),方法ml、m2、m3和main的SSA扩展形式以及方法概要(我们略过方法抽象直接给出方法概要)如图3.7、3.8、3.9、3.10所示。经过简化后,ml、m2和main的方法概要公式为空。91011)publicvoidm10(thisl20();//in_paraOvl=0ss;v1.fl=null;out_cp9_ar90=thisI;out_cp9_argl=vl;out_cp9_argI.f=v1.fi;out_cp9_ar92=vl;out_cp9_ar92.f=VI,fi;m联怫WI200;flin_cp9_retV1.最200;//in_cp9_ar91.fV1.毛200;Ilin_cp9_ar92.f方法公式O方法锚点表(in,para0,thisj),(in,ep9__ret,w1)(in,cp9_argi.eVI.fi),(in,cp9_ar92.eV1.f3)(out,cp9._ar90,thist),(out,cp9_argI,v0(out,cp9_ar91.eV1.fi),(out,cp9_ar92,V1)(out,cp9_ar92.eVI.fi)变量常值列表(Vl,O蝠),(VI.f1,null)(a)(b)图3.7方法ml的SSA扩展形式及方法概要1publicstaticvoidmain(){2al=O吐2;3out_cp23_ar90=al;击m《*4out_cp24_argO2a1;艄拂)(a)方法公式O方法锚点表(out,cp23_ar90,aO,(out,ep24_ar90,a1)变量常值表(a1,0122)(b)图3.10方法main的SSA扩展形式及方法概要45 东南大学博士学位论文publicvoidm20{thisl=0();//in_para0sl=Otl2;SI.£=null;tl=oIt3;tt.£=null;out_cp14_re"gO==thisl;out_cpi4__ar912sl;out_cpl4_ar91.f2S1.6;out_cpl4_ar922tl;ouLcpl4_ar92.f2t1.fi;带哭鞋*u1=0();//in_cpl4retS1.垃=00;//incpl4_arg!.ft1.如=Ⅸ);Ilincpl4_ar92.f(a)方法公式O方法锚点表(in,para0,thisD,(in,cpl4_ret,u0(in,cpl4_ar91.£S1.fi),(in,cpl4ar92.et1.fi)(out,cpl4_argO,thisD,(out,cpl4_argl,s3(out,cpl4_ar91.eSI.fi),(out,epl4_ar92,t1)(out,cpl4_ar92.et1.fi)变量常值表(3l,0312),(S1.fl,null)(tl,O。13),(tI.fl,null)(b)图3.8方法m2的SSA扩展形式及方法概要publicAm3(BP,Bq){thisl200;//in_argOpl=00;//in_argIP1.fl=“);//in_ar91.fq1=烈);//in_ar92q卜fI=0();//in_ar92.f“岛=0117;q1.乞=o(q1.£,P1.£);qI.6=olis;p卜6=烈p1.毛qI.6);outret2P1.fi;out_ar91.f2P1.fi;out_ar92.f2qI.fi;(a)方法公式(q1.6付qI.f1)锚点列表(in,argO,thisl),(in,argI,p1)(in,ar91.eP1.fi),(in,ar92,q1)(in,ar92.£q1.fi),(out,ret,P1.6)(out,ar91.£PI.6),(out,ar92.£qI.6)常量列表(P1.坛O。17),(qm.如,0$17)(q1.6,O。is),(p卜£,0517)(p1.£,Oll8)(b)图3.9方法m3的SSA扩展形式及方法概要根据上下文不敏感调用图,按照2.6.1节介绍的联结规则,由方法概要公式联结成的程序公式为(我们通过在变量前添加方法名前缀来区分不同方法的变量):Formula(program)::=Formula(C.main)AFormula(C.main--->C.m1)AFormula(C.main---}C.m2)AFormula(C.m1)/O"ormula(C.m2)A(Formula(C.ml—"C.m3)vFormula(C.m2—÷C.m3)AFormula(C.m3)AFormula(C.m3---}C.m1)AFormula(C.m3—÷C.m2)A(Formula(C.m1一C.main)vFormula(C.m2---}C.main))。(ml_thisl<->main_a1)A(m2thisl<-->main_a1)A((m3_thisl付ml_thisDv(m3thislHm2jhisl))^((m3_pi<--}m1_v1)v(m3_pl<-->m2_s1))A((m3_.pm.flHml—v1.fov(m3_p1.f1”m2_sI.f1))^((m3ql+-}ml_vDv(m3_qi,,-->m2__ti))A((m3_q1.fi<--争mlvi.fi)v(m3_q1.毛付m2-tI.fI))A(m3q!.f2÷->m3_q].f1)^(ml-wlHm3-p卜f3)A(mlvl.f2《->m3_p1.f3)A(mlvl.6付m3-q1.f3)^(m2_ulHm3-pI.f3)^(m2s,.丘”m3_p卜f3)A(m2_t1.丘Hm3_q卜f3)2(ml__thisl20。22)^(m2_thisl=O,22)((m3_thisl七÷mljhisl)V(m3jhisl七÷m2jhiss))^((m3一p120s8)v(m3_pI=osl2))A((m3__p1.fi=null)v(m3__p1.fi=null))46,23456789mn屹BM,●23456789m¨坦B} 东南大学博士学位论文人((mtql=os3)V(m3』120s13)_)人((m3_q卜fi--null)v(m3一q1.fi--null))^(m3_q1.f2*->m3_qi.fi)^((ml_wt=Osl7)V(ml_wl=O。18))^((m1-y1.6=0s17)v(mlJ卜fr=O,18))A(m1.V1.f3=Osls)A((m2_ul=OslT)v(m2_ul=Osl8))^((m2._s1.丘=Osl7)v(m2_s1.最20s18))A(m2h.fj20s18)对该公式求解并与方法概要中记录的变量常值信息综合可得分析结果如表3.1所示(其中“@”前是行号):表3.1分析结果源程序中变量SSA扩展形式中变量指向集.8@vml_vl{O娼)9@wml——Wl{q17,0.8)12@sm2一sI{0。12}13@‘m2_tl{0。13}14@um2_ul{O。17,0s18)16@pm3__pl{0h,Osl2)16@qm3_ql{O蛆,osl3)17@p.fnd_p1.如{O。17}18@q.fm3_q1.6{0。18}19@retm3__p1.f3{0317,Osl8}22@arealn--ai{0,22)根据分析结果精化公式,考虑图3.9方法m3中对象属性。函数语句8和lO的优化:由T-Ipts(p1)I一扫如(q1)f一2,Jipts(p1)npts(q1)一(O。8}存在交集,因此语句不被优化,方法公式不发生改变,分析终止。3.2.2上下文敏感分析图3.1l程序实例的上下文敏感调用图我们以长度为l的调用路径为上下文,相应的程序实例上下文敏感调用图如图3.11所示,图中方法m3有两个副本(设为m3和m3’)。为了方便起见,我们通过添加⋯”米区别方法m3’中的变量和抽象对象。根据调用图,方法ml、m2、m3以及main的SSA扩展形式及方法概要仍然如图3.7、3.8、3.9、3.10所示,方法m3’的SSA扩展形式及方法概要与方法m3的区别仅仅是命名不同,因此,我们就不再重复给出了。根据上下文敏感调用图,按照2.6.1节介绍的联结规则,由方法概要公式联结成的程序公式为(我们通过在变量前添加方法名前缀来区分不同方法的变量):Formula(program)::=Formula(C.main)AFormula(C.main-,C.m1)AFormula(C.main->C.mE)AFormula(C.m1)^Formula(C.m1—争C.m3)AForrnula(C.m3)AFormula(C.m3—争C.m1)AFormula(C.m2)AFormula(C.m2--,C.m3’)AFormula(C.m3’)mFormula(C.m3’专C.m2)^(Formula(C.ml—C.main)vFormula(C.m2--}C.main))2(m1—曲islHmain-a1)^(m2jhislx,--,main._a1)A(m3._thislHmljhisl)^(m3’_thislom2_thisi)A(m3__pl<--}ml_vi)A(m3’_pl《--)m2_S1)A(m3_p1.fl针m1-V1.f1)A(m3’-p1.fl付m2-s1.fi)47 东南大学博士学位论文州帕_ql付ml_V1)人(m3’_qlHm2.j1)^(m3’-q1.fi<--->ml_v1.f1)A(m3’_q1.6÷÷m2_h.fi)A(1ldq1.最付m3_q1.f0A(m3’_q卜f2,c-》m3’_q1.fi)A(ml—wlHm3_p1.f3)A(ml_v1.最付m3J卜fi)A(ml_v1.6Hm3_qI.f3)A(m2._UFc--}m3’_P1.fi)A(m2..S1.fi<-->m3’_p1.f3)A(m2._t1.f2<->m3’_q1.6)=(mi_thisl=Os22)A(m2_thisl=os22)^(m3jhislHml』isl)^(m3’』isl付m2jhisO^(m3_..pi=Oss)A(m3’_pl=O。12)A(m3_p1.fi--null)A(m3’-p1.fi=null)A(m3_qr=Oss)A(m3’-q120s13)A(m3_qn.fr-null)A(m3’_q卜fr-null)A(m3q1.fi<--->m3_qi.f1)A(m3’-qI.f29m3’_q1.fi)A((mlWl=Osl7)v(ml_wl=Osl8))^((ml_v1.6=Osl7)v(m1._V1.fi=osis))A(ml__V1.620s18)A((m2_uI=O"si7)v(m2_ul=O"sIs))A((m2_s1.丘=O’。17)v(m2_s1.f2=O"sls))A(m2__t1.£20’sis)对该公式求解并与方法概要中记录的变量常值信息综合可得分析结果如表3.2所示(其中“@”前是行号)。表3.2分析结果源程序中变量SSA扩展形式中变量指向集8@vml_vl{O娼}9@wml_wl{Osl7,O,18}12@sm2_sl{Osl2}13@tm2_h{O。13}14@um2一Ul{o’。17’O"s18)16铆m3_pl{O螺l16@qm3_q1{O蛆)17@p.fm3p1.£{Osl7)18@q.fm3_q1.£(O,18}19@retm3_p1.f3{osl7,O。18}16@p’m3’-pl{O。12)16@q’m3’_ql{Osl3}17@p.f’m3’_p1.G{O"s17}18@q.f"m3’_q1.6{O’s18)19@ret’m3’_p1.£{0’s17,o’s18}22@amaln--ai{Oaa}根据分析结果精化公式:1)首先考虑方法m3中对象属性a函数语句8和10的优化。由于pa(p1)==pts(q1)一{o。8>,因此将原语句8修改为“q1.f2=p1.f2;”,原语句10修改为“Pi.f3=q1.fi;”,优化后方法m3的SSA扩展形式如图3.12所示。2)其次考虑方法m3’中对象属性。函数语句8和10的优化。由于pts(pf)Apts(ql")一O,因此将原语句8和语句10直接删除,优化后方法m3’的SSA扩展形式如图3.13所示。根据优化了的SSA扩展形式获得精化的程序公式为:Formula(program)::=Fonnu肠(C.main)AFormula(C.main-}C.m1),xFormula(C.main---}C.m2)AFormula(C.m1)AFormula(C.m1—争C.m3)AFormula(C.m3)AFormula(C.m3—÷C.m1)/,,Formula(C.m2)AFormula(C.m2—争C.m3’)AFormula(C.m3’)AFormula(C.m3’—"C.m2)A(Formula(C.ml—C.main)vFormula(C.m2-}C.main))=(ml_thisl<->mainal)A(m2._thislHmain--a1)^(m3_thisl.∈÷mljhisl)^(m3’jhisl‘÷m2-曲isl)^(髓oIHml-V1)^(m3’_pl付m2-SI)^(m3-p1.flHml_v卜fi)A(m3’_P1.flHm2_S卜fi)^(IIl3-ql付m1-V1)^(m3’-qlHm2j1)A(m3’_q1.fl付m1-V卜fi)A(m3’_q幽付m2_h.fi)“ml—wlHm3-p卜f3)A(mI._VI.£÷÷m3_p1.£)^(ml—V1.£付m3』1.fs) 东南大学博士学位论文1publicAm3(BP,Bq){2thisl=oO;f|试—簪曲3Pm2Ⅸ);//in_argl4P1.^=“);//in_ar91.f5ql=00;//in_ar926q1.fl=o();//in__ar92.f7p卜丘=Osl7;8qI.£=P1.B;9q1.6=Osl8;10Pt.B=q1.6;11out_ret=p1.6;12out_ar91.f=P1.6;13out_ar92.f=q1.£;>(a)方法公式0方法锚点表(in,argO,this0,(in,argl,p1)(in,ar91.CPt.ft),(氓ar92,q1)(in,ar92.eq卜f1),(out,ret,P1.£)(out,ar91.£p卜f3),(out,ar92.£q1.£)变量常值表(pI.6,0。17),(q1.丘,0s17)(q1.£,0118),(PJ.6,OslB)(b)图3.12优化后方法m3的SSA扩展形式及方法概要^(m2_ul<--}m3’-p卜f2)^(m2_s1.f2Hm3’_P1.f2)A(m2,t!.f2,e--}m3’』1.疋)=(mljhisl=os22)^(m2』isl=0322)^(m3jhisIHmljhiSl)^(m3’_thisr<-}m2_thisD^(m3_pl=Oss)A(m3’_pl=O。12)A(m3...p1.fi--null)^(m3’_p1.f12null)A(m3_ql=Oss)A(m3’_ql=O。13)A(m3_q1.fi--null)^(m3’-q卜fi=null)^(ml_wl=Osl8)^(m1J1.f2_0sls)^(ml_.v1.f320sis)A(m2_Ul=O"s17)^(m2_s1.f2=o"s17)A(m2._t1.f≯O’。18)对该公式求解并与方法概要中记录的变量常值信息综合可得分析结果如表3.3所示(其中“@”前是行号)。表3.3分析结果源程序中变量SSA扩展形式中变量指向集8@vml_Vl{O。8}9@wml—Wl{Osl8)J2@sm2_sl{O。12)13@tm2_hf0,13}14@um2一ul{O’s17}16@pm3__pl{Ossl16@qm3一ql{0娼)17@p.fm3-p卜如{O,17)18@q.fm3_q,.6{O。18}19@retm3_p1.6{0。18}i6@p’m3’.pl{Osz2}16@q’m3’-qI{0。13)17@p.f’m3’-p1.如{0’s17)18@q.f’m3’_q卜6{o’s;8}19@ret’m3’-p1.£{0’317}22@amaln_al{0s22)根据分析结果,方法公式无法继续精化,因此分析终止。分析结果表明上下文敏感的分析比上下文不敏感的分析更加精确。49 东南大学博士学位论文publicAm3(BP,Bq){thisl=双);//in_ar90Pl2o();//in_argIP1.fl=00;//in_argI.fql2以);//in_ar92qI.fl=双);#in_ar92.fp1.丘=O。17;q1.f2=0s18;out__ret2P1.允out_argI.f=P1.f2;out_ar92.f=q1.f2;方法锚点表(in,argo,this,),(in,argl,p0(in,ar91.£P1.f1),(in,ar92,q1)(in,嘴2.eq1.fI),(out,rot,P1.f2)(out,ar91.eP1.f2),(out,ar92.£q1.劬变量常值表(p1.B,Osl7),(q1.f2,o|18)(a)【I图3.13优化后方法m3’的SSA扩展形式及方法概要3.3类型分析与指向分析的综合指向分析结果也可以指导类型分析中方法公式的精化,从而迸一步提高调用图的构造精度,而调用图精度的提高反过来又能改善指向分析,因此,一种理想的分析方法是将类型分析和指向分析综合起来,这样就能够获得高精度的程序调用图和指向信息。类型分析与指向分析综合的分析流程如图3.14所示:首先进行过程内的类型分析构造出程序的初始调用图,基于它进行指向分析,然后利用分析结果精化类型分析的方法抽象,并基于已有的调用图进行过程间的类型分析构造出更精确的调用图,然后基于该调用图再次进行指向分析,如此分析直至分析结果不再改变为止。需要指出的是,指向分析本身包含反复迭代的过程,它基于每个调用图都分析到精度不再提高为止,但由于综合分析时程序的凋用图也在不断的精化,因此可以限定每次指向分析只迭代2到3次,这样能够加大综合分析的前进步伐,加快分析速度。‘3.4本章小结利用指向信息图3.14类型分析与指向分析综合的分析流程指向分析是Java程序分析中的一个基本问题,具有非常重要的研究意义。多年来,人们在指向分析上投入了大量的精力,展开了广泛而深入的研究。本章我们采取了不同于前人的研究思路,另辟蹊径,提出了基于SAT求解的Java程序指向分析方法,相比较他人的方法,我们方法的优势主要有:·该方法将SAT问题应用于指向分析,有利于大大缓解精确分析下的状态空间爆炸问题。·该方法是流敏感以及属性敏感的,因此精度比传统方法更高。·该方法既可以进行上下文不敏感的分析,也可以进行上下文敏感的分析。·该方法利用了SAT求解器包含的多种高效的启发式搜索技术,能够加快变量指向集的推导。50●23456789mn} 东南大学博士学位论文第四章AspectJ面向方面调用图及其构造程序调用图是一种描述函数(或方法)间调用关系的有向多图,图中节点表示函数(或方法)(通常用一元组<函数名(或方法名)>表示),有向边表示调用关系(通常用三元组<头节点,尾节点,调用行号>表示),节点间的有向边可以不止一条以表示不同程序点上的方法调用。程序调用图可按照上下文敏感性分为上下文不敏感调用图和上下文敏感调用图,其中,上下文不敏感调用图的显著特征是无论方法在哪种情况下被调用,图中都只用一个节点表示。例如,如图4.1所示的程序片段及其上下文不敏感调用图,虽然程序中C.main方法在语句8和语句l0处分别以B对象实例和c对象实例弧次调用了A.foobar方法,但在图中用同一个节点表示。ipublicclassA{2publicvoidfoobar0{⋯)3}4publicclassBextendsA{⋯>5publicclassCextendsA(6publicvoidmain(){7Aa=flahtB0;8a.foobar();9a=newc0;10a.foobar0;Ill12l(a)(b)图4.1程序实例及其上下文不敏感调用图调用图是一种关于程序的重要信息,大多数程序分析需要依靠调用图进行过程间的分析。由于上下文不敏感调用图的构造更为高效,因此程序分析时大都采用此类调用图。但是当用于AspectJ程序分析时,传统的上下文不敏感调用图主要存在以下两点不足:第一,此类调用图不能表示AspectJ定义的新事件。AspectJ定义了程序运行时的事件集,除了将传统意义上的方法调用细分为方法调用和方法执行两个事件以外,还引入了诸如对象属性读、对象属性写、对象初始化等新的程序执行事件,而传统调用图只能表示传统的方法调用(可以看作是AspectJ的方法执行),其它的程序执行事件都无法表示出来。第二,此类调用图只能表示:市点的静态类型,无法表示其动态类型。面向对象程序中的方法调用通过被调对象的类型动态绑定到具体的方法。我们称方法定义所在的类为该方法的静态类型,称方法执行时被调对象的类型为方法的动态类型。由于上下文不敏感的缘故,该类调用图只能表示出静态类型。例如,图4.1中“A.foobar”节点代表的方法的静态类型是A,而其在语句8处被调用时的动态类型为B,在语句10处被调用时的动态类型为C,这两种不同的动态类型都丢失了。为了弥补上述缺点,我们提出了一种改进的程序调用图——面向方面调用图ACG(Aspect-orientedCallGraph)。该调用图可以在上下文不敏感的方式下通过一种间接的方式保留节点的动态类型信息,从而既保证了构造的高效性又能够适应AsepctJ程序分析的需求。本章安排如下,4.1节介绍面向方面调用图;4.2节讨论上下文不敏感面向方面调用的构造;4.3节总结及介绍相关工作。4.1面向方面调用图面向方面调用图ACG是在传统调用图的基础上对节点的种类及其类型,以及边的种类进行了扩展。5l 东南大学博士学位论文4.1.1节点分类首先,我们扩充节点的种类,使得ACG能够表示AspectJ事件集中的大部分事件。逻辑上,AspectJ的连接点是程序流中一些特定的点,每个点代表了一种程序执行事件。物理上,连接点是程序中的某些特定代码段,这段代码完成了该连接点所表示的某个程序执行事件。方面可以横切到连接点的前面(before)、后面(after)或周围(around)。也就是说,方面代码可以插入到相应的代码段的前面或后面,或者完全取代原来的代码段。连接点是由语言设计者预先定义好的,程序员无法扩充。Aspectl的连接点模型共定义了11类连接点[131,即方法调用、方法执行、构造方法调用、构造方法执行、类静态初始化执行、对象前期初始化(objectpre.initialization)、对象后期初始化(objectinitialization)、属性读、‘属性写、异常处理执行、通知执行。表4.1列出了每个连接点对应的字节码段(通常称为该连接点的shadow)[231,从中我们能透彻的理解每个连接点的具体含义。表4.1连接点对应的字节码段连接点字节码段语句“invokeinterface”、“invokespecial”、方法调用“invokestatie”和“invokevirtual”方法执行方法的整个代码段构造方法调用语句“invokespecial”构造方法执行方法中super调用后的代码段类静态初始化执方法的整个代码段对象前}{耳初始化方法dd调用super前的代码段对象后期初始化对象的第一个构造方法代码段属性读语句“gctfieid”和“gctstatic”属性写语句“putfield”和“putstatie”异常处理执行相心的异常处理代码段通知执行编织后通知的整个代码段在这ll类连接点代表的程序执行事件中,由于异常处理执行事件和类静态初始化执行事件的发生时机是难以通过静态分析获悉的,因此我们不在ACG中表示这两类事件。另外,我们将对象前期初始化事件和对象后期初始化事件并入构造方法执行事件,因为从语义的角度分析,这三类事件代表了对象初始化过程的不同阶段。因此,需要在ACG上表示的程序执行事件共有7类,分别是:·方法调用事件;·方法执行事件;·构造方法调用事件;·构造方法执行事件;·属性读事件;·属性写事件;·通知执行事件;·我们扩展节点的结构,使之包含表示自身种类的字段||}。表4.2给出了7类事件对应的k值。今后如果要表示新的:i了点,则只需扩充k的取值范围即可。表4.2ACG上表示的事件及其相应的k值事件k值方法调用meall方法执行meXeC构造方法调用coall构造方法执行ccXeC属性渎绝et属性写fset通知执行aeXeC52 东南大学博士学位论文4.1.2节点类型其次,由于AspectJ的连接点具有上下文属性,主要包括程序执行到连接点时执行对象、目标对象、参数对象以及返回值等信息,这些信息可以被捕获。因此我们给节点赋予类型属性T=-,其中,%j。表示事件发生时执行对象的类型,Ct。州表示事件发生时目标对象的类型。表4.3给出了7类事件各自的C『崎,ct哪d的含义,从中可见,方法执行事件和构造方法执行事件的c『this与G。瑁既的含义相同。表4.3各类事件表示节点的‰。,ct州的含义事件Ghi.G.㈣方法调用调用方法时伪变量珐妇指向的对象的类型调用方法时被调对象的类型方法执行方法执行时伪变量this指向的对象的类型方法执行时执行对象的类型构造方法调用调用构造方法时伪变量this指向的对象的类型调用构造方法时被调对象的类型构造方法执行构造方法执行时伪变量this指向的对象的类型构造方泫执行时执行对象的类型属性读属性读时伪变量this指向的对象的类型属性访问时被访问对象的类型属性写属性写时伪变量this指向的对象的类型属性赋值时被访问对象的类型通知执行时target切点暴露出的对通知执行通知执行时this切点暴露出的对象的类型象的类型上下文不敏感的性质决定了上下文不敏感面向方面调用图无法利用节点的类型属性直接表示出大部分节点的动态类型。例如,图4.2是图4.1程序片段的不完全ACG(节点上没有标注类型),图中椭圆形节点表示方法执行事件,长方形节点表示方法调用事件,源程序中语句8处的方法调用对应左边的两条有向边,语句11处的方法调用对应右边的两条有向边。分析程序的语义可以获知,程序沿左边的路径执行到节点4时,其动态类型为,而程序沿右边的路径执行到该节点时,其动态类型为。由此可见,节点4不仅具有两种不同的动态类型,而且其动态类型还和程序执行到该点时的路径相关,因此,我们无法在该节点上直接将其所有的动态类型都表示出来。图4.2程序示例的不完全ACG为此,我们通过一种间接的方式记录节点的动态类型,基本思想是将节点的动态类型信息记录在路径中,若需知道程序沿某条路径执行到某节点时该节点的动态类型,则只须从起点开始沿着相应的路径推导到该节点即可。例如,对于图4.2所示的ACG,静态分析时可获知节点2的类型是<℃,B>(下文称之为节点2的静态类型),当程序沿着左边路径执行时,节点2的动态类型等于其在静态分析时获取的类型,而节点4的动态类型<13,B>可以从=肯点2的动态类型中推导出来(节点4的动态类型的cthi。和‰都等于节点2的动态类型的‰)。同样的,当程序沿着右边路径执行时,节点3和节点4的动态类型可类似推导出来。具体的,我们记录节点动态类型的方法包含两个方面的内容:其一是将节点的类型分为静态类型和动态类型;其二是确定节点间类型的依赖关系。53 东南大学博士学位论文1)静态类型与动态类型首先,我们将节点的类型分为静态的和动态的两种。静态节点类型是在构造程序ACG时赋予节点的。表4.4给出了各事件表示节点的静态节点类型。表4.4各事件表示节点的静态类型静态节点类型事件GmC。Ⅲ方法调用相应方法调用语句所在的类型构造时分析所得被调对象的类型方法执行定义该方法的类型.构造方法调用相应构造方法调用语句所在的类型构造时分析所得被调对象的类型构造方法执行定义该构造方法的类型属性读相应属性读语句所在的类型构造时分析所得被访问对象的类型属性写相应属性写语句所在的类型构造时分析所得被访问对象的类型this切点中声明的类型,若没有声target切点中声明的类型,若没有声通知执行明则为Object图4.3(a)是一程序片段,图4.3(b)是该程序片段的不完全ACG,由于节点种类较多不方便使用不同的形状来区分,我们通过节点最左边的数字表示该节点的种类(如1代表该节点是表示方法调用的节点),符号“@”左边为节点表示事件的名字,右边为该节点的静态类型。例如,表示方法ml执行事件的节点的静态类型为,表示属性fl写事件的节点的静态类型为,表示通知执行事件的节点的静态类型为。publicclassA(publicStringfl;publicvoidmlO{⋯))publicclassBextendsAfpublicB(Stringp1){fi=pl;"publicstaticvoidmain(Strin91]args){Bob=newB(“foobar"’);Strings=ob.fl;(a)0b.ml();publicaspectAspecti{before0:call(+mlO)&&this(B)&&target(B){⋯)//adi)图4.3程序示例及其不完全ACG 东南大学博士学位论文2)节点间类型依赖关系其次,我们明确节点间的类型依赖关系。若节点B的动态类型需推导自节点A的动态类型,则我们称节点B类型依赖于节点A。相反的,若节点B的动态类型等于自身的静态类型,则我们称节点B类型不依赖于节点A。由于节点种类较多,因此节点间类型依赖关系的分析较为繁复,我们分情况讨论。表4.5给出了每类节点可能的前驱节点的种类。该表的行表示前驱节点,列表示后继节点,若表项(nl,n2)为“√”则表示节点nl的前驱可以是节点n2。例如,mcall节点的前驱节点可以是mexec节点、ceXec节点和aexec节点;mexee节点的前驱节点只能是meall节点。表4.5节点间的前驱关系披mealImeXeCccallCexeC窀etfsctaeXeCmeall√meXeC√coall’,√CeXeC√麾et√fset√aeXeC√^,√我们逐一针对每种节点间的前驱关系讨论节点间的类型依赖关系i1)施调方法mexec节点指向被调方法meall节点。这种情况下,·若通过this或super伪变量调用方法,则被调方法.mcall节点的瓯i。和ct州等于施调方法mexec节点的Ctarget;·若通过其它变量调用方法,则被调方法mcall节点的Crthi。等于施调方法mexee节点的ct雄d。2)施调构造方法cexec节点指向被调方法mcall节点。这种情况下,·若通过this或super伪变量调用方法,则被调方法mcall节点的Crmi。和Ct球。等于施调构造方法eexee节点的ctarget;·若通过其它变量调用方法,则被调方法mcail节点的CIhi。等于施调构造方法cexec节点的Ct。rgcI。3)施调通知aexec节点指向被调方法mcall节点。这种情况下,·若通知体内通过this切点中的参数调用方法,则被调方法mcall节点的ct。州等于通知执行节点的Cthis;·若通知体内通过target切点中的参数调用方法,则被调方法mcall节点的ct。啊等于通知执行节点的G。增eta‘4)被调方法mcall节点指向被调方法mexec节点。这种情况下,·若通过this或super伪变量调用方法,则被调方法mexec节点的Ghi。和ct。啊等于被调方法mcall节点的cIarg。l;·若通过其它变量调用子类继承的方法,则被调方法mexec节点的C"this和G哪。等于被调方法mcall节点的Ct。增et。.5)施调方法mexec节点指向被调构造方法ccall节点。这种情况下,节点间不存在类型依赖。6)施调构造方法cexec节点指向被调构造方法ccall节点,其含义是在一个构造方法中调用另一个构造方法,而凋用的可能是同一个类的构造方法,也可能是其它类的构造方法。这种情况下,·若通过this或super伪变量调用另一个构造方法,表明调用的是同一个类或其父类的构造方法,则被调构造方法ccall节点的%。和ct。喇等于施调构造方法cexec节点的Ct。州。7)施调通知aexec节点指向被调构造方法ccall节点。这种情况下,节点间不存在类型依赖。8)被调构造方法ccall节点指向被调构造方法cexcc节点。这种情况下,·若通过this或super伪变量调用构造方法,表明调用的是同一个类或其父类的构造方法,则被凋构造方法cexec节点的Cthi。和G喇等于被调构造方法ccall节点的Ctwget·若通过其它方式调用子类继承的构造方法,表明调用的是另一个类的构造方法,则被调构造方法cexec节点的Clhi。和CI。氇ef等于被调构造方法ccall节点的Ct。rget。55 东南大学博士学位论文9)旎调方法mexee节点指向对象属性龟et节点。这种情况下,·若通过this或super伪变量访问属性,则对象属性fget节点的Ckis和ct。啊等于施调方法mexee节点的‰。10)旎调构造方法cexec节点指向对象属性fget节点。这种情况下,·若通过this或super伪变量访问属性,则对象属性fget节点的CIllis和‰等于施调构造方法cexec节点的‰。11)旎调通知aexec节点指向对象属性fget节点。这种情况下,·若通知体内通过this切点中的参数访问对象属性,则对象属性fget节点的‰等于施调通知agxec节点的Cthis;··若通知体内通过target切点中的参数访问对象属性,则对象属性fget节点的Ct。r鲫等于施调通知aexec节点的cta恻。12)施调方法mexec节点指向对象属性fset节点。这种情况下,·若通过this或super伪变量访闯属性,则对象属性fset节点的C缸和Cl。瓣t等于施调方法mgxec节点的Cl缎eI。13)施调构造方法cexec节点指向对象属性fret节点。这种情况下,·若通过this或super伪变量访问属性,则对象属性fset节点的Clhi。和G盯gel等于施调构造方法CeXCC节点的Cl。耀et。14)旌调通知aexec节点指向对象属性fset节点。这种情况下,·若通知体内通过this切点中的参数访问对象属性,则对象属性fset节点的‰等于施调通知aexec节点的Cthis;·若通知体内通过target切点中的参数访问对象属性,则对象属性fset节点的G。喇等于施调通知aexec节点的Ct。倒。15)任意节点指向被调通知aexec节点。这种情况下,被调通知aexec节点的Ghi。和G删分别等于前驱节点的Ghi。和G。州。总结上述各种情况,可以将后继节点对于前驱节点的类型依赖分为以下几类:a)后继节点动态类型的‰。和c切啊等于前驱节点动态类型的ct。啊;b)后继节点动态类型的‰。等于前驱节点动态类型的Ct椎既,cI。恻等于自身静态类型的Ctarget;c)后继节点动态类型的Cl。删等于前驱节点动态类型的%is,cfhis等于自身静态类型的Cthi。。d)后继节点动态类型的ct删等于前驱节点动态类型的Ct崛时,CIhi。等于自身静态类型的Cthis;e)后继节点动态类型的瓯i。和G啊分别等于前驱节点动态类型的ClIIi。和Ct。恻。4.1.3边的分类ACG的最后一个扩展是令有向边的结构包含字段d,用以表示该边连接的两个节点间的类型依赖关系。我们令d=0表示该边连接的节点间不存在类型依赖,d=l~5分别表示前一节中分析得出的五种依赖。我们称d=0的边为类型不依赖边,d>0的边为类型依赖边。至此,.我们给出面向方面调用图ACG的完整定义。定义4.1面向方面调用图是一个有向图ACG=毗厂>,其中:(1)Ⅳ是节点集,VneN,n=,d表示边的种类,nhead表示头节点,ntail表示尾节点。(3),.是入口节点,通常为main方法执行节点。图4.4是一AspecO程序实例,该程序包含A、B两个类和一个方面Aspectl,方面中包含一个通知。图4.5是该程序实例的上下文不敏感ACG,为了方便起见,我们只表示出了方法调用、方法执行和通知执行三类事件,部分节点上标注了静态类型,虚线边是类型依赖边,实线边是类型不依赖边,部分类型依赖边上标注了边的种类。 东南大学博士学位论文classA(B两ewsO;publicvoidm1(){⋯}扎m2();publicvoidm20(b.ndO;ml();}’)"classBextendsA{publicaspectAspectI(publicvoidml(){⋯)/‘adl+/publicvoidm3(){atter(Bb):call(+mIO)&&target(b)&&m2();cflow(call(+nd0)&&target(B)){)’b.m40;publicstaticvoidmain(String[]args){}Aa---newA0;"图4.4AspectJ程序实例图4.5AspecO程序实例的ACG4.1.4节点动态类型推导在构造好的AspectJ程序上下文不敏感ACG上,我们可以推导出具体路径中节点的动态类型。推导从起始节点开始,沿着路径中的边一段段的推导下去。定义4.2给出了边e上的节点动态类型推导规则。定义4.2设e是ACG上的一条有向边,d表示e的种类,11l是e的头节点,其动态类型为DynaType(n!),n2是e的尾节点,其静态类型为StaT》pe(n2),则n2的动态类型为:1)若d==-0,则DynaType(n2)=;2)若d一---I,且DynaType(nO.cIa曙甜不是StaType(n2).Cthi。以及StaType(n2).‰鼬的父类,则DynaType(n2)=,否则DynaType(n2)=<上,上>;3)若d-一-2,且DynaType(n!).G删不是StaType(n2).Cthi。的父类,则DynaType(n2)=,否则DynaType(n2)2<上,上>;4)若d一3,且DynaType(nO.cthjs不是StaType(n2)。GI罾e|的父类,则DynaType(n2)=;5)若d—=4,且DynaType(nO.CI州不是StaType(n2).cI孤伊t的父类,则DynaType(n2)=;6)若d一---5,且DynaType(nO.Ghi。不是StaType(n2).‰。的父类,DynaType(nO.cI。恻不是StaType(n2).cI删的父类,则DynaType(n2)=,否则DynaType(n2)=<上,上>;上述定义中每条类型依赖边上的推导规则都包含后继节点静态类型与前驱节点动态类型的比较,比较的目的是排除ACG上的虚假边。57 东南大学博士学位论文当程序沿着某条路径执行到某个节点时,若遇到虚假边则不会沿该边继续执行下去。上下文不敏感ACG上虚假边的产生是由面向对象的多态和重载(overload)机制导致的。图上,虚假边一定是一条类型依赖边,而类型依赖边是否是虚假边则依赖于程序执行到该边前驱节点时执行对象的实际类型。以图4.4的程序举例说明,程序中父类A定义了方法m1和m2,并在m2中调用ml,子类B重载了A的方法ml,在图4.5所示的该程序ACG中,节点6分别射出边e7指向节点7以及边e9指向节点8。当程序执行到节点6时,若执行对象的实际类型是A,则不会沿边e7继续执行,因为父类对象不能调用子类的方法,此时e,是虚假边;相反的,若执行对象的类型是B,则不会沿边e9继续执行,因为子类对象应该调用重载的方法,此时e9是虚假边。由此,按照产生的原因,虚假边可分为两类:一类是父类指向子类的虚假边,如边e7;.另一类是子类指向父类的虚假边,如边e9。目前,定义4.2的节点动态类型推导规则只能识别第一类虚假边,在该定义中,若后继节点的动态类型为<上,上>,则表示该边是一条虚假边。我们称包含虚假边的路径为虚假路径。我们以图4.5中路径ele2e7e8以及路径e3e4e5e6e7e8上的节点类型推导为例。首先沿ele2e7e8推导:节点1的动态类型等于自身的静态类型为,边el为类型不依赖边,因此节点2的动态类型为,边e2也为类型不依赖边,因此节点6的动态类型为,边e7是第一类类型依赖边,节点7的静态类型为,由于A是B的父类,因此节点7的动态类型为<上,上>,边e7是一条虚假边,路径ele2e7e8是一条虚假路径。我们再沿e3e4e5e6e7e8推导:类似的,我们可推导出节点1、节点3、节点4、节点5和节点6的动态类型都为,沿边e7推导时,由于B不是B的父类,因此节点7的动态类型为,此时边e7不是虚假边,路径e3e4e5e6e7e8不是一条虚假路径。4.2面向方面调用图的构造AspectJ程序上下文不敏感面向方面调用图的构造面临三个新的问题。首先,是新事件的识别。在目前ACG可以表示的7类事件中,识别方法调用和方法执行事件只需分析源程序中的方法调用语句,识别构造方法调用和构造方法执行事件只需分析源程序中的对象创建语句,识别属性访问事件则只需分析源程序中的属性访问语句。最困难的是通知执行事件的识别,因为通知没有相应的显式调用语句。对于不考察对象动态类型以及运行时调用栈状态的静态通知,可以在ACO上准确的找到调用点;但对于考察对象动态类型或运行时调用栈状态的动态通知,初始只能找到可能的调用点,若要进~步提高ACG的精度,可以采用第六章的方法进行优化。另一方面,虽然ACG可表示的事件种类较多,但构造ACG时不需要全部表示出来(例如属性读写事件、构造方法调用或执行事件等),可以按需选择。一般的,ACG的最小节点集包括表示方法调用的节点和表示方法执行的节点。另外,某些节点通常也是伴随出现的,譬如表示方法调用的节点和表示方法执行的节点、表示构造方法调用的节点和表示构造方法执行的:1了点。其次,是节点静态类型的获取。表4.4给出了每类节点静态类型的含义,通过类型分析和简单的语法分析即可获得各类节点的静态类型。最后,是:i了点间类型依赖关系的确定。这也不难做到,只需通过简单的语法分析并根据4.1.2节介绍的标准判断即可。‘我们称AspectJ程序中方面程序以外的Java程序部分为基程序。具体的,我们分两步构造AspectJ程序的上下文不敏感ACG:第一步,构造基程序ACG;第二步,关联通知。4.2.1基程序ACG的构造为了构造基程序的ACG,首先我们采用第二章介绍的过程内分析方法对基程序做类型分析,其中方法入口锚点变量类型的估计范围是整个程序,而不仅仅是基程序。然后,针对需要构造的节点类型,构造相应的节点和边,具体的:·若需构造表示方法调用以及执行的节点,则参考相应的方法调用语句,针对被调对象的每一种可能类型构造对应的mcali节点,并据此查找调用的具体方法,针对该具体方法建立对应的mexec节点,并用正确的有向边连接这些:悔点;·若需构造表示构造方法调用以及执行的节点,则参考相应的对象创建语句,根据类声明的继承关系58 东南大学博士学位论文构造对应的一系列ccall节点以及cexec节点,并用正确的有向边连接这些节点。·若需构造表示对象属性读或写的节点,则参考相应的对象属性读或写语句,针对被访问对象的每一种可能类型构造对应的fget或fset节点,并用正确的有向边连接这些节点。4.2.2通知关联及通知ACG的构造关联通知,即是在已有的ACG上寻找其新的所有可能的织入点,从这些织入点引出有向边到通知执行节点上,若没有构造该通知体的ACG则构造之,与原有的ACG连接形成关联后的ACG。通知织入点的寻找需要对通知的切点做快速的解析。我们将切点解析为四元组(kiD,C『mis’%gel),其中各个元素的含义与定义4.1中的相同。具体的解析过程如算法4.1所示,其中,四元组上操作“n”的含义是由两个四元组中非空的项拼成一个新的四元组。由于从FieldPattern、MethodPattern以及ConstructorPattern中解析出的类型是静态类型,而从this0和target()切点中解析出的类型是动态类型【I引,因此在进行“n”操作时,若“js或CI。Iget同时存在静态类型和动态类型,则需用动态类型取代静态类型。输入:切点输出:解析出的四元组集合S算法:1.首先利用切点与联结符“&&”对或联结符“旷的分配率,将“¨”提取到切点的最外面,从而将切点分解为多个予切点的或。2.然后对每个子切点,去掉其中最外层的cflow(⋯)或cflowbelow(⋯)部分,对剩下部分中的每一个原子切点做(令该子切点解析fIj的四元组为R):1)若该原子切点是get(FieldPattern)切点,则R=(fgekfName,。SType);2)若该原予切点足set(FieldPattern)切点,则R=(fset,fName,JSType);3)若该原子切点足call(MethodPattern)切点,则R=(recall,mName,。SType);4)若该原子切点是call(ConstructorPattern)切点,则R=(ccall,cName,JSType);5)若该原予切点是execution(MethodPattern)七.)J点,则R。(mexee,reName,SType,SType);6)若该原予切点足execution(ConstructorPattern)切点,则R=(cexec,cName,SType,SType);7)若该原子切点是adviceexecution()切点,则R=(aexec,。。j;8)若该原子切点是this(Type)切点,则R=RnL。Orym,j;9)若该原子切点是target(Type)七3J点,则R=Rf"l乙。。DType);3.将解析每个子切点得到的口q元组R组成该切点的四元组集合S算法4.1切点快速解析算法例如,切点(call(·ml0)llexecution(幸m20))&&this(A)&&target(B)&&cflowbelow(call(串m30))的解析过程为:首先提取“0”,分解为两个子切点call(丰m10)&&this(A)&&target(B)&&cflowbelow(call(·m30))和execution(·m20)&&this(A)&&target(B)&&eftowbelow(call(幸m30))其次去掉最外层的cflowbeiow0切点,得到子切点call(掌ml0)&&this(A)&&target(B)和execution(幸m20)&&this(A)&&target(B)然后解析每个子切点,得到四元组集合为{(mcall,ml,A,B),(mexec,m2,A,B))。将通知的切点解析为四元纽集合后,针对每个四元组在ACG上查找与之匹配的节点。设待匹配的四元组为(七』D,C’lhis"C么唣et),匹配分为k的匹配,1D的匹配以及的匹配。其中,k和仞’的匹配是文字匹配。而的匹配分两种情况:1)一种是与类型不依赖于前驱节点的节点匹配,此时要求:常点的静态类型clhi。字段值为C;his或其子类,cf。恻字段值为Cj。啊或其子类;2)另一种是与类型依赖于前驱节点的节点匹配,此时要求节点的静态类型cmi。字段值为C"thi。或其父类,CI。喇字段值为C’协倒或其父类。在k、ID和<℃饥,C,la馏cl>都匹配成功的节点上织入通知,连接上类型依赖边,若通知体的ACG还没有构造则构造之。对于通知体ACG的构造,可以把它当作一个普通的Java方法,采用相同的过程内分析方法构造,通知体入口锚点类型的估计范围也是整个程序。59 东南大学博士学位论文关联通知操作需反复进行,直至没有新的织入点。至此,程序的ACG构造完毕。4.3本章小结目前,讨论AspectJ程序调用图及其构造的文献很少。HayashidaR等人i64J以及TakashiIshio等人阱J直接将面向对象程序调用图用于AspectJ程序的表示。他们将通知也看做普通的方法,调用图只表示了方法执行和通知执行这两种程序事件。他们利用已有的面向对象程序调用图的构造方法分别构造基程序和方面程序的调用图,然后通过文本匹配确定通知的调用点,但仅仅考虑了静态切点。李楠等人将面向对象程序调用图中的节点扩展为两类,分别表示方法调用和方法执行事件,并且也将通知看做普通的方法。他们将RA、RTA、VTA方法扩展到AspeetJ程序中,并且同样通过文本匹配确定通知的调用点,但考虑了oflow切点的匹配166,671。前人提出的AspectJ程序调用图只能表示连接点模型中少数的程序执行事件,并且都没有考虑节点动态类型的表示。调用图的构造方法也都是基于传统方法,因而不可避免的存在传统方法精度低的缺陷。针对这些不足,我们提出了面向方面调用图,该调用图能够表示AspectJ语言连接点模型中的大部分程序执行事件,并且能够通过推导的方式间接的表示出节点的动态类型。我们利用第二章的方法对基程序和方面程序中的方法进行类型分析,因而构造出的调用图更加精确。我们通过对切点进行快速解析来估计通知的织入点。对于静态通知,我们的方法能够准备的估计织入点,但对于动态通知,我们只能估计出所有可能的织入点。 东南大学博士学位论文第五章AspectJ动态通知编织优化AspectJ将软件中的横切关注点封装为单独的方面程序,并通过连接点将基程序和方面程序联系起来。连接点是AspectJ预定义的一组程序执行事件。AspectJ用这些执行事件组成程序调用栈。在程序运行过程中,当调用栈出现特定状态时,相应通知中的代码就会被执行。通知与切点关联,通知的切点指定了该通知关注的调用栈模式。AspectJ的切点可分为静态和动态两种。静态切点只考察调用栈的栈项元素,同时忽略对象的运行时类型。例如切点call(voidm0)表示关注当前任意对象m方法的调用。动态切点又可分为三类:第一类动态切点通过cflowO或cflowbelow0考察调用栈中的信息。例如切点call(宰mlO)&&cflow(call(事m3())要求栈中包含m3方法的调用;第二类动态切点通过thisO或targetO考察对象的运行时类型。例如切点call(*m10)&&larget(B)要求被调对象是B的实例;第三类动态切点则兼具前两类动态特性,既考察调用栈的状态,又考察运行时类型,例如切点call(*m10)&&target(b)&&cflow(call(*m30)&&target(B))。通常,方面程序中第三类动态切点居多。我们分别把包含静态切点和动态切点的通知称为静态通知和动态通知。AspectJ编译程序将方面静态织入到程序中【23埘】。这种织入方式将编织代价转移到编译时,并且使得方面的执行不需要修改Java虚拟机。它通过分析通知的切点,确定程序中的织入点,织入相应通知的调用。AspecO编译程序能够确定静态通知的织入点,但难以确定动态通知的织入点,只能将其调用织入所有可能的织入点,并插入条件判断语句作为滞留程序。留待运行时做匹配。例如,编织包含切点call(*m10)&&target(B)的通知会在通知调用前插入如下所示的instanceof判断语句(其中obj是被调对象)if(objinstanceofB)ca//advice;obj.m10;编织包含切点calI(奉ml())&&cflow(call(木m30)的通知会在通知调用前插入如下所示的调用栈是否为空的判断语句(编译程序会在m3方法调用前后分别插入入栈和出栈语句)if(!cflowstack.getThreadStack0.isEmptyO)calladvice;obj.mlO;滞留程序无疑增加了程序运行时的开销。由于方面程序通常包含较多的动态通知,如何减少这部分开销成为提高AspectJ程序运行效率的关键。人们在深入研究的基础上提出了一些解决方法。其中,MasuharaH使用部分求值技术,利用编译时获得的静态信息确定织入点,该方法对静态切点有效,但对动态切点的优化效果不好【681。AspectJ编译程序针对cflow的匹配做了优化,它通过构造匹配自动机使得匹配时只需查看栈顶元素【69】。这两种方法只能适当提高动态匹配效率,均未尝试确定动态切点的织入点以消除匹配过程。AvgustinovP等人提出了基于cflow分析的优化方法,但该方法只考虑了cflow的优化,忽略了对象运行时类型的分析,因此不适用于优化具有此类动态性的切点,而在所有的动态切点中又以这种切点居引63,70】。针对前人方法的不足,我们提出了一种AspectJ程序动态通知编织的优化方法。该方法利用程序的上下文不敏感面向方面调用图ACG求解调用栈,并对调用栈中的节点进行动态类型推导,再将调用栈与切点匹配,根据匹配结果优化通知的织入。实例研究结果表明,在ACG上求解调用栈并结合动态类型推导的方法能够显著提高优化的精度,有效减少运行时匹配过程,从而有助于提高程序的运行效率。5.1问题分析AspectJ语言的连接点模型定义了11种程序执行事件,每一种事件都对应一段特定模式的Java字节码程序(见表4.1)113】。例如,方法调用事件对应字节码程序中的invoke语句,方法执行事件对应方法的整个代码段。通知通过其切点指定源程序中若干具体的连接点,并根据关键词“before”、“aRer”或“around”在相应的字节码程序段前、后插入通知调用,或者用通知调用取代原米的代码段。若是动态通知,则通知6l 东南大学博士学位论文调用前还将插入滞留程序。我们利用程序的上下文不敏感ACG来优化动态通知的编织。我们用ACG的节点表示程序中动态通知可能的织入点。方法执行、构造方法调用、构造方法执行以及通知执行等织入点对应于ACG上的单个节点,而方法调用、属性读和属性写等织入点则对应于ACG上的若干个节点。例如,图5.1所示是一AspectJ程序实例,其通知adl的切点属于第二类动态切点,通知ad2的切点属于第一类动态切点,而通知ad3和通知ad4的切点则都属于第三类动态切点。图5.2是该程序的上下文不敏感ACG。为了方便起见,我们只表示出了方法调用、方法执行和通知执行三类事件,部分节点上标注了静态类型,虚线边是类型依赖边,实线边是类型不依赖边,部分类型依赖边上标注了边的种类。该程序通知adl在语句18前的可能织入点对应节点4,通知ad4在方法m4中的可能织入点对应节点14。classA{publicvoidml(){⋯)publicvoidm2(){mlO;)}classBextendsA(publicvoidm30{ml();m20;}publicvoidm40{⋯}publicstaticvoidmain(String[]args){Aa--newA0;Bb--newB0;a.ml();a-m20;b.mlO;19a_b:20a.m30;2l}22)2324publicaspectAspectl(25before():call(’mlO)26&&target(B){⋯}//adl27befo喊):call(+ml())28&&cflow(call(‘m30){⋯’//ad229afler(Bb):call(。ml())&&targct(b)&&30cflow(call(+m30)&&target(B)){//ad33Ib.m40;‘32"33voidaround():execution(+m40)//ad434&&this(B)&&cflow(adviceexecutionO){⋯)35l图5.1AspeetJ程序实例图5.2AspeetJ程序实例的上下文不敏感ACG对于第一类动态切点,如果能够求出程序执行到织入点时调用栈的所有可能模式,那么通过判断这些模式是否被切点包含就能优化通知的编织:若所有模式都被切点包含,则明确织入通知调用;若切点不包含任一种模式,则无需织入;否则仍需条件织入。而调用栈的所有可能模式可以用上下文不敏感ACG上●23456789加“伦B¨:2撕"墙 东南大学博士学位论文从起始节点到织入点对应节点的所有路径的逆序列来描述。例如,在图5.2中,当程序执行到节点10时,调用栈为(recall.,m1);(mexec,m3);(mcal!,m3);(mcxec,,main)当程序执行到节点9时,调用栈为(mcall,m1);(mexec,,m2);(mcall,m2);(mexec,main)或(meal!,m1);(mexec,m2),(mcail,m2);(mexec,,m3);(mcall,m3);(mexec,main)其中,mcall与mexec分别表示方法调用与方法执行。因此通知ad2可织入节点lO,但需条件织入节点9。对于第二类动态切点,则可以利用上下文不敏感ACG的类型推导能力求出由起始节点沿一切可能的路径到达织入点对应节点时相关对象所有可能的动态类型,若这些类型被切点包含,则明确织入:若切点不包含任一种类型,则无需织入;否则仍需条件织入。例如,在图5.2中,节点5处被调对象的类型是A,节点9处被调对象的类型是A或B,节点10处被调对象的类型是B,因此通知adl织入节点10,不织入节点5,条件织入节点9。对于第三类动态切点的优化,则需综合前两类的优化方法。由此,我们提出的方法的大致优化过程是:首先构造程序的上下文不敏感ACG,然后在其上求出可能织入点的路径表达式,并推导式中所含节点的动态类型,最后将该表达式与切点匹配,若切点包含表达式中的所有模式,则将通知调用无条件织入该节点;若切点不包含其中任一种模式,则通知调用不织入;至于其它情况,通知调用仍需条件织入。为了突出重点,我们对方面使用的切点加以约束,采用AspectJ切点语言的子集,但这不妨碍将该方法推广到一般情况下:切点::=callC方法名)Iexecution(方法名)Iadvieeexecution0Ithis(!类名)Itarget(类名,...)cflow(切点)Icflowbelow(切点)I(切点&&切点)I(切点Il切点)5。2编织优化优化AspectJ动态通知编织的具体步骤如下:(1)将方面中的所有切点转换成正规表达式的形式。(2)构造AspectJ程序的上下文不敏感ACG。(3)采用高斯消去法在ACG上求解从起点到达每个待分析织入点的路径表达式,并推导表达式中节点的类型。(4)将路径表达式转换成凋用栈表达式,并与切点表达式匹配,根据匹配结果确定通知调用的织入方式。下面以5.1节的切点集为例分别详细论述这些步骤。5.2.1切点转换为便于与调用栈表达式匹配,我们将切点转换成如下正规表达式的形式:切点表达式::=基本项{;基本项)·基本项::=伉皿c矗is,Gargel)ftrue’ftrue+其中,k、ID、瓯is、Ct。瓣t的含义和定义4.1相同,“true’"和“true+’’类似于通配符,当与调用栈表达式进行匹配时,“true啊可以匹配调用栈表达式中任何连续的零项至若干项,“true+’’可以匹配调用栈表达式中任何连续的一项至若干项。例如,切点’call(木m10)&&target(B)&&cflow(call(母m3())&&ta唱et(B))转换成的切点表达式为(mcall,ml,_,B);true。;(mcall,,m3,_,B);true’。我们首先给出~个辅助定义及基本转换函数,然后给出切点转换算法。定义5.1设R,、局是切点表达式,定义切点表达式的n运算如下,63 东南大学博士学位论文(1)如果R,和飓都是基本项,则R,f"lR2生成新的基本项,项中各字段的值取自R,或飓中的相应字段。(2)如果R,是基本项,彤形如“true‘l码;切点表达式”,且风≠tI.ue’或true+,若RI=R3,则RINRz----true’;局;切点表达式;若R,≠飓,则R,flRz=R,;true’皿,;切点表达式。(3)如果R,是基本项,而形如“仇矿两;切点表达式”,且R:true’或true+,则Rtn飓=泛,;tme+l如;切点表达式。算法5.1给出了基本转换函数。输入:切点输出:切点表达式算法:beginif(切点一--------七jj点1&&切点2)thenreturn“切点1)n“切点2)endifif(切点≈flow(切点1))thenreturn‘"true’;”“切点1)endifif(切点=cflowbelow(切点1))thenreturn‘"true+;”“切点1)endifif(切点=call(方法名))thenreturn“(meall,方法名,一,j”endifif(切点一-execution(方法名))thenreturn“(mexec,方法名,。j”endifif(切点一adviceexecution0)thenretum“(aexec,_"j”endifif(切点—carge“类名))thenretum“乙u。类名)”endifif(切点=--this(类名))thenreturn“L。类名J”endifend算法5.1基本转换函数t切点转换算法PCTrans如算法5.2所示。输入:通知的切点输出:切点表达式集算法:1.运用分配率提取出切点中的0运算符,将原切点转换成“切点lII...Il切点n”的形式,收集切点I至切点n,组成待转换切点集;2.针对待转换切点集中的每个切点调用基本转换函数,(切点)转换成正规表达式:算法5.2切点转换算法PCTrans5.2.2ACG构造我们利用4.2节介绍的方法构造AspeetJ程序的上下文不敏感ACG。该构造方法分为两步:首先是构造基程序的上下文不敏感ACG,其次是反复的关联通知。在通知关联过程中,需要将通知的切点解析为一个四元组,由于该四元组的结构与切点正规表达式中基本项的结构一致,因此,将切点转换成正规表达式的形式以后,在构造AspectJ程序上下文不敏感ACG过程中关联通知时就不需要再次解析通知的切点,可以利用切点表达式寻找通知的所有可能织入点,方法是查看切点表达式集中每个表达式的第一项(即第一个“:”前的项):(1)如果该项形如“(meail,方法名,,类名)”,表示可能织入点是类型为“类名”的方法调用点,这对应于上下文不敏感ACG上两类节点,一类是静态节点类型Ct。噼。字段值为该类或其子类,且类型不依赖于前驱节点的方法调用节点;另一类是静态节点类型cI。哪。字段值为该类或其父类,且类型依赖于前驱节点的方法调用节点。例如,图5.2中adl在节点10上的关联就属于后者。(2)如果该项形如“(mexec,方法名,,类名)”或“(mexec,方法名,类名,)”,表示可能织入点是类型为“类名”的方法执行点,这对应于上下文不敏感ACG上两类可能节点,一类是静态节点类型Ghi。字段值为该类或其子类,且类型不依赖于前驱节点的方法执行节点;另一类是静态节点类型Cthi。字段值为该类或其父类,且类型依赖于前驱节点的方法执行节点。例如,图5.2中ad4在节点14上的关联就属于后者。上下文不敏感ACG中被通知关联的节点成为待分析织入点,留待下一步分析。5.2.3调用栈表达式求解构造好程序的上下文不敏感ACG,并确定了待分析织入点后,下一步要做的是求解这些待分析织入点的调用栈表达式。我们用调用栈表达式描述程序沿不同路径执行到某节点时调用栈的所有模式,其定义如 东南大学博士学位论文定义5.2所示。定义5.2调用栈表达式是四元组e---(LID,SCthis,蹈删)上的正规表达式,其中:(1)k和仍的含义与定义4.1中的相同,分别表示节点的种类和节点的标识。(2)SCthis和踞。倒是类型集,分别表示节点类型‰字段的值的集合和节点类型‰字段的值的集合,我们称茭tj节点的类型集。例如,图5.2中节点9的调用栈表达式为(mcall,ml,{A,B},{A,B});(mexec,m2,{A,B),{A,B));{(mcall,m2,{B},{A})+(mcall,m2,{B),{B});(mexec,m3,{B},{B});(mcall,m3,{B>,{B>););(mexec,main,{B):{B))我们分三步求解上下文不敏感ACG上待分析织入点的调用栈表达式:首先求出图上由起点至该节点的路径表达式,然后推导表达式中节点的动态类型集,并且在推导的过程中实时地修正路径表达式,最后再将路径表达式转换成调用栈表达式。两点间的路径表达式(pathexpression)是由上下文不敏感ACG上的边组成的正规表达式,包含了由起点至终点的所有路径。例如,图5.2中起点至节点9的路径表达式为(ele2+e3e4e5e6)e7。我们采用高斯消去法求路径表达式[120,121】。该方法首先求起点到终点的路径序列。路径序列(pathsequence)是一个序列(Pl,Vl,W1),(P2,V2,W2),⋯,(Pk,Vk,Wk),其中Vi和Wi是节点,Pi是Vi和Wi间的路径。该序列要求满足这样的性质,即起点到终点间的任一条路径都能够由序列中的某些子路径拼接而成。文献[120,121]给出了求路径序列的算法ELIMINATE。例如,图5.2中起点至节点9的路径序列为(el,l,2),(e2,2,8),(e3,1,3),(e4,3,6),(e5,6,7),(e6,7,8),(e7,8,9)。然后运用算法SOLVE[120,121]即可从路径序列中可求出路径表达式。由于路径表达式包含了从起点至待分析织入点的所有路径,因此表达式中节点的动态类型就可能不只一种取值,我们用节点的类型集的集合。节点类型集的推导不同于单条路径上节点动态类型的推导。在介绍推导算法前,我们首先定义类型集上的“,”操作如定义5.3所示,以及边e上的类型集推导函数疋如定义5.4所示。定义5.3令S∈ST是一类型集合,t∈T是一具体的类型,定义STXT--)ST的操作/如下:S/t=“t’)It’∈S,且t’等于t或者是t的子类}定义5.4设e是ACG上的一条有向边,d表示e的种类,n1是e的头节点,其动态类型集为DTS(n1),n2是e的尾节点,其静态类型为ST(n2),则n2的动态类型集DTS(n2)推导函数工:DTSxST"-)DTS为:1)若e.d==0,贝JJA(Drs(n1),s致n2))=<{S及n2).C,h插},{ST(n2).cf懈,)>;2)若e.d一1,则石(D碱n1),ST(n2))=;3)若e.d一2,贝IJA(DTS(n1),ST(n2))=;4)若e.d一3,则A(DTS(nt),S孔n2))《{S致n2).%括},DTS(n1).SCthis/ST(n2).Ctarget>;5)若e.d一4,贝Ufe(DTS(n1),s孔n2))=<{S及n2).c赢),DTS(n1).5B哪cl心及n2).G哪矿;6)若e.d一5,贝,Ufe(DTS(n1),S及n2))=:endforwodd/a={头节点vo);whileworklist-#{)dotakevfromworldist;foreachqePRED(v)doD双v)q_+v=f,(DTS(q),sT(V));,.e是q—v的边·,if(DTS(v)qⅢ.SGhi。一0orDTS(v)qwSG。噔d一0)thenDelete(e);//删除包含e作为必经路径的子表达式调整VP;endifendforif(P魍D(v)==0)thenDTS(v)={SHv));elseDTS(v)=uqe艘蹦v)DTS(v)q-"vI与r包含的节点类型集≮Sc|his,踞哪。t>的匹配规则为:·若SCthi。(或Ⅸ砀)中所有的类要么等于C矗i。(或cIarget)要么是其子类,则返回true;·若SCthi。(或SCt。gct)中存在某个类等于C,mis(或Ct哗t)或者是其子类,则返回possible;·其它情况则返回false。.最后根据判定结果决定通知调用的织入方式。令D∽)是表示历是否包含wJ(f-J⋯胛)的函数,那么:1)若^M..,烈M,f)=true,则通知调用织入此节点;2)若v卢J⋯.D(wj)=false,则通知调用不织入此节点;3)其它情况下通知调用仍需条件织入。 东南大学博士学位论文输入:调用栈串C,切点表达式P输出:判定结果true、false或者possible算法:begin取c的第一个四元组r’P的第一个基本项f’;result=match(r,r’);if(resu忙一false)thenretumfalse;endif取c的下一个四元组r"P的下一个基本项r’;ta92“”;while(true)doif(r’==‘"true*”)or(r’==‘‘true-h,)then.ta92r’:count=0:if(r’足P的最后一个基本项)thenrelm"nresult;else取P的下一个基本项r’:continue;endifendifresult=match(r,r’);if(resul户false)thenif((tag==‘‘true.’’)or(t炉‘tru矿’))thencount=count+1;if(r是C的最后一个四元组)thenretunlfalse;else取C的下一个四元组r;continue;endifelseretumfalse;endifelseif(tag--一"true.’’)thentag=“”;endifif(tag==‘‘true“)thenif(count>0)thentag=“’’:endifelseretumfalse;endifif(r’是P的最后一个基本项)thenreturnresult;else取c的下一个四元组r"P的下一个基本项r’;continue;endifendwhileend算法5.6判定算法Judge5.3实例研究输入:四元组r,基本项r’输出:true。faIse或possible算法:beginif(r.k!---r".k)or(r.ID!--r".ID)thenretumfalse;endifif(Vt∈r.SCtltis"t等于r’.Ct№或是其子类)and(Vt∈r.Sc凶睁t等于r’.C【|Igd或足其子类)thenreturntrue;endifif(3t∈r.SCthb,t等于r’.Cthh或是其子类)and(3tEr.SCt。rget,t等于r’.Ct。删或是其子类)thenreturnpossible;endifretumfalse;end算法5.7匹配函数Match我们以图5。l所示的程序做实例研究,该程序包含了4种常见的动态通知。图5.2是该程序的上下文不敏感ACG。通知adl~ad4的编织优化结果见表5.1,其中,打“、/”表示确定织入,打“X”表示确定不织入,打“?”表示条件织入。表5.1实例编织优化结果彩瀚a童5910414adI×?√ad2X?’,×ad3×?’,×ad4’,节点9上通知的织入方式确定过程为:首先节点9的路径表达式为(e102-I-03040506)e7,其次式中节点动态类型推导过程如下节点1:DynTypes(1)=<{StaType(1).C『恼},{StaType(1).cI。恻)>=<{B),{B)>;节点2:DynTypes(2)=<{StaType(2).Ck},{StaType(2).cI。.get}>=<{B),{A)>;节点3:DynTypes(3)=<{StaType(3).Ck’,{StaType(3).cl。rget)>=<{B},{B)>;67 东南大学博士学位论文节点6:DynTypes(6)=<{StaType(6).Ck。},{StaType(6).G嘴咀}>2<‘B},{B}>;节点7:DynTypes(7)=fes(DynTypes(6),StaType(7))=<{B},{B)>;节点8:DynTypes(8)=fc6(DynTypes(7),StaType(8))uStaType(8)=<{B},{B)xJ<{A>,{A)>=<{A,B),{A,B>>;节点9:DynTypes(9)=fe7(DynType(8),StaType(9))=<{A,B),{A,B}>;由此可知节点9处的调用栈表达式为(mcall,ml,{A,B),{A,B});(mexec,m2,{A,B>,{A,B));{(mcall,m2,{B),{A})+(mcall,m2,{B},{B});(mexec,m3,{B),{B));(mcall,m3,{B),{B}););(mexec,main,{B),{B)).因此adl、ad2、ad3在节点9上需条件织入。5.4本章小结我们曾在指向分析以及AOP语言程序分析方面做了深入的研究[122,123】,本章我们在此基础上进一步研究AspectJ程序的编织优化,提出了通用的动态通知优化方法。我们的方法具有以下优点:·该方法能够优化具有两种动态特性的通知。·该方法通过扩展ACG节点的种类,并且给出新的推导函数,可以优化包含大部分AspectJ切点的动态通知。·该方法可以比较容易的推广到其它的面向对象的AOP语言中,例如AspectC++等。·该方法都是安全的,不论AspectJ程序上下文敏感ACG的精度如何,基于该ACG的优化不会产生错误的通知调用。 东南大学博士学位论文第六章总结与展望AspeetJ语言是--f-3新兴的程序设计语言,它是在Java语言的基础上扩充了AOP系统而来的。AspeetJ语言具有的面向方面程序设计技术能够弥补现有技术(面向过程程序设计技术和面向对象程序设计技术)在模块化横切关注点方面的不足。AspectJ语言是研究AOP语言及其应用的主要平台。AspectJ语言的诞生既对程序分析领域提出了新问题,也对传统的分析提出了新的挑战。我们对AspectJ程序的面向方面调用图及其构造,以及动态通知的编织优化进行了深入的研究,并以此为出发点,按照新的需求重新考虑了Java程序类型分析和指向分析等问题。6.1论文总结本论文在以下几个方面取得了进展:·提出了基于SAT求解的Java程序类型分析的新方法,该方法是流敏感、属性敏感以及上下文敏感的,能够在复杂度可接受的情况下构造出更加精确的程序调用图。方法的基本思想是将程序抽象为命题逻辑公式,然后利用SAT求解器求解来完成分析。我们以方法为单位进行抽象,首先将方法转换成SSA扩展形式,然后将变量和属性抽象为布尔向量,类型被编码为具体的向量,相关语句的公式通过联结符“A”联结成方法的公式。我们通过求取方法抽象的概要进一步缩小方法公式的规模并化简推导过程。对于方法概要公式,既可以单独求解(过程内分析)也可以按照上下文不敏感或敏感的方式联结起来求解(过程间分析)。·提出了基于SAT求解的Java程序指向分析的新方法,该方法同样是流敏感、属性敏感以及上下文敏感的,能够有效缓解传统方法精确分析时的状态空间爆炸问题。方法的基本思想和主要分析流程与基于SAT求解的Java程序类型分析方法相同。主要区别在于指向分析方法是一个反复迭代、逐步求精的过程,它利用已有的分析结果精化当前的方法公式,再次组成程序的公式并求解,从而获得更加精确的分析结果,如此反复直至达到稳定。·提出了适合AspectJ程序分析的面向方面调用图,该调用图能够表示AspectJ语言定义的多种程序执行事件,并且能够在上下文不敏感的情况下间接表示出与节点相关的部分对象的动态类型,解决了传统上下文不敏感调用图的缺陷。我们在传统调用图的基础上增加了节点的种类,定义了节点的类型并区分静态节点类型和动态节点类型,另外还定义了边的种类。我们将基于SAT求解的Java程序类型分析方法用于上下文不敏感面向方面调JHj图的构造。对于基程序和方面程序中的通知,我们采用基于SAT的方法分析。对于通知在程序中的织入点,我们通过对切点做快速的解析来估计。对于静态通知,我们能够准确的估计通知的织入点,但对于动态通知,我们只能估计出所有可能的织入点。要想进一步提高动态通知织入点的估计精度,可以运用我们提出的动态通知编织优化方法。·提出了基于上下文不敏感面向方面调用图的AspectJ程序动态通知编织优化方法,相比较其它优化方法,该方法考虑了具有分别与对象的动态类型和程序运行时调用栈有关的两类动态性的通知的编织优化。我们的方法在上下文不敏感面向方面调用图上求解程序运行到可能织入点时的调用栈表达式,并利用面向方面调用图的动态类型推导能力推导调用栈表达式中节点的所有可能的类型,然后将该表达式与切点匹配,若切点包含表达式中的所有模式,则将通知调用无条件织入该节点;若切点不包含其中任一种模式,则通知调用不织入;’至于其它情况,通知调用仍需条件织入。6.2未来工作展望在未来的研究工作中,还需要在以下方面进行深入探讨:69 东南大学博士学位论文(1)与基于SAT求解的类型及指向分析相关·研究结构抽象过程中循环验证的新方法,进一步提高验证的效率。·目前的分析方法在联结方法公式时考虑了方法的所有锚点,但我们发现其中存在一些不必要的联结。例如,对于增加的方法入口锚点,并非所有的方法入口锚点都被方法内部引用,联结方法时可以不考虑那些没有被引用的入口锚点。今后将研究锚点联结的新方法,旨在减少不必要的公式,进一步缩小程序公式的规模。·指向分析的抽象精化步骤需对优化了的方法SSA扩展形式再次抽象,由于优化前后的方法SSA扩展形式具有相似性,今后将研究如何简化再次抽象的过程(例如再次抽象时的循环验证是否可以略去)。·目前我们对方法递归调用入口锚点的初始值进行全局的估计,该估计是安全的,但也是保守的,精度较低。另一种可能的估计方法是用递归方法内部的值来估计,今后我们将进一步证实该设想。·类型分析对方法的抽象与指向分析对方法的抽象具有很多共同点,今后我们将研究如何在综合两者的分析中共享并复用方法抽象以减少抽象方法的次数。·目前我们的方法在进行过程间分析时有可能因方法调用导致联结后的多个方法公式包含循环赋值路径,但这只有在循环结构中被调方法的返回值与调用该方法的参数之间存在赋值路径的情况下才可能发生,我们认为现实中该情况是很少见的。今后我们将研究更加完善的程序公式获取方法。·研究路径敏感的类型分析与指向分析方法。·研究如何将基于SAT的类型及指向分析方法推广到c程序分析中。·研究一般性的基于SAT求解的Java程序数据流分析方法。·完善SATTAS系统,实现过程问的类型分析,在此基础上进一步开发Java程序指向分析原型系统。(2)与AspectJ面向方面调用图及其构造相关·目前在沿某条路径推导节点动态类型时只能识别第一类虚假边,今后我们将研究第二类虚假边的识别方法。·研究如何进一步提高动态通知织入点的估计精度。·目前对基程序和通知的分析采用的是过程内分析方法,精度低于过程间分析,今后我们将研究如何对AspectJ程序进行过程间的类型分析以构造ACG。·研究上下文敏感的面向方面调用图及其构造方法。·研究如何在ACG节点类型中表示程序执行事件发生时参数的类型。(3)与AspectJ动态通知编织优化相关·由于受ACG的节点动态类型推导能力的限制,.目前在推导调用栈表达式中节点的动态类型时只能识别出第一类虚假边,今后我们将结合ACG的识别虚假边能力的增强,研究推导表达式中节点动态类型时第二类虚假边的识别方法。·在ACG节点扩充了参数类型的表示后,研究包含args0切点的动态通知编织优化。·研究基于上下文敏感ACG的动态通知编织优化。70 东南大学博士学位论文致谢首先,衷心感谢我的导师徐宝文教授。在研究生和博士生阶段的学习和工作中,徐老师一直给我无微不至的指导、关心和照顾,其中倾注了徐老师大量的心血。徐老师治学严谨、知识渊博、为人正直、心胸坦荡,对学生平易近人,对工作执着追求,传授给我的不仅仅是理论知识和实践能力,更重要的是做人的道理。徐老师对计算机软件理论的透彻理解和高瞻远瞩,使得我们教研室在计算机理论方面的研究工作一直不断进步;正是依靠了这样一个坚实的研究基础,我们才可能在程序分析与测试研究方面得到一系列的成果。其次我要感谢东南大学计算机系Ada实验室的老师(周晓宇老师、聂长海老师、戚晓芳老师、姜淑娟老师、钱俊彦老师、卢红敏老师、许蕾老师、陈林老师、张德平老师、周吴杰老师、查日军老师、吴军华老师等)、师兄师姐(刘园、周毓明、陈振强、张迎周、史亮、沈小丰等)、同学(汪鹏、李强、左赋斌、顾客、王玉宝、杜渐、曾奕、孙莉等)、和师弟师妹(崔志峰、解凯、谢二辂丹、余斌、杨彬、钱巨、曲波、章晓芳、吴重强、蒋翼翔、梁陈良、李亚军、闵洪波、何惠贞、董国伟、王子元、周天琳、徐峻岭等)对我的无私帮助;感谢计算机系资料室的教师和管理人员,他们为我的研究和实践工作提供了很多便利条件。论文的研究工作部分得到了国家杰出青年科学基金项目(60425206)、国家自然科学基金项目(60503033)、国防“九五”及“十五”重点预研项目、国防武器装备预研基金项目、江苏省自然科学基金项目(BK2006094)、江苏省高技术研究项目(BK2006094)、南京大学软件新技术国家重点实验室基金项目、武汉大学软件工程国家重点实验宝开放基金项目、江苏省计算机信息处理技术重点实验室开放基金项目(苏州大学)。非常感谢上述科研项目资助机构和校友或者企业奖学金的设立者或设立单位,没有他们的热心支持,我很难完成论文的研究和实践工作。感谢我的父母和我的女友等亲人,是他们给予我一贯的关爱、理解,是他们助我建立正确的人生观,是他们在我最困难的时候对我鼎力支持,助我摆脱困境,激发我的斗志,树立信心,全身心投入到学习、科研和工作中。感谢所有帮助过我、关心我的朋友们。7l 东南大学博士学位论文参考文献【l】StevensWP,MyersGJ,ConstantineL.Structureddesign.IBMSystemsJournal,1974,13(2):115-39.【2】PressmanRS,PressmanR.SoftwareEngineering:APractitioner"sApproach,FifthEdition[M].NewYork:McGraw-Hill,2001.【3】SullivanKJ,GriswoldWGCaiYThestructureandvalueofmodularityinsoftwaredesign[C].In:Proc.ofthe8thEuropeansoftwareengineeringconference(ESEC2001).NewYork:ACMPress,2001.99-108.[4】GoidbergA,RobsonD.Smalltalk-80:TheLanguageanditsImplementation[M].Massachusetts:AddisonWesley,1983.【5】FlanaganD,MatsumotoY.TheRubyProgrammingLanguage[M].Cambfidge:O’ReillyMedia,2008.【6】MendhekarA,KiczalesGLampingJ.RG:ACase-StudyforAspect-OrientedProgramming[TR].TRNo.SPL97-009P9710044.XeroxPARC,1997.【7】IrwinJ,LoingtierJM,GilbertJ心eta1.Aspect-OrientedProgrammingofSparseMatrixCode[C].In:Proc.ofInternationalScientificComputinginObject-OrientedParallelEnvironments(ISCOPEl997).Berlin:Springer-Verlang,1997.1-9.【8】LippertM,LopesCVAStudyonExceptionDetectionandHandlingUsingAspect-OrientedProgramming[TR].TRNo.P9910229.Xeroxf.ARC.·1999.【9】Kiczales13ILampingJ,MendhekarA,eta1.Aspect—OrientedProgramming[C].In:Proe.ofthe1lthEuropeanConferenceonObject-OrientedProgramming(ECOOP1997).JyV{iskyl蕴:Springer-Verlang,1997.220-242.【10】KiczalesGAspect—OrientedProgramming:TheFunHasJustBegun[C].InWorkshoponNewVisionsorSoftwareDesignandProductivity:ResearchandApplications,Nashville,Tenessee,December2001.【1l】EiradT,FiimanRE,BaderA.Aspect-OrientedProgramming[J].CommunicationsoftheACM,2001,44(10):79-82.【12】KiczalesGHilsdaleE,HuguninJ,eta1.AnOverviewofAspectJ[C].In:Proe.ofthe15thEuropeanConferenceonObject-OrientedProgramming(ECOOP2001).Budapest:Springer-Verlang,2001.327-355.[13】AspecOTeam.TheAspectJProgrammingGuide[EB/OL].http://www.eclipse.org/aspectj/doc/released/prog-guide/index.html.【14】ColyerA,ClementA,HarleyGeta1.EclipseAspectJ:Aspect-OrientedProgrammingwithAspectJandtheEclipseAspectJDevelopmentTools[M].NewYork:Addison-Wesley,2005.【15】LaddadR.AspectJinAction:PracticalAspect-OrientedProgramming[M].Greenwich:ManningPublications,2003.【16】AspectWerkzTeam.AspectWerkz—PlainJavaAOP-.Overview[EB/OL].http://aspectwerkz.codehaus.ore,/.[17】Bon6rJ,AspectWerkz-dynamicAOPforJava.In:Proe.ofthe3rdinternationalconferenceonAspect—orientedsoftwaredevelopment(AOSD2004).NewYork:ACMPress。2004.51“2.【18】AspecOTeam,AspectWerkzTeam.AspeeOandAspectWerkztoJoinForces[EB/OL].http://dev.eclipse.org/viewcvs/indextech.cgi/aspectj·home/aj5announee.html.【19】KhanK.AnIntroductiontoAspect—OrientedprogrammingwithJBossAOP[J/OL].http://java.dzone.com/ne—ws/an—introduction—aspect-oriente.【20】JBossTeam.JBossAOP-Aspect—OrientedFrameworkforJava[EB/OL].http://docsjboss.org/aop/1.3/aspect-framework/reference/en/html_single/index.html.【21】GhagGImplementcrosscuttingconcernsusingSpring2.0AOP[J/OL].http://www.javaworld.corn/java-world/jW一01-20070w-0105-aop.html. 东南大学博士学位论文【2Z】Johnson&HoellerJ,ArendsenA.TheSpringFramework.-ReferenceDocumentation[EB/OL].http://static.spdng仔amework,org/spring/docs/2.5.x/reference/index.html.[23】HilsdaleE,HuguninJ.AdviceWeavinginAspectJ[C].In:Proe.ofthe3rdinternationalconferenceonAspect-orientedsoftwaredevelopment(AOSD2004)..NewYork:ACMPress,2004.26·.35.[24】MasuharaH,KiczalesG,DutchynC.CompilationSemanticsofAspect-.OrientedPrograms[C].In:Proe.ofthe1stAOSDWorkshoponFoundationsofAspect-OrientedLanguages(FOAL2002),.NewYork:ACMPress,.2002.17--25.【"25】DeanJ,GroveD,ChambersC.OptimizationofObject-OrientedProgramsUsingStaticClassHierarchyAnalysis[C].In:Proe.ofthe9thEuropeanconferenceonObject-OrientedProgramming(ECOOPl995).Aarhus:Springer-Verlag,1995.77.-101.【26】FernandezMF.SimpleandEffectiveLink-TimeOptimizationofModula-3Programs[C].In:Proe,.oftheACMSIGPLAN1995conferenceonProgramminglanguagedesignandimplementation(PLDI1995),.NewYork:ACMPress,1995.103-115.【27】BaconDF,SweeneyPF.FaststaticanalysisofC++virtualfunctioncalls[C].In:Proe.ofthellthACMSIGPLANconfe3renceonObject-orientedprogramming,systems,languages,andapplications(IOOPSLA1996).NewYork:ACMPress,,1996.324—341.【"2K】币pF,PalsbergJ.ScalablePropagation.-BasedCallGraphConstructionAlgorithms[C].In:Proe.ofthe15thACMSIGPLANconferenceonObject-orientedprogramming,systems,languages,andapplications(OOPSLA2000).NewYork:ACMPress,2000..281—293.【29】SundaresanVRazafimahefaC,Vallte-RaiR.PracticalVirtualMethodCallResolutionforJava[C].In:Proc.ofthe15thACMSIGPLANconferenceonObject-.orientedprogramming,systems,languages,andapplications(OOPSLA2000).NewYork:ACMPress,,2000.264.-280.【30】Shiverso.Control·-FlowAnalysisofHiigher-OrderLanguagesorTamingLambda[D]:【PhDthesis].Pittsburgh:SchoolofComputerScience,Carnegie,·MellonUniversity,1991.【31】ShiversO.ControlFlowAnalysisinScheme[C].In:Proc.oftheACMSIGPLAN1988conferenceonProgrammingLanguagedesignandImplementation(PLDI1988).NewYork:ACMPress,,1988.164—174.【32】EmamiM,GhiyaR,HendrenLJ.Context-sensitiveinterproceduralpoints.-toanalysisinthepresenceoffunctionpointers[C].In:Proc.oftheSIGPLAN1994conferenceonProgrammingLanguageDesignandImplementation(PLDII994).NewYork:ACMPress,,1994.242-256.【33】Landiw’RyderBG’ZhangS.Interproceduralmodificationsideeffectanalysiswithpointeraliasing[C].In:Proe.oftheSIGPLAN1993conferenceonProgrammingLanguageDesignandImplementation(PLDI1993).NewYork:ACMPress,1993.56.-67.【34】ChoiJD,BurkeM,CariniP.EfficientFlow—SensitiveInterproceduralComputationofPointer-InducedAliasesandSideEffects[C].In:Proe.ofthe20thACMSIGPLAN-SIGACTsymposiumonPrinciplesofprogramminglanguages(POPLl993).NewYork:ACMPress.,1993.232-245.【351‘WilsonR只LamMS.Efficientcontext.-sensitivepointeranalysisforCprograms[C].In:Proe.oftheSIGPLAN1995conferenceonProgrammingLanguageDesignandImplementation(PLDI1995).NewYork:ACMPress..1995.1-12.["36】MichaelHind,MichaelBurke.,PaulCarini,andJong-DeokChoi.Interproceduralpointeraliasanalysis[J].ACMTransactionsonProgrammingLanguagesandSystems(TOPLAS),1999,2l(4):848一-894.【37】"SteensgaardB.Points·.toanalysisinalmostlineartime[C].In:Proe.ofthe23rdACMSIGPLAN-SIGACTsymposiumonPrinciplesofprogramminglanguages(POPLl996).NewYork:ACMPress,1996.32.-41.【38】DasM.Unification.-basedpointeranalysiswilthdirectionalassignments[C].In:Proc.oftheSIGPLAN2000conferenceonProgrammingLanguageDesignandImplementation(PLDl2000).NewYork:ACMPress.,2000.35.46.【39】DasM,LiblitB,FaehndrichM,RehofJ,.Estimatingtheimpactofscalablepointeranalysison73 东南大学博士学位论文optimization[C].InProc.ofthe8thInternationalStaticAnalysisSymposium.London:Springer-Verlag,2001.260.278.【40]I_,a/tnerC,LenharthA,Advev.MakingContext-sensitivePoints-toAnalysiswithHeapCloningPracticalForTheRealWorld[C].In:Proe.oftheACMSIGPLAN2007conferenceonProgrammingLanguageDesignandImplementation(PLDl2007).NewYork:ACMPress,2007.278—289.【4l】AndersenLO.ProgramAnalysisandSpecializationfortheCProgrammingLanguage[D]:[PhDthesis].Denmark:DIKU,UniversityofCopenhagen,1994.【42】FaehndrichM,FosterJS,SuZ,eta1.Partialonlinecycleeliminationininclusionconstraintgraphs[C].In:Prae.oftheACMSIGPLAN1998conferenceonProgramminglanguagedesignandimplementation(PLDll998).NewYork:ACMPress,1998.85-96.[43】FaehndrichM,RehofJ,DasM.Scalablecontext—sensitiveflowanalysisusinginstantiationconstraints[C].In:Proe.oftheACMSIGPLAN2000conferenceonProgrammingLanguageDesignandImplementation(PLDl2000).NewYork:ACMPress,2000.253-263.【44】FaehndrichM,RehofJ,AikenA.Polymorphicversusmonomorphicflow—insensitivepoints-toanalysisforcIc].In:Proc.ofthe7thInternationalStaticAnalysisSymposium.London:Springer-Verlag,2000.175-198.[45】HeintzeN,TardieuO.Ultra-fastaliasinganalysisusingCLA:AmillionlinesofCcodeinasecond[C].In:Pixie.oftheACMSIGPLAN2001conferenceonProgrammingLanguageDesignandImplementation(PLDl2001).NewYork:ACMPress,2001.254—263.【46】PeareeDJ,KellyP,HankinC.Onlinecycledetectionanddifferencepropagationforpointeranalysis[C].In:Proe.ofthe3rdInternationalIEEEWorkshoponSourceCodeAnalysisandManipulation(SCAM2003).WashingtonDC:IEEEComputerSociety,2003.3—12.【47】PeareeD,Kelly只HankinC.Efficientfield—sensitivepointeranalysisforC[C】.InACM.SIGPLAN-SIGSOFTWorkshoponProgramAnalysisforSoftwareToolsandEngineering(PASTE2004).NewYork:ACMPress,2004.37-42.【48】WhaleyJ,LamMS.Anefficientinclusion—basedpoints—toanalysisforstrictly-typedlanguages[C].In:Proe.oflhe9thInternationalStaticAnalysisSymposium.London:Springer-Verlag,2002.180—195.[49】HardekopfB,LinC.TheAntandtheGrasshopper:FastandAccuratePointerAnalysisforMillionsofLinesofCode[C].In:Proe.oftheACMSIGPLAN2007conferenceonProgrammingLanguageDesignandImplementation(PLDl2007).NewYork:ACMPress,2007.290-299.【50】SridharanM,GopanD,ShanL.Demand—drivenpoints-toanalysisforJava[C].In:Proc.ofthe20thannualACMSIGPLANconferenceonObjectorientedprogramming,systems,languages,andapplications(OOPSLA2005).NewYork:ACMPress,2005.59·76.【51】BemdlM,LhotfikO,QianF"eta1.PointstoAnalysisusingBDDs[C].In:Proc.oftheACMSIGPLAN2003conferenceonProgrammingLanguageDesignandImplementation(PLDl2003).NewYork:ACMPress,2003.103-114.f52】LhotfikO,HendrenL.ScalingJavapoints—toanalysisusingSpark[C].In:Proc.ofthe12thIntemationalConferenceonCompilerConstruction(CC2003).NewYork:Springer-Verlag,2003.153-169.【53】LhotzikO,CurialS,AmaralJN.UsingZBDDsinPoints-toAnalysis[C].In:Proc.ofthe20thIntemationalWorkshoponLanguagesandCompilersforParallelComputing(LCPC2007).NewYork:Springer-Verlag,2007.338.352.【54】WhaleyJ,S.LamM.Cloning-basedcontext-sensitivepointeraliasanalysis[C].In:Proc.oftheACMS1GPLAN2004conferenceonProgrammingLanguageDesignandImplementation(PLDl2004).NewYork:ACMPress,2004.13l-144.[55】ZhuJ.SymbolicPointerAnalysis[C].In:Proe.ofthe2002IEEE/ACMinternationalconferenceonComputer-aideddesign(ICCAD2002).NewYork:ACMPress,2002.150—157.【56】ZhuJ,CaimanS.SymbolicPointerAnalysisRevisited[C].In:Proc.oftheACMSIGPLAN2004conference74 东南大学博士学位论文onProgrammingLanguageDesignandImplementation(PLDl2004).NewYork:ACMPress,2004.145-157.[571ZhuJ,CaimanS.ContextSensitiveSymbolicPointerAnalysis[J].IEEETransactiononCADofIntegratedCircuitsandSystems,2005,24(4):5l“531.【58】BryantRE.GraphBasedAlgorithmsforBooleanFunctionManipulation[J].IEEETransactiononComputers(TOC),1986,35(8):677旬1.[59】HindM.PointerAnalysis:Haven’tWeSolvedThisProblemYet?[C】In:ACMSIGPLAN—SIGSOFTWorkshoponProgramAnalysisforSoRwareToolsandEngineering(PASTE2001).NewYork:ACMPress,2001.54-61.【60】HindM,PioliA.WhichPointerAnalysisShouldIUse?[C】In:Proe.ofthe2000ACMSIGSOFTinternationalsymposiumonSoftwaretestingandanalysis.NewYork:ACMPress,2000.113-123.【61】ChakaravarthyVT.NewResultsontheComputabilityandComplexityofPoints-toAnalysis[C].In:Proe.ofthe30thACMSIGPLAN—SIGACTsymposiumonPrinciplesofprogramminglanguages(POPL2003).NewYork:ACMPress.2003.115-125.【62】RyderBt3.DimensionsofPrecisioninReferenceAnalysisofObject—orientedProgrammingLanguages[C].In:Proc.ofthe2007internationalsymposiumonSoftwaretestingandanalysis.NewYork:ACMPress,2007.118—128.【63】Avgustinov只ChristensenAS,HendrenL’eta1.OptimisingAspectJ[C].In:Proc.oftheACMSIGPLAN2005conferenceonProgrammingLanguageDesignandImplementation(PLDl2005).NewYork:ACMPress,2004.117一128.【64】HayashidaR,1wamotoM,TokumonA.CallGraphConstructionforAspect—OrientedPrograms[TR].TRNo.570.FukuokaInstituteofTechnology,2005.【65】TakashiI,ShinjiK,KatsuroI.DebuggingSupportforAspect-OrientedProgramBasedonProgramSlicingandCallGraph[C].In:Proc.ofthe20thIEEEInternationalConferenceonSoftwareMaintenance(ICSM2004).Washington,DC:IEEEComputerSociety,2004.178-187.【66】李楠,赵建军,沈备军等.面向方面程序的调用图生成算法【J】.计算机应用与软件,2008,25(6):107.109.[67】ZhangS,GuZ,LinYeta1.Celadon:AChangeImpactAnalysisToolforAspect-OrientedPrograms[C].In:Companionofthe30thinternationalconferenceonSoftwareengineering(ICSECompanion2008).New‘York:ACMPress.2008.913-914.【68】MasuharaH,KiczalesGDutchynC.CompilationSemanticsofAspect·OrientedPrograms[TR].TR#02—06,IowaStateUniversity,2002..【69】WandM,KiczalesG,DutchynC.Asemanticsforadviceanddynamicjoinpointsinaspect—orientedprogramming[J].ACMTransactionsOnProgrammingLanguagesandSystems(TOPLAS),2004,26(5):890-910.【70】SereniD,deMoorO.Staticanalysisofaspects[C].In:Proc.ofthe2ndinternationalconferenceonAspect-orientedsoftwaredevelopment(AOSD2003).NewYork:ACMPress.2003.30—39.【711CookSA.Thecomplexityoftheorem-provingprocedures[C].In:Proe.ofthe3rdAnnualACMSymposiumOnTheoryofComputing.NewYork:ACMPress,1971.151.158.【72】TafertshoferRGanzA,HenfilingM.ASAT-basedimplicationengineforefficientATPGequivalencechecking,andoptimizationofnetlists[C].In:Proe.ofthe1997IEEE/ACMinternationalconferenceonComputer-aideddesign(ICCADl997).WashingtonDC:IEEEComputerSociety,1997.648-655.f73】Tafertshofer只GanzA.SATbasedATPGusingfastjustificationandpropagationintheimplicationgraph[C]。In:Proe.ofthe1999lEEE/ACMinternationalconferenceonComputer-aideddesign(ICCAD1999).WashingtonDC:IEEEComputerSociety,1999.139-146.【74】GuptaA,YangZ,Ashar只eta1.SAT-basedImageComputationwithApplicationinReachabilityAnalysis[C].In:Proe.ofthe3rdInternationalConferenceonFormalMethodsinComputer-AidedDesign.London:Spfinger-Verlag,2000.354—371.【75】Fagin&HalpemJ,MosesYeta1.Reasoningaboutknowledge[M].Cambridge:MITPress,1995。75 东南大学博士学位论文【76】DavisM,LogemannGLovelandD.Amachineprogramfortheoremproving[J].CommunicationsoftheACM,1962,5(7):394-397.【77】BallLCookB,LahiriSK.Zapato:Automatictheoremprovingforpredicateabstractionrefinement[C].InProc.ofthe16thInternationalConferenceonComputerAddedVerificatoin(CAV2004).London:Spfinger-Verlag,2004.457-461.【78】BiereA,CimaRiA,ClarkeEM.SymbolicModelCheckingwithoutBDDs[CJ.In:Proe.ofthe5thInternationalConferenceonToolsandAlgorithmsforConstructionandAnalysisofSystems.London:Springe卜Verlag,l999.193-207.【79】McMillanKL.ApplyingSATmethodsinUnboundedSymbolicModelChecking[C].In:Proc.ofthe14thInternationalConferenceonComputerAidedVerification(CAV2002).London:Springer-Ver|ag,2002.250-264.【80】ClarkeEM,KroeningD,SharyginaN.PredicateAbstractionofANSI-CProgramsusingSAT[J].FormalMethodsinSystemDesign,2004,25(2-3):105—127.【81】ClarkeEM,KroeningD,SharyginaN.SAT-BasedPredicateAbstractionofPrograms[TR].No.CMU/SEI一2005·TR-006,SoftwareEngineeringInstitute,Carnegie·MellonUniversity,2005.【82】XieYAikenA.ScalableErrorDetectionusingBooleanSatisfiability[C】.In:Proc.ofthe32ndACMSIGPLAN—SIGACTsymposiumonPrinciplesofprogramminglanguages(POPL2005).NewYork:ACMpress,2005.351-363.【83】XieYAikenA.Saturn:AScalableFrameworkforErrorDetectionusingBooleanSatisfiability阴.ACMTransactionsonProgrammingLanguagesandSystems(TOPLAS),2007,29(3).[84】DennisGChangSH,JacksonD,ModularverificationofcodewithSAT[C].In:Proc.ofthe2006InternationalSymposiumonSoftwareTestingandAnalysis(ISSTA2006).NewYork:ACMpress,2006.109-U9.【85】DavisM,PutnamH.AComputingProcedureforQuantificationTheory[J].JournaloftheAssociationforComputingMachinery(JACM),1960,7(3):201-215.【86】ZhangL,MalikS.Thequestforefficientbooleansatisfiabilitysolver[C].In:Proc.ofthe18thInternationalConferenceonAutomatedDeduction(CADE2002).London:Springer-Verlag,2002.295—313.[87】CrawfordJ,AutonL.Experimentalresultsonthecross-overpointinsatisfiabilityproblems[C].InProe.ofthell廿lNationalConferenceonAmericanAssociationofArtificialIntelligence(AAAIl993).Cambridge:AAAIPress,1993.21—27.[88】SelmanB,KautzH,CohenB.Localsearchstrategiesforsatisfiabilitytesting[J].DIMACSSeriesinDiscreteMathematicsandTheoreticalComputerScience,1996(35)。521.532.【89】GuJ,PurdomP,FrancoJ,eta1.AlgorithmsforSatisfiabilityproblem:aSurvey[J].DIMACSSeriesinDiscreteMathematicsandTheoreticalComputerScience,1996(35),19.152.[90】Marques—SilvaJ只SakallahKA.GRASP:ASearchAlgorithmforPropositionalSatisfiability[J].IEEETransactionsonComputers,1999,48(5):506—521.‘【91】MoskewiczM,MadiganC,ZhaoY,eta1.Chaff:Engineeringanefficientsatsolver[C].In:Proc.of38thDesignAutomationConference(DAC2001).NewYork:ACMPress,2001.530.535.【92】FuZ.MahajanYMalikS.NewFeaturesoftheSAT"04versionsofzChafif[J].SATCompetition2004-SolverDescription,2004.[93】SelmanB,LevesqueH,MitchellD.GSAT:anewmethodforsolvinghardsatisfiabilityproblems[C].In:Proe.oftheNationalConferenceonAmericanAssociationofArtificialIntelligence(AAAll992).SanJose:AAAIPress,1992.440—446.【94]GoldbergE,NovikovY.BerkMin:afastandrobustsat—solver[C]。In:Proc.oftheconferenceonDesign,automationandtestinEurope(DATE2002).Amsterdam:ElsevierScience,2002.142-149.【95】ZhangH.SATO:Anefficientpropositionalprover[C].In:Proc.ofthe14thInternationalConferenceon76 东南大学博士学位论文AutomatedDeduction(CADEl997).London:Springer-Verlag,1997.272—275.【96】GroveD,DeFouwGDeanJ,eta1.CallGraphConstructioninObject-OrientedLanguages[C],InProc.ofthe12thannualACMSIGPLANconferenceonObjectOrientedProgrammingSystem,LanguagesandApplication(OOPSLAl997).NewYork:ACMpress,1997.108~124.【97】GroveD,ChambersC.AFrameworkforCallGraphConstructionAlgorithms[J].ACMTransactionsonProgrammingLanguagesandSystems(TOPLAS),2001,23(6),685-746.【98】SethiR。ProgrammingLanguages,Concepts&Constructs,secondedition[M].NewYork:Adison-Wesley,1997.【99】LoudenKC.ProgrammingLanguages—PrinciplesandPractice,secondedition[M].Philadelphia:ThomsonPress,2002.【100】ShidrM,PnuelliA.TwoApproachestoInterproceduralDataFlowAnalysis[J].ProgramFlowAnalysis:TheoryandApplications.EnglewoodC“舔:Prentice-Hall,1981,189—234.【101】RosenBK,WegmanMN,ZadeckFK.GlobalValueNumbersandRedundantComputations[C].In:Proc.ofthel5thACMSIGPLAN-SIGACTsymposiumonPrinciplesofprogramminglanguages(POPLl988).NewYork:ACMpress,1988.12—27.[102】MarkN。Wegman,F.KennethZadeck.Constantpropagationwithconditionalbranches[J]。ACMTransactionsonProgrammingLanguagesandSystems(TOPLAS),1991,13(2):181-210.【103】AlpernB,WegmanMN,ZadeckFK.Detectingequalityofvaluesinprograms[C].In:Proc.ofthe15thACMSIGPLAN-SIGACTsymposiumonPrinciplesofprogramminglanguages(POPLl988).NewYork:ACMpress,1988.1—11.【104】KnobeK,SarkarVConditionalConstantPropagationofScalarandArrayReferencesUsingArraySSAF0m.【1051LLVMteam.TheLLVMCompilerInfrastructure[EB/OL].http://llvm.org/.【l06】OReteam.OpenResearchCompilerforltaniumProcessorFamily[EB/OL].http://ipf-orc.sourceforge.net/.【107]Wikipedia.Staticsingleassignmentform[EB/OL].http:Hen.wikipedia.org/wiki/Static_single_.assignment_form#Compilers_using_SSA_form.【108】AllenFE.Controlflowanalysis[J].ACMSIGPLANNotice,1970,5(7):l一19.【109】AhoAVSethiR,UlimanJD.Compilers:Principles,Techniques,andTools[M].NewYork:AddisonWesley,1986.【l10】CytronRFerranteJ,RosenBK.AnEfficientMethodofComputingStaticSingleAssignmentForm[C].In:Proe.ofthe16thACMSIGPLAN—SIGACTsymposiumonPrinciplesofprogramminglanguages(POPLI989).NewYork:ACMpress,1989.25-35.【1ll】CytronKFerranteJ,RosenBK.EfficientlyComputingStaticSingleAssignmentFormandtheControlDependenceGraph[J].ACMTransactionsonProgrammingLanguagesandSystems(TOPLAS),1991,13(4):451-490.【l12】JamesGosling,BillJoy,GuySteele.TheJavaLanguageSpecification,ThirdEdition[M].NewYork:AddisonWesley,2005.[113】D"AnjouJ,ShavorS,FairbrotherS,etal。TheJavaDeveloper"sGuidetoEclipse[M]。NewYork:AddisonWesley,2004.【114】Eclipseteam.JDTPlug—inDeveloperGuide[EB/OL].http://help.eclipse.org/help32/index.jsp?topic=/org.eelipse.jdt.doc.isv/reference/api/org/eclipse/jdt/core/dom/package-summary.html.【l15】EbnenasirA.Astand-aloneapplicationforconvertingSATDIMACSformulastoCNF[EB/OL].http://www.cs.mtu.edu/-aebnenas/research/tools/sat2cnf.htm.[116】DIMACS.SatisfiabilitySuggestedFormat[EB/OL].http://www.cs.ubc.ca/~babic/doc/dimacs_.cnf,pdf.[117】MarloweLLandiWRyderB,eta1.Pointer-inducedaliasing:Aclarification[J].SIGPLANNotices,1993,28(9):67,70. 东南大学博士学位论文【I18】BurkeM,Carini只ChoiJD,eta1.Interproceduralpointeraliasanalysis[TR].No.RC21055.IBMT.J.WatsonResearchCenter,1997.【119】NielsenF"NielsenHR’HankinC.PrinciplesofProgramAnalysis[M].Berlin:Springer-Verlag,2005.【120】TarjanRE.Solvingpathproblemsondirectedgraphs[TR].No.CS-TR-75·528,ComputerScienceDepartment,StanfordUniversity,1975.【121】TarjanRE.Fastalgorithmsforsolvingpathproblems[J].JournaloftheACM,1981,28(3):594—614.【122】ZhouX,XuB,ShiL,ChenL.Expresscalculationdecompositionwithextendedaspect-orientedprogramminglanguage[J].JournalofElectronics&ComputerScience,2005,7(1):89—99.【123】QianJ,XuB,MingH.Interstatementmustaliasesfordatadependenceanalysisofheaplocations[C].In:Proc.oftheWorkshoponProgramAnalysisforSoftwareToolsandEngineering(PASTE2007).NewYork:ACMPress.2007.17-24.78 东南大学博士学位论文附录一攻读博士学位期间完成的论文列表【1】曹璨,徐宝文,周晓宇,钱巨,杨彬.基于面向方面调用图的AspectJ动态通知编织优化.软件学报,2008.19(9):2218-2227.【2】曹瑕,徐宝文.基于非严格平行继承模式的安全元类程序设计.全国第五次程序设计语言发展与教学学术会议,南京.2006.10.【3】曹壕,徐宝文.基于SAT求解的面向对象程序类型分析.计算机科学,已录用.[4】JingCao,BaowenXu.Shrek:DynamicObject-OrientedProgrammingLanguage.JournalofSoutheastUniversity(Englishedition),Accepted.【5】陈林,徐宝文,周晓宇,曹瑕.一种基于类型约束的泛型Java程序重构方法.全国软件及应用学术会议。西安,2007.9. 东南大学博士学位论文附录二攻读博士学位期间参加的科研项目列表(1)嵌入式软件测试支撑系统ETS(该项目获得2004年度教育部提名国家科学技术进步二等奖)。(2)江苏省自然科学基金面上项I;1(BK2006094),软件设计模式的形式化描述及程序代码识别技术研究。(3)国家自然科学基金重点项目(60633010),高可信软件的测试与评估。