1. gijsv
  2. stance-java-frontend


| STANCE Java frontend |

Based on OpenJDK http://openjdk.java.net/

This repository contains the source files necessary to build the STANCE Java 
frontend. The STANCE Java frontend is a frontend (scanner, parser, type checker, 
and normalizer) for the Java programming language being developed by Gijs 
Vanspauwen [1] and Bart Jacobs [2] at the DistriNet Research Group [3] at the 
Department of Computer Science [4] of KU Leuven - University of Leuven [5] as 
part of the STANCE [6] research project sponsored by the European Commission as 
part of its 7th Framework Programme, whose goal is to develop a Source code 
analysis Toolbox for software security AssuraNCE.

[1]: http://distrinet.cs.kuleuven.be/people/gijs
[2]: http://distrinet.cs.kuleuven.be/people/bartj
[3]: http://distrinet.cs.kuleuven.be/
[4]: http://www.cs.kuleuven.be/
[5]: http://www.kuleuven.be/
[6]: http://www.stance-project.eu/

The main extensions with respect to OpenJDK are 1) the retention in the AST of 
specially marked comments that are used as annotations by the STANCE 
verification approaches, and 2) code that makes the output of the frontend 
available to OCaml programs (including the STANCE verification tools, which are 
written in OCaml), consisting of Java code that serializes the OpenJDK AST and 
OCaml code that deserializes it into an OCaml datatype value.

While our first priority is to support the STANCE goals, we intend this frontend 
to be reusable also for the development of other tools that consume Java source 
code with comment-based annotations and that are written in OCaml.

There are four important directories: the protocol subdirectory, the top level 
directory, the java_frontend subdirectory and the examples subdirectory. The 
contents of these directories are explained below.

To build the frontend and pretty print a Java file using the frontend run:

  ./frontend.py -h

for detailed instructions.

build requirements

-Requirements to build JDK (see README_JDK file)
-GNU Make: version 3.81 or later
-OCaml: version 3.12.1 or later

  Modify the file make/build.properties to your configuration, i.e. set the 
boot.java.home variable to the location of your Java installation


In this directory the protocol that is implemented by the "AST Server" (see 
further) is described. The protocol is called the "AST Server Protocol" and is 
specified in the file protocol.pdf.

top level

This folder contains a fork of the "langtools" workspace of OpenJDK so all files 
and all added files from this workspace are under the GNU General Public 
License, version 2, with the Classpath Exception. To make diffs possible 
(mercurial does not cleanly support moving files), this repository is kept as 
the top level directory. The original cloned mercurial repository is:
This repository is updated (i.e. merged) occasionally with the developments 
from that repository.

By running:

  ant ast-server

in the make directory the jar file ast_server.jar (in directory dist/lib) is 
build. This jar contains an application, called the "AST Server", that 
serializes a type checked AST. To do this, the application uses different 
modified source files from javac and it's own added source files, see directory:


The "AST Server" implements the "AST Server Protocol" and it communicates with 
the OCaml part through pipes (can be modified to IPC for example in the future).


This directory contains the OCaml part of the frontend. All files in this 
directory are under the "3-clause BSD license". This code communicates with the 
"AST Server" using the "AST Server Protocol". The file java_frontend.mli 
specifies the interface to interact with the java frontend. When receiving a 
request to create an AST, the frontend launches the "AST Server" and reads back 
in the serialized AST into an OCaml data structure (see general_ast.ml). This 
folder also contains a demo application (see main.ml) which prints out the 
generated type checked AST as an OCaml expression.

Currently annotations are kept as uninterpreted AST nodes by the frontend. But a 
callback is performed when an annotation is encountered (see the "AST Server 
Protocol" and see annotation_type_checker.mli). The functionality to allow each 
verifier to type check annotations during these callbacks is not finished yet.


This directory contains different exemplary Java source files. They demonstrate 
the current status of the Java frontend. Currently the frontend supports at 
least classes, exceptions and (limited) generics. The OCaml expression generated 
for a Java source file "filename.java", is given in the corresponding file