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
Search WWH ::




Custom Search