Fix Lem generation for CHERI-MIPS and Aarch64

- Update Lem bindings and extras files
- Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's
  (used for cap_size in the CHERI spec)
- Add Lem and Isabelle Makefile targets for CHERI

6 files changed, 205 insertions, 200 deletions

diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem
new file mode 100644
index 00000000..58f1b9c7
--- /dev/null
+++ b/aarch64/aarch64_extras.lem
@@ -0,0 +1,136 @@
+open import Pervasives_extra
+open import Sail_instr_kinds
+open import Sail_values
+open import Sail_operators_bitlists
+open import Prompt_monad
+open import Prompt
+
+type ty512
+instance (Size ty512) let size = 512 end
+declare isabelle target_rep type ty512 = `512`
+type ty1024
+instance (Size ty1024) let size = 1024 end
+declare isabelle target_rep type ty1024 = `1024`
+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 slice : list bitU -> integer -> integer -> list bitU
+let slice v lo len =
+  subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
+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 : integer -> integer -> integer -> list bitU
+let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
+
+val set_slice_int : integer -> integer -> integer -> list bitU -> integer
+let set_slice_int len n lo v =
+  let hi = lo + len - 1 in
+  let bs = bit_list_of_int n in
+  let len_n = max (hi + 1) (integerFromNat (List.length bs)) in
+  let ext_bs = exts_bits len_n bs in
+  maybe_failwith (signed (update_subrange_list false ext_bs 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_bool_list c =
+  if c = #'0' then      Just ([false;false;false;false])
+  else if c = #'1' then Just ([false;false;false;true ])
+  else if c = #'2' then Just ([false;false;true; false])
+  else if c = #'3' then Just ([false;false;true; true ])
+  else if c = #'4' then Just ([false;true; false;false])
+  else if c = #'5' then Just ([false;true; false;true ])
+  else if c = #'6' then Just ([false;true; true; false])
+  else if c = #'7' then Just ([false;true; true; true ])
+  else if c = #'8' then Just ([true; false;false;false])
+  else if c = #'9' then Just ([true; false;false;true ])
+  else if c = #'A' then Just ([true; false;true; false])
+  else if c = #'a' then Just ([true; false;true; false])
+  else if c = #'B' then Just ([true; false;true; true ])
+  else if c = #'b' then Just ([true; false;true; true ])
+  else if c = #'C' then Just ([true; true; false;false])
+  else if c = #'c' then Just ([true; true; false;false])
+  else if c = #'D' then Just ([true; true; false;true ])
+  else if c = #'d' then Just ([true; true; false;true ])
+  else if c = #'E' then Just ([true; true; true; false])
+  else if c = #'e' then Just ([true; true; true; false])
+  else if c = #'F' then Just ([true; true; true; true ])
+  else if c = #'f' then Just ([true; true; true; true ])
+  else Nothing
+
+let hexstring_to_bools s =
+  match (toCharList s) with
+    | z :: x :: hs ->
+       let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
+       Maybe.map List.concat (just_list (List.map hexchar_to_bool_list str))
+    | _ -> Nothing
+  end
+
+val hex_slice : forall 'rv 'e. string -> integer -> integer -> monad 'rv (list bitU) 'e
+let hex_slice v len lo =
+  match hexstring_to_bools v with
+    | Just bs ->
+       let hi = len + lo - 1 in
+       let bs = ext_list false (len + lo) bs in
+       return (of_bools (subrange_list false bs hi lo))
+    | Nothing -> Fail "hex_slice"
+  end
+
+let internal_pick vs = return (head vs)
+
+(* Use constants for undefined values for now *)
+let undefined_string () = return ""
+let undefined_unit () = return ()
+let undefined_int () = return (0:ii)
+val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e
+let undefined_vector len u = return (repeat [u] len)
+val undefined_bitvector : forall 'rv 'e. integer -> monad 'rv (list bitU) 'e
+let undefined_bitvector len = return (of_bools (repeat [false] len))
+val undefined_bits : forall 'rv 'e. integer -> monad 'rv (list bitU) 'e
+let undefined_bits = undefined_bitvector
+let undefined_bit () = return B0
+let undefined_real () = return (realFromFrac 0 1)
+let undefined_range i j = return i
+let undefined_atom i = return i
+let undefined_nat () = return (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 =
+  read_mem Read_plain address size
diff --git a/aarch64/aarch64_extras_embed_sequential.lem b/aarch64/aarch64_extras_embed_sequential.lem
deleted file mode 100644
index 4f9e0fe3..00000000
--- a/aarch64/aarch64_extras_embed_sequential.lem
+++ /dev/null
@@ -1,131 +0,0 @@
-open import Pervasives_extra
-open import Sail_impl_base
-open import Sail_values
-open import Sail_operators_bitlists
-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 : list bitU -> integer
-let uint = unsigned
-val sint : list bitU -> integer
-let sint = signed
-
-val slice : list bitU -> integer -> integer -> list bitU
-let slice v lo len =
-  subrange_vec_dec v (lo + len - 1) lo
-
-val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
-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 : integer -> integer -> integer -> list bitU
-let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
-
-val set_slice_int : integer -> integer -> integer -> list bitU -> 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 : string -> integer -> integer -> list bitU
-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 : integer -> list bitU
-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 false Read_plain address size*)
-  undefined_bitvector (8 * size)
diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index 8af9ee5d..0a6bab11 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -3,7 +3,7 @@ open import Sail_instr_kinds
 open import Sail_values
 open import Sail_operators_mwords
 open import Prompt_monad
-open import State
+open import Prompt
 
 type ty512
 instance (Size ty512) let size = 512 end
@@ -26,11 +26,6 @@ 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
@@ -42,28 +37,28 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) 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
+  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_bits (get_slice_int_bl len n lo)
+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 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 bs = bool_list_of_int 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 ext_bs hi lo (bitlistFromWord v))
 
-let ext_slice signed v i j =
+(*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
+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
@@ -71,61 +66,66 @@ 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 =
+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 ])
+  else if c = #'2' then Just ([false;false;true; false])
+  else if c = #'3' then Just ([false;false;true; true ])
+  else if c = #'4' then Just ([false;true; false;false])
+  else if c = #'5' then Just ([false;true; false;true ])
+  else if c = #'6' then Just ([false;true; true; false])
+  else if c = #'7' then Just ([false;true; true; true ])
+  else if c = #'8' then Just ([true; false;false;false])
+  else if c = #'9' then Just ([true; false;false;true ])
+  else if c = #'A' then Just ([true; false;true; false])
+  else if c = #'a' then Just ([true; false;true; false])
+  else if c = #'B' then Just ([true; false;true; true ])
+  else if c = #'b' then Just ([true; false;true; true ])
+  else if c = #'C' then Just ([true; true; false;false])
+  else if c = #'c' then Just ([true; true; false;false])
+  else if c = #'D' then Just ([true; true; false;true ])
+  else if c = #'d' then Just ([true; true; false;true ])
+  else if c = #'E' then Just ([true; true; true; false])
+  else if c = #'e' then Just ([true; true; true; false])
+  else if c = #'F' then Just ([true; true; true; true ])
+  else if c = #'f' then Just ([true; true; true; true ])
+  else Nothing
+
+let hexstring_to_bools 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"
+    | z :: x :: hs ->
+       let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
+       Maybe.map List.concat (just_list (List.map hexchar_to_bool_list str))
+    | _ -> Nothing
   end
 
-val hex_slice : forall 'n. Size 'n => string -> integer -> integer -> mword 'n
+val hex_slice : forall 'rv 'n 'e. Size 'n => string -> integer -> integer -> monad 'rv (mword 'n) 'e
 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)
+  match hexstring_to_bools v with
+    | Just bs ->
+       let hi = len + lo - 1 in
+       let bs = ext_list false (len + lo) bs in
+       return (of_bools (subrange_list false bs hi lo))
+    | Nothing -> Fail "hex_slice"
+  end
+
+let internal_pick vs = return (head vs)
+
+(* Use constants for undefined values for now *)
+let undefined_string () = return ""
+let undefined_unit () = return ()
+let undefined_int () = return (0:ii)
+val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e
+let undefined_vector len u = return (repeat [u] len)
+val undefined_bitvector : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e
+let undefined_bitvector len = return (of_bools (repeat [false] len))
+val undefined_bits : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e
+let undefined_bits = undefined_bitvector
+let undefined_bit () = return B0
+let undefined_real () = return (realFromFrac 0 1)
+let undefined_range i j = return i
+let undefined_atom i = return i
+let undefined_nat () = return (0:ii)
 
 let write_ram addrsize size hexRAM address value =
   write_mem_ea Write_plain address size >>
diff --git a/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector.sail b/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector.sail
index 2960240d..202f69ac 100644
--- a/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector.sail
+++ b/aarch64/mono/demo/aarch64_no_vector/aarch64_no_vector.sail
@@ -2546,7 +2546,7 @@ function PACInvSub Tinput = {
   return(Toutput)
 }
 
-val ComputePAC : (bits(64), bits(64), bits(64), bits(64)) -> bits(64) effect {rreg, undef, wreg}
+val ComputePAC : (bits(64), bits(64), bits(64), bits(64)) -> bits(64) effect {rreg, undef, wreg, escape}
 
 function ComputePAC (data, modifier, key0, key1) = {
   workingval : bits(64) = undefined;
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index 21448bc1..44dc4224 100644
--- a/aarch64/no_vector/spec.sail
+++ b/aarch64/no_vector/spec.sail
@@ -2544,7 +2544,7 @@ function PACInvSub Tinput = {
   return(Toutput)
 }
 
-val ComputePAC : (bits(64), bits(64), bits(64), bits(64)) -> bits(64) effect {rreg, undef, wreg}
+val ComputePAC : (bits(64), bits(64), bits(64), bits(64)) -> bits(64) effect {escape, rreg, undef, wreg}
 
 function ComputePAC (data, modifier, key0, key1) = {
   workingval : bits(64) = undefined;
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index d9ba1cde..097dbf47 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -142,7 +142,7 @@ val UInt = {
 
 val SInt = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
-val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
+val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) effect {escape}
 
 val __SetSlice_bits = "set_slice" : forall 'n 'm.
   (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)