Fix off-by-one bugs in monomorphisation rewrites involving bitvector subranges

CHERI test suite now passes using Isabelle-generated emulator

1 files changed, 9 insertions, 9 deletions

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index c9164b6c..aa8d05cd 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -42,14 +42,14 @@ val is_zero_subrange : forall 'n, 'n >= 0.
   (bits('n), int, int) -> bool effect pure
 
 function is_zero_subrange (xs, i, j) = {
-  (xs & slice_mask(j, i-j)) == extzv(0b0)
+  (xs & slice_mask(j, i-j+1)) == extzv(0b0)
 }
 
 val is_ones_subrange : forall 'n, 'n >= 0.
   (bits('n), int, int) -> bool effect pure
 
 function is_ones_subrange (xs, i, j) = {
-  let m : bits('n) = slice_mask(j,j-i) in
+  let m : bits('n) = slice_mask(j,j-i+1) in
   (xs & m) == m
 }
 
@@ -76,8 +76,8 @@ val subrange_subrange_eq : forall 'n, 'n >= 0.
   (bits('n), int, int, bits('n), int, int) -> bool effect pure
 
 function subrange_subrange_eq (xs, i, j, ys, i', j') = {
-  let xs = (xs & slice_mask(j,i-j)) >> j in
-  let ys = (ys & slice_mask(j',i'-j')) >> j' in
+  let xs = (xs & slice_mask(j,i-j+1)) >> j in
+  let ys = (ys & slice_mask(j',i'-j'+1)) >> j' in
   xs == ys
 }
 
@@ -85,16 +85,16 @@ val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's = 'o - ('p - 1) +
   (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure
 
 function subrange_subrange_concat (xs, i, j, ys, i', j') = {
-  let xs = (xs & slice_mask(j,i-j)) >> j in
-  let ys = (ys & slice_mask(j',i'-j')) >> j' in
-  extzv(xs) << i' - (j' - 1) | extzv(ys)
+  let xs = (xs & slice_mask(j,i-j+1)) >> j in
+  let ys = (ys & slice_mask(j',i'-j'+1)) >> j' in
+  extzv(xs) << (i' - j' + 1) | extzv(ys)
 }
 
 val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
   (bits('n), int, int, int) -> bits('m) effect pure
 
 function place_subrange(xs,i,j,shift) = {
-  let xs = (xs & slice_mask(j,i-j)) >> j in
+  let xs = (xs & slice_mask(j,i-j+1)) >> j in
   extzv(xs) << shift
 }
 
@@ -144,7 +144,7 @@ val unsigned_subrange : forall 'n, 'n >= 0.
   (bits('n), int, int) -> int effect pure
 
 function unsigned_subrange(xs,i,j) = {
-  let xs = (xs & slice_mask(j,i-j)) >> i in
+  let xs = (xs & slice_mask(j,i-j+1)) >> i in
   _builtin_unsigned(xs)
 }