A generic framework for interprocedural analysis o

AGenericFrameworkforInterproceduralAnalysisofNumericalPropertiesMarkusM¨uller-Olm1andHelmutSeidl21Universit¨atDortmund,FachbereichInformatik,LS5BaroperStr.301,44221Dortmund,[e-mail]2TUM¨unchen,Institutf¨urInformatik,I280333M¨unchen,[e-mail][5],Grangerpresentsananalysiswhichinferslin-earcongruencerelationsbetweenintegervariables.Forafneprogramswithoutguards,hisanalysisiscomplete,i.e.,infersallsuchcongruences.Nouppercom-plexitybound,though,hasbeenfoundforGranger'salgorithm.Here,wepresentavariationofthisanalysiswhichrunsinpolynomialtime.Moreover,weprovideaninterproceduralextensionofthisalgorithm.Thesealgorithmsareobtainedbymeansofmultipleinstancesofageneralframeworkforconstructinginterproce-duralanalysesofnumericalproperties.Finally,weindicatehowtheanalysescanbeenhancedtodealwithequalityguardsinterprocedurally.1IntroductionInrecentyears,agrowinginterestinthedesignofverypreciseanalysesofnumericalpropertiesofprogramscouldbeobserved.Ontheonehand,thiscomesfromarevivedinterestinaggressiveprogramoptimizationsasdemandedbylow-costembeddedpro-cessors.Ontheotherhandwhendesigningandimplementingcriticalapplications,wearefacedwithaneedforcertifyingabsenceofcertainprogramerrors[2,11]orsecurityvulnerabilitiessuchasbuffer-overows[3,15].Here,weconcentrateonequality-basednumericalproperties.Suchpropertiesareparticularlyuseful,e.g.,forinductionvariabledetectionoridenticationofdataalign-ments[1].ThistypeofanalysishasbeenpioneeredbyKarrin[9]wherehepresentsarstintraproceduralanalysisofvalidafnerelationsoveraeld.Karr'sanalysismain-tainsforeveryprogrampointavectorspaceofvalidafnerelations.Fifteenyearslater,hisanalysiswasgeneralizedbyGranger[4,5].SinceGrangerusesZinsteadofQ,hisintraproceduralanalysisnotonlyreturnsvalidafnerelationsbutalsovalidafnecon-gruencerelations—withthedraw-back,perhaps,thatnouppercomplexityboundisknown.Granger'sanalysisalsodiffersfromKarr'sinthatGrangerrstdeterminesalinear(infactafne)abstractionofthesetsofintraprocedurallyreachablestatesfromwhichthesetofvalidrelationsthenisderivedinasecondstep.Aforwardaccumu-lationoftheabstractedcollectingsemanticsisalsousedbyM¨uller-OlmandSeidlin[12]where(inabsenceofequalityguards)therun-timeofKarr'sanalysisalgorithmisimprovedandalsothesizesofoccurringnumbersisbounded.ThesameauthorsalsoprovidetherstpreciseinterproceduralextensionofKarr'sanalysis[13]andshowhowitcanbeadaptedtoworknotonlyovereldsbutalsoovermodularringsZmwherem=2wasusedbystandardprogramminglanguageslikeJava[14].In[6,7],GulwaniandNeculare-considerKarr'sanalysisproblem.Inordertoimproveonthecomplexityoftheanalysis,theyproposerandomization.Inparticular,sizesofoccurringnumbersareboundedbycomputingmodulorandomprimes.Inthispaper,wepresentgeneralmethodshowintraproceduralanalysesofnumericalpropertiescanbeconstructedwhichnaturallyextendtointerproceduralanalysesofthesameproperties.Ourframeworkisparametricintheringwithinwhichthecomputationoftheanalysisisperformed.ForthecaseofafnerelationsovereldsormodularringsZm(mapowerof2),wesubsumeversionsoftheintra-andinterproceduralanalysesfrom[12,13]and[14],respectively.Beyondtheseknownanalyses,wesucceedinderivinganinterproceduralextensionofGranger'sanalysis[5]thatdeterminesnotonlyallvalidafnerelationsbutalsoallvalidcongruencerelations.Wealsoindicatehowtheanalysescanbeenhancedtodealwithequalityguardsinterprocedurally.TheimmediateinterproceduralextensionofGranger'sanalysisasprovidedbythegeneralframeworkshareswithGranger'soriginalalgorithmthedraw-backofperform-ingxpointiterationsovercompletelatticeswithunbounded(thoughnite)ascendingchains.Inordertoimproveonthis,weproposeanewalgorithmwhich,inabsenceofprocedures,runsinpolynomialtime.ThenewalgorithmisbasedonacarefulinspectionofGranger'sanalysisproblemwhichallowsustodividetheanalysisintooneanalysisovertheeldQtogetherwithseveralanalysesovercarefullychosenmodularrings.Thepaperisorganizedasfollows.Insection2weintroduceafneprogramsto-getherwiththeircollectingsemantics.Insection3weintroduce,foreveryringR,theR-linearabstractionandshowhowitcanbeusedtodeterminevalidR-linearrelationsandalso(incaseofR=Z)validlinearcongruencerelations.Insection4,wethenshowforeveryprincipalidealringRthattheR-linearabstractionofthecollectingsemanticscanbecomputedpreciselyandprovidecomplexityboundsforeldsandmodularringsZm.Insection5,weparticularlydealwiththecaseR=Zandprovideanalternativealgorithmwhich(atleastinabsenceofequalityguards)determinesallintraprocedu-rallyvalidlinearcongruencerelationsinpolynomialtime.Intheinterproceduralcase,thenewalgorithmispolynomialifthelengthofintermediatelyoccurringnumbersispolynomiallybounded.Insection6,wenallyextendtheproposedapproachtotakeequalityguardsintoaccount.Finally,section7summarizesandgiveshintsondirec-tionsoffutureresearch.2TheGeneralSet-upWeusesimilarconventionsasin[13]and[14]whichwerecallhereforreasonsofselfcontainedness.Thus,programsaremodeledbysystemsofnon-deterministicowgraphsthatcanrecursivelycalleachotherasinFigure1.LetX=fx1;::