Transcript PPT

Transformation of Java
Card into Diet Java
Semester Project Presentation
Erich Laube <[email protected]>
Overview
1. Introduction to Jive and Background
2. Transformation Basics
3. Examples
4. Future Work
5. Conclusion
Jive
 Java Interactive Verification Environment
 Code (Java) vs. Specification (JML)
 Diet Java
Goals
 Transformation of forbidden constructs.
 Reporting errors at compile time for
constructs that are not transformed.
Involved Tools
 ANTLR
parser, lexer
 Abstract Syntax Tree (AST)

 Multijava
java compiler
 static checks, type information

 JML

Multijava enhanced with JML
Difficulties
 Tracking (nested Expressions)
 Still knowing where one is
 Execution order
 Genericity
 Constructs forbidden in program but allowed
in specification part
 large amount of node classes
 non-uniform node layout
Try-Catch
 Only one Catch per Try
 done in Grammar file
try {
// something
}
catch (Exception1 e1){
// handler1
}
catch (Exception2 e2){
// handler2
}
try{
try {
// something
}
catch (Exception1 e1){
// handler1
}
}
catch (Exception2 e2){
// handler2
}
Do While => While
do {
[body]
} while (cond)
do {
if (x) break;
} while (cond)
{
boolean b = true
while (b){
if (x) break;
b = cond;
}
}
[body]
while (cond){
[body]
}
if (x) break;
while (cond){
if (x) break;
}
{
boolean b = true
while (b||cond){
if (x) break;
b = false
}}
Constructors
 conversion to method:

alter all constructor calls


find them, spread all over the code
call constructor of super method
create default constructor method
 but only if no other constructor specified




special case: this() calls
call the initializer method (not always there)
also needs a JML specification
Constructor conversion example
Class K extends M{
int f
f;= 2;
K(int i){
super(i);
f = i;
}
K(){
this(2);
this(f);
}
}
Class K extends M{
int f;
void °cK(int
°inst_init(){
boolean
°init;
i){
f = 2; }
void
super.°cM(i);
°cK(int i){
°inst_init(){
f =(°init){}
i;
°inst_init();
if
} else
{ f = 2;
super.°cM(i);
f =
i; = true;
void
°init
°cK(){
} }}
°cK(2);
}
void
°cK(){ i){
°cK(int
}
°inst_init();
super.°cM(i);
°cK(f);
°inst_init();
} f = i;}
} void °cK(){
°inst_init();
°cK(f);
} }
Future Work
 Remaining Transformations
non-strict operators
 pre- and postfix operators (++,--)
 inner classes

 Optimizations:


reuse temporary variables
simple trafos for simple cases
Conclusion
 Many constructs covered
 Mangled code:

difficult for user to still understand
 Interesting and complex project
Implemented Transformations

constructors

nonstatic initializers

variable initializers

local variables only at beginning of blocks

short if, for and do-loops, switch-blocks

multiple catch blocks for a try-block

casts within expressions

array access within expressions

compound assignment

assignment within expressions

assignments with side effects (partially)

pre- and postfix operators (partially)
Questions...?
Grammar File (ANTLR)
 Passes every code construct
 No Type Information
 Also affects JML part
 Work done here:

finding and forbidding


types
simple transformations


If-then-else
Try-catch
Abstract Syntax Tree (Multijava)
 Statements
can hold more Statements
 can hold Expressions

 Expressions


never hold Statements
can hold further Expressions