riscv decode now uses mapping-decode and passes tests

2 files changed, 25 insertions, 4 deletions

diff --git a/src/gen_lib/sail_string.lem b/src/gen_lib/sail_string.lem
index b1f0fbe3..07b39ddc 100644
--- a/src/gen_lib/sail_string.lem
+++ b/src/gen_lib/sail_string.lem
@@ -66,10 +66,10 @@ let rec n_leading_spaces s =
            end
   end
 
-let opt_spaces_matches_prefix s =
+let opt_spc_matches_prefix s =
   Just ((), n_leading_spaces s)
 
-let spaces_matches_prefix s =
+let spc_matches_prefix s =
   let n = n_leading_spaces s in
   match n with
   | 0 -> Nothing
@@ -136,4 +136,15 @@ let hex_bits_21_matches_prefix s =
        Nothing
   end
 
+let hex_bits_32_matches_prefix s =
+  match maybe_int_of_prefix s with
+  | Nothing -> Nothing
+  | Just (n, len) ->
+     if 0 <= n && n < 4294967296 then
+       Just ((of_int 2147483648 n, len))
+     else
+       Nothing
+  end
+
+
 let string_of_bits = string_of_vec
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 3e304796..665ff3af 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -635,10 +635,10 @@ let rec n_leading_spaces s =
            end
 
 
-let opt_spaces_matches_prefix s =
+let opt_spc_matches_prefix s =
   ZSome ((), n_leading_spaces s |> Big_int.of_int)
 
-let spaces_matches_prefix s =
+let spc_matches_prefix s =
   let n = n_leading_spaces s in
   match n with
   | 0 -> ZNone ()
@@ -703,3 +703,13 @@ let hex_bits_21_matches_prefix s =
        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 ()