Source file sail2_operators.ml

(*Generated by Lem from sail2_operators.lem.*)
open Lem_pervasives_extra
open Lem_machine_word
open Sail2_values

(*** Bit vector operations *)

(*val concat_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => 'a -> 'b -> list bitU*)
let concat_bv dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b l r:(bitU)list=  ( List.rev_append (List.rev (
  dict_Sail2_values_Bitvector_a.bits_of_method l)) (dict_Sail2_values_Bitvector_b.bits_of_method r))

(*val cons_bv : forall 'a. Bitvector 'a => bitU -> 'a -> list bitU*)
let cons_bv dict_Sail2_values_Bitvector_a b v:(bitU)list=  (b :: 
  dict_Sail2_values_Bitvector_a.bits_of_method v)

(*val cast_unit_bv : bitU -> list bitU*)
let cast_unit_bv b:(bitU)list=  ([b])

(*val bv_of_bit : integer -> bitU -> list bitU*)
let bv_of_bit len b:(bitU)list=  (extz_bits len [b])

let most_significant dict_Sail2_values_Bitvector_a v:bitU=  ((match  
  dict_Sail2_values_Bitvector_a.bits_of_method v with
  | b :: _ -> b
  | _ -> B0 (* Treat empty bitvector as all zeros *)
  ))

let get_max_representable_in sign (n : Nat_big_num.num) : Nat_big_num.num=
   (if ( Nat_big_num.equal n( (Nat_big_num.of_int 64))) then (match sign with | true -> max_64 | false -> max_64u )
  else if (Nat_big_num.equal n( (Nat_big_num.of_int 32))) then (match sign with | true -> max_32 | false -> max_32u )
  else if (Nat_big_num.equal n( (Nat_big_num.of_int 8))) then max_8
  else if (Nat_big_num.equal n( (Nat_big_num.of_int 5))) then max_5
  else (match sign with | true -> Nat_big_num.pow_int( (Nat_big_num.of_int 2)) ( Nat_num.nat_monus(abs (Nat_big_num.to_int n))1)
                       | false -> Nat_big_num.pow_int( (Nat_big_num.of_int 2)) (abs (Nat_big_num.to_int n))
       ))

let get_min_representable_in _ (n : Nat_big_num.num) : Nat_big_num.num=
   (if Nat_big_num.equal n( (Nat_big_num.of_int 64)) then min_64
  else if Nat_big_num.equal n( (Nat_big_num.of_int 32)) then min_32
  else if Nat_big_num.equal n( (Nat_big_num.of_int 8)) then min_8
  else if Nat_big_num.equal n( (Nat_big_num.of_int 5)) then min_5
  else Nat_big_num.sub( (Nat_big_num.of_int 0)) (Nat_big_num.pow_int( (Nat_big_num.of_int 2)) (abs (Nat_big_num.to_int n))))

(*val arith_op_bv_int : forall 'a 'b. Bitvector 'a =>
  (integer -> integer -> integer) -> bool -> 'a -> integer -> 'a*)
let arith_op_bv_int dict_Sail2_values_Bitvector_a op sign l r:'a=
   (let r' = (dict_Sail2_values_Bitvector_a.of_int_method (dict_Sail2_values_Bitvector_a.length_method l) r) in  dict_Sail2_values_Bitvector_a.arith_op_bv_method 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 dict_Sail2_values_Bitvector_a op sign l r:'a=
   (let l' = (dict_Sail2_values_Bitvector_a.of_int_method (dict_Sail2_values_Bitvector_a.length_method r) l) in  dict_Sail2_values_Bitvector_a.arith_op_bv_method op sign l' r)

let arith_op_bv_bool dict_Sail2_values_Bitvector_a op sign l r:'a=  (arith_op_bv_int 
  dict_Sail2_values_Bitvector_a op sign l (if r then  (Nat_big_num.of_int 1) else  (Nat_big_num.of_int 0)))
let arith_op_bv_bit dict_Sail2_values_Bitvector_a op sign l r:'a option=  (Lem.option_map (arith_op_bv_bool 
  dict_Sail2_values_Bitvector_a 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:shift ->shift=  ((function
  | LL_shift -> RR_shift
  | RR_shift -> LL_shift
  | RR_shift_arith -> LL_shift
  | LL_rot -> RR_rot
  | RR_rot -> LL_rot
))

(*val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> list bitU*)
let shift_op_bv dict_Sail2_values_Bitvector_a op v n:(bitU)list=
   (let v = (dict_Sail2_values_Bitvector_a.bits_of_method v) in
  if Nat_big_num.equal n( (Nat_big_num.of_int 0)) then v else
  let (op, n) = (if Nat_big_num.greater n( (Nat_big_num.of_int 0)) then (op, n) else (invert_shift op, Nat_big_num.negate n)) in
  (match op with
  | LL_shift -> 
     List.rev_append (List.rev (subrange_list true v n ( Nat_big_num.sub(Nat_big_num.of_int (List.length v))( (Nat_big_num.of_int 1))))) (repeat [B0] n)
  | RR_shift -> 
     List.rev_append (List.rev (repeat [B0] n)) (subrange_list true v( (Nat_big_num.of_int 0)) ( Nat_big_num.sub (Nat_big_num.sub(Nat_big_num.of_int (List.length v)) n)( (Nat_big_num.of_int 1))))
  | RR_shift_arith -> 
     List.rev_append (List.rev (repeat [most_significant 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) v] n)) (subrange_list true v( (Nat_big_num.of_int 0)) ( Nat_big_num.sub (Nat_big_num.sub(Nat_big_num.of_int (List.length v)) n)( (Nat_big_num.of_int 1))))
  | LL_rot -> 
     List.rev_append (List.rev (subrange_list true v n ( Nat_big_num.sub(Nat_big_num.of_int (List.length v))( (Nat_big_num.of_int 1))))) (subrange_list true v( (Nat_big_num.of_int 0)) ( Nat_big_num.sub n( (Nat_big_num.of_int 1))))
  | RR_rot -> 
     List.rev_append (List.rev (subrange_list false v( (Nat_big_num.of_int 0)) ( Nat_big_num.sub n( (Nat_big_num.of_int 1))))) (subrange_list false v n ( Nat_big_num.sub(Nat_big_num.of_int (List.length v))( (Nat_big_num.of_int 1))))
  ))

let shiftl_bv dict_Sail2_values_Bitvector_a:'a ->Nat_big_num.num ->(bitU)list=  (shift_op_bv 
  dict_Sail2_values_Bitvector_a LL_shift) (*"<<"*)
let shiftr_bv dict_Sail2_values_Bitvector_a:'a ->Nat_big_num.num ->(bitU)list=  (shift_op_bv 
  dict_Sail2_values_Bitvector_a RR_shift) (*">>"*)
let arith_shiftr_bv dict_Sail2_values_Bitvector_a:'a ->Nat_big_num.num ->(bitU)list=  (shift_op_bv 
  dict_Sail2_values_Bitvector_a RR_shift_arith)
let rotl_bv dict_Sail2_values_Bitvector_a:'a ->Nat_big_num.num ->(bitU)list=  (shift_op_bv 
  dict_Sail2_values_Bitvector_a LL_rot) (*"<<<"*)
let rotr_bv dict_Sail2_values_Bitvector_a:'a ->Nat_big_num.num ->(bitU)list=  (shift_op_bv 
  dict_Sail2_values_Bitvector_a LL_rot) (*">>>"*)

let shiftl_mword w n:Lem.mword=  (Lem.word_shiftLeft w (nat_of_int n))
let shiftr_mword w n:Lem.mword=  (Lem.word_shiftRight w (nat_of_int n))
let arith_shiftr_mword w n:Lem.mword=  (Lem.word_arithShiftRight w (nat_of_int n))
let rotl_mword w n:Lem.mword=  (Lem.word_rol (nat_of_int n) w)
let rotr_mword w n:Lem.mword=  (Lem.word_ror (nat_of_int n) w)

let arith_op_no0 (op : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) l r:(Nat_big_num.num)option=
   (if Nat_big_num.equal r( (Nat_big_num.of_int 0))
  then None
  else Some (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 dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b op sign size l r:'b option=
   (Lem.option_bind (int_of_bv 
  dict_Sail2_values_Bitvector_a sign l) (fun l' ->
  Lem.option_bind (int_of_bv 
  dict_Sail2_values_Bitvector_a sign r) (fun r' ->
  if Nat_big_num.equal r'( (Nat_big_num.of_int 0)) then None else Some (
  dict_Sail2_values_Bitvector_b.of_int_method ( Nat_big_num.mul(dict_Sail2_values_Bitvector_a.length_method l) size) (op l' r')))))

let mod_bv dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b:'b ->'b ->'a option=  (arith_op_bv_no0 
  dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a tmod_int false( (Nat_big_num.of_int 1)))
let quot_bv dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b:'b ->'b ->'a option=  (arith_op_bv_no0 
  dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a tdiv_int false( (Nat_big_num.of_int 1)))
let quots_bv dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b:'b ->'b ->'a option=  (arith_op_bv_no0 
  dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a tdiv_int true( (Nat_big_num.of_int 1)))

let mod_mword:Lem.mword ->Lem.mword ->Lem.mword=  Lem.word_mod
let quot_mword:Lem.mword ->Lem.mword ->Lem.mword=  Lem.word_udiv
let quots_mword:Lem.mword ->Lem.mword ->Lem.mword=  Lem_machine_word.signedDivide

let arith_op_bv_int_no0 dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b op sign size l r:'b option=
   (arith_op_bv_no0 dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b op sign size l (dict_Sail2_values_Bitvector_a.of_int_method (dict_Sail2_values_Bitvector_a.length_method l) r))

let quot_bv_int dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b:'b ->Nat_big_num.num ->'a option=  (arith_op_bv_int_no0 
  dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a tdiv_int false( (Nat_big_num.of_int 1)))
let mod_bv_int dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b:'b ->Nat_big_num.num ->'a option=  (arith_op_bv_int_no0 
  dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a tmod_int false( (Nat_big_num.of_int 1)))

let mod_mword_int dict_Machine_word_Size_a l r:Lem.mword=  (Lem.word_mod l (wordFromInteger 
  dict_Machine_word_Size_a r))
let quot_mword_int dict_Machine_word_Size_a l r:Lem.mword=  (Lem.word_udiv l (wordFromInteger 
  dict_Machine_word_Size_a r))
let quots_mword_int dict_Machine_word_Size_a l r:Lem.mword=  (Lem_machine_word.signedDivide l (wordFromInteger 
  dict_Machine_word_Size_a r))

let replicate_bits_bv dict_Sail2_values_Bitvector_a v count:(bitU)list=  (repeat (
  dict_Sail2_values_Bitvector_a.bits_of_method v) count)
let duplicate_bit_bv dict_Sail2_values_BitU_a bit len:(bitU)list=  (replicate_bits_bv 
  (instance_Sail2_values_Bitvector_list_dict dict_Sail2_values_BitU_a) [bit] len)

(*val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*)
let eq_bv dict_Sail2_values_Bitvector_a l r:bool=  ( (listEqualBy (=)(
  dict_Sail2_values_Bitvector_a.bits_of_method l) (dict_Sail2_values_Bitvector_a.bits_of_method r)))

(*val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool*)
let neq_bv dict_Sail2_values_Bitvector_a l r:bool=  (not (eq_bv 
  dict_Sail2_values_Bitvector_a l r))

(*val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a*)
let get_slice_int_bv dict_Sail2_values_Bitvector_a len n lo:'a=
   (let hi = (Nat_big_num.sub (Nat_big_num.add lo len)( (Nat_big_num.of_int 1))) in
  let bs = (bools_of_int ( Nat_big_num.add hi( (Nat_big_num.of_int 1))) n) in  
  dict_Sail2_values_Bitvector_a.of_bools_method (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 dict_Sail2_values_Bitvector_a len n lo v:Nat_big_num.num=
   (let hi = (Nat_big_num.sub (Nat_big_num.add lo len)( (Nat_big_num.of_int 1))) in
  let bs = (bits_of_int ( Nat_big_num.add hi( (Nat_big_num.of_int 1))) n) in
  maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (
  dict_Sail2_values_Bitvector_a.bits_of_method v))))