Information Technology Reference
In-Depth Information
the same and only the occurrences of variable
threshold
are replaced by the
constant value
100
. If we perform symbolic execution on this program, then the
resulting execution tree spanned by two executions of the loop is shown in Fig. 6.
The first conditional divides the execution tree in two subtrees. The left subtree
deals with the case that the value of
y
is too high and needs to be decreased.
The right subtree with the complementary case.
All subsequent branches result from either
the loop condition (omitted in Fig. 6) or the
conditional expression inside the loop body
testing the value of
decrease
.As
decrease
is not modified within the loop, some of
these branches are infeasible. For example the
branch below the boxed occurrence of
y=y+1
(filled in red) is infeasible, because the value of
decrease
is true in that branch. Symbolic ex-
ecution will not continue on these branches (at
least for simple cases like that), but abandon
them as infeasible by
proving
that the path
condition is contradictory. Since the value of
decrease
is only tested
inside
the loop, how-
ever, the loop must still be first unwound and
the proof that the current path condition is
contradictory must be repeated. Partial eval-
uation can replace this potentially expensive
proof search by
computation
which is drastically cheaper.
In the example, specializing the remaining program in each of the two subtrees
after the first assignment to
decrease
eliminates the inner-loop conditional, see
Fig. 7 (the partial evaluation steps are labelled with
mix
). Hence, interleaving
symbolic execution and partial evaluation promises to achieve a significant speed-
up by removing redundancy from subsequent symbolic execution.
threshold=100
mix
y>100
?
decrease=true
decrease=false
mix
mix
|y-100|>eps
?
|y-100|>eps
?
y=y-1
y=y+1
|y-100|>eps
?
|y-100|>eps
?
y=y-1
y=y+1
Fig. 7.
Symbolic execution with
interleaved partial evaluation
4.2 The Program Specialization Operator
We define a program specialization operator suitable for interleaving with sym-
bolic execution in
. A soundness condition ensures that the operator can
be safely integrated into the sequent calculus. This approach avoids to formalize
the partial evaluator in
DPL
which would be tedious and inecient.
Definition 7 (Program Specialization Operator).
Let
Σ
be a signature
and
Σ
an extension of
Σ
as in Def. 5 containing countably infinite additional
program variables and function symbols for any type and arity. Let
σ
be the
embedding of
Σ
in
Σ
(
σ
(
Σ
)
DPL
Σ
). The
program specialization operator
⊆
↓
Σ
⊇Σ
:
P rogramElement
×
Updates
Σ
×
For
Σ
→
P rogramElement
takes as arguments a
PL
-statement (-expression), an update and a
DPL
-formula
and maps these to a
PL
-statement (-expression), where all arguments and the
result are over
Σ
.
