path: root/src/gen_lib/sail_values.lem

open import Pervasives
open import State
open import Vector
open import Arch

let to_bool = function
  | B0 -> false
  | B1  -> true
(*  | BU -> assert false *)
  end

let get_elements (Vector elements _) = elements
let get_start (Vector _ s) = s
let length (Vector bs _) = length bs

(*
let write_two_registers r1 r2 vec =
  let size = length_register r1 in
  let start = get_start vec in
  let vsize = length vec in
  let r1_v = read_vector_subrange is_inc vec start ((if is_inc then size - start else start - size) - 1) in
  let r2_v =
    read_vector_subrange is_inc
      vec (if is_inc then size - start else start - size)
      (if is_inc then vsize - start else start - vsize) in
  write_register r1 r1_v >> write_register r2 r2_v
 *)

let rec replace bs ((n : nat),b') = match (n,bs) with
  | (_, []) -> []
  | (0, _::bs) -> b' :: bs
  | (n+1, b::bs) -> b :: replace bs (n,b')
  end

let make_indexed_vector entries default start length =
  let default = match default with Nothing -> BU | Just v -> v end in
  Vector (List.foldl replace (replicate length default) entries) start

let vector_concat (Vector bs start) (Vector bs' _) = Vector(bs ++ bs') start

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

let most_significant (Vector bs _) =
  let (b :: _) = bs in b

let bitwise_not_bit = function
  | B1 -> B0
  | B0 -> B1
  | _ -> BU
  end

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

let bool_to_bit b = if b then B1 else B0

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

let bitwise_and_bit = bitwise_binop_bit (&&)
let bitwise_or_bit = bitwise_binop_bit (||)
let bitwise_xor_bit = bitwise_binop_bit xor

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

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

let unsigned (Vector bs _ as v) : integer =
  match has_undef v with
  | true ->
     fst (List.foldl
            (fun (acc,exp) b -> (acc + (if b = B1 then integerPow 2 exp else 0),exp +1)) (0,0) bs)
  end

let signed v =
  match most_significant v with
  | B1 -> 0 - (1 + (unsigned (bitwise_not v)))
  | B0 -> unsigned v
  end

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 = 
  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 (n -1)
                       | false -> integerPow 2 n
       end

let get_min_representable_in _ n = 
  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 n)


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

let rec add_one_bit bs co i =
  if i < 0 then bs
  else match (nth bs i,co) with
    | (B0,false) -> replace bs (i,B1)
    | (B0,true)  -> add_one_bit (replace bs (i,B1)) true (i-1)
    | (B1,false) -> add_one_bit (replace bs (i,B0)) true (i-1)
    | (B1,true)  -> add_one_bit bs true (i-1)
   (*    | Vundef,_ -> assert false*) 
  end

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

let to_vec_inc = to_vec
let to_vec_dec = to_vec

let to_vec_undef len =
  Vector (replicate len BU) (if is_inc then 0 else len-1)

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

let arith_op_vec op sign size (l,r) =
  let (l',r') = (to_num sign l, to_num sign r) in
  let n = op  l' r' in
  to_vec (size * (length l),n)

let add_vec = arith_op_vec integerAdd false 1
let add_vec_signed = arith_op_vec integerAdd true 1
let minus_vec = arith_op_vec integerMinus false 1
let multiply_vec = arith_op_vec integerMult false 2
let multiply_vec_signed = arith_op_vec integerMult true 2

let arith_op_vec_range op sign size (l,r) =
  arith_op_vec op sign size (l, to_vec (length l,r))

let add_vec_range = arith_op_vec_range integerAdd false 1
let add_vec_range_signed = arith_op_vec_range integerAdd true 1
let minus_vec_range = arith_op_vec_range integerMinus false 1
let mult_vec_range = arith_op_vec_range integerMult false 2
let mult_vec_range_signed = arith_op_vec_range integerMult true 2

let arith_op_range_vec op sign size (l,r) =
  arith_op_vec op sign size (to_vec (length r, l), r)

let add_range_vec = arith_op_range_vec integerAdd false 1
let add_range_vec_signed = arith_op_range_vec integerAdd true 1
let minus_range_vec = arith_op_range_vec integerMinus false 1
let mult_range_vec = arith_op_range_vec integerMult false 2
let mult_range_vec_signed = arith_op_range_vec integerMult true 2

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

let add_range_vec_range = arith_op_range_vec_range integerAdd false
let add_range_vec_range_signed = arith_op_range_vec_range integerAdd true
let minus_range_vec_range = arith_op_range_vec_range integerMinus false

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

let add_vec_range_range = arith_op_vec_range_range integerAdd false
let add_vec_range_range_signed = arith_op_vec_range_range integerAdd true
let minus_vec_range_range = 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'

let add_vec_vec_range = arith_op_vec_vec_range integerAdd false
let add_vec_vec_range_signed = arith_op_vec_vec_range integerAdd true

let arith_op_vec_bit op sign (size : nat) (l,r) =
  let l' = to_num sign l in
  let n = op l' match r with | B1 -> (1 : integer) | _ -> 0 end in
  to_vec (length l * size,n)
    
let add_vec_bit = arith_op_vec_bit integerAdd false 1
let add_vec_bit_signed = arith_op_vec_bit integerAdd true 1
let minus_vec_bit = arith_op_vec_bit integerMinus true 1

let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (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 (act_size,n) in
  let one_more_size_u = to_vec (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_num,overflow,c_out)

let add_overflow_vec = arith_op_overflow_vec integerAdd false 1
let add_overflow_vec_signed = arith_op_overflow_vec integerAdd true 1
let minus_overflow_vec = arith_op_overflow_vec integerMinus false 1
let minus_overflow_vec_signed = arith_op_overflow_vec integerMinus true 1
let mult_overflow_vec = arith_op_overflow_vec integerMult false 2
let mult_overflow_vec_signed = arith_op_overflow_vec integerMult true 2
    
let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : nat) (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
    | B1 -> (op l' 1, op l_u 1, true)
    | B0 -> (l',l_u,false)
    end in
(*    | _ -> assert false *)
  let correct_size_num = to_vec (act_size,n) in
  let one_larger = to_vec (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 B1 in
  (correct_size_num,overflow,most_significant one_larger)

let add_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerAdd true 1
let minus_overflow_vec_bit = arith_op_overflow_vec_bit integerMinus false 1
let minus_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerMinus true 1
    
type shift = LL | RR | LLL

let shift_op_vec op (((Vector bs start) as l),r) =
  let len = List.length bs in
  let n = r in
    match op with
     | LL (*"<<"*) ->
       let right_vec = Vector (List.replicate n B0) 0 in
       let left_vec = read_vector_subrange is_inc l n (if is_inc then len + start else start - len) in
       vector_concat left_vec right_vec
     | RR (*">>"*) ->
       let right_vec = read_vector_subrange is_inc l start n in
       let left_vec = Vector (List.replicate n B0) 0 in
       vector_concat left_vec right_vec 
     | LLL (*"<<<"*) ->
       let left_vec = read_vector_subrange is_inc l n (if is_inc then len + start else start - len) in
       let right_vec = read_vector_subrange is_inc l start n in
       vector_concat left_vec right_vec
     end

let bitwise_leftshift = shift_op_vec LL (*"<<"*)
let bitwise_rightshift = shift_op_vec RR (*">>"*)
let bitwise_rotate = shift_op_vec LLL (*"<<<"*)

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) 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 (act_size,n')
  else Vector (List.replicate act_size BU) start

let mod_vec = arith_op_vec_no0 integerMod false 1
let quot_vec = arith_op_vec_no0 integerDiv false 1
let quot_vec_signed = arith_op_vec_no0 integerDiv true 1

let arith_op_overflow_no0_vec op sign size (((Vector _ start) 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 (act_size,n'),to_vec (act_size + 1,n_u'))
    else
      (Vector (List.replicate act_size BU) start,
       Vector (List.replicate (act_size + 1) BU) start) in
  let overflow = if representable then B0 else B1 in
  (correct_size_num,overflow,most_significant one_more)

let quot_overflow_vec = arith_op_overflow_no0_vec integerDiv false 1
let quot_overflow_vec_signed = arith_op_overflow_no0_vec integerDiv true 1

let arith_op_vec_range_no0 op sign size (l,r) =
  arith_op_vec_no0 op sign size (l,to_vec (length l,r))

let mod_vec_range = arith_op_vec_range_no0 integerMod false 1

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


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_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_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r))