jDFA - The Data-Flow Analysis Framework for Java

Overview

jDFA is a Java framework for data-flow based program analysis. It allows to implement analyses, test their correctness, and evaluate their performance. In addition, the framework allows the definition of intraprocedural analyses for Java Virtual Machine (JVM) code on a high level of abstraction.

The framework is provided as a set of APIs for Java:

de.rwth.dfa

The core of this package is the class DataFlowSolver, which contains an implementation of the classical iterative algorithm for intra-procedural data-flow analysis.

de.rwth.dfa.jvm

This package adds an additional level of abstraction on the de.rwth.dfa package.

de.rwth.dfa.jvm.samples

This package contains bytecode analyses implemented using the de.rwth.dfa.jvm package.

de.rwth.domains

This package contains interfaces for modelling the mathematical structures.

de.rwth.domains.templates

This package contains implementations of the interfaces from the package de.rwth.domains for standard domains and domain constructors like bit vectors, Cartesian product, or lifted partially ordered sets.

de.rwth.graph

This package implements an API for representing directed graphs.

de.rwth.utils

This package contains useful utilities.

Download

Visit the SourceForge project page to download.

Requirements

For the JVM related APIs of jDFA, you need the ByteCode Engineering Library (BCEL). Please use the SourceForge version of BCEL, not the Apache version.

Installation

Just put the JAR file somewhere and add the location to the CLASSPATH environment variable.

Examples

The package de.rwth.dfa.jvm.samples contains simple example applications:

java de.rwth.dfa.jvm.samples.SSAnalyser classfile

Shows the size of the operand stack at each instruction of all methods of the classfile.

java de.rwth.dfa.jvm.samples.LVAnalyser classfile

Shows which local variable slots are live at each instruction of all methods of the classfile. A slot is live at an instruction if its value may be used in some execution starting from the instruction.

java de.rwth.dfa.jvm.samples.CPAnalyser classfile

Shows which constants from the program exist in the local variable slots and the operand stack at each instruction of all methods of the classfile.

java de.rwth.dfa.jvm.samples.CFPAnalyser classfile

Shows which computed constants exist in the local variable slots and the operand stack at each instruction of all methods of the classfile.

Projects

• Jopt - The Java Class File Optimizer (Markus Jansen)
• JoGa - Global Optimisation of Java Applications and APIs (Arnd Houben)

Documentation

• API Documentation for release 1.0
• RWTH Technical Report: SourceForge (PDF), RWTH (PDF), RWTH (PostScript, gzip)
• Workshop Paper (IRE'02): SourceForge (PDF)

CVS

To check out the complete source tree using anonymous CVS:

cvs -d:pserver:anonymous@cvs.jdfa.sourceforge.net:/cvsroot/jdfa login 
      

cvs -z3 -d:pserver:anonymous@cvs.jdfa.sourceforge.net:/cvsroot/jdfa co de