Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
91
Inequalities such as c · x + n
2
n
c
· x/2
n
≤ b can be handled similarly. For
completeness, we note that expansion can be applied for non-powers of 2:
Proposition 4. Suppose n > 0. Then
c · x + n
c
· x/n ≤ b
LIA
=
u
i=
(c · x ≤ b − n
i ∧ ni ≤ c
· x ≤ ni − 1)
LIA
where = min{{c
· x/n | x ∈ M
d
} and u = max{{c
· x/n | x ∈ M
d
}.
4 Experiments
To evaluate the performance of boxing we implemented a model checker based
on the lazy abstraction (IMPACT) [25] algorithm. The model checker is implemented in Python 3.7.2 and uses MathSAT5 [9] for satisfiability checking and
interpolation over LIA. The model checker parses a subset of the C language, but
is rich enough to handle 312 benchmarks drawn from [2, 12]. The model checker
was instantiated in one of three ways to use: (1) LIA interpolation [17]; (2) BV
interpolation by covering the solutions of an LIA interpolate with columns (recall
f 2 of section 2); and (3) BV interpolation by covering the solutions of an LIA interpolate using boxing, gapping and flipping. Experiments were performed using
an Amazon Web Service EC2 c3.xlarge cloud architecture of 14 EC2 Computing
Units [31] each equipped with 4 cores and 7.5 GB of RAM. The timeout for each
run of IMPACT was set to 600 seconds.
All arithmetic is idealised in configuration (1) taking no account of integer
overflow and underflow. This is not, in general, safe. In configurations (2) and
(3) the model checker interprets machine arithmetic and bit operations using
the LIA encoding of BV operations outlined in [16, Fig 1]. This is safe but
complicates the LIA formulae, often substantially. One would expect this to
enlarge the interpolants, even before boxing and gapping are deployed. We would
also expect (1) to be substantially faster than (2) and (3). Due to differences
in the semantics of arithmetic, we might also see differences in the number of
programs proved to be safe or found to be unsafe. The experiments quantify
these predictions. To discuss the experiments, (2) will be referred to as the
naive encoding, even though it improves on complete enumeration (recall f 1 of
section 2).
4.1 Overall Result
Table 4.1 summarises the outcomes of running IMPACT on all 312 programs,
using the three different instances of interpolation, categorised as to whether
the run proved safety (safe rows) or found a counterexample (unsafe rows).
The Solved column of the left-hand table gives the total of the programs there
were either shown to be safe or unsafe within 600 seconds. Time is the mean
execution of a run (for all those programs which did not timeout). Size is mean
91
Inequalities such as c · x + n
2
n
c
· x/2
n
≤ b can be handled similarly. For
completeness, we note that expansion can be applied for non-powers of 2:
Proposition 4. Suppose n > 0. Then
c · x + n
c
· x/n ≤ b
LIA
=
u
i=
(c · x ≤ b − n
i ∧ ni ≤ c
· x ≤ ni − 1)
LIA
where = min{{c
· x/n | x ∈ M
d
} and u = max{{c
· x/n | x ∈ M
d
}.
4 Experiments
To evaluate the performance of boxing we implemented a model checker based
on the lazy abstraction (IMPACT) [25] algorithm. The model checker is implemented in Python 3.7.2 and uses MathSAT5 [9] for satisfiability checking and
interpolation over LIA. The model checker parses a subset of the C language, but
is rich enough to handle 312 benchmarks drawn from [2, 12]. The model checker
was instantiated in one of three ways to use: (1) LIA interpolation [17]; (2) BV
interpolation by covering the solutions of an LIA interpolate with columns (recall
f 2 of section 2); and (3) BV interpolation by covering the solutions of an LIA interpolate using boxing, gapping and flipping. Experiments were performed using
an Amazon Web Service EC2 c3.xlarge cloud architecture of 14 EC2 Computing
Units [31] each equipped with 4 cores and 7.5 GB of RAM. The timeout for each
run of IMPACT was set to 600 seconds.
All arithmetic is idealised in configuration (1) taking no account of integer
overflow and underflow. This is not, in general, safe. In configurations (2) and
(3) the model checker interprets machine arithmetic and bit operations using
the LIA encoding of BV operations outlined in [16, Fig 1]. This is safe but
complicates the LIA formulae, often substantially. One would expect this to
enlarge the interpolants, even before boxing and gapping are deployed. We would
also expect (1) to be substantially faster than (2) and (3). Due to differences
in the semantics of arithmetic, we might also see differences in the number of
programs proved to be safe or found to be unsafe. The experiments quantify
these predictions. To discuss the experiments, (2) will be referred to as the
naive encoding, even though it improves on complete enumeration (recall f 1 of
section 2).
4.1 Overall Result
Table 4.1 summarises the outcomes of running IMPACT on all 312 programs,
using the three different instances of interpolation, categorised as to whether
the run proved safety (safe rows) or found a counterexample (unsafe rows).
The Solved column of the left-hand table gives the total of the programs there
were either shown to be safe or unsafe within 600 seconds. Time is the mean
execution of a run (for all those programs which did not timeout). Size is mean