Information Technology Reference
In-Depth Information
that every Boogie execution is finitized by
some
Boogaloo execution. The converse does
not hold in general: in particular, for some programs
S
,
I
[
S
]=
∅
F
[
S
]
∅
contains
executions (which we regard as spurious). For example, the following program:
var
a
:
[
int
]
int
;
assume
(
but
=
∀
i, j
:
int
•
i<j
=
⇒
a[i] < a[j]);
a[1000]
=
1;
has no feasible executions in
assume
a[0]
=
0
∧
, while the current implementation of Boogaloo produces
a passing execution where the quantified constraint is only instantiated for
i
=0and
j
= 1000. Sec. 5 demonstrates that such unsound executions are infrequent in practice,
and, even when they occur, workarounds are possible, for example forcing the evalua-
tion on more points by accessing them in a loop. Also, Boogaloo's implementation of
Φ
does not produces spurious executions for programs where all quantified constraints
are derived from terminating recursive function definition (see Sec. 4).
There is an additional source of discrepancies between
I
, due to the fact that
Boogie always uses the specification semantics for loops and procedure calls, while
Boogaloo defaults to the implementation semantics, which might contain fewer exe-
cutions. This discrepancy between the two semantics is a useful feature, which makes
it possible to debug programs in presence of incomplete specifications. The specifica-
tion semantics is still available on demand in Boogaloo: it is sufficient to replace an
imperative construct with its specification.
I
and
F
4
Boogaloo: Implementation Details
This section presents some details of the Boogaloo tool—our prototype implementa-
tion of the approach described in the previous sections. The tool takes as input a Boogie
source file and a procedure name as entry point, and produces a set of feasible execu-
tions, characterized by their concrete initial and final states. Boogaloo is implemented
in Haskell, and uses the SMT solver Z3 [5] in the back-end.
Finitizing Universal Constraints.
The choice of the finitization mapping
Φ
plays an
important role. Our experiments suggest that the powerful quantifier instantiation strate-
gies available in SMT solvers such as Z3 have some downsides when applied to solve
constraints generated by executing Boogie programs, as their performance is unpre-
dictable unless additional user input (in the form of “triggers”) is provided. Instead,
Boogaloo preprocesses constraints using a simple strategy, based on the observation that
universally quantified formulas are typically used to axiomatize uninterpreted maps;
since we are only interested in finitely many points (those stored in
μ
), we just instanti-
ate the bound variables at those points. Quantified constraints that do not contain map
applications are simply ignored; the examples in Sec. 5 suggests that this finitization
strategy is not too restrictive on typical verification examples.
This is how Boogaloo implements
Φ
for a formula
P
(
x
). For each term
m
[
y
]
in
P
such that
y
includes some bound variable (i.e.,
y
∩
x
∀
x
•
), Boogaloo extracts
a parametrized map constraint of the form (
m,Q
(
y
,m
[
y
])),where
Q
is a subformula
of
P
including the term, and
y
are the parameters free in
Q
;if
x
⊆
y
,then
Q
is
itself quantified. For example,
=
∅
∀
i
•
a
[
i
]
>i
∧
b
[
i,
0] = 1 determines two parametrized
