Bit-blasting

Bit-blasting decides formulas over fixed-width bit-vectors, the machine integers of programs and hardware, by reducing them to propositional satisfiability. Each $w$ -bit variable becomes $w$ Boolean variables, each operation becomes a Boolean circuit over those bits, the circuits are encoded as clauses with the Tseitin transformation, and a SAT solver decides the result^[1]. Addition becomes a ripple-carry adder, comparison a chain of bit comparisons, and multiplication an array of adders. The method is complete, since every bit-vector operation is a finite Boolean function, and it is how SMT solvers decide the theory of bit-vectors after simplifying at the word level^[3]^[4]^[5]. Its weakness is multiplication, whose circuits are quadratic in the width and notoriously hard for SAT solvers to reason about^[7].

§ 01

Bit-vector semantics

A bit-vector of width $w$ is a sequence of $w$ bits, read as an unsigned integer in $[0, 2^{w})$ or as a two's-complement integer in $[- 2^{w - 1}, 2^{w - 1})$ . Arithmetic is modulo $2^{w}$ : $x + y$ is $(x + y) mod 2^{w}$ , and overflow wraps around, exactly as in machine arithmetic. The SMT-LIB theory of fixed-size bit-vectors, QF_BV in its quantifier-free form, provides arithmetic, bitwise operations, shifts, signed and unsigned comparisons, concatenation and extraction^[11]. Bit-precise reasoning is what program analysis needs: a verifier that treats machine integers as mathematical integers misses overflow bugs, and one that treats them as bit-vectors finds them.

§ 02

Encoding

Every Boolean gate becomes a fresh variable $g$ with clauses that force it to equal its function of the inputs^[2]:

g \leftrightarrow a \land b : (\neg g \lor a) \land (\neg g \lor b) \land (g \lor \neg a \lor \neg b)

g \leftrightarrow a \oplus b : (\neg g \lor a \lor b) \land (\neg g \lor \neg a \lor \neg b) \land (g \lor \neg a \lor b) \land (g \lor a \lor \neg b)

Arithmetic is built from these. A full adder computes the sum bit and the carry of three bits:

s_{i} = a_{i} \oplus b_{i} \oplus c_{i} c_{i + 1} = (a_{i} \land b_{i}) \lor (c_{i} \land (a_{i} \oplus b_{i}))

and $w$ of them in a chain add two $w$ -bit numbers modulo $2^{w}$ , using $O (w)$ gates. Multiplication adds $w$ shifted partial products $a \cdot b_{i} \cdot 2^{i}$ , using $O (w^{2})$ gates. Equality is a conjunction of bitwise equivalences, and unsigned less-than a chain that decides at the most significant differing bit^[1].

A small DPLL solver with watched literals, used by the examples.

(* A small DPLL solver with two watched literals and no clause learning,
   enough for the circuits below. Literals are non-zero integers. *)
type t = {
  mutable nvars : int;
  mutable clauses : int array list;
}
 
let create () = { nvars = 0; clauses = [] }
let fresh s = s.nvars <- s.nvars + 1; s.nvars
let add s c = s.clauses <- Array.of_list c :: s.clauses
 
let decisions = ref 0
 
let solve s =
  let n = s.nvars in
  let cls = Array.of_list s.clauses in
  let assign = Array.make (n + 1) 0 and trail = Array.make (n + 1) 0 and len = ref 0 and qhead = ref 0 in
  let idx l = if l > 0 then 2 * l else (2 * -l) + 1 in
  let watches = Array.make ((2 * n) + 2) [] in
  let value l = let v = assign.(abs l) in if l > 0 then v else -v in
  let set l = assign.(abs l) <- (if l > 0 then 1 else -1); trail.(!len) <- l; incr len in
  let units = ref [] in
  Array.iteri (fun ci c ->
    if Array.length c = 1 then units := c.(0) :: !units
    else (watches.(idx c.(0)) <- ci :: watches.(idx c.(0)); watches.(idx c.(1)) <- ci :: watches.(idx c.(1)))) cls;
  let propagate () =
    let ok = ref true in
    while !ok && !qhead < !len do
      let f = - trail.(!qhead) in
      incr qhead;
      let pending = ref watches.(idx f) in
      watches.(idx f) <- [];
      while !pending <> [] do
        let ci = List.hd !pending in
        pending := List.tl !pending;
        let c = cls.(ci) in
        if c.(0) = f then (c.(0) <- c.(1); c.(1) <- f);
        let keep () = watches.(idx f) <- ci :: watches.(idx f) in
        if value c.(0) = 1 then keep ()
        else begin
          let k = ref 2 in
          while !k < Array.length c && value c.(!k) = -1 do incr k done;
          if !k < Array.length c then (c.(1) <- c.(!k); c.(!k) <- f; watches.(idx c.(1)) <- ci :: watches.(idx c.(1)))
          else begin
            keep ();
            if value c.(0) = -1 then (ok := false; watches.(idx f) <- !pending @ watches.(idx f); pending := [])
            else set c.(0)
          end
        end
      done
    done;
    !ok
  in
  let undo mark = for i = !len - 1 downto mark do assign.(abs trail.(i)) <- 0 done; len := mark; qhead := mark in
  let rec dpll () =
    if not (propagate ()) then false
    else
      let rec first v = if v > n then 0 else if assign.(v) = 0 then v else first (v + 1) in
      let v = first 1 in
      if v = 0 then true
      else begin
        let mark = !len in
        incr decisions;
        set (-v);
        dpll () || (undo mark; set v; dpll ()) || (undo mark; false)
      end
  in
  let ok = List.for_all (fun l -> if value l = -1 then false else (if value l = 0 then set l; true)) !units in
  if ok && dpll () then Some (Array.copy assign) else None

Bit-vector circuits encoded as clauses.

(* Bit-blasting: a bit-vector is an array of SAT literals, least
   significant bit first, and every operation is a circuit whose gates
   are encoded as clauses (the Tseitin encoding). Each instance of the
   functor has its own solver. *)
module type S = sig
  val s : Sat.t
  val clause : int list -> unit
  val var : int -> int array
  val add : int array -> int array -> int array
  val mul : int array -> int array -> int array
  val eq : int array -> int array -> int
end
 
module Make () = struct
  let s = Sat.create ()
  let fresh () = Sat.fresh s
  let clause = Sat.add s
 
  (* Constants 1 and 0 as literals. *)
  let tt = let v = fresh () in clause [ v ]; v
  let ff = - tt
 
  (* g <-> a /\ b,  g <-> a \/ b,  g <-> a xor b *)
  let and_ a b = let g = fresh () in clause [ -g; a ]; clause [ -g; b ]; clause [ g; -a; -b ]; g
  let or_ a b = - (and_ (-a) (-b))
  let xor_ a b =
    let g = fresh () in
    clause [ -g; a; b ]; clause [ -g; -a; -b ]; clause [ g; -a; b ]; clause [ g; a; -b ]; g
 
  let var w = Array.init w (fun _ -> fresh ())
  let const w k = Array.init w (fun i -> if (k lsr i) land 1 = 1 then tt else ff)
 
  (* Ripple-carry addition modulo 2^w: a full adder per bit. *)
  let add a b =
    let carry = ref ff in
    Array.init (Array.length a) (fun i ->
      let s = xor_ (xor_ a.(i) b.(i)) !carry in
      carry := or_ (and_ a.(i) b.(i)) (and_ !carry (xor_ a.(i) b.(i)));
      s)
 
  (* Shift-and-add multiplication modulo 2^w: w partial products. *)
  let mul a b =
    let w = Array.length a in
    let acc = ref (const w 0) in
    for i = 0 to w - 1 do
      let partial = Array.init w (fun j -> if j < i then ff else and_ a.(j - i) b.(i)) in
      acc := add !acc partial
    done;
    !acc
 
  (* Equality of two vectors as one literal, and unsigned a < b. *)
  let eq a b = let d = Array.map2 (fun x y -> - (xor_ x y)) a b in Array.fold_left and_ tt d
  let ult a b =
    (* scan from the least significant bit: lt := (not a_i and b_i) or (a_i = b_i and lt) *)
    let lt = ref ff in
    Array.iteri (fun i x -> let y = b.(i) in lt := or_ (and_ (-x) y) (and_ (- (xor_ x y)) !lt)) a;
    !lt
 
  let value model v = Array.fold_left (fun (acc, k) l -> ((if model.(abs l) = (if l > 0 then 1 else -1) then acc lor (1 lsl k) else acc), k + 1)) (0, 0) v |> fst
end

§ 03

Solving

A query asserts the output literal of a circuit and asks for a satisfying assignment, from which the values of the bit-vectors are read back. Asking for $x \cdot y = 143$ with $x, y > 1$ finds a factorization:

Factoring 143 with a multiplier circuit, with and without overflow.

(* Factor 143 with multiplier circuits. Bit-vector multiplication is
   modulo 2^w, so the first query finds a product that wraps around; the
   second zero-extends 8-bit operands to 16 bits so that it cannot. *)
let query w ext =
  let module B = Bv.Make () in
  let open B in
  let x = var 8 and y = var 8 in
  let widen v = if ext then Array.append v (const 8 0) else v in
  let p = mul (widen x) (widen y) in
  clause [ eq p (const w 143) ];
  clause [ ult (const 8 1) x ];
  clause [ ult (const 8 1) y ];
  let nv = s.Sat.nvars and nc = List.length s.Sat.clauses in
  match Sat.solve s with
  | Some m -> Printf.printf "%2d-bit product: %4d variables, %5d clauses: x = %3d, y = %3d, x * y = %d\n" w nv nc (value m x) (value m y) (value m x * value m y)
  | None -> Printf.printf "%2d-bit product: unsatisfiable\n" w

Running it.

 8-bit product:  517 variables,  1720 clauses: x = 129, y =  15, x * y = 1935
16-bit product: 1785 variables,  6108 clauses: x =  13, y =  11, x * y = 143

The 8-bit query finds $129 \cdot 15 = 1935 \equiv 143 (mod 256)$ : a correct answer to the question that was asked, since 8-bit multiplication wraps around. Zero-extending the operands to 16 bits before multiplying rules out overflow and gives the factorization $13 \cdot 11$ . The distinction is the one a program verifier has to get right, and the kind of bug bit-precise reasoning is used to find.

Proving identities

A property holds for all inputs exactly when its negation is unsatisfiable. Commutativity of addition and multiplication at width $w$ is proved by asserting $x + y \neq = y + x$ or $x \cdot y \neq = y \cdot x$ and finding no model:

Proving commutativity by unsatisfiability.

(* x + y = y + x and x * y = y * x hold for all w-bit x and y exactly when
   their negations are unsatisfiable. *)
let prove w name op =
  let module B = Bv.Make () in
  let x = B.var w and y = B.var w in
  let l = op (module B : Bv.S) x y and r = op (module B : Bv.S) y x in
  B.clause [ - (B.eq l r) ];
  Sat.decisions := 0;
  let result = Sat.solve B.s in
  Printf.printf "%-3s w = %-2d %6d vars %7d clauses   %s %9d decisions\n%!" name w B.s.Sat.nvars
    (List.length B.s.Sat.clauses) (if result = None then "proved        " else "counterexample") !Sat.decisions

Running it with the DPLL solver above.

x+y w = 4      65 vars     198 clauses   proved               255 decisions
x+y w = 6      97 vars     296 clauses   proved              4095 decisions
x+y w = 8     129 vars     394 clauses   proved             65535 decisions
x+y w = 10    161 vars     492 clauses   proved           1048575 decisions
x*y w = 3     133 vars     437 clauses   proved                42 decisions
x*y w = 4     229 vars     762 clauses   proved               170 decisions
x*y w = 5     351 vars    1177 clauses   proved               682 decisions
x*y w = 6     499 vars    1682 clauses   proved              2730 decisions
x*y w = 7     673 vars    2277 clauses   proved             10922 decisions

Without clause learning, the solver proves the adder identity by trying every combination of inputs, $2^{2 w} - 1$ decisions, since it branches on the input bits first and only finds a conflict once all of them are set. A CDCL solver learns clauses that summarize why each carry must agree and proves adder identities for any practical width almost immediately. Multipliers are different: equivalence of two multiplier circuits, even commutativity of one, remains hard for CDCL solvers even at moderate widths, and dedicated methods based on computer algebra are used to verify large multipliers^[7]. Binary decision diagrams have the same difficulty: Bryant proved that every BDD for the middle output bit of a multiplier has exponential size^[8].

§ 04

In SMT solvers

Solvers do not bit-blast a formula as written. Word-level preprocessing first rewrites it: constant propagation, normalization of arithmetic, elimination of variables defined by equations, and simplifications such as replacing multiplication by a constant with shifts and additions. What remains is bit-blasted, eagerly, all at once, or lazily, with parts of the formula handled at the word level and blasted only when needed^[6]. STP^[3] and Boolector^[4] pioneered this for program analysis; Z3^[5], cvc5 and Bitwuzla are current examples. Because the result is a SAT problem, bit-vector solvers inherit every improvement in SAT solving.

§ 05

Uses

Symbolic execution tools such as KLEE represent program values as bit-vector expressions and ask a solver for inputs that reach each branch^[9]. Bounded model checking unrolls a hardware or software transition system for a fixed number of steps and bit-blasts the result into one SAT query^[10]. Equivalence checking of circuits, superoptimization of instruction sequences, translation validation in compilers and the analysis of cryptographic code all reduce to bit-vector queries.

§ 06

History

Reducing arithmetic on machine words to propositional logic is as old as circuit design, and Tseitin's encoding of 1968 made the translation to clauses linear^[2]. Bounded model checking made bit-blasted SAT queries a mainstream verification technique in 1999^[10]. Ganesh and Dill's STP of 2007 and Brummayer and Biere's Boolector of 2009 showed that word-level preprocessing followed by bit-blasting could handle the formulas produced by program analysis^[3]^[4], and bit-vectors became one of the most used theories of SMT-LIB^[11].