Bandera

A toolset for model checking Java programs

We assume that for Windows environment, the Windows is installed in C:. You should replace the "(username)" with the appropriate user login name. In some variants of Windows 95/98, the directory location is placed in C:\WINDOWS\ directory.

Inside the .bandera directory, we have a preferences file .banderarc, an abstraction file Abstractions, and three directories integral, real, and log.

The preferences file is meant to store user preferences, e.g. directory locations and colors. Later versions of the tool will add more functionality. We currently have no GUI to modify these values. You can hack the color values if you wish, but manually modifying the other entries of this file is highly discouraged.

The Abstractions file is used by Abstraction Manager to store user's custom abstraction library. The directories integral and real are used to categorize these files. However, this functionality is not fully supported in the current version of Bandera.

The log subdirectory is used to store all log files upon Bandera's failure. Please send all these logs along with their related files when you submit a bug report. Whenever you need a spare disk space, you can safely delete these log files.

If you experience some problems in running Bandera, you can try to delete the .bandera directory and re-run Bandera. This is usually due to the growing requirements for Bandera setup settings.

See the tutorial for a detailed walk through of some of the tools capabilities.

4) POINTERS TO ONLINE RESOURCES:

• Bandera Project web-page:
  http://www.cis.ksu.edu/santos/bandera/
• SOOT Project web-page:
  http://www.sable.mcgill.ca/soot/
• SPIN model checker:
  http://netlib.bell-labs.com/netlib/spin/whatispin.html
• NuSMV model checker:
  http://sra.itc.it/tools/nusmv/
• JavaPathFinder model checker:
  http://ase.arc.nasa.gov/visser/jpf/
• PVS theorem prover:
  http://pvs.csl.sri.com/
• Specification pattern project:
  http://www.cis.ksu.edu/santos/spec-patterns/

5) KNOWN LIMITATIONS:

Bandera consists of the following components:

1. Java to Jimple compiler (JJJC)
2. Bandera specification language (BSL) compiler
3. program slicer
4. abstraction library manager
5. abstraction type inference engine
6. source-level abstraction (SLABS) compiler
7. Jimple to Java decompiler
8. Bandera intermediate representation (BIR) constructor (BIRC)
9. BIR to Promela translator
10. prototype BIR to SMV translator
11. prototype BIR to DSpin translator

Several of these components (1-5) have GUI interfaces associated with them and the translators (8-11) also interface with a GUI that allows navigation of the source code statements that correspond to a counter-example. These GUI components are collectively refered to as the Bandera User Interface (BUI).

5a) Main Limitations:

A detailed component-by-component listing of the known limitations is given below. Here we outline the main toolset-wide limitations.

• One instance per Thread/Runnable class:

  The current translators to SPIN/SMV/DSPIN only support a form of static description of threads. Each class in the program that is a subtype of java.lang.Thread or implements java.lang.Runnable can have at most one allocated instance during program execution. This is a serious limitation, since it prohibits code like:

       p1 = new Producer();
       p2 = new Producer();

  Instead one must replicate the definition of Producer and rename it, e.g., Producer1, then transform the code as:

       p1 = new Producer();
       p2 = new Producer1();

  Fortunately, this is not a difficult problem to fix and we believe that our first minor release will lift this limitation.

  JavaPathFinder (JPF) does not have this limitation, so it is possible to use JPF as the model checking engine on code that has not been transformed as described above.
  
  

• Resource Bounds

  The translators impose limits on the maximum sizes for: maximal and minimal integer values, number of instances allocated by any new C() expression and array size. User's are free to select whatever values they would like for these bounds.

  While this may seem like a serious limitation, in fact, its more of a feature. Model checking integers that range over all integral values will be infeasible in practice. Bandera's abstractions provides one means for reducing the cost of checking systems that manipulate integral values. In addition, with Bandera one can perform "Resource Bounded" model checks. These are exhaustive depth-bounded state space searches where the bound is determined not by the number of transitions, but rather by "values" of the bounded quantities. For example, one might be interested in checking properties of a program only in states where the value of some integer field is less than 10; note that this is not safe in the sense that abstractions are, but it can be effective for quickly finding errors. It is also possible to disable "Resource Bounded" checks in which case the tool will report a "Range Limit Exception", and terminate checking, when an execution is found that exceeds one of the resource bounds.

  As suggested by the discussion above, the Bandera translators do not model garbage collection. JavaPathfinder and DSPIN do, however, model garbage collection.
  
  

• No recursion

  Bandera's built in translators do not currently support recursion. Program's are inlined before SPIN/SMV models are constructed. Our long-term approach to treating recursion is to exploit recent work on shape analysis to transform the program's data space and to transform recursive methods to compute over this new data space (thereby eliminating recursion).

  While in principle DSPIN can deal with recursion, our current translator does not take advantage of this. An update to the translators is in the works to fix this situation for DSPIN. JavaPathFinder can process models with recursion.
  
  

• Exception handling code is ignored

  Bandera's translators do not currently model exception handling code. The translators do model the raising of builtin exceptions, e.g., NullReference. The translator update mentioned above will provide a more complete solution for exceptions.

  JavaPathfinder support exceptions.
  
  

• Library code

  Bandera extracts models from Java source code, not class files, therefore it must have the source and cannot handle native methods. In order for calls to library code to work one must insure that the library is pure java and the source is in the classpath provided to Bandera. We have run a variety of examples that use library code, e.g., java.util.Vector, java.util.Stack, and java.lang.Object, that has the native methods replaced by Java code.

  JavaPathfinder processes class files and can therefore handle library code as is, although it has some trouble with native methods as well.
  
  

• Specifications

  JavaPathfinder can only analyze for deadlock and assertions. Work is underway by the JPF team to lift this limitation.

To summarize how to navigate the set of limitations to various components here are some guidelines:

1. If you don't have source ==> Use JPF standalone.
2. If you have source
   • If you are interested in using SPIN/SMV ==> Use Bandera's translators.
   • If minimal code modifications are a priority ==> Use Bandera & JPF.
   • If you want to check temporal properties ==> Use Bandera & SPIN.

5b) Component Limitations:

Features not supported by JJJC:

• Inner/anonymous classes (and any Java features related to them).
• Break and continue statements with label.
• Try with finally statement.
• Non-constant switch's case (e.g. fields or expression).
• T.class, where T is a type (e.g. int.class).
• Circular symbolic links in JJJC's (sub-)classpath cause problems.
• Does not do comprehensive checks on the program as in javac, it assumes the input to be a well-formed Java program (note: use javac to get better error messages).

Features not supported by BSL compiler:

• Inner/anonymous classes
• Predicates and assertion disregards inheritance.

Abstract Type Inference Limitations:

• Array and class types.

Slicer limitations:

• Slicer does not consider any dependence analysis in the presence of exception handlings. As a result of this limitation, the residual program will keep all original exceptions and their handlers
• Slicer does not solve the calling context problem which exists in Weiser's algorithm, the interprocedural slicing is inaccurate. A more accurate approach is under construction.
• All locks in programs are assumed to be safe. A safe lock is a lock that is guaranteed to be released at some point.
• If you are running a version 1.3.0_01 or earlier of the SDK there is a swing bug in the "drag & drop" feature of the PDG browser. Upgrading the SDK fixes this.

Abstract Type Inference Limitations:

• Array and class types are not currently supported.

Abstraction Library and BASL Limitations:

• Only supports integral (byte, char, short, int, long) and real (float, double) type abstraction.

SLABS Limitations:

• Array and class types not supported.

Decompiler Limitations:

• Complex boolean expressions cannot be decompiled, especially the "? :" operator and arbitrary compositions of && and || operators. Even though the decompilation may succeed at some point, it is still very buggy.
• Since much of the assertions are translated into "? :", the chance of going through the decompilation is also dim.

BIRC Limitation:

• Raises exception using java 1.3 on linux (but not on other platforms) switch to 1.2.

SPIN Translator Limitations:

• Return predicates for run methods not supported properly.

SMV Translator Limitations:

• This translator has been less well tested (its pretty brittle).
• Predicate mappings for BSL not implemented => deadlock checks only.
• No depth-bounded search switch.

BUI Limitations:

• Counter-example display doesn't illustrate cyclic nature of liveness property violations.

Helpful Hints for using the BUI:

• When specifying a property using object universal quantification, a dot "." must be typed after each "forall[c:C]" construct.
• The type inference GUI can be used properly only if the previous compilation by JJJC is successful.

Helpful Hints for using the JPF and Bandera:

• The program's class files are needed when model checking using JPF if Bandera does not slice or abstract the program.

Bandera README ends