| Juzi | Download | Example | Publications | Email me |
|---|
|
Overview: |
| Juzi is a tool for automatic repair of complex data structures. Juzi takes a Java class representing the data structure as well as a predicate method that specifies the structural integrity constraints as inputs, instruments its inputs, and generates a new Java class which behaves similarly to the original class, yet automatically repairs itself when the predicate representing the structural constraints is asserted. Juzi implements a novel repair algorithm. Given a structure that violates its integrity constraints, Juzi performs a systematic search based on symbolic execution to repair the structure, i.e., mutate it such that the resulting structure satisfies the given constraints. |
The binary files for Juzi can be found here
Extract the tar file using the following command: tar -xvf juzi.tar.gz
The directory Juzi will be created and will contain the following:
|
|
The following example illustrates how to use Juzi to repair corrupt doubly linked lists.
The examples directory holds a set of data structures example. To be repaired by
Juzi, a class defining a data structure MUST implement the "Repairable" interface which forces the class
to implement the boolean method "repOk" which represents a predicate that defines the structural integrity
constraints of the data structure.
To illustrate, the "linkedlist" directory holds the class "LinkedList.Java" which implements a circular doubly linked list. The class implements the "Repairable" interface and in turn the "repOk" method which checks for the circularity property of the list, the transpose relationship between the "next" and "prev" fields, as well as the consistency of the size field. To check for the validity of a data structure Juzi defines a new assertion "assertRepair" which uses the Java assert on repOk to check the validity of the structure. To enable repair, Juzi instruments the data structure class and generates a new class where an assertion violation (a violation of the assertRepair call) triggers a repair algorithm that mutates the corrupt structure to satisfy the structural integrity constraints given by repOk. To illustrate, the LinkedList class implements a "buggy" add method, and a createList method which constructs a list of a given size and asserts the validity of the list after each element addition. Check the output of running the linkedlist example when creating a list with three nodes: To compile linked list.java, from the examples directory run the following command: javac -sourcepath linkedlist/ -classpath ../Juzi.jar linkedlist/LinkedList.java To run the main method, from the examples directory run the following command: java -ea -classpath ../Juzi.jar:./: linkedlist.LinkedList
Note how a java assertion exception is thrown due to a corruption in the list detected upon teh first addition. To enable repair (error recovery) from the assertion violation, instrument the class using Juzi using the following steps:
Note how instead of terminating the code, the repair routine is triggered with every element addition and the program proceeds with its execution. Three log files are created to present the performed by the repair routine. Such logs helps debugging the source of the errors in the code. Juzi enables configuring the log files. For example, to visualize the repair actions, in the Juzi GUI select double click the "logging" tree node. A logging dialog will pop up. Select visualize from the drop down menu, click ok, transform the code and run it again. A visualization of the doubly linked list graph occurs with every trigger of the repair routine. Here are some screenshots for the output of the visualization. |
|