Information Technology Reference
In-Depth Information
s
,orithasapredecessor
violates
the safety property. Following [21] we will think of the as-early-possible placing
strategy and the SE-transformation realizing it throughout this article in terms
of this characterization of insertion points. The equivalence proof of the two
characterizations relies on the Safety Lemma 1. It states that in the intraproce-
dural setting safety can equivalently be expressed as the disjunction of up-safety
and down-safety.
m
such that (
m; n
) is not transparent or
m
Lemma 1 (Safety).
8 n 2 N:
Safe
(
n
)
()
Up-Safe
(
n
)
_
Dn-Safe
(
n
)
:
This lemma plays actually a major role in the soundness and completeness
proof of the SE-transformation (cf. [21]), but usually fails in more advanced set-
tings as we we are going to demonstrate in Section 7. Crucial in the proof of
this lemma is only the proof of the forward implication. The validity of the con-
verse implication is indeed obvious from the denitions. The forward implication
is essentially a consequence of considering branching nondeterministically. This
allows us to complete every path leading to a node by every path starting at
that node. In particular, this allows us to link every path violating the up-safety
condition at a node
n
with every path violating the down-safety condition at
n
.
Every path resulting from this violates the safety condition at
n
, which proves
the contrapositive of the forward implication.
Technically, the sets of program points which are up-safe and down-safe for
a computation
evolve as the greatest solutions of the Equation Systems 1 and
2, respectively, where
Comp
and
Transp
denote two predicates of edges. They
are true for an edge
t
e
t
, if it contains an occurrence of
, and if it does not modify
t
an operand of
, respectively.
Equation System 1 (Up-safety)
)=
(
false
if
n
=
s
V
us
(
n
(
Comp
(
m;n
)
_
us
(
m
))
^
Transp
(
m;n
)
otherwise
m2pred
(
n
)
Equation System 2 (Down-safety)
)=
(
false
if
n
=
e
V
ds
(
n
Comp
(
n;m
)
_
(
ds
(
m
)
^
Transp
(
n;m
)
)
otherwise
m2succ
(
n
)
In the following section we reconsider the theoretical background of program
analysis providing the formal foundation for proving these claims.
3.2 Analysis Level
In the context of optimizing compilers program analysis is usually called
data-
flow analysis
(
DFA
). Its essence is to compute run-time properties of a program
without actually executing them. Theoretically well-founded are DFAs based
Search WWH ::
Custom Search