Join us on:

Static Analysis and Types

Session Chair: Erik Ernst, Aarhus University
Strictly Declarative Specification of Sophisticated Points-to Analyses
Martin Bravenboer, University of Massachusetts, Amherst
Yannis Smaragdakis, University of Massachusetts, Amherst

We present the DOOP framework for points-to analysis of Java programs. DOOP builds on the idea of specifying pointer analysis algorithms declaratively, using Datalog: a logicbased language for defining (recursive) relations. We carry the declarative approach further than past work by describing the full end-to-end analysis in Datalog and optimizing aggressively using a novel technique that takes into account Datalog incremental evaluation.

As a result, DOOP achieves several benefits, including stunning (full order-of-magnitude) improvements in runtime. We compare DOOP with Lhotak and Hendren's PADDLE, which defines the state of the art for context-sensitive analyses. For the exact same logical points-to definitions (and, consequently, identical precision) DOOP is more than 15x faster than PADDLE for a 1-call-site sensitive analysis of the DaCapo benchmarks, with lower but still substantial speedups for other important analyses. Additionally, DOOP scales to very precise analyses that are impossible with PADDLE and Whaley et al.'s bddbddb, directly addressing open problems in past literature. Finally, our implementation is modular and can be easily configured to analyses with a wide range of characteristics, largely due to its declarativeness.

Self Type Constructors
Chieri Saito, Kyoto University
Atsushi Igarashi, Kyoto University

Bruce and Foster proposed the language LOOJ, an extension of Java with the notion of MyType, which represents the type of a self reference and changes its meaning along with inheritance. MyType is useful to write extensible yet typesafe classes for objects with recursive interfaces, that is, ones with methods that take or return objects of the same type as the receiver.

Although LOOJ has also generics, MyType has been introduced as a feature rather orthogonal to generics. As a result, LOOJ cannot express an interface that refers to the same generic class recursively but with different type arguments. This is a significant limitation because such an interface naturally arises in practice, for example, in a generic collection class with method map(), which converts a collection to the same kind of collection of different elements. Altherr and Cremet and Moors, Piessens, and Odersky gave solutions to this problem but they used a highly sophisticated combination of advanced mechanisms such as abstract type members, higher-order type constructors, and F-bounded polymorphism.

In this paper, we give another solution by introducing self type constructors, which integrate MyType and generics so that MyType can take type arguments in a generic class. Our solution is simpler—it uses only first-order type constructors and neither abstract type members nor F-bounds. We demonstrate the expressive power of self type constructors by means of examples, formalize a core language with self type constructors, and prove its type safety.

Profile-Guided Static Typing for Dynamic Scripting Languages
Michael Furr, University of Maryland, College Park
Jong-hoon (David) An, University of Maryland, College Park
Jeffrey S. Foster, University of Maryland, College Park

Many popular scripting languages such as Ruby, Python, and Perl include highly dynamic language constructs, such as an eval method that evaluates a string as program text. While these constructs allow terse and expressive code, they have traditionally obstructed static analysis. In this paper we present PRuby, an extension to Diamondback Ruby (DRuby), a static type inference system for Ruby. PRuby augments DRuby with a novel dynamic analysis and transformation that allows us to precisely type uses of highly dynamic constructs. PRuby's analysis proceeds in three steps. First, we use run-time instrumentation to gather per-application profiles of dynamic feature usage. Next, we replace dynamic features with statically analyzable alternatives based on the profile. We also add instrumentation to safely handle cases when subsequent runs do not match the profile. Finally, we run DRuby's static type inference on the transformed code to enforce type safety.

We used PRuby to gather profiles for a benchmark suite of sample Ruby programs. We found that dynamic features are pervasive throughout the benchmarks and the libraries they include, but that most uses of these features are highly constrained and hence can be effectively profiled. Using the profiles to guide type inference, we found that DRuby can generally statically type our benchmarks modulo some refactoring, and we discovered several previously unknown type errors. These results suggest that profiling and transformation is a lightweight but highly effective approach to bring static typing to highly dynamic languages.

Please email any questions to . This e-mail address is being protected from spambots. You need JavaScript enabled to view it