Last of the aarch64_no_vector monomorphisation replacements

3 files changed, 98 insertions, 0 deletions

diff --git a/aarch64/mono/aarch64_memory_literal_general.sail b/aarch64/mono/aarch64_memory_literal_general.sail
new file mode 100644
index 00000000..24012aef
--- /dev/null
+++ b/aarch64/mono/aarch64_memory_literal_general.sail
@@ -0,0 +1,42 @@
+/* Change argument to number of bits rather than bytes
+   (also, move constraint as size may be undefined...) */
+
+val aarch64_memory_literal_general : forall ('size : Int).
+  (MemOp, bits(64), bool, atom('size), int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+
+function aarch64_memory_literal_general (memop, offset, signed, size, t) = {
+  address : bits(64) = aget_PC() + offset;
+  data : bits('size) = undefined;
+  match memop {
+    MemOp_LOAD => {
+      assert(constraint('size >= 0));
+      let 'bytes = size / 8;
+      assert(constraint(8 * 'bytes = 'size));
+      data = aget_Mem(address, bytes, AccType_NORMAL);
+      if signed then aset_X(t, SignExtend(data, 64)) else aset_X(t, data)
+    },
+    MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0))
+  }
+}
+
+val memory_literal_general_decode : (bits(2), bits(1), bits(19), bits(5)) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
+
+function memory_literal_general_decode (opc, V, imm19, Rt) = {
+  __unconditional = true;
+  t : int = UInt(Rt);
+  memop : MemOp = MemOp_LOAD;
+  signed : bool = false;
+  size : int = undefined;
+  offset : bits(64) = undefined;
+  match opc {
+    0b00 => size = 4,
+    0b01 => size = 8,
+    0b10 => {
+      size = 4;
+      signed = true
+    },
+    0b11 => memop = MemOp_PREFETCH
+  };
+  offset = SignExtend(imm19 @ 0b00, 64);
+  aarch64_memory_literal_general(memop, offset, signed, 8 * size, t)
+}
diff --git a/aarch64/mono/aarch64_memory_literal_simdfp.sail b/aarch64/mono/aarch64_memory_literal_simdfp.sail
new file mode 100644
index 00000000..cfbe87e1
--- /dev/null
+++ b/aarch64/mono/aarch64_memory_literal_simdfp.sail
@@ -0,0 +1,14 @@
+/* Needed set constraint */
+
+val aarch64_memory_literal_simdfp : forall ('size : Int).
+  (bits(64), atom('size), int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+
+function aarch64_memory_literal_simdfp (offset, size, t) = {
+  assert(constraint('size >= 0));
+  assert(constraint('size in {4,8,16}));
+  address : bits(64) = aget_PC() + offset;
+  data : bits(8 * 'size) = undefined;
+  CheckFPAdvSIMDEnabled64();
+  data = aget_Mem(address, size, AccType_VEC);
+  aset_V(t, data)
+}
diff --git a/aarch64/mono/aarch64_memory_vector_single_nowb.sail b/aarch64/mono/aarch64_memory_vector_single_nowb.sail
new file mode 100644
index 00000000..545a8351
--- /dev/null
+++ b/aarch64/mono/aarch64_memory_vector_single_nowb.sail
@@ -0,0 +1,42 @@
+val aarch64_memory_vector_single_nowb : forall ('datasize : Int) ('esize : Int) ('selem : Int).
+  (atom('datasize), atom('esize), int, int, MemOp, int, bool, atom('selem), int, bool) -> unit effect {escape, rmem, wmem, undef, wreg, rreg}
+
+function aarch64_memory_vector_single_nowb (datasize, esize, index, m, memop, n, replicate, selem, t__arg, wback) = {
+  assert(constraint('datasize >= 0 & 'selem >= 1 & 'esize >= 0));
+  t = t__arg;
+  CheckFPAdvSIMDEnabled64();
+  address : bits(64) = undefined;
+  offs : bits(64) = undefined;
+  rval : bits(128) = undefined;
+  element : bits('esize) = undefined;
+  s : int = undefined;
+  let 'ebytes : {'n, true. atom('n)} = ex_int(esize / 8);
+  assert(constraint(8 * 'ebytes = 'esize));
+  if n == 31 then {
+    CheckSPAlignment();
+    address = aget_SP()
+  } else address = aget_X(n);
+  offs = Zeros();
+  if replicate then foreach (s from 0 to (selem - 1) by 1 in inc) {
+    element = aget_Mem(address + offs, ebytes, AccType_VEC);
+    let 'v : {'n, true. atom('n)} = ex_int(datasize / esize) in {
+      assert(constraint('esize * 'v = 'datasize));
+      aset_V(t, replicate_bits(element, 'v))
+    };
+    offs = offs + ebytes;
+    t = (t + 1) % 32
+  } else foreach (s from 0 to (selem - 1) by 1 in inc) {
+    rval = aget_V(t);
+    if memop == MemOp_LOAD then {
+      rval = aset_Elem(rval, index, esize, aget_Mem(address + offs, ebytes, AccType_VEC));
+      aset_V(t, rval)
+    } else aset_Mem(address + offs, ebytes, AccType_VEC, aget_Elem(rval, index, esize));
+    offs = offs + ebytes;
+    t = (t + 1) % 32
+  };
+  if wback then {
+    if m != 31 then offs = aget_X(m)
+    else ();
+    if n == 31 then aset_SP(address + offs) else aset_X(n, address + offs)
+  } else ()
+}