Mind the Gap: Bit-vector Interpolation recast
over Linear Integer Arithmetic
Takamasa Okudono
1,2
and Andy King
3
1 National Institute of Informatics, Tokyo, Japan
2 The Graduate University for Advanced Studies (SOKENDAI), Tokyo, Japan
3 University of Kent, Canterbury, UK
Abstract. Much of an interpolation engine for bit-vector (BV) arithmetic can be constructed by observing that BV arithmetic can be modeled with linear integer arithmetic (LIA). Two BV formulae can thus be
translated into two LIA formulae and then an interpolation engine for
LIA used to derive an interpolant, albeit one expressed in LIA. The construction is completed by back-translating the LIA interpolant into a BV
formula whose models coincide with those of the LIA interpolant. This
paper develops a back-translation algorithm showing, for the first time,
how back-translation can be universally applied, whatever the LIA interpolant. This avoids the need for deriving a BV interpolant by bit-blasting
the BV formulae, as a backup process when back-translation fails. The
new back-translation process relies on a novel geometric technique, called
gapping, the correctness and practicality of which are demonstrated.
1 Introduction
Given two formulae A and B which are inconsistent, an interpolant for the
ordered pair A, B is a formula I over the variables common to both A and B
which is a relaxation of A that is still inconsistent with B. For example, when
working over the theory of linear inequalities, if A = (x = y + 1) ∧ (y = 0)
and B = (x = z + 2) ∧ (1 ≤ z) then interpolants for A, B are I 1 = (x = 1),
I 2 = (x ≤ 1) and I 3 = (x < 3), ordering by increasing generality. The intuition
behind I 1 , I 2 and I 3 is that they are abstractions of A which concisely explain the
inconsistency between A and B. Interpolation has attracted growing attention
over the last decade [26], because of the crucial role it plays in model checking in
lazy [18] predicate abstraction [15] and lazy abstraction with interpolants [25],
as exemplified in BLAST [5] and IMPACT [25] respectively. In lazy predicate
abstraction [25], interpolation is used to synthesise predicates which describe
program state. Predicates are added, on demand, to explain why a path through
a program cannot reach an error state. In lazy abstraction with interpolants
[25], program state is described with unrestricted formulae, rather than merely
using predicates, and interpolation is applied to relax sequences of formulae
that describe the states down paths which do not error. Interpolation simplify
these formulae but increasing the likelihood of covering, again accelerating path
exploration. In effect, interpolation is the key abstraction mechanism.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 79–96, 2020.
https://doi.org/10.1007/978-3-030-45190-5 5
TACAS
Evaluation
Artifact
2020
Accepted
over Linear Integer Arithmetic
Takamasa Okudono
1,2
and Andy King
3
1 National Institute of Informatics, Tokyo, Japan
2 The Graduate University for Advanced Studies (SOKENDAI), Tokyo, Japan
3 University of Kent, Canterbury, UK
Abstract. Much of an interpolation engine for bit-vector (BV) arithmetic can be constructed by observing that BV arithmetic can be modeled with linear integer arithmetic (LIA). Two BV formulae can thus be
translated into two LIA formulae and then an interpolation engine for
LIA used to derive an interpolant, albeit one expressed in LIA. The construction is completed by back-translating the LIA interpolant into a BV
formula whose models coincide with those of the LIA interpolant. This
paper develops a back-translation algorithm showing, for the first time,
how back-translation can be universally applied, whatever the LIA interpolant. This avoids the need for deriving a BV interpolant by bit-blasting
the BV formulae, as a backup process when back-translation fails. The
new back-translation process relies on a novel geometric technique, called
gapping, the correctness and practicality of which are demonstrated.
1 Introduction
Given two formulae A and B which are inconsistent, an interpolant for the
ordered pair A, B is a formula I over the variables common to both A and B
which is a relaxation of A that is still inconsistent with B. For example, when
working over the theory of linear inequalities, if A = (x = y + 1) ∧ (y = 0)
and B = (x = z + 2) ∧ (1 ≤ z) then interpolants for A, B are I 1 = (x = 1),
I 2 = (x ≤ 1) and I 3 = (x < 3), ordering by increasing generality. The intuition
behind I 1 , I 2 and I 3 is that they are abstractions of A which concisely explain the
inconsistency between A and B. Interpolation has attracted growing attention
over the last decade [26], because of the crucial role it plays in model checking in
lazy [18] predicate abstraction [15] and lazy abstraction with interpolants [25],
as exemplified in BLAST [5] and IMPACT [25] respectively. In lazy predicate
abstraction [25], interpolation is used to synthesise predicates which describe
program state. Predicates are added, on demand, to explain why a path through
a program cannot reach an error state. In lazy abstraction with interpolants
[25], program state is described with unrestricted formulae, rather than merely
using predicates, and interpolation is applied to relax sequences of formulae
that describe the states down paths which do not error. Interpolation simplify
these formulae but increasing the likelihood of covering, again accelerating path
exploration. In effect, interpolation is the key abstraction mechanism.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 79–96, 2020.
https://doi.org/10.1007/978-3-030-45190-5 5
TACAS
Evaluation
Artifact
2020
Accepted