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.