The reachability algorithm is based on summarization edges, which are "summerized" from "matched" push frames and pop frames. Therefore, we want to know what are the "pushed" frames whenever we encounter a pop frame. The "pushed" frame, for example, s0 --+f---> s1, +f is the pushed frame. s0 is the call site, and s1 is the starting statement of the callee function. In some sense, the edge between s0 and s1 is the call-to-start-edge that was presented in Tom Reps's early paper about static analysis as graph search.

However, when we perform abstract garbage collection, we want to inspect the entire stack, rather than the top ones. I mean, especially, we want to know what are the live records on stack, and so we can compute what are the reachable live addresses while garbage collecting those unreachable ones. Therefore, we have a structure to record, what are the possible stack frames for a specific control state.

The three structures we mentioned above is NonEpsPredState, predStateForPushFrame and PossibleStackFrames respectively. In addition to the two central structures, we have additional four data structures to help updating the information for the three central DS.

EpsPreds -- Epslang predecessors.

EpsSuccs -- Epslang successors.

TopFrames -- top frames for some control state

Now let's look at the code:

For new edges, we will perform the updates on all the structures. However, it depends on what kind of edge:

def update(newEdges: Set[Edge]) { for (e <- newEdges) { e match { case Edge(s1, Eps, s2) => equalize(s1, s2) case Edge(s1, Pop(f), s2) => processPop(s1, f, s2) case Edge(s1, Push(f), s2) => processPush(s1, f, s2) case Edge(_, se@Switch(_, _, _), _) => throw new DSGException("Illegal switch edge: " + se) } } }

Easy case first--let's look at the push case, which is s1 --+f---> s2

//Update topFrames and predForPushFrames for a new edge s1 --[+f]--> s2 private def processPush(s1: S, f: Frame, s2: S) { // get the s2 *and* s2's successor states, they will all be updated with the topFrames // predForPushFrames val nexts = Set(s2) ++ gets(epsSuccs, s2) for (s <- nexts) { puts(topFrames, s, Set(f)) // the current f is s' top frame // the predStateForPush frame of course if s1 puts(predStateForPushFrame, (s, f), Set(s1)) // s1 is of course s's non epse preds puts(nonEpsPreds, s, Set(s1)) // this part will be illustrated shortly updatePossibleStackFrames(s) } }

Here is updatePossibleStackFrames for a state:

def updatePossibleStackFrames(s: S) { // first get the top frames of the currnet s, which will be its possible stack frames val possibleAsTop = gets(topFrames, s) puts(possibleStackFrames, s, possibleAsTop) // for all [non-eps] predecessors of s for (spred <- gets(nonEpsPreds, s) ++ gets(epsPreds, s)) { // see what are their possible stack-frames val newPossibleStackFrames = gets(possibleStackFrames, spred) // add them to possible stack frames of s puts(possibleStackFrames, s, newPossibleStackFrames) } }

Now let's look at pop: and so we want to find the caller state (after which the pushed frame was generated) which can be found from predStateForPushFrame:

// Update eps-graphs for a new egde s1 --[-f]--> s2 private def processPop(s1: S, f: Frame, s2: S) { val newEpsPreds = gets(predStateForPushFrame, (s1, f)) // for each pred, we genenrate the new epslang edge from callsite node to the return site node. for (s <- newEpsPreds) { equalize(s, s2) } }

Now it is time to look at the epslang rule:

private def equalize(s1: S, s2: S) { val preds = Set(s1) ++ gets(epsPreds, s1) val nexts = Set(s2) ++ gets(epsSuccs, s2) // Add new successors, this is easy, since for preds, what happened after does not matter, we only need to remember there are nexts successors. for (s <- preds) { puts(epsSuccs, s, nexts) } // Add new predecessors and top frames val topFramesToAdd = preds.flatMap(x => gets(topFrames, x)) // *what happened matters*, in the sense that, for the current epslang edge, we want to update the information before the sucessor nodes (including s2) for (s <- nexts) { // update eps-predecessors puts(epsPreds, s, preds) // update top-frames puts(topFrames, s, topFramesToAdd) // update immediate non-esp predecessors for (f <- gets(topFrames, s1)) { val predForPushForS1 = gets(predStateForPushFrame, (s1, f)) puts(predStateForPushFrame, (s, f), predForPushForS1) } // Update introspective history for GC updatePossibleStackFrames(s) } }