separate decimal_string_of_bits from string_of_bits

4 files changed, 33 insertions, 8 deletions

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index 186e0a09..bacf59e7 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -115,6 +115,9 @@ let int_of_vec sign v = maybe_failwith (int_of_vec_maybe sign v)
 val string_of_bits : list bitU -> string
 let string_of_bits = string_of_bv
 
+val decimal_string_of_bits : list bitU -> string
+let decimal_string_of_bits = decimal_string_of_bv
+
 val and_vec : list bitU -> list bitU -> list bitU
 val or_vec  : list bitU -> list bitU -> list bitU
 val xor_vec : list bitU -> list bitU -> list bitU
diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index a7fb7c50..d47d9b40 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -120,6 +120,9 @@ let int_of_vec_fail sign w = return (int_of_vec sign w)
 val string_of_bits : forall 'a. Size 'a => mword 'a -> string
 let string_of_bits = string_of_bv
 
+val decimal_string_of_bits : forall 'a. Size 'a => mword 'a -> string
+let decimal_string_of_bits = decimal_string_of_bv
+
 val and_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val or_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val xor_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index fd742fb1..8957f0dd 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -628,6 +628,24 @@ let exts_bv n v = exts_bits n (bits_of v)
 val string_of_bv : forall 'a. Bitvector 'a => 'a -> string
 let string_of_bv v = show_bitlist (bits_of v)
 
+val int_of_bit : bitU -> integer
+let int_of_bit b =
+  match b with
+  | B0 -> 0
+  | B1 -> 1
+  | _ -> failwith "int_of_bit saw unknown"
+  end
+
+val decimal_string_of_bv : forall 'a. Bitvector 'a => 'a -> string
+let decimal_string_of_bv bv =
+  let place_values =
+    List.mapi
+      (fun i b -> (int_of_bit b) * (2 ** i))
+      (List.reverse (bits_of bv))
+  in
+  let sum = List.foldl (+) 0 place_values in
+  show sum
+
 (*** Bytes and addresses *)
 
 type memory_byte = list bitU
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 03559fba..fbe700aa 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -384,15 +384,16 @@ let string_of_hex = function
 let string_of_bits bits =
   if List.length bits mod 4 == 0
   then "0x" ^ String.concat "" (List.map string_of_hex (break 4 bits))
-  else
-    let place_values =
-      List.mapi
-        (fun i b -> (Big_int.mul (bigint_of_bit b) (Big_int.pow_int_positive 2 i)))
-        (List.rev bits)
-    in
-    let sum = List.fold_left Big_int.add Big_int.zero place_values in
-    Big_int.to_string sum
+  else "0b" ^ String.concat "" (List.map string_of_bit bits)
 
+let decimal_string_of_bits bits =
+  let place_values =
+    List.mapi
+      (fun i b -> (Big_int.mul (bigint_of_bit b) (Big_int.pow_int_positive 2 i)))
+      (List.rev bits)
+  in
+  let sum = List.fold_left Big_int.add Big_int.zero place_values in
+  Big_int.to_string sum
 
 let hex_slice (str, n, m) =
   let bits = List.concat (List.map hex_char (list_of_string (String.sub str 2 (String.length str - 2)))) in