Fix implementation of valid_hex_bits

Previously it wasn't strict enough about the length of the hex string.

lib/sail.c

@@ -1654,7 +1654,7 @@ void decimal_string_of_lbits(sail_string *str, const lbits op)
 
 void parse_hex_bits(lbits *res, const mpz_t n, const_sail_string hex)
 {
-  if (strncmp(hex, "0x", 2) != 0) {
+  if (!valid_hex_bits(n, hex)) {
     goto failure;
   }
 
@@ -1675,11 +1675,48 @@ void parse_hex_bits(lbits *res, const mpz_t n, const_sail_string hex)
 }
 
 bool valid_hex_bits(const mpz_t n, const_sail_string hex) {
+  // The string must be prefixed by '0x'
   if (strncmp(hex, "0x", 2) != 0) {
     return false;
   }
 
-  for (int i = 2; i < strlen(hex); i++) {
+  size_t len = strlen(hex);
+
+  // There must be at least one character after the '0x'
+  if (len < 3) {
+    return false;
+  }
+
+  // Ignore any leading zeros
+  int non_zero = 2;
+  while (hex[non_zero] == '0' && non_zero < len - 1) {
+    non_zero++;
+  }
+
+  // Check how many bits we need for the first-non-zero (fnz) character.
+  int fnz_width;
+  char fnz = hex[non_zero];
+  if (fnz == '0') {
+    fnz_width = 0;
+  } else if (fnz == '1') {
+    fnz_width = 1;
+  } else if (fnz >= '2' && fnz <= '3') {
+    fnz_width = 2;
+  } else if (fnz >= '4' && fnz <= '7') {
+    fnz_width = 3;
+  } else {
+    fnz_width = 4;
+  }
+
+  // The width of the hex string is the width of the first non zero,
+  // plus 4 times the remaining hex digits
+  int hex_width = fnz_width + ((len - (non_zero + 1)) * 4);
+  if (mpz_cmp_si(n, hex_width) < 0) {
+    return false;
+  }
+
+  // All the non-zero characters must be valid hex digits
+  for (int i = non_zero; i < len; i++) {
     char c = hex[i];
     if (!((c >= '0' && c <= '9') || (c >= 'a' && c <= 'f') || (c >= 'A' && c <= 'F'))) {
       return false;

src/lib/sail_lib.ml

@@ -1115,15 +1115,33 @@ let is_hex_char ch =
   || (Char.code 'a' <= c && c <= Char.code 'f')
   || (Char.code 'A' <= c && c <= Char.code 'F')
 
-let valid_hex_bits (_, s) =
+let hex_char_width c =
+  if c = '0' then 0
+  else if c = '1' then 1
+  else if c = '2' || c = '3' then 2
+  else if c = '4' || c = '5' || c = '6' || c = '7' then 3
+  else 4
+
+let valid_hex_bits (n, s) =
   let len = String.length s in
   (* We must have at least the 0x prefix, then one character *)
   if len < 3 || String.sub s 0 2 <> "0x" then false
   else (
     let hex = String.sub s 2 (len - 2) in
     let is_valid = ref true in
-    String.iter (fun c -> is_valid := !is_valid && is_hex_char c) hex;
-    !is_valid
+    let actual_len = ref 0 in
+    let seen_non_zero = ref false in
+    String.iter
+      (fun c ->
+        if !seen_non_zero then actual_len := !actual_len + 4
+        else if c <> '0' then (
+          actual_len := !actual_len + hex_char_width c;
+          seen_non_zero := true
+        );
+        is_valid := !is_valid && is_hex_char c
+      )
+      hex;
+    !actual_len <= Big_int.to_int n && !is_valid
   )
 
 let parse_hex_bits (n, s) =

test/c/lib_valid_hex_bits.expect

@@ -0,0 +1 @@
+ok

test/c/lib_valid_hex_bits.sail

@@ -0,0 +1,56 @@
+default Order dec
+
+$include <prelude.sail>
+$include <hex_bits.sail>
+
+overload not = {not_bool}
+
+val main : unit -> unit
+
+function main() = {
+  foreach (n from 1 to 64) {
+    assert(not(valid_hex_bits(n, "not_hex_bits")));
+  };
+
+  assert(valid_hex_bits(1, "0x0"));
+  assert(valid_hex_bits(1, "0x1"));
+  assert(not(valid_hex_bits(1, "0x2")));
+  assert(not(valid_hex_bits(1, "0x3")));
+  assert(not(valid_hex_bits(1, "0x4")));
+  assert(not(valid_hex_bits(1, "0x5")));
+  assert(not(valid_hex_bits(1, "0x6")));
+  assert(not(valid_hex_bits(1, "0x7")));
+  assert(not(valid_hex_bits(1, "0x8")));
+  assert(not(valid_hex_bits(1, "0x9")));
+  assert(not(valid_hex_bits(1, "0xA")));
+  assert(not(valid_hex_bits(1, "0xB")));
+  assert(not(valid_hex_bits(1, "0xC")));
+  assert(not(valid_hex_bits(1, "0xD")));
+  assert(not(valid_hex_bits(1, "0xE")));
+  assert(not(valid_hex_bits(1, "0xF")));
+
+  assert(valid_hex_bits(2, "0x0"));
+  assert(valid_hex_bits(2, "0x00"));
+  assert(valid_hex_bits(2, "0x000"));
+  assert(valid_hex_bits(2, "0x0000"));
+
+  assert(valid_hex_bits(2, "0x3"));
+  assert(valid_hex_bits(2, "0x02"));
+  assert(valid_hex_bits(2, "0x001"));
+  assert(valid_hex_bits(2, "0x0003"));
+
+  assert(valid_hex_bits(2, "0x3"));
+  assert(valid_hex_bits(2, "0x02"));
+  assert(valid_hex_bits(2, "0x001"));
+  assert(valid_hex_bits(2, "0x0003"));
+
+  assert(valid_hex_bits(8, "0xFF"));
+  assert(valid_hex_bits(8, "0x0FF"));
+  assert(not(valid_hex_bits(8, "0xZF")));
+  assert(not(valid_hex_bits(8, "0x0ZF")));
+  assert(not(valid_hex_bits(8, "0xFZ")));
+  assert(not(valid_hex_bits(8, "0x0FZ")));
+  assert(not(valid_hex_bits(8, "0xZ0FZ")));
+
+  print_endline("ok");
+}