diff options
| -rw-r--r-- | riscv/prelude.sail | 44 | ||||
| -rw-r--r-- | src/sail_lib.ml | 141 |
2 files changed, 180 insertions, 5 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 8d56a756..7ddb9369 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -9,6 +9,10 @@ val def_spc : unit <-> string val hex_bits : forall 'n . (atom('n), bits('n)) <-> string +val hex_bits_3 : bits(3) <-> string +val hex_bits_3_forwards = "string_of_bits" : bits(3) -> string +val "hex_bits_3_matches_prefix" : string -> option((bits(3), nat)) + val hex_bits_4 : bits(4) <-> string val hex_bits_4_forwards = "string_of_bits" : bits(4) -> string val "hex_bits_4_matches_prefix" : string -> option((bits(4), nat)) @@ -21,6 +25,26 @@ val hex_bits_6 : bits(6) <-> string val hex_bits_6_forwards = "string_of_bits" : bits(6) -> string val "hex_bits_6_matches_prefix" : string -> option((bits(6), nat)) +val hex_bits_7 : bits(7) <-> string +val hex_bits_7_forwards = "string_of_bits" : bits(7) -> string +val "hex_bits_7_matches_prefix" : string -> option((bits(7), nat)) + +val hex_bits_8 : bits(8) <-> string +val hex_bits_8_forwards = "string_of_bits" : bits(8) -> string +val "hex_bits_8_matches_prefix" : string -> option((bits(8), nat)) + +val hex_bits_9 : bits(9) <-> string +val hex_bits_9_forwards = "string_of_bits" : bits(9) -> string +val "hex_bits_9_matches_prefix" : string -> option((bits(9), nat)) + +val hex_bits_10 : bits(10) <-> string +val hex_bits_10_forwards = "string_of_bits" : bits(10) -> string +val "hex_bits_10_matches_prefix" : string -> option((bits(10), nat)) + +val hex_bits_11 : bits(11) <-> string +val hex_bits_11_forwards = "string_of_bits" : bits(11) -> string +val "hex_bits_11_matches_prefix" : string -> option((bits(11), nat)) + val hex_bits_12 : bits(12) <-> string val hex_bits_12_forwards = "string_of_bits" : bits(12) -> string val "hex_bits_12_matches_prefix" : string -> option((bits(12), nat)) @@ -29,6 +53,18 @@ val hex_bits_13 : bits(13) <-> string val hex_bits_13_forwards = "string_of_bits" : bits(13) -> string val "hex_bits_13_matches_prefix" : string -> option((bits(13), nat)) +val hex_bits_14 : bits(14) <-> string +val hex_bits_14_forwards = "string_of_bits" : bits(14) -> string +val "hex_bits_14_matches_prefix" : string -> option((bits(14), nat)) + +val hex_bits_15 : bits(15) <-> string +val hex_bits_15_forwards = "string_of_bits" : bits(15) -> string +val "hex_bits_15_matches_prefix" : string -> option((bits(15), nat)) + +val hex_bits_16 : bits(16) <-> string +val hex_bits_16_forwards = "string_of_bits" : bits(16) -> string +val "hex_bits_16_matches_prefix" : string -> option((bits(16), nat)) + val hex_bits_20 : bits(20) <-> string val hex_bits_20_forwards = "string_of_bits" : bits(20) -> string val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat)) @@ -37,10 +73,18 @@ val hex_bits_21 : bits(21) <-> string val hex_bits_21_forwards = "string_of_bits" : bits(21) -> string val "hex_bits_21_matches_prefix" : string -> option((bits(21), nat)) +val hex_bits_28 : bits(28) <-> string +val hex_bits_28_forwards = "string_of_bits" : bits(28) -> string +val "hex_bits_28_matches_prefix" : string -> option((bits(28), nat)) + val hex_bits_32 : bits(32) <-> string val hex_bits_32_forwards = "string_of_bits" : bits(32) -> string val "hex_bits_32_matches_prefix" : string -> option((bits(32), nat)) +val hex_bits_33 : bits(33) <-> string +val hex_bits_33_forwards = "string_of_bits" : bits(33) -> string +val "hex_bits_33_matches_prefix" : string -> option((bits(33), nat)) + val spc_forwards : unit -> string function spc_forwards () = " " diff --git a/src/sail_lib.ml b/src/sail_lib.ml index a7f91beb..41b7c383 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)) - else "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)) *) + string_of_int (int_of_string ("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 @@ -494,9 +494,9 @@ let debug (str1, n, str2, v) = prerr_endline (str1 ^ Big_int.to_string n ^ str2 let eq_string (str1, str2) = String.compare str1 str2 == 0 -let string_startswith (str1, str2) = String.compare (String.sub str1 0 (String.length str2)) str2 == 0 +let string_startswith (str1, str2) = String.length str1 >= String.length str2 && String.compare (String.sub str1 0 (String.length str2)) str2 == 0 -let string_drop (str, n) = let n = Big_int.to_int n in String.sub str n (String.length str - n) +let string_drop (str, n) = if (Big_int.less_equal (Big_int.of_int (String.length str)) n) then "" else let n = Big_int.to_int n in String.sub str n (String.length str - n) let string_length str = Big_int.of_int (String.length str) @@ -692,6 +692,47 @@ let spc_matches_prefix s = | 0 -> ZNone () | n -> ZSome ((), Big_int.of_int n) +let hex_bits_1_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 2 then + ZSome ((bits_of_int 1 n, len)) + else + ZNone () + + +let hex_bits_2_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 4 then + ZSome ((bits_of_int 2 n, len)) + else + ZNone () + +let hex_bits_3_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 8 then + ZSome ((bits_of_int 4 n, len)) + else + ZNone () + +let hex_bits_4_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 16 then + ZSome ((bits_of_int 8 n, len)) + else + ZNone () + let hex_bits_5_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () @@ -712,6 +753,56 @@ let hex_bits_6_matches_prefix s = else ZNone () +let hex_bits_7_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 128 then + ZSome ((bits_of_int 64 n, len)) + else + ZNone () + +let hex_bits_8_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 256 then + ZSome ((bits_of_int 128 n, len)) + else + ZNone () + +let hex_bits_9_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 512 then + ZSome ((bits_of_int 256 n, len)) + else + ZNone () + +let hex_bits_10_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 1024 then + ZSome ((bits_of_int 512 n, len)) + else + ZNone () + +let hex_bits_11_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 2048 then + ZSome ((bits_of_int 1024 n, len)) + else + ZNone () + let hex_bits_12_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () @@ -732,6 +823,26 @@ let hex_bits_13_matches_prefix s = else ZNone () +let hex_bits_14_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 16384 then + ZSome ((bits_of_int 8192 n, len)) + else + ZNone () + +let hex_bits_15_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 32768 then + ZSome ((bits_of_int 16384 n, len)) + else + ZNone () + let hex_bits_16_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () @@ -762,6 +873,16 @@ let hex_bits_21_matches_prefix s = else ZNone () +let hex_bits_28_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 268435456 then + ZSome ((bits_of_int 134217728 n, len)) + else + ZNone () + let hex_bits_32_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () @@ -772,6 +893,16 @@ let hex_bits_32_matches_prefix s = else ZNone () +let hex_bits_33_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 8589934592 then + ZSome ((bits_of_int 4294967296 n, len)) + else + ZNone () + let string_of_bool = function | true -> "true" | false -> "false" |