| 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  and Bart Jacobs  at the DistriNet Research Group  at the
Department of Computer Science  of KU Leuven - University of Leuven  as
part of the STANCE  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.
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:
for detailed instructions.
-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.
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.
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