- 4.48 MB
- 2022-06-17 14:58:31 发布
- 1、本文档共5页,可阅读全部内容。
- 2、本文档内容版权归属内容提供方,所产生的收益全部归内容提供方所有。如果您对本文有版权争议,可选择认领,认领后既往收益都归您。
- 3、本文档由用户上传,本站不保证质量和数量令人满意,可能有诸多瑕疵,付费之前,请仔细先通过免费阅读内容等途径辨别内容交易风险。如存在严重挂羊头卖狗肉之情形,可联系本站下载客服投诉处理。
- 文档侵权举报电话: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)是一个三元组