rename all lem support files to sail2_foo to avoid conflict with sail1 in rmem

1 files changed, 0 insertions, 207 deletions

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
deleted file mode 100644
index 0c5da675..00000000
--- a/src/gen_lib/sail_operators.lem
+++ /dev/null
@@ -1,207 +0,0 @@
-open import Pervasives_extra
-open import Machine_word
-open import Sail_values
-
-(*** Bit vector operations *)
-
-val concat_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => 'a -> 'b -> list bitU
-let concat_bv l r = (bits_of l ++ bits_of r)
-
-val cons_bv : forall 'a. Bitvector 'a => bitU -> 'a -> list bitU
-let cons_bv b v = b :: bits_of v
-
-val cast_unit_bv : bitU -> list bitU
-let cast_unit_bv b = [b]
-
-val bv_of_bit : integer -> bitU -> list bitU
-let bv_of_bit len b = extz_bits len [b]
-
-let most_significant v = match bits_of v with
-  | b :: _ -> b
-  | _ -> B0 (* Treat empty bitvector as all zeros *)
-  end
-
-let get_max_representable_in sign (n : integer) : integer =
-  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
-  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
-  else if (n=8) then max_8
-  else if (n=5) then max_5
-  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
-                       | false -> integerPow 2 (natFromInteger n)
-       end
-
-let get_min_representable_in _ (n : integer) : integer =
-  if n = 64 then min_64
-  else if n = 32 then min_32
-  else if n = 8 then min_8
-  else if n = 5 then min_5
-  else 0 - (integerPow 2 (natFromInteger n))
-
-val arith_op_bv_int : forall 'a 'b. Bitvector 'a =>
-  (integer -> integer -> integer) -> bool -> 'a -> integer -> 'a
-let arith_op_bv_int op sign l r =
-  let r' = of_int (length l) r in
-  arith_op_bv op sign l r'
-
-val arith_op_int_bv : forall 'a 'b. Bitvector 'a =>
-  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a
-let arith_op_int_bv op sign l r =
-  let l' = of_int (length r) l in
-  arith_op_bv op sign l' r
-
-let arith_op_bv_bool op sign l r = arith_op_bv_int op sign l (if r then 1 else 0)
-let arith_op_bv_bit op sign l r = Maybe.map (arith_op_bv_bool op sign l) (bool_of_bitU r)
-
-(* TODO (or just omit and define it per spec if needed)
-val arith_op_overflow_bv : forall 'a. Bitvector 'a =>
-  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> (list bitU * bitU * bitU)
-let arith_op_overflow_bv op sign size l r =
-  let len = length l in
-  let act_size = len * size in
-  match (int_of_bv sign l, int_of_bv sign r, int_of_bv false l, int_of_bv false r) with
-    | (Just l_sign, Just r_sign, Just l_unsign, Just r_unsign) ->
-       let n = op l_sign r_sign in
-       let n_unsign = op l_unsign r_unsign in
-       let correct_size = of_int act_size n in
-       let one_more_size_u = bits_of_int (act_size + 1) n_unsign in
-       let overflow =
-         if n <= get_max_representable_in sign len &&
-              n >= get_min_representable_in sign len
-         then B0 else B1 in
-       let c_out = most_significant one_more_size_u in
-       (correct_size,overflow,c_out)
-    | (_, _, _, _) ->
-       (repeat [BU] act_size, BU, BU)
-  end
-
-let add_overflow_bv = arith_op_overflow_bv integerAdd false 1
-let adds_overflow_bv = arith_op_overflow_bv integerAdd true 1
-let sub_overflow_bv = arith_op_overflow_bv integerMinus false 1
-let subs_overflow_bv = arith_op_overflow_bv integerMinus true 1
-let mult_overflow_bv = arith_op_overflow_bv integerMult false 2
-let mults_overflow_bv = arith_op_overflow_bv integerMult true 2
-
-val arith_op_overflow_bv_bit : forall 'a. Bitvector 'a =>
-  (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> (list bitU * bitU * bitU)
-let arith_op_overflow_bv_bit op sign size l r_bit =
-  let act_size = length l * size in
-  match (int_of_bv sign l, int_of_bv false l, r_bit = BU) with
-    | (Just l', Just l_u, false) ->
-       let (n, nu, changed) = match r_bit with
-         | B1 -> (op l' 1, op l_u 1, true)
-         | B0 -> (l', l_u, false)
-         | BU -> (* unreachable due to check above *)
-            failwith "arith_op_overflow_bv_bit applied to undefined bit"
-         end in
-       let correct_size = of_int act_size n in
-       let one_larger = bits_of_int (act_size + 1) nu in
-       let overflow =
-         if changed
-         then
-           if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
-           then B0 else B1
-         else B0 in
-       (correct_size, overflow, most_significant one_larger)
-    | (_, _, _) ->
-       (repeat [BU] act_size, BU, BU)
-  end
-
-let add_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd false 1
-let adds_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd true 1
-let sub_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus false 1
-let subs_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus true 1*)
-
-type shift = LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot
-
-let invert_shift = function
-  | LL_shift -> RR_shift
-  | RR_shift -> LL_shift
-  | RR_shift_arith -> LL_shift
-  | LL_rot -> RR_rot
-  | RR_rot -> LL_rot
-end
-
-val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> list bitU
-let shift_op_bv op v n =
-  let v = bits_of v in
-  if n = 0 then v else
-  let (op, n) = if n > 0 then (op, n) else (invert_shift op, ~n) in
-  match op with
-  | LL_shift ->
-     subrange_list true v n (length v - 1) ++ repeat [B0] n
-  | RR_shift ->
-     repeat [B0] n ++ subrange_list true v 0 (length v - n - 1)
-  | RR_shift_arith ->
-     repeat [most_significant v] n ++ subrange_list true v 0 (length v - n - 1)
-  | LL_rot ->
-     subrange_list true v n (length v - 1) ++ subrange_list true v 0 (n - 1)
-  | RR_rot ->
-     subrange_list false v 0 (n - 1) ++ subrange_list false v n (length v - 1)
-  end
-
-let shiftl_bv = shift_op_bv LL_shift (*"<<"*)
-let shiftr_bv = shift_op_bv RR_shift (*">>"*)
-let arith_shiftr_bv = shift_op_bv RR_shift_arith
-let rotl_bv = shift_op_bv LL_rot (*"<<<"*)
-let rotr_bv = shift_op_bv LL_rot (*">>>"*)
-
-let shiftl_mword w n = Machine_word.shiftLeft w (nat_of_int n)
-let shiftr_mword w n = Machine_word.shiftRight w (nat_of_int n)
-let arith_shiftr_mword w n = Machine_word.arithShiftRight w (nat_of_int n)
-let rotl_mword w n = Machine_word.rotateLeft (nat_of_int n) w
-let rotr_mword w n = Machine_word.rotateRight (nat_of_int n) w
-
-let rec arith_op_no0 (op : integer -> integer -> integer) l r =
-  if r = 0
-  then Nothing
-  else Just (op l r)
-
-val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
-  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> maybe 'b
-let arith_op_bv_no0 op sign size l r =
-  Maybe.bind (int_of_bv sign l) (fun l' ->
-  Maybe.bind (int_of_bv sign r) (fun r' ->
-  if r' = 0 then Nothing else Just (of_int (length l * size) (op l' r'))))
-
-let mod_bv = arith_op_bv_no0 hardware_mod false 1
-let quot_bv = arith_op_bv_no0 hardware_quot false 1
-let quots_bv = arith_op_bv_no0 hardware_quot true 1
-
-let mod_mword = Machine_word.modulo
-let quot_mword = Machine_word.unsignedDivide
-let quots_mword = Machine_word.signedDivide
-
-let arith_op_bv_int_no0 op sign size l r =
-  arith_op_bv_no0 op sign size l (of_int (length l) r)
-
-let quot_bv_int = arith_op_bv_int_no0 hardware_quot false 1
-let mod_bv_int = arith_op_bv_int_no0 hardware_mod false 1
-
-let mod_mword_int l r = Machine_word.modulo l (wordFromInteger r)
-let quot_mword_int l r = Machine_word.unsignedDivide l (wordFromInteger r)
-let quots_mword_int l r = Machine_word.signedDivide l (wordFromInteger r)
-
-let replicate_bits_bv v count = repeat (bits_of v) count
-let duplicate_bit_bv bit len = replicate_bits_bv [bit] len
-
-val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let eq_bv l r = (bits_of l = bits_of r)
-
-let inline eq_mword l r = (l = r)
-
-val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let neq_bv l r = not (eq_bv l r)
-
-let inline neq_mword l r = (l <> r)
-
-val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
-let get_slice_int_bv len n lo =
-  let hi = lo + len - 1 in
-  let bs = bools_of_int (hi + 1) n in
-  of_bools (subrange_list false bs hi lo)
-
-val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer
-let set_slice_int_bv len n lo v =
-  let hi = lo + len - 1 in
-  let bs = bits_of_int (hi + 1) n in
-  maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (bits_of v)))