Abstract:
A computer implemented method for performing a path-sensitive analysis of a computer program using path-insensitive techniques employing an elaboration of the program which advantageously permits a correctness determination of the program as well as a simplification and optimization.

Description:
CROSS REFERENCE TO RELATED APPLICATIONS  
       [0001]     This application claims the benefit of U.S. Provisional Application Ser. No. 60/743,849 filed Mar. 28, 2006. 
     
    
     FIELD OF THE INVENTION  
       [0002]     This invention relates to computational methods. More particularly this invention relates to the analysis of software programs and the application of this analysis to produce a path-sensitive result using conventional path-insensitive methods.  
       BACKGROUND OF THE INVENTION  
       [0003]     Static analysis over numerical domains has been used to check software programs for buffer overflows, null pointer references, division by zero and floating point errors among others. [See, e.g., Wagner, D., Foster, J., Brewer, E., , and Aiken, A. A first step towards automated detection of buffer overrun vulnerabilities. In Proc. Network and Distributed Systems Security Conference (2000), ACM Press, pp. 3-17; Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min_e, A., Monniaux, D., and Rival, X. A static analyzer for large safety-critical software. In ACM SIGPLAN PLDI&#39;03 (June 2003), vol. 548030, ACM Press, pp. 196-207; and Floyd, R. W. Assigning meanings to programs. Proc. Symposia in Applied Mathematics 19 (1967), 19-32]. Numerical domains such as intervals, octagons and polyhedra maintain information about the set of possible values of integer and real-valued program variables along with their inter-relationships. The convexity of these domains makes the analysis tractable. On the other hand, fundamental limitations of convexity lead to imprecision in the analysis, ultimately yielding many false alarms. Elimination of these false alarms is achieved through path-sensitive analysis employing disjunctive domains obtained through power-set extensions. Such extensions can be constructed systematically from the base domain using known techniques [See, e.g., Handjieva, M., and Tzolovski, S. Refining static analyses by tracebased partitioning using control flow. In SAS (1998), vol. 1503 of LNCS, Springer-Verlag, pp. 200-214; Cousot, P., and Cousot, R. Comparing the Galois connection and widening/narrowing approaches to Abstract interpretation, invited paper. In PLILP &#39;92 (1992), vol. 631 of LNCS, Springer-Verlag, pp. 269-295].  
         [0004]     Power-set extensions of numerical domains consider a disjunction of predicates at each program location. While these disjuncts help overcome convexity limitations, the complexity of the analysis can still be exponentially higher due to more complex domain operations and also due to the large number of disjuncts that can be produced during the course of the analysis. Furthermore, the presence of disjuncts require special techniques to lift the widening from the base domain up to the disjunctive domain [See, e.g., Bagnara, R., Hill, P. M., and Zaffanella, E. Widening operators for powerset domains. In Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004) (2004), vol. 2947 of LNCS, pp. 135-148].  
         [0005]     Controlling the production of disjuncts during the course of the analysis is one of the key aspects of managing the complexity of the analysis. The design of such strategies can be performed by techniques that annotate data flow objects by partial trace information such as trace partitioning, and other path sensitive data-flow analysis techniques that implicitly manage complexity by joining predicates only when the property to be proved remains unchanged as a result, or “semantically” by careful domain construction [See, e.g., Bagnara, R., Hill, P. M., and Zaffanella, E. Widening operators for powerset domains. In Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004) (2004), vol. 2947 of LNCS, pp. 135-148; and Manevich, R., Sagiv, S., Ramalingam, G., and Field, J. Partially disjunctive heap abstraction. In Static Analysis Symposium (SAS) (2004), vol. 3148 of LNCS, Springer-Verlag, pp. 265-279].  
       SUMMARY OF THE INVENTION  
       [0006]     According to an aspect of the invention, a path-sensitive program analysis is achieved through the use of path-insensitive techniques.  
         [0007]     More particularly, according to the present invention fixed points computed over power-set extensions correspond to fixed points over a base domain computed on an “elaboration” of the CFG. As a result, the complexity of path-sensitive analysis can also be controlled by means of a strategy for producing elaborations of the CFG being analyzed.  
         [0008]     Accordingly we demonstrate analysis techniques according to the present invention that perform the fixed point iteration hand in hand with the construction of the elaboration that characterizes the fixed point (On-The-Fly). As an application, we consider bounded elaborations, that correspond to power-set extensions wherein the number of disjuncts in each abstract object is bounded by a fixed number K. We discuss the implementation our ideas in a light weight static analyzer for the C language as a part of the F-Soft project and demonstrate results.  
         [0009]     One advantage of the elaboration approach of the present invention is that it provides a connection between the disjuncts in a power-set domain and the syntactic connections between them in a trace partitioning scheme. 
     
    
     BRIEF DESCRIPTION OF THE DRAWING  
       [0010]     A more complete understanding of the present invention may be realized by reference to the accompanying drawings in which:  
         [0011]      FIG. 1  is simple flow diagram showing disadvantages associated with prior-art static analysis techniques;  
         [0012]      FIG. 2   a  and  FIG. 2   b  are simple flow diagrams showing the flow diagram of  FIG. 1  and its elaboration  FIG. 2   b;    
         [0013]      FIG. 3  is simple flow diagram depicting a fixed point obtained on a power-set extension according to the present invention;  
         [0014]      FIG. 4  shows an example program and the invariants computed using the octagon domain; a  
         [0015]      FIG. 5   a  shows that an elaboration of a CFG C is another CFG E according to the present invention;  
         [0016]      FIG. 5   b  shows replication relationships between CFG C and an elaboration CFG E according to the present invention;  
         [0017]      FIG. 5   c  shows a CFG from an example along with an elaboration;  
         [0018]      FIG. 5   d  shows an additional example of an elaboration according to the present invention;  
         [0019]      FIG. 5   e  shows yet another example of an elaboration according to the present invention;  
         [0020]      FIG. 6  shows an exemplary bounded disjunctive elaboration according to the present invention; 
     
    
     DETAILED DESCRIPTION  
       [0021]     The following merely illustrates the principles of the invention. It will thus be appreciated that those skilled in the art will be able to devise various arrangements which, although not explicitly described or shown herein, embody the principles of the invention and are included within its spirit and scope.  
         [0022]     Furthermore, all examples and conditional language recited herein are principally intended expressly to be only for pedagogical purposes to aid the reader in understanding the principles of the invention and the concepts contributed by the inventor(s) to furthering the art, and are to be construed as being without limitation to such specifically recited examples and conditions.  
         [0023]     Moreover, all statements herein reciting principles, aspects, and embodiments of the invention, as well as specific examples thereof, are intended to encompass both structural and functional equivalents thereof. Additionally, it is intended that such equivalents include both currently known equivalents as well as equivalents developed in the future, i.e., any elements developed that perform the same function, regardless of structure.  
         [0024]     Thus, for example, it will be appreciated by those skilled in the art that the diagrams herein represent conceptual views of illustrative structures embodying the principles of the invention.  
         [0025]     Before discussing the present invention, the following definitions will provide the reader with the proper context.  
         [0026]     Data flow analysis discovers “facts” that hold true at different program locations.  
         [0027]     Example:  
                                                                       int i=0;           for (i=0; i &lt; 100; ++i)                /*-- Fact: 0 &lt;= i and i &lt;= 100 --*/                ...                      
 
         [0028]     A Dataflow analysis can answer specific questions about the programs behaviour. Examples include:  
         [0029]     (a) Constant folding analysis: Is the value of some variable always a constant at some program location? If so, what is it? 
         [0030]     (b) Interval analysis: Compute some safe intervals inside which the value of variables lie at a program location.  
         [0031]     (c) Octagon analysis: What are the bounds on the pairwise differences of variables.  
         [0032]     (d) Pointer analysis: What memory locations can a particular pointer point to at some program location.  
         [0033]     In general, answering these questions exactly is not possible because of undecidability. Therefore, we seek sound (conservative) answers. A sound answer to a data flow problem is one which takes into account every possible real program behaviour and more (some behaviors may be spurious).  
         [0034]     Example:  
         [0035]     (a) Interval analysis: Suppose variable x actually lies in the interval [0,100], it is sound for our interval analysis to infer that x lies in the interval [−100,101]. But it is *unsound* to infer that x lies in the interval [0,50], because in reality, the program may actually exhibit the value 100 which our analysis does not take into account.  
         [0036]     (b) Pointer analysis: A sound pointer analysis should include all the memory locations that a pointer may actually point to. It may include other locations too.  
         [0037]     A key metric for dataflow analysis algorithm is their precision. The precision of an analysis is measured by how close the answer comes to being as exactly as possible.  
         [0038]     Example:  
         [0039]     Interval analysis: The least precise interval that holds trivially is that a variable can have any possible value in the interval [−infinity, infinity]. Such an interval is computed trivially and is useless for all practical purposes. The most precise interval cannot be computed by an algorithm due to undecidability. In practice, we try to approach as close to this most precise interval as possible, but remaining sound at the same time.  
         [0040]     Data flow analysis problems may be classified in many ways:  
         [0041]     (a) Flow-sensitive/insensitive dataflow:  
         [0042]     A flow sensitive dataflow algorithm computes different facts at different locations of the program. On the other hand, a flow-insensitive algorithm computes one single fact that holds true for the program as a whole, regardless of where the control resides.  
         [0043]     (b) Context-sensitive/insensitive:  
         [0044]     When a program is executed, we define the current context of a program as a sequence of function calls from the main function that leads us to the current program point. A context sensitive dataflow algorithm tracks different contexts (function calls) by which a particular program point may be reached. The results of such an algorithm are predicated by what context a location is reached in.  
                                                                                                                                                                                               int f(int x){                print(x); /*--                context: main --&gt; g --&gt; f, fact: x = 0 ,           context: main --&gt; h --&gt; f, fact: x = 2                --*/                }           int g(int x){                f(x); /*-- context: main --&gt; g: fact: x = 0 --*/                }           int h(int x){                f(x+1); /*-- context: main ---&gt; h: fact: x =1 --*/                }           int main(int x){                if (x == 0)                g(x);                if (x == 1)                h(x);                return;                }                      
 
         [0045]     (c)Path-sensitive/insensitive: The analysis is sensitive to some aspects of the path taken to reach a location.  
         [0046]     Example:  
                                                                                                                                   int y;           if (x &gt; 0) /*-- branch B1 --*/                y=0;                else                y=1;                Path insensitive interval analysis will infer                y in [0,1]                Path sensitive interval analysis:                branch B1, then branch --&gt; y in [0,0]                branch B1, else branch --&gt; y in [1,1]                      
 
         [0047]     Perfect path sensitivity is very hard to achieve (expensive) in practice. Therefore, practical path sensitive algorithms may be partially path sensitive. That is, they may be sensitive to some aspects of the path while insensitive to others.  
         [0048]     Note: Path/context sensitivity are independent in practice. We may have context insensitive algorithms that may be partially path sensitive. We may have a context sensitive algorithm that is path sensitive. But a perfect path sensitive algorithm is always context sensitive.  
         [0049]     By way of additional background, it is noted that path-sensitivity is one significant drawback associated with static analysis techniques. And while path-insensitive static analysis techniques are more scalable, this scalability comes at the cost of accuracy, i.e., the analysis produces a number of false alarms.  
         [0050]     With initial reference to  FIG. 1 , there is shown a flow diagram of a simple program. As can be observed, the invariants computed by a simple flow-sensitive but path-insensitive linear relations analysis are shown next to each node (in dotted boxes). A path insensitive-analysis merges the data-flow information at node A, thereby missing the relation between the values of I, X at this point. Such an analysis may not be able to prove the safety of the array access A[X]. Thus, we need to consider analysis using a disjunction of data-flow predicates at each program location. There are at least two distinct approaches to this problem.  
         [0051]     Powerset Extensions  
         [0052]     Powerset extensions of a base domain enrich the domain by considering disjunctions of the domain objects as the new data flow objects. The domain operations on such extensions can be defined readily in terms of the operations on the base domain. Widening operations on this domain can also be defined in terms of the extensions on the base-domain objects.  
         [0053]     The advantage of a powerset extension is that it can be done independently of the base domain. On the other hand, powerset extensions are practically expensive. For numerical domains such as octagons and polyhedra, program analysis using these extensions are exponentially more expensive than in the base domain. Furthermore, the requirement of widening to enforce termination means that heuristic operators are required over the base domain widening. The impact of these operators on the precision of the analysis are not well characterized. For instance, a powerset extension of the polyhedral domain analyzes the program of  FIG. 1  by not merging the data flow objects incoming at the join point A.  
         [0054]     Trace Partitioning Techniques  
         [0055]     Trace partitioning techniques are aimed at performing a flow-sensitive analysis using the base-domain operations. Such algorithms typically associate multiple abstract objects with each CFG location. Each object carries some trace information on the paths that were used to create them. In order to limit this complexity, these objects may be merged heuristically, merging the historical trace information associated with them. Approaches that fall in this category typically differ in their use of heuristics.  
         [0056]     According to the present invention, we show a connection between the result of a static analysis on any powerset extension to the result of the static analysis carried out in the base domain on an “elaboration” of the CFG. As a result, we show that the design of the powerset extension can be thought of as the design of the elaboration scheme.  
         [0057]     We demonstrate an analysis method that creates the elaboration hand-in-hand as it carries out the analysis on the base-domain. The advantage of the elaboration based approach is that it gives a connection between the semantic connection between the disjuncts in a power-set domain an the syntactic connections between them in a trace-partitioning scheme. Furthermore, since the notion of an elaboration is more general than a trace partitioning, it provides more freedom in the design of the analysis.  
         [0058]      FIG. 2   a  shows a flow diagram of the program of  FIG. 1  with an elaboration of the flow diagram ( FIG. 2   b ). Note that a base domain analysis on the elaboration of the flow diagram may prove the safety of the array access to A.  
         [0059]     With reference to  FIG. 3 , there is shown a flow diagram depicting the fixed point obtained on a powerset extension. Note that the presence of the disjoint at point A enables the analysis to prove freedom from overflows. Also note that the elaboration shown is implicit in the source of the disjuncts—which are shown in dotted lines.  
         [0060]     In describing the present invention, we first present basic notions of abstract interpretation and the polyhedral domain, which is used as the representative numerical domain.  
         [0000]     Programs and Invariants  
         [0061]     Since we focus on static analysis over numerical domains, we may regard programs as purely ranging over integer or real-valued variables. Accordingly, we let V={x 1 , . . . , X n } denote integer-valued program variables, collectively referred to as {right arrow over (x)}. The program operations over these variables include numerical operations such as addition and multiplication.  
         [0062]     We assume first-order predicates over the program state belonging to an appropriate language. Given such a predicate ψ, the set of valuations to {right arrow over (x)} satisfying is denoted [[ψ]]. A program is represented by its Control-flow graph (CFG).  
         [0063]     Def. 2.1 (Control-flow Graphs (CFGs)). Formally, a CFG is a tuple Π:(V,L,T,l 0 ,Θ): 
    L: a set of locations (cutpoints);     T: a set of transitions (edges), where each transition τ: l 1 →l j  is an edge between the pre-location l i  and a post-location l j . Each transition models the changes in the values of program variables using guards and updates.     l o ∈L: the initial location; Θ is an assertion over {right arrow over (x)} representing the initial condition.    
 
         [0067]     A state s of the program maps each variable x i  to an integer value s(x i ). Let Σ denote the set of program states. An assertion ψ over {right arrow over (x)} is an invariant of a CFG at location l if and only if it is satisfied by every state reachable at l. An assertion map associates each location of a CFG to predicate. An assertion map η is invariant if η(l) is an invariant, for each l∈L. The (concrete) post condition post Σ (φ,τ) of an assertion φ across a transition τ models the effect of executing τ on each state satisfying φ. Invariants are established using known inductive assertions method [See, e.g., Manevich, R., Sagiv, S., Ramalingam, G., and Field, J. Partially disjunctive heap abstraction. In Static Analysis Symposium (SAS) (2004), vol. 3148 of LNCS, Springer-Verlag, pp. 265-279].  
         [0068]     Def. 2.2 (Inductive Assertion Maps). An assertion map η is inductive if an only if it satisfies the following conditions:  
         [0069]     Initiation: Θ                     
         [0070]     Consecution: For each transition τ: l i           l j ,  
         [0071]     post Σ             
         [0072]     It is well known that any inductive assertion map is invariant. However, the converse need not be true. The standard technique for proving an assertion invariant is to find an inductive assertion that strengthens it.  
         [0073]     Abstract Interpretation  
         [0074]     Abstract interpretation [See, e.g., Cousot, P., and Cousot, R. Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM Principles of Programming Languages (1977), pp. 238-252] is a generic technique for computing inductive assertions of CFGs using an iterative process. In order to compute an inductive map, we start from an initial map and repeatedly weaken the predicates mapped at each location to converge to a fixed point. The assertions labeling each location can be shown to be inductive when the fixed point is reached.  
         [0075]     Abstract Domain.  
         [0076]     In order to carry out an abstract interpretation, we define an abstract domain along with some operations on the elements of the abstract domain known as the domain operations. Informally, an abstract domain is a lattice of predicates Γ over the program state including the assertions T and ⊥ representing true and false respectively. The domain is defined by the abstract lattice           and the concrete lattice of sets of program states ordered by inclusion z, 4  along with the abstraction function α:2 Σ           Γ and the concretization (or the meaning) function γ:Γ         →2 Σ . A key requirement is that α,γ form a Galois connection (see [6, 8] for comprehensive surveys). The abstract domain operations include:  
         [0077]     Join Given abstract objects d 1 , . . . , d m , we construct an abstract object d:d 1 ␣ . . . ␣d m  such that d i           d.  
         [0078]     Meet (Intersection) Given abstract objects d 1 , . . . , d m , we construct an object d:d 1            . . .          d m  such that d         d i , 1≦i≦m.  
         [0079]     Post-Condition Given an abstract object d and a transition τ, we compute its abstract condition d′: post Γ (d,τ) such that
 
post Σ (γ(d),τ)         γ(d′).
 
         [0080]     Note that if the domain is clear from context, we drop the subscript from the post-condition.  
         [0081]     Inclusion Test Given objects d 1  and d 2 , decide if d 1           d 2 .  
         [0082]     Widening Given abstract d 1 , d 2  such that d 1           d 2  their widening d:d 1 ∇d 2  over-approximates the join operation, i.e., d 1 ␣d 2           d. Furthermore, repeated applications of widening on an increasing sequence of abstract objects, guarantees convergence to a fixed point in a finite number of iterations. Other operations of interest include projection, which is commonly used to eliminate variables that are out of scope in the interprocedural analysis.  
         [0083]     Forward Propagation. An abstract assertion map η:L         Γ labels CFG location l with an abstract object η(l)∈Γ. An abstract assertion map η is inductive iff the map           is an inductive assertion map. Given a CFG Π along with an abstract domain Γ, forward propagation seeks to construct an inductive abstract assertion map, iteratively as follows:  
         [0084]     Initial Step The initial map η (0)  is defined as follows:  
           η     (   0   )       ⁡     (     l   0     )       =     {           Θ   ,     l   =     l   0                   ⊥     ,   otherwise                   
 
         [0085]     Iterative Step The iterative step computes the join of the current assertion at a location           with the post-condition of all its incoming transitions.  
           η     (     i   +   1     )       ⁡     (   ℓ   )       =         η     (   i   )       ⁡     (   ℓ   )       ⊔     
     ⁢     ⊔       T   j     :       l   j     →   ℓ         ⁢         post   Γ     ⁡     (         η     (   i   )       ⁡     (     ℓ   j     )       ,     τ   j       )       .           
 
         [0086]     For convenience, we denote this as           Note that ℑ is monotonic w.r.t          , i.e.,           for all            
         [0087]     Convergence Convergence occurs if           for each l∈L .  
         [0088]     Given an initial map           until convergence           Such a map is a fixed point w.r.t           It can be shown that a fixed point map is also inductive. Hence, if the forward propagation converges, its results in an inductive assertion at each cutpoint. Convergence is guaranteed in finitely many iterative steps if the domain sastifies the ascending chain condition. Examples of such domains include finite domains and notably the domain of linear equalities. On the other hand, domains such as intervals and polyhedra do not satisfy this condition. Hence, the widening operation ∇ is used repeatedly to force convergence in finitely many steps.  
         [0089]     Numerical Domains.  
         [0090]     Numerical domains such as intervals, octagons and polyhedra reason about the values of integer or real-valued program variables. These domains are widely used to check programs for buffer-overflows, null pointer dereferences, division-by-zero, floating point instabilities [See, e.g., Cousot, P., and Cousot, R. Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM Principles of Programming Languages (1977), pp. 238-252].  
         [0091]     The interval domain consists of interval predicates of the form          ∈[l i , u i ,] with the possibility of open intervals. The complexity of the domain operations is linear in the number of variables. Analysis techniques for this domain have been widely studied. The octagon domain due to Miné consists of assertions of the form          ±x i ±x j ≦c along with interval constraints over the variables. The nature of the constrains in this domain permits a graphical representation and the computation of many domain operations using the shortest path algorithm as a primitive. The operations in this domain are at most cubic in the number variables. The polyhedral domain consists of convex polyhedra over the program variables represented by the constrains of the form          +α 1 x 1 + . . . +α n x n ≧0. Domain operations over this domain are expensive (exponential space in the size of the polyhedra). However, relaxations of the operations and the structure of the constraints in the domain can yield polynomial time approximations to these operations [See, e.g., Cousot, P., and Halbwachs, N. Automatic discovery of linear restraints among the variables of a program. In ACM POPL (January 1978), pp. 84-972].  
         [0092]     One of the key properties of these domains is that of convexity which limits the ability of these domains to represent sets of states. For instance, a convex numerical domain over x 1 ,x 2  including points A and B, representing program states necessarily includes states that lie on the line joining these two points. Such a drawback leads to cases wherein the domain is unable to compute an invariant that proves the property of interest.  
         [0093]     Example 2.1.  FIG. 1  shows a simple program that checks for a condition, storing its result in a variable x. Later that result is used in lieu of check the condition again. The table to the right shows the invariants computed after each labeled location. Note that the invariant i≦10, required L 4  to prove the absence of overflows, cannot be established. Even though the program is free from overflows, convex numerical domains will not be able to establish the required invariants to prove correctness.  
         [0094]     On the other hand, convexity is desirable since it makes the domain operations tractable. The problem can be avoided using powerset extensions.  
         [0095]     Powerset Extensions  
         [0096]     Given a base abstract domain of predicates, a powerset extension of the domain consists of disjunctions of the base domain predicates. Assume the concrete domain           consisting of subsets of program states along with a base abstract domain           and functions α,γ representing the abstraction and concretization. We shall assume that all the domain operations are computable in the base domain.  
         [0097]     Def. 3.1 (Powerset extension). A powerset extension of an abstract domain           is given by the domain           such that
 
{circumflex over (Γ)}={ S =           d   i   ∈Γ, m≧ 0}.
 
         [0098]     Without loss of generality, we may require that the domain be redundancy free, i.e., no disjuncts in a predicate is subsumed by any other disjuncts. Formally, for any set S∈{circumflex over (Γ)}
 
(∀, d   2   ∈S )( d   1   ≠d   2 )         ( d   1             d   2 ).
 
         [0099]     The concretization function {circumflex over (γ)} for a powerset extension is defined as           The ordering relation           may be defined in many ways to derive different extensions. However, any such definition needs to be faithful to the semantics induced by {circumflex over (γ)}, i.e. if S 1           S 2  then {circumflex over (γ)}(S 1 )         {circumflex over (γ)}(S 2 ).  
         [0100]     Extending Partial Orders. The natural powerset extension is obtained by considering           such that S 1             N S 2  iff {circumflex over (γ)}(S 1 )         {circumflex over (γ)}(S 2 ). This is the partial order induced by the concrete domain on the abstract domain through {circumflex over (γ)}. The Hoare powerset extension            P  is a partial order defined as follows:            
         [0101]     Informally, we require that every object in S 1  be “covered” by some object in S 2 . This can be refined to yield a Egli-Milner type partial order            EM.    
         [0102]     S 1           S 2           S 1 =Ø or (S 1             P S 2  and (∀d 2 ∈S 2 )(∃d 1 ∈S 1 )d 1           d 2 ).  
         [0103]     In addition to S 1           S 2 , each element in S 2  must cover some element in S 1 .  
         [0104]     Example 3.1. Consider the interval domain           over variables x 1 ,x 2 . Let S 1 ={φ 1 :x 1 ∈[0,1]} and S 2 =         :x 1 ∈[−1,½]}, it is easily seen that S 1           S 2 , however S 1            (not) pS 2  since each element of S 2  is incomparable with the element in S 1 .  
         [0105]     On the other hand let S 3 ={ξ 1 :x 1 ∈[0,2],ξ 2 :x 1 ∈[−1,0]}. Note that S 1           pS 3  since φ 1           ξ 1 . On the other hand ξ 2  does not cover any object in S 1 , hence S 1            (not)  EM S 3 .  
         [0106]     Consider the interval domain           of conjunctions of closed, open and half open intervals over the program variables and its natural powerset extension           It is computationally hard to decide the           relation.  
         [0107]     Theorem 3.1. Given S 1 ,S 2 ∈Î, deciding if S 1           S 2  is so co-NP-hard.  
         [0108]     Proof. We perform a reduction from the problem of proving universality of DNF formulas. We introduce one variable x i  corresponding to each position p i . The literal p i  is represented by the predicate x i ∈[0,∞) and           by x i ∈(−∞,0). Each DNF clause translates into an interval domain predicate          ∈         . Therefore the validity of the propositional formula can be reduced to checking the inclusion {T}         {T(D 1 ), . . . ,T(D m )} wherein T(D i ) represents the interval predicate modeling the DNF clause D i .  
         [0109]     The hardness of           extends to natural powerset extensions of most numerical domains and many non-numerical domains that are sufficiently powerful to enable the translation above. Other partial orders           and           are easier to compute using O(|S 1 |+|S 2 |) 2  many base domain           comparisons.  
         [0110]     The domain operation is a powerset domain can be defined by suitably lifting the base domain operations. Notably, the join operation in a powerset domain reduces to a set union. The meet operation S 1           S 2  is given by the pairwise meet of elements from S 1 ,S 2 . Post condition is computed element-wise; i.e., if S={d 1 , . . . , d k }∈           
         [0111]     {circumflex over (post)}(S,τ)={post(d 1 ,τ), . . . , post(d k ,τ)}.  
         [0112]     Widening operations can be obtained as extensions of the widening on the base domain using carefully crafted strategies. Such operators over powerset extensions of numerical domains widen over the           ordering. Thus, even if a domain were designed to use joins over the           ordering, the final fixed point could be obtained by using the           or the           ordering.  
         [0113]     Example 3.2. Consider the program below:  
                                                                       s := −1           while... do                s := −s{invariant : (s = 1           s = −1)}                end while                      
 
         [0114]     The invariant s=1 v s=−1 is a fixed point in the powerset extension of the interval domain using the           ordering.  
         [0115]     CFG Elaboration  
         [0116]     We now prove a simple connection between the fixed point obtained on a domain           using the forward propagation on a CFG Π and the fixed point in the base domain using the notion of an “elaboration”. Intuitively, an elaboration of CFG replicates each location of the CFG multiple times. Each such replication preserves all the outgoing transitions from the original location.  
         [0117]     An elaboration of a CFG C is another CFG E. That is to say, for each node c present in C, there are some replications in E. This is shown schematically in  FIG. 5   a.    
         [0118]     Continuing, and with particular reference to  FIG. 5   b , forall c→d in C and for each replication c′ in E, there is an edge c′→d′ such that d′ replicates d  
         [0119]     Def. 3.2. Consider CFGs Π e :          and Π           over the same set of variables V. The CFG Π e  is an elaboration of Π iff there exists a map p:L e           L such that 
    The initial location in Π e  maps to the inital location of Π:               Consider locations          Π and           such that           For each outgoing transition           there is an outgoing transition           such that p(m e )=m.    
 
         [0122]     Each          ∈L e  is said to be a replication of p         ∈L . Note that every outgoing transition of p          is replicated in           We denote the replication of the transition           starting from           as           An elaboration resembles a (structural) simulation relation between Π e  and Π.  
         [0123]     Example 3.3.  FIG. 5  shows a CFG Π from Example 3.2 along with an elaboration. The dashed line shows the relation p.  
         [0124]     We shall now prove that every fixed point assertion on a powerset domain           on a CFG Π corresponds to a fixed point in the base domain           on some elaboration Π e  and vice-versa.  
         [0125]     Def. 3.3 (Collapsing). Let η e :L e           Γ be a fixed point map on the elaboration Π e  in the base domain. Its collapse C(η e ) is a map on the original CFG, L         {circumflex over (Γ)} such that for each            
         [0126]     z, 69   
         [0127]     The collapsing operator computes the disjunction of the domain objects at each replicated location.  
         [0128]     Lemma 3.1. If η e  is a fixed point for Π e  in the domain Γ then C(η e ) is a fixed point map for Π in the domain {circumflex over (Γ)}.  
         [0129]     Proof. (Sketch) For convenience we denote η e =C(η e ). It suffices to show initiation           and consecution for each transition          , we require           Initiation is obtained by nothing that initial states must be replicated in an elaboration. Expanding the definition for LHS,  
                   post     ⁡     (         η   c     ⁡     (     ℓ   i     )       ,   τ     )       =       post     ⁡     (       {           η   e     ⁡     (     ℓ   e     )       ❘     p   ⁡     (     ℓ   e     )         =     ℓ   i       }     ,   τ     )                   =     {     post   ⁡     (     {         η   e     ⁡     (     ℓ   e     )       ,       τ   ❘     p   ⁡     (     ℓ   e     )         =     ℓ   i         }     )                 ⁢               
 
         [0130]     Similarly the RHS is expanded           In order to show the containment, note that an elaboration requires that           should be an outgoing transition fore each replication l ie  with           with           Using the fact that η e  is a fixed point map, we note that each element           on the LHS is contained in the element           from the RHS.  
         [0131]     Conversely, the fixed point in           induces an elaboration of the CFG.  
         [0132]     Def. 3.4 (Induced Elaboration). Let           be a fixed point map for Π in the domain           Such a fixed point induces an elaboration Π e  and an induced map η e  defined as follows: 
    Locations: Let          ={d 1 , . . . , d m }. The elaboration contains replicated locations          , . . . ,          ∈L e , one per disjuncts such that           Further the map               Transitions: For each transition           we require an outgoing transition           for some l. We make this choice directly based on the proof of consecution of η under           Let          ={α 1 , . . . , α m } and η(l j )={β 1 , . . . , β n } (Note that we may represent the empty set equivalently by the singleton {⊥}). The post condition          ={post         |1≦k≦m}. By definition of           order, we require for each           for some 1≦l≦n. As a result, we replicate the outgoing transition           in Π e  to connect           to          . It immediately follows that η e  satisfies consecution for this transition. Not that since this choice is not unique, there may be many induced elaborations.    
 
         [0135]     Example 3.4. The elaboration shown in Example 3.3 is induced by the fixed point shown in Example 3.2.  
         [0136]     Lemma 3.2. Given a fixed point map η c  for Π in the domain           its induced map η e  is a fixed point for the induced elaboration Π e  in the base domain            
         [0137]     Proof The proof follows from the definition above.  
         [0138]     An elaboration Π e  is said to be connected if every location          L e  is reachable from the initial location          . By a process of removing unnecessary disjuncts from a fixed point for the original CFG, it can be shown that the induced elaboration Π e  is connected.  
         [0139]     On-the-Fly Elaborations  
         [0140]     In the previous section, we have demonstrated a close connection between fixed point in a broad class of powerset domains and the fixed point in the base domain computed on a structural elaboration of the original CFG. As a result, analysis in powerset domains can be reduced to the process of an analysis on the base domain carried out on some CFG elaboration. As a caveat, we observe the even though it is possible to find some elaboration that produces the same fixed point as in the powerset extension with some widening operator, an apriori fixed elaboration scheme may not be able to produce the same fixed point on all CFGs.  
         [0141]     In order to realize the full potential of a powerset extension, the process of producing an elaboration of the CFG needs to be dynamic by considering partial elaborations of the CFG as the analysis progresses. Such a scheme can be viewed as a powerset extension wherein the containment relations between the individual disjuncts in a predicate are explicitly depicted.  
         [0142]     The main advantage of such a scheme is the widening on the partially elaborated CFG can be performed by simply using the base-domain widening. Furthermore, the structure of the elaborated CFG can be used to make fine grained optimizations such as avoiding unnecessary widenings on replicated loops by dynamically tracking loop structures. We now consider a scheme for producing elaborations on-the-fly during the analysis process.  
         [0143]     Partial Elaboration A partial elaboration Π e ,U of a CFG Π: L,,          is a tuple consisting of a CFG Π e : L e,e,            and an unresolved set U         L e x of pairs, each consisting of a location from Π e  and a transition from Π. As with a CFG elaboration, each location          Π e  is a replication of some location          Π. Furthermore, for each transition          Π and each          ∈L e  replicating           exactly one of the following holds: 
    There exists a replicated transition          , or else,                  
 
         [0146]     In other words, U contains all the outgoing transitions of Π which have not been replicated in a given location of Π e . A partial elaboration is a (complete) elaboration iff U=Ø. Given a CFG Π, an initial partial elaboration Π e   0  is given by L e   0 ={l 0 }, e =Ø and U={l 0 ,τ|τ:l 0 →l i }; in other words, the initial location of Π is replicated exactly once and all its outgoing transitions are unresolved. Two basic transformations are permitted on a partial elaboration: 
    Location Addition: We add a new location           to L e  replicating some node p         ∈L, i.e., L e =L e            Furthermore, all transitions in outgoing from           are treated as unresolved, i.e,               Transition Resolution: Given a pair           we replicate           in Π e  as           for some replication           of the target location              
 
         [0149]     Our analysis at each stage consists of a partial elaboration Π e   (i) ,U (i)  along with an abstract assertion map η (i) :L e           Γ. Each iteration involves an update to the map η (i)  followed by an update to the partial elaboration.  
         [0150]     Consider an unresolved entry           Its resolution involves the choice of a target node           replicating           Let d:(η (i)            denote the result of the post condition of the unresolved transition. Furthermore, let          ∈=L e  denote the existing replications of the target location           and           denote the k th  disjunct. The choice of a target location for the transition           depends on the post condition d and the assertions d 1 , . . . , d m . The target can either be chosen from the existing target replications           or a new node           can be added as a new replication of the target. We shall assume a merging heuristic MergeHeuristic (d, d 1 , . . . , d m ) to compute the index i s.t. 1≦i≦m+1 for the target location of the transition.  
         [0151]     Formally, at each step we first update the map η (i) =(η (i−1)  as described in Section 2. The partial elaboration Π e   (i) , U (i)  is then refined by first choosing an unresolved pair           and then applying a merging heuristic
 
z, 134  =MergeHeuristic         replicates         
 
         [0152]     The transition           is resolved as a result, and the entry           is removed from U (i) . If the merging heuristic results in a new location           then new entries are added to U (i)  to reflect unresolved outgoing transitions from the newly added location. If there are no more unresolved pairs in U (i+1) , the partial elaboration is also a full elaboration. Thenceforth, the map η is simply propagated on this elaboration until fixed point is reached.  
         [0153]     Upon termination, we guarantee that U (i) =Ø, i.e., the partial elaboration is a full elaboration and the map η (i)  is a fixed point map on this elaboration. Termination of the scheme depends mainly on the nature of the merging heuristic chosen. Since a transition from U is resolved at each step, termination is guaranteed as long as the creation of new locations ceases at some point in the analysis. A simple way to ensure this requirement is to bound the number of replications of each location to a prespecified limit K&gt;0.  
         [0154]     Merging Heurstics  
         [0155]     Formally a merging heuristic MergeHeuristic (d, d 1 , . . . , d m ) chooses an index 1≦i≦m+1≦K in order to compute the join d i           d if i≦m or create a new location in the partial elaboration as described above. The key goal of a merging heuristic is that the resulting join add as few extraneous concrete states as possible. Such extraneous states arise since the join is but an approximation of the disjunction of concrete states: γ(d 1 )∪γ(d 2 )         γ(d 1 ␣d 2 ).  
         [0156]     In numerical domains, the states of the program can be viewed as points in n. It is possible to correlate the extraneous concrete states with a distance metric on the abstract objects. Let k(d,d′) be a distance metric defined on Γ and α∈ be a distance cutoff. Let d min =argmin{k(d,d 1 )|1≦i≦m} be the “closest” abstract object to d w.r.t k. The merging heuristic induced by k,α is defined as  
         MergeHeuristic   ⁡     (     d   ,     〈       d   1     ,   …   ⁢           ,     d   m       〉       )       =           ⁢     {             d     m   +   1       ,     m   &lt;     K   ⁢           ⁢   and   ⁢           ⁢     k   ⁡     (     d   ,     d   min       )         ≥   α                   d   min     ,     m   =       K   ⁢           ⁢   or   ⁢           ⁢     k   ⁡     (     d   ,     d   min       )         &lt;   α                     
 
         [0157]     In other words, a new location is spawned whenever it is possible to do so (i.e., m&lt;K) and the closest object is farther than a apart in terms of distance. Failing these, the closest object is chosen as the target of the unresolved transition. The cutoff α ensures that the newly formed disjuncts are initially well separated from the others in terms of the metric k .  
         [0158]     The Hausdorff distance, is a commonly used measure of distance between two sets. Given          , their Hausdorff distance is defined as
 
Hausdorff         
 
         [0159]     While such metrics provide a good measure of the accuracy of the join, they are hard to compute. We shall use a range-based Hausdorff distance metric.  
         [0000]     Range Distance Metric  
         [0160]     Let x 1 , . . . , x n  be the program variables and d 1 ,d 2  be abstract objects. For each variable x i , we shall compute ranges  1 :[p 1 ,q 1 ] and  2 :[p 2 ,q 2 ] of the values of x i . Such ranges may be efficiently computed for most numerical domains including the polyhedral domain by resorting to linear programming. The ranges are said to be incompatible if one of the two intervals is open in a direction where the other interval is closed, i.e., their Hausdorff distance is unbounded (∞). If the ranges are compatible, the Hausdorff distance is computed based on their end points. The overall distance is a lexicographic tuple m,s where m is the number of dimensions along which d 1 ,d 2  have incompatible ranges while s is the sum of the distances along the compatible dimensions.  
         [0161]     Consider the polyhedra p 1 :1≦x≦5Λy≧0 and p 2 :−1≦y≦1Λ10≦x≦20. The ranges along x, [1,5] and [10,20] have a Hausdorff distance of 9. On the other hand the ranges along y are [0,∞) and [−1,1] are incompatible. The overall distance between p 1 ,p 2  is therefore (1,9).  
         [0162]     Widening.  
         [0163]     Widening is applied to loops formed on the partial elaboration of the CFG by identifying cutpoints, i.e., a set of CFG locations that cut every loop in the CFG. Note that any loop in the partial elaboration results from a loop in the original CFG: If C e  be a loop in a partial elaboration Π e , then p(C e ) is a loop in the original CFG. The converse is not true. Therefore, not all loops in a CFG be replicated as a loop in the partial elaboration. However, once a loop is formed in a partial elaboration, it remains a cycle regardless of the other edges or locations that may be added to it. Furthermore, the post condition computed along such new edges can only accelerate the termination once the widening phase has begun. These observations can be used to simplify the use of widening to that on the base domain, to reuse widening strategies available on the base domain to partial elaborations and finally, to limit the number of applications of widening. This is one of the key advantages of maintaining structural connections among the disjuncts in terms of a partial elaboration.  
         [0164]     At this point, while we have discussed and described our invention using some specific examples, those skilled in the art will recognize that our teachings are not so limited. Accordingly, our invention should be only limited by the scope of the claims attached hereto.