Shape analysis through predicate abstraction and model check(2)

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

arerepresentedwithbooleanvariables:theprocessisaninstanceofpredicateabstraction[14].Thecorrectnessoftheabstractinterpretationisguaranteedbythealgorithm.Anadvantageisthatnon-shapepredicates(suchasarithmeticin-equalities),whichimprovetheprecisionofabstraction,areincludedinastraight-forwardmanner.Oneofthemaincontributionsofthispaperisthecalculationofweakestpreconditionsforsecond-ordershapepredicateslikereachability,theidenti cationofotherpredicatesthatariseinthisprocess,andthecalculationoftheirwp’s.WehaveimplementedaweakestpreconditioncalculatorforshapepredicatesrelativetoC-likeprogramconstructs,includingheuristicstoacceler-ateconvergence.

Theabstractprogramcomputedbythisalgorithmisanalyzedwithagenericmodelchecker.Thisenablesonetotapintoawealthoftechniquesandhighlyoptimizedimplementationsforstatespaceexploration.Furthermore,onecancheckfortemporalpropertiesthatgobeyondinvariances.Ourcalculatorgener-atestheabstractedprograminformatsthatareacceptedbytheexplicitstatemodelcheckerSPIN[18]andtheBDD-basedmodelcheckerCOSPAN[16].Wedemonstrateourapproachona“classical”listreversalprogram.Adetailedde-scriptionoftheexperiments,includinginputandresult les,canbefoundat[32].typedefstructnode

{structnode*n;intdata;}Node;

typedefNode*List;

Listinsert(Listx,inta)

{

Listt;

n1:t=(List)malloc(sizeof(Node));

n2:t->data=a;

n3:t->n=x;

n4:x=t;

ne:returnx;

}n1:{reach[;n](x,k),false}t=(List)malloc(sizeof(Node));n2:{reach[&(t->n);n](x,k),(t==k)}t->data=a;n3:{reach[&(t->n);n](x,k)\/(t==k)}t->n=x;n4:{reach[;n](t,k)}x=t;ne:{reach[;n](x,k)}returnx;

Fig.1.Listinsertionprocedure(left)andwpcalculations(right)

OverviewWeintroduceourframeworkthroughtheanalysisofaCprogramforinsertinganelementattheheadofalist,showninFigure1.Weareinter-estedincheckingthepropertythattheinsertionprocessdoesnot,inadvertently,makeoneoftheexistinglistmembersunreachablefromx.De nethepredicatereach[A;F](i,j)@ltobetrueofthoseprogramstateswherecontrolisatlocationland,intheheap,itispossibletoreachaddressjfromaddressi,followingonlythose eldsinFandavoidingalladdressesinsetA.Wewritereach[;F](i,j)ifAisempty,andwhenF={n}itiswrittenasn.Theabovepropertycanthenbeexpressedformallybythelineartemporallogicformula( k:G(reach[;n](x,k)@n1 G(true@ne reach[;n](x,k)@ne))).