Information Technology Reference
In-Depth Information
they must not alias. Hence, in principle, we should filter this type of interferen-
tial configurations generated from backward analysis when checking whether a
shadow can be removed. Based on this insight, our optimized NSA can success-
fully identify the shadows, similar to the shadow at line 8, as “nop shadows”.
Figure 3 shows another example to motivate the second optimization ap-
proach. Different from the former one, the typestate property “Connection-
Closed” is not violated by the method
m
. Therefore, all the shadows in method
m
can be safely removed. However, by using the original NSA, all the shadows
will remain.
1 public static void m(String args[]) {
2
Connection c1 = new Connection(args[0]);
…………………
S
12
= (0, T)
S
22
= (1, C = {O})
F
12
= ({1,2}, C = {O})
F
22
=
({0,1,2}, C = {O})
3
c1.write(args[1]);
…………………
S
13
= (0, C = {O})
S
23
= (2, C = {O})
F
13
= ({2}, T)
F
23
=
({0,1,2}, C = {O})
4
c1.close();
…………………
S
14
= (1, C = {O})
S
24
= (1, C = {O})
F
24
=
({1,2}, C = {O})
5}
Fig. 3.
The example for motivating the second optimization
The problem is mainly resulted by the approximated inter-procedure analysis.
Figure 3 shows partial forward and backward analysis results that are next to
the two downward arrows and two upward arrows, respectively. Because there
may be several consecutive method calls to a method in a program, for ensuring
the soundness, the forward analysis needs to propagate the configuration at the
end of a method to the entry of the method until a fixed-point is reached. For
example,
S
14
is propagated to the entry configuration
S
22
of the next iteration
(indicated by the red dotted line). The propagation also happens in backward
analysis. After reaching the fixed-point, the shadow at line 3 can produce the
configuration
S
23
, which contains an error state. Thus, this shadow cannot be
removed. In addition, the shadow at line 4 changes the configuration
S
13
to
S
14
,
but state 0 in
S
13
and state 1 in
S
14
are not both contained in the state set
{
1,
2
of the configuration
F
24
. Therefore, the shadow at line 4 cannot be removed
either.
After carefully analyzing the example program, we find the reason is that the
configuration propagation disregards the
local object
information. In this paper,
we call a static object, which is created by a “
new
” statement within the method
currently being analyzed, a
local object
. For example, the static object
O
created
by the statement at line 2 is a local object. Obviously, at runtime, each local ob-
ject will be assigned with a different runtime object each time when the method
is invoked and the “
new
” statement is executed. Therefore, for the example in
Figure 3, the configuration
S
22
should not have a same variable binding as
S
14
.
If we have the local object information of the example program,
i.e.
, no need to
do the second forward iteration and the second backward iteration, then both
of the “nop shadows” at line 3 and line 4 can be removed. Based on the obser-
}
