Shape analysis through predicate abstraction and model check(8)

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

reach[A;F](x,b,M):itispossibletoreachaddressbfromaddressxin0ormoresteps.Thewpisgivenby

reach[Ai;F](x,b,M)∨(¬A(i)∧reach[Ai;F](x,i,M)∧reach[Ai;F](c,b,M)) reachp[A;F](x,b,M):itispossibletoreachaddressbfromaddressxin1ormoresteps.Thisisde nedbyalloc(x)∧( k:F (x,k,A):¬A(k)∧reach[A;F](M(k),b,M)),withwp:

reachp[Ai;F](x,b,M)∨(reach[Ai;F](c,b,M)∧¬A(i)∧reach[Ai,F](x,i,M)) dshared[A;F](x,y,M):thereexistsanon-nullnodereachablefrombothxandy.Thisisde nedby( v:v=NULL:reach[A;F](x,v,M)∧reach[A;F](y,v,M)),withwp:

dshared[Ai;F](x,y,M)∨

(¬A(i)∧reach[Ai;F](x,i,M)∧dshared[Ai;F](y,c,M))∨

(¬A(i)∧reach[Ai;F](y,i,M)∧dshared[Ai;F](x,c,M))∨

(¬A(i)∧(c=NULL)∧reach[Ai;F](x,i,M)∧reach[Ai;F](y,i,M))

cyclic[A;F](x,M):xreachesanodethatisinvolvedinacycle.Thisisde nedby( v:reach[A;F](x,v,M)∧reachp[A;F](v,v,M)),withwp:

cyclic[Ai;F](x,M)∨

(¬A(i)∧reach[Ai;F](x,i,M)∧cyclic[Ai;F](c,M))∨

(¬A(i)∧reach[Ai;F](x,i,M)∧reach[Ai;F](c,i,M))

Fig.5.WeakestpreconditionsforshapepredicatesforM =M[i←c].Inthesefor-mulas,weuseAitorepresentA∪{i}

apreludetocomputingwpisgivenbyreach[valM(A);F](valM(e1),valM(e2),M).

Asanexample,intheprogramfromSection1,considerthepredicatereach[;n](x,k),andtheassignmentx:=t,wheretandxareoftypeList.Thetranslatedpredicateisgivenbyreach[;n](valM(x),valM(k),M),whiletheassignmentresultsinthememoryupdateM =M[α(x)←valM(t)].Sub-stitutingM forMgivesreach[;n](valM (x),valM (k),M )).Thissimpli es,usingthewpforreach,toreach[α(x);n](valM(t),valM(k),M)∨(true∧reach[;n](valM(t),α(x),M)∧reach[;n](valM(t),valM(k),M)).Fromthedef-thattcanneverreachtheaddressofx.Thus,theunderlinedtermsimpli estofalse,andtheresultis:reach[α(x);n](valM(t),valM(k),M).Theavoidingaddressα(x)issuper uousforthesamereason,soitcanberemoved,givingtheresult(inprogramsyntax)asreach[;n](t,k).