Abstract. We propose a new framework, based on predicate abstraction and model checking, for shape analysis of programs. Shape analysis is used to statically collect information — such as possible reachability and sharing — about program stores. Rather t
ShapeAnalysisthroughPredicateAbstraction
andModelChecking
DennisDamsandKedarS.Namjoshi
BellLabs,LucentTechnologies,600MountainAve.,MurrayHill,NJ07974.
{dennis,kedar}@
Abstract.Weproposeanewframework,basedonpredicateabstrac-tionandmodelchecking,forshapeanalysisofprograms.Shapeanalysisisusedtostaticallycollectinformation—suchaspossiblereachabil-ityandsharing—aboutprogramstores.Ratherthanuseaspecializedabstractinterpretationbasedonshapegraphs,weinstantiateagenericandautomatedabstractionprocedurewithshapepredicatesfromacor-rectnessproperty.Thisresultsinapredicate-discoveryprocedurethatidenti espredicatesrelevantforcorrectness,usingananalysisbasedonweakestpreconditions,andcreatesa nitestateabstractprogram.Thecorrectnesspropertyisthencheckedontheabstractionwithamodelcheckingtool.Toenablethisprocess,wecalculateweakestpreconditionsforcommonshapeproperties,andpresentheuristicsforacceleratingcon-vergence.
Exploringabstractstatespaceswithmodelcheckersenablesonetotapintoawealthoftechniquesandhighlyoptimizedimplementationsforstatespaceexploration,andtoanalyzepropertiesthatgobeyondinvari-ances.Weillustratethissimpleand exibleframeworkwiththeanalysisofsome“classical”listmanipulationprograms,usingourimplementa-tionoftheabstractionalgorithm,andtheSPINandCOSPANmodelcheckersforstatespaceexploration.
1Introduction
Shapeanalysisisusedtostaticallydetermineglobalpropertiesoftheprogramheap.Examplesofsuchpropertiesare“points-to”reachabilitybetweenobjects,theexistenceofcycles,orsharingwithintheheap.Typically,suchanalysesarebasedonabstractinterpretations[7]ofheapswithvariouskindsofshapegraphs.Thispaperpresentsanewframeworkforshapeanalysis,whichisbasedonSchmidtandSte en’sobservationthatstaticanalysisismodelcheckingofanabstractinterpretation[30].Theexploitationofthisparadigmrendersourframeworkdi erentinseveralkeyways.
Amajordi erenceisthewayinwhichabstractinterpretationisperformed.Weuseagenericabstractionalgorithmtocalculateanabstractionofthepro-gram,relativetoagivenshapeproperty.Startingwiththeshapepredicatesintheproperty,thealgorithmiteratively,andinagoal-directedmanner,discoversotherpredicatesthatarerelevanttotheproperty,bycomputingweakestpre-conditions(wp)[12].Italsoconstructsanabstractionwherethesepredicates