diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/mono_rewrites.sail | 92 | ||||
| -rw-r--r-- | lib/vector_dec.sail | 2 |
2 files changed, 60 insertions, 34 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index 8259ec47..90d74149 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -19,13 +19,9 @@ overload operator >> = {shiftright} val arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order). (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure -val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extzv(v) = extz_vec(sizeof('m),v) +val extzv = "extz_vec" : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extsv(v) = exts_vec(sizeof('m),v) +val extsv = "exts_vec" : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure /* This is generated internally to deal with case splits which reveal the size of a bitvector */ @@ -34,9 +30,9 @@ val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect p /* Definitions for the rewrites */ -val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure -function slice_mask(i,l) = - let one : bits('n) = extzv(0b1) in +val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n) effect pure +function slice_mask(n,i,l) = + let one : bits('n) = extzv(n, 0b1) in ((one << l) - one) << i val is_zero_subrange : forall 'n, 'n >= 0. @@ -46,6 +42,13 @@ function is_zero_subrange (xs, i, j) = { (xs & slice_mask(j, i-j+1)) == extzv(0b0) } +val is_zeros_slice : forall 'n, 'n >= 0. + (bits('n), int, int) -> bool effect pure + +function is_zeros_slice (xs, i, l) = { + (xs & slice_mask(i, l)) == extzv(0b0) +} + val is_ones_subrange : forall 'n, 'n >= 0. (bits('n), int, int) -> bool effect pure @@ -54,21 +57,29 @@ function is_ones_subrange (xs, i, j) = { (xs & m) == m } +val is_ones_slice : forall 'n, 'n >= 0. + (bits('n), int, int) -> bool effect pure + +function is_ones_slice (xs, i, j) = { + let m : bits('n) = slice_mask(i,j) in + (xs & m) == m +} + val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0. - (bits('n), int, int, bits('m), int, int) -> bits('r) effect pure + (implicit('r), bits('n), int, int, bits('m), int, int) -> bits('r) effect pure -function slice_slice_concat (xs, i, l, ys, i', l') = { +function slice_slice_concat (r, xs, i, l, ys, i', l') = { let xs = (xs & slice_mask(i,l)) >> i in let ys = (ys & slice_mask(i',l')) >> i' in - extzv(xs) << l' | extzv(ys) + extzv(r, xs) << l' | extzv(r, ys) } -val slice_zeros_concat : forall 'n 'p 'q 'r, 'r == 'p + 'q & 'n >= 0 & /*'p >= 0 & 'q >= 0 &*/ 'r >= 0. - (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure +val slice_zeros_concat : forall 'n 'p 'q, 'n >= 0 & 'p + 'q >= 0. + (bits('n), int, atom('p), atom('q)) -> bits('p + 'q) effect pure function slice_zeros_concat (xs, i, l, l') = { let xs = (xs & slice_mask(i,l)) >> i in - extzv(xs) << l' + extzv(l + l', xs) << l' } /* Assumes initial vectors are of equal size */ @@ -83,44 +94,59 @@ function subrange_subrange_eq (xs, i, j, ys, i', j') = { } val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's >= 0 & 'n >= 0 & 'm >= 0. - (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure + (implicit('s), 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') = { +function subrange_subrange_concat (s, xs, i, j, ys, i', j') = { 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) + extzv(s, xs) << (i' - j' + 1) | extzv(s, ys) } val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int, int) -> bits('m) effect pure + (implicit('m), bits('n), int, int, int) -> bits('m) effect pure -function place_subrange(xs,i,j,shift) = { +function place_subrange(m,xs,i,j,shift) = { let xs = (xs & slice_mask(j,i-j+1)) >> j in - extzv(xs) << shift + extzv(m, xs) << shift } val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int, int) -> bits('m) effect pure + (implicit('m), bits('n), int, int, int) -> bits('m) effect pure -function place_slice(xs,i,l,shift) = { +function place_slice(m,xs,i,l,shift) = { let xs = (xs & slice_mask(i,l)) >> i in - extzv(xs) << shift + extzv(m, xs) << shift +} + +val set_slice_zeros : forall 'n, 'n >= 0. + (atom('n), int, bits('n), int) -> bits('n) effect pure + +function set_slice_zeros(n, i, xs, l) = { + let ys : bits('n) = slice_mask(n, i, l) in + xs & ~(ys) } val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int) -> bits('m) effect pure + (implicit('m), bits('n), int, int) -> bits('m) effect pure -function zext_slice(xs,i,l) = { +function zext_slice(m,xs,i,l) = { let xs = (xs & slice_mask(i,l)) >> i in - extzv(xs) + extzv(m, xs) } val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int) -> bits('m) effect pure + (implicit('m), bits('n), int, int) -> bits('m) effect pure -function sext_slice(xs,i,l) = { +function sext_slice(m,xs,i,l) = { let xs = arith_shiftright(((xs & slice_mask(i,l)) << ('n - i - l)), 'n - l) in - extsv(xs) + extsv(m, xs) +} + +val place_slice_signed : forall 'n 'm, 'n >= 0 & 'm >= 0. + (implicit('m), bits('n), int, int, int) -> bits('m) effect pure + +function place_slice_signed(m,xs,i,l,shift) = { + sext_slice(m, xs, i, l) << shift } /* This has different names in the aarch64 prelude (UInt) and the other @@ -150,9 +176,9 @@ function unsigned_subrange(xs,i,j) = { } -val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure +val zext_ones : forall 'n, 'n >= 0. (implicit('n), int) -> bits('n) effect pure -function zext_ones(m) = { +function zext_ones(n, m) = { let v : bits('n) = extsv(0b1) in - v >> ('n - m) + v >> (n - m) } diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 166db243..8c6426d4 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -166,6 +166,6 @@ val signed = { _: "sint" } : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) -overload __size = {length} +overload __size = {__id, length} $endif |