Information Technology Reference
In-Depth Information
where
K
is the set of concrete values defined above; unary
UOp
and binary
BOp
op-
erators are in Fig. 2, and
L
denotes a set of
logical variables
of the same types as the
concrete values. A logical variable
of type
T
corresponds to a symbolic placeholder
(a “promise”) for a concrete value of type
T
. To represent quantifiers in constraints, we
also introduce a set of
universal symbolic values
Σ
∀
::=
Σ
V
,where
Σ
V
is a symbolic expression, which can also include bound variables
V
. Given a set
X
of
expressions, LV(
X
) is the set of all logical variables appearing in
X
.
∀
V
:
T
+
•
Symbolic States.
A symbolic state (environment) is a tuple
E
=
σ,λ,μ,κ,υ,τ
,
where the store
σ
:
V
→
Σ
maps variables to symbolic values; the logical store
λ
:
L
→
Σ
maps scalar logical variables to symbolic values; the map store
μ
:
L
→
(
Σ
∗
→
Σ
) maps map logical variables to symbolic maps;
κ
⊂
Σ
is a finite set of
simple state constraints
;
υ
⊂
Σ
∀
is a finite set of
universal state constraints
;and
τ
is one of
✧
,
✓
,
✗
, denoting an intermediate state (
✧
), or the final state of a passing
(
) execution. The map store associates logical variables of map type to
symbolic maps
: finite maps whose domain and range are in
Σ
; symbolic maps extend
their finite domains as execution progresses;
pick
concretizes their domain and range,
turning symbolic maps into concrete ones.
✓
) or failing (
✗
Expression Evaluation.
Let
E
denote the set of all expressions defined by
E
in Fig. 2
but whose atoms range over
C
∪
V
∪
L
(i.e., including logical variables
L
). The
eval-
uation
of an expression
e
∈
E
in an environment
E
is a symbolic value in
Σ
.Weuse
E
=
E
e
to denote that
e
to
e
∈
the notation:
Σ
.Aswede-
tail shortly, evaluating an expression may change the environment; correspondingly,
e
∈
E
evaluates in
E
E
σ
,λ
,μ
,κ
,υ
,τ
denotes the updated environment, whose components are written
.
When convenient, we extend this notation to
sequences
e
=
e
1
,...,e
n
of expressions,
evaluated one after another. Fig. 3 shows the evaluation rules for the most interesting
expression kinds. Since evaluation does not change the
λ
,
κ
,and
τ
environment com-
ponents, Fig. 3 omits them. Also notice that evaluating a symbolic value never changes
the environment, and every concrete value evaluates to itself.
Rules
LOG
-
IN
and
LOG
-
OUT
describe the simple cases of evaluating a logical vari-
able
:if
λ
[
] is defined, it yields
's evaluation; otherwise,
evaluates to itself.
Rules
VA R
-
IN
and
VA R
-
OUT
describe the evaluation of a (program) variable
v
.If
it has already been initialized, the evaluation of
σ
[
v
] gives its symbolic value. Other-
wise (
VA R
-
OUT
), such as when
v
enters the scope or after executing
havoc
v
,
σ
[
v
] gets
initialized to a fresh logical variable
.
The rules for map selection are similar to those for variables but target the map store
μ
: if a map selection has already been evaluated, its symbolic value is returned (
SEL
-
IN
); otherwise, a fresh logical variable is generated and stored in
μ
(
SEL
-
OUT
).
Rules
UPD
and
LAMBDA
deal with evaluating expressions of map type for updates
and lambda abstractions. Both rules introduce a fresh map logical variable and add
to
υ
a universally quantified constraint that defines the map. Thus, map expressions
(variables, updates, and lambdas) always evaluate to a logical variable; this justifies
using the evaluation
m
of
m
as an index in
μ
in the premises of
SEL
-
IN
,
SEL
-
OUT
,
and
UPD
.
