diff --git a/lib/sail.c b/lib/sail.c index a5e709c9c..4ffa07c81 100644 --- a/lib/sail.c +++ b/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; diff --git a/src/lib/sail_lib.ml b/src/lib/sail_lib.ml index 6c7027c7f..cc800179a 100644 --- a/src/lib/sail_lib.ml +++ b/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) = diff --git a/test/c/lib_valid_hex_bits.expect b/test/c/lib_valid_hex_bits.expect new file mode 100644 index 000000000..9766475a4 --- /dev/null +++ b/test/c/lib_valid_hex_bits.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/lib_valid_hex_bits.sail b/test/c/lib_valid_hex_bits.sail new file mode 100644 index 000000000..02501c151 --- /dev/null +++ b/test/c/lib_valid_hex_bits.sail @@ -0,0 +1,56 @@ +default Order dec + +$include +$include + +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"); +}