Run ARM built-in tests for Lem backend (via OCaml)

1 files changed, 12 insertions, 0 deletions

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index d4275c87..78aab65e 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -223,3 +223,15 @@ let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedInteger
 
 val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
 let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r)
+
+val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
+let get_slice_int_bv len n lo =
+  let hi = lo + len - 1 in
+  let bs = bools_of_int (hi + 1) n in
+  of_bools (subrange_list false bs hi lo)
+
+val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer
+let set_slice_int_bv len n lo v =
+  let hi = lo + len - 1 in
+  let bs = bits_of_int (hi + 1) n in
+  maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (bits_of v)))