|
Jedd Home
Overview
Using Jedd
Installation
Download
Compiling
Copyright
Sable Home
|
Jedd: Java Extension for Decision Diagrams
Jedd is a Java language extension designed for implementing program analyses
using binary decision diagrams (BDDs). BDDs are abstracted in Jedd as
a new primitive data type, database-style relations. A detailed paper about
Jedd was presented at
PLDI 2004, and is available
from the
Sable publications page. Additional information about Jedd can also be
found in my PhD thesis, in Chapter 3 and Appendix B.
Jedd is based on the
Polyglot extensible compiler framework. Currently, Jedd supports four
BDD libraries as backends:
BuDDy,
CUDD,
SableJBDD,
and
JavaBDD.
When building Jedd from source, these libraries
should be downloaded separately. The binary distribution of Jedd has these
libraries linked in.
Jedd is freely available for download under the
GNU Lesser General Public License.
A mini-tutorial on Jedd is available in PDF format.
The javadoc documentation of the (rather small) API available to Jedd programs
is available. In particular, this includes the
jedd.Jedd class with methods controlling the behaviour of Jedd in general,
and the jedd.Relation interface of methods that can be called on any
relation type.
| Installation instructions |
top |
A precompiled binary distribution of Jedd is available for download.
If you prefer to compile Jedd yourself, please see
the instructions below.
To use the Jedd translator to compile Jedd programs, you need the following:
- Add jedd-translator.jar from the Jedd distribution to your CLASSPATH
environment variable.
- Add the Polyglot classes jar to your CLASSPATH environment variable.
You can download a pre-compiled jar of Polyglot from the Soot download page.
- Install a SAT solver. I have been using Jedd with
zChaff, but it
should also work with other SAT solvers such as
Grasp and
Sato.
The -s switch to Jedd is used to specify the full path of the SAT
solver binary. If the solver has an unsatisfiable core extractor (like
the zcore program bundled with Zchaff), specify its full
path using the -sc switch to Jedd. Because the zChaff command-line
syntax changes from version to version, I have written two shell
scripts, zchaff and zcore, for invoking zChaff
version 2004.5.13 with the correct syntax. The scripts can be found in
the scripts directory of the Jedd distribution. Should the
command-line syntax change again in future versions of zChaff, the
scripts can be modified to match the new syntax.
(Optional) To browse the output of the Jedd profiler, an SQL
database, a CGI-capable web server, Gnuplot, Python to execute the CGI scripts,
and a web browser are required. I use SQLite and thttpd because of their
simplicity and ease-of-installation. The SQL code and CGI scripts are
somewhat SQLite-specific, but they should work with any CGI-capable
web server and with any standards-compliant web browser. The version
numbers of the tools used during Jedd development are given below. Other
versions may also work.
Release 0.3 (October 2005)
The main changes in this release are:
- Updated to BuDDy 2.4 and Polyglot 1.3.2
- More efficient attribute copying operation
- More flexible specification of BDD variable ordering
- Profile graphs now show physical domains
- Bug fixes
Release 0.2 (July 2004)
The main changes in this release are:
- Numberers changed to use longs instead of ints
- More efficient encoding of the physical domain assignment as a SAT problem
- Bug fixes
Release 0.1 (June 2004)
Initial public release of Jedd.
| Compiling Jedd from source |
top |
Jedd comes with an Ant build file for
building it from source. Jedd has been developed on GNU/Linux and also tested
on Windows XP, but few modifications
should be required to build it under other operating systems.
The following tools are required to build Jedd. The version numbers specify
the versions of the tools that were used in Jedd development. Other versions
may also work.
Jedd links to the following libraries, and these are also required to build
Jedd.
First, download and build/install all the dependencies above.
After expanding the Jedd source archive, you will find a file named
ant.settings.template in the Jedd directory. Copy this
file to a ant.settings. This file tells the build process where
to find all the tools needed to build Jedd. Edit the file with a text
editor to specify the locations of all the tools. Then, just run
ant, and Jedd should be built in the lib subdirectory.
(Optional) Jedd also includes a Soot-based live variable analysis
that optimizes Jedd code to free the BDD nodes of relations that become
dead. To build this optimizer, you will need the latest version of Soot
from Soot Subversion repository. The optimizer is built using the Ant
target compile-deadvaroptimizer.
| Copyright information |
top |
Jedd is Copyright (C) 2003-2005 Ondřej Lhoták, and is
distributed under the
GNU Lesser General Public License.
Copyright to Polyglot is held by several people listed on the
Polyglot home page, and is distributed under the
GNU Lesser General Public License.
The copyright notice of BuDDy is below:
==========================================================================
*** BuDDy ***
Binary Decision Diagrams
Library Package v2.2
--------------------------------------------------------------------------
Copyright (C) 1996-2002 by Jorn Lind-Nielsen
All rights reserved
Permission is hereby granted, without written agreement and without
license or royalty fees, to use, reproduce, prepare derivative
works, distribute, and display this software and its documentation
for any purpose, provided that (1) the above copyright notice and
the following two paragraphs appear in all copies of the source code
and (2) redistributions, including without limitation binaries,
reproduce these notices in the supporting documentation. Substantial
modifications to this software may be copyrighted by their authors
and need not follow the licensing terms described here, provided
that the new terms are clearly indicated in all files where they apply.
IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
MODIFICATIONS.
==========================================================================
CUDD is primarily written by Fabio Somenzi at the University of Colorado.
Its copyright notice is below:
This file was created at the University of Colorado at
Boulder. The University of Colorado at Boulder makes no warranty
about the suitability of this software for any purpose. It is
presented on an AS IS basis.
SableJBDD is Copyright (C) 2004 Feng Qian,
and is distributed under the
GNU Lesser General Public License.
The copyright notice for JavaBDD is below:
Copyright (C) 2003 John Whaley (jwhaley at alum.mit.edu)
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Library General Public
License as published by the Free Software Foundation; either
version 2 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Library General Public License for more details.
You should have received a copy of the GNU Library General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
|