Information Technology Reference
In-Depth Information
3.
φ
must be chosen in such a way that if
K
Σ
|
=
{U}
φ
then there exists also
p
K
Σ
over an extended signature
Σ
such
an extended
DPL
-Kripke structure
φ
. This ensures that the post condition of
p
is correctly
represented by
φ
. One possible heuristic to obtain
φ
consists of symbolic
execution of
p
and applying the resulting update to
φ
. This yields a formula
φ
from which we obtain a candidate for
φ
by “anonymizing” all occurrences
of locations in it that occur in
mod
.
{U
}
that
K
Σ
|
=
The first two soundness conditions can be expressed in
, the third one only
in absence of quantified updates. In the latter case, the necessary proofs could be
added as additional nodes that spawn side proofs. A more e
cient (and generally
necessary) approach is to show once and for all that the oracle used to determine
mod
and
φ
is correct wrt the conditions.
DPL
Constant propagation and constant expression evaluation.
Constant propagation
is one of the most basic operations in partial evaluation and often a prerequisite
for more complex rewrite operations. Constant propagation entails that if the
value of a variable
v
is known to have a constant value
c
within a certain program
region (typically, until the variable is potentially reassigned) then usages of
v
can
be replaced by
c
. The rewrite rule
(
v
)
↓
(
U,ϕ
)
c
models the replacement operation. To ensure soundness the rather obvious con-
dition
v
=
c
) has to be proved where
c
is a rigid constant. The above
rule can be easily modified to include constant expression evaluation.
U
(
ϕ
→
Dead-Code Elimination.
Constant propagation and constant expression evalu-
ation result often in specializations where the guard of a conditional (or loop)
becomes constant. In this case, unreachable code in the current state and path
condition can be easily located and pruned. A typical example for a specialization
operation eliminating an infeasible symbolic execution branch is the rule
(
if (b) {p} else {q}
)
↓
(
U
,φ
)
↓
(
U
,φ
)
p
which eliminates the
else
branch of a conditional if the guard can be proved
true. The soundness condition of the rule is straightforward and self-explaining:
U
=
TRUE
).
(
φ
→
b
Safe Field Access.
Partial evaluation can be used to mark expressions as safe
that contain field accesses or casts that may otherwise cause non-termination.
We use the notation
@(e)
to mark an expression
e
as safe, for example, if we can
ensure that
o
=
null
, then we can derive the annotation
@(o.a)
for any field
a
inthetypeof
o
. The advantage of safe annotations is that symbolic execution
can assume that safe expressions terminate normally and needs not to spawn
side proofs that ensure it. The rewrite rule for safe field accesses is
↓
o.a
(
U
,φ
)
↓
(
U
,φ
)
.
@(o.a)
=
null
)).
Its soundness condition is
U
(
φ
→¬
(
o
