|
Abstract : |
Abstract. Precise type information is invaluable for analysis and optimization of object-oriented programs. Some forms of polymorphism found in object-oriented languages pose signicant diculty for type inference, in particular data polymorphism. Agesen's Cartesian Product Algorithm (CPA) can analyze programs with parametric polymorphism in a reasonably precise and ecient manner, but CPA loses precision for programs with data polymorphism. This paper presents a precise constraint-based type inference system for Java. It uses Data Polymorphic CPA, a constraint-based type inference algorithm which extends CPA with the ability to accurately and eciently analyze data polymorphic programs. The system is implemented for the full Java language, and is used to statically verify the correctness of Java downcasts. Benchmark results are given which show the system performs very well: it is signi cantly more accurate and is nearly as ecient as CPA. The implementation itself contains a number of novel optimizations which proved necessary to achieve scalability. 1, |
