{'fraction_non_alphanumeric': 0.02985421578720154, 'fraction_numerical': 0.00903264370869724, 'mean_word_length': 4.592200557103064, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
An efficient approach to computing fixpoints for complex program analysis

Abstract interpretation has been widely used for the analysis of object-oriented languages and, in particular, Java source and bytecode. However, while most existing work deals with the problem of finding expressive abstract domains that track accurately the characteristics of a particular concrete property, the underlying fixpoint algorithms have received comparatively less attention. In fact, many existing (abstract interpretation based-) fixpoint algorithms rely on relatively inefficient techniques for solving inter-procedural call graphs or are specific and tied to particular analyses. We also argue that the design of an efficient fixpoint algorithm is pivotal to supporting the analysis of large programs. In this paper we introduce a novel algorithm for analysis of Java bytecode which includes a number of optimizations in order to reduce the number of iterations. The algorithm is parametric -in the sense that it is independent of the abstract domain used and it can be applied to different domains as ''plug-ins''-, multivariant, and flow-sensitive. Also, is based on a program transformation, prior to the analysis, that results in a highly uniform representation of all the features in the language and therefore simplifies analysis. Detailed descriptions of decompilation solutions are given and discussed with an example. We also provide some performance data from a preliminary implementation of the analysis


Introduction
Analysis of the Java language (either in its source version or its compiled bytecode [19]) using the framework of abstract interpretation [8] has been the subject of significant research in the last decade (see, e.g., [20] and its references). Most of this research concentrates on finding new abstract domains that better approximate a particular concrete property of the program analyzed in order to optimize compilation (e.g., [3,31]) or statically verify certain properties about the run-time behavior of the code (e.g., [13,17]). In contrast to this concentration and progress on the development of new, refined domains there has been comparatively little work in the underlying fixpoint algorithms and frameworks. In fact, many existing abstract interpretation-based analyses use relatively inefficient fixpoint algorithms. In other cases, the fixpoint algorithms are specific and/or tied to particular analyses and cannot easily be reused for other domains.
Instead, interesting progress on fixpoint algorithms has been made for example in functional and logic programming, where a number of solutions have been proposed to speed up analysis fixpoint convergence (see, e.g., [24,6,14,29] and its references). However, the formulation of these algorithms is strongly tied to the operational semantics of those languages. As a result, their adaptation to Java and Java bytecode is not straightforward, since fundamental aspects of the semantics of object-oriented programming such as virtual calls, object instantiation, static methods and variables, destructive update, etc. are not dealt with, at least directly.
We argue that the design of an efficient fixpoint algorithm is pivotal to supporting the analysis of large programs. In this paper we propose and describe in detail a novel algorithm for analysis of Java bytecode which includes a number of optimizations in order to reduce the number of iterations as well as other unique characteristics. In particular, dependencies are kept during analysis so that only the really affected parts need to be revisited after a change during the convergence process. The algorithm deals thus efficiently with mutually recursive call graphs. In addition, recomputation is avoided using memoing. The proposed algorithm is parametric in the sense that it is independent of the abstract domain used and it can be applied to different domains. The algorithm specifies a reduced number of basic operations that each domain must implement. This allows having a single implementation to which the designer of new analyses can add new domains as "plug-ins." The algorithm is also multivariant: abstract calls to a given method that represent different input patterns are automatically analyzed separately. This is both more precise and efficient than alternative techniques such as cloning methods for each call site, since cloning can produce either too many versions of methods (if two call sites are determined to use the same input pattern) or too few (if two different, separate input patterns arise from a single call site). The algorithm is also top-down/flow-sensitive, in order to allow modeling properties that depend on the data flow characteristics of the program.
Finally, another interesting characteristic of the algorithm is that it is preceded by a program transformation, prior to the analysis, that results in a highly uniform representation of all the features in the language and therefore simplifies analysis. This program transformation includes a certain level of decompilation of the bytecode which recovers part of the original code structure lost in the bytecode representation. Our decompilation process is based in part on existing tools [23,35] to which we add a number of steps (normalizing the intermediate representation which is actually analyzed, representing different classes of statements in a unified way, automatically introducing relational information between initial and final states on methods calls, etc.) which we argue greatly simplify the burden of designing new analyses and abstract operations. While not the subject of this paper, the algorithm can also be applied to Java source code, applying a similar transformation.
Java programs rely heavily on libraries and analysis thus usually expands to many imported classes. Thus, modular analysis is definitely an important issue in this context. However, and in order to concentrate on the description of the fixpoint algorithm, we will not deal with modular analysis issues in this paper. Instead, we assume that methods exported by libraries are annotated in an assertion language that describes which output abstract states are provided for certain input abstract states (we use a particular assertion language based on [28] but adapted to resemble the Java Modeling Language [16], however we omit also a detailed description of this assertion language from the description for brevity). A solution for modular analysis in the context of Java can be found for example in [27], and, more specifically relevant to our algorithm, in [4,7].
Regarding other related work, as mentioned before, most published analyses based on abstract interpretation for Java or Java bytecode do not provide much detail regarding the implementation of the fixpoint algorithm. Also, most of the published research (e.g., [3,5]) focuses on particular properties and therefore their solutions (abstract domains) are tied to them, even when they are explicitly multipurpose [18]. In [25] the authors mention a choice of several univariant and multivariant computations, but no further information is given. The more recent and quite interesting Julia framework [33] is intended to be generic and targets bytecode as in our case. Their fixpoint techniques are based on prioritizing analysis of non-recursive components over those requiring fixpoint computations and using abstract compilation [15]. However, few implementation details are provided. Also, this is a bottom-up framework, while our objective is to develop a top-down, multivariant framework. While it is well-known that bottom-up analysis can be adapted to perform top-down analyses by subjecting the program to a "magic-sets"-style transformation [30], the resulting analyzers typically lack some of the characteristics that are the objective of our proposal, and, specially, multivariance. Finally, in [21] a generic static analyzer for the modular analysis and verification of Java classes is presented. The algorithm presented is also bottom-up, and only a naive version of it (which is not efficient for mutually recursive call graphs) is presented.

Intermediate program representation
We start by describing the first phase of the analysis: the translation of the Java bytecode into an intermediate representation. In order to concentrate on the fixpoint algorithm, which is the main objective of the paper, this description is summarized, concentrating on the characteristics of the transformation and illustrating it with a relatively complete example (the full description can be found in [22]). The  translation process produces a structured, decompiled representation of the Java bytecode and is based on the SOOT framework [35] which has been successfully used in previous analyses [9,2]. However, instead of analyzing directly the Jimple representation -based on gotos-it is processed further in order to build a control flow graph (CFG) in a similar way to the Dava tool [23]. The idea is also analogous to the approach of [13,33] but the graph obtained is somewhat different since we do not distinguish between stack and local variables, and all the operands are explicit in the expressions. The actual internal representation used is described by the grammar in Fig. 1. 5 In our current implementation we deal only with the fundamental features of the language such as inheritance, virtual calls, and method visibility.
Here and in the rest of the paper, we will denote by V the set of variables in the program and by M the set of method names. The types T of the application include classes K and atomic types. The decompilation process represents methods as OR-tuples (name, f p, k callee , body) ∈ M × P(V × T ) × K × P(Stmt). The domain of OR-tuples is denoted by O and therefore a program P is just an element of P(O). A first key idea in the transformation is to have a single representation for all types of loops, as well as for conditional structures and standard methods, which are all transformed into OR-tuples. For example, an unconditional jump in the bytecode is first decompiled as a conditional block, which is further converted into a "pseudo" method. This label refers to the fact that those methods did not exist in the original bytecode. Given a statement if cond 1 stmt 1 else if cond 2 stmt 2 . . . else stmt n in the context of a class k, n OR-tuples are obtained of the form A second important aspect in the representation of the code is the metainformation stored about it. Although that information could be indirectly retrieved from intermediate data structures, a more convenient approach is to maintain a ta-  ble containing which classes implement which methods, as well as the hierarchy, interface relations, etc. In this way, we can easily determine (for example) the set of classes in which a virtual call might take place without having to resort every time to an abstract syntax tree transversal. A third key idea is to expose the internal structure of the more complex bytecode instructions. Java bytecodes are sometimes high-level instructions that encode relatively complex operations. Instead of delegating the treatment of such complexities to the abstract domain, we make these aspects of the operational semantics explicit in the intermediate representation itself using program transformations as in [13]. In the same way, a pivotal aspect in languages with destructive updates is the stor-age of relational information about the formal parameters in a method invocation, so that on method exit we can distinguish whether the parameter state should be propagated back to the caller or it refers to a new, fresh instance. In [25,32] the solution is based on the framework by altering call semantics. Instead we introduce explicit assignments to temporal variables which are undone at the end of the method's body. We argue that the solutions that we apply result in simple domain implementations (important for our parametric approach), as well as increased portability of the domains: analysis of similar languages (e.g., C#) can (almost) reuse existing abstractions, provided that the compilation phase decompiles in this way the language-dependent features. We also argue that the representation proposed greatly facilitates later analyses. Figure 2 shows three representations of the same code, an alternative implementation of the JDK Vector class. We include the original source in Fig. 2a for better understanding of the example. Figure 2b is the output of the SOOT (de-)compiler, in Jimple format, for the Vector bytecode. Stack and local elements have been converted into named variables and all the expressions are typed, but the presence of gotos complicates later analyses. Meta-information about class hierarchies, overwritten methods, etc. is also implicit in the code.
The data structure that represents the Control Flow Graph that is the input to our fixpoint algorithm is shown in Fig. 2c. The meta-information part (first five lines) states that ZipVector is a direct descendant of the user-defined Vector class. Both implement an add method that receives an Element object and returns nothing. We now focus on the append method. Most of the statements in the Jimple representation are kept in a very similar format (the line numbers will help the reader identify the correspondences) except for gotos and ifs which are now OR-tuples. For example, the if block starting at line 2 corresponds to the two OR-tuples named user:vector:append if00, which have as formal parameters all the variables of the container method because they are referenced in their bodies. The while loop in lines 5-6 is constructed in a similar way, although recursive calls are inserted by the compiler. Space limitations prevent us from showing how the relational information is copied at the beginning and end of every method.

Top-down Approach to Bytecode Analysis
The program transformations of Sect. 2 greatly simplify our bytecode analysis since we only have two possible flows in the CFG: the branching invocations of OR-tuples or serial execution of all other statements. For the first case we will not distinguish in analysis between real (existing in the source) and pseudo (generated via program transformation) methods, which are semantically equivalent. In the event of an invocation i = invoke(mname, ap, k caller) ∈ M × P(V × T ) × K the semantics of both is computed by calculating the least upper bound of the semantics of all possible OR tuples compatible with such invocation: SS invoke(mname, ap, k caller ) σ = ⊔(SS stmt i σ) if (name, f p, k callee , stmt i ) ∈ O and comp(i, o). The function comp returns a boolean value indicating if a particular implementation o = (name, f p, k callee , stmt i ) is compatible with the invocation: i.e., if their names are identical and their signatures and the class where they are 6 defined are compatible according to a partial order for Java classes ≤ T like the one described in [17].
true if name = mname and k caller ≤ T k callee and |ap| = |f p| and ap i .k ≤ T f p i .k i = 1 . . . n f alse otherwise However, this high-level description of the semantics of an invocation does not take into account implementation issues like the particular strategy (bottom-up or top-down) followed or fixpoint calculations. We now develop a refined approach to the problem, which in fact handles the two types of flows in a uniform fashion.
A particularly useful and efficient way of controlling the interpretation process is to follow a top-down strategy starting from the program main entry point and an abstraction of the input data (or a topmost value, if such abstraction is not available). The top-down strategy proposed implicitly creates a graph during analysis where nodes (statements) with several descendants correspond to branches in the concrete execution (conditionals, virtual calls, loops), all of them abstracted as invocations of OR-tuples. Nodes with one descendant indicate serial execution and are abstracted by recursively applying the process to the child node. More precisely, an invocation is an OR-node whose children are the bodies of all the OR-tuples whose signature matches that of the call, and each body is an AND-node where the semantics of each statement (possibly containing further OR-nodes) are composed.
Given a call state CA prior to a statement stmt, the exit state CP is computed by the function SS stmt : D → D, with three subcases: (i) If the statement is a invocation i = invoke(mname, ap, k caller ), let o 1 , . . . , o n be the OR-tuples such that comp(i, o i ) = true. First we restrict the actual state to those variables that are in ap. This is performed by means of the project operation described below and results in a new state λ = CA| ap . The description is further modified to rename the variables so they work in each context of the callee: β i = λ| f p ap . Then we call recursively SS stmt i β i in order to obtain an exit state for the callee β ′ i . Now we proceed in the opposite direction, first by renaming back all variables so that each abstraction is described in terms of the variables in the caller and then by lubbing their partial results: The last step implies conjoining λ ′ with the initial description via the extend operation described below: CP = extend(CA, λ ′ ).
(ii) If the statement is a concatenation of statements {stmt 1 , . . . , stmt n }, the output state is calculated as the composition of the semantics of each element in the list, starting with the initial state: CP = SS stmt n (. . . SS stmt 1 (CA)) (iii) If the statement is atomic (does not include further statements) we have a base case that is resolved directly by the domain: CP = SS stmt (σ i ).
The interprocedural, top-down approach requires the designer of the domain to provide two extra operations in addition to the standard [8] lattice functions such as least upper bound or ordering. The project : D × P(V) → D operator restricts the current abstraction to the set of variables specified. The intuition behind it is the removal of irrelevant information in the actual state, in the sense that it does not relate to the actual parameters of the invocation, reflecting the scoping rules of the blocks being analyzed. The second operation is extend : D × D → D, which updates an abstract state CA based on another description λ ′ that involves only variables in CA. The purpose of extend is somehow symmetric to the projection, because after returning from a method invocation we need to reconcile the result of the call (affecting only a few variables within the scope of the caller) with the previous state (affecting all the variables in such scope).
In the example of Fig. 2c, assume that the actual state before the call to vector:append if00 while00 is CA The extend operation is less straightforward. Assume the existence of a method After analyzing the body of foo the resulting state is λ probably because some field in R 0 has been assigned to R 1 or to any of its non null fields (or vice versa) within the method. The information discovered is propagated back to the caller and, thus, Note that precision can be further improved if, for example, the abstraction captures the run-time class of the objects invoked. Our solution to this issue makes use in the implementation of object orientation by allowing specialization of the base framework through subclassing. For the particular example in hand, domains containing class analysis information [1,10] would just overwrite the implementation of the comp predicate in order to obtain smaller sets of candidate methods to analyze.
In addition to the points above, there is one more issue that needs to be addressed. The overall abstract interpretation framework scheme described works in a relatively straightforward way if the (transformed) program has no recursion (i.e., there are no loops or recursion in the original bytecode). Consider, on the other hand, a recursive OR-tuple. If there are two OR-nodes for the tuple in the tree such that the actual parameters apars and input state CA are identical, and one node is a descendant of the other, then the tree is infinite and analysis does not terminate. In order to ensure termination, some sort of fixpoint computation is needed. This is the subject of the following section.

Generic Top-Down Analysis Algorithm
We now describe our generic top-down analysis algorithm. The algorithm computes the least fixed point making use of memo tables [12,36,11]. A memo table contains the results of computations already performed and it is typically used to avoid needless recomputation. However, in our context it is also used to store results  There are three major subcases. If the statement is an invocation of a non recursive method, AnalyzeNoLoop handles the call. It first checks whether there is an entry in the memo table for the name of the invoked method and its λ. In that case the stored value of λ ′ is immediately passed to the Extend operation to yield the exit state.
Otherwise, the variables of its λ are renamed to the set of variables {R 0 , . . . , R n } and for each method m returned by the Lookup procedure the following actions are carried out: a projection of λ onto the m variables and addition of the variables of Finally, when a method is recursive the fixpoint computation defined by the AnalyzeLoop procedure in Fig 4 is required since analysis needs to be repeated until fixpoint is reached for the abstract and-or tree, i.e., until it remains the same before and after one round of iteration. In order to do this, we keep track of a flag to signal the termination of the fixpoint computation. Firstly, AnalyzeLoop begins analyzing those non-recursive instances of the invoked method in the same way as AnalyzeNoLoop. With this, we are able to yield a possible λ ′ different from ⊥ which will accelerate the further fixpoint computation, and then an entry in the memo table is inserted with this information and characterized as fixpoint. After this, the CompFixpo procedure (also defined in Fig. 4) is called. At each iteration, a similar process to that described in AnalyzeNoLoop is performed. However, between the end of one iteration and the beginning of the next one, the values of the previous λ ′ and the new λ ′ are compared. If they are the same, then fixpoint has been reached and the procedure finishes ensuring that the least fixed point has been computed. Otherwise, the least fixed point has not been reached yet and a new iteration will be performed.
Dealing with Mutually Recursive Methods. For the sake of simplicity, the description of the analysis so far has omitted some details which are needed in order to support mutually recursive methods. In this case, our algorithm operates as follows. Firstly, we need to use new values for the status field in memo table entries. fixpoint is used when the fixpoint has not been reached yet. approximate represents when the fixpoint has been reached for a method m 1 in this entry but by using a possibly incomplete value of λ ′ of some other method m 2 (i.e., a value that does not correspond yet to a fixpoint). Finally, complete is used when fixpoint has been reached for this method. Furthermore, we also need to use the ID field in order to detect occurrences of mutual recursion. We also need to use a set of ID's to keep track of the recursive methods during the analysis. When a fixpoint computation is started, the analysis searches for an entry in the memo table. Given a method and its λ, if there exists an entry characterized as complete, then the λ ′ is obtained from it. If the entry is characterized as fixpoint means that the method is recursive and thus we add its ID in the set of ID's. If the entry is approximate, then the method or one of its successors in the and-or tree has an approximate value of its exit state. Thus, we need to mark it as fixpoint and start its fixpoint computation again. Finally, after a fixpoint computation is reached we need to verify the ID's contained in the set of ID's. If this set contains only the ID corresponding to the method which is being analyzed, then the value of its λ ′ is complete. Otherwise, the method depends on other ID's (i.e., methods) and so, we mark its output abstract value as approximate. In both cases, we eliminate the method's ID from the set of ID's.

Example 4.1
We now illustrate how the fixpoint algorithm described in Sect. 4 works for the program in Fig. 2. The domain used will be pair sharing. The objective is to analyze the semantics of the append method in the context of the Vector and ZipVector classes. Space limitations obviously prevent us from showing the entire process in detail. We will instead assume that the starting program point for analysis is right before var byt var src The invocation is classified as non recursive and handled by AnalyzeNoLoop. We now have to project CA V ector append over the two actual parameters and then rename these to the equivalent formal parameters. 7 Since R 0 is T his and R 1 is V we get λ append = {{R 0 , R 0 } , {R 1 , R 1 }}. To simplify notation we will denote append if00 and append if while00 by if and while respectively. Analysis of the append body results in a call to AnalyzeCond, since the last statement is an invocation to if. At Conditional invocations are simpler to handle: no project, extend, or rename operations are required. Instead, we directly examine the two methods corresponding to if.
The first branch implies that R 2 is null and that a R 0 's field and R 3 point to the vector passed as argument R 1 , The second compatible method with the invocation implies R 2 = null but its semantics depends on a loop call to while.
Control of the algorithm is passed to the AnalyzeLoop subroutine which projects and renames The non recursive part is then analyzed first. Since termination depends on R 4 being null and the final assignment (line 7 in the source) forces R 1 and R 2 to share through intermediate variable R 5 we have λ A new entry e 1 =(while,λ while ,fixpoint,λ ′ while,1 ,id 1 ) is inserted in the memo table.
Fixpoint computation starts by analyzing (recursive) methods that are compatible with the invocation. The only tuple found (last in Fig. 2c) is processed in a straightforward manner until the self-invocation, which triggers a search in the memo table with return value e 1 (AnalyzeLoop subroutine). We use the current approximation of the while semantics, derived from the base case. On return to the fixpoint routine, we will calculate a λ ′ while,2 which is identical to λ ′ while,1 , because the statements in the body of the recursive tuple do not really alter any information about variables in λ while . The relation (λ while , λ ′ while ) did not change after one single iteration and the process can be considered as complete for the while method.  dyndisp  71  68  3  114  30  clone  41  38  3  42  52  dfs  102  98  4  103  68  passau  167  164  3  296  97  qsort  185  142  43  182  125  intgrqsort  191  148  43  159  110  pollet01  154  126  28  276  196  zipvector  272  269  3  513  388  cleanness  314  277  37  360  233 Fig. 6. Analysis times, number of program points, and number of abstract states.
The memo table status of the e 1 tuple is updated accordingly. Coming back to the semantics of the second branch of the if method, we observe that it has to be identical to extend(CA if , λ ′ while,1 ), which forces further sharings with the R 0 object to produce λ . This semantics is congruent with the concatenation that takes place inside the method.
We are now in the position of inferring the abstract semantics of add in class Vector.
Remember If we repeat the process for a call state CA append where T his and V share, CP append will remain the same on exit, but the memo table now contains two entries for the same method reflecting the two different call contexts (multivariance).

Some Experimental Results
We have completed a preliminary implementation of our framework, and coded a pair sharing (P S) analysis extending the operations described in [32] in order to handle some additional cases required by our benchmark programs such as primitive variables, visibility of methods, etc. The benchmarks used have been adapted from previous literature on either abstract interpretation for Java or points-to analysis [32,26,25,34]. Our experimental results are summarized in Fig. 6. The first column (#tp) shows the total number of program points (commands or expressions) for each program. Column #rp then provides, for each analysis, the total number of reachable program points, i.e., the number of program points that the analysis explores, while #up represents the (#tp−#rp) points that are not analyzed because the analysis determines that they are unreachable. Since our framework is multivariant and can thus keep track of different contexts at each program point, at the end of analysis there may be more than one abstract state associated with each program point. Thus, the number of abstract states is typically larger than the number of reachable program points. Column #σ provides the total number of these abstract states inferred by analysis. The level of multivariance is the ratio #σ/#rp. In general, such a larger number for #σ tends to indicate more precise results. The t column in Fig. 6 provides preliminary results regarding running times for the different benchmarks, in milliseconds, on a Pentium III 2.0Ghz, 1Gb of RAM, and averaging several runs after eliminating the best and worst values.

Conclusions
We have presented a novel algorithm for analysis of Java bytecode which includes a number of optimizations in order to reduce the number of iterations. The algorithm is parametric in the sense that it is independent of the abstract domain used. The algorithm is also multivariant and top-down/flow-sensitive. Also, the algorithm uses a program transformation, prior to the analysis, that results in a highly uniform representation of all the features in the language and which simplifies analysis.