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
1.Initially,Scontainsallpairsfromthecorrectnessproperty,togetherwith(q,m),foreachpredicateqthatoccursintheguardofsomeactionsm,n:g→a.Initially,theabstractactionsarede nedasm,n:→skip.AllpairsinSareunmarked,andNisempty.
2.Ateachiteration,aslongasthereisanunmarkedpairinS,andtheiterationboundkisnotreached,dothefollowing.
(a)Foreachunmarkedpair(p,n),markitasexamined,and:
i.ifthereisanapproximationhintmapping(p,n)toanexpressionh,thenaddtheequivalencebp≡atnodenandinsert{(q,n)|q∈pred(h)}
intoN.
ii.else,consideractionsm,n:g→a,foreachm,and:
putewp(sm,n,p),andsimplifyittoobtainaformulaf.
B.foreachqinpred(f),add(q,m)tothesetN.
C.addbp:=totheupdateofabstractactionm,n.
(b)AddallpairsinNtoS.
3.Afterstep2hasterminated,over-approximatethebooleanscorrespondingtoanyunmarkedpredicates,usingeitheranapproximationhint,ornon-determinism({false,true}),or .
Fig.3.Thepredicateabstractionalgorithm
besu cientinsomecases(e.g.,listinsertion)itisnecessary,ingeneral,tousehints.Theapproximationhintforp@ncanbeanyexpressionhthatis“moreabstract”thanp.Thisisformalizedasp 3h,where 3isthe“abstractionorder”relationof3-valuedlogic2.Forinstance,(x>3)maybeapproximatedbyif(x≤0)thenfalseelse .
Thealgorithmalwayscomputesaconservativeapproximationtothesourceprogram,whereaprogramstate(s,n)isrelatedtoanabstractstate(s ,n )if,andonlyif,thecontrollocationsn,n areidentical,andforeverypredicatepsuchthatthepair(p,n)isconsideredduringabstraction,p(s) 3bp(s ).Thisalgorithmisalsocompleteinthesenseshownin[26,2].
Asstated,thisalgorithmisintra-procedural.Itcanbeextendedtohandleprocedurecallsbytheprocessdescribedin[1].Forexample,wp(x:=F(y),p(x))canbecalculatedbydeterminingwp(body(F),p(r))(y),whereristhereturnvalueofthebodyofF.ThisintroducesadditionalpredicateswithinthebodyofF.ThecalltoFisthenreplacedbyacalltotheabstractversionofF,i.e.,bp:=({bq|q∈pred(wp(body(F),p(r)))}).
3WeakestPreconditionsforShapeAnalysis
Toutilizetheaboveabstractionalgorithmforshapeanalysis,weneedtocal-culateweakestpreconditionsforcommonshapepropertiessuchasreachability,cyclicity,andsharing.Thede nitionsoftheseproperties,andtheirweakestpreconditioncalculations,arebothbasedonamemorymodel.
2x 3xforallx,andx 3 ,forallx. and{false,true}areidenti edforthispurpose.