Sail_lib and RISCV prelude: functions for bitwise operations on ints

2 files changed, 7 insertions, 1 deletions

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)