jDFA - The Data-Flow Analysis Framework for Java

SourceForge.net Logo

[Overview] [Download] [Requirements] [Installation] [Examples] [Projects] [Documentation] [CVS] [Contribute] [License]


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:

The core of this package is the class DataFlowSolver, which contains an implementation of the classical iterative algorithm for intra-procedural data-flow analysis.
This package adds an additional level of abstraction on the de.rwth.dfa package.
This package contains bytecode analyses implemented using the de.rwth.dfa.jvm package.
This package contains interfaces for modelling the mathematical structures.
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.
This package implements an API for representing directed graphs.
This package contains useful utilities.
Through the extensive use of the Java interface concept, we established an open framework: For instance, specific implementations of abstract domains can easily be used in our framework.


Visit the SourceForge project page to download.


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.


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


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.




To check out the complete source tree using anonymous CVS:

cvs -d:pserver:anonymous@cvs.jdfa.sourceforge.net:/cvsroot/jdfa login 
When prompted for a password for anonymous, simply press the Enter key.
cvs -z3 -d:pserver:anonymous@cvs.jdfa.sourceforge.net:/cvsroot/jdfa co de


You are welcome to join the project as a developer and commit your improvements to the CVS repository. To do so, please contact me.

For more details please visit the Site Documentation page of SourceForge.


jDFA is published under BSD License.

© 2002 Markus Mohnen
Last modified: Sep 19 2002