Information Technology Reference
In-Depth Information
Algorithm 1.
transition
((
Q
c
,b
c
,T
c
)
,s,δ
)
1:
cs
:=
∅
; // initialize result set
2:
l
:=
label
(
s
)
,β
s
:=
shadowBinding
(
s
); //extract label and bindings from
s
3: //compute target states
4:
Q
t
:=
δ
(
Q
c
,l
);
5: //compute configurations for objects moving to
Q
t
;
6:
β
+
:=
and
(
b
c
,β
s
);
7:
if
β
+
=
⊥
then
8:
cs
:=
cs ∪
(
Q
t
,β
+
,true
);
9:
end if
10: //compute configurations for objects staying in
Q
c
;
11:
B
−
:=
v∈dom
(
β
s
)
andNot
(
b
c
,β
s
,v
)
\{⊥}
;
12:
cs
:=
cs ∪{
(
Q
c
,β
−
,T
c
)
| β
−
∈ B
−
}
;
13:
return
cs
;
(Lines 11-12). Moreover, for the backward analysis, when we create an initial
configuration, the value of
T
in the initial configuration is set to
false
.
Based on the extended configuration definition and the transition algorithm,
we can identify changeless configurations produced by backward analysis. For
agivenshadow
s
and a configuration (
Q,b,T
)in
futures
(
s
), if
T
is
false
,the
configuration will be considered to be interferential, and should be filtered when
checking whether the shadow
s
is a “nop shadow”.
4.2 Exploiting Local Object Information
First, we present how to determine whether a static object is a
local object
.We
have the following two observations: first, for a given static object inside in a
method, if it is created by a “
new
” statement within the method, the object
must be a
local object
to this method; second, for any two
strong must-alias
[9]
static objects
O
1
and
O
2
inside a method, these two objects always refer to a
same heap object, which implies that they always point to a same local object
or a same non-local object. Based on these two insights, Algorithm 2 is designed
to identify local objects.
For a given method
m
and a static object
O
, the algorithm returns
true
if
O
is a local object in
m
; otherwise returns
false
. Algorithm 2 first declares
aset
newObjects
, and then adds all the local objects created by the “
new
”
statements in
m
to
newObjects
(Lines 1-7). Then, the algorithm checks whether
there exists an element in
newObjects
that is
strong must-alias
to
O
(Lines 8-
12). Currently, the must-alias analysis is only intra-procedural flow-sensitive,
and makes a conservative assumption that any two static objects coming from
different methods may alias. Therefore, Algorithm 2 is an approximated, but
sound, evaluation. In order to gain more eciency, we extract Lines 2-7 from
Algorithm 2 and compute the
newObjects
set before the optimized NSA.
