Solving Constraints over Bit-Vectors with SAT-based Model Checking Extended Abstract

Introduction

We present BVMC, a novel decision procedure for constraints over xed-width bit-vectors, which is based on propositional model checking (MC).

Nowadays, Satis ability Modulo Theory (SMT) [ 6 ] solvers for the quanti erfree xed-width bit-vector (QF BV) logic are widely used, especially when bitprecise reasoning is required. One subset of QF BV, which is particularly important in formal veri cation of software (SW), is quanti er-free linear arithmetic over integers modulo 2N (LIAN ). This paper presents an e cient decision procedure, BVMC, suitable for solving LIAN .

Formal veri cation of SW is one of the main forces driving SMT research. SW veri cation usually involves reasoning about arithmetic constraints, and in particular, linear arithmetic constraints over integers modulo 2N for some N 2 N. This is due to the fact that SW uses a nite representation for integers. More precisely, arithmetic operations over integers are interpreted over the ring Z=2N Z (\machine arithmetic") rather than over the ring Z. As a result, e cient bit-precise reasoning is highly desired.

In order to capture the semantics of linear arithmetic over Z=2N Z (LIAN ), SMT solvers for the theory of xed-width bit-vectors (BV solvers) are often used. BV solvers, however, are not e cient when the bit-vectors are wide. Namely, when the value of 2N is large (e.g. N = 128), solving linear arithmetic constraints over Z=2N Z becomes intractable for BV solvers. This ine ciency is mainly due to the way BV solvers are implemented: in most cases, the formula is reduced to a propositional formula using bit-blasting. Therefore, as N increases, so is the complexity of the resulting SAT formula. One way to overcome this ine ciency is by applying a LIA solver. Unlike BV solvers, LIA solvers reason about linear arithmetic over Z. While LIA solvers are more e cient than that of BV solvers for this task, they are less precise. This imprecision comes from the di erent semantics of LIA and LIAN . Namely, arithmetic operations over Z cannot result in an \over ow" (i.e. wrap-around). In the context of SW veri cation, this may lead to unsound results. Hence, an e cient LIAN solver, which this paper presents, should be extremely useful for SW veri cation.

Our Approach

Our novel decision procedure BVMC is based on a reduction of the input formula to a safety veri cation problem. Namely, a formula ' in LIAN is transformed to a transition system T such that the satis ability of ' corresponds to whether T is SAFE or UNSAFE. The key to our reduction lies in treating bit-vectors as unbounded streams of bits over time. More precisely, for each input bit-vector, the least signi cant bit (LSB) corresponds to time 0 in the corresponding stream, and the k-th bit corresponds to the bit received at time k. The structure of T captures the constraints between the bit-vector variables that appear in '. To determine if T is SAFE or UNSAFE, BVMC uses SAT-based model checking (SATMC) [ 10 ].

One possible way to reason about T is by using Bounded Model Checking (BMC) [ 2 ], an e cient SATMC algorithm that can show T is UNSAFE. Considering our reduction, if BMC nds a counterexample of length N in T (T is UNSAFE), then ' is satis able over Z=2N Z. If no counterexample of length N exists in T , then ' is unsatis able over Z=2N Z. This can be used as a decision procedure for LIAN . However, the performance of such an approach is usually not better then that of BV solvers [ 7 ]. BMC can either nd a counterexample of length N , or prove that counterexample of length N does not exist. In that sense, in the context of BVMC, it can only reason about LIAN for a given N . In fact, this approach is somewhat \equivalent" to how modern eager BV solvers are implemented. Consequently, this approach is, in general, not superior to solving the bit-blasted formula.

Unlike BMC, modern SATMC algorithms [ 8,3,9 ] use generalization in order to show that no counterexample, of any length, exists, and by that they can prove a transition system is SAFE. BVMC takes advantage of this generalization mechanism. In case BVMC nds ' to be unsatis able over Z=2kZ, SATMC's generalization mechanism is applied to show ' is unsatis able over Z=2N Z for every N > k. For the case a counterexample of length k is found, we have implemented an e cient procedure in BVMC that tries to extend the counterexample to some target N (where N > k) and by that show ' is satis able over Z=2N Z. When such a counterexample cannot be extended, BVMC blocks it and continues the search until either a new counterexample is found (possibly longer) or until unsatis ability is established.

Evaluation

As discussed above, our goal in designing BVMC is to support QF BV. Currently, we implemented a prototype which supports all bit-wise operators, as well as all operators required to support LIAN . For evaluation, we transformed the QF LIA subset of the SMT-COMP'16 benchmark to QF BV using xed-width bit-vectors of sizes 32, 64, and 128. We then compared BVMC to Boolector3 [ 4 ], and Z34 [ 5 ]. BVMC solved the most satis able instances out of the three, even for a width as low as 32. Moreover, it was able to solve many more instances, that were not solved by neither Boolector nor Z3.

Related and Future Work

A closely related line of work appears in [ 1,7 ], where a reduction from a fragment of BV, restricted to addition, shift by one and equality, to propositional model checking has been introduced (as a by-product of studying the complexity of bit-vector logic). The proposed method has been implemented and shown to outperform traditional SMT solvers on crafted BV benchmarks, restricted to the aforementioned BV fragment. Unlike the transformation applied by BVMC, the modeling suggested in [ 1 ] only supports xed-width bit-vectors, making SATMC algorithms ine cient. As a result, BDD-based model checking algorithms were found to be the most e cient experimentally [ 1 ]. BVMC shows how SATMC can be applied e ciently even for the subset supported by [ 1 ]5. In addition, our approach can handle a more extensive set of operators, which makes it applicable to arbitrary formulas in LIAN .

Our future work in this direction includes the following: { Extend our method to fully support QF BV, and { Implement dedicated SATMC algorithms that can e ciently solve transition systems originating from LIAN and from QF BV. 5 Note that throughout our experiments, the transition systems include more than thousands of state elements, making BDD-based MC intractable. 0

References

1. A. B. Andreas Frohlich, Gergely Kovasznai . E ciently solving bit-vector problems using model checkers . In 11th International Workshop on Satis ability Modulo Theories , 2013 .

2. A. Biere , A. Cimatti , E. M. Clarke , O. Strichman , and Y. Zhu . Bounded model checking . Advances in Computers , 58 : 117 { 148 , 2003 .

3. A. R. Bradley . SAT-Based Model Checking without Unrolling . In VMCAI , pages 70 { 87 , 2011 .

4. R. Brummayer and A. Biere . Boolector: An e cient SMT solver for bit-vectors and arrays . In Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009 , pages 174 { 177 , 2009 .

5. L. M. de Moura and N. Bj rner. Z3: an e cient SMT solver . In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008 , pages 337 { 340 , 2008 .

6. L. M. de Moura and N. Bj rner. Satis ability modulo theories: introduction and applications . Commun. ACM , 54 ( 9 ): 69 { 77 , 2011 .

7. G. Kovasznai , A. Frohlich, and A. Biere . Complexity of xed-size bit-vector logics . Theory Comput. Syst. , 59 ( 2 ): 323 { 376 , 2016 .

8. K. L. McMillan . Interpolation and SAT-Based Model Checking . In CAV , pages 1 { 13 , 2003 .

9. Y. Vizel and A. Gur nkel. Interpolating property directed reachability . In CAV , pages 260 { 276 , 2014 .

10. Y. Vizel , G. Weissenbacher, and S. Malik . Boolean satis ability solvers and their applications in model checking . Proceedings of the IEEE , 103 ( 11 ): 2021 { 2035 , 2015 .