Re-implement space-related mapping functions in Sail rather than backends

Uses new primop 'string_take' which is much easier to implement in e.g. C

6 files changed, 75 insertions, 45 deletions

diff --git a/lib/sail.c b/lib/sail.c
index 9b7a1696..94cd5c2c 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -151,7 +151,25 @@ void string_drop(sail_string *dst, sail_string s, sail_int ns)
     *dst = realloc(*dst, (len - n) + 1);
     memcpy(*dst, s + n, len - n);
     (*dst)[len - n] = '\0';
+  } else {
+    *dst = realloc(*dst, 1);
+    **dst = '\0';
+  }
+}
+
+void string_take(sail_string *dst, sail_string s, sail_int ns)
+{
+  size_t len = strlen(s);
+  mach_int n = CREATE_OF(mach_int, sail_int)(ns);
+  mach_int to_copy;
+  if (len <= n) {
+    to_copy = len;
+  } else {
+    to_copy = n;
   }
+  *dst = realloc(*dst, to_copy + 1);
+  memcpy(*dst, s, to_copy);
+  *dst[to_copy] = '\0';
 }
 
 /* ***** Sail integers ***** */
diff --git a/lib/sail.h b/lib/sail.h
index 598ac67d..4ccd8b93 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -327,6 +327,7 @@ void random_real(real *rop, unit);
 
 void string_length(sail_int *len, sail_string s);
 void string_drop(sail_string *dst, sail_string s, sail_int len);
+void string_take(sail_string *dst, sail_string s, sail_int len);
 
 /* ***** Printing ***** */
 
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 1be06536..24913719 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -13,6 +13,7 @@ val hex_bits : forall 'n . (atom('n), bits('n)) <-> string
 
 val string_startswith = "string_startswith" : (string, string) -> bool
 val string_drop = "string_drop" : (string, nat) -> string
+val string_take = "string_take" : (string, nat) -> string
 val string_length = "string_length" : string -> nat
 val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
 val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat))
@@ -710,29 +711,6 @@ function hex_bits_64_backwards s =
   }
 
 
-
-val spc_forwards : unit -> string
-function spc_forwards () = " "
-val spc_backwards : string -> unit
-function spc_backwards s = ()
-
-val spc_matches_prefix = "spc_matches_prefix" : string -> option((unit, nat))
-
-val opt_spc_forwards : unit -> string
-function opt_spc_forwards () = ""
-val opt_spc_backwards : string -> unit
-function opt_spc_backwards s = ()
-
-val opt_spc_matches_prefix = "opt_spc_matches_prefix" : string -> option((unit, nat))
-
-val def_spc_forwards : unit -> string
-function def_spc_forwards () = " "
-val def_spc_backwards : string -> unit
-function def_spc_backwards s = ()
-
-val def_spc_matches_prefix = "opt_spc_matches_prefix" : string -> option((unit, nat))
-
-
 val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
@@ -1153,3 +1131,42 @@ function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
 /* Special version of zero_extend that the Lem back-end knows will be at a
    case split on 'm and uses a more generic type for.  (Temporary hack, honest) */
 val zero_extend_type_hack = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+
+
+val n_leading_spaces : string -> nat
+function n_leading_spaces s =
+  match s {
+    "" => 0,
+    _ => match string_take(s, 1) {
+      " " => 1 + n_leading_spaces(string_drop(s, 1)),
+      _ => 0
+    }
+  }
+
+val spc_forwards : unit -> string
+function spc_forwards () = " "
+val spc_backwards : string -> unit
+function spc_backwards s = ()
+val spc_matches_prefix : string -> option((unit, nat))
+function spc_matches_prefix s = {
+  let n = n_leading_spaces(s);
+  match n {
+    0 => None(),
+    _ => Some((), n)
+  }
+}
+
+val opt_spc_forwards : unit -> string
+function opt_spc_forwards () = ""
+val opt_spc_backwards : string -> unit
+function opt_spc_backwards s = ()
+val opt_spc_matches_prefix : string -> option((unit, nat))
+function opt_spc_matches_prefix s =
+  Some((), n_leading_spaces(s))
+
+val def_spc_forwards : unit -> string
+function def_spc_forwards () = " "
+val def_spc_backwards : string -> unit
+function def_spc_backwards s = ()
+val def_spc_matches_prefix : string -> option((unit, nat))
+function def_spc_matches_prefix s = opt_spc_matches_prefix(s)
diff --git a/src/gen_lib/sail2_string.lem b/src/gen_lib/sail2_string.lem
index c50db099..de7588dc 100644
--- a/src/gen_lib/sail2_string.lem
+++ b/src/gen_lib/sail2_string.lem
@@ -20,6 +20,10 @@ val string_drop : string -> ii -> string
 let string_drop str n =
   toString (drop (natFromInteger n) (toCharList str))
 
+val string_take : string -> ii -> string
+let string_take str n =
+  toString (take (natFromInteger n) (toCharList str))
+
 val string_length : string -> ii
 let string_length s = integerFromNat (stringLength s)
 
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index eecf9579..a718e6d5 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -530,6 +530,13 @@ let string_startswith (str1, str2) = String.length str1 >= String.length str2 &&
 
 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_take (str, n) =
+  let n = Big_int.to_int n in
+  if String.length str <= n then
+    str
+  else
+    String.sub str 0 n
+
 let string_length str = Big_int.of_int (String.length str)
 
 let string_append (s1, s2) = s1 ^ s2
@@ -704,28 +711,6 @@ 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)
-
 (* Python:
 f = """let hex_bits_{0}_matches_prefix s =
   match maybe_int_of_prefix s with
diff --git a/src/value.ml b/src/value.ml
index 6c9990a1..157c16fc 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -219,6 +219,10 @@ let value_string_drop = function
   | [v1; v2] -> V_string (Sail_lib.string_drop (coerce_string v1, coerce_int v2))
   | _ -> failwith "value string_drop"
 
+let value_string_take = function
+  | [v1; v2] -> V_string (Sail_lib.string_take (coerce_string v1, coerce_int v2))
+  | _ -> failwith "value string_take"
+
 let value_string_length = function
   | [v] -> V_int (coerce_string v |> Sail_lib.string_length)
   | _ -> failwith "value string_length"
@@ -549,6 +553,7 @@ let primops =
       ("eq_string", value_eq_string);
       ("string_startswith", value_string_startswith);
       ("string_drop", value_string_drop);
+      ("string_take", value_string_take);
       ("string_length", value_string_length);
       ("eq_bit", value_eq_bit);
       ("eq_anything", value_eq_anything);