Lazy Bit-vector Solving and Witnessing Compiler Transformations

Liana Hadarean ( New York University )

The Satisfiability Modulo Theories (SMT) problem is a generalization of the Boolean satisfiability problem to first-order logic. SMT solvers are now at the forefront of automated reasoning and they are increasingly used in a number of diverse applications. In this talk I will first present a new decision procedure for the theory of fixed-width bit-vectors, and then describe an application of SMT techniques to verifying compiler transformations.

Most SMT solvers decide bit-vector constraints via eager reduction to propositional logic after first applying powerful word-level rewrite techniques. While often efficient in practice, this method does not scale on problems for which top-level rewrites cannot reduce the problem size sufficiently. We present a lazy solver that targets such problems by maintaining the word-level structure during search. This approach also enables efficient combination with the theory of arrays using variants of the Nelson-Oppen combination procedure.

The combination of the array and bit-vector theories offers a natural way of encoding the semantics of compiler intermediate representation languages. We show how to integrate an SMT solver with a compiler to build a “self-certifying” compiler: a compiler that generates a verifiable justification for its own correctness on every run. Our compiler produces as justification a refinement relation between the source and target programs of every optimization step. This “witness” relation is produced by an auxiliary witness generator, and is untrusted: its correctness is checked by an external SMT solver. Our implementation is based on the LLVM compiler: we have written generators for a number of intra-procedural optimizations. Preliminary results suggest the overhead of witness generation and checking make this approach practical.