From c8fb1fb5f4c93629ec302a49286d75d58f000536 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <basile.clement@ocamlpro.com>
Date: Fri, 29 Mar 2024 16:08:58 +0100
Subject: [PATCH] feat(BV): Display BV constants using hexadecimal

We currently always print bit-vector constants using binary
representation. This can lead to quite large values in models when using
32- or 64-bit values that are essentially unreadable. When the
bit-vector width is a multiple of 4, this patch uses hexadecimal
notation instead, as allowed by the SMT-LIB specification.

Note that this only applies to bit-vector terms; bit-vector semantic
values are always printed in their binary representation for debugging
purposes.
---
 src/lib/structures/expr.ml                        | 5 ++++-
 tests/bitv/testfile-bv2nat-models.dolmen.expected | 2 +-
 tests/models/bitv/bvand-1.models.expected         | 4 ++--
 tests/models/bitv/bvand-2.models.expected         | 2 +-
 tests/models/bitv/bvor-1.models.expected          | 4 ++--
 tests/models/bitv/bvor-2.models.expected          | 2 +-
 tests/models/bitv/bvxor-1.models.expected         | 4 ++--
 tests/models/bitv/bvxor-2.models.expected         | 2 +-
 tests/models/bitv/specified.models.expected       | 2 +-
 9 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 4bf0cfdcc..828697b15 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -462,7 +462,10 @@ module SmtPrinter = struct
       pp_rational ppf q
 
     | Sy.Bitv (n, s), [] ->
-      Fmt.pf ppf "#b%s" (Z.format (Fmt.str "%%0%db" n) s)
+      if n mod 4 = 0 then
+        Fmt.pf ppf "#x%s" (Z.format (Fmt.str "%%0%dx" (n / 4)) s)
+      else
+        Fmt.pf ppf "#b%s" (Z.format (Fmt.str "%%0%db" n) s)
 
     | Sy.MapsTo v, [t] ->
       Fmt.pf ppf "@[<2>(ae.mapsto %a %a@])" Var.print v pp t
diff --git a/tests/bitv/testfile-bv2nat-models.dolmen.expected b/tests/bitv/testfile-bv2nat-models.dolmen.expected
index a37f6f187..c79ed8694 100644
--- a/tests/bitv/testfile-bv2nat-models.dolmen.expected
+++ b/tests/bitv/testfile-bv2nat-models.dolmen.expected
@@ -1,5 +1,5 @@
 
 unknown
 (
-  (define-fun x () (_ BitVec 4) #b0111)
+  (define-fun x () (_ BitVec 4) #x7)
 )
diff --git a/tests/models/bitv/bvand-1.models.expected b/tests/models/bitv/bvand-1.models.expected
index 14d57ec04..97dc85664 100644
--- a/tests/models/bitv/bvand-1.models.expected
+++ b/tests/models/bitv/bvand-1.models.expected
@@ -1,6 +1,6 @@
 
 unknown
 (
-  (define-fun x () (_ BitVec 8) #b10100101)
-  (define-fun y () (_ BitVec 8) #b01011010)
+  (define-fun x () (_ BitVec 8) #xa5)
+  (define-fun y () (_ BitVec 8) #x5a)
 )
diff --git a/tests/models/bitv/bvand-2.models.expected b/tests/models/bitv/bvand-2.models.expected
index 959e4881d..389856c52 100644
--- a/tests/models/bitv/bvand-2.models.expected
+++ b/tests/models/bitv/bvand-2.models.expected
@@ -1,5 +1,5 @@
 
 unknown
 (
-  (define-fun x () (_ BitVec 8) #b00000101)
+  (define-fun x () (_ BitVec 8) #x05)
 )
diff --git a/tests/models/bitv/bvor-1.models.expected b/tests/models/bitv/bvor-1.models.expected
index 358806061..a9cd47cf5 100644
--- a/tests/models/bitv/bvor-1.models.expected
+++ b/tests/models/bitv/bvor-1.models.expected
@@ -1,6 +1,6 @@
 
 unknown
 (
-  (define-fun x () (_ BitVec 8) #b11111111)
-  (define-fun y () (_ BitVec 8) #b11111111)
+  (define-fun x () (_ BitVec 8) #xff)
+  (define-fun y () (_ BitVec 8) #xff)
 )
diff --git a/tests/models/bitv/bvor-2.models.expected b/tests/models/bitv/bvor-2.models.expected
index 504bb5f38..3d9364421 100644
--- a/tests/models/bitv/bvor-2.models.expected
+++ b/tests/models/bitv/bvor-2.models.expected
@@ -1,5 +1,5 @@
 
 unknown
 (
-  (define-fun x () (_ BitVec 8) #b11110101)
+  (define-fun x () (_ BitVec 8) #xf5)
 )
diff --git a/tests/models/bitv/bvxor-1.models.expected b/tests/models/bitv/bvxor-1.models.expected
index de8cce943..a131f5562 100644
--- a/tests/models/bitv/bvxor-1.models.expected
+++ b/tests/models/bitv/bvxor-1.models.expected
@@ -1,6 +1,6 @@
 
 unknown
 (
-  (define-fun x () (_ BitVec 8) #b00000000)
-  (define-fun y () (_ BitVec 8) #b10100101)
+  (define-fun x () (_ BitVec 8) #x00)
+  (define-fun y () (_ BitVec 8) #xa5)
 )
diff --git a/tests/models/bitv/bvxor-2.models.expected b/tests/models/bitv/bvxor-2.models.expected
index 87afcb376..2519dac8a 100644
--- a/tests/models/bitv/bvxor-2.models.expected
+++ b/tests/models/bitv/bvxor-2.models.expected
@@ -1,5 +1,5 @@
 
 unknown
 (
-  (define-fun x () (_ BitVec 8) #b11110000)
+  (define-fun x () (_ BitVec 8) #xf0)
 )
diff --git a/tests/models/bitv/specified.models.expected b/tests/models/bitv/specified.models.expected
index 720c05e74..58c561fdb 100644
--- a/tests/models/bitv/specified.models.expected
+++ b/tests/models/bitv/specified.models.expected
@@ -1,5 +1,5 @@
 
 unknown
 (
-  (define-fun x () (_ BitVec 4) #b0101)
+  (define-fun x () (_ BitVec 4) #x5)
 )