外公是棵樱桃树读后感-成全一棵树读后感

CompactlyRepresentingFirst-OrderStructuresforStaticAnalysisR.Manevich1,⋆,G.Ramalingam2,J.Field2,D.Goyal2,andM.Sagiv11TelAvivUniversity{rumster,msagiv}@post.tau.ac.il2IBMT.J.WatsonResearchCenter{rama,jfield,dgoyal}@watson.ibm.comAbstract.Afundamentalbottleneckinapplyingsophisticatedstaticanalysestolargeprogramsisthespaceconsumedbyabstractprogramstates.Thisispartic-ularlytruewhenanalyzingprogramsthatmakeextensiveuseofheap-allocateddata.TheTVLA(Three-ValuedLogicAnalysis)programanalysisandverifica-tionsystemmodelsdynamicallocationpreciselybyrepresentingprogramstatesasfirst-orderstructures.Insucharepresentation,afinitecollectionofpredicatesisusedtodefinestates;thepredicatesrangeoverauniverseofindividualsthatmayevolve—expandandcontract—duringanalysis.Evolvingfirst-orderstruc-turescanbeusedtoencodeawidevarietyofanalyses,includingmostanalyseswhoseabstractstatesarerepresentedbydirectedgraphsormaps.Thispaperad-dressestheproblemofspaceconsumptioninsuchanalysesbydescribingandevaluatingtwonovelstructurerepresentationtechniques.Onetechniqueusesor-deredbinarydecisiondiagrams(OBDDs);theotherusesavariantofafunctionalmapdatastructure.Usingasuiteofbenchmarkanalysisproblems,wesystemati-callycomparethenewrepresentationswithTVLA’sexistingstaterepresentation.TheresultsshowthatboththeOBDDandfunctionalimplementationsreducespaceconsumptioninTVLAbyafactorof4to10relativetothecurrentTVLAstaterepresentation,withoutcompromisinganalysistime.InadditiontoTVLA,webelievethatourresultsareapplicabletomanyprogramanalysissystemsthatrepresentstatesasgraphs,maps,orotherstructuresofsimilarcomplexity.1OverviewandMainResultsAfundamentalbottleneckinapplyingsophisticatedstaticanalysestolargeprogramsisthespaceconsumedduringanalysisbyabstractprogramstates.Thisisparticularlytrueformodernprogramswheremuchofthedatamanipulatedbytheapplicationliesintheheap(i.e.,indynamicallyallocateddatastructures),insteadofbeingstoredinafixedsetofvariables.Anabstractionofthepotentiallyunboundedheapthatispreciseenoughforaparticularanalysismayoftenhaveprohibitivespacerequirements.TheTVLA(Three-ValuedLogicAnalysis)programanalysisandverificationsystem[6]isdesignedtomodeldynamicallocationpreciselybyrepresentingprogramstatesasfirst-orderstructures.Insucharepresentation,afinitecollectionofpredicatesisusedtodefinestates;thepredicatesrangeoverauniverseofindividualsthatmayevolve—expandandcontract—duringanalysis.Theuseoffirst-orderstructurespermits,e.g.,⋆PartiallysupportedbytheIsraeliAcademyofScience.PartofthisworkwasdonewhilevisitingIBM’sT.J.WatsonResearchCenter.dynamicmemoryallocationordynamicthreadcreationtobemodeledinanaturalway[13,17].Inaddition,first-orderstaterepresentationscanbemuchmorecompactthanrepresentationsbasedonfinite-statemodels.Forexample,whenrepresentingprogramswithpointers,anaturalfinitestaterepresentationofpointeraliasesusuallyconsumesquadraticspace[14],whereasagraphbased(first-order)representationsuchtheoneusedbyTVLAcanbelinearinmanycases.TVLAhasbeensuccessfullyappliedtoawidevarietyofdeepprogramanalysisandverificationproblems,includingcheckingCprogramsforthepresenceofmemoryleaksanddanglingoruninitializedpointers[4],verifyingthecorrectnessofasimplegarbagecollector[12],determiningwhetherclientsofaJavalibrarysatisfythelibrary’sconformanceconstraintsforcorrectusage[11],andverifyingcertainsafetypropertiesofapacketrouter[10].Incarryingoutthesetasks,TVLAutilizesanabstractinterpretationthatmaintainsdetailedinformationonthestateofdynamicallyallocatedmemory.Whilethisdegreeofprecisioniscrucialtoavoidreportinganexcessivenumberof“falsealarms”,itcomesataprice:thespacerequiredtoanalyzeprogramsofmorethanafewthousandlinesofcodeisoftenprohibitive.Thispaperaddressestheproblemofspaceconsumptioninfirst-orderstaterepresen-tationsbydescribingandevaluatingtwonewstructurerepresentationtechniques.Thefirstrepresentationusesanexistingorderedbinarydecisiondiagram[2,18](OBDD)implementation[15]toencodefirst-orderstructures.Thesecondstaterepresentationcombinesideasfromefficientimplementationsoffunctionalmaps(whereamapderivedbyupdatetoanothermapsharessubstructuresoftheinitialmap)withnormalizationviahash-consing.Bothofthesecoredatastructuresarewell-known,andOBDDshavebeenusedinseveralprogramanalysissystemstorepresentautomataorfinitesets.However,itisnotobviousthattheyshouldbeadaptableto,orbeneficialfor,representingevolvingfirst-orderstructures,especiallygiventheirpoorworst-casebehavior.Happily,ourevaluationofthenewstaterepresentationsindicatesthattheycanre-duceTVLA’sspaceconsumptionbyafactorof4to10withoutcompromisingtimeperformance.Inaddition,asthenumberofstructuresmanipulatedbytheanalysisin-creases,therelativeadvantageofthenewrepresentationsalsoincreases.Sincethenotionofevolvingfirst-orderstructureispowerfulenoughtoencodeanumberofnontrivialstaterepresentations(e.g.,thosebasedondirectedgraphsormaps),webelievethatourresultsarealsolikelytobeapplicableinawidevarietyofprogramanalysistechniquesrequiringsuchstructures.2TVLAPrimerInthissection,wegiveabriefoverviewofthoseaspectsoftheTVLAsystemthatpertaintostatemanipulation.Completed