Skip to content

Commit

Permalink
feat(BV): Display BV constants using hexadecimal
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
bclement-ocp committed Mar 29, 2024
1 parent f379389 commit c8fb1fb
Show file tree
Hide file tree
Showing 9 changed files with 15 additions and 12 deletions.
5 changes: 4 additions & 1 deletion src/lib/structures/expr.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion tests/bitv/testfile-bv2nat-models.dolmen.expected
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@

unknown
(
(define-fun x () (_ BitVec 4) #b0111)
(define-fun x () (_ BitVec 4) #x7)
)
4 changes: 2 additions & 2 deletions tests/models/bitv/bvand-1.models.expected
Original file line number Diff line number Diff line change
@@ -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)
)
2 changes: 1 addition & 1 deletion tests/models/bitv/bvand-2.models.expected
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@

unknown
(
(define-fun x () (_ BitVec 8) #b00000101)
(define-fun x () (_ BitVec 8) #x05)
)
4 changes: 2 additions & 2 deletions tests/models/bitv/bvor-1.models.expected
Original file line number Diff line number Diff line change
@@ -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)
)
2 changes: 1 addition & 1 deletion tests/models/bitv/bvor-2.models.expected
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@

unknown
(
(define-fun x () (_ BitVec 8) #b11110101)
(define-fun x () (_ BitVec 8) #xf5)
)
4 changes: 2 additions & 2 deletions tests/models/bitv/bvxor-1.models.expected
Original file line number Diff line number Diff line change
@@ -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)
)
2 changes: 1 addition & 1 deletion tests/models/bitv/bvxor-2.models.expected
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@

unknown
(
(define-fun x () (_ BitVec 8) #b11110000)
(define-fun x () (_ BitVec 8) #xf0)
)
2 changes: 1 addition & 1 deletion tests/models/bitv/specified.models.expected
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@

unknown
(
(define-fun x () (_ BitVec 4) #b0101)
(define-fun x () (_ BitVec 4) #x5)
)

0 comments on commit c8fb1fb

Please sign in to comment.