11Introduction.tex

\chapter{Introduction}
Shape analysis is an useful tool for many other program analyses such as compiler optimisation~~\cite{6494978}, parallelisation~\cite{sharing-analysis-arrays-collections-recursive-structures}, or termination checking, where the termination of code that uses linked data structures can depend on said data structured being cycle-free.  Existing methods such as in AProVE~\cite{automated-termination-proofs-for-java-bytecode-with-cyclic-data}, Julia~\cite{DBLP:journals/scp/ScapinS14} or COSTA~\cite{GenaimZ13} currently do not perform a modular and path-sensitive type analysis.

We introduce a \emph{reachable type analysis}, a sound interprocedual analysis which for each method generates a \emph{method result} consisting of a \emph{parametric type set} for the return value, each argument and all modified static fields, describing how the reachable types for all affected references change after an invocation of the method. This method result is parametric, meaning that it can then be instantiated with argument type information only when used, allowing for improved locality during analysis in addition to improved performance as each method has to be analysed only once. Furthermore it is possible to access the parametric type set of any local reference or static field at any code location.

Our analysis requires existing path-sensitive heap-shape information and can be used in further analyses, for example by reducing the set of possible concrete targets of a virtual method invoke or disproving the existence of a path from one reference to another. In particular it can then be invoked again on refined heap-shape information to get even more refined types.

In \cref{chap:bg}, we give an overview over the abstract path representation used, our requirements for the heap-shape analysis and Soot~\cite{vallee1999soot}, the framework used for our analysis. \Cref{chap:rta} describes the reachable types of a program at runtime, the structure of our static data-flow analysis in detail, proves its correctness and elaborates how reachable type information can be used to refine heap-shape information.
Finally, \cref{chap:results} compares the quality of dynamic dispatch resolution in the analysis itself with and without refinement. A short overview over related work is given in \cref{chap:related} and areas of improvement are highlighted in \cref{chap:future}.