Modular and field-sensitive termination analysis of java bytecode

Resumen

Static program analysis of object-oriented languages poses some challenges for termination analyzers. One of these challenges is that termination analysis traditionally requires the use of global analysis techniques to prove that the execution of an entry method terminates for any input value. In order to solve this problem, it is necessary to prove termination for all methods invoked from the entry method during its execution. Scalability is an important disadvantage of global analysis, especially in memory consumption, because it needs to analyze over and over again the whole code even if there is a small part modified. It also requires to have the code available, of all methods reachable from the method being analyzed. Some techniques developed to provide a modular termination analysis of a Java program, are presented in an approach that allows a high level of scalability, granularity and reusability to perform termination analysis of incomplete code. This approach is able to decompose large programs into small parts and can reuse previous analysis results. Also it allows reusability and scalability through the use of assertions, to store the analysis results obtained by analyzing a method at a time. Then the assertions generated are applied to the analysis of subsequent methods. Most static analyzers do not keep track of object fields, because they are field-insensitive. This type of analysis produces too imprecise results whereas applying only field-sensitive analysis is computationally intractable. There has been significant interest in developing techniques that result in a good balance between the accuracy of analysis and its associated computational cost. To solve this challenge, an implementation of field-sensitive analysis performed on object fields is presented. This transformation is based on a context-sensitive analysis that splits a program into fragments, to provide a safe way to replace an object field by a local variable in each fragment. Also using a polyvariant transformation achieves, a very good balance between accuracy and efficiency. The modular and field-sensitive termination analyses were developed, implemented and tested in a COSt and Termination Analyzer of java bytecode(COSTA). An analyzer that receives as entry a method signature and infers termination for all possible input values of its code and related methods. In order to test the applicability of the modular termination framework it has been applied to phoneME core libraries. Based on the implementation of Java Micro Edition (JavaME), that corresponds to the libraries used for developing mobile applications or MIDlets. Also these libraries have been used for estimating execution time of a mobile application, before running it in a specific mobile device. Finally, another contribution of this thesis is the availability of the COSTA system through a web interface, to allow users try out the system on a set of representative examples, and also to upload their own bytecode programs.