Information Technology Reference
In-Depth Information
states. Merging back different nodes is usually not possible without approxima-
tion or abstraction [15,16].
The hope with employing partial evaluation is that it is possible to factor
out common parts of computations in different branches by evaluating them
partially
before
symbolic execution takes place. The na ıve approach, however, to
first
evaluate partially and
then
perform symbolic execution fails miserably. The
reason is that for partial evaluation to work well the input space dimension of
a program must be significantly reducible by identifying certain input variables
to have static values.
Typical usage scenarios for symbolic execution like program verification are
not of this kind. For example, in the program of Fig. 2 in Sect. 2.3 it is unrealistic
to classify the value of
y
as static. If we redo the example without the initial
assignment
y=80
then partial evaluation can only perform one trivial constant
propagation. The fact that input values for variables are not required to be static
can even be considered to be one of the main advantages of symbolic execution
and is the source of its generality: it is possible to cover all finite execution paths
simultaneously and one can start execution at any given source code position
without the need for initialization code.
The central observation that makes partial evaluation work in this context
is that
during
symbolic execution static values are accumulated continuously as
path conditions added to the current symbolic execution path. This suggests to
perform partial evaluation
interleaved
with symbolic execution.
To be specific, we reconsider the example shown in Fig. 2, but we remove the
first statement assigning the static value 80 to
y
. As observed above, no notewor-
thy simplification of the program's CFG can be achieved by partial evaluation
any longer. The structure of the CFG after partial evaluation remains exactly
threshold=100
y>threshold
?
decrease=true
decrease=false
|y-threshold|>eps
?
|y-threshold|>eps
?
decrease
?
decrease
?
y=y-1
y=y+1
y=y-1
y=y+1
|y-threshold|>eps
?
|y-threshold|>eps
?
|y-threshold|>eps
?
|y-threshold|>eps
?
decrease
?
decrease
?
decrease
?
decrease
?
y=y-1
y=y+1
y=y-1
y=y+1
y=y-1
y=y+1
y=y-1
y=y+1
Fig. 6.
Symbolic execution tree of the control circuit program
