Shape analysis through predicate abstraction and model check(3)

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