Add generated ARM spec and test cases for it

We add the generated ARM no_vector spec from the public v8.3 XML
release, mostly so that we can add end-to-end test cases for sail
using it. This kind of large example is very useful for thoroughly
testing the sail compiler and interpreter.

1 files changed, 23 insertions, 0 deletions

diff --git a/aarch64/main.sail b/aarch64/main.sail
new file mode 100644
index 00000000..b48f84d9
--- /dev/null
+++ b/aarch64/main.sail
@@ -0,0 +1,23 @@
+val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+
+function fetch_and_execute () = while true do {
+  let instr = aget_Mem(_PC, 4, AccType_IFETCH);
+  decode(instr);
+  if __BranchTaken then __BranchTaken = false else _PC = _PC + 4
+}
+
+val elf_entry = "Elf_loader.elf_entry" : unit -> int
+
+val main : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+
+function main () = {
+  _PC = __GetSlice_int(64, elf_entry(), 0);
+  SP_EL0 = ZeroExtend(0x3C00, 64);
+  PSTATE.D = 0b1;
+  PSTATE.A = 0b1;
+  PSTATE.I = 0b1;
+  PSTATE.F = 0b1;
+  OSLSR_EL1 = ZeroExtend(0b10, 32);
+  __BranchTaken = false;
+  fetch_and_execute()
+}