PluggableTypes
Download
Report
Transcript PluggableTypes
Practical Pluggable types for Java
Chris Andreae
James Noble
Shane Arkus
Todd Millstein
Victoria University of
Wellington
University of California
Presented by Lina Zarivach
1
Existing type systems are not sufficient
Non-null types
Declaring and Checking Non-null Types by M.
Fahndrich, OOPSLA’03
Non-Null Safety in Eiffel by B. Meyer,
ECOOP’05
Readonly types
Javari by M. Tschantz, OOPSLA’05
Other type systems
Confined Types by J. Vitek, OOPSLA’99
…
2
Implementation
Ad-hoc: New keywords and compiler
reimplementation.
Pluggable type systems:
Idea by Gilad Bracha, ’04.
Implementation by Andreae, Nobel et.al. ’06:
JavaCOP
Define new types with Java Annotations
Express new type requirements via JavaCOP
Rule Language
3
NonNull types example –
Pseudo-Declarative syntax & semantics
class Person {
@NonNull String firstName = "Chris";
void setFirstName(String newName)
{ firstName = newName;}
}
newName may
be NULL!!!
A JavaCOP rule to discover this case:
rule checkNonNull(Assign a) {
where(nonnull(a.lhs)) {
require(defNonNull(a.rhs)):
error(a,“Assigning possible null to @NonNull variable”);
}
}
4
JavaCOP Architecture
JavaCOP
rules
Java program
with
new types
javac
compiler
AST
of
the
program
5
JavaCOP Rule Language Types
A subset of data types generated in the javac
compiler. In particular:
AST nodes types
Type type
Symbol type
String and generic List types
Env
Globals
6
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
7
Symbols and Types
Type
Symbol Table
+isPrimitive() : Boolean
+restype() : Type
+outer() : Type
ClassType
…
MethodType
Symbol
-name
-type : Type
ClassSymbol
…
VarSymbol
MethodSymbol
8
Rules for AST nodes
rule aTreeRule(Tree arg) {
<sequence of constraints>
}
Huge API
rule finalClass(ClassDef c){
require(!c.supertype().getSym().hasAnnotation("Final"));
}
Only one argument of type Tree or subclasses of Tree.
The rule will be applied to each node of the specified
type.
9
Primitive Constraints
require(<condition>);
Instance of
Globals
rule UnconditionalIf (If i){
require(i.cond.getSymbol != globals.trueConst ):
warning(i.cond ,"The body of this if will
unconditionally be executed");
require(i.cond.getSymbol != globals.falseConst ):
warning(i.cond ,"The body of this if will never be
executed");
}
10
Conditional Constraints
where(<condition>) {<sequence of constraints>}
rule MicroPatternsExample (ClassDef c){
where(c.isInterface &&
c.getSym.members.length == 0){
require(c.interfaces.length != 1):
warning(globals.NOPOS ,
Primitive
"Taxonomy:"+c.flatName );
constraint
}
}
11
Pattern matching
where(<vardefs>; tree => [match using
vars]) {<body>}
rule checkNonNullFieldAccess(Assign a){ % is a wildcard for
Tree.
where(nonnull(a.lhs)) {
where(String n; a.rhs => [%.n]){
require(n.equals("class")):
error(a, "Assigning possibly null field access " +
" to @NonNull variable");
}}}
12
Universal quantifier
Similar to the “enhanced for” in Java 1.5.
rule finalMethod(MethodDef m){
forall(Type st: m.enclClass.transitiveSupertypes){
forall(Symbol other:
st.getSymbol.memberLookup(m.name)){
where(other.isFinal){
require(!m.overrides(other, st.getSymbol))
:error(m, "You may not override final method "+other );
}
}}}
13
Existential quantifier
Implicit depth-first traversal from a given AST
node.
Only nodes that match the declared type of
the quantifier variable are considered.
rule allLocalVarsMustBeAssigned (MethodDef m){
forall(VarDef v : m.varDefs()){
where(v.init == null){
exists(Assign a : m){
require(a.lhs.getSymbol == v.getSymbol );
}: error(v,"The variable " + v + "is never assigned");
14
}}}
Predicates (package several conditions
into boolean function)
declare <predicate name>(<vardef> [, <vardef>]) {
<list of constraints> }
Invoked by the bodies of rules and other
predicates.
declare nonnull(Tree t){
require(t.holdsSymbol
&& t.getSymbol.hasAnnotation("NonNull"));
}
15
Predicates - achieving disjunctive
constraints
Predicate can have multiple definitions.
An invocation of the predicate succeeds if
at least
one of the definitions’ bodies is satisfied.
declare defNotNull(Tree t){
require(nonnull(t));
}
declare defNotNull(Tree t){
require(t.type.isPrimitive());
}
declare defNotNull(NewClass t){
require(true);
}
t is non-null if it
has @NonNull
annotation.
Primitives can’t
be null.
New instance
can’t be null.
16
Error reporting
:<errortype>(<position>,<message>)
<errortype> is either error or warning.
When a constraint fails to be satisfied, 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")
17
Rules for custs – syntactic sugar
rule aCustRule(origType <: custedType @ Tree)
{<sequence of constraints>}
Applied to every Tree node that performs explicit or
implicit cust
rule checkNonNullCust (a <: b @ e){
where(!nonnull(a)){
require(!nonnull(b)):
error(e, “A possibly null type "+a +" may not be cast
to Non-Null type "+b);
}
}
18
Applications
A checker for non-null types.
A checker for Confined Types.
Rules supplied by PMD Java Checker.
Rules to identify some micro-patterns.
Rules that gather information for software
metrics.
An EJB3.0 verifier.
19
NonNull assignment
rule checkNonNullAssignment (Assign a){
where(nonnull(a.lhs )){
require(defNotNull(a.rhs)):
error(a,"Assigning possibly null value to @NonNull”
"+"variable.");
}
}
if(x != null){
@NonNull Object nonnull_x = x;
...}
The above rule will
issue an error for
this case!!!
20
NonNull assignment –
flow-sensitive check
rule checkNonNull (Assign a){
where(nonnull(a.lhs )){
require(defNotNull(a.rhs) || safeNullableAssign (a)):
error(a,"Assigning possibly null value to @NonNull "+"variable.");
}}
declare safeNullableAssign (Assign a){
require(localVariable (a.rhs ));
Env represents
require(safeNullableAssign (env.tree , env.next , a)); traversal
information
}
declare safeNullableAssign (Block b, Env e, Assign a){
require(safeNullableAssign (e.tree , e.next , a));
}
declare safeNullableAssign (If i, Env e, Assign a){
require(nonNullTest(i.cond , a.rhs)&& firstExpression (i.thenpart , a));
21
}
Confined types
Confined type is a type
whose instances may
not be referenced or
accessed from outside
a certain protection
domain.
Confined types protect
objects from use by
untrusted code.
outside
X
unconf
conf
22
Confined types – example 1
A confined type must not be declared public and
must not belong to the unnamed global package.
rule ConfinedExample1 (ClassDef c){
where(confined(c)){
require(!c.isPublic ()):
error(c, "Confined class may not be public");
require(c.packge() != globals.emptyPackage):
error(c, "Confined class may not be in the default
package");
}
}
23
Confined Types – example 2
Subtypes of a confined type must be confined and
belong to the same package as their supertype.
rule ConfinedExample2 (ClassDef c){
where(confined(c.supertype)){
require(confined(c)):
error(c, "An unconfined class may not extend "
+ "a confined superclass");
require(c.packge == c.supertype.packge):
error(c, “A confined subclass must belong to the
same package as its superclass”);
}
}
}
24
JavaCOP Architecture - details
Parse syntax tree
JavaCOP Compiler
JavaCOP rules and
predicates
Generate Java source
Performance:
~0.02 sec/class
Compiled rules into Java
Calls methods which
Emit
Errors and
Warnings
JavaCOP Framework
Constraint Engine
Java Program
(source)
Parsing
and
Attribution
Produces
Augmented AST
Bytecode
Generation
Javac compiler with
JavaCOP Framework
Compiled Java
Program
(bytecode)
25
Conclusions
The first practical framework for pluggable types.
Contributions:
Design of JavaCOP Rule Language
Implementation of JavaCOP
Validation on various kinds of application
Future extensions:
More support for flow sensitivity
Error clause, that count the number of times a
constraint failed.
Increasing the efficiency of checking the constraints.
26