diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 4 | ||||
| -rw-r--r-- | riscv/riscv_extras.lem | 6 |
2 files changed, 5 insertions, 5 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index b6c80ffb..f6532215 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -110,9 +110,9 @@ function or_vec (xs, ys) = builtin_or_vec(xs, ys) overload operator | = {or_bool, or_vec} -val unsigned = {ocaml: "uint", lem: "unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) +val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) -val signed = {ocaml: "sint", lem: "signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) +val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem index 49499445..9d9ccf89 100644 --- a/riscv/riscv_extras.lem +++ b/riscv/riscv_extras.lem @@ -49,7 +49,7 @@ let get_slice_int len n lo = (* TODO: Is this the intended behaviour? *) let hi = lo + len - 1 in let bits = bits_of_int (hi + 1) n in - of_bits (get_bits false bits hi lo) + of_bits_failwith (subrange_list false bits hi lo) val sign_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b let sign_extend v len = exts_vec len v @@ -57,9 +57,9 @@ val zero_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> b let zero_extend v len = extz_vec len v val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a -let shift_bits_right v m = shiftr v (unsigned m) +let shift_bits_right v m = shiftr v (uint m) val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a -let shift_bits_left v m = shiftl v (unsigned m) +let shift_bits_left v m = shiftl v (uint m) val prerr_endline : string -> unit let prerr_endline _ = () |