Information Technology Reference
In-Depth Information
k ∈{
1
,...,n}E−
@
x
k
E
E−
goto
x
1
,...,
x
n
E
E
τ
=
✧
E−
E
1
E
1
−
τ
=
✧
I
J
SEQ
GOTO
E−
I
;
J
E
E
=
E
p
E
τ
=
✧
τ
=
✧
E−
@
caller
P
RETURN
ASSUME
E
σ
,λ
,μ
,κ
∪{p},υ
,τ
E−
E−
return
assume
P
e
E
=
E
e
τ
=
✧
τ
=
✧
E−
havoc
v
σ \{
(
v
,σ
[
v
])
},λ,μ,κ,υ,τ
HAVOC
ASS
e
]
,λ
,μ
,κ
,υ
,τ
E−
v
:=
e
σ
[
v
→
τ
=
✧
E−
halt
σ, λ, μ, κ, υ,
✓
τ
=
✧
E−
abort
σ, λ, μ, κ, υ,
✗
HALT
ABORT
κ
E
=
E
κ
=
κ ∪ κ
μ
∪ Φ
(
υ
) om
Λ
)=
{ ∈
LV (
κ
)
|
}E
=
σ, λ ∪ Λ, μ, ∅,υ,τ
PICK
τ
= ✧
scalar
pick
E
E−
Fig. 4.
Symbolic execution: operational semantics. All rules describe transformations of a generic
symbolic state
E
=
σ, λ, μ, κ, υ, τ
.
(
m,
x
,y
)
, which express the information in
μ
about symbolic maps; as well
as
finitized
universal constraints
Φ
(
υ
). It then picks a
solution
Λ
:
L
∈
μ
}
K
of
κ
:an
assignment of concrete values to scalar logical variables for which the conjunction of
constraints in
κ
evaluates to true. It finally adds the picked solution to
λ
and drops
the solved constraints. The rule is nondeterministic, as
κ
might have multiple solu-
tions. When
κ
has no solutions, the rule cannot apply and executions gets stuck at
pick
: we call such executions
infeasible
. The rule is also agnostic with respect to the
exact method of solving simple constraints, as well as to the finitization mapping
Φ
.
The only requirement on
Φ
:
Σ
∀
∗
→
→
Σ
is that it is an over-approximation: any valid
solution of
υ
is also a solution of
Φ
(
υ
). In practice,
Φ
performs quantifier instantia-
tion: it replaces a quantified formula
∀
x
•
q
with a finite set of quantifier-free formulas
{
, for some finite set
R
of “relevant” symbolic values. The challenge
is to choose an
R
that is large enough to describe all relevant values in the current envi-
ronment, yet small enough to produce constraints that can be solved efficiently. Sec. 4
gives more details about Boogaloo's finitization procedure.
q
[
x
→
e
]
|
e
∈
R
}
Boogaloo vs. Boogie Semantics.
How does the operational semantics discussed in this
section compare with the original Boogie semantics? For this discussion, a
semantics
of a program
P
is a set of sequences of concrete states, corresponding to its feasible
terminating executions; a (concrete) state
C
=
σ,τ
consists of a store
σ
(involving
finitely many variables) and a termination flag
τ
∈{
✧
,
✓
,
✗
}
.Astate
C
is
finitary
if
it involves only finite maps: for all
m
∈
dom(
σ
),
|
dom(
σ
[
m
])
|
is finite; otherwise, it
is
infinitary
.Astate
C
F
finitizes
another state
C
(written
C
F
F
C
)iff
C
F
is finitary,
τ
F
=
τ
, dom(
σ
F
)=dom(
σ
) and, for all map variables
m
σ
[
m
].
A sequence
e
of states is finitary (infinitary) if all its elements are finitary (infinitary);
e
finitizes another sequence
e
if every state of
e
finitizes the corresponding state of
e
.
For a program
P
,
∈
dom(
σ
),
σ
F
[
m
]
⊆
[
P
] denotes the Boogie semantics defined in [17], which is infini-
tary since all maps are total; and
I
[
P
] denotes the finitary semantics of this paper, where
all maps have finite domains. Assuming perfect constraint-solving capabilities, the only
aspect where
F
is in the rule
PICK
, and more precisely in
the finitization mapping
Φ
. The requirement that
Φ
be an over-approximation implies
F
maydropinformationw.r.t.
I
