Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
81
circuits for arithmetic) and show that the approach usually gives a modest slowdown relative to LIA. We also prove the validity of the BV encoding, and the
correctness of the reductions the encoding relies on, though the proofs themselves
are omitted here for brevity. To summarise, the contributions of this paper are
as follows:
– We show how interpolating theorem provers for LIA can be used to interpolate BV formulae, without recourse to bit-blasting.
– We develop a rigorous theory which explains gapping and proves that the
resulting BV interpolant has exactly the same set of models as the LIA
interpolant of the two BV formulae.
– We provide evaluation, within the established [6] framework of lazy abstraction with interpolants [25] which demonstrates the practicality of the approach for BV interpolation.
Use case Since BV formulae are converted to LIA one might wonder why one
cannot work with LIA throughout and avoid BV interpolation all together. First,
such an approach would not fit with a layered approach to interpolation [17]
where one uses one lightweight theory (eg. uninterpreted functors) and then, if
necessary, a more complicated one (eg. LIA) to construct a BV interpolant. BV
formulae provide a uniform way expressing interpolants, no matter how they are
derived. Second, computing LIA interpolants is complex and it is not surprising
that these engines contain subtle
5 bugs. Translating a LIA interpolant back
into a BV formula enables interpolants to be validated using a BV solver [3,
7, 27], using the reference (BV) semantics of a program. Moreover, validation
need make no assumption on the correctness of a translation between theories.
Validation can be performed on-the-fly, as the unwinding tree [25] is constructed,
or by translating the complete, stable unwinding tree into its BV counterpart.
The BV version can then be validated as a form of post-processing, akin to
post-fixpoint validation in abstract interpretation [4, 14].
Road map This paper is structured as follows: Section 2 gives the intuition behind boxing and gapping whereas Section 3 argues for the correctness of the
approach. Section 4 presents the experimental work. Section 5 presents the related work and section 6 concludes.
2 Boxing and Gapping in Pictures
Given a linear inequality , we seek to find a bit-vector formula f such that
f
BV
=
LIA
where
f
BV
and
LIA
are respectively the sets of solutions
(models) of f and in the linear integer arithmetic (LIA) and bit-vector (BV)
semantics. Ideally f should be compact where we measure size by the number
of binary logical connectives in f . This section gives the intuition behind two
5 We refrain from mentioning specific solvers because we do not want to embarrass
any particular research team to whom we are grateful.
81
circuits for arithmetic) and show that the approach usually gives a modest slowdown relative to LIA. We also prove the validity of the BV encoding, and the
correctness of the reductions the encoding relies on, though the proofs themselves
are omitted here for brevity. To summarise, the contributions of this paper are
as follows:
– We show how interpolating theorem provers for LIA can be used to interpolate BV formulae, without recourse to bit-blasting.
– We develop a rigorous theory which explains gapping and proves that the
resulting BV interpolant has exactly the same set of models as the LIA
interpolant of the two BV formulae.
– We provide evaluation, within the established [6] framework of lazy abstraction with interpolants [25] which demonstrates the practicality of the approach for BV interpolation.
Use case Since BV formulae are converted to LIA one might wonder why one
cannot work with LIA throughout and avoid BV interpolation all together. First,
such an approach would not fit with a layered approach to interpolation [17]
where one uses one lightweight theory (eg. uninterpreted functors) and then, if
necessary, a more complicated one (eg. LIA) to construct a BV interpolant. BV
formulae provide a uniform way expressing interpolants, no matter how they are
derived. Second, computing LIA interpolants is complex and it is not surprising
that these engines contain subtle
5 bugs. Translating a LIA interpolant back
into a BV formula enables interpolants to be validated using a BV solver [3,
7, 27], using the reference (BV) semantics of a program. Moreover, validation
need make no assumption on the correctness of a translation between theories.
Validation can be performed on-the-fly, as the unwinding tree [25] is constructed,
or by translating the complete, stable unwinding tree into its BV counterpart.
The BV version can then be validated as a form of post-processing, akin to
post-fixpoint validation in abstract interpretation [4, 14].
Road map This paper is structured as follows: Section 2 gives the intuition behind boxing and gapping whereas Section 3 argues for the correctness of the
approach. Section 4 presents the experimental work. Section 5 presents the related work and section 6 concludes.
2 Boxing and Gapping in Pictures
Given a linear inequality , we seek to find a bit-vector formula f such that
f
BV
=
LIA
where
f
BV
and
LIA
are respectively the sets of solutions
(models) of f and in the linear integer arithmetic (LIA) and bit-vector (BV)
semantics. Ideally f should be compact where we measure size by the number
of binary logical connectives in f . This section gives the intuition behind two
5 We refrain from mentioning specific solvers because we do not want to embarrass
any particular research team to whom we are grateful.