Shape analysis through predicate abstraction and model check(9)

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

4APredicateCalculatorforShapeAnalysis

Wehaveimplementedaprototypepredicateabstractorforshapeanalysis,basedonthesetofpredicatesdiscussedabove,inOCaml.Theinputtothistoolconsistsofa ow-chartprogramwithC-styleinstructionsandvariabletypesincludingallbasictypesaswellasstructandpointertypes.Nestedstructs,unions,andarraytypesarenotcurrentlyacceptedbythetoolbuttheirinclusionposesnotechnicaldi culties.Thetooldoesnotyethandleprocedurecalls.Alongwiththeprogram,asetofpredicate-locationpairsisgiven,ase.g.extractedfromthepropertytobechecked.Theseserveasthestartingpointforthewpcalculations.Finally,aniterationboundanda(possiblyempty)collectionofapproximationhintsaregivenasinput.

Thetool’smainchallengeisinsimplifyingthe“raw”formulasthatareob-tainedaswp’s.Thesemaybelargeduetocasedistinctionsforaliasing.Byrewritingnewlygeneratedpredicatestosimplerones,semanticalequivalencewithalready-computedpredicatescanoftenbedetected.Thisreducestheover-allnumberofgeneratedpredicates,whichisessentialinapracticalapplicationofthealgorithm.Also,itrendersthepredicatesmorereadable,whichfacili-tatestheidenti cationofgoodapproximations.Wehaveimplementedavarietyofrulesthataimtosimplifyindividualpredicateslikereachandtheirargu-ments,andpointer(in)equalities.Forexample,reach[A;F](null,e)rewritestofalseregardlessofA,F,ande;inreach[A;F](e1,e2),e2canberemovedfromtheavoidsetA;and&(x→n)=&yistruewhenyisavariable.Anotheressentialclassofrewriterulesisformedbytypereasoning,furtherdiscussedbe-low.Furthermore,weapplyseveralstandardrules,includingtheDavis-Putnam-Logemann-Lovelandprocedure[11],tosimplifybooleanexpressions.ThetoolincludesautomaticconversionofabstractprogramstoS/RorPromelaformat,theresp.inputformalismsforthemodelcheckersCOSPANandSPIN.Thecor-rectnesspropertytobeveri edcanbeaddedtotheabstractprogrambyusingassertionsortemporallogic.

4.1TypeReasoning

SupposethatxandyareprogramvariablesoftheListtypefromourexam-ples.Atypicalpredicatethatmayoccurduringthemanipulationofwp’sisreach[A;n](x,&y).Regardlessoftheavoidset,thispredicateisfalse,ascanbeseenbyreasoningabouttypes,asfollows.VariablexitselfisoftypeList.Bydereferencingx,wegetanobjectofstruct-typeNode,inwhichselectionofthen eldyieldsaListagain.SotheonlytypesthatarereachablefromListareListandNode.Thetypeof&yhoweverispointertoList.So&ycannotbereachablefromx.

Reachabilitybetweentypesisformalizedbyapredicatetypreach.ForasetFof eldnames,typreach[F](t1,t2)expressesthatfromanobjectofaddresstypet1itispossibletoreachanobjectofaddresstypet2ifonlyselectionof eldsfromFisallowed.Itispossibletoprovethekeycorrectnesspropertythatifreach[A;F](e1,e2),thentypreach[F](t1,t2)foranyaddressexpressionse1