path: root/src/gen_lib/sail_values.lem

open import Pervasives_extra
open import Sail_impl_base
open import Vector

type i = integer
type n = natural

type bitU = O | I | Undef


type register_field = string
type register_field_index = string * (integer * integer) (* name, start and end *)

type register =
  | Register of string * (* name *)
                integer * (* length *)
                integer * (* start index *)
                bool * (* is increasing *)
                  list register_field_index
  | UndefinedRegister of integer (* length *)
  | RegisterPair of register * register

let dir is_inc = if is_inc then D_increasing else D_decreasing

let name_of_reg (Register name _ _ _ _) = name
let size_of_reg (Register _ size _ _ _) = size
let start_of_reg (Register _ _ start _ _) = start
let is_inc_of_reg (Register _ _ _ is_inc _) = is_inc
let dir_of_reg (Register _ _ _ is_inc _) = dir is_inc

let size_of_reg_nat reg = natFromInteger (size_of_reg reg)
let start_of_reg_nat reg = natFromInteger (start_of_reg reg)


val register_field_indices : register -> register_field -> integer * integer
let register_field_indices (Register _ _ _ _ rfields) rfield =
  match List.lookup rfield rfields with
  | None -> failwith "Invalid register/register-field combination"
  | Just indices -> indices
  end

let register_field_indices_nat reg regfield=
  let (i,j) = register_field_indices reg regfield in
  (natFromInteger i,natFromInteger j)

let to_bool = function
  | O -> false
  | I  -> true
  | Undef -> failwith "to_bool applied to Undef"
  end


let bit_lifted_of_bitU = function
  | O -> Bitl_zero
  | I -> Bitl_one
  | Undef -> Bitl_undef
  end

let bitU_of_bit = function
  | Bitc_zero -> O
  | Bitc_one  -> I
  end

let bitU_of_bit_lifted = function
  | Bitl_zero -> O
  | Bitl_one  -> I
  | Bitl_undef -> Undef
  | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown"
  end

let has_undef (Vector bs _ _) = List.any (function Undef -> true | _ -> false end) bs

let most_significant = function
  | (Vector (b :: _) _ _) -> b
  | _ -> failwith "most_significant applied to empty vector"
  end

let bitwise_not_bit = function
  | I -> O
  | O -> I
  | _ -> Undef
  end

let (~) = bitwise_not_bit

val pow : integer -> integer -> integer
let pow m n = m ** (natFromInteger n)


let bitwise_not (Vector bs start is_inc) =
  Vector (List.map bitwise_not_bit bs) start is_inc

val is_one : integer -> bitU
let is_one i =
  if i = 1 then I else O

let bool_to_bit b = if b then I else O

let bitwise_binop_bit op = function
  | (Undef,_) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
  | (_,Undef) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
  | (x,y) -> bool_to_bit (op (to_bool x) (to_bool y))
  end

val bitwise_and_bit : bitU * bitU -> bitU
let bitwise_and_bit = bitwise_binop_bit (&&)

val bitwise_or_bit : bitU * bitU -> bitU
let bitwise_or_bit = bitwise_binop_bit (||)

val bitwise_xor_bit : bitU * bitU -> bitU
let bitwise_xor_bit = bitwise_binop_bit xor

val (&.) : bitU -> bitU -> bitU
let (&.) x y = bitwise_and_bit (x,y)

val (|.) : bitU -> bitU -> bitU
let (|.) x y = bitwise_or_bit (x,y)

val (+.) : bitU -> bitU -> bitU
let (+.) x y = bitwise_xor_bit (x,y)

let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) =
  let revbs = foldl (fun acc pair -> bitwise_binop_bit op pair :: acc) [] (zip bsl bsr) in
  Vector (reverse revbs) start is_inc

let bitwise_and = bitwise_binop (&&)
let bitwise_or = bitwise_binop (||)
let bitwise_xor = bitwise_binop xor

let unsigned (Vector bs _ _ as v) : integer =
  if has_undef v then failwith "unsigned applied to vector with undefined bits" else
    fst (List.foldl
           (fun (acc,exp) b -> (acc + (if b = I then integerPow 2 exp else 0),exp +1)) (0,0) bs)

let unsigned_big = unsigned
        
let signed v : integer =
  match most_significant v with
  | I -> 0 - (1 + (unsigned (bitwise_not v)))
  | O -> unsigned v
  | _ -> failwith "signed applied to vector with undefined bits"
  end

let signed_big = signed

let to_num sign = if sign then signed else unsigned
  
let max_64u = (integerPow 2 64) - 1
let max_64  = (integerPow 2 63) - 1
let min_64  = 0 - (integerPow 2 63)
let max_32u = (4294967295 : integer)
let max_32  = (2147483647 : integer)
let min_32  = (0 - 2147483648 : integer)
let max_8   = (127 : integer)
let min_8   = (0 - 128 : integer)
let max_5   = (31 : integer)
let min_5   = (0 - 32 : integer)

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))


let rec divide_by_2 bs (i : integer) (n : integer) =
  if i < 0 || n = 0
  then bs
  else
    if (n mod 2 = 1)
    then divide_by_2 (replace bs (i,I)) (i - 1) (n / 2)
    else divide_by_2 bs (i-1) (n div 2)

let rec add_one_bit bs co (i : integer) =
  if i < 0 then bs
  else match (List_extra.nth bs (natFromInteger i),co) with
    | (O,false) -> replace bs (i,I)
    | (O,true)  -> add_one_bit (replace bs (i,I)) true (i-1)
    | (I,false) -> add_one_bit (replace bs (i,O)) true (i-1)
    | (I,true)  -> add_one_bit bs true (i-1)
    | _ -> failwith "add_one_bit applied to list with undefined bit"
   (*    | Vundef,_ -> assert false*) 
  end

let to_vec is_inc ((len : integer),(n : integer)) =
  let bs = List.replicate (natFromInteger len) O in
  let start = if is_inc then 0 else len-1 in
  if n = 0 then
    Vector bs start is_inc
  else if n > 0 then
    Vector (divide_by_2 bs (len-1) n) start is_inc
  else
    let abs_bs = divide_by_2 bs (len-1) (abs n) in
    let (Vector bs start is_inc) = bitwise_not (Vector abs_bs start is_inc) in
    Vector (add_one_bit bs false (len-1)) start is_inc

let to_vec_big = to_vec
      
let to_vec_inc = to_vec true
let to_vec_dec = to_vec false

let to_vec_undef is_inc (len : integer) =
  Vector (replicate (natFromInteger len) Undef) (if is_inc then 0 else len-1) is_inc

let to_vec_inc_undef = to_vec_undef true
let to_vec_dec_undef = to_vec_undef false
                                    
let exts (len, vec) = to_vec (get_dir vec) (len,signed vec)
let extz (len, vec) = to_vec (get_dir vec) (len,unsigned vec)

let exts_big (len, vec) = to_vec_big (get_dir vec) (len, signed_big vec)
let extz_big (len, vec) = to_vec_big (get_dir vec) (len, unsigned_big vec)

let add = integerAdd
let add_signed = integerAdd
let minus = integerMinus
let multiply = integerMult
let modulo = integerMod
let quot = integerDiv
let power = integerPow

let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r =
  let (l',r') = (to_num sign l, to_num sign r) in
  let n = op  l' r' in
  to_vec is_inc (size * (length l),n)


(* add_vec
 * add_vec_signed
 * minus_vec 
 * multiply_vec 
 * multiply_vec_signed
 *)
let add_VVV = arith_op_vec integerAdd false 1
let addS_VVV = arith_op_vec integerAdd true 1
let minus_VVV = arith_op_vec integerMinus false 1
let mult_VVV = arith_op_vec integerMult false 2
let multS_VVV = arith_op_vec integerMult true 2

let arith_op_vec_range op sign size (Vector _ _ is_inc as l) r =
  arith_op_vec op sign size l (to_vec is_inc (length l,r))

(* add_vec_range
 * add_vec_range_signed
 * minus_vec_range 
 * mult_vec_range 
 * mult_vec_range_signed
 *)
let add_VIV = arith_op_vec_range integerAdd false 1
let addS_VIV = arith_op_vec_range integerAdd true 1
let minus_VIV = arith_op_vec_range integerMinus false 1
let mult_VIV = arith_op_vec_range integerMult false 2
let multS_VIV = arith_op_vec_range integerMult true 2

let arith_op_range_vec op sign size l (Vector _ _ is_inc as r) =
  arith_op_vec op sign size (to_vec is_inc (length r, l)) r

(* add_range_vec
 * add_range_vec_signed
 * minus_range_vec 
 * mult_range_vec
 * mult_range_vec_signed
 *)
let add_IVV = arith_op_range_vec integerAdd false 1
let addS_IVV = arith_op_range_vec integerAdd true 1
let minus_IVV = arith_op_range_vec integerMinus false 1
let mult_IVV = arith_op_range_vec integerMult false 2
let multS_IVV = arith_op_range_vec integerMult true 2

let arith_op_range_vec_range op sign l r = op l (to_num sign r)

(* add_range_vec_range
 * add_range_vec_range_signed
 * minus_range_vec_range 
 *)
let add_IVI = arith_op_range_vec_range integerAdd false
let addS_IVI = arith_op_range_vec_range integerAdd true
let minus_IVI = arith_op_range_vec_range integerMinus false

let arith_op_vec_range_range op sign l r = op (to_num sign l) r

(* add_vec_range_range
 * add_vec_range_range_signed
 * minus_vec_range_range
 *)
let add_VII = arith_op_vec_range_range integerAdd false
let addS_VII = arith_op_vec_range_range integerAdd true
let minus_VII = arith_op_vec_range_range integerMinus false



let arith_op_vec_vec_range op sign l r = 
  let (l',r') = (to_num sign l,to_num sign r) in
  op l' r'

(* add_vec_vec_range
 * add_vec_vec_range_signed
 *)
let add_VVI = arith_op_vec_vec_range integerAdd false
let addS_VVI = arith_op_vec_vec_range integerAdd true

let arith_op_vec_bit op sign (size : integer) (Vector _ _ is_inc as l)r =
  let l' = to_num sign l in
  let n = op l' (match r with | I -> (1 : integer) | _ -> 0 end) in
  to_vec is_inc (length l * size,n)
    
(* add_vec_bit
 * add_vec_bit_signed
 * minus_vec_bit_signed
 *)
let add_VBV = arith_op_vec_bit integerAdd false 1
let addS_VBV = arith_op_vec_bit integerAdd true 1
let minus_VBV = arith_op_vec_bit integerMinus true 1

let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (Vector _ _ is_inc as l) r =
  let len = length l in
  let act_size = len * size in
  let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
  let n = op l_sign r_sign in
  let n_unsign = op l_unsign r_unsign in
  let correct_size_num = to_vec is_inc (act_size,n) in
  let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in
  let overflow =
    if n <= get_max_representable_in sign len &&
         n >= get_min_representable_in sign len
    then O else I in
  let c_out = most_significant one_more_size_u in
  (correct_size_num,overflow,c_out)

(* add_overflow_vec
 * add_overflow_vec_signed
 * minus_overflow_vec
 * minus_overflow_vec_signed
 * mult_overflow_vec
 * mult_overflow_vec_signed
 *)
let addO_VVV = arith_op_overflow_vec integerAdd false 1
let addSO_VVV = arith_op_overflow_vec integerAdd true 1
let minusO_VVV = arith_op_overflow_vec integerMinus false 1
let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
let multO_VVV = arith_op_overflow_vec integerMult false 2
let multSO_VVV = arith_op_overflow_vec integerMult true 2

let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
                                  (Vector _ _ is_inc as l) r_bit =
  let act_size = length l * size in
  let l' = to_num sign l in
  let l_u = to_num false l in
  let (n,nu,changed) = match r_bit with
    | I -> (op l' 1, op l_u 1, true)
    | O -> (l',l_u,false)
    | _ -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
    end in
(*    | _ -> assert false *)
  let correct_size_num = to_vec is_inc (act_size,n) in
  let one_larger = to_vec is_inc (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 O else I 
    else I in
  (correct_size_num,overflow,most_significant one_larger)

(* add_overflow_vec_bit_signed
 * minus_overflow_vec_bit
 * minus_overflow_vec_bit_signed 
 *)
let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1
let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1
let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1
    
type shift = LL_shift | RR_shift | LLL_shift

let shift_op_vec op ((Vector bs start is_inc as l),(n : integer)) =
  let len = integerFromNat (List.length bs) in
    match op with
     | LL_shift (*"<<"*) ->
       let right_vec = Vector (List.replicate (natFromInteger n) O) 0 true in
       let left_vec = slice l n (if is_inc then len + start else start - len) in
       vector_concat left_vec right_vec
     | RR_shift (*">>"*) ->
       let right_vec = slice l start n in
       let left_vec = Vector (List.replicate (natFromInteger n) O) 0 true in
       vector_concat left_vec right_vec 
     | LLL_shift (*"<<<"*) ->
       let left_vec = slice l n (if is_inc then len + start else start - len) in
       let right_vec = slice l start n in
       vector_concat left_vec right_vec
     end

let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)

let rec arith_op_no0 (op : integer -> integer -> integer) l r = 
  if r = 0
  then Nothing
  else Just (op l r)

let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector _ start is_inc) as l) r =
  let act_size = length l * size in
  let (l',r') = (to_num sign l,to_num sign r) in
  let n = arith_op_no0 op l' r' in
  let (representable,n') = 
    match n with 
    | Just n' ->  
      (n' <= get_max_representable_in sign act_size &&
         n' >= get_min_representable_in sign act_size, n')
    | _ -> (false,0)
    end in
  if representable 
  then to_vec is_inc (act_size,n')
  else Vector (List.replicate (natFromInteger act_size) Undef) start is_inc

let mod_VVV = arith_op_vec_no0 integerMod false 1
let quot_VVV = arith_op_vec_no0 integerDiv false 1
let quotS_VVV = arith_op_vec_no0 integerDiv true 1

let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
  let rep_size = length r * size in
  let act_size = length l * size in
  let (l',r') = (to_num sign l,to_num sign r) in
  let (l_u,r_u) = (to_num false l,to_num false r) in
  let n = arith_op_no0 op l' r' in
  let n_u = arith_op_no0 op l_u r_u in
  let (representable,n',n_u') = 
    match (n, n_u) with 
    | (Just n',Just n_u') ->  
       ((n' <= get_max_representable_in sign rep_size &&
           n' >= (get_min_representable_in sign rep_size)), n', n_u')
    | _ -> (true,0,0)
    end in
  let (correct_size_num,one_more) = 
    if representable then
      (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
    else
      (Vector (List.replicate (natFromInteger act_size) Undef) start is_inc,
       Vector (List.replicate (natFromInteger (act_size + 1)) Undef) start is_inc) in
  let overflow = if representable then O else I in
  (correct_size_num,overflow,most_significant one_more)

let quotO_VVV = arith_op_overflow_no0_vec integerDiv false 1
let quotSO_VVV = arith_op_overflow_no0_vec integerDiv true 1

let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r =
  arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r))

let mod_VIV = arith_op_vec_range_no0 integerMod false 1

let duplicate (bit,length) =
  Vector (List.replicate (natFromInteger length) bit) 0 true

val repeat : forall 'a. list 'a -> integer -> list 'a
let rec repeat xs n =
  if n = 0 then []
  else xs ++ repeat xs (n-1)

let duplicate_bits (Vector bits start direction,len) = 
  let bits' = repeat bits len in
  Vector bits' start direction

let compare_op op (l,r) = bool_to_bit (op l r)

let lt = compare_op (<)
let gt = compare_op (>)
let lteq = compare_op (<=)
let gteq = compare_op (>=)


let compare_op_vec op sign (l,r) = 
  let (l',r') = (to_num sign l, to_num sign r) in
  compare_op op (l',r')

let lt_vec = compare_op_vec (>) true
let gt_vec = compare_op_vec (>) true
let lteq_vec = compare_op_vec (<=) true
let gteq_vec = compare_op_vec (>=) true

let lt_vec_signed = compare_op_vec (<) true
let gt_vec_signed = compare_op_vec (>) true
let lteq_vec_signed = compare_op_vec (<=) true
let gteq_vec_signed = compare_op_vec (>=) true
let lt_vec_unsigned = compare_op_vec (<) false
let gt_vec_unsigned = compare_op_vec (>) false
let lteq_vec_unsigned = compare_op_vec (<=) false
let gteq_vec_unsigned = compare_op_vec (>=) false

let compare_op_vec_range op sign (l,r) = 
  compare_op op ((to_num sign l),r)

let lt_vec_range = compare_op_vec_range (<) true
let gt_vec_range = compare_op_vec_range (>) true
let lteq_vec_range = compare_op_vec_range (<=) true
let gteq_vec_range = compare_op_vec_range (>=) true

let compare_op_range_vec op sign (l,r) =
  compare_op op (l, (to_num sign r))

let lt_range_vec = compare_op_range_vec (<) true
let gt_range_vec = compare_op_range_vec (>) true
let lteq_range_vec = compare_op_range_vec (<=) true
let gteq_range_vec = compare_op_range_vec (>=) true

let eq (l,r) = bool_to_bit (l = r)
let eq_range (l,r) = bool_to_bit (l = r)
let eq_vec (l,r) = bool_to_bit (l = r)
let eq_bit (l,r) = bool_to_bit (l = r)
let eq_vec_range (l,r) = eq (to_num false l,r)
let eq_range_vec (l,r) = eq (l, to_num false r)
let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)

let neq (l,r) = bitwise_not_bit (eq (l,r))
let neq_bit (l,r) = bitwise_not_bit (eq_bit (l,r))
let neq_range (l,r) = bitwise_not_bit (eq_range (l,r))
let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r))
let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r))
let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r))


val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
let make_indexed_vector entries default start length dir =
  let length = natFromInteger length in
  Vector (List.foldl replace (replicate length default) entries) start dir

val make_bit_vector_undef : integer -> vector bitU
let make_bitvector_undef length =
  Vector (replicate (natFromInteger length) Undef) 0 true

(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)

let mask (n,Vector bits start dir) =
  let current_size = List.length bits in
  Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir


let bit_of_bit_lifted = function
  | Bitl_zero -> O
  | Bitl_one  -> I
  | Bitl_undef -> Undef
  | _ -> failwith "bit_of_bit_lifted: unexpected Bitl_unknown"
end

val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
let rec byte_chunks n list = match (n,list) with
  | (0,_) -> []
  | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
  | _ -> failwith "byte_chunks not given enough bits"
end


val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> vector bitU
let bitv_of_byte_lifteds v =
  Vector (foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v) 0 true


val byte_lifteds_of_bitv : vector bitU -> list byte_lifted
let byte_lifteds_of_bitv (Vector bits length is_inc) = 
  let bits = List.map bit_lifted_of_bitU bits in
  byte_lifteds_of_bit_lifteds bits

val address_lifted_of_bitv : vector bitU -> address_lifted
let address_lifted_of_bitv v =
  Address_lifted (byte_lifteds_of_bitv v) Nothing


val bitvFromRegisterValue : register_value -> vector bitU
let bitvFromRegisterValue v =
  Vector (List.map bitU_of_bit_lifted v.rv_bits)
         (integerFromNat v.rv_start_internal)
         (v.rv_dir = D_increasing)


val registerValueFromBitv : vector bitU -> register -> register_value
let registerValueFromBitv (Vector bits start is_inc) reg = 
  let start = natFromInteger start in
  let bit_lifteds =
    List.map bit_lifted_of_bitU bits in
  <| rv_bits = bit_lifteds;
     rv_dir = dir is_inc;
     rv_start_internal = start;
     rv_start = if is_inc then start else start+1 - (size_of_reg_nat reg) |>


class (ToNatural 'a)
  val toNatural : 'a -> natural
end


instance (ToNatural integer)
  let toNatural = naturalFromInteger
end

instance (ToNatural int)
  let toNatural = naturalFromInt
end

instance (ToNatural nat)
  let toNatural = naturalFromNat
end

instance (ToNatural natural)
  let toNatural = id
end


let toNaturalFiveTup (n1,n2,n3,n4,n5) =
  (toNatural n1,
   toNatural n2,
   toNatural n3,
   toNatural n4,
   toNatural n5)


val foreach_inc :  forall 'vars. (integer * integer * integer) -> 'vars ->
                   (integer -> 'vars -> 'vars) -> 'vars
let rec foreach_inc (i,stop,by) vars body = 
  if i <= stop
  then let vars = body i vars in
       foreach_inc (i + by,stop,by) vars body
  else vars

val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
                  (integer -> 'vars -> 'vars) -> 'vars
let rec foreach_dec (i,stop,by) vars body = 
  if i >= stop
  then let vars = body i vars in
       foreach_dec (i - by,stop,by) vars body
  else vars

let assert' b msg_opt =
  let msg = match msg_opt with
  | Just msg -> msg
  | Nothing  -> "unspecified error"
  end in
  if to_bool b then failwith msg else ()