Information Technology Reference
In-Depth Information
Type Inference.
For deep type hierarchies dynamic dispatch of method invo-
cations may cause serious performance issues in symbolic execution, because a
long cascade of method calls is created by the method invocation rule (Sect. 3.2,
p. 136). To reduce the number of implementation candidates we use information
from preceding symbolic execution to narrow the static type of the callee as far
as possible and to (safely) cast the reference to that type. The method invocation
rule can then determine the implementation candidates more precisely:
res
=
o.m
(
a
1
,...,a
n
);
↓
(
U
,φ
)
res
=@((
C
)
o
↓
(
U
,φ
))
.m
(
a
1
↓
(
U
,φ
)
,...,a
n
↓
(
U
,φ
));
=
x
)) ensures that the
The accompanying soundness condition
U
(
φ
→∃
C
x
;(
o
type of
o
is compatible with
C
in any state specified by
U
,φ
.
5 Application
As an application of interleaving symbolic execution and partial evaluation, con-
sider the verification of a GUI library. It includes standard visual elements such
as
Window
,
Icon
,
Menu
and
Pointer
. An element has different implementations
for different platforms or operating systems. Consider the following program
snippet involving dynamic method dispatch:
framework.ui.Button button = radiobuttonX11;
button.paint();
The element
Button
is implemented in one way for Max OS X, while it is im-
plemented in a different way for the X Window System. The method
paint
()
is defined in
Button
whichisextendedby
CheckBox
,
Component
,and
Dialog
.
Altogether,
paint
() is implemented in 16 different classes including
ButtonX11
,
ButtonMPC
,
RadioButtonX11
,
MenuItemX11
, etc. The complete type hierarchy
is shown in Fig. 8. In the code above
button
is assigned an object with type
RadioButtonX11
which implements
paint
(). As a consequence, it should always
terminate and the
DPL
-formula
gui
true
should be provable where
gui
abbre-
viates the code above.
First, we employ symbolic execution alone to do the proof. During this process,
button
.
paint
() is unfolded into 16 different cases by the method invocation rule
(Sect. 3.2, p. 136), each corresponding to a possible implementation of
button
Button
Component
CheckBox
ButtonAqua
ButtonMFC
Dialog
ButtonX11
RadioButtonX11 MenuItemX11 ... ...
... ... ... ... ... ... ... ... ...
Fig. 8.
Type hierarchy for the GUI example