Clean up aarch64_extras.lem

1 files changed, 14 insertions, 8 deletions

diff --git a/aarch64/mono/demo/aarch64_no_vector/main.sail b/aarch64/mono/demo/aarch64_no_vector/main.sail
index 1e44f531..e9e2f84f 100644
--- a/aarch64/mono/demo/aarch64_no_vector/main.sail
+++ b/aarch64/mono/demo/aarch64_no_vector/main.sail
@@ -1,18 +1,24 @@
-val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+$include <elf.sail>
 
-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
-}
+// Simple top level fetch and execute loop.
+val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
 
-val elf_entry = "Elf_loader.elf_entry" : unit -> int
+function fetch_and_execute () =
+  while true do {
+    try {
+      let instr = aget_Mem(_PC, 4, AccType_IFETCH);
+      decode(instr);
+    } catch {
+      Error_See("HINT") => (),
+      _ => exit(())
+    };
+    if __BranchTaken then __BranchTaken = false else _PC = _PC + 4
+  }
 
 val main : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
 
 function main () = {
   _PC = __GetSlice_int(64, elf_entry(), 0);
-  print(BitStr(_PC));
   SP_EL0 = ZeroExtend(0x3C00, 64);
   PSTATE.D = 0b1;
   PSTATE.A = 0b1;