Merge branch 'sail2' into rmem_interpreter

2 files changed, 10 insertions, 0 deletions

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index bacf59e7..8b75fa38 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -41,6 +41,9 @@ let zeros len = repeat [B0] len
 val vector_truncate : list bitU -> integer -> list bitU
 let vector_truncate bs len = extz_bv len bs
 
+val vector_truncateLSB : list bitU -> integer -> list bitU
+let vector_truncateLSB bs len = take_list len bs
+
 val vec_of_bits_maybe    : list bitU -> maybe (list bitU)
 val vec_of_bits_fail     : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
 val vec_of_bits_nondet   : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index d47d9b40..181fa149 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -82,6 +82,13 @@ let zeros _ = Machine_word.wordFromNatural 0
 val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
 let vector_truncate w _ = Machine_word.zeroExtend w
 
+val vector_truncateLSB : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+let vector_truncateLSB w len =
+  let len = nat_of_int len in
+  let lo = Machine_word.word_length w - len in
+  let hi = lo + len - 1 in
+  Machine_word.word_extract lo hi w
+
 val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c
 let concat_vec = Machine_word.word_concat