Information Technology Reference
In-Depth Information
The first work on generic constraint based data structure repair belongs to Demsky
and Rinard [5, 6]. Their method supports constraints in a declarative language similar
to Alloy. Also similar to SAT, their method translates constraints to disjunctive normal
form and solves them using an ad hoc search.
The Juzi tool [7,17] implements assertion based data structure repair. The user writes
data structure invariants in repOK methods. Juzi monitors the execution of repOK as it
checks the invariants. If a repOK check returns false, Juzi keeps systematically mutating
fields and running repOK until repOK returns true. Juzi mutates fields starting from the
ones accessed later in repOK, hypothesizing that those are more likely to be responsible
for the false return value. As an improvement, symbolic execution of repOK is added
to make the repair process even faster. Juzi only supports invariants that are checked
at one given point during the execution, hence it misses failures that correspond to the
relationship between pre- and post-conditions of methods.
Dynamic Symbolic Data Structure Repair [13] (DSDR) extends Juzi's technique by
producing a symbolic representation of fields and objects along the path executed in re-
pOK. DSDR builds the path constraint required to take the current path in repOK. When
repOK returns false, DSDR uses the conjunction of the negation of the path constraint
with the other path conditions and solves them, directly generating a fix irrespective of
the exact location of the corrupted object references or fields in the repOK method.
The Plan B approach and its tool PBnJ [27] support data structure invariants as well
as method pre- and post-conditions in a declarative first order relational logic extension
to Java that is similar to Alloy. Once a failure is observed, PBnJ falls back on executing
the specifications: i.e., it ignores the Java implementation and uses a SAT solver to
come up with a data structure that satisfies both invariants and method post-conditions.
Similarly to DREAM, PBnJ translates specifications to Java predicates which it uses for
fast checking. However, PBnJ suffers from a low repair performance, as it completely
ignores the Java code, the execution history of the program, the previous repair actions,
and the current faulty data structure.
Cobbler [23] aims to improve the scalability of SAT based data structure repair by
iteratively calling SAT and pruning the state space. To do so, Cobbler takes advantage
of program execution history: It considers the dynamic trace of field write and reads that
happened during the execution to guide repair actions. In addition, it uses unsatisfiable
cores provided by SAT solvers to limit the search space.
We would like to emphasize that DREAM's technique is independent of the underly-
ing repair framework and will enhance the performance of any repair routine. DREAM
can be combined with any of the above repair tools, or new data structure repair frame-
work tools and techniques. Furthermore, in the event that the failure is due to a bug in
code, DREAM can serve as a debugging aid, by providing an intuitive description of
the repair actions performed so that the user can incorporate a bug fix and eliminate the
need to repair altogether.
Even though our technique differs from automated debugging and program repair
techniques [2, 11, 15, 16, 20, 28, 30, 31], which mainly try to debug programs before de-
ployment, as we previously suggested [19] dynamic data structure repair can translate
into program statements that patch programs. Data structure repair actions can act as
an input to program repair frameworks such as the AUTO E-FIX tool [30], providing
 
Search WWH ::




Custom Search