Information Technology Reference
In-Depth Information
The abstraction process has two steps:
1. A breath first search of the data structure (for both the input and the faulty output)
is performed along all concrete fields. This search assigns a concrete dereferencing
list that can be used to reach any object. For example,
N
0
in Fig. 1 (a) is reached
via
header
and
N
1
is reached via
header.next
.
2. Using the above repository of abstractions, all possible abstractions that are equal to
a concrete dereferencing list are built. For instance
header.next
is considered
equal to
FIRST NODE.next
,
FIRST NODE.NEIGHBOR
,and
LAST NODE
.The
abstractions Self, Null, Offset, and Coefficient are only helpful as the right hand
side of a repair action.
The concretization process is an exact reverse of the abstraction. First, DREAM
transforms the abstract fields of a dereferencing list to their concrete forms which only
use the data structure fields. Then, it traverses the data structure along those fields to get
to the desired objects. When multiple abstractions/concretizations are valid, all of them
are used as possible candidates.
Both abstraction and concretization can be performed on the input data structure as
well as the faulty output of a method. This flexibility enhances DREAM's ability to
access objects that get lost because of broken pointers.
derefLeftInOutput
and
similar boolean flags are put in place to distinguish between the cases that the faulty
output and the input are used to access an object.
4
DREAM with Different Back-Ends
The idea of abstracting concrete repair actions is orthogonal to the underlying repair
framework used. Therefore, we can plug in our repair framework of interest to DREAM
and utilize its abstraction power. Some repair frameworks [23, 24, 27] use a SAT solver
to search the space of correct data structures while others [8, 13, 17] leverage dedicated
solvers. To showcase how DREAM can be used regardless of the underlying repair
method, we integrate it with Cobbler [23], our previous SAT based repair framework,
and Juzi [8, 9], which uses a dedicated Java based solver.
4.1
DREAM with Alloy Back-End
Connecting DREAM with an Alloy based repair framework (like PBnJ [27], Cob-
bler [23] or Tarmeem [24, 25]) is quite straightforward. The underlying repair frame-
work performs regular checks and provides concrete repair actions in case the abstrac-
tions do not work.
The only limitation is that even
checking
the correctness of a data structure using
SAT might be rather time consuming. To tackle this limitation, we used the Minshar [1]
technique. Minshar is a tool that translates Alloy specification checks to Java assertions
by viewing Alloy as a set based language. Minshar starts by parsing the Alloy specifica-
tion into Alloy Abstract Syntax Tree (AST), which indicates how Alloy expressions are
