From bd7c2be6fe9cb955e25e04d59c5af089a04bcf9e Mon Sep 17 00:00:00 2001 From: Jon French Date: Fri, 14 Sep 2018 15:07:25 +0100 Subject: Sail_lib and RISCV prelude: functions for bitwise operations on ints --- riscv/prelude.sail | 4 +++- src/sail_lib.ml | 4 ++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/riscv/prelude.sail b/riscv/prelude.sail index abdb3da0..a073b20f 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -373,8 +373,10 @@ overload operator % = {modulus} val Real = {ocaml: "Num.num_of_big_int", lem: "realFromInteger"} : int -> real val shl_int = "shl_int" : (int, int) -> int - val shr_int = "shr_int" : (int, int) -> int +val lor_int = "lor_int" : (int, int) -> int +val land_int = "land_int" : (int, int) -> int +val lxor_int = "lxor_int" : (int, int) -> int val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat diff --git a/src/sail_lib.ml b/src/sail_lib.ml index f1203725..09a90ba9 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -491,6 +491,10 @@ let zcast_unit_vec x = [x] let shl_int (n, m) = Big_int.shift_left n (Big_int.to_int m) let shr_int (n, m) = Big_int.shift_right n (Big_int.to_int m) +let lor_int (n, m) = Big_int.bitwise_or n m +let land_int (n, m) = Big_int.bitwise_and n m +let lxor_int (n, m) = Big_int.bitwise_xor n m + let debug (str1, n, str2, v) = prerr_endline (str1 ^ Big_int.to_string n ^ str2 ^ string_of_bits v) -- cgit v1.2.3