Shape analysis through predicate abstraction and model check(10)

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.