LICENSE
-------

        A BDD Solver of Andersen's Points-to Analysis for Java
    Copyright (C) 2002 by Marc Berndl, Ondrej Lhotak and Feng Qian
                            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 AUTHORS, 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.

    AUTHORS 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.

Note: The BuDDy library package is copyrighted by Jørn Lind-Nielsen.


Description
-----------

This software implements a new approach to solving a subset-based
points-to analysis for Java using Binary Decision Diagrams (BDDs). In
the model checking community, BDDs have been shown very effective for
representing large sets and solving very large verification
problems. Our work shows that BDDs can also be very effective for
developing a points-to analysis that is simple to implement and that
scales well, in both space and time, to large programs.

The detailed description of the algorithm and optimizations can be
found in our technical report at
http://www.sable.mcgill.ca/publications/#report2002-10

Requirements
------------

* A C++ compiler:  Currently tested under Linux with the GNU toolchain
  and versions 2.95, 2.96, 3.0.4, and 3.2.1 of GCC.

Installation
------------

(1) Untar bddprograms.tar.gz.  For example:

tar -zxvf bddprograms.tar.gz

    This will create bddprograms/ under the current directory.

(2) Obtain the latest version of the BuDDy from
    http://www.itu.dk/research/buddy/ and untar it under the directory
    created in the previous step.  For example:

cd bddprograms
tar -zxvf ../buddy2?.tar.gz

(3) Compile BuDDy.  Please see bddprograms/buddy2?/README for
    instructions.  Usually a simple "make" is sufficient.  Explicit
    installation is not necessary.  For example:

cd buddy2?
make
cd ..

(4) Review "bddprograms/Makefile".  In particular, the BUDDY variable
    may have to be updated to point to the necessary directory. 

(5) Compile the program with "make".  For example:

make

Obtaining benchmarks
--------------------

Benchmarks in the required format for the points-to analysis input 
constraints can be obtained from from http://www.sable.mcgill.ca/bdd/

Usage
-----

ABDD inputFile [n #ofInitialOfNodes]
               [c cacheSize]
               [(t)ypes (y)es (n)o]
               [O ordering]
               [e inputformat_nul(old|new)]
               [l controlcode(ite|part)]
               [a aliasstrategy(merge|sep|none|flow)
               [i incremental optimization (y)es (n)o]
               [r reversed local ordering (y)es (n)o]

Example
-------

./ABDD examples/smalltest-1.dat

Files
-----

README:                 This file.
Makefile:               The BUDDY variable may require updating before
                        compilation.
Solver-noalias.cxx:  	Solver implementation.
Parameters.cxx:         Processes input and parameters.
Parameters.h:           Definition of constants, macros, etc.
helpers.h:              Some inlined functions.
examples/:              Example input files.

===============================================================================
Sable Research Group,                                         McGill University
Montreal, Canada                                     http://www.sable.mcgill.ca