Clean up aarch64_extras.lem

2 files changed, 14 insertions, 48 deletions

diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index a50ba76f..03a3b390 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -15,46 +15,6 @@ type ty2048
 instance (Size ty2048) let size = 2048 end
 declare isabelle target_rep type ty2048 = `2048`
 
-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 bs = bools_of_int (hi + 1) n in
-  subrange_list false bs hi lo
-
-val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a
-let get_slice_int len n lo = of_bools (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 bs = bools_of_int (hi + 1) n in
-  (*let len_n = max (hi + 1) (integerFromNat (List.length bs)) in
-  let ext_bs = exts_bools len_n bs in*)
-  signed_of_bools (update_subrange_list false bs hi lo (bitlistFromWord 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_bool_list c =
   if c = #'0' then      Just ([false;false;false;false])
   else if c = #'1' then Just ([false;false;false;true ])
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;