Implement bitwise library operations

1 files changed, 14 insertions, 0 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index f2c7ef0f..b9fdb5a1 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -5,6 +5,7 @@ import Maybe_extra
 open import Num
 open import List
 open import Word
+open import Bool
 
 let ignore_sail x = V_lit (L_aux L_unit Unknown) ;;
 
@@ -29,6 +30,15 @@ let bool_to_bit b = match b with
   | true -> V_lit (L_aux L_one Unknown)
   end ;;
 
+let bitwise_not (V_vector idx inc v) =
+  let apply x = bool_to_bit(not (bit_to_bool x)) in
+  V_vector idx inc (List.map apply v)
+
+let bitwise_binop op (V_tuple [V_vector idx inc v; V_vector idx' inc' v']) =
+  (* typechecker ensures inc = inc', idx = idx' and length v = length v' *)
+  let apply (x, y) = bool_to_bit(op (bit_to_bool x) (bit_to_bool y)) in
+  V_vector idx inc (List.map apply (List.zip v v'))
+
 (* BitSeq expects LSB first.
  * By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
  * hence MSB first.
@@ -71,6 +81,10 @@ let function_map = [
   (* XXX the size of the target vector should be given by the interpreter *)
   ("to_vec_inc", to_vec_inc 64);
   ("to_vec_dec", to_vec_dec 64);
+  ("bitwise_not", bitwise_not);
+  ("bitwise_and", bitwise_binop (&&));
+  ("bitwise_or", bitwise_binop (||));
+  ("bitwise_xor", bitwise_binop xor);
 ] ;;
 
 let eval_external name v = (Maybe_extra.fromJust (List.lookup name function_map)) v ;;