Shape analysis through predicate abstraction and model check(12)

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

satis abilityquestionsoverpredicateformulae,andthuswemightbene therefromworkondecidablelogicstoreasonaboutheapsorarrays[4,19,21,31].ModelcheckingNext,weinstructthetooltoproducethecorrespondingab-stractedlistreversalprograminbothS/RandPromelaformats,andusetheCOSPANandSPINmodelcheckerstoindependentlyverifytheoriginalcyclic-ityproperty.Inbothcases,thecheckingisdoneintheorderofhundredthsofasecond,withinminimalamountsofmemory(0.1MBwithSPINandlesswithCOSPAN4).ThePromelaversionhas34reachablestates,each48bytesinsize.FortheS/Rversion,32statesarereached5andtheconstructedBDD’shave2454nodes.Bothveri cationscon rmthatthepropertyholds.Removingthepreconditionthatxisacyclicresultsinfailure,showingthatitisnecessary.Incaseofthelist-insertionexamplefromtheIntroduction,thetoolconvergesafter4iterationswithouttheneedforanyapproximations.Sointhiscasetheabstractionisfullyautomatic.TheresultingS/RandPromelamodelshave12and7reachablestatesresp.,andveri cationisagaindoneinafractionofasecondwithminimalamountsofmemoryinbothcases.

6RelatedWorkandConclusions

Asynthesisandgeneralizationofseveralexistingalgorithmsforshapeanalysisispresentedin[29].Theiralgorithmconstructsashapegraphinvariant,expressedin3-valuedlogic,byanabstractinterpretationofprogramactions.Theinvariantisbasedontwocorepredicates:x(v)(thenodeforvariablex)andn(v1,v2)(alinkfromv1tov2via eldn).Toimproveprecision,user-suppliedinstrumenta-tionpredicateshavetobeused,includingshapepredicatesandalsonon-shapepredicatessuchas≤.Precisioncanalsobeimprovedbyafocusoperationthatturnsunde nedvaluesintonon-determinism,orbymaterializingnewelements(e.g.,todistinguishbetweenreachabilityin0,1,ormoresteps).Acoerceopera-tioneliminatesinconsistentpartsofaninvariant.Theimplementation(TVLA)

[24]includesabluroperation,whichweakensaninvariant.

Althoughtheexactrelationshipbetweenouralgorithmsis—asyet—unclear,somegeneralcommentscanbemade.First,theabstractioncomputedbyoural-gorithmcanbeusedtoconstructshapegraphinvariants—thisisdoneimplicitlybythemodelcheckingprocedure—butalsotochecknon-invarianceproperties.Secondly,operationssimilartofocus,coerce,andblur,allofwhichhavetodowiththeprecisionofthereachabilitycomputation,areimplementedinmodelcheckers.Determininghowwellthesegenerictechniquesworkfortheparticularproblemofshapeanalysisisanintriguingquestionforfutureworkbut,intheexampleswehaveconsidered,themodelcheckingwasnotanissue.

Oneofthechiefdi erencesisthebackward,goal-directednatureofourab-stractionmethod,andthecorrespondinglackofdistinctionbetweencoreandinstrumentationpredicates.Infact,theiteratedwpcalculations,startingwith4

5SPINalwaysseemstotakeatleast0.1MBduetooverheadorabuilt-inlowerbound.Thedi erenceinthenumberofreachablestatesisduetodi erentwaysofmodeling.