Shape analysis through predicate abstraction and model check(4)

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

[17];however,several(semi-)algorithmsexist[26,6,3,22].Weuseamodi edformofthealgorithmfrom[26].Thisalgorithmsimultaneouslyderivesasetofrelevantpredicatesandcomputestheabstractactions,throughaniteratedweakestpreconditioncalculation.

Theoriginalalgorithmoperatesonprogramsmodeledbyasetofactionsde nedasguardedcommands.Asequentialprocedurebodycanbeeasilytrans-latedtothisnotationbyusingavariable,say“pc”,torepresentthecontrollocation.Withthisencoding,however,theschemein[26]examineseveryactionateachiteration,resultinginseveralunnecessarycalculations.Thus,weencodethecontroltransitionintheactionnameitself,andtailorthealgorithmtoonlyinspectrelevantactions.Acontrol owedgefromlocationmtonlabeledwithguardgandupdateaisturnedintotheactionsm,n:g→a(notethataisdeterministic).Foranupdates:g→a,wp(s,p)≡g∧wp(a,p)1.Theothermajordi erenceisthatweallowforuserguidanceoftheabstractionintheformofabstractionhints.

Ourmodi edalgorithmispresentedinFigure3.Thealgorithmiterativelycomputesasetofpairs(p,n),wherepisapredicateandnisacontrollocation.Thepair(p,n)assertsthatpredicatepholdsatlocationn.Thedatastructuresusedareasetofpairs,S,andasetofnewlygeneratedpairs,N.Theparameterstothealgorithmare:(a)acorrectnessproperty,writteninauniversaltempo-rallogicsuchasLTLorACTL ,(b)aniterationboundk,and(c)asetofapproximationhints.

Inthemainloop(step2),thealgorithmprocessesunmarkedpairsinabreadth- rstmanner.Foreachunmarkedpair(p,n),andeveryactionsm,n,thealgorithmcomputeswp(sm,n,p).Bythesemanticsofwp,thetruthofpredicatepatnodenafterexecutingstatementsm,nisgivenbythevalueofwp(sm,n,p)atnodem.This,inturn,isdeterminedbythevaluesofitsconstituentpredicatesatnodem.Thesepredicatesareextracted,andprocessedinthenextiteration.Fromtheundecidabilityresult,therecanbenoterminationguaranteeingeneral,soauser-suppliedboundkisusedtolimitthenumberofiterations.Theap-proximationhintsareusedtointroducenewpredicatesthatmayacceleratetheterminationoftheloop–anexampleisprovidedinSection5.Everypredicatepgeneratedduringthealgorithmhasacorrespondingbooleanvariable,calledbp.Thesubstitutionofpredicatesinaformulafwiththeircorrespondingbooleansresultsinaformula–asageneralrule,werepresenttheabstractversionofaconcreteobjectoby.Simpli cationisusedinstep2toreducethenumberofnewlygeneratedpairsforfastertermination:correctnessdoesnotdependonthepower,butonlyonthesoundnessofthesimpli er.

Wenowexaminesomeotherissuesthatariseinapplyingthisalgorithm.Aninitialcondition,init,canbeencodedbyintroducinganewtransitionsn0,n1:init→skip,betweenanewinitiallocation(n0)andtheoldone(n1).Anabstrac-tioncomputedwithouthintscanbeusedonlytoprovepropertiesthatdependsolelyonpredicatesgeneratedbytheiteratedwpcalculations.Whilethismay1Thisre ectsthesemanticsthatanactionisexecutedatastateonlyifitsguardholdsatthatstate.