Transcript javacop

JavaCOP
A Framework for Implementing
Pluggable Type Systems
Chris Andreae
James Noble
Victoria University of
Wellington
Shane Arkus
Todd Millstein
University of California
OOPSLA 2006, Oregon, Portland
Types are good…
• Type-checkers help the programmer
• But, they don’t always help enough!
• Existing type systems are not always sufficient:
–
–
–
–
–
Non-null references
Read-only references
Confined types
Style checking
…
2/26
…But not all the time
• Type systems are not always relevant:
– Particularly restrictive systems
– Domain-specific or limited applicability
– Conflicting type systems
• Too many systems exist to use at once:
@Nonnull @Readonly @Borrowed @LockedBy(“this”)
@TransactionAttribute(MANDATORY) @ReadEffect(“foo”)
@WriteEffect(“bar”) public String<Owner>
fetchString(@Nonnull Integer<World> which){...
3/26
Pluggable Types
• Bracha [2004] introduced “Pluggable Types” :
– Type systems should be optional
– No effect on the runtime semantics
• Type annotations not mandatory in syntax
– Type systems should be pluggable
• Multiple type systems for different needs
• JAVACOP
– Express these constraints
– Check and enforce the constraints on programs
4/26
Running Example – motivation
• protection of access to variables, methods,
classes is enabled
– No mechanism to ensure that references to protected
object do not escape
• Security example
Returns a reference
to the actual array!
private Identity[] signers;
public Identity[] getSigners()
{ return signers; }
5/26
Confined types
prevents leaks of
sensitive object
references from outside a
certain protection domain.
outside
X
unconf
conf
6/26
Confined Class Declaration
• Confined types can not be public
public @confined class C {
…
};
+
rule ConfinedClassDef(ClassDef c){
where(confined(c)){
require(!c.getSym().isPublic ()):
error(c, "Confined class may not be public");
}
c.java:4: Confined class may not be public
public @confined class C
^
1 error
8/26
JavaCOP System - Overview
JavaCOP Rules
JavaCOP.Compiler
Compiled constraints
(Java class)
Errors and
Warnings
JavaCOP.Framework
Java
Program
javac compiler
Compiled
Program
9/26
JavaCOP and Javac
JavaCOP
rules
Java program
with
new types
javac
compiler
AST
of
the
program
10/26
AST Node types
Tree
Field or method
selection, i.e.,
o.field or
o.method();
+type : Type
+pos : int
Select
MethodDef
Instance creation, like
new World(“Hello”);
Method call,
like
meth(args);
NewClass
+selected : Tree
+name
Assign
…
+lhs : Tree
+rhs : Tree
ClassDef
Apply
+meth : Tree
+args
11/26
JavaCOP Object Model
• An abstraction of javac AST
Type
– Hides irrelevant structures
+isPrimitive() : Boolean
+restype() : Type
+outer() : Type
– Augmented with typing and
information on program entities:
MethodType
ClassType
• Type nodes
…
• Symbol nodes
Symbol
• Env structs
-name
-type : Type
• Globals
ClassSymbol
VarSymbol
MethodSymbol
12/26
The Rule Language
• JavaCOP.Language source file is a set of rules
• Each rule
• appliesrules
to a particular kind of AST node
declares
• an advicerequirements
on a static joinpoint in the AST traversal
program
Compiled
• Has a setJavaCOP.
of
constraints
constraints
Compiler
– If fail, error/warning is emitted
Errors and
Warnings
JavaCOP.
Framework
• Expressive language
Java
Program
javac compiler
Compiled
Program
– Pattern matching, quantifiers, conditionals…
13/26
Conditional Constraints
• If a method is public or protected and is confined,
it must be in a confined class
MethodDef
node type
rule ConfinedMethodDef(MethodDef m){
where((m.isPublic() ||
m.isProtected()) &&
confined(m.type().restype)){
require(confined(m.enclClass())):
error(m, "Confined non private
method return type in
unconfined class”) }}
}
Condition
Primitive
constraint
Failure clause
14/26
Pattern Matching rules
• Conditions on structural patterns.
• Example – Anonymity preserving
– method calls with an (explicit or implicit) receiver of this are
either to static methods or to other anonymous methods.
rule AnonCallsAnon(Apply a){
where(anonymous(env.enclMethod ){
where(a.meth => [this.*] || a.meth => [*]){
require(a.meth.isStatic || anonymous(a.meth)):
error(i, "’this ’ may not be used to "+
"call non -anonymous methods."); }}}
15/26
Quantification Rules
• Constrain properties of collection of objects
– Lists, AST subtrees
• Similar to Java 5 enhanced for loop
• Example- confined class as extension
– A confined class may not extend an unconfined type.
rule ConfinedClassDef2(ClassDef c){
where(confined(c)){
forall(Type s : c.supertypes ()){
require(confined(s) || s == globals.objectType):
error(c, "A confined class may not extend "
+ "an unconfined superclass");}}}
16/26
Subtype Rules
• Subtyping is fundamental to Java’s type system
– Subtype Rules allow declaring subtyping relations
• Example- a value of confined type cannot be viewed at an unconfined
supertype
rule checkConfined(a <: b @ t){
where(confined(a)){
require(confined(b)):
error(t, "Confined type "+a
+" may not be treated as a subtype of"
+"unconfined type "+b); }}
• Applies to AST nodes change the type of an expression
– Assignment, parameter passing, result returning, type casts.
• Passed:
– type of the expression
– supertype it must conform to
– AST node where the test occurs
17/26
Predicates Declarations
• Describe complex properties without repeating.
– Readable
– Reusable
• Invoked by the bodies of rules and other
predicates
declare anonymous(Tree t){
require(t.holdsSymbol &&
t.sym.hasAnnotation("Anon"));
}
18/26
Disjunctive Constraints using Predicates
• Can have multiple predicates with same signature.
–Prolog like
• The predicate holds if any of its definitions hold
• Example- definition of Confined
declare confined(Type t){
require(t.isArray());
rule ConfinedClassDef(ClassDef
c){
require(confined(t.elemtype));
}
where(confined(c)){
declare confined(Type t){ ()):
require(!c.getSym().isPublic
require(!t.isArray());
error(c,
"Confined class may not be public");
require(t.hasAnnotation("Confined")); }
declare confined(Type t){
require(!t.isArray());
exists(Type p : t.allparams()){
require(confined(p)); }}
19/26
Failure Clauses
• Three parts
–error/warning
–Position in source
–Message to report
• If a statement fails, JavaCOP searches for the
nearest enclosing failure clause and executes it.
require(a){
require(b);
require(c): error(pos1 , "error - c has failed");
}: warning(globals.NOPOS , "warning - a or b have failed")
20/26
The JavaCop Framework
• Augmented Sun javac compiler
JavaCOP Rules
– Passes over each class after type checking
JavaCOP.
Compiler
Compiled constraints
(Java class)
and
• Defines JavaCOP API methods Errors
Warnings
– Can be used directly JavaCOP.
Framework
– Can serve as a Type
base forAugmented
high-level
systems
Rest of
AST
Parser
Java
Checking
Compiler
AST
Program
• JavaCOP rule
language
javac compiler
Compiled
Program
21/26
The JavaCOP Framework Implementation
• Checks source code, not byte code
– More information available
• Generic types
• Many annotations
• Compiles each .java file separately
– Modular design, like javac
– Extract interface information from bytecode
• Performance
– Less than twice the compile time
• Insulates compiled rulesets from compiler
implementation
– Port to other compilers without changing the language
• Implemented in Java
22/26
The JavaCOP Compiler
• Translates rules into java code
– Source–level transformation
• New code
JavaCOP Rules
Parse syntax tree
Compiledby Framework.
– ExtendsJavaCOP.Compiler
interface exposed
constraints
Generate Java source
– Compiled into bytecode using regular Java
JavaCOP.
Framework
compiler
Errors and
Warnings
• Implemented in Haskell
Java
Program
javac compiler
Compiled
Program
23/26
Applications
Successfully implemented several existing systems:
• Type systems:
–
–
–
–
–
Confined Types [Vitek & Bokowski 1999]
Scoped Types for Real-Time Scoped Java [Zhao et al. 2004]
Race Condition Detection [Flanagan & Freund 2000]
Generic Ownership [Potanin et al. 2006]
Javari’s notion of reference immutability [Tschantz & Ernst 2005]
• Other program constraints:
–
–
–
–
An EJB3.0 verifier
Two rulesets from the PMD Java style checker
Identifying “Degenerate Class” micro-patterns [Gil & Maman 2005]
Collecting structural information for OO metrics [Chidamber & Kemerer
1991]
24/26
Contribution
The first practical framework for pluggable
types.
• Rule Language for Pluggable Types
– Clear, expressive, easy to use
• Implementation
– Integrated into standard development process
– Rule language compiler
• Validation
– Demonstrated on a range of type systems and other
constraints
• Useful for programmers
– Choose type systems as needed
• Useful for researchers
– Experiment easily with novel type systems
25/26
Limitations
JavaCOP doesn’t support:
• Whole program analysis
– Integrated with Java’s modular compilation.
• Dynamic checks
– Necessary for downcasts
• Flow sensitivity
26/26