Core-Java: An Expression-Oriented Java

Florin Craciun Hong Yaw Goh Corneliu Popeea Wei-Ngan Chin

Department of Computer Science, National University of Singapore
{craciunm,gohhy,corneliu,chinwn}@[Link]

Abstract Core-Java is an expression-oriented language, that makes eas-

A common practice for rapid prototyping of an object-oriented pro- ier the formulation of static and dynamic semantics. Expression
gram analysis is to define a lightweight fragment of Java, that is languages are more suitable for type-based analyses that work on
sufficiently small to facilitate a rigorous analysis of key properties. an abstract syntax tree rather than on a control flow graph. Addi-
Such a lightweight fragment lacks important Java features, thus the tionally, Core-Java language contains constructions that control the
experimental evaluation on real-world code is not easy. The solu- program flow, as well as imperative and object-oriented features.
tion is either to extend the prototype to the whole Java or to rewrite
the real-world code in the lightweight language. We propose an in- 2. Core-Java Language
termediate solution through Core-Java, an expression-oriented core A program P (Figure 1) consists of a set of class and interface
calculus of Java and a comprehensive set of translation rules from declarations, def . The language supports simple inheritance by ex-
Java to Core-Java. The translation can be guided by the specific re- tending a class, but also multiple inheritance through the interface
quirements of each program analysis. We have built an implemen- mechanism.
tation of our framework and have used it for two different analyses
on Java programs.
P ::= package n (import n)∗ def∗
Categories and Subject Descriptors D.3.2 [Programming Lan- def ::= mdf∗ class c1 extends c2 implements c∗ {fld∗ meth∗ }
guages]: Language Classifications—Object-oriented languages | mdf∗ interface c1 extends c∗ {meth∗ }
General Terms Design, Languages τ ::= c | prim | void
fld ::= mdf∗ τ f
Keywords language design, type-based analysis
meth ::= mdf∗ τ mn ((τ v)∗ ) throws c∗ eb
x ::= v | k
1. Introduction
w ::= v | v.f | c.f
We propose a framework for rapid prototyping of various type- ∗
eb ::= {(τ v) e}
based analyses for object oriented languages like Java. Java has a
lot of features, a large syntax with a complicated semantics. Our e ::= k | w | (c)null | eb | () | w = e | e1 ; e2 | (τ )v
| [Link](x∗ ) | [Link](x∗ ) | new c(x∗ ) | if x then e1 else e2
framework consists of a minimal core calculus for Java, called | return x | continue | break | while x eb
Core-Java and set of rules that permit a type-based source-to- | throw v | try e catch (c v eb)∗ | synchronized v in e
source transformation of Java programs into Core-Java programs. v ∈ variable names c ∈ class or interface names
Core-Java is designed in the same minimalist spirit as the pure f ∈ field names mn ∈ method names
functional calculus, Featherweight Java [8], but it incorporates im- k ∈ constants prim ∈ primitive types
perative features as Middleweight Java [1], and concurrent features n ∈ package names mdf ∈ modifiers (e.g. static, public, etc.)
as the small multithreaded calculus, Concurrent Java [6]. In contrast
to the main motivations of these proposals, we are interested in a Figure 1. The Syntax of Core-Java
more practical core calculus that incorporates all Java features [7] A class contains the declared fields and methods while an interface
and makes it easy to analyze and manipulate real-world Java pro- contains only methods without body. A method declaration meth
grams. A good intermediate language for such a task should be consists of the method modifiers, its return type, method name,
simple to analyse, close to source and able to handle real-world its arguments with their types, its raised exceptions, and a block
code. expression for the method body. Core-Java uses by default pass-
Our Core-Java language is more abstract than typical interme- by-value mechanism, but it also supports pass-by-reference mech-
diate languages designed for compilation as these intermediate lan- anism used in languages like C#. A block expression eb of the form
guages lose structural information about types, loops and other {(τ v)∗ e} consists of a list of local variable declarations and a body
high-level constructs. expression e. A block expression is evaluated to its body. The no-
tation w denotes a lvalue, a value that can appear on the left-hand
side of an assignment. A lvalue can be either a variable, v, or an ob-
ject field, v.f or a static field, c.f . Note that field access is restricted
to the simplest form, v.f . Java keywords this and super are treated
as special variable names in Core-Java. The notation x denotes ei-
ther a variable or a constant value and is used to restrict some ex-
Copyright is held by the author/owner(s). pressions (e.g. method arguments, returned expression, etc). Core-
OOPSLA’06 October 22–26, 2006, Portland, Oregon, USA. Java does not contain statements as it contains only expressions.
ACM 1-59593-491-X/06/0010. Expressions e include expression blocks, assignments, cast oper-

639
ations, method invocations, conditionals, control-flow primitives, der. On the other hand, for the flow-sensitive analyses the program
loops, exceptions, and concurrency primitives. The notation () de- flow is important and the constructions that alter it complicate the
notes an empty expression and its type is void. An assignment eval- formulation of such analyses. Therefore, we further translate Core-
uates to a void value, a sequence e1 ;e2 evaluates to the value of ex- Java: while loops are converted to equivalent tail-recursive meth-
pression e2 , and a loop also evaluates to void. A new c(x∗ ) invokes ods. To mimic the effects of loops, such converted methods differ
a default constructor of the c class. A constructor is a non-static from user-defined methods in that they use pass-by-reference pa-
method having the same name as its class. Core-Java monomor- rameters instead of pass-by-value ones. This conversion is for anal-
phic type, τ can be either a class type, or void or any Java primitive ysis purposes only; the while form is still used for execution.
type. Java array type is treated as a class. Core-Java does not have Core-Java was designed to support annotations to represent ei-
operators on primitive types, instead it defines a special class, called ther the output of a program analysis (e.g. the region annotations
Primitives that contains a static method for each primitive operator. produced by the region inference [3]) or the translation of a Java
program with type based annotations (e.g. region annotations given
3. Java to Core-Java Translation by the programmer as input for the region typechecker [3]). In gen-
We formulate the translation as a set of type-directed rules that eral, the analyses use three kinds of annotations: annotations of the
follow the syntax of the Java source language. The rules are type- normal Java types, invariants for the class declarations, and pre/post
preserving, that is, they guarantee that both programs, the Java conditions attached to the method declarations. All these annota-
input and the Core-Java output, have the same type. Our algorithm tions are specific to each type-based program analysis. In order to
consists of three main steps: support a specific analysis, the translator has to be specialised to
Generating Descriptors of Compilation Units. For each compi- work with the new annotated types instead of the normal Java types.
lation unit, we generate its attached descriptor file. A descriptor We experimented the passing of type annotations through translator
consists of typing information of each interface, class and their in [2], where a Java program was annotated with variant paramet-
fields and methods, but without the method body. The descriptor ric types. Core-Java methods were extended to parametric methods
also contains the class type dependencies. that contain type variables as arguments.
Computing the Global Dependency Graph. Our translation is re-
quired to process the class and interface declarations in some partic- 5. Conclusion and Future Work
ular order given by the complex inter-dependency among classes, We have implemented the translator in Haskell and we used it to
interfaces and methods. The dependency graph has the class and help two analyses: a region inference for Java [3] and a typechecker
interface declarations organised into a hierarchy of strongly con- of a variant parametric type system for Java [2]. The translator was
nected components (SCCs). Through a bottom-up processing of very useful in extending the experiments of our projects to real-
each SCC, we perform the translation in a systematic fashion. The world applications.
global dependency graph is also kept after the translation to be used Our goal is to have an integrated framework: translator, global
by the subsequent program analyses. dependency graph and any other specific data structure that can
Translation. The type-based translation is formulated as a mod- help and simplify the program analyses. Another aspect is the
ular type inference for the Java input program. The type system correctness of the translation rules. We experimentally validated
behind translation is similar with that formalised in [5]. The main that translated programs are correct and currently we are working
judgement has the following form: D, Γ  e ⇒exp e : τ denoting the on a formal proof of the translation rules.
translation of a Java expression e into a Core-Java expression e ,
where e and e have the type τ with respect to the type environ- Acknowledgements
ment, Γ and the set of descriptors, D. Details about our translation This work is supported by AStar* research grant R-252-000-233-
rules can be found in the companion technical report [4]. 305.
4. Support for Program Analyses
References
The goal of designing Core-Java language was to help the pro-
[1] Gavin Bierman, Matthew Parkinson, and Andrew Pitts. MJ: An
gram analyses on the Java-like languages, especially those analy- imperative core calculus for Java and Java with effects. Technical
ses which are type-based and modular. Core-Java in essence is an report, Cambridge University, 2003.
expression-oriented language, that makes easier the formulation of
[2] Wei-Ngan Chin, Florin Craciun, Siau-Cheng Khoo, and Corneliu
static and dynamic semantics. Expression languages are more suit-
Popeea. A Flow-Based Approach for Variant Parametric Types. In
able for type-based analyses that work on an abstract syntax tree ACM OOPSLA, Portland, 2006.
rather than on a control flow graph.
However, the syntax of Core-Java contains some constructions [3] Wei-Ngan Chin, Florin Craciun, Shengchao Qin, and Martin Rinard.
Region Inference for an Object-Oriented Language. In ACM PLDI,
that control the program flow. These constructions can be classified
Washington, 2004.
in the following categories: (1) intra-method flow: that is not altered
by exceptions or by return, but it can be controlled by the while [4] Florin Craciun, Hong Yaw Goh, and Wei-Ngan Chin. A Frame-
loop, if..then..else, break (forward jump) and continue (back- work for Object-Oriented Program Analyses via Core-Java. Tech-
nical report, National University of Singapore, 2006. avail. at
ward jump); (2) return flow: that is given by the return; and (3) ex-
[Link] chinwn/papers/[Link].
ceptional flow: controlled by throws and try..catch. To manage the
different categories of flow, we use a tuple of types, (intra-method [5] Sophia Drossopoulou, Tanya Valkevych, and Susan Eisenbach. Java
type, return type, exceptional type) similar with [5] to represent the type soundness revisited. Tech report, Imperial College, 1999.
type of an expression: Γ  e : tn #tr #ta , ϕ, where tn is the intra- [6] Cormac Flanagan and Stephen N. Freund. Type-based race detection
method type that characterizes normal execution of the expression, for Java. In ACM PLDI. ACM Press, 2000.
tr is the return type, denoting the type of a possible return expres- [7] James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. Java(TM)
sion from e, and ta is the exceptional type that characterizes the Language Specification, Third Edition. Addison-Wesley, 2005.
exceptional execution of e. [8] A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A Minimal
A flow-insensitive analysis is not affected by while loop, break Core Calculus for Java and GJ. In ACM OOPSLA, Denver, 1999.
and continue. Flow-insensitive results can be composed in any or-

640