Add alternative definitions of aarch64 functions for monomorphisation

12 files changed, 397 insertions, 0 deletions

diff --git a/aarch64/mono/ASR_C.sail b/aarch64/mono/ASR_C.sail
new file mode 100644
index 00000000..988af5a2
--- /dev/null
+++ b/aarch64/mono/ASR_C.sail
@@ -0,0 +1,9 @@
+val ASR_C : forall ('N : Int), 'N >= 0 & 'N >= 0 & 1 >= 0.
+  (bits('N), int) -> (bits('N), bits(1)) effect {escape}
+
+function ASR_C (x, shift) = {
+  assert(shift > 0, "(shift > 0)");
+  result : bits('N) = arith_shiftright(x, shift);
+  carry_out : bits(1) = if shift > 'N then [x['N - 1]] else [x[shift - 1]];
+  return((result, carry_out))
+}
diff --git a/aarch64/mono/BigEndianReverse.sail b/aarch64/mono/BigEndianReverse.sail
new file mode 100644
index 00000000..23b222f4
--- /dev/null
+++ b/aarch64/mono/BigEndianReverse.sail
@@ -0,0 +1,10 @@
+val BigEndianReverse : forall ('width : Int), 'width >= 0 & 'width >= 0.
+  bits('width) -> bits('width) effect {escape}
+
+function BigEndianReverse value_name = {
+  assert(('width == 8) | (('width == 16) | (('width == 32) | (('width == 64) | ('width == 128)))));
+  result : bits('width) = replicate_bits(0b0,'width);
+  foreach (i from 0 to ('width - 1) by 8)
+    result[i+7 .. i] = (value_name['width-i - 1 .. 'width-i - 8] : bits(8));
+  return result
+}
diff --git a/aarch64/mono/CountLeadingSignBits.sail b/aarch64/mono/CountLeadingSignBits.sail
new file mode 100644
index 00000000..8470da75
--- /dev/null
+++ b/aarch64/mono/CountLeadingSignBits.sail
@@ -0,0 +1,3 @@
+val CountLeadingSignBits : forall ('N : Int), 'N >= 3. bits('N) -> int
+
+function CountLeadingSignBits x = return(CountLeadingZeroBits((x >> 1) ^ (x & slice_mask(0,'N))))
diff --git a/aarch64/mono/LSL_C.sail b/aarch64/mono/LSL_C.sail
new file mode 100644
index 00000000..b8d316bb
--- /dev/null
+++ b/aarch64/mono/LSL_C.sail
@@ -0,0 +1,9 @@
+val LSL_C : forall ('N : Int), 'N >= 0 & 'N >= 0 & 1 >= 0.
+  (bits('N), int) -> (bits('N), bits(1)) effect {escape}
+
+function LSL_C (x, shift) = {
+  assert(shift > 0, "(shift > 0)");
+  result : bits('N) = x << shift;
+  carry_out : bits(1) = if shift > 'N then 0b0 else [x['N - shift]];
+  return((result, carry_out))
+}
diff --git a/aarch64/mono/LSR_C.sail b/aarch64/mono/LSR_C.sail
new file mode 100644
index 00000000..65bdfd7f
--- /dev/null
+++ b/aarch64/mono/LSR_C.sail
@@ -0,0 +1,9 @@
+val LSR_C : forall ('N : Int), 'N >= 0 & 'N >= 0 & 1 >= 0.
+  (bits('N), int) -> (bits('N), bits(1)) effect {escape}
+
+function LSR_C (x, shift) = {
+  assert(shift > 0, "(shift > 0)");
+  result : bits('N) = x >> shift;
+  carry_out : bits(1) = if shift > 'N then 0b0 else [x[shift - 1]];
+  return((result, carry_out))
+}
diff --git a/aarch64/mono/Poly32Mod2.sail b/aarch64/mono/Poly32Mod2.sail
new file mode 100644
index 00000000..346e6f83
--- /dev/null
+++ b/aarch64/mono/Poly32Mod2.sail
@@ -0,0 +1,11 @@
+val Poly32Mod2 : forall ('N : Int), 'N >= 0 & 32 >= 0 & 32 >= 0.
+  (bits('N), bits(32)) -> bits(32) effect {escape}
+
+function Poly32Mod2 (data__arg, poly) = {
+  data = data__arg;
+  assert('N > 32, "(N > 32)");
+  let poly' : bits('N) = extzv(poly) in
+  foreach (i from ('N - 1) to 32 by 1 in dec)
+    if [data[i]] == 0b1 then data = data | (poly' << i - 32) else ();
+  return(slice(data, 0, 32))
+}
diff --git a/aarch64/mono/Reduce.sail b/aarch64/mono/Reduce.sail
new file mode 100644
index 00000000..efa49b27
--- /dev/null
+++ b/aarch64/mono/Reduce.sail
@@ -0,0 +1,19 @@
+val Reduce : forall ('N : Int) ('esize : Int), 'N >= 0 & 'esize >= 0.
+  (ReduceOp, bits('N), atom('esize)) -> bits('esize) effect {escape, rreg, undef, wreg}
+
+function Reduce (op, input, esize) = {
+  result : bits('esize) = input['esize - 1 .. 0];
+  if 'N > 'esize then
+    foreach (i from 'esize to ('N - 1) by 'esize) {
+      operand : bits('esize) = input[i+'esize - 1 .. i];
+      match op {
+        ReduceOp_FMINNUM => result = FPMinNum(result, operand, FPCR),
+        ReduceOp_FMAXNUM => result = FPMaxNum(result, operand, FPCR),
+        ReduceOp_FMIN => result = FPMin(result, operand, FPCR),
+        ReduceOp_FMAX => result = FPMax(result, operand, FPCR),
+        ReduceOp_FADD => result = FPAdd(result, operand, FPCR),
+        ReduceOp_ADD => result = result + operand
+      };
+    };
+  return(result)
+}
diff --git a/aarch64/mono/SignExtend__0.sail b/aarch64/mono/SignExtend__0.sail
new file mode 100644
index 00000000..1d5449c9
--- /dev/null
+++ b/aarch64/mono/SignExtend__0.sail
@@ -0,0 +1,7 @@
+val SignExtend__0 : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
+  (bits('M), atom('N)) -> bits('N) effect {escape}
+
+function SignExtend__0 (x, N) = {
+  assert('N >= 'M);
+  return(extsv(x))
+}
diff --git a/aarch64/mono/ZeroExtend__0.sail b/aarch64/mono/ZeroExtend__0.sail
new file mode 100644
index 00000000..c84868a0
--- /dev/null
+++ b/aarch64/mono/ZeroExtend__0.sail
@@ -0,0 +1,7 @@
+val ZeroExtend__0 : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
+  (bits('M), atom('N)) -> bits('N) effect {escape}
+
+function ZeroExtend__0 (x, N) = {
+  assert(true);
+  extzv(x)
+}
\ No newline at end of file
diff --git a/aarch64/mono/_slice.sail b/aarch64/mono/_slice.sail
new file mode 100644
index 00000000..2bac9f8c
--- /dev/null
+++ b/aarch64/mono/_slice.sail
@@ -0,0 +1,35 @@
+val IsZero_slice : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect {escape}
+
+function IsZero_slice (xs, i, 'l) = {
+  assert(constraint('l >= 0));
+  IsZero(xs & slice_mask(i, l))
+}
+
+val IsOnes_slice : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect {escape}
+
+function IsOnes_slice (xs, i, 'l) = {
+  assert(constraint('l >= 0));
+  let m : bits('n) = slice_mask(i,l) in
+  (xs & m) == m
+}
+
+val ZeroExtend_slice_append : forall 'n 'm 'o, 'n >= 0 & 'm >= 0 & 'o >= 0.
+  (bits('n), int, int, bits('m)) -> bits('o) effect {escape}
+
+function ZeroExtend_slice_append (xs, i, 'l, ys) = {
+  assert(constraint('l >= 0));
+  let xs = xs & slice_mask(i,l) in
+  let xs : bits('o) = ZeroExtend(xs >> i) << 'm in
+  let ys : bits('o) = ZeroExtend(ys) in
+  xs | ys
+}
+
+val IsZero_slice2 : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect {escape}
+
+function IsZero_slice2 (xs, i, 'l) = {
+  assert(constraint('l >= 0));
+  IsZero(xs & slice_mask(i, l))
+}
diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
new file mode 100644
index 00000000..4a32ad44
--- /dev/null
+++ b/aarch64/mono/aarch64_extras.lem
@@ -0,0 +1,131 @@
+open import Pervasives_extra
+open import Sail_instr_kinds
+open import Sail_values
+open import Sail_operators_mwords
+open import Prompt_monad
+open import State
+
+type ty2048
+instance (Size ty2048) let size = 2048 end
+declare isabelle target_rep type ty2048 = `2048`
+
+val prerr_endline : string -> unit
+let prerr_endline _ = ()
+declare ocaml target_rep function prerr_endline = `prerr_endline`
+
+val print_int : string -> integer -> unit
+let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
+
+val putchar : integer -> unit
+let putchar _ = ()
+declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
+
+val uint : forall 'a. Size 'a => mword 'a -> integer
+let uint = unsigned
+val sint : forall 'a. Size 'a => mword 'a -> integer
+let sint = signed
+
+val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
+let slice v lo len =
+  subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : forall 'a 'b. Size 'a, Size 'b => integer -> integer -> mword 'a -> integer -> mword 'b -> mword 'a
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+  update_subrange_vec_dec out (n + slice_len - 1) n v
+
+let get_slice_int_bl len n lo =
+  (* TODO: Is this the intended behaviour? *)
+  let hi = lo + len - 1 in
+  let bits = bits_of_int (hi + 1) n in
+  get_bits false bits hi lo
+
+val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a
+let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
+
+val set_slice_int :  forall 'a. Size 'a => integer -> integer -> integer -> mword 'a -> integer
+let set_slice_int len n lo v =
+  let hi = lo + len - 1 in
+  let bits = bitlist_of_int n in
+  let len_n = max (hi + 1) (integerFromNat (List.length bits)) in
+  let ext_bits = exts_bits len_n bits in
+  signed (set_bits false ext_bits hi lo (bits_of v))
+
+let ext_slice signed v i j =
+  let len = length v in
+  let bits = get_bits false (bits_of v) i j in
+  of_bits (if signed then exts_bits len bits else extz_bits len bits)
+val exts_slice : list bitU -> integer -> integer -> list bitU
+let exts_slice v i j = ext_slice true v i j
+val extz_slice : list bitU -> integer -> integer -> list bitU
+let extz_slice v i j = ext_slice false v i j
+
+val shr_int : ii -> ii -> ii
+let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
+
+val shl_int : integer -> integer -> integer
+let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
+
+let hexchar_to_bitlist c =
+  if c = #'0' then [B0;B0;B0;B0]
+  else if c = #'1' then [B0;B0;B0;B1]
+  else if c = #'2' then [B0;B0;B1;B0]
+  else if c = #'3' then [B0;B0;B1;B1]
+  else if c = #'4' then [B0;B1;B0;B0]
+  else if c = #'5' then [B0;B1;B0;B1]
+  else if c = #'6' then [B0;B1;B1;B0]
+  else if c = #'7' then [B0;B1;B1;B1]
+  else if c = #'8' then [B1;B0;B0;B0]
+  else if c = #'9' then [B1;B0;B0;B1]
+  else if c = #'A' then [B1;B0;B1;B0]
+  else if c = #'a' then [B1;B0;B1;B0]
+  else if c = #'B' then [B1;B0;B1;B1]
+  else if c = #'b' then [B1;B0;B1;B1]
+  else if c = #'C' then [B1;B1;B0;B0]
+  else if c = #'c' then [B1;B1;B0;B0]
+  else if c = #'D' then [B1;B1;B0;B1]
+  else if c = #'d' then [B1;B1;B0;B1]
+  else if c = #'E' then [B1;B1;B1;B0]
+  else if c = #'e' then [B1;B1;B1;B0]
+  else if c = #'F' then [B1;B1;B1;B1]
+  else if c = #'f' then [B1;B1;B1;B1]
+  else failwith "hexchar_to_bitlist given unrecognized character"
+
+let hexstring_to_bits s =
+  match (toCharList s) with
+  | z :: x :: hs ->
+    let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
+    List.concat (List.map hexchar_to_bitlist str)
+  | _ -> failwith "hexstring_to_bits called with unexpected string"
+  end
+
+val hex_slice : forall 'n. Size 'n => string -> integer -> integer -> mword 'n
+let hex_slice v len lo =
+  let hi = len + lo - 1 in
+  let bits = extz_bits (len + lo) (hexstring_to_bits v) in
+  of_bits (get_bits false bits hi lo)
+
+let internal_pick vs = head vs
+
+let undefined_string () = ""
+let undefined_unit () = ()
+let undefined_int () = (0:ii)
+let undefined_bool () = false
+val undefined_vector : forall 'a. integer -> 'a -> list 'a
+let undefined_vector len u = repeat [u] len
+val undefined_bitvector : forall 'a. Size 'a => integer -> mword 'a
+let undefined_bitvector len = duplicate B0 len
+let undefined_bits len = undefined_bitvector len
+let undefined_bit () = B0
+let undefined_real () = realFromFrac 0 1
+let undefined_range i j = i
+let undefined_atom i = i
+let undefined_nat () = (0:ii)
+
+let write_ram addrsize size hexRAM address value =
+  write_mem_ea Write_plain address size >>
+  write_mem_val value >>= fun _ ->
+  return ()
+
+let read_ram addrsize size hexRAM address =
+  (*let _ = prerr_endline ("Reading " ^ (stringFromInteger size) ^ " bytes from address " ^ (stringFromInteger (unsigned address))) in*)
+  read_mem Read_plain address size
diff --git a/aarch64/mono/mono_rewrites.sail b/aarch64/mono/mono_rewrites.sail
new file mode 100644
index 00000000..2958c890
--- /dev/null
+++ b/aarch64/mono/mono_rewrites.sail
@@ -0,0 +1,147 @@
+/* Definitions for use with the -mono_rewrites option */
+
+/* External definitions not in the usual asl prelude */
+
+infix 6 <<
+
+val shiftleft = "shiftl" : forall 'n ('ord : Order).
+    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+
+overload operator << = {shiftleft}
+
+infix 6 >>
+
+val shiftright = "shiftr" : forall 'n ('ord : Order).
+    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+
+overload operator >> = {shiftright}
+
+val arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order).
+    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extzv(v) = extz_vec(sizeof('m),v)
+
+val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extsv(v) = exts_vec(sizeof('m),v)
+
+/* This is generated internally to deal with case splits which reveal the size
+   of a bitvector */
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+
+/* Definitions for the rewrites */
+
+val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure
+function slice_mask(i,l) =
+  let one : bits('n) = extzv(0b1) in
+  ((one << l) - one) << i
+
+val is_zero_subrange : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect pure
+
+function is_zero_subrange (xs, i, j) = {
+  (xs & slice_mask(j, i-j)) == extzv(0b0)
+}
+
+val is_ones_subrange : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect pure
+
+function is_ones_subrange (xs, i, j) = {
+  let m : bits('n) = slice_mask(j,j-i) in
+  (xs & m) == m
+}
+
+val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0.
+  (bits('n), int, int, bits('m), int, int) -> bits('r) effect pure
+
+function slice_slice_concat (xs, i, l, ys, i', l') = {
+  let xs = (xs & slice_mask(i,l)) >> i in
+  let ys = (ys & slice_mask(i',l')) >> i' in
+  extzv(xs) << l' | extzv(ys)
+}
+
+val slice_zeros_concat : forall 'n 'p 'q 'r, 'r = 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0.
+  (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure
+
+function slice_zeros_concat (xs, i, l, l') = {
+  let xs = (xs & slice_mask(i,l)) >> i in
+  extzv(xs) << l'
+}
+
+/* Assumes initial vectors are of equal size */
+
+val subrange_subrange_eq : forall 'n, 'n >= 0.
+  (bits('n), int, int, bits('n), int, int) -> bool effect pure
+
+function subrange_subrange_eq (xs, i, j, ys, i', j') = {
+  let xs = (xs & slice_mask(j,i-j)) >> j in
+  let ys = (ys & slice_mask(j',i'-j')) >> j' in
+  xs == ys
+}
+
+val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's = 'o - ('p - 1) + 'q - ('r - 1) & 'n >= 0 & 'm >= 0.
+  (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure
+
+function subrange_subrange_concat (xs, i, j, ys, i', j') = {
+  let xs = (xs & slice_mask(j,i-j)) >> j in
+  let ys = (ys & slice_mask(j',i'-j')) >> j' in
+  extzv(xs) << i' - (j' - 1) | extzv(ys)
+}
+
+val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
+  (bits('n), int, int, int) -> bits('m) effect pure
+
+function place_subrange(xs,i,j,shift) = {
+  let xs = (xs & slice_mask(j,i-j)) >> j in
+  extzv(xs) << shift
+}
+
+val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
+  (bits('n), int, int, int) -> bits('m) effect pure
+
+function place_slice(xs,i,l,shift) = {
+  let xs = (xs & slice_mask(i,l)) >> i in
+  extzv(xs) << shift
+}
+
+val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
+  (bits('n), int, int) -> bits('m) effect pure
+
+function zext_slice(xs,i,l) = {
+  let xs = (xs & slice_mask(i,l)) >> i in
+  extzv(xs)
+}
+
+val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
+  (bits('n), int, int) -> bits('m) effect pure
+
+function sext_slice(xs,i,l) = {
+  let xs = (xs & slice_mask(i,l)) >> i in
+  extsv(xs)
+}
+
+val UInt_slice : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> int effect pure
+
+function UInt_slice(xs,i,l) = {
+  let xs = (xs & slice_mask(i,l)) >> i in
+  UInt(xs)
+}
+
+val UInt_subrange : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> int effect pure
+
+function UInt_subrange(xs,i,j) = {
+  let xs = (xs & slice_mask(j,i-j)) >> i in
+  UInt(xs)
+}
+
+
+val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure
+
+function zext_ones(m) = {
+  let v : bits('n) = extsv(0b1) in
+  v >> ('n - m)
+}