C: Tweaks to RISC-V to get compiling to C

Revert a change to string_of_bits because it broke all the RISC-V
tests in OCaml. string_of_int (int_of_string x) is not valid because x may not
fit within an integer.

11 files changed, 101 insertions, 66 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index e5d2d6ea..61a1ff76 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -6,7 +6,7 @@ $include <flow.sail>
 // ***** Addition *****
 
 val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm.
-  (atom('n), atom('m)) -> atom('n + 'm)
+  (int('n), int('m)) -> int('n + 'm)
 
 val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int
 
@@ -15,15 +15,21 @@ overload operator + = {add_atom, add_int}
 // ***** Subtraction *****
 
 val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm.
-  (atom('n), atom('m)) -> atom('n - 'm)
+  (int('n), int('m)) -> int('n - 'm)
 
 val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int
 
 overload operator - = {sub_atom, sub_int}
 
+val sub_nat = {
+  ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
+  lem: "integerMinus",
+  _: "sub_nat"
+} : (nat, nat) -> nat
+
 // ***** Negation *****
 
-val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. atom('n) -> atom(- 'n)
+val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n)
 
 val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int
 
@@ -32,7 +38,7 @@ overload negate = {negate_atom, negate_int}
 // ***** Multiplication *****
 
 val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm.
-  (atom('n), atom('m)) -> atom('n * 'm)
+  (int('n), int('m)) -> int('n * 'm)
 
 val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int
 
diff --git a/lib/flow.sail b/lib/flow.sail
index c16763ee..5ee9a74a 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -1,8 +1,18 @@
 $ifndef _FLOW
 $define _FLOW
 
+/*
+
+This file contains the basic definitions for equality and comparison
+that is required for flow typing to work correctly. It should
+therefore be included in just about every Sail specification.
+
+*/
+
 val eq_unit : (unit, unit) -> bool
 
+val "eq_bit" : (bit, bit) -> bool
+
 function eq_unit(_, _) = true
 
 val not_bool = {coq: "negb", _: "not"} : bool -> bool
@@ -49,7 +59,7 @@ val gteq_int = {coq: "Z.geb", _:"gteq"} : (int, int) -> bool
 val lt_int = {coq: "Z.ltb", _:"lt"} : (int, int) -> bool
 val gt_int = {coq: "Z.gtb", _:"gt"} : (int, int) -> bool
 
-overload operator == = {eq_atom, eq_range, eq_int, eq_bool, eq_unit}
+overload operator == = {eq_atom, eq_range, eq_int, eq_bit, eq_bool, eq_unit}
 overload operator != = {neq_atom, neq_range, neq_int, neq_bool}
 overload operator | = {or_bool}
 overload operator & = {and_bool}
diff --git a/lib/sail.c b/lib/sail.c
index c702455c..886f6a37 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -301,6 +301,14 @@ void sub_int(sail_int *rop, const sail_int op1, const sail_int op2)
   mpz_sub(*rop, op1, op2);
 }
 
+void sub_nat(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  mpz_sub(*rop, op1, op2);
+  if (mpz_cmp_ui(*rop, 0) < 0ul) {
+    mpz_set_ui(*rop, 0ul);
+  }
+}
+
 inline
 void mult_int(sail_int *rop, const sail_int op1, const sail_int op2)
 {
@@ -361,7 +369,15 @@ void abs_int(sail_int *rop, const sail_int op)
   mpz_abs(*rop, op);
 }
 
-void pow2(sail_int *rop, const sail_int exp) {
+inline
+void pow_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  uint64_t n = mpz_get_ui(op2);
+  mpz_pow_ui(*rop, op1, n);
+}
+
+void pow2(sail_int *rop, const sail_int exp)
+{
   /* Assume exponent is never more than 2^64... */
   uint64_t exp_ui = mpz_get_ui(exp);
   mpz_t base;
diff --git a/lib/sail.h b/lib/sail.h
index 8533cd21..57897957 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -150,6 +150,7 @@ SAIL_INT_FUNCTION(undefined_range, sail_int, const sail_int, const sail_int);
  */
 SAIL_INT_FUNCTION(add_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(sub_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(sub_nat, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(mult_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(tdiv_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(tmod_int, sail_int, const sail_int, const sail_int);
@@ -162,6 +163,8 @@ SAIL_INT_FUNCTION(min_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(neg_int, sail_int, const sail_int);
 SAIL_INT_FUNCTION(abs_int, sail_int, const sail_int);
 
+SAIL_INT_FUNCTION(pow_int, sail_int, const sail_int, const sail_int);
+
 SAIL_INT_FUNCTION(pow2, sail_int, const sail_int);
 
 /* ***** Sail bitvectors ***** */
diff --git a/riscv/Makefile b/riscv/Makefile
index b5f518d8..80b3ebf7 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -2,7 +2,8 @@ SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail ris
 PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml
 SAIL_DIR ?= $(realpath ..)
 SAIL ?= $(SAIL_DIR)/sail
-C_WARNINGS ?= -Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
+C_WARNINGS ?=
+#-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
 C_SRCS = riscv_prelude.c riscv_platform.c
 
 export SAIL_DIR
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 6b2e13ff..5d418aad 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -1,5 +1,7 @@
 default Order dec
 
+$include <flow.sail>
+
 type bits ('n : Int) = vector('n, dec, bit)
 union option ('a : Type) = {None : unit, Some : 'a}
 
@@ -144,8 +146,17 @@ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
 
 overload operator == = {eq_atom, eq_int, eq_bit, eq_vec, eq_string, eq_real, eq_anything}
 
+val vector_subrange = {
+  ocaml: "subrange",
+  lem: "subrange_vec_dec",
+  c: "vector_subrange",
+  coq: "subrange_vec_dec"
+} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n.
+  (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1)
+/*
 val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
   (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+*/
 
 val bitvector_access = {c: "bitvector_access", ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n.
   (bits('n), atom('m)) -> bit
@@ -183,14 +194,6 @@ val not_vec = {c: "not_bits", _: "not_vec"} : forall 'n. bits('n) -> bits('n)
 
 overload ~ = {not_bool, not_vec}
 
-val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-
-function neq_atom (x, y) = not_bool(eq_atom(x, y))
-
-val neq_int = {lem: "neq"} : (int, int) -> bool
-
-function neq_int (x, y) = not_bool(eq_int(x, y))
-
 val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
 
 function neq_vec (x, y) = not_bool(eq_vec(x, y))
@@ -199,27 +202,15 @@ val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, '
 
 function neq_anything (x, y) = not_bool(x == y)
 
-overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
-
-val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
-
-val builtin_and_vec = {c: "and_bits", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-val and_vec = {lem: "and_vec", coq: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-function and_vec (xs, ys) = builtin_and_vec(xs, ys)
-
-overload operator & = {and_bool, and_vec}
-
-val or_bool = {coq: "orb", _:"or_bool"} : (bool, bool) -> bool
+overload operator != = {neq_vec, neq_anything}
 
-val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val or_vec = {lem: "or_vec", coq: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+overload operator & = {and_vec}
 
-function or_vec (xs, ys) = builtin_or_vec(xs, ys)
+val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-overload operator | = {or_bool, or_vec}
+overload operator | = {or_vec}
 
 val unsigned = {ocaml: "uint", lem: "uint", coq: "uint", c: "sail_unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
 
@@ -276,16 +267,16 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
 
 val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val int_power = {ocaml: "int_power", lem: "pow", coq: "pow"} : (int, int) -> int
+val int_power = {ocaml: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int
 
 val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> real
 
 overload operator ^ = {xor_vec, int_power, real_power, concat_str}
 
-val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p.
+val add_range = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val add_int = {ocaml: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int
+val add_int = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int
 
 val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -295,12 +286,12 @@ val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real
 
 overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
 
-val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
+val sub_range = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
-val sub_int = {ocaml: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int
+val sub_int = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int
 val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
-               lem: "integerMinus", coq: "sub_nat"}
+	       lem: "integerMinus", coq: "sub_nat", c: "sub_nat"}
             : (nat, nat) -> nat
 
 val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -372,10 +363,10 @@ val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int
 
 overload operator / = {quotient_nat, quotient, quotient_real}
 
-val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot"} : (int, int) -> int
-val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod"} : (int, int) -> int
+val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int
+val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int
 
-val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int
+val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int
 
 overload operator % = {modulus}
 
@@ -385,13 +376,13 @@ val shl_int = "shl_int" : (int, int) -> int
 
 val shr_int = "shr_int" : (int, int) -> int
 
-val min_nat = {ocaml: "min_int", lem: "min"} : (nat, nat) -> nat
+val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat
 
-val min_int = {ocaml: "min_int", lem: "min", coq: "Z.min"} : (int, int) -> int
+val min_int = {ocaml: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int
 
-val max_nat = {ocaml: "max_int", lem: "max"} : (nat, nat) -> nat
+val max_nat = {ocaml: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat
 
-val max_int = {ocaml: "max_int", lem: "max", coq: "Z.max"} : (int, int) -> int
+val max_int = {ocaml: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int
 
 overload min = {min_nat, min_int}
 
@@ -522,7 +513,7 @@ function vector64 n = __raw_GetSlice_int(64, n, 0)
 val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l)
 function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
 
-val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+val vector_update_subrange_dec = {ocaml: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
   (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
 val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o.
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 7268e9cc..6c341341 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -58,17 +58,17 @@ function mem_read (addr, width, aq, rl, res) = {
   }
 }
 
-val MEMea = {ocaml: "memea", lem: "MEMea"} : forall 'n.
+val MEMea = {lem: "MEMea", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_release = {ocaml: "memea", lem: "MEMea_release"} : forall 'n.
+val MEMea_release = {lem: "MEMea_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_strong_release = {ocaml: "memea", lem: "MEMea_strong_release"} : forall 'n.
+val MEMea_strong_release = {lem: "MEMea_strong_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional = {ocaml: "memea", lem: "MEMea_conditional"} : forall 'n.
+val MEMea_conditional = {lem: "MEMea_conditional", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional_release = {ocaml: "memea", lem: "MEMea_conditional_release"} : forall 'n.
+val MEMea_conditional_release = {lem: "MEMea_conditional_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional_strong_release = {ocaml: "memea", lem: "MEMea_conditional_strong_release"} : forall 'n.
+val MEMea_conditional_strong_release = {lem: "MEMea_conditional_strong_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
 
 val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}
@@ -136,13 +136,13 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
   }
 }
 
-val MEM_fence_rw_rw = {ocaml: "skip", lem: "MEM_fence_rw_rw"} : unit -> unit effect {barr}
-val MEM_fence_r_rw  = {ocaml: "skip", lem: "MEM_fence_r_rw"}  : unit -> unit effect {barr}
-val MEM_fence_r_r   = {ocaml: "skip", lem: "MEM_fence_r_r"}   : unit -> unit effect {barr}
-val MEM_fence_rw_w  = {ocaml: "skip", lem: "MEM_fence_rw_w"}  : unit -> unit effect {barr}
-val MEM_fence_w_w   = {ocaml: "skip", lem: "MEM_fence_w_w"}   : unit -> unit effect {barr}
-val MEM_fence_w_rw  = {ocaml: "skip", lem: "MEM_fence_w_rw"}  : unit -> unit effect {barr}
-val MEM_fence_rw_r  = {ocaml: "skip", lem: "MEM_fence_rw_r"}  : unit -> unit effect {barr}
-val MEM_fence_r_w   = {ocaml: "skip", lem: "MEM_fence_r_w"}   : unit -> unit effect {barr}
-val MEM_fence_w_r   = {ocaml: "skip", lem: "MEM_fence_w_r"}   : unit -> unit effect {barr}
-val MEM_fence_i     = {ocaml: "skip", lem: "MEM_fence_i"}     : unit -> unit effect {barr}
+val MEM_fence_rw_rw = {lem: "MEM_fence_rw_rw", _: "skip"} : unit -> unit effect {barr}
+val MEM_fence_r_rw  = {lem: "MEM_fence_r_rw", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_r_r   = {lem: "MEM_fence_r_r", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_rw_w  = {lem: "MEM_fence_rw_w", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_w_w   = {lem: "MEM_fence_w_w", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_w_rw  = {lem: "MEM_fence_w_rw", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_rw_r  = {lem: "MEM_fence_rw_r", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_r_w   = {lem: "MEM_fence_r_w", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_w_r   = {lem: "MEM_fence_w_r", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_i     = {lem: "MEM_fence_i", _: "skip"}     : unit -> unit effect {barr}
diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c
index 2ad3d3c1..d21824a3 100644
--- a/riscv/riscv_platform.c
+++ b/riscv/riscv_platform.c
@@ -46,3 +46,8 @@ void plat_insns_per_tick(sail_int *rop, unit u)
 
 mach_bits plat_htif_tohost(unit u)
 { return 0; }
+
+unit memea(mach_bits len, sail_int n)
+{
+  return UNIT;
+}
diff --git a/riscv/riscv_platform.h b/riscv/riscv_platform.h
index 2d63dca6..4401ad49 100644
--- a/riscv/riscv_platform.h
+++ b/riscv/riscv_platform.h
@@ -22,3 +22,6 @@ void plat_insns_per_tick(sail_int *rop, unit);
 
 unit plat_term_write(mach_bits);
 mach_bits plat_htif_tohost(unit);
+
+unit memea(mach_bits, sail_int);
+
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 94643ec2..59bff606 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -765,7 +765,7 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
 
 val load_reservation = {ocaml: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit
 
-val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success"} : xlenbits -> bool effect {exmem}
+val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success", c: "match_reservation"} : xlenbits -> bool effect {exmem}
 
 val cancel_reservation = {ocaml: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit
 
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 41b7c383..505227ef 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -373,9 +373,9 @@ let string_of_hex = function
   | _ -> failwith "Cannot convert binary sequence to hex"
 
 let string_of_bits bits =
-  (* if List.length bits mod 4 == 0
-   * then "0x" ^ String.concat "" (List.map string_of_hex (break 4 bits)) *)
-  string_of_int (int_of_string ("0b" ^ String.concat "" (List.map string_of_bit bits)))
+  if List.length bits mod 4 == 0
+  then "0x" ^ String.concat "" (List.map string_of_hex (break 4 bits))
+  else "0b" ^ String.concat "" (List.map string_of_bit bits)
 
 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