Shuying's research blog

I have spent some hours to reflect the reachability algorithm. My goal is to make it run faster and more memory efficiency. (It seems that the space efficiency is important to make a practical piece of software.)

I realized that I have do many things to possibly achieve this: 1. The algorithm itself. 2. The data structure I used.

For the first point, I explored some dyck-reachability algorithm. Their motivation is all about pointer-to analysis. and their strategy is usually to merge nodes. It is undesirable to merge all those nodes in my scenario, at least as I see it for now.

For the second point, I think about using Godel hashing, or check out the WALA framework, how they manage the pointer-to information compactly represented.

This is important since I realized that no matter what is in your dyck-state-graph, you need to represent those states (can be huge amount) compactly. I believe exploring WALA again, is the first right direction.

The other thing I am trying to do this week is profiling the application.

All we want is the summarization edges, which connects from push and pop nodes. e.g. s1----> +f ----> s2 ----> -f ----> s3. we want to connect s1 and s3. For the first point, we can know it is matching precisely to the returning point.

In addition, we also want to know all the possible pushed frames, to do abstract garbage collection, e.g. that s1---> +f1 -----> s2 ---> +f2 ----> s3. we know that +f1 and +f2 are the pushded frames.

For achieve the two purposes, we have to record a lot of information. we may want to have a data structure that possibleFrames, to record for every node, its is possible frames.

However, essentially, we have to take care of the propagation information, which is encoded in the epslang closure graph.

In the epslang closure graph, it is used to propagate the top frame information, the epslang closure information, the epslang successor information, the predessor node for pushed frames, as well as updating the possible frames.

In pushing frames, we only need to record the top frames and predecessor node for pushed frames for the target node. Of course, mark the possible frames structure.

In popping frames, we want to get the all the epslang predecessors of the source node and equalize each of them with the target node, which can be reduced to the logic of handling epslang edge.

I think this is the first time I have clearer idea of how this algorithm works!

However, this algorithm is not memory efficiency. At least, for every node, we are recoding the predecessors, top frames... though state node are passed by reference, the memory will not be allocated in those entries.

One spirit to inspired by the PLDI paper, maybe we can define the equivalence class and use union find to think up new scheme?

This year's PLDI has a paper about fast dyck-CFL-reachability algorithm presented. I think it is promising to adapt it into the current reachability analysis. However, a few things come to mind:

What's the fixed point algorithm

How they manage some other cases: how to add edges.

What will be potential problem in our case. I will consider the questions asked by Prof. Might.

OR, can we adapt the same spirit to shrink the size of epslang closure in some way? (this could yield less efficient result maybe)

If we can characterize the stack, and so we can define the partial orderness on it, and so we can define parital orderness for the configuration and so we can soundly apply the agressive cut off technique to significantly speed up the the fixed point computation.

There is a paper talking about the subsumption oriented pushdown automata.

The take for the paper is that for a derivation or transition or stack action, it models the stack with respect to the stack changes:

What are the elements are involved to compute the transition (context zone)

The modification zone of the stack.

The instantiation zone (s1 <= s2) s2 is an instance of s1

The identification zone, which involves no changes on the stack.

and so it has the three things to model the transition (p, b, delta)

p is the number of stack top elements involved for the transition.

b is the modification height

delta is the stack height change between input and output stack.

and so

each transition depends on the top elements

transition is order compatible.

ACTIION axiom I don't quite undersatnd.

The most important thing is that the partial orderness defined for the stack is totally bullshit, which equals defining nothing. Just for reference

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) } }

I just decided to find my advisor to talk about something. Here are something that is educating me:

Don't need to constraint yourself to the contents in the paper.

All it needs is talking about something interesting and educating, including reflection, which might be interesting, malware? fine!

It would be wasting everybody's time by giving a boring talk!

Hey, I think I have pretty good idea how the other works deal with string analysis. Let's take a brief review:

For the same example:

x = “a”; while (cond) do x = “0“ + x; x = x + “1”; print x;

We are expected to get {0^na1^n | n>=0}.

Statically analyze the program and determine a context-free grammar G which represents the values of a variable, x at the hot spot.

So the G is equivalent to the reference grammar: S -> "a" | "0" S "1"

The problem of the research:

Checking a context-free grammar is included in antoher context-free grammar is "undecidable".

Regular expresssion approximation: Moler

CFG Regular expression X0 -> "a" X0 -> "a" X1 -> X0\|X3 X1 -> X0 X2\|X3 X2 -> "0" X1 X3 -> "0"X3 \| eps X3 -> X2"1" X2 -> "1"X2 \| eps X4-> X1 X4 -> X1

The string values represented by RG include the string values represented by the refernece grammar.

The Shortcoming: Not clear how to deal with other string ops! print replace("00", "0",x)] at the end of the example, there will be X4->X1

Context-free: Minamide

CFG Regular grammar transformed from reference grammar X0 -> "a" S0 -> "a" X1 -> X0\|X3 S1 -> "0" S0 "1" X2 -> "0" X1 S2 -> "0"S1 "1" X3 -> X2"1" … X4-> X1 Si -> "0" Si-1 "1"

Advantage: Improvement in dealing with string operators. For example, the replace operation, its image can be mapped under transdurcer.

Abstract interpretation

(1) A string value is abstracted as a "regular string" which is the same as regular expression except that a consecutive repetition is not allowed, i.e. 01 => {0,1}* (2) Abstract interpretation of a program on the abstract domain of regular strings.

So the walk through of the example using this approach is: a -- a -- 0a1

a -- a widening 0a1 = 0\*a1\* --00\*a1\*1

a -- 0\*a1\* widening 00\*a1\*1 = 0\*a1\* -- 00\*a1\*1

fixed point reached: 0\*a1\*

The last result include the string values represented by the refernce gramamr.

Abstract parsing & Analysis

Feeling like the time spent is all gone, recently.

First I explored the Non-nullability. and then I spent time for widening strategy for pushdown. and then I spent time to explore the string analysis.

These are important things for the recent research.

There are many analysis based on SSA IR. Soot, Wala, etc.

For those analyzers targeting Android, they convert the Dalvik bytecode to Java bytecode, or directly, convert the SSA between the two, so as to leverage the existing analysis for Java.

I am trying to speed up the pushdown system, since it is really the foundation I have to add more sophisticated analysis.

Previously, abstract garbage collection and live register analysis has improved the performance. The two techniques both wipe out the some kind of values of some addresses, where garbage collection garbage collects discards unreachable addresses and live register analysis discard the addresses that are not 'live' with respect to the live register at the program point.

In this case, if we apply widening, which will merge the store values for some addresses, and its foundation is based on monotonicity. and so it can speed up the fixed-point computation.

Therefore, obviously, when abstract garbage collection is turning on as well as live register, and the same time with widening, the improvement may not be considerable since values of some stores of some addresses may be garbage collected by AGC and LRA, and therefore, when it is time to apply widening, the lattice is lifting up again a little bit, but still needs some time to reach the fixed-point.

On the other hand, if you purely apply widneing, not using live register analysis, it is not suitable for object-oriented program analysis. There are the object mergeing problem! (Imprecise object points-to set will cause spurious flows, while live register analysis allieviate some pain here).

Recently I have encountered some problem in Scala that has been encountered before.

The basic issue is the path dependent types: For any class that is defined inside of a trait or an abstract class, and then you want to reference some nested types from another class, for example:

trait A { type Addr sealed class Value type Store = Map[Addr, Value] } Class AnalysisThreadHelper extends Thread { var wideningTable: MMap[Stmt, Set[Store]] = Map.empty // MMap is mutable map // The Store can not find its type }

AnalysisThreadHelper can not find type definition for Store.

One option is to extend A. However, AnalysisThreadHelper is supposed to be instantiated, if the Ahas abstract types, it can not be instantiated.

The other option is to define some types in the AnalysisThreadHelperwith the same names as those defined in A. and whenever we get some instnace from wideningTable, the data type is AnalysisThreadHelper.Addr and the like, and we have to interact with instances of the the type from A, we can use some the notation # to reference the nested defined type, for example, s.asInstanceOf[A.Store]. This all looks fine. Problems come when we want to update the wideningTable with the instances dynamically computed from instances of type A.Store. There will be type mismatch errors in the compile time. Then you may to patch it up by strong casting from type A.Store to AnalysisThreadHelper#Store, but this does not work, since the place you do this casting has its own instance class path (path dependent path). Still mismatch!

The current (I think it is still kind of crappy way) worked out way that eliminated compiling errors is creating another accomponied trait that implementes some abstract types and methods in A. Then AnalysisThreadHelper extends that 'concrete' trait. Note that the other important thing is that the type in wideningTable is defined using A#Store. Otherwise, in the st->Set(s) won't compile, since it will say the found type is A.this.Store, while the required type is AnalysisThreadHelper.Addr, AnalysisThreadHelper.Value in the immutable map.

No detection of computed control state

No detection of computed edges in dyck state graph

No detection of computed edges in epslang closure graph

Not the three reasons above. But worth noting!

No aggressive cut off: for a to-explore control state, the algo does not detect whether the control state is weaker than any seen states before. The right way should skip exploration of the weaker states.

Now I know why their implmentation does not encounter state explosion problem! The key is that: for conditional branches, it takes one branch in most cases!

I have had pretty exciting two days before, exploring the performance bottleneck in the current implementation of pushdown system.

However, I realized that the paper revision for TAPAS needs to be done no matter what, so I have to shift my focus on rewrite the paper! Argh!