Shape analysis through predicate abstraction and model check(5)

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.