Shape analysis through predicate abstraction and model check(11)

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