JavalibSawja

Download: Javalib 2.3.2 / Sawja 1.5.2

Introduction

Javalib is a library that parses Java .class files into OCaml data structures. Javalib offers primitives to extract information from, manipulate, and generate valid .class files.

It is distributed under the GNU Lesser General Public License (see the LICENSE file).

Sawja is a library written in OCaml, relying on Javalib to provide a high level representation of Java bytecode programs. Its name stands for Static Analysis Workshop for JAva. Whereas Javalib is dedicated to isolated classes, Sawja handles bytecode programs with their class hierarchy and control flow algorithms1.

Moreover, Sawja provides some stackless intermediate representations of code, called JBir and A3Bir. The transformation algorithm, common to these representations, has been formalized and proved to be semantics-preserving2,3.

It is distributed under the GNU General Public License (either version 3 of the License, or (at your option) any later version).

An Eclipse plugin for Sawja analyses is now available: it allows developers to add an analysis in Eclipse just by adding an executable.


  1. Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, Vincent Monfort, David Pichardie, and Tiphaine Turpin. Sawja: Static Analysis Workshop for Java. In Proc. of the 1st International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), volume 6528 of Lecture Notes in Computer Science, pages 92-106. Springer-Verlag, 2010. [.pdf]
  2. Delphine Demange, Thomas Jensen, and David Pichardie. A provably correct stackless intermediate representation for Java bytecode. In Proc. of the 8th Asian Symposium on Programming Languages and Systems (APLAS 2010), volume 6461 of Lecture Notes in Computer Science, pages 97-113. Springer-Verlag, 2010. [.pdf]

  3. D. Demange, T. Jensen and D. Pichardie. A Provably Correct Stackless Intermediate Representation For Java Bytecode. Research Report 7021, INRIA, 2009. [.pdf]

Quick start

We quickly present some OCaml code allowing to load a full program and to transform it into JBir intermediate representation. To get started, run the command make ocaml in the source repository of Sawja. Then you can run the generated toplevel named ocaml, which includes Javalib and Sawja modules. You need to enter some #directory directives to specify the location of the .cmi files needed by Javalib and Sawja.

Loading a program

Given an archive test.jar containing a class named Test.class defining a main method, we can load the corresponding program, assuming that the $CLASSPATH environment variable contains the test.jar file and the Java Runtime rt.jar.

Enter the following directives in your toplevel:

    #cd "... path of your test.jar archive ...";;
    #directory "... path of Ptrees sources ...";;
    #directory "... path of Extlib sources ...";;
    #directory "... path of Camlzip sources ...";;
    #directory "... path of Javalib sources ...";;
    #directory "... path of Sawja sources ...";;

The different modules of Sawja and Javalib are encapsulated in Sawja_pack and Javalib_pack modules. To uses them, you have to load the different used library and thoses packs:

    #load "ptrees.cma";;
#load "extLib.cma";;
#load "str.cma";;
#load "unix.cma";;
#load "zip.cma";;
#load "javalib_pack.cmo";;
#load "sawja_pack.cmo";;
    let (prta,instantiated_classes) =
      JRTA.parse_program (Sys.getenv "CLASSPATH")
         (JBasics.make_cms (JBasics.make_cn "Test") JProgram.main_signature);;

Now we generate the .html files corresponding to the parsed program prta. One file per class is generated and the package tree is reproduced in the destination directory. The destination directory must exist otherwise an exception will be raised.

    let outputdir = "./test";;
    let () = JPrintHtml.JCodePrinter.print_program prta outputdir;;

You can open the file ./test/Test.html with a web browser and navigate through the class hierarchy, or follow the control flow graph.

Transforming a program

We transform the previously loaded program from the JCode representation to the JBir intermediate representation.

    
let pbir = JProgram.map_program2
  (fun _ -> JBir.transform ~bcv:false ~ch_link:false ~formula:false ~formula_cmd:[])
  (Some (fun code pp -> (Ptmap.find pp (JBir.pc_bc2ir code)))) prta;;

To see how JBir representation looks like, we can generate the corresponding .html files.

    let () = JBir.print_program pbir outputdir;;
Last modification: