feat(BV): Word-level propagation for BV logic

src/lib/dune

@@ -42,7 +42,7 @@
     Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel
     Instances IntervalCalculus Intervals Ite_rel Ite Matching Matching_types
     Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml
-    Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use Rel_utils
+    Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use Rel_utils Bitlist
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols

src/lib/reasoners/bitlist.ml

@@ -0,0 +1,153 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
+(*     Copyright (C) 2013-2023 --- OCamlPro SAS                           *)
+(*                                                                        *)
+(*     This file is distributed under the terms of OCamlPro               *)
+(*     Non-Commercial Purpose License, version 1.                         *)
+(*                                                                        *)
+(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
+(*     use this file under the terms of the Apache Software License       *)
+(*     version 2.0.                                                       *)
+(*                                                                        *)
+(*     More details can be found in the directory licenses/               *)
+(*                                                                        *)
+(**************************************************************************)
+
+module Ex = Explanation
+
+exception Inconsistent of Ex.t
+
+(** A bitlist representing the known bits of a bit-vector of width [width].
+
+    Active bits in [bits_set] are necessarily equal to [1].
+    Active bits in [bits_clr] are necessarily equal to [0].
+
+    The explanation [ex] justifies that the bitlist applies. *)
+type t = { width: int ; bits_set : Z.t ; bits_clr : Z.t ; ex : Ex.t }
+
+let unknown width ex =
+  { width ; bits_set = Z.zero ; bits_clr = Z.zero ; ex }
+
+let empty =
+  { width = 0 ; bits_set = Z.zero ; bits_clr = Z.zero ; ex = Ex.empty }
+
+let width { width; _ } = width
+
+let explanation { ex; _ } = ex
+
+let exact width value ex =
+  { width
+  ; bits_set = value
+  ; bits_clr = Z.extract (Z.lognot value) 0 width
+  ; ex }
+
+let equal b1 b2 =
+  b1.width = b2.width &&
+  Z.equal b1.bits_set b2.bits_set &&
+  Z.equal b1.bits_clr b2.bits_clr
+
+let ones b = { b with bits_clr = Z.zero }
+
+let zeroes b = { b with bits_set = Z.zero }
+
+let add_explanation b ex = { b with ex = Ex.union b.ex ex }
+
+let pp ppf { width; bits_set; bits_clr; ex } =
+  for i = width - 1 downto 0 do
+    if Z.testbit bits_set i then
+      Fmt.pf ppf "1"
+    else if Z.testbit bits_clr i then
+      Fmt.pf ppf "0"
+    else
+      Fmt.pf ppf "?"
+  done;
+  if Options.(get_verbose () || get_unsat_core ()) then
+    Fmt.pf ppf " %a" (Fmt.box Ex.print) ex
+
+let bitlist ~width ~bits_set ~bits_clr ex =
+  if not (Z.equal (Z.logand bits_set bits_clr) Z.zero) then
+    raise @@ Inconsistent ex;
+
+  { width; bits_set; bits_clr ; ex }
+
+let bits_known b = Z.logor b.bits_set b.bits_clr
+
+let num_unknown b = b.width - Z.popcount (bits_known b)
+
+let value b = b.bits_set
+
+let is_fully_known b =
+  Z.(equal (shift_right (bits_known b + ~$1) b.width) ~$1)
+
+let intersect b1 b2 ex =
+  let width = b1.width in
+  let bits_set = Z.logor b1.bits_set b2.bits_set in
+  let bits_clr = Z.logor b1.bits_clr b2.bits_clr in
+  bitlist ~width ~bits_set ~bits_clr
+    (Ex.union b1.ex (Ex.union ex b2.ex))
+
+let concat b1 b2 =
+  let bits_set = Z.(logor (b1.bits_set lsl b2.width) b2.bits_set)
+  and bits_clr = Z.(logor (b1.bits_clr lsl b2.width) b2.bits_clr)
+  in
+  (* Always consistent *)
+  { width = b1.width + b2.width
+  ; bits_set
+  ; bits_clr
+  ; ex = Ex.union b1.ex b2.ex
+  }
+
+let ( @ ) = concat
+
+let extract b i j =
+  (* Always consistent *)
+  { width = j - i + 1
+  ; bits_set = Z.extract b.bits_set i (j - i + 1)
+  ; bits_clr = Z.extract b.bits_clr i (j - i + 1)
+  ; ex = b.ex
+  }
+
+let lognot b =
+  (* Always consistent *)
+  { b with bits_set = b.bits_clr; bits_clr = b.bits_set }
+
+let logand b1 b2 =
+  let width = b1.width in
+  let bits_set = Z.logand b1.bits_set b2.bits_set in
+  let bits_clr = Z.logor b1.bits_clr b2.bits_clr in
+  (* Always consistent *)
+  { width
+  ; bits_set
+  ; bits_clr
+  ; ex = Ex.union b1.ex b2.ex
+  }
+
+let logor b1 b2 =
+  let width = b1.width in
+  let bits_set = Z.logor b1.bits_set b2.bits_set in
+  let bits_clr = Z.logand b1.bits_clr b2.bits_clr in
+  (* Always consistent *)
+  { width
+  ; bits_set
+  ; bits_clr
+  ; ex = Ex.union b1.ex b2.ex
+  }
+
+let logxor b1 b2 =
+  let width = b1.width in
+  let bits_set =
+    Z.logor
+      (Z.logand b1.bits_set b2.bits_clr)
+      (Z.logand b1.bits_clr b2.bits_set)
+  and bits_clr =
+    Z.logor
+      (Z.logand b1.bits_set b2.bits_set)
+      (Z.logand b1.bits_clr b2.bits_clr)
+  in
+  (* Always consistent *)
+  { width
+  ; bits_set
+  ; bits_clr
+  ; ex = Ex.union b1.ex b2.ex
+  }

src/lib/reasoners/bitlist.mli

@@ -0,0 +1,120 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
+(*     Copyright (C) 2013-2023 --- OCamlPro SAS                           *)
+(*                                                                        *)
+(*     This file is distributed under the terms of OCamlPro               *)
+(*     Non-Commercial Purpose License, version 1.                         *)
+(*                                                                        *)
+(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
+(*     use this file under the terms of the Apache Software License       *)
+(*     version 2.0.                                                       *)
+(*                                                                        *)
+(*     More details can be found in the directory licenses/               *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Bit-lists provide a domain on bit-vectors that represent the known bits
+    sets to [1] and [0], respectively.
+
+    This module provides an implementation of bitlists and related operators.*)
+
+type t
+(** The type of bitlists.
+
+    Bitlists are indexed from the right: the least-significant bit has index
+    [0].
+
+    Bitlists include an explanation (that can be recovered through the
+    [explanation] function). The explanation indicates why the bitlist applies
+    to a value, which must be maintained separately.
+
+    The explanation associated with the result of any bitlist operation is the
+    union of the explanations associated with its arguments. *)
+
+val pp : t Fmt.t
+(** Pretty-printer for bitlists *)
+
+exception Inconsistent of Explanation.t
+(** Exception raised when an inconsistency is detected. *)
+
+val unknown : int -> Explanation.t -> t
+(** [unknown w ex] returns an bitlist of width [w] with no known bits. *)
+
+val empty : t
+(** An empty bitlist of width 0 and no explanation. *)
+
+val width : t -> int
+(** Returns the width of the bitlist. *)
+
+val explanation : t -> Explanation.t
+(** Returns the explanation associated with the bitlist. See the type-level
+    documentation for details. *)
+
+val exact : int -> Z.t -> Explanation.t -> t
+(** [exact w v ex] returns a bitlist of width [w] that represents the [w]-bits
+    constant [v]. *)
+
+val equal : t -> t -> bool
+(** [equal b1 b2] returns [true] if the bitlists [b1] and [b2] are equal, albeit
+    with possibly different explanations. *)
+
+val ones : t -> t
+(** [ones b] returns a bitlist where the zero bits in [b] are replaced with
+    unknown bits. *)
+
+val zeroes : t -> t
+(** [zeroes b] returns a bitlist where the one bits in [b] are replaced with
+    unknown bits. *)
+
+val add_explanation : t -> Explanation.t -> t
+(** [add_explanation b ex] adds the explanation [ex] to the bitlist [b]. The
+    returned bitlist has both the explanation of [b] and [ex] as explanation. *)
+
+val bits_known : t -> Z.t
+(** [bits_known b] returns the sets of bits known to be either [1] or [0] as a
+    bitmask. *)
+
+val num_unknown : t -> int
+(** [num_unknown b] returns the number of bits unknown in [b]. *)
+
+val is_fully_known : t -> bool
+(** [is_fully_known b] determines if there are unknown bits in [b] or not.
+    [is_fully_known b] is [true] iff [num_unknown b] is [0]. *)
+
+val value : t -> Z.t
+(** [value b] returns the value associated with the bitlist [b]. If the bitlist
+    [b] is not fully known, then only the known bits (those that are set in
+    [bits_known b]) are meaningful; unknown bits are set to [0]. *)
+
+val intersect : t -> t -> Explanation.t -> t
+(** [intersect b1 b2 ex] returns a new bitlist [b] that subsumes both [b1] and
+    [b2]. The explanation [ex] justifies that the two bitlists can be merged.
+
+    Raises [Inconsistent] if [b1] and [b2] are not compatible (i.e. there are
+    bits set in one bitlist and cleared in the other). The justification
+    includes the justifications of [b1] and [b2], as well as the justification
+    [ex] for the intersection. *)
+
+val lognot : t -> t
+(** [lognot b] swaps the bits that are set and cleared. *)
+
+val logand : t -> t -> t
+(** Bitwise and. *)
+
+val logor : t -> t -> t
+(** Bitwise or. *)
+
+val logxor : t -> t -> t
+(** Bitwise xor. *)
+
+val concat : t -> t -> t
+(** Bit-vector concatenation. *)
+
+val ( @ ) : t -> t -> t
+(** Alias for [concat]. *)
+
+val extract : t -> int -> int -> t
+(** [extract b i j] returns the bitlist from index [i] to index [j] inclusive.
+
+    The resulting bitlist has length [j - i + 1]. *)

src/lib/reasoners/bitv.ml

@@ -301,6 +301,35 @@ let fresh_bitv genre sz : bitv =
 
 let negate_bitv : bitv -> bitv = List.map negate_solver_simple_term
 
+let extract_st i j { bv; sz } =
+  if sz = j - i + 1 then
+    [ { bv ; sz } ]
+  else
+    match bv with
+    | Cte b -> [{ bv = Cte (Z.extract b i (j - i + 1)); sz = j - i + 1 }]
+    | Other r -> [{ bv = Ext (r, sz, i, j) ; sz = j - i + 1 }]
+    | Ext (r, sz, k, _) ->
+      [{ bv = Ext (r, sz, i + k, j + k) ; sz = j - i + 1 }]
+
+(* extract [i..j] from a composition of size [size]
+
+    an element of size [sz] at the head of the composition contains the bits
+    [size - 1 .. size - sz] inclusive *)
+let rec extract size i j = function
+  | [] ->
+    (* We can't extract from a bv of length 0! *)
+    assert false
+  | [ st ] ->
+    assert (st.sz = size);
+    extract_st i j st
+  | { sz; _ } :: sts when j < size - sz ->
+    extract (size - sz) i j sts
+  | ({ sz; _ } as st) :: _ when i >= size - sz ->
+    extract_st (i - (size - sz)) (j - (size - sz)) st
+  | ({ sz; _ } as st) :: sts ->
+    extract_st 0 (j - (size - sz)) st @
+    extract (size - sz) i (size - sz - 1) sts
+
 module type ALIEN = sig
   include Sig.X
   val embed : r abstract -> r
@@ -374,32 +403,6 @@ module Shostak(X : ALIEN) = struct
       let bv = embed r in
       if neg then negate_abstract bv, ctx else bv, ctx
 
-    let extract_st i j { bv; sz } =
-      match bv with
-      | Cte b -> [{ bv = Cte (Z.extract b i (j - i + 1)); sz = j - i + 1 }]
-      | Other r -> [{ bv = Ext (r, sz, i, j) ; sz = j - i + 1 }]
-      | Ext (r, sz, k, _) ->
-        [{ bv = Ext (r, sz, i + k, j + k) ; sz = j - i + 1 }]
-
-    (* extract i..j from a composition of size size
-
-       an element of size [sz] at the head of the composition contains the bits
-       [size - 1 .. size - sz] inclusive *)
-    let rec extract size i j = function
-      | [] ->
-        (* We can't extract a bv of length 0! *)
-        assert false
-      | [ st ] ->
-        assert (st.sz = size);
-        extract_st i j st
-      | { sz; _ } :: sts when j < size - sz ->
-        extract (size - sz) i j sts
-      | ({ sz; _ } as st) :: _ when i >= size - sz ->
-        extract_st (i - (size - sz)) (j - (size - sz)) st
-      | ({ sz; _ } as st) :: sts ->
-        extract_st 0 (j - (size - sz)) st @
-        extract (size - sz) i (size - sz - 1) sts
-
     let normalize_st st =
       match st.bv with
       | Ext (o, sz, i, j) when sz = j - i + 1 ->
@@ -1212,7 +1215,7 @@ module Shostak(X : ALIEN) = struct
        an abstract term, involving only constants and *fresh* A, B and C
        variables.
 
-       @raises Valid if the two terms are already equal. *)
+       @raise Valid if the two terms are already equal. *)
     let solve u v =
       if equal_abstract X.equal u v then raise Valid
       else begin
@@ -1391,6 +1394,8 @@ module Shostak(X : ALIEN) = struct
 
     match X.extract u , X.extract t with
     | None   , None   -> if X.str_cmp u t > 0 then [u,t] else [t,u]
+    | None   , Some [ { bv = Cte _; _ } ] -> [u,t]
+    | Some [ { bv = Cte _; _ } ],    None -> [t,u]
     | None   , Some t -> solve_ter (embed u) t
     | Some u , None   -> solve_ter u (embed t)
     | Some u , Some t -> solve_ter u t
@@ -1417,7 +1422,7 @@ module Shostak(X : ALIEN) = struct
           embed (X.subst x subs y.value)
       in
       let y' = if y.negated then negate_abstract y' else y' in
-      Canon.extract y_sz i j y' @ subst_rec x subs biv
+      extract y_sz i j y' @ subst_rec x subs biv
 
   let subst x subs biv =
     if Options.get_debug_bitv () then