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

This patch implements constraint propagation for the logical operators
(and, or, xor) on bit-vectors.

The goal of this patch is to ensure that Alt-Ergo has a complete
understanding of the logical operators on bit-vectors, and in particular
that it will never violate the definition of the logical operators when
generating models. They are thus removed from the "suspicious" operators
(along with `int2bv` and `bv2nat` that are now handled through the
"delayed functions" mechanism, even though this patch does not impact
these functions).

The patch can be decomposed in changes of the following categories,
where each category can mostly be reviewed independently (all in the
same patch because they wouldn't really make sense on their own):

 - Some minor refactoring in `Bitv`, `Th_util`, `Expr`, `ModelMap` and
   `Symbols` to expose the required functions and types, including a
   `Th_bitv` constructor for bit-vector case-splits and a built-in
   symbol for `bvxor`

 - The new `Bitlist` module introduces a representation of bit-vector
   domains as bit-lists, i.e. pairs of `(ones, zeroes)` represented as
   integers where the bits forced to `1` are set in `ones`, and the bits
   forced to `0` are set in `zeroes`.

 - There is a new `Congruence` module in `Rel_utils` that is exploited
   by the BV constraint propagators. The `Congruence` module can be
   understood as a lighter version of `Use` for semantic values (rather
   than terms): it provides a mechanism to register "semantic values of
   interest" (in our case, it will be the arguments of the logical
   operators and the result of the logical operator themselves) and be
   notified when the representative of these semantic values of interest
   are updated. To avoid partially inconsistent states, the congruence
   module computes the leaves the each semantic values of interest and
   updates all the semantic values that have a given leaf at once.

   This `Congruence` module is not BV-specific, hence why it is in
   `Rel_utils`.

 - Finally, the main course is in the `Bitv_rel` module, where the new
   constraint propagators are added. The constraint propagators are
   represented using separate `Domains` and `Constraints` modules that
   are kept normalized (i.e. they only reference current class
   representatives in `Uf`) through the `Congruence` utility.

   The `Domains` module is simply a map from class representatives to
   their domain, represented as a `Bitlist`. To avoid unnecessary
   propagations, the `Domains` module keeps track of the values whose
   domain has changed since the last propagation, to know that we must
   propagate the associated constraints again.

   The `Constraints` module is a set of `Constraint`s that keeps track
   of the semantic values that are involved in each constraint to avoid
   unnecessary propagations. The `Constraint`s are normalized (so that
   if we have both `a = b & c` and `a = b & d`, we only keep one once we
   learn that `c = d`), and we also keep track of the constraints that
   were never propagated.

   The `Bitv_rel` environment then keeps track of a `Domains` and a
   `Constraints` set that are updated through `Congruence` whenever a
   class representative changes (detected through equalities with
   `Subst` origin). After each change to either the domains or the
   constraints (either through a class representative change or because
   we added a new constraint), we propagate the fresh constraints and
   the constraints involving values whose domain has changed. We
   maintain the invariant that, outside of the `add` and `assume`
   functions, all the constraints in the `Constraints` set are satisfied
   by the domains of the `Domains`.

In the interest of keeping the patch relatively short and facilitate its
review, many desirable features have been left out for now, and there
are many places where the implementation can be improved. Notably:

 - We do not perform any sort of constraint simplification (outside of
   the normalization used for de-duplication). This can cause
   backtracking inefficiencies: if we have a constraint involving the
   concatenation `a @ b`, and we substitute `b -> c`, then detect a
   conflict involving `a`, the explanation for the substitution `b -> c`
   will end up in the conflict even though it had no impact, causing
   more work than necessary. This can be added in a second step.

 - The constraints are represented in a relational way rather than a
   functional way. This means that if we have both `a = b & c` and
   `d = b & c` as constraints, we will not learn that `a = d`. I don't
   think this has any impact currently, because the only way we can
   learn a constraint `a = b & c` is if `a` is equal to `b & c` as a
   term, but could have one in the future if we want to perform
   simplifications.

 - Only logical operators are supported. In particular, there is no
   support for combined reasoning with arithmetic, which is a whole can
   of worms in itself (in the current Alt-Ergo architecture, we do not
   have access to the interval domains from the bit-vector theory and
   conversely).

Finally, this patch purposely does not implement any sort of algebraic
reasoning on bit-vectors [^1]: while with this patch Alt-Ergo is able to
prove theorems such as De Morgan's laws or algebraic properties
(associativity, commutativity, neutral elements, inverses, etc.) of the
logical operators, this will currently happen through painstaking
case-splitting which gets slow on large bit-vector sizes [^2].

[^1]: The equation `x ^ x = 0` happens to be known as a side-effect of
the representation of XOR constraints.

[^2]: The value of "large" here is actually fairly small, because
proving these laws through propagation often requires exploring the full
space, which is exponential.

src/lib/dune

@@ -41,7 +41,7 @@
     Fun_sat 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,158 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     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)
+
+(* True if everything known by b2 is known by b1 (b1 has more info than b2) *)
+let subsumes b1 b2 =
+  let b1_known = bits_known b1 and b2_known = bits_known b2 in
+  Z.(equal (logand (lognot b1_known) b2_known) Z.zero)
+
+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,126 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     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 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 subsumes : t -> t -> bool
+(** [subsumes b1 b2] returns [true] if [b1] has more information than [b2].
+
+    More precisely, it checks that all the bits known by [b2] are also known by
+    [b1]; it *does not* check that [b1] and [b2] are consistent. *)
+
+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

@@ -178,6 +178,8 @@ type 'a alpha_term = {
   sz : int;
 }
 
+let pp_alpha_term pp ppf { bv; _ } = pp ppf bv
+
 let equal_alpha_term eq { bv = bv1; sz = sz1 } {bv = bv2; sz = sz2 } =
   Int.equal sz1 sz2 && eq bv1 bv2
 
@@ -294,6 +296,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 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
@@ -367,32 +398,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 ->
@@ -1377,6 +1382,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
@@ -1403,7 +1410,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