From fd706bc10a21577861d1c909ceeeed523d43dc63 Mon Sep 17 00:00:00 2001 From: Jon French Date: Wed, 23 May 2018 16:51:31 +0100 Subject: riscv decode now uses mapping-decode and passes tests --- src/gen_lib/sail_string.lem | 15 +++++++++++++-- src/sail_lib.ml | 14 ++++++++++++-- 2 files changed, 25 insertions(+), 4 deletions(-) (limited to 'src') 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 () -- cgit v1.2.3