open import Pervasives_extra
open import Machine_word
open import Sail2_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 tmod_int false 1
let quot_bv = arith_op_bv_no0 tdiv_int false 1
let quots_bv = arith_op_bv_no0 tdiv_int 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 tdiv_int false 1
let mod_bv_int = arith_op_bv_int_no0 tmod_int 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)))