|
BogorVM: Customizing Bogor for model checking Java programs |
|
A Bogor customization for model checking Java programs at the bytecode level.
Author: Robby
BogorVM is a model checker for Java built on top of the Bogor
software model checking framework. While closely related to the Bandera
project, BogorVM aims to be more of an open experimental platform to
demonstrate how Bogor can be customized to model check a specific
abstract/virtual machine, in this case, for Java. Therefore, it does
not include many features in Bandera such as the Indus
static analysis framework.
Note that BogorVM is currently an early
prototype.
BogorVM consists of three main components:
-
Bytecode-to-BIR Translator (BB): a translator written
using the ASM
Java bytecode manipulation framework
-
VM Extension (VMExt): a BIR language extension for
modeling Java Virtual Machine (JVM) instructions as described in the JVM Specification
book, and
-
VM Library (VMLib): BogorVM library that model Java
standard library.
Table 1. BogorVM
Features
| Bytecode-to-BIR
Translator |
|
VM Library |
| Supports all Java 5 class format and bytecode
instructions (except jsr; see Limitations below). |
Supports all Java bytecodes (except jsr; see
Limitations below) |
| Allows hand-customized class models and method
substitutions as BogorVM library |
|
| Fast translation (as it is almost transliteration of
Java bytecodes to Java bytecodes in BIR) |
| Reflection type allows embedding of Java objects
inside BIR objects that eases modeling of Java classes as mere delegates |
|
| Allows lifting of classes as "native" abstract
data types and abstract operations to reduce the size of state-space |
|
| Designed to generate Partial Order Reduction
(POR)-ready BIR model that leverages thread-local property of Java
bytecodes to reduce the cost of model checking |
| Allows custom class (object) to bit-vector
linearizer to reduce memory requirement for state storage |
|
| Allows custom backtracking algorithms for lifted
classes to reduce memory and time requirements when backtracking |
|
| Supports incremental compilation that eases integration
with the Eclipse JDT build process - see the Bogor-Java Eclipse
Environment project at http://www.cis.ksu.edu/~yongpeng |
| Allows different kinds of bytecode interpreters
(e.g., concrete or symbolic) as Bogor/Eclipse plug-ins |
|
| Standard library models use the actual Java
library classes to guarantee the same object behaviors as in runtime |
|
The tests module contains some JUnit
test cases. After checking it out to your Eclipse workspace, you will
be able to run the following in Eclipse Junit Launcher
(Run->Run...->JUnit):
-
[bogor-vm] BBShortTest, translates some Java examples
(AlarmClock, BoundedBuffer, Deadlock, LinkedQueue, ProducerConsumer,
ReaderWriters, SleepingBarber) in the module.
-
[bogor-vm] BogorVMTest, runs the model checker on the
examples above.
Note that, the JUnit test cases run BogorVM in debugging mode
that checks consistency of states after backtracking. To disable this,
comment edu.ksu.cis.projects.bogor.module.ISearcher.checkBacktrack=true
in all the .bogor-conf
file in the tests module.
VM Extensionis a language extension for modeling Java
bytecodes, i.e., its interpretation is done according to the JVM
Specification book. You can choose to use a different interpretation if
you want to (you first need to understand the concept behind Bogor
language extension -- see the Set Extension Walkthrough). For
example, in order to implement a customized interpretation, one only
needs to extend the edu.ksu.cis.projects.bogor.vm.module.VM
class as follows:
public class myorg.MyVM extends VM {
// Override IADD interpretation
@Override protected IActionBacktrackingInfo opIADD(IExtArguments args, Frame f) {
if (/* default case */ ...)
{
return super.opIADD(args, f);
}
... // my customized interpretation of IADD
}
}
Once a customized interpretation is implemented, use myorg.MyVM in the BB-generated
model as follows:
extension VM for myorg.MyVM {
...
}
This exact mechanism is used to implement the symbolic
execution presented in our Bogor/Kiasan paper.
As mentioned previously, BogorVM is an early prototype. There
are some limitations:
-
The Java library models in the VM Library is really
inadequate. Many of the Java library classes that require native
methods are not modeled. The rule of thumb is if you are trying to
translate your Java code using BB, and BB sucks in classes from sun.*
pacakages, this means your code cannot be handled by BogorVM at the
moment.
-
BB currently only generates BIR models that do not support
dynamic class loading. It currently use a rudementary static class
loading mechanism (where there is no guarantee on class ordering)
-
The jsr
instruction is not supported. Configure your compiler not to output jsr instruction; this is the
default in Eclipse JDT.
-
etc.
We refer you to more mature tools such as Bandera
or JPF if you need the features above.
|
