diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/mono_rewrites.sail | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index 0702b374..1e7fe58f 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -8,9 +8,15 @@ $include <vector_dec.sail> /* External definitions not in the usual asl prelude */ -val extzv = "extz_vec" : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure +val extzv = {lem: "extz_vec", coq: "extz_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure +function extzv(m, v) = { + if m < 'n then truncate(v, m) else sail_zero_extend(v, m) +} -val extsv = "exts_vec" : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure +val extsv = {lem: "exts_vec", coq: "exts_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure +function extsv(m, v) = { + if m < 'n then truncate(v, m) else sail_sign_extend(v, m) +} /* This is generated internally to deal with case splits which reveal the size of a bitvector */ |