Shape analysis through predicate abstraction and model check(6)

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

3.1MemoryModel

HeapandstackcontentsaremodeledbyanunboundedarrayM,indexedbytheintegers,togetherwitha nitesubsetoftheintegers,calledalloc,whichrecordstheallocatedaddresses.Astructure eldname,suchasn,isrepresentedwithafunction,calledn ,whichmapstheaddressofthestructuretotheaddresswhere eldnis‘stored’–weassume eldnamesaregloballydistinct.AnexpressionehastwoattributesrelativetoM:itsaddress,denotedbyaddrM(e),anditsvalue,denotedbyvalM(e).Therulesforcalculatingtheseattributes,andtheinterpretationsofbasicprogramstatements,aregiveninFigure4.Intheserules,attributesarewrittenasapair(address,value),⊥representsanunde nedresult,andwehavesimpli edmattersbyhavingmallocallocateasinglememorylocation.

Programvariablex:(α(x),M[α(x)]),whereαmapsprogramvariablestoaddressesStructureaccesse.n:( n(addrM(e)),M[ n(addrM(e))])

Addressexpression&e:(⊥,addrM(e))

Dereference e:(valM(e),M[valM(e)]),ifvalM(e)∈alloc,elseerror

Numericconstantc:(⊥,c)

Arithmeticoperationop(e1,...,en):(⊥,op(valM(e1),...,valM(en)))

Pointeradditione+i:(⊥,valM(e)+i)

Guardg:valM(g)

Ordinaryassignmente1:=e2:M[addrM(e1)]:=valM(e2)

Memoryallocatione:=malloc:M[addrM(e)]:=a;alloc:=alloc∪{a},

forsomea∈alloc

Memoryde-allocationfree(e):alloc:=alloc\{valM(e)}

Fig.4.Thememorymodel

ThewpofapredicateprelativetoastatementsiscomputedbytranslatingbothpandsintermsofM,calculatingwpinthestandardwayforarrayupdates3

[15],andtranslatingtheresultbacktothesyntaxofprogramexpressions(seee.g.

[5]).Forexample,considerthepredicatep≡(x=0),foraprogramvariablex,andstatements: u:=10.TheassignmentisinterpretedasamemoryupdateresultinginM ≡M[valM(u)←10],andwp(s,p)isgivenby(valM(x )=0).DistributingM intovalresultsin(if(valM(u)=α(x))then10elsevalM(x))=0,whichsimpli esto(valM(u)=α(x))∧(valM(x)=0).Translatingbacktoprogramsyntaxgives(u=&x)∧(x=0)astheweakestprecondition.ThisprocessoftranslatingbackandforthfromMthuscorrectlytakesintoaccountaliasinge ects.Itistedioustocarryoutsuchcalculationsbyhand,buttheyareeasilyautomated,asdescribedinthefollowingsection.

3wp(M[a]:=v,p(M))isgivenbyp(M ),whereM [i]=M[i]fori=a,andM [a]=v,denotedbyM =M[a←v].DistributingM intopresultsinanexpressionintermsofM.