Shape analysis through predicate abstraction and model checking

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

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

arerepresentedwithbooleanvariables:theprocessisaninstanceofpredicateabstraction[14].Thecorrectnessoftheabstractinterpretationisguaranteedbythealgorithm.Anadvantageisthatnon-shapepredicates(suchasarithmeticin-equalities),whichimprovetheprecisionofabstraction,areincludedinastraight-forwardmanner.Oneofthemaincontributionsofthispaperisthecalculationofweakestpreconditionsforsecond-ordershapepredicateslikereachability,theidenti cationofotherpredicatesthatariseinthisprocess,andthecalculationoftheirwp’s.WehaveimplementedaweakestpreconditioncalculatorforshapepredicatesrelativetoC-likeprogramconstructs,includingheuristicstoacceler-ateconvergence.

Theabstractprogramcomputedbythisalgorithmisanalyzedwithagenericmodelchecker.Thisenablesonetotapintoawealthoftechniquesandhighlyoptimizedimplementationsforstatespaceexploration.Furthermore,onecancheckfortemporalpropertiesthatgobeyondinvariances.Ourcalculatorgener-atestheabstractedprograminformatsthatareacceptedbytheexplicitstatemodelcheckerSPIN[18]andtheBDD-basedmodelcheckerCOSPAN[16].Wedemonstrateourapproachona“classical”listreversalprogram.Adetailedde-scriptionoftheexperiments,includinginputandresult les,canbefoundat[32].typedefstructnode

{structnode*n;intdata;}Node;

typedefNode*List;

Listinsert(Listx,inta)

{

Listt;

n1:t=(List)malloc(sizeof(Node));

n2:t->data=a;

n3:t->n=x;

n4:x=t;

ne:returnx;

}n1:{reach[;n](x,k),false}t=(List)malloc(sizeof(Node));n2:{reach[&(t->n);n](x,k),(t==k)}t->data=a;n3:{reach[&(t->n);n](x,k)\/(t==k)}t->n=x;n4:{reach[;n](t,k)}x=t;ne:{reach[;n](x,k)}returnx;

Fig.1.Listinsertionprocedure(left)andwpcalculations(right)

OverviewWeintroduceourframeworkthroughtheanalysisofaCprogramforinsertinganelementattheheadofalist,showninFigure1.Weareinter-estedincheckingthepropertythattheinsertionprocessdoesnot,inadvertently,makeoneoftheexistinglistmembersunreachablefromx.De nethepredicatereach[A;F](i,j)@ltobetrueofthoseprogramstateswherecontrolisatlocationland,intheheap,itispossibletoreachaddressjfromaddressi,followingonlythose eldsinFandavoidingalladdressesinsetA.Wewritereach[;F](i,j)ifAisempty,andwhenF={n}itiswrittenasn.Theabovepropertycanthenbeexpressedformallybythelineartemporallogicformula( k:G(reach[;n](x,k)@n1 G(true@ne reach[;n](x,k)@ne))).

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

Thepredicatereach[;n](x,k)holdsatnei itsweakestprecondition(wp)

[12]holdsatn4.Whileweakestpreconditionsforsimpleconstructscanbecom-putedbysyntacticsubstitution,thisisnottrueforsecondorderpredicateslikereachability.WeshowinSection3howtocomputewpforreachability:forthepresentdiscussion,itsu cestoknowthatthewpforthispredicatesimpli estotheexpectedvalue:reach[;n](t,k).Theabstractionalgorithm(Section2)com-puteswp’sforindividualpredicatesinthisgoal-directed,“backward”manneruntiltheinitiallocationn1isreached.Theresultsareshownenclosedin{...}inFigure1(right)withwp’sforpredicatesatn3separatedbyacommaatn2.Thekeypointtonoteishowthewpcalculationsidentifyfurtherpredicatesthatarerelevanttothecorrectnessproperty.

n1:

n2:

n3:

n4:

ne:b2b2b1b0:=:=:=:=b0,b3:=false;b2,b3:=b3;b2\/b3;b1;b0b1b2b3<-><-><-><->reach[;n](x,k)reach[;n](t,k)reach[&(t->n);n](x,k)(t==k)

Fig.2.Predicate-booleancorrespondence(left)andabstractprogram(right)Theabstractprogram,andthepredicate-booleancorrespondence,isshowninFigure2.Theabstractactionsarecalculatedbysubstitutingbooleanvariablesforpredicatesintheresultsofthewpcalculations.Forinstance,theupdateforb1onedgen3ton4isgivenbyb2∨b3,whichistheresultofsubstitutiononthewpforitscorrespondingpredicatereach[;n](t,k).Notethatbooleansareonlyguaranteedtohavecorrectvalueswhereitmatters—e.g.b1mayhavethe(clearlywrong)valuetrueatn2,butitissettoitscorrectvalueatlocationn3,justbeforeitisusedtocalculateb0.Theabstractionalgorithmensuresthispropertywhich,inturn,ensuresthecorrectnessoftheabstraction.

Theadjustedcorrectnesspropertyfortheabstractprogram,G(b0@n1 G(true@ne b0@ne))canbeestablishedusingamodelchecker.Forthisex-ample,thepropertycanbeestablisheddirectlyfromthewpcalculations;how-ever,thisisdi culttodofortheanalysisofprogramswithloops.Ingeneral,thewpcalculationsservetotransformtheprogramlocally,whilethemodelcheckingdeterminesglobalproperties.Astheabstractionisalwaysconservativeinnature,apropertythatholdsoftheabstractionalsoholdsofthesourceprogram.Hence,thesourceprogramisalsocorrect.

Thevariouscomponentsoftheframeworkaredescribedindetailinsubse-quentsections.

2AbstractionbyIteratedWeakestPreconditions

InPredicateAbstraction[14],theabstractprogramisde nedoverasetofbooleanvariableswhichrepresentsourceprogrampredicates.Determiningasetofpredicatesrelevanttoshowingacorrectnesspropertyisundecidableingeneral

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

[17];however,several(semi-)algorithmsexist[26,6,3,22].Weuseamodi edformofthealgorithmfrom[26].Thisalgorithmsimultaneouslyderivesasetofrelevantpredicatesandcomputestheabstractactions,throughaniteratedweakestpreconditioncalculation.

Theoriginalalgorithmoperatesonprogramsmodeledbyasetofactionsde nedasguardedcommands.Asequentialprocedurebodycanbeeasilytrans-latedtothisnotationbyusingavariable,say“pc”,torepresentthecontrollocation.Withthisencoding,however,theschemein[26]examineseveryactionateachiteration,resultinginseveralunnecessarycalculations.Thus,weencodethecontroltransitionintheactionnameitself,andtailorthealgorithmtoonlyinspectrelevantactions.Acontrol owedgefromlocationmtonlabeledwithguardgandupdateaisturnedintotheactionsm,n:g→a(notethataisdeterministic).Foranupdates:g→a,wp(s,p)≡g∧wp(a,p)1.Theothermajordi erenceisthatweallowforuserguidanceoftheabstractionintheformofabstractionhints.

Ourmodi edalgorithmispresentedinFigure3.Thealgorithmiterativelycomputesasetofpairs(p,n),wherepisapredicateandnisacontrollocation.Thepair(p,n)assertsthatpredicatepholdsatlocationn.Thedatastructuresusedareasetofpairs,S,andasetofnewlygeneratedpairs,N.Theparameterstothealgorithmare:(a)acorrectnessproperty,writteninauniversaltempo-rallogicsuchasLTLorACTL ,(b)aniterationboundk,and(c)asetofapproximationhints.

Inthemainloop(step2),thealgorithmprocessesunmarkedpairsinabreadth- rstmanner.Foreachunmarkedpair(p,n),andeveryactionsm,n,thealgorithmcomputeswp(sm,n,p).Bythesemanticsofwp,thetruthofpredicatepatnodenafterexecutingstatementsm,nisgivenbythevalueofwp(sm,n,p)atnodem.This,inturn,isdeterminedbythevaluesofitsconstituentpredicatesatnodem.Thesepredicatesareextracted,andprocessedinthenextiteration.Fromtheundecidabilityresult,therecanbenoterminationguaranteeingeneral,soauser-suppliedboundkisusedtolimitthenumberofiterations.Theap-proximationhintsareusedtointroducenewpredicatesthatmayacceleratetheterminationoftheloop–anexampleisprovidedinSection5.Everypredicatepgeneratedduringthealgorithmhasacorrespondingbooleanvariable,calledbp.Thesubstitutionofpredicatesinaformulafwiththeircorrespondingbooleansresultsinaformula–asageneralrule,werepresenttheabstractversionofaconcreteobjectoby.Simpli cationisusedinstep2toreducethenumberofnewlygeneratedpairsforfastertermination:correctnessdoesnotdependonthepower,butonlyonthesoundnessofthesimpli er.

Wenowexaminesomeotherissuesthatariseinapplyingthisalgorithm.Aninitialcondition,init,canbeencodedbyintroducinganewtransitionsn0,n1:init→skip,betweenanewinitiallocation(n0)andtheoldone(n1).Anabstrac-tioncomputedwithouthintscanbeusedonlytoprovepropertiesthatdependsolelyonpredicatesgeneratedbytheiteratedwpcalculations.Whilethismay1Thisre ectsthesemanticsthatanactionisexecutedatastateonlyifitsguardholdsatthatstate.

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

1.Initially,Scontainsallpairsfromthecorrectnessproperty,togetherwith(q,m),foreachpredicateqthatoccursintheguardofsomeactionsm,n:g→a.Initially,theabstractactionsarede nedasm,n:→skip.AllpairsinSareunmarked,andNisempty.

2.Ateachiteration,aslongasthereisanunmarkedpairinS,andtheiterationboundkisnotreached,dothefollowing.

(a)Foreachunmarkedpair(p,n),markitasexamined,and:

i.ifthereisanapproximationhintmapping(p,n)toanexpressionh,thenaddtheequivalencebp≡atnodenandinsert{(q,n)|q∈pred(h)}

intoN.

ii.else,consideractionsm,n:g→a,foreachm,and:

putewp(sm,n,p),andsimplifyittoobtainaformulaf.

B.foreachqinpred(f),add(q,m)tothesetN.

C.addbp:=totheupdateofabstractactionm,n.

(b)AddallpairsinNtoS.

3.Afterstep2hasterminated,over-approximatethebooleanscorrespondingtoanyunmarkedpredicates,usingeitheranapproximationhint,ornon-determinism({false,true}),or .

Fig.3.Thepredicateabstractionalgorithm

besu cientinsomecases(e.g.,listinsertion)itisnecessary,ingeneral,tousehints.Theapproximationhintforp@ncanbeanyexpressionhthatis“moreabstract”thanp.Thisisformalizedasp 3h,where 3isthe“abstractionorder”relationof3-valuedlogic2.Forinstance,(x>3)maybeapproximatedbyif(x≤0)thenfalseelse .

Thealgorithmalwayscomputesaconservativeapproximationtothesourceprogram,whereaprogramstate(s,n)isrelatedtoanabstractstate(s ,n )if,andonlyif,thecontrollocationsn,n areidentical,andforeverypredicatepsuchthatthepair(p,n)isconsideredduringabstraction,p(s) 3bp(s ).Thisalgorithmisalsocompleteinthesenseshownin[26,2].

Asstated,thisalgorithmisintra-procedural.Itcanbeextendedtohandleprocedurecallsbytheprocessdescribedin[1].Forexample,wp(x:=F(y),p(x))canbecalculatedbydeterminingwp(body(F),p(r))(y),whereristhereturnvalueofthebodyofF.ThisintroducesadditionalpredicateswithinthebodyofF.ThecalltoFisthenreplacedbyacalltotheabstractversionofF,i.e.,bp:=({bq|q∈pred(wp(body(F),p(r)))}).

3WeakestPreconditionsforShapeAnalysis

Toutilizetheaboveabstractionalgorithmforshapeanalysis,weneedtocal-culateweakestpreconditionsforcommonshapepropertiessuchasreachability,cyclicity,andsharing.Thede nitionsoftheseproperties,andtheirweakestpreconditioncalculations,arebothbasedonamemorymodel.

2x 3xforallx,andx 3 ,forallx. and{false,true}areidenti edforthispurpose.

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

3.1MemoryModel

HeapandstackcontentsaremodeledbyanunboundedarrayM,indexedbytheintegers,togetherwitha nitesubsetoftheintegers,calledalloc,whichrecordstheallocatedaddresses.Astructure eldname,suchasn,isrepresentedwithafunction,calledn ,whichmapstheaddressofthestructuretotheaddresswhere eldnis‘stored’–weassume eldnamesaregloballydistinct.AnexpressionehastwoattributesrelativetoM:itsaddress,denotedbyaddrM(e),anditsvalue,denotedbyvalM(e).Therulesforcalculatingtheseattributes,andtheinterpretationsofbasicprogramstatements,aregiveninFigure4.Intheserules,attributesarewrittenasapair(address,value),⊥representsanunde nedresult,andwehavesimpli edmattersbyhavingmallocallocateasinglememorylocation.

Programvariablex:(α(x),M[α(x)]),whereαmapsprogramvariablestoaddressesStructureaccesse.n:( n(addrM(e)),M[ n(addrM(e))])

Addressexpression&e:(⊥,addrM(e))

Dereference e:(valM(e),M[valM(e)]),ifvalM(e)∈alloc,elseerror

Numericconstantc:(⊥,c)

Arithmeticoperationop(e1,...,en):(⊥,op(valM(e1),...,valM(en)))

Pointeradditione+i:(⊥,valM(e)+i)

Guardg:valM(g)

Ordinaryassignmente1:=e2:M[addrM(e1)]:=valM(e2)

Memoryallocatione:=malloc:M[addrM(e)]:=a;alloc:=alloc∪{a},

forsomea∈alloc

Memoryde-allocationfree(e):alloc:=alloc\{valM(e)}

Fig.4.Thememorymodel

ThewpofapredicateprelativetoastatementsiscomputedbytranslatingbothpandsintermsofM,calculatingwpinthestandardwayforarrayupdates3

[15],andtranslatingtheresultbacktothesyntaxofprogramexpressions(seee.g.

[5]).Forexample,considerthepredicatep≡(x=0),foraprogramvariablex,andstatements: u:=10.TheassignmentisinterpretedasamemoryupdateresultinginM ≡M[valM(u)←10],andwp(s,p)isgivenby(valM(x )=0).DistributingM intovalresultsin(if(valM(u)=α(x))then10elsevalM(x))=0,whichsimpli esto(valM(u)=α(x))∧(valM(x)=0).Translatingbacktoprogramsyntaxgives(u=&x)∧(x=0)astheweakestprecondition.ThisprocessoftranslatingbackandforthfromMthuscorrectlytakesintoaccountaliasinge ects.Itistedioustocarryoutsuchcalculationsbyhand,buttheyareeasilyautomated,asdescribedinthefollowingsection.

3wp(M[a]:=v,p(M))isgivenbyp(M ),whereM [i]=M[i]fori=a,andM [a]=v,denotedbyM =M[a←v].DistributingM intopresultsinanexpressionintermsofM.

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

3.2WeakestPreconditionsforShapePredicates

Wehave,sofar,consideredwpcalculationsforsimplekindsofpredicates,albeittakingintoaccountcomplexaliasinge ects.Weareprimarilyinterestedinmoreglobal,second-ordershapeproperties.Thekeypropertyisreach[A;F](i,j,M).Informally,thissaysthatthereisasequenceofstepsinMfromaddressitoaddressj,whichavoidsalladdressesinA,andusesonlythe eldsinF.Wede nethispreciselybelowasaleast xpoint.Astepreferstoamemorydereference.Forexample,ifzisavariableoftypeNode(seeFigure1),thelocationwheretheaddressofthenextnodeisstoredisn (α(z))(thevalueof&(( z).n)).ButtheaddressofthenextelementitselfisgivenbyM[ n(α(z))],whichresultsfromamemorydereference.

ForasetFof eldnames,letF (w,y,A)holdi yisreachablefromwusingonly eldaccessesfromF(e.g.x.a.b.c),whileavoidingaddressesinA.Thisisde nedasfollows:

F (w,y,A)≡alloc(y)∧

(µZ,x:alloc(x)∧(x=y∨(¬A(x)∧( a:a∈F:Z( a(x))))))(w)Wecanthende nereachby

reach[A;F](w,b,M)≡

(µZ,x:alloc(x)∧( k:F (x,k,A):(k=b∨(¬A(k)∧Z(M[k])))))(w)NotetheexplicitdereferencingstepM[k]inthisde nition.

ThewpforreachiscalculatedforanupdateM =M[i←c]bysubstitutingM forMinthis xpointexpression,andsimplifyingtheresult.Fortheotherpredicates,whicharede nedintermsofreach,theirwp’sarecalculatedusingthewpforreach.Thede nitionsofthesepredicatesandtheirwp’sareshowninFigure5;theirderivationsareavailableat[32].Informally,thewpforreachabilitysaysthatitispossibletoreachbfromxafteranupdateM =M[i←c]providedthat,inthepreviousstate,either:(i)itispossibletoreachbfromxavoidingaddressesinA∪{i},or(ii)iisnotinA,andtherearepathsfromxtoi,andfromctobthatavoidA.Inthe rstcase,thememoryupdatedoesnotinvalidatethepathand,inthesecondcase,thememoryupdateservestolinktwopathsintothedesiredpathfromxtob.Theotherwpexpressionshavesimilarinformalreadings.

Aremarkablefeatureonemayobserveisakindofclosureproperty,inthatthewpforashapepredicateisexpressibleintermsofothershapepredicates—ofcourse,withdi erencesinthearguments.Closureensuresthatonlythesetypesofshapepredicatesariseduringtheiterationsoftheabstractionalgorithm,makingitpossibletospotpatternsthatindicatewhereapproximationisneeded.AnexampleofsuchapatternisgivenintheanalysisofalistreversalprograminSection5.

Weusepredicateswiththesamenamestostateprogramproperties:e.g.,reach[A;F](e1,e2),whereAisasetofprogramexpressions,ande1,e2arepro-gramexpressions.Thetranslationofthepredicateintothememorymodelas

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

reach[A;F](x,b,M):itispossibletoreachaddressbfromaddressxin0ormoresteps.Thewpisgivenby

reach[Ai;F](x,b,M)∨(¬A(i)∧reach[Ai;F](x,i,M)∧reach[Ai;F](c,b,M)) reachp[A;F](x,b,M):itispossibletoreachaddressbfromaddressxin1ormoresteps.Thisisde nedbyalloc(x)∧( k:F (x,k,A):¬A(k)∧reach[A;F](M(k),b,M)),withwp:

reachp[Ai;F](x,b,M)∨(reach[Ai;F](c,b,M)∧¬A(i)∧reach[Ai,F](x,i,M)) dshared[A;F](x,y,M):thereexistsanon-nullnodereachablefrombothxandy.Thisisde nedby( v:v=NULL:reach[A;F](x,v,M)∧reach[A;F](y,v,M)),withwp:

dshared[Ai;F](x,y,M)∨

(¬A(i)∧reach[Ai;F](x,i,M)∧dshared[Ai;F](y,c,M))∨

(¬A(i)∧reach[Ai;F](y,i,M)∧dshared[Ai;F](x,c,M))∨

(¬A(i)∧(c=NULL)∧reach[Ai;F](x,i,M)∧reach[Ai;F](y,i,M))

cyclic[A;F](x,M):xreachesanodethatisinvolvedinacycle.Thisisde nedby( v:reach[A;F](x,v,M)∧reachp[A;F](v,v,M)),withwp:

cyclic[Ai;F](x,M)∨

(¬A(i)∧reach[Ai;F](x,i,M)∧cyclic[Ai;F](c,M))∨

(¬A(i)∧reach[Ai;F](x,i,M)∧reach[Ai;F](c,i,M))

Fig.5.WeakestpreconditionsforshapepredicatesforM =M[i←c].Inthesefor-mulas,weuseAitorepresentA∪{i}

apreludetocomputingwpisgivenbyreach[valM(A);F](valM(e1),valM(e2),M).

Asanexample,intheprogramfromSection1,considerthepredicatereach[;n](x,k),andtheassignmentx:=t,wheretandxareoftypeList.Thetranslatedpredicateisgivenbyreach[;n](valM(x),valM(k),M),whiletheassignmentresultsinthememoryupdateM =M[α(x)←valM(t)].Sub-stitutingM forMgivesreach[;n](valM (x),valM (k),M )).Thissimpli es,usingthewpforreach,toreach[α(x);n](valM(t),valM(k),M)∨(true∧reach[;n](valM(t),α(x),M)∧reach[;n](valM(t),valM(k),M)).Fromthedef-thattcanneverreachtheaddressofx.Thus,theunderlinedtermsimpli estofalse,andtheresultis:reach[α(x);n](valM(t),valM(k),M).Theavoidingaddressα(x)issuper uousforthesamereason,soitcanberemoved,givingtheresult(inprogramsyntax)asreach[;n](t,k).

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

4APredicateCalculatorforShapeAnalysis

Wehaveimplementedaprototypepredicateabstractorforshapeanalysis,basedonthesetofpredicatesdiscussedabove,inOCaml.Theinputtothistoolconsistsofa ow-chartprogramwithC-styleinstructionsandvariabletypesincludingallbasictypesaswellasstructandpointertypes.Nestedstructs,unions,andarraytypesarenotcurrentlyacceptedbythetoolbuttheirinclusionposesnotechnicaldi culties.Thetooldoesnotyethandleprocedurecalls.Alongwiththeprogram,asetofpredicate-locationpairsisgiven,ase.g.extractedfromthepropertytobechecked.Theseserveasthestartingpointforthewpcalculations.Finally,aniterationboundanda(possiblyempty)collectionofapproximationhintsaregivenasinput.

Thetool’smainchallengeisinsimplifyingthe“raw”formulasthatareob-tainedaswp’s.Thesemaybelargeduetocasedistinctionsforaliasing.Byrewritingnewlygeneratedpredicatestosimplerones,semanticalequivalencewithalready-computedpredicatescanoftenbedetected.Thisreducestheover-allnumberofgeneratedpredicates,whichisessentialinapracticalapplicationofthealgorithm.Also,itrendersthepredicatesmorereadable,whichfacili-tatestheidenti cationofgoodapproximations.Wehaveimplementedavarietyofrulesthataimtosimplifyindividualpredicateslikereachandtheirargu-ments,andpointer(in)equalities.Forexample,reach[A;F](null,e)rewritestofalseregardlessofA,F,ande;inreach[A;F](e1,e2),e2canberemovedfromtheavoidsetA;and&(x→n)=&yistruewhenyisavariable.Anotheressentialclassofrewriterulesisformedbytypereasoning,furtherdiscussedbe-low.Furthermore,weapplyseveralstandardrules,includingtheDavis-Putnam-Logemann-Lovelandprocedure[11],tosimplifybooleanexpressions.ThetoolincludesautomaticconversionofabstractprogramstoS/RorPromelaformat,theresp.inputformalismsforthemodelcheckersCOSPANandSPIN.Thecor-rectnesspropertytobeveri edcanbeaddedtotheabstractprogrambyusingassertionsortemporallogic.

4.1TypeReasoning

SupposethatxandyareprogramvariablesoftheListtypefromourexam-ples.Atypicalpredicatethatmayoccurduringthemanipulationofwp’sisreach[A;n](x,&y).Regardlessoftheavoidset,thispredicateisfalse,ascanbeseenbyreasoningabouttypes,asfollows.VariablexitselfisoftypeList.Bydereferencingx,wegetanobjectofstruct-typeNode,inwhichselectionofthen eldyieldsaListagain.SotheonlytypesthatarereachablefromListareListandNode.Thetypeof&yhoweverispointertoList.So&ycannotbereachablefromx.

Reachabilitybetweentypesisformalizedbyapredicatetypreach.ForasetFof eldnames,typreach[F](t1,t2)expressesthatfromanobjectofaddresstypet1itispossibletoreachanobjectofaddresstypet2ifonlyselectionof eldsfromFisallowed.Itispossibletoprovethekeycorrectnesspropertythatifreach[A;F](e1,e2),thentypreach[F](t1,t2)foranyaddressexpressionse1

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

ande2withtypest1andt2resp.Thispropertyallowsthesimpli ertoreplaceapredicateoftheformreach[A;F](e1,e2)byfalseiftypreach[F](t1,t2)failstohold.(Otherwise,nothingisreplaced.)Typereasoningisalsousedtosimplifyequalities;e.g.(x==y)isfalseifthetypesofxandydi er.

5AnExample

Weillustrateourapproachonaprogramforin-placereversalofsingly-linkedlists,alsoconsideredine.g.[4,24,33,28,29].ThecoreoftheprogramisgiveninFigure6.

Listx,y,t;/*xisanacycliclist*/

n1:y=NULL;

n2:while(x!=NULL){

n3:t=y;

n4:y=x;

n5:x=x->n;

n6:y->n=NULL;

n7:y->n=t;};

n8:

Fig.6.Thelistreversalprogram

Initially,xisthelisttobereversed.Itistraversedheadtotail,reversingthenext-pointers(n)onebyone.Atthestartofeveryiterationofthewhileloop,xistherestofthelisttobereversedandyistheinitialsegmentthathasbeenreversedsofar.Variabletisauxiliary;atanypointduringthereversal,itpointstooneofthe ingshapeanalysis,wewanttoverifythatyisanacycliclistafterthereversal(usingthenegationofpredicatep1=cyclic[;n]y@n8),giventhepreconditionthatxisacyclic(p2=cyclic[;n]x@n1).

Werunourtoolon(the ow-chartdescriptionof)theprogramtogetherwithpredicatesp1andp2,butwithoutanyapproximation.Bychoosingarelativelylargeiterationbound,predicatesaregeneratedthatoccurinwp’sobtainedbypropagatingp1backwardsthroughthesequenceofstatementsofthewhileloopforaseveraliterations(p2,beingatn1,doesnotgenerateanynewpredicates).Bymanuallyinspectingthesepredicates,wecangetanideaoftheappropriateapproximationstobeapplied.Settingtheiterationboundto30,185predi-cate/locationpairsarecalculatedcorrespondingtoabout3backwarditerationsthroughthewhileloop.Allpredicatesareoftypecyclic,reach,orequality;theydi erintheirarguments.Thefollowingisanexcerptfromthetool’soutput,showingsomepredicatesrelevantatlocationn5.

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

n5:reach[(&(y->n),&(*(x).n->n));n](t,*(x).n)

n5:reach[(&(y->n),&(*(x).n->n),&(*(*(x).n).n->n));n](t,*(x).n)

n5:reach[(&(y->n),&(*(x).n->n),&(*(*(x).n).n->n));n](t,*(*(x).n).n)

Thedi erencebetweentheseinstantiationsofthereachpredicateisinthenum-berof“→ndereferences”ofx.Clearly,thepredicateswillkeepgrowingalongthispatternforeverynextiterationofwp’saroundthewhileloop,duetotheassignmentx=x→naftern5.Anapproximationthatweedsoutthisgrowthisfoundbyobservingthattheunionofallthesepredicatesimpliesthatfromt,anaddresscanbereachedthatcanalsobereachedbyfollowingkn- eldsstartingfrom (x).n,forsomek.Asimilarpropertycanbeexpressedbyasingledsharedpredicate—henceweusethatasanapproximation.Ifdshared[;n](t,x)isfalse,thensoiseveryofthepredicatesabove.Sowewilltrytocuto thegrowthpatternbyapproximatingthe rstofthosepredicates,reach[(&(y→n),&( (x).n→n));n](t, (x).n)atn5,by“if¬dshared[;n](t,x)thenfalseelse ”.

Thisistheonlypatternthatoccursinthelistofpredicates,andindeedseveralotherpredicatesatn5canbeapproximatedintermsofdshared[;n](t,x)aswell.Thepatternalsooccursinasequenceofequalitypredicates.Atn5theseequationsareintermsofyandx,anditisnotimmediatelyclearhowtoapproximatethem.Butifweconsiderthesamepatternatn4,wherethey’sgetreplacedbyx’sduetothewpovertheassignmenty=x,itshowsupasfollows.n4:(x==*(x).n)

n4:(x==*(*(x).n).n)

n4:(x==*(*(*(x).n).n).n)

Itisclearthatnoneofthepredicatescanbetrueunderthegivenpreconditionthatxisnotcyclic.Soherewebringinthepredicatecyclic[;n]xbyapproxi-matingx=( (x).n)by“if¬cyclic[;n]xthenfalseelse ”.

Havingadded5approximations,introducingthetwonewpredicatesmen-tionedabove,wererunthetool.Wechoosealargeriterationbound(40)sothatnotonlyallpointswillbereachedwheretheapproximationsapply,butalsothetwonewpredicatesintroducedbythemarepropagatedbackwardsfarenoughsothatanypatternsthattheythemselvesmaygeneratebecomeapparent.Thistime,thepattern(thesameasbefore:growing→n-dereferences)occursin3newpredicates.Oneofthemisadsharedpredicateandcanbeapproximated,atn5,intermsofthepredicatedshared[;n](t,x)fromabove.Theother2stemfromthepredicatecyclic[;n]xandcanbeapproximatedbythatsamepredicate,atn4.

Thethirdrunofthetool,althoughstartedwithiterationbound40again,convergesafter29iterationswiththemessagethatnopredicatesremaintobeexamined.Atotalnumberof33relevantpredicateshavebeenfoundatthatpoint,3ofwhicharesuggestedbytheapproximations,ofwhichthereare8altogether.Eachrunofthetooltakesabout1second.

Anotherwaytoidentifysuitablepredicatesforapproximationisthroughtheanalysisofcounter-examplesthatareproducedbythemodelcheckersincasethecurrentabstractionistoocoarse.Error-traceanalysisboilsdowntosolving

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.

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

predicatesfromtheproperty,naturallyidentifyotherrelevantpredicates,includ-ingalloftheneededinstrumentationpredicates.Ontheotherhand,theTVLAtoolanalyzesthelistreversalexamplefullyautomatically,incontrasttoouruseofuser-suppliedapproximationhints.However,webelievethatitispossibletoautomatetheheuristicswehaveusedforidentifyingapproximations,sothatprogramssuchasthisarehandledfullyautomatically.

In[25,27],wpforreachabilityiscalculated,butnoothershapepredicatesareconsidered.Predicateabstraction,combinedwithmodelchecking,hasbeenusedinanalysesofsomeheapproperties:points-toanalysis[1],correctnessofconcur-rentgarbagecollectors[10,9],andloopinvariants[13].Thesepapers,however,donothandleshapeproperties.

Inconclusion,webelievethattheseparationofconcernsbetweenabstractionandstatespaceexplorationthatisproposedinthenewframeworkopensupsev-eralpossibilities.Theabstractionmethodservestodiscoverthepredicatesthatarerelevantforprovingagivenproperty.Thewpcalculationsperformabstrac-tionlocally,leavingtheglobalstatespaceexplorationtoamodelchecker.Onecanthustakeadvantageofhighlyoptimizedmodelcheckingimplementations,andthewidevarietyoflogicsandsystemmodelstowhichtheyapply.Ourinitialexperiencehas,wehope,demonstratedthepromiseofthismethod,whilerais-ingseveralinterestingquestionsfortheoreticalinvestigationsandexperimentalimprovements.

Ourongoinge ortsarefocusedonmechanizingtheheuristicsforapprox-imations.Astheveri cationproblemforshapepropertiesisundecidable,wecannothopeforafullyautomatedprocedurethatworksonallinstances.How-ever,therehavebeensuccessfulattempts[23]toautomatesimilarapproximationheuristicsusingrecognitionofpatterngrowthin(regular)expressions,basedontheframeworkofwidening[7,8].Also,wecanpotentiallybene tfromthede-signoftheoremprovingtools,suchasACL2[20],whichsuccessfullyrecognizeinductionpatternsinmanycases.

References

1.T.Ball,R.Majumdar,T.D.Millstein,andS.K.Rajamani.AutomaticpredicateabstractionofCprograms.InPLDI,2001.

2.T.Ball,A.Podelski,andS.Rajamani.Relativecompletenessofabstractionre- nementforsoftwaremodelchecking.InTACAS,volume2280ofLNCS,2002.

3.T.BallandS.Rajamani.TheSLAMtoolkit.InCAV,volume2102ofLNCS,2001.

4.M.Benedikt,T.Reps,andM.Sagiv.Adecidablelogicfordescribinglinkeddatastructures.InESOP,volume1576ofLNCS,pages2–19,1999.

5.R.Bornat.ProvingpointerprogramsinHoarelogic.InMathematicsofProgramConstruction,volume1837ofLNCS,pages102–126,2000.

6.E.M.Clarke,O.Grumberg,S.Jha,Y.Lu,andH.Veith.Counterexample-guidedabstractionre nement.InCAV,volume1855ofLNCS,2000.

7.P.CousotandR.Cousot.Abstractinterpretation:Auni edlatticemodelforstaticanalysisofprogramsbyconstructionorapproximationof xpoints.InPOPL,pages238–252,1977.

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

paringtheGaloisconnectionandwiden-ing/narrowingapproachestoabstractinterpretation.InM.BruynoogheandM.Wirsing,editors,ProgrammingLanguageImplementationandLogicProgram-ming,volume631ofLNCS,pages269–295,1992.

9.S.DasandD.Dill.Successiveapproximationofabstracttransitionrelations.InLICS,2001.

10.S.Das,D.Dill,andS.Park.Experiencewithpredicateabstraction.InCAV,

volume1633ofLNCS,1999.

11.M.DavisandH.Putnam.Acomputingprocedureforquanti cationtheory.J.

putingMachinery,7:201–215,1960.

12.E.W.Dijkstra.Guardedcommands,nondeterminacy,andformalderivationof

programs.C.ACM,18,1975.

13.C.FlanaganandS.Qadeer.Predicateabstractionforsoftwareveri cation.In

POPL,2002.

14.S.GrafandH.Sa¨ di.ConstructionofabstractstategraphswithPVS.InCAV,

volume1254ofLNCS,1997.

15.D.Gries.TheScienceOfProgramming.Springer-Verlag,1981.

16.R.H.Hardin,Z.Har’el,andR.P.Kurshan.COSPAN.InCAV,volume1102of

LNCS,1996.

17.T.A.Henzinger,R.Jhala,R.Majumdar,zyabstraction.InPOPL,

2002.

18.G.Holzmann.TheSPINmodelchecker.IEEETransactionsonSoftwareEngi-

neering,23(5),May1997.

19.J.L.Jensen,M.E.Jørgensen,N.Klarlund,andM.I.Schwartzbach.Automatic

veri cationofpointerprogramsusingmonadicsecond-orderlogic.InSIGPLANConferenceonProgrammingLanguageDesignandImplementation,pages226–236,1997.

20.M.Kaufmann,P.Manolios,puter-AidedReasoning:AnAp-

proach.KluwerAcademicPublishers,2000.

21.N.KlarlundandM.I.Schwartzbach.Graphsanddecidabletransductionsbased

onedgeconstraints(extendedabstract).InColloquiumonTreesinAlgebraandProgramming,pages187–201,1994.

khnech,S.Bensalem,S.Berezin,andS.Owre.Incrementalveri cationby

abstraction.InTACAS,volume2031ofLNCS,2001.

23.D.Lesens,N.Halbwachs,andP.Raymond.Automaticveri cationofparameter-

izednetworksofprocesses.TheoreticalComputerScience,256:113–144,2001.

LA:Asystemforimplementingstaticanalyses.In

SAS,volume1824ofLNCS,2000.

25.J.Morris.(1)Ageneralaxiomofassignment(2)Assignmentandlinkeddata

structures.InM.BroyandG.Schmidt,editors,TheoreticalFoundationsofPro-grammingMethodology,1981.

26.K.S.NamjoshiandR.P.Kurshan.Syntacticprogramtransformationsforauto-

maticabstraction.InCAV,volume1855ofLNCS,2000.

27.G.Nelson.Verifyingreachabilityinvariantsoflinkedstructures.InPOPL,1983.

28.N.RinetzkyandS.Sagiv.Interproceduralshapeanalysisforrecursiveprograms.

InComputationalComplexity,pages133–149,2001.

29.M.Sagiv,T.Reps,andR.Wilhelm.Parametricshapeanalysisvia3-valuedlogic.

TOPLAS,24(3):217–298,2002.

30.D.A.SchmidtandB.Ste en.Programanalysisasmodelcheckingofabstract

interpretations.InSAS,volume1503ofLNCS,1998.

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

31.A.Stump,C.W.Barrett,D.L.Dill,andJ.R.Levitt.Adecisionprocedureforan

extensionaltheoryofarrays.InLICS,pages29–37,2001.

32./~kedar/shape.

33.E.Yahav.VerifyingsafetypropertiesofconcurrentJavaprogramsusing3-valued

logic.InPOPL,pages27–40,2001.

本文来源：https://www.bwwdw.com/article/m9km.html