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))).