Shape analysis through predicate abstraction and model check(7)

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.2WeakestPreconditionsforShapePredicates

Wehave,sofar,consideredwpcalculationsforsimplekindsofpredicates,albeittakingintoaccountcomplexaliasinge ects.Weareprimarilyinterestedinmoreglobal,second-ordershapeproperties.Thekeypropertyisreach[A;F](i,j,M).Informally,thissaysthatthereisasequenceofstepsinMfromaddressitoaddressj,whichavoidsalladdressesinA,andusesonlythe eldsinF.Wede nethispreciselybelowasaleast xpoint.Astepreferstoamemorydereference.Forexample,ifzisavariableoftypeNode(seeFigure1),thelocationwheretheaddressofthenextnodeisstoredisn (α(z))(thevalueof&(( z).n)).ButtheaddressofthenextelementitselfisgivenbyM[ n(α(z))],whichresultsfromamemorydereference.

ForasetFof eldnames,letF (w,y,A)holdi yisreachablefromwusingonly eldaccessesfromF(e.g.x.a.b.c),whileavoidingaddressesinA.Thisisde nedasfollows:

F (w,y,A)≡alloc(y)∧

(µZ,x:alloc(x)∧(x=y∨(¬A(x)∧( a:a∈F:Z( a(x))))))(w)Wecanthende nereachby

reach[A;F](w,b,M)≡

(µZ,x:alloc(x)∧( k:F (x,k,A):(k=b∨(¬A(k)∧Z(M[k])))))(w)NotetheexplicitdereferencingstepM[k]inthisde nition.

ThewpforreachiscalculatedforanupdateM =M[i←c]bysubstitutingM forMinthis xpointexpression,andsimplifyingtheresult.Fortheotherpredicates,whicharede nedintermsofreach,theirwp’sarecalculatedusingthewpforreach.Thede nitionsofthesepredicatesandtheirwp’sareshowninFigure5;theirderivationsareavailableat[32].Informally,thewpforreachabilitysaysthatitispossibletoreachbfromxafteranupdateM =M[i←c]providedthat,inthepreviousstate,either:(i)itispossibletoreachbfromxavoidingaddressesinA∪{i},or(ii)iisnotinA,andtherearepathsfromxtoi,andfromctobthatavoidA.Inthe rstcase,thememoryupdatedoesnotinvalidatethepathand,inthesecondcase,thememoryupdateservestolinktwopathsintothedesiredpathfromxtob.Theotherwpexpressionshavesimilarinformalreadings.

Aremarkablefeatureonemayobserveisakindofclosureproperty,inthatthewpforashapepredicateisexpressibleintermsofothershapepredicates—ofcourse,withdi erencesinthearguments.Closureensuresthatonlythesetypesofshapepredicatesariseduringtheiterationsoftheabstractionalgorithm,makingitpossibletospotpatternsthatindicatewhereapproximationisneeded.AnexampleofsuchapatternisgivenintheanalysisofalistreversalprograminSection5.

Weusepredicateswiththesamenamestostateprogramproperties:e.g.,reach[A;F](e1,e2),whereAisasetofprogramexpressions,ande1,e2arepro-gramexpressions.Thetranslationofthepredicateintothememorymodelas