Designers of context-sensitive program analyses need to take special care of the memory consumption of the analysis results. In general, they need to sacrifice accuracy to cope with restricted memory resources. We introduce terms as a general data structure to capture and manipulate context-sensitive analysis results. A -term is a compact representation of arbitrary forward program analysis distinguishing the effects of different control-flow paths. While -terms can be represented by trees, we propose a memory efficient representation generalizing ordered binary decision diagrams (OBDDs).
if (...)
x = 1; else
x = 2; if (...){ y = x; b = 3; } else { y = 2; b = 4; } if (...)
a = x; else
a = y; return a+b; x = 1
x = 2
Phi7 return
In Figure 1, we show a simple piece of code containing three if-statements and the corresponding basic block structure and SSA graph. In the SSA graph, we have annotated each -function P hib with their basic block number b. The leaves 1, 2, 3 and 4 (in boxes) in the rightmost part of the figure represent integer values.
The -functions in the SSA graph forbid static data-flow analysis to select a unique definition of a given variable. For example, the value of variable x in Figure 1 depends on which branch of the first if-statement that is chosen. This uncertainty, which we in general can not resolve, is in the SSA graph symbolized by the node P hi4.
In a context-insensitive data-flow analysis, the interpretation of the -functions assume that any possible definition is a value of that variable. This approach results in a set approximation of the run-time values. For example, the value of the variables x, y, and a in Figure 1 is f1; 2g, and the value of b is f3; 4g. Notice that in the context-insensitive interpretation, the variable value sets resulting from a join point in the control-flow graph do not contain any information about the different flow-path options that generated all the different values. It simply contains the possible values.
Context-sensitive data-flow analyses are more precise and map control-flow path(s) to possible value(s). As the number of possible paths grows exponentially with the number of if-statements (and is even unbounded if loops are involved) we should aim for compact representations of this mapping. Such a compact context-sensitive description of a given variable value can be achieved with -functions.
A -function is a representation of how different control-flow options affect the value of a variable. For example, we can write down the value of variable b in Figure 1 using -functions as b = 7(3; 4). Interpretation: variable b has the value 3 if it was reached from the first predecessor to block 7 in the control-flow graph, and the value 4 if it was reached from the second predecessor block. That is, a value expressed using -functions (a so-called -term) does not only contain all possible values, it also contains which control-flow options that generated each of these values. Using this approach we can write down the -term values for the variables in Figure 1 as: x = y = b = a = 4(1; 2); 7( 4(1; 2); 2); 7(3; 4); 10( 4(1; 2); 7( 4(1; 2); 2)) Notice that values of variables depending on several control-flow options (e.g., the value of variable a) correspond to -terms over -terms, i.e., they are constructed as a composition of the -functions representing the different options. 2.1
-term Construction The construction of the -term values and the numbering of the -functions is a part of a context-sensitive analysis. Every -node in an SSA graph represents a join point for several possible definitions of a single variable, say x. When the analysis reaches a block b containing a -node for x it “asks” all the predecessor blocks to give their definition of x and constructs a new -term b(x1; : : : ; xn) where xi is the -term value for x given by the i:th predecessor.
If the i:th predecessor block does not define x by itself, it “asks” its predecessor for the value. This process continues recursively until each predecessor has presented a -term value for x. The process will terminate if any use of a value also has a corresponding definition.
Loops in the control-flow cause some problems as they would lead to ever growing -term, i.e., analysis would not reach a fixed point. We will ignore the termination problem for now, and discuss and solve this problem later. For a first try, we may have a (possibly countable) number of -terms with the same block number b since every -node in b generates a new -term value when the analysis reaches that block. As discussed in the introduction to Section 2, -term construction is tightly coupled to a context-sensitive analysis. A new set of -terms is generated every time t the analysis reaches a block b containing -nodes. We denote this set with tb.
All -terms generated of block b at time t have the same switching behavior. That is, for any two -terms ib(x1; : : : ; xn) and jb(y1; : : : ; yn), and for any execution of the program, it holds that if i = j and branch xk in ib(x1; : : : ; xn) is selected, then also branch yk in jb(y1; : : : ; yn) is selected. This property will be important later on when we introduce operations on -terms. Anyhow, two -terms generated from the same block but at different times of the analysis will not necessarily have the same switching behavior.
This situation is illustrated in Figure 2 where we show a while-loop that encloses an if-statement that assigns a new value to a variable x. At first entry of a block w containing the while loop header, we assign x the value 0w(1; ?) where the bottom element ? symbolizes “value undefined”. This value is later propagated inside the loop body where the if-statement is handled. After the if statement (in block i) we assign x the value i0( 0w(2; ?); 0w(0; ?)), a value that is later propagated to the loop header block w. Using this approach we can compute all possible values for x after an arbitrary number of loop iterations. The first three x values that might escape the loop are: Every term can be naturally viewed as a tree and -terms are no exception. This is illustrated in Figure 3 (left) where we show the tree representation of the -term values for the variable a in Figure 1. Each edge represents a particular control flow option in this view and each path from the root node to a leaf value contains the sequence of control flow decisions required for that particular leaf value to come into play. ret ret
+ ret χ ret a+b ret
That is, we can in this case make use of the fact that both -terms have the same switching behavior and apply the + operator on each of the two branches separately before we merge the result. This transformation is illustrated Figure 6. That we can rewrite the addition of two -terms as a -term over the addition of a and b for each individual branch is in this case quite obvious. However, this rule can be applied on any operator and any -function jb. This rewrite rule for -term expressions is called a Shannon expansion1.
Finally, once we applied the Shannon expansion of the operator + in Figure 4, we are in a position where we can apply + on a set of leaf values. In this case + is well defined and we can fall back on ordinary integer arithmetics. The resulting simplifications are shown in Figure 6 where we also used the redundancy rule (t; t) = t. This manipulation can symbolically be written as: The result indicates that no matter what branch of the if-statement we use, we will always get the result a + b. This simple example illustrates one of the strengths of using -terms, we can by using a few simple rewrite-rules make use of having stored flow-path information and "compute" more precise results than would have been possible in a context-insensitive approach.
Finally, it should be noted that our presentation of -terms as a tree, and all operations on -terms as tree manipulations, is very much inspired by Orded Binary Decision Diagrams2 (OBDD) as presented in [Bry86, Bry92]. Furthermore, the 1The word "Shannon expansion" is taken from the OBDD literature where a similar procedure is used to rewrite boolean functions represented as OBDDs.
2An OBDD is a clever (and slim) representation of Boolean functions as a directed acyclic graph that allows an efficient computation of frequently used operations such as disjunction, conjunction and function composition. algorithms describing various operations on -terms presented in this chapter are intended to be easy to understand, more efficient algorithms can be found in the above cited papers. 3
In this section, we present a number of definitions and notations related to -terms that are of general interest and that will be used in the remainder of this paper later on. Many of the ideas and notations are taken from [Tra99] and [Bry86, Bry92] and adjusted to fit our needs. The set of -functions depends on the set of -functions which depends on the program we are analyzing. Furthermore, the exact number of -functions at use depends on how we handle loops and other approximations we do in the analysis (e.g. finite k approximations). To simplify what follows, we assume that each program p has a (possibly infinite) set of -functions X (p).
Each -function jb 2 X (p) is identified by a pair (b; j) where: 1. The block number b = block( jb); b 2 [1; Bp] indicates in what basic block its generating -node is contained. Here
Bp is the number of basic blocks in a program p. 2. The iteration index j = index( jb) indicates on what analysis iteration over block b the -function was generated.
The -functions generated from the first analysis iteration over b always have iteration index 0.
Two -terms ib(x1; : : : ; xn) and jb(y1; : : : ; yn) from the same block b have the same switching behavior if they have the same iteration index (i.e. i = j). That is, for any execution of the program it holds that
branch xk is selected , branch yk is selected Thus, the switching behavior of a -function is determined by a pair (b; i) where b is the block number and i is the iteration index. In what follows, we will often skip the iteration index to simplify the notations. In these cases we assume that all involved -function have the same iteration index.
Finally, the arity of a -function, denoted arity( jb), with n arguments is n.3 3.2
-terms A programming language type is a set of concrete values. In program analysis, concrete values are abstracted to abstract values requiring a Galois connection between concrete and abstract types [CC77]. Associated with each abstract type V , we have a set of -terms. These -terms form the context-sensitive counterpart to the abstract values V as used in a context-insensitive analysis.
Definition 1 ( -terms) Let LV = fV; u; t; >; ?g be a lattice4 of abstract values of type V and let X (p) be the set of -functions associated with a given program p. The set of all -terms XV (p) over the abstract values V is then defined recursively as: ) ) v 2 V
v 2 XV (p) b t1; : : : ; tn 2 XV (p) ^ j 2 X (p) jb(t1; : : : ; tn) 2 XV (p); n 2 arity( jb) Notice, even if the set of abstract values V is finite, XV (p) of a program with loops is infinite since there is no upper limit on the composition depth.
We have previously associated all -functions jb with a block number b = block( jb). This notation can be extended to -terms as well.
Definition 2 (Block number) The block number of a -term t 2 XV , denoted block(t), is defined as: block(t) = 0 b if t 2 V , if t = b(t1; : : : ; tn). 3The arity is independent of the loop iteration j. However, we index jb with j to be consistent in our notations.
4The lattice property is introduced because it is required to widen the abstract values. This, in turn, is required for an analysis to terminate (in general). However, widening and termination of analysis are deliberately omitted from the present discussion. Notice that we have associated all the values v 2 V with a (default) block number 0 not corresponding to any existing block in the program.
Definition 3 (Function set) The function set of a -term t 2 XV (p), denoted f unc(t), is the set of all -functions jb 2 X (p) used to construct t.
3( 1(1; 2); 2( 1(3; 4); 2)) ) f unc(t) = f 3; 2; 1g From now on we will drop the reference to a specific program p in X (p) and XV (p) and assume that it is implicit. It should by now be clear that all these entities are directly related to a given analysis instantiation. 3.3
Each -term t 2 XV has a unique tree representation Gt = fN; E; rg where N XV is a set of nodes, E is a set of edges, and r 2 N is the root of the tree. The two sets N and E can be defined recursively as; XV
XV r n 2 N = ) t; ni 2 N ^ (n; ni) 2 E: where ni denotes the i:th argument of n = jb(n1; : : : ; nn).
Our reason for introducing the tree representation of a -term is that many notions and -term operations are easiest to understand in terms of tree manipulations. Basic operations include
V , is the set of all leaf values in the tree representation of t.
of t. The leaves and t are not included.
XV , is defined as: children(t) = ; ft1; : : : ; tng if t 2 V if t = jb(t1; : : : ; tn) The depth of a -term t 2 XV , denoted depth(t), is the depth of the tree representation of t.
Let n 2 XV be a node in the tree representation of a -term t 2 XV . The depth of n in t, denoted depth(t; n) = depth(t) depth(n), is the depth of the node n in the tree representation of t.
XV , is the set of all subtrees of t in the tree representation For example, t = 8 leaves(t) = f1; 2; 3; 4g >>>> subterms(t) = f 4(1; 2); 7( 4(3; 4); 2); 4(3; 4)g 10( 4(1; 2); 7( 4(3; 4); 2)) ) < children(t) = f 4(1; 2); 7( 4(3; 4); 2)g >> depth(t) = 3; > >: depth(t; 4(3; 4)) = 2 3.4
In this section we present further basic operations on -terms. Most important is the Shannon expansion which can be used to manipulate -term expressions without affecting their value.
Definition 4 (Restriction) The restriction of a -term t 2 XV to the k:th branch of jb, denoted tj(b;j):k, is a new -term where every subterm jb(t1; : : : ; tn) with switching behavior (b; j) in t has been replaced by its k:th child tk. t = 03( 01(1; 2); 02( 10(1; 2); 2)) ) tj(3;0):2 = tj(1;0):1 = A restriction f jxi=true in the OBDD description of a Boolean formula f (x1; : : : ; xn) is a new formula where the i:th variable xi has been assigned the constant value true. The -term counterpart is that we define a new -term tj(b;j):k by only considering the value from the k:th predecessor of block b (in iteration j) in the construction of t. It should also be noticed that if we restrict us to the k:th branch of jb, when j 62 f unc(t), t is left unaffected.
b Definition 5 (Equivalence) Two -terms are equivalent ( ) if they are (syntactically) the same or represent the same -term value, i.e. if they can be transformed into the same -term by sequences of Shannon expansions or redundancy eliminations.
Definition 6 (Shannon expansion) The Shannon expansion of a -term t 2 XV over jb is a new -term defined as: t = jb(tj(b;j):1; tj(b;j):2; : : : ; tj(b;j):n) where n = arity( jb) Notice, the Shannon expansion creates a new -term but not a new -term value. It is just a rewrite rule that can be used to manipulate a -term expression. For example, t = 13( 11(1; 2); 12( 11(1; 2); 2)) 11( 13( 12(1; 1); 12(1; 2)); 13( 12(2; 2); 12(2; 2))) 12( 13( 11(1; 2); 11(1; 2)); 13( 11(1; 2); 11(2; 2))) (expansion over 11) (expansion over 21) Definition 7 (Redundancy and redundancy elimination) A -term is redundant if all its sub-terms are equivalent. That is, jb(t1; : : : ; tn) t if t1 : : : tn. The process of removing redundant -terms is called redundancy elimination.
Obviously, a -term t containing a redundant subterm the pattern
r can, without any loss of information, be reduced according to t = : : : i(: : : ; r(t; : : : ; t); : : :) : : : : : : i(: : : ; t; : : :) : : : In the tree view of a -term, this corresponds to replace a subtree rooted by r by any of its subterms (which are all equal). For example, t = 11( 13(1; 12(1; 2)); 13(2; 12(2; 2))) 11( 13(1; 12(1; 2)); 13(2; 2)) 11( 13(1; 12(1; 2)); 2) (since 21(2; 2) (since 31(2; 2) 2) 2) 4
When doing a program analysis there is a need of defining an abstract operator related to an existing concrete operation. The aim of this section is to say that every context-insensitive operator has a -induced context-sensitive counterpart e with a semantics completely determined by the semantics of . We will define e in terms of an algorithm apply that recursively performs Shannon expansions of the operator e over the -functions in the input -term values. We think of this process as if we "push" the operator towards the leafs of the input -term where the ordinary context-insensitive semantics of the operation can be applied. This idea is inspired by the ideas of evaluating logical formulas represented as OBDDs [Bry86, Bry92].
Definition 8 (Restriction) Let e : X1 : : : Xn 7! Xv be an operator on -terms. The restriction of an operation e(t1; : : : ; tn) to the k:th branch of jb, denoted ej(b;j):k, is defined as
ej(b;j):k(t1; : : : ; tn) = e(t1j(b;j):k; : : : ; tnj(b;j):k) where tij(b;j):k is the restriction of the i:th operand ti to the k:th branch of jb. tIhtasti mifplyjb m62efaunsncth(at1t)w[e :a:r:e[refsturinccti(ntgn)awll einhpauvteotpiej(rba;nj)d:ks t=o tthieankd:thcobnrsaenqcuheonftlyjbthbaetfoerj(eb;wj)e:ka=ppley(tth1;e:o:p: e;rtant)io.nThea. tNiso,ttihcee restriction has no effect in such cases.
Definition 9 (Shannon expansion) Let e : X1 : : : Xn 7!: Xv be an operator on -terms. The Shannon expansion of an operation e(t1; : : : ; tn) over the -function jb is defined as e(t1; : : : ; tn) = b j (ej(b;j):1; : : : ; ej(b;j):m) where m = arity( jb) and ej(b;j):k is the restriction of the operation e(t1; : : : ; tn) to the k:th branch of jb. The Shannon expansion of an operation e(t1; : : : ; tn) over jb can be seen as if we "push" the operator e one step towards tthheesleeavfalvuaelsueussionfgthejb.input operands ti by computing e for each one of the branches of jb individually, and then merge The Shannon expansion has the following properties:
It is a rewrite rule for a -term expression that has no effect on the resulting -term value. It can be seen as a first step in the computation of the operation.
It leaves the -expression unchanged if jb 62 f unc(t1) [ : : : [ f unc(tn) since in that case ej(b;j):k = e(t1; : : : ; tn) and we can apply the redundancy rule b j (e(t1; : : : ; tn); : : : ; e(t1; : : : ; tn)) = e(t1; : : : ; tn): If jb 2 f unc(ti) for any ti in t1; : : : ; tn then
jf unc(ej(b;j):1) [ : : : [ f unc(ej(b;j):m)j < jf unc(t1) [ : : : [ f unc(tn)j; m = arity( jb). That is, the “size" of the input-operands to the e operator (in terms of the number of unique functions contained) is always decreasing.
This last property indicates that repeated Shannon expansions over the -functions in the input operands will result in a situation where the input-operands to e are all leaf values. Thus, the semantics of e is completely defined in how e operates on the leaf values. This observation leads to the concept of -induced operations to be presented shortly.
The algorithm apply (see Algorithm 1) is a recursive function that performs repeated Shannon expansion until it reaches the leaf values where the context-insensitive operator can be applied.
Algorithm 1 apply( ; t1; : : : ; tn) 7! t let f unc_set = f unc(t1) [ : : : [ f unc(tn) if f unc_set = ; then
return (t1; : : : ; tn) else pick jb from f unc_set for all i 2 1 : : : arity( jb) do
let ci =apply( ; t1jj:i; : : : ; tnjj:i) end for return jb(c1; : : : ; carity( jb)) end if
The test f unc_set = ; checks if t1; : : : ; tn are all leaf values. If so, we apply the context-insensitive operator . Otherwise, we push the operator towards the leafs by a Shannon expansion in one of the remaining -functions. Note also that:
apply( ; v1; : : : ; vn) = (v1; : : : ; vn) if v1; : : : ; vn are all leaf values.
This follows immediately from the base case in the algorithm apply.
Finally, Algorithm 1 is intended to be easy to understand, not efficient, since it will be used in the definition of -induced context-sensitive operators. More efficient algorithms are available [Bry86]. One important observation is that the algorithm apply in general increases the depth of the resulting -term expression. More precisely, a closer look at apply shows that
depth(e(t1; : : : ; tn)) = jf unc(t1) [ : : : [ f unc(tn)j: As a consequence, e applied on operands with a similar control-flow history (i.e. jf unc(t1) [ : : : [ f unc(tn)j jf unc(t1)j + : : : + jf unc(tn)j) will generate less complex results than if applied on operands with very different controlflow histories (i.e. jf unc(t1) [ : : : [ f unc(tn)j jf unc(t1)j + : : : + jf unc(tn)j).
In conclusion, every context-insensitive operator has a -induced counterpart e and its semantics is completely determined by the context-insensitive semantics of . We compute e by repeated Shannon expansions where each step means that we are “pushing" e closer to the leaf values where the context-sensitive operator is defined and can be applied. 5
We defined -terms as a means to capture context-sensitive analysis values for programs represented as SSA-graphs. Each program point, i.e., each SSA-node, is mapped to a corresponding -term representing a context-sensitive analysis value for that point. Especially, each meet point of execution paths in the program, i.e., each phi-node, is mapped to a -term whose children represent the alternative analysis values of these paths. -terms are represented by graphs without any redundancy which generalizes the idea behind BDDs. This leads to a memory efficient representation of context-sensitive analysis information. Operations over context-insensitive analysis values, needed to implement transfer functions of the analysis, are defined using restriction and Shannon expansion which are also similar to the corresponding BDD operations. As a result, any context-insensitive analysis can automatically be transformed into a corresponding context-sensitive analysis.
We deliberately ignored the merging of analysis values of different contexts, which is needed for making contextsensitive analysis practical for large and iterative programs; otherwise even -terms grow beyond any memory bound. Merging, and, hence, the reduction memory requirements of -term at the price of analysis precision, can easily be achieved by applying the meet operation of the context-insensitive analysis values to leafs of -(sub-)terms. Controlling this merging of sub-terms based on available memory and precision of analysis values is matter of future work. [Ake78] [Bry92]
Sheldon B. Akers. Binary decision diagrams. IEEE Transactions on Computers, 27(6):509–516, June 1978. R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
R. E. Bryant. Symbolic boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixed points. In Conference Record of the Fourth Annual ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages, pages 238–252, January 1977. [Tra99]
Martin Trapp. Optimerung Objektorientierter Programme. PhD thesis, Universität Karlsruhe, December 1999.