From 86e74abc52d2cecd215666d1cb9f9baa504654dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <basile.clement@ocamlpro.com>
Date: Thu, 29 Aug 2024 19:13:59 +0200
Subject: [PATCH] fix(BV): Do not build unnormalized values in zero_extend

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.

This patch fixes the [zero_extend] function (and moves 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     | 21 +++++++++++++++++++--
 src/lib/reasoners/bitv.mli    |  5 ++++-
 src/lib/reasoners/bitv_rel.ml | 10 ++++------
 3 files changed, 27 insertions(+), 9 deletions(-)

diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index 66431a44b..e05e3c93f 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/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
diff --git a/src/lib/reasoners/bitv.mli b/src/lib/reasoners/bitv.mli
index 77b68f080..aecf132a0 100644
--- a/src/lib/reasoners/bitv.mli
+++ b/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
 
diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
index f7f72d70a..457bfc4c9 100644
--- a/src/lib/reasoners/bitv_rel.ml
+++ b/src/lib/reasoners/bitv_rel.ml
@@ -39,7 +39,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.
@@ -171,7 +171,7 @@ module BV2Nat = struct
         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') =
@@ -389,9 +389,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 ->
@@ -2230,7 +2228,7 @@ let case_split env uf ~for_model =
         Bitv.extract w bitidx bitidx (Shostak.Bitv.embed r)
       in
       (* Just always pick zero for now. *)
-      let zero = Shostak.Bitv.is_mine Bitv.[ { bv = Cte Z.zero ; sz = 1 } ] in
+      let zero = const 1 Z.zero in
       if Options.get_debug_bitv () then
         Printer.print_dbg
           ~module_name:"Bitv_rel" ~function_name:"case_split"