diff options
Diffstat (limited to 'src/sail_lib.ml')
| -rw-r--r-- | src/sail_lib.ml | 118 |
1 files changed, 118 insertions, 0 deletions
diff --git a/src/sail_lib.ml b/src/sail_lib.ml index afacf681..89056347 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -1,6 +1,9 @@ module Big_int = Nat_big_num type 'a return = { return : 'b . 'a -> 'b } +type 'za zoption = | ZNone of unit | ZSome of 'za;; + +let zint_forwards i = string_of_int (Big_int.to_int i) let opt_trace = ref false @@ -491,6 +494,28 @@ 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_drop (str, n) = 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) + +let string_append (s1, s2) = s1 ^ s2 + +(* highly inefficient recursive implementation *) +let rec maybe_int_of_prefix = function + | "" -> ZNone () + | str -> + let len = String.length str in + match int_of_string_opt str with + | Some n -> ZSome (Big_int.of_int n, Big_int.of_int len) + | None -> maybe_int_of_prefix (String.sub str 0 (len - 1)) + +let maybe_int_of_string str = + match int_of_string_opt str with + | None -> ZNone () + | Some n -> ZSome (Big_int.of_int n) + let lt_int (x, y) = Big_int.less x y let set_slice (out_len, slice_len, out, n, slice) = @@ -634,6 +659,98 @@ let speculate_conditional_success () = true (* Return nanoseconds since epoch. Truncates to ocaml int but will be OK for next 100 years or so... *) let get_time_ns () = Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())) +let rec n_leading_spaces s = + match String.length s with + | 0 -> 0 + | 1 -> begin match s with + | " " -> 1 + | _ -> 0 + end + | len -> begin match String.get s 0 with + | ' ' -> 1 + (n_leading_spaces (String.sub s 1 (len - 1))) + | _ -> 0 + end + + +let opt_spc_matches_prefix s = + ZSome ((), n_leading_spaces s |> Big_int.of_int) + +let spc_matches_prefix s = + let n = n_leading_spaces s in + match n with + | 0 -> ZNone () + | n -> ZSome ((), Big_int.of_int n) + +let hex_bits_5_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 < 32 then + ZSome ((bits_of_int 16 n, len)) + else + ZNone () + +let hex_bits_6_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 < 64 then + ZSome ((bits_of_int 32 n, len)) + else + ZNone () + +let hex_bits_12_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 < 4096 then + ZSome ((bits_of_int 2048 n, len)) + else + ZNone () + +let hex_bits_13_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 < 8192 then + ZSome ((bits_of_int 4096 n, len)) + else + ZNone () + +let hex_bits_20_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 < 1048576 then + ZSome ((bits_of_int 524288 n, len)) + else + ZNone () + +let hex_bits_21_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 < 2097152 then + ZSome ((bits_of_int 1048576 n, len)) + else + ZNone () + +let hex_bits_32_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 < 4294967296 then + ZSome ((bits_of_int 2147483648 n, len)) + else + ZNone () + let string_of_bool = function | true -> "true" | false -> "false" @@ -659,3 +776,4 @@ let load_raw (paddr, file) = done with | End_of_file -> () + |