fix(BV): Do not build unnormalized values in zero_extend (#1226)

There is a stupid bug in the [zero_extend] function introduced in #1154:
if the high bits of the extended value are known, it can create an
unnormalized semantic value, which causes unsoundness.

Fix the [zero_extend] function, which is renamed to [zero_extend_to]
since it takes as argument the extended size rather than the number of
additional bits to add. Move the implementation to the [Bitv] module.

To prevent similar failures in the future, an heavy assertion is added
in [solve] (where unsoundness would otherwise occur). I also tried to
make the [Bitv.abstract] type private again, but that was a pain as it
is used in several places in [Bitv_rel], so instead I simplified the
code to avoid creating [Bitv.abstract] values from outside of the [Bitv]
module where it was easy to do so.

No regression tests because I don't believe we can hit the bug with the
code in `next`: we are only calling [zero_extend] on variables, so we
can never create an unnormalized value this way.

src/lib/reasoners/bitv.ml

@@ -355,6 +355,14 @@ let sign_extend n sts =
         (repeat n [ extract_st (sz - 1) (sz - 1) st ])
         (st :: sts)
 
+let zero_extend sz sts =
+  if sz < 0 then
+    Fmt.invalid_arg "zero_extend: got negative extension: %d" sz;
+  match sts with
+  | { bv = (Cte _ as bv) ; sz = sz' } :: sts' ->
+    { bv ; sz = sz + sz' } :: sts'
+  | _ -> { bv = Cte Z.zero ; sz } :: sts
+
 module type ALIEN = sig
   include Sig.X
   val embed : r abstract -> r
@@ -1322,8 +1330,17 @@ module Shostak(X : ALIEN) = struct
         let varsU = get_vars u in
         let varsV = get_vars v in
         if Compat.List.is_empty varsU && Compat.List.is_empty varsV
-        then raise Util.Unsolvable
-        else
+        then (
+          (* If either side is non-normalized (this is a bug!!), it would be
+             unsound to raise [Unsolvable] here. *)
+          Options.heavy_assert (fun () ->
+              not @@
+              equal_abstract X.equal
+                (Canon.normalize u) (Canon.normalize v)
+            );
+
+          raise Util.Unsolvable
+        ) else
           begin
             let st_sys = slice u v in
             if Options.get_debug_bitv () then

src/lib/reasoners/bitv.mli

@@ -47,11 +47,14 @@ type 'a simple_term = ('a simple_term_aux) alpha_term
 
 type 'a abstract = 'a simple_term list
 
+val extract : int -> int -> int -> 'a abstract -> 'a abstract
 (** [extract size i j x] extracts [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. *)
-val extract : int -> int -> int -> 'a abstract -> 'a abstract
+
+val zero_extend : int -> 'a abstract -> 'a abstract
+(** [zero_extract sz bv] adds [sz] zeros to the front (high bits) of [bv]. *)
 
 val lognot : 'a abstract -> 'a abstract
 

src/lib/reasoners/bitv_rel.ml

@@ -41,7 +41,7 @@ let bitwidth r =
 
 
 let const sz n =
-  Shostak.Bitv.is_mine [ { bv = Cte (Z.extract n 0 sz); sz } ]
+  Shostak.Bitv.is_mine @@ Bitv.int2bv_const sz n
 
 module BitvNormalForm = struct
   (** Normal form for bit-vector values.
@@ -167,19 +167,19 @@ module BV2Nat = struct
         Bitv.extract (bitwidth bv) ofs (ofs + len - 1) @@
         Shostak.Bitv.embed bv
 
-      let zero_extend sz r =
+      let zero_extend_to sz r =
         let r_sz = bitwidth r in
         if sz < r_sz then invalid_arg "zero_extend";
         if sz = r_sz then r
         else
           Shostak.Bitv.is_mine @@
-          { Bitv.bv = Bitv.Cte Z.zero ; sz = sz - r_sz } ::
+          Bitv.zero_extend (sz - r_sz) @@
           Shostak.Bitv.embed r
 
       let mkv_eq (r, ext) (r', ext') =
         let sz = max ext.len ext'.len in
         let r = extract r ext and r' = extract r' ext' in
-        Uf.LX.mkv_eq (zero_extend sz r) (zero_extend sz r')
+        Uf.LX.mkv_eq (zero_extend_to sz r) (zero_extend_to sz r')
     end
   end
 
@@ -391,9 +391,7 @@ module BV2Nat = struct
       let lit =
         Uf.LX.mkv_eq
           (T.BV.extract bv ext)
-          (Shostak.Bitv.is_mine [
-              { bv = Cte (Z.extract cte 0 ext.len) ; sz = ext.len }
-            ])
+          (const ext.len cte)
       in
       { t with eqs = (lit, ex) :: t.eqs }
     | None ->
@@ -503,7 +501,7 @@ module BV2Nat = struct
           (* bv_r is extension of bv' *)
           Uf.LX.mkv_eq
             bv_r
-            (T.BV.zero_extend sz @@ T.BV.extract bv' ext')
+            (T.BV.zero_extend_to sz @@ T.BV.extract bv' ext')
       in
       { t with eqs = (lit, Ex.union ex ex') :: t.eqs }
     | exception Not_found ->