Information Technology Reference
In-Depth Information
In general, the symbolic exploration of a program may diverge differently
from a fully exhaustive exploration, since a symbolic computation aggregates a
possibly infinite set of concrete states that may behave differently with respect to
divergence. As an example, the C program
while
(
x
>
0
)
{
x
=
x
−
1
;
}
produces
the infinite symbolic computation (
{x → x},true
)
p
→
(
{x → x −
1
},x >
0)
p
→
,x>
1)
p
(
...
that represents the set of all the computations from
states with
x>
0, none of which is infinite
5
.
In practice, symbolic execution must rely on incomplete theorem provers for
deciding over logical statements. The actual precision of symbolic execution is
strongly affected by these “hard points”:
{
x
→
x
−
2
}
→
Check for failure:
decide whether a symbolic state contains an error state;
Compute the successors:
decide whether a path condition is satisfiable;
Check for success:
decide whether a set of symbolic states is subsumed by
another set of symbolic states.
The problem of checking reachability is sometimes tackled by encoding error
states within the control flow (error states are all and only the states at a given
location). In these cases, error states are identified by simply observing the cur-
rent locations of the symbolic states, and the problem is therefore collapsed with
that of computing the symbolic successors. The problem of computing the sym-
bolic successors requires a decision procedure for checking the satisfiability of
the path conditions. Path conditions are typically existential quantifications of
conjunctions of atomic clauses, and thus the problem is less hard than full first-
order logic satisfiability checking. The problem of e
ciently detecting symbolic
invariance (i.e., checking symbolic equivalence of states) is hard and has not been
solved satisfactorily yet. Most approaches do not detect invariance at all.
Example: Predicate abstractions.
Predicate abstractions exploit finite sets of
predicates to interpret the state space of a program abstractly. The abstract
lattice is the boolean lattice built over the set of predicates, which has finite
height.
Let
H
de
=
E
a set of predicates with finite size
m
.Wede-
fine the lattice of predicate abstraction over
H
as the powerset lattice over the
powerset of the possible predicates,
{
h
0
,...h
m−
1
}⊆
(
H
)) . The abstract lattice elements
are usually interpreted as sets of
abstract states
, in analogy with the concrete
powerset lattice of (concrete) program states. The meaning of an abstract state
σ
P
(
P
(
H
) is the set of all and only the concrete states which verify the predicates
in
σ
, and falsify all the other predicates. We formalize this interpretation by a
translation function
∈P
−
defined as follows:
de
=(
h∈σ
(
h∈σ
de
=
σ∈Σ
σ
h
)
∧
¬
h
)
,
Σ
σ
.
5
While this shows that symbolic execution loses information about program termina-
tion, such imprecision is irrelevant in the context of this paper, where we consider
only reachability properties.
Search WWH ::
Custom Search